nna4b4nsq

Description: Strengthening of Fermat's last theorem for exponent 4, where the sum is only assumed to be a square. (Contributed by SN, 23-Aug-2024)

	Ref	Expression
Hypotheses	nna4b4nsq.a	$⊢ φ \to A \in ℕ$
	nna4b4nsq.b	$⊢ φ \to B \in ℕ$
	nna4b4nsq.c	$⊢ φ \to C \in ℕ$
Assertion	nna4b4nsq	$⊢ φ \to A^{4} + B^{4} \neq C^{2}$

Proof

Step	Hyp	Ref	Expression
1		nna4b4nsq.a	$⊢ φ \to A \in ℕ$
2		nna4b4nsq.b	$⊢ φ \to B \in ℕ$
3		nna4b4nsq.c	$⊢ φ \to C \in ℕ$
4		oveq1	$⊢ a = A \to a^{4} = A^{4}$
5	4	oveq1d	$⊢ a = A \to a^{4} + b^{4} = A^{4} + b^{4}$
6	5	eqeq1d	$⊢ a = A \to (a^{4} + b^{4} = c^{2} \leftrightarrow A^{4} + b^{4} = c^{2})$
7		oveq1	$⊢ b = B \to b^{4} = B^{4}$
8	7	oveq2d	$⊢ b = B \to A^{4} + b^{4} = A^{4} + B^{4}$
9	8	eqeq1d	$⊢ b = B \to (A^{4} + b^{4} = c^{2} \leftrightarrow A^{4} + B^{4} = c^{2})$
10	1	ad2antrr	$⊢ ((φ \land c \in ℕ) \land A^{4} + B^{4} = c^{2}) \to A \in ℕ$
11	2	ad2antrr	$⊢ ((φ \land c \in ℕ) \land A^{4} + B^{4} = c^{2}) \to B \in ℕ$
12		simpr	$⊢ ((φ \land c \in ℕ) \land A^{4} + B^{4} = c^{2}) \to A^{4} + B^{4} = c^{2}$
13	6 9 10 11 12	2rspcedvdw	$⊢ ((φ \land c \in ℕ) \land A^{4} + B^{4} = c^{2}) \to \exists a \in ℕ \exists b \in ℕ a^{4} + b^{4} = c^{2}$
14	13	ex	$⊢ (φ \land c \in ℕ) \to (A^{4} + B^{4} = c^{2} \to \exists a \in ℕ \exists b \in ℕ a^{4} + b^{4} = c^{2})$
15	14	ss2rabdv	$⊢ φ \to \{c \in ℕ \| A^{4} + B^{4} = c^{2}\} \subseteq \{c \in ℕ \| \exists a \in ℕ \exists b \in ℕ a^{4} + b^{4} = c^{2}\}$
16		oveq1	$⊢ f = i \to f^{2} = i^{2}$
17	16	eqeq2d	$⊢ f = i \to (g^{4} + h^{4} = f^{2} \leftrightarrow g^{4} + h^{4} = i^{2})$
18	17	anbi2d	$⊢ f = i \to ((g \gcd h = 1 \land g^{4} + h^{4} = f^{2}) \leftrightarrow (g \gcd h = 1 \land g^{4} + h^{4} = i^{2}))$
19	18	anbi2d	$⊢ f = i \to ((\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = f^{2})) \leftrightarrow (\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = i^{2})))$
20	19	2rexbidv	$⊢ f = i \to (\exists g \in ℕ \exists h \in ℕ (\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = f^{2})) \leftrightarrow \exists g \in ℕ \exists h \in ℕ (\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = i^{2})))$
21		oveq1	$⊢ f = l \to f^{2} = l^{2}$
22	21	eqeq2d	$⊢ f = l \to (g^{4} + h^{4} = f^{2} \leftrightarrow g^{4} + h^{4} = l^{2})$
23	22	anbi2d	$⊢ f = l \to ((g \gcd h = 1 \land g^{4} + h^{4} = f^{2}) \leftrightarrow (g \gcd h = 1 \land g^{4} + h^{4} = l^{2}))$
24	23	anbi2d	$⊢ f = l \to ((\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = f^{2})) \leftrightarrow (\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = l^{2})))$
25	24	2rexbidv	$⊢ f = l \to (\exists g \in ℕ \exists h \in ℕ (\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = f^{2})) \leftrightarrow \exists g \in ℕ \exists h \in ℕ (\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = l^{2})))$
26		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
27	26	eqimssi	$⊢ ℕ \subseteq ℤ_{\geq 1}$
28	27	a1i	$⊢ φ \to ℕ \subseteq ℤ_{\geq 1}$
29		breq2	$⊢ g = j \to (2 ∥ g \leftrightarrow 2 ∥ j)$
30	29	notbid	$⊢ g = j \to (\neg 2 ∥ g \leftrightarrow \neg 2 ∥ j)$
31		oveq1	$⊢ g = j \to g \gcd h = j \gcd h$
32	31	eqeq1d	$⊢ g = j \to (g \gcd h = 1 \leftrightarrow j \gcd h = 1)$
33		oveq1	$⊢ g = j \to g^{4} = j^{4}$
34	33	oveq1d	$⊢ g = j \to g^{4} + h^{4} = j^{4} + h^{4}$
35	34	eqeq1d	$⊢ g = j \to (g^{4} + h^{4} = i^{2} \leftrightarrow j^{4} + h^{4} = i^{2})$
36	32 35	anbi12d	$⊢ g = j \to ((g \gcd h = 1 \land g^{4} + h^{4} = i^{2}) \leftrightarrow (j \gcd h = 1 \land j^{4} + h^{4} = i^{2}))$
37	30 36	anbi12d	$⊢ g = j \to ((\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = i^{2})) \leftrightarrow (\neg 2 ∥ j \land (j \gcd h = 1 \land j^{4} + h^{4} = i^{2})))$
38		oveq2	$⊢ h = k \to j \gcd h = j \gcd k$
39	38	eqeq1d	$⊢ h = k \to (j \gcd h = 1 \leftrightarrow j \gcd k = 1)$
40		oveq1	$⊢ h = k \to h^{4} = k^{4}$
41	40	oveq2d	$⊢ h = k \to j^{4} + h^{4} = j^{4} + k^{4}$
42	41	eqeq1d	$⊢ h = k \to (j^{4} + h^{4} = i^{2} \leftrightarrow j^{4} + k^{4} = i^{2})$
43	39 42	anbi12d	$⊢ h = k \to ((j \gcd h = 1 \land j^{4} + h^{4} = i^{2}) \leftrightarrow (j \gcd k = 1 \land j^{4} + k^{4} = i^{2}))$
44	43	anbi2d	$⊢ h = k \to ((\neg 2 ∥ j \land (j \gcd h = 1 \land j^{4} + h^{4} = i^{2})) \leftrightarrow (\neg 2 ∥ j \land (j \gcd k = 1 \land j^{4} + k^{4} = i^{2})))$
45	37 44	cbvrex2vw	$⊢ \exists g \in ℕ \exists h \in ℕ (\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = i^{2})) \leftrightarrow \exists j \in ℕ \exists k \in ℕ (\neg 2 ∥ j \land (j \gcd k = 1 \land j^{4} + k^{4} = i^{2}))$
46		simplrl	$⊢ (((φ \land i \in ℕ) \land (j \in ℕ \land k \in ℕ)) \land (\neg 2 ∥ j \land (j \gcd k = 1 \land j^{4} + k^{4} = i^{2}))) \to j \in ℕ$
47		simplrr	$⊢ (((φ \land i \in ℕ) \land (j \in ℕ \land k \in ℕ)) \land (\neg 2 ∥ j \land (j \gcd k = 1 \land j^{4} + k^{4} = i^{2}))) \to k \in ℕ$
48		simpllr	$⊢ (((φ \land i \in ℕ) \land (j \in ℕ \land k \in ℕ)) \land (\neg 2 ∥ j \land (j \gcd k = 1 \land j^{4} + k^{4} = i^{2}))) \to i \in ℕ$
49		simprl	$⊢ (((φ \land i \in ℕ) \land (j \in ℕ \land k \in ℕ)) \land (\neg 2 ∥ j \land (j \gcd k = 1 \land j^{4} + k^{4} = i^{2}))) \to \neg 2 ∥ j$
50		simprrl	$⊢ (((φ \land i \in ℕ) \land (j \in ℕ \land k \in ℕ)) \land (\neg 2 ∥ j \land (j \gcd k = 1 \land j^{4} + k^{4} = i^{2}))) \to j \gcd k = 1$
51		simprrr	$⊢ (((φ \land i \in ℕ) \land (j \in ℕ \land k \in ℕ)) \land (\neg 2 ∥ j \land (j \gcd k = 1 \land j^{4} + k^{4} = i^{2}))) \to j^{4} + k^{4} = i^{2}$
52	46 47 48 49 50 51	flt4lem7	$⊢ (((φ \land i \in ℕ) \land (j \in ℕ \land k \in ℕ)) \land (\neg 2 ∥ j \land (j \gcd k = 1 \land j^{4} + k^{4} = i^{2}))) \to \exists l \in ℕ (\exists g \in ℕ \exists h \in ℕ (\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = l^{2})) \land l < i)$
53	52	ex	$⊢ ((φ \land i \in ℕ) \land (j \in ℕ \land k \in ℕ)) \to ((\neg 2 ∥ j \land (j \gcd k = 1 \land j^{4} + k^{4} = i^{2})) \to \exists l \in ℕ (\exists g \in ℕ \exists h \in ℕ (\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = l^{2})) \land l < i))$
54	53	rexlimdvva	$⊢ (φ \land i \in ℕ) \to (\exists j \in ℕ \exists k \in ℕ (\neg 2 ∥ j \land (j \gcd k = 1 \land j^{4} + k^{4} = i^{2})) \to \exists l \in ℕ (\exists g \in ℕ \exists h \in ℕ (\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = l^{2})) \land l < i))$
55	45 54	syl5bi	$⊢ (φ \land i \in ℕ) \to (\exists g \in ℕ \exists h \in ℕ (\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = i^{2})) \to \exists l \in ℕ (\exists g \in ℕ \exists h \in ℕ (\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = l^{2})) \land l < i))$
56	55	impr	$⊢ (φ \land (i \in ℕ \land \exists g \in ℕ \exists h \in ℕ (\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = i^{2})))) \to \exists l \in ℕ (\exists g \in ℕ \exists h \in ℕ (\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = l^{2})) \land l < i)$
57	20 25 28 56	infdesc	$⊢ φ \to \{f \in ℕ \| \exists g \in ℕ \exists h \in ℕ (\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = f^{2}))\} = \emptyset$
58		breq2	$⊢ g = d \to (2 ∥ g \leftrightarrow 2 ∥ d)$
59	58	notbid	$⊢ g = d \to (\neg 2 ∥ g \leftrightarrow \neg 2 ∥ d)$
60		oveq1	$⊢ g = d \to g \gcd h = d \gcd h$
61	60	eqeq1d	$⊢ g = d \to (g \gcd h = 1 \leftrightarrow d \gcd h = 1)$
62		oveq1	$⊢ g = d \to g^{4} = d^{4}$
63	62	oveq1d	$⊢ g = d \to g^{4} + h^{4} = d^{4} + h^{4}$
64	63	eqeq1d	$⊢ g = d \to (g^{4} + h^{4} = f^{2} \leftrightarrow d^{4} + h^{4} = f^{2})$
65	61 64	anbi12d	$⊢ g = d \to ((g \gcd h = 1 \land g^{4} + h^{4} = f^{2}) \leftrightarrow (d \gcd h = 1 \land d^{4} + h^{4} = f^{2}))$
66	59 65	anbi12d	$⊢ g = d \to ((\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = f^{2})) \leftrightarrow (\neg 2 ∥ d \land (d \gcd h = 1 \land d^{4} + h^{4} = f^{2})))$
67		oveq2	$⊢ h = e \to d \gcd h = d \gcd e$
68	67	eqeq1d	$⊢ h = e \to (d \gcd h = 1 \leftrightarrow d \gcd e = 1)$
69		oveq1	$⊢ h = e \to h^{4} = e^{4}$
70	69	oveq2d	$⊢ h = e \to d^{4} + h^{4} = d^{4} + e^{4}$
71	70	eqeq1d	$⊢ h = e \to (d^{4} + h^{4} = f^{2} \leftrightarrow d^{4} + e^{4} = f^{2})$
72	68 71	anbi12d	$⊢ h = e \to ((d \gcd h = 1 \land d^{4} + h^{4} = f^{2}) \leftrightarrow (d \gcd e = 1 \land d^{4} + e^{4} = f^{2}))$
73	72	anbi2d	$⊢ h = e \to ((\neg 2 ∥ d \land (d \gcd h = 1 \land d^{4} + h^{4} = f^{2})) \leftrightarrow (\neg 2 ∥ d \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})))$
74		simprl	$⊢ ((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \to d \in ℕ$
75	74	ad2antrr	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land \neg 2 ∥ d) \to d \in ℕ$
76		simprr	$⊢ ((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \to e \in ℕ$
77	76	ad2antrr	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land \neg 2 ∥ d) \to e \in ℕ$
78		simpr	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land \neg 2 ∥ d) \to \neg 2 ∥ d$
79		simplr	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land \neg 2 ∥ d) \to (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})$
80	78 79	jca	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land \neg 2 ∥ d) \to (\neg 2 ∥ d \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2}))$
81	66 73 75 77 80	2rspcedvdw	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land \neg 2 ∥ d) \to \exists g \in ℕ \exists h \in ℕ (\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = f^{2}))$
82		breq2	$⊢ g = e \to (2 ∥ g \leftrightarrow 2 ∥ e)$
83	82	notbid	$⊢ g = e \to (\neg 2 ∥ g \leftrightarrow \neg 2 ∥ e)$
84		oveq1	$⊢ g = e \to g \gcd h = e \gcd h$
85	84	eqeq1d	$⊢ g = e \to (g \gcd h = 1 \leftrightarrow e \gcd h = 1)$
86		oveq1	$⊢ g = e \to g^{4} = e^{4}$
87	86	oveq1d	$⊢ g = e \to g^{4} + h^{4} = e^{4} + h^{4}$
88	87	eqeq1d	$⊢ g = e \to (g^{4} + h^{4} = f^{2} \leftrightarrow e^{4} + h^{4} = f^{2})$
89	85 88	anbi12d	$⊢ g = e \to ((g \gcd h = 1 \land g^{4} + h^{4} = f^{2}) \leftrightarrow (e \gcd h = 1 \land e^{4} + h^{4} = f^{2}))$
90	83 89	anbi12d	$⊢ g = e \to ((\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = f^{2})) \leftrightarrow (\neg 2 ∥ e \land (e \gcd h = 1 \land e^{4} + h^{4} = f^{2})))$
91		oveq2	$⊢ h = d \to e \gcd h = e \gcd d$
92	91	eqeq1d	$⊢ h = d \to (e \gcd h = 1 \leftrightarrow e \gcd d = 1)$
93		oveq1	$⊢ h = d \to h^{4} = d^{4}$
94	93	oveq2d	$⊢ h = d \to e^{4} + h^{4} = e^{4} + d^{4}$
95	94	eqeq1d	$⊢ h = d \to (e^{4} + h^{4} = f^{2} \leftrightarrow e^{4} + d^{4} = f^{2})$
96	92 95	anbi12d	$⊢ h = d \to ((e \gcd h = 1 \land e^{4} + h^{4} = f^{2}) \leftrightarrow (e \gcd d = 1 \land e^{4} + d^{4} = f^{2}))$
97	96	anbi2d	$⊢ h = d \to ((\neg 2 ∥ e \land (e \gcd h = 1 \land e^{4} + h^{4} = f^{2})) \leftrightarrow (\neg 2 ∥ e \land (e \gcd d = 1 \land e^{4} + d^{4} = f^{2})))$
98	76	ad2antrr	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land \neg 2 ∥ e) \to e \in ℕ$
99	74	ad2antrr	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land \neg 2 ∥ e) \to d \in ℕ$
100		simpr	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land \neg 2 ∥ e) \to \neg 2 ∥ e$
101	98	nnzd	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land \neg 2 ∥ e) \to e \in ℤ$
102	99	nnzd	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land \neg 2 ∥ e) \to d \in ℤ$
103	101 102	gcdcomd	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land \neg 2 ∥ e) \to e \gcd d = d \gcd e$
104		simplrl	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land \neg 2 ∥ e) \to d \gcd e = 1$
105	103 104	eqtrd	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land \neg 2 ∥ e) \to e \gcd d = 1$
106		4nn0	$⊢ 4 \in ℕ_{0}$
107	106	a1i	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land \neg 2 ∥ e) \to 4 \in ℕ_{0}$
108	98 107	nnexpcld	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land \neg 2 ∥ e) \to e^{4} \in ℕ$
109	108	nncnd	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land \neg 2 ∥ e) \to e^{4} \in ℂ$
110	99 107	nnexpcld	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land \neg 2 ∥ e) \to d^{4} \in ℕ$
111	110	nncnd	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land \neg 2 ∥ e) \to d^{4} \in ℂ$
112	109 111	addcomd	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land \neg 2 ∥ e) \to e^{4} + d^{4} = d^{4} + e^{4}$
113		simplrr	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land \neg 2 ∥ e) \to d^{4} + e^{4} = f^{2}$
114	112 113	eqtrd	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land \neg 2 ∥ e) \to e^{4} + d^{4} = f^{2}$
115	100 105 114	jca32	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land \neg 2 ∥ e) \to (\neg 2 ∥ e \land (e \gcd d = 1 \land e^{4} + d^{4} = f^{2}))$
116	90 97 98 99 115	2rspcedvdw	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land \neg 2 ∥ e) \to \exists g \in ℕ \exists h \in ℕ (\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = f^{2}))$
117	74	ad2antrr	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land 2 ∥ d) \to d \in ℕ$
118	117	nnsqcld	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land 2 ∥ d) \to d^{2} \in ℕ$
119	76	ad2antrr	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land 2 ∥ d) \to e \in ℕ$
120	119	nnsqcld	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land 2 ∥ d) \to e^{2} \in ℕ$
121		simp-4r	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land 2 ∥ d) \to f \in ℕ$
122		2z	$⊢ 2 \in ℤ$
123		simplrl	$⊢ (((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \to d \in ℕ$
124	123	nnzd	$⊢ (((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \to d \in ℤ$
125		2nn	$⊢ 2 \in ℕ$
126	125	a1i	$⊢ (((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \to 2 \in ℕ$
127		dvdsexp2im	$⊢ (2 \in ℤ \land d \in ℤ \land 2 \in ℕ) \to (2 ∥ d \to 2 ∥ d^{2})$
128	122 124 126 127	mp3an2i	$⊢ (((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \to (2 ∥ d \to 2 ∥ d^{2})$
129	128	imp	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land 2 ∥ d) \to 2 ∥ d^{2}$
130		2nn0	$⊢ 2 \in ℕ_{0}$
131	130	a1i	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land 2 ∥ d) \to 2 \in ℕ_{0}$
132	117	nncnd	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land 2 ∥ d) \to d \in ℂ$
133	132	flt4lem	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land 2 ∥ d) \to d^{4} = {(d^{2})}^{2}$
134	119	nncnd	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land 2 ∥ d) \to e \in ℂ$
135	134	flt4lem	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land 2 ∥ d) \to e^{4} = {(e^{2})}^{2}$
136	133 135	oveq12d	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land 2 ∥ d) \to d^{4} + e^{4} = {(d^{2})}^{2} + {(e^{2})}^{2}$
137		simplrr	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land 2 ∥ d) \to d^{4} + e^{4} = f^{2}$
138	136 137	eqtr3d	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land 2 ∥ d) \to {(d^{2})}^{2} + {(e^{2})}^{2} = f^{2}$
139		simplrl	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land 2 ∥ d) \to d \gcd e = 1$
140	125	a1i	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land 2 ∥ d) \to 2 \in ℕ$
141		rppwr	$⊢ (d \in ℕ \land e \in ℕ \land 2 \in ℕ) \to (d \gcd e = 1 \to d^{2} \gcd e^{2} = 1)$
142	117 119 140 141	syl3anc	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land 2 ∥ d) \to (d \gcd e = 1 \to d^{2} \gcd e^{2} = 1)$
143	139 142	mpd	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land 2 ∥ d) \to d^{2} \gcd e^{2} = 1$
144	118 120 121 131 138 143	fltaccoprm	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land 2 ∥ d) \to d^{2} \gcd f = 1$
145	118 120 121 129 144 138	flt4lem2	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land 2 ∥ d) \to \neg 2 ∥ e^{2}$
146	119	nnzd	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land 2 ∥ d) \to e \in ℤ$
147		dvdsexp2im	$⊢ (2 \in ℤ \land e \in ℤ \land 2 \in ℕ) \to (2 ∥ e \to 2 ∥ e^{2})$
148	122 146 140 147	mp3an2i	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land 2 ∥ d) \to (2 ∥ e \to 2 ∥ e^{2})$
149	145 148	mtod	$⊢ ((((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \land 2 ∥ d) \to \neg 2 ∥ e$
150	149	ex	$⊢ (((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \to (2 ∥ d \to \neg 2 ∥ e)$
151		imor	$⊢ (2 ∥ d \to \neg 2 ∥ e) \leftrightarrow (\neg 2 ∥ d \lor \neg 2 ∥ e)$
152	150 151	sylib	$⊢ (((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \to (\neg 2 ∥ d \lor \neg 2 ∥ e)$
153	81 116 152	mpjaodan	$⊢ (((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \to \exists g \in ℕ \exists h \in ℕ (\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = f^{2}))$
154	153	ex	$⊢ ((φ \land f \in ℕ) \land (d \in ℕ \land e \in ℕ)) \to ((d \gcd e = 1 \land d^{4} + e^{4} = f^{2}) \to \exists g \in ℕ \exists h \in ℕ (\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = f^{2})))$
155	154	rexlimdvva	$⊢ (φ \land f \in ℕ) \to (\exists d \in ℕ \exists e \in ℕ (d \gcd e = 1 \land d^{4} + e^{4} = f^{2}) \to \exists g \in ℕ \exists h \in ℕ (\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = f^{2})))$
156	155	reximdva	$⊢ φ \to (\exists f \in ℕ \exists d \in ℕ \exists e \in ℕ (d \gcd e = 1 \land d^{4} + e^{4} = f^{2}) \to \exists f \in ℕ \exists g \in ℕ \exists h \in ℕ (\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = f^{2})))$
157	156	con3d	$⊢ φ \to (\neg \exists f \in ℕ \exists g \in ℕ \exists h \in ℕ (\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = f^{2})) \to \neg \exists f \in ℕ \exists d \in ℕ \exists e \in ℕ (d \gcd e = 1 \land d^{4} + e^{4} = f^{2}))$
158		ralnex	$⊢ \forall f \in ℕ \neg \exists g \in ℕ \exists h \in ℕ (\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = f^{2})) \leftrightarrow \neg \exists f \in ℕ \exists g \in ℕ \exists h \in ℕ (\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = f^{2}))$
159		ralnex	$⊢ \forall f \in ℕ \neg \exists d \in ℕ \exists e \in ℕ (d \gcd e = 1 \land d^{4} + e^{4} = f^{2}) \leftrightarrow \neg \exists f \in ℕ \exists d \in ℕ \exists e \in ℕ (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})$
160	157 158 159	3imtr4g	$⊢ φ \to (\forall f \in ℕ \neg \exists g \in ℕ \exists h \in ℕ (\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = f^{2})) \to \forall f \in ℕ \neg \exists d \in ℕ \exists e \in ℕ (d \gcd e = 1 \land d^{4} + e^{4} = f^{2}))$
161		rabeq0	$⊢ \{f \in ℕ \| \exists g \in ℕ \exists h \in ℕ (\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = f^{2}))\} = \emptyset \leftrightarrow \forall f \in ℕ \neg \exists g \in ℕ \exists h \in ℕ (\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = f^{2}))$
162		rabeq0	$⊢ \{f \in ℕ \| \exists d \in ℕ \exists e \in ℕ (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})\} = \emptyset \leftrightarrow \forall f \in ℕ \neg \exists d \in ℕ \exists e \in ℕ (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})$
163	160 161 162	3imtr4g	$⊢ φ \to (\{f \in ℕ \| \exists g \in ℕ \exists h \in ℕ (\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = f^{2}))\} = \emptyset \to \{f \in ℕ \| \exists d \in ℕ \exists e \in ℕ (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})\} = \emptyset)$
164	57 163	mpd	$⊢ φ \to \{f \in ℕ \| \exists d \in ℕ \exists e \in ℕ (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})\} = \emptyset$
165		oveq1	$⊢ f = \frac{c}{{(a \gcd b)}^{2}} \to f^{2} = {(\frac{c}{{(a \gcd b)}^{2}})}^{2}$
166	165	eqeq2d	$⊢ f = \frac{c}{{(a \gcd b)}^{2}} \to (d^{4} + e^{4} = f^{2} \leftrightarrow d^{4} + e^{4} = {(\frac{c}{{(a \gcd b)}^{2}})}^{2})$
167	166	anbi2d	$⊢ f = \frac{c}{{(a \gcd b)}^{2}} \to ((d \gcd e = 1 \land d^{4} + e^{4} = f^{2}) \leftrightarrow (d \gcd e = 1 \land d^{4} + e^{4} = {(\frac{c}{{(a \gcd b)}^{2}})}^{2}))$
168		oveq1	$⊢ d = \frac{a}{a \gcd b} \to d \gcd e = (\frac{a}{a \gcd b}) \gcd e$
169	168	eqeq1d	$⊢ d = \frac{a}{a \gcd b} \to (d \gcd e = 1 \leftrightarrow (\frac{a}{a \gcd b}) \gcd e = 1)$
170		oveq1	$⊢ d = \frac{a}{a \gcd b} \to d^{4} = {(\frac{a}{a \gcd b})}^{4}$
171	170	oveq1d	$⊢ d = \frac{a}{a \gcd b} \to d^{4} + e^{4} = {(\frac{a}{a \gcd b})}^{4} + e^{4}$
172	171	eqeq1d	$⊢ d = \frac{a}{a \gcd b} \to (d^{4} + e^{4} = {(\frac{c}{{(a \gcd b)}^{2}})}^{2} \leftrightarrow {(\frac{a}{a \gcd b})}^{4} + e^{4} = {(\frac{c}{{(a \gcd b)}^{2}})}^{2})$
173	169 172	anbi12d	$⊢ d = \frac{a}{a \gcd b} \to ((d \gcd e = 1 \land d^{4} + e^{4} = {(\frac{c}{{(a \gcd b)}^{2}})}^{2}) \leftrightarrow ((\frac{a}{a \gcd b}) \gcd e = 1 \land {(\frac{a}{a \gcd b})}^{4} + e^{4} = {(\frac{c}{{(a \gcd b)}^{2}})}^{2}))$
174		oveq2	$⊢ e = \frac{b}{a \gcd b} \to (\frac{a}{a \gcd b}) \gcd e = (\frac{a}{a \gcd b}) \gcd (\frac{b}{a \gcd b})$
175	174	eqeq1d	$⊢ e = \frac{b}{a \gcd b} \to ((\frac{a}{a \gcd b}) \gcd e = 1 \leftrightarrow (\frac{a}{a \gcd b}) \gcd (\frac{b}{a \gcd b}) = 1)$
176		oveq1	$⊢ e = \frac{b}{a \gcd b} \to e^{4} = {(\frac{b}{a \gcd b})}^{4}$
177	176	oveq2d	$⊢ e = \frac{b}{a \gcd b} \to {(\frac{a}{a \gcd b})}^{4} + e^{4} = {(\frac{a}{a \gcd b})}^{4} + {(\frac{b}{a \gcd b})}^{4}$
178	177	eqeq1d	$⊢ e = \frac{b}{a \gcd b} \to ({(\frac{a}{a \gcd b})}^{4} + e^{4} = {(\frac{c}{{(a \gcd b)}^{2}})}^{2} \leftrightarrow {(\frac{a}{a \gcd b})}^{4} + {(\frac{b}{a \gcd b})}^{4} = {(\frac{c}{{(a \gcd b)}^{2}})}^{2})$
179	175 178	anbi12d	$⊢ e = \frac{b}{a \gcd b} \to (((\frac{a}{a \gcd b}) \gcd e = 1 \land {(\frac{a}{a \gcd b})}^{4} + e^{4} = {(\frac{c}{{(a \gcd b)}^{2}})}^{2}) \leftrightarrow ((\frac{a}{a \gcd b}) \gcd (\frac{b}{a \gcd b}) = 1 \land {(\frac{a}{a \gcd b})}^{4} + {(\frac{b}{a \gcd b})}^{4} = {(\frac{c}{{(a \gcd b)}^{2}})}^{2}))$
180		simplrr	$⊢ ((φ \land (c \in ℕ \land a \in ℕ)) \land (b \in ℕ \land a^{4} + b^{4} = c^{2})) \to a \in ℕ$
181		simprl	$⊢ ((φ \land (c \in ℕ \land a \in ℕ)) \land (b \in ℕ \land a^{4} + b^{4} = c^{2})) \to b \in ℕ$
182		simplrl	$⊢ ((φ \land (c \in ℕ \land a \in ℕ)) \land (b \in ℕ \land a^{4} + b^{4} = c^{2})) \to c \in ℕ$
183		simprr	$⊢ ((φ \land (c \in ℕ \land a \in ℕ)) \land (b \in ℕ \land a^{4} + b^{4} = c^{2})) \to a^{4} + b^{4} = c^{2}$
184	180 181 182 183	flt4lem6	$⊢ ((φ \land (c \in ℕ \land a \in ℕ)) \land (b \in ℕ \land a^{4} + b^{4} = c^{2})) \to ((\frac{a}{a \gcd b} \in ℕ \land \frac{b}{a \gcd b} \in ℕ \land \frac{c}{{(a \gcd b)}^{2}} \in ℕ) \land {(\frac{a}{a \gcd b})}^{4} + {(\frac{b}{a \gcd b})}^{4} = {(\frac{c}{{(a \gcd b)}^{2}})}^{2})$
185	184	simpld	$⊢ ((φ \land (c \in ℕ \land a \in ℕ)) \land (b \in ℕ \land a^{4} + b^{4} = c^{2})) \to (\frac{a}{a \gcd b} \in ℕ \land \frac{b}{a \gcd b} \in ℕ \land \frac{c}{{(a \gcd b)}^{2}} \in ℕ)$
186	185	simp3d	$⊢ ((φ \land (c \in ℕ \land a \in ℕ)) \land (b \in ℕ \land a^{4} + b^{4} = c^{2})) \to \frac{c}{{(a \gcd b)}^{2}} \in ℕ$
187	185	simp1d	$⊢ ((φ \land (c \in ℕ \land a \in ℕ)) \land (b \in ℕ \land a^{4} + b^{4} = c^{2})) \to \frac{a}{a \gcd b} \in ℕ$
188	185	simp2d	$⊢ ((φ \land (c \in ℕ \land a \in ℕ)) \land (b \in ℕ \land a^{4} + b^{4} = c^{2})) \to \frac{b}{a \gcd b} \in ℕ$
189	180	nnzd	$⊢ ((φ \land (c \in ℕ \land a \in ℕ)) \land (b \in ℕ \land a^{4} + b^{4} = c^{2})) \to a \in ℤ$
190	181	nnzd	$⊢ ((φ \land (c \in ℕ \land a \in ℕ)) \land (b \in ℕ \land a^{4} + b^{4} = c^{2})) \to b \in ℤ$
191	181	nnne0d	$⊢ ((φ \land (c \in ℕ \land a \in ℕ)) \land (b \in ℕ \land a^{4} + b^{4} = c^{2})) \to b \neq 0$
192		divgcdcoprm0	$⊢ (a \in ℤ \land b \in ℤ \land b \neq 0) \to (\frac{a}{a \gcd b}) \gcd (\frac{b}{a \gcd b}) = 1$
193	189 190 191 192	syl3anc	$⊢ ((φ \land (c \in ℕ \land a \in ℕ)) \land (b \in ℕ \land a^{4} + b^{4} = c^{2})) \to (\frac{a}{a \gcd b}) \gcd (\frac{b}{a \gcd b}) = 1$
194	184	simprd	$⊢ ((φ \land (c \in ℕ \land a \in ℕ)) \land (b \in ℕ \land a^{4} + b^{4} = c^{2})) \to {(\frac{a}{a \gcd b})}^{4} + {(\frac{b}{a \gcd b})}^{4} = {(\frac{c}{{(a \gcd b)}^{2}})}^{2}$
195	193 194	jca	$⊢ ((φ \land (c \in ℕ \land a \in ℕ)) \land (b \in ℕ \land a^{4} + b^{4} = c^{2})) \to ((\frac{a}{a \gcd b}) \gcd (\frac{b}{a \gcd b}) = 1 \land {(\frac{a}{a \gcd b})}^{4} + {(\frac{b}{a \gcd b})}^{4} = {(\frac{c}{{(a \gcd b)}^{2}})}^{2})$
196	167 173 179 186 187 188 195	3rspcedvdw	$⊢ ((φ \land (c \in ℕ \land a \in ℕ)) \land (b \in ℕ \land a^{4} + b^{4} = c^{2})) \to \exists f \in ℕ \exists d \in ℕ \exists e \in ℕ (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})$
197	196	rexlimdvaa	$⊢ (φ \land (c \in ℕ \land a \in ℕ)) \to (\exists b \in ℕ a^{4} + b^{4} = c^{2} \to \exists f \in ℕ \exists d \in ℕ \exists e \in ℕ (d \gcd e = 1 \land d^{4} + e^{4} = f^{2}))$
198	197	rexlimdvva	$⊢ φ \to (\exists c \in ℕ \exists a \in ℕ \exists b \in ℕ a^{4} + b^{4} = c^{2} \to \exists f \in ℕ \exists d \in ℕ \exists e \in ℕ (d \gcd e = 1 \land d^{4} + e^{4} = f^{2}))$
199	198	con3d	$⊢ φ \to (\neg \exists f \in ℕ \exists d \in ℕ \exists e \in ℕ (d \gcd e = 1 \land d^{4} + e^{4} = f^{2}) \to \neg \exists c \in ℕ \exists a \in ℕ \exists b \in ℕ a^{4} + b^{4} = c^{2})$
200		ralnex	$⊢ \forall c \in ℕ \neg \exists a \in ℕ \exists b \in ℕ a^{4} + b^{4} = c^{2} \leftrightarrow \neg \exists c \in ℕ \exists a \in ℕ \exists b \in ℕ a^{4} + b^{4} = c^{2}$
201	199 159 200	3imtr4g	$⊢ φ \to (\forall f \in ℕ \neg \exists d \in ℕ \exists e \in ℕ (d \gcd e = 1 \land d^{4} + e^{4} = f^{2}) \to \forall c \in ℕ \neg \exists a \in ℕ \exists b \in ℕ a^{4} + b^{4} = c^{2})$
202		rabeq0	$⊢ \{c \in ℕ \| \exists a \in ℕ \exists b \in ℕ a^{4} + b^{4} = c^{2}\} = \emptyset \leftrightarrow \forall c \in ℕ \neg \exists a \in ℕ \exists b \in ℕ a^{4} + b^{4} = c^{2}$
203	201 162 202	3imtr4g	$⊢ φ \to (\{f \in ℕ \| \exists d \in ℕ \exists e \in ℕ (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})\} = \emptyset \to \{c \in ℕ \| \exists a \in ℕ \exists b \in ℕ a^{4} + b^{4} = c^{2}\} = \emptyset)$
204	164 203	mpd	$⊢ φ \to \{c \in ℕ \| \exists a \in ℕ \exists b \in ℕ a^{4} + b^{4} = c^{2}\} = \emptyset$
205		sseq0	$⊢ (\{c \in ℕ \| A^{4} + B^{4} = c^{2}\} \subseteq \{c \in ℕ \| \exists a \in ℕ \exists b \in ℕ a^{4} + b^{4} = c^{2}\} \land \{c \in ℕ \| \exists a \in ℕ \exists b \in ℕ a^{4} + b^{4} = c^{2}\} = \emptyset) \to \{c \in ℕ \| A^{4} + B^{4} = c^{2}\} = \emptyset$
206	15 204 205	syl2anc	$⊢ φ \to \{c \in ℕ \| A^{4} + B^{4} = c^{2}\} = \emptyset$
207		rabeq0	$⊢ \{c \in ℕ \| A^{4} + B^{4} = c^{2}\} = \emptyset \leftrightarrow \forall c \in ℕ \neg A^{4} + B^{4} = c^{2}$
208	206 207	sylib	$⊢ φ \to \forall c \in ℕ \neg A^{4} + B^{4} = c^{2}$
209		oveq1	$⊢ c = C \to c^{2} = C^{2}$
210	209	eqeq2d	$⊢ c = C \to (A^{4} + B^{4} = c^{2} \leftrightarrow A^{4} + B^{4} = C^{2})$
211	210	necon3bbid	$⊢ c = C \to (\neg A^{4} + B^{4} = c^{2} \leftrightarrow A^{4} + B^{4} \neq C^{2})$
212	211	rspcv	$⊢ C \in ℕ \to (\forall c \in ℕ \neg A^{4} + B^{4} = c^{2} \to A^{4} + B^{4} \neq C^{2})$
213	3 208 212	sylc	$⊢ φ \to A^{4} + B^{4} \neq C^{2}$

Metamath Proof Explorer

Theorem nna4b4nsq

Proof