Proof of Theorem faclbnd3
| Step | Hyp | Ref
| Expression |
| 1 | | elnn0 12528 |
. 2
⊢ (𝑀 ∈ ℕ0
↔ (𝑀 ∈ ℕ
∨ 𝑀 =
0)) |
| 2 | | nnre 12273 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℝ) |
| 3 | 2 | adantr 480 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ 𝑀 ∈
ℝ) |
| 4 | | nnge1 12294 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → 1 ≤
𝑀) |
| 5 | 4 | adantr 480 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ 1 ≤ 𝑀) |
| 6 | | nn0z 12638 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
| 7 | 6 | adantl 481 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ 𝑁 ∈
ℤ) |
| 8 | | uzid 12893 |
. . . . . 6
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
(ℤ≥‘𝑁)) |
| 9 | | peano2uz 12943 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝑁) → (𝑁 + 1) ∈
(ℤ≥‘𝑁)) |
| 10 | 7, 8, 9 | 3syl 18 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (𝑁 + 1) ∈
(ℤ≥‘𝑁)) |
| 11 | 3, 5, 10 | leexp2ad 14293 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (𝑀↑𝑁) ≤ (𝑀↑(𝑁 + 1))) |
| 12 | | nnnn0 12533 |
. . . . 5
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℕ0) |
| 13 | | faclbnd 14329 |
. . . . 5
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑀↑(𝑁 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑁))) |
| 14 | 12, 13 | sylan 580 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (𝑀↑(𝑁 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑁))) |
| 15 | | nn0re 12535 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℝ) |
| 16 | | reexpcl 14119 |
. . . . . . 7
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℕ0)
→ (𝑀↑𝑁) ∈
ℝ) |
| 17 | 15, 16 | sylan 580 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑀↑𝑁) ∈ ℝ) |
| 18 | | peano2nn0 12566 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
| 19 | | reexpcl 14119 |
. . . . . . 7
⊢ ((𝑀 ∈ ℝ ∧ (𝑁 + 1) ∈
ℕ0) → (𝑀↑(𝑁 + 1)) ∈ ℝ) |
| 20 | 15, 18, 19 | syl2an 596 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑀↑(𝑁 + 1)) ∈ ℝ) |
| 21 | | reexpcl 14119 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℝ ∧ 𝑀 ∈ ℕ0)
→ (𝑀↑𝑀) ∈
ℝ) |
| 22 | 15, 21 | mpancom 688 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ0
→ (𝑀↑𝑀) ∈
ℝ) |
| 23 | | faccl 14322 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ∈
ℕ) |
| 24 | 23 | nnred 12281 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ∈
ℝ) |
| 25 | | remulcl 11240 |
. . . . . . 7
⊢ (((𝑀↑𝑀) ∈ ℝ ∧ (!‘𝑁) ∈ ℝ) → ((𝑀↑𝑀) · (!‘𝑁)) ∈ ℝ) |
| 26 | 22, 24, 25 | syl2an 596 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → ((𝑀↑𝑀) · (!‘𝑁)) ∈ ℝ) |
| 27 | | letr 11355 |
. . . . . 6
⊢ (((𝑀↑𝑁) ∈ ℝ ∧ (𝑀↑(𝑁 + 1)) ∈ ℝ ∧ ((𝑀↑𝑀) · (!‘𝑁)) ∈ ℝ) → (((𝑀↑𝑁) ≤ (𝑀↑(𝑁 + 1)) ∧ (𝑀↑(𝑁 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑁))) → (𝑀↑𝑁) ≤ ((𝑀↑𝑀) · (!‘𝑁)))) |
| 28 | 17, 20, 26, 27 | syl3anc 1373 |
. . . . 5
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (((𝑀↑𝑁) ≤ (𝑀↑(𝑁 + 1)) ∧ (𝑀↑(𝑁 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑁))) → (𝑀↑𝑁) ≤ ((𝑀↑𝑀) · (!‘𝑁)))) |
| 29 | 12, 28 | sylan 580 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (((𝑀↑𝑁) ≤ (𝑀↑(𝑁 + 1)) ∧ (𝑀↑(𝑁 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑁))) → (𝑀↑𝑁) ≤ ((𝑀↑𝑀) · (!‘𝑁)))) |
| 30 | 11, 14, 29 | mp2and 699 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (𝑀↑𝑁) ≤ ((𝑀↑𝑀) · (!‘𝑁))) |
| 31 | | elnn0 12528 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
↔ (𝑁 ∈ ℕ
∨ 𝑁 =
0)) |
| 32 | | 0exp 14138 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
(0↑𝑁) =
0) |
| 33 | | 0le1 11786 |
. . . . . . . . 9
⊢ 0 ≤
1 |
| 34 | 32, 33 | eqbrtrdi 5182 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
(0↑𝑁) ≤
1) |
| 35 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑁 = 0 → (0↑𝑁) = (0↑0)) |
| 36 | | 0exp0e1 14107 |
. . . . . . . . . 10
⊢
(0↑0) = 1 |
| 37 | | 1le1 11891 |
. . . . . . . . . 10
⊢ 1 ≤
1 |
| 38 | 36, 37 | eqbrtri 5164 |
. . . . . . . . 9
⊢
(0↑0) ≤ 1 |
| 39 | 35, 38 | eqbrtrdi 5182 |
. . . . . . . 8
⊢ (𝑁 = 0 → (0↑𝑁) ≤ 1) |
| 40 | 34, 39 | jaoi 858 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) → (0↑𝑁) ≤ 1) |
| 41 | 31, 40 | sylbi 217 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (0↑𝑁) ≤
1) |
| 42 | | 1nn 12277 |
. . . . . . . 8
⊢ 1 ∈
ℕ |
| 43 | | nnmulcl 12290 |
. . . . . . . 8
⊢ ((1
∈ ℕ ∧ (!‘𝑁) ∈ ℕ) → (1 ·
(!‘𝑁)) ∈
ℕ) |
| 44 | 42, 23, 43 | sylancr 587 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (1 · (!‘𝑁)) ∈ ℕ) |
| 45 | 44 | nnge1d 12314 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ 1 ≤ (1 · (!‘𝑁))) |
| 46 | | 0re 11263 |
. . . . . . . 8
⊢ 0 ∈
ℝ |
| 47 | | reexpcl 14119 |
. . . . . . . 8
⊢ ((0
∈ ℝ ∧ 𝑁
∈ ℕ0) → (0↑𝑁) ∈ ℝ) |
| 48 | 46, 47 | mpan 690 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (0↑𝑁) ∈
ℝ) |
| 49 | | 1re 11261 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
| 50 | | remulcl 11240 |
. . . . . . . 8
⊢ ((1
∈ ℝ ∧ (!‘𝑁) ∈ ℝ) → (1 ·
(!‘𝑁)) ∈
ℝ) |
| 51 | 49, 24, 50 | sylancr 587 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (1 · (!‘𝑁)) ∈ ℝ) |
| 52 | | letr 11355 |
. . . . . . . 8
⊢
(((0↑𝑁) ∈
ℝ ∧ 1 ∈ ℝ ∧ (1 · (!‘𝑁)) ∈ ℝ) → (((0↑𝑁) ≤ 1 ∧ 1 ≤ (1
· (!‘𝑁)))
→ (0↑𝑁) ≤ (1
· (!‘𝑁)))) |
| 53 | 49, 52 | mp3an2 1451 |
. . . . . . 7
⊢
(((0↑𝑁) ∈
ℝ ∧ (1 · (!‘𝑁)) ∈ ℝ) → (((0↑𝑁) ≤ 1 ∧ 1 ≤ (1
· (!‘𝑁)))
→ (0↑𝑁) ≤ (1
· (!‘𝑁)))) |
| 54 | 48, 51, 53 | syl2anc 584 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (((0↑𝑁) ≤ 1
∧ 1 ≤ (1 · (!‘𝑁))) → (0↑𝑁) ≤ (1 · (!‘𝑁)))) |
| 55 | 41, 45, 54 | mp2and 699 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (0↑𝑁) ≤ (1
· (!‘𝑁))) |
| 56 | 55 | adantl 481 |
. . . 4
⊢ ((𝑀 = 0 ∧ 𝑁 ∈ ℕ0) →
(0↑𝑁) ≤ (1 ·
(!‘𝑁))) |
| 57 | | oveq1 7438 |
. . . . . 6
⊢ (𝑀 = 0 → (𝑀↑𝑁) = (0↑𝑁)) |
| 58 | | oveq12 7440 |
. . . . . . . . 9
⊢ ((𝑀 = 0 ∧ 𝑀 = 0) → (𝑀↑𝑀) = (0↑0)) |
| 59 | 58 | anidms 566 |
. . . . . . . 8
⊢ (𝑀 = 0 → (𝑀↑𝑀) = (0↑0)) |
| 60 | 59, 36 | eqtrdi 2793 |
. . . . . . 7
⊢ (𝑀 = 0 → (𝑀↑𝑀) = 1) |
| 61 | 60 | oveq1d 7446 |
. . . . . 6
⊢ (𝑀 = 0 → ((𝑀↑𝑀) · (!‘𝑁)) = (1 · (!‘𝑁))) |
| 62 | 57, 61 | breq12d 5156 |
. . . . 5
⊢ (𝑀 = 0 → ((𝑀↑𝑁) ≤ ((𝑀↑𝑀) · (!‘𝑁)) ↔ (0↑𝑁) ≤ (1 · (!‘𝑁)))) |
| 63 | 62 | adantr 480 |
. . . 4
⊢ ((𝑀 = 0 ∧ 𝑁 ∈ ℕ0) → ((𝑀↑𝑁) ≤ ((𝑀↑𝑀) · (!‘𝑁)) ↔ (0↑𝑁) ≤ (1 · (!‘𝑁)))) |
| 64 | 56, 63 | mpbird 257 |
. . 3
⊢ ((𝑀 = 0 ∧ 𝑁 ∈ ℕ0) → (𝑀↑𝑁) ≤ ((𝑀↑𝑀) · (!‘𝑁))) |
| 65 | 30, 64 | jaoian 959 |
. 2
⊢ (((𝑀 ∈ ℕ ∨ 𝑀 = 0) ∧ 𝑁 ∈ ℕ0) → (𝑀↑𝑁) ≤ ((𝑀↑𝑀) · (!‘𝑁))) |
| 66 | 1, 65 | sylanb 581 |
1
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑀↑𝑁) ≤ ((𝑀↑𝑀) · (!‘𝑁))) |