nna4b4nsq - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > nna4b4nsq		Structured version Visualization version GIF version

Theorem nna4b4nsq 28005

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.)

**Hypotheses**
Ref	Expression
nna4b4nsq.a	⊢ (𝜑 → 𝐴 ∈ ℕ)
nna4b4nsq.b	⊢ (𝜑 → 𝐵 ∈ ℕ)
nna4b4nsq.c	⊢ (𝜑 → 𝐶 ∈ ℕ)

**Assertion**
Ref	Expression
nna4b4nsq	⊢ (𝜑 → ((𝐴↑4) + (𝐵↑4)) ≠ (𝐶↑2))

Proof of Theorem nna4b4nsq Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 𝑓 𝑔 ℎ 𝑖 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq1 7437	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑓 → (𝑐↑2) = (𝑓↑2))
2	1	eqeq2d 2774	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑓 → (((𝑑↑4) + (𝑒↑4)) = (𝑐↑2) ↔ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2)))
3	2	anbi2d 642	. . . . . . . . . 10 ⊢ (𝑐 = 𝑓 → (((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑐↑2)) ↔ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))))
4	3	anbi2d 642	. . . . . . . . 9 ⊢ (𝑐 = 𝑓 → ((¬ 2 ∥ 𝑑 ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑐↑2))) ↔ (¬ 2 ∥ 𝑑 ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2)))))
5	4	2rexbidv 3231	. . . . . . . 8 ⊢ (𝑐 = 𝑓 → (∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ (¬ 2 ∥ 𝑑 ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑐↑2))) ↔ ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ (¬ 2 ∥ 𝑑 ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2)))))
6		oveq1 7437	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑔 → (𝑐↑2) = (𝑔↑2))
7	6	eqeq2d 2774	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑔 → (((𝑑↑4) + (𝑒↑4)) = (𝑐↑2) ↔ ((𝑑↑4) + (𝑒↑4)) = (𝑔↑2)))
8	7	anbi2d 642	. . . . . . . . . 10 ⊢ (𝑐 = 𝑔 → (((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑐↑2)) ↔ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑔↑2))))
9	8	anbi2d 642	. . . . . . . . 9 ⊢ (𝑐 = 𝑔 → ((¬ 2 ∥ 𝑑 ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑐↑2))) ↔ (¬ 2 ∥ 𝑑 ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑔↑2)))))
10	9	2rexbidv 3231	. . . . . . . 8 ⊢ (𝑐 = 𝑔 → (∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ (¬ 2 ∥ 𝑑 ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑐↑2))) ↔ ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ (¬ 2 ∥ 𝑑 ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑔↑2)))))
11		nnuz 13017	. . . . . . . . . 10 ⊢ ℕ = (ℤ_≥‘1)
12	11	eqimssi 3973	. . . . . . . . 9 ⊢ ℕ ⊆ (ℤ_≥‘1)
13	12	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ℕ ⊆ (ℤ_≥‘1))
14		breq2 5110	. . . . . . . . . . . . 13 ⊢ (𝑑 = ℎ → (2 ∥ 𝑑 ↔ 2 ∥ ℎ))
15	14	notbid 321	. . . . . . . . . . . 12 ⊢ (𝑑 = ℎ → (¬ 2 ∥ 𝑑 ↔ ¬ 2 ∥ ℎ))
16		oveq1 7437	. . . . . . . . . . . . . 14 ⊢ (𝑑 = ℎ → (𝑑 gcd 𝑒) = (ℎ gcd 𝑒))
17	16	eqeq1d 2765	. . . . . . . . . . . . 13 ⊢ (𝑑 = ℎ → ((𝑑 gcd 𝑒) = 1 ↔ (ℎ gcd 𝑒) = 1))
18		oveq1 7437	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = ℎ → (𝑑↑4) = (ℎ↑4))
19	18	oveq1d 7445	. . . . . . . . . . . . . 14 ⊢ (𝑑 = ℎ → ((𝑑↑4) + (𝑒↑4)) = ((ℎ↑4) + (𝑒↑4)))
20	19	eqeq1d 2765	. . . . . . . . . . . . 13 ⊢ (𝑑 = ℎ → (((𝑑↑4) + (𝑒↑4)) = (𝑓↑2) ↔ ((ℎ↑4) + (𝑒↑4)) = (𝑓↑2)))
21	17, 20	anbi12d 644	. . . . . . . . . . . 12 ⊢ (𝑑 = ℎ → (((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2)) ↔ ((ℎ gcd 𝑒) = 1 ∧ ((ℎ↑4) + (𝑒↑4)) = (𝑓↑2))))
22	15, 21	anbi12d 644	. . . . . . . . . . 11 ⊢ (𝑑 = ℎ → ((¬ 2 ∥ 𝑑 ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ↔ (¬ 2 ∥ ℎ ∧ ((ℎ gcd 𝑒) = 1 ∧ ((ℎ↑4) + (𝑒↑4)) = (𝑓↑2)))))
23		oveq2 7438	. . . . . . . . . . . . . 14 ⊢ (𝑒 = 𝑖 → (ℎ gcd 𝑒) = (ℎ gcd 𝑖))
24	23	eqeq1d 2765	. . . . . . . . . . . . 13 ⊢ (𝑒 = 𝑖 → ((ℎ gcd 𝑒) = 1 ↔ (ℎ gcd 𝑖) = 1))
25		oveq1 7437	. . . . . . . . . . . . . . 15 ⊢ (𝑒 = 𝑖 → (𝑒↑4) = (𝑖↑4))
26	25	oveq2d 7446	. . . . . . . . . . . . . 14 ⊢ (𝑒 = 𝑖 → ((ℎ↑4) + (𝑒↑4)) = ((ℎ↑4) + (𝑖↑4)))
27	26	eqeq1d 2765	. . . . . . . . . . . . 13 ⊢ (𝑒 = 𝑖 → (((ℎ↑4) + (𝑒↑4)) = (𝑓↑2) ↔ ((ℎ↑4) + (𝑖↑4)) = (𝑓↑2)))
28	24, 27	anbi12d 644	. . . . . . . . . . . 12 ⊢ (𝑒 = 𝑖 → (((ℎ gcd 𝑒) = 1 ∧ ((ℎ↑4) + (𝑒↑4)) = (𝑓↑2)) ↔ ((ℎ gcd 𝑖) = 1 ∧ ((ℎ↑4) + (𝑖↑4)) = (𝑓↑2))))
29	28	anbi2d 642	. . . . . . . . . . 11 ⊢ (𝑒 = 𝑖 → ((¬ 2 ∥ ℎ ∧ ((ℎ gcd 𝑒) = 1 ∧ ((ℎ↑4) + (𝑒↑4)) = (𝑓↑2))) ↔ (¬ 2 ∥ ℎ ∧ ((ℎ gcd 𝑖) = 1 ∧ ((ℎ↑4) + (𝑖↑4)) = (𝑓↑2)))))
30	22, 29	cbvrex2vw 3249	. . . . . . . . . 10 ⊢ (∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ (¬ 2 ∥ 𝑑 ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ↔ ∃ℎ ∈ ℕ ∃𝑖 ∈ ℕ (¬ 2 ∥ ℎ ∧ ((ℎ gcd 𝑖) = 1 ∧ ((ℎ↑4) + (𝑖↑4)) = (𝑓↑2))))
31		simplrl 789	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑓 ∈ ℕ) ∧ (ℎ ∈ ℕ ∧ 𝑖 ∈ ℕ)) ∧ (¬ 2 ∥ ℎ ∧ ((ℎ gcd 𝑖) = 1 ∧ ((ℎ↑4) + (𝑖↑4)) = (𝑓↑2)))) → ℎ ∈ ℕ)
32		simplrr 790	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑓 ∈ ℕ) ∧ (ℎ ∈ ℕ ∧ 𝑖 ∈ ℕ)) ∧ (¬ 2 ∥ ℎ ∧ ((ℎ gcd 𝑖) = 1 ∧ ((ℎ↑4) + (𝑖↑4)) = (𝑓↑2)))) → 𝑖 ∈ ℕ)
33		simpllr 788	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑓 ∈ ℕ) ∧ (ℎ ∈ ℕ ∧ 𝑖 ∈ ℕ)) ∧ (¬ 2 ∥ ℎ ∧ ((ℎ gcd 𝑖) = 1 ∧ ((ℎ↑4) + (𝑖↑4)) = (𝑓↑2)))) → 𝑓 ∈ ℕ)
34		simprl 783	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑓 ∈ ℕ) ∧ (ℎ ∈ ℕ ∧ 𝑖 ∈ ℕ)) ∧ (¬ 2 ∥ ℎ ∧ ((ℎ gcd 𝑖) = 1 ∧ ((ℎ↑4) + (𝑖↑4)) = (𝑓↑2)))) → ¬ 2 ∥ ℎ)
35		simprrl 793	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑓 ∈ ℕ) ∧ (ℎ ∈ ℕ ∧ 𝑖 ∈ ℕ)) ∧ (¬ 2 ∥ ℎ ∧ ((ℎ gcd 𝑖) = 1 ∧ ((ℎ↑4) + (𝑖↑4)) = (𝑓↑2)))) → (ℎ gcd 𝑖) = 1)
36		simprrr 794	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑓 ∈ ℕ) ∧ (ℎ ∈ ℕ ∧ 𝑖 ∈ ℕ)) ∧ (¬ 2 ∥ ℎ ∧ ((ℎ gcd 𝑖) = 1 ∧ ((ℎ↑4) + (𝑖↑4)) = (𝑓↑2)))) → ((ℎ↑4) + (𝑖↑4)) = (𝑓↑2))
37	31, 32, 33, 34, 35, 36	flt4lem7 28004	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑓 ∈ ℕ) ∧ (ℎ ∈ ℕ ∧ 𝑖 ∈ ℕ)) ∧ (¬ 2 ∥ ℎ ∧ ((ℎ gcd 𝑖) = 1 ∧ ((ℎ↑4) + (𝑖↑4)) = (𝑓↑2)))) → ∃𝑔 ∈ ℕ (∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ (¬ 2 ∥ 𝑑 ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑔↑2))) ∧ 𝑔 < 𝑓))
38	37	ex 418	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ ℕ) ∧ (ℎ ∈ ℕ ∧ 𝑖 ∈ ℕ)) → ((¬ 2 ∥ ℎ ∧ ((ℎ gcd 𝑖) = 1 ∧ ((ℎ↑4) + (𝑖↑4)) = (𝑓↑2))) → ∃𝑔 ∈ ℕ (∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ (¬ 2 ∥ 𝑑 ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑔↑2))) ∧ 𝑔 < 𝑓)))
39	38	rexlimdvva 3223	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑓 ∈ ℕ) → (∃ℎ ∈ ℕ ∃𝑖 ∈ ℕ (¬ 2 ∥ ℎ ∧ ((ℎ gcd 𝑖) = 1 ∧ ((ℎ↑4) + (𝑖↑4)) = (𝑓↑2))) → ∃𝑔 ∈ ℕ (∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ (¬ 2 ∥ 𝑑 ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑔↑2))) ∧ 𝑔 < 𝑓)))
40	30, 39	biimtrid 245	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ ℕ) → (∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ (¬ 2 ∥ 𝑑 ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) → ∃𝑔 ∈ ℕ (∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ (¬ 2 ∥ 𝑑 ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑔↑2))) ∧ 𝑔 < 𝑓)))
41	40	impr 460	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ ℕ ∧ ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ (¬ 2 ∥ 𝑑 ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))))) → ∃𝑔 ∈ ℕ (∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ (¬ 2 ∥ 𝑑 ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑔↑2))) ∧ 𝑔 < 𝑓))
42	5, 10, 13, 41	infdesc 27982	. . . . . . 7 ⊢ (𝜑 → {𝑐 ∈ ℕ ∣ ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ (¬ 2 ∥ 𝑑 ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑐↑2)))} = ∅)
43		rabeq0 4341	. . . . . . 7 ⊢ ({𝑐 ∈ ℕ ∣ ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ (¬ 2 ∥ 𝑑 ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑐↑2)))} = ∅ ↔ ∀𝑐 ∈ ℕ ¬ ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ (¬ 2 ∥ 𝑑 ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑐↑2))))
44	42, 43	sylib 221	. . . . . 6 ⊢ (𝜑 → ∀𝑐 ∈ ℕ ¬ ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ (¬ 2 ∥ 𝑑 ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑐↑2))))
45		ralnex 3092	. . . . . 6 ⊢ (∀𝑐 ∈ ℕ ¬ ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ (¬ 2 ∥ 𝑑 ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑐↑2))) ↔ ¬ ∃𝑐 ∈ ℕ ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ (¬ 2 ∥ 𝑑 ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑐↑2))))
46	44, 45	sylib 221	. . . . 5 ⊢ (𝜑 → ¬ ∃𝑐 ∈ ℕ ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ (¬ 2 ∥ 𝑑 ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑐↑2))))
47		breq2 5110	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝑎 → (2 ∥ 𝑑 ↔ 2 ∥ 𝑎))
48	47	notbid 321	. . . . . . . . . . 11 ⊢ (𝑑 = 𝑎 → (¬ 2 ∥ 𝑑 ↔ ¬ 2 ∥ 𝑎))
49		oveq1 7437	. . . . . . . . . . . . 13 ⊢ (𝑑 = 𝑎 → (𝑑 gcd 𝑒) = (𝑎 gcd 𝑒))
50	49	eqeq1d 2765	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝑎 → ((𝑑 gcd 𝑒) = 1 ↔ (𝑎 gcd 𝑒) = 1))
51		oveq1 7437	. . . . . . . . . . . . . 14 ⊢ (𝑑 = 𝑎 → (𝑑↑4) = (𝑎↑4))
52	51	oveq1d 7445	. . . . . . . . . . . . 13 ⊢ (𝑑 = 𝑎 → ((𝑑↑4) + (𝑒↑4)) = ((𝑎↑4) + (𝑒↑4)))
53	52	eqeq1d 2765	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝑎 → (((𝑑↑4) + (𝑒↑4)) = (𝑐↑2) ↔ ((𝑎↑4) + (𝑒↑4)) = (𝑐↑2)))
54	50, 53	anbi12d 644	. . . . . . . . . . 11 ⊢ (𝑑 = 𝑎 → (((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑐↑2)) ↔ ((𝑎 gcd 𝑒) = 1 ∧ ((𝑎↑4) + (𝑒↑4)) = (𝑐↑2))))
55	48, 54	anbi12d 644	. . . . . . . . . 10 ⊢ (𝑑 = 𝑎 → ((¬ 2 ∥ 𝑑 ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑐↑2))) ↔ (¬ 2 ∥ 𝑎 ∧ ((𝑎 gcd 𝑒) = 1 ∧ ((𝑎↑4) + (𝑒↑4)) = (𝑐↑2)))))
56		oveq2 7438	. . . . . . . . . . . . 13 ⊢ (𝑒 = 𝑏 → (𝑎 gcd 𝑒) = (𝑎 gcd 𝑏))
57	56	eqeq1d 2765	. . . . . . . . . . . 12 ⊢ (𝑒 = 𝑏 → ((𝑎 gcd 𝑒) = 1 ↔ (𝑎 gcd 𝑏) = 1))
58		oveq1 7437	. . . . . . . . . . . . . 14 ⊢ (𝑒 = 𝑏 → (𝑒↑4) = (𝑏↑4))
59	58	oveq2d 7446	. . . . . . . . . . . . 13 ⊢ (𝑒 = 𝑏 → ((𝑎↑4) + (𝑒↑4)) = ((𝑎↑4) + (𝑏↑4)))
60	59	eqeq1d 2765	. . . . . . . . . . . 12 ⊢ (𝑒 = 𝑏 → (((𝑎↑4) + (𝑒↑4)) = (𝑐↑2) ↔ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2)))
61	57, 60	anbi12d 644	. . . . . . . . . . 11 ⊢ (𝑒 = 𝑏 → (((𝑎 gcd 𝑒) = 1 ∧ ((𝑎↑4) + (𝑒↑4)) = (𝑐↑2)) ↔ ((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))))
62	61	anbi2d 642	. . . . . . . . . 10 ⊢ (𝑒 = 𝑏 → ((¬ 2 ∥ 𝑎 ∧ ((𝑎 gcd 𝑒) = 1 ∧ ((𝑎↑4) + (𝑒↑4)) = (𝑐↑2))) ↔ (¬ 2 ∥ 𝑎 ∧ ((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2)))))
63		simprr 785	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ ℕ) ∧ (𝑏 ∈ ℕ ∧ 𝑎 ∈ ℕ)) → 𝑎 ∈ ℕ)
64	63	ad2antrr 739	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑐 ∈ ℕ) ∧ (𝑏 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ ((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) ∧ ¬ 2 ∥ 𝑎) → 𝑎 ∈ ℕ)
65		simprl 783	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑐 ∈ ℕ) ∧ (𝑏 ∈ ℕ ∧ 𝑎 ∈ ℕ)) → 𝑏 ∈ ℕ)
66	65	ad2antrr 739	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑐 ∈ ℕ) ∧ (𝑏 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ ((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) ∧ ¬ 2 ∥ 𝑎) → 𝑏 ∈ ℕ)
67		simpr 490	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑐 ∈ ℕ) ∧ (𝑏 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ ((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) → ((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2)))
68	67	anim1ci 628	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑐 ∈ ℕ) ∧ (𝑏 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ ((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) ∧ ¬ 2 ∥ 𝑎) → (¬ 2 ∥ 𝑎 ∧ ((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))))
69	55, 62, 64, 66, 68	2rspcedvdw 3593	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑐 ∈ ℕ) ∧ (𝑏 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ ((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) ∧ ¬ 2 ∥ 𝑎) → ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ (¬ 2 ∥ 𝑑 ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑐↑2))))
70		breq2 5110	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝑏 → (2 ∥ 𝑑 ↔ 2 ∥ 𝑏))
71	70	notbid 321	. . . . . . . . . . 11 ⊢ (𝑑 = 𝑏 → (¬ 2 ∥ 𝑑 ↔ ¬ 2 ∥ 𝑏))
72		oveq1 7437	. . . . . . . . . . . . 13 ⊢ (𝑑 = 𝑏 → (𝑑 gcd 𝑒) = (𝑏 gcd 𝑒))
73	72	eqeq1d 2765	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝑏 → ((𝑑 gcd 𝑒) = 1 ↔ (𝑏 gcd 𝑒) = 1))
74		oveq1 7437	. . . . . . . . . . . . . 14 ⊢ (𝑑 = 𝑏 → (𝑑↑4) = (𝑏↑4))
75	74	oveq1d 7445	. . . . . . . . . . . . 13 ⊢ (𝑑 = 𝑏 → ((𝑑↑4) + (𝑒↑4)) = ((𝑏↑4) + (𝑒↑4)))
76	75	eqeq1d 2765	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝑏 → (((𝑑↑4) + (𝑒↑4)) = (𝑐↑2) ↔ ((𝑏↑4) + (𝑒↑4)) = (𝑐↑2)))
77	73, 76	anbi12d 644	. . . . . . . . . . 11 ⊢ (𝑑 = 𝑏 → (((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑐↑2)) ↔ ((𝑏 gcd 𝑒) = 1 ∧ ((𝑏↑4) + (𝑒↑4)) = (𝑐↑2))))
78	71, 77	anbi12d 644	. . . . . . . . . 10 ⊢ (𝑑 = 𝑏 → ((¬ 2 ∥ 𝑑 ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑐↑2))) ↔ (¬ 2 ∥ 𝑏 ∧ ((𝑏 gcd 𝑒) = 1 ∧ ((𝑏↑4) + (𝑒↑4)) = (𝑐↑2)))))
79		oveq2 7438	. . . . . . . . . . . . 13 ⊢ (𝑒 = 𝑎 → (𝑏 gcd 𝑒) = (𝑏 gcd 𝑎))
80	79	eqeq1d 2765	. . . . . . . . . . . 12 ⊢ (𝑒 = 𝑎 → ((𝑏 gcd 𝑒) = 1 ↔ (𝑏 gcd 𝑎) = 1))
81		oveq1 7437	. . . . . . . . . . . . . 14 ⊢ (𝑒 = 𝑎 → (𝑒↑4) = (𝑎↑4))
82	81	oveq2d 7446	. . . . . . . . . . . . 13 ⊢ (𝑒 = 𝑎 → ((𝑏↑4) + (𝑒↑4)) = ((𝑏↑4) + (𝑎↑4)))
83	82	eqeq1d 2765	. . . . . . . . . . . 12 ⊢ (𝑒 = 𝑎 → (((𝑏↑4) + (𝑒↑4)) = (𝑐↑2) ↔ ((𝑏↑4) + (𝑎↑4)) = (𝑐↑2)))
84	80, 83	anbi12d 644	. . . . . . . . . . 11 ⊢ (𝑒 = 𝑎 → (((𝑏 gcd 𝑒) = 1 ∧ ((𝑏↑4) + (𝑒↑4)) = (𝑐↑2)) ↔ ((𝑏 gcd 𝑎) = 1 ∧ ((𝑏↑4) + (𝑎↑4)) = (𝑐↑2))))
85	84	anbi2d 642	. . . . . . . . . 10 ⊢ (𝑒 = 𝑎 → ((¬ 2 ∥ 𝑏 ∧ ((𝑏 gcd 𝑒) = 1 ∧ ((𝑏↑4) + (𝑒↑4)) = (𝑐↑2))) ↔ (¬ 2 ∥ 𝑏 ∧ ((𝑏 gcd 𝑎) = 1 ∧ ((𝑏↑4) + (𝑎↑4)) = (𝑐↑2)))))
86	65	ad2antrr 739	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑐 ∈ ℕ) ∧ (𝑏 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ ((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) ∧ ¬ 2 ∥ 𝑏) → 𝑏 ∈ ℕ)
87	63	ad2antrr 739	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑐 ∈ ℕ) ∧ (𝑏 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ ((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) ∧ ¬ 2 ∥ 𝑏) → 𝑎 ∈ ℕ)
88		simpr 490	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑐 ∈ ℕ) ∧ (𝑏 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ ((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) ∧ ¬ 2 ∥ 𝑏) → ¬ 2 ∥ 𝑏)
89	86	nnzd 12732	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑐 ∈ ℕ) ∧ (𝑏 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ ((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) ∧ ¬ 2 ∥ 𝑏) → 𝑏 ∈ ℤ)
90	87	nnzd 12732	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑐 ∈ ℕ) ∧ (𝑏 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ ((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) ∧ ¬ 2 ∥ 𝑏) → 𝑎 ∈ ℤ)
91	89, 90	gcdcomd 16701	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑐 ∈ ℕ) ∧ (𝑏 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ ((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) ∧ ¬ 2 ∥ 𝑏) → (𝑏 gcd 𝑎) = (𝑎 gcd 𝑏))
92		simplrl 789	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑐 ∈ ℕ) ∧ (𝑏 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ ((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) ∧ ¬ 2 ∥ 𝑏) → (𝑎 gcd 𝑏) = 1)
93	91, 92	eqtrd 2798	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑐 ∈ ℕ) ∧ (𝑏 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ ((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) ∧ ¬ 2 ∥ 𝑏) → (𝑏 gcd 𝑎) = 1)
94		4nn0 12638	. . . . . . . . . . . . . . . 16 ⊢ 4 ∈ ℕ₀
95	94	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑐 ∈ ℕ) ∧ (𝑏 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ ((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) ∧ ¬ 2 ∥ 𝑏) → 4 ∈ ℕ₀)
96	86, 95	nnexpcld 14402	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑐 ∈ ℕ) ∧ (𝑏 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ ((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) ∧ ¬ 2 ∥ 𝑏) → (𝑏↑4) ∈ ℕ)
97	96	nncnd 12364	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑐 ∈ ℕ) ∧ (𝑏 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ ((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) ∧ ¬ 2 ∥ 𝑏) → (𝑏↑4) ∈ ℂ)
98	87, 95	nnexpcld 14402	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑐 ∈ ℕ) ∧ (𝑏 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ ((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) ∧ ¬ 2 ∥ 𝑏) → (𝑎↑4) ∈ ℕ)
99	98	nncnd 12364	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑐 ∈ ℕ) ∧ (𝑏 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ ((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) ∧ ¬ 2 ∥ 𝑏) → (𝑎↑4) ∈ ℂ)
100	97, 99	addcomd 11525	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑐 ∈ ℕ) ∧ (𝑏 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ ((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) ∧ ¬ 2 ∥ 𝑏) → ((𝑏↑4) + (𝑎↑4)) = ((𝑎↑4) + (𝑏↑4)))
101		simplrr 790	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑐 ∈ ℕ) ∧ (𝑏 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ ((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) ∧ ¬ 2 ∥ 𝑏) → ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))
102	100, 101	eqtrd 2798	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑐 ∈ ℕ) ∧ (𝑏 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ ((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) ∧ ¬ 2 ∥ 𝑏) → ((𝑏↑4) + (𝑎↑4)) = (𝑐↑2))
103	88, 93, 102	jca32 525	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑐 ∈ ℕ) ∧ (𝑏 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ ((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) ∧ ¬ 2 ∥ 𝑏) → (¬ 2 ∥ 𝑏 ∧ ((𝑏 gcd 𝑎) = 1 ∧ ((𝑏↑4) + (𝑎↑4)) = (𝑐↑2))))
104	78, 85, 86, 87, 103	2rspcedvdw 3593	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑐 ∈ ℕ) ∧ (𝑏 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ ((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) ∧ ¬ 2 ∥ 𝑏) → ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ (¬ 2 ∥ 𝑑 ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑐↑2))))
105	63	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑐 ∈ ℕ) ∧ (𝑏 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ ((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) ∧ 2 ∥ 𝑎) → 𝑎 ∈ ℕ)
106	65	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑐 ∈ ℕ) ∧ (𝑏 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ ((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) ∧ 2 ∥ 𝑎) → 𝑏 ∈ ℕ)
107		simpr 490	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑐 ∈ ℕ) ∧ (𝑏 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ ((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) ∧ 2 ∥ 𝑎) → 2 ∥ 𝑎)
108		simplrl 789	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑐 ∈ ℕ) ∧ (𝑏 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ ((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) ∧ 2 ∥ 𝑎) → (𝑎 gcd 𝑏) = 1)
109	105, 106, 107, 108	flt4lem2 27992	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑐 ∈ ℕ) ∧ (𝑏 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ ((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) ∧ 2 ∥ 𝑎) → ¬ 2 ∥ 𝑏)
110	109	ex 418	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑐 ∈ ℕ) ∧ (𝑏 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ ((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) → (2 ∥ 𝑎 → ¬ 2 ∥ 𝑏))
111		imor 867	. . . . . . . . . 10 ⊢ ((2 ∥ 𝑎 → ¬ 2 ∥ 𝑏) ↔ (¬ 2 ∥ 𝑎 ∨ ¬ 2 ∥ 𝑏))
112	110, 111	sylib 221	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑐 ∈ ℕ) ∧ (𝑏 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ ((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) → (¬ 2 ∥ 𝑎 ∨ ¬ 2 ∥ 𝑏))
113	69, 104, 112	mpjaodan 973	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑐 ∈ ℕ) ∧ (𝑏 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ ((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) → ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ (¬ 2 ∥ 𝑑 ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑐↑2))))
114	113	ex 418	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑐 ∈ ℕ) ∧ (𝑏 ∈ ℕ ∧ 𝑎 ∈ ℕ)) → (((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2)) → ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ (¬ 2 ∥ 𝑑 ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑐↑2)))))
115	114	rexlimdvva 3223	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ ℕ) → (∃𝑏 ∈ ℕ ∃𝑎 ∈ ℕ ((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2)) → ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ (¬ 2 ∥ 𝑑 ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑐↑2)))))
116	115	reximdva 3179	. . . . 5 ⊢ (𝜑 → (∃𝑐 ∈ ℕ ∃𝑏 ∈ ℕ ∃𝑎 ∈ ℕ ((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2)) → ∃𝑐 ∈ ℕ ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ (¬ 2 ∥ 𝑑 ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑐↑2)))))
117	46, 116	mtod 201	. . . 4 ⊢ (𝜑 → ¬ ∃𝑐 ∈ ℕ ∃𝑏 ∈ ℕ ∃𝑎 ∈ ℕ ((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2)))
118		rexcom13 3299	. . . 4 ⊢ (∃𝑐 ∈ ℕ ∃𝑏 ∈ ℕ ∃𝑎 ∈ ℕ ((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2)) ↔ ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ∃𝑐 ∈ ℕ ((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2)))
119	117, 118	sylnib 331	. . 3 ⊢ (𝜑 → ¬ ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ∃𝑐 ∈ ℕ ((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2)))
120		oveq1 7437	. . . . . 6 ⊢ (𝑎 = (𝐴 / (𝐴 gcd 𝐵)) → (𝑎 gcd 𝑏) = ((𝐴 / (𝐴 gcd 𝐵)) gcd 𝑏))
121	120	eqeq1d 2765	. . . . 5 ⊢ (𝑎 = (𝐴 / (𝐴 gcd 𝐵)) → ((𝑎 gcd 𝑏) = 1 ↔ ((𝐴 / (𝐴 gcd 𝐵)) gcd 𝑏) = 1))
122		oveq1 7437	. . . . . . 7 ⊢ (𝑎 = (𝐴 / (𝐴 gcd 𝐵)) → (𝑎↑4) = ((𝐴 / (𝐴 gcd 𝐵))↑4))
123	122	oveq1d 7445	. . . . . 6 ⊢ (𝑎 = (𝐴 / (𝐴 gcd 𝐵)) → ((𝑎↑4) + (𝑏↑4)) = (((𝐴 / (𝐴 gcd 𝐵))↑4) + (𝑏↑4)))
124	123	eqeq1d 2765	. . . . 5 ⊢ (𝑎 = (𝐴 / (𝐴 gcd 𝐵)) → (((𝑎↑4) + (𝑏↑4)) = (𝑐↑2) ↔ (((𝐴 / (𝐴 gcd 𝐵))↑4) + (𝑏↑4)) = (𝑐↑2)))
125	121, 124	anbi12d 644	. . . 4 ⊢ (𝑎 = (𝐴 / (𝐴 gcd 𝐵)) → (((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2)) ↔ (((𝐴 / (𝐴 gcd 𝐵)) gcd 𝑏) = 1 ∧ (((𝐴 / (𝐴 gcd 𝐵))↑4) + (𝑏↑4)) = (𝑐↑2))))
126		oveq2 7438	. . . . . 6 ⊢ (𝑏 = (𝐵 / (𝐴 gcd 𝐵)) → ((𝐴 / (𝐴 gcd 𝐵)) gcd 𝑏) = ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))))
127	126	eqeq1d 2765	. . . . 5 ⊢ (𝑏 = (𝐵 / (𝐴 gcd 𝐵)) → (((𝐴 / (𝐴 gcd 𝐵)) gcd 𝑏) = 1 ↔ ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1))
128		oveq1 7437	. . . . . . 7 ⊢ (𝑏 = (𝐵 / (𝐴 gcd 𝐵)) → (𝑏↑4) = ((𝐵 / (𝐴 gcd 𝐵))↑4))
129	128	oveq2d 7446	. . . . . 6 ⊢ (𝑏 = (𝐵 / (𝐴 gcd 𝐵)) → (((𝐴 / (𝐴 gcd 𝐵))↑4) + (𝑏↑4)) = (((𝐴 / (𝐴 gcd 𝐵))↑4) + ((𝐵 / (𝐴 gcd 𝐵))↑4)))
130	129	eqeq1d 2765	. . . . 5 ⊢ (𝑏 = (𝐵 / (𝐴 gcd 𝐵)) → ((((𝐴 / (𝐴 gcd 𝐵))↑4) + (𝑏↑4)) = (𝑐↑2) ↔ (((𝐴 / (𝐴 gcd 𝐵))↑4) + ((𝐵 / (𝐴 gcd 𝐵))↑4)) = (𝑐↑2)))
131	127, 130	anbi12d 644	. . . 4 ⊢ (𝑏 = (𝐵 / (𝐴 gcd 𝐵)) → ((((𝐴 / (𝐴 gcd 𝐵)) gcd 𝑏) = 1 ∧ (((𝐴 / (𝐴 gcd 𝐵))↑4) + (𝑏↑4)) = (𝑐↑2)) ↔ (((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1 ∧ (((𝐴 / (𝐴 gcd 𝐵))↑4) + ((𝐵 / (𝐴 gcd 𝐵))↑4)) = (𝑐↑2))))
132		oveq1 7437	. . . . . 6 ⊢ (𝑐 = (𝐶 / ((𝐴 gcd 𝐵)↑2)) → (𝑐↑2) = ((𝐶 / ((𝐴 gcd 𝐵)↑2))↑2))
133	132	eqeq2d 2774	. . . . 5 ⊢ (𝑐 = (𝐶 / ((𝐴 gcd 𝐵)↑2)) → ((((𝐴 / (𝐴 gcd 𝐵))↑4) + ((𝐵 / (𝐴 gcd 𝐵))↑4)) = (𝑐↑2) ↔ (((𝐴 / (𝐴 gcd 𝐵))↑4) + ((𝐵 / (𝐴 gcd 𝐵))↑4)) = ((𝐶 / ((𝐴 gcd 𝐵)↑2))↑2)))
134	133	anbi2d 642	. . . 4 ⊢ (𝑐 = (𝐶 / ((𝐴 gcd 𝐵)↑2)) → ((((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1 ∧ (((𝐴 / (𝐴 gcd 𝐵))↑4) + ((𝐵 / (𝐴 gcd 𝐵))↑4)) = (𝑐↑2)) ↔ (((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1 ∧ (((𝐴 / (𝐴 gcd 𝐵))↑4) + ((𝐵 / (𝐴 gcd 𝐵))↑4)) = ((𝐶 / ((𝐴 gcd 𝐵)↑2))↑2))))
135		nna4b4nsq.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℕ)
136	135	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2)) → 𝐴 ∈ ℕ)
137		nna4b4nsq.b	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ ℕ)
138	137	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2)) → 𝐵 ∈ ℕ)
139		nna4b4nsq.c	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ ℕ)
140	139	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2)) → 𝐶 ∈ ℕ)
141		simpr 490	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2)) → ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2))
142	136, 138, 140, 141	flt4lem6 28003	. . . . . 6 ⊢ ((𝜑 ∧ ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2)) → (((𝐴 / (𝐴 gcd 𝐵)) ∈ ℕ ∧ (𝐵 / (𝐴 gcd 𝐵)) ∈ ℕ ∧ (𝐶 / ((𝐴 gcd 𝐵)↑2)) ∈ ℕ) ∧ (((𝐴 / (𝐴 gcd 𝐵))↑4) + ((𝐵 / (𝐴 gcd 𝐵))↑4)) = ((𝐶 / ((𝐴 gcd 𝐵)↑2))↑2)))
143	142	simpld 500	. . . . 5 ⊢ ((𝜑 ∧ ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2)) → ((𝐴 / (𝐴 gcd 𝐵)) ∈ ℕ ∧ (𝐵 / (𝐴 gcd 𝐵)) ∈ ℕ ∧ (𝐶 / ((𝐴 gcd 𝐵)↑2)) ∈ ℕ))
144	143	simp1d 1160	. . . 4 ⊢ ((𝜑 ∧ ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2)) → (𝐴 / (𝐴 gcd 𝐵)) ∈ ℕ)
145	143	simp2d 1161	. . . 4 ⊢ ((𝜑 ∧ ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2)) → (𝐵 / (𝐴 gcd 𝐵)) ∈ ℕ)
146	143	simp3d 1162	. . . 4 ⊢ ((𝜑 ∧ ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2)) → (𝐶 / ((𝐴 gcd 𝐵)↑2)) ∈ ℕ)
147	135	nnzd 12732	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℤ)
148	147	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2)) → 𝐴 ∈ ℤ)
149	137	nnzd 12732	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℤ)
150	149	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2)) → 𝐵 ∈ ℤ)
151	137	nnne0d 12401	. . . . . . 7 ⊢ (𝜑 → 𝐵 ≠ 0)
152	151	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2)) → 𝐵 ≠ 0)
153		divgcdcoprm0 16855	. . . . . 6 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) → ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1)
154	148, 150, 152, 153	syl3anc 1398	. . . . 5 ⊢ ((𝜑 ∧ ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2)) → ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1)
155	142	simprd 501	. . . . 5 ⊢ ((𝜑 ∧ ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2)) → (((𝐴 / (𝐴 gcd 𝐵))↑4) + ((𝐵 / (𝐴 gcd 𝐵))↑4)) = ((𝐶 / ((𝐴 gcd 𝐵)↑2))↑2))
156	154, 155	jca 521	. . . 4 ⊢ ((𝜑 ∧ ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2)) → (((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1 ∧ (((𝐴 / (𝐴 gcd 𝐵))↑4) + ((𝐵 / (𝐴 gcd 𝐵))↑4)) = ((𝐶 / ((𝐴 gcd 𝐵)↑2))↑2)))
157	125, 131, 134, 144, 145, 146, 156	3rspcedvdw 3597	. . 3 ⊢ ((𝜑 ∧ ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2)) → ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ∃𝑐 ∈ ℕ ((𝑎 gcd 𝑏) = 1 ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2)))
158	119, 157	mtand 828	. 2 ⊢ (𝜑 → ¬ ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2))
159	158	neqned 2966	1 ⊢ (𝜑 → ((𝐴↑4) + (𝐵↑4)) ≠ (𝐶↑2))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1569 ∈ wcel 2146 ≠ wne 2959 ∀wral 3080 ∃wrex 3090 {crab 3416 ⊆ wss 3900 ∅c0 4281 class class class wbr 5106 ‘cfv 6547 (class class class)co 7430 0cc0 11213 1c1 11214 + caddc 11216 < clt 11356 / cdiv 11986 ℕcn 12348 2c2 12410 4c4 12412 ℕ₀cn0 12619 ℤcz 12706 ℤ_≥cuz 12978 ↑cexp 14217 ∥ cdvds 16437 gcd cgcd 16679

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1944 ax-6 2001 ax-7 2042 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2196 ax-12 2215 ax-ext 2735 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7761 ax-cnex 11269 ax-resscn 11270 ax-1cn 11271 ax-icn 11272 ax-addcl 11273 ax-addrcl 11274 ax-mulcl 11275 ax-mulrcl 11276 ax-mulcom 11277 ax-addass 11278 ax-mulass 11279 ax-distr 11280 ax-i2m1 11281 ax-1ne0 11282 ax-1rid 11283 ax-rnegex 11284 ax-rrecex 11285 ax-cnre 11286 ax-pre-lttri 11287 ax-pre-lttrn 11288 ax-pre-ltadd 11289 ax-pre-mulgt0 11290 ax-pre-sup 11291

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2101 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-iun 4956 df-br 5107 df-opab 5171 df-mpt 5190 df-tr 5216 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6311 df-ord 6372 df-on 6373 df-lim 6374 df-suc 6375 df-iota 6501 df-fun 6549 df-fn 6550 df-f 6551 df-f1 6552 df-fo 6553 df-f1o 6554 df-fv 6555 df-riota 7387 df-ov 7433 df-oprab 7434 df-mpo 7435 df-om 7888 df-1st 8011 df-2nd 8012 df-frecs 8313 df-wrecs 8344 df-recs 8393 df-rdg 8432 df-1o 8490 df-2o 8491 df-er 8731 df-en 8988 df-dom 8989 df-sdom 8990 df-fin 8991 df-sup 9447 df-inf 9448 df-pnf 11358 df-mnf 11359 df-xr 11360 df-ltxr 11361 df-le 11362 df-sub 11556 df-neg 11557 df-div 11987 df-nn 12349 df-2 12418 df-3 12419 df-4 12420 df-n0 12620 df-z 12707 df-uz 12979 df-q 13089 df-rp 13134 df-fz 13653 df-fl 13945 df-mod 14023 df-seq 14158 df-exp 14218 df-cj 15281 df-re 15282 df-im 15283 df-sqrt 15417 df-abs 15418 df-dvds 16438 df-gcd 16680 df-prm 16862 df-numer 16926 df-denom 16927

This theorem is used by: flt4 28006

W3C validator