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 40053
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 7171 . . . . . . . . 9 (𝑎 = 𝐴 → (𝑎↑4) = (𝐴↑4))
32oveq1d 7179 . . . . . . . 8 (𝑎 = 𝐴 → ((𝑎↑4) + (𝑏↑4)) = ((𝐴↑4) + (𝑏↑4)))
43eqeq1d 2740 . . . . . . 7 (𝑎 = 𝐴 → (((𝑎↑4) + (𝑏↑4)) = (𝑐↑2) ↔ ((𝐴↑4) + (𝑏↑4)) = (𝑐↑2)))
5 oveq1 7171 . . . . . . . . 9 (𝑏 = 𝐵 → (𝑏↑4) = (𝐵↑4))
65oveq2d 7180 . . . . . . . 8 (𝑏 = 𝐵 → ((𝐴↑4) + (𝑏↑4)) = ((𝐴↑4) + (𝐵↑4)))
76eqeq1d 2740 . . . . . . 7 (𝑏 = 𝐵 → (((𝐴↑4) + (𝑏↑4)) = (𝑐↑2) ↔ ((𝐴↑4) + (𝐵↑4)) = (𝑐↑2)))
8 nna4b4nsq.a . . . . . . . 8 (𝜑𝐴 ∈ ℕ)
98ad2antrr 726 . . . . . . 7 (((𝜑𝑐 ∈ ℕ) ∧ ((𝐴↑4) + (𝐵↑4)) = (𝑐↑2)) → 𝐴 ∈ ℕ)
10 nna4b4nsq.b . . . . . . . 8 (𝜑𝐵 ∈ ℕ)
1110ad2antrr 726 . . . . . . 7 (((𝜑𝑐 ∈ ℕ) ∧ ((𝐴↑4) + (𝐵↑4)) = (𝑐↑2)) → 𝐵 ∈ ℕ)
12 simpr 488 . . . . . . 7 (((𝜑𝑐 ∈ ℕ) ∧ ((𝐴↑4) + (𝐵↑4)) = (𝑐↑2)) → ((𝐴↑4) + (𝐵↑4)) = (𝑐↑2))
134, 7, 9, 11, 122rspcedvdw 39756 . . . . . 6 (((𝜑𝑐 ∈ ℕ) ∧ ((𝐴↑4) + (𝐵↑4)) = (𝑐↑2)) → ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))
1413ex 416 . . . . 5 ((𝜑𝑐 ∈ ℕ) → (((𝐴↑4) + (𝐵↑4)) = (𝑐↑2) → ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2)))
1514ss2rabdv 3963 . . . 4 (𝜑 → {𝑐 ∈ ℕ ∣ ((𝐴↑4) + (𝐵↑4)) = (𝑐↑2)} ⊆ {𝑐 ∈ ℕ ∣ ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2)})
16 oveq1 7171 . . . . . . . . . . 11 (𝑓 = 𝑖 → (𝑓↑2) = (𝑖↑2))
1716eqeq2d 2749 . . . . . . . . . 10 (𝑓 = 𝑖 → (((𝑔↑4) + (↑4)) = (𝑓↑2) ↔ ((𝑔↑4) + (↑4)) = (𝑖↑2)))
1817anbi2d 632 . . . . . . . . 9 (𝑓 = 𝑖 → (((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2)) ↔ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑖↑2))))
1918anbi2d 632 . . . . . . . 8 (𝑓 = 𝑖 → ((¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2))) ↔ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑖↑2)))))
20192rexbidv 3209 . . . . . . 7 (𝑓 = 𝑖 → (∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2))) ↔ ∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑖↑2)))))
21 oveq1 7171 . . . . . . . . . . 11 (𝑓 = 𝑙 → (𝑓↑2) = (𝑙↑2))
2221eqeq2d 2749 . . . . . . . . . 10 (𝑓 = 𝑙 → (((𝑔↑4) + (↑4)) = (𝑓↑2) ↔ ((𝑔↑4) + (↑4)) = (𝑙↑2)))
2322anbi2d 632 . . . . . . . . 9 (𝑓 = 𝑙 → (((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2)) ↔ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑙↑2))))
2423anbi2d 632 . . . . . . . 8 (𝑓 = 𝑙 → ((¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2))) ↔ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑙↑2)))))
25242rexbidv 3209 . . . . . . 7 (𝑓 = 𝑙 → (∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2))) ↔ ∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑙↑2)))))
26 nnuz 12356 . . . . . . . . 9 ℕ = (ℤ‘1)
2726eqimssi 3933 . . . . . . . 8 ℕ ⊆ (ℤ‘1)
2827a1i 11 . . . . . . 7 (𝜑 → ℕ ⊆ (ℤ‘1))
29 breq2 5031 . . . . . . . . . . . 12 (𝑔 = 𝑗 → (2 ∥ 𝑔 ↔ 2 ∥ 𝑗))
3029notbid 321 . . . . . . . . . . 11 (𝑔 = 𝑗 → (¬ 2 ∥ 𝑔 ↔ ¬ 2 ∥ 𝑗))
31 oveq1 7171 . . . . . . . . . . . . 13 (𝑔 = 𝑗 → (𝑔 gcd ) = (𝑗 gcd ))
3231eqeq1d 2740 . . . . . . . . . . . 12 (𝑔 = 𝑗 → ((𝑔 gcd ) = 1 ↔ (𝑗 gcd ) = 1))
33 oveq1 7171 . . . . . . . . . . . . . 14 (𝑔 = 𝑗 → (𝑔↑4) = (𝑗↑4))
3433oveq1d 7179 . . . . . . . . . . . . 13 (𝑔 = 𝑗 → ((𝑔↑4) + (↑4)) = ((𝑗↑4) + (↑4)))
3534eqeq1d 2740 . . . . . . . . . . . 12 (𝑔 = 𝑗 → (((𝑔↑4) + (↑4)) = (𝑖↑2) ↔ ((𝑗↑4) + (↑4)) = (𝑖↑2)))
3632, 35anbi12d 634 . . . . . . . . . . 11 (𝑔 = 𝑗 → (((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑖↑2)) ↔ ((𝑗 gcd ) = 1 ∧ ((𝑗↑4) + (↑4)) = (𝑖↑2))))
3730, 36anbi12d 634 . . . . . . . . . 10 (𝑔 = 𝑗 → ((¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑖↑2))) ↔ (¬ 2 ∥ 𝑗 ∧ ((𝑗 gcd ) = 1 ∧ ((𝑗↑4) + (↑4)) = (𝑖↑2)))))
38 oveq2 7172 . . . . . . . . . . . . 13 ( = 𝑘 → (𝑗 gcd ) = (𝑗 gcd 𝑘))
3938eqeq1d 2740 . . . . . . . . . . . 12 ( = 𝑘 → ((𝑗 gcd ) = 1 ↔ (𝑗 gcd 𝑘) = 1))
40 oveq1 7171 . . . . . . . . . . . . . 14 ( = 𝑘 → (↑4) = (𝑘↑4))
4140oveq2d 7180 . . . . . . . . . . . . 13 ( = 𝑘 → ((𝑗↑4) + (↑4)) = ((𝑗↑4) + (𝑘↑4)))
4241eqeq1d 2740 . . . . . . . . . . . 12 ( = 𝑘 → (((𝑗↑4) + (↑4)) = (𝑖↑2) ↔ ((𝑗↑4) + (𝑘↑4)) = (𝑖↑2)))
4339, 42anbi12d 634 . . . . . . . . . . 11 ( = 𝑘 → (((𝑗 gcd ) = 1 ∧ ((𝑗↑4) + (↑4)) = (𝑖↑2)) ↔ ((𝑗 gcd 𝑘) = 1 ∧ ((𝑗↑4) + (𝑘↑4)) = (𝑖↑2))))
4443anbi2d 632 . . . . . . . . . 10 ( = 𝑘 → ((¬ 2 ∥ 𝑗 ∧ ((𝑗 gcd ) = 1 ∧ ((𝑗↑4) + (↑4)) = (𝑖↑2))) ↔ (¬ 2 ∥ 𝑗 ∧ ((𝑗 gcd 𝑘) = 1 ∧ ((𝑗↑4) + (𝑘↑4)) = (𝑖↑2)))))
4537, 44cbvrex2vw 3362 . . . . . . . . 9 (∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑖↑2))) ↔ ∃𝑗 ∈ ℕ ∃𝑘 ∈ ℕ (¬ 2 ∥ 𝑗 ∧ ((𝑗 gcd 𝑘) = 1 ∧ ((𝑗↑4) + (𝑘↑4)) = (𝑖↑2))))
46 simplrl 777 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ ℕ) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) ∧ (¬ 2 ∥ 𝑗 ∧ ((𝑗 gcd 𝑘) = 1 ∧ ((𝑗↑4) + (𝑘↑4)) = (𝑖↑2)))) → 𝑗 ∈ ℕ)
47 simplrr 778 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ ℕ) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) ∧ (¬ 2 ∥ 𝑗 ∧ ((𝑗 gcd 𝑘) = 1 ∧ ((𝑗↑4) + (𝑘↑4)) = (𝑖↑2)))) → 𝑘 ∈ ℕ)
48 simpllr 776 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ ℕ) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) ∧ (¬ 2 ∥ 𝑗 ∧ ((𝑗 gcd 𝑘) = 1 ∧ ((𝑗↑4) + (𝑘↑4)) = (𝑖↑2)))) → 𝑖 ∈ ℕ)
49 simprl 771 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ ℕ) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) ∧ (¬ 2 ∥ 𝑗 ∧ ((𝑗 gcd 𝑘) = 1 ∧ ((𝑗↑4) + (𝑘↑4)) = (𝑖↑2)))) → ¬ 2 ∥ 𝑗)
50 simprrl 781 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ ℕ) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) ∧ (¬ 2 ∥ 𝑗 ∧ ((𝑗 gcd 𝑘) = 1 ∧ ((𝑗↑4) + (𝑘↑4)) = (𝑖↑2)))) → (𝑗 gcd 𝑘) = 1)
51 simprrr 782 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ ℕ) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) ∧ (¬ 2 ∥ 𝑗 ∧ ((𝑗 gcd 𝑘) = 1 ∧ ((𝑗↑4) + (𝑘↑4)) = (𝑖↑2)))) → ((𝑗↑4) + (𝑘↑4)) = (𝑖↑2))
5246, 47, 48, 49, 50, 51flt4lem7 40052 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ ℕ) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) ∧ (¬ 2 ∥ 𝑗 ∧ ((𝑗 gcd 𝑘) = 1 ∧ ((𝑗↑4) + (𝑘↑4)) = (𝑖↑2)))) → ∃𝑙 ∈ ℕ (∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝑖))
5352ex 416 . . . . . . . . . 10 (((𝜑𝑖 ∈ ℕ) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → ((¬ 2 ∥ 𝑗 ∧ ((𝑗 gcd 𝑘) = 1 ∧ ((𝑗↑4) + (𝑘↑4)) = (𝑖↑2))) → ∃𝑙 ∈ ℕ (∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝑖)))
5453rexlimdvva 3203 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ) → (∃𝑗 ∈ ℕ ∃𝑘 ∈ ℕ (¬ 2 ∥ 𝑗 ∧ ((𝑗 gcd 𝑘) = 1 ∧ ((𝑗↑4) + (𝑘↑4)) = (𝑖↑2))) → ∃𝑙 ∈ ℕ (∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝑖)))
5545, 54syl5bi 245 . . . . . . . 8 ((𝜑𝑖 ∈ ℕ) → (∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑖↑2))) → ∃𝑙 ∈ ℕ (∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝑖)))
5655impr 458 . . . . . . 7 ((𝜑 ∧ (𝑖 ∈ ℕ ∧ ∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑖↑2))))) → ∃𝑙 ∈ ℕ (∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝑖))
5720, 25, 28, 56infdesc 40036 . . . . . 6 (𝜑 → {𝑓 ∈ ℕ ∣ ∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2)))} = ∅)
58 breq2 5031 . . . . . . . . . . . . . . . 16 (𝑔 = 𝑑 → (2 ∥ 𝑔 ↔ 2 ∥ 𝑑))
5958notbid 321 . . . . . . . . . . . . . . 15 (𝑔 = 𝑑 → (¬ 2 ∥ 𝑔 ↔ ¬ 2 ∥ 𝑑))
60 oveq1 7171 . . . . . . . . . . . . . . . . 17 (𝑔 = 𝑑 → (𝑔 gcd ) = (𝑑 gcd ))
6160eqeq1d 2740 . . . . . . . . . . . . . . . 16 (𝑔 = 𝑑 → ((𝑔 gcd ) = 1 ↔ (𝑑 gcd ) = 1))
62 oveq1 7171 . . . . . . . . . . . . . . . . . 18 (𝑔 = 𝑑 → (𝑔↑4) = (𝑑↑4))
6362oveq1d 7179 . . . . . . . . . . . . . . . . 17 (𝑔 = 𝑑 → ((𝑔↑4) + (↑4)) = ((𝑑↑4) + (↑4)))
6463eqeq1d 2740 . . . . . . . . . . . . . . . 16 (𝑔 = 𝑑 → (((𝑔↑4) + (↑4)) = (𝑓↑2) ↔ ((𝑑↑4) + (↑4)) = (𝑓↑2)))
6561, 64anbi12d 634 . . . . . . . . . . . . . . 15 (𝑔 = 𝑑 → (((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2)) ↔ ((𝑑 gcd ) = 1 ∧ ((𝑑↑4) + (↑4)) = (𝑓↑2))))
6659, 65anbi12d 634 . . . . . . . . . . . . . 14 (𝑔 = 𝑑 → ((¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2))) ↔ (¬ 2 ∥ 𝑑 ∧ ((𝑑 gcd ) = 1 ∧ ((𝑑↑4) + (↑4)) = (𝑓↑2)))))
67 oveq2 7172 . . . . . . . . . . . . . . . . 17 ( = 𝑒 → (𝑑 gcd ) = (𝑑 gcd 𝑒))
6867eqeq1d 2740 . . . . . . . . . . . . . . . 16 ( = 𝑒 → ((𝑑 gcd ) = 1 ↔ (𝑑 gcd 𝑒) = 1))
69 oveq1 7171 . . . . . . . . . . . . . . . . . 18 ( = 𝑒 → (↑4) = (𝑒↑4))
7069oveq2d 7180 . . . . . . . . . . . . . . . . 17 ( = 𝑒 → ((𝑑↑4) + (↑4)) = ((𝑑↑4) + (𝑒↑4)))
7170eqeq1d 2740 . . . . . . . . . . . . . . . 16 ( = 𝑒 → (((𝑑↑4) + (↑4)) = (𝑓↑2) ↔ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2)))
7268, 71anbi12d 634 . . . . . . . . . . . . . . 15 ( = 𝑒 → (((𝑑 gcd ) = 1 ∧ ((𝑑↑4) + (↑4)) = (𝑓↑2)) ↔ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))))
7372anbi2d 632 . . . . . . . . . . . . . 14 ( = 𝑒 → ((¬ 2 ∥ 𝑑 ∧ ((𝑑 gcd ) = 1 ∧ ((𝑑↑4) + (↑4)) = (𝑓↑2))) ↔ (¬ 2 ∥ 𝑑 ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2)))))
74 simprl 771 . . . . . . . . . . . . . . 15 (((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) → 𝑑 ∈ ℕ)
7574ad2antrr 726 . . . . . . . . . . . . . 14 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑑) → 𝑑 ∈ ℕ)
76 simprr 773 . . . . . . . . . . . . . . 15 (((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) → 𝑒 ∈ ℕ)
7776ad2antrr 726 . . . . . . . . . . . . . 14 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑑) → 𝑒 ∈ ℕ)
78 simpr 488 . . . . . . . . . . . . . . 15 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑑) → ¬ 2 ∥ 𝑑)
79 simplr 769 . . . . . . . . . . . . . . 15 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑑) → ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2)))
8078, 79jca 515 . . . . . . . . . . . . . 14 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑑) → (¬ 2 ∥ 𝑑 ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))))
8166, 73, 75, 77, 802rspcedvdw 39756 . . . . . . . . . . . . 13 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑑) → ∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2))))
82 breq2 5031 . . . . . . . . . . . . . . . 16 (𝑔 = 𝑒 → (2 ∥ 𝑔 ↔ 2 ∥ 𝑒))
8382notbid 321 . . . . . . . . . . . . . . 15 (𝑔 = 𝑒 → (¬ 2 ∥ 𝑔 ↔ ¬ 2 ∥ 𝑒))
84 oveq1 7171 . . . . . . . . . . . . . . . . 17 (𝑔 = 𝑒 → (𝑔 gcd ) = (𝑒 gcd ))
8584eqeq1d 2740 . . . . . . . . . . . . . . . 16 (𝑔 = 𝑒 → ((𝑔 gcd ) = 1 ↔ (𝑒 gcd ) = 1))
86 oveq1 7171 . . . . . . . . . . . . . . . . . 18 (𝑔 = 𝑒 → (𝑔↑4) = (𝑒↑4))
8786oveq1d 7179 . . . . . . . . . . . . . . . . 17 (𝑔 = 𝑒 → ((𝑔↑4) + (↑4)) = ((𝑒↑4) + (↑4)))
8887eqeq1d 2740 . . . . . . . . . . . . . . . 16 (𝑔 = 𝑒 → (((𝑔↑4) + (↑4)) = (𝑓↑2) ↔ ((𝑒↑4) + (↑4)) = (𝑓↑2)))
8985, 88anbi12d 634 . . . . . . . . . . . . . . 15 (𝑔 = 𝑒 → (((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2)) ↔ ((𝑒 gcd ) = 1 ∧ ((𝑒↑4) + (↑4)) = (𝑓↑2))))
9083, 89anbi12d 634 . . . . . . . . . . . . . 14 (𝑔 = 𝑒 → ((¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2))) ↔ (¬ 2 ∥ 𝑒 ∧ ((𝑒 gcd ) = 1 ∧ ((𝑒↑4) + (↑4)) = (𝑓↑2)))))
91 oveq2 7172 . . . . . . . . . . . . . . . . 17 ( = 𝑑 → (𝑒 gcd ) = (𝑒 gcd 𝑑))
9291eqeq1d 2740 . . . . . . . . . . . . . . . 16 ( = 𝑑 → ((𝑒 gcd ) = 1 ↔ (𝑒 gcd 𝑑) = 1))
93 oveq1 7171 . . . . . . . . . . . . . . . . . 18 ( = 𝑑 → (↑4) = (𝑑↑4))
9493oveq2d 7180 . . . . . . . . . . . . . . . . 17 ( = 𝑑 → ((𝑒↑4) + (↑4)) = ((𝑒↑4) + (𝑑↑4)))
9594eqeq1d 2740 . . . . . . . . . . . . . . . 16 ( = 𝑑 → (((𝑒↑4) + (↑4)) = (𝑓↑2) ↔ ((𝑒↑4) + (𝑑↑4)) = (𝑓↑2)))
9692, 95anbi12d 634 . . . . . . . . . . . . . . 15 ( = 𝑑 → (((𝑒 gcd ) = 1 ∧ ((𝑒↑4) + (↑4)) = (𝑓↑2)) ↔ ((𝑒 gcd 𝑑) = 1 ∧ ((𝑒↑4) + (𝑑↑4)) = (𝑓↑2))))
9796anbi2d 632 . . . . . . . . . . . . . 14 ( = 𝑑 → ((¬ 2 ∥ 𝑒 ∧ ((𝑒 gcd ) = 1 ∧ ((𝑒↑4) + (↑4)) = (𝑓↑2))) ↔ (¬ 2 ∥ 𝑒 ∧ ((𝑒 gcd 𝑑) = 1 ∧ ((𝑒↑4) + (𝑑↑4)) = (𝑓↑2)))))
9876ad2antrr 726 . . . . . . . . . . . . . 14 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑒) → 𝑒 ∈ ℕ)
9974ad2antrr 726 . . . . . . . . . . . . . 14 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑒) → 𝑑 ∈ ℕ)
100 simpr 488 . . . . . . . . . . . . . . 15 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑒) → ¬ 2 ∥ 𝑒)
10198nnzd 12160 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑒) → 𝑒 ∈ ℤ)
10299nnzd 12160 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑒) → 𝑑 ∈ ℤ)
103101, 102gcdcomd 15950 . . . . . . . . . . . . . . . 16 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑒) → (𝑒 gcd 𝑑) = (𝑑 gcd 𝑒))
104 simplrl 777 . . . . . . . . . . . . . . . 16 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑒) → (𝑑 gcd 𝑒) = 1)
105103, 104eqtrd 2773 . . . . . . . . . . . . . . 15 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑒) → (𝑒 gcd 𝑑) = 1)
106 4nn0 11988 . . . . . . . . . . . . . . . . . . . 20 4 ∈ ℕ0
107106a1i 11 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑒) → 4 ∈ ℕ0)
10898, 107nnexpcld 13691 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑒) → (𝑒↑4) ∈ ℕ)
109108nncnd 11725 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑒) → (𝑒↑4) ∈ ℂ)
11099, 107nnexpcld 13691 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑒) → (𝑑↑4) ∈ ℕ)
111110nncnd 11725 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑒) → (𝑑↑4) ∈ ℂ)
112109, 111addcomd 10913 . . . . . . . . . . . . . . . 16 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑒) → ((𝑒↑4) + (𝑑↑4)) = ((𝑑↑4) + (𝑒↑4)))
113 simplrr 778 . . . . . . . . . . . . . . . 16 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑒) → ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))
114112, 113eqtrd 2773 . . . . . . . . . . . . . . 15 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑒) → ((𝑒↑4) + (𝑑↑4)) = (𝑓↑2))
115100, 105, 114jca32 519 . . . . . . . . . . . . . 14 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑒) → (¬ 2 ∥ 𝑒 ∧ ((𝑒 gcd 𝑑) = 1 ∧ ((𝑒↑4) + (𝑑↑4)) = (𝑓↑2))))
11690, 97, 98, 99, 1152rspcedvdw 39756 . . . . . . . . . . . . 13 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ ¬ 2 ∥ 𝑒) → ∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2))))
11774ad2antrr 726 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → 𝑑 ∈ ℕ)
118117nnsqcld 13690 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → (𝑑↑2) ∈ ℕ)
11976ad2antrr 726 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → 𝑒 ∈ ℕ)
120119nnsqcld 13690 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → (𝑒↑2) ∈ ℕ)
121 simp-4r 784 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → 𝑓 ∈ ℕ)
122 2z 12088 . . . . . . . . . . . . . . . . . . 19 2 ∈ ℤ
123 simplrl 777 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) → 𝑑 ∈ ℕ)
124123nnzd 12160 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) → 𝑑 ∈ ℤ)
125 2nn 11782 . . . . . . . . . . . . . . . . . . . 20 2 ∈ ℕ
126125a1i 11 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) → 2 ∈ ℕ)
127 dvdsexp2im 15765 . . . . . . . . . . . . . . . . . . 19 ((2 ∈ ℤ ∧ 𝑑 ∈ ℤ ∧ 2 ∈ ℕ) → (2 ∥ 𝑑 → 2 ∥ (𝑑↑2)))
128122, 124, 126, 127mp3an2i 1467 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) → (2 ∥ 𝑑 → 2 ∥ (𝑑↑2)))
129128imp 410 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → 2 ∥ (𝑑↑2))
130 2nn0 11986 . . . . . . . . . . . . . . . . . . 19 2 ∈ ℕ0
131130a1i 11 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → 2 ∈ ℕ0)
132117nncnd 11725 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → 𝑑 ∈ ℂ)
133132flt4lem 40038 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → (𝑑↑4) = ((𝑑↑2)↑2))
134119nncnd 11725 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → 𝑒 ∈ ℂ)
135134flt4lem 40038 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → (𝑒↑4) = ((𝑒↑2)↑2))
136133, 135oveq12d 7182 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → ((𝑑↑4) + (𝑒↑4)) = (((𝑑↑2)↑2) + ((𝑒↑2)↑2)))
137 simplrr 778 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))
138136, 137eqtr3d 2775 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → (((𝑑↑2)↑2) + ((𝑒↑2)↑2)) = (𝑓↑2))
139 simplrl 777 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → (𝑑 gcd 𝑒) = 1)
140125a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → 2 ∈ ℕ)
141 rppwr 15998 . . . . . . . . . . . . . . . . . . . 20 ((𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ ∧ 2 ∈ ℕ) → ((𝑑 gcd 𝑒) = 1 → ((𝑑↑2) gcd (𝑒↑2)) = 1))
142117, 119, 140, 141syl3anc 1372 . . . . . . . . . . . . . . . . . . 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 40033 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → ((𝑑↑2) gcd 𝑓) = 1)
145118, 120, 121, 129, 144, 138flt4lem2 40040 . . . . . . . . . . . . . . . 16 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → ¬ 2 ∥ (𝑒↑2))
146119nnzd 12160 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → 𝑒 ∈ ℤ)
147 dvdsexp2im 15765 . . . . . . . . . . . . . . . . 17 ((2 ∈ ℤ ∧ 𝑒 ∈ ℤ ∧ 2 ∈ ℕ) → (2 ∥ 𝑒 → 2 ∥ (𝑒↑2)))
148122, 146, 140, 147mp3an2i 1467 . . . . . . . . . . . . . . . 16 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → (2 ∥ 𝑒 → 2 ∥ (𝑒↑2)))
149145, 148mtod 201 . . . . . . . . . . . . . . 15 (((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) ∧ 2 ∥ 𝑑) → ¬ 2 ∥ 𝑒)
150149ex 416 . . . . . . . . . . . . . 14 ((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) → (2 ∥ 𝑑 → ¬ 2 ∥ 𝑒))
151 imor 852 . . . . . . . . . . . . . 14 ((2 ∥ 𝑑 → ¬ 2 ∥ 𝑒) ↔ (¬ 2 ∥ 𝑑 ∨ ¬ 2 ∥ 𝑒))
152150, 151sylib 221 . . . . . . . . . . . . 13 ((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) → (¬ 2 ∥ 𝑑 ∨ ¬ 2 ∥ 𝑒))
15381, 116, 152mpjaodan 958 . . . . . . . . . . . 12 ((((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) ∧ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))) → ∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2))))
154153ex 416 . . . . . . . . . . 11 (((𝜑𝑓 ∈ ℕ) ∧ (𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ)) → (((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2)) → ∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2)))))
155154rexlimdvva 3203 . . . . . . . . . 10 ((𝜑𝑓 ∈ ℕ) → (∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2)) → ∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2)))))
156155reximdva 3183 . . . . . . . . 9 (𝜑 → (∃𝑓 ∈ ℕ ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2)) → ∃𝑓 ∈ ℕ ∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2)))))
157156con3d 155 . . . . . . . 8 (𝜑 → (¬ ∃𝑓 ∈ ℕ ∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2))) → ¬ ∃𝑓 ∈ ℕ ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))))
158 ralnex 3148 . . . . . . . 8 (∀𝑓 ∈ ℕ ¬ ∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2))) ↔ ¬ ∃𝑓 ∈ ℕ ∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2))))
159 ralnex 3148 . . . . . . . 8 (∀𝑓 ∈ ℕ ¬ ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2)) ↔ ¬ ∃𝑓 ∈ ℕ ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2)))
160157, 158, 1593imtr4g 299 . . . . . . 7 (𝜑 → (∀𝑓 ∈ ℕ ¬ ∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2))) → ∀𝑓 ∈ ℕ ¬ ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))))
161 rabeq0 4270 . . . . . . 7 ({𝑓 ∈ ℕ ∣ ∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2)))} = ∅ ↔ ∀𝑓 ∈ ℕ ¬ ∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2))))
162 rabeq0 4270 . . . . . . 7 ({𝑓 ∈ ℕ ∣ ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))} = ∅ ↔ ∀𝑓 ∈ ℕ ¬ ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2)))
163160, 161, 1623imtr4g 299 . . . . . 6 (𝜑 → ({𝑓 ∈ ℕ ∣ ∃𝑔 ∈ ℕ ∃ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ) = 1 ∧ ((𝑔↑4) + (↑4)) = (𝑓↑2)))} = ∅ → {𝑓 ∈ ℕ ∣ ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))} = ∅))
16457, 163mpd 15 . . . . 5 (𝜑 → {𝑓 ∈ ℕ ∣ ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))} = ∅)
165 oveq1 7171 . . . . . . . . . . . . 13 (𝑓 = (𝑐 / ((𝑎 gcd 𝑏)↑2)) → (𝑓↑2) = ((𝑐 / ((𝑎 gcd 𝑏)↑2))↑2))
166165eqeq2d 2749 . . . . . . . . . . . 12 (𝑓 = (𝑐 / ((𝑎 gcd 𝑏)↑2)) → (((𝑑↑4) + (𝑒↑4)) = (𝑓↑2) ↔ ((𝑑↑4) + (𝑒↑4)) = ((𝑐 / ((𝑎 gcd 𝑏)↑2))↑2)))
167166anbi2d 632 . . . . . . . . . . 11 (𝑓 = (𝑐 / ((𝑎 gcd 𝑏)↑2)) → (((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2)) ↔ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = ((𝑐 / ((𝑎 gcd 𝑏)↑2))↑2))))
168 oveq1 7171 . . . . . . . . . . . . 13 (𝑑 = (𝑎 / (𝑎 gcd 𝑏)) → (𝑑 gcd 𝑒) = ((𝑎 / (𝑎 gcd 𝑏)) gcd 𝑒))
169168eqeq1d 2740 . . . . . . . . . . . 12 (𝑑 = (𝑎 / (𝑎 gcd 𝑏)) → ((𝑑 gcd 𝑒) = 1 ↔ ((𝑎 / (𝑎 gcd 𝑏)) gcd 𝑒) = 1))
170 oveq1 7171 . . . . . . . . . . . . . 14 (𝑑 = (𝑎 / (𝑎 gcd 𝑏)) → (𝑑↑4) = ((𝑎 / (𝑎 gcd 𝑏))↑4))
171170oveq1d 7179 . . . . . . . . . . . . 13 (𝑑 = (𝑎 / (𝑎 gcd 𝑏)) → ((𝑑↑4) + (𝑒↑4)) = (((𝑎 / (𝑎 gcd 𝑏))↑4) + (𝑒↑4)))
172171eqeq1d 2740 . . . . . . . . . . . 12 (𝑑 = (𝑎 / (𝑎 gcd 𝑏)) → (((𝑑↑4) + (𝑒↑4)) = ((𝑐 / ((𝑎 gcd 𝑏)↑2))↑2) ↔ (((𝑎 / (𝑎 gcd 𝑏))↑4) + (𝑒↑4)) = ((𝑐 / ((𝑎 gcd 𝑏)↑2))↑2)))
173169, 172anbi12d 634 . . . . . . . . . . 11 (𝑑 = (𝑎 / (𝑎 gcd 𝑏)) → (((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = ((𝑐 / ((𝑎 gcd 𝑏)↑2))↑2)) ↔ (((𝑎 / (𝑎 gcd 𝑏)) gcd 𝑒) = 1 ∧ (((𝑎 / (𝑎 gcd 𝑏))↑4) + (𝑒↑4)) = ((𝑐 / ((𝑎 gcd 𝑏)↑2))↑2))))
174 oveq2 7172 . . . . . . . . . . . . 13 (𝑒 = (𝑏 / (𝑎 gcd 𝑏)) → ((𝑎 / (𝑎 gcd 𝑏)) gcd 𝑒) = ((𝑎 / (𝑎 gcd 𝑏)) gcd (𝑏 / (𝑎 gcd 𝑏))))
175174eqeq1d 2740 . . . . . . . . . . . 12 (𝑒 = (𝑏 / (𝑎 gcd 𝑏)) → (((𝑎 / (𝑎 gcd 𝑏)) gcd 𝑒) = 1 ↔ ((𝑎 / (𝑎 gcd 𝑏)) gcd (𝑏 / (𝑎 gcd 𝑏))) = 1))
176 oveq1 7171 . . . . . . . . . . . . . 14 (𝑒 = (𝑏 / (𝑎 gcd 𝑏)) → (𝑒↑4) = ((𝑏 / (𝑎 gcd 𝑏))↑4))
177176oveq2d 7180 . . . . . . . . . . . . 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 634 . . . . . . . . . . 11 (𝑒 = (𝑏 / (𝑎 gcd 𝑏)) → ((((𝑎 / (𝑎 gcd 𝑏)) gcd 𝑒) = 1 ∧ (((𝑎 / (𝑎 gcd 𝑏))↑4) + (𝑒↑4)) = ((𝑐 / ((𝑎 gcd 𝑏)↑2))↑2)) ↔ (((𝑎 / (𝑎 gcd 𝑏)) gcd (𝑏 / (𝑎 gcd 𝑏))) = 1 ∧ (((𝑎 / (𝑎 gcd 𝑏))↑4) + ((𝑏 / (𝑎 gcd 𝑏))↑4)) = ((𝑐 / ((𝑎 gcd 𝑏)↑2))↑2))))
180 simplrr 778 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑐 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ (𝑏 ∈ ℕ ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) → 𝑎 ∈ ℕ)
181 simprl 771 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑐 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ (𝑏 ∈ ℕ ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) → 𝑏 ∈ ℕ)
182 simplrl 777 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑐 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ (𝑏 ∈ ℕ ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) → 𝑐 ∈ ℕ)
183 simprr 773 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑐 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ (𝑏 ∈ ℕ ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) → ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))
184180, 181, 182, 183flt4lem6 40051 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑐 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ (𝑏 ∈ ℕ ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) → (((𝑎 / (𝑎 gcd 𝑏)) ∈ ℕ ∧ (𝑏 / (𝑎 gcd 𝑏)) ∈ ℕ ∧ (𝑐 / ((𝑎 gcd 𝑏)↑2)) ∈ ℕ) ∧ (((𝑎 / (𝑎 gcd 𝑏))↑4) + ((𝑏 / (𝑎 gcd 𝑏))↑4)) = ((𝑐 / ((𝑎 gcd 𝑏)↑2))↑2)))
185184simpld 498 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑐 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ (𝑏 ∈ ℕ ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) → ((𝑎 / (𝑎 gcd 𝑏)) ∈ ℕ ∧ (𝑏 / (𝑎 gcd 𝑏)) ∈ ℕ ∧ (𝑐 / ((𝑎 gcd 𝑏)↑2)) ∈ ℕ))
186185simp3d 1145 . . . . . . . . . . 11 (((𝜑 ∧ (𝑐 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ (𝑏 ∈ ℕ ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) → (𝑐 / ((𝑎 gcd 𝑏)↑2)) ∈ ℕ)
187185simp1d 1143 . . . . . . . . . . 11 (((𝜑 ∧ (𝑐 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ (𝑏 ∈ ℕ ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) → (𝑎 / (𝑎 gcd 𝑏)) ∈ ℕ)
188185simp2d 1144 . . . . . . . . . . 11 (((𝜑 ∧ (𝑐 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ (𝑏 ∈ ℕ ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) → (𝑏 / (𝑎 gcd 𝑏)) ∈ ℕ)
189180nnzd 12160 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑐 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ (𝑏 ∈ ℕ ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) → 𝑎 ∈ ℤ)
190181nnzd 12160 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑐 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ (𝑏 ∈ ℕ ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) → 𝑏 ∈ ℤ)
191181nnne0d 11759 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑐 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ (𝑏 ∈ ℕ ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) → 𝑏 ≠ 0)
192 divgcdcoprm0 16099 . . . . . . . . . . . . 13 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝑏 ≠ 0) → ((𝑎 / (𝑎 gcd 𝑏)) gcd (𝑏 / (𝑎 gcd 𝑏))) = 1)
193189, 190, 191, 192syl3anc 1372 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑐 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ (𝑏 ∈ ℕ ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) → ((𝑎 / (𝑎 gcd 𝑏)) gcd (𝑏 / (𝑎 gcd 𝑏))) = 1)
194184simprd 499 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑐 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ (𝑏 ∈ ℕ ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) → (((𝑎 / (𝑎 gcd 𝑏))↑4) + ((𝑏 / (𝑎 gcd 𝑏))↑4)) = ((𝑐 / ((𝑎 gcd 𝑏)↑2))↑2))
195193, 194jca 515 . . . . . . . . . . 11 (((𝜑 ∧ (𝑐 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ (𝑏 ∈ ℕ ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) → (((𝑎 / (𝑎 gcd 𝑏)) gcd (𝑏 / (𝑎 gcd 𝑏))) = 1 ∧ (((𝑎 / (𝑎 gcd 𝑏))↑4) + ((𝑏 / (𝑎 gcd 𝑏))↑4)) = ((𝑐 / ((𝑎 gcd 𝑏)↑2))↑2)))
196167, 173, 179, 186, 187, 188, 1953rspcedvdw 39757 . . . . . . . . . 10 (((𝜑 ∧ (𝑐 ∈ ℕ ∧ 𝑎 ∈ ℕ)) ∧ (𝑏 ∈ ℕ ∧ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))) → ∃𝑓 ∈ ℕ ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2)))
197196rexlimdvaa 3194 . . . . . . . . 9 ((𝜑 ∧ (𝑐 ∈ ℕ ∧ 𝑎 ∈ ℕ)) → (∃𝑏 ∈ ℕ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2) → ∃𝑓 ∈ ℕ ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))))
198197rexlimdvva 3203 . . . . . . . 8 (𝜑 → (∃𝑐 ∈ ℕ ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2) → ∃𝑓 ∈ ℕ ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))))
199198con3d 155 . . . . . . 7 (𝜑 → (¬ ∃𝑓 ∈ ℕ ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2)) → ¬ ∃𝑐 ∈ ℕ ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2)))
200 ralnex 3148 . . . . . . 7 (∀𝑐 ∈ ℕ ¬ ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2) ↔ ¬ ∃𝑐 ∈ ℕ ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))
201199, 159, 2003imtr4g 299 . . . . . 6 (𝜑 → (∀𝑓 ∈ ℕ ¬ ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2)) → ∀𝑐 ∈ ℕ ¬ ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2)))
202 rabeq0 4270 . . . . . 6 ({𝑐 ∈ ℕ ∣ ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2)} = ∅ ↔ ∀𝑐 ∈ ℕ ¬ ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2))
203201, 162, 2023imtr4g 299 . . . . 5 (𝜑 → ({𝑓 ∈ ℕ ∣ ∃𝑑 ∈ ℕ ∃𝑒 ∈ ℕ ((𝑑 gcd 𝑒) = 1 ∧ ((𝑑↑4) + (𝑒↑4)) = (𝑓↑2))} = ∅ → {𝑐 ∈ ℕ ∣ ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2)} = ∅))
204164, 203mpd 15 . . . 4 (𝜑 → {𝑐 ∈ ℕ ∣ ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2)} = ∅)
205 sseq0 4285 . . . 4 (({𝑐 ∈ ℕ ∣ ((𝐴↑4) + (𝐵↑4)) = (𝑐↑2)} ⊆ {𝑐 ∈ ℕ ∣ ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2)} ∧ {𝑐 ∈ ℕ ∣ ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑4) + (𝑏↑4)) = (𝑐↑2)} = ∅) → {𝑐 ∈ ℕ ∣ ((𝐴↑4) + (𝐵↑4)) = (𝑐↑2)} = ∅)
20615, 204, 205syl2anc 587 . . 3 (𝜑 → {𝑐 ∈ ℕ ∣ ((𝐴↑4) + (𝐵↑4)) = (𝑐↑2)} = ∅)
207 rabeq0 4270 . . 3 ({𝑐 ∈ ℕ ∣ ((𝐴↑4) + (𝐵↑4)) = (𝑐↑2)} = ∅ ↔ ∀𝑐 ∈ ℕ ¬ ((𝐴↑4) + (𝐵↑4)) = (𝑐↑2))
208206, 207sylib 221 . 2 (𝜑 → ∀𝑐 ∈ ℕ ¬ ((𝐴↑4) + (𝐵↑4)) = (𝑐↑2))
209 oveq1 7171 . . . . 5 (𝑐 = 𝐶 → (𝑐↑2) = (𝐶↑2))
210209eqeq2d 2749 . . . 4 (𝑐 = 𝐶 → (((𝐴↑4) + (𝐵↑4)) = (𝑐↑2) ↔ ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2)))
211210necon3bbid 2971 . . 3 (𝑐 = 𝐶 → (¬ ((𝐴↑4) + (𝐵↑4)) = (𝑐↑2) ↔ ((𝐴↑4) + (𝐵↑4)) ≠ (𝐶↑2)))
212211rspcv 3519 . 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 399  wo 846  w3a 1088   = wceq 1542  wcel 2113  wne 2934  wral 3053  wrex 3054  {crab 3057  wss 3841  c0 4209   class class class wbr 5027  cfv 6333  (class class class)co 7164  0cc0 10608  1c1 10609   + caddc 10611   < clt 10746   / cdiv 11368  cn 11709  2c2 11764  4c4 11766  0cn0 11969  cz 12055  cuz 12317  cexp 13514  cdvds 15692   gcd cgcd 15930
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-sep 5164  ax-nul 5171  ax-pow 5229  ax-pr 5293  ax-un 7473  ax-cnex 10664  ax-resscn 10665  ax-1cn 10666  ax-icn 10667  ax-addcl 10668  ax-addrcl 10669  ax-mulcl 10670  ax-mulrcl 10671  ax-mulcom 10672  ax-addass 10673  ax-mulass 10674  ax-distr 10675  ax-i2m1 10676  ax-1ne0 10677  ax-1rid 10678  ax-rnegex 10679  ax-rrecex 10680  ax-cnre 10681  ax-pre-lttri 10682  ax-pre-lttrn 10683  ax-pre-ltadd 10684  ax-pre-mulgt0 10685  ax-pre-sup 10686
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-nel 3039  df-ral 3058  df-rex 3059  df-reu 3060  df-rmo 3061  df-rab 3062  df-v 3399  df-sbc 3680  df-csb 3789  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-pss 3860  df-nul 4210  df-if 4412  df-pw 4487  df-sn 4514  df-pr 4516  df-tp 4518  df-op 4520  df-uni 4794  df-iun 4880  df-br 5028  df-opab 5090  df-mpt 5108  df-tr 5134  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6123  df-ord 6169  df-on 6170  df-lim 6171  df-suc 6172  df-iota 6291  df-fun 6335  df-fn 6336  df-f 6337  df-f1 6338  df-fo 6339  df-f1o 6340  df-fv 6341  df-riota 7121  df-ov 7167  df-oprab 7168  df-mpo 7169  df-om 7594  df-1st 7707  df-2nd 7708  df-wrecs 7969  df-recs 8030  df-rdg 8068  df-1o 8124  df-2o 8125  df-er 8313  df-en 8549  df-dom 8550  df-sdom 8551  df-fin 8552  df-sup 8972  df-inf 8973  df-pnf 10748  df-mnf 10749  df-xr 10750  df-ltxr 10751  df-le 10752  df-sub 10943  df-neg 10944  df-div 11369  df-nn 11710  df-2 11772  df-3 11773  df-4 11774  df-n0 11970  df-z 12056  df-uz 12318  df-q 12424  df-rp 12466  df-fz 12975  df-fl 13246  df-mod 13322  df-seq 13454  df-exp 13515  df-cj 14541  df-re 14542  df-im 14543  df-sqrt 14677  df-abs 14678  df-dvds 15693  df-gcd 15931  df-prm 16106  df-numer 16168  df-denom 16169
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator