Theorem faclbnd6 6906

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

Assertion

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

Proof of Theorem faclbnd6

Step	Hyp	Ref	Expression
1		opreq2 3964	. . . . . 6 |- (m = 0 -> ((N + 1)^m) = ((N + 1)^0))
2	1	opreq2d 3971	. . . . 5 |- (m = 0 -> ((!` N) x. ((N + 1)^m)) = ((!` N) x. ((N + 1)^0)))
3		opreq2 3964	. . . . . 6 |- (m = 0 -> (N + m) = (N + 0))
4	3	fveq2d 3723	. . . . 5 |- (m = 0 -> (!` (N + m)) = (!` (N + 0)))
5	2, 4	breq12d 2627	. . . 4 |- (m = 0 -> (((!` N) x. ((N + 1)^m)) <_ (!` (N + m)) <-> ((!` N) x. ((N + 1)^0)) <_ (!` (N + 0))))
6	5	imbi2d 611	. . 3 |- (m = 0 -> ((N e. NN0 -> ((!` N) x. ((N + 1)^m)) <_ (!` (N + m))) <-> (N e. NN0 -> ((!` N) x. ((N + 1)^0)) <_ (!` (N + 0)))))
7		opreq2 3964	. . . . . 6 |- (m = k -> ((N + 1)^m) = ((N + 1)^k))
8	7	opreq2d 3971	. . . . 5 |- (m = k -> ((!` N) x. ((N + 1)^m)) = ((!` N) x. ((N + 1)^k)))
9		opreq2 3964	. . . . . 6 |- (m = k -> (N + m) = (N + k))
10	9	fveq2d 3723	. . . . 5 |- (m = k -> (!` (N + m)) = (!` (N + k)))
11	8, 10	breq12d 2627	. . . 4 |- (m = k -> (((!` N) x. ((N + 1)^m)) <_ (!` (N + m)) <-> ((!` N) x. ((N + 1)^k)) <_ (!` (N + k))))
12	11	imbi2d 611	. . 3 |- (m = k -> ((N e. NN0 -> ((!` N) x. ((N + 1)^m)) <_ (!` (N + m))) <-> (N e. NN0 -> ((!` N) x. ((N + 1)^k)) <_ (!` (N + k)))))
13		opreq2 3964	. . . . . 6 |- (m = (k + 1) -> ((N + 1)^m) = ((N + 1)^(k + 1)))
14	13	opreq2d 3971	. . . . 5 |- (m = (k + 1) -> ((!` N) x. ((N + 1)^m)) = ((!` N) x. ((N + 1)^(k + 1))))
15		opreq2 3964	. . . . . 6 |- (m = (k + 1) -> (N + m) = (N + (k + 1)))
16	15	fveq2d 3723	. . . . 5 |- (m = (k + 1) -> (!` (N + m)) = (!` (N + (k + 1))))
17	14, 16	breq12d 2627	. . . 4 |- (m = (k + 1) -> (((!` N) x. ((N + 1)^m)) <_ (!` (N + m)) <-> ((!` N) x. ((N + 1)^(k + 1))) <_ (!` (N + (k + 1)))))
18	17	imbi2d 611	. . 3 |- (m = (k + 1) -> ((N e. NN0 -> ((!` N) x. ((N + 1)^m)) <_ (!` (N + m))) <-> (N e. NN0 -> ((!` N) x. ((N + 1)^(k + 1))) <_ (!` (N + (k + 1))))))
19		opreq2 3964	. . . . . 6 |- (m = M -> ((N + 1)^m) = ((N + 1)^M))
20	19	opreq2d 3971	. . . . 5 |- (m = M -> ((!` N) x. ((N + 1)^m)) = ((!` N) x. ((N + 1)^M)))
21		opreq2 3964	. . . . . 6 |- (m = M -> (N + m) = (N + M))
22	21	fveq2d 3723	. . . . 5 |- (m = M -> (!` (N + m)) = (!` (N + M)))
23	20, 22	breq12d 2627	. . . 4 |- (m = M -> (((!` N) x. ((N + 1)^m)) <_ (!` (N + m)) <-> ((!` N) x. ((N + 1)^M)) <_ (!` (N + M))))
24	23	imbi2d 611	. . 3 |- (m = M -> ((N e. NN0 -> ((!` N) x. ((N + 1)^m)) <_ (!` (N + m))) <-> (N e. NN0 -> ((!` N) x. ((N + 1)^M)) <_ (!` (N + M)))))
25		facclt 6892	. . . . 5 |- (N e. NN0 -> (!` N) e. NN)
26		nnret 5887	. . . . 5 |- ((!` N) e. NN -> (!` N) e. RR)
27		leidt 5514	. . . . 5 |- ((!` N) e. RR -> (!` N) <_ (!` N))
28	25, 26, 27	3syl 20	. . . 4 |- (N e. NN0 -> (!` N) <_ (!` N))
29		nn0cnt 6066	. . . . . . . 8 |- (N e. NN0 -> N e. CC)
30		peano2cn 5327	. . . . . . . 8 |- (N e. CC -> (N + 1) e. CC)
31	29, 30	syl 10	. . . . . . 7 |- (N e. NN0 -> (N + 1) e. CC)
32		exp0t 6516	. . . . . . 7 |- ((N + 1) e. CC -> ((N + 1)^0) = 1)
33	31, 32	syl 10	. . . . . 6 |- (N e. NN0 -> ((N + 1)^0) = 1)
34	33	opreq2d 3971	. . . . 5 |- (N e. NN0 -> ((!` N) x. ((N + 1)^0)) = ((!` N) x. 1))
35		nncnt 5888	. . . . . . 7 |- ((!` N) e. NN -> (!` N) e. CC)
36	25, 35	syl 10	. . . . . 6 |- (N e. NN0 -> (!` N) e. CC)
37		ax1id 5265	. . . . . 6 |- ((!` N) e. CC -> ((!` N) x. 1) = (!` N))
38	36, 37	syl 10	. . . . 5 |- (N e. NN0 -> ((!` N) x. 1) = (!` N))
39	34, 38	eqtrd 1505	. . . 4 |- (N e. NN0 -> ((!` N) x. ((N + 1)^0)) = (!` N))
40		ax0id 5264	. . . . . 6 |- (N e. CC -> (N + 0) = N)
41	29, 40	syl 10	. . . . 5 |- (N e. NN0 -> (N + 0) = N)
42	41	fveq2d 3723	. . . 4 |- (N e. NN0 -> (!` (N + 0)) = (!` N))
43	28, 39, 42	3brtr4d 2641	. . 3 |- (N e. NN0 -> ((!` N) x. ((N + 1)^0)) <_ (!` (N + 0)))
44		lemul12itOLD 5809	. . . . . . . 8 |- ((((((!` N) x. ((N + 1)^k)) e. RR /\ (!` (N + k)) e. RR) /\ (0 <_ ((!` N) x. ((N + 1)^k)) /\ ((!` N) x. ((N + 1)^k)) <_ (!` (N + k)))) /\ (((N + 1) e. RR /\ (N + (k + 1)) e. RR) /\ (0 <_ (N + 1) /\ (N + 1) <_ (N + (k + 1))))) -> (((!` N) x. ((N + 1)^k)) x. (N + 1)) <_ ((!` (N + k)) x. (N + (k + 1))))
45		axmulrcl 5257	. . . . . . . . . . . 12 |- (((!` N) e. RR /\ ((N + 1)^k) e. RR) -> ((!` N) x. ((N + 1)^k)) e. RR)
46	25, 26	syl 10	. . . . . . . . . . . . 13 |- (N e. NN0 -> (!` N) e. RR)
47	46	adantr 389	. . . . . . . . . . . 12 |- ((N e. NN0 /\ k e. NN0) -> (!` N) e. RR)
48		reexpclt 6525	. . . . . . . . . . . . 13 |- (((N + 1) e. RR /\ k e. NN0) -> ((N + 1)^k) e. RR)
49		nn0ret 6065	. . . . . . . . . . . . . 14 |- (N e. NN0 -> N e. RR)
50		peano2re 5419	. . . . . . . . . . . . . 14 |- (N e. RR -> (N + 1) e. RR)
51	49, 50	syl 10	. . . . . . . . . . . . 13 |- (N e. NN0 -> (N + 1) e. RR)
52	48, 51	sylan 448	. . . . . . . . . . . 12 |- ((N e. NN0 /\ k e. NN0) -> ((N + 1)^k) e. RR)
53	45, 47, 52	sylanc 471	. . . . . . . . . . 11 |- ((N e. NN0 /\ k e. NN0) -> ((!` N) x. ((N + 1)^k)) e. RR)
54		nn0addclt 6077	. . . . . . . . . . . 12 |- ((N e. NN0 /\ k e. NN0) -> (N + k) e. NN0)
55		facclt 6892	. . . . . . . . . . . 12 |- ((N + k) e. NN0 -> (!` (N + k)) e. NN)
56		nnret 5887	. . . . . . . . . . . 12 |- ((!` (N + k)) e. NN -> (!` (N + k)) e. RR)
57	54, 55, 56	3syl 20	. . . . . . . . . . 11 |- ((N e. NN0 /\ k e. NN0) -> (!` (N + k)) e. RR)
58	53, 57	jca 288	. . . . . . . . . 10 |- ((N e. NN0 /\ k e. NN0) -> (((!` N) x. ((N + 1)^k)) e. RR /\ (!` (N + k)) e. RR))
59	58	adantr 389	. . . . . . . . 9 |- (((N e. NN0 /\ k e. NN0) /\ ((!` N) x. ((