Proof of Theorem flt4lem5f
Step | Hyp | Ref
| Expression |
1 | | flt4lem5a.m |
. . 3
⊢ 𝑀 = (((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2) |
2 | | flt4lem5a.n |
. . 3
⊢ 𝑁 = (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2) |
3 | | flt4lem5a.r |
. . 3
⊢ 𝑅 = (((√‘(𝑀 + 𝑁)) + (√‘(𝑀 − 𝑁))) / 2) |
4 | | flt4lem5a.s |
. . 3
⊢ 𝑆 = (((√‘(𝑀 + 𝑁)) − (√‘(𝑀 − 𝑁))) / 2) |
5 | | flt4lem5a.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ ℕ) |
6 | | flt4lem5a.b |
. . 3
⊢ (𝜑 → 𝐵 ∈ ℕ) |
7 | | flt4lem5a.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ ℕ) |
8 | | flt4lem5a.1 |
. . 3
⊢ (𝜑 → ¬ 2 ∥ 𝐴) |
9 | | flt4lem5a.2 |
. . 3
⊢ (𝜑 → (𝐴 gcd 𝐶) = 1) |
10 | | flt4lem5a.3 |
. . 3
⊢ (𝜑 → ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2)) |
11 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | flt4lem5d 40242 |
. 2
⊢ (𝜑 → 𝑀 = ((𝑅↑2) + (𝑆↑2))) |
12 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | flt4lem5e 40243 |
. . . . . 6
⊢ (𝜑 → (((𝑅 gcd 𝑆) = 1 ∧ (𝑅 gcd 𝑀) = 1 ∧ (𝑆 gcd 𝑀) = 1) ∧ (𝑅 ∈ ℕ ∧ 𝑆 ∈ ℕ ∧ 𝑀 ∈ ℕ) ∧ ((𝑀 · (𝑅 · 𝑆)) = ((𝐵 / 2)↑2) ∧ (𝐵 / 2) ∈ ℕ))) |
13 | 12 | simp2d 1145 |
. . . . 5
⊢ (𝜑 → (𝑅 ∈ ℕ ∧ 𝑆 ∈ ℕ ∧ 𝑀 ∈ ℕ)) |
14 | 13 | simp3d 1146 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℕ) |
15 | 13 | simp1d 1144 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ ℕ) |
16 | 13 | simp2d 1145 |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ ℕ) |
17 | 15, 16 | nnmulcld 11912 |
. . . 4
⊢ (𝜑 → (𝑅 · 𝑆) ∈ ℕ) |
18 | 12 | simp3d 1146 |
. . . . 5
⊢ (𝜑 → ((𝑀 · (𝑅 · 𝑆)) = ((𝐵 / 2)↑2) ∧ (𝐵 / 2) ∈ ℕ)) |
19 | 18 | simprd 499 |
. . . 4
⊢ (𝜑 → (𝐵 / 2) ∈ ℕ) |
20 | 14 | nnzd 12310 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℤ) |
21 | 15 | nnzd 12310 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ ℤ) |
22 | 20, 21 | gcdcomd 16105 |
. . . . . 6
⊢ (𝜑 → (𝑀 gcd 𝑅) = (𝑅 gcd 𝑀)) |
23 | 12 | simp1d 1144 |
. . . . . . 7
⊢ (𝜑 → ((𝑅 gcd 𝑆) = 1 ∧ (𝑅 gcd 𝑀) = 1 ∧ (𝑆 gcd 𝑀) = 1)) |
24 | 23 | simp2d 1145 |
. . . . . 6
⊢ (𝜑 → (𝑅 gcd 𝑀) = 1) |
25 | 22, 24 | eqtrd 2779 |
. . . . 5
⊢ (𝜑 → (𝑀 gcd 𝑅) = 1) |
26 | 16 | nnzd 12310 |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈ ℤ) |
27 | 20, 26 | gcdcomd 16105 |
. . . . . 6
⊢ (𝜑 → (𝑀 gcd 𝑆) = (𝑆 gcd 𝑀)) |
28 | 23 | simp3d 1146 |
. . . . . 6
⊢ (𝜑 → (𝑆 gcd 𝑀) = 1) |
29 | 27, 28 | eqtrd 2779 |
. . . . 5
⊢ (𝜑 → (𝑀 gcd 𝑆) = 1) |
30 | | rpmul 16248 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝑆 ∈ ℤ) → (((𝑀 gcd 𝑅) = 1 ∧ (𝑀 gcd 𝑆) = 1) → (𝑀 gcd (𝑅 · 𝑆)) = 1)) |
31 | 20, 21, 26, 30 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → (((𝑀 gcd 𝑅) = 1 ∧ (𝑀 gcd 𝑆) = 1) → (𝑀 gcd (𝑅 · 𝑆)) = 1)) |
32 | 25, 29, 31 | mp2and 699 |
. . . 4
⊢ (𝜑 → (𝑀 gcd (𝑅 · 𝑆)) = 1) |
33 | 18 | simpld 498 |
. . . 4
⊢ (𝜑 → (𝑀 · (𝑅 · 𝑆)) = ((𝐵 / 2)↑2)) |
34 | 14, 17, 19, 32, 33 | flt4lem4 40236 |
. . 3
⊢ (𝜑 → (𝑀 = ((𝑀 gcd (𝐵 / 2))↑2) ∧ (𝑅 · 𝑆) = (((𝑅 · 𝑆) gcd (𝐵 / 2))↑2))) |
35 | 34 | simpld 498 |
. 2
⊢ (𝜑 → 𝑀 = ((𝑀 gcd (𝐵 / 2))↑2)) |
36 | 14, 16 | nnmulcld 11912 |
. . . . . . 7
⊢ (𝜑 → (𝑀 · 𝑆) ∈ ℕ) |
37 | 36 | nnzd 12310 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 · 𝑆) ∈ ℤ) |
38 | 37, 21 | gcdcomd 16105 |
. . . . . . . 8
⊢ (𝜑 → ((𝑀 · 𝑆) gcd 𝑅) = (𝑅 gcd (𝑀 · 𝑆))) |
39 | 23 | simp1d 1144 |
. . . . . . . . 9
⊢ (𝜑 → (𝑅 gcd 𝑆) = 1) |
40 | | rpmul 16248 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑆 ∈ ℤ) → (((𝑅 gcd 𝑀) = 1 ∧ (𝑅 gcd 𝑆) = 1) → (𝑅 gcd (𝑀 · 𝑆)) = 1)) |
41 | 21, 20, 26, 40 | syl3anc 1373 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑅 gcd 𝑀) = 1 ∧ (𝑅 gcd 𝑆) = 1) → (𝑅 gcd (𝑀 · 𝑆)) = 1)) |
42 | 24, 39, 41 | mp2and 699 |
. . . . . . . 8
⊢ (𝜑 → (𝑅 gcd (𝑀 · 𝑆)) = 1) |
43 | 38, 42 | eqtrd 2779 |
. . . . . . 7
⊢ (𝜑 → ((𝑀 · 𝑆) gcd 𝑅) = 1) |
44 | 14 | nncnd 11875 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℂ) |
45 | 16 | nncnd 11875 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ ℂ) |
46 | 15 | nncnd 11875 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ ℂ) |
47 | 44, 45, 46 | mul32d 11071 |
. . . . . . . 8
⊢ (𝜑 → ((𝑀 · 𝑆) · 𝑅) = ((𝑀 · 𝑅) · 𝑆)) |
48 | 44, 46, 45 | mulassd 10885 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑀 · 𝑅) · 𝑆) = (𝑀 · (𝑅 · 𝑆))) |
49 | 48, 33 | eqtrd 2779 |
. . . . . . . 8
⊢ (𝜑 → ((𝑀 · 𝑅) · 𝑆) = ((𝐵 / 2)↑2)) |
50 | 47, 49 | eqtrd 2779 |
. . . . . . 7
⊢ (𝜑 → ((𝑀 · 𝑆) · 𝑅) = ((𝐵 / 2)↑2)) |
51 | 36, 15, 19, 43, 50 | flt4lem4 40236 |
. . . . . 6
⊢ (𝜑 → ((𝑀 · 𝑆) = (((𝑀 · 𝑆) gcd (𝐵 / 2))↑2) ∧ 𝑅 = ((𝑅 gcd (𝐵 / 2))↑2))) |
52 | 51 | simprd 499 |
. . . . 5
⊢ (𝜑 → 𝑅 = ((𝑅 gcd (𝐵 / 2))↑2)) |
53 | 52 | oveq1d 7249 |
. . . 4
⊢ (𝜑 → (𝑅↑2) = (((𝑅 gcd (𝐵 / 2))↑2)↑2)) |
54 | | gcdnncl 16098 |
. . . . . . 7
⊢ ((𝑅 ∈ ℕ ∧ (𝐵 / 2) ∈ ℕ) →
(𝑅 gcd (𝐵 / 2)) ∈ ℕ) |
55 | 15, 19, 54 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → (𝑅 gcd (𝐵 / 2)) ∈ ℕ) |
56 | 55 | nncnd 11875 |
. . . . 5
⊢ (𝜑 → (𝑅 gcd (𝐵 / 2)) ∈ ℂ) |
57 | 56 | flt4lem 40232 |
. . . 4
⊢ (𝜑 → ((𝑅 gcd (𝐵 / 2))↑4) = (((𝑅 gcd (𝐵 / 2))↑2)↑2)) |
58 | 53, 57 | eqtr4d 2782 |
. . 3
⊢ (𝜑 → (𝑅↑2) = ((𝑅 gcd (𝐵 / 2))↑4)) |
59 | 14, 15 | nnmulcld 11912 |
. . . . . . 7
⊢ (𝜑 → (𝑀 · 𝑅) ∈ ℕ) |
60 | 59 | nnzd 12310 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 · 𝑅) ∈ ℤ) |
61 | 60, 26 | gcdcomd 16105 |
. . . . . . . 8
⊢ (𝜑 → ((𝑀 · 𝑅) gcd 𝑆) = (𝑆 gcd (𝑀 · 𝑅))) |
62 | 26, 21 | gcdcomd 16105 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑆 gcd 𝑅) = (𝑅 gcd 𝑆)) |
63 | 62, 39 | eqtrd 2779 |
. . . . . . . . 9
⊢ (𝜑 → (𝑆 gcd 𝑅) = 1) |
64 | | rpmul 16248 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑅 ∈ ℤ) → (((𝑆 gcd 𝑀) = 1 ∧ (𝑆 gcd 𝑅) = 1) → (𝑆 gcd (𝑀 · 𝑅)) = 1)) |
65 | 26, 20, 21, 64 | syl3anc 1373 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑆 gcd 𝑀) = 1 ∧ (𝑆 gcd 𝑅) = 1) → (𝑆 gcd (𝑀 · 𝑅)) = 1)) |
66 | 28, 63, 65 | mp2and 699 |
. . . . . . . 8
⊢ (𝜑 → (𝑆 gcd (𝑀 · 𝑅)) = 1) |
67 | 61, 66 | eqtrd 2779 |
. . . . . . 7
⊢ (𝜑 → ((𝑀 · 𝑅) gcd 𝑆) = 1) |
68 | 59, 16, 19, 67, 49 | flt4lem4 40236 |
. . . . . 6
⊢ (𝜑 → ((𝑀 · 𝑅) = (((𝑀 · 𝑅) gcd (𝐵 / 2))↑2) ∧ 𝑆 = ((𝑆 gcd (𝐵 / 2))↑2))) |
69 | 68 | simprd 499 |
. . . . 5
⊢ (𝜑 → 𝑆 = ((𝑆 gcd (𝐵 / 2))↑2)) |
70 | 69 | oveq1d 7249 |
. . . 4
⊢ (𝜑 → (𝑆↑2) = (((𝑆 gcd (𝐵 / 2))↑2)↑2)) |
71 | | gcdnncl 16098 |
. . . . . . 7
⊢ ((𝑆 ∈ ℕ ∧ (𝐵 / 2) ∈ ℕ) →
(𝑆 gcd (𝐵 / 2)) ∈ ℕ) |
72 | 16, 19, 71 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → (𝑆 gcd (𝐵 / 2)) ∈ ℕ) |
73 | 72 | nncnd 11875 |
. . . . 5
⊢ (𝜑 → (𝑆 gcd (𝐵 / 2)) ∈ ℂ) |
74 | 73 | flt4lem 40232 |
. . . 4
⊢ (𝜑 → ((𝑆 gcd (𝐵 / 2))↑4) = (((𝑆 gcd (𝐵 / 2))↑2)↑2)) |
75 | 70, 74 | eqtr4d 2782 |
. . 3
⊢ (𝜑 → (𝑆↑2) = ((𝑆 gcd (𝐵 / 2))↑4)) |
76 | 58, 75 | oveq12d 7252 |
. 2
⊢ (𝜑 → ((𝑅↑2) + (𝑆↑2)) = (((𝑅 gcd (𝐵 / 2))↑4) + ((𝑆 gcd (𝐵 / 2))↑4))) |
77 | 11, 35, 76 | 3eqtr3d 2787 |
1
⊢ (𝜑 → ((𝑀 gcd (𝐵 / 2))↑2) = (((𝑅 gcd (𝐵 / 2))↑4) + ((𝑆 gcd (𝐵 / 2))↑4))) |