Theorem flt4lem5e

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