This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
nna4b4nsq.b ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
nna4b4nsq.c ⊢ ( 𝜑 → 𝐶 ∈ ℕ )
Assertion nna4b4nsq ( 𝜑 → ( ( 𝐴 ↑ 4 ) + ( 𝐵 ↑ 4 ) ) ≠ ( 𝐶 ↑ 2 ) )

Proof

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