Step | Hyp | Ref
| Expression |
1 | | fveq2 5496 |
. . . 4
⊢ (𝑚 = 0 → (!‘𝑚) =
(!‘0)) |
2 | | fac0 10662 |
. . . 4
⊢
(!‘0) = 1 |
3 | 1, 2 | eqtrdi 2219 |
. . 3
⊢ (𝑚 = 0 → (!‘𝑚) = 1) |
4 | | id 19 |
. . . . 5
⊢ (𝑚 = 0 → 𝑚 = 0) |
5 | 4, 4 | oveq12d 5871 |
. . . 4
⊢ (𝑚 = 0 → (𝑚↑𝑚) = (0↑0)) |
6 | | 0exp0e1 10481 |
. . . 4
⊢
(0↑0) = 1 |
7 | 5, 6 | eqtrdi 2219 |
. . 3
⊢ (𝑚 = 0 → (𝑚↑𝑚) = 1) |
8 | 3, 7 | breq12d 4002 |
. 2
⊢ (𝑚 = 0 → ((!‘𝑚) ≤ (𝑚↑𝑚) ↔ 1 ≤ 1)) |
9 | | fveq2 5496 |
. . 3
⊢ (𝑚 = 𝑘 → (!‘𝑚) = (!‘𝑘)) |
10 | | id 19 |
. . . 4
⊢ (𝑚 = 𝑘 → 𝑚 = 𝑘) |
11 | 10, 10 | oveq12d 5871 |
. . 3
⊢ (𝑚 = 𝑘 → (𝑚↑𝑚) = (𝑘↑𝑘)) |
12 | 9, 11 | breq12d 4002 |
. 2
⊢ (𝑚 = 𝑘 → ((!‘𝑚) ≤ (𝑚↑𝑚) ↔ (!‘𝑘) ≤ (𝑘↑𝑘))) |
13 | | fveq2 5496 |
. . 3
⊢ (𝑚 = (𝑘 + 1) → (!‘𝑚) = (!‘(𝑘 + 1))) |
14 | | id 19 |
. . . 4
⊢ (𝑚 = (𝑘 + 1) → 𝑚 = (𝑘 + 1)) |
15 | 14, 14 | oveq12d 5871 |
. . 3
⊢ (𝑚 = (𝑘 + 1) → (𝑚↑𝑚) = ((𝑘 + 1)↑(𝑘 + 1))) |
16 | 13, 15 | breq12d 4002 |
. 2
⊢ (𝑚 = (𝑘 + 1) → ((!‘𝑚) ≤ (𝑚↑𝑚) ↔ (!‘(𝑘 + 1)) ≤ ((𝑘 + 1)↑(𝑘 + 1)))) |
17 | | fveq2 5496 |
. . 3
⊢ (𝑚 = 𝑁 → (!‘𝑚) = (!‘𝑁)) |
18 | | id 19 |
. . . 4
⊢ (𝑚 = 𝑁 → 𝑚 = 𝑁) |
19 | 18, 18 | oveq12d 5871 |
. . 3
⊢ (𝑚 = 𝑁 → (𝑚↑𝑚) = (𝑁↑𝑁)) |
20 | 17, 19 | breq12d 4002 |
. 2
⊢ (𝑚 = 𝑁 → ((!‘𝑚) ≤ (𝑚↑𝑚) ↔ (!‘𝑁) ≤ (𝑁↑𝑁))) |
21 | | 1le1 8491 |
. 2
⊢ 1 ≤
1 |
22 | | faccl 10669 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ (!‘𝑘) ∈
ℕ) |
23 | 22 | adantr 274 |
. . . . . . 7
⊢ ((𝑘 ∈ ℕ0
∧ (!‘𝑘) ≤
(𝑘↑𝑘)) → (!‘𝑘) ∈ ℕ) |
24 | 23 | nnred 8891 |
. . . . . 6
⊢ ((𝑘 ∈ ℕ0
∧ (!‘𝑘) ≤
(𝑘↑𝑘)) → (!‘𝑘) ∈ ℝ) |
25 | | nn0re 9144 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℝ) |
26 | 25 | adantr 274 |
. . . . . . 7
⊢ ((𝑘 ∈ ℕ0
∧ (!‘𝑘) ≤
(𝑘↑𝑘)) → 𝑘 ∈ ℝ) |
27 | | simpl 108 |
. . . . . . 7
⊢ ((𝑘 ∈ ℕ0
∧ (!‘𝑘) ≤
(𝑘↑𝑘)) → 𝑘 ∈ ℕ0) |
28 | 26, 27 | reexpcld 10626 |
. . . . . 6
⊢ ((𝑘 ∈ ℕ0
∧ (!‘𝑘) ≤
(𝑘↑𝑘)) → (𝑘↑𝑘) ∈ ℝ) |
29 | | nn0p1nn 9174 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℕ) |
30 | 29 | adantr 274 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ0
∧ (!‘𝑘) ≤
(𝑘↑𝑘)) → (𝑘 + 1) ∈ ℕ) |
31 | 30 | nnred 8891 |
. . . . . . 7
⊢ ((𝑘 ∈ ℕ0
∧ (!‘𝑘) ≤
(𝑘↑𝑘)) → (𝑘 + 1) ∈ ℝ) |
32 | 31, 27 | reexpcld 10626 |
. . . . . 6
⊢ ((𝑘 ∈ ℕ0
∧ (!‘𝑘) ≤
(𝑘↑𝑘)) → ((𝑘 + 1)↑𝑘) ∈ ℝ) |
33 | | simpr 109 |
. . . . . 6
⊢ ((𝑘 ∈ ℕ0
∧ (!‘𝑘) ≤
(𝑘↑𝑘)) → (!‘𝑘) ≤ (𝑘↑𝑘)) |
34 | | nn0ge0 9160 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ 0 ≤ 𝑘) |
35 | 34 | adantr 274 |
. . . . . . 7
⊢ ((𝑘 ∈ ℕ0
∧ (!‘𝑘) ≤
(𝑘↑𝑘)) → 0 ≤ 𝑘) |
36 | 26 | lep1d 8847 |
. . . . . . 7
⊢ ((𝑘 ∈ ℕ0
∧ (!‘𝑘) ≤
(𝑘↑𝑘)) → 𝑘 ≤ (𝑘 + 1)) |
37 | | leexp1a 10531 |
. . . . . . 7
⊢ (((𝑘 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ ∧ 𝑘 ∈ ℕ0)
∧ (0 ≤ 𝑘 ∧ 𝑘 ≤ (𝑘 + 1))) → (𝑘↑𝑘) ≤ ((𝑘 + 1)↑𝑘)) |
38 | 26, 31, 27, 35, 36, 37 | syl32anc 1241 |
. . . . . 6
⊢ ((𝑘 ∈ ℕ0
∧ (!‘𝑘) ≤
(𝑘↑𝑘)) → (𝑘↑𝑘) ≤ ((𝑘 + 1)↑𝑘)) |
39 | 24, 28, 32, 33, 38 | letrd 8043 |
. . . . 5
⊢ ((𝑘 ∈ ℕ0
∧ (!‘𝑘) ≤
(𝑘↑𝑘)) → (!‘𝑘) ≤ ((𝑘 + 1)↑𝑘)) |
40 | 30 | nngt0d 8922 |
. . . . . 6
⊢ ((𝑘 ∈ ℕ0
∧ (!‘𝑘) ≤
(𝑘↑𝑘)) → 0 < (𝑘 + 1)) |
41 | | lemul1 8512 |
. . . . . 6
⊢
(((!‘𝑘) ∈
ℝ ∧ ((𝑘 +
1)↑𝑘) ∈ ℝ
∧ ((𝑘 + 1) ∈
ℝ ∧ 0 < (𝑘 +
1))) → ((!‘𝑘)
≤ ((𝑘 + 1)↑𝑘) ↔ ((!‘𝑘) · (𝑘 + 1)) ≤ (((𝑘 + 1)↑𝑘) · (𝑘 + 1)))) |
42 | 24, 32, 31, 40, 41 | syl112anc 1237 |
. . . . 5
⊢ ((𝑘 ∈ ℕ0
∧ (!‘𝑘) ≤
(𝑘↑𝑘)) → ((!‘𝑘) ≤ ((𝑘 + 1)↑𝑘) ↔ ((!‘𝑘) · (𝑘 + 1)) ≤ (((𝑘 + 1)↑𝑘) · (𝑘 + 1)))) |
43 | 39, 42 | mpbid 146 |
. . . 4
⊢ ((𝑘 ∈ ℕ0
∧ (!‘𝑘) ≤
(𝑘↑𝑘)) → ((!‘𝑘) · (𝑘 + 1)) ≤ (((𝑘 + 1)↑𝑘) · (𝑘 + 1))) |
44 | | facp1 10664 |
. . . . 5
⊢ (𝑘 ∈ ℕ0
→ (!‘(𝑘 + 1)) =
((!‘𝑘) ·
(𝑘 + 1))) |
45 | 44 | adantr 274 |
. . . 4
⊢ ((𝑘 ∈ ℕ0
∧ (!‘𝑘) ≤
(𝑘↑𝑘)) → (!‘(𝑘 + 1)) = ((!‘𝑘) · (𝑘 + 1))) |
46 | 30 | nncnd 8892 |
. . . . 5
⊢ ((𝑘 ∈ ℕ0
∧ (!‘𝑘) ≤
(𝑘↑𝑘)) → (𝑘 + 1) ∈ ℂ) |
47 | 46, 27 | expp1d 10610 |
. . . 4
⊢ ((𝑘 ∈ ℕ0
∧ (!‘𝑘) ≤
(𝑘↑𝑘)) → ((𝑘 + 1)↑(𝑘 + 1)) = (((𝑘 + 1)↑𝑘) · (𝑘 + 1))) |
48 | 43, 45, 47 | 3brtr4d 4021 |
. . 3
⊢ ((𝑘 ∈ ℕ0
∧ (!‘𝑘) ≤
(𝑘↑𝑘)) → (!‘(𝑘 + 1)) ≤ ((𝑘 + 1)↑(𝑘 + 1))) |
49 | 48 | ex 114 |
. 2
⊢ (𝑘 ∈ ℕ0
→ ((!‘𝑘) ≤
(𝑘↑𝑘) → (!‘(𝑘 + 1)) ≤ ((𝑘 + 1)↑(𝑘 + 1)))) |
50 | 8, 12, 16, 20, 21, 49 | nn0ind 9326 |
1
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ≤
(𝑁↑𝑁)) |