flt4lem5e

Description: Satisfy the hypotheses of flt4lem4 . (Contributed by SN, 23-Aug-2024)

	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	flt4lem5e	$⊢ φ \to ((R \gcd S = 1 \land R \gcd M = 1 \land S \gcd M = 1) \land (R \in ℕ \land S \in ℕ \land M \in ℕ) \land (M R S = {(\frac{B}{2})}^{2} \land \frac{B}{2} \in ℕ))$

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	flt4lem	$⊢ φ \to A^{4} = {(A^{2})}^{2}$
25	6	nncnd	$⊢ φ \to B \in ℂ$
26	25	flt4lem	$⊢ φ \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	flt4lem5	$⊢ ((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 R \gcd S = 1$
50	5 31 33 34 48 8 49	syl312anc	$⊢ φ \to R \gcd S = 1$
51	3	pythagtriplem11	$⊢ ((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 R \in ℕ$
52	5 31 33 34 48 8 51	syl312anc	$⊢ φ \to R \in ℕ$
53	4	pythagtriplem13	$⊢ ((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 S \in ℕ$
54	5 31 33 34 48 8 53	syl312anc	$⊢ φ \to S \in ℕ$
55	1 2 3 4 5 6 7 8 9 10	flt4lem5d	$⊢ φ \to M = R^{2} + S^{2}$
56	33 52 54 55 50	flt4lem5elem	$⊢ φ \to (R \gcd M = 1 \land S \gcd M = 1)$
57		3anass	$⊢ (R \gcd S = 1 \land R \gcd M = 1 \land S \gcd M = 1) \leftrightarrow (R \gcd S = 1 \land (R \gcd M = 1 \land S \gcd M = 1))$
58	50 56 57	sylanbrc	$⊢ φ \to (R \gcd S = 1 \land R \gcd M = 1 \land S \gcd M = 1)$
59	52 54 33	3jca	$⊢ φ \to (R \in ℕ \land S \in ℕ \land M \in ℕ)$
60		sq2	$⊢ 2^{2} = 4$
61		4cn	$⊢ 4 \in ℂ$
62	60 61	eqeltri	$⊢ 2^{2} \in ℂ$
63	62	a1i	$⊢ φ \to 2^{2} \in ℂ$
64	52 54	nnmulcld	$⊢ φ \to R S \in ℕ$
65	33 64	nnmulcld	$⊢ φ \to M R S \in ℕ$
66	65	nncnd	$⊢ φ \to M R S \in ℂ$
67		4ne0	$⊢ 4 \neq 0$
68	60 67	eqnetri	$⊢ 2^{2} \neq 0$
69	68	a1i	$⊢ φ \to 2^{2} \neq 0$
70		2cn	$⊢ 2 \in ℂ$
71	70	sqvali	$⊢ 2^{2} = 2 \cdot 2$
72	71	oveq1i	$⊢ 2^{2} M R S = 2 \cdot 2 M R S$
73		2cnd	$⊢ φ \to 2 \in ℂ$
74	33	nncnd	$⊢ φ \to M \in ℂ$
75	64	nncnd	$⊢ φ \to R S \in ℂ$
76	73 73 74 75	mul4d	$⊢ φ \to 2 \cdot 2 M R S = 2 \cdot M 2 R S$
77	1 2 3 4 5 6 7 8 9 10	flt4lem5c	$⊢ φ \to N = 2 R S$
78	77 31	eqeltrrd	$⊢ φ \to 2 R S \in ℕ$
79	78	nncnd	$⊢ φ \to 2 R S \in ℂ$
80	73 74 79	mulassd	$⊢ φ \to 2 \cdot M 2 R S = 2 M 2 R S$
81	77	eqcomd	$⊢ φ \to 2 R S = N$
82	81	oveq2d	$⊢ φ \to M 2 R S = M \cdot N$
83	82	oveq2d	$⊢ φ \to 2 M 2 R S = 2 M \cdot N$
84	80 83	eqtrd	$⊢ φ \to 2 \cdot M 2 R S = 2 M \cdot N$
85	1 2 3 4 5 6 7 8 9 10	flt4lem5b	$⊢ φ \to 2 M \cdot N = B^{2}$
86	76 84 85	3eqtrd	$⊢ φ \to 2 \cdot 2 M R S = B^{2}$
87	72 86	syl5eq	$⊢ φ \to 2^{2} M R S = B^{2}$
88	63 66 69 87	mvllmuld	$⊢ φ \to M R S = \frac{B^{2}}{2^{2}}$
89		2ne0	$⊢ 2 \neq 0$
90	89	a1i	$⊢ φ \to 2 \neq 0$
91	25 73 90	sqdivd	$⊢ φ \to {(\frac{B}{2})}^{2} = \frac{B^{2}}{2^{2}}$
92	88 91	eqtr4d	$⊢ φ \to M R S = {(\frac{B}{2})}^{2}$
93	65	nnzd	$⊢ φ \to M R S \in ℤ$
94	92 93	eqeltrrd	$⊢ φ \to {(\frac{B}{2})}^{2} \in ℤ$
95	6	nnzd	$⊢ φ \to B \in ℤ$
96		znq	$⊢ (B \in ℤ \land 2 \in ℕ) \to \frac{B}{2} \in ℚ$
97	95 18 96	sylancl	$⊢ φ \to \frac{B}{2} \in ℚ$
98	6	nngt0d	$⊢ φ \to 0 < B$
99	6	nnred	$⊢ φ \to B \in ℝ$
100		halfpos2	$⊢ B \in ℝ \to (0 < B \leftrightarrow 0 < \frac{B}{2})$
101	99 100	syl	$⊢ φ \to (0 < B \leftrightarrow 0 < \frac{B}{2})$
102	98 101	mpbid	$⊢ φ \to 0 < \frac{B}{2}$
103	94 97 102	posqsqznn	$⊢ φ \to \frac{B}{2} \in ℕ$
104	92 103	jca	$⊢ φ \to (M R S = {(\frac{B}{2})}^{2} \land \frac{B}{2} \in ℕ)$
105	58 59 104	3jca	$⊢ φ \to ((R \gcd S = 1 \land R \gcd M = 1 \land S \gcd M = 1) \land (R \in ℕ \land S \in ℕ \land M \in ℕ) \land (M R S = {(\frac{B}{2})}^{2} \land \frac{B}{2} \in ℕ))$

Metamath Proof Explorer

Theorem flt4lem5e

Proof