Metamath Proof Explorer

Theorem faclbnd6

Description: Geometric lower bound for the factorial function, where N is usually held constant. (Contributed by Paul Chapman, 28-Dec-2007)

Ref Expression
Assertion faclbnd6 
|- ( ( N e. NN0 /\ M e. NN0 ) -> ( ( ! ` N ) x. ( ( N + 1 ) ^ M ) ) <_ ( ! ` ( N + M ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( m = 0 -> ( ( N + 1 ) ^ m ) = ( ( N + 1 ) ^ 0 ) )
2 1 oveq2d 
 |-  ( m = 0 -> ( ( ! ` N ) x. ( ( N + 1 ) ^ m ) ) = ( ( ! ` N ) x. ( ( N + 1 ) ^ 0 ) ) )
3 oveq2 
 |-  ( m = 0 -> ( N + m ) = ( N + 0 ) )
4 3 fveq2d 
 |-  ( m = 0 -> ( ! ` ( N + m ) ) = ( ! ` ( N + 0 ) ) )
5 2 4 breq12d 
 |-  ( m = 0 -> ( ( ( ! ` N ) x. ( ( N + 1 ) ^ m ) ) <_ ( ! ` ( N + m ) ) <-> ( ( ! ` N ) x. ( ( N + 1 ) ^ 0 ) ) <_ ( ! ` ( N + 0 ) ) ) )
6 oveq2 
 |-  ( m = k -> ( ( N + 1 ) ^ m ) = ( ( N + 1 ) ^ k ) )
7 6 oveq2d 
 |-  ( m = k -> ( ( ! ` N ) x. ( ( N + 1 ) ^ m ) ) = ( ( ! ` N ) x. ( ( N + 1 ) ^ k ) ) )
8 oveq2 
 |-  ( m = k -> ( N + m ) = ( N + k ) )
9 8 fveq2d 
 |-  ( m = k -> ( ! ` ( N + m ) ) = ( ! ` ( N + k ) ) )
10 7 9 breq12d 
 |-  ( m = k -> ( ( ( ! ` N ) x. ( ( N + 1 ) ^ m ) ) <_ ( ! ` ( N + m ) ) <-> ( ( ! ` N ) x. ( ( N + 1 ) ^ k ) ) <_ ( ! ` ( N + k ) ) ) )
11 oveq2 
 |-  ( m = ( k + 1 ) -> ( ( N + 1 ) ^ m ) = ( ( N + 1 ) ^ ( k + 1 ) ) )
12 11 oveq2d 
 |-  ( m = ( k + 1 ) -> ( ( ! ` N ) x. ( ( N + 1 ) ^ m ) ) = ( ( ! ` N ) x. ( ( N + 1 ) ^ ( k + 1 ) ) ) )
13 oveq2 
 |-  ( m = ( k + 1 ) -> ( N + m ) = ( N + ( k + 1 ) ) )
14 13 fveq2d 
 |-  ( m = ( k + 1 ) -> ( ! ` ( N + m ) ) = ( ! ` ( N + ( k + 1 ) ) ) )
15 12 14 breq12d 
 |-  ( m = ( k + 1 ) -> ( ( ( ! ` N ) x. ( ( N + 1 ) ^ m ) ) <_ ( ! ` ( N + m ) ) <-> ( ( ! ` N ) x. ( ( N + 1 ) ^ ( k + 1 ) ) ) <_ ( ! ` ( N + ( k + 1 ) ) ) ) )
16 oveq2 
 |-  ( m = M -> ( ( N + 1 ) ^ m ) = ( ( N + 1 ) ^ M ) )
17 16 oveq2d 
 |-  ( m = M -> ( ( ! ` N ) x. ( ( N + 1 ) ^ m ) ) = ( ( ! ` N ) x. ( ( N + 1 ) ^ M ) ) )
18 oveq2 
 |-  ( m = M -> ( N + m ) = ( N + M ) )
19 18 fveq2d 
 |-  ( m = M -> ( ! ` ( N + m ) ) = ( ! ` ( N + M ) ) )
20 17 19 breq12d 
 |-  ( m = M -> ( ( ( ! ` N ) x. ( ( N + 1 ) ^ m ) ) <_ ( ! ` ( N + m ) ) <-> ( ( ! ` N ) x. ( ( N + 1 ) ^ M ) ) <_ ( ! ` ( N + M ) ) ) )
21 faccl 
 |-  ( N e. NN0 -> ( ! ` N ) e. NN )
22 21 nnred 
 |-  ( N e. NN0 -> ( ! ` N ) e. RR )
23 22 leidd 
 |-  ( N e. NN0 -> ( ! ` N ) <_ ( ! ` N ) )
24 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
25 peano2cn 
 |-  ( N e. CC -> ( N + 1 ) e. CC )
26 24 25 syl 
 |-  ( N e. NN0 -> ( N + 1 ) e. CC )
27 26 exp0d 
 |-  ( N e. NN0 -> ( ( N + 1 ) ^ 0 ) = 1 )
28 27 oveq2d 
 |-  ( N e. NN0 -> ( ( ! ` N ) x. ( ( N + 1 ) ^ 0 ) ) = ( ( ! ` N ) x. 1 ) )
29 21 nncnd 
 |-  ( N e. NN0 -> ( ! ` N ) e. CC )
30 29 mulid1d 
 |-  ( N e. NN0 -> ( ( ! ` N ) x. 1 ) = ( ! ` N ) )
31 28 30 eqtrd 
 |-  ( N e. NN0 -> ( ( ! ` N ) x. ( ( N + 1 ) ^ 0 ) ) = ( ! ` N ) )
32 24 addid1d 
 |-  ( N e. NN0 -> ( N + 0 ) = N )
33 32 fveq2d 
 |-  ( N e. NN0 -> ( ! ` ( N + 0 ) ) = ( ! ` N ) )
34 23 31 33 3brtr4d 
 |-  ( N e. NN0 -> ( ( ! ` N ) x. ( ( N + 1 ) ^ 0 ) ) <_ ( ! ` ( N + 0 ) ) )
35 22 adantr 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ! ` N ) e. RR )
36 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
37 36 nn0red 
 |-  ( N e. NN0 -> ( N + 1 ) e. RR )
38 reexpcl 
 |-  ( ( ( N + 1 ) e. RR /\ k e. NN0 ) -> ( ( N + 1 ) ^ k ) e. RR )
39 37 38 sylan 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( N + 1 ) ^ k ) e. RR )
40 35 39 remulcld 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( ! ` N ) x. ( ( N + 1 ) ^ k ) ) e. RR )
41 nnnn0 
 |-  ( ( ! ` N ) e. NN -> ( ! ` N ) e. NN0 )
42 41 nn0ge0d 
 |-  ( ( ! ` N ) e. NN -> 0 <_ ( ! ` N ) )
43 21 42 syl 
 |-  ( N e. NN0 -> 0 <_ ( ! ` N ) )
44 43 adantr 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> 0 <_ ( ! ` N ) )
45 37 adantr 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( N + 1 ) e. RR )
46 simpr 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> k e. NN0 )
47 36 nn0ge0d 
 |-  ( N e. NN0 -> 0 <_ ( N + 1 ) )
48 47 adantr 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> 0 <_ ( N + 1 ) )
49 45 46 48 expge0d 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> 0 <_ ( ( N + 1 ) ^ k ) )
50 35 39 44 49 mulge0d 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> 0 <_ ( ( ! ` N ) x. ( ( N + 1 ) ^ k ) ) )
51 40 50 jca 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( ( ! ` N ) x. ( ( N + 1 ) ^ k ) ) e. RR /\ 0 <_ ( ( ! ` N ) x. ( ( N + 1 ) ^ k ) ) ) )
52 nn0addcl 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( N + k ) e. NN0 )
53 52 faccld 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ! ` ( N + k ) ) e. NN )
54 53 nnred 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ! ` ( N + k ) ) e. RR )
55 nn0re 
 |-  ( N e. NN0 -> N e. RR )
56 peano2nn0 
 |-  ( k e. NN0 -> ( k + 1 ) e. NN0 )
57 56 nn0red 
 |-  ( k e. NN0 -> ( k + 1 ) e. RR )
58 readdcl 
 |-  ( ( N e. RR /\ ( k + 1 ) e. RR ) -> ( N + ( k + 1 ) ) e. RR )
59 55 57 58 syl2an 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( N + ( k + 1 ) ) e. RR )
60 45 48 59 jca31 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( ( N + 1 ) e. RR /\ 0 <_ ( N + 1 ) ) /\ ( N + ( k + 1 ) ) e. RR ) )
61 51 54 60 jca31 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( ( ( ( ! ` N ) x. ( ( N + 1 ) ^ k ) ) e. RR /\ 0 <_ ( ( ! ` N ) x. ( ( N + 1 ) ^ k ) ) ) /\ ( ! ` ( N + k ) ) e. RR ) /\ ( ( ( N + 1 ) e. RR /\ 0 <_ ( N + 1 ) ) /\ ( N + ( k + 1 ) ) e. RR ) ) )
62 61 adantr 
 |-  ( ( ( N e. NN0 /\ k e. NN0 ) /\ ( ( ! ` N ) x. ( ( N + 1 ) ^ k ) ) <_ ( ! ` ( N + k ) ) ) -> ( ( ( ( ( ! ` N ) x. ( ( N + 1 ) ^ k ) ) e. RR /\ 0 <_ ( ( ! ` N ) x. ( ( N + 1 ) ^ k ) ) ) /\ ( ! ` ( N + k ) ) e. RR ) /\ ( ( ( N + 1 ) e. RR /\ 0 <_ ( N + 1 ) ) /\ ( N + ( k + 1 ) ) e. RR ) ) )
63 32 adantr 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( N + 0 ) = N )
64 nn0ge0 
 |-  ( k e. NN0 -> 0 <_ k )
65 64 adantl 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> 0 <_ k )
66 0re 
 |-  0 e. RR
67 nn0re 
 |-  ( k e. NN0 -> k e. RR )
68 67 adantl 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> k e. RR )
69 55 adantr 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> N e. RR )
70 leadd2 
 |-  ( ( 0 e. RR /\ k e. RR /\ N e. RR ) -> ( 0 <_ k <-> ( N + 0 ) <_ ( N + k ) ) )
71 66 68 69 70 mp3an2i 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( 0 <_ k <-> ( N + 0 ) <_ ( N + k ) ) )
72 65 71 mpbid 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( N + 0 ) <_ ( N + k ) )
73 63 72 eqbrtrrd 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> N <_ ( N + k ) )
74 52 nn0red 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( N + k ) e. RR )
75 1re 
 |-  1 e. RR
76 leadd1 
 |-  ( ( N e. RR /\ ( N + k ) e. RR /\ 1 e. RR ) -> ( N <_ ( N + k ) <-> ( N + 1 ) <_ ( ( N + k ) + 1 ) ) )
77 75 76 mp3an3 
 |-  ( ( N e. RR /\ ( N + k ) e. RR ) -> ( N <_ ( N + k ) <-> ( N + 1 ) <_ ( ( N + k ) + 1 ) ) )
78 69 74 77 syl2anc 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( N <_ ( N + k ) <-> ( N + 1 ) <_ ( ( N + k ) + 1 ) ) )
79 73 78 mpbid 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( N + 1 ) <_ ( ( N + k ) + 1 ) )
80 nn0cn 
 |-  ( k e. NN0 -> k e. CC )
81 ax-1cn 
 |-  1 e. CC
82 addass 
 |-  ( ( N e. CC /\ k e. CC /\ 1 e. CC ) -> ( ( N + k ) + 1 ) = ( N + ( k + 1 ) ) )
83 81 82 mp3an3 
 |-  ( ( N e. CC /\ k e. CC ) -> ( ( N + k ) + 1 ) = ( N + ( k + 1 ) ) )
84 24 80 83 syl2an 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( N + k ) + 1 ) = ( N + ( k + 1 ) ) )
85 79 84 breqtrd 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( N + 1 ) <_ ( N + ( k + 1 ) ) )
86 85 anim1ci 
 |-  ( ( ( N e. NN0 /\ k e. NN0 ) /\ ( ( ! ` N ) x. ( ( N + 1 ) ^ k ) ) <_ ( ! ` ( N + k ) ) ) -> ( ( ( ! ` N ) x. ( ( N + 1 ) ^ k ) ) <_ ( ! ` ( N + k ) ) /\ ( N + 1 ) <_ ( N + ( k + 1 ) ) ) )
87 lemul12a 
 |-  ( ( ( ( ( ( ! ` N ) x. ( ( N + 1 ) ^ k ) ) e. RR /\ 0 <_ ( ( ! ` N ) x. ( ( N + 1 ) ^ k ) ) ) /\ ( ! ` ( N + k ) ) e. RR ) /\ ( ( ( N + 1 ) e. RR /\ 0 <_ ( N + 1 ) ) /\ ( N + ( k + 1 ) ) e. RR ) ) -> ( ( ( ( ! ` N ) x. ( ( N + 1 ) ^ k ) ) <_ ( ! ` ( N + k ) ) /\ ( N + 1 ) <_ ( N + ( k + 1 ) ) ) -> ( ( ( ! ` N ) x. ( ( N + 1 ) ^ k ) ) x. ( N + 1 ) ) <_ ( ( ! ` ( N + k ) ) x. ( N + ( k + 1 ) ) ) ) )
88 62 86 87 sylc 
 |-  ( ( ( N e. NN0 /\ k e. NN0 ) /\ ( ( ! ` N ) x. ( ( N + 1 ) ^ k ) ) <_ ( ! ` ( N + k ) ) ) -> ( ( ( ! ` N ) x. ( ( N + 1 ) ^ k ) ) x. ( N + 1 ) ) <_ ( ( ! ` ( N + k ) ) x. ( N + ( k + 1 ) ) ) )
89 expp1 
 |-  ( ( ( N + 1 ) e. CC /\ k e. NN0 ) -> ( ( N + 1 ) ^ ( k + 1 ) ) = ( ( ( N + 1 ) ^ k ) x. ( N + 1 ) ) )
90 26 89 sylan 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( N + 1 ) ^ ( k + 1 ) ) = ( ( ( N + 1 ) ^ k ) x. ( N + 1 ) ) )
91 90 oveq2d 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( ! ` N ) x. ( ( N + 1 ) ^ ( k + 1 ) ) ) = ( ( ! ` N ) x. ( ( ( N + 1 ) ^ k ) x. ( N + 1 ) ) ) )
92 29 adantr 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ! ` N ) e. CC )
93 expcl 
 |-  ( ( ( N + 1 ) e. CC /\ k e. NN0 ) -> ( ( N + 1 ) ^ k ) e. CC )
94 26 93 sylan 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( N + 1 ) ^ k ) e. CC )
95 26 adantr 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( N + 1 ) e. CC )
96 92 94 95 mulassd 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( ( ! ` N ) x. ( ( N + 1 ) ^ k ) ) x. ( N + 1 ) ) = ( ( ! ` N ) x. ( ( ( N + 1 ) ^ k ) x. ( N + 1 ) ) ) )
97 91 96 eqtr4d 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( ! ` N ) x. ( ( N + 1 ) ^ ( k + 1 ) ) ) = ( ( ( ! ` N ) x. ( ( N + 1 ) ^ k ) ) x. ( N + 1 ) ) )
98 97 adantr 
 |-  ( ( ( N e. NN0 /\ k e. NN0 ) /\ ( ( ! ` N ) x. ( ( N + 1 ) ^ k ) ) <_ ( ! ` ( N + k ) ) ) -> ( ( ! ` N ) x. ( ( N + 1 ) ^ ( k + 1 ) ) ) = ( ( ( ! ` N ) x. ( ( N + 1 ) ^ k ) ) x. ( N + 1 ) ) )
99 facp1 
 |-  ( ( N + k ) e. NN0 -> ( ! ` ( ( N + k ) + 1 ) ) = ( ( ! ` ( N + k ) ) x. ( ( N + k ) + 1 ) ) )
100 52 99 syl 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ! ` ( ( N + k ) + 1 ) ) = ( ( ! ` ( N + k ) ) x. ( ( N + k ) + 1 ) ) )
101 84 fveq2d 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ! ` ( ( N + k ) + 1 ) ) = ( ! ` ( N + ( k + 1 ) ) ) )
102 84 oveq2d 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ( ! ` ( N + k ) ) x. ( ( N + k ) + 1 ) ) = ( ( ! ` ( N + k ) ) x. ( N + ( k + 1 ) ) ) )
103 100 101 102 3eqtr3d 
 |-  ( ( N e. NN0 /\ k e. NN0 ) -> ( ! ` ( N + ( k + 1 ) ) ) = ( ( ! ` ( N + k ) ) x. ( N + ( k + 1 ) ) ) )
104 103 adantr 
 |-  ( ( ( N e. NN0 /\ k e. NN0 ) /\ ( ( ! ` N ) x. ( ( N + 1 ) ^ k ) ) <_ ( ! ` ( N + k ) ) ) -> ( ! ` ( N + ( k + 1 ) ) ) = ( ( ! ` ( N + k ) ) x. ( N + ( k + 1 ) ) ) )
105 88 98 104 3brtr4d 
 |-  ( ( ( N e. NN0 /\ k e. NN0 ) /\ ( ( ! ` N ) x. ( ( N + 1 ) ^ k ) ) <_ ( ! ` ( N + k ) ) ) -> ( ( ! ` N ) x. ( ( N + 1 ) ^ ( k + 1 ) ) ) <_ ( ! ` ( N + ( k + 1 ) ) ) )
106 5 10 15 20 34 105 nn0indd 
 |-  ( ( N e. NN0 /\ M e. NN0 ) -> ( ( ! ` N ) x. ( ( N + 1 ) ^ M ) ) <_ ( ! ` ( N + M ) ) )