Metamath Proof Explorer

Theorem flt4lem7

Description: Convert flt4lem5f into a convenient form for nna4b4nsq . (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 13 14 15 16 1 2 3 4 5 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 ) ∈ ℕ ) ) )
18 17 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 ) ∈ ℕ ) )
19 18 simp3d ⊢ ( 𝜑 → ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ∈ ℕ )
20 17 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 ) ∈ ℕ ) )
21 20 simprd ⊢ ( 𝜑 → ( 𝐵 / 2 ) ∈ ℕ )
22 gcdnncl ⊢ ( ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ∈ ℕ ∧ ( 𝐵 / 2 ) ∈ ℕ ) → ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ∈ ℕ )
23 19 21 22 syl2anc ⊢ ( 𝜑 → ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ∈ ℕ )
24 23 nnred ⊢ ( 𝜑 → ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ∈ ℝ )
25 21 nnred ⊢ ( 𝜑 → ( 𝐵 / 2 ) ∈ ℝ )
26 3 nnred ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
27 19 nnzd ⊢ ( 𝜑 → ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ∈ ℤ )
28 27 21 gcdle2d ⊢ ( 𝜑 → ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ≤ ( 𝐵 / 2 ) )
29 2 nnred ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
30 2 nnrpd ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
31 rphalflt ⊢ ( 𝐵 ∈ ℝ+ → ( 𝐵 / 2 ) < 𝐵 )
32 30 31 syl ⊢ ( 𝜑 → ( 𝐵 / 2 ) < 𝐵 )
33 2 nnsqcld ⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℕ )
34 33 nnred ⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℝ )
35 4nn0 ⊢ 4 ∈ ℕ0
36 35 a1i ⊢ ( 𝜑 → 4 ∈ ℕ0 )
37 2 36 nnexpcld ⊢ ( 𝜑 → ( 𝐵 ↑ 4 ) ∈ ℕ )
38 37 nnred ⊢ ( 𝜑 → ( 𝐵 ↑ 4 ) ∈ ℝ )
39 3 nnsqcld ⊢ ( 𝜑 → ( 𝐶 ↑ 2 ) ∈ ℕ )
40 39 nnred ⊢ ( 𝜑 → ( 𝐶 ↑ 2 ) ∈ ℝ )
41 2lt4 ⊢ 2 < 4
42 2z ⊢ 2 ∈ ℤ
43 42 a1i ⊢ ( 𝜑 → 2 ∈ ℤ )
44 4z ⊢ 4 ∈ ℤ
45 44 a1i ⊢ ( 𝜑 → 4 ∈ ℤ )
46 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
47 21 nnge1d ⊢ ( 𝜑 → 1 ≤ ( 𝐵 / 2 ) )
48 46 25 29 47 32 lelttrd ⊢ ( 𝜑 → 1 < 𝐵 )
49 29 43 45 48 ltexp2d ⊢ ( 𝜑 → ( 2 < 4 ↔ ( 𝐵 ↑ 2 ) < ( 𝐵 ↑ 4 ) ) )
50 41 49 mpbii ⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) < ( 𝐵 ↑ 4 ) )
51 1 36 nnexpcld ⊢ ( 𝜑 → ( 𝐴 ↑ 4 ) ∈ ℕ )
52 51 nngt0d ⊢ ( 𝜑 → 0 < ( 𝐴 ↑ 4 ) )
53 51 nnred ⊢ ( 𝜑 → ( 𝐴 ↑ 4 ) ∈ ℝ )
54 53 38 ltaddpos2d ⊢ ( 𝜑 → ( 0 < ( 𝐴 ↑ 4 ) ↔ ( 𝐵 ↑ 4 ) < ( ( 𝐴 ↑ 4 ) + ( 𝐵 ↑ 4 ) ) ) )
55 52 54 mpbid ⊢ ( 𝜑 → ( 𝐵 ↑ 4 ) < ( ( 𝐴 ↑ 4 ) + ( 𝐵 ↑ 4 ) ) )
56 55 6 breqtrd ⊢ ( 𝜑 → ( 𝐵 ↑ 4 ) < ( 𝐶 ↑ 2 ) )
57 34 38 40 50 56 lttrd ⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) < ( 𝐶 ↑ 2 ) )
58 3 nnrpd ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
59 2nn ⊢ 2 ∈ ℕ
60 59 a1i ⊢ ( 𝜑 → 2 ∈ ℕ )
61 30 58 60 ltexp1d ⊢ ( 𝜑 → ( 𝐵 < 𝐶 ↔ ( 𝐵 ↑ 2 ) < ( 𝐶 ↑ 2 ) ) )
62 57 61 mpbird ⊢ ( 𝜑 → 𝐵 < 𝐶 )
63 25 29 26 32 62 lttrd ⊢ ( 𝜑 → ( 𝐵 / 2 ) < 𝐶 )
64 24 25 26 28 63 lelttrd ⊢ ( 𝜑 → ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) < 𝐶 )
65 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 𝑛 ) )
66 65 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 ) )
67 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 ) )
68 67 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 ) ) )
69 68 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 ) ) )
70 66 69 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 ) ) ) )
71 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 ) ) ) )
72 71 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 ) )
73 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 ) )
74 73 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 ) ) )
75 74 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 ) ) )
76 72 75 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 ) ) ) )
77 18 simp1d ⊢ ( 𝜑 → ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ∈ ℕ )
78 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 ) ) ∈ ℕ )
79 77 21 78 syl2anc ⊢ ( 𝜑 → ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ∈ ℕ )
80 18 simp2d ⊢ ( 𝜑 → ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ∈ ℕ )
81 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 ) ) ∈ ℕ )
82 80 21 81 syl2anc ⊢ ( 𝜑 → ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ∈ ℕ )
83 77 nnzd ⊢ ( 𝜑 → ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) + ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ∈ ℤ )
84 21 nnzd ⊢ ( 𝜑 → ( 𝐵 / 2 ) ∈ ℤ )
85 82 nnzd ⊢ ( 𝜑 → ( ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ∈ ℤ )
86 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 ) ) ) ) )
87 83 84 85 86 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 ) ) ) ) )
88 80 nnzd ⊢ ( 𝜑 → ( ( ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) + ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) − ( √ ‘ ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) − ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) ) ) ) / 2 ) ∈ ℤ )
89 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 ) ) ) )
90 84 84 88 89 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 ) ) ) )
91 21 nnnn0d ⊢ ( 𝜑 → ( 𝐵 / 2 ) ∈ ℕ0 )
92 gcdnn0id ⊢ ( ( 𝐵 / 2 ) ∈ ℕ0 → ( ( 𝐵 / 2 ) gcd ( 𝐵 / 2 ) ) = ( 𝐵 / 2 ) )
93 91 92 syl ⊢ ( 𝜑 → ( ( 𝐵 / 2 ) gcd ( 𝐵 / 2 ) ) = ( 𝐵 / 2 ) )
94 93 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 ) ) )
95 84 88 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 ) ) )
96 94 95 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 ) ) )
97 88 84 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 ) ) )
98 97 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 ) ) ) )
99 90 96 98 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 ) ) )
100 99 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 ) ) ) )
101 17 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 ) )
102 101 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 )
103 102 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 ) ) )
104 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 ) ) ) )
105 83 88 84 104 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 ) ) ) )
106 1gcd ⊢ ( ( 𝐵 / 2 ) ∈ ℤ → ( 1 gcd ( 𝐵 / 2 ) ) = 1 )
107 84 106 syl ⊢ ( 𝜑 → ( 1 gcd ( 𝐵 / 2 ) ) = 1 )
108 103 105 107 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 )
109 87 100 108 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 )
110 13 14 15 16 1 2 3 4 5 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 ) ) )
111 110 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 ) )
112 109 111 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 ) ) )
113 70 76 79 82 112 2rspcedvdw ⊢ ( 𝜑 → ∃ 𝑚 ∈ ℕ ∃ 𝑛 ∈ ℕ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ↑ 2 ) ) )
114 64 113 jca ⊢ ( 𝜑 → ( ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) < 𝐶 ∧ ∃ 𝑚 ∈ ℕ ∃ 𝑛 ∈ ℕ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( ( ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 ) gcd ( 𝐵 / 2 ) ) ↑ 2 ) ) ) )
115 12 23 114 rspcedvdw ⊢ ( 𝜑 → ∃ 𝑙 ∈ ℕ ( 𝑙 < 𝐶 ∧ ∃ 𝑚 ∈ ℕ ∃ 𝑛 ∈ ℕ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) )
116 breq2 ⊢ ( 𝑔 = 𝑚 → ( 2 ∥ 𝑔 ↔ 2 ∥ 𝑚 ) )
117 116 notbid ⊢ ( 𝑔 = 𝑚 → ( ¬ 2 ∥ 𝑔 ↔ ¬ 2 ∥ 𝑚 ) )
118 oveq1 ⊢ ( 𝑔 = 𝑚 → ( 𝑔 gcd ℎ ) = ( 𝑚 gcd ℎ ) )
119 118 eqeq1d ⊢ ( 𝑔 = 𝑚 → ( ( 𝑔 gcd ℎ ) = 1 ↔ ( 𝑚 gcd ℎ ) = 1 ) )
120 oveq1 ⊢ ( 𝑔 = 𝑚 → ( 𝑔 ↑ 4 ) = ( 𝑚 ↑ 4 ) )
121 120 oveq1d ⊢ ( 𝑔 = 𝑚 → ( ( 𝑔 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( ( 𝑚 ↑ 4 ) + ( ℎ ↑ 4 ) ) )
122 121 eqeq1d ⊢ ( 𝑔 = 𝑚 → ( ( ( 𝑔 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ↔ ( ( 𝑚 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) )
123 119 122 anbi12d ⊢ ( 𝑔 = 𝑚 → ( ( ( 𝑔 gcd ℎ ) = 1 ∧ ( ( 𝑔 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ↔ ( ( 𝑚 gcd ℎ ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) )
124 117 123 anbi12d ⊢ ( 𝑔 = 𝑚 → ( ( ¬ 2 ∥ 𝑔 ∧ ( ( 𝑔 gcd ℎ ) = 1 ∧ ( ( 𝑔 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ↔ ( ¬ 2 ∥ 𝑚 ∧ ( ( 𝑚 gcd ℎ ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ) )
125 oveq2 ⊢ ( ℎ = 𝑛 → ( 𝑚 gcd ℎ ) = ( 𝑚 gcd 𝑛 ) )
126 125 eqeq1d ⊢ ( ℎ = 𝑛 → ( ( 𝑚 gcd ℎ ) = 1 ↔ ( 𝑚 gcd 𝑛 ) = 1 ) )
127 oveq1 ⊢ ( ℎ = 𝑛 → ( ℎ ↑ 4 ) = ( 𝑛 ↑ 4 ) )
128 127 oveq2d ⊢ ( ℎ = 𝑛 → ( ( 𝑚 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) )
129 128 eqeq1d ⊢ ( ℎ = 𝑛 → ( ( ( 𝑚 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ↔ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) )
130 126 129 anbi12d ⊢ ( ℎ = 𝑛 → ( ( ( 𝑚 gcd ℎ ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ↔ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) )
131 130 anbi2d ⊢ ( ℎ = 𝑛 → ( ( ¬ 2 ∥ 𝑚 ∧ ( ( 𝑚 gcd ℎ ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ↔ ( ¬ 2 ∥ 𝑚 ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ) )
132 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → 𝑚 ∈ ℕ )
133 132 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑚 ) → 𝑚 ∈ ℕ )
134 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → 𝑛 ∈ ℕ )
135 134 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑚 ) → 𝑛 ∈ ℕ )
136 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑚 ) → ¬ 2 ∥ 𝑚 )
137 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑚 ) → ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) )
138 136 137 jca ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑚 ) → ( ¬ 2 ∥ 𝑚 ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) )
139 124 131 133 135 138 2rspcedvdw ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑚 ) → ∃ 𝑔 ∈ ℕ ∃ ℎ ∈ ℕ ( ¬ 2 ∥ 𝑔 ∧ ( ( 𝑔 gcd ℎ ) = 1 ∧ ( ( 𝑔 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) )
140 simp-4r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑚 ) → 𝑙 < 𝐶 )
141 139 140 jca ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑚 ) → ( ∃ 𝑔 ∈ ℕ ∃ ℎ ∈ ℕ ( ¬ 2 ∥ 𝑔 ∧ ( ( 𝑔 gcd ℎ ) = 1 ∧ ( ( 𝑔 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 𝑙 < 𝐶 ) )
142 breq2 ⊢ ( 𝑔 = 𝑛 → ( 2 ∥ 𝑔 ↔ 2 ∥ 𝑛 ) )
143 142 notbid ⊢ ( 𝑔 = 𝑛 → ( ¬ 2 ∥ 𝑔 ↔ ¬ 2 ∥ 𝑛 ) )
144 oveq1 ⊢ ( 𝑔 = 𝑛 → ( 𝑔 gcd ℎ ) = ( 𝑛 gcd ℎ ) )
145 144 eqeq1d ⊢ ( 𝑔 = 𝑛 → ( ( 𝑔 gcd ℎ ) = 1 ↔ ( 𝑛 gcd ℎ ) = 1 ) )
146 oveq1 ⊢ ( 𝑔 = 𝑛 → ( 𝑔 ↑ 4 ) = ( 𝑛 ↑ 4 ) )
147 146 oveq1d ⊢ ( 𝑔 = 𝑛 → ( ( 𝑔 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( ( 𝑛 ↑ 4 ) + ( ℎ ↑ 4 ) ) )
148 147 eqeq1d ⊢ ( 𝑔 = 𝑛 → ( ( ( 𝑔 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ↔ ( ( 𝑛 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) )
149 145 148 anbi12d ⊢ ( 𝑔 = 𝑛 → ( ( ( 𝑔 gcd ℎ ) = 1 ∧ ( ( 𝑔 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ↔ ( ( 𝑛 gcd ℎ ) = 1 ∧ ( ( 𝑛 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) )
150 143 149 anbi12d ⊢ ( 𝑔 = 𝑛 → ( ( ¬ 2 ∥ 𝑔 ∧ ( ( 𝑔 gcd ℎ ) = 1 ∧ ( ( 𝑔 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ↔ ( ¬ 2 ∥ 𝑛 ∧ ( ( 𝑛 gcd ℎ ) = 1 ∧ ( ( 𝑛 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ) )
151 oveq2 ⊢ ( ℎ = 𝑚 → ( 𝑛 gcd ℎ ) = ( 𝑛 gcd 𝑚 ) )
152 151 eqeq1d ⊢ ( ℎ = 𝑚 → ( ( 𝑛 gcd ℎ ) = 1 ↔ ( 𝑛 gcd 𝑚 ) = 1 ) )
153 oveq1 ⊢ ( ℎ = 𝑚 → ( ℎ ↑ 4 ) = ( 𝑚 ↑ 4 ) )
154 153 oveq2d ⊢ ( ℎ = 𝑚 → ( ( 𝑛 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( ( 𝑛 ↑ 4 ) + ( 𝑚 ↑ 4 ) ) )
155 154 eqeq1d ⊢ ( ℎ = 𝑚 → ( ( ( 𝑛 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ↔ ( ( 𝑛 ↑ 4 ) + ( 𝑚 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) )
156 152 155 anbi12d ⊢ ( ℎ = 𝑚 → ( ( ( 𝑛 gcd ℎ ) = 1 ∧ ( ( 𝑛 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ↔ ( ( 𝑛 gcd 𝑚 ) = 1 ∧ ( ( 𝑛 ↑ 4 ) + ( 𝑚 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) )
157 156 anbi2d ⊢ ( ℎ = 𝑚 → ( ( ¬ 2 ∥ 𝑛 ∧ ( ( 𝑛 gcd ℎ ) = 1 ∧ ( ( 𝑛 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ↔ ( ¬ 2 ∥ 𝑛 ∧ ( ( 𝑛 gcd 𝑚 ) = 1 ∧ ( ( 𝑛 ↑ 4 ) + ( 𝑚 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ) )
158 134 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑛 ) → 𝑛 ∈ ℕ )
159 132 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑛 ) → 𝑚 ∈ ℕ )
160 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑛 ) → ¬ 2 ∥ 𝑛 )
161 158 nnzd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑛 ) → 𝑛 ∈ ℤ )
162 159 nnzd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑛 ) → 𝑚 ∈ ℤ )
163 161 162 gcdcomd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑛 ) → ( 𝑛 gcd 𝑚 ) = ( 𝑚 gcd 𝑛 ) )
164 simplrl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑛 ) → ( 𝑚 gcd 𝑛 ) = 1 )
165 163 164 eqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑛 ) → ( 𝑛 gcd 𝑚 ) = 1 )
166 35 a1i ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑛 ) → 4 ∈ ℕ0 )
167 158 166 nnexpcld ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑛 ) → ( 𝑛 ↑ 4 ) ∈ ℕ )
168 167 nncnd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑛 ) → ( 𝑛 ↑ 4 ) ∈ ℂ )
169 159 166 nnexpcld ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑛 ) → ( 𝑚 ↑ 4 ) ∈ ℕ )
170 169 nncnd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑛 ) → ( 𝑚 ↑ 4 ) ∈ ℂ )
171 168 170 addcomd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑛 ) → ( ( 𝑛 ↑ 4 ) + ( 𝑚 ↑ 4 ) ) = ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) )
172 simplrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑛 ) → ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) )
173 171 172 eqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑛 ) → ( ( 𝑛 ↑ 4 ) + ( 𝑚 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) )
174 160 165 173 jca32 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑛 ) → ( ¬ 2 ∥ 𝑛 ∧ ( ( 𝑛 gcd 𝑚 ) = 1 ∧ ( ( 𝑛 ↑ 4 ) + ( 𝑚 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) )
175 150 157 158 159 174 2rspcedvdw ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑛 ) → ∃ 𝑔 ∈ ℕ ∃ ℎ ∈ ℕ ( ¬ 2 ∥ 𝑔 ∧ ( ( 𝑔 gcd ℎ ) = 1 ∧ ( ( 𝑔 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) )
176 simp-4r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑛 ) → 𝑙 < 𝐶 )
177 175 176 jca ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ ¬ 2 ∥ 𝑛 ) → ( ∃ 𝑔 ∈ ℕ ∃ ℎ ∈ ℕ ( ¬ 2 ∥ 𝑔 ∧ ( ( 𝑔 gcd ℎ ) = 1 ∧ ( ( 𝑔 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 𝑙 < 𝐶 ) )
178 132 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 2 ∥ 𝑚 ) → 𝑚 ∈ ℕ )
179 178 nnsqcld ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 2 ∥ 𝑚 ) → ( 𝑚 ↑ 2 ) ∈ ℕ )
180 134 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 2 ∥ 𝑚 ) → 𝑛 ∈ ℕ )
181 180 nnsqcld ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 2 ∥ 𝑚 ) → ( 𝑛 ↑ 2 ) ∈ ℕ )
182 simplrl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) → 𝑚 ∈ ℕ )
183 182 nnzd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) → 𝑚 ∈ ℤ )
184 59 a1i ⊢ ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) → 2 ∈ ℕ )
185 dvdsexp2im ⊢ ( ( 2 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 2 ∈ ℕ ) → ( 2 ∥ 𝑚 → 2 ∥ ( 𝑚 ↑ 2 ) ) )
186 42 183 184 185 mp3an2i ⊢ ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) → ( 2 ∥ 𝑚 → 2 ∥ ( 𝑚 ↑ 2 ) ) )
187 186 imp ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 2 ∥ 𝑚 ) → 2 ∥ ( 𝑚 ↑ 2 ) )
188 simplrl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 2 ∥ 𝑚 ) → ( 𝑚 gcd 𝑛 ) = 1 )
189 59 a1i ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 2 ∥ 𝑚 ) → 2 ∈ ℕ )
190 rppwr ⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ∧ 2 ∈ ℕ ) → ( ( 𝑚 gcd 𝑛 ) = 1 → ( ( 𝑚 ↑ 2 ) gcd ( 𝑛 ↑ 2 ) ) = 1 ) )
191 178 180 189 190 syl3anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 2 ∥ 𝑚 ) → ( ( 𝑚 gcd 𝑛 ) = 1 → ( ( 𝑚 ↑ 2 ) gcd ( 𝑛 ↑ 2 ) ) = 1 ) )
192 188 191 mpd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 2 ∥ 𝑚 ) → ( ( 𝑚 ↑ 2 ) gcd ( 𝑛 ↑ 2 ) ) = 1 )
193 179 181 187 192 flt4lem2 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 2 ∥ 𝑚 ) → ¬ 2 ∥ ( 𝑛 ↑ 2 ) )
194 180 nnzd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 2 ∥ 𝑚 ) → 𝑛 ∈ ℤ )
195 dvdsexp2im ⊢ ( ( 2 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 2 ∈ ℕ ) → ( 2 ∥ 𝑛 → 2 ∥ ( 𝑛 ↑ 2 ) ) )
196 42 194 189 195 mp3an2i ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 2 ∥ 𝑚 ) → ( 2 ∥ 𝑛 → 2 ∥ ( 𝑛 ↑ 2 ) ) )
197 193 196 mtod ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 2 ∥ 𝑚 ) → ¬ 2 ∥ 𝑛 )
198 197 ex ⊢ ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) → ( 2 ∥ 𝑚 → ¬ 2 ∥ 𝑛 ) )
199 imor ⊢ ( ( 2 ∥ 𝑚 → ¬ 2 ∥ 𝑛 ) ↔ ( ¬ 2 ∥ 𝑚 ∨ ¬ 2 ∥ 𝑛 ) )
200 198 199 sylib ⊢ ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) → ( ¬ 2 ∥ 𝑚 ∨ ¬ 2 ∥ 𝑛 ) )
201 141 177 200 mpjaodan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) → ( ∃ 𝑔 ∈ ℕ ∃ ℎ ∈ ℕ ( ¬ 2 ∥ 𝑔 ∧ ( ( 𝑔 gcd ℎ ) = 1 ∧ ( ( 𝑔 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 𝑙 < 𝐶 ) )
202 201 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) → ( ∃ 𝑔 ∈ ℕ ∃ ℎ ∈ ℕ ( ¬ 2 ∥ 𝑔 ∧ ( ( 𝑔 gcd ℎ ) = 1 ∧ ( ( 𝑔 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 𝑙 < 𝐶 ) ) )
203 202 rexlimdvva ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) → ( ∃ 𝑚 ∈ ℕ ∃ 𝑛 ∈ ℕ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) → ( ∃ 𝑔 ∈ ℕ ∃ ℎ ∈ ℕ ( ¬ 2 ∥ 𝑔 ∧ ( ( 𝑔 gcd ℎ ) = 1 ∧ ( ( 𝑔 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 𝑙 < 𝐶 ) ) )
204 203 expimpd ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) → ( ( 𝑙 < 𝐶 ∧ ∃ 𝑚 ∈ ℕ ∃ 𝑛 ∈ ℕ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) → ( ∃ 𝑔 ∈ ℕ ∃ ℎ ∈ ℕ ( ¬ 2 ∥ 𝑔 ∧ ( ( 𝑔 gcd ℎ ) = 1 ∧ ( ( 𝑔 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 𝑙 < 𝐶 ) ) )
205 204 reximdva ⊢ ( 𝜑 → ( ∃ 𝑙 ∈ ℕ ( 𝑙 < 𝐶 ∧ ∃ 𝑚 ∈ ℕ ∃ 𝑛 ∈ ℕ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) → ∃ 𝑙 ∈ ℕ ( ∃ 𝑔 ∈ ℕ ∃ ℎ ∈ ℕ ( ¬ 2 ∥ 𝑔 ∧ ( ( 𝑔 gcd ℎ ) = 1 ∧ ( ( 𝑔 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 𝑙 < 𝐶 ) ) )
206 115 205 mpd ⊢ ( 𝜑 → ∃ 𝑙 ∈ ℕ ( ∃ 𝑔 ∈ ℕ ∃ ℎ ∈ ℕ ( ¬ 2 ∥ 𝑔 ∧ ( ( 𝑔 gcd ℎ ) = 1 ∧ ( ( 𝑔 ↑ 4 ) + ( ℎ ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 𝑙 < 𝐶 ) )