Proof of Theorem lcmineqlem22
Step | Hyp | Ref
| Expression |
1 | | 2re 11733 |
. . . . 5
⊢ 2 ∈
ℝ |
2 | 1 | a1i 11 |
. . . 4
⊢ (𝜑 → 2 ∈
ℝ) |
3 | | 2nn0 11936 |
. . . . . . 7
⊢ 2 ∈
ℕ0 |
4 | 3 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 2 ∈
ℕ0) |
5 | | lcmineqlem22.1 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℕ) |
6 | 5 | nnnn0d 11979 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
7 | 4, 6 | nn0mulcld 11984 |
. . . . 5
⊢ (𝜑 → (2 · 𝑁) ∈
ℕ0) |
8 | | 1nn0 11935 |
. . . . . 6
⊢ 1 ∈
ℕ0 |
9 | 8 | a1i 11 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℕ0) |
10 | 7, 9 | nn0addcld 11983 |
. . . 4
⊢ (𝜑 → ((2 · 𝑁) + 1) ∈
ℕ0) |
11 | 2, 10 | reexpcld 13562 |
. . 3
⊢ (𝜑 → (2↑((2 · 𝑁) + 1)) ∈
ℝ) |
12 | 7, 4 | nn0addcld 11983 |
. . . 4
⊢ (𝜑 → ((2 · 𝑁) + 2) ∈
ℕ0) |
13 | 2, 12 | reexpcld 13562 |
. . 3
⊢ (𝜑 → (2↑((2 · 𝑁) + 2)) ∈
ℝ) |
14 | | fz1ssnn 12972 |
. . . . . 6
⊢ (1...((2
· 𝑁) + 1)) ⊆
ℕ |
15 | | fzfi 13374 |
. . . . . 6
⊢ (1...((2
· 𝑁) + 1)) ∈
Fin |
16 | | lcmfnncl 16010 |
. . . . . 6
⊢
(((1...((2 · 𝑁) + 1)) ⊆ ℕ ∧ (1...((2
· 𝑁) + 1)) ∈
Fin) → (lcm‘(1...((2 · 𝑁) + 1))) ∈ ℕ) |
17 | 14, 15, 16 | mp2an 692 |
. . . . 5
⊢
(lcm‘(1...((2 · 𝑁) + 1))) ∈ ℕ |
18 | 17 | a1i 11 |
. . . 4
⊢ (𝜑 → (lcm‘(1...((2
· 𝑁) + 1))) ∈
ℕ) |
19 | 18 | nnred 11674 |
. . 3
⊢ (𝜑 → (lcm‘(1...((2
· 𝑁) + 1))) ∈
ℝ) |
20 | | 1red 10665 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℝ) |
21 | 5 | nnred 11674 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℝ) |
22 | 2, 21 | remulcld 10694 |
. . . . 5
⊢ (𝜑 → (2 · 𝑁) ∈
ℝ) |
23 | | 1lt2 11830 |
. . . . . . 7
⊢ 1 <
2 |
24 | 23 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 1 < 2) |
25 | 20, 2, 24 | ltled 10811 |
. . . . 5
⊢ (𝜑 → 1 ≤ 2) |
26 | 20, 2, 22, 25 | leadd2dd 11278 |
. . . 4
⊢ (𝜑 → ((2 · 𝑁) + 1) ≤ ((2 · 𝑁) + 2)) |
27 | | 2z 12038 |
. . . . . . . 8
⊢ 2 ∈
ℤ |
28 | 27 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 2 ∈
ℤ) |
29 | 5 | nnzd 12110 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℤ) |
30 | 28, 29 | zmulcld 12117 |
. . . . . 6
⊢ (𝜑 → (2 · 𝑁) ∈
ℤ) |
31 | 30 | peano2zd 12114 |
. . . . 5
⊢ (𝜑 → ((2 · 𝑁) + 1) ∈
ℤ) |
32 | 30, 28 | zaddcld 12115 |
. . . . 5
⊢ (𝜑 → ((2 · 𝑁) + 2) ∈
ℤ) |
33 | 2, 31, 32, 24 | leexp2d 13650 |
. . . 4
⊢ (𝜑 → (((2 · 𝑁) + 1) ≤ ((2 · 𝑁) + 2) ↔ (2↑((2
· 𝑁) + 1)) ≤
(2↑((2 · 𝑁) +
2)))) |
34 | 26, 33 | mpbid 235 |
. . 3
⊢ (𝜑 → (2↑((2 · 𝑁) + 1)) ≤ (2↑((2
· 𝑁) +
2))) |
35 | | lcmineqlem22.2 |
. . . 4
⊢ (𝜑 → 4 ≤ 𝑁) |
36 | 5, 35 | lcmineqlem21 39601 |
. . 3
⊢ (𝜑 → (2↑((2 · 𝑁) + 2)) ≤
(lcm‘(1...((2 · 𝑁) + 1)))) |
37 | 11, 13, 19, 34, 36 | letrd 10820 |
. 2
⊢ (𝜑 → (2↑((2 · 𝑁) + 1)) ≤
(lcm‘(1...((2 · 𝑁) + 1)))) |
38 | | fz1ssnn 12972 |
. . . . . 6
⊢ (1...((2
· 𝑁) + 2)) ⊆
ℕ |
39 | | fzfi 13374 |
. . . . . 6
⊢ (1...((2
· 𝑁) + 2)) ∈
Fin |
40 | | lcmfnncl 16010 |
. . . . . 6
⊢
(((1...((2 · 𝑁) + 2)) ⊆ ℕ ∧ (1...((2
· 𝑁) + 2)) ∈
Fin) → (lcm‘(1...((2 · 𝑁) + 2))) ∈ ℕ) |
41 | 38, 39, 40 | mp2an 692 |
. . . . 5
⊢
(lcm‘(1...((2 · 𝑁) + 2))) ∈ ℕ |
42 | 41 | a1i 11 |
. . . 4
⊢ (𝜑 → (lcm‘(1...((2
· 𝑁) + 2))) ∈
ℕ) |
43 | 42 | nnred 11674 |
. . 3
⊢ (𝜑 → (lcm‘(1...((2
· 𝑁) + 2))) ∈
ℝ) |
44 | 18 | nnzd 12110 |
. . . . . . . 8
⊢ (𝜑 → (lcm‘(1...((2
· 𝑁) + 1))) ∈
ℤ) |
45 | 44, 32 | jca 516 |
. . . . . . 7
⊢ (𝜑 →
((lcm‘(1...((2 · 𝑁) + 1))) ∈ ℤ ∧ ((2 ·
𝑁) + 2) ∈
ℤ)) |
46 | | dvdslcm 15979 |
. . . . . . 7
⊢
(((lcm‘(1...((2 · 𝑁) + 1))) ∈ ℤ ∧ ((2 ·
𝑁) + 2) ∈ ℤ)
→ ((lcm‘(1...((2 · 𝑁) + 1))) ∥ ((lcm‘(1...((2
· 𝑁) + 1))) lcm ((2
· 𝑁) + 2)) ∧ ((2
· 𝑁) + 2) ∥
((lcm‘(1...((2 · 𝑁) + 1))) lcm ((2 · 𝑁) + 2)))) |
47 | 45, 46 | syl 17 |
. . . . . 6
⊢ (𝜑 →
((lcm‘(1...((2 · 𝑁) + 1))) ∥ ((lcm‘(1...((2
· 𝑁) + 1))) lcm ((2
· 𝑁) + 2)) ∧ ((2
· 𝑁) + 2) ∥
((lcm‘(1...((2 · 𝑁) + 1))) lcm ((2 · 𝑁) + 2)))) |
48 | 47 | simpld 499 |
. . . . 5
⊢ (𝜑 → (lcm‘(1...((2
· 𝑁) + 1))) ∥
((lcm‘(1...((2 · 𝑁) + 1))) lcm ((2 · 𝑁) + 2))) |
49 | | 2nn 11732 |
. . . . . . . . . 10
⊢ 2 ∈
ℕ |
50 | 49 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 2 ∈
ℕ) |
51 | 50, 5 | nnmulcld 11712 |
. . . . . . . 8
⊢ (𝜑 → (2 · 𝑁) ∈
ℕ) |
52 | 51, 50 | nnaddcld 11711 |
. . . . . . 7
⊢ (𝜑 → ((2 · 𝑁) + 2) ∈
ℕ) |
53 | 52 | lcmfunnnd 39564 |
. . . . . 6
⊢ (𝜑 → (lcm‘(1...((2
· 𝑁) + 2))) =
((lcm‘(1...(((2 · 𝑁) + 2) − 1))) lcm ((2 · 𝑁) + 2))) |
54 | 22 | recnd 10692 |
. . . . . . . . . . 11
⊢ (𝜑 → (2 · 𝑁) ∈
ℂ) |
55 | 2 | recnd 10692 |
. . . . . . . . . . 11
⊢ (𝜑 → 2 ∈
ℂ) |
56 | | 1cnd 10659 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 ∈
ℂ) |
57 | 54, 55, 56 | addsubassd 11040 |
. . . . . . . . . 10
⊢ (𝜑 → (((2 · 𝑁) + 2) − 1) = ((2 ·
𝑁) + (2 −
1))) |
58 | | 2m1e1 11785 |
. . . . . . . . . . 11
⊢ (2
− 1) = 1 |
59 | 58 | oveq2i 7154 |
. . . . . . . . . 10
⊢ ((2
· 𝑁) + (2 −
1)) = ((2 · 𝑁) +
1) |
60 | 57, 59 | eqtrdi 2810 |
. . . . . . . . 9
⊢ (𝜑 → (((2 · 𝑁) + 2) − 1) = ((2 ·
𝑁) + 1)) |
61 | 60 | oveq2d 7159 |
. . . . . . . 8
⊢ (𝜑 → (1...(((2 · 𝑁) + 2) − 1)) = (1...((2
· 𝑁) +
1))) |
62 | 61 | fveq2d 6655 |
. . . . . . 7
⊢ (𝜑 →
(lcm‘(1...(((2 · 𝑁) + 2) − 1))) =
(lcm‘(1...((2 · 𝑁) + 1)))) |
63 | 62 | oveq1d 7158 |
. . . . . 6
⊢ (𝜑 →
((lcm‘(1...(((2 · 𝑁) + 2) − 1))) lcm ((2 · 𝑁) + 2)) =
((lcm‘(1...((2 · 𝑁) + 1))) lcm ((2 · 𝑁) + 2))) |
64 | 53, 63 | eqtrd 2794 |
. . . . 5
⊢ (𝜑 → (lcm‘(1...((2
· 𝑁) + 2))) =
((lcm‘(1...((2 · 𝑁) + 1))) lcm ((2 · 𝑁) + 2))) |
65 | 48, 64 | breqtrrd 5053 |
. . . 4
⊢ (𝜑 → (lcm‘(1...((2
· 𝑁) + 1))) ∥
(lcm‘(1...((2 · 𝑁) + 2)))) |
66 | 44, 42 | jca 516 |
. . . . 5
⊢ (𝜑 →
((lcm‘(1...((2 · 𝑁) + 1))) ∈ ℤ ∧
(lcm‘(1...((2 · 𝑁) + 2))) ∈ ℕ)) |
67 | | dvdsle 15696 |
. . . . 5
⊢
(((lcm‘(1...((2 · 𝑁) + 1))) ∈ ℤ ∧
(lcm‘(1...((2 · 𝑁) + 2))) ∈ ℕ) →
((lcm‘(1...((2 · 𝑁) + 1))) ∥ (lcm‘(1...((2
· 𝑁) + 2))) →
(lcm‘(1...((2 · 𝑁) + 1))) ≤ (lcm‘(1...((2
· 𝑁) +
2))))) |
68 | 66, 67 | syl 17 |
. . . 4
⊢ (𝜑 →
((lcm‘(1...((2 · 𝑁) + 1))) ∥ (lcm‘(1...((2
· 𝑁) + 2))) →
(lcm‘(1...((2 · 𝑁) + 1))) ≤ (lcm‘(1...((2
· 𝑁) +
2))))) |
69 | 65, 68 | mpd 15 |
. . 3
⊢ (𝜑 → (lcm‘(1...((2
· 𝑁) + 1))) ≤
(lcm‘(1...((2 · 𝑁) + 2)))) |
70 | 13, 19, 43, 36, 69 | letrd 10820 |
. 2
⊢ (𝜑 → (2↑((2 · 𝑁) + 2)) ≤
(lcm‘(1...((2 · 𝑁) + 2)))) |
71 | 37, 70 | jca 516 |
1
⊢ (𝜑 → ((2↑((2 ·
𝑁) + 1)) ≤
(lcm‘(1...((2 · 𝑁) + 1))) ∧ (2↑((2 · 𝑁) + 2)) ≤
(lcm‘(1...((2 · 𝑁) + 2))))) |