Step | Hyp | Ref
| Expression |
1 | | oveq2 6557 |
. . . 4
⊢ (𝑥 = 4 → (2↑𝑥) = (2↑4)) |
2 | | 2exp4 15632 |
. . . 4
⊢
(2↑4) = ;16 |
3 | 1, 2 | syl6eq 2660 |
. . 3
⊢ (𝑥 = 4 → (2↑𝑥) = ;16) |
4 | | fveq2 6103 |
. . . 4
⊢ (𝑥 = 4 → (!‘𝑥) =
(!‘4)) |
5 | | fac4 12930 |
. . . 4
⊢
(!‘4) = ;24 |
6 | 4, 5 | syl6eq 2660 |
. . 3
⊢ (𝑥 = 4 → (!‘𝑥) = ;24) |
7 | 3, 6 | breq12d 4596 |
. 2
⊢ (𝑥 = 4 → ((2↑𝑥) < (!‘𝑥) ↔ ;16 < ;24)) |
8 | | oveq2 6557 |
. . 3
⊢ (𝑥 = 𝑛 → (2↑𝑥) = (2↑𝑛)) |
9 | | fveq2 6103 |
. . 3
⊢ (𝑥 = 𝑛 → (!‘𝑥) = (!‘𝑛)) |
10 | 8, 9 | breq12d 4596 |
. 2
⊢ (𝑥 = 𝑛 → ((2↑𝑥) < (!‘𝑥) ↔ (2↑𝑛) < (!‘𝑛))) |
11 | | oveq2 6557 |
. . 3
⊢ (𝑥 = (𝑛 + 1) → (2↑𝑥) = (2↑(𝑛 + 1))) |
12 | | fveq2 6103 |
. . 3
⊢ (𝑥 = (𝑛 + 1) → (!‘𝑥) = (!‘(𝑛 + 1))) |
13 | 11, 12 | breq12d 4596 |
. 2
⊢ (𝑥 = (𝑛 + 1) → ((2↑𝑥) < (!‘𝑥) ↔ (2↑(𝑛 + 1)) < (!‘(𝑛 + 1)))) |
14 | | oveq2 6557 |
. . 3
⊢ (𝑥 = 𝑁 → (2↑𝑥) = (2↑𝑁)) |
15 | | fveq2 6103 |
. . 3
⊢ (𝑥 = 𝑁 → (!‘𝑥) = (!‘𝑁)) |
16 | 14, 15 | breq12d 4596 |
. 2
⊢ (𝑥 = 𝑁 → ((2↑𝑥) < (!‘𝑥) ↔ (2↑𝑁) < (!‘𝑁))) |
17 | | 1nn0 11185 |
. . . 4
⊢ 1 ∈
ℕ0 |
18 | | 2nn0 11186 |
. . . 4
⊢ 2 ∈
ℕ0 |
19 | | 6nn0 11190 |
. . . 4
⊢ 6 ∈
ℕ0 |
20 | | 4nn0 11188 |
. . . 4
⊢ 4 ∈
ℕ0 |
21 | | 6lt10 11552 |
. . . 4
⊢ 6 <
;10 |
22 | | 1lt2 11071 |
. . . 4
⊢ 1 <
2 |
23 | 17, 18, 19, 20, 21, 22 | decltc 11408 |
. . 3
⊢ ;16 < ;24 |
24 | 23 | a1i 11 |
. 2
⊢ (4 ∈
ℤ → ;16 < ;24) |
25 | | 2nn 11062 |
. . . . . . . . 9
⊢ 2 ∈
ℕ |
26 | 25 | a1i 11 |
. . . . . . . 8
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 2 ∈ ℕ) |
27 | | 4nn 11064 |
. . . . . . . . . 10
⊢ 4 ∈
ℕ |
28 | | simpl 472 |
. . . . . . . . . 10
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 𝑛 ∈
(ℤ≥‘4)) |
29 | | eluznn 11634 |
. . . . . . . . . 10
⊢ ((4
∈ ℕ ∧ 𝑛
∈ (ℤ≥‘4)) → 𝑛 ∈ ℕ) |
30 | 27, 28, 29 | sylancr 694 |
. . . . . . . . 9
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 𝑛 ∈ ℕ) |
31 | 30 | nnnn0d 11228 |
. . . . . . . 8
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 𝑛 ∈ ℕ0) |
32 | 26, 31 | nnexpcld 12892 |
. . . . . . 7
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (2↑𝑛) ∈ ℕ) |
33 | 32 | nnred 10912 |
. . . . . 6
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (2↑𝑛) ∈ ℝ) |
34 | | 2re 10967 |
. . . . . . 7
⊢ 2 ∈
ℝ |
35 | 34 | a1i 11 |
. . . . . 6
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 2 ∈ ℝ) |
36 | 33, 35 | remulcld 9949 |
. . . . 5
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → ((2↑𝑛) · 2) ∈
ℝ) |
37 | 31 | faccld 12933 |
. . . . . . 7
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (!‘𝑛) ∈ ℕ) |
38 | 37 | nnred 10912 |
. . . . . 6
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (!‘𝑛) ∈ ℝ) |
39 | 38, 35 | remulcld 9949 |
. . . . 5
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → ((!‘𝑛) · 2) ∈
ℝ) |
40 | 30 | nnred 10912 |
. . . . . . 7
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 𝑛 ∈ ℝ) |
41 | | 1red 9934 |
. . . . . . 7
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 1 ∈ ℝ) |
42 | 40, 41 | readdcld 9948 |
. . . . . 6
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (𝑛 + 1) ∈ ℝ) |
43 | 38, 42 | remulcld 9949 |
. . . . 5
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → ((!‘𝑛) · (𝑛 + 1)) ∈ ℝ) |
44 | | 2rp 11713 |
. . . . . . 7
⊢ 2 ∈
ℝ+ |
45 | 44 | a1i 11 |
. . . . . 6
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 2 ∈
ℝ+) |
46 | | simpr 476 |
. . . . . 6
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (2↑𝑛) < (!‘𝑛)) |
47 | 33, 38, 45, 46 | ltmul1dd 11803 |
. . . . 5
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → ((2↑𝑛) · 2) < ((!‘𝑛) · 2)) |
48 | 37 | nnnn0d 11228 |
. . . . . . 7
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (!‘𝑛) ∈
ℕ0) |
49 | 48 | nn0ge0d 11231 |
. . . . . 6
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 0 ≤ (!‘𝑛)) |
50 | | df-2 10956 |
. . . . . . 7
⊢ 2 = (1 +
1) |
51 | 30 | nnge1d 10940 |
. . . . . . . 8
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 1 ≤ 𝑛) |
52 | 41, 40, 41, 51 | leadd1dd 10520 |
. . . . . . 7
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (1 + 1) ≤ (𝑛 + 1)) |
53 | 50, 52 | syl5eqbr 4618 |
. . . . . 6
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 2 ≤ (𝑛 + 1)) |
54 | 35, 42, 38, 49, 53 | lemul2ad 10843 |
. . . . 5
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → ((!‘𝑛) · 2) ≤ ((!‘𝑛) · (𝑛 + 1))) |
55 | 36, 39, 43, 47, 54 | ltletrd 10076 |
. . . 4
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → ((2↑𝑛) · 2) < ((!‘𝑛) · (𝑛 + 1))) |
56 | | 2cnd 10970 |
. . . . 5
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → 2 ∈ ℂ) |
57 | 56, 31 | expp1d 12871 |
. . . 4
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (2↑(𝑛 + 1)) = ((2↑𝑛) · 2)) |
58 | | facp1 12927 |
. . . . 5
⊢ (𝑛 ∈ ℕ0
→ (!‘(𝑛 + 1)) =
((!‘𝑛) ·
(𝑛 + 1))) |
59 | 31, 58 | syl 17 |
. . . 4
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (!‘(𝑛 + 1)) = ((!‘𝑛) · (𝑛 + 1))) |
60 | 55, 57, 59 | 3brtr4d 4615 |
. . 3
⊢ ((𝑛 ∈
(ℤ≥‘4) ∧ (2↑𝑛) < (!‘𝑛)) → (2↑(𝑛 + 1)) < (!‘(𝑛 + 1))) |
61 | 60 | ex 449 |
. 2
⊢ (𝑛 ∈
(ℤ≥‘4) → ((2↑𝑛) < (!‘𝑛) → (2↑(𝑛 + 1)) < (!‘(𝑛 + 1)))) |
62 | 7, 10, 13, 16, 24, 61 | uzind4 11622 |
1
⊢ (𝑁 ∈
(ℤ≥‘4) → (2↑𝑁) < (!‘𝑁)) |