flt4lem5e

Description: Satisfy the hypotheses of flt4lem4 . EDITORIAL: This is not minimized! (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	50 56	jca	$⊢ φ \to (R \gcd S = 1 \land (R \gcd M = 1 \land S \gcd M = 1))$
58		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))$
59	57 58	sylibr	$⊢ φ \to (R \gcd S = 1 \land R \gcd M = 1 \land S \gcd M = 1)$
60	52 54 33	3jca	$⊢ φ \to (R \in ℕ \land S \in ℕ \land M \in ℕ)$
61		sq2	$⊢ 2^{2} = 4$
62		4cn	$⊢ 4 \in ℂ$
63	61 62	eqeltri	$⊢ 2^{2} \in ℂ$
64	63	a1i	$⊢ φ \to 2^{2} \in ℂ$
65	52 54	nnmulcld	$⊢ φ \to R S \in ℕ$
66	33 65	nnmulcld	$⊢ φ \to M R S \in ℕ$
67	66	nncnd	$⊢ φ \to M R S \in ℂ$
68		4ne0	$⊢ 4 \neq 0$
69	61 68	eqnetri	$⊢ 2^{2} \neq 0$
70	69	a1i	$⊢ φ \to 2^{2} \neq 0$
71		2cn	$⊢ 2 \in ℂ$
72	71	sqvali	$⊢ 2^{2} = 2 \cdot 2$
73	72	oveq1i	$⊢ 2^{2} M R S = 2 \cdot 2 M R S$
74		2cnd	$⊢ φ \to 2 \in ℂ$
75	33	nncnd	$⊢ φ \to M \in ℂ$
76	65	nncnd	$⊢ φ \to R S \in ℂ$
77	74 74 75 76	mul4d	$⊢ φ \to 2 \cdot 2 M R S = 2 \cdot M 2 R S$
78	1 2 3 4 5 6 7 8 9 10	flt4lem5c	$⊢ φ \to N = 2 R S$
79	78	eqcomd	$⊢ φ \to 2 R S = N$
80	79 31	eqeltrd	$⊢ φ \to 2 R S \in ℕ$
81	80	nncnd	$⊢ φ \to 2 R S \in ℂ$
82	74 75 81	mulassd	$⊢ φ \to 2 \cdot M 2 R S = 2 M 2 R S$
83	79	oveq2d	$⊢ φ \to M 2 R S = M \cdot N$
84	83	oveq2d	$⊢ φ \to 2 M 2 R S = 2 M \cdot N$
85	82 84	eqtrd	$⊢ φ \to 2 \cdot M 2 R S = 2 M \cdot N$
86	1 2 3 4 5 6 7 8 9 10	flt4lem5b	$⊢ φ \to 2 M \cdot N = B^{2}$
87	77 85 86	3eqtrd	$⊢ φ \to 2 \cdot 2 M R S = B^{2}$
88	73 87	syl5eq	$⊢ φ \to 2^{2} M R S = B^{2}$
89	64 67 70 88	mvllmuld	$⊢ φ \to M R S = \frac{B^{2}}{2^{2}}$
90		2ne0	$⊢ 2 \neq 0$
91	90	a1i	$⊢ φ \to 2 \neq 0$
92	25 74 91	sqdivd	$⊢ φ \to {(\frac{B}{2})}^{2} = \frac{B^{2}}{2^{2}}$
93	89 92	eqtr4d	$⊢ φ \to M R S = {(\frac{B}{2})}^{2}$
94	66	nnzd	$⊢ φ \to M R S \in ℤ$
95	93 94	eqeltrrd	$⊢ φ \to {(\frac{B}{2})}^{2} \in ℤ$
96	6	nnzd	$⊢ φ \to B \in ℤ$
97		znq	$⊢ (B \in ℤ \land 2 \in ℕ) \to \frac{B}{2} \in ℚ$
98	96 18 97	sylancl	$⊢ φ \to \frac{B}{2} \in ℚ$
99	6	nngt0d	$⊢ φ \to 0 < B$
100	6	nnred	$⊢ φ \to B \in ℝ$
101		halfpos2	$⊢ B \in ℝ \to (0 < B \leftrightarrow 0 < \frac{B}{2})$
102	100 101	syl	$⊢ φ \to (0 < B \leftrightarrow 0 < \frac{B}{2})$
103	99 102	mpbid	$⊢ φ \to 0 < \frac{B}{2}$
104	95 98 103	posqsqznn	$⊢ φ \to \frac{B}{2} \in ℕ$
105	93 104	jca	$⊢ φ \to (M R S = {(\frac{B}{2})}^{2} \land \frac{B}{2} \in ℕ)$
106	59 60 105	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