Metamath Proof Explorer

Theorem facwordi

Description: Ordering property of factorial. (Contributed by NM, 9-Dec-2005)

Ref Expression
Assertion facwordi ⊢M∈ℕ0∧N∈ℕ0∧M≤N→M!≤N!

Proof

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