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	$⊢ c = f \to c^{2} = f^{2}$
5	4	eqeq2d	$⊢ c = f \to (d^{4} + e^{4} = c^{2} \leftrightarrow d^{4} + e^{4} = f^{2})$
6	5	anbi2d	$⊢ c = f \to ((d \gcd e = 1 \land d^{4} + e^{4} = c^{2}) \leftrightarrow (d \gcd e = 1 \land d^{4} + e^{4} = f^{2}))$
7	6	anbi2d	$⊢ c = f \to ((\neg 2 ∥ d \land (d \gcd e = 1 \land d^{4} + e^{4} = c^{2})) \leftrightarrow (\neg 2 ∥ d \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})))$
8	7	2rexbidv	$⊢ c = f \to (\exists d \in ℕ \exists e \in ℕ (\neg 2 ∥ d \land (d \gcd e = 1 \land d^{4} + e^{4} = c^{2})) \leftrightarrow \exists d \in ℕ \exists e \in ℕ (\neg 2 ∥ d \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})))$
9		oveq1	$⊢ c = g \to c^{2} = g^{2}$
10	9	eqeq2d	$⊢ c = g \to (d^{4} + e^{4} = c^{2} \leftrightarrow d^{4} + e^{4} = g^{2})$
11	10	anbi2d	$⊢ c = g \to ((d \gcd e = 1 \land d^{4} + e^{4} = c^{2}) \leftrightarrow (d \gcd e = 1 \land d^{4} + e^{4} = g^{2}))$
12	11	anbi2d	$⊢ c = g \to ((\neg 2 ∥ d \land (d \gcd e = 1 \land d^{4} + e^{4} = c^{2})) \leftrightarrow (\neg 2 ∥ d \land (d \gcd e = 1 \land d^{4} + e^{4} = g^{2})))$
13	12	2rexbidv	$⊢ c = g \to (\exists d \in ℕ \exists e \in ℕ (\neg 2 ∥ d \land (d \gcd e = 1 \land d^{4} + e^{4} = c^{2})) \leftrightarrow \exists d \in ℕ \exists e \in ℕ (\neg 2 ∥ d \land (d \gcd e = 1 \land d^{4} + e^{4} = g^{2})))$
14		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
15	14	eqimssi	$⊢ ℕ \subseteq ℤ_{\geq 1}$
16	15	a1i	$⊢ φ \to ℕ \subseteq ℤ_{\geq 1}$
17		breq2	$⊢ d = h \to (2 ∥ d \leftrightarrow 2 ∥ h)$
18	17	notbid	$⊢ d = h \to (\neg 2 ∥ d \leftrightarrow \neg 2 ∥ h)$
19		oveq1	$⊢ d = h \to d \gcd e = h \gcd e$
20	19	eqeq1d	$⊢ d = h \to (d \gcd e = 1 \leftrightarrow h \gcd e = 1)$
21		oveq1	$⊢ d = h \to d^{4} = h^{4}$
22	21	oveq1d	$⊢ d = h \to d^{4} + e^{4} = h^{4} + e^{4}$
23	22	eqeq1d	$⊢ d = h \to (d^{4} + e^{4} = f^{2} \leftrightarrow h^{4} + e^{4} = f^{2})$
24	20 23	anbi12d	$⊢ d = h \to ((d \gcd e = 1 \land d^{4} + e^{4} = f^{2}) \leftrightarrow (h \gcd e = 1 \land h^{4} + e^{4} = f^{2}))$
25	18 24	anbi12d	$⊢ d = h \to ((\neg 2 ∥ d \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \leftrightarrow (\neg 2 ∥ h \land (h \gcd e = 1 \land h^{4} + e^{4} = f^{2})))$
26		oveq2	$⊢ e = i \to h \gcd e = h \gcd i$
27	26	eqeq1d	$⊢ e = i \to (h \gcd e = 1 \leftrightarrow h \gcd i = 1)$
28		oveq1	$⊢ e = i \to e^{4} = i^{4}$
29	28	oveq2d	$⊢ e = i \to h^{4} + e^{4} = h^{4} + i^{4}$
30	29	eqeq1d	$⊢ e = i \to (h^{4} + e^{4} = f^{2} \leftrightarrow h^{4} + i^{4} = f^{2})$
31	27 30	anbi12d	$⊢ e = i \to ((h \gcd e = 1 \land h^{4} + e^{4} = f^{2}) \leftrightarrow (h \gcd i = 1 \land h^{4} + i^{4} = f^{2}))$
32	31	anbi2d	$⊢ e = i \to ((\neg 2 ∥ h \land (h \gcd e = 1 \land h^{4} + e^{4} = f^{2})) \leftrightarrow (\neg 2 ∥ h \land (h \gcd i = 1 \land h^{4} + i^{4} = f^{2})))$
33	25 32	cbvrex2vw	$⊢ \exists d \in ℕ \exists e \in ℕ (\neg 2 ∥ d \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \leftrightarrow \exists h \in ℕ \exists i \in ℕ (\neg 2 ∥ h \land (h \gcd i = 1 \land h^{4} + i^{4} = f^{2}))$
34		simplrl	$⊢ (((φ \land f \in ℕ) \land (h \in ℕ \land i \in ℕ)) \land (\neg 2 ∥ h \land (h \gcd i = 1 \land h^{4} + i^{4} = f^{2}))) \to h \in ℕ$
35		simplrr	$⊢ (((φ \land f \in ℕ) \land (h \in ℕ \land i \in ℕ)) \land (\neg 2 ∥ h \land (h \gcd i = 1 \land h^{4} + i^{4} = f^{2}))) \to i \in ℕ$
36		simpllr	$⊢ (((φ \land f \in ℕ) \land (h \in ℕ \land i \in ℕ)) \land (\neg 2 ∥ h \land (h \gcd i = 1 \land h^{4} + i^{4} = f^{2}))) \to f \in ℕ$
37		simprl	$⊢ (((φ \land f \in ℕ) \land (h \in ℕ \land i \in ℕ)) \land (\neg 2 ∥ h \land (h \gcd i = 1 \land h^{4} + i^{4} = f^{2}))) \to \neg 2 ∥ h$
38		simprrl	$⊢ (((φ \land f \in ℕ) \land (h \in ℕ \land i \in ℕ)) \land (\neg 2 ∥ h \land (h \gcd i = 1 \land h^{4} + i^{4} = f^{2}))) \to h \gcd i = 1$
39		simprrr	$⊢ (((φ \land f \in ℕ) \land (h \in ℕ \land i \in ℕ)) \land (\neg 2 ∥ h \land (h \gcd i = 1 \land h^{4} + i^{4} = f^{2}))) \to h^{4} + i^{4} = f^{2}$
40	34 35 36 37 38 39	flt4lem7	$⊢ (((φ \land f \in ℕ) \land (h \in ℕ \land i \in ℕ)) \land (\neg 2 ∥ h \land (h \gcd i = 1 \land h^{4} + i^{4} = f^{2}))) \to \exists g \in ℕ (\exists d \in ℕ \exists e \in ℕ (\neg 2 ∥ d \land (d \gcd e = 1 \land d^{4} + e^{4} = g^{2})) \land g < f)$
41	40	ex	$⊢ ((φ \land f \in ℕ) \land (h \in ℕ \land i \in ℕ)) \to ((\neg 2 ∥ h \land (h \gcd i = 1 \land h^{4} + i^{4} = f^{2})) \to \exists g \in ℕ (\exists d \in ℕ \exists e \in ℕ (\neg 2 ∥ d \land (d \gcd e = 1 \land d^{4} + e^{4} = g^{2})) \land g < f))$
42	41	rexlimdvva	$⊢ (φ \land f \in ℕ) \to (\exists h \in ℕ \exists i \in ℕ (\neg 2 ∥ h \land (h \gcd i = 1 \land h^{4} + i^{4} = f^{2})) \to \exists g \in ℕ (\exists d \in ℕ \exists e \in ℕ (\neg 2 ∥ d \land (d \gcd e = 1 \land d^{4} + e^{4} = g^{2})) \land g < f))$
43	33 42	biimtrid	$⊢ (φ \land f \in ℕ) \to (\exists d \in ℕ \exists e \in ℕ (\neg 2 ∥ d \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})) \to \exists g \in ℕ (\exists d \in ℕ \exists e \in ℕ (\neg 2 ∥ d \land (d \gcd e = 1 \land d^{4} + e^{4} = g^{2})) \land g < f))$
44	43	impr	$⊢ (φ \land (f \in ℕ \land \exists d \in ℕ \exists e \in ℕ (\neg 2 ∥ d \land (d \gcd e = 1 \land d^{4} + e^{4} = f^{2})))) \to \exists g \in ℕ (\exists d \in ℕ \exists e \in ℕ (\neg 2 ∥ d \land (d \gcd e = 1 \land d^{4} + e^{4} = g^{2})) \land g < f)$
45	8 13 16 44	infdesc	$⊢ φ \to \{c \in ℕ \| \exists d \in ℕ \exists e \in ℕ (\neg 2 ∥ d \land (d \gcd e = 1 \land d^{4} + e^{4} = c^{2}))\} = \emptyset$
46		rabeq0	$⊢ \{c \in ℕ \| \exists d \in ℕ \exists e \in ℕ (\neg 2 ∥ d \land (d \gcd e = 1 \land d^{4} + e^{4} = c^{2}))\} = \emptyset \leftrightarrow \forall c \in ℕ \neg \exists d \in ℕ \exists e \in ℕ (\neg 2 ∥ d \land (d \gcd e = 1 \land d^{4} + e^{4} = c^{2}))$
47	45 46	sylib	$⊢ φ \to \forall c \in ℕ \neg \exists d \in ℕ \exists e \in ℕ (\neg 2 ∥ d \land (d \gcd e = 1 \land d^{4} + e^{4} = c^{2}))$
48		ralnex	$⊢ \forall c \in ℕ \neg \exists d \in ℕ \exists e \in ℕ (\neg 2 ∥ d \land (d \gcd e = 1 \land d^{4} + e^{4} = c^{2})) \leftrightarrow \neg \exists c \in ℕ \exists d \in ℕ \exists e \in ℕ (\neg 2 ∥ d \land (d \gcd e = 1 \land d^{4} + e^{4} = c^{2}))$
49	47 48	sylib	$⊢ φ \to \neg \exists c \in ℕ \exists d \in ℕ \exists e \in ℕ (\neg 2 ∥ d \land (d \gcd e = 1 \land d^{4} + e^{4} = c^{2}))$
50		breq2	$⊢ d = a \to (2 ∥ d \leftrightarrow 2 ∥ a)$
51	50	notbid	$⊢ d = a \to (\neg 2 ∥ d \leftrightarrow \neg 2 ∥ a)$
52		oveq1	$⊢ d = a \to d \gcd e = a \gcd e$
53	52	eqeq1d	$⊢ d = a \to (d \gcd e = 1 \leftrightarrow a \gcd e = 1)$
54		oveq1	$⊢ d = a \to d^{4} = a^{4}$
55	54	oveq1d	$⊢ d = a \to d^{4} + e^{4} = a^{4} + e^{4}$
56	55	eqeq1d	$⊢ d = a \to (d^{4} + e^{4} = c^{2} \leftrightarrow a^{4} + e^{4} = c^{2})$
57	53 56	anbi12d	$⊢ d = a \to ((d \gcd e = 1 \land d^{4} + e^{4} = c^{2}) \leftrightarrow (a \gcd e = 1 \land a^{4} + e^{4} = c^{2}))$
58	51 57	anbi12d	$⊢ d = a \to ((\neg 2 ∥ d \land (d \gcd e = 1 \land d^{4} + e^{4} = c^{2})) \leftrightarrow (\neg 2 ∥ a \land (a \gcd e = 1 \land a^{4} + e^{4} = c^{2})))$
59		oveq2	$⊢ e = b \to a \gcd e = a \gcd b$
60	59	eqeq1d	$⊢ e = b \to (a \gcd e = 1 \leftrightarrow a \gcd b = 1)$
61		oveq1	$⊢ e = b \to e^{4} = b^{4}$
62	61	oveq2d	$⊢ e = b \to a^{4} + e^{4} = a^{4} + b^{4}$
63	62	eqeq1d	$⊢ e = b \to (a^{4} + e^{4} = c^{2} \leftrightarrow a^{4} + b^{4} = c^{2})$
64	60 63	anbi12d	$⊢ e = b \to ((a \gcd e = 1 \land a^{4} + e^{4} = c^{2}) \leftrightarrow (a \gcd b = 1 \land a^{4} + b^{4} = c^{2}))$
65	64	anbi2d	$⊢ e = b \to ((\neg 2 ∥ a \land (a \gcd e = 1 \land a^{4} + e^{4} = c^{2})) \leftrightarrow (\neg 2 ∥ a \land (a \gcd b = 1 \land a^{4} + b^{4} = c^{2})))$
66		simprr	$⊢ ((φ \land c \in ℕ) \land (b \in ℕ \land a \in ℕ)) \to a \in ℕ$
67	66	ad2antrr	$⊢ ((((φ \land c \in ℕ) \land (b \in ℕ \land a \in ℕ)) \land (a \gcd b = 1 \land a^{4} + b^{4} = c^{2})) \land \neg 2 ∥ a) \to a \in ℕ$
68		simprl	$⊢ ((φ \land c \in ℕ) \land (b \in ℕ \land a \in ℕ)) \to b \in ℕ$
69	68	ad2antrr	$⊢ ((((φ \land c \in ℕ) \land (b \in ℕ \land a \in ℕ)) \land (a \gcd b = 1 \land a^{4} + b^{4} = c^{2})) \land \neg 2 ∥ a) \to b \in ℕ$
70		simpr	$⊢ (((φ \land c \in ℕ) \land (b \in ℕ \land a \in ℕ)) \land (a \gcd b = 1 \land a^{4} + b^{4} = c^{2})) \to (a \gcd b = 1 \land a^{4} + b^{4} = c^{2})$
71	70	anim1ci	$⊢ ((((φ \land c \in ℕ) \land (b \in ℕ \land a \in ℕ)) \land (a \gcd b = 1 \land a^{4} + b^{4} = c^{2})) \land \neg 2 ∥ a) \to (\neg 2 ∥ a \land (a \gcd b = 1 \land a^{4} + b^{4} = c^{2}))$
72	58 65 67 69 71	2rspcedvdw	$⊢ ((((φ \land c \in ℕ) \land (b \in ℕ \land a \in ℕ)) \land (a \gcd b = 1 \land a^{4} + b^{4} = c^{2})) \land \neg 2 ∥ a) \to \exists d \in ℕ \exists e \in ℕ (\neg 2 ∥ d \land (d \gcd e = 1 \land d^{4} + e^{4} = c^{2}))$
73		breq2	$⊢ d = b \to (2 ∥ d \leftrightarrow 2 ∥ b)$
74	73	notbid	$⊢ d = b \to (\neg 2 ∥ d \leftrightarrow \neg 2 ∥ b)$
75		oveq1	$⊢ d = b \to d \gcd e = b \gcd e$
76	75	eqeq1d	$⊢ d = b \to (d \gcd e = 1 \leftrightarrow b \gcd e = 1)$
77		oveq1	$⊢ d = b \to d^{4} = b^{4}$
78	77	oveq1d	$⊢ d = b \to d^{4} + e^{4} = b^{4} + e^{4}$
79	78	eqeq1d	$⊢ d = b \to (d^{4} + e^{4} = c^{2} \leftrightarrow b^{4} + e^{4} = c^{2})$
80	76 79	anbi12d	$⊢ d = b \to ((d \gcd e = 1 \land d^{4} + e^{4} = c^{2}) \leftrightarrow (b \gcd e = 1 \land b^{4} + e^{4} = c^{2}))$
81	74 80	anbi12d	$⊢ d = b \to ((\neg 2 ∥ d \land (d \gcd e = 1 \land d^{4} + e^{4} = c^{2})) \leftrightarrow (\neg 2 ∥ b \land (b \gcd e = 1 \land b^{4} + e^{4} = c^{2})))$
82		oveq2	$⊢ e = a \to b \gcd e = b \gcd a$
83	82	eqeq1d	$⊢ e = a \to (b \gcd e = 1 \leftrightarrow b \gcd a = 1)$
84		oveq1	$⊢ e = a \to e^{4} = a^{4}$
85	84	oveq2d	$⊢ e = a \to b^{4} + e^{4} = b^{4} + a^{4}$
86	85	eqeq1d	$⊢ e = a \to (b^{4} + e^{4} = c^{2} \leftrightarrow b^{4} + a^{4} = c^{2})$
87	83 86	anbi12d	$⊢ e = a \to ((b \gcd e = 1 \land b^{4} + e^{4} = c^{2}) \leftrightarrow (b \gcd a = 1 \land b^{4} + a^{4} = c^{2}))$
88	87	anbi2d	$⊢ e = a \to ((\neg 2 ∥ b \land (b \gcd e = 1 \land b^{4} + e^{4} = c^{2})) \leftrightarrow (\neg 2 ∥ b \land (b \gcd a = 1 \land b^{4} + a^{4} = c^{2})))$
89	68	ad2antrr	$⊢ ((((φ \land c \in ℕ) \land (b \in ℕ \land a \in ℕ)) \land (a \gcd b = 1 \land a^{4} + b^{4} = c^{2})) \land \neg 2 ∥ b) \to b \in ℕ$
90	66	ad2antrr	$⊢ ((((φ \land c \in ℕ) \land (b \in ℕ \land a \in ℕ)) \land (a \gcd b = 1 \land a^{4} + b^{4} = c^{2})) \land \neg 2 ∥ b) \to a \in ℕ$
91		simpr	$⊢ ((((φ \land c \in ℕ) \land (b \in ℕ \land a \in ℕ)) \land (a \gcd b = 1 \land a^{4} + b^{4} = c^{2})) \land \neg 2 ∥ b) \to \neg 2 ∥ b$
92	89	nnzd	$⊢ ((((φ \land c \in ℕ) \land (b \in ℕ \land a \in ℕ)) \land (a \gcd b = 1 \land a^{4} + b^{4} = c^{2})) \land \neg 2 ∥ b) \to b \in ℤ$
93	90	nnzd	$⊢ ((((φ \land c \in ℕ) \land (b \in ℕ \land a \in ℕ)) \land (a \gcd b = 1 \land a^{4} + b^{4} = c^{2})) \land \neg 2 ∥ b) \to a \in ℤ$
94	92 93	gcdcomd	$⊢ ((((φ \land c \in ℕ) \land (b \in ℕ \land a \in ℕ)) \land (a \gcd b = 1 \land a^{4} + b^{4} = c^{2})) \land \neg 2 ∥ b) \to b \gcd a = a \gcd b$
95		simplrl	$⊢ ((((φ \land c \in ℕ) \land (b \in ℕ \land a \in ℕ)) \land (a \gcd b = 1 \land a^{4} + b^{4} = c^{2})) \land \neg 2 ∥ b) \to a \gcd b = 1$
96	94 95	eqtrd	$⊢ ((((φ \land c \in ℕ) \land (b \in ℕ \land a \in ℕ)) \land (a \gcd b = 1 \land a^{4} + b^{4} = c^{2})) \land \neg 2 ∥ b) \to b \gcd a = 1$
97		4nn0	$⊢ 4 \in ℕ_{0}$
98	97	a1i	$⊢ ((((φ \land c \in ℕ) \land (b \in ℕ \land a \in ℕ)) \land (a \gcd b = 1 \land a^{4} + b^{4} = c^{2})) \land \neg 2 ∥ b) \to 4 \in ℕ_{0}$
99	89 98	nnexpcld	$⊢ ((((φ \land c \in ℕ) \land (b \in ℕ \land a \in ℕ)) \land (a \gcd b = 1 \land a^{4} + b^{4} = c^{2})) \land \neg 2 ∥ b) \to b^{4} \in ℕ$
100	99	nncnd	$⊢ ((((φ \land c \in ℕ) \land (b \in ℕ \land a \in ℕ)) \land (a \gcd b = 1 \land a^{4} + b^{4} = c^{2})) \land \neg 2 ∥ b) \to b^{4} \in ℂ$
101	90 98	nnexpcld	$⊢ ((((φ \land c \in ℕ) \land (b \in ℕ \land a \in ℕ)) \land (a \gcd b = 1 \land a^{4} + b^{4} = c^{2})) \land \neg 2 ∥ b) \to a^{4} \in ℕ$
102	101	nncnd	$⊢ ((((φ \land c \in ℕ) \land (b \in ℕ \land a \in ℕ)) \land (a \gcd b = 1 \land a^{4} + b^{4} = c^{2})) \land \neg 2 ∥ b) \to a^{4} \in ℂ$
103	100 102	addcomd	$⊢ ((((φ \land c \in ℕ) \land (b \in ℕ \land a \in ℕ)) \land (a \gcd b = 1 \land a^{4} + b^{4} = c^{2})) \land \neg 2 ∥ b) \to b^{4} + a^{4} = a^{4} + b^{4}$
104		simplrr	$⊢ ((((φ \land c \in ℕ) \land (b \in ℕ \land a \in ℕ)) \land (a \gcd b = 1 \land a^{4} + b^{4} = c^{2})) \land \neg 2 ∥ b) \to a^{4} + b^{4} = c^{2}$
105	103 104	eqtrd	$⊢ ((((φ \land c \in ℕ) \land (b \in ℕ \land a \in ℕ)) \land (a \gcd b = 1 \land a^{4} + b^{4} = c^{2})) \land \neg 2 ∥ b) \to b^{4} + a^{4} = c^{2}$
106	91 96 105	jca32	$⊢ ((((φ \land c \in ℕ) \land (b \in ℕ \land a \in ℕ)) \land (a \gcd b = 1 \land a^{4} + b^{4} = c^{2})) \land \neg 2 ∥ b) \to (\neg 2 ∥ b \land (b \gcd a = 1 \land b^{4} + a^{4} = c^{2}))$
107	81 88 89 90 106	2rspcedvdw	$⊢ ((((φ \land c \in ℕ) \land (b \in ℕ \land a \in ℕ)) \land (a \gcd b = 1 \land a^{4} + b^{4} = c^{2})) \land \neg 2 ∥ b) \to \exists d \in ℕ \exists e \in ℕ (\neg 2 ∥ d \land (d \gcd e = 1 \land d^{4} + e^{4} = c^{2}))$
108	66	ad2antrr	$⊢ ((((φ \land c \in ℕ) \land (b \in ℕ \land a \in ℕ)) \land (a \gcd b = 1 \land a^{4} + b^{4} = c^{2})) \land 2 ∥ a) \to a \in ℕ$
109	68	ad2antrr	$⊢ ((((φ \land c \in ℕ) \land (b \in ℕ \land a \in ℕ)) \land (a \gcd b = 1 \land a^{4} + b^{4} = c^{2})) \land 2 ∥ a) \to b \in ℕ$
110		simpr	$⊢ ((((φ \land c \in ℕ) \land (b \in ℕ \land a \in ℕ)) \land (a \gcd b = 1 \land a^{4} + b^{4} = c^{2})) \land 2 ∥ a) \to 2 ∥ a$
111		simplrl	$⊢ ((((φ \land c \in ℕ) \land (b \in ℕ \land a \in ℕ)) \land (a \gcd b = 1 \land a^{4} + b^{4} = c^{2})) \land 2 ∥ a) \to a \gcd b = 1$
112	108 109 110 111	flt4lem2	$⊢ ((((φ \land c \in ℕ) \land (b \in ℕ \land a \in ℕ)) \land (a \gcd b = 1 \land a^{4} + b^{4} = c^{2})) \land 2 ∥ a) \to \neg 2 ∥ b$
113	112	ex	$⊢ (((φ \land c \in ℕ) \land (b \in ℕ \land a \in ℕ)) \land (a \gcd b = 1 \land a^{4} + b^{4} = c^{2})) \to (2 ∥ a \to \neg 2 ∥ b)$
114		imor	$⊢ (2 ∥ a \to \neg 2 ∥ b) \leftrightarrow (\neg 2 ∥ a \lor \neg 2 ∥ b)$
115	113 114	sylib	$⊢ (((φ \land c \in ℕ) \land (b \in ℕ \land a \in ℕ)) \land (a \gcd b = 1 \land a^{4} + b^{4} = c^{2})) \to (\neg 2 ∥ a \lor \neg 2 ∥ b)$
116	72 107 115	mpjaodan	$⊢ (((φ \land c \in ℕ) \land (b \in ℕ \land a \in ℕ)) \land (a \gcd b = 1 \land a^{4} + b^{4} = c^{2})) \to \exists d \in ℕ \exists e \in ℕ (\neg 2 ∥ d \land (d \gcd e = 1 \land d^{4} + e^{4} = c^{2}))$
117	116	ex	$⊢ ((φ \land c \in ℕ) \land (b \in ℕ \land a \in ℕ)) \to ((a \gcd b = 1 \land a^{4} + b^{4} = c^{2}) \to \exists d \in ℕ \exists e \in ℕ (\neg 2 ∥ d \land (d \gcd e = 1 \land d^{4} + e^{4} = c^{2})))$
118	117	rexlimdvva	$⊢ (φ \land c \in ℕ) \to (\exists b \in ℕ \exists a \in ℕ (a \gcd b = 1 \land a^{4} + b^{4} = c^{2}) \to \exists d \in ℕ \exists e \in ℕ (\neg 2 ∥ d \land (d \gcd e = 1 \land d^{4} + e^{4} = c^{2})))$
119	118	reximdva	$⊢ φ \to (\exists c \in ℕ \exists b \in ℕ \exists a \in ℕ (a \gcd b = 1 \land a^{4} + b^{4} = c^{2}) \to \exists c \in ℕ \exists d \in ℕ \exists e \in ℕ (\neg 2 ∥ d \land (d \gcd e = 1 \land d^{4} + e^{4} = c^{2})))$
120	49 119	mtod	$⊢ φ \to \neg \exists c \in ℕ \exists b \in ℕ \exists a \in ℕ (a \gcd b = 1 \land a^{4} + b^{4} = c^{2})$
121		rexcom13	$⊢ \exists c \in ℕ \exists b \in ℕ \exists a \in ℕ (a \gcd b = 1 \land a^{4} + b^{4} = c^{2}) \leftrightarrow \exists a \in ℕ \exists b \in ℕ \exists c \in ℕ (a \gcd b = 1 \land a^{4} + b^{4} = c^{2})$
122	120 121	sylnib	$⊢ φ \to \neg \exists a \in ℕ \exists b \in ℕ \exists c \in ℕ (a \gcd b = 1 \land a^{4} + b^{4} = c^{2})$
123		oveq1	$⊢ a = \frac{A}{A \gcd B} \to a \gcd b = (\frac{A}{A \gcd B}) \gcd b$
124	123	eqeq1d	$⊢ a = \frac{A}{A \gcd B} \to (a \gcd b = 1 \leftrightarrow (\frac{A}{A \gcd B}) \gcd b = 1)$
125		oveq1	$⊢ a = \frac{A}{A \gcd B} \to a^{4} = {(\frac{A}{A \gcd B})}^{4}$
126	125	oveq1d	$⊢ a = \frac{A}{A \gcd B} \to a^{4} + b^{4} = {(\frac{A}{A \gcd B})}^{4} + b^{4}$
127	126	eqeq1d	$⊢ a = \frac{A}{A \gcd B} \to (a^{4} + b^{4} = c^{2} \leftrightarrow {(\frac{A}{A \gcd B})}^{4} + b^{4} = c^{2})$
128	124 127	anbi12d	$⊢ a = \frac{A}{A \gcd B} \to ((a \gcd b = 1 \land a^{4} + b^{4} = c^{2}) \leftrightarrow ((\frac{A}{A \gcd B}) \gcd b = 1 \land {(\frac{A}{A \gcd B})}^{4} + b^{4} = c^{2}))$
129		oveq2	$⊢ b = \frac{B}{A \gcd B} \to (\frac{A}{A \gcd B}) \gcd b = (\frac{A}{A \gcd B}) \gcd (\frac{B}{A \gcd B})$
130	129	eqeq1d	$⊢ b = \frac{B}{A \gcd B} \to ((\frac{A}{A \gcd B}) \gcd b = 1 \leftrightarrow (\frac{A}{A \gcd B}) \gcd (\frac{B}{A \gcd B}) = 1)$
131		oveq1	$⊢ b = \frac{B}{A \gcd B} \to b^{4} = {(\frac{B}{A \gcd B})}^{4}$
132	131	oveq2d	$⊢ b = \frac{B}{A \gcd B} \to {(\frac{A}{A \gcd B})}^{4} + b^{4} = {(\frac{A}{A \gcd B})}^{4} + {(\frac{B}{A \gcd B})}^{4}$
133	132	eqeq1d	$⊢ b = \frac{B}{A \gcd B} \to ({(\frac{A}{A \gcd B})}^{4} + b^{4} = c^{2} \leftrightarrow {(\frac{A}{A \gcd B})}^{4} + {(\frac{B}{A \gcd B})}^{4} = c^{2})$
134	130 133	anbi12d	$⊢ b = \frac{B}{A \gcd B} \to (((\frac{A}{A \gcd B}) \gcd b = 1 \land {(\frac{A}{A \gcd B})}^{4} + b^{4} = c^{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} = c^{2}))$
135		oveq1	$⊢ c = \frac{C}{{(A \gcd B)}^{2}} \to c^{2} = {(\frac{C}{{(A \gcd B)}^{2}})}^{2}$
136	135	eqeq2d	$⊢ c = \frac{C}{{(A \gcd B)}^{2}} \to ({(\frac{A}{A \gcd B})}^{4} + {(\frac{B}{A \gcd B})}^{4} = c^{2} \leftrightarrow {(\frac{A}{A \gcd B})}^{4} + {(\frac{B}{A \gcd B})}^{4} = {(\frac{C}{{(A \gcd B)}^{2}})}^{2})$
137	136	anbi2d	$⊢ c = \frac{C}{{(A \gcd B)}^{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} = c^{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}))$
138	1	adantr	$⊢ (φ \land A^{4} + B^{4} = C^{2}) \to A \in ℕ$
139	2	adantr	$⊢ (φ \land A^{4} + B^{4} = C^{2}) \to B \in ℕ$
140	3	adantr	$⊢ (φ \land A^{4} + B^{4} = C^{2}) \to C \in ℕ$
141		simpr	$⊢ (φ \land A^{4} + B^{4} = C^{2}) \to A^{4} + B^{4} = C^{2}$
142	138 139 140 141	flt4lem6	$⊢ (φ \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})$
143	142	simpld	$⊢ (φ \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 ℕ)$
144	143	simp1d	$⊢ (φ \land A^{4} + B^{4} = C^{2}) \to \frac{A}{A \gcd B} \in ℕ$
145	143	simp2d	$⊢ (φ \land A^{4} + B^{4} = C^{2}) \to \frac{B}{A \gcd B} \in ℕ$
146	143	simp3d	$⊢ (φ \land A^{4} + B^{4} = C^{2}) \to \frac{C}{{(A \gcd B)}^{2}} \in ℕ$
147	1	nnzd	$⊢ φ \to A \in ℤ$
148	147	adantr	$⊢ (φ \land A^{4} + B^{4} = C^{2}) \to A \in ℤ$
149	2	nnzd	$⊢ φ \to B \in ℤ$
150	149	adantr	$⊢ (φ \land A^{4} + B^{4} = C^{2}) \to B \in ℤ$
151	2	nnne0d	$⊢ φ \to B \neq 0$
152	151	adantr	$⊢ (φ \land A^{4} + B^{4} = C^{2}) \to B \neq 0$
153		divgcdcoprm0	$⊢ (A \in ℤ \land B \in ℤ \land B \neq 0) \to (\frac{A}{A \gcd B}) \gcd (\frac{B}{A \gcd B}) = 1$
154	148 150 152 153	syl3anc	$⊢ (φ \land A^{4} + B^{4} = C^{2}) \to (\frac{A}{A \gcd B}) \gcd (\frac{B}{A \gcd B}) = 1$
155	142	simprd	$⊢ (φ \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}$
156	154 155	jca	$⊢ (φ \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})$
157	128 134 137 144 145 146 156	3rspcedvdw	$⊢ (φ \land A^{4} + B^{4} = C^{2}) \to \exists a \in ℕ \exists b \in ℕ \exists c \in ℕ (a \gcd b = 1 \land a^{4} + b^{4} = c^{2})$
158	122 157	mtand	$⊢ φ \to \neg A^{4} + B^{4} = C^{2}$
159	158	neqned	$⊢ φ \to A^{4} + B^{4} \neq C^{2}$

Metamath Proof Explorer

Theorem nna4b4nsq

Proof