faclbnd

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

		Ref	Expression
	Assertion	faclbnd	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to M^{N + 1} \leq M^{M} N!$

Proof

Step	Hyp	Ref	Expression
1		elnn0	$⊢ M \in ℕ_{0} \leftrightarrow (M \in ℕ \lor M = 0)$
2		oveq1	$⊢ j = 0 \to j + 1 = 0 + 1$
3	2	oveq2d	$⊢ j = 0 \to M^{j + 1} = M^{0 + 1}$
4		fveq2	$⊢ j = 0 \to j! = 0!$
5	4	oveq2d	$⊢ j = 0 \to M^{M} j! = M^{M} 0!$
6	3 5	breq12d	$⊢ j = 0 \to (M^{j + 1} \leq M^{M} j! \leftrightarrow M^{0 + 1} \leq M^{M} 0!)$
7	6	imbi2d	$⊢ j = 0 \to ((M \in ℕ \to M^{j + 1} \leq M^{M} j!) \leftrightarrow (M \in ℕ \to M^{0 + 1} \leq M^{M} 0!))$
8		oveq1	$⊢ j = k \to j + 1 = k + 1$
9	8	oveq2d	$⊢ j = k \to M^{j + 1} = M^{k + 1}$
10		fveq2	$⊢ j = k \to j! = k!$
11	10	oveq2d	$⊢ j = k \to M^{M} j! = M^{M} k!$
12	9 11	breq12d	$⊢ j = k \to (M^{j + 1} \leq M^{M} j! \leftrightarrow M^{k + 1} \leq M^{M} k!)$
13	12	imbi2d	$⊢ j = k \to ((M \in ℕ \to M^{j + 1} \leq M^{M} j!) \leftrightarrow (M \in ℕ \to M^{k + 1} \leq M^{M} k!))$
14		oveq1	$⊢ j = k + 1 \to j + 1 = k + 1 + 1$
15	14	oveq2d	$⊢ j = k + 1 \to M^{j + 1} = M^{k + 1 + 1}$
16		fveq2	$⊢ j = k + 1 \to j! = (k + 1)!$
17	16	oveq2d	$⊢ j = k + 1 \to M^{M} j! = M^{M} (k + 1)!$
18	15 17	breq12d	$⊢ j = k + 1 \to (M^{j + 1} \leq M^{M} j! \leftrightarrow M^{k + 1 + 1} \leq M^{M} (k + 1)!)$
19	18	imbi2d	$⊢ j = k + 1 \to ((M \in ℕ \to M^{j + 1} \leq M^{M} j!) \leftrightarrow (M \in ℕ \to M^{k + 1 + 1} \leq M^{M} (k + 1)!))$
20		oveq1	$⊢ j = N \to j + 1 = N + 1$
21	20	oveq2d	$⊢ j = N \to M^{j + 1} = M^{N + 1}$
22		fveq2	$⊢ j = N \to j! = N!$
23	22	oveq2d	$⊢ j = N \to M^{M} j! = M^{M} N!$
24	21 23	breq12d	$⊢ j = N \to (M^{j + 1} \leq M^{M} j! \leftrightarrow M^{N + 1} \leq M^{M} N!)$
25	24	imbi2d	$⊢ j = N \to ((M \in ℕ \to M^{j + 1} \leq M^{M} j!) \leftrightarrow (M \in ℕ \to M^{N + 1} \leq M^{M} N!))$
26		nnre	$⊢ M \in ℕ \to M \in ℝ$
27		nnge1	$⊢ M \in ℕ \to 1 \leq M$
28		elnnuz	$⊢ M \in ℕ \leftrightarrow M \in ℤ_{\geq 1}$
29	28	biimpi	$⊢ M \in ℕ \to M \in ℤ_{\geq 1}$
30	26 27 29	leexp2ad	$⊢ M \in ℕ \to M^{1} \leq M^{M}$
31		0p1e1	$⊢ 0 + 1 = 1$
32	31	oveq2i	$⊢ M^{0 + 1} = M^{1}$
33	32	a1i	$⊢ M \in ℕ \to M^{0 + 1} = M^{1}$
34		fac0	$⊢ 0! = 1$
35	34	oveq2i	$⊢ M^{M} 0! = M^{M} \cdot 1$
36		nnnn0	$⊢ M \in ℕ \to M \in ℕ_{0}$
37	26 36	reexpcld	$⊢ M \in ℕ \to M^{M} \in ℝ$
38	37	recnd	$⊢ M \in ℕ \to M^{M} \in ℂ$
39	38	mulridd	$⊢ M \in ℕ \to M^{M} \cdot 1 = M^{M}$
40	35 39	eqtrid	$⊢ M \in ℕ \to M^{M} 0! = M^{M}$
41	30 33 40	3brtr4d	$⊢ M \in ℕ \to M^{0 + 1} \leq M^{M} 0!$
42	26	ad3antrrr	$⊢ (((M \in ℕ \land k \in ℕ_{0}) \land M^{k + 1} \leq M^{M} k!) \land ((M \in ℕ \land k \in ℕ_{0}) \land M \leq k + 1)) \to M \in ℝ$
43		simpllr	$⊢ (((M \in ℕ \land k \in ℕ_{0}) \land M^{k + 1} \leq M^{M} k!) \land ((M \in ℕ \land k \in ℕ_{0}) \land M \leq k + 1)) \to k \in ℕ_{0}$
44		peano2nn0	$⊢ k \in ℕ_{0} \to k + 1 \in ℕ_{0}$
45	43 44	syl	$⊢ (((M \in ℕ \land k \in ℕ_{0}) \land M^{k + 1} \leq M^{M} k!) \land ((M \in ℕ \land k \in ℕ_{0}) \land M \leq k + 1)) \to k + 1 \in ℕ_{0}$
46	42 45	reexpcld	$⊢ (((M \in ℕ \land k \in ℕ_{0}) \land M^{k + 1} \leq M^{M} k!) \land ((M \in ℕ \land k \in ℕ_{0}) \land M \leq k + 1)) \to M^{k + 1} \in ℝ$
47	36	ad3antrrr	$⊢ (((M \in ℕ \land k \in ℕ_{0}) \land M^{k + 1} \leq M^{M} k!) \land ((M \in ℕ \land k \in ℕ_{0}) \land M \leq k + 1)) \to M \in ℕ_{0}$
48	42 47	reexpcld	$⊢ (((M \in ℕ \land k \in ℕ_{0}) \land M^{k + 1} \leq M^{M} k!) \land ((M \in ℕ \land k \in ℕ_{0}) \land M \leq k + 1)) \to M^{M} \in ℝ$
49	43	faccld	$⊢ (((M \in ℕ \land k \in ℕ_{0}) \land M^{k + 1} \leq M^{M} k!) \land ((M \in ℕ \land k \in ℕ_{0}) \land M \leq k + 1)) \to k! \in ℕ$
50	49	nnred	$⊢ (((M \in ℕ \land k \in ℕ_{0}) \land M^{k + 1} \leq M^{M} k!) \land ((M \in ℕ \land k \in ℕ_{0}) \land M \leq k + 1)) \to k! \in ℝ$
51	48 50	remulcld	$⊢ (((M \in ℕ \land k \in ℕ_{0}) \land M^{k + 1} \leq M^{M} k!) \land ((M \in ℕ \land k \in ℕ_{0}) \land M \leq k + 1)) \to M^{M} k! \in ℝ$
52		nn0re	$⊢ k \in ℕ_{0} \to k \in ℝ$
53		peano2re	$⊢ k \in ℝ \to k + 1 \in ℝ$
54	43 52 53	3syl	$⊢ (((M \in ℕ \land k \in ℕ_{0}) \land M^{k + 1} \leq M^{M} k!) \land ((M \in ℕ \land k \in ℕ_{0}) \land M \leq k + 1)) \to k + 1 \in ℝ$
55		nngt0	$⊢ M \in ℕ \to 0 < M$
56	55	ad3antrrr	$⊢ (((M \in ℕ \land k \in ℕ_{0}) \land M^{k + 1} \leq M^{M} k!) \land ((M \in ℕ \land k \in ℕ_{0}) \land M \leq k + 1)) \to 0 < M$
57		0re	$⊢ 0 \in ℝ$
58		ltle	$⊢ (0 \in ℝ \land M \in ℝ) \to (0 < M \to 0 \leq M)$
59	57 58	mpan	$⊢ M \in ℝ \to (0 < M \to 0 \leq M)$
60	42 56 59	sylc	$⊢ (((M \in ℕ \land k \in ℕ_{0}) \land M^{k + 1} \leq M^{M} k!) \land ((M \in ℕ \land k \in ℕ_{0}) \land M \leq k + 1)) \to 0 \leq M$
61	42 45 60	expge0d	$⊢ (((M \in ℕ \land k \in ℕ_{0}) \land M^{k + 1} \leq M^{M} k!) \land ((M \in ℕ \land k \in ℕ_{0}) \land M \leq k + 1)) \to 0 \leq M^{k + 1}$
62		simplr	$⊢ (((M \in ℕ \land k \in ℕ_{0}) \land M^{k + 1} \leq M^{M} k!) \land ((M \in ℕ \land k \in ℕ_{0}) \land M \leq k + 1)) \to M^{k + 1} \leq M^{M} k!$
63		simprr	$⊢ (((M \in ℕ \land k \in ℕ_{0}) \land M^{k + 1} \leq M^{M} k!) \land ((M \in ℕ \land k \in ℕ_{0}) \land M \leq k + 1)) \to M \leq k + 1$
64	46 51 42 54 61 60 62 63	lemul12ad	$⊢ (((M \in ℕ \land k \in ℕ_{0}) \land M^{k + 1} \leq M^{M} k!) \land ((M \in ℕ \land k \in ℕ_{0}) \land M \leq k + 1)) \to M^{k + 1} \cdot M \leq M^{M} k! (k + 1)$
65	64	anandis	$⊢ ((M \in ℕ \land k \in ℕ_{0}) \land (M^{k + 1} \leq M^{M} k! \land M \leq k + 1)) \to M^{k + 1} \cdot M \leq M^{M} k! (k + 1)$
66		nncn	$⊢ M \in ℕ \to M \in ℂ$
67		expp1	$⊢ (M \in ℂ \land k + 1 \in ℕ_{0}) \to M^{k + 1 + 1} = M^{k + 1} \cdot M$
68	66 44 67	syl2an	$⊢ (M \in ℕ \land k \in ℕ_{0}) \to M^{k + 1 + 1} = M^{k + 1} \cdot M$
69	68	adantr	$⊢ ((M \in ℕ \land k \in ℕ_{0}) \land (M^{k + 1} \leq M^{M} k! \land M \leq k + 1)) \to M^{k + 1 + 1} = M^{k + 1} \cdot M$
70		facp1	$⊢ k \in ℕ_{0} \to (k + 1)! = k! (k + 1)$
71	70	adantl	$⊢ (M \in ℕ \land k \in ℕ_{0}) \to (k + 1)! = k! (k + 1)$
72	71	oveq2d	$⊢ (M \in ℕ \land k \in ℕ_{0}) \to M^{M} (k + 1)! = M^{M} k! (k + 1)$
73	38	adantr	$⊢ (M \in ℕ \land k \in ℕ_{0}) \to M^{M} \in ℂ$
74		faccl	$⊢ k \in ℕ_{0} \to k! \in ℕ$
75	74	nncnd	$⊢ k \in ℕ_{0} \to k! \in ℂ$
76	75	adantl	$⊢ (M \in ℕ \land k \in ℕ_{0}) \to k! \in ℂ$
77		nn0cn	$⊢ k \in ℕ_{0} \to k \in ℂ$
78		peano2cn	$⊢ k \in ℂ \to k + 1 \in ℂ$
79	77 78	syl	$⊢ k \in ℕ_{0} \to k + 1 \in ℂ$
80	79	adantl	$⊢ (M \in ℕ \land k \in ℕ_{0}) \to k + 1 \in ℂ$
81	73 76 80	mulassd	$⊢ (M \in ℕ \land k \in ℕ_{0}) \to M^{M} k! (k + 1) = M^{M} k! (k + 1)$
82	72 81	eqtr4d	$⊢ (M \in ℕ \land k \in ℕ_{0}) \to M^{M} (k + 1)! = M^{M} k! (k + 1)$
83	82	adantr	$⊢ ((M \in ℕ \land k \in ℕ_{0}) \land (M^{k + 1} \leq M^{M} k! \land M \leq k + 1)) \to M^{M} (k + 1)! = M^{M} k! (k + 1)$
84	65 69 83	3brtr4d	$⊢ ((M \in ℕ \land k \in ℕ_{0}) \land (M^{k + 1} \leq M^{M} k! \land M \leq k + 1)) \to M^{k + 1 + 1} \leq M^{M} (k + 1)!$
85	84	exp32	$⊢ (M \in ℕ \land k \in ℕ_{0}) \to (M^{k + 1} \leq M^{M} k! \to (M \leq k + 1 \to M^{k + 1 + 1} \leq M^{M} (k + 1)!))$
86	85	com23	$⊢ (M \in ℕ \land k \in ℕ_{0}) \to (M \leq k + 1 \to (M^{k + 1} \leq M^{M} k! \to M^{k + 1 + 1} \leq M^{M} (k + 1)!))$
87		nn0ltp1le	$⊢ (k + 1 \in ℕ_{0} \land M \in ℕ_{0}) \to (k + 1 < M \leftrightarrow k + 1 + 1 \leq M)$
88	44 36 87	syl2anr	$⊢ (M \in ℕ \land k \in ℕ_{0}) \to (k + 1 < M \leftrightarrow k + 1 + 1 \leq M)$
89		peano2nn0	$⊢ k + 1 \in ℕ_{0} \to k + 1 + 1 \in ℕ_{0}$
90	44 89	syl	$⊢ k \in ℕ_{0} \to k + 1 + 1 \in ℕ_{0}$
91		reexpcl	$⊢ (M \in ℝ \land k + 1 + 1 \in ℕ_{0}) \to M^{k + 1 + 1} \in ℝ$
92	26 90 91	syl2an	$⊢ (M \in ℕ \land k \in ℕ_{0}) \to M^{k + 1 + 1} \in ℝ$
93	92	adantr	$⊢ ((M \in ℕ \land k \in ℕ_{0}) \land k + 1 + 1 \leq M) \to M^{k + 1 + 1} \in ℝ$
94	37	ad2antrr	$⊢ ((M \in ℕ \land k \in ℕ_{0}) \land k + 1 + 1 \leq M) \to M^{M} \in ℝ$
95	44	faccld	$⊢ k \in ℕ_{0} \to (k + 1)! \in ℕ$
96	95	nnred	$⊢ k \in ℕ_{0} \to (k + 1)! \in ℝ$
97		remulcl	$⊢ (M^{M} \in ℝ \land (k + 1)! \in ℝ) \to M^{M} (k + 1)! \in ℝ$
98	37 96 97	syl2an	$⊢ (M \in ℕ \land k \in ℕ_{0}) \to M^{M} (k + 1)! \in ℝ$
99	98	adantr	$⊢ ((M \in ℕ \land k \in ℕ_{0}) \land k + 1 + 1 \leq M) \to M^{M} (k + 1)! \in ℝ$
100	26	ad2antrr	$⊢ ((M \in ℕ \land k \in ℕ_{0}) \land k + 1 + 1 \leq M) \to M \in ℝ$
101	27	ad2antrr	$⊢ ((M \in ℕ \land k \in ℕ_{0}) \land k + 1 + 1 \leq M) \to 1 \leq M$
102		simpr	$⊢ ((M \in ℕ \land k \in ℕ_{0}) \land k + 1 + 1 \leq M) \to k + 1 + 1 \leq M$
103	90	ad2antlr	$⊢ ((M \in ℕ \land k \in ℕ_{0}) \land k + 1 + 1 \leq M) \to k + 1 + 1 \in ℕ_{0}$
104	103	nn0zd	$⊢ ((M \in ℕ \land k \in ℕ_{0}) \land k + 1 + 1 \leq M) \to k + 1 + 1 \in ℤ$
105		nnz	$⊢ M \in ℕ \to M \in ℤ$
106	105	ad2antrr	$⊢ ((M \in ℕ \land k \in ℕ_{0}) \land k + 1 + 1 \leq M) \to M \in ℤ$
107		eluz	$⊢ (k + 1 + 1 \in ℤ \land M \in ℤ) \to (M \in ℤ_{\geq (k + 1 + 1)} \leftrightarrow k + 1 + 1 \leq M)$
108	104 106 107	syl2anc	$⊢ ((M \in ℕ \land k \in ℕ_{0}) \land k + 1 + 1 \leq M) \to (M \in ℤ_{\geq (k + 1 + 1)} \leftrightarrow k + 1 + 1 \leq M)$
109	102 108	mpbird	$⊢ ((M \in ℕ \land k \in ℕ_{0}) \land k + 1 + 1 \leq M) \to M \in ℤ_{\geq (k + 1 + 1)}$
110	100 101 109	leexp2ad	$⊢ ((M \in ℕ \land k \in ℕ_{0}) \land k + 1 + 1 \leq M) \to M^{k + 1 + 1} \leq M^{M}$
111	37 96	anim12i	$⊢ (M \in ℕ \land k \in ℕ_{0}) \to (M^{M} \in ℝ \land (k + 1)! \in ℝ)$
112		nn0re	$⊢ M \in ℕ_{0} \to M \in ℝ$
113		id	$⊢ M \in ℕ_{0} \to M \in ℕ_{0}$
114		nn0ge0	$⊢ M \in ℕ_{0} \to 0 \leq M$
115	112 113 114	expge0d	$⊢ M \in ℕ_{0} \to 0 \leq M^{M}$
116	36 115	syl	$⊢ M \in ℕ \to 0 \leq M^{M}$
117	95	nnge1d	$⊢ k \in ℕ_{0} \to 1 \leq (k + 1)!$
118	116 117	anim12i	$⊢ (M \in ℕ \land k \in ℕ_{0}) \to (0 \leq M^{M} \land 1 \leq (k + 1)!)$
119		lemulge11	$⊢ ((M^{M} \in ℝ \land (k + 1)! \in ℝ) \land (0 \leq M^{M} \land 1 \leq (k + 1)!)) \to M^{M} \leq M^{M} (k + 1)!$
120	111 118 119	syl2anc	$⊢ (M \in ℕ \land k \in ℕ_{0}) \to M^{M} \leq M^{M} (k + 1)!$
121	120	adantr	$⊢ ((M \in ℕ \land k \in ℕ_{0}) \land k + 1 + 1 \leq M) \to M^{M} \leq M^{M} (k + 1)!$
122	93 94 99 110 121	letrd	$⊢ ((M \in ℕ \land k \in ℕ_{0}) \land k + 1 + 1 \leq M) \to M^{k + 1 + 1} \leq M^{M} (k + 1)!$
123	122	ex	$⊢ (M \in ℕ \land k \in ℕ_{0}) \to (k + 1 + 1 \leq M \to M^{k + 1 + 1} \leq M^{M} (k + 1)!)$
124	88 123	sylbid	$⊢ (M \in ℕ \land k \in ℕ_{0}) \to (k + 1 < M \to M^{k + 1 + 1} \leq M^{M} (k + 1)!)$
125	124	a1dd	$⊢ (M \in ℕ \land k \in ℕ_{0}) \to (k + 1 < M \to (M^{k + 1} \leq M^{M} k! \to M^{k + 1 + 1} \leq M^{M} (k + 1)!))$
126	52 53	syl	$⊢ k \in ℕ_{0} \to k + 1 \in ℝ$
127		lelttric	$⊢ (M \in ℝ \land k + 1 \in ℝ) \to (M \leq k + 1 \lor k + 1 < M)$
128	26 126 127	syl2an	$⊢ (M \in ℕ \land k \in ℕ_{0}) \to (M \leq k + 1 \lor k + 1 < M)$
129	86 125 128	mpjaod	$⊢ (M \in ℕ \land k \in ℕ_{0}) \to (M^{k + 1} \leq M^{M} k! \to M^{k + 1 + 1} \leq M^{M} (k + 1)!)$
130	129	expcom	$⊢ k \in ℕ_{0} \to (M \in ℕ \to (M^{k + 1} \leq M^{M} k! \to M^{k + 1 + 1} \leq M^{M} (k + 1)!))$
131	130	a2d	$⊢ k \in ℕ_{0} \to ((M \in ℕ \to M^{k + 1} \leq M^{M} k!) \to (M \in ℕ \to M^{k + 1 + 1} \leq M^{M} (k + 1)!))$
132	7 13 19 25 41 131	nn0ind	$⊢ N \in ℕ_{0} \to (M \in ℕ \to M^{N + 1} \leq M^{M} N!)$
133	132	impcom	$⊢ (M \in ℕ \land N \in ℕ_{0}) \to M^{N + 1} \leq M^{M} N!$
134		faccl	$⊢ N \in ℕ_{0} \to N! \in ℕ$
135	134	nnnn0d	$⊢ N \in ℕ_{0} \to N! \in ℕ_{0}$
136	135	nn0ge0d	$⊢ N \in ℕ_{0} \to 0 \leq N!$
137		nn0p1nn	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ$
138	137	0expd	$⊢ N \in ℕ_{0} \to 0^{N + 1} = 0$
139		0exp0e1	$⊢ 0^{0} = 1$
140	139	oveq1i	$⊢ 0^{0} N! = 1 N!$
141	134	nncnd	$⊢ N \in ℕ_{0} \to N! \in ℂ$
142	141	mullidd	$⊢ N \in ℕ_{0} \to 1 N! = N!$
143	140 142	eqtrid	$⊢ N \in ℕ_{0} \to 0^{0} N! = N!$
144	136 138 143	3brtr4d	$⊢ N \in ℕ_{0} \to 0^{N + 1} \leq 0^{0} N!$
145		oveq1	$⊢ M = 0 \to M^{N + 1} = 0^{N + 1}$
146		oveq12	$⊢ (M = 0 \land M = 0) \to M^{M} = 0^{0}$
147	146	anidms	$⊢ M = 0 \to M^{M} = 0^{0}$
148	147	oveq1d	$⊢ M = 0 \to M^{M} N! = 0^{0} N!$
149	145 148	breq12d	$⊢ M = 0 \to (M^{N + 1} \leq M^{M} N! \leftrightarrow 0^{N + 1} \leq 0^{0} N!)$
150	144 149	imbitrrid	$⊢ M = 0 \to (N \in ℕ_{0} \to M^{N + 1} \leq M^{M} N!)$
151	150	imp	$⊢ (M = 0 \land N \in ℕ_{0}) \to M^{N + 1} \leq M^{M} N!$
152	133 151	jaoian	$⊢ ((M \in ℕ \lor M = 0) \land N \in ℕ_{0}) \to M^{N + 1} \leq M^{M} N!$
153	1 152	sylanb	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to M^{N + 1} \leq M^{M} N!$

Metamath Proof Explorer

Theorem faclbnd

Proof