Step |
Hyp |
Ref |
Expression |
1 |
|
breq2 |
⊢ ( 𝑗 = 0 → ( 𝑀 ≤ 𝑗 ↔ 𝑀 ≤ 0 ) ) |
2 |
1
|
anbi2d |
⊢ ( 𝑗 = 0 → ( ( 𝑀 ∈ ℕ0 ∧ 𝑀 ≤ 𝑗 ) ↔ ( 𝑀 ∈ ℕ0 ∧ 𝑀 ≤ 0 ) ) ) |
3 |
|
fveq2 |
⊢ ( 𝑗 = 0 → ( ! ‘ 𝑗 ) = ( ! ‘ 0 ) ) |
4 |
3
|
breq2d |
⊢ ( 𝑗 = 0 → ( ( ! ‘ 𝑀 ) ≤ ( ! ‘ 𝑗 ) ↔ ( ! ‘ 𝑀 ) ≤ ( ! ‘ 0 ) ) ) |
5 |
2 4
|
imbi12d |
⊢ ( 𝑗 = 0 → ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑀 ≤ 𝑗 ) → ( ! ‘ 𝑀 ) ≤ ( ! ‘ 𝑗 ) ) ↔ ( ( 𝑀 ∈ ℕ0 ∧ 𝑀 ≤ 0 ) → ( ! ‘ 𝑀 ) ≤ ( ! ‘ 0 ) ) ) ) |
6 |
|
breq2 |
⊢ ( 𝑗 = 𝑘 → ( 𝑀 ≤ 𝑗 ↔ 𝑀 ≤ 𝑘 ) ) |
7 |
6
|
anbi2d |
⊢ ( 𝑗 = 𝑘 → ( ( 𝑀 ∈ ℕ0 ∧ 𝑀 ≤ 𝑗 ) ↔ ( 𝑀 ∈ ℕ0 ∧ 𝑀 ≤ 𝑘 ) ) ) |
8 |
|
fveq2 |
⊢ ( 𝑗 = 𝑘 → ( ! ‘ 𝑗 ) = ( ! ‘ 𝑘 ) ) |
9 |
8
|
breq2d |
⊢ ( 𝑗 = 𝑘 → ( ( ! ‘ 𝑀 ) ≤ ( ! ‘ 𝑗 ) ↔ ( ! ‘ 𝑀 ) ≤ ( ! ‘ 𝑘 ) ) ) |
10 |
7 9
|
imbi12d |
⊢ ( 𝑗 = 𝑘 → ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑀 ≤ 𝑗 ) → ( ! ‘ 𝑀 ) ≤ ( ! ‘ 𝑗 ) ) ↔ ( ( 𝑀 ∈ ℕ0 ∧ 𝑀 ≤ 𝑘 ) → ( ! ‘ 𝑀 ) ≤ ( ! ‘ 𝑘 ) ) ) ) |
11 |
|
breq2 |
⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝑀 ≤ 𝑗 ↔ 𝑀 ≤ ( 𝑘 + 1 ) ) ) |
12 |
11
|
anbi2d |
⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝑀 ∈ ℕ0 ∧ 𝑀 ≤ 𝑗 ) ↔ ( 𝑀 ∈ ℕ0 ∧ 𝑀 ≤ ( 𝑘 + 1 ) ) ) ) |
13 |
|
fveq2 |
⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ! ‘ 𝑗 ) = ( ! ‘ ( 𝑘 + 1 ) ) ) |
14 |
13
|
breq2d |
⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( ! ‘ 𝑀 ) ≤ ( ! ‘ 𝑗 ) ↔ ( ! ‘ 𝑀 ) ≤ ( ! ‘ ( 𝑘 + 1 ) ) ) ) |
15 |
12 14
|
imbi12d |
⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑀 ≤ 𝑗 ) → ( ! ‘ 𝑀 ) ≤ ( ! ‘ 𝑗 ) ) ↔ ( ( 𝑀 ∈ ℕ0 ∧ 𝑀 ≤ ( 𝑘 + 1 ) ) → ( ! ‘ 𝑀 ) ≤ ( ! ‘ ( 𝑘 + 1 ) ) ) ) ) |
16 |
|
breq2 |
⊢ ( 𝑗 = 𝑁 → ( 𝑀 ≤ 𝑗 ↔ 𝑀 ≤ 𝑁 ) ) |
17 |
16
|
anbi2d |
⊢ ( 𝑗 = 𝑁 → ( ( 𝑀 ∈ ℕ0 ∧ 𝑀 ≤ 𝑗 ) ↔ ( 𝑀 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) ) ) |
18 |
|
fveq2 |
⊢ ( 𝑗 = 𝑁 → ( ! ‘ 𝑗 ) = ( ! ‘ 𝑁 ) ) |
19 |
18
|
breq2d |
⊢ ( 𝑗 = 𝑁 → ( ( ! ‘ 𝑀 ) ≤ ( ! ‘ 𝑗 ) ↔ ( ! ‘ 𝑀 ) ≤ ( ! ‘ 𝑁 ) ) ) |
20 |
17 19
|
imbi12d |
⊢ ( 𝑗 = 𝑁 → ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑀 ≤ 𝑗 ) → ( ! ‘ 𝑀 ) ≤ ( ! ‘ 𝑗 ) ) ↔ ( ( 𝑀 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) → ( ! ‘ 𝑀 ) ≤ ( ! ‘ 𝑁 ) ) ) ) |
21 |
|
nn0le0eq0 |
⊢ ( 𝑀 ∈ ℕ0 → ( 𝑀 ≤ 0 ↔ 𝑀 = 0 ) ) |
22 |
21
|
biimpa |
⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑀 ≤ 0 ) → 𝑀 = 0 ) |
23 |
22
|
fveq2d |
⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑀 ≤ 0 ) → ( ! ‘ 𝑀 ) = ( ! ‘ 0 ) ) |
24 |
|
fac0 |
⊢ ( ! ‘ 0 ) = 1 |
25 |
|
1re |
⊢ 1 ∈ ℝ |
26 |
24 25
|
eqeltri |
⊢ ( ! ‘ 0 ) ∈ ℝ |
27 |
26
|
leidi |
⊢ ( ! ‘ 0 ) ≤ ( ! ‘ 0 ) |
28 |
23 27
|
eqbrtrdi |
⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑀 ≤ 0 ) → ( ! ‘ 𝑀 ) ≤ ( ! ‘ 0 ) ) |
29 |
|
impexp |
⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑀 ≤ 𝑘 ) → ( ! ‘ 𝑀 ) ≤ ( ! ‘ 𝑘 ) ) ↔ ( 𝑀 ∈ ℕ0 → ( 𝑀 ≤ 𝑘 → ( ! ‘ 𝑀 ) ≤ ( ! ‘ 𝑘 ) ) ) ) |
30 |
|
nn0re |
⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℝ ) |
31 |
|
nn0re |
⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℝ ) |
32 |
|
peano2re |
⊢ ( 𝑘 ∈ ℝ → ( 𝑘 + 1 ) ∈ ℝ ) |
33 |
31 32
|
syl |
⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℝ ) |
34 |
|
leloe |
⊢ ( ( 𝑀 ∈ ℝ ∧ ( 𝑘 + 1 ) ∈ ℝ ) → ( 𝑀 ≤ ( 𝑘 + 1 ) ↔ ( 𝑀 < ( 𝑘 + 1 ) ∨ 𝑀 = ( 𝑘 + 1 ) ) ) ) |
35 |
30 33 34
|
syl2an |
⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑀 ≤ ( 𝑘 + 1 ) ↔ ( 𝑀 < ( 𝑘 + 1 ) ∨ 𝑀 = ( 𝑘 + 1 ) ) ) ) |
36 |
|
nn0leltp1 |
⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑀 ≤ 𝑘 ↔ 𝑀 < ( 𝑘 + 1 ) ) ) |
37 |
|
faccl |
⊢ ( 𝑘 ∈ ℕ0 → ( ! ‘ 𝑘 ) ∈ ℕ ) |
38 |
37
|
nnred |
⊢ ( 𝑘 ∈ ℕ0 → ( ! ‘ 𝑘 ) ∈ ℝ ) |
39 |
37
|
nnnn0d |
⊢ ( 𝑘 ∈ ℕ0 → ( ! ‘ 𝑘 ) ∈ ℕ0 ) |
40 |
39
|
nn0ge0d |
⊢ ( 𝑘 ∈ ℕ0 → 0 ≤ ( ! ‘ 𝑘 ) ) |
41 |
|
nn0p1nn |
⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℕ ) |
42 |
41
|
nnge1d |
⊢ ( 𝑘 ∈ ℕ0 → 1 ≤ ( 𝑘 + 1 ) ) |
43 |
38 33 40 42
|
lemulge11d |
⊢ ( 𝑘 ∈ ℕ0 → ( ! ‘ 𝑘 ) ≤ ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) ) |
44 |
|
facp1 |
⊢ ( 𝑘 ∈ ℕ0 → ( ! ‘ ( 𝑘 + 1 ) ) = ( ( ! ‘ 𝑘 ) · ( 𝑘 + 1 ) ) ) |
45 |
43 44
|
breqtrrd |
⊢ ( 𝑘 ∈ ℕ0 → ( ! ‘ 𝑘 ) ≤ ( ! ‘ ( 𝑘 + 1 ) ) ) |
46 |
45
|
adantl |
⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ! ‘ 𝑘 ) ≤ ( ! ‘ ( 𝑘 + 1 ) ) ) |
47 |
|
faccl |
⊢ ( 𝑀 ∈ ℕ0 → ( ! ‘ 𝑀 ) ∈ ℕ ) |
48 |
47
|
nnred |
⊢ ( 𝑀 ∈ ℕ0 → ( ! ‘ 𝑀 ) ∈ ℝ ) |
49 |
48
|
adantr |
⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ! ‘ 𝑀 ) ∈ ℝ ) |
50 |
38
|
adantl |
⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ! ‘ 𝑘 ) ∈ ℝ ) |
51 |
|
peano2nn0 |
⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℕ0 ) |
52 |
51
|
faccld |
⊢ ( 𝑘 ∈ ℕ0 → ( ! ‘ ( 𝑘 + 1 ) ) ∈ ℕ ) |
53 |
52
|
nnred |
⊢ ( 𝑘 ∈ ℕ0 → ( ! ‘ ( 𝑘 + 1 ) ) ∈ ℝ ) |
54 |
53
|
adantl |
⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ! ‘ ( 𝑘 + 1 ) ) ∈ ℝ ) |
55 |
|
letr |
⊢ ( ( ( ! ‘ 𝑀 ) ∈ ℝ ∧ ( ! ‘ 𝑘 ) ∈ ℝ ∧ ( ! ‘ ( 𝑘 + 1 ) ) ∈ ℝ ) → ( ( ( ! ‘ 𝑀 ) ≤ ( ! ‘ 𝑘 ) ∧ ( ! ‘ 𝑘 ) ≤ ( ! ‘ ( 𝑘 + 1 ) ) ) → ( ! ‘ 𝑀 ) ≤ ( ! ‘ ( 𝑘 + 1 ) ) ) ) |
56 |
49 50 54 55
|
syl3anc |
⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( ! ‘ 𝑀 ) ≤ ( ! ‘ 𝑘 ) ∧ ( ! ‘ 𝑘 ) ≤ ( ! ‘ ( 𝑘 + 1 ) ) ) → ( ! ‘ 𝑀 ) ≤ ( ! ‘ ( 𝑘 + 1 ) ) ) ) |
57 |
46 56
|
mpan2d |
⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ( ! ‘ 𝑀 ) ≤ ( ! ‘ 𝑘 ) → ( ! ‘ 𝑀 ) ≤ ( ! ‘ ( 𝑘 + 1 ) ) ) ) |
58 |
57
|
imim2d |
⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑀 ≤ 𝑘 → ( ! ‘ 𝑀 ) ≤ ( ! ‘ 𝑘 ) ) → ( 𝑀 ≤ 𝑘 → ( ! ‘ 𝑀 ) ≤ ( ! ‘ ( 𝑘 + 1 ) ) ) ) ) |
59 |
58
|
com23 |
⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑀 ≤ 𝑘 → ( ( 𝑀 ≤ 𝑘 → ( ! ‘ 𝑀 ) ≤ ( ! ‘ 𝑘 ) ) → ( ! ‘ 𝑀 ) ≤ ( ! ‘ ( 𝑘 + 1 ) ) ) ) ) |
60 |
36 59
|
sylbird |
⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑀 < ( 𝑘 + 1 ) → ( ( 𝑀 ≤ 𝑘 → ( ! ‘ 𝑀 ) ≤ ( ! ‘ 𝑘 ) ) → ( ! ‘ 𝑀 ) ≤ ( ! ‘ ( 𝑘 + 1 ) ) ) ) ) |
61 |
|
fveq2 |
⊢ ( 𝑀 = ( 𝑘 + 1 ) → ( ! ‘ 𝑀 ) = ( ! ‘ ( 𝑘 + 1 ) ) ) |
62 |
48
|
leidd |
⊢ ( 𝑀 ∈ ℕ0 → ( ! ‘ 𝑀 ) ≤ ( ! ‘ 𝑀 ) ) |
63 |
|
breq2 |
⊢ ( ( ! ‘ 𝑀 ) = ( ! ‘ ( 𝑘 + 1 ) ) → ( ( ! ‘ 𝑀 ) ≤ ( ! ‘ 𝑀 ) ↔ ( ! ‘ 𝑀 ) ≤ ( ! ‘ ( 𝑘 + 1 ) ) ) ) |
64 |
62 63
|
syl5ibcom |
⊢ ( 𝑀 ∈ ℕ0 → ( ( ! ‘ 𝑀 ) = ( ! ‘ ( 𝑘 + 1 ) ) → ( ! ‘ 𝑀 ) ≤ ( ! ‘ ( 𝑘 + 1 ) ) ) ) |
65 |
61 64
|
syl5 |
⊢ ( 𝑀 ∈ ℕ0 → ( 𝑀 = ( 𝑘 + 1 ) → ( ! ‘ 𝑀 ) ≤ ( ! ‘ ( 𝑘 + 1 ) ) ) ) |
66 |
65
|
adantr |
⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑀 = ( 𝑘 + 1 ) → ( ! ‘ 𝑀 ) ≤ ( ! ‘ ( 𝑘 + 1 ) ) ) ) |
67 |
66
|
a1dd |
⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑀 = ( 𝑘 + 1 ) → ( ( 𝑀 ≤ 𝑘 → ( ! ‘ 𝑀 ) ≤ ( ! ‘ 𝑘 ) ) → ( ! ‘ 𝑀 ) ≤ ( ! ‘ ( 𝑘 + 1 ) ) ) ) ) |
68 |
60 67
|
jaod |
⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑀 < ( 𝑘 + 1 ) ∨ 𝑀 = ( 𝑘 + 1 ) ) → ( ( 𝑀 ≤ 𝑘 → ( ! ‘ 𝑀 ) ≤ ( ! ‘ 𝑘 ) ) → ( ! ‘ 𝑀 ) ≤ ( ! ‘ ( 𝑘 + 1 ) ) ) ) ) |
69 |
35 68
|
sylbid |
⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑀 ≤ ( 𝑘 + 1 ) → ( ( 𝑀 ≤ 𝑘 → ( ! ‘ 𝑀 ) ≤ ( ! ‘ 𝑘 ) ) → ( ! ‘ 𝑀 ) ≤ ( ! ‘ ( 𝑘 + 1 ) ) ) ) ) |
70 |
69
|
ex |
⊢ ( 𝑀 ∈ ℕ0 → ( 𝑘 ∈ ℕ0 → ( 𝑀 ≤ ( 𝑘 + 1 ) → ( ( 𝑀 ≤ 𝑘 → ( ! ‘ 𝑀 ) ≤ ( ! ‘ 𝑘 ) ) → ( ! ‘ 𝑀 ) ≤ ( ! ‘ ( 𝑘 + 1 ) ) ) ) ) ) |
71 |
70
|
com13 |
⊢ ( 𝑀 ≤ ( 𝑘 + 1 ) → ( 𝑘 ∈ ℕ0 → ( 𝑀 ∈ ℕ0 → ( ( 𝑀 ≤ 𝑘 → ( ! ‘ 𝑀 ) ≤ ( ! ‘ 𝑘 ) ) → ( ! ‘ 𝑀 ) ≤ ( ! ‘ ( 𝑘 + 1 ) ) ) ) ) ) |
72 |
71
|
com4l |
⊢ ( 𝑘 ∈ ℕ0 → ( 𝑀 ∈ ℕ0 → ( ( 𝑀 ≤ 𝑘 → ( ! ‘ 𝑀 ) ≤ ( ! ‘ 𝑘 ) ) → ( 𝑀 ≤ ( 𝑘 + 1 ) → ( ! ‘ 𝑀 ) ≤ ( ! ‘ ( 𝑘 + 1 ) ) ) ) ) ) |
73 |
72
|
a2d |
⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑀 ∈ ℕ0 → ( 𝑀 ≤ 𝑘 → ( ! ‘ 𝑀 ) ≤ ( ! ‘ 𝑘 ) ) ) → ( 𝑀 ∈ ℕ0 → ( 𝑀 ≤ ( 𝑘 + 1 ) → ( ! ‘ 𝑀 ) ≤ ( ! ‘ ( 𝑘 + 1 ) ) ) ) ) ) |
74 |
73
|
imp4a |
⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑀 ∈ ℕ0 → ( 𝑀 ≤ 𝑘 → ( ! ‘ 𝑀 ) ≤ ( ! ‘ 𝑘 ) ) ) → ( ( 𝑀 ∈ ℕ0 ∧ 𝑀 ≤ ( 𝑘 + 1 ) ) → ( ! ‘ 𝑀 ) ≤ ( ! ‘ ( 𝑘 + 1 ) ) ) ) ) |
75 |
29 74
|
syl5bi |
⊢ ( 𝑘 ∈ ℕ0 → ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑀 ≤ 𝑘 ) → ( ! ‘ 𝑀 ) ≤ ( ! ‘ 𝑘 ) ) → ( ( 𝑀 ∈ ℕ0 ∧ 𝑀 ≤ ( 𝑘 + 1 ) ) → ( ! ‘ 𝑀 ) ≤ ( ! ‘ ( 𝑘 + 1 ) ) ) ) ) |
76 |
5 10 15 20 28 75
|
nn0ind |
⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑀 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) → ( ! ‘ 𝑀 ) ≤ ( ! ‘ 𝑁 ) ) ) |
77 |
76
|
3impib |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) → ( ! ‘ 𝑀 ) ≤ ( ! ‘ 𝑁 ) ) |
78 |
77
|
3com12 |
⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) → ( ! ‘ 𝑀 ) ≤ ( ! ‘ 𝑁 ) ) |