flt4lem7 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > flt4lem7		Structured version Visualization version GIF version

Theorem flt4lem7 27971

Description: Convert flt4lem5f 27969 into a convenient form for nna4b4nsq 27972. 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 5106	. . . 4 ⊢ (𝑙 = ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) → (𝑙 < 𝐶 ↔ ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) < 𝐶))
2		oveq1 7419	. . . . . . 7 ⊢ (𝑙 = ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) → (𝑙↑2) = (((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2))↑2))
3	2	eqeq2d 2772	. . . . . 6 ⊢ (𝑙 = ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) → (((𝑚↑4) + (𝑛↑4)) = (𝑙↑2) ↔ ((𝑚↑4) + (𝑛↑4)) = (((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2))↑2)))
4	3	anbi2d 642	. . . . 5 ⊢ (𝑙 = ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) → (((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2)) ↔ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2))↑2))))
5	4	2rexbidv 3228	. . . 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 644	. . 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 2761	. . . . . . 7 ⊢ (((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) = (((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2)
8		eqid 2761	. . . . . . 7 ⊢ (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2) = (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)
9		eqid 2761	. . . . . . 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 2761	. . . . . . 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 14368	. . . . . . . . 9 ⊢ (𝜑 → (𝐴↑2) ∈ ℕ)
16	12	nnsqcld 14368	. . . . . . . . 9 ⊢ (𝜑 → (𝐵↑2) ∈ ℕ)
17		2nn0 12604	. . . . . . . . . 10 ⊢ 2 ∈ ℕ₀
18	17	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 2 ∈ ℕ₀)
19	11	nncnd 12332	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ ℂ)
20	19	exp4sqsq 14324	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴↑4) = ((𝐴↑2)↑2))
21	12	nncnd 12332	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ ℂ)
22	21	exp4sqsq 14324	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵↑4) = ((𝐵↑2)↑2))
23	20, 22	oveq12d 7430	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴↑4) + (𝐵↑4)) = (((𝐴↑2)↑2) + ((𝐵↑2)↑2)))
24		flt4lem7.3	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2))
25	23, 24	eqtr3d 2798	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴↑2)↑2) + ((𝐵↑2)↑2)) = (𝐶↑2))
26		flt4lem7.2	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)
27		2nn 12397	. . . . . . . . . . . 12 ⊢ 2 ∈ ℕ
28	27	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ∈ ℕ)
29		rppwr 16714	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 2 ∈ ℕ) → ((𝐴 gcd 𝐵) = 1 → ((𝐴↑2) gcd (𝐵↑2)) = 1))
30	11, 12, 28, 29	syl3anc 1398	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 gcd 𝐵) = 1 → ((𝐴↑2) gcd (𝐵↑2)) = 1))
31	26, 30	mpd 16	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴↑2) gcd (𝐵↑2)) = 1)
32	15, 16, 13, 18, 25, 31	fltaccoprm 27954	. . . . . . . 8 ⊢ (𝜑 → ((𝐴↑2) gcd 𝐶) = 1)
33	11	nnzd 12700	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ ℤ)
34	13	nnzd 12700	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ ℤ)
35		rpexp 16878	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ 2 ∈ ℕ) → (((𝐴↑2) gcd 𝐶) = 1 ↔ (𝐴 gcd 𝐶) = 1))
36	33, 34, 28, 35	syl3anc 1398	. . . . . . . 8 ⊢ (𝜑 → (((𝐴↑2) gcd 𝐶) = 1 ↔ (𝐴 gcd 𝐶) = 1))
37	32, 36	mpbid 235	. . . . . . 7 ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1)
38	7, 8, 9, 10, 11, 12, 13, 14, 37, 24	flt4lem5e 27968	. . . . . 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 1161	. . . . 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 1162	. . . 4 ⊢ (𝜑 → (((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) ∈ ℕ)
41	38	simp3d 1162	. . . . 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 501	. . . 4 ⊢ (𝜑 → (𝐵 / 2) ∈ ℕ)
43		gcdnncl 16657	. . . 4 ⊢ (((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) ∈ ℕ ∧ (𝐵 / 2) ∈ ℕ) → ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) ∈ ℕ)
44	40, 42, 43	syl2anc 596	. . 3 ⊢ (𝜑 → ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) ∈ ℕ)
45	44	nnred 12331	. . . . 5 ⊢ (𝜑 → ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) ∈ ℝ)
46	42	nnred 12331	. . . . 5 ⊢ (𝜑 → (𝐵 / 2) ∈ ℝ)
47	13	nnred 12331	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ ℝ)
48	40	nnzd 12700	. . . . . 6 ⊢ (𝜑 → (((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) ∈ ℤ)
49	48, 42	gcdle2d 16661	. . . . 5 ⊢ (𝜑 → ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) ≤ (𝐵 / 2))
50	12	nnred 12331	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ ℝ)
51	12	nnrpd 13143	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℝ⁺)
52		rphalflt 13132	. . . . . . 7 ⊢ (𝐵 ∈ ℝ⁺ → (𝐵 / 2) < 𝐵)
53	51, 52	syl 18	. . . . . 6 ⊢ (𝜑 → (𝐵 / 2) < 𝐵)
54	16	nnred 12331	. . . . . . . 8 ⊢ (𝜑 → (𝐵↑2) ∈ ℝ)
55		4nn0 12606	. . . . . . . . . . 11 ⊢ 4 ∈ ℕ₀
56	55	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 4 ∈ ℕ₀)
57	12, 56	nnexpcld 14369	. . . . . . . . 9 ⊢ (𝜑 → (𝐵↑4) ∈ ℕ)
58	57	nnred 12331	. . . . . . . 8 ⊢ (𝜑 → (𝐵↑4) ∈ ℝ)
59	13	nnsqcld 14368	. . . . . . . . 9 ⊢ (𝜑 → (𝐶↑2) ∈ ℕ)
60	59	nnred 12331	. . . . . . . 8 ⊢ (𝜑 → (𝐶↑2) ∈ ℝ)
61		2lt4 12501	. . . . . . . . 9 ⊢ 2 < 4
62		2z 12709	. . . . . . . . . . 11 ⊢ 2 ∈ ℤ
63	62	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 2 ∈ ℤ)
64		4z 12711	. . . . . . . . . . 11 ⊢ 4 ∈ ℤ
65	64	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 4 ∈ ℤ)
66		1red 11290	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℝ)
67		2re 12398	. . . . . . . . . . . 12 ⊢ 2 ∈ ℝ
68	67	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ∈ ℝ)
69		1lt2 12496	. . . . . . . . . . . 12 ⊢ 1 < 2
70	69	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 1 < 2)
71		2t1e2 12486	. . . . . . . . . . . 12 ⊢ (2 · 1) = 2
72	42	nnge1d 12367	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 ≤ (𝐵 / 2))
73		2rp 13106	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℝ⁺
74	73	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 2 ∈ ℝ⁺)
75	66, 50, 74	lemuldiv2d 13195	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 · 1) ≤ 𝐵 ↔ 1 ≤ (𝐵 / 2)))
76	72, 75	mpbird 260	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 · 1) ≤ 𝐵)
77	71, 76	eqbrtrrid 5141	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ≤ 𝐵)
78	66, 68, 50, 70, 77	ltletrd 11451	. . . . . . . . . 10 ⊢ (𝜑 → 1 < 𝐵)
79	50, 63, 65, 78	ltexp2d 14375	. . . . . . . . 9 ⊢ (𝜑 → (2 < 4 ↔ (𝐵↑2) < (𝐵↑4)))
80	61, 79	mpbii 236	. . . . . . . 8 ⊢ (𝜑 → (𝐵↑2) < (𝐵↑4))
81	11, 56	nnexpcld 14369	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴↑4) ∈ ℕ)
82	81	nngt0d 12368	. . . . . . . . . 10 ⊢ (𝜑 → 0 < (𝐴↑4))
83	81	nnred 12331	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴↑4) ∈ ℝ)
84	83, 58	ltaddpos2d 11882	. . . . . . . . . 10 ⊢ (𝜑 → (0 < (𝐴↑4) ↔ (𝐵↑4) < ((𝐴↑4) + (𝐵↑4))))
85	82, 84	mpbid 235	. . . . . . . . 9 ⊢ (𝜑 → (𝐵↑4) < ((𝐴↑4) + (𝐵↑4)))
86	85, 24	breqtrd 5131	. . . . . . . 8 ⊢ (𝜑 → (𝐵↑4) < (𝐶↑2))
87	54, 58, 60, 80, 86	lttrd 11452	. . . . . . 7 ⊢ (𝜑 → (𝐵↑2) < (𝐶↑2))
88	13	nnrpd 13143	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ ℝ⁺)
89	51, 88, 28	ltexp1d 14383	. . . . . . 7 ⊢ (𝜑 → (𝐵 < 𝐶 ↔ (𝐵↑2) < (𝐶↑2)))
90	87, 89	mpbird 260	. . . . . 6 ⊢ (𝜑 → 𝐵 < 𝐶)
91	46, 50, 47, 53, 90	lttrd 11452	. . . . 5 ⊢ (𝜑 → (𝐵 / 2) < 𝐶)
92	45, 46, 47, 49, 91	lelttrd 11449	. . . 4 ⊢ (𝜑 → ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) < 𝐶)
93		oveq1 7419	. . . . . . 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 2763	. . . . . 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 7419	. . . . . . . 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 7427	. . . . . . 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 2763	. . . . . 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 644	. . . . 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 7420	. . . . . . 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 2763	. . . . . 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 7419	. . . . . . . 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 7428	. . . . . . 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 2763	. . . . . 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 644	. . . . 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 1160	. . . . . 6 ⊢ (𝜑 → (((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) + (√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) − (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)))) / 2) ∈ ℕ)
106		gcdnncl 16657	. . . . . 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 596	. . . . 5 ⊢ (𝜑 → ((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) + (√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) − (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)))) / 2) gcd (𝐵 / 2)) ∈ ℕ)
108	39	simp2d 1161	. . . . . 6 ⊢ (𝜑 → (((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) − (√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) − (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)))) / 2) ∈ ℕ)
109		gcdnncl 16657	. . . . . 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 596	. . . . 5 ⊢ (𝜑 → ((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) − (√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) − (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)))) / 2) gcd (𝐵 / 2)) ∈ ℕ)
111	105	nnzd 12700	. . . . . . . 8 ⊢ (𝜑 → (((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) + (√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) − (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)))) / 2) ∈ ℤ)
112	42	nnzd 12700	. . . . . . . 8 ⊢ (𝜑 → (𝐵 / 2) ∈ ℤ)
113	110	nnzd 12700	. . . . . . . 8 ⊢ (𝜑 → ((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) − (√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) − (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)))) / 2) gcd (𝐵 / 2)) ∈ ℤ)
114		gcdass 16700	. . . . . . . 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 1398	. . . . . . 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 12700	. . . . . . . . . 10 ⊢ (𝜑 → (((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) − (√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) − (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)))) / 2) ∈ ℤ)
117		gcdass 16700	. . . . . . . . . 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 1398	. . . . . . . . 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 12648	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵 / 2) ∈ ℕ₀)
120		gcdnn0id 16680	. . . . . . . . . . . 12 ⊢ ((𝐵 / 2) ∈ ℕ₀ → ((𝐵 / 2) gcd (𝐵 / 2)) = (𝐵 / 2))
121	119, 120	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 / 2) gcd (𝐵 / 2)) = (𝐵 / 2))
122	121	oveq1d 7427	. . . . . . . . . 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 16666	. . . . . . . . . 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 2797	. . . . . . . . 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 16666	. . . . . . . . . 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 7428	. . . . . . . . 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 2807	. . . . . . . 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 7428	. . . . . . 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 1160	. . . . . . . . . 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 1160	. . . . . . . . 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 7427	. . . . . . . 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 16700	. . . . . . . . 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 1398	. . . . . . . 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 16686	. . . . . . . . 9 ⊢ ((𝐵 / 2) ∈ ℤ → (1 gcd (𝐵 / 2)) = 1)
135	112, 134	syl 18	. . . . . . . 8 ⊢ (𝜑 → (1 gcd (𝐵 / 2)) = 1)
136	131, 133, 135	3eqtr3d 2804	. . . . . . 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 2800	. . . . . 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 27969	. . . . . . 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 2767	. . . . . 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 521	. . . . 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 3590	. . . 4 ⊢ (𝜑 → ∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2))↑2)))
142	92, 141	jca 521	. . 3 ⊢ (𝜑 → (((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) < 𝐶 ∧ ∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2))↑2))))
143	6, 44, 142	rspcedvdw 3580	. 2 ⊢ (𝜑 → ∃𝑙 ∈ ℕ (𝑙 < 𝐶 ∧ ∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))))
144		breq2 5107	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑚 → (2 ∥ 𝑔 ↔ 2 ∥ 𝑚))
145	144	notbid 321	. . . . . . . . . 10 ⊢ (𝑔 = 𝑚 → (¬ 2 ∥ 𝑔 ↔ ¬ 2 ∥ 𝑚))
146		oveq1 7419	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑚 → (𝑔 gcd ℎ) = (𝑚 gcd ℎ))
147	146	eqeq1d 2763	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑚 → ((𝑔 gcd ℎ) = 1 ↔ (𝑚 gcd ℎ) = 1))
148		oveq1 7419	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑚 → (𝑔↑4) = (𝑚↑4))
149	148	oveq1d 7427	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑚 → ((𝑔↑4) + (ℎ↑4)) = ((𝑚↑4) + (ℎ↑4)))
150	149	eqeq1d 2763	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑚 → (((𝑔↑4) + (ℎ↑4)) = (𝑙↑2) ↔ ((𝑚↑4) + (ℎ↑4)) = (𝑙↑2)))
151	147, 150	anbi12d 644	. . . . . . . . . 10 ⊢ (𝑔 = 𝑚 → (((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2)) ↔ ((𝑚 gcd ℎ) = 1 ∧ ((𝑚↑4) + (ℎ↑4)) = (𝑙↑2))))
152	145, 151	anbi12d 644	. . . . . . . . 9 ⊢ (𝑔 = 𝑚 → ((¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ↔ (¬ 2 ∥ 𝑚 ∧ ((𝑚 gcd ℎ) = 1 ∧ ((𝑚↑4) + (ℎ↑4)) = (𝑙↑2)))))
153		oveq2 7420	. . . . . . . . . . . 12 ⊢ (ℎ = 𝑛 → (𝑚 gcd ℎ) = (𝑚 gcd 𝑛))
154	153	eqeq1d 2763	. . . . . . . . . . 11 ⊢ (ℎ = 𝑛 → ((𝑚 gcd ℎ) = 1 ↔ (𝑚 gcd 𝑛) = 1))
155		oveq1 7419	. . . . . . . . . . . . 13 ⊢ (ℎ = 𝑛 → (ℎ↑4) = (𝑛↑4))
156	155	oveq2d 7428	. . . . . . . . . . . 12 ⊢ (ℎ = 𝑛 → ((𝑚↑4) + (ℎ↑4)) = ((𝑚↑4) + (𝑛↑4)))
157	156	eqeq1d 2763	. . . . . . . . . . 11 ⊢ (ℎ = 𝑛 → (((𝑚↑4) + (ℎ↑4)) = (𝑙↑2) ↔ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2)))
158	154, 157	anbi12d 644	. . . . . . . . . 10 ⊢ (ℎ = 𝑛 → (((𝑚 gcd ℎ) = 1 ∧ ((𝑚↑4) + (ℎ↑4)) = (𝑙↑2)) ↔ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))))
159	158	anbi2d 642	. . . . . . . . 9 ⊢ (ℎ = 𝑛 → ((¬ 2 ∥ 𝑚 ∧ ((𝑚 gcd ℎ) = 1 ∧ ((𝑚↑4) + (ℎ↑4)) = (𝑙↑2))) ↔ (¬ 2 ∥ 𝑚 ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2)))))
160		simplrl 789	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → 𝑚 ∈ ℕ)
161	160	adantr 486	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑚) → 𝑚 ∈ ℕ)
162		simprr 785	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → 𝑛 ∈ ℕ)
163	162	ad2antrr 739	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑚) → 𝑛 ∈ ℕ)
164		simpr 490	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑚) → ¬ 2 ∥ 𝑚)
165		simplr 781	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑚) → ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2)))
166	164, 165	jca 521	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑚) → (¬ 2 ∥ 𝑚 ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))))
167	152, 159, 161, 163, 166	2rspcedvdw 3590	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑚) → ∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))))
168		simp-4r 796	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑚) → 𝑙 < 𝐶)
169	167, 168	jca 521	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑚) → (∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶))
170		breq2 5107	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑛 → (2 ∥ 𝑔 ↔ 2 ∥ 𝑛))
171	170	notbid 321	. . . . . . . . . 10 ⊢ (𝑔 = 𝑛 → (¬ 2 ∥ 𝑔 ↔ ¬ 2 ∥ 𝑛))
172		oveq1 7419	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑛 → (𝑔 gcd ℎ) = (𝑛 gcd ℎ))
173	172	eqeq1d 2763	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑛 → ((𝑔 gcd ℎ) = 1 ↔ (𝑛 gcd ℎ) = 1))
174		oveq1 7419	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑛 → (𝑔↑4) = (𝑛↑4))
175	174	oveq1d 7427	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑛 → ((𝑔↑4) + (ℎ↑4)) = ((𝑛↑4) + (ℎ↑4)))
176	175	eqeq1d 2763	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑛 → (((𝑔↑4) + (ℎ↑4)) = (𝑙↑2) ↔ ((𝑛↑4) + (ℎ↑4)) = (𝑙↑2)))
177	173, 176	anbi12d 644	. . . . . . . . . 10 ⊢ (𝑔 = 𝑛 → (((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2)) ↔ ((𝑛 gcd ℎ) = 1 ∧ ((𝑛↑4) + (ℎ↑4)) = (𝑙↑2))))
178	171, 177	anbi12d 644	. . . . . . . . 9 ⊢ (𝑔 = 𝑛 → ((¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ↔ (¬ 2 ∥ 𝑛 ∧ ((𝑛 gcd ℎ) = 1 ∧ ((𝑛↑4) + (ℎ↑4)) = (𝑙↑2)))))
179		oveq2 7420	. . . . . . . . . . . 12 ⊢ (ℎ = 𝑚 → (𝑛 gcd ℎ) = (𝑛 gcd 𝑚))
180	179	eqeq1d 2763	. . . . . . . . . . 11 ⊢ (ℎ = 𝑚 → ((𝑛 gcd ℎ) = 1 ↔ (𝑛 gcd 𝑚) = 1))
181		oveq1 7419	. . . . . . . . . . . . 13 ⊢ (ℎ = 𝑚 → (ℎ↑4) = (𝑚↑4))
182	181	oveq2d 7428	. . . . . . . . . . . 12 ⊢ (ℎ = 𝑚 → ((𝑛↑4) + (ℎ↑4)) = ((𝑛↑4) + (𝑚↑4)))
183	182	eqeq1d 2763	. . . . . . . . . . 11 ⊢ (ℎ = 𝑚 → (((𝑛↑4) + (ℎ↑4)) = (𝑙↑2) ↔ ((𝑛↑4) + (𝑚↑4)) = (𝑙↑2)))
184	180, 183	anbi12d 644	. . . . . . . . . 10 ⊢ (ℎ = 𝑚 → (((𝑛 gcd ℎ) = 1 ∧ ((𝑛↑4) + (ℎ↑4)) = (𝑙↑2)) ↔ ((𝑛 gcd 𝑚) = 1 ∧ ((𝑛↑4) + (𝑚↑4)) = (𝑙↑2))))
185	184	anbi2d 642	. . . . . . . . 9 ⊢ (ℎ = 𝑚 → ((¬ 2 ∥ 𝑛 ∧ ((𝑛 gcd ℎ) = 1 ∧ ((𝑛↑4) + (ℎ↑4)) = (𝑙↑2))) ↔ (¬ 2 ∥ 𝑛 ∧ ((𝑛 gcd 𝑚) = 1 ∧ ((𝑛↑4) + (𝑚↑4)) = (𝑙↑2)))))
186	162	ad2antrr 739	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → 𝑛 ∈ ℕ)
187	160	adantr 486	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → 𝑚 ∈ ℕ)
188		simpr 490	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → ¬ 2 ∥ 𝑛)
189	186	nnzd 12700	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → 𝑛 ∈ ℤ)
190	187	nnzd 12700	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → 𝑚 ∈ ℤ)
191	189, 190	gcdcomd 16666	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (𝑛 gcd 𝑚) = (𝑚 gcd 𝑛))
192		simplrl 789	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (𝑚 gcd 𝑛) = 1)
193	191, 192	eqtrd 2796	. . . . . . . . . 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 14369	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (𝑛↑4) ∈ ℕ)
196	195	nncnd 12332	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (𝑛↑4) ∈ ℂ)
197	187, 194	nnexpcld 14369	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (𝑚↑4) ∈ ℕ)
198	197	nncnd 12332	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (𝑚↑4) ∈ ℂ)
199	196, 198	addcomd 11493	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → ((𝑛↑4) + (𝑚↑4)) = ((𝑚↑4) + (𝑛↑4)))
200		simplrr 790	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))
201	199, 200	eqtrd 2796	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → ((𝑛↑4) + (𝑚↑4)) = (𝑙↑2))
202	188, 193, 201	jca32 525	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (¬ 2 ∥ 𝑛 ∧ ((𝑛 gcd 𝑚) = 1 ∧ ((𝑛↑4) + (𝑚↑4)) = (𝑙↑2))))
203	178, 185, 186, 187, 202	2rspcedvdw 3590	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → ∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))))
204		simp-4r 796	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → 𝑙 < 𝐶)
205	203, 204	jca 521	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶))
206		simprl 783	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → 𝑚 ∈ ℕ)
207	206	ad2antrr 739	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → 𝑚 ∈ ℕ)
208	207	nnsqcld 14368	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → (𝑚↑2) ∈ ℕ)
209	162	ad2antrr 739	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → 𝑛 ∈ ℕ)
210	209	nnsqcld 14368	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → (𝑛↑2) ∈ ℕ)
211		simp-5r 798	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → 𝑙 ∈ ℕ)
212	160	nnzd 12700	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → 𝑚 ∈ ℤ)
213	27	a1i 11	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → 2 ∈ ℕ)
214		dvdsexp2im 16477	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 2 ∈ ℕ) → (2 ∥ 𝑚 → 2 ∥ (𝑚↑2)))
215	62, 212, 213, 214	mp3an2i 1495	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → (2 ∥ 𝑚 → 2 ∥ (𝑚↑2)))
216	215	imp 412	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → 2 ∥ (𝑚↑2))
217	17	a1i 11	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → 2 ∈ ℕ₀)
218	207	nncnd 12332	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → 𝑚 ∈ ℂ)
219	218	exp4sqsq 14324	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → (𝑚↑4) = ((𝑚↑2)↑2))
220	209	nncnd 12332	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → 𝑛 ∈ ℂ)
221	220	exp4sqsq 14324	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → (𝑛↑4) = ((𝑛↑2)↑2))
222	219, 221	oveq12d 7430	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → ((𝑚↑4) + (𝑛↑4)) = (((𝑚↑2)↑2) + ((𝑛↑2)↑2)))
223		simplrr 790	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))
224	222, 223	eqtr3d 2798	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → (((𝑚↑2)↑2) + ((𝑛↑2)↑2)) = (𝑙↑2))
225		simplrl 789	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → (𝑚 gcd 𝑛) = 1)
226	27	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → 2 ∈ ℕ)
227		rppwr 16714	. . . . . . . . . . . . . 14 ⊢ ((𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ∧ 2 ∈ ℕ) → ((𝑚 gcd 𝑛) = 1 → ((𝑚↑2) gcd (𝑛↑2)) = 1))
228	207, 209, 226, 227	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → ((𝑚 gcd 𝑛) = 1 → ((𝑚↑2) gcd (𝑛↑2)) = 1))
229	225, 228	mpd 16	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → ((𝑚↑2) gcd (𝑛↑2)) = 1)
230	208, 210, 211, 217, 224, 229	fltaccoprm 27954	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → ((𝑚↑2) gcd 𝑙) = 1)
231	208, 210, 211, 216, 230, 224	flt4lem2 27959	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → ¬ 2 ∥ (𝑛↑2))
232	209	nnzd 12700	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → 𝑛 ∈ ℤ)
233		dvdsexp2im 16477	. . . . . . . . . . 11 ⊢ ((2 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 2 ∈ ℕ) → (2 ∥ 𝑛 → 2 ∥ (𝑛↑2)))
234	62, 232, 226, 233	mp3an2i 1495	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → (2 ∥ 𝑛 → 2 ∥ (𝑛↑2)))
235	231, 234	mtod 201	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → ¬ 2 ∥ 𝑛)
236	235	ex 418	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → (2 ∥ 𝑚 → ¬ 2 ∥ 𝑛))
237		imor 867	. . . . . . . 8 ⊢ ((2 ∥ 𝑚 → ¬ 2 ∥ 𝑛) ↔ (¬ 2 ∥ 𝑚 ∨ ¬ 2 ∥ 𝑛))
238	236, 237	sylib 221	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → (¬ 2 ∥ 𝑚 ∨ ¬ 2 ∥ 𝑛))
239	169, 205, 238	mpjaodan 973	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → (∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶))
240	239	ex 418	. . . . 5 ⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → (((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2)) → (∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶)))
241	240	rexlimdvva 3220	. . . 4 ⊢ (((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) → (∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2)) → (∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶)))
242	241	expimpd 459	. . 3 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → ((𝑙 < 𝐶 ∧ ∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → (∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶)))
243	242	reximdva 3176	. 2 ⊢ (𝜑 → (∃𝑙 ∈ ℕ (𝑙 < 𝐶 ∧ ∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → ∃𝑙 ∈ ℕ (∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶)))
244	143, 243	mpd 16	1 ⊢ (𝜑 → ∃𝑙 ∈ ℕ (∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ∃wrex 3087 class class class wbr 5103 ‘cfv 6531 (class class class)co 7412 ℝcr 11180 0cc0 11181 1c1 11182 + caddc 11184 · cmul 11186 < clt 11324 ≤ cle 11325 − cmin 11522 / cdiv 11954 ℕcn 12316 2c2 12378 4c4 12380 ℕ₀cn0 12587 ℤcz 12674 ℝ⁺crp 13101 ↑cexp 14184 √csqrt 15380 ∥ cdvds 16402 gcd cgcd 16644

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7740 ax-cnex 11237 ax-resscn 11238 ax-1cn 11239 ax-icn 11240 ax-addcl 11241 ax-addrcl 11242 ax-mulcl 11243 ax-mulrcl 11244 ax-mulcom 11245 ax-addass 11246 ax-mulass 11247 ax-distr 11248 ax-i2m1 11249 ax-1ne0 11250 ax-1rid 11251 ax-rnegex 11252 ax-rrecex 11253 ax-cnre 11254 ax-pre-lttri 11255 ax-pre-lttrn 11256 ax-pre-ltadd 11257 ax-pre-mulgt0 11258 ax-pre-sup 11259

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6297 df-ord 6358 df-on 6359 df-lim 6360 df-suc 6361 df-iota 6487 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7867 df-1st 7990 df-2nd 7991 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-1o 8460 df-2o 8461 df-er 8701 df-en 8958 df-dom 8959 df-sdom 8960 df-fin 8961 df-sup 9418 df-inf 9419 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11524 df-neg 11525 df-div 11955 df-nn 12317 df-2 12386 df-3 12387 df-4 12388 df-n0 12588 df-z 12675 df-uz 12947 df-q 13057 df-rp 13102 df-fz 13621 df-fl 13912 df-mod 13990 df-seq 14125 df-exp 14185 df-cj 15246 df-re 15247 df-im 15248 df-sqrt 15382 df-abs 15383 df-dvds 16403 df-gcd 16645 df-prm 16827 df-numer 16891 df-denom 16892

This theorem is used by: nna4b4nsq 27972

W3C validator