Step | Hyp | Ref
| Expression |
1 | | oveq2 7199 |
. . . 4
⊢ (𝑥 = 4 → (2↑𝑥) = (2↑4)) |
2 | | 2exp4 16601 |
. . . 4
⊢
(2↑4) = ;16 |
3 | 1, 2 | eqtrdi 2787 |
. . 3
⊢ (𝑥 = 4 → (2↑𝑥) = ;16) |
4 | | fveq2 6695 |
. . . 4
⊢ (𝑥 = 4 → (!‘𝑥) =
(!‘4)) |
5 | | fac4 13812 |
. . . 4
⊢
(!‘4) = ;24 |
6 | 4, 5 | eqtrdi 2787 |
. . 3
⊢ (𝑥 = 4 → (!‘𝑥) = ;24) |
7 | 3, 6 | breq12d 5052 |
. 2
⊢ (𝑥 = 4 → ((2↑𝑥) < (!‘𝑥) ↔ ;16 < ;24)) |
8 | | oveq2 7199 |
. . 3
⊢ (𝑥 = 𝑛 → (2↑𝑥) = (2↑𝑛)) |
9 | | fveq2 6695 |
. . 3
⊢ (𝑥 = 𝑛 → (!‘𝑥) = (!‘𝑛)) |
10 | 8, 9 | breq12d 5052 |
. 2
⊢ (𝑥 = 𝑛 → ((2↑𝑥) < (!‘𝑥) ↔ (2↑𝑛) < (!‘𝑛))) |
11 | | oveq2 7199 |
. . 3
⊢ (𝑥 = (𝑛 + 1) → (2↑𝑥) = (2↑(𝑛 + 1))) |
12 | | fveq2 6695 |
. . 3
⊢ (𝑥 = (𝑛 + 1) → (!‘𝑥) = (!‘(𝑛 + 1))) |
13 | 11, 12 | breq12d 5052 |
. 2
⊢ (𝑥 = (𝑛 + 1) → ((2↑𝑥) < (!‘𝑥) ↔ (2↑(𝑛 + 1)) < (!‘(𝑛 + 1)))) |
14 | | oveq2 7199 |
. . 3
⊢ (𝑥 = 𝑁 → (2↑𝑥) = (2↑𝑁)) |
15 | | fveq2 6695 |
. . 3
⊢ (𝑥 = 𝑁 → (!‘𝑥) = (!‘𝑁)) |
16 | 14, 15 | breq12d 5052 |
. 2
⊢ (𝑥 = 𝑁 → ((2↑𝑥) < (!‘𝑥) ↔ (2↑𝑁) < (!‘𝑁))) |
17 | | 1nn0 12071 |
. . 3
⊢ 1 ∈
ℕ0 |
18 | | 2nn0 12072 |
. . 3
⊢ 2 ∈
ℕ0 |
19 | | 6nn0 12076 |
. . 3
⊢ 6 ∈
ℕ0 |
20 | | 4nn0 12074 |
. . 3
⊢ 4 ∈
ℕ0 |
21 | | 6lt10 12392 |
. . 3
⊢ 6 <
;10 |
22 | | 1lt2 11966 |
. . 3
⊢ 1 <
2 |
23 | 17, 18, 19, 20, 21, 22 | decltc 12287 |
. 2
⊢ ;16 < ;24 |
24 | | 2nn 11868 |
. . . . . . . . 9
⊢ 2 ∈
ℕ |
25 | 24 | a1i 11 |
. . . . . . . 8
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 2 ∈ ℕ) |
26 | | 4nn 11878 |
. . . . . . . . . 10
⊢ 4 ∈
ℕ |
27 | | simpl 486 |
. . . . . . . . . 10
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 𝑛 ∈
(ℤ≥‘4)) |
28 | | eluznn 12479 |
. . . . . . . . . 10
⊢ ((4
∈ ℕ ∧ 𝑛
∈ (ℤ≥‘4)) → 𝑛 ∈ ℕ) |
29 | 26, 27, 28 | sylancr 590 |
. . . . . . . . 9
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 𝑛 ∈ ℕ) |
30 | 29 | nnnn0d 12115 |
. . . . . . . 8
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 𝑛 ∈ ℕ0) |
31 | 25, 30 | nnexpcld 13777 |
. . . . . . 7
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (2↑𝑛) ∈ ℕ) |
32 | 31 | nnred 11810 |
. . . . . 6
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (2↑𝑛) ∈ ℝ) |
33 | | 2re 11869 |
. . . . . . 7
⊢ 2 ∈
ℝ |
34 | 33 | a1i 11 |
. . . . . 6
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 2 ∈ ℝ) |
35 | 32, 34 | remulcld 10828 |
. . . . 5
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → ((2↑𝑛) · 2) ∈
ℝ) |
36 | 30 | faccld 13815 |
. . . . . . 7
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (!‘𝑛) ∈ ℕ) |
37 | 36 | nnred 11810 |
. . . . . 6
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (!‘𝑛) ∈ ℝ) |
38 | 37, 34 | remulcld 10828 |
. . . . 5
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → ((!‘𝑛) · 2) ∈
ℝ) |
39 | 29 | nnred 11810 |
. . . . . . 7
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 𝑛 ∈ ℝ) |
40 | | 1red 10799 |
. . . . . . 7
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 1 ∈ ℝ) |
41 | 39, 40 | readdcld 10827 |
. . . . . 6
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (𝑛 + 1) ∈ ℝ) |
42 | 37, 41 | remulcld 10828 |
. . . . 5
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → ((!‘𝑛) · (𝑛 + 1)) ∈ ℝ) |
43 | | 2rp 12556 |
. . . . . . 7
⊢ 2 ∈
ℝ+ |
44 | 43 | a1i 11 |
. . . . . 6
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 2 ∈
ℝ+) |
45 | | simpr 488 |
. . . . . 6
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (2↑𝑛) < (!‘𝑛)) |
46 | 32, 37, 44, 45 | ltmul1dd 12648 |
. . . . 5
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → ((2↑𝑛) · 2) < ((!‘𝑛) · 2)) |
47 | 36 | nnnn0d 12115 |
. . . . . . 7
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (!‘𝑛) ∈
ℕ0) |
48 | 47 | nn0ge0d 12118 |
. . . . . 6
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 0 ≤ (!‘𝑛)) |
49 | | df-2 11858 |
. . . . . . 7
⊢ 2 = (1 +
1) |
50 | 29 | nnge1d 11843 |
. . . . . . . 8
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 1 ≤ 𝑛) |
51 | 40, 39, 40, 50 | leadd1dd 11411 |
. . . . . . 7
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (1 + 1) ≤ (𝑛 + 1)) |
52 | 49, 51 | eqbrtrid 5074 |
. . . . . 6
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 2 ≤ (𝑛 + 1)) |
53 | 34, 41, 37, 48, 52 | lemul2ad 11737 |
. . . . 5
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → ((!‘𝑛) · 2) ≤ ((!‘𝑛) · (𝑛 + 1))) |
54 | 35, 38, 42, 46, 53 | ltletrd 10957 |
. . . 4
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → ((2↑𝑛) · 2) < ((!‘𝑛) · (𝑛 + 1))) |
55 | | 2cnd 11873 |
. . . . 5
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 2 ∈ ℂ) |
56 | 55, 30 | expp1d 13682 |
. . . 4
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (2↑(𝑛 + 1)) = ((2↑𝑛) · 2)) |
57 | | facp1 13809 |
. . . . 5
⊢ (𝑛 ∈ ℕ0
→ (!‘(𝑛 + 1)) =
((!‘𝑛) ·
(𝑛 + 1))) |
58 | 30, 57 | syl 17 |
. . . 4
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (!‘(𝑛 + 1)) = ((!‘𝑛) · (𝑛 + 1))) |
59 | 54, 56, 58 | 3brtr4d 5071 |
. . 3
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (2↑(𝑛 + 1)) < (!‘(𝑛 + 1))) |
60 | 59 | ex 416 |
. 2
⊢ (𝑛 ∈
(ℤ≥‘4) → ((2↑𝑛) < (!‘𝑛) → (2↑(𝑛 + 1)) < (!‘(𝑛 + 1)))) |
61 | 7, 10, 13, 16, 23, 60 | uzind4i 12471 |
1
⊢ (𝑁 ∈
(ℤ≥‘4) → (2↑𝑁) < (!‘𝑁)) |