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	flt4lem	⊢ ( 𝜑 → ( 𝐴 ↑ 4 ) = ( ( 𝐴 ↑ 2 ) ↑ 2 ) )
23	2	nncnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
24	23	flt4lem	⊢ ( 𝜑 → ( 𝐵 ↑ 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	flt4lem	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 2 ∥ 𝑚 ) → ( 𝑚 ↑ 4 ) = ( ( 𝑚 ↑ 2 ) ↑ 2 ) )
220	209	nncnd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 gcd 𝑛 ) = 1 ∧ ( ( 𝑚 ↑ 4 ) + ( 𝑛 ↑ 4 ) ) = ( 𝑙 ↑ 2 ) ) ) ∧ 2 ∥ 𝑚 ) → 𝑛 ∈ ℂ )
221	220	flt4lem	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ ) ∧ 𝑙 < 𝐶 ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 𝑚 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 ) ) ) ∧ 𝑙 < 𝐶 ) )