Metamath Proof Explorer

Theorem flt4lem5e

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

Ref Expression
Hypotheses flt4lem5a.m ⊢ M = C + B 2 + C − B 2 2
flt4lem5a.n ⊢ N = C + B 2 − C − B 2 2
flt4lem5a.r ⊢ R = M + N + M − N 2
flt4lem5a.s ⊢ S = M + N − M − N 2
flt4lem5a.a ⊢ φ → A ∈ ℕ
flt4lem5a.b ⊢ φ → B ∈ ℕ
flt4lem5a.c ⊢ φ → C ∈ ℕ
flt4lem5a.1 ⊢ φ → ¬ 2 ∥ A
flt4lem5a.2 ⊢ φ → A gcd B = 1
flt4lem5a.3 ⊢ φ → A 4 + B 4 = C 2
Assertion flt4lem5e ⊢ φ → R gcd S = 1 ∧ R gcd M = 1 ∧ S gcd M = 1 ∧ R ∈ ℕ ∧ S ∈ ℕ ∧ M ∈ ℕ ∧ M ⁢ R ⁢ S = B 2 2 ∧ B 2 ∈ ℕ

Proof

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