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		rplpwr	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐶 ∈ ℕ ∧ 2 ∈ ℕ ) → ( ( 𝐴 gcd 𝐶 ) = 1 → ( ( 𝐴 ↑ 2 ) gcd 𝐶 ) = 1 ) )
21	5 7 19 20	syl3anc	⊢ ( 𝜑 → ( ( 𝐴 gcd 𝐶 ) = 1 → ( ( 𝐴 ↑ 2 ) gcd 𝐶 ) = 1 ) )
22	9 21	mpd	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) gcd 𝐶 ) = 1 )
23	5	nncnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
24	23	flt4lem	⊢ ( 𝜑 → ( 𝐴 ↑ 4 ) = ( ( 𝐴 ↑ 2 ) ↑ 2 ) )
25	6	nncnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
26	25	flt4lem	⊢ ( 𝜑 → ( 𝐵 ↑ 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	1 2 3 4 5 6 7 8 9 10	flt4lem5a	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) + ( 𝑁 ↑ 2 ) ) = ( 𝑀 ↑ 2 ) )
35	31	nnzd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
36	14 35	gcdcomd	⊢ ( 𝜑 → ( 𝐴 gcd 𝑁 ) = ( 𝑁 gcd 𝐴 ) )
37	33	nnzd	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
38	35 37	gcdcomd	⊢ ( 𝜑 → ( 𝑁 gcd 𝑀 ) = ( 𝑀 gcd 𝑁 ) )
39	1 2	flt4lem5	⊢ ( ( ( ( 𝐴 ↑ 2 ) ∈ ℕ ∧ ( 𝐵 ↑ 2 ) ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( ( 𝐴 ↑ 2 ) ↑ 2 ) + ( ( 𝐵 ↑ 2 ) ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) = 1 ∧ ¬ 2 ∥ ( 𝐴 ↑ 2 ) ) ) → ( 𝑀 gcd 𝑁 ) = 1 )
40	29 39	syl	⊢ ( 𝜑 → ( 𝑀 gcd 𝑁 ) = 1 )
41	38 40	eqtrd	⊢ ( 𝜑 → ( 𝑁 gcd 𝑀 ) = 1 )
42	31	nnsqcld	⊢ ( 𝜑 → ( 𝑁 ↑ 2 ) ∈ ℕ )
43	42	nncnd	⊢ ( 𝜑 → ( 𝑁 ↑ 2 ) ∈ ℂ )
44	11	nncnd	⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℂ )
45	43 44	addcomd	⊢ ( 𝜑 → ( ( 𝑁 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) + ( 𝑁 ↑ 2 ) ) )
46	45 34	eqtrd	⊢ ( 𝜑 → ( ( 𝑁 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) = ( 𝑀 ↑ 2 ) )
47	31 5 33 41 46	fltabcoprm	⊢ ( 𝜑 → ( 𝑁 gcd 𝐴 ) = 1 )
48	36 47	eqtrd	⊢ ( 𝜑 → ( 𝐴 gcd 𝑁 ) = 1 )
49	3 4	flt4lem5	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝑁 ↑ 2 ) ) = ( 𝑀 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝑁 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → ( 𝑅 gcd 𝑆 ) = 1 )
50	5 31 33 34 48 8 49	syl312anc	⊢ ( 𝜑 → ( 𝑅 gcd 𝑆 ) = 1 )
51	3	pythagtriplem11	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝑁 ↑ 2 ) ) = ( 𝑀 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝑁 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝑅 ∈ ℕ )
52	5 31 33 34 48 8 51	syl312anc	⊢ ( 𝜑 → 𝑅 ∈ ℕ )
53	4	pythagtriplem13	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝑁 ↑ 2 ) ) = ( 𝑀 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝑁 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝑆 ∈ ℕ )
54	5 31 33 34 48 8 53	syl312anc	⊢ ( 𝜑 → 𝑆 ∈ ℕ )
55	1 2 3 4 5 6 7 8 9 10	flt4lem5d	⊢ ( 𝜑 → 𝑀 = ( ( 𝑅 ↑ 2 ) + ( 𝑆 ↑ 2 ) ) )
56	33 52 54 55 50	flt4lem5elem	⊢ ( 𝜑 → ( ( 𝑅 gcd 𝑀 ) = 1 ∧ ( 𝑆 gcd 𝑀 ) = 1 ) )
57		3anass	⊢ ( ( ( 𝑅 gcd 𝑆 ) = 1 ∧ ( 𝑅 gcd 𝑀 ) = 1 ∧ ( 𝑆 gcd 𝑀 ) = 1 ) ↔ ( ( 𝑅 gcd 𝑆 ) = 1 ∧ ( ( 𝑅 gcd 𝑀 ) = 1 ∧ ( 𝑆 gcd 𝑀 ) = 1 ) ) )
58	50 56 57	sylanbrc	⊢ ( 𝜑 → ( ( 𝑅 gcd 𝑆 ) = 1 ∧ ( 𝑅 gcd 𝑀 ) = 1 ∧ ( 𝑆 gcd 𝑀 ) = 1 ) )
59	52 54 33	3jca	⊢ ( 𝜑 → ( 𝑅 ∈ ℕ ∧ 𝑆 ∈ ℕ ∧ 𝑀 ∈ ℕ ) )
60		sq2	⊢ ( 2 ↑ 2 ) = 4
61		4cn	⊢ 4 ∈ ℂ
62	60 61	eqeltri	⊢ ( 2 ↑ 2 ) ∈ ℂ
63	62	a1i	⊢ ( 𝜑 → ( 2 ↑ 2 ) ∈ ℂ )
64	52 54	nnmulcld	⊢ ( 𝜑 → ( 𝑅 · 𝑆 ) ∈ ℕ )
65	33 64	nnmulcld	⊢ ( 𝜑 → ( 𝑀 · ( 𝑅 · 𝑆 ) ) ∈ ℕ )
66	65	nncnd	⊢ ( 𝜑 → ( 𝑀 · ( 𝑅 · 𝑆 ) ) ∈ ℂ )
67		4ne0	⊢ 4 ≠ 0
68	60 67	eqnetri	⊢ ( 2 ↑ 2 ) ≠ 0
69	68	a1i	⊢ ( 𝜑 → ( 2 ↑ 2 ) ≠ 0 )
70		2cn	⊢ 2 ∈ ℂ
71	70	sqvali	⊢ ( 2 ↑ 2 ) = ( 2 · 2 )
72	71	oveq1i	⊢ ( ( 2 ↑ 2 ) · ( 𝑀 · ( 𝑅 · 𝑆 ) ) ) = ( ( 2 · 2 ) · ( 𝑀 · ( 𝑅 · 𝑆 ) ) )
73		2cnd	⊢ ( 𝜑 → 2 ∈ ℂ )
74	33	nncnd	⊢ ( 𝜑 → 𝑀 ∈ ℂ )
75	64	nncnd	⊢ ( 𝜑 → ( 𝑅 · 𝑆 ) ∈ ℂ )
76	73 73 74 75	mul4d	⊢ ( 𝜑 → ( ( 2 · 2 ) · ( 𝑀 · ( 𝑅 · 𝑆 ) ) ) = ( ( 2 · 𝑀 ) · ( 2 · ( 𝑅 · 𝑆 ) ) ) )
77	1 2 3 4 5 6 7 8 9 10	flt4lem5c	⊢ ( 𝜑 → 𝑁 = ( 2 · ( 𝑅 · 𝑆 ) ) )
78	77 31	eqeltrrd	⊢ ( 𝜑 → ( 2 · ( 𝑅 · 𝑆 ) ) ∈ ℕ )
79	78	nncnd	⊢ ( 𝜑 → ( 2 · ( 𝑅 · 𝑆 ) ) ∈ ℂ )
80	73 74 79	mulassd	⊢ ( 𝜑 → ( ( 2 · 𝑀 ) · ( 2 · ( 𝑅 · 𝑆 ) ) ) = ( 2 · ( 𝑀 · ( 2 · ( 𝑅 · 𝑆 ) ) ) ) )
81	77	eqcomd	⊢ ( 𝜑 → ( 2 · ( 𝑅 · 𝑆 ) ) = 𝑁 )
82	81	oveq2d	⊢ ( 𝜑 → ( 𝑀 · ( 2 · ( 𝑅 · 𝑆 ) ) ) = ( 𝑀 · 𝑁 ) )
83	82	oveq2d	⊢ ( 𝜑 → ( 2 · ( 𝑀 · ( 2 · ( 𝑅 · 𝑆 ) ) ) ) = ( 2 · ( 𝑀 · 𝑁 ) ) )
84	80 83	eqtrd	⊢ ( 𝜑 → ( ( 2 · 𝑀 ) · ( 2 · ( 𝑅 · 𝑆 ) ) ) = ( 2 · ( 𝑀 · 𝑁 ) ) )
85	1 2 3 4 5 6 7 8 9 10	flt4lem5b	⊢ ( 𝜑 → ( 2 · ( 𝑀 · 𝑁 ) ) = ( 𝐵 ↑ 2 ) )
86	76 84 85	3eqtrd	⊢ ( 𝜑 → ( ( 2 · 2 ) · ( 𝑀 · ( 𝑅 · 𝑆 ) ) ) = ( 𝐵 ↑ 2 ) )
87	72 86	eqtrid	⊢ ( 𝜑 → ( ( 2 ↑ 2 ) · ( 𝑀 · ( 𝑅 · 𝑆 ) ) ) = ( 𝐵 ↑ 2 ) )
88	63 66 69 87	mvllmuld	⊢ ( 𝜑 → ( 𝑀 · ( 𝑅 · 𝑆 ) ) = ( ( 𝐵 ↑ 2 ) / ( 2 ↑ 2 ) ) )
89		2ne0	⊢ 2 ≠ 0
90	89	a1i	⊢ ( 𝜑 → 2 ≠ 0 )
91	25 73 90	sqdivd	⊢ ( 𝜑 → ( ( 𝐵 / 2 ) ↑ 2 ) = ( ( 𝐵 ↑ 2 ) / ( 2 ↑ 2 ) ) )
92	88 91	eqtr4d	⊢ ( 𝜑 → ( 𝑀 · ( 𝑅 · 𝑆 ) ) = ( ( 𝐵 / 2 ) ↑ 2 ) )
93	65	nnzd	⊢ ( 𝜑 → ( 𝑀 · ( 𝑅 · 𝑆 ) ) ∈ ℤ )
94	92 93	eqeltrrd	⊢ ( 𝜑 → ( ( 𝐵 / 2 ) ↑ 2 ) ∈ ℤ )
95	6	nnzd	⊢ ( 𝜑 → 𝐵 ∈ ℤ )
96		znq	⊢ ( ( 𝐵 ∈ ℤ ∧ 2 ∈ ℕ ) → ( 𝐵 / 2 ) ∈ ℚ )
97	95 18 96	sylancl	⊢ ( 𝜑 → ( 𝐵 / 2 ) ∈ ℚ )
98	6	nngt0d	⊢ ( 𝜑 → 0 < 𝐵 )
99	6	nnred	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
100		halfpos2	⊢ ( 𝐵 ∈ ℝ → ( 0 < 𝐵 ↔ 0 < ( 𝐵 / 2 ) ) )
101	99 100	syl	⊢ ( 𝜑 → ( 0 < 𝐵 ↔ 0 < ( 𝐵 / 2 ) ) )
102	98 101	mpbid	⊢ ( 𝜑 → 0 < ( 𝐵 / 2 ) )
103	94 97 102	posqsqznn	⊢ ( 𝜑 → ( 𝐵 / 2 ) ∈ ℕ )
104	92 103	jca	⊢ ( 𝜑 → ( ( 𝑀 · ( 𝑅 · 𝑆 ) ) = ( ( 𝐵 / 2 ) ↑ 2 ) ∧ ( 𝐵 / 2 ) ∈ ℕ ) )
105	58 59 104	3jca	⊢ ( 𝜑 → ( ( ( 𝑅 gcd 𝑆 ) = 1 ∧ ( 𝑅 gcd 𝑀 ) = 1 ∧ ( 𝑆 gcd 𝑀 ) = 1 ) ∧ ( 𝑅 ∈ ℕ ∧ 𝑆 ∈ ℕ ∧ 𝑀 ∈ ℕ ) ∧ ( ( 𝑀 · ( 𝑅 · 𝑆 ) ) = ( ( 𝐵 / 2 ) ↑ 2 ) ∧ ( 𝐵 / 2 ) ∈ ℕ ) ) )