flt4lem7

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

	Ref	Expression
Hypotheses	flt4lem7.a	$⊢ φ \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	1	nnsqcld	$⊢ φ \to A^{2} \in ℕ$
18	2	nnsqcld	$⊢ φ \to B^{2} \in ℕ$
19		2nn0	$⊢ 2 \in ℕ_{0}$
20	19	a1i	$⊢ φ \to 2 \in ℕ_{0}$
21	1	nncnd	$⊢ φ \to A \in ℂ$
22	21	flt4lem	$⊢ φ \to A^{4} = {(A^{2})}^{2}$
23	2	nncnd	$⊢ φ \to B \in ℂ$
24	23	flt4lem	$⊢ φ \to B^{4} = {(B^{2})}^{2}$
25	22 24	oveq12d	$⊢ φ \to A^{4} + B^{4} = {(A^{2})}^{2} + {(B^{2})}^{2}$
26	25 6	eqtr3d	$⊢ φ \to {(A^{2})}^{2} + {(B^{2})}^{2} = C^{2}$
27		2nn	$⊢ 2 \in ℕ$
28	27	a1i	$⊢ φ \to 2 \in ℕ$
29		rppwr	$⊢ (A \in ℕ \land B \in ℕ \land 2 \in ℕ) \to (A \gcd B = 1 \to A^{2} \gcd B^{2} = 1)$
30	1 2 28 29	syl3anc	$⊢ φ \to (A \gcd B = 1 \to A^{2} \gcd B^{2} = 1)$
31	5 30	mpd	$⊢ φ \to A^{2} \gcd B^{2} = 1$
32	17 18 3 20 26 31	fltaccoprm	$⊢ φ \to A^{2} \gcd C = 1$
33	1	nnzd	$⊢ φ \to A \in ℤ$
34	3	nnzd	$⊢ φ \to C \in ℤ$
35		rpexp	$⊢ (A \in ℤ \land C \in ℤ \land 2 \in ℕ) \to (A^{2} \gcd C = 1 \leftrightarrow A \gcd C = 1)$
36	33 34 28 35	syl3anc	$⊢ φ \to (A^{2} \gcd C = 1 \leftrightarrow A \gcd C = 1)$
37	32 36	mpbid	$⊢ φ \to A \gcd C = 1$
38	13 14 15 16 1 2 3 4 37 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 ℕ))$
39	38	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 ℕ)$
40	39	simp3d	$⊢ φ \to \frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2} \in ℕ$
41	38	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 ℕ)$
42	41	simprd	$⊢ φ \to \frac{B}{2} \in ℕ$
43		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 ℕ$
44	40 42 43	syl2anc	$⊢ φ \to (\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) \gcd (\frac{B}{2}) \in ℕ$
45	44	nnred	$⊢ φ \to (\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) \gcd (\frac{B}{2}) \in ℝ$
46	42	nnred	$⊢ φ \to \frac{B}{2} \in ℝ$
47	3	nnred	$⊢ φ \to C \in ℝ$
48	40	nnzd	$⊢ φ \to \frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2} \in ℤ$
49	48 42	gcdle2d	$⊢ φ \to (\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) \gcd (\frac{B}{2}) \leq \frac{B}{2}$
50	2	nnred	$⊢ φ \to B \in ℝ$
51	2	nnrpd	$⊢ φ \to B \in ℝ^{+}$
52		rphalflt	$⊢ B \in ℝ^{+} \to \frac{B}{2} < B$
53	51 52	syl	$⊢ φ \to \frac{B}{2} < B$
54	18	nnred	$⊢ φ \to B^{2} \in ℝ$
55		4nn0	$⊢ 4 \in ℕ_{0}$
56	55	a1i	$⊢ φ \to 4 \in ℕ_{0}$
57	2 56	nnexpcld	$⊢ φ \to B^{4} \in ℕ$
58	57	nnred	$⊢ φ \to B^{4} \in ℝ$
59	3	nnsqcld	$⊢ φ \to C^{2} \in ℕ$
60	59	nnred	$⊢ φ \to C^{2} \in ℝ$
61		2lt4	$⊢ 2 < 4$
62		2z	$⊢ 2 \in ℤ$
63	62	a1i	$⊢ φ \to 2 \in ℤ$
64		4z	$⊢ 4 \in ℤ$
65	64	a1i	$⊢ φ \to 4 \in ℤ$
66		1red	$⊢ φ \to 1 \in ℝ$
67		2re	$⊢ 2 \in ℝ$
68	67	a1i	$⊢ φ \to 2 \in ℝ$
69		1lt2	$⊢ 1 < 2$
70	69	a1i	$⊢ φ \to 1 < 2$
71		2t1e2	$⊢ 2 \cdot 1 = 2$
72	42	nnge1d	$⊢ φ \to 1 \leq \frac{B}{2}$
73		2rp	$⊢ 2 \in ℝ^{+}$
74	73	a1i	$⊢ φ \to 2 \in ℝ^{+}$
75	66 50 74	lemuldiv2d	$⊢ φ \to (2 \cdot 1 \leq B \leftrightarrow 1 \leq \frac{B}{2})$
76	72 75	mpbird	$⊢ φ \to 2 \cdot 1 \leq B$
77	71 76	eqbrtrrid	$⊢ φ \to 2 \leq B$
78	66 68 50 70 77	ltletrd	$⊢ φ \to 1 < B$
79	50 63 65 78	ltexp2d	$⊢ φ \to (2 < 4 \leftrightarrow B^{2} < B^{4})$
80	61 79	mpbii	$⊢ φ \to B^{2} < B^{4}$
81	1 56	nnexpcld	$⊢ φ \to A^{4} \in ℕ$
82	81	nngt0d	$⊢ φ \to 0 < A^{4}$
83	81	nnred	$⊢ φ \to A^{4} \in ℝ$
84	83 58	ltaddpos2d	$⊢ φ \to (0 < A^{4} \leftrightarrow B^{4} < A^{4} + B^{4})$
85	82 84	mpbid	$⊢ φ \to B^{4} < A^{4} + B^{4}$
86	85 6	breqtrd	$⊢ φ \to B^{4} < C^{2}$
87	54 58 60 80 86	lttrd	$⊢ φ \to B^{2} < C^{2}$
88	3	nnrpd	$⊢ φ \to C \in ℝ^{+}$
89	51 88 28	ltexp1d	$⊢ φ \to (B < C \leftrightarrow B^{2} < C^{2})$
90	87 89	mpbird	$⊢ φ \to B < C$
91	46 50 47 53 90	lttrd	$⊢ φ \to \frac{B}{2} < C$
92	45 46 47 49 91	lelttrd	$⊢ φ \to (\frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}) \gcd (\frac{B}{2}) < C$
93		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$
94	93	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)$
95		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}$
96	95	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}$
97	96	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})$
98	94 97	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}))$
99		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}))$
100	99	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)$
101		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}$
102	101	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}$
103	102	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})$
104	100 103	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}))$
105	39	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 ℕ$
106		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 ℕ$
107	105 42 106	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 ℕ$
108	39	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 ℕ$
109		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 ℕ$
110	108 42 109	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 ℕ$
111	105	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 ℤ$
112	42	nnzd	$⊢ φ \to \frac{B}{2} \in ℤ$
113	110	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 ℤ$
114		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})))$
115	111 112 113 114	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})))$
116	108	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 ℤ$
117		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}))$
118	112 112 116 117	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}))$
119	42	nnnn0d	$⊢ φ \to \frac{B}{2} \in ℕ_{0}$
120		gcdnn0id	$⊢ \frac{B}{2} \in ℕ_{0} \to (\frac{B}{2}) \gcd (\frac{B}{2}) = \frac{B}{2}$
121	119 120	syl	$⊢ φ \to (\frac{B}{2}) \gcd (\frac{B}{2}) = \frac{B}{2}$
122	121	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})$
123	112 116	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})$
124	122 123	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})$
125	116 112	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})$
126	125	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}))$
127	118 124 126	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})$
128	127	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}))$
129	38	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)$
130	129	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$
131	130	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})$
132		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}))$
133	111 116 112 132	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}))$
134		1gcd	$⊢ \frac{B}{2} \in ℤ \to 1 \gcd (\frac{B}{2}) = 1$
135	112 134	syl	$⊢ φ \to 1 \gcd (\frac{B}{2}) = 1$
136	131 133 135	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$
137	115 128 136	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$
138	13 14 15 16 1 2 3 4 37 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}$
139	138	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}$
140	137 139	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})$
141	98 104 107 110 140	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})$
142	92 141	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}))$
143	12 44 142	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}))$
144		breq2	$⊢ g = m \to (2 ∥ g \leftrightarrow 2 ∥ m)$
145	144	notbid	$⊢ g = m \to (\neg 2 ∥ g \leftrightarrow \neg 2 ∥ m)$
146		oveq1	$⊢ g = m \to g \gcd h = m \gcd h$
147	146	eqeq1d	$⊢ g = m \to (g \gcd h = 1 \leftrightarrow m \gcd h = 1)$
148		oveq1	$⊢ g = m \to g^{4} = m^{4}$
149	148	oveq1d	$⊢ g = m \to g^{4} + h^{4} = m^{4} + h^{4}$
150	149	eqeq1d	$⊢ g = m \to (g^{4} + h^{4} = l^{2} \leftrightarrow m^{4} + h^{4} = l^{2})$
151	147 150	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}))$
152	145 151	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})))$
153		oveq2	$⊢ h = n \to m \gcd h = m \gcd n$
154	153	eqeq1d	$⊢ h = n \to (m \gcd h = 1 \leftrightarrow m \gcd n = 1)$
155		oveq1	$⊢ h = n \to h^{4} = n^{4}$
156	155	oveq2d	$⊢ h = n \to m^{4} + h^{4} = m^{4} + n^{4}$
157	156	eqeq1d	$⊢ h = n \to (m^{4} + h^{4} = l^{2} \leftrightarrow m^{4} + n^{4} = l^{2})$
158	154 157	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}))$
159	158	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})))$
160		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 ℕ$
161	160	adantr	$⊢ (((((φ \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 ℕ$
162		simprr	$⊢ (((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \to n \in ℕ$
163	162	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 ℕ$
164		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$
165		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})$
166	164 165	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}))$
167	152 159 161 163 166	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}))$
168		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$
169	167 168	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)$
170		breq2	$⊢ g = n \to (2 ∥ g \leftrightarrow 2 ∥ n)$
171	170	notbid	$⊢ g = n \to (\neg 2 ∥ g \leftrightarrow \neg 2 ∥ n)$
172		oveq1	$⊢ g = n \to g \gcd h = n \gcd h$
173	172	eqeq1d	$⊢ g = n \to (g \gcd h = 1 \leftrightarrow n \gcd h = 1)$
174		oveq1	$⊢ g = n \to g^{4} = n^{4}$
175	174	oveq1d	$⊢ g = n \to g^{4} + h^{4} = n^{4} + h^{4}$
176	175	eqeq1d	$⊢ g = n \to (g^{4} + h^{4} = l^{2} \leftrightarrow n^{4} + h^{4} = l^{2})$
177	173 176	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}))$
178	171 177	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})))$
179		oveq2	$⊢ h = m \to n \gcd h = n \gcd m$
180	179	eqeq1d	$⊢ h = m \to (n \gcd h = 1 \leftrightarrow n \gcd m = 1)$
181		oveq1	$⊢ h = m \to h^{4} = m^{4}$
182	181	oveq2d	$⊢ h = m \to n^{4} + h^{4} = n^{4} + m^{4}$
183	182	eqeq1d	$⊢ h = m \to (n^{4} + h^{4} = l^{2} \leftrightarrow n^{4} + m^{4} = l^{2})$
184	180 183	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}))$
185	184	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})))$
186	162	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 ℕ$
187	160	adantr	$⊢ (((((φ \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 ℕ$
188		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$
189	186	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 ℤ$
190	187	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 ℤ$
191	189 190	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$
192		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$
193	191 192	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$
194	55	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}$
195	186 194	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 ℕ$
196	195	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 ℂ$
197	187 194	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 ℕ$
198	197	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 ℂ$
199	196 198	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}$
200		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}$
201	199 200	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}$
202	188 193 201	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}))$
203	178 185 186 187 202	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}))$
204		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$
205	203 204	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)$
206		simprl	$⊢ (((φ \land l \in ℕ) \land l < C) \land (m \in ℕ \land n \in ℕ)) \to m \in ℕ$
207	206	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 ℕ$
208	207	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 ℕ$
209	162	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 ℕ$
210	209	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 ℕ$
211		simp-5r	$⊢ (((((φ \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 l \in ℕ$
212	160	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 ℤ$
213	27	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 ℕ$
214		dvdsexp2im	$⊢ (2 \in ℤ \land m \in ℤ \land 2 \in ℕ) \to (2 ∥ m \to 2 ∥ m^{2})$
215	62 212 213 214	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})$
216	215	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}$
217	19	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 ℕ_{0}$
218	207	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 2 ∥ m) \to m \in ℂ$
219	218	flt4lem	$⊢ (((((φ \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^{4} = {(m^{2})}^{2}$
220	209	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 2 ∥ m) \to n \in ℂ$
221	220	flt4lem	$⊢ (((((φ \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^{4} = {(n^{2})}^{2}$
222	219 221	oveq12d	$⊢ (((((φ \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^{4} + n^{4} = {(m^{2})}^{2} + {(n^{2})}^{2}$
223		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 2 ∥ m) \to m^{4} + n^{4} = l^{2}$
224	222 223	eqtr3d	$⊢ (((((φ \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})}^{2} + {(n^{2})}^{2} = l^{2}$
225		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$
226	27	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 ℕ$
227		rppwr	$⊢ (m \in ℕ \land n \in ℕ \land 2 \in ℕ) \to (m \gcd n = 1 \to m^{2} \gcd n^{2} = 1)$
228	207 209 226 227	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)$
229	225 228	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$
230	208 210 211 217 224 229	fltaccoprm	$⊢ (((((φ \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 l = 1$
231	208 210 211 216 230 224	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}$
232	209	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 ℤ$
233		dvdsexp2im	$⊢ (2 \in ℤ \land n \in ℤ \land 2 \in ℕ) \to (2 ∥ n \to 2 ∥ n^{2})$
234	62 232 226 233	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})$
235	231 234	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$
236	235	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)$
237		imor	$⊢ (2 ∥ m \to \neg 2 ∥ n) \leftrightarrow (\neg 2 ∥ m \lor \neg 2 ∥ n)$
238	236 237	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)$
239	169 205 238	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)$
240	239	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))$
241	240	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))$
242	241	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))$
243	242	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))$
244	143 243	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