| Step | Hyp | Ref
| Expression |
| 1 | | oveq2 7439 |
. . . 4
⊢ (𝑥 = 4 → (2↑𝑥) = (2↑4)) |
| 2 | | 2exp4 17122 |
. . . 4
⊢
(2↑4) = ;16 |
| 3 | 1, 2 | eqtrdi 2793 |
. . 3
⊢ (𝑥 = 4 → (2↑𝑥) = ;16) |
| 4 | | fveq2 6906 |
. . . 4
⊢ (𝑥 = 4 → (!‘𝑥) =
(!‘4)) |
| 5 | | fac4 14320 |
. . . 4
⊢
(!‘4) = ;24 |
| 6 | 4, 5 | eqtrdi 2793 |
. . 3
⊢ (𝑥 = 4 → (!‘𝑥) = ;24) |
| 7 | 3, 6 | breq12d 5156 |
. 2
⊢ (𝑥 = 4 → ((2↑𝑥) < (!‘𝑥) ↔ ;16 < ;24)) |
| 8 | | oveq2 7439 |
. . 3
⊢ (𝑥 = 𝑛 → (2↑𝑥) = (2↑𝑛)) |
| 9 | | fveq2 6906 |
. . 3
⊢ (𝑥 = 𝑛 → (!‘𝑥) = (!‘𝑛)) |
| 10 | 8, 9 | breq12d 5156 |
. 2
⊢ (𝑥 = 𝑛 → ((2↑𝑥) < (!‘𝑥) ↔ (2↑𝑛) < (!‘𝑛))) |
| 11 | | oveq2 7439 |
. . 3
⊢ (𝑥 = (𝑛 + 1) → (2↑𝑥) = (2↑(𝑛 + 1))) |
| 12 | | fveq2 6906 |
. . 3
⊢ (𝑥 = (𝑛 + 1) → (!‘𝑥) = (!‘(𝑛 + 1))) |
| 13 | 11, 12 | breq12d 5156 |
. 2
⊢ (𝑥 = (𝑛 + 1) → ((2↑𝑥) < (!‘𝑥) ↔ (2↑(𝑛 + 1)) < (!‘(𝑛 + 1)))) |
| 14 | | oveq2 7439 |
. . 3
⊢ (𝑥 = 𝑁 → (2↑𝑥) = (2↑𝑁)) |
| 15 | | fveq2 6906 |
. . 3
⊢ (𝑥 = 𝑁 → (!‘𝑥) = (!‘𝑁)) |
| 16 | 14, 15 | breq12d 5156 |
. 2
⊢ (𝑥 = 𝑁 → ((2↑𝑥) < (!‘𝑥) ↔ (2↑𝑁) < (!‘𝑁))) |
| 17 | | 1nn0 12542 |
. . 3
⊢ 1 ∈
ℕ0 |
| 18 | | 2nn0 12543 |
. . 3
⊢ 2 ∈
ℕ0 |
| 19 | | 6nn0 12547 |
. . 3
⊢ 6 ∈
ℕ0 |
| 20 | | 4nn0 12545 |
. . 3
⊢ 4 ∈
ℕ0 |
| 21 | | 6lt10 12867 |
. . 3
⊢ 6 <
;10 |
| 22 | | 1lt2 12437 |
. . 3
⊢ 1 <
2 |
| 23 | 17, 18, 19, 20, 21, 22 | decltc 12762 |
. 2
⊢ ;16 < ;24 |
| 24 | | 2nn 12339 |
. . . . . . . . 9
⊢ 2 ∈
ℕ |
| 25 | 24 | a1i 11 |
. . . . . . . 8
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 2 ∈ ℕ) |
| 26 | | 4nn 12349 |
. . . . . . . . . 10
⊢ 4 ∈
ℕ |
| 27 | | simpl 482 |
. . . . . . . . . 10
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 𝑛 ∈
(ℤ≥‘4)) |
| 28 | | eluznn 12960 |
. . . . . . . . . 10
⊢ ((4
∈ ℕ ∧ 𝑛
∈ (ℤ≥‘4)) → 𝑛 ∈ ℕ) |
| 29 | 26, 27, 28 | sylancr 587 |
. . . . . . . . 9
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 𝑛 ∈ ℕ) |
| 30 | 29 | nnnn0d 12587 |
. . . . . . . 8
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 𝑛 ∈ ℕ0) |
| 31 | 25, 30 | nnexpcld 14284 |
. . . . . . 7
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (2↑𝑛) ∈ ℕ) |
| 32 | 31 | nnred 12281 |
. . . . . 6
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (2↑𝑛) ∈ ℝ) |
| 33 | | 2re 12340 |
. . . . . . 7
⊢ 2 ∈
ℝ |
| 34 | 33 | a1i 11 |
. . . . . 6
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 2 ∈ ℝ) |
| 35 | 32, 34 | remulcld 11291 |
. . . . 5
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → ((2↑𝑛) · 2) ∈
ℝ) |
| 36 | 30 | faccld 14323 |
. . . . . . 7
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (!‘𝑛) ∈ ℕ) |
| 37 | 36 | nnred 12281 |
. . . . . 6
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (!‘𝑛) ∈ ℝ) |
| 38 | 37, 34 | remulcld 11291 |
. . . . 5
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → ((!‘𝑛) · 2) ∈
ℝ) |
| 39 | 29 | nnred 12281 |
. . . . . . 7
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 𝑛 ∈ ℝ) |
| 40 | | 1red 11262 |
. . . . . . 7
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 1 ∈ ℝ) |
| 41 | 39, 40 | readdcld 11290 |
. . . . . 6
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (𝑛 + 1) ∈ ℝ) |
| 42 | 37, 41 | remulcld 11291 |
. . . . 5
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → ((!‘𝑛) · (𝑛 + 1)) ∈ ℝ) |
| 43 | | 2rp 13039 |
. . . . . . 7
⊢ 2 ∈
ℝ+ |
| 44 | 43 | a1i 11 |
. . . . . 6
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 2 ∈
ℝ+) |
| 45 | | simpr 484 |
. . . . . 6
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (2↑𝑛) < (!‘𝑛)) |
| 46 | 32, 37, 44, 45 | ltmul1dd 13132 |
. . . . 5
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → ((2↑𝑛) · 2) < ((!‘𝑛) · 2)) |
| 47 | 36 | nnnn0d 12587 |
. . . . . . 7
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (!‘𝑛) ∈
ℕ0) |
| 48 | 47 | nn0ge0d 12590 |
. . . . . 6
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 0 ≤ (!‘𝑛)) |
| 49 | | df-2 12329 |
. . . . . . 7
⊢ 2 = (1 +
1) |
| 50 | 29 | nnge1d 12314 |
. . . . . . . 8
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 1 ≤ 𝑛) |
| 51 | 40, 39, 40, 50 | leadd1dd 11877 |
. . . . . . 7
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (1 + 1) ≤ (𝑛 + 1)) |
| 52 | 49, 51 | eqbrtrid 5178 |
. . . . . 6
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 2 ≤ (𝑛 + 1)) |
| 53 | 34, 41, 37, 48, 52 | lemul2ad 12208 |
. . . . 5
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → ((!‘𝑛) · 2) ≤ ((!‘𝑛) · (𝑛 + 1))) |
| 54 | 35, 38, 42, 46, 53 | ltletrd 11421 |
. . . 4
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → ((2↑𝑛) · 2) < ((!‘𝑛) · (𝑛 + 1))) |
| 55 | | 2cnd 12344 |
. . . . 5
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 2 ∈ ℂ) |
| 56 | 55, 30 | expp1d 14187 |
. . . 4
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (2↑(𝑛 + 1)) = ((2↑𝑛) · 2)) |
| 57 | | facp1 14317 |
. . . . 5
⊢ (𝑛 ∈ ℕ0
→ (!‘(𝑛 + 1)) =
((!‘𝑛) ·
(𝑛 + 1))) |
| 58 | 30, 57 | syl 17 |
. . . 4
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (!‘(𝑛 + 1)) = ((!‘𝑛) · (𝑛 + 1))) |
| 59 | 54, 56, 58 | 3brtr4d 5175 |
. . 3
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (2↑(𝑛 + 1)) < (!‘(𝑛 + 1))) |
| 60 | 59 | ex 412 |
. 2
⊢ (𝑛 ∈
(ℤ≥‘4) → ((2↑𝑛) < (!‘𝑛) → (2↑(𝑛 + 1)) < (!‘(𝑛 + 1)))) |
| 61 | 7, 10, 13, 16, 23, 60 | uzind4i 12952 |
1
⊢ (𝑁 ∈
(ℤ≥‘4) → (2↑𝑁) < (!‘𝑁)) |