| 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
|
exp4sqsq |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ℕ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ ) ) ∧ ( ( 𝑑 gcd 𝑒 ) = 1 ∧ ( ( 𝑑 ↑ 4 ) + ( 𝑒 ↑ 4 ) ) = ( 𝑓 ↑ 2 ) ) ) ∧ 2 ∥ 𝑑 ) → ( 𝑑 ↑ 4 ) = ( ( 𝑑 ↑ 2 ) ↑ 2 ) ) |
| 134 |
119
|
nncnd |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ℕ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ ) ) ∧ ( ( 𝑑 gcd 𝑒 ) = 1 ∧ ( ( 𝑑 ↑ 4 ) + ( 𝑒 ↑ 4 ) ) = ( 𝑓 ↑ 2 ) ) ) ∧ 2 ∥ 𝑑 ) → 𝑒 ∈ ℂ ) |
| 135 |
134
|
exp4sqsq |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ℕ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑒 ∈ ℕ ) ) ∧ ( ( 𝑑 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 ) ) |