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 \in ℕ_{0} \land M \in ℕ_{0}) \to N! {(N + 1)}^{M} \leq (N + M)!$

Proof

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

Metamath Proof Explorer

Theorem faclbnd6

Proof