| Step | Hyp | Ref
| Expression |
| 1 | | breq2 5147 |
. . . . . 6
⊢ (𝑗 = 0 → (𝑀 ≤ 𝑗 ↔ 𝑀 ≤ 0)) |
| 2 | 1 | anbi2d 630 |
. . . . 5
⊢ (𝑗 = 0 → ((𝑀 ∈ ℕ0 ∧ 𝑀 ≤ 𝑗) ↔ (𝑀 ∈ ℕ0 ∧ 𝑀 ≤ 0))) |
| 3 | | fveq2 6906 |
. . . . . 6
⊢ (𝑗 = 0 → (!‘𝑗) =
(!‘0)) |
| 4 | 3 | breq2d 5155 |
. . . . 5
⊢ (𝑗 = 0 → ((!‘𝑀) ≤ (!‘𝑗) ↔ (!‘𝑀) ≤
(!‘0))) |
| 5 | 2, 4 | imbi12d 344 |
. . . 4
⊢ (𝑗 = 0 → (((𝑀 ∈ ℕ0 ∧ 𝑀 ≤ 𝑗) → (!‘𝑀) ≤ (!‘𝑗)) ↔ ((𝑀 ∈ ℕ0 ∧ 𝑀 ≤ 0) → (!‘𝑀) ≤
(!‘0)))) |
| 6 | | breq2 5147 |
. . . . . 6
⊢ (𝑗 = 𝑘 → (𝑀 ≤ 𝑗 ↔ 𝑀 ≤ 𝑘)) |
| 7 | 6 | anbi2d 630 |
. . . . 5
⊢ (𝑗 = 𝑘 → ((𝑀 ∈ ℕ0 ∧ 𝑀 ≤ 𝑗) ↔ (𝑀 ∈ ℕ0 ∧ 𝑀 ≤ 𝑘))) |
| 8 | | fveq2 6906 |
. . . . . 6
⊢ (𝑗 = 𝑘 → (!‘𝑗) = (!‘𝑘)) |
| 9 | 8 | breq2d 5155 |
. . . . 5
⊢ (𝑗 = 𝑘 → ((!‘𝑀) ≤ (!‘𝑗) ↔ (!‘𝑀) ≤ (!‘𝑘))) |
| 10 | 7, 9 | imbi12d 344 |
. . . 4
⊢ (𝑗 = 𝑘 → (((𝑀 ∈ ℕ0 ∧ 𝑀 ≤ 𝑗) → (!‘𝑀) ≤ (!‘𝑗)) ↔ ((𝑀 ∈ ℕ0 ∧ 𝑀 ≤ 𝑘) → (!‘𝑀) ≤ (!‘𝑘)))) |
| 11 | | breq2 5147 |
. . . . . 6
⊢ (𝑗 = (𝑘 + 1) → (𝑀 ≤ 𝑗 ↔ 𝑀 ≤ (𝑘 + 1))) |
| 12 | 11 | anbi2d 630 |
. . . . 5
⊢ (𝑗 = (𝑘 + 1) → ((𝑀 ∈ ℕ0 ∧ 𝑀 ≤ 𝑗) ↔ (𝑀 ∈ ℕ0 ∧ 𝑀 ≤ (𝑘 + 1)))) |
| 13 | | fveq2 6906 |
. . . . . 6
⊢ (𝑗 = (𝑘 + 1) → (!‘𝑗) = (!‘(𝑘 + 1))) |
| 14 | 13 | breq2d 5155 |
. . . . 5
⊢ (𝑗 = (𝑘 + 1) → ((!‘𝑀) ≤ (!‘𝑗) ↔ (!‘𝑀) ≤ (!‘(𝑘 + 1)))) |
| 15 | 12, 14 | imbi12d 344 |
. . . 4
⊢ (𝑗 = (𝑘 + 1) → (((𝑀 ∈ ℕ0 ∧ 𝑀 ≤ 𝑗) → (!‘𝑀) ≤ (!‘𝑗)) ↔ ((𝑀 ∈ ℕ0 ∧ 𝑀 ≤ (𝑘 + 1)) → (!‘𝑀) ≤ (!‘(𝑘 + 1))))) |
| 16 | | breq2 5147 |
. . . . . 6
⊢ (𝑗 = 𝑁 → (𝑀 ≤ 𝑗 ↔ 𝑀 ≤ 𝑁)) |
| 17 | 16 | anbi2d 630 |
. . . . 5
⊢ (𝑗 = 𝑁 → ((𝑀 ∈ ℕ0 ∧ 𝑀 ≤ 𝑗) ↔ (𝑀 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁))) |
| 18 | | fveq2 6906 |
. . . . . 6
⊢ (𝑗 = 𝑁 → (!‘𝑗) = (!‘𝑁)) |
| 19 | 18 | breq2d 5155 |
. . . . 5
⊢ (𝑗 = 𝑁 → ((!‘𝑀) ≤ (!‘𝑗) ↔ (!‘𝑀) ≤ (!‘𝑁))) |
| 20 | 17, 19 | imbi12d 344 |
. . . 4
⊢ (𝑗 = 𝑁 → (((𝑀 ∈ ℕ0 ∧ 𝑀 ≤ 𝑗) → (!‘𝑀) ≤ (!‘𝑗)) ↔ ((𝑀 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁) → (!‘𝑀) ≤ (!‘𝑁)))) |
| 21 | | nn0le0eq0 12554 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ0
→ (𝑀 ≤ 0 ↔
𝑀 = 0)) |
| 22 | 21 | biimpa 476 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ0
∧ 𝑀 ≤ 0) →
𝑀 = 0) |
| 23 | 22 | fveq2d 6910 |
. . . . 5
⊢ ((𝑀 ∈ ℕ0
∧ 𝑀 ≤ 0) →
(!‘𝑀) =
(!‘0)) |
| 24 | | fac0 14315 |
. . . . . . 7
⊢
(!‘0) = 1 |
| 25 | | 1re 11261 |
. . . . . . 7
⊢ 1 ∈
ℝ |
| 26 | 24, 25 | eqeltri 2837 |
. . . . . 6
⊢
(!‘0) ∈ ℝ |
| 27 | 26 | leidi 11797 |
. . . . 5
⊢
(!‘0) ≤ (!‘0) |
| 28 | 23, 27 | eqbrtrdi 5182 |
. . . 4
⊢ ((𝑀 ∈ ℕ0
∧ 𝑀 ≤ 0) →
(!‘𝑀) ≤
(!‘0)) |
| 29 | | impexp 450 |
. . . . 5
⊢ (((𝑀 ∈ ℕ0
∧ 𝑀 ≤ 𝑘) → (!‘𝑀) ≤ (!‘𝑘)) ↔ (𝑀 ∈ ℕ0 → (𝑀 ≤ 𝑘 → (!‘𝑀) ≤ (!‘𝑘)))) |
| 30 | | nn0re 12535 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℝ) |
| 31 | | nn0re 12535 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℝ) |
| 32 | | peano2re 11434 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℝ → (𝑘 + 1) ∈
ℝ) |
| 33 | 31, 32 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℝ) |
| 34 | | leloe 11347 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ) →
(𝑀 ≤ (𝑘 + 1) ↔ (𝑀 < (𝑘 + 1) ∨ 𝑀 = (𝑘 + 1)))) |
| 35 | 30, 33, 34 | syl2an 596 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑀 ≤ (𝑘 + 1) ↔ (𝑀 < (𝑘 + 1) ∨ 𝑀 = (𝑘 + 1)))) |
| 36 | | nn0leltp1 12677 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑀 ≤ 𝑘 ↔ 𝑀 < (𝑘 + 1))) |
| 37 | | faccl 14322 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ ℕ0
→ (!‘𝑘) ∈
ℕ) |
| 38 | 37 | nnred 12281 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ ℕ0
→ (!‘𝑘) ∈
ℝ) |
| 39 | 37 | nnnn0d 12587 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ ℕ0
→ (!‘𝑘) ∈
ℕ0) |
| 40 | 39 | nn0ge0d 12590 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ ℕ0
→ 0 ≤ (!‘𝑘)) |
| 41 | | nn0p1nn 12565 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℕ) |
| 42 | 41 | nnge1d 12314 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ ℕ0
→ 1 ≤ (𝑘 +
1)) |
| 43 | 38, 33, 40, 42 | lemulge11d 12205 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℕ0
→ (!‘𝑘) ≤
((!‘𝑘) ·
(𝑘 + 1))) |
| 44 | | facp1 14317 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℕ0
→ (!‘(𝑘 + 1)) =
((!‘𝑘) ·
(𝑘 + 1))) |
| 45 | 43, 44 | breqtrrd 5171 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℕ0
→ (!‘𝑘) ≤
(!‘(𝑘 +
1))) |
| 46 | 45 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (!‘𝑘) ≤ (!‘(𝑘 + 1))) |
| 47 | | faccl 14322 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 ∈ ℕ0
→ (!‘𝑀) ∈
ℕ) |
| 48 | 47 | nnred 12281 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ∈ ℕ0
→ (!‘𝑀) ∈
ℝ) |
| 49 | 48 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (!‘𝑀) ∈ ℝ) |
| 50 | 38 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (!‘𝑘) ∈ ℝ) |
| 51 | | peano2nn0 12566 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℕ0) |
| 52 | 51 | faccld 14323 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ ℕ0
→ (!‘(𝑘 + 1))
∈ ℕ) |
| 53 | 52 | nnred 12281 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℕ0
→ (!‘(𝑘 + 1))
∈ ℝ) |
| 54 | 53 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (!‘(𝑘 + 1)) ∈ ℝ) |
| 55 | | letr 11355 |
. . . . . . . . . . . . . . . . 17
⊢
(((!‘𝑀) ∈
ℝ ∧ (!‘𝑘)
∈ ℝ ∧ (!‘(𝑘 + 1)) ∈ ℝ) →
(((!‘𝑀) ≤
(!‘𝑘) ∧
(!‘𝑘) ≤
(!‘(𝑘 + 1))) →
(!‘𝑀) ≤
(!‘(𝑘 +
1)))) |
| 56 | 49, 50, 54, 55 | syl3anc 1373 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (((!‘𝑀) ≤ (!‘𝑘) ∧ (!‘𝑘) ≤ (!‘(𝑘 + 1))) → (!‘𝑀) ≤ (!‘(𝑘 + 1)))) |
| 57 | 46, 56 | mpan2d 694 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → ((!‘𝑀) ≤ (!‘𝑘) → (!‘𝑀) ≤ (!‘(𝑘 + 1)))) |
| 58 | 57 | imim2d 57 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → ((𝑀 ≤ 𝑘 → (!‘𝑀) ≤ (!‘𝑘)) → (𝑀 ≤ 𝑘 → (!‘𝑀) ≤ (!‘(𝑘 + 1))))) |
| 59 | 58 | com23 86 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑀 ≤ 𝑘 → ((𝑀 ≤ 𝑘 → (!‘𝑀) ≤ (!‘𝑘)) → (!‘𝑀) ≤ (!‘(𝑘 + 1))))) |
| 60 | 36, 59 | sylbird 260 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑀 < (𝑘 + 1) → ((𝑀 ≤ 𝑘 → (!‘𝑀) ≤ (!‘𝑘)) → (!‘𝑀) ≤ (!‘(𝑘 + 1))))) |
| 61 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 = (𝑘 + 1) → (!‘𝑀) = (!‘(𝑘 + 1))) |
| 62 | 48 | leidd 11829 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℕ0
→ (!‘𝑀) ≤
(!‘𝑀)) |
| 63 | | breq2 5147 |
. . . . . . . . . . . . . . . 16
⊢
((!‘𝑀) =
(!‘(𝑘 + 1)) →
((!‘𝑀) ≤
(!‘𝑀) ↔
(!‘𝑀) ≤
(!‘(𝑘 +
1)))) |
| 64 | 62, 63 | syl5ibcom 245 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ0
→ ((!‘𝑀) =
(!‘(𝑘 + 1)) →
(!‘𝑀) ≤
(!‘(𝑘 +
1)))) |
| 65 | 61, 64 | syl5 34 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ0
→ (𝑀 = (𝑘 + 1) → (!‘𝑀) ≤ (!‘(𝑘 + 1)))) |
| 66 | 65 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑀 = (𝑘 + 1) → (!‘𝑀) ≤ (!‘(𝑘 + 1)))) |
| 67 | 66 | a1dd 50 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑀 = (𝑘 + 1) → ((𝑀 ≤ 𝑘 → (!‘𝑀) ≤ (!‘𝑘)) → (!‘𝑀) ≤ (!‘(𝑘 + 1))))) |
| 68 | 60, 67 | jaod 860 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → ((𝑀 < (𝑘 + 1) ∨ 𝑀 = (𝑘 + 1)) → ((𝑀 ≤ 𝑘 → (!‘𝑀) ≤ (!‘𝑘)) → (!‘𝑀) ≤ (!‘(𝑘 + 1))))) |
| 69 | 35, 68 | sylbid 240 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ0
∧ 𝑘 ∈
ℕ0) → (𝑀 ≤ (𝑘 + 1) → ((𝑀 ≤ 𝑘 → (!‘𝑀) ≤ (!‘𝑘)) → (!‘𝑀) ≤ (!‘(𝑘 + 1))))) |
| 70 | 69 | ex 412 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ0
→ (𝑘 ∈
ℕ0 → (𝑀 ≤ (𝑘 + 1) → ((𝑀 ≤ 𝑘 → (!‘𝑀) ≤ (!‘𝑘)) → (!‘𝑀) ≤ (!‘(𝑘 + 1)))))) |
| 71 | 70 | com13 88 |
. . . . . . . 8
⊢ (𝑀 ≤ (𝑘 + 1) → (𝑘 ∈ ℕ0 → (𝑀 ∈ ℕ0
→ ((𝑀 ≤ 𝑘 → (!‘𝑀) ≤ (!‘𝑘)) → (!‘𝑀) ≤ (!‘(𝑘 + 1)))))) |
| 72 | 71 | com4l 92 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ (𝑀 ∈
ℕ0 → ((𝑀 ≤ 𝑘 → (!‘𝑀) ≤ (!‘𝑘)) → (𝑀 ≤ (𝑘 + 1) → (!‘𝑀) ≤ (!‘(𝑘 + 1)))))) |
| 73 | 72 | a2d 29 |
. . . . . 6
⊢ (𝑘 ∈ ℕ0
→ ((𝑀 ∈
ℕ0 → (𝑀 ≤ 𝑘 → (!‘𝑀) ≤ (!‘𝑘))) → (𝑀 ∈ ℕ0 → (𝑀 ≤ (𝑘 + 1) → (!‘𝑀) ≤ (!‘(𝑘 + 1)))))) |
| 74 | 73 | imp4a 422 |
. . . . 5
⊢ (𝑘 ∈ ℕ0
→ ((𝑀 ∈
ℕ0 → (𝑀 ≤ 𝑘 → (!‘𝑀) ≤ (!‘𝑘))) → ((𝑀 ∈ ℕ0 ∧ 𝑀 ≤ (𝑘 + 1)) → (!‘𝑀) ≤ (!‘(𝑘 + 1))))) |
| 75 | 29, 74 | biimtrid 242 |
. . . 4
⊢ (𝑘 ∈ ℕ0
→ (((𝑀 ∈
ℕ0 ∧ 𝑀
≤ 𝑘) →
(!‘𝑀) ≤
(!‘𝑘)) → ((𝑀 ∈ ℕ0
∧ 𝑀 ≤ (𝑘 + 1)) → (!‘𝑀) ≤ (!‘(𝑘 + 1))))) |
| 76 | 5, 10, 15, 20, 28, 75 | nn0ind 12713 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ ((𝑀 ∈
ℕ0 ∧ 𝑀
≤ 𝑁) →
(!‘𝑀) ≤
(!‘𝑁))) |
| 77 | 76 | 3impib 1117 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0 ∧ 𝑀
≤ 𝑁) →
(!‘𝑀) ≤
(!‘𝑁)) |
| 78 | 77 | 3com12 1124 |
1
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑀
≤ 𝑁) →
(!‘𝑀) ≤
(!‘𝑁)) |