Proof of Theorem lcmineqlem23
| Step | Hyp | Ref
| Expression |
| 1 | | lcmineqlem23.1 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 2 | | 2nn 12339 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℕ |
| 3 | 2 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 2 ∈
ℕ) |
| 4 | 1, 3 | jca 511 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 2 ∈
ℕ)) |
| 5 | | nndivdvds 16299 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 2 ∈
ℕ) → (2 ∥ 𝑁 ↔ (𝑁 / 2) ∈ ℕ)) |
| 6 | 4, 5 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (2 ∥ 𝑁 ↔ (𝑁 / 2) ∈ ℕ)) |
| 7 | 6 | biimpa 476 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 2 ∥ 𝑁) → (𝑁 / 2) ∈ ℕ) |
| 8 | 7 | nnzd 12640 |
. . . . . . . 8
⊢ ((𝜑 ∧ 2 ∥ 𝑁) → (𝑁 / 2) ∈ ℤ) |
| 9 | | 1zzd 12648 |
. . . . . . . 8
⊢ ((𝜑 ∧ 2 ∥ 𝑁) → 1 ∈ ℤ) |
| 10 | 8, 9 | zsubcld 12727 |
. . . . . . 7
⊢ ((𝜑 ∧ 2 ∥ 𝑁) → ((𝑁 / 2) − 1) ∈
ℤ) |
| 11 | | 0red 11264 |
. . . . . . . 8
⊢ ((𝜑 ∧ 2 ∥ 𝑁) → 0 ∈ ℝ) |
| 12 | | 4re 12350 |
. . . . . . . . 9
⊢ 4 ∈
ℝ |
| 13 | 12 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 2 ∥ 𝑁) → 4 ∈ ℝ) |
| 14 | 7 | nnred 12281 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 2 ∥ 𝑁) → (𝑁 / 2) ∈ ℝ) |
| 15 | | 1red 11262 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 2 ∥ 𝑁) → 1 ∈ ℝ) |
| 16 | 14, 15 | resubcld 11691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 2 ∥ 𝑁) → ((𝑁 / 2) − 1) ∈
ℝ) |
| 17 | | 4pos 12373 |
. . . . . . . . 9
⊢ 0 <
4 |
| 18 | 17 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 2 ∥ 𝑁) → 0 < 4) |
| 19 | | 5m1e4 12396 |
. . . . . . . . 9
⊢ (5
− 1) = 4 |
| 20 | | 5re 12353 |
. . . . . . . . . . 11
⊢ 5 ∈
ℝ |
| 21 | 20 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 2 ∥ 𝑁) → 5 ∈ ℝ) |
| 22 | 2 | nncni 12276 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℂ |
| 23 | | 5cn 12354 |
. . . . . . . . . . . . . 14
⊢ 5 ∈
ℂ |
| 24 | 22, 23 | mulcomi 11269 |
. . . . . . . . . . . . 13
⊢ (2
· 5) = (5 · 2) |
| 25 | | 5t2e10 12833 |
. . . . . . . . . . . . 13
⊢ (5
· 2) = ;10 |
| 26 | 24, 25 | eqtri 2765 |
. . . . . . . . . . . 12
⊢ (2
· 5) = ;10 |
| 27 | | 10re 12752 |
. . . . . . . . . . . . . 14
⊢ ;10 ∈ ℝ |
| 28 | 27 | recni 11275 |
. . . . . . . . . . . . 13
⊢ ;10 ∈ ℂ |
| 29 | 2 | nnne0i 12306 |
. . . . . . . . . . . . 13
⊢ 2 ≠
0 |
| 30 | 28, 22, 23, 29 | divmuli 12021 |
. . . . . . . . . . . 12
⊢ ((;10 / 2) = 5 ↔ (2 · 5) =
;10) |
| 31 | 26, 30 | mpbir 231 |
. . . . . . . . . . 11
⊢ (;10 / 2) = 5 |
| 32 | 27 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 2 ∥ 𝑁) → ;10 ∈ ℝ) |
| 33 | 1 | nnred 12281 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℝ) |
| 34 | 33 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 2 ∥ 𝑁) → 𝑁 ∈ ℝ) |
| 35 | | 2rp 13039 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℝ+ |
| 36 | 35 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 2 ∥ 𝑁) → 2 ∈
ℝ+) |
| 37 | | 9p1e10 12735 |
. . . . . . . . . . . . 13
⊢ (9 + 1) =
;10 |
| 38 | | lcmineqlem23.2 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 9 ≤ 𝑁) |
| 39 | | 9re 12365 |
. . . . . . . . . . . . . . . . . . 19
⊢ 9 ∈
ℝ |
| 40 | 39 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 9 ∈
ℝ) |
| 41 | 40, 33 | leloed 11404 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (9 ≤ 𝑁 ↔ (9 < 𝑁 ∨ 9 = 𝑁))) |
| 42 | 38, 41 | mpbid 232 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (9 < 𝑁 ∨ 9 = 𝑁)) |
| 43 | 42 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 2 ∥ 𝑁) → (9 < 𝑁 ∨ 9 = 𝑁)) |
| 44 | | 4cn 12351 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 4 ∈
ℂ |
| 45 | 22, 44 | mulcomi 11269 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (2
· 4) = (4 · 2) |
| 46 | | 4t2e8 12434 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (4
· 2) = 8 |
| 47 | 45, 46 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (2
· 4) = 8 |
| 48 | | 8re 12362 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 8 ∈
ℝ |
| 49 | 48 | recni 11275 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 8 ∈
ℂ |
| 50 | 49, 22, 44, 29 | divmuli 12021 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((8 / 2)
= 4 ↔ (2 · 4) = 8) |
| 51 | 47, 50 | mpbir 231 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (8 / 2) =
4 |
| 52 | | 4nn 12349 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 4 ∈
ℕ |
| 53 | 51, 52 | eqeltri 2837 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (8 / 2)
∈ ℕ |
| 54 | | 8nn 12361 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 8 ∈
ℕ |
| 55 | | nndivdvds 16299 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((8
∈ ℕ ∧ 2 ∈ ℕ) → (2 ∥ 8 ↔ (8 / 2)
∈ ℕ)) |
| 56 | 54, 2, 55 | mp2an 692 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (2
∥ 8 ↔ (8 / 2) ∈ ℕ) |
| 57 | 53, 56 | mpbir 231 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∥
8 |
| 58 | | 9m1e8 12400 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (9
− 1) = 8 |
| 59 | 57, 58 | breqtrri 5170 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ∥
(9 − 1) |
| 60 | | 9nn 12364 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 9 ∈
ℕ |
| 61 | 60 | nnzi 12641 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 9 ∈
ℤ |
| 62 | | oddm1even 16380 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (9 ∈
ℤ → (¬ 2 ∥ 9 ↔ 2 ∥ (9 −
1))) |
| 63 | 61, 62 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬ 2
∥ 9 ↔ 2 ∥ (9 − 1)) |
| 64 | 59, 63 | mpbir 231 |
. . . . . . . . . . . . . . . . . 18
⊢ ¬ 2
∥ 9 |
| 65 | | breq2 5147 |
. . . . . . . . . . . . . . . . . 18
⊢ (9 =
𝑁 → (2 ∥ 9
↔ 2 ∥ 𝑁)) |
| 66 | 64, 65 | mtbii 326 |
. . . . . . . . . . . . . . . . 17
⊢ (9 =
𝑁 → ¬ 2 ∥
𝑁) |
| 67 | 66 | con2i 139 |
. . . . . . . . . . . . . . . 16
⊢ (2
∥ 𝑁 → ¬ 9 =
𝑁) |
| 68 | 67 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 2 ∥ 𝑁) → ¬ 9 = 𝑁) |
| 69 | 43, 68 | olcnd 878 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 2 ∥ 𝑁) → 9 < 𝑁) |
| 70 | 1 | nnzd 12640 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 71 | | zltp1le 12667 |
. . . . . . . . . . . . . . . . 17
⊢ ((9
∈ ℤ ∧ 𝑁
∈ ℤ) → (9 < 𝑁 ↔ (9 + 1) ≤ 𝑁)) |
| 72 | 61, 71 | mpan 690 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℤ → (9 <
𝑁 ↔ (9 + 1) ≤ 𝑁)) |
| 73 | 70, 72 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (9 < 𝑁 ↔ (9 + 1) ≤ 𝑁)) |
| 74 | 73 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 2 ∥ 𝑁) → (9 < 𝑁 ↔ (9 + 1) ≤ 𝑁)) |
| 75 | 69, 74 | mpbid 232 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 2 ∥ 𝑁) → (9 + 1) ≤ 𝑁) |
| 76 | 37, 75 | eqbrtrrid 5179 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 2 ∥ 𝑁) → ;10 ≤ 𝑁) |
| 77 | 32, 34, 36, 76 | lediv1dd 13135 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 2 ∥ 𝑁) → (;10 / 2) ≤ (𝑁 / 2)) |
| 78 | 31, 77 | eqbrtrrid 5179 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 2 ∥ 𝑁) → 5 ≤ (𝑁 / 2)) |
| 79 | 21, 14, 15, 78 | lesub1dd 11879 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 2 ∥ 𝑁) → (5 − 1) ≤ ((𝑁 / 2) −
1)) |
| 80 | 19, 79 | eqbrtrrid 5179 |
. . . . . . . 8
⊢ ((𝜑 ∧ 2 ∥ 𝑁) → 4 ≤ ((𝑁 / 2) − 1)) |
| 81 | 11, 13, 16, 18, 80 | ltletrd 11421 |
. . . . . . 7
⊢ ((𝜑 ∧ 2 ∥ 𝑁) → 0 < ((𝑁 / 2) − 1)) |
| 82 | 10, 81 | jca 511 |
. . . . . 6
⊢ ((𝜑 ∧ 2 ∥ 𝑁) → (((𝑁 / 2) − 1) ∈ ℤ ∧ 0 <
((𝑁 / 2) −
1))) |
| 83 | | elnnz 12623 |
. . . . . 6
⊢ (((𝑁 / 2) − 1) ∈ ℕ
↔ (((𝑁 / 2) − 1)
∈ ℤ ∧ 0 < ((𝑁 / 2) − 1))) |
| 84 | 82, 83 | sylibr 234 |
. . . . 5
⊢ ((𝜑 ∧ 2 ∥ 𝑁) → ((𝑁 / 2) − 1) ∈
ℕ) |
| 85 | 84, 80 | lcmineqlem22 42051 |
. . . 4
⊢ ((𝜑 ∧ 2 ∥ 𝑁) → ((2↑((2 · ((𝑁 / 2) − 1)) + 1)) ≤
(lcm‘(1...((2 · ((𝑁 / 2) − 1)) + 1))) ∧ (2↑((2
· ((𝑁 / 2) −
1)) + 2)) ≤ (lcm‘(1...((2 · ((𝑁 / 2) − 1)) + 2))))) |
| 86 | 85 | simprd 495 |
. . 3
⊢ ((𝜑 ∧ 2 ∥ 𝑁) → (2↑((2 · ((𝑁 / 2) − 1)) + 2)) ≤
(lcm‘(1...((2 · ((𝑁 / 2) − 1)) + 2)))) |
| 87 | 3 | nncnd 12282 |
. . . . . . . . . 10
⊢ (𝜑 → 2 ∈
ℂ) |
| 88 | 1 | nncnd 12282 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℂ) |
| 89 | 88 | halfcld 12511 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 / 2) ∈ ℂ) |
| 90 | 87, 89 | muls1d 11723 |
. . . . . . . . 9
⊢ (𝜑 → (2 · ((𝑁 / 2) − 1)) = ((2 ·
(𝑁 / 2)) −
2)) |
| 91 | 90 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝜑 → ((2 · ((𝑁 / 2) − 1)) + 2) = (((2
· (𝑁 / 2)) −
2) + 2)) |
| 92 | 87, 89 | mulcld 11281 |
. . . . . . . . 9
⊢ (𝜑 → (2 · (𝑁 / 2)) ∈
ℂ) |
| 93 | 92, 87 | npcand 11624 |
. . . . . . . 8
⊢ (𝜑 → (((2 · (𝑁 / 2)) − 2) + 2) = (2
· (𝑁 /
2))) |
| 94 | 91, 93 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 → ((2 · ((𝑁 / 2) − 1)) + 2) = (2
· (𝑁 /
2))) |
| 95 | 3 | nnne0d 12316 |
. . . . . . . 8
⊢ (𝜑 → 2 ≠ 0) |
| 96 | 88, 87, 95 | divcan2d 12045 |
. . . . . . 7
⊢ (𝜑 → (2 · (𝑁 / 2)) = 𝑁) |
| 97 | 94, 96 | eqtrd 2777 |
. . . . . 6
⊢ (𝜑 → ((2 · ((𝑁 / 2) − 1)) + 2) = 𝑁) |
| 98 | 97 | oveq2d 7447 |
. . . . 5
⊢ (𝜑 → (2↑((2 ·
((𝑁 / 2) − 1)) + 2))
= (2↑𝑁)) |
| 99 | 97 | oveq2d 7447 |
. . . . . 6
⊢ (𝜑 → (1...((2 · ((𝑁 / 2) − 1)) + 2)) =
(1...𝑁)) |
| 100 | 99 | fveq2d 6910 |
. . . . 5
⊢ (𝜑 → (lcm‘(1...((2
· ((𝑁 / 2) −
1)) + 2))) = (lcm‘(1...𝑁))) |
| 101 | 98, 100 | breq12d 5156 |
. . . 4
⊢ (𝜑 → ((2↑((2 ·
((𝑁 / 2) − 1)) + 2))
≤ (lcm‘(1...((2 · ((𝑁 / 2) − 1)) + 2))) ↔
(2↑𝑁) ≤
(lcm‘(1...𝑁)))) |
| 102 | 101 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 2 ∥ 𝑁) → ((2↑((2 · ((𝑁 / 2) − 1)) + 2)) ≤
(lcm‘(1...((2 · ((𝑁 / 2) − 1)) + 2))) ↔
(2↑𝑁) ≤
(lcm‘(1...𝑁)))) |
| 103 | 86, 102 | mpbid 232 |
. 2
⊢ ((𝜑 ∧ 2 ∥ 𝑁) → (2↑𝑁) ≤ (lcm‘(1...𝑁))) |
| 104 | | oddm1even 16380 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ → (¬ 2
∥ 𝑁 ↔ 2 ∥
(𝑁 −
1))) |
| 105 | 70, 104 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (¬ 2 ∥ 𝑁 ↔ 2 ∥ (𝑁 − 1))) |
| 106 | 105 | biimpa 476 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 2 ∥ 𝑁) → 2 ∥ (𝑁 − 1)) |
| 107 | 2 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 2 ∥ 𝑁) → 2 ∈
ℕ) |
| 108 | | 1zzd 12648 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 ∈
ℤ) |
| 109 | 70, 108 | zsubcld 12727 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 − 1) ∈ ℤ) |
| 110 | | 0red 11264 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ∈
ℝ) |
| 111 | 48 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 8 ∈
ℝ) |
| 112 | | 1red 11262 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ∈
ℝ) |
| 113 | 33, 112 | resubcld 11691 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 − 1) ∈ ℝ) |
| 114 | | 8pos 12378 |
. . . . . . . . . . . 12
⊢ 0 <
8 |
| 115 | 114 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 < 8) |
| 116 | 40, 33, 112, 38 | lesub1dd 11879 |
. . . . . . . . . . . 12
⊢ (𝜑 → (9 − 1) ≤ (𝑁 − 1)) |
| 117 | 58, 116 | eqbrtrrid 5179 |
. . . . . . . . . . 11
⊢ (𝜑 → 8 ≤ (𝑁 − 1)) |
| 118 | 110, 111,
113, 115, 117 | ltletrd 11421 |
. . . . . . . . . 10
⊢ (𝜑 → 0 < (𝑁 − 1)) |
| 119 | 109, 118 | jca 511 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁 − 1) ∈ ℤ ∧ 0 <
(𝑁 −
1))) |
| 120 | | elnnz 12623 |
. . . . . . . . 9
⊢ ((𝑁 − 1) ∈ ℕ
↔ ((𝑁 − 1)
∈ ℤ ∧ 0 < (𝑁 − 1))) |
| 121 | 119, 120 | sylibr 234 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 − 1) ∈ ℕ) |
| 122 | 121 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 2 ∥ 𝑁) → (𝑁 − 1) ∈ ℕ) |
| 123 | 107, 122 | nndivdvdsd 42000 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 2 ∥ 𝑁) → (2 ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / 2) ∈
ℕ)) |
| 124 | 106, 123 | mpbid 232 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 2 ∥ 𝑁) → ((𝑁 − 1) / 2) ∈
ℕ) |
| 125 | 44, 22 | mulcomi 11269 |
. . . . . . . . 9
⊢ (4
· 2) = (2 · 4) |
| 126 | 125, 46 | eqtr3i 2767 |
. . . . . . . 8
⊢ (2
· 4) = 8 |
| 127 | 126, 50 | mpbir 231 |
. . . . . . 7
⊢ (8 / 2) =
4 |
| 128 | 3 | nnrpd 13075 |
. . . . . . . 8
⊢ (𝜑 → 2 ∈
ℝ+) |
| 129 | 111, 113,
128, 117 | lediv1dd 13135 |
. . . . . . 7
⊢ (𝜑 → (8 / 2) ≤ ((𝑁 − 1) /
2)) |
| 130 | 127, 129 | eqbrtrrid 5179 |
. . . . . 6
⊢ (𝜑 → 4 ≤ ((𝑁 − 1) / 2)) |
| 131 | 130 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 2 ∥ 𝑁) → 4 ≤ ((𝑁 − 1) /
2)) |
| 132 | 124, 131 | lcmineqlem22 42051 |
. . . 4
⊢ ((𝜑 ∧ ¬ 2 ∥ 𝑁) → ((2↑((2 ·
((𝑁 − 1) / 2)) + 1))
≤ (lcm‘(1...((2 · ((𝑁 − 1) / 2)) + 1))) ∧ (2↑((2
· ((𝑁 − 1) /
2)) + 2)) ≤ (lcm‘(1...((2 · ((𝑁 − 1) / 2)) + 2))))) |
| 133 | 132 | simpld 494 |
. . 3
⊢ ((𝜑 ∧ ¬ 2 ∥ 𝑁) → (2↑((2 ·
((𝑁 − 1) / 2)) + 1))
≤ (lcm‘(1...((2 · ((𝑁 − 1) / 2)) + 1)))) |
| 134 | | 1cnd 11256 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℂ) |
| 135 | 88, 134 | subcld 11620 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁 − 1) ∈ ℂ) |
| 136 | 135, 87, 95 | divcan2d 12045 |
. . . . . . . 8
⊢ (𝜑 → (2 · ((𝑁 − 1) / 2)) = (𝑁 − 1)) |
| 137 | 136 | oveq1d 7446 |
. . . . . . 7
⊢ (𝜑 → ((2 · ((𝑁 − 1) / 2)) + 1) = ((𝑁 − 1) +
1)) |
| 138 | 88, 134 | npcand 11624 |
. . . . . . 7
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) |
| 139 | 137, 138 | eqtrd 2777 |
. . . . . 6
⊢ (𝜑 → ((2 · ((𝑁 − 1) / 2)) + 1) = 𝑁) |
| 140 | 139 | oveq2d 7447 |
. . . . 5
⊢ (𝜑 → (2↑((2 ·
((𝑁 − 1) / 2)) + 1))
= (2↑𝑁)) |
| 141 | 139 | oveq2d 7447 |
. . . . . 6
⊢ (𝜑 → (1...((2 · ((𝑁 − 1) / 2)) + 1)) =
(1...𝑁)) |
| 142 | 141 | fveq2d 6910 |
. . . . 5
⊢ (𝜑 → (lcm‘(1...((2
· ((𝑁 − 1) /
2)) + 1))) = (lcm‘(1...𝑁))) |
| 143 | 140, 142 | breq12d 5156 |
. . . 4
⊢ (𝜑 → ((2↑((2 ·
((𝑁 − 1) / 2)) + 1))
≤ (lcm‘(1...((2 · ((𝑁 − 1) / 2)) + 1))) ↔
(2↑𝑁) ≤
(lcm‘(1...𝑁)))) |
| 144 | 143 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ ¬ 2 ∥ 𝑁) → ((2↑((2 ·
((𝑁 − 1) / 2)) + 1))
≤ (lcm‘(1...((2 · ((𝑁 − 1) / 2)) + 1))) ↔
(2↑𝑁) ≤
(lcm‘(1...𝑁)))) |
| 145 | 133, 144 | mpbid 232 |
. 2
⊢ ((𝜑 ∧ ¬ 2 ∥ 𝑁) → (2↑𝑁) ≤
(lcm‘(1...𝑁))) |
| 146 | 103, 145 | pm2.61dan 813 |
1
⊢ (𝜑 → (2↑𝑁) ≤ (lcm‘(1...𝑁))) |