Step | Hyp | Ref
| Expression |
1 | | oveq2 6658 |
. . . 4
⊢ (𝑥 = 4 → (2↑𝑥) = (2↑4)) |
2 | | 2exp4 15794 |
. . . 4
⊢
(2↑4) = ;16 |
3 | 1, 2 | syl6eq 2672 |
. . 3
⊢ (𝑥 = 4 → (2↑𝑥) = ;16) |
4 | | fveq2 6191 |
. . . 4
⊢ (𝑥 = 4 → (!‘𝑥) =
(!‘4)) |
5 | | fac4 13068 |
. . . 4
⊢
(!‘4) = ;24 |
6 | 4, 5 | syl6eq 2672 |
. . 3
⊢ (𝑥 = 4 → (!‘𝑥) = ;24) |
7 | 3, 6 | breq12d 4666 |
. 2
⊢ (𝑥 = 4 → ((2↑𝑥) < (!‘𝑥) ↔ ;16 < ;24)) |
8 | | oveq2 6658 |
. . 3
⊢ (𝑥 = 𝑛 → (2↑𝑥) = (2↑𝑛)) |
9 | | fveq2 6191 |
. . 3
⊢ (𝑥 = 𝑛 → (!‘𝑥) = (!‘𝑛)) |
10 | 8, 9 | breq12d 4666 |
. 2
⊢ (𝑥 = 𝑛 → ((2↑𝑥) < (!‘𝑥) ↔ (2↑𝑛) < (!‘𝑛))) |
11 | | oveq2 6658 |
. . 3
⊢ (𝑥 = (𝑛 + 1) → (2↑𝑥) = (2↑(𝑛 + 1))) |
12 | | fveq2 6191 |
. . 3
⊢ (𝑥 = (𝑛 + 1) → (!‘𝑥) = (!‘(𝑛 + 1))) |
13 | 11, 12 | breq12d 4666 |
. 2
⊢ (𝑥 = (𝑛 + 1) → ((2↑𝑥) < (!‘𝑥) ↔ (2↑(𝑛 + 1)) < (!‘(𝑛 + 1)))) |
14 | | oveq2 6658 |
. . 3
⊢ (𝑥 = 𝑁 → (2↑𝑥) = (2↑𝑁)) |
15 | | fveq2 6191 |
. . 3
⊢ (𝑥 = 𝑁 → (!‘𝑥) = (!‘𝑁)) |
16 | 14, 15 | breq12d 4666 |
. 2
⊢ (𝑥 = 𝑁 → ((2↑𝑥) < (!‘𝑥) ↔ (2↑𝑁) < (!‘𝑁))) |
17 | | 1nn0 11308 |
. . . 4
⊢ 1 ∈
ℕ0 |
18 | | 2nn0 11309 |
. . . 4
⊢ 2 ∈
ℕ0 |
19 | | 6nn0 11313 |
. . . 4
⊢ 6 ∈
ℕ0 |
20 | | 4nn0 11311 |
. . . 4
⊢ 4 ∈
ℕ0 |
21 | | 6lt10 11676 |
. . . 4
⊢ 6 <
;10 |
22 | | 1lt2 11194 |
. . . 4
⊢ 1 <
2 |
23 | 17, 18, 19, 20, 21, 22 | decltc 11532 |
. . 3
⊢ ;16 < ;24 |
24 | 23 | a1i 11 |
. 2
⊢ (4 ∈
ℤ → ;16 < ;24) |
25 | | 2nn 11185 |
. . . . . . . . 9
⊢ 2 ∈
ℕ |
26 | 25 | a1i 11 |
. . . . . . . 8
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 2 ∈ ℕ) |
27 | | 4nn 11187 |
. . . . . . . . . 10
⊢ 4 ∈
ℕ |
28 | | simpl 473 |
. . . . . . . . . 10
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 𝑛 ∈
(ℤ≥‘4)) |
29 | | eluznn 11758 |
. . . . . . . . . 10
⊢ ((4
∈ ℕ ∧ 𝑛
∈ (ℤ≥‘4)) → 𝑛 ∈ ℕ) |
30 | 27, 28, 29 | sylancr 695 |
. . . . . . . . 9
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 𝑛 ∈ ℕ) |
31 | 30 | nnnn0d 11351 |
. . . . . . . 8
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 𝑛 ∈ ℕ0) |
32 | 26, 31 | nnexpcld 13030 |
. . . . . . 7
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (2↑𝑛) ∈ ℕ) |
33 | 32 | nnred 11035 |
. . . . . 6
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (2↑𝑛) ∈ ℝ) |
34 | | 2re 11090 |
. . . . . . 7
⊢ 2 ∈
ℝ |
35 | 34 | a1i 11 |
. . . . . 6
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 2 ∈ ℝ) |
36 | 33, 35 | remulcld 10070 |
. . . . 5
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → ((2↑𝑛) · 2) ∈
ℝ) |
37 | 31 | faccld 13071 |
. . . . . . 7
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (!‘𝑛) ∈ ℕ) |
38 | 37 | nnred 11035 |
. . . . . 6
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (!‘𝑛) ∈ ℝ) |
39 | 38, 35 | remulcld 10070 |
. . . . 5
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → ((!‘𝑛) · 2) ∈
ℝ) |
40 | 30 | nnred 11035 |
. . . . . . 7
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 𝑛 ∈ ℝ) |
41 | | 1red 10055 |
. . . . . . 7
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 1 ∈ ℝ) |
42 | 40, 41 | readdcld 10069 |
. . . . . 6
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (𝑛 + 1) ∈ ℝ) |
43 | 38, 42 | remulcld 10070 |
. . . . 5
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → ((!‘𝑛) · (𝑛 + 1)) ∈ ℝ) |
44 | | 2rp 11837 |
. . . . . . 7
⊢ 2 ∈
ℝ+ |
45 | 44 | a1i 11 |
. . . . . 6
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 2 ∈
ℝ+) |
46 | | simpr 477 |
. . . . . 6
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (2↑𝑛) < (!‘𝑛)) |
47 | 33, 38, 45, 46 | ltmul1dd 11927 |
. . . . 5
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → ((2↑𝑛) · 2) < ((!‘𝑛) · 2)) |
48 | 37 | nnnn0d 11351 |
. . . . . . 7
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (!‘𝑛) ∈
ℕ0) |
49 | 48 | nn0ge0d 11354 |
. . . . . 6
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 0 ≤ (!‘𝑛)) |
50 | | df-2 11079 |
. . . . . . 7
⊢ 2 = (1 +
1) |
51 | 30 | nnge1d 11063 |
. . . . . . . 8
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 1 ≤ 𝑛) |
52 | 41, 40, 41, 51 | leadd1dd 10641 |
. . . . . . 7
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (1 + 1) ≤ (𝑛 + 1)) |
53 | 50, 52 | syl5eqbr 4688 |
. . . . . 6
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 2 ≤ (𝑛 + 1)) |
54 | 35, 42, 38, 49, 53 | lemul2ad 10964 |
. . . . 5
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → ((!‘𝑛) · 2) ≤ ((!‘𝑛) · (𝑛 + 1))) |
55 | 36, 39, 43, 47, 54 | ltletrd 10197 |
. . . 4
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → ((2↑𝑛) · 2) < ((!‘𝑛) · (𝑛 + 1))) |
56 | | 2cnd 11093 |
. . . . 5
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 2 ∈ ℂ) |
57 | 56, 31 | expp1d 13009 |
. . . 4
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (2↑(𝑛 + 1)) = ((2↑𝑛) · 2)) |
58 | | facp1 13065 |
. . . . 5
⊢ (𝑛 ∈ ℕ0
→ (!‘(𝑛 + 1)) =
((!‘𝑛) ·
(𝑛 + 1))) |
59 | 31, 58 | syl 17 |
. . . 4
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (!‘(𝑛 + 1)) = ((!‘𝑛) · (𝑛 + 1))) |
60 | 55, 57, 59 | 3brtr4d 4685 |
. . 3
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (2↑(𝑛 + 1)) < (!‘(𝑛 + 1))) |
61 | 60 | ex 450 |
. 2
⊢ (𝑛 ∈
(ℤ≥‘4) → ((2↑𝑛) < (!‘𝑛) → (2↑(𝑛 + 1)) < (!‘(𝑛 + 1)))) |
62 | 7, 10, 13, 16, 24, 61 | uzind4 11746 |
1
⊢ (𝑁 ∈
(ℤ≥‘4) → (2↑𝑁) < (!‘𝑁)) |