Users' Mathboxes Mathbox for Steven Nguyen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  nna4b4nsq Structured version   Visualization version   GIF version

Theorem nna4b4nsq 40497
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.
StepHypRef Expression
1 nna4b4nsq.c . 2 (𝜑𝐶 ∈ ℕ)
2 oveq1 7282 . . . . . . . . 9 (𝑎 = 𝐴 → (𝑎↑4) = (𝐴↑4))
32oveq1d 7290 . . . . . . . 8 (𝑎 = 𝐴 → ((𝑎↑4) + (𝑏↑4)) = ((𝐴↑4) + (𝑏↑4)))
43eqeq1d 2740 . . . . . . 7 (𝑎 = 𝐴 → (((𝑎↑4) + (𝑏↑4)) = (𝑐↑2) ↔ ((𝐴↑4) + (𝑏↑4)) = (𝑐↑2)))
5 oveq1 7282 . . . . . . . . 9 (𝑏 = 𝐵 → (𝑏↑4) = (𝐵↑4))
65oveq2d 7291 . . . . . . . 8 (𝑏 = 𝐵 → ((𝐴↑4) + (𝑏↑4)) = ((𝐴↑4) + (𝐵↑4)))
76eqeq1d 2740 . . . . . . 7 (𝑏 = 𝐵 → (((𝐴↑4) + (𝑏↑4)) = (𝑐↑2) ↔ ((𝐴↑4) + (𝐵↑4)) = (𝑐↑2)))
8 nna4b4nsq.a . . . . . . . 8 (𝜑𝐴 ∈ ℕ)
98ad2antrr 723 . . . . . . 7 (((𝜑𝑐 ∈ ℕ) ∧ ((𝐴↑4) + (𝐵↑4)) = (𝑐↑2)) → 𝐴 ∈ ℕ)
10 nna4b4nsq.b . . . . . . . 8 (𝜑𝐵 ∈ ℕ)
1110ad2antrr 723 . . . . . . 7 (((𝜑𝑐 ∈ ℕ) ∧ ((𝐴↑4) + (𝐵↑4)) = (𝑐↑2)) → 𝐵 ∈ ℕ)
12 simpr 485 . . . . . . 7 (((𝜑𝑐 ∈ ℕ) ∧ ((𝐴↑4) + (𝐵↑4)) = (𝑐↑2)) → ((𝐴↑4) + (𝐵↑4)) = (𝑐↑2))
134, 7, 9, 11, 122rspcedvdw 40180 . . . . . 6 (((𝜑𝑐 ∈ ℕ) ∧ ((𝐴↑4) + (𝐵↑4)) = (𝑐↑2)) → ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))
1413ex 413 . . . . 5 ((𝜑𝑐 ∈ ℕ) → (((𝐴↑4) + (𝐵↑4)) = (𝑐↑2) → ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2)))
1514ss2rabdv 4009 . . . 4 (𝜑 → {𝑐 ∈ ℕ ∣ ((𝐴↑4) + (𝐵↑4)) = (𝑐↑2)} ⊆ {𝑐 ∈ ℕ ∣ ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2)})
16 oveq1 7282 . . . . . . . . . . 11 (𝑓 = 𝑖 → (𝑓↑2) = (𝑖↑2))
1716eqeq2d 2749 . . . . . . . . . 10 (𝑓 = 𝑖 → (((𝑔↑4) + (↑4)) = (𝑓↑2) ↔ ((𝑔↑4) + (↑4)) = (𝑖↑2)))
1817anbi2d 629 . . . . . . . . 9 (𝑓 = 𝑖 → (((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2)) ↔ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑖↑2))))
1918anbi2d 629 . . . . . . . 8 (𝑓 = 𝑖 → ((¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2))) ↔ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑖↑2)))))
20192rexbidv 3229 . . . . . . 7 (𝑓 = 𝑖 → (∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2))) ↔ ∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑖↑2)))))
21 oveq1 7282 . . . . . . . . . . 11 (𝑓 = 𝑙 → (𝑓↑2) = (𝑙↑2))
2221eqeq2d 2749 . . . . . . . . . 10 (𝑓 = 𝑙 → (((𝑔↑4) + (↑4)) = (𝑓↑2) ↔ ((𝑔↑4) + (↑4)) = (𝑙↑2)))
2322anbi2d 629 . . . . . . . . 9 (𝑓 = 𝑙 → (((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2)) ↔ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑙↑2))))
2423anbi2d 629 . . . . . . . 8 (𝑓 = 𝑙 → ((¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2))) ↔ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑙↑2)))))
25242rexbidv 3229 . . . . . . 7 (𝑓 = 𝑙 → (∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2))) ↔ ∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑙↑2)))))
26 nnuz 12621 . . . . . . . . 9 ℕ = (ℤ‘1)
2726eqimssi 3979 . . . . . . . 8 ℕ ⊆ (ℤ‘1)
2827a1i 11 . . . . . . 7 (𝜑 → ℕ ⊆ (ℤ‘1))
29 breq2 5078 . . . . . . . . . . . 12 (𝑔 = 𝑗 → (2 ∥ 𝑔 ↔ 2 ∥ 𝑗))
3029notbid 318 . . . . . . . . . . 11 (𝑔 = 𝑗 → (¬ 2 ∥ 𝑔 ↔ ¬ 2 ∥ 𝑗))
31 oveq1 7282 . . . . . . . . . . . . 13 (𝑔 = 𝑗 → (𝑔 gcd ) = (𝑗 gcd ))
3231eqeq1d 2740 . . . . . . . . . . . 12 (𝑔 = 𝑗 → ((𝑔 gcd ) = 1 ↔ (𝑗 gcd ) = 1))
33 oveq1 7282 . . . . . . . . . . . . . 14 (𝑔 = 𝑗 → (𝑔↑4) = (𝑗↑4))
3433oveq1d 7290 . . . . . . . . . . . . 13 (𝑔 = 𝑗 → ((𝑔↑4) + (↑4)) = ((𝑗↑4) + (↑4)))
3534eqeq1d 2740 . . . . . . . . . . . 12 (𝑔 = 𝑗 → (((𝑔↑4) + (↑4)) = (𝑖↑2) ↔ ((𝑗↑4) + (↑4)) = (𝑖↑2)))
3632, 35anbi12d 631 . . . . . . . . . . 11 (𝑔 = 𝑗 → (((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑖↑2)) ↔ ((𝑗 gcd ) = 1 ∧ ((𝑗↑4) + (↑4)) = (𝑖↑2))))
3730, 36anbi12d 631 . . . . . . . . . 10 (𝑔 = 𝑗 → ((¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑖↑2))) ↔ (¬ 2 ∥ 𝑗 ∧ ((𝑗 gcd ) = 1 ∧ ((𝑗↑4) + (↑4)) = (𝑖↑2)))))
38 oveq2 7283 . . . . . . . . . . . . 13 ( = 𝑘 → (𝑗 gcd ) = (𝑗 gcd 𝑘))
3938eqeq1d 2740 . . . . . . . . . . . 12 ( = 𝑘 → ((𝑗 gcd ) = 1 ↔ (𝑗 gcd 𝑘) = 1))
40 oveq1 7282 . . . . . . . . . . . . . 14 ( = 𝑘 → (↑4) = (𝑘↑4))
4140oveq2d 7291 . . . . . . . . . . . . 13 ( = 𝑘 → ((𝑗↑4) + (↑4)) = ((𝑗↑4) + (𝑘↑4)))
4241eqeq1d 2740 . . . . . . . . . . . 12 ( = 𝑘 → (((𝑗↑4) + (↑4)) = (𝑖↑2) ↔ ((𝑗↑4) + (𝑘↑4)) = (𝑖↑2)))
4339, 42anbi12d 631 . . . . . . . . . . 11 ( = 𝑘 → (((𝑗 gcd ) = 1 ∧ ((𝑗↑4) + (↑4)) = (𝑖↑2)) ↔ ((𝑗 gcd 𝑘) = 1 ∧ ((𝑗↑4) + (𝑘↑4)) = (𝑖↑2))))
4443anbi2d 629 . . . . . . . . . 10 ( = 𝑘 → ((¬ 2 ∥ 𝑗 ∧ ((𝑗 gcd ) = 1 ∧ ((𝑗↑4) + (↑4)) = (𝑖↑2))) ↔ (¬ 2 ∥ 𝑗 ∧ ((𝑗 gcd 𝑘) = 1 ∧ ((𝑗↑4) + (𝑘↑4)) = (𝑖↑2)))))
4537, 44cbvrex2vw 3397 . . . . . . . . 9 (∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑖↑2))) ↔ ∃𝑗 ∈ ℕ ∃𝑘 ∈ ℕ (¬ 2 ∥ 𝑗 ∧ ((𝑗 gcd 𝑘) = 1 ∧ ((𝑗↑4) + (𝑘↑4)) = (𝑖↑2))))
46 simplrl 774 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ ℕ) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) ∧ (¬ 2 ∥ 𝑗 ∧ ((𝑗 gcd 𝑘) = 1 ∧ ((𝑗↑4) + (𝑘↑4)) = (𝑖↑2)))) → 𝑗 ∈ ℕ)
47 simplrr 775 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ ℕ) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) ∧ (¬ 2 ∥ 𝑗 ∧ ((𝑗 gcd 𝑘) = 1 ∧ ((𝑗↑4) + (𝑘↑4)) = (𝑖↑2)))) → 𝑘 ∈ ℕ)
48 simpllr 773 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ ℕ) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) ∧ (¬ 2 ∥ 𝑗 ∧ ((𝑗 gcd 𝑘) = 1 ∧ ((𝑗↑4) + (𝑘↑4)) = (𝑖↑2)))) → 𝑖 ∈ ℕ)
49 simprl 768 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ ℕ) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) ∧ (¬ 2 ∥ 𝑗 ∧ ((𝑗 gcd 𝑘) = 1 ∧ ((𝑗↑4) + (𝑘↑4)) = (𝑖↑2)))) → ¬ 2 ∥ 𝑗)
50 simprrl 778 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ ℕ) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) ∧ (¬ 2 ∥ 𝑗 ∧ ((𝑗 gcd 𝑘) = 1 ∧ ((𝑗↑4) + (𝑘↑4)) = (𝑖↑2)))) → (𝑗 gcd 𝑘) = 1)
51 simprrr 779 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ ℕ) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) ∧ (¬ 2 ∥ 𝑗 ∧ ((𝑗 gcd 𝑘) = 1 ∧ ((𝑗↑4) + (𝑘↑4)) = (𝑖↑2)))) → ((𝑗↑4) + (𝑘↑4)) = (𝑖↑2))
5246, 47, 48, 49, 50, 51flt4lem7 40496 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ ℕ) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) ∧ (¬ 2 ∥ 𝑗 ∧ ((𝑗 gcd 𝑘) = 1 ∧ ((𝑗↑4) + (𝑘↑4)) = (𝑖↑2)))) → ∃𝑙 ∈ ℕ (∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝑖))
5352ex 413 . . . . . . . . . 10 (((𝜑𝑖 ∈ ℕ) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((¬ 2 ∥ 𝑗 ∧ ((𝑗 gcd 𝑘) = 1 ∧ ((𝑗↑4) + (𝑘↑4)) = (𝑖↑2))) → ∃𝑙 ∈ ℕ (∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝑖)))
5453rexlimdvva 3223 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ) → (∃𝑗 ∈ ℕ ∃𝑘 ∈ ℕ (¬ 2 ∥ 𝑗 ∧ ((𝑗 gcd 𝑘) = 1 ∧ ((𝑗↑4) + (𝑘↑4)) = (𝑖↑2))) → ∃𝑙 ∈ ℕ (∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝑖)))
5545, 54syl5bi 241 . . . . . . . 8 ((𝜑𝑖 ∈ ℕ) → (∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑖↑2))) → ∃𝑙 ∈ ℕ (∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝑖)))
5655impr 455 . . . . . . 7 ((𝜑 ∧ (𝑖 ∈ ℕ ∧ ∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑖↑2))))) → ∃𝑙 ∈ ℕ (∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝑖))
5720, 25, 28, 56infdesc 40480 . . . . . 6 (𝜑 → {𝑓 ∈ ℕ ∣ ∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2)))} = ∅)
58 breq2 5078 . . . . . . . . . . . . . . . 16 (𝑔 = 𝑑 → (2 ∥ 𝑔 ↔ 2 ∥ 𝑑))
5958notbid 318 . . . . . . . . . . . . . . 15 (𝑔 = 𝑑 → (¬ 2 ∥ 𝑔 ↔ ¬ 2 ∥ 𝑑))
60 oveq1 7282 . . . . . . . . . . . . . . . . 17 (𝑔 = 𝑑 → (𝑔 gcd ) = (𝑑 gcd ))
6160eqeq1d 2740 . . . . . . . . . . . . . . . 16 (𝑔 = 𝑑 → ((𝑔 gcd ) = 1 ↔ (𝑑 gcd ) = 1))
62 oveq1 7282 . . . . . . . . . . . . . . . . . 18 (𝑔 = 𝑑 → (𝑔↑4) = (𝑑↑4))
6362oveq1d 7290 . . . . . . . . . . . . . . . . 17 (𝑔 = 𝑑 → ((𝑔↑4) + (↑4)) = ((𝑑↑4) + (↑4)))
6463eqeq1d 2740 . . . . . . . . . . . . . . . 16 (𝑔 = 𝑑 → (((𝑔↑4) + (↑4)) = (𝑓↑2) ↔ ((𝑑↑4) + (↑4)) = (𝑓↑2)))
6561, 64anbi12d 631 . . . . . . . . . . . . . . 15 (𝑔 = 𝑑 → (((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2)) ↔ ((𝑑 gcd ) = 1 ∧ ((𝑑↑4) + (↑4)) = (𝑓↑2))))
6659, 65anbi12d 631 . . . . . . . . . . . . . 14 (𝑔 = 𝑑 → ((¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2))) ↔ (¬ 2 ∥ 𝑑 ∧ ((𝑑 gcd ) = 1 ∧ ((𝑑↑4) + (↑4)) = (𝑓↑2)))))
67 oveq2 7283 . . . . . . . . . . . . . . . . 17 ( = 𝑒 → (𝑑 gcd ) = (𝑑 gcd 𝑒))
6867eqeq1d 2740 . . . . . . . . . . . . . . . 16 ( = 𝑒 → ((𝑑 gcd ) = 1 ↔ (𝑑 gcd 𝑒) = 1))
69 oveq1 7282 . . . . . . . . . . . . . . . . . 18 ( = 𝑒 → (↑4) = (𝑒↑4))
7069oveq2d 7291 . . . . . . . . . . . . . . . . 17 ( = 𝑒 → ((𝑑↑4) + (↑4)) = ((𝑑↑4) + (𝑒↑4)))
7170eqeq1d 2740 . . . . . . . . . . . . . . . 16 ( = 𝑒 → (((𝑑↑4) + (↑4)) = (𝑓↑2) ↔ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2)))
7268, 71anbi12d 631 . . . . . . . . . . . . . . 15 ( = 𝑒 → (((𝑑 gcd ) = 1 ∧ ((𝑑↑4) + (↑4)) = (𝑓↑2)) ↔ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))))
7372anbi2d 629 . . . . . . . . . . . . . 14 ( = 𝑒 → ((¬ 2 ∥ 𝑑 ∧ ((𝑑 gcd ) = 1 ∧ ((𝑑↑4) + (↑4)) = (𝑓↑2))) ↔ (¬ 2 ∥ 𝑑 ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2)))))
74 simprl 768 . . . . . . . . . . . . . . 15 (((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) → 𝑑 ∈ ℕ)
7574ad2antrr 723 . . . . . . . . . . . . . 14 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑑) → 𝑑 ∈ ℕ)
76 simprr 770 . . . . . . . . . . . . . . 15 (((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) → 𝑒 ∈ ℕ)
7776ad2antrr 723 . . . . . . . . . . . . . 14 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑑) → 𝑒 ∈ ℕ)
78 simpr 485 . . . . . . . . . . . . . . 15 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑑) → ¬ 2 ∥ 𝑑)
79 simplr 766 . . . . . . . . . . . . . . 15 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑑) → ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2)))
8078, 79jca 512 . . . . . . . . . . . . . 14 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑑) → (¬ 2 ∥ 𝑑 ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))))
8166, 73, 75, 77, 802rspcedvdw 40180 . . . . . . . . . . . . 13 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑑) → ∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2))))
82 breq2 5078 . . . . . . . . . . . . . . . 16 (𝑔 = 𝑒 → (2 ∥ 𝑔 ↔ 2 ∥ 𝑒))
8382notbid 318 . . . . . . . . . . . . . . 15 (𝑔 = 𝑒 → (¬ 2 ∥ 𝑔 ↔ ¬ 2 ∥ 𝑒))
84 oveq1 7282 . . . . . . . . . . . . . . . . 17 (𝑔 = 𝑒 → (𝑔 gcd ) = (𝑒 gcd ))
8584eqeq1d 2740 . . . . . . . . . . . . . . . 16 (𝑔 = 𝑒 → ((𝑔 gcd ) = 1 ↔ (𝑒 gcd ) = 1))
86 oveq1 7282 . . . . . . . . . . . . . . . . . 18 (𝑔 = 𝑒 → (𝑔↑4) = (𝑒↑4))
8786oveq1d 7290 . . . . . . . . . . . . . . . . 17 (𝑔 = 𝑒 → ((𝑔↑4) + (↑4)) = ((𝑒↑4) + (↑4)))
8887eqeq1d 2740 . . . . . . . . . . . . . . . 16 (𝑔 = 𝑒 → (((𝑔↑4) + (↑4)) = (𝑓↑2) ↔ ((𝑒↑4) + (↑4)) = (𝑓↑2)))
8985, 88anbi12d 631 . . . . . . . . . . . . . . 15 (𝑔 = 𝑒 → (((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2)) ↔ ((𝑒 gcd ) = 1 ∧ ((𝑒↑4) + (↑4)) = (𝑓↑2))))
9083, 89anbi12d 631 . . . . . . . . . . . . . 14 (𝑔 = 𝑒 → ((¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2))) ↔ (¬ 2 ∥ 𝑒 ∧ ((𝑒 gcd ) = 1 ∧ ((𝑒↑4) + (↑4)) = (𝑓↑2)))))
91 oveq2 7283 . . . . . . . . . . . . . . . . 17 ( = 𝑑 → (𝑒 gcd ) = (𝑒 gcd 𝑑))
9291eqeq1d 2740 . . . . . . . . . . . . . . . 16 ( = 𝑑 → ((𝑒 gcd ) = 1 ↔ (𝑒 gcd 𝑑) = 1))
93 oveq1 7282 . . . . . . . . . . . . . . . . . 18 ( = 𝑑 → (↑4) = (𝑑↑4))
9493oveq2d 7291 . . . . . . . . . . . . . . . . 17 ( = 𝑑 → ((𝑒↑4) + (↑4)) = ((𝑒↑4) + (𝑑↑4)))
9594eqeq1d 2740 . . . . . . . . . . . . . . . 16 ( = 𝑑 → (((𝑒↑4) + (↑4)) = (𝑓↑2) ↔ ((𝑒↑4) + (𝑑↑4)) = (𝑓↑2)))
9692, 95anbi12d 631 . . . . . . . . . . . . . . 15 ( = 𝑑 → (((𝑒 gcd ) = 1 ∧ ((𝑒↑4) + (↑4)) = (𝑓↑2)) ↔ ((𝑒 gcd 𝑑) = 1 ∧ ((𝑒↑4) + (𝑑↑4)) = (𝑓↑2))))
9796anbi2d 629 . . . . . . . . . . . . . 14 ( = 𝑑 → ((¬ 2 ∥ 𝑒 ∧ ((𝑒 gcd ) = 1 ∧ ((𝑒↑4) + (↑4)) = (𝑓↑2))) ↔ (¬ 2 ∥ 𝑒 ∧ ((𝑒 gcd 𝑑) = 1 ∧ ((𝑒↑4) + (𝑑↑4)) = (𝑓↑2)))))
9876ad2antrr 723 . . . . . . . . . . . . . 14 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑒) → 𝑒 ∈ ℕ)
9974ad2antrr 723 . . . . . . . . . . . . . 14 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑒) → 𝑑 ∈ ℕ)
100 simpr 485 . . . . . . . . . . . . . . 15 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑒) → ¬ 2 ∥ 𝑒)
10198nnzd 12425 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑒) → 𝑒 ∈ ℤ)
10299nnzd 12425 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑒) → 𝑑 ∈ ℤ)
103101, 102gcdcomd 16221 . . . . . . . . . . . . . . . 16 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑒) → (𝑒 gcd 𝑑) = (𝑑 gcd 𝑒))
104 simplrl 774 . . . . . . . . . . . . . . . 16 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑒) → (𝑑 gcd 𝑒) = 1)
105103, 104eqtrd 2778 . . . . . . . . . . . . . . 15 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑒) → (𝑒 gcd 𝑑) = 1)
106 4nn0 12252 . . . . . . . . . . . . . . . . . . . 20 4 ∈ ℕ0
107106a1i 11 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑒) → 4 ∈ ℕ0)
10898, 107nnexpcld 13960 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑒) → (𝑒↑4) ∈ ℕ)
109108nncnd 11989 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑒) → (𝑒↑4) ∈ ℂ)
11099, 107nnexpcld 13960 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑒) → (𝑑↑4) ∈ ℕ)
111110nncnd 11989 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑒) → (𝑑↑4) ∈ ℂ)
112109, 111addcomd 11177 . . . . . . . . . . . . . . . 16 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑒) → ((𝑒↑4) + (𝑑↑4)) = ((𝑑↑4) + (𝑒↑4)))
113 simplrr 775 . . . . . . . . . . . . . . . 16 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑒) → ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))
114112, 113eqtrd 2778 . . . . . . . . . . . . . . 15 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑒) → ((𝑒↑4) + (𝑑↑4)) = (𝑓↑2))
115100, 105, 114jca32 516 . . . . . . . . . . . . . 14 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑒) → (¬ 2 ∥ 𝑒 ∧ ((𝑒 gcd 𝑑) = 1 ∧ ((𝑒↑4) + (𝑑↑4)) = (𝑓↑2))))
11690, 97, 98, 99, 1152rspcedvdw 40180 . . . . . . . . . . . . 13 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑒) → ∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2))))
11774ad2antrr 723 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → 𝑑 ∈ ℕ)
118117nnsqcld 13959 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → (𝑑↑2) ∈ ℕ)
11976ad2antrr 723 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → 𝑒 ∈ ℕ)
120119nnsqcld 13959 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → (𝑒↑2) ∈ ℕ)
121 simp-4r 781 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → 𝑓 ∈ ℕ)
122 2z 12352 . . . . . . . . . . . . . . . . . . 19 2 ∈ ℤ
123 simplrl 774 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) → 𝑑 ∈ ℕ)
124123nnzd 12425 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) → 𝑑 ∈ ℤ)
125 2nn 12046 . . . . . . . . . . . . . . . . . . . 20 2 ∈ ℕ
126125a1i 11 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) → 2 ∈ ℕ)
127 dvdsexp2im 16036 . . . . . . . . . . . . . . . . . . 19 ((2 ∈ ℤ ∧ 𝑑 ∈ ℤ ∧ 2 ∈ ℕ) → (2 ∥ 𝑑 → 2 ∥ (𝑑↑2)))
128122, 124, 126, 127mp3an2i 1465 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) → (2 ∥ 𝑑 → 2 ∥ (𝑑↑2)))
129128imp 407 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → 2 ∥ (𝑑↑2))
130 2nn0 12250 . . . . . . . . . . . . . . . . . . 19 2 ∈ ℕ0
131130a1i 11 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → 2 ∈ ℕ0)
132117nncnd 11989 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → 𝑑 ∈ ℂ)
133132flt4lem 40482 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → (𝑑↑4) = ((𝑑↑2)↑2))
134119nncnd 11989 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → 𝑒 ∈ ℂ)
135134flt4lem 40482 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → (𝑒↑4) = ((𝑒↑2)↑2))
136133, 135oveq12d 7293 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → ((𝑑↑4) + (𝑒↑4)) = (((𝑑↑2)↑2) + ((𝑒↑2)↑2)))
137 simplrr 775 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))
138136, 137eqtr3d 2780 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → (((𝑑↑2)↑2) + ((𝑒↑2)↑2)) = (𝑓↑2))
139 simplrl 774 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → (𝑑 gcd 𝑒) = 1)
140125a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → 2 ∈ ℕ)
141 rppwr 16269 . . . . . . . . . . . . . . . . . . . 20 ((𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ ∧ 2 ∈ ℕ) → ((𝑑 gcd 𝑒) = 1 → ((𝑑↑2) gcd (𝑒↑2)) = 1))
142117, 119, 140, 141syl3anc 1370 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → ((𝑑 gcd 𝑒) = 1 → ((𝑑↑2) gcd (𝑒↑2)) = 1))
143139, 142mpd 15 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → ((𝑑↑2) gcd (𝑒↑2)) = 1)
144118, 120, 121, 131, 138, 143fltaccoprm 40477 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → ((𝑑↑2) gcd 𝑓) = 1)
145118, 120, 121, 129, 144, 138flt4lem2 40484 . . . . . . . . . . . . . . . 16 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → ¬ 2 ∥ (𝑒↑2))
146119nnzd 12425 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → 𝑒 ∈ ℤ)
147 dvdsexp2im 16036 . . . . . . . . . . . . . . . . 17 ((2 ∈ ℤ ∧ 𝑒 ∈ ℤ ∧ 2 ∈ ℕ) → (2 ∥ 𝑒 → 2 ∥ (𝑒↑2)))
148122, 146, 140, 147mp3an2i 1465 . . . . . . . . . . . . . . . 16 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → (2 ∥ 𝑒 → 2 ∥ (𝑒↑2)))
149145, 148mtod 197 . . . . . . . . . . . . . . 15 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → ¬ 2 ∥ 𝑒)
150149ex 413 . . . . . . . . . . . . . 14 ((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) → (2 ∥ 𝑑 → ¬ 2 ∥ 𝑒))
151 imor 850 . . . . . . . . . . . . . 14 ((2 ∥ 𝑑 → ¬ 2 ∥ 𝑒) ↔ (¬ 2 ∥ 𝑑 ∨ ¬ 2 ∥ 𝑒))
152150, 151sylib 217 . . . . . . . . . . . . 13 ((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) → (¬ 2 ∥ 𝑑 ∨ ¬ 2 ∥ 𝑒))
15381, 116, 152mpjaodan 956 . . . . . . . . . . . 12 ((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) → ∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2))))
154153ex 413 . . . . . . . . . . 11 (((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) → (((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2)) → ∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2)))))
155154rexlimdvva 3223 . . . . . . . . . 10 ((𝜑𝑓 ∈ ℕ) → (∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2)) → ∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2)))))
156155reximdva 3203 . . . . . . . . 9 (𝜑 → (∃𝑓 ∈ ℕ ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2)) → ∃𝑓 ∈ ℕ ∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2)))))
157156con3d 152 . . . . . . . 8 (𝜑 → (¬ ∃𝑓 ∈ ℕ ∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2))) → ¬ ∃𝑓 ∈ ℕ ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))))
158 ralnex 3167 . . . . . . . 8 (∀𝑓 ∈ ℕ ¬ ∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2))) ↔ ¬ ∃𝑓 ∈ ℕ ∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2))))
159 ralnex 3167 . . . . . . . 8 (∀𝑓 ∈ ℕ ¬ ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2)) ↔ ¬ ∃𝑓 ∈ ℕ ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2)))
160157, 158, 1593imtr4g 296 . . . . . . 7 (𝜑 → (∀𝑓 ∈ ℕ ¬ ∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2))) → ∀𝑓 ∈ ℕ ¬ ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))))
161 rabeq0 4318 . . . . . . 7 ({𝑓 ∈ ℕ ∣ ∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2)))} = ∅ ↔ ∀𝑓 ∈ ℕ ¬ ∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2))))
162 rabeq0 4318 . . . . . . 7 ({𝑓 ∈ ℕ ∣ ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))} = ∅ ↔ ∀𝑓 ∈ ℕ ¬ ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2)))
163160, 161, 1623imtr4g 296 . . . . . 6 (𝜑 → ({𝑓 ∈ ℕ ∣ ∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2)))} = ∅ → {𝑓 ∈ ℕ ∣ ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))} = ∅))
16457, 163mpd 15 . . . . 5 (𝜑 → {𝑓 ∈ ℕ ∣ ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))} = ∅)
165 oveq1 7282 . . . . . . . . . . . . 13 (𝑓 = (𝑐 / ((𝑎 gcd 𝑏)↑2)) → (𝑓↑2) = ((𝑐 / ((𝑎 gcd 𝑏)↑2))↑2))
166165eqeq2d 2749 . . . . . . . . . . . 12 (𝑓 = (𝑐 / ((𝑎 gcd 𝑏)↑2)) → (((𝑑↑4) + (𝑒↑4)) = (𝑓↑2) ↔ ((𝑑↑4) + (𝑒↑4)) = ((𝑐 / ((𝑎 gcd 𝑏)↑2))↑2)))
167166anbi2d 629 . . . . . . . . . . 11 (𝑓 = (𝑐 / ((𝑎 gcd 𝑏)↑2)) → (((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2)) ↔ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = ((𝑐 / ((𝑎 gcd 𝑏)↑2))↑2))))
168 oveq1 7282 . . . . . . . . . . . . 13 (𝑑 = (𝑎 / (𝑎 gcd 𝑏)) → (𝑑 gcd 𝑒) = ((𝑎 / (𝑎 gcd 𝑏)) gcd 𝑒))
169168eqeq1d 2740 . . . . . . . . . . . 12 (𝑑 = (𝑎 / (𝑎 gcd 𝑏)) → ((𝑑 gcd 𝑒) = 1 ↔ ((𝑎 / (𝑎 gcd 𝑏)) gcd 𝑒) = 1))
170 oveq1 7282 . . . . . . . . . . . . . 14 (𝑑 = (𝑎 / (𝑎 gcd 𝑏)) → (𝑑↑4) = ((𝑎 / (𝑎 gcd 𝑏))↑4))
171170oveq1d 7290 . . . . . . . . . . . . 13 (𝑑 = (𝑎 / (𝑎 gcd 𝑏)) → ((𝑑↑4) + (𝑒↑4)) = (((𝑎 / (𝑎 gcd 𝑏))↑4) + (𝑒↑4)))
172171eqeq1d 2740 . . . . . . . . . . . 12 (𝑑 = (𝑎 / (𝑎 gcd 𝑏)) → (((𝑑↑4) + (𝑒↑4)) = ((𝑐 / ((𝑎 gcd 𝑏)↑2))↑2) ↔ (((𝑎 / (𝑎 gcd 𝑏))↑4) + (𝑒↑4)) = ((𝑐 / ((𝑎 gcd 𝑏)↑2))↑2)))
173169, 172anbi12d 631 . . . . . . . . . . 11 (𝑑 = (𝑎 / (𝑎 gcd 𝑏)) → (((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = ((𝑐 / ((𝑎 gcd 𝑏)↑2))↑2)) ↔ (((𝑎 / (𝑎 gcd 𝑏)) gcd 𝑒) = 1 ∧ (((𝑎 / (𝑎 gcd 𝑏))↑4) + (𝑒↑4)) = ((𝑐 / ((𝑎 gcd 𝑏)↑2))↑2))))
174 oveq2 7283 . . . . . . . . . . . . 13 (𝑒 = (𝑏 / (𝑎 gcd 𝑏)) → ((𝑎 / (𝑎 gcd 𝑏)) gcd 𝑒) = ((𝑎 / (𝑎 gcd 𝑏)) gcd (𝑏 / (𝑎 gcd 𝑏))))
175174eqeq1d 2740 . . . . . . . . . . . 12 (𝑒 = (𝑏 / (𝑎 gcd 𝑏)) → (((𝑎 / (𝑎 gcd 𝑏)) gcd 𝑒) = 1 ↔ ((𝑎 / (𝑎 gcd 𝑏)) gcd (𝑏 / (𝑎 gcd 𝑏))) = 1))
176 oveq1 7282 . . . . . . . . . . . . . 14 (𝑒 = (𝑏 / (𝑎 gcd 𝑏)) → (𝑒↑4) = ((𝑏 / (𝑎 gcd 𝑏))↑4))
177176oveq2d 7291 . . . . . . . . . . . . 13 (𝑒 = (𝑏 / (𝑎 gcd 𝑏)) → (((𝑎 / (𝑎 gcd 𝑏))↑4) + (𝑒↑4)) = (((𝑎 / (𝑎 gcd 𝑏))↑4) + ((𝑏 / (𝑎 gcd 𝑏))↑4)))
178177eqeq1d 2740 . . . . . . . . . . . 12 (𝑒 = (𝑏 / (𝑎 gcd 𝑏)) → ((((𝑎 / (𝑎 gcd 𝑏))↑4) + (𝑒↑4)) = ((𝑐 / ((𝑎 gcd 𝑏)↑2))↑2) ↔ (((𝑎 / (𝑎 gcd 𝑏))↑4) + ((𝑏 / (𝑎 gcd 𝑏))↑4)) = ((𝑐 / ((𝑎 gcd 𝑏)↑2))↑2)))
179175, 178anbi12d 631 . . . . . . . . . . 11 (𝑒 = (𝑏 / (𝑎 gcd 𝑏)) → ((((𝑎 / (𝑎 gcd 𝑏)) gcd 𝑒) = 1 ∧ (((𝑎 / (𝑎 gcd 𝑏))↑4) + (𝑒↑4)) = ((𝑐 / ((𝑎 gcd 𝑏)↑2))↑2)) ↔ (((𝑎 / (𝑎 gcd 𝑏)) gcd (𝑏 / (𝑎 gcd 𝑏))) = 1 ∧ (((𝑎 / (𝑎 gcd 𝑏))↑4) + ((𝑏 / (𝑎 gcd 𝑏))↑4)) = ((𝑐 / ((𝑎 gcd 𝑏)↑2))↑2))))
180 simplrr 775 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑐 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ (𝑏 ∈ ℕ ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) → 𝑎 ∈ ℕ)
181 simprl 768 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑐 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ (𝑏 ∈ ℕ ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) → 𝑏 ∈ ℕ)
182 simplrl 774 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑐 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ (𝑏 ∈ ℕ ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) → 𝑐 ∈ ℕ)
183 simprr 770 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑐 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ (𝑏 ∈ ℕ ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) → ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))
184180, 181, 182, 183flt4lem6 40495 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑐 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ (𝑏 ∈ ℕ ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) → (((𝑎 / (𝑎 gcd 𝑏)) ∈ ℕ ∧ (𝑏 / (𝑎 gcd 𝑏)) ∈ ℕ ∧ (𝑐 / ((𝑎 gcd 𝑏)↑2)) ∈ ℕ) ∧ (((𝑎 / (𝑎 gcd 𝑏))↑4) + ((𝑏 / (𝑎 gcd 𝑏))↑4)) = ((𝑐 / ((𝑎 gcd 𝑏)↑2))↑2)))
185184simpld 495 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑐 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ (𝑏 ∈ ℕ ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) → ((𝑎 / (𝑎 gcd 𝑏)) ∈ ℕ ∧ (𝑏 / (𝑎 gcd 𝑏)) ∈ ℕ ∧ (𝑐 / ((𝑎 gcd 𝑏)↑2)) ∈ ℕ))
186185simp3d 1143 . . . . . . . . . . 11 (((𝜑 ∧ (𝑐 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ (𝑏 ∈ ℕ ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) → (𝑐 / ((𝑎 gcd 𝑏)↑2)) ∈ ℕ)
187185simp1d 1141 . . . . . . . . . . 11 (((𝜑 ∧ (𝑐 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ (𝑏 ∈ ℕ ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) → (𝑎 / (𝑎 gcd 𝑏)) ∈ ℕ)
188185simp2d 1142 . . . . . . . . . . 11 (((𝜑 ∧ (𝑐 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ (𝑏 ∈ ℕ ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) → (𝑏 / (𝑎 gcd 𝑏)) ∈ ℕ)
189180nnzd 12425 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑐 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ (𝑏 ∈ ℕ ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) → 𝑎 ∈ ℤ)
190181nnzd 12425 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑐 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ (𝑏 ∈ ℕ ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) → 𝑏 ∈ ℤ)
191181nnne0d 12023 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑐 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ (𝑏 ∈ ℕ ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) → 𝑏 ≠ 0)
192 divgcdcoprm0 16370 . . . . . . . . . . . . 13 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝑏 ≠ 0) → ((𝑎 / (𝑎 gcd 𝑏)) gcd (𝑏 / (𝑎 gcd 𝑏))) = 1)
193189, 190, 191, 192syl3anc 1370 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑐 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ (𝑏 ∈ ℕ ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) → ((𝑎 / (𝑎 gcd 𝑏)) gcd (𝑏 / (𝑎 gcd 𝑏))) = 1)
194184simprd 496 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑐 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ (𝑏 ∈ ℕ ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) → (((𝑎 / (𝑎 gcd 𝑏))↑4) + ((𝑏 / (𝑎 gcd 𝑏))↑4)) = ((𝑐 / ((𝑎 gcd 𝑏)↑2))↑2))
195193, 194jca 512 . . . . . . . . . . 11 (((𝜑 ∧ (𝑐 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ (𝑏 ∈ ℕ ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) → (((𝑎 / (𝑎 gcd 𝑏)) gcd (𝑏 / (𝑎 gcd 𝑏))) = 1 ∧ (((𝑎 / (𝑎 gcd 𝑏))↑4) + ((𝑏 / (𝑎 gcd 𝑏))↑4)) = ((𝑐 / ((𝑎 gcd 𝑏)↑2))↑2)))
196167, 173, 179, 186, 187, 188, 1953rspcedvdw 40181 . . . . . . . . . 10 (((𝜑 ∧ (𝑐 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ (𝑏 ∈ ℕ ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) → ∃𝑓 ∈ ℕ ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2)))
197196rexlimdvaa 3214 . . . . . . . . 9 ((𝜑 ∧ (𝑐 ∈ ℕ ∧ 𝑎 ∈ ℕ)) → (∃𝑏 ∈ ℕ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2) → ∃𝑓 ∈ ℕ ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))))
198197rexlimdvva 3223 . . . . . . . 8 (𝜑 → (∃𝑐 ∈ ℕ ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2) → ∃𝑓 ∈ ℕ ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))))
199198con3d 152 . . . . . . 7 (𝜑 → (¬ ∃𝑓 ∈ ℕ ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2)) → ¬ ∃𝑐 ∈ ℕ ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2)))
200 ralnex 3167 . . . . . . 7 (∀𝑐 ∈ ℕ ¬ ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2) ↔ ¬ ∃𝑐 ∈ ℕ ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))
201199, 159, 2003imtr4g 296 . . . . . 6 (𝜑 → (∀𝑓 ∈ ℕ ¬ ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2)) → ∀𝑐 ∈ ℕ ¬ ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2)))
202 rabeq0 4318 . . . . . 6 ({𝑐 ∈ ℕ ∣ ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2)} = ∅ ↔ ∀𝑐 ∈ ℕ ¬ ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))
203201, 162, 2023imtr4g 296 . . . . 5 (𝜑 → ({𝑓 ∈ ℕ ∣ ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))} = ∅ → {𝑐 ∈ ℕ ∣ ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2)} = ∅))
204164, 203mpd 15 . . . 4 (𝜑 → {𝑐 ∈ ℕ ∣ ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2)} = ∅)
205 sseq0 4333 . . . 4 (({𝑐 ∈ ℕ ∣ ((𝐴↑4) + (𝐵↑4)) = (𝑐↑2)} ⊆ {𝑐 ∈ ℕ ∣ ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2)} ∧ {𝑐 ∈ ℕ ∣ ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2)} = ∅) → {𝑐 ∈ ℕ ∣ ((𝐴↑4) + (𝐵↑4)) = (𝑐↑2)} = ∅)
20615, 204, 205syl2anc 584 . . 3 (𝜑 → {𝑐 ∈ ℕ ∣ ((𝐴↑4) + (𝐵↑4)) = (𝑐↑2)} = ∅)
207 rabeq0 4318 . . 3 ({𝑐 ∈ ℕ ∣ ((𝐴↑4) + (𝐵↑4)) = (𝑐↑2)} = ∅ ↔ ∀𝑐 ∈ ℕ ¬ ((𝐴↑4) + (𝐵↑4)) = (𝑐↑2))
208206, 207sylib 217 . 2 (𝜑 → ∀𝑐 ∈ ℕ ¬ ((𝐴↑4) + (𝐵↑4)) = (𝑐↑2))
209 oveq1 7282 . . . . 5 (𝑐 = 𝐶 → (𝑐↑2) = (𝐶↑2))
210209eqeq2d 2749 . . . 4 (𝑐 = 𝐶 → (((𝐴↑4) + (𝐵↑4)) = (𝑐↑2) ↔ ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2)))
211210necon3bbid 2981 . . 3 (𝑐 = 𝐶 → (¬ ((𝐴↑4) + (𝐵↑4)) = (𝑐↑2) ↔ ((𝐴↑4) + (𝐵↑4)) ≠ (𝐶↑2)))
212211rspcv 3557 . 2 (𝐶 ∈ ℕ → (∀𝑐 ∈ ℕ ¬ ((𝐴↑4) + (𝐵↑4)) = (𝑐↑2) → ((𝐴↑4) + (𝐵↑4)) ≠ (𝐶↑2)))
2131, 208, 212sylc 65 1 (𝜑 → ((𝐴↑4) + (𝐵↑4)) ≠ (𝐶↑2))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  wo 844  w3a 1086   = wceq 1539  wcel 2106  wne 2943  wral 3064  wrex 3065  {crab 3068  wss 3887  c0 4256   class class class wbr 5074  cfv 6433  (class class class)co 7275  0cc0 10871  1c1 10872   + caddc 10874   < clt 11009   / cdiv 11632  cn 11973  2c2 12028  4c4 12030  0cn0 12233  cz 12319  cuz 12582  cexp 13782  cdvds 15963   gcd cgcd 16201
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-cnex 10927  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948  ax-pre-sup 10949
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-om 7713  df-1st 7831  df-2nd 7832  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-1o 8297  df-2o 8298  df-er 8498  df-en 8734  df-dom 8735  df-sdom 8736  df-fin 8737  df-sup 9201  df-inf 9202  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-div 11633  df-nn 11974  df-2 12036  df-3 12037  df-4 12038  df-n0 12234  df-z 12320  df-uz 12583  df-q 12689  df-rp 12731  df-fz 13240  df-fl 13512  df-mod 13590  df-seq 13722  df-exp 13783  df-cj 14810  df-re 14811  df-im 14812  df-sqrt 14946  df-abs 14947  df-dvds 15964  df-gcd 16202  df-prm 16377  df-numer 16439  df-denom 16440
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator