flt4lem7 - Mathbox for Steven Nguyen

	Mathbox for Steven Nguyen		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > flt4lem7		Structured version Visualization version GIF version

Theorem flt4lem7 43014

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

**Hypotheses**
Ref	Expression
flt4lem7.a	⊢ (𝜑 → 𝐴 ∈ ℕ)
flt4lem7.b	⊢ (𝜑 → 𝐵 ∈ ℕ)
flt4lem7.c	⊢ (𝜑 → 𝐶 ∈ ℕ)
flt4lem7.1	⊢ (𝜑 → ¬ 2 ∥ 𝐴)
flt4lem7.2	⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)
flt4lem7.3	⊢ (𝜑 → ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2))

**Assertion**
Ref	Expression
flt4lem7	⊢ (𝜑 → ∃𝑙 ∈ ℕ (∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶))

Distinct variable groups: 𝜑,𝑙 𝐵,𝑙 𝐶,𝑙 𝑔,ℎ,𝑙 Allowed substitution hints: 𝜑(𝑔,ℎ) 𝐴(𝑔,ℎ,𝑙) 𝐵(𝑔,ℎ) 𝐶(𝑔,ℎ)

Proof of Theorem flt4lem7 Dummy variables 𝑚 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq1 5103	. . . 4 ⊢ (𝑙 = ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) → (𝑙 < 𝐶 ↔ ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) < 𝐶))
2		oveq1 7375	. . . . . . 7 ⊢ (𝑙 = ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) → (𝑙↑2) = (((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2))↑2))
3	2	eqeq2d 2748	. . . . . 6 ⊢ (𝑙 = ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) → (((𝑚↑4) + (𝑛↑4)) = (𝑙↑2) ↔ ((𝑚↑4) + (𝑛↑4)) = (((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2))↑2)))
4	3	anbi2d 631	. . . . 5 ⊢ (𝑙 = ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) → (((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2)) ↔ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2))↑2))))
5	4	2rexbidv 3203	. . . 4 ⊢ (𝑙 = ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) → (∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2)) ↔ ∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2))↑2))))
6	1, 5	anbi12d 633	. . 3 ⊢ (𝑙 = ((((√‘(𝐶 + (𝐵↑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)))))
7		eqid 2737	. . . . . . 7 ⊢ (((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) = (((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2)
8		eqid 2737	. . . . . . 7 ⊢ (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2) = (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)
9		eqid 2737	. . . . . . 7 ⊢ (((√‘((((√‘(𝐶 + (𝐵↑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)
10		eqid 2737	. . . . . . 7 ⊢ (((√‘((((√‘(𝐶 + (𝐵↑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)
11		flt4lem7.a	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℕ)
12		flt4lem7.b	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℕ)
13		flt4lem7.c	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ ℕ)
14		flt4lem7.1	. . . . . . 7 ⊢ (𝜑 → ¬ 2 ∥ 𝐴)
15	11	nnsqcld 14179	. . . . . . . . 9 ⊢ (𝜑 → (𝐴↑2) ∈ ℕ)
16	12	nnsqcld 14179	. . . . . . . . 9 ⊢ (𝜑 → (𝐵↑2) ∈ ℕ)
17		2nn0 12430	. . . . . . . . . 10 ⊢ 2 ∈ ℕ₀
18	17	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 2 ∈ ℕ₀)
19	11	nncnd 12173	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ ℂ)
20	19	flt4lem 43000	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴↑4) = ((𝐴↑2)↑2))
21	12	nncnd 12173	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ ℂ)
22	21	flt4lem 43000	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵↑4) = ((𝐵↑2)↑2))
23	20, 22	oveq12d 7386	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴↑4) + (𝐵↑4)) = (((𝐴↑2)↑2) + ((𝐵↑2)↑2)))
24		flt4lem7.3	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2))
25	23, 24	eqtr3d 2774	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴↑2)↑2) + ((𝐵↑2)↑2)) = (𝐶↑2))
26		flt4lem7.2	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)
27		2nn 12230	. . . . . . . . . . . 12 ⊢ 2 ∈ ℕ
28	27	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ∈ ℕ)
29		rppwr 16499	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 2 ∈ ℕ) → ((𝐴 gcd 𝐵) = 1 → ((𝐴↑2) gcd (𝐵↑2)) = 1))
30	11, 12, 28, 29	syl3anc 1374	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 gcd 𝐵) = 1 → ((𝐴↑2) gcd (𝐵↑2)) = 1))
31	26, 30	mpd 15	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴↑2) gcd (𝐵↑2)) = 1)
32	15, 16, 13, 18, 25, 31	fltaccoprm 42995	. . . . . . . 8 ⊢ (𝜑 → ((𝐴↑2) gcd 𝐶) = 1)
33	11	nnzd 12526	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ ℤ)
34	13	nnzd 12526	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ ℤ)
35		rpexp 16661	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ 2 ∈ ℕ) → (((𝐴↑2) gcd 𝐶) = 1 ↔ (𝐴 gcd 𝐶) = 1))
36	33, 34, 28, 35	syl3anc 1374	. . . . . . . 8 ⊢ (𝜑 → (((𝐴↑2) gcd 𝐶) = 1 ↔ (𝐴 gcd 𝐶) = 1))
37	32, 36	mpbid 232	. . . . . . 7 ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1)
38	7, 8, 9, 10, 11, 12, 13, 14, 37, 24	flt4lem5e 43011	. . . . . 6 ⊢ (𝜑 → ((((((√‘((((√‘(𝐶 + (𝐵↑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 1144	. . . . 5 ⊢ (𝜑 → ((((√‘((((√‘(𝐶 + (𝐵↑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 1145	. . . 4 ⊢ (𝜑 → (((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) ∈ ℕ)
41	38	simp3d 1145	. . . . 5 ⊢ (𝜑 → (((((√‘(𝐶 + (𝐵↑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 495	. . . 4 ⊢ (𝜑 → (𝐵 / 2) ∈ ℕ)
43		gcdnncl 16446	. . . 4 ⊢ (((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) ∈ ℕ ∧ (𝐵 / 2) ∈ ℕ) → ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) ∈ ℕ)
44	40, 42, 43	syl2anc 585	. . 3 ⊢ (𝜑 → ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) ∈ ℕ)
45	44	nnred 12172	. . . . 5 ⊢ (𝜑 → ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) ∈ ℝ)
46	42	nnred 12172	. . . . 5 ⊢ (𝜑 → (𝐵 / 2) ∈ ℝ)
47	13	nnred 12172	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ ℝ)
48	40	nnzd 12526	. . . . . 6 ⊢ (𝜑 → (((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) ∈ ℤ)
49	48, 42	gcdle2d 42698	. . . . 5 ⊢ (𝜑 → ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) ≤ (𝐵 / 2))
50	12	nnred 12172	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ ℝ)
51	12	nnrpd 12959	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℝ⁺)
52		rphalflt 12948	. . . . . . 7 ⊢ (𝐵 ∈ ℝ⁺ → (𝐵 / 2) < 𝐵)
53	51, 52	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐵 / 2) < 𝐵)
54	16	nnred 12172	. . . . . . . 8 ⊢ (𝜑 → (𝐵↑2) ∈ ℝ)
55		4nn0 12432	. . . . . . . . . . 11 ⊢ 4 ∈ ℕ₀
56	55	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 4 ∈ ℕ₀)
57	12, 56	nnexpcld 14180	. . . . . . . . 9 ⊢ (𝜑 → (𝐵↑4) ∈ ℕ)
58	57	nnred 12172	. . . . . . . 8 ⊢ (𝜑 → (𝐵↑4) ∈ ℝ)
59	13	nnsqcld 14179	. . . . . . . . 9 ⊢ (𝜑 → (𝐶↑2) ∈ ℕ)
60	59	nnred 12172	. . . . . . . 8 ⊢ (𝜑 → (𝐶↑2) ∈ ℝ)
61		2lt4 12327	. . . . . . . . 9 ⊢ 2 < 4
62		2z 12535	. . . . . . . . . . 11 ⊢ 2 ∈ ℤ
63	62	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 2 ∈ ℤ)
64		4z 12537	. . . . . . . . . . 11 ⊢ 4 ∈ ℤ
65	64	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 4 ∈ ℤ)
66		1red 11145	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℝ)
67		2re 12231	. . . . . . . . . . . 12 ⊢ 2 ∈ ℝ
68	67	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ∈ ℝ)
69		1lt2 12323	. . . . . . . . . . . 12 ⊢ 1 < 2
70	69	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 1 < 2)
71		2t1e2 12315	. . . . . . . . . . . 12 ⊢ (2 · 1) = 2
72	42	nnge1d 12205	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 ≤ (𝐵 / 2))
73		2rp 12922	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℝ⁺
74	73	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 2 ∈ ℝ⁺)
75	66, 50, 74	lemuldiv2d 13011	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 · 1) ≤ 𝐵 ↔ 1 ≤ (𝐵 / 2)))
76	72, 75	mpbird 257	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 · 1) ≤ 𝐵)
77	71, 76	eqbrtrrid 5136	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ≤ 𝐵)
78	66, 68, 50, 70, 77	ltletrd 11305	. . . . . . . . . 10 ⊢ (𝜑 → 1 < 𝐵)
79	50, 63, 65, 78	ltexp2d 14186	. . . . . . . . 9 ⊢ (𝜑 → (2 < 4 ↔ (𝐵↑2) < (𝐵↑4)))
80	61, 79	mpbii 233	. . . . . . . 8 ⊢ (𝜑 → (𝐵↑2) < (𝐵↑4))
81	11, 56	nnexpcld 14180	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴↑4) ∈ ℕ)
82	81	nngt0d 12206	. . . . . . . . . 10 ⊢ (𝜑 → 0 < (𝐴↑4))
83	81	nnred 12172	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴↑4) ∈ ℝ)
84	83, 58	ltaddpos2d 11734	. . . . . . . . . 10 ⊢ (𝜑 → (0 < (𝐴↑4) ↔ (𝐵↑4) < ((𝐴↑4) + (𝐵↑4))))
85	82, 84	mpbid 232	. . . . . . . . 9 ⊢ (𝜑 → (𝐵↑4) < ((𝐴↑4) + (𝐵↑4)))
86	85, 24	breqtrd 5126	. . . . . . . 8 ⊢ (𝜑 → (𝐵↑4) < (𝐶↑2))
87	54, 58, 60, 80, 86	lttrd 11306	. . . . . . 7 ⊢ (𝜑 → (𝐵↑2) < (𝐶↑2))
88	13	nnrpd 12959	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ ℝ⁺)
89	51, 88, 28	ltexp1d 14194	. . . . . . 7 ⊢ (𝜑 → (𝐵 < 𝐶 ↔ (𝐵↑2) < (𝐶↑2)))
90	87, 89	mpbird 257	. . . . . 6 ⊢ (𝜑 → 𝐵 < 𝐶)
91	46, 50, 47, 53, 90	lttrd 11306	. . . . 5 ⊢ (𝜑 → (𝐵 / 2) < 𝐶)
92	45, 46, 47, 49, 91	lelttrd 11303	. . . 4 ⊢ (𝜑 → ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) < 𝐶)
93		oveq1 7375	. . . . . . 7 ⊢ (𝑚 = ((((√‘((((√‘(𝐶 + (𝐵↑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 2739	. . . . . 6 ⊢ (𝑚 = ((((√‘((((√‘(𝐶 + (𝐵↑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 7375	. . . . . . . 8 ⊢ (𝑚 = ((((√‘((((√‘(𝐶 + (𝐵↑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 7383	. . . . . . 7 ⊢ (𝑚 = ((((√‘((((√‘(𝐶 + (𝐵↑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 2739	. . . . . 6 ⊢ (𝑚 = ((((√‘((((√‘(𝐶 + (𝐵↑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 633	. . . . 5 ⊢ (𝑚 = ((((√‘((((√‘(𝐶 + (𝐵↑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 7376	. . . . . . 7 ⊢ (𝑛 = ((((√‘((((√‘(𝐶 + (𝐵↑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 2739	. . . . . 6 ⊢ (𝑛 = ((((√‘((((√‘(𝐶 + (𝐵↑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 7375	. . . . . . . 8 ⊢ (𝑛 = ((((√‘((((√‘(𝐶 + (𝐵↑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 7384	. . . . . . 7 ⊢ (𝑛 = ((((√‘((((√‘(𝐶 + (𝐵↑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 2739	. . . . . 6 ⊢ (𝑛 = ((((√‘((((√‘(𝐶 + (𝐵↑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 633	. . . . 5 ⊢ (𝑛 = ((((√‘((((√‘(𝐶 + (𝐵↑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 1143	. . . . . 6 ⊢ (𝜑 → (((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) + (√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) − (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)))) / 2) ∈ ℕ)
106		gcdnncl 16446	. . . . . 6 ⊢ (((((√‘((((√‘(𝐶 + (𝐵↑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 585	. . . . 5 ⊢ (𝜑 → ((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) + (√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) − (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)))) / 2) gcd (𝐵 / 2)) ∈ ℕ)
108	39	simp2d 1144	. . . . . 6 ⊢ (𝜑 → (((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) − (√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) − (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)))) / 2) ∈ ℕ)
109		gcdnncl 16446	. . . . . 6 ⊢ (((((√‘((((√‘(𝐶 + (𝐵↑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 585	. . . . 5 ⊢ (𝜑 → ((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) − (√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) − (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)))) / 2) gcd (𝐵 / 2)) ∈ ℕ)
111	105	nnzd 12526	. . . . . . . 8 ⊢ (𝜑 → (((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) + (√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) − (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)))) / 2) ∈ ℤ)
112	42	nnzd 12526	. . . . . . . 8 ⊢ (𝜑 → (𝐵 / 2) ∈ ℤ)
113	110	nnzd 12526	. . . . . . . 8 ⊢ (𝜑 → ((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) − (√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) − (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)))) / 2) gcd (𝐵 / 2)) ∈ ℤ)
114		gcdass 16486	. . . . . . . 8 ⊢ (((((√‘((((√‘(𝐶 + (𝐵↑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 1374	. . . . . . 7 ⊢ (𝜑 → (((((√‘((((√‘(𝐶 + (𝐵↑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 12526	. . . . . . . . . 10 ⊢ (𝜑 → (((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) − (√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) − (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)))) / 2) ∈ ℤ)
117		gcdass 16486	. . . . . . . . . 10 ⊢ (((𝐵 / 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 1374	. . . . . . . . 9 ⊢ (𝜑 → (((𝐵 / 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 12474	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵 / 2) ∈ ℕ₀)
120		gcdnn0id 42696	. . . . . . . . . . . 12 ⊢ ((𝐵 / 2) ∈ ℕ₀ → ((𝐵 / 2) gcd (𝐵 / 2)) = (𝐵 / 2))
121	119, 120	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 / 2) gcd (𝐵 / 2)) = (𝐵 / 2))
122	121	oveq1d 7383	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐵 / 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 16453	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵 / 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 2773	. . . . . . . . 9 ⊢ (𝜑 → ((((√‘((((√‘(𝐶 + (𝐵↑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 16453	. . . . . . . . . 10 ⊢ (𝜑 → ((((√‘((((√‘(𝐶 + (𝐵↑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 7384	. . . . . . . . 9 ⊢ (𝜑 → ((𝐵 / 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 2783	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 / 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 7384	. . . . . . 7 ⊢ (𝜑 → ((((√‘((((√‘(𝐶 + (𝐵↑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 1143	. . . . . . . . . 10 ⊢ (𝜑 → (((((√‘((((√‘(𝐶 + (𝐵↑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 1143	. . . . . . . . 9 ⊢ (𝜑 → ((((√‘((((√‘(𝐶 + (𝐵↑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 7383	. . . . . . . 8 ⊢ (𝜑 → (((((√‘((((√‘(𝐶 + (𝐵↑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 16486	. . . . . . . . 9 ⊢ (((((√‘((((√‘(𝐶 + (𝐵↑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 1374	. . . . . . . 8 ⊢ (𝜑 → (((((√‘((((√‘(𝐶 + (𝐵↑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 16472	. . . . . . . . 9 ⊢ ((𝐵 / 2) ∈ ℤ → (1 gcd (𝐵 / 2)) = 1)
135	112, 134	syl 17	. . . . . . . 8 ⊢ (𝜑 → (1 gcd (𝐵 / 2)) = 1)
136	131, 133, 135	3eqtr3d 2780	. . . . . . 7 ⊢ (𝜑 → ((((√‘((((√‘(𝐶 + (𝐵↑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 2776	. . . . . 6 ⊢ (𝜑 → (((((√‘((((√‘(𝐶 + (𝐵↑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	7, 8, 9, 10, 11, 12, 13, 14, 37, 24	flt4lem5f 43012	. . . . . . 7 ⊢ (𝜑 → (((((√‘(𝐶 + (𝐵↑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 2743	. . . . . 6 ⊢ (𝜑 → ((((((√‘((((√‘(𝐶 + (𝐵↑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 511	. . . . 5 ⊢ (𝜑 → ((((((√‘((((√‘(𝐶 + (𝐵↑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 3592	. . . 4 ⊢ (𝜑 → ∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2))↑2)))
142	92, 141	jca 511	. . 3 ⊢ (𝜑 → (((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) < 𝐶 ∧ ∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2))↑2))))
143	6, 44, 142	rspcedvdw 3581	. 2 ⊢ (𝜑 → ∃𝑙 ∈ ℕ (𝑙 < 𝐶 ∧ ∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))))
144		breq2 5104	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑚 → (2 ∥ 𝑔 ↔ 2 ∥ 𝑚))
145	144	notbid 318	. . . . . . . . . 10 ⊢ (𝑔 = 𝑚 → (¬ 2 ∥ 𝑔 ↔ ¬ 2 ∥ 𝑚))
146		oveq1 7375	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑚 → (𝑔 gcd ℎ) = (𝑚 gcd ℎ))
147	146	eqeq1d 2739	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑚 → ((𝑔 gcd ℎ) = 1 ↔ (𝑚 gcd ℎ) = 1))
148		oveq1 7375	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑚 → (𝑔↑4) = (𝑚↑4))
149	148	oveq1d 7383	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑚 → ((𝑔↑4) + (ℎ↑4)) = ((𝑚↑4) + (ℎ↑4)))
150	149	eqeq1d 2739	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑚 → (((𝑔↑4) + (ℎ↑4)) = (𝑙↑2) ↔ ((𝑚↑4) + (ℎ↑4)) = (𝑙↑2)))
151	147, 150	anbi12d 633	. . . . . . . . . 10 ⊢ (𝑔 = 𝑚 → (((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2)) ↔ ((𝑚 gcd ℎ) = 1 ∧ ((𝑚↑4) + (ℎ↑4)) = (𝑙↑2))))
152	145, 151	anbi12d 633	. . . . . . . . 9 ⊢ (𝑔 = 𝑚 → ((¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ↔ (¬ 2 ∥ 𝑚 ∧ ((𝑚 gcd ℎ) = 1 ∧ ((𝑚↑4) + (ℎ↑4)) = (𝑙↑2)))))
153		oveq2 7376	. . . . . . . . . . . 12 ⊢ (ℎ = 𝑛 → (𝑚 gcd ℎ) = (𝑚 gcd 𝑛))
154	153	eqeq1d 2739	. . . . . . . . . . 11 ⊢ (ℎ = 𝑛 → ((𝑚 gcd ℎ) = 1 ↔ (𝑚 gcd 𝑛) = 1))
155		oveq1 7375	. . . . . . . . . . . . 13 ⊢ (ℎ = 𝑛 → (ℎ↑4) = (𝑛↑4))
156	155	oveq2d 7384	. . . . . . . . . . . 12 ⊢ (ℎ = 𝑛 → ((𝑚↑4) + (ℎ↑4)) = ((𝑚↑4) + (𝑛↑4)))
157	156	eqeq1d 2739	. . . . . . . . . . 11 ⊢ (ℎ = 𝑛 → (((𝑚↑4) + (ℎ↑4)) = (𝑙↑2) ↔ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2)))
158	154, 157	anbi12d 633	. . . . . . . . . 10 ⊢ (ℎ = 𝑛 → (((𝑚 gcd ℎ) = 1 ∧ ((𝑚↑4) + (ℎ↑4)) = (𝑙↑2)) ↔ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))))
159	158	anbi2d 631	. . . . . . . . 9 ⊢ (ℎ = 𝑛 → ((¬ 2 ∥ 𝑚 ∧ ((𝑚 gcd ℎ) = 1 ∧ ((𝑚↑4) + (ℎ↑4)) = (𝑙↑2))) ↔ (¬ 2 ∥ 𝑚 ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2)))))
160		simplrl 777	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → 𝑚 ∈ ℕ)
161	160	adantr 480	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑚) → 𝑚 ∈ ℕ)
162		simprr 773	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → 𝑛 ∈ ℕ)
163	162	ad2antrr 727	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑚) → 𝑛 ∈ ℕ)
164		simpr 484	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑚) → ¬ 2 ∥ 𝑚)
165		simplr 769	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑚) → ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2)))
166	164, 165	jca 511	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑚) → (¬ 2 ∥ 𝑚 ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))))
167	152, 159, 161, 163, 166	2rspcedvdw 3592	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑚) → ∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))))
168		simp-4r 784	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑚) → 𝑙 < 𝐶)
169	167, 168	jca 511	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑚) → (∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶))
170		breq2 5104	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑛 → (2 ∥ 𝑔 ↔ 2 ∥ 𝑛))
171	170	notbid 318	. . . . . . . . . 10 ⊢ (𝑔 = 𝑛 → (¬ 2 ∥ 𝑔 ↔ ¬ 2 ∥ 𝑛))
172		oveq1 7375	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑛 → (𝑔 gcd ℎ) = (𝑛 gcd ℎ))
173	172	eqeq1d 2739	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑛 → ((𝑔 gcd ℎ) = 1 ↔ (𝑛 gcd ℎ) = 1))
174		oveq1 7375	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑛 → (𝑔↑4) = (𝑛↑4))
175	174	oveq1d 7383	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑛 → ((𝑔↑4) + (ℎ↑4)) = ((𝑛↑4) + (ℎ↑4)))
176	175	eqeq1d 2739	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑛 → (((𝑔↑4) + (ℎ↑4)) = (𝑙↑2) ↔ ((𝑛↑4) + (ℎ↑4)) = (𝑙↑2)))
177	173, 176	anbi12d 633	. . . . . . . . . 10 ⊢ (𝑔 = 𝑛 → (((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2)) ↔ ((𝑛 gcd ℎ) = 1 ∧ ((𝑛↑4) + (ℎ↑4)) = (𝑙↑2))))
178	171, 177	anbi12d 633	. . . . . . . . 9 ⊢ (𝑔 = 𝑛 → ((¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ↔ (¬ 2 ∥ 𝑛 ∧ ((𝑛 gcd ℎ) = 1 ∧ ((𝑛↑4) + (ℎ↑4)) = (𝑙↑2)))))
179		oveq2 7376	. . . . . . . . . . . 12 ⊢ (ℎ = 𝑚 → (𝑛 gcd ℎ) = (𝑛 gcd 𝑚))
180	179	eqeq1d 2739	. . . . . . . . . . 11 ⊢ (ℎ = 𝑚 → ((𝑛 gcd ℎ) = 1 ↔ (𝑛 gcd 𝑚) = 1))
181		oveq1 7375	. . . . . . . . . . . . 13 ⊢ (ℎ = 𝑚 → (ℎ↑4) = (𝑚↑4))
182	181	oveq2d 7384	. . . . . . . . . . . 12 ⊢ (ℎ = 𝑚 → ((𝑛↑4) + (ℎ↑4)) = ((𝑛↑4) + (𝑚↑4)))
183	182	eqeq1d 2739	. . . . . . . . . . 11 ⊢ (ℎ = 𝑚 → (((𝑛↑4) + (ℎ↑4)) = (𝑙↑2) ↔ ((𝑛↑4) + (𝑚↑4)) = (𝑙↑2)))
184	180, 183	anbi12d 633	. . . . . . . . . 10 ⊢ (ℎ = 𝑚 → (((𝑛 gcd ℎ) = 1 ∧ ((𝑛↑4) + (ℎ↑4)) = (𝑙↑2)) ↔ ((𝑛 gcd 𝑚) = 1 ∧ ((𝑛↑4) + (𝑚↑4)) = (𝑙↑2))))
185	184	anbi2d 631	. . . . . . . . 9 ⊢ (ℎ = 𝑚 → ((¬ 2 ∥ 𝑛 ∧ ((𝑛 gcd ℎ) = 1 ∧ ((𝑛↑4) + (ℎ↑4)) = (𝑙↑2))) ↔ (¬ 2 ∥ 𝑛 ∧ ((𝑛 gcd 𝑚) = 1 ∧ ((𝑛↑4) + (𝑚↑4)) = (𝑙↑2)))))
186	162	ad2antrr 727	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → 𝑛 ∈ ℕ)
187	160	adantr 480	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → 𝑚 ∈ ℕ)
188		simpr 484	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → ¬ 2 ∥ 𝑛)
189	186	nnzd 12526	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → 𝑛 ∈ ℤ)
190	187	nnzd 12526	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → 𝑚 ∈ ℤ)
191	189, 190	gcdcomd 16453	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (𝑛 gcd 𝑚) = (𝑚 gcd 𝑛))
192		simplrl 777	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (𝑚 gcd 𝑛) = 1)
193	191, 192	eqtrd 2772	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (𝑛 gcd 𝑚) = 1)
194	55	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → 4 ∈ ℕ₀)
195	186, 194	nnexpcld 14180	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (𝑛↑4) ∈ ℕ)
196	195	nncnd 12173	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (𝑛↑4) ∈ ℂ)
197	187, 194	nnexpcld 14180	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (𝑚↑4) ∈ ℕ)
198	197	nncnd 12173	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (𝑚↑4) ∈ ℂ)
199	196, 198	addcomd 11347	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → ((𝑛↑4) + (𝑚↑4)) = ((𝑚↑4) + (𝑛↑4)))
200		simplrr 778	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))
201	199, 200	eqtrd 2772	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → ((𝑛↑4) + (𝑚↑4)) = (𝑙↑2))
202	188, 193, 201	jca32 515	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (¬ 2 ∥ 𝑛 ∧ ((𝑛 gcd 𝑚) = 1 ∧ ((𝑛↑4) + (𝑚↑4)) = (𝑙↑2))))
203	178, 185, 186, 187, 202	2rspcedvdw 3592	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → ∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))))
204		simp-4r 784	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → 𝑙 < 𝐶)
205	203, 204	jca 511	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶))
206		simprl 771	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → 𝑚 ∈ ℕ)
207	206	ad2antrr 727	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → 𝑚 ∈ ℕ)
208	207	nnsqcld 14179	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → (𝑚↑2) ∈ ℕ)
209	162	ad2antrr 727	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → 𝑛 ∈ ℕ)
210	209	nnsqcld 14179	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → (𝑛↑2) ∈ ℕ)
211		simp-5r 786	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → 𝑙 ∈ ℕ)
212	160	nnzd 12526	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → 𝑚 ∈ ℤ)
213	27	a1i 11	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → 2 ∈ ℕ)
214		dvdsexp2im 16266	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 2 ∈ ℕ) → (2 ∥ 𝑚 → 2 ∥ (𝑚↑2)))
215	62, 212, 213, 214	mp3an2i 1469	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → (2 ∥ 𝑚 → 2 ∥ (𝑚↑2)))
216	215	imp 406	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → 2 ∥ (𝑚↑2))
217	17	a1i 11	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → 2 ∈ ℕ₀)
218	207	nncnd 12173	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → 𝑚 ∈ ℂ)
219	218	flt4lem 43000	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → (𝑚↑4) = ((𝑚↑2)↑2))
220	209	nncnd 12173	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → 𝑛 ∈ ℂ)
221	220	flt4lem 43000	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → (𝑛↑4) = ((𝑛↑2)↑2))
222	219, 221	oveq12d 7386	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → ((𝑚↑4) + (𝑛↑4)) = (((𝑚↑2)↑2) + ((𝑛↑2)↑2)))
223		simplrr 778	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))
224	222, 223	eqtr3d 2774	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → (((𝑚↑2)↑2) + ((𝑛↑2)↑2)) = (𝑙↑2))
225		simplrl 777	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → (𝑚 gcd 𝑛) = 1)
226	27	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → 2 ∈ ℕ)
227		rppwr 16499	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ∧ 2 ∈ ℕ) → ((𝑚 gcd 𝑛) = 1 → ((𝑚↑2) gcd (𝑛↑2)) = 1))
228	207, 209, 226, 227	syl3anc 1374	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → ((𝑚 gcd 𝑛) = 1 → ((𝑚↑2) gcd (𝑛↑2)) = 1))
229	225, 228	mpd 15	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → ((𝑚↑2) gcd (𝑛↑2)) = 1)
230	208, 210, 211, 217, 224, 229	fltaccoprm 42995	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → ((𝑚↑2) gcd 𝑙) = 1)
231	208, 210, 211, 216, 230, 224	flt4lem2 43002	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → ¬ 2 ∥ (𝑛↑2))
232	209	nnzd 12526	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → 𝑛 ∈ ℤ)
233		dvdsexp2im 16266	. . . . . . . . . . 11 ⊢ ((2 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 2 ∈ ℕ) → (2 ∥ 𝑛 → 2 ∥ (𝑛↑2)))
234	62, 232, 226, 233	mp3an2i 1469	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → (2 ∥ 𝑛 → 2 ∥ (𝑛↑2)))
235	231, 234	mtod 198	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → ¬ 2 ∥ 𝑛)
236	235	ex 412	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → (2 ∥ 𝑚 → ¬ 2 ∥ 𝑛))
237		imor 854	. . . . . . . 8 ⊢ ((2 ∥ 𝑚 → ¬ 2 ∥ 𝑛) ↔ (¬ 2 ∥ 𝑚 ∨ ¬ 2 ∥ 𝑛))
238	236, 237	sylib 218	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → (¬ 2 ∥ 𝑚 ∨ ¬ 2 ∥ 𝑛))
239	169, 205, 238	mpjaodan 961	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → (∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶))
240	239	ex 412	. . . . 5 ⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → (((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2)) → (∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶)))
241	240	rexlimdvva 3195	. . . 4 ⊢ (((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) → (∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2)) → (∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶)))
242	241	expimpd 453	. . 3 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → ((𝑙 < 𝐶 ∧ ∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → (∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶)))
243	242	reximdva 3151	. 2 ⊢ (𝜑 → (∃𝑙 ∈ ℕ (𝑙 < 𝐶 ∧ ∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → ∃𝑙 ∈ ℕ (∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶)))
244	143, 243	mpd 15	1 ⊢ (𝜑 → ∃𝑙 ∈ ℕ (∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 848 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ∃wrex 3062 class class class wbr 5100 ‘cfv 6500 (class class class)co 7368 ℝcr 11037 0cc0 11038 1c1 11039 + caddc 11041 · cmul 11043 < clt 11178 ≤ cle 11179 − cmin 11376 / cdiv 11806 ℕcn 12157 2c2 12212 4c4 12214 ℕ₀cn0 12413 ℤcz 12500 ℝ⁺crp 12917 ↑cexp 13996 √csqrt 15168 ∥ cdvds 16191 gcd cgcd 16433

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115 ax-pre-sup 11116

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-iun 4950 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5527 df-eprel 5532 df-po 5540 df-so 5541 df-fr 5585 df-we 5587 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-pred 6267 df-ord 6328 df-on 6329 df-lim 6330 df-suc 6331 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-riota 7325 df-ov 7371 df-oprab 7372 df-mpo 7373 df-om 7819 df-1st 7943 df-2nd 7944 df-frecs 8233 df-wrecs 8264 df-recs 8313 df-rdg 8351 df-1o 8407 df-2o 8408 df-er 8645 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-sup 9357 df-inf 9358 df-pnf 11180 df-mnf 11181 df-xr 11182 df-ltxr 11183 df-le 11184 df-sub 11378 df-neg 11379 df-div 11807 df-nn 12158 df-2 12220 df-3 12221 df-4 12222 df-n0 12414 df-z 12501 df-uz 12764 df-q 12874 df-rp 12918 df-fz 13436 df-fl 13724 df-mod 13802 df-seq 13937 df-exp 13997 df-cj 15034 df-re 15035 df-im 15036 df-sqrt 15170 df-abs 15171 df-dvds 16192 df-gcd 16434 df-prm 16611 df-numer 16674 df-denom 16675

This theorem is referenced by: nna4b4nsq 43015

W3C validator