Metamath Proof Explorer


Theorem faclbnd3

Description: A lower bound for the factorial function. (Contributed by NM, 19-Dec-2005)

Ref Expression
Assertion faclbnd3 M 0 N 0 M N M M N !

Proof

Step Hyp Ref Expression
1 elnn0 M 0 M M = 0
2 nnre M M
3 2 adantr M N 0 M
4 nnge1 M 1 M
5 4 adantr M N 0 1 M
6 nn0z N 0 N
7 6 adantl M N 0 N
8 uzid N N N
9 peano2uz N N N + 1 N
10 7 8 9 3syl M N 0 N + 1 N
11 3 5 10 leexp2ad M N 0 M N M N + 1
12 nnnn0 M M 0
13 faclbnd M 0 N 0 M N + 1 M M N !
14 12 13 sylan M N 0 M N + 1 M M N !
15 nn0re M 0 M
16 reexpcl M N 0 M N
17 15 16 sylan M 0 N 0 M N
18 peano2nn0 N 0 N + 1 0
19 reexpcl M N + 1 0 M N + 1
20 15 18 19 syl2an M 0 N 0 M N + 1
21 reexpcl M M 0 M M
22 15 21 mpancom M 0 M M
23 faccl N 0 N !
24 23 nnred N 0 N !
25 remulcl M M N ! M M N !
26 22 24 25 syl2an M 0 N 0 M M N !
27 letr M N M N + 1 M M N ! M N M N + 1 M N + 1 M M N ! M N M M N !
28 17 20 26 27 syl3anc M 0 N 0 M N M N + 1 M N + 1 M M N ! M N M M N !
29 12 28 sylan M N 0 M N M N + 1 M N + 1 M M N ! M N M M N !
30 11 14 29 mp2and M N 0 M N M M N !
31 elnn0 N 0 N N = 0
32 0exp N 0 N = 0
33 0le1 0 1
34 32 33 eqbrtrdi N 0 N 1
35 oveq2 N = 0 0 N = 0 0
36 0exp0e1 0 0 = 1
37 1le1 1 1
38 36 37 eqbrtri 0 0 1
39 35 38 eqbrtrdi N = 0 0 N 1
40 34 39 jaoi N N = 0 0 N 1
41 31 40 sylbi N 0 0 N 1
42 1nn 1
43 nnmulcl 1 N ! 1 N !
44 42 23 43 sylancr N 0 1 N !
45 44 nnge1d N 0 1 1 N !
46 0re 0
47 reexpcl 0 N 0 0 N
48 46 47 mpan N 0 0 N
49 1re 1
50 remulcl 1 N ! 1 N !
51 49 24 50 sylancr N 0 1 N !
52 letr 0 N 1 1 N ! 0 N 1 1 1 N ! 0 N 1 N !
53 49 52 mp3an2 0 N 1 N ! 0 N 1 1 1 N ! 0 N 1 N !
54 48 51 53 syl2anc N 0 0 N 1 1 1 N ! 0 N 1 N !
55 41 45 54 mp2and N 0 0 N 1 N !
56 55 adantl M = 0 N 0 0 N 1 N !
57 oveq1 M = 0 M N = 0 N
58 oveq12 M = 0 M = 0 M M = 0 0
59 58 anidms M = 0 M M = 0 0
60 59 36 syl6eq M = 0 M M = 1
61 60 oveq1d M = 0 M M N ! = 1 N !
62 57 61 breq12d M = 0 M N M M N ! 0 N 1 N !
63 62 adantr M = 0 N 0 M N M M N ! 0 N 1 N !
64 56 63 mpbird M = 0 N 0 M N M M N !
65 30 64 jaoian M M = 0 N 0 M N M M N !
66 1 65 sylanb M 0 N 0 M N M M N !