flt4lem7

Description: Convert flt4lem5f into a convenient form for nna4b4nsq . (Contributed by SN, 25-Aug-2024)

	Ref	Expression
Hypotheses	flt4lem7.a	$⊢ φ \to A \in ℕ$
	flt4lem7.b	$⊢ φ \to B \in ℕ$
	flt4lem7.c	$⊢ φ \to C \in ℕ$
	flt4lem7.1	$⊢ φ \to \neg 2 ∥ A$
	flt4lem7.2	$⊢ φ \to A \gcd B = 1$
	flt4lem7.3	$⊢ φ \to A^{4} + B^{4} = C^{2}$
Assertion	flt4lem7	$⊢ φ \to \exists l \in ℕ (\exists g \in ℕ \exists h \in ℕ (\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = l^{2})) \land l < C)$

Proof

Step	Hyp	Ref	Expression
1		flt4lem7.a	$⊢ φ \to A \in ℕ$
2		flt4lem7.b	$⊢ φ \to B \in ℕ$
3		flt4lem7.c	$⊢ φ \to C \in ℕ$
4		flt4lem7.1	$⊢ φ \to \neg 2 ∥ A$
5		flt4lem7.2	$⊢ φ \to A \gcd B = 1$
6		flt4lem7.3	$⊢ φ \to A^{4} + B^{4} = C^{2}$
7		breq1	$⊢ l = (\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) \gcd (\frac{B}{2}) \to (l < C \leftrightarrow (\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) \gcd (\frac{B}{2}) < C)$
8		oveq1	$⊢ l = (\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) \gcd (\frac{B}{2}) \to l^{2} = {((\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) \gcd (\frac{B}{2}))}^{2}$
9	8	eqeq2d	$⊢ l = (\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) \gcd (\frac{B}{2}) \to (m^{4} + n^{4} = l^{2} \leftrightarrow m^{4} + n^{4} = {((\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) \gcd (\frac{B}{2}))}^{2})$
10	9	anbi2d	$⊢ l = (\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) \gcd (\frac{B}{2}) \to ((m \gcd n = 1 \land m^{4} + n^{4} = l^{2}) \leftrightarrow (m \gcd n = 1 \land m^{4} + n^{4} = {((\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) \gcd (\frac{B}{2}))}^{2}))$
11	10	2rexbidv	$⊢ l = (\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) \gcd (\frac{B}{2}) \to (\exists m \in ℕ \exists n \in ℕ (m \gcd n = 1 \land m^{4} + n^{4} = l^{2}) \leftrightarrow \exists m \in ℕ \exists n \in ℕ (m \gcd n = 1 \land m^{4} + n^{4} = {((\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) \gcd (\frac{B}{2}))}^{2}))$
12	7 11	anbi12d	$⊢ l = (\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) \gcd (\frac{B}{2}) \to ((l < C \land \exists m \in ℕ \exists n \in ℕ (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \leftrightarrow ((\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) \gcd (\frac{B}{2}) < C \land \exists m \in ℕ \exists n \in ℕ (m \gcd n = 1 \land m^{4} + n^{4} = {((\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) \gcd (\frac{B}{2}))}^{2})))$
13		eqid	$⊢ \frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2} = \frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}$
14		eqid	$⊢ \frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2} = \frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2}$
15		eqid	$⊢ \frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2} = \frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}$
16		eqid	$⊢ \frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2} = \frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}$
17	13 14 15 16 1 2 3 4 5 6	flt4lem5e	$⊢ φ \to (((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) = 1 \land (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) = 1 \land (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) = 1) \land (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2} \in ℕ \land \frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2} \in ℕ \land \frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2} \in ℕ) \land ((\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) = {(\frac{B}{2})}^{2} \land \frac{B}{2} \in ℕ))$
18	17	simp2d	$⊢ φ \to (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2} \in ℕ \land \frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2} \in ℕ \land \frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2} \in ℕ)$
19	18	simp3d	$⊢ φ \to \frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2} \in ℕ$
20	17	simp3d	$⊢ φ \to ((\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) = {(\frac{B}{2})}^{2} \land \frac{B}{2} \in ℕ)$
21	20	simprd	$⊢ φ \to \frac{B}{2} \in ℕ$
22		gcdnncl	$⊢ (\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2} \in ℕ \land \frac{B}{2} \in ℕ) \to (\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) \gcd (\frac{B}{2}) \in ℕ$
23	19 21 22	syl2anc	$⊢ φ \to (\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) \gcd (\frac{B}{2}) \in ℕ$
24	23	nnred	$⊢ φ \to (\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) \gcd (\frac{B}{2}) \in ℝ$
25	21	nnred	$⊢ φ \to \frac{B}{2} \in ℝ$
26	3	nnred	$⊢ φ \to C \in ℝ$
27	19	nnzd	$⊢ φ \to \frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2} \in ℤ$
28	27 21	gcdle2d	$⊢ φ \to (\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) \gcd (\frac{B}{2}) \leq \frac{B}{2}$
29	2	nnred	$⊢ φ \to B \in ℝ$
30	2	nnrpd	$⊢ φ \to B \in ℝ^{+}$
31		rphalflt	$⊢ B \in ℝ^{+} \to \frac{B}{2} < B$
32	30 31	syl	$⊢ φ \to \frac{B}{2} < B$
33	2	nnsqcld	$⊢ φ \to B^{2} \in ℕ$
34	33	nnred	$⊢ φ \to B^{2} \in ℝ$
35		4nn0	$⊢ 4 \in ℕ_{0}$
36	35	a1i	$⊢ φ \to 4 \in ℕ_{0}$
37	2 36	nnexpcld	$⊢ φ \to B^{4} \in ℕ$
38	37	nnred	$⊢ φ \to B^{4} \in ℝ$
39	3	nnsqcld	$⊢ φ \to C^{2} \in ℕ$
40	39	nnred	$⊢ φ \to C^{2} \in ℝ$
41		2lt4	$⊢ 2 < 4$
42		2z	$⊢ 2 \in ℤ$
43	42	a1i	$⊢ φ \to 2 \in ℤ$
44		4z	$⊢ 4 \in ℤ$
45	44	a1i	$⊢ φ \to 4 \in ℤ$
46		1red	$⊢ φ \to 1 \in ℝ$
47	21	nnge1d	$⊢ φ \to 1 \leq \frac{B}{2}$
48	46 25 29 47 32	lelttrd	$⊢ φ \to 1 < B$
49	29 43 45 48	ltexp2d	$⊢ φ \to (2 < 4 \leftrightarrow B^{2} < B^{4})$
50	41 49	mpbii	$⊢ φ \to B^{2} < B^{4}$
51	1 36	nnexpcld	$⊢ φ \to A^{4} \in ℕ$
52	51	nngt0d	$⊢ φ \to 0 < A^{4}$
53	51	nnred	$⊢ φ \to A^{4} \in ℝ$
54	53 38	ltaddpos2d	$⊢ φ \to (0 < A^{4} \leftrightarrow B^{4} < A^{4} + B^{4})$
55	52 54	mpbid	$⊢ φ \to B^{4} < A^{4} + B^{4}$
56	55 6	breqtrd	$⊢ φ \to B^{4} < C^{2}$
57	34 38 40 50 56	lttrd	$⊢ φ \to B^{2} < C^{2}$
58	3	nnrpd	$⊢ φ \to C \in ℝ^{+}$
59		2nn	$⊢ 2 \in ℕ$
60	59	a1i	$⊢ φ \to 2 \in ℕ$
61	30 58 60	ltexp1d	$⊢ φ \to (B < C \leftrightarrow B^{2} < C^{2})$
62	57 61	mpbird	$⊢ φ \to B < C$
63	25 29 26 32 62	lttrd	$⊢ φ \to \frac{B}{2} < C$
64	24 25 26 28 63	lelttrd	$⊢ φ \to (\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) \gcd (\frac{B}{2}) < C$
65		oveq1	$⊢ m = (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}) \to m \gcd n = ((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2})) \gcd n$
66	65	eqeq1d	$⊢ m = (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}) \to (m \gcd n = 1 \leftrightarrow ((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2})) \gcd n = 1)$
67		oveq1	$⊢ m = (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}) \to m^{4} = {((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}))}^{4}$
68	67	oveq1d	$⊢ m = (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}) \to m^{4} + n^{4} = {((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}))}^{4} + n^{4}$
69	68	eqeq1d	$⊢ m = (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}) \to (m^{4} + n^{4} = {((\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) \gcd (\frac{B}{2}))}^{2} \leftrightarrow {((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}))}^{4} + n^{4} = {((\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) \gcd (\frac{B}{2}))}^{2})$
70	66 69	anbi12d	$⊢ m = (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}) \to ((m \gcd n = 1 \land m^{4} + n^{4} = {((\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) \gcd (\frac{B}{2}))}^{2}) \leftrightarrow (((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2})) \gcd n = 1 \land {((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}))}^{4} + n^{4} = {((\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) \gcd (\frac{B}{2}))}^{2}))$
71		oveq2	$⊢ n = (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}) \to ((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2})) \gcd n = ((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2})) \gcd ((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}))$
72	71	eqeq1d	$⊢ n = (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}) \to (((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2})) \gcd n = 1 \leftrightarrow ((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2})) \gcd ((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2})) = 1)$
73		oveq1	$⊢ n = (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}) \to n^{4} = {((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}))}^{4}$
74	73	oveq2d	$⊢ n = (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}) \to {((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}))}^{4} + n^{4} = {((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}))}^{4} + {((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}))}^{4}$
75	74	eqeq1d	$⊢ n = (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}) \to ({((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}))}^{4} + n^{4} = {((\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) \gcd (\frac{B}{2}))}^{2} \leftrightarrow {((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}))}^{4} + {((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}))}^{4} = {((\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) \gcd (\frac{B}{2}))}^{2})$
76	72 75	anbi12d	$⊢ n = (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}) \to ((((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2})) \gcd n = 1 \land {((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}))}^{4} + n^{4} = {((\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) \gcd (\frac{B}{2}))}^{2}) \leftrightarrow (((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2})) \gcd ((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2})) = 1 \land {((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}))}^{4} + {((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}))}^{4} = {((\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) \gcd (\frac{B}{2}))}^{2}))$
77	18	simp1d	$⊢ φ \to \frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2} \in ℕ$
78		gcdnncl	$⊢ (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2} \in ℕ \land \frac{B}{2} \in ℕ) \to (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}) \in ℕ$
79	77 21 78	syl2anc	$⊢ φ \to (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}) \in ℕ$
80	18	simp2d	$⊢ φ \to \frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2} \in ℕ$
81		gcdnncl	$⊢ (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2} \in ℕ \land \frac{B}{2} \in ℕ) \to (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}) \in ℕ$
82	80 21 81	syl2anc	$⊢ φ \to (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}) \in ℕ$
83	77	nnzd	$⊢ φ \to \frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2} \in ℤ$
84	21	nnzd	$⊢ φ \to \frac{B}{2} \in ℤ$
85	82	nnzd	$⊢ φ \to (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}) \in ℤ$
86		gcdass	$⊢ (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2} \in ℤ \land \frac{B}{2} \in ℤ \land (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}) \in ℤ) \to ((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2})) \gcd ((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2})) = (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd ((\frac{B}{2}) \gcd ((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2})))$
87	83 84 85 86	syl3anc	$⊢ φ \to ((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2})) \gcd ((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2})) = (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd ((\frac{B}{2}) \gcd ((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2})))$
88	80	nnzd	$⊢ φ \to \frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2} \in ℤ$
89		gcdass	$⊢ (\frac{B}{2} \in ℤ \land \frac{B}{2} \in ℤ \land \frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2} \in ℤ) \to ((\frac{B}{2}) \gcd (\frac{B}{2})) \gcd (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) = (\frac{B}{2}) \gcd ((\frac{B}{2}) \gcd (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}))$
90	84 84 88 89	syl3anc	$⊢ φ \to ((\frac{B}{2}) \gcd (\frac{B}{2})) \gcd (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) = (\frac{B}{2}) \gcd ((\frac{B}{2}) \gcd (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}))$
91	21	nnnn0d	$⊢ φ \to \frac{B}{2} \in ℕ_{0}$
92		gcdnn0id	$⊢ \frac{B}{2} \in ℕ_{0} \to (\frac{B}{2}) \gcd (\frac{B}{2}) = \frac{B}{2}$
93	91 92	syl	$⊢ φ \to (\frac{B}{2}) \gcd (\frac{B}{2}) = \frac{B}{2}$
94	93	oveq1d	$⊢ φ \to ((\frac{B}{2}) \gcd (\frac{B}{2})) \gcd (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) = (\frac{B}{2}) \gcd (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2})$
95	84 88	gcdcomd	$⊢ φ \to (\frac{B}{2}) \gcd (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) = (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2})$
96	94 95	eqtr2d	$⊢ φ \to (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}) = ((\frac{B}{2}) \gcd (\frac{B}{2})) \gcd (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2})$
97	88 84	gcdcomd	$⊢ φ \to (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}) = (\frac{B}{2}) \gcd (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2})$
98	97	oveq2d	$⊢ φ \to (\frac{B}{2}) \gcd ((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2})) = (\frac{B}{2}) \gcd ((\frac{B}{2}) \gcd (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}))$
99	90 96 98	3eqtr4rd	$⊢ φ \to (\frac{B}{2}) \gcd ((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2})) = (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2})$
100	99	oveq2d	$⊢ φ \to (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd ((\frac{B}{2}) \gcd ((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}))) = (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd ((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}))$
101	17	simp1d	$⊢ φ \to ((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) = 1 \land (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) = 1 \land (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) = 1)$
102	101	simp1d	$⊢ φ \to (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) = 1$
103	102	oveq1d	$⊢ φ \to ((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2})) \gcd (\frac{B}{2}) = 1 \gcd (\frac{B}{2})$
104		gcdass	$⊢ (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2} \in ℤ \land \frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2} \in ℤ \land \frac{B}{2} \in ℤ) \to ((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2})) \gcd (\frac{B}{2}) = (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd ((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}))$
105	83 88 84 104	syl3anc	$⊢ φ \to ((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2})) \gcd (\frac{B}{2}) = (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd ((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}))$
106		1gcd	$⊢ \frac{B}{2} \in ℤ \to 1 \gcd (\frac{B}{2}) = 1$
107	84 106	syl	$⊢ φ \to 1 \gcd (\frac{B}{2}) = 1$
108	103 105 107	3eqtr3d	$⊢ φ \to (\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd ((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2})) = 1$
109	87 100 108	3eqtrd	$⊢ φ \to ((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2})) \gcd ((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2})) = 1$
110	13 14 15 16 1 2 3 4 5 6	flt4lem5f	$⊢ φ \to {((\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) \gcd (\frac{B}{2}))}^{2} = {((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}))}^{4} + {((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}))}^{4}$
111	110	eqcomd	$⊢ φ \to {((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}))}^{4} + {((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}))}^{4} = {((\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) \gcd (\frac{B}{2}))}^{2}$
112	109 111	jca	$⊢ φ \to (((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2})) \gcd ((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2})) = 1 \land {((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} + \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}))}^{4} + {((\frac{\sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) + (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})} - \sqrt{(\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) - (\frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2})}}{2}) \gcd (\frac{B}{2}))}^{4} = {((\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) \gcd (\frac{B}{2}))}^{2})$
113	70 76 79 82 112	2rspcedvdw	$⊢ φ \to \exists m \in ℕ \exists n \in ℕ (m \gcd n = 1 \land m^{4} + n^{4} = {((\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) \gcd (\frac{B}{2}))}^{2})$
114	64 113	jca	$⊢ φ \to ((\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) \gcd (\frac{B}{2}) < C \land \exists m \in ℕ \exists n \in ℕ (m \gcd n = 1 \land m^{4} + n^{4} = {((\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) \gcd (\frac{B}{2}))}^{2}))$
115	12 23 114	rspcedvdw	$⊢ φ \to \exists l \in ℕ (l < C \land \exists m \in ℕ \exists n \in ℕ (m \gcd n = 1 \land m^{4} + n^{4} = l^{2}))$
116		breq2	$⊢ g = m \to (2 ∥ g \leftrightarrow 2 ∥ m)$
117	116	notbid	$⊢ g = m \to (\neg 2 ∥ g \leftrightarrow \neg 2 ∥ m)$
118		oveq1	$⊢ g = m \to g \gcd h = m \gcd h$
119	118	eqeq1d	$⊢ g = m \to (g \gcd h = 1 \leftrightarrow m \gcd h = 1)$
120		oveq1	$⊢ g = m \to g^{4} = m^{4}$
121	120	oveq1d	$⊢ g = m \to g^{4} + h^{4} = m^{4} + h^{4}$
122	121	eqeq1d	$⊢ g = m \to (g^{4} + h^{4} = l^{2} \leftrightarrow m^{4} + h^{4} = l^{2})$
123	119 122	anbi12d	$⊢ g = m \to ((g \gcd h = 1 \land g^{4} + h^{4} = l^{2}) \leftrightarrow (m \gcd h = 1 \land m^{4} + h^{4} = l^{2}))$
124	117 123	anbi12d	$⊢ g = m \to ((\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = l^{2})) \leftrightarrow (\neg 2 ∥ m \land (m \gcd h = 1 \land m^{4} + h^{4} = l^{2})))$
125		oveq2	$⊢ h = n \to m \gcd h = m \gcd n$
126	125	eqeq1d	$⊢ h = n \to (m \gcd h = 1 \leftrightarrow m \gcd n = 1)$
127		oveq1	$⊢ h = n \to h^{4} = n^{4}$
128	127	oveq2d	$⊢ h = n \to m^{4} + h^{4} = m^{4} + n^{4}$
129	128	eqeq1d	$⊢ h = n \to (m^{4} + h^{4} = l^{2} \leftrightarrow m^{4} + n^{4} = l^{2})$
130	126 129	anbi12d	$⊢ h = n \to ((m \gcd h = 1 \land m^{4} + h^{4} = l^{2}) \leftrightarrow (m \gcd n = 1 \land m^{4} + n^{4} = l^{2}))$
131	130	anbi2d	$⊢ h = n \to ((\neg 2 ∥ m \land (m \gcd h = 1 \land m^{4} + h^{4} = l^{2})) \leftrightarrow (\neg 2 ∥ m \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})))$
132		simprl	$⊢ (((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \to m \in ℕ$
133	132	ad2antrr	$⊢ (((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \land \neg 2 ∥ m) \to m \in ℕ$
134		simprr	$⊢ (((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \to n \in ℕ$
135	134	ad2antrr	$⊢ (((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \land \neg 2 ∥ m) \to n \in ℕ$
136		simpr	$⊢ (((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \land \neg 2 ∥ m) \to \neg 2 ∥ m$
137		simplr	$⊢ (((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \land \neg 2 ∥ m) \to (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})$
138	136 137	jca	$⊢ (((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \land \neg 2 ∥ m) \to (\neg 2 ∥ m \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2}))$
139	124 131 133 135 138	2rspcedvdw	$⊢ (((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \land \neg 2 ∥ m) \to \exists g \in ℕ \exists h \in ℕ (\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = l^{2}))$
140		simp-4r	$⊢ (((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \land \neg 2 ∥ m) \to l < C$
141	139 140	jca	$⊢ (((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \land \neg 2 ∥ m) \to (\exists g \in ℕ \exists h \in ℕ (\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = l^{2})) \land l < C)$
142		breq2	$⊢ g = n \to (2 ∥ g \leftrightarrow 2 ∥ n)$
143	142	notbid	$⊢ g = n \to (\neg 2 ∥ g \leftrightarrow \neg 2 ∥ n)$
144		oveq1	$⊢ g = n \to g \gcd h = n \gcd h$
145	144	eqeq1d	$⊢ g = n \to (g \gcd h = 1 \leftrightarrow n \gcd h = 1)$
146		oveq1	$⊢ g = n \to g^{4} = n^{4}$
147	146	oveq1d	$⊢ g = n \to g^{4} + h^{4} = n^{4} + h^{4}$
148	147	eqeq1d	$⊢ g = n \to (g^{4} + h^{4} = l^{2} \leftrightarrow n^{4} + h^{4} = l^{2})$
149	145 148	anbi12d	$⊢ g = n \to ((g \gcd h = 1 \land g^{4} + h^{4} = l^{2}) \leftrightarrow (n \gcd h = 1 \land n^{4} + h^{4} = l^{2}))$
150	143 149	anbi12d	$⊢ g = n \to ((\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = l^{2})) \leftrightarrow (\neg 2 ∥ n \land (n \gcd h = 1 \land n^{4} + h^{4} = l^{2})))$
151		oveq2	$⊢ h = m \to n \gcd h = n \gcd m$
152	151	eqeq1d	$⊢ h = m \to (n \gcd h = 1 \leftrightarrow n \gcd m = 1)$
153		oveq1	$⊢ h = m \to h^{4} = m^{4}$
154	153	oveq2d	$⊢ h = m \to n^{4} + h^{4} = n^{4} + m^{4}$
155	154	eqeq1d	$⊢ h = m \to (n^{4} + h^{4} = l^{2} \leftrightarrow n^{4} + m^{4} = l^{2})$
156	152 155	anbi12d	$⊢ h = m \to ((n \gcd h = 1 \land n^{4} + h^{4} = l^{2}) \leftrightarrow (n \gcd m = 1 \land n^{4} + m^{4} = l^{2}))$
157	156	anbi2d	$⊢ h = m \to ((\neg 2 ∥ n \land (n \gcd h = 1 \land n^{4} + h^{4} = l^{2})) \leftrightarrow (\neg 2 ∥ n \land (n \gcd m = 1 \land n^{4} + m^{4} = l^{2})))$
158	134	ad2antrr	$⊢ (((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \land \neg 2 ∥ n) \to n \in ℕ$
159	132	ad2antrr	$⊢ (((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \land \neg 2 ∥ n) \to m \in ℕ$
160		simpr	$⊢ (((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \land \neg 2 ∥ n) \to \neg 2 ∥ n$
161	158	nnzd	$⊢ (((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \land \neg 2 ∥ n) \to n \in ℤ$
162	159	nnzd	$⊢ (((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \land \neg 2 ∥ n) \to m \in ℤ$
163	161 162	gcdcomd	$⊢ (((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \land \neg 2 ∥ n) \to n \gcd m = m \gcd n$
164		simplrl	$⊢ (((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \land \neg 2 ∥ n) \to m \gcd n = 1$
165	163 164	eqtrd	$⊢ (((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \land \neg 2 ∥ n) \to n \gcd m = 1$
166	35	a1i	$⊢ (((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \land \neg 2 ∥ n) \to 4 \in ℕ_{0}$
167	158 166	nnexpcld	$⊢ (((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \land \neg 2 ∥ n) \to n^{4} \in ℕ$
168	167	nncnd	$⊢ (((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \land \neg 2 ∥ n) \to n^{4} \in ℂ$
169	159 166	nnexpcld	$⊢ (((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \land \neg 2 ∥ n) \to m^{4} \in ℕ$
170	169	nncnd	$⊢ (((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \land \neg 2 ∥ n) \to m^{4} \in ℂ$
171	168 170	addcomd	$⊢ (((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \land \neg 2 ∥ n) \to n^{4} + m^{4} = m^{4} + n^{4}$
172		simplrr	$⊢ (((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \land \neg 2 ∥ n) \to m^{4} + n^{4} = l^{2}$
173	171 172	eqtrd	$⊢ (((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \land \neg 2 ∥ n) \to n^{4} + m^{4} = l^{2}$
174	160 165 173	jca32	$⊢ (((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \land \neg 2 ∥ n) \to (\neg 2 ∥ n \land (n \gcd m = 1 \land n^{4} + m^{4} = l^{2}))$
175	150 157 158 159 174	2rspcedvdw	$⊢ (((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \land \neg 2 ∥ n) \to \exists g \in ℕ \exists h \in ℕ (\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = l^{2}))$
176		simp-4r	$⊢ (((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \land \neg 2 ∥ n) \to l < C$
177	175 176	jca	$⊢ (((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \land \neg 2 ∥ n) \to (\exists g \in ℕ \exists h \in ℕ (\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = l^{2})) \land l < C)$
178	132	ad2antrr	$⊢ (((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \land 2 ∥ m) \to m \in ℕ$
179	178	nnsqcld	$⊢ (((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \land 2 ∥ m) \to m^{2} \in ℕ$
180	134	ad2antrr	$⊢ (((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \land 2 ∥ m) \to n \in ℕ$
181	180	nnsqcld	$⊢ (((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \land 2 ∥ m) \to n^{2} \in ℕ$
182		simplrl	$⊢ ((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \to m \in ℕ$
183	182	nnzd	$⊢ ((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \to m \in ℤ$
184	59	a1i	$⊢ ((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \to 2 \in ℕ$
185		dvdsexp2im	$⊢ (2 \in ℤ \land m \in ℤ \land 2 \in ℕ) \to (2 ∥ m \to 2 ∥ m^{2})$
186	42 183 184 185	mp3an2i	$⊢ ((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \to (2 ∥ m \to 2 ∥ m^{2})$
187	186	imp	$⊢ (((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \land 2 ∥ m) \to 2 ∥ m^{2}$
188		simplrl	$⊢ (((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \land 2 ∥ m) \to m \gcd n = 1$
189	59	a1i	$⊢ (((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \land 2 ∥ m) \to 2 \in ℕ$
190		rppwr	$⊢ (m \in ℕ \land n \in ℕ \land 2 \in ℕ) \to (m \gcd n = 1 \to m^{2} \gcd n^{2} = 1)$
191	178 180 189 190	syl3anc	$⊢ (((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \land 2 ∥ m) \to (m \gcd n = 1 \to m^{2} \gcd n^{2} = 1)$
192	188 191	mpd	$⊢ (((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \land 2 ∥ m) \to m^{2} \gcd n^{2} = 1$
193	179 181 187 192	flt4lem2	$⊢ (((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \land 2 ∥ m) \to \neg 2 ∥ n^{2}$
194	180	nnzd	$⊢ (((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \land 2 ∥ m) \to n \in ℤ$
195		dvdsexp2im	$⊢ (2 \in ℤ \land n \in ℤ \land 2 \in ℕ) \to (2 ∥ n \to 2 ∥ n^{2})$
196	42 194 189 195	mp3an2i	$⊢ (((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \land 2 ∥ m) \to (2 ∥ n \to 2 ∥ n^{2})$
197	193 196	mtod	$⊢ (((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \land 2 ∥ m) \to \neg 2 ∥ n$
198	197	ex	$⊢ ((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \to (2 ∥ m \to \neg 2 ∥ n)$
199		imor	$⊢ (2 ∥ m \to \neg 2 ∥ n) \leftrightarrow (\neg 2 ∥ m \lor \neg 2 ∥ n)$
200	198 199	sylib	$⊢ ((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \to (\neg 2 ∥ m \lor \neg 2 ∥ n)$
201	141 177 200	mpjaodan	$⊢ ((((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \land (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \to (\exists g \in ℕ \exists h \in ℕ (\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = l^{2})) \land l < C)$
202	201	ex	$⊢ (((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \to ((m \gcd n = 1 \land m^{4} + n^{4} = l^{2}) \to (\exists g \in ℕ \exists h \in ℕ (\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = l^{2})) \land l < C))$
203	202	rexlimdvva	$⊢ ((φ \land l \in ℕ) \land l < C) \to (\exists m \in ℕ \exists n \in ℕ (m \gcd n = 1 \land m^{4} + n^{4} = l^{2}) \to (\exists g \in ℕ \exists h \in ℕ (\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = l^{2})) \land l < C))$
204	203	expimpd	$⊢ (φ \land l \in ℕ) \to ((l < C \land \exists m \in ℕ \exists n \in ℕ (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \to (\exists g \in ℕ \exists h \in ℕ (\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = l^{2})) \land l < C))$
205	204	reximdva	$⊢ φ \to (\exists l \in ℕ (l < C \land \exists m \in ℕ \exists n \in ℕ (m \gcd n = 1 \land m^{4} + n^{4} = l^{2})) \to \exists l \in ℕ (\exists g \in ℕ \exists h \in ℕ (\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = l^{2})) \land l < C))$
206	115 205	mpd	$⊢ φ \to \exists l \in ℕ (\exists g \in ℕ \exists h \in ℕ (\neg 2 ∥ g \land (g \gcd h = 1 \land g^{4} + h^{4} = l^{2})) \land l < C)$

Metamath Proof Explorer

Theorem flt4lem7

Proof