Proof of Theorem lcmineqlem
Step | Hyp | Ref
| Expression |
1 | | lcmineqlem.2 |
. 2
⊢ (𝜑 → 7 ≤ 𝑁) |
2 | | 7re 12066 |
. . . . 5
⊢ 7 ∈
ℝ |
3 | 2 | a1i 11 |
. . . 4
⊢ (𝜑 → 7 ∈
ℝ) |
4 | | lcmineqlem.1 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℕ) |
5 | 4 | nnred 11988 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ ℝ) |
6 | 3, 5 | leloed 11118 |
. . 3
⊢ (𝜑 → (7 ≤ 𝑁 ↔ (7 < 𝑁 ∨ 7 = 𝑁))) |
7 | 4 | nnzd 12424 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℤ) |
8 | | 7nn 12065 |
. . . . . . . . 9
⊢ 7 ∈
ℕ |
9 | 8 | nnzi 12344 |
. . . . . . . 8
⊢ 7 ∈
ℤ |
10 | | zltp1le 12370 |
. . . . . . . 8
⊢ ((7
∈ ℤ ∧ 𝑁
∈ ℤ) → (7 < 𝑁 ↔ (7 + 1) ≤ 𝑁)) |
11 | 9, 10 | mpan 687 |
. . . . . . 7
⊢ (𝑁 ∈ ℤ → (7 <
𝑁 ↔ (7 + 1) ≤ 𝑁)) |
12 | 7, 11 | syl 17 |
. . . . . 6
⊢ (𝜑 → (7 < 𝑁 ↔ (7 + 1) ≤ 𝑁)) |
13 | | 7p1e8 12122 |
. . . . . . 7
⊢ (7 + 1) =
8 |
14 | 13 | breq1i 5086 |
. . . . . 6
⊢ ((7 + 1)
≤ 𝑁 ↔ 8 ≤ 𝑁) |
15 | 12, 14 | bitrdi 287 |
. . . . 5
⊢ (𝜑 → (7 < 𝑁 ↔ 8 ≤ 𝑁)) |
16 | | 8re 12069 |
. . . . . . . 8
⊢ 8 ∈
ℝ |
17 | 16 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 8 ∈
ℝ) |
18 | 17, 5 | leloed 11118 |
. . . . . 6
⊢ (𝜑 → (8 ≤ 𝑁 ↔ (8 < 𝑁 ∨ 8 = 𝑁))) |
19 | 4 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 8 < 𝑁) → 𝑁 ∈ ℕ) |
20 | | 8p1e9 12123 |
. . . . . . . . . 10
⊢ (8 + 1) =
9 |
21 | | 8nn 12068 |
. . . . . . . . . . . . . . 15
⊢ 8 ∈
ℕ |
22 | 21 | nnzi 12344 |
. . . . . . . . . . . . . 14
⊢ 8 ∈
ℤ |
23 | | zltp1le 12370 |
. . . . . . . . . . . . . 14
⊢ ((8
∈ ℤ ∧ 𝑁
∈ ℤ) → (8 < 𝑁 ↔ (8 + 1) ≤ 𝑁)) |
24 | 22, 23 | mpan 687 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℤ → (8 <
𝑁 ↔ (8 + 1) ≤ 𝑁)) |
25 | 7, 24 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (8 < 𝑁 ↔ (8 + 1) ≤ 𝑁)) |
26 | 25 | biimpd 228 |
. . . . . . . . . . 11
⊢ (𝜑 → (8 < 𝑁 → (8 + 1) ≤ 𝑁)) |
27 | 26 | imp 407 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 8 < 𝑁) → (8 + 1) ≤ 𝑁) |
28 | 20, 27 | eqbrtrrid 5115 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 8 < 𝑁) → 9 ≤ 𝑁) |
29 | 19, 28 | lcmineqlem23 40056 |
. . . . . . . 8
⊢ ((𝜑 ∧ 8 < 𝑁) → (2↑𝑁) ≤ (lcm‘(1...𝑁))) |
30 | 29 | ex 413 |
. . . . . . 7
⊢ (𝜑 → (8 < 𝑁 → (2↑𝑁) ≤ (lcm‘(1...𝑁)))) |
31 | | 2nn0 12250 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℕ0 |
32 | | 8nn0 12256 |
. . . . . . . . . . . 12
⊢ 8 ∈
ℕ0 |
33 | | 5nn0 12253 |
. . . . . . . . . . . 12
⊢ 5 ∈
ℕ0 |
34 | | 4nn0 12252 |
. . . . . . . . . . . 12
⊢ 4 ∈
ℕ0 |
35 | | 6nn0 12254 |
. . . . . . . . . . . 12
⊢ 6 ∈
ℕ0 |
36 | | 0nn0 12248 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℕ0 |
37 | | 2lt8 12170 |
. . . . . . . . . . . 12
⊢ 2 <
8 |
38 | | 5lt10 12571 |
. . . . . . . . . . . 12
⊢ 5 <
;10 |
39 | | 6lt10 12570 |
. . . . . . . . . . . 12
⊢ 6 <
;10 |
40 | 31, 32, 33, 34, 35, 36, 37, 38, 39 | 3decltc 12469 |
. . . . . . . . . . 11
⊢ ;;256 < ;;840 |
41 | | 5nn 12059 |
. . . . . . . . . . . . . . . 16
⊢ 5 ∈
ℕ |
42 | 31, 41 | decnncl 12456 |
. . . . . . . . . . . . . . 15
⊢ ;25 ∈ ℕ |
43 | 42 | nnnn0i 12241 |
. . . . . . . . . . . . . 14
⊢ ;25 ∈
ℕ0 |
44 | | 6nn 12062 |
. . . . . . . . . . . . . 14
⊢ 6 ∈
ℕ |
45 | 43, 44 | decnncl 12456 |
. . . . . . . . . . . . 13
⊢ ;;256 ∈ ℕ |
46 | 45 | nnrei 11982 |
. . . . . . . . . . . 12
⊢ ;;256 ∈ ℝ |
47 | | 4nn 12056 |
. . . . . . . . . . . . . . 15
⊢ 4 ∈
ℕ |
48 | 32, 47 | decnncl 12456 |
. . . . . . . . . . . . . 14
⊢ ;84 ∈ ℕ |
49 | 48 | decnncl2 12460 |
. . . . . . . . . . . . 13
⊢ ;;840 ∈ ℕ |
50 | 49 | nnrei 11982 |
. . . . . . . . . . . 12
⊢ ;;840 ∈ ℝ |
51 | 46, 50 | ltlei 11097 |
. . . . . . . . . . 11
⊢ (;;256 < ;;840
→ ;;256 ≤ ;;840) |
52 | 40, 51 | ax-mp 5 |
. . . . . . . . . 10
⊢ ;;256 ≤ ;;840 |
53 | | 2exp8 16788 |
. . . . . . . . . . . 12
⊢
(2↑8) = ;;256 |
54 | | oveq2 7279 |
. . . . . . . . . . . 12
⊢ (8 =
𝑁 → (2↑8) =
(2↑𝑁)) |
55 | 53, 54 | eqtr3id 2794 |
. . . . . . . . . . 11
⊢ (8 =
𝑁 → ;;256 =
(2↑𝑁)) |
56 | | lcm8un 40025 |
. . . . . . . . . . . 12
⊢
(lcm‘(1...8)) = ;;840 |
57 | | oveq2 7279 |
. . . . . . . . . . . . 13
⊢ (8 =
𝑁 → (1...8) =
(1...𝑁)) |
58 | 57 | fveq2d 6775 |
. . . . . . . . . . . 12
⊢ (8 =
𝑁 →
(lcm‘(1...8)) = (lcm‘(1...𝑁))) |
59 | 56, 58 | eqtr3id 2794 |
. . . . . . . . . . 11
⊢ (8 =
𝑁 → ;;840 =
(lcm‘(1...𝑁))) |
60 | 55, 59 | breq12d 5092 |
. . . . . . . . . 10
⊢ (8 =
𝑁 → (;;256 ≤ ;;840
↔ (2↑𝑁) ≤
(lcm‘(1...𝑁)))) |
61 | 52, 60 | mpbii 232 |
. . . . . . . . 9
⊢ (8 =
𝑁 → (2↑𝑁) ≤
(lcm‘(1...𝑁))) |
62 | 61 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 8 = 𝑁) → (2↑𝑁) ≤ (lcm‘(1...𝑁))) |
63 | 62 | ex 413 |
. . . . . . 7
⊢ (𝜑 → (8 = 𝑁 → (2↑𝑁) ≤ (lcm‘(1...𝑁)))) |
64 | 30, 63 | jaod 856 |
. . . . . 6
⊢ (𝜑 → ((8 < 𝑁 ∨ 8 = 𝑁) → (2↑𝑁) ≤ (lcm‘(1...𝑁)))) |
65 | 18, 64 | sylbid 239 |
. . . . 5
⊢ (𝜑 → (8 ≤ 𝑁 → (2↑𝑁) ≤ (lcm‘(1...𝑁)))) |
66 | 15, 65 | sylbid 239 |
. . . 4
⊢ (𝜑 → (7 < 𝑁 → (2↑𝑁) ≤ (lcm‘(1...𝑁)))) |
67 | | 1nn0 12249 |
. . . . . . . 8
⊢ 1 ∈
ℕ0 |
68 | | 1lt4 12149 |
. . . . . . . 8
⊢ 1 <
4 |
69 | | 2lt10 12574 |
. . . . . . . 8
⊢ 2 <
;10 |
70 | | 8lt10 12568 |
. . . . . . . 8
⊢ 8 <
;10 |
71 | 67, 34, 31, 31, 32, 36, 68, 69, 70 | 3decltc 12469 |
. . . . . . 7
⊢ ;;128 < ;;420 |
72 | | 2nn 12046 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℕ |
73 | 67, 72 | decnncl 12456 |
. . . . . . . . . . 11
⊢ ;12 ∈ ℕ |
74 | 73 | nnnn0i 12241 |
. . . . . . . . . 10
⊢ ;12 ∈
ℕ0 |
75 | 74, 21 | decnncl 12456 |
. . . . . . . . 9
⊢ ;;128 ∈ ℕ |
76 | 75 | nnrei 11982 |
. . . . . . . 8
⊢ ;;128 ∈ ℝ |
77 | 34, 72 | decnncl 12456 |
. . . . . . . . . 10
⊢ ;42 ∈ ℕ |
78 | 77 | decnncl2 12460 |
. . . . . . . . 9
⊢ ;;420 ∈ ℕ |
79 | 78 | nnrei 11982 |
. . . . . . . 8
⊢ ;;420 ∈ ℝ |
80 | 76, 79 | ltlei 11097 |
. . . . . . 7
⊢ (;;128 < ;;420
→ ;;128 ≤ ;;420) |
81 | 71, 80 | ax-mp 5 |
. . . . . 6
⊢ ;;128 ≤ ;;420 |
82 | | 2exp7 16787 |
. . . . . . . 8
⊢
(2↑7) = ;;128 |
83 | | oveq2 7279 |
. . . . . . . 8
⊢ (7 =
𝑁 → (2↑7) =
(2↑𝑁)) |
84 | 82, 83 | eqtr3id 2794 |
. . . . . . 7
⊢ (7 =
𝑁 → ;;128 =
(2↑𝑁)) |
85 | | lcm7un 40024 |
. . . . . . . 8
⊢
(lcm‘(1...7)) = ;;420 |
86 | | oveq2 7279 |
. . . . . . . . 9
⊢ (7 =
𝑁 → (1...7) =
(1...𝑁)) |
87 | 86 | fveq2d 6775 |
. . . . . . . 8
⊢ (7 =
𝑁 →
(lcm‘(1...7)) = (lcm‘(1...𝑁))) |
88 | 85, 87 | eqtr3id 2794 |
. . . . . . 7
⊢ (7 =
𝑁 → ;;420 =
(lcm‘(1...𝑁))) |
89 | 84, 88 | breq12d 5092 |
. . . . . 6
⊢ (7 =
𝑁 → (;;128 ≤ ;;420
↔ (2↑𝑁) ≤
(lcm‘(1...𝑁)))) |
90 | 81, 89 | mpbii 232 |
. . . . 5
⊢ (7 =
𝑁 → (2↑𝑁) ≤
(lcm‘(1...𝑁))) |
91 | 90 | a1i 11 |
. . . 4
⊢ (𝜑 → (7 = 𝑁 → (2↑𝑁) ≤ (lcm‘(1...𝑁)))) |
92 | 66, 91 | jaod 856 |
. . 3
⊢ (𝜑 → ((7 < 𝑁 ∨ 7 = 𝑁) → (2↑𝑁) ≤ (lcm‘(1...𝑁)))) |
93 | 6, 92 | sylbid 239 |
. 2
⊢ (𝜑 → (7 ≤ 𝑁 → (2↑𝑁) ≤ (lcm‘(1...𝑁)))) |
94 | 1, 93 | mpd 15 |
1
⊢ (𝜑 → (2↑𝑁) ≤ (lcm‘(1...𝑁))) |