flt4lem5c

	Ref	Expression
Hypotheses	flt4lem5a.m	$⊢ M = \frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}$
	flt4lem5a.n	$⊢ N = \frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2}$
	flt4lem5a.r	$⊢ R = \frac{\sqrt{M + N} + \sqrt{M - N}}{2}$
	flt4lem5a.s	$⊢ S = \frac{\sqrt{M + N} - \sqrt{M - N}}{2}$
	flt4lem5a.a	$⊢ φ \to A \in ℕ$
	flt4lem5a.b	$⊢ φ \to B \in ℕ$
	flt4lem5a.c	$⊢ φ \to C \in ℕ$
	flt4lem5a.1	$⊢ φ \to \neg 2 ∥ A$
	flt4lem5a.2	$⊢ φ \to A \gcd C = 1$
	flt4lem5a.3	$⊢ φ \to A^{4} + B^{4} = C^{2}$
Assertion	flt4lem5c	$⊢ φ \to N = 2 R S$

Proof

Step	Hyp	Ref	Expression
1		flt4lem5a.m	$⊢ M = \frac{\sqrt{C + B^{2}} + \sqrt{C - B^{2}}}{2}$
2		flt4lem5a.n	$⊢ N = \frac{\sqrt{C + B^{2}} - \sqrt{C - B^{2}}}{2}$
3		flt4lem5a.r	$⊢ R = \frac{\sqrt{M + N} + \sqrt{M - N}}{2}$
4		flt4lem5a.s	$⊢ S = \frac{\sqrt{M + N} - \sqrt{M - N}}{2}$
5		flt4lem5a.a	$⊢ φ \to A \in ℕ$
6		flt4lem5a.b	$⊢ φ \to B \in ℕ$
7		flt4lem5a.c	$⊢ φ \to C \in ℕ$
8		flt4lem5a.1	$⊢ φ \to \neg 2 ∥ A$
9		flt4lem5a.2	$⊢ φ \to A \gcd C = 1$
10		flt4lem5a.3	$⊢ φ \to A^{4} + B^{4} = C^{2}$
11	5	nnsqcld	$⊢ φ \to A^{2} \in ℕ$
12	6	nnsqcld	$⊢ φ \to B^{2} \in ℕ$
13		2prm	$⊢ 2 \in ℙ$
14	5	nnzd	$⊢ φ \to A \in ℤ$
15		prmdvdssq	$⊢ (2 \in ℙ \land A \in ℤ) \to (2 ∥ A \leftrightarrow 2 ∥ A^{2})$
16	13 14 15	sylancr	$⊢ φ \to (2 ∥ A \leftrightarrow 2 ∥ A^{2})$
17	8 16	mtbid	$⊢ φ \to \neg 2 ∥ A^{2}$
18		2nn	$⊢ 2 \in ℕ$
19	18	a1i	$⊢ φ \to 2 \in ℕ$
20		rplpwr	$⊢ (A \in ℕ \land C \in ℕ \land 2 \in ℕ) \to (A \gcd C = 1 \to A^{2} \gcd C = 1)$
21	5 7 19 20	syl3anc	$⊢ φ \to (A \gcd C = 1 \to A^{2} \gcd C = 1)$
22	9 21	mpd	$⊢ φ \to A^{2} \gcd C = 1$
23	5	nncnd	$⊢ φ \to A \in ℂ$
24	23	exp4sqsq	$⊢ φ \to A^{4} = {(A^{2})}^{2}$
25	6	nncnd	$⊢ φ \to B \in ℂ$
26	25	exp4sqsq	$⊢ φ \to B^{4} = {(B^{2})}^{2}$
27	24 26	oveq12d	$⊢ φ \to A^{4} + B^{4} = {(A^{2})}^{2} + {(B^{2})}^{2}$
28	27 10	eqtr3d	$⊢ φ \to {(A^{2})}^{2} + {(B^{2})}^{2} = C^{2}$
29	11 12 7 17 22 28	flt4lem1	$⊢ φ \to ((A^{2} \in ℕ \land B^{2} \in ℕ \land C \in ℕ) \land {(A^{2})}^{2} + {(B^{2})}^{2} = C^{2} \land (A^{2} \gcd B^{2} = 1 \land \neg 2 ∥ A^{2}))$
30	2	pythagtriplem13	$⊢ ((A^{2} \in ℕ \land B^{2} \in ℕ \land C \in ℕ) \land {(A^{2})}^{2} + {(B^{2})}^{2} = C^{2} \land (A^{2} \gcd B^{2} = 1 \land \neg 2 ∥ A^{2})) \to N \in ℕ$
31	29 30	syl	$⊢ φ \to N \in ℕ$
32	1	pythagtriplem11	$⊢ ((A^{2} \in ℕ \land B^{2} \in ℕ \land C \in ℕ) \land {(A^{2})}^{2} + {(B^{2})}^{2} = C^{2} \land (A^{2} \gcd B^{2} = 1 \land \neg 2 ∥ A^{2})) \to M \in ℕ$
33	29 32	syl	$⊢ φ \to M \in ℕ$
34	1 2 3 4 5 6 7 8 9 10	flt4lem5a	$⊢ φ \to A^{2} + N^{2} = M^{2}$
35	31	nnzd	$⊢ φ \to N \in ℤ$
36	14 35	gcdcomd	$⊢ φ \to A \gcd N = N \gcd A$
37	33	nnzd	$⊢ φ \to M \in ℤ$
38	35 37	gcdcomd	$⊢ φ \to N \gcd M = M \gcd N$
39	1 2	flt4lem5	$⊢ ((A^{2} \in ℕ \land B^{2} \in ℕ \land C \in ℕ) \land {(A^{2})}^{2} + {(B^{2})}^{2} = C^{2} \land (A^{2} \gcd B^{2} = 1 \land \neg 2 ∥ A^{2})) \to M \gcd N = 1$
40	29 39	syl	$⊢ φ \to M \gcd N = 1$
41	38 40	eqtrd	$⊢ φ \to N \gcd M = 1$
42	31	nnsqcld	$⊢ φ \to N^{2} \in ℕ$
43	42	nncnd	$⊢ φ \to N^{2} \in ℂ$
44	11	nncnd	$⊢ φ \to A^{2} \in ℂ$
45	43 44	addcomd	$⊢ φ \to N^{2} + A^{2} = A^{2} + N^{2}$
46	45 34	eqtrd	$⊢ φ \to N^{2} + A^{2} = M^{2}$
47	31 5 33 41 46	fltabcoprm	$⊢ φ \to N \gcd A = 1$
48	36 47	eqtrd	$⊢ φ \to A \gcd N = 1$
49	3 4	pythagtriplem16	$⊢ ((A \in ℕ \land N \in ℕ \land M \in ℕ) \land A^{2} + N^{2} = M^{2} \land (A \gcd N = 1 \land \neg 2 ∥ A)) \to N = 2 R S$
50	5 31 33 34 48 8 49	syl312anc	$⊢ φ \to N = 2 R S$

Metamath Proof Explorer

Theorem flt4lem5c

Proof