Metamath Proof Explorer

Theorem facwordi

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

Ref Expression
Assertion facwordi 
|- ( ( M e. NN0 /\ N e. NN0 /\ M <_ N ) -> ( ! ` M ) <_ ( ! ` N ) )

Proof

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