Theorem flt4lem5e

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

	Ref	Expression
Hypotheses	flt4lem5a.m	⊢ 𝑀 = ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 )
	flt4lem5a.n	⊢ 𝑁 = ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 )
	flt4lem5a.r	⊢ 𝑅 = ( ( ( √ ‘ ( 𝑀 + 𝑁 ) ) + ( √ ‘ ( 𝑀 − 𝑁 ) ) ) / 2 )
	flt4lem5a.s	⊢ 𝑆 = ( ( ( √ ‘ ( 𝑀 + 𝑁 ) ) − ( √ ‘ ( 𝑀 − 𝑁 ) ) ) / 2 )
	flt4lem5a.a	⊢ ( 𝜑 → 𝐴 ∈ ℕ )
	flt4lem5a.b	⊢ ( 𝜑 → 𝐵 ∈ ℕ )
	flt4lem5a.c	⊢ ( 𝜑 → 𝐶 ∈ ℕ )
	flt4lem5a.1	⊢ ( 𝜑 → ¬ 2 ∥ 𝐴 )
	flt4lem5a.2	⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) = 1 )
	flt4lem5a.3	⊢ ( 𝜑 → ( ( 𝐴 ↑ 4 ) + ( 𝐵 ↑ 4 ) ) = ( 𝐶 ↑ 2 ) )
Assertion	flt4lem5e	⊢ ( 𝜑 → ( ( ( 𝑅 gcd 𝑆 ) = 1 ∧ ( 𝑅 gcd 𝑀 ) = 1 ∧ ( 𝑆 gcd 𝑀 ) = 1 ) ∧ ( 𝑅 ∈ ℕ ∧ 𝑆 ∈ ℕ ∧ 𝑀 ∈ ℕ ) ∧ ( ( 𝑀 · ( 𝑅 · 𝑆 ) ) = ( ( 𝐵 / 2 ) ↑ 2 ) ∧ ( 𝐵 / 2 ) ∈ ℕ ) ) )

Proof

Step	Hyp	Ref	Expression
1		flt4lem5a.m	⊢ 𝑀 = ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 )
2		flt4lem5a.n	⊢ 𝑁 = ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 )
3		flt4lem5a.r	⊢ 𝑅 = ( ( ( √ ‘ ( 𝑀 + 𝑁 ) ) + ( √ ‘ ( 𝑀 − 𝑁 ) ) ) / 2 )
4		flt4lem5a.s	⊢ 𝑆 = ( ( ( √ ‘ ( 𝑀 + 𝑁 ) ) − ( √ ‘ ( 𝑀 − 𝑁 ) ) ) / 2 )
5		flt4lem5a.a	⊢ ( 𝜑 → 𝐴 ∈ ℕ )
6		flt4lem5a.b	⊢ ( 𝜑 → 𝐵 ∈ ℕ )
7		flt4lem5a.c	⊢ ( 𝜑 → 𝐶 ∈ ℕ )
8		flt4lem5a.1	⊢ ( 𝜑 → ¬ 2 ∥ 𝐴 )
9		flt4lem5a.2	⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) = 1 )
10		flt4lem5a.3	⊢ ( 𝜑 → ( ( 𝐴 ↑ 4 ) + ( 𝐵 ↑ 4 ) ) = ( 𝐶 ↑ 2 ) )
11	5	nnsqcld	⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℕ )
12	6	nnsqcld	⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℕ )
13		2prm	⊢ 2 ∈ ℙ
14	5	nnzd	⊢ ( 𝜑 → 𝐴 ∈ ℤ )
15		prmdvdssq	⊢ ( ( 2 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( 2 ∥ 𝐴 ↔ 2 ∥ ( 𝐴 ↑ 2 ) ) )
16	13 14 15	sylancr	⊢ ( 𝜑 → ( 2 ∥ 𝐴 ↔ 2 ∥ ( 𝐴 ↑ 2 ) ) )
17	8 16	mtbid	⊢ ( 𝜑 → ¬ 2 ∥ ( 𝐴 ↑ 2 ) )
18		2nn	⊢ 2 ∈ ℕ
19	18	a1i	⊢ ( 𝜑 → 2 ∈ ℕ )
20		rppwr	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 2 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) = 1 → ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) = 1 ) )
21	5 6 19 20	syl3anc	⊢ ( 𝜑 → ( ( 𝐴 gcd 𝐵 ) = 1 → ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) = 1 ) )
22	9 21	mpd	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) = 1 )
23	5	nncnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
24	23	exp4sqsq	⊢ ( 𝜑 → ( 𝐴 ↑ 4 ) = ( ( 𝐴 ↑ 2 ) ↑ 2 ) )
25	6	nncnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
26	25	exp4sqsq	⊢ ( 𝜑 → ( 𝐵 ↑ 4 ) = ( ( 𝐵 ↑ 2 ) ↑ 2 ) )
27	24 26	oveq12d	⊢ ( 𝜑 → ( ( 𝐴 ↑ 4 ) + ( 𝐵 ↑ 4 ) ) = ( ( ( 𝐴 ↑ 2 ) ↑ 2 ) + ( ( 𝐵 ↑ 2 ) ↑ 2 ) ) )
28	27 10	eqtr3d	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) ↑ 2 ) + ( ( 𝐵 ↑ 2 ) ↑ 2 ) ) = ( 𝐶 ↑ 2 ) )
29	11 12 7 17 22 28	flt4lem1	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) ∈ ℕ ∧ ( 𝐵 ↑ 2 ) ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( ( 𝐴 ↑ 2 ) ↑ 2 ) + ( ( 𝐵 ↑ 2 ) ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) = 1 ∧ ¬ 2 ∥ ( 𝐴 ↑ 2 ) ) ) )
30	2	pythagtriplem13	⊢ ( ( ( ( 𝐴 ↑ 2 ) ∈ ℕ ∧ ( 𝐵 ↑ 2 ) ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( ( 𝐴 ↑ 2 ) ↑ 2 ) + ( ( 𝐵 ↑ 2 ) ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) = 1 ∧ ¬ 2 ∥ ( 𝐴 ↑ 2 ) ) ) → 𝑁 ∈ ℕ )
31	29 30	syl	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
32	1	pythagtriplem11	⊢ ( ( ( ( 𝐴 ↑ 2 ) ∈ ℕ ∧ ( 𝐵 ↑ 2 ) ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( ( 𝐴 ↑ 2 ) ↑ 2 ) + ( ( 𝐵 ↑ 2 ) ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) = 1 ∧ ¬ 2 ∥ ( 𝐴 ↑ 2 ) ) ) → 𝑀 ∈ ℕ )
33	29 32	syl	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
34	31	nnzd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
35	14 34	gcdcomd	⊢ ( 𝜑 → ( 𝐴 gcd 𝑁 ) = ( 𝑁 gcd 𝐴 ) )
36	33	nnzd	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
37	34 36	gcdcomd	⊢ ( 𝜑 → ( 𝑁 gcd 𝑀 ) = ( 𝑀 gcd 𝑁 ) )
38	1 2	flt4lem5	⊢ ( ( ( ( 𝐴 ↑ 2 ) ∈ ℕ ∧ ( 𝐵 ↑ 2 ) ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( ( 𝐴 ↑ 2 ) ↑ 2 ) + ( ( 𝐵 ↑ 2 ) ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) = 1 ∧ ¬ 2 ∥ ( 𝐴 ↑ 2 ) ) ) → ( 𝑀 gcd 𝑁 ) = 1 )
39	29 38	syl	⊢ ( 𝜑 → ( 𝑀 gcd 𝑁 ) = 1 )
40	37 39	eqtrd	⊢ ( 𝜑 → ( 𝑁 gcd 𝑀 ) = 1 )
41	31	nnsqcld	⊢ ( 𝜑 → ( 𝑁 ↑ 2 ) ∈ ℕ )
42	41	nncnd	⊢ ( 𝜑 → ( 𝑁 ↑ 2 ) ∈ ℂ )
43	11	nncnd	⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℂ )
44	42 43	addcomd	⊢ ( 𝜑 → ( ( 𝑁 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) + ( 𝑁 ↑ 2 ) ) )
45	1 2 3 4 5 6 7 8 9 10	flt4lem5a	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) + ( 𝑁 ↑ 2 ) ) = ( 𝑀 ↑ 2 ) )
46	44 45	eqtrd	⊢ ( 𝜑 → ( ( 𝑁 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) = ( 𝑀 ↑ 2 ) )
47	31 5 33 40 46	fltabcoprm	⊢ ( 𝜑 → ( 𝑁 gcd 𝐴 ) = 1 )
48	35 47	eqtrd	⊢ ( 𝜑 → ( 𝐴 gcd 𝑁 ) = 1 )
49	5 31 33 8 48 45	flt4lem1	⊢ ( 𝜑 → ( ( 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝑁 ↑ 2 ) ) = ( 𝑀 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝑁 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) )
50	3 4	flt4lem5	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝑁 ↑ 2 ) ) = ( 𝑀 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝑁 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 𝑅 gcd 𝑆 ) = 1 )
51	49 50	syl	⊢ ( 𝜑 → ( 𝑅 gcd 𝑆 ) = 1 )
52	3	pythagtriplem11	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝑁 ↑ 2 ) ) = ( 𝑀 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝑁 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝑅 ∈ ℕ )
53	49 52	syl	⊢ ( 𝜑 → 𝑅 ∈ ℕ )
54	4	pythagtriplem13	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝑁 ↑ 2 ) ) = ( 𝑀 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝑁 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝑆 ∈ ℕ )
55	49 54	syl	⊢ ( 𝜑 → 𝑆 ∈ ℕ )
56	1 2 3 4 5 6 7 8 9 10	flt4lem5d	⊢ ( 𝜑 → 𝑀 = ( ( 𝑅 ↑ 2 ) + ( 𝑆 ↑ 2 ) ) )
57	33 53 55 56 51	flt4lem5elem	⊢ ( 𝜑 → ( ( 𝑅 gcd 𝑀 ) = 1 ∧ ( 𝑆 gcd 𝑀 ) = 1 ) )
58		3anass	⊢ ( ( ( 𝑅 gcd 𝑆 ) = 1 ∧ ( 𝑅 gcd 𝑀 ) = 1 ∧ ( 𝑆 gcd 𝑀 ) = 1 ) ↔ ( ( 𝑅 gcd 𝑆 ) = 1 ∧ ( ( 𝑅 gcd 𝑀 ) = 1 ∧ ( 𝑆 gcd 𝑀 ) = 1 ) ) )
59	51 57 58	sylanbrc	⊢ ( 𝜑 → ( ( 𝑅 gcd 𝑆 ) = 1 ∧ ( 𝑅 gcd 𝑀 ) = 1 ∧ ( 𝑆 gcd 𝑀 ) = 1 ) )
60	53 55 33	3jca	⊢ ( 𝜑 → ( 𝑅 ∈ ℕ ∧ 𝑆 ∈ ℕ ∧ 𝑀 ∈ ℕ ) )
61		2cnd	⊢ ( 𝜑 → 2 ∈ ℂ )
62	61	sqcld	⊢ ( 𝜑 → ( 2 ↑ 2 ) ∈ ℂ )
63	53 55	nnmulcld	⊢ ( 𝜑 → ( 𝑅 · 𝑆 ) ∈ ℕ )
64	33 63	nnmulcld	⊢ ( 𝜑 → ( 𝑀 · ( 𝑅 · 𝑆 ) ) ∈ ℕ )
65	64	nncnd	⊢ ( 𝜑 → ( 𝑀 · ( 𝑅 · 𝑆 ) ) ∈ ℂ )
66		2ne0	⊢ 2 ≠ 0
67	66	a1i	⊢ ( 𝜑 → 2 ≠ 0 )
68		2z	⊢ 2 ∈ ℤ
69	68	a1i	⊢ ( 𝜑 → 2 ∈ ℤ )
70	61 67 69	expne0d	⊢ ( 𝜑 → ( 2 ↑ 2 ) ≠ 0 )
71		2cn	⊢ 2 ∈ ℂ
72	71	sqvali	⊢ ( 2 ↑ 2 ) = ( 2 · 2 )
73	72	oveq1i	⊢ ( ( 2 ↑ 2 ) · ( 𝑀 · ( 𝑅 · 𝑆 ) ) ) = ( ( 2 · 2 ) · ( 𝑀 · ( 𝑅 · 𝑆 ) ) )
74	33	nncnd	⊢ ( 𝜑 → 𝑀 ∈ ℂ )
75	63	nncnd	⊢ ( 𝜑 → ( 𝑅 · 𝑆 ) ∈ ℂ )
76	61 61 74 75	mul4d	⊢ ( 𝜑 → ( ( 2 · 2 ) · ( 𝑀 · ( 𝑅 · 𝑆 ) ) ) = ( ( 2 · 𝑀 ) · ( 2 · ( 𝑅 · 𝑆 ) ) ) )
77	1 2 3 4 5 6 7 8 9 10	flt4lem5c	⊢ ( 𝜑 → 𝑁 = ( 2 · ( 𝑅 · 𝑆 ) ) )
78	77	oveq2d	⊢ ( 𝜑 → ( ( 2 · 𝑀 ) · 𝑁 ) = ( ( 2 · 𝑀 ) · ( 2 · ( 𝑅 · 𝑆 ) ) ) )
79	31	nncnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
80	61 74 79	mulassd	⊢ ( 𝜑 → ( ( 2 · 𝑀 ) · 𝑁 ) = ( 2 · ( 𝑀 · 𝑁 ) ) )
81	78 80	eqtr3d	⊢ ( 𝜑 → ( ( 2 · 𝑀 ) · ( 2 · ( 𝑅 · 𝑆 ) ) ) = ( 2 · ( 𝑀 · 𝑁 ) ) )
82	1 2 3 4 5 6 7 8 9 10	flt4lem5b	⊢ ( 𝜑 → ( 2 · ( 𝑀 · 𝑁 ) ) = ( 𝐵 ↑ 2 ) )
83	76 81 82	3eqtrd	⊢ ( 𝜑 → ( ( 2 · 2 ) · ( 𝑀 · ( 𝑅 · 𝑆 ) ) ) = ( 𝐵 ↑ 2 ) )
84	73 83	eqtrid	⊢ ( 𝜑 → ( ( 2 ↑ 2 ) · ( 𝑀 · ( 𝑅 · 𝑆 ) ) ) = ( 𝐵 ↑ 2 ) )
85	62 65 70 84	mvllmuld	⊢ ( 𝜑 → ( 𝑀 · ( 𝑅 · 𝑆 ) ) = ( ( 𝐵 ↑ 2 ) / ( 2 ↑ 2 ) ) )
86	25 61 67	sqdivd	⊢ ( 𝜑 → ( ( 𝐵 / 2 ) ↑ 2 ) = ( ( 𝐵 ↑ 2 ) / ( 2 ↑ 2 ) ) )
87	85 86	eqtr4d	⊢ ( 𝜑 → ( 𝑀 · ( 𝑅 · 𝑆 ) ) = ( ( 𝐵 / 2 ) ↑ 2 ) )
88	64	nnzd	⊢ ( 𝜑 → ( 𝑀 · ( 𝑅 · 𝑆 ) ) ∈ ℤ )
89	87 88	eqeltrrd	⊢ ( 𝜑 → ( ( 𝐵 / 2 ) ↑ 2 ) ∈ ℤ )
90	6	nnzd	⊢ ( 𝜑 → 𝐵 ∈ ℤ )
91		znq	⊢ ( ( 𝐵 ∈ ℤ ∧ 2 ∈ ℕ ) → ( 𝐵 / 2 ) ∈ ℚ )
92	90 18 91	sylancl	⊢ ( 𝜑 → ( 𝐵 / 2 ) ∈ ℚ )
93	6	nngt0d	⊢ ( 𝜑 → 0 < 𝐵 )
94	6	nnred	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
95		halfpos2	⊢ ( 𝐵 ∈ ℝ → ( 0 < 𝐵 ↔ 0 < ( 𝐵 / 2 ) ) )
96	94 95	syl	⊢ ( 𝜑 → ( 0 < 𝐵 ↔ 0 < ( 𝐵 / 2 ) ) )
97	93 96	mpbid	⊢ ( 𝜑 → 0 < ( 𝐵 / 2 ) )
98	89 92 97	posqsqznn	⊢ ( 𝜑 → ( 𝐵 / 2 ) ∈ ℕ )
99	87 98	jca	⊢ ( 𝜑 → ( ( 𝑀 · ( 𝑅 · 𝑆 ) ) = ( ( 𝐵 / 2 ) ↑ 2 ) ∧ ( 𝐵 / 2 ) ∈ ℕ ) )
100	59 60 99	3jca	⊢ ( 𝜑 → ( ( ( 𝑅 gcd 𝑆 ) = 1 ∧ ( 𝑅 gcd 𝑀 ) = 1 ∧ ( 𝑆 gcd 𝑀 ) = 1 ) ∧ ( 𝑅 ∈ ℕ ∧ 𝑆 ∈ ℕ ∧ 𝑀 ∈ ℕ ) ∧ ( ( 𝑀 · ( 𝑅 · 𝑆 ) ) = ( ( 𝐵 / 2 ) ↑ 2 ) ∧ ( 𝐵 / 2 ) ∈ ℕ ) ) )