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∈ℕ0∧M∈ℕ0→N!⁢N+1M≤N+M!

Proof

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