Theorem faclbnd 6897

Description: A lower bound for the factorial function.

Assertion

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

Proof of Theorem faclbnd

Step	Hyp	Ref	Expression
1		opreq1 3963	. . . . . . . 8 |- (j = 0 -> (j + 1) = (0 + 1))
2	1	opreq2d 3971	. . . . . . 7 |- (j = 0 -> (M^(j + 1)) = (M^(0 + 1)))
3		fveq2 3719	. . . . . . . 8 |- (j = 0 -> (!` j) = (!` 0))
4	3	opreq2d 3971	. . . . . . 7 |- (j = 0 -> ((M^M) x. (!` j)) = ((M^M) x. (!` 0)))
5	2, 4	breq12d 2627	. . . . . 6 |- (j = 0 -> ((M^(j + 1)) <_ ((M^M) x. (!` j)) <-> (M^(0 + 1)) <_ ((M^M) x. (!` 0))))
6	5	imbi2d 611	. . . . 5 |- (j = 0 -> ((M e. NN -> (M^(j + 1)) <_ ((M^M) x. (!` j))) <-> (M e. NN -> (M^(0 + 1)) <_ ((M^M) x. (!` 0)))))
7		opreq1 3963	. . . . . . . 8 |- (j = k -> (j + 1) = (k + 1))
8	7	opreq2d 3971	. . . . . . 7 |- (j = k -> (M^(j + 1)) = (M^(k + 1)))
9		fveq2 3719	. . . . . . . 8 |- (j = k -> (!` j) = (!` k))
10	9	opreq2d 3971	. . . . . . 7 |- (j = k -> ((M^M) x. (!` j)) = ((M^M) x. (!` k)))
11	8, 10	breq12d 2627	. . . . . 6 |- (j = k -> ((M^(j + 1)) <_ ((M^M) x. (!` j)) <-> (M^(k + 1)) <_ ((M^M) x. (!` k))))
12	11	imbi2d 611	. . . . 5 |- (j = k -> ((M e. NN -> (M^(j + 1)) <_ ((M^M) x. (!` j))) <-> (M e. NN -> (M^(k + 1)) <_ ((M^M) x. (!` k)))))
13		opreq1 3963	. . . . . . . 8 |- (j = (k + 1) -> (j + 1) = ((k + 1) + 1))
14	13	opreq2d 3971	. . . . . . 7 |- (j = (k + 1) -> (M^(j + 1)) = (M^((k + 1) + 1)))
15		fveq2 3719	. . . . . . . 8 |- (j = (k + 1) -> (!` j) = (!` (k + 1)))
16	15	opreq2d 3971	. . . . . . 7 |- (j = (k + 1) -> ((M^M) x. (!` j)) = ((M^M) x. (!` (k + 1))))
17	14, 16	breq12d 2627	. . . . . 6 |- (j = (k + 1) -> ((M^(j + 1)) <_ ((M^M) x. (!` j)) <-> (M^((k + 1) + 1)) <_ ((M^M) x. (!` (k + 1)))))
18	17	imbi2d 611	. . . . 5 |- (j = (k + 1) -> ((M e. NN -> (M^(j + 1)) <_ ((M^M) x. (!` j))) <-> (M e. NN -> (M^((k + 1) + 1)) <_ ((M^M) x. (!` (k + 1))))))
19		opreq1 3963	. . . . . . . 8 |- (j = N -> (j + 1) = (N + 1))
20	19	opreq2d 3971	. . . . . . 7 |- (j = N -> (M^(j + 1)) = (M^(N + 1)))
21		fveq2 3719	. . . . . . . 8 |- (j = N -> (!` j) = (!` N))
22	21	opreq2d 3971	. . . . . . 7 |- (j = N -> ((M^M) x. (!` j)) = ((M^M) x. (!` N)))
23	20, 22	breq12d 2627	. . . . . 6 |- (j = N -> ((M^(j + 1)) <_ ((M^M) x. (!` j)) <-> (M^(N + 1)) <_ ((M^M) x. (!` N))))
24	23	imbi2d 611	. . . . 5 |- (j = N -> ((M e. NN -> (M^(j + 1)) <_ ((M^M) x. (!` j))) <-> (M e. NN -> (M^(N + 1)) <_ ((M^M) x. (!` N)))))
25		expwordit 6548	. . . . . . 7 |- (((M e. RR /\ 1 e. NN0 /\ M e. NN0) /\ (1 <_ M /\ 1 <_ M)) -> (M^1) <_ (M^M))
26		nnret 5887	. . . . . . . 8 |- (M e. NN -> M e. RR)
27		1nn0 6071	. . . . . . . . 9 |- 1 e. NN0
28	27	a1i 8	. . . . . . . 8 |- (M e. NN -> 1 e. NN0)
29		nnnn0t 6063	. . . . . . . 8 |- (M e. NN -> M e. NN0)
30	26, 28, 29	3jca 818	. . . . . . 7 |- (M e. NN -> (M e. RR /\ 1 e. NN0 /\ M e. NN0))
31		nnge1t 5901	. . . . . . . 8 |- (M e. NN -> 1 <_ M)
32	31, 31	jca 288	. . . . . . 7 |- (M e. NN -> (1 <_ M /\ 1 <_ M))
33	25, 30, 32	sylanc 471	. . . . . 6 |- (M e. NN -> (M^1) <_ (M^M))
34		ax1cn 5252	. . . . . . . . 9 |- 1 e. CC
35	34	addid2 5314	. . . . . . . 8 |- (0 + 1) = 1
36	35	opreq2i 3967	. . . . . . 7 |- (M^(0 + 1)) = (M^1)
37	36	a1i 8	. . . . . 6 |- (M e. NN -> (M^(0 + 1)) = (M^1))
38		reexpclt 6525	. . . . . . . . . 10 |- ((M e. RR /\ M e. NN0) -> (M^M) e. RR)
39	38, 26, 29	sylanc 471	. . . . . . . . 9 |- (M e. NN -> (M^M) e. RR)
40	39	recnd 5298	. . . . . . . 8 |- (M e. NN -> (M^M) e. CC)
41		ax1id 5265	. . . . . . . 8 |- ((M^M) e. CC -> ((M^M) x. 1) = (M^M))
42	40, 41	syl 10	. . . . . . 7 |- (M e. NN -> ((M^M) x. 1) = (M^M))
43		fac0 6886	. . . . . . . 8 |- (!` 0) = 1
44	43	opreq2i 3967	. . . . . . 7 |- ((M^M) x. (!` 0)) = ((M^M) x. 1)
45	42, 44	syl5eq 1517	. . . . . 6 |- (M e. NN -> ((M^M) x. (!` 0)) = (M^M))
46	33, 37, 45	3brtr4d 2641	. . . . 5 |- (M e. NN -> (M^(0 + 1)) <_ ((M^M) x. (!` 0)))
47		lelttrit 5606	. . . . . . . . 9 |- ((M e. RR /\ (k + 1) e. RR) -> (M <_ (k + 1) \/ (k + 1) < M))
48		nn0ret 6065	. . . . . . . . . 10 |- (k e. NN0 -> k e. RR)
49		peano2re 5419	. . . . . . . . . 10 |- (k e. RR -> (k + 1) e. RR)
50	48, 49	syl 10	. . . . . . . . 9 |- (k e. NN0 -> (k + 1) e. RR)
51	47, 26, 50	syl2an 454	. . . . . . . 8 |- ((M e. NN /\ k e. NN0) -> (M <_ (k + 1) \/ (k + 1) < M))
52		lemul12itOLD 5809	. . . . . . . . . . . . . 14 |- (((((M^(k + 1)) e. RR /\ ((M^M) x. (!` k)) e. RR) /\ (0 <_ (M^(k + 1)) /\ (M^(k + 1)) <_ ((M^M) x. (!` k)))) /\ ((M e. RR /\ (k + 1) e. RR) /\ (0 <_ M /\ M <_ (k + 1)))) -> ((M^(k + 1)) x. M) <_ (((M^M) x. (!` k)) x. (k + 1)))
53		reexpclt 6525	. . . . . . . . . . . . . . . . . 18 |- ((M e. RR /\ (k + 1) e. NN0) -> (M^(k + 1)) e. RR)
54		peano2nn0 6081	. . . . . . . . . . . . . . . . . 18 |- (k e. NN0 -> (k + 1) e. NN0)
55	53, 26, 54	syl2an 454	. . . . . . . . . . . . . . . . 17 |- ((M e. NN /\ k e. NN0) -> (M^(k + 1)) e. RR)
56	55	adantr 389	. . . . . . . . . . . . . . . 16 |- (((M e. NN /\ k e. NN0) /\ (M^(k + 1)) <_ ((M^M) x. (!` k))) -> (M^(k + 1)) e. RR)
57		axmulrcl 5257	. . . . . . . . . . . . . . . . . 18 |- (((M^M) e. RR /\ (!` k) e. RR) -> ((M^M) x. (!` k)) e. RR)
58		facclt 6892	. . . . . . . . . . . . . . . . . . 19 |- (k e. NN0 -> (!` k) e. NN)
59		nnret 5887	. . . . . . . . . . . . . . . . . . 19 |- ((!` k) e. NN -> (!` k) e. RR)
60	58, 59	syl 10	. . . . . . . . . . . . . . . . . 18 |- (k e. NN0 -> (!` k) e. RR)
61	57, 39, 60	syl2an 454	. . . . . . . . . . . . . . . . 17 |- ((M e. NN /\ k e. NN0) -> ((M^M) x. (!` k)) e. RR)
62	61	adantr 389	. . . . . . . . . . . . . . . 16 |- (((M e. NN /\ k e. NN0) /\ (M^(k + 1)) <_ ((M^M) x. (!` k))) -> ((M^M) x. (!` k)) e. RR)
63	56, 62	jca 288	. . . . . . . . . . . . . . 15 |- (((M e. NN /\ k e. NN0) /\ (M^(k + 1)) <_ ((M^M) x. (!` k))) -> ((M^(k + 1)) e. RR /\ ((M^M) x. (!` k)) e. RR))
64		expge0t 6536	. . . . . . . . . . . . . . . . 17 |- ((M e. RR /\ (k + 1) e. NN0 /\ 0 <_ M) -> 0 <_ (M^(k + 1)))
65	26	adantr 389	. . . . . . . . . . . . . . . . 17 |- ((M e. NN /\ k e. NN0) -> M e. RR)
66	54	adantl 388	. . . . . . . . . . . . . . . . 17 |- ((M e. NN /\ k e. NN0) -> (k + 1)