Metamath Proof Explorer

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 ) ∈ ℕ ) ) )