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 27995

Description: Convert flt4lem5f 27993 into a convenient form for nna4b4nsq 27996. (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 5105	. . . 4 ⊢ (𝑙 = ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) → (𝑙 < 𝐶 ↔ ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) < 𝐶))
2		oveq1 7428	. . . . . . 7 ⊢ (𝑙 = ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) → (𝑙↑2) = (((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2))↑2))
3	2	eqeq2d 2771	. . . . . 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 3227	. . . 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 2760	. . . . . . 7 ⊢ (((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) = (((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2)
8		eqid 2760	. . . . . . 7 ⊢ (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2) = (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)
9		eqid 2760	. . . . . . 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 2760	. . . . . . 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		flt4lem7.2	. . . . . . 7 ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)
16		flt4lem7.3	. . . . . . 7 ⊢ (𝜑 → ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2))
17	7, 8, 9, 10, 11, 12, 13, 14, 15, 16	flt4lem5e 27992	. . . . . 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) ∈ ℕ)))
18	17	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) ∈ ℕ))
19	18	simp3d 1162	. . . 4 ⊢ (𝜑 → (((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) ∈ ℕ)
20	17	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) ∈ ℕ))
21	20	simprd 501	. . . 4 ⊢ (𝜑 → (𝐵 / 2) ∈ ℕ)
22		gcdnncl 16683	. . . 4 ⊢ (((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) ∈ ℕ ∧ (𝐵 / 2) ∈ ℕ) → ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) ∈ ℕ)
23	19, 21, 22	syl2anc 596	. . 3 ⊢ (𝜑 → ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) ∈ ℕ)
24	23	nnred 12354	. . . . 5 ⊢ (𝜑 → ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) ∈ ℝ)
25	21	nnred 12354	. . . . 5 ⊢ (𝜑 → (𝐵 / 2) ∈ ℝ)
26	13	nnred 12354	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ ℝ)
27	19	nnzd 12723	. . . . . 6 ⊢ (𝜑 → (((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) ∈ ℤ)
28	27, 21	gcdle2d 16687	. . . . 5 ⊢ (𝜑 → ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) ≤ (𝐵 / 2))
29	12	nnred 12354	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ ℝ)
30	12	nnrpd 13166	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℝ⁺)
31		rphalflt 13155	. . . . . . 7 ⊢ (𝐵 ∈ ℝ⁺ → (𝐵 / 2) < 𝐵)
32	30, 31	syl 18	. . . . . 6 ⊢ (𝜑 → (𝐵 / 2) < 𝐵)
33	12	nnsqcld 14392	. . . . . . . . 9 ⊢ (𝜑 → (𝐵↑2) ∈ ℕ)
34	33	nnred 12354	. . . . . . . 8 ⊢ (𝜑 → (𝐵↑2) ∈ ℝ)
35		4nn0 12629	. . . . . . . . . . 11 ⊢ 4 ∈ ℕ₀
36	35	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 4 ∈ ℕ₀)
37	12, 36	nnexpcld 14393	. . . . . . . . 9 ⊢ (𝜑 → (𝐵↑4) ∈ ℕ)
38	37	nnred 12354	. . . . . . . 8 ⊢ (𝜑 → (𝐵↑4) ∈ ℝ)
39	13	nnsqcld 14392	. . . . . . . . 9 ⊢ (𝜑 → (𝐶↑2) ∈ ℕ)
40	39	nnred 12354	. . . . . . . 8 ⊢ (𝜑 → (𝐶↑2) ∈ ℝ)
41		2lt4 12524	. . . . . . . . 9 ⊢ 2 < 4
42		2z 12732	. . . . . . . . . . 11 ⊢ 2 ∈ ℤ
43	42	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 2 ∈ ℤ)
44		4z 12734	. . . . . . . . . . 11 ⊢ 4 ∈ ℤ
45	44	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 4 ∈ ℤ)
46		1red 11313	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℝ)
47	21	nnge1d 12390	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ≤ (𝐵 / 2))
48	46, 25, 29, 47, 32	lelttrd 11472	. . . . . . . . . 10 ⊢ (𝜑 → 1 < 𝐵)
49	29, 43, 45, 48	ltexp2d 14399	. . . . . . . . 9 ⊢ (𝜑 → (2 < 4 ↔ (𝐵↑2) < (𝐵↑4)))
50	41, 49	mpbii 236	. . . . . . . 8 ⊢ (𝜑 → (𝐵↑2) < (𝐵↑4))
51	11, 36	nnexpcld 14393	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴↑4) ∈ ℕ)
52	51	nngt0d 12391	. . . . . . . . . 10 ⊢ (𝜑 → 0 < (𝐴↑4))
53	51	nnred 12354	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴↑4) ∈ ℝ)
54	53, 38	ltaddpos2d 11905	. . . . . . . . . 10 ⊢ (𝜑 → (0 < (𝐴↑4) ↔ (𝐵↑4) < ((𝐴↑4) + (𝐵↑4))))
55	52, 54	mpbid 235	. . . . . . . . 9 ⊢ (𝜑 → (𝐵↑4) < ((𝐴↑4) + (𝐵↑4)))
56	55, 16	breqtrd 5130	. . . . . . . 8 ⊢ (𝜑 → (𝐵↑4) < (𝐶↑2))
57	34, 38, 40, 50, 56	lttrd 11475	. . . . . . 7 ⊢ (𝜑 → (𝐵↑2) < (𝐶↑2))
58	13	nnrpd 13166	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ ℝ⁺)
59		2nn 12420	. . . . . . . . 9 ⊢ 2 ∈ ℕ
60	59	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 2 ∈ ℕ)
61	30, 58, 60	ltexp1d 14407	. . . . . . 7 ⊢ (𝜑 → (𝐵 < 𝐶 ↔ (𝐵↑2) < (𝐶↑2)))
62	57, 61	mpbird 260	. . . . . 6 ⊢ (𝜑 → 𝐵 < 𝐶)
63	25, 29, 26, 32, 62	lttrd 11475	. . . . 5 ⊢ (𝜑 → (𝐵 / 2) < 𝐶)
64	24, 25, 26, 28, 63	lelttrd 11472	. . . 4 ⊢ (𝜑 → ((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) < 𝐶)
65		oveq1 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)) gcd 𝑛))
66	65	eqeq1d 2762	. . . . . 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))
67		oveq1 7428	. . . . . . . 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))
68	67	oveq1d 7436	. . . . . . 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)))
69	68	eqeq1d 2762	. . . . . 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)))
70	66, 69	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))))
71		oveq2 7429	. . . . . . 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))))
72	71	eqeq1d 2762	. . . . . 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))
73		oveq1 7428	. . . . . . . 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))
74	73	oveq2d 7437	. . . . . . 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)))
75	74	eqeq1d 2762	. . . . . 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)))
76	72, 75	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))))
77	18	simp1d 1160	. . . . . 6 ⊢ (𝜑 → (((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) + (√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) − (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)))) / 2) ∈ ℕ)
78		gcdnncl 16683	. . . . . 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)) ∈ ℕ)
79	77, 21, 78	syl2anc 596	. . . . 5 ⊢ (𝜑 → ((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) + (√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) − (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)))) / 2) gcd (𝐵 / 2)) ∈ ℕ)
80	18	simp2d 1161	. . . . . 6 ⊢ (𝜑 → (((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) − (√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) − (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)))) / 2) ∈ ℕ)
81		gcdnncl 16683	. . . . . 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)) ∈ ℕ)
82	80, 21, 81	syl2anc 596	. . . . 5 ⊢ (𝜑 → ((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) − (√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) − (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)))) / 2) gcd (𝐵 / 2)) ∈ ℕ)
83	77	nnzd 12723	. . . . . . . 8 ⊢ (𝜑 → (((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) + (√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) − (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)))) / 2) ∈ ℤ)
84	21	nnzd 12723	. . . . . . . 8 ⊢ (𝜑 → (𝐵 / 2) ∈ ℤ)
85	82	nnzd 12723	. . . . . . . 8 ⊢ (𝜑 → ((((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) − (√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) − (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)))) / 2) gcd (𝐵 / 2)) ∈ ℤ)
86		gcdass 16726	. . . . . . . 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)))))
87	83, 84, 85, 86	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)))))
88	80	nnzd 12723	. . . . . . . . . 10 ⊢ (𝜑 → (((√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) + (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2))) − (√‘((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) − (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)))) / 2) ∈ ℤ)
89		gcdass 16726	. . . . . . . . . 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))))
90	84, 84, 88, 89	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))))
91	21	nnnn0d 12671	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵 / 2) ∈ ℕ₀)
92		gcdnn0id 16706	. . . . . . . . . . . 12 ⊢ ((𝐵 / 2) ∈ ℕ₀ → ((𝐵 / 2) gcd (𝐵 / 2)) = (𝐵 / 2))
93	91, 92	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 / 2) gcd (𝐵 / 2)) = (𝐵 / 2))
94	93	oveq1d 7436	. . . . . . . . . 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)))
95	84, 88	gcdcomd 16692	. . . . . . . . . 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)))
96	94, 95	eqtr2d 2796	. . . . . . . . 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)))
97	88, 84	gcdcomd 16692	. . . . . . . . . 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)))
98	97	oveq2d 7437	. . . . . . . . 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))))
99	90, 96, 98	3eqtr4rd 2806	. . . . . . . 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)))
100	99	oveq2d 7437	. . . . . . 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))))
101	17	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))
102	101	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)
103	102	oveq1d 7436	. . . . . . . 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)))
104		gcdass 16726	. . . . . . . . 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))))
105	83, 88, 84, 104	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))))
106		1gcd 16712	. . . . . . . . 9 ⊢ ((𝐵 / 2) ∈ ℤ → (1 gcd (𝐵 / 2)) = 1)
107	84, 106	syl 18	. . . . . . . 8 ⊢ (𝜑 → (1 gcd (𝐵 / 2)) = 1)
108	103, 105, 107	3eqtr3d 2803	. . . . . . 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)
109	87, 100, 108	3eqtrd 2799	. . . . . 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)
110	7, 8, 9, 10, 11, 12, 13, 14, 15, 16	flt4lem5f 27993	. . . . . . 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)))
111	110	eqcomd 2766	. . . . . 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))
112	109, 111	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)))
113	70, 76, 79, 82, 112	2rspcedvdw 3589	. . . 4 ⊢ (𝜑 → ∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2))↑2)))
114	64, 113	jca 521	. . 3 ⊢ (𝜑 → (((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2)) < 𝐶 ∧ ∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (((((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) gcd (𝐵 / 2))↑2))))
115	6, 23, 114	rspcedvdw 3579	. 2 ⊢ (𝜑 → ∃𝑙 ∈ ℕ (𝑙 < 𝐶 ∧ ∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))))
116		breq2 5106	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑚 → (2 ∥ 𝑔 ↔ 2 ∥ 𝑚))
117	116	notbid 321	. . . . . . . . . 10 ⊢ (𝑔 = 𝑚 → (¬ 2 ∥ 𝑔 ↔ ¬ 2 ∥ 𝑚))
118		oveq1 7428	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑚 → (𝑔 gcd ℎ) = (𝑚 gcd ℎ))
119	118	eqeq1d 2762	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑚 → ((𝑔 gcd ℎ) = 1 ↔ (𝑚 gcd ℎ) = 1))
120		oveq1 7428	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑚 → (𝑔↑4) = (𝑚↑4))
121	120	oveq1d 7436	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑚 → ((𝑔↑4) + (ℎ↑4)) = ((𝑚↑4) + (ℎ↑4)))
122	121	eqeq1d 2762	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑚 → (((𝑔↑4) + (ℎ↑4)) = (𝑙↑2) ↔ ((𝑚↑4) + (ℎ↑4)) = (𝑙↑2)))
123	119, 122	anbi12d 644	. . . . . . . . . 10 ⊢ (𝑔 = 𝑚 → (((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2)) ↔ ((𝑚 gcd ℎ) = 1 ∧ ((𝑚↑4) + (ℎ↑4)) = (𝑙↑2))))
124	117, 123	anbi12d 644	. . . . . . . . 9 ⊢ (𝑔 = 𝑚 → ((¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ↔ (¬ 2 ∥ 𝑚 ∧ ((𝑚 gcd ℎ) = 1 ∧ ((𝑚↑4) + (ℎ↑4)) = (𝑙↑2)))))
125		oveq2 7429	. . . . . . . . . . . 12 ⊢ (ℎ = 𝑛 → (𝑚 gcd ℎ) = (𝑚 gcd 𝑛))
126	125	eqeq1d 2762	. . . . . . . . . . 11 ⊢ (ℎ = 𝑛 → ((𝑚 gcd ℎ) = 1 ↔ (𝑚 gcd 𝑛) = 1))
127		oveq1 7428	. . . . . . . . . . . . 13 ⊢ (ℎ = 𝑛 → (ℎ↑4) = (𝑛↑4))
128	127	oveq2d 7437	. . . . . . . . . . . 12 ⊢ (ℎ = 𝑛 → ((𝑚↑4) + (ℎ↑4)) = ((𝑚↑4) + (𝑛↑4)))
129	128	eqeq1d 2762	. . . . . . . . . . 11 ⊢ (ℎ = 𝑛 → (((𝑚↑4) + (ℎ↑4)) = (𝑙↑2) ↔ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2)))
130	126, 129	anbi12d 644	. . . . . . . . . 10 ⊢ (ℎ = 𝑛 → (((𝑚 gcd ℎ) = 1 ∧ ((𝑚↑4) + (ℎ↑4)) = (𝑙↑2)) ↔ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))))
131	130	anbi2d 642	. . . . . . . . 9 ⊢ (ℎ = 𝑛 → ((¬ 2 ∥ 𝑚 ∧ ((𝑚 gcd ℎ) = 1 ∧ ((𝑚↑4) + (ℎ↑4)) = (𝑙↑2))) ↔ (¬ 2 ∥ 𝑚 ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2)))))
132		simprl 783	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → 𝑚 ∈ ℕ)
133	132	ad2antrr 739	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑚) → 𝑚 ∈ ℕ)
134		simprr 785	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → 𝑛 ∈ ℕ)
135	134	ad2antrr 739	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑚) → 𝑛 ∈ ℕ)
136		simpr 490	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑚) → ¬ 2 ∥ 𝑚)
137		simplr 781	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑚) → ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2)))
138	136, 137	jca 521	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑚) → (¬ 2 ∥ 𝑚 ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))))
139	124, 131, 133, 135, 138	2rspcedvdw 3589	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑚) → ∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))))
140		simp-4r 796	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑚) → 𝑙 < 𝐶)
141	139, 140	jca 521	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑚) → (∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶))
142		breq2 5106	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑛 → (2 ∥ 𝑔 ↔ 2 ∥ 𝑛))
143	142	notbid 321	. . . . . . . . . 10 ⊢ (𝑔 = 𝑛 → (¬ 2 ∥ 𝑔 ↔ ¬ 2 ∥ 𝑛))
144		oveq1 7428	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑛 → (𝑔 gcd ℎ) = (𝑛 gcd ℎ))
145	144	eqeq1d 2762	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑛 → ((𝑔 gcd ℎ) = 1 ↔ (𝑛 gcd ℎ) = 1))
146		oveq1 7428	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑛 → (𝑔↑4) = (𝑛↑4))
147	146	oveq1d 7436	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑛 → ((𝑔↑4) + (ℎ↑4)) = ((𝑛↑4) + (ℎ↑4)))
148	147	eqeq1d 2762	. . . . . . . . . . 11 ⊢ (𝑔 = 𝑛 → (((𝑔↑4) + (ℎ↑4)) = (𝑙↑2) ↔ ((𝑛↑4) + (ℎ↑4)) = (𝑙↑2)))
149	145, 148	anbi12d 644	. . . . . . . . . 10 ⊢ (𝑔 = 𝑛 → (((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2)) ↔ ((𝑛 gcd ℎ) = 1 ∧ ((𝑛↑4) + (ℎ↑4)) = (𝑙↑2))))
150	143, 149	anbi12d 644	. . . . . . . . 9 ⊢ (𝑔 = 𝑛 → ((¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ↔ (¬ 2 ∥ 𝑛 ∧ ((𝑛 gcd ℎ) = 1 ∧ ((𝑛↑4) + (ℎ↑4)) = (𝑙↑2)))))
151		oveq2 7429	. . . . . . . . . . . 12 ⊢ (ℎ = 𝑚 → (𝑛 gcd ℎ) = (𝑛 gcd 𝑚))
152	151	eqeq1d 2762	. . . . . . . . . . 11 ⊢ (ℎ = 𝑚 → ((𝑛 gcd ℎ) = 1 ↔ (𝑛 gcd 𝑚) = 1))
153		oveq1 7428	. . . . . . . . . . . . 13 ⊢ (ℎ = 𝑚 → (ℎ↑4) = (𝑚↑4))
154	153	oveq2d 7437	. . . . . . . . . . . 12 ⊢ (ℎ = 𝑚 → ((𝑛↑4) + (ℎ↑4)) = ((𝑛↑4) + (𝑚↑4)))
155	154	eqeq1d 2762	. . . . . . . . . . 11 ⊢ (ℎ = 𝑚 → (((𝑛↑4) + (ℎ↑4)) = (𝑙↑2) ↔ ((𝑛↑4) + (𝑚↑4)) = (𝑙↑2)))
156	152, 155	anbi12d 644	. . . . . . . . . 10 ⊢ (ℎ = 𝑚 → (((𝑛 gcd ℎ) = 1 ∧ ((𝑛↑4) + (ℎ↑4)) = (𝑙↑2)) ↔ ((𝑛 gcd 𝑚) = 1 ∧ ((𝑛↑4) + (𝑚↑4)) = (𝑙↑2))))
157	156	anbi2d 642	. . . . . . . . 9 ⊢ (ℎ = 𝑚 → ((¬ 2 ∥ 𝑛 ∧ ((𝑛 gcd ℎ) = 1 ∧ ((𝑛↑4) + (ℎ↑4)) = (𝑙↑2))) ↔ (¬ 2 ∥ 𝑛 ∧ ((𝑛 gcd 𝑚) = 1 ∧ ((𝑛↑4) + (𝑚↑4)) = (𝑙↑2)))))
158	134	ad2antrr 739	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → 𝑛 ∈ ℕ)
159	132	ad2antrr 739	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → 𝑚 ∈ ℕ)
160		simpr 490	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → ¬ 2 ∥ 𝑛)
161	158	nnzd 12723	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → 𝑛 ∈ ℤ)
162	159	nnzd 12723	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → 𝑚 ∈ ℤ)
163	161, 162	gcdcomd 16692	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (𝑛 gcd 𝑚) = (𝑚 gcd 𝑛))
164		simplrl 789	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (𝑚 gcd 𝑛) = 1)
165	163, 164	eqtrd 2795	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (𝑛 gcd 𝑚) = 1)
166	35	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → 4 ∈ ℕ₀)
167	158, 166	nnexpcld 14393	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (𝑛↑4) ∈ ℕ)
168	167	nncnd 12355	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (𝑛↑4) ∈ ℂ)
169	159, 166	nnexpcld 14393	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (𝑚↑4) ∈ ℕ)
170	169	nncnd 12355	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (𝑚↑4) ∈ ℂ)
171	168, 170	addcomd 11516	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → ((𝑛↑4) + (𝑚↑4)) = ((𝑚↑4) + (𝑛↑4)))
172		simplrr 790	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))
173	171, 172	eqtrd 2795	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → ((𝑛↑4) + (𝑚↑4)) = (𝑙↑2))
174	160, 165, 173	jca32 525	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (¬ 2 ∥ 𝑛 ∧ ((𝑛 gcd 𝑚) = 1 ∧ ((𝑛↑4) + (𝑚↑4)) = (𝑙↑2))))
175	150, 157, 158, 159, 174	2rspcedvdw 3589	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → ∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))))
176		simp-4r 796	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → 𝑙 < 𝐶)
177	175, 176	jca 521	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ ¬ 2 ∥ 𝑛) → (∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶))
178	132	ad2antrr 739	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → 𝑚 ∈ ℕ)
179	178	nnsqcld 14392	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → (𝑚↑2) ∈ ℕ)
180	134	ad2antrr 739	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → 𝑛 ∈ ℕ)
181	180	nnsqcld 14392	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → (𝑛↑2) ∈ ℕ)
182		simplrl 789	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → 𝑚 ∈ ℕ)
183	182	nnzd 12723	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → 𝑚 ∈ ℤ)
184	59	a1i 11	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → 2 ∈ ℕ)
185		dvdsexp2im 16503	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 2 ∈ ℕ) → (2 ∥ 𝑚 → 2 ∥ (𝑚↑2)))
186	42, 183, 184, 185	mp3an2i 1495	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → (2 ∥ 𝑚 → 2 ∥ (𝑚↑2)))
187	186	imp 412	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → 2 ∥ (𝑚↑2))
188		simplrl 789	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → (𝑚 gcd 𝑛) = 1)
189	59	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → 2 ∈ ℕ)
190		rppwr 16740	. . . . . . . . . . . . 13 ⊢ ((𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ∧ 2 ∈ ℕ) → ((𝑚 gcd 𝑛) = 1 → ((𝑚↑2) gcd (𝑛↑2)) = 1))
191	178, 180, 189, 190	syl3anc 1398	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → ((𝑚 gcd 𝑛) = 1 → ((𝑚↑2) gcd (𝑛↑2)) = 1))
192	188, 191	mpd 16	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → ((𝑚↑2) gcd (𝑛↑2)) = 1)
193	179, 181, 187, 192	flt4lem2 27983	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → ¬ 2 ∥ (𝑛↑2))
194	180	nnzd 12723	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → 𝑛 ∈ ℤ)
195		dvdsexp2im 16503	. . . . . . . . . . 11 ⊢ ((2 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 2 ∈ ℕ) → (2 ∥ 𝑛 → 2 ∥ (𝑛↑2)))
196	42, 194, 189, 195	mp3an2i 1495	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → (2 ∥ 𝑛 → 2 ∥ (𝑛↑2)))
197	193, 196	mtod 201	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) ∧ 2 ∥ 𝑚) → ¬ 2 ∥ 𝑛)
198	197	ex 418	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → (2 ∥ 𝑚 → ¬ 2 ∥ 𝑛))
199		imor 867	. . . . . . . 8 ⊢ ((2 ∥ 𝑚 → ¬ 2 ∥ 𝑛) ↔ (¬ 2 ∥ 𝑚 ∨ ¬ 2 ∥ 𝑛))
200	198, 199	sylib 221	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → (¬ 2 ∥ 𝑚 ∨ ¬ 2 ∥ 𝑛))
201	141, 177, 200	mpjaodan 973	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → (∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶))
202	201	ex 418	. . . . 5 ⊢ ((((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → (((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2)) → (∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶)))
203	202	rexlimdvva 3219	. . . 4 ⊢ (((𝜑 ∧ 𝑙 ∈ ℕ) ∧ 𝑙 < 𝐶) → (∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2)) → (∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶)))
204	203	expimpd 459	. . 3 ⊢ ((𝜑 ∧ 𝑙 ∈ ℕ) → ((𝑙 < 𝐶 ∧ ∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → (∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶)))
205	204	reximdva 3175	. 2 ⊢ (𝜑 → (∃𝑙 ∈ ℕ (𝑙 < 𝐶 ∧ ∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ ((𝑚 gcd 𝑛) = 1 ∧ ((𝑚↑4) + (𝑛↑4)) = (𝑙↑2))) → ∃𝑙 ∈ ℕ (∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶)))
206	115, 205	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 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ∃wrex 3086 class class class wbr 5102 ‘cfv 6539 (class class class)co 7421 0cc0 11204 1c1 11205 + caddc 11207 · cmul 11209 < clt 11347 − cmin 11545 / cdiv 11977 ℕcn 12339 2c2 12401 4c4 12403 ℕ₀cn0 12610 ℤcz 12697 ℝ⁺crp 13124 ↑cexp 14208 √csqrt 15406 ∥ cdvds 16428 gcd cgcd 16670

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7752 ax-cnex 11260 ax-resscn 11261 ax-1cn 11262 ax-icn 11263 ax-addcl 11264 ax-addrcl 11265 ax-mulcl 11266 ax-mulrcl 11267 ax-mulcom 11268 ax-addass 11269 ax-mulass 11270 ax-distr 11271 ax-i2m1 11272 ax-1ne0 11273 ax-1rid 11274 ax-rnegex 11275 ax-rrecex 11276 ax-cnre 11277 ax-pre-lttri 11278 ax-pre-lttrn 11279 ax-pre-ltadd 11280 ax-pre-mulgt0 11281 ax-pre-sup 11282

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6541 df-fn 6542 df-f 6543 df-f1 6544 df-fo 6545 df-f1o 6546 df-fv 6547 df-riota 7378 df-ov 7424 df-oprab 7425 df-mpo 7426 df-om 7879 df-1st 8002 df-2nd 8003 df-frecs 8303 df-wrecs 8334 df-recs 8383 df-rdg 8422 df-1o 8480 df-2o 8481 df-er 8721 df-en 8978 df-dom 8979 df-sdom 8980 df-fin 8981 df-sup 9438 df-inf 9439 df-pnf 11349 df-mnf 11350 df-xr 11351 df-ltxr 11352 df-le 11353 df-sub 11547 df-neg 11548 df-div 11978 df-nn 12340 df-2 12409 df-3 12410 df-4 12411 df-n0 12611 df-z 12698 df-uz 12970 df-q 13080 df-rp 13125 df-fz 13644 df-fl 13936 df-mod 14014 df-seq 14149 df-exp 14209 df-cj 15272 df-re 15273 df-im 15274 df-sqrt 15408 df-abs 15409 df-dvds 16429 df-gcd 16671 df-prm 16853 df-numer 16917 df-denom 16918

This theorem is used by: nna4b4nsq 27996

W3C validator