Metamath Proof Explorer


Theorem facubnd

Description: An upper bound for the factorial function. (Contributed by Mario Carneiro, 15-Apr-2016)

Ref Expression
Assertion facubnd N 0 N ! N N

Proof

Step Hyp Ref Expression
1 fveq2 m = 0 m ! = 0 !
2 fac0 0 ! = 1
3 1 2 eqtrdi m = 0 m ! = 1
4 id m = 0 m = 0
5 4 4 oveq12d m = 0 m m = 0 0
6 0exp0e1 0 0 = 1
7 5 6 eqtrdi m = 0 m m = 1
8 3 7 breq12d m = 0 m ! m m 1 1
9 fveq2 m = k m ! = k !
10 id m = k m = k
11 10 10 oveq12d m = k m m = k k
12 9 11 breq12d m = k m ! m m k ! k k
13 fveq2 m = k + 1 m ! = k + 1 !
14 id m = k + 1 m = k + 1
15 14 14 oveq12d m = k + 1 m m = k + 1 k + 1
16 13 15 breq12d m = k + 1 m ! m m k + 1 ! k + 1 k + 1
17 fveq2 m = N m ! = N !
18 id m = N m = N
19 18 18 oveq12d m = N m m = N N
20 17 19 breq12d m = N m ! m m N ! N N
21 1le1 1 1
22 faccl k 0 k !
23 22 adantr k 0 k ! k k k !
24 23 nnred k 0 k ! k k k !
25 nn0re k 0 k
26 25 adantr k 0 k ! k k k
27 simpl k 0 k ! k k k 0
28 26 27 reexpcld k 0 k ! k k k k
29 nn0p1nn k 0 k + 1
30 29 adantr k 0 k ! k k k + 1
31 30 nnred k 0 k ! k k k + 1
32 31 27 reexpcld k 0 k ! k k k + 1 k
33 simpr k 0 k ! k k k ! k k
34 nn0ge0 k 0 0 k
35 34 adantr k 0 k ! k k 0 k
36 26 lep1d k 0 k ! k k k k + 1
37 leexp1a k k + 1 k 0 0 k k k + 1 k k k + 1 k
38 26 31 27 35 36 37 syl32anc k 0 k ! k k k k k + 1 k
39 24 28 32 33 38 letrd k 0 k ! k k k ! k + 1 k
40 30 nngt0d k 0 k ! k k 0 < k + 1
41 lemul1 k ! k + 1 k k + 1 0 < k + 1 k ! k + 1 k k ! k + 1 k + 1 k k + 1
42 24 32 31 40 41 syl112anc k 0 k ! k k k ! k + 1 k k ! k + 1 k + 1 k k + 1
43 39 42 mpbid k 0 k ! k k k ! k + 1 k + 1 k k + 1
44 facp1 k 0 k + 1 ! = k ! k + 1
45 44 adantr k 0 k ! k k k + 1 ! = k ! k + 1
46 30 nncnd k 0 k ! k k k + 1
47 46 27 expp1d k 0 k ! k k k + 1 k + 1 = k + 1 k k + 1
48 43 45 47 3brtr4d k 0 k ! k k k + 1 ! k + 1 k + 1
49 48 ex k 0 k ! k k k + 1 ! k + 1 k + 1
50 8 12 16 20 21 49 nn0ind N 0 N ! N N