Theorem faclbnd3 6892

Description: A lower bound for the factorial function.

Assertion

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

Proof of Theorem faclbnd3

Step	Hyp	Ref	Expression
1		expwordit 6542	. . . . 5 |- (((M e. RR /\ N e. NN0 /\ (N + 1) e. NN0) /\ (1 <_ M /\ N <_ (N + 1))) -> (M^N) <_ (M^(N + 1)))
2		nnret 5885	. . . . . . 7 |- (M e. NN -> M e. RR)
3	2	adantr 389	. . . . . 6 |- ((M e. NN /\ N e. NN0) -> M e. RR)
4		pm3.27 323	. . . . . 6 |- ((M e. NN /\ N e. NN0) -> N e. NN0)
5		peano2nn0 6079	. . . . . . 7 |- (N e. NN0 -> (N + 1) e. NN0)
6	5	adantl 388	. . . . . 6 |- ((M e. NN /\ N e. NN0) -> (N + 1) e. NN0)
7	3, 4, 6	3jca 818	. . . . 5 |- ((M e. NN /\ N e. NN0) -> (M e. RR /\ N e. NN0 /\ (N + 1) e. NN0))
8		nnge1t 5899	. . . . . 6 |- (M e. NN -> 1 <_ M)
9		letrp1t 5780	. . . . . . 7 |- ((N e. RR /\ N e. RR /\ N <_ N) -> N <_ (N + 1))
10		nn0ret 6063	. . . . . . 7 |- (N e. NN0 -> N e. RR)
11		leidt 5512	. . . . . . . 8 |- (N e. RR -> N <_ N)
12	10, 11	syl 10	. . . . . . 7 |- (N e. NN0 -> N <_ N)
13	9, 10, 10, 12	syl3anc 857	. . . . . 6 |- (N e. NN0 -> N <_ (N + 1))
14	8, 13	anim12i 333	. . . . 5 |- ((M e. NN /\ N e. NN0) -> (1 <_ M /\ N <_ (N + 1)))
15	1, 7, 14	sylanc 471	. . . 4 |- ((M e. NN /\ N e. NN0) -> (M^N) <_ (M^(N + 1)))
16		faclbnd 6890	. . . . 5 |- ((M e. NN0 /\ N e. NN0) -> (M^(N + 1)) <_ ((M^M) x. (!` N)))
17		nnnn0t 6061	. . . . 5 |- (M e. NN -> M e. NN0)
18	16, 17	sylan 448	. . . 4 |- ((M e. NN /\ N e. NN0) -> (M^(N + 1)) <_ ((M^M) x. (!` N)))
19		letrt 5506	. . . . . 6 |- (((M^N) e. RR /\ (M^(N + 1)) e. RR /\ ((M^M) x. (!` N)) e. RR) -> (((M^N) <_ (M^(N + 1)) /\ (M^(N + 1)) <_ ((M^M) x. (!` N))) -> (M^N) <_ ((M^M) x. (!` N))))
20		reexpclt 6520	. . . . . . 7 |- ((M e. RR /\ N e. NN0) -> (M^N) e. RR)
21		nn0ret 6063	. . . . . . 7 |- (M e. NN0 -> M e. RR)
22	20, 21	sylan 448	. . . . . 6 |- ((M e. NN0 /\ N e. NN0) -> (M^N) e. RR)
23		reexpclt 6520	. . . . . . 7 |- ((M e. RR /\ (N + 1) e. NN0) -> (M^(N + 1)) e. RR)
24	23, 21, 5	syl2an 454	. . . . . 6 |- ((M e. NN0 /\ N e. NN0) -> (M^(N + 1)) e. RR)
25		axmulrcl 5254	. . . . . . 7 |- (((M^M) e. RR /\ (!` N) e. RR) -> ((M^M) x. (!` N)) e. RR)
26		reexpclt 6520	. . . . . . . 8 |- ((M e. RR /\ M e. NN0) -> (M^M) e. RR)
27	21, 26	mpancom 704	. . . . . . 7 |- (M e. NN0 -> (M^M) e. RR)
28		facclt 6885	. . . . . . . 8 |- (N e. NN0 -> (!` N) e. NN)
29		nnret 5885	. . . . . . . 8 |- ((!` N) e. NN -> (!` N) e. RR)
30	28, 29	syl 10	. . . . . . 7 |- (N e. NN0 -> (!` N) e. RR)
31	25, 27, 30	syl2an 454	. . . . . 6 |- ((M e. NN0 /\ N e. NN0) -> ((M^M) x. (!` N)) e. RR)
32	19, 22, 24, 31	syl3anc 857	. . . . 5 |- ((M e. NN0 /\ N e. NN0) -> (((M^N) <_ (M^(N + 1)) /\ (M^(N + 1)) <_ ((M^M) x. (!` N))) -> (M^N) <_ ((M^M) x. (!` N))))
33	32, 17	sylan 448	. . . 4 |- ((M e. NN /\ N e. NN0) -> (((M^N) <_ (M^(N + 1)) /\ (M^(N + 1)) <_ ((M^M) x. (!` N))) -> (M^N) <_ ((M^M) x. (!` N))))
34	15, 18, 33	mp2and 702	. . 3 |- ((M e. NN /\ N e. NN0) -> (M^N) <_ ((M^M) x. (!` N)))
35		elnn0 6056	. . . . . . 7 |- (N e. NN0 <-> (N e. NN \/ N = 0))
36		0expt 6529	. . . . . . . . 9 |- (N e. NN -> (0^N) = 0)
37		0re 5420	. . . . . . . . . 10 |- 0 e. RR
38		1re 5415	. . . . . . . . . 10 |- 1 e. RR
39		lt01 5661	. . . . . . . . . 10 |- 0 < 1
40	37, 38, 39	ltlei 5562	. . . . . . . . 9 |- 0 <_ 1
41	36, 40	syl6eqbr 2647	. . . . . . . 8 |- (N e. NN -> (0^N) <_ 1)
42		opreq2 3960	. . . . . . . . 9 |- (N = 0 -> (0^N) = (0^0))
43		0cn 5308	. . . . . . . . . . 11 |- 0 e. CC
44		exp0t 6511	. . . . . . . . . . 11 |- (0 e. CC -> (0^0) = 1)
45	43, 44	ax-mp 7	. . . . . . . . . 10 |- (0^0) = 1
46	38	leid 5592	. . . . . . . . . 10 |- 1 <_ 1
47	45, 46	eqbrtr 2629	. . . . . . . . 9 |- (0^0) <_ 1
48	42, 47	syl6eqbr 2647	. . . . . . . 8 |- (N = 0 -> (0^N) <_ 1)
49	41, 48	jaoi 341	. . . . . . 7 |- ((N e. NN \/ N = 0) -> (0^N) <_ 1)
50	35, 49	sylbi 199	. . . . . 6 |- (N e. NN0 -> (0^N) <_ 1)
51		1nn 5890	. . . . . . . . 9 |- 1 e. NN
52		nnmulclt 5897	. . . . . . . . 9 |- ((1 e. NN /\ (!` N) e. NN) -> (1 x. (!` N)) e. NN)
53	51, 52	mpan 694	. . . . . . . 8 |- ((!` N) e. NN -> (1 x. (!` N)) e. NN)
54	28, 53	syl 10	. . . . . . 7 |- (N e. NN0 -> (1 x. (!` N)) e. NN)
55		nnge1t 5899	. . . . . . 7 |- ((1 x. (!` N)) e. NN -> 1 <_ (1 x. (!` N)))
56	54, 55	syl 10	. . . . . 6 |- (N e. NN0 -> 1 <_ (1 x. (!` N)))
57		letrt 5506	. . . . . . . 8 |- (((0^N) e. RR /\ 1 e. RR /\ (1 x. (!` N)) e. RR) -> (((0^N) <_ 1 /\ 1 <_ (1 x. (!` N))) -> (0^N) <_ (1 x. (!` N))))
58	38, 57	mp3an2 902	. . . . . . 7 |- (((0^N) e. RR /\ (1 x. (!` N)) e. RR) -> (((0^N) <_ 1 /\ 1 <_ (1 x. (!` N))) -> (0^N) <_ (1 x. (!` N))))
59		reexpclt 6520	. . . . . . . 8 |- ((0 e. RR /\ N e. NN0) -> (0^N) e. RR)
60	37, 59	mpan 694	. . . . . . 7 |- (N e. NN0 -> (0^N) e. RR)
61		axmulrcl 5254	. . . . . . . . 9 |- ((1 e. RR /\ (!` N) e. RR) -> (1 x. (!` N)) e. RR)
62	38, 61	mpan 694	. . . . . . . 8 |- ((!` N) e. RR -> (1 x. (!` N)) e. RR)
63	30, 62	syl 10	. . . . . . 7 |- (N e. NN0 -> (1 x. (!` N)) e. RR)
64	58, 60, 63	sylanc 471	. . . . . 6 |- (N e. NN0 -> (((0^N) <_ 1 /\ 1 <_ (1 x. (!` N))) -> (0^N) <_ (1 x. (!` N))))
65	50, 56, 64	mp2and 702	. . . . 5 |- (N e. NN0 -> (0^N) <_ (1 x. (!` N)))
66	65	adantl 388	. . . 4 |- ((M = 0 /\ N e. NN0) -> (0^N) <_ (1 x. (!` N)))
67		opreq1 3959	. . . . . 6 |- (M = 0 -> (M^N) = (0^N))
68		opreq12 3961	. . . . . . . . 9 |- ((M = 0 /\ M = 0) -> (M^M) = (0^0))
69	68	anidms 434	. . . . . . . 8 |- (M = 0 -> (M^M) = (0^0))
70	69, 45	syl6eq 1520	. . . . . . 7 |- (M = 0 -> (M^M) = 1)
71	70	opreq1d 3966	. . . . . 6 |- (M = 0 -> ((M^M) x. (!` N)) = (1 x. (!` N)))
72	67, 71	breq12d 2626	. . . . 5 |- (M = 0 -> ((M^N) <_ ((M^M) x. (!` N)) <-> (0^N) <_ (1 x. (!` N))))
73	72	adantr 389	. . . 4 |- ((M = 0 /\ N e. NN0) -> ((M^N) <_ ((M^M) x. (!` N)) <-> (0^N) <_ (1 x. (!` N))))
74	66, 73	mpbird 196	. . 3 |- ((M = 0 /\ N e. NN0) -> (M^N) <_ ((M^M) x. (!` N)))
75	34, 74	jaoian 425	. 2 |- (((M e. NN \/ M = 0) /\ N e. NN0) -> (M^N) <_ ((M^M) x. (!` N)))
76		elnn0 6056	. 2 |- (M e. NN0 <-> (M e. NN \/ M = 0))
77	75, 76	sylanb 449	1 |- ((M e. NN0 /\ N e. NN0) -> (M^N) <_ ((M^M) x. (!` N)))

Syntax hints:   -> wi 3   <-> wb 146   \/ wo 222   /\ wa 223   /\ w3a 774   = wceq 954   e. wcel 956   class class class wbr 2614  ` cfv 3177  (class class class)co 3954  CCcc 5212  RRcr 5213  0cc0 5214  1c1 5215   + caddc 5217   x. cmul 5219   <_ cle 5275  NNcn 5276  NN0cn0 5277  ^cexp 6508  !cfa 6876

This theorem is referenced by:  faclbnd4lem4 6896

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-9 963  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17