Metamath Proof Explorer

Theorem flt4lem7

Description: Convert flt4lem5f into a convenient form for nna4b4nsq . TODO-SN: The change to ( A gcd B ) = 1 points at some inefficiency in the lemmas. (Contributed by SN, 25-Aug-2024)

Ref Expression
Hypotheses flt4lem7.a ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
flt4lem7.b ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
flt4lem7.c ⊢ ( 𝜑 → 𝐶 ∈ ℕ )
flt4lem7.1 ⊢ ( 𝜑 → ¬ 2 ∥ 𝐴 )
flt4lem7.2 ⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) = 1 )
flt4lem7.3 ⊢ ( 𝜑 → ( ( 𝐴 ↑ 4 ) + ( 𝐵 ↑ 4 ) ) = ( 𝐶 ↑ 2 ) )
Assertion flt4lem7 ( 𝜑 → ∃ 𝑙 ∈ ℕ ( ∃ 𝑔 ∈ ℕ ∃ ℎ ∈ ℕ ( ¬ 2 ∥ 𝑔 ∧ ( ( 𝑔 gcd ℎ ) = 1 ∧ ( ( 𝑔 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 𝑙 < 𝐶 ) )

Proof

Step Hyp Ref Expression
1 flt4lem7.a ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
2 flt4lem7.b ⊢ ( 𝜑 → 𝐵 ∈ ℕ )
3 flt4lem7.c ⊢ ( 𝜑 → 𝐶 ∈ ℕ )
4 flt4lem7.1 ⊢ ( 𝜑 → ¬ 2 ∥ 𝐴 )
5 flt4lem7.2 ⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) = 1 )
6 flt4lem7.3 ⊢ ( 𝜑 → ( ( 𝐴 ↑ 4 ) + ( 𝐵 ↑ 4 ) ) = ( 𝐶 ↑ 2 ) )
7 breq1 ⊢ ( 𝑙 = ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) → ( 𝑙 < 𝐶 ↔ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) < 𝐶 ) )
8 oveq1 ⊢ ( 𝑙 = ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) → ( 𝑙 ↑ 2 ) = ( ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ↑ 2 ) )
9 8 eqeq2d ⊢ ( 𝑙 = ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) → ( ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ↔ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ↑ 2 ) ) )
10 9 anbi2d ⊢ ( 𝑙 = ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) → ( ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ↔ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ↑ 2 ) ) ) )
11 10 2rexbidv ⊢ ( 𝑙 = ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) → ( ∃ 𝑚 ∈ ℕ ∃ 𝑛 ∈ ℕ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ↔ ∃ 𝑚 ∈ ℕ ∃ 𝑛 ∈ ℕ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ↑ 2 ) ) ) )
12 7 11 anbi12d ⊢ ( 𝑙 = ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) → ( ( 𝑙 < 𝐶 ∧ ∃ 𝑚 ∈ ℕ ∃ 𝑛 ∈ ℕ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ↔ ( ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) < 𝐶 ∧ ∃ 𝑚 ∈ ℕ ∃ 𝑛 ∈ ℕ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ↑ 2 ) ) ) ) )
13 eqid ⊢ ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) = ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 )
14 eqid ⊢ ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) = ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 )
15 eqid ⊢ ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) = ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 )
16 eqid ⊢ ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) = ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 )
17 1 nnsqcld ⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℕ )
18 2 nnsqcld ⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℕ )
19 2nn0 ⊢ 2 ∈ ℕ0
20 19 a1i ⊢ ( 𝜑 → 2 ∈ ℕ0 )
21 1 nncnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
22 21 exp4sqsq ⊢ ( 𝜑 → ( 𝐴 ↑ 4 ) = ( ( 𝐴 ↑ 2 ) ↑ 2 ) )
23 2 nncnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
24 23 exp4sqsq ⊢ ( 𝜑 → ( 𝐵 ↑ 4 ) = ( ( 𝐵 ↑ 2 ) ↑ 2 ) )
25 22 24 oveq12d ⊢ ( 𝜑 → ( ( 𝐴 ↑ 4 ) + ( 𝐵 ↑ 4 ) ) = ( ( ( 𝐴 ↑ 2 ) ↑ 2 ) + ( ( 𝐵 ↑ 2 ) ↑ 2 ) ) )
26 25 6 eqtr3d ⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) ↑ 2 ) + ( ( 𝐵 ↑ 2 ) ↑ 2 ) ) = ( 𝐶 ↑ 2 ) )
27 2nn ⊢ 2 ∈ ℕ
28 27 a1i ⊢ ( 𝜑 → 2 ∈ ℕ )
29 rppwr ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 2 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) = 1 → ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) = 1 ) )
30 1 2 28 29 syl3anc ⊢ ( 𝜑 → ( ( 𝐴 gcd 𝐵 ) = 1 → ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) = 1 ) )
31 5 30 mpd ⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) = 1 )
32 17 18 3 20 26 31 fltaccoprm ⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) gcd 𝐶 ) = 1 )
33 1 nnzd ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
34 3 nnzd ⊢ ( 𝜑 → 𝐶 ∈ ℤ )
35 rpexp ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ 2 ∈ ℕ ) → ( ( ( 𝐴 ↑ 2 ) gcd 𝐶 ) = 1 ↔ ( 𝐴 gcd 𝐶 ) = 1 ) )
36 33 34 28 35 syl3anc ⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) gcd 𝐶 ) = 1 ↔ ( 𝐴 gcd 𝐶 ) = 1 ) )
37 32 36 mpbid ⊢ ( 𝜑 → ( 𝐴 gcd 𝐶 ) = 1 )
38 13 14 15 16 1 2 3 4 37 6 flt4lem5e ⊢ ( 𝜑 → ( ( ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ) = 1 ∧ ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) = 1 ∧ ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) = 1 ) ∧ ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ∈ ℕ ∧ ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ∈ ℕ ∧ ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ∈ ℕ ) ∧ ( ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) · ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) · ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ) ) = ( ( 𝐵 / 2 ) ↑ 2 ) ∧ ( 𝐵 / 2 ) ∈ ℕ ) ) )
39 38 simp2d ⊢ ( 𝜑 → ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ∈ ℕ ∧ ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ∈ ℕ ∧ ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ∈ ℕ ) )
40 39 simp3d ⊢ ( 𝜑 → ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ∈ ℕ )
41 38 simp3d ⊢ ( 𝜑 → ( ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) · ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) · ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ) ) = ( ( 𝐵 / 2 ) ↑ 2 ) ∧ ( 𝐵 / 2 ) ∈ ℕ ) )
42 41 simprd ⊢ ( 𝜑 → ( 𝐵 / 2 ) ∈ ℕ )
43 gcdnncl ⊢ ( ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ∈ ℕ ∧ ( 𝐵 / 2 ) ∈ ℕ ) → ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ∈ ℕ )
44 40 42 43 syl2anc ⊢ ( 𝜑 → ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ∈ ℕ )
45 44 nnred ⊢ ( 𝜑 → ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ∈ ℝ )
46 42 nnred ⊢ ( 𝜑 → ( 𝐵 / 2 ) ∈ ℝ )
47 3 nnred ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
48 40 nnzd ⊢ ( 𝜑 → ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ∈ ℤ )
49 48 42 gcdle2d ⊢ ( 𝜑 → ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ≤ ( 𝐵 / 2 ) )
50 2 nnred ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
51 2 nnrpd ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
52 rphalflt ⊢ ( 𝐵 ∈ ℝ+ → ( 𝐵 / 2 ) < 𝐵 )
53 51 52 syl ⊢ ( 𝜑 → ( 𝐵 / 2 ) < 𝐵 )
54 18 nnred ⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℝ )
55 4nn0 ⊢ 4 ∈ ℕ0
56 55 a1i ⊢ ( 𝜑 → 4 ∈ ℕ0 )
57 2 56 nnexpcld ⊢ ( 𝜑 → ( 𝐵 ↑ 4 ) ∈ ℕ )
58 57 nnred ⊢ ( 𝜑 → ( 𝐵 ↑ 4 ) ∈ ℝ )
59 3 nnsqcld ⊢ ( 𝜑 → ( 𝐶 ↑ 2 ) ∈ ℕ )
60 59 nnred ⊢ ( 𝜑 → ( 𝐶 ↑ 2 ) ∈ ℝ )
61 2lt4 ⊢ 2 < 4
62 2z ⊢ 2 ∈ ℤ
63 62 a1i ⊢ ( 𝜑 → 2 ∈ ℤ )
64 4z ⊢ 4 ∈ ℤ
65 64 a1i ⊢ ( 𝜑 → 4 ∈ ℤ )
66 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
67 2re ⊢ 2 ∈ ℝ
68 67 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
69 1lt2 ⊢ 1 < 2
70 69 a1i ⊢ ( 𝜑 → 1 < 2 )
71 2t1e2 ⊢ ( 2 · 1 ) = 2
72 42 nnge1d ⊢ ( 𝜑 → 1 ≤ ( 𝐵 / 2 ) )
73 2rp ⊢ 2 ∈ ℝ+
74 73 a1i ⊢ ( 𝜑 → 2 ∈ ℝ+ )
75 66 50 74 lemuldiv2d ⊢ ( 𝜑 → ( ( 2 · 1 ) ≤ 𝐵 ↔ 1 ≤ ( 𝐵 / 2 ) ) )
76 72 75 mpbird ⊢ ( 𝜑 → ( 2 · 1 ) ≤ 𝐵 )
77 71 76 eqbrtrrid ⊢ ( 𝜑 → 2 ≤ 𝐵 )
78 66 68 50 70 77 ltletrd ⊢ ( 𝜑 → 1 < 𝐵 )
79 50 63 65 78 ltexp2d ⊢ ( 𝜑 → ( 2 < 4 ↔ ( 𝐵 ↑ 2 ) < ( 𝐵 ↑ 4 ) ) )
80 61 79 mpbii ⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) < ( 𝐵 ↑ 4 ) )
81 1 56 nnexpcld ⊢ ( 𝜑 → ( 𝐴 ↑ 4 ) ∈ ℕ )
82 81 nngt0d ⊢ ( 𝜑 → 0 < ( 𝐴 ↑ 4 ) )
83 81 nnred ⊢ ( 𝜑 → ( 𝐴 ↑ 4 ) ∈ ℝ )
84 83 58 ltaddpos2d ⊢ ( 𝜑 → ( 0 < ( 𝐴 ↑ 4 ) ↔ ( 𝐵 ↑ 4 ) < ( ( 𝐴 ↑ 4 ) + ( 𝐵 ↑ 4 ) ) ) )
85 82 84 mpbid ⊢ ( 𝜑 → ( 𝐵 ↑ 4 ) < ( ( 𝐴 ↑ 4 ) + ( 𝐵 ↑ 4 ) ) )
86 85 6 breqtrd ⊢ ( 𝜑 → ( 𝐵 ↑ 4 ) < ( 𝐶 ↑ 2 ) )
87 54 58 60 80 86 lttrd ⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) < ( 𝐶 ↑ 2 ) )
88 3 nnrpd ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
89 51 88 28 ltexp1d ⊢ ( 𝜑 → ( 𝐵 < 𝐶 ↔ ( 𝐵 ↑ 2 ) < ( 𝐶 ↑ 2 ) ) )
90 87 89 mpbird ⊢ ( 𝜑 → 𝐵 < 𝐶 )
91 46 50 47 53 90 lttrd ⊢ ( 𝜑 → ( 𝐵 / 2 ) < 𝐶 )
92 45 46 47 49 91 lelttrd ⊢ ( 𝜑 → ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) < 𝐶 )
93 oveq1 ⊢ ( 𝑚 = ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) → ( 𝑚 gcd 𝑛 ) = ( ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) gcd 𝑛 ) )
94 93 eqeq1d ⊢ ( 𝑚 = ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) → ( ( 𝑚 gcd 𝑛 ) = 1 ↔ ( ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) gcd 𝑛 ) = 1 ) )
95 oveq1 ⊢ ( 𝑚 = ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) → ( 𝑚 ↑ 4 ) = ( ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ↑ 4 ) )
96 95 oveq1d ⊢ ( 𝑚 = ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) → ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( ( ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ↑ 4 ) + ( 𝑛 ↑ 4 ) ) )
97 96 eqeq1d ⊢ ( 𝑚 = ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) → ( ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ↑ 2 ) ↔ ( ( ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ↑ 2 ) ) )
98 94 97 anbi12d ⊢ ( 𝑚 = ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) → ( ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ↑ 2 ) ) ↔ ( ( ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) gcd 𝑛 ) = 1 ∧ ( ( ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ↑ 2 ) ) ) )
99 oveq2 ⊢ ( 𝑛 = ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) → ( ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) gcd 𝑛 ) = ( ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) gcd ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ) )
100 99 eqeq1d ⊢ ( 𝑛 = ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) → ( ( ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) gcd 𝑛 ) = 1 ↔ ( ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) gcd ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ) = 1 ) )
101 oveq1 ⊢ ( 𝑛 = ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) → ( 𝑛 ↑ 4 ) = ( ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ↑ 4 ) )
102 101 oveq2d ⊢ ( 𝑛 = ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) → ( ( ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( ( ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ↑ 4 ) + ( ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ↑ 4 ) ) )
103 102 eqeq1d ⊢ ( 𝑛 = ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) → ( ( ( ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ↑ 2 ) ↔ ( ( ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ↑ 4 ) + ( ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ↑ 4 ) ) = ( ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ↑ 2 ) ) )
104 100 103 anbi12d ⊢ ( 𝑛 = ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) → ( ( ( ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) gcd 𝑛 ) = 1 ∧ ( ( ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ↑ 2 ) ) ↔ ( ( ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) gcd ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ) = 1 ∧ ( ( ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ↑ 4 ) + ( ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ↑ 4 ) ) = ( ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ↑ 2 ) ) ) )
105 39 simp1d ⊢ ( 𝜑 → ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ∈ ℕ )
106 gcdnncl ⊢ ( ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ∈ ℕ ∧ ( 𝐵 / 2 ) ∈ ℕ ) → ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ∈ ℕ )
107 105 42 106 syl2anc ⊢ ( 𝜑 → ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ∈ ℕ )
108 39 simp2d ⊢ ( 𝜑 → ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ∈ ℕ )
109 gcdnncl ⊢ ( ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ∈ ℕ ∧ ( 𝐵 / 2 ) ∈ ℕ ) → ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ∈ ℕ )
110 108 42 109 syl2anc ⊢ ( 𝜑 → ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ∈ ℕ )
111 105 nnzd ⊢ ( 𝜑 → ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ∈ ℤ )
112 42 nnzd ⊢ ( 𝜑 → ( 𝐵 / 2 ) ∈ ℤ )
113 110 nnzd ⊢ ( 𝜑 → ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ∈ ℤ )
114 gcdass ⊢ ( ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ∈ ℤ ∧ ( 𝐵 / 2 ) ∈ ℤ ∧ ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ∈ ℤ ) → ( ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) gcd ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ) = ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( ( 𝐵 / 2 ) gcd ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ) ) )
115 111 112 113 114 syl3anc ⊢ ( 𝜑 → ( ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) gcd ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ) = ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( ( 𝐵 / 2 ) gcd ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ) ) )
116 108 nnzd ⊢ ( 𝜑 → ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ∈ ℤ )
117 gcdass ⊢ ( ( ( 𝐵 / 2 ) ∈ ℤ ∧ ( 𝐵 / 2 ) ∈ ℤ ∧ ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ∈ ℤ ) → ( ( ( 𝐵 / 2 ) gcd ( 𝐵 / 2 ) ) gcd ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ) = ( ( 𝐵 / 2 ) gcd ( ( 𝐵 / 2 ) gcd ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ) ) )
118 112 112 116 117 syl3anc ⊢ ( 𝜑 → ( ( ( 𝐵 / 2 ) gcd ( 𝐵 / 2 ) ) gcd ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ) = ( ( 𝐵 / 2 ) gcd ( ( 𝐵 / 2 ) gcd ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ) ) )
119 42 nnnn0d ⊢ ( 𝜑 → ( 𝐵 / 2 ) ∈ ℕ0 )
120 gcdnn0id ⊢ ( ( 𝐵 / 2 ) ∈ ℕ0 → ( ( 𝐵 / 2 ) gcd ( 𝐵 / 2 ) ) = ( 𝐵 / 2 ) )
121 119 120 syl ⊢ ( 𝜑 → ( ( 𝐵 / 2 ) gcd ( 𝐵 / 2 ) ) = ( 𝐵 / 2 ) )
122 121 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐵 / 2 ) gcd ( 𝐵 / 2 ) ) gcd ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ) = ( ( 𝐵 / 2 ) gcd ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ) )
123 112 116 gcdcomd ⊢ ( 𝜑 → ( ( 𝐵 / 2 ) gcd ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ) = ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) )
124 122 123 eqtr2d ⊢ ( 𝜑 → ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) = ( ( ( 𝐵 / 2 ) gcd ( 𝐵 / 2 ) ) gcd ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ) )
125 116 112 gcdcomd ⊢ ( 𝜑 → ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) = ( ( 𝐵 / 2 ) gcd ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ) )
126 125 oveq2d ⊢ ( 𝜑 → ( ( 𝐵 / 2 ) gcd ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ) = ( ( 𝐵 / 2 ) gcd ( ( 𝐵 / 2 ) gcd ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ) ) )
127 118 124 126 3eqtr4rd ⊢ ( 𝜑 → ( ( 𝐵 / 2 ) gcd ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ) = ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) )
128 127 oveq2d ⊢ ( 𝜑 → ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( ( 𝐵 / 2 ) gcd ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ) ) = ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ) )
129 38 simp1d ⊢ ( 𝜑 → ( ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ) = 1 ∧ ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) = 1 ∧ ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) = 1 ) )
130 129 simp1d ⊢ ( 𝜑 → ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ) = 1 )
131 130 oveq1d ⊢ ( 𝜑 → ( ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ) gcd ( 𝐵 / 2 ) ) = ( 1 gcd ( 𝐵 / 2 ) ) )
132 gcdass ⊢ ( ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ∈ ℤ ∧ ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ∈ ℤ ∧ ( 𝐵 / 2 ) ∈ ℤ ) → ( ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ) gcd ( 𝐵 / 2 ) ) = ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ) )
133 111 116 112 132 syl3anc ⊢ ( 𝜑 → ( ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ) gcd ( 𝐵 / 2 ) ) = ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ) )
134 1gcd ⊢ ( ( 𝐵 / 2 ) ∈ ℤ → ( 1 gcd ( 𝐵 / 2 ) ) = 1 )
135 112 134 syl ⊢ ( 𝜑 → ( 1 gcd ( 𝐵 / 2 ) ) = 1 )
136 131 133 135 3eqtr3d ⊢ ( 𝜑 → ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ) = 1 )
137 115 128 136 3eqtrd ⊢ ( 𝜑 → ( ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) gcd ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ) = 1 )
138 13 14 15 16 1 2 3 4 37 6 flt4lem5f ⊢ ( 𝜑 → ( ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ↑ 2 ) = ( ( ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ↑ 4 ) + ( ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ↑ 4 ) ) )
139 138 eqcomd ⊢ ( 𝜑 → ( ( ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ↑ 4 ) + ( ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ↑ 4 ) ) = ( ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ↑ 2 ) )
140 137 139 jca ⊢ ( 𝜑 → ( ( ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) gcd ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ) = 1 ∧ ( ( ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ↑ 4 ) + ( ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ↑ 4 ) ) = ( ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ↑ 2 ) ) )
141 98 104 107 110 140 2rspcedvdw ⊢ ( 𝜑 → ∃ 𝑚 ∈ ℕ ∃ 𝑛 ∈ ℕ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ↑ 2 ) ) )
142 92 141 jca ⊢ ( 𝜑 → ( ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) < 𝐶 ∧ ∃ 𝑚 ∈ ℕ ∃ 𝑛 ∈ ℕ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ↑ 2 ) ) ) )
143 12 44 142 rspcedvdw ⊢ ( 𝜑 → ∃ 𝑙 ∈ ℕ ( 𝑙 < 𝐶 ∧ ∃ 𝑚 ∈ ℕ ∃ 𝑛 ∈ ℕ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) )
144 breq2 ⊢ ( 𝑔 = 𝑚 → ( 2 ∥ 𝑔 ↔ 2 ∥ 𝑚 ) )
145 144 notbid ⊢ ( 𝑔 = 𝑚 → ( ¬ 2 ∥ 𝑔 ↔ ¬ 2 ∥ 𝑚 ) )
146 oveq1 ⊢ ( 𝑔 = 𝑚 → ( 𝑔 gcd ℎ ) = ( 𝑚 gcd ℎ ) )
147 146 eqeq1d ⊢ ( 𝑔 = 𝑚 → ( ( 𝑔 gcd ℎ ) = 1 ↔ ( 𝑚 gcd ℎ ) = 1 ) )
148 oveq1 ⊢ ( 𝑔 = 𝑚 → ( 𝑔 ↑ 4 ) = ( 𝑚 ↑ 4 ) )
149 148 oveq1d ⊢ ( 𝑔 = 𝑚 → ( ( 𝑔 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( ( 𝑚 ↑ 4 ) + ( ℎ ↑ 4 ) ) )
150 149 eqeq1d ⊢ ( 𝑔 = 𝑚 → ( ( ( 𝑔 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ↔ ( ( 𝑚 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) )
151 147 150 anbi12d ⊢ ( 𝑔 = 𝑚 → ( ( ( 𝑔 gcd ℎ ) = 1 ∧ ( ( 𝑔 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ↔ ( ( 𝑚 gcd ℎ ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) )
152 145 151 anbi12d ⊢ ( 𝑔 = 𝑚 → ( ( ¬ 2 ∥ 𝑔 ∧ ( ( 𝑔 gcd ℎ ) = 1 ∧ ( ( 𝑔 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ↔ ( ¬ 2 ∥ 𝑚 ∧ ( ( 𝑚 gcd ℎ ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ) )
153 oveq2 ⊢ ( ℎ = 𝑛 → ( 𝑚 gcd ℎ ) = ( 𝑚 gcd 𝑛 ) )
154 153 eqeq1d ⊢ ( ℎ = 𝑛 → ( ( 𝑚 gcd ℎ ) = 1 ↔ ( 𝑚 gcd 𝑛 ) = 1 ) )
155 oveq1 ⊢ ( ℎ = 𝑛 → ( ℎ ↑ 4 ) = ( 𝑛 ↑ 4 ) )
156 155 oveq2d ⊢ ( ℎ = 𝑛 → ( ( 𝑚 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) )
157 156 eqeq1d ⊢ ( ℎ = 𝑛 → ( ( ( 𝑚 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ↔ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) )
158 154 157 anbi12d ⊢ ( ℎ = 𝑛 → ( ( ( 𝑚 gcd ℎ ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ↔ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) )
159 158 anbi2d ⊢ ( ℎ = 𝑛 → ( ( ¬ 2 ∥ 𝑚 ∧ ( ( 𝑚 gcd ℎ ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ↔ ( ¬ 2 ∥ 𝑚 ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ) )
160 simplrl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) → 𝑚 ∈ ℕ )
161 160 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑚 ) → 𝑚 ∈ ℕ )
162 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → 𝑛 ∈ ℕ )
163 162 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑚 ) → 𝑛 ∈ ℕ )
164 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑚 ) → ¬ 2 ∥ 𝑚 )
165 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑚 ) → ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) )
166 164 165 jca ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑚 ) → ( ¬ 2 ∥ 𝑚 ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) )
167 152 159 161 163 166 2rspcedvdw ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑚 ) → ∃ 𝑔 ∈ ℕ ∃ ℎ ∈ ℕ ( ¬ 2 ∥ 𝑔 ∧ ( ( 𝑔 gcd ℎ ) = 1 ∧ ( ( 𝑔 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) )
168 simp-4r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑚 ) → 𝑙 < 𝐶 )
169 167 168 jca ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑚 ) → ( ∃ 𝑔 ∈ ℕ ∃ ℎ ∈ ℕ ( ¬ 2 ∥ 𝑔 ∧ ( ( 𝑔 gcd ℎ ) = 1 ∧ ( ( 𝑔 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 𝑙 < 𝐶 ) )
170 breq2 ⊢ ( 𝑔 = 𝑛 → ( 2 ∥ 𝑔 ↔ 2 ∥ 𝑛 ) )
171 170 notbid ⊢ ( 𝑔 = 𝑛 → ( ¬ 2 ∥ 𝑔 ↔ ¬ 2 ∥ 𝑛 ) )
172 oveq1 ⊢ ( 𝑔 = 𝑛 → ( 𝑔 gcd ℎ ) = ( 𝑛 gcd ℎ ) )
173 172 eqeq1d ⊢ ( 𝑔 = 𝑛 → ( ( 𝑔 gcd ℎ ) = 1 ↔ ( 𝑛 gcd ℎ ) = 1 ) )
174 oveq1 ⊢ ( 𝑔 = 𝑛 → ( 𝑔 ↑ 4 ) = ( 𝑛 ↑ 4 ) )
175 174 oveq1d ⊢ ( 𝑔 = 𝑛 → ( ( 𝑔 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( ( 𝑛 ↑ 4 ) + ( ℎ ↑ 4 ) ) )
176 175 eqeq1d ⊢ ( 𝑔 = 𝑛 → ( ( ( 𝑔 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ↔ ( ( 𝑛 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) )
177 173 176 anbi12d ⊢ ( 𝑔 = 𝑛 → ( ( ( 𝑔 gcd ℎ ) = 1 ∧ ( ( 𝑔 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ↔ ( ( 𝑛 gcd ℎ ) = 1 ∧ ( ( 𝑛 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) )
178 171 177 anbi12d ⊢ ( 𝑔 = 𝑛 → ( ( ¬ 2 ∥ 𝑔 ∧ ( ( 𝑔 gcd ℎ ) = 1 ∧ ( ( 𝑔 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ↔ ( ¬ 2 ∥ 𝑛 ∧ ( ( 𝑛 gcd ℎ ) = 1 ∧ ( ( 𝑛 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ) )
179 oveq2 ⊢ ( ℎ = 𝑚 → ( 𝑛 gcd ℎ ) = ( 𝑛 gcd 𝑚 ) )
180 179 eqeq1d ⊢ ( ℎ = 𝑚 → ( ( 𝑛 gcd ℎ ) = 1 ↔ ( 𝑛 gcd 𝑚 ) = 1 ) )
181 oveq1 ⊢ ( ℎ = 𝑚 → ( ℎ ↑ 4 ) = ( 𝑚 ↑ 4 ) )
182 181 oveq2d ⊢ ( ℎ = 𝑚 → ( ( 𝑛 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( ( 𝑛 ↑ 4 ) + ( 𝑚 ↑ 4 ) ) )
183 182 eqeq1d ⊢ ( ℎ = 𝑚 → ( ( ( 𝑛 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ↔ ( ( 𝑛 ↑ 4 ) + ( 𝑚 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) )
184 180 183 anbi12d ⊢ ( ℎ = 𝑚 → ( ( ( 𝑛 gcd ℎ ) = 1 ∧ ( ( 𝑛 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ↔ ( ( 𝑛 gcd 𝑚 ) = 1 ∧ ( ( 𝑛 ↑ 4 ) + ( 𝑚 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) )
185 184 anbi2d ⊢ ( ℎ = 𝑚 → ( ( ¬ 2 ∥ 𝑛 ∧ ( ( 𝑛 gcd ℎ ) = 1 ∧ ( ( 𝑛 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ↔ ( ¬ 2 ∥ 𝑛 ∧ ( ( 𝑛 gcd 𝑚 ) = 1 ∧ ( ( 𝑛 ↑ 4 ) + ( 𝑚 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ) )
186 162 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑛 ) → 𝑛 ∈ ℕ )
187 160 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑛 ) → 𝑚 ∈ ℕ )
188 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑛 ) → ¬ 2 ∥ 𝑛 )
189 186 nnzd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑛 ) → 𝑛 ∈ ℤ )
190 187 nnzd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑛 ) → 𝑚 ∈ ℤ )
191 189 190 gcdcomd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑛 ) → ( 𝑛 gcd 𝑚 ) = ( 𝑚 gcd 𝑛 ) )
192 simplrl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑛 ) → ( 𝑚 gcd 𝑛 ) = 1 )
193 191 192 eqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑛 ) → ( 𝑛 gcd 𝑚 ) = 1 )
194 55 a1i ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑛 ) → 4 ∈ ℕ0 )
195 186 194 nnexpcld ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑛 ) → ( 𝑛 ↑ 4 ) ∈ ℕ )
196 195 nncnd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑛 ) → ( 𝑛 ↑ 4 ) ∈ ℂ )
197 187 194 nnexpcld ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑛 ) → ( 𝑚 ↑ 4 ) ∈ ℕ )
198 197 nncnd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑛 ) → ( 𝑚 ↑ 4 ) ∈ ℂ )
199 196 198 addcomd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑛 ) → ( ( 𝑛 ↑ 4 ) + ( 𝑚 ↑ 4 ) ) = ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) )
200 simplrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑛 ) → ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) )
201 199 200 eqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑛 ) → ( ( 𝑛 ↑ 4 ) + ( 𝑚 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) )
202 188 193 201 jca32 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑛 ) → ( ¬ 2 ∥ 𝑛 ∧ ( ( 𝑛 gcd 𝑚 ) = 1 ∧ ( ( 𝑛 ↑ 4 ) + ( 𝑚 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) )
203 178 185 186 187 202 2rspcedvdw ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑛 ) → ∃ 𝑔 ∈ ℕ ∃ ℎ ∈ ℕ ( ¬ 2 ∥ 𝑔 ∧ ( ( 𝑔 gcd ℎ ) = 1 ∧ ( ( 𝑔 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) )
204 simp-4r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑛 ) → 𝑙 < 𝐶 )
205 203 204 jca ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑛 ) → ( ∃ 𝑔 ∈ ℕ ∃ ℎ ∈ ℕ ( ¬ 2 ∥ 𝑔 ∧ ( ( 𝑔 gcd ℎ ) = 1 ∧ ( ( 𝑔 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 𝑙 < 𝐶 ) )
206 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → 𝑚 ∈ ℕ )
207 206 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 2 ∥ 𝑚 ) → 𝑚 ∈ ℕ )
208 207 nnsqcld ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 2 ∥ 𝑚 ) → ( 𝑚 ↑ 2 ) ∈ ℕ )
209 162 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 2 ∥ 𝑚 ) → 𝑛 ∈ ℕ )
210 209 nnsqcld ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 2 ∥ 𝑚 ) → ( 𝑛 ↑ 2 ) ∈ ℕ )
211 simp-5r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 2 ∥ 𝑚 ) → 𝑙 ∈ ℕ )
212 160 nnzd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) → 𝑚 ∈ ℤ )
213 27 a1i ⊢ ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) → 2 ∈ ℕ )
214 dvdsexp2im ⊢ ( ( 2 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 2 ∈ ℕ ) → ( 2 ∥ 𝑚 → 2 ∥ ( 𝑚 ↑ 2 ) ) )
215 62 212 213 214 mp3an2i ⊢ ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) → ( 2 ∥ 𝑚 → 2 ∥ ( 𝑚 ↑ 2 ) ) )
216 215 imp ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 2 ∥ 𝑚 ) → 2 ∥ ( 𝑚 ↑ 2 ) )
217 19 a1i ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 2 ∥ 𝑚 ) → 2 ∈ ℕ0 )
218 207 nncnd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 2 ∥ 𝑚 ) → 𝑚 ∈ ℂ )
219 218 exp4sqsq ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 2 ∥ 𝑚 ) → ( 𝑚 ↑ 4 ) = ( ( 𝑚 ↑ 2 ) ↑ 2 ) )
220 209 nncnd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 2 ∥ 𝑚 ) → 𝑛 ∈ ℂ )
221 220 exp4sqsq ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 2 ∥ 𝑚 ) → ( 𝑛 ↑ 4 ) = ( ( 𝑛 ↑ 2 ) ↑ 2 ) )
222 219 221 oveq12d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 2 ∥ 𝑚 ) → ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( ( ( 𝑚 ↑ 2 ) ↑ 2 ) + ( ( 𝑛 ↑ 2 ) ↑ 2 ) ) )
223 simplrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 2 ∥ 𝑚 ) → ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) )
224 222 223 eqtr3d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 2 ∥ 𝑚 ) → ( ( ( 𝑚 ↑ 2 ) ↑ 2 ) + ( ( 𝑛 ↑ 2 ) ↑ 2 ) ) = ( 𝑙 ↑ 2 ) )
225 simplrl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 2 ∥ 𝑚 ) → ( 𝑚 gcd 𝑛 ) = 1 )
226 27 a1i ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 2 ∥ 𝑚 ) → 2 ∈ ℕ )
227 rppwr ⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ∧ 2 ∈ ℕ ) → ( ( 𝑚 gcd 𝑛 ) = 1 → ( ( 𝑚 ↑ 2 ) gcd ( 𝑛 ↑ 2 ) ) = 1 ) )
228 207 209 226 227 syl3anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 2 ∥ 𝑚 ) → ( ( 𝑚 gcd 𝑛 ) = 1 → ( ( 𝑚 ↑ 2 ) gcd ( 𝑛 ↑ 2 ) ) = 1 ) )
229 225 228 mpd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 2 ∥ 𝑚 ) → ( ( 𝑚 ↑ 2 ) gcd ( 𝑛 ↑ 2 ) ) = 1 )
230 208 210 211 217 224 229 fltaccoprm ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 2 ∥ 𝑚 ) → ( ( 𝑚 ↑ 2 ) gcd 𝑙 ) = 1 )
231 208 210 211 216 230 224 flt4lem2 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 2 ∥ 𝑚 ) → ¬ 2 ∥ ( 𝑛 ↑ 2 ) )
232 209 nnzd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 2 ∥ 𝑚 ) → 𝑛 ∈ ℤ )
233 dvdsexp2im ⊢ ( ( 2 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 2 ∈ ℕ ) → ( 2 ∥ 𝑛 → 2 ∥ ( 𝑛 ↑ 2 ) ) )
234 62 232 226 233 mp3an2i ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 2 ∥ 𝑚 ) → ( 2 ∥ 𝑛 → 2 ∥ ( 𝑛 ↑ 2 ) ) )
235 231 234 mtod ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 2 ∥ 𝑚 ) → ¬ 2 ∥ 𝑛 )
236 235 ex ⊢ ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) → ( 2 ∥ 𝑚 → ¬ 2 ∥ 𝑛 ) )
237 imor ⊢ ( ( 2 ∥ 𝑚 → ¬ 2 ∥ 𝑛 ) ↔ ( ¬ 2 ∥ 𝑚 ∨ ¬ 2 ∥ 𝑛 ) )
238 236 237 sylib ⊢ ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) → ( ¬ 2 ∥ 𝑚 ∨ ¬ 2 ∥ 𝑛 ) )
239 169 205 238 mpjaodan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) → ( ∃ 𝑔 ∈ ℕ ∃ ℎ ∈ ℕ ( ¬ 2 ∥ 𝑔 ∧ ( ( 𝑔 gcd ℎ ) = 1 ∧ ( ( 𝑔 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 𝑙 < 𝐶 ) )
240 239 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) → ( ∃ 𝑔 ∈ ℕ ∃ ℎ ∈ ℕ ( ¬ 2 ∥ 𝑔 ∧ ( ( 𝑔 gcd ℎ ) = 1 ∧ ( ( 𝑔 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 𝑙 < 𝐶 ) ) )
241 240 rexlimdvva ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) → ( ∃ 𝑚 ∈ ℕ ∃ 𝑛 ∈ ℕ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) → ( ∃ 𝑔 ∈ ℕ ∃ ℎ ∈ ℕ ( ¬ 2 ∥ 𝑔 ∧ ( ( 𝑔 gcd ℎ ) = 1 ∧ ( ( 𝑔 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 𝑙 < 𝐶 ) ) )
242 241 expimpd ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) → ( ( 𝑙 < 𝐶 ∧ ∃ 𝑚 ∈ ℕ ∃ 𝑛 ∈ ℕ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) → ( ∃ 𝑔 ∈ ℕ ∃ ℎ ∈ ℕ ( ¬ 2 ∥ 𝑔 ∧ ( ( 𝑔 gcd ℎ ) = 1 ∧ ( ( 𝑔 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 𝑙 < 𝐶 ) ) )
243 242 reximdva ⊢ ( 𝜑 → ( ∃ 𝑙 ∈ ℕ ( 𝑙 < 𝐶 ∧ ∃ 𝑚 ∈ ℕ ∃ 𝑛 ∈ ℕ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) → ∃ 𝑙 ∈ ℕ ( ∃ 𝑔 ∈ ℕ ∃ ℎ ∈ ℕ ( ¬ 2 ∥ 𝑔 ∧ ( ( 𝑔 gcd ℎ ) = 1 ∧ ( ( 𝑔 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 𝑙 < 𝐶 ) ) )
244 143 243 mpd ⊢ ( 𝜑 → ∃ 𝑙 ∈ ℕ ( ∃ 𝑔 ∈ ℕ ∃ ℎ ∈ ℕ ( ¬ 2 ∥ 𝑔 ∧ ( ( 𝑔 gcd ℎ ) = 1 ∧ ( ( 𝑔 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 𝑙 < 𝐶 ) )