Theorem faclbnd3 7070

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		expwordi 6725	. . . . 5 |- (((M e. RR /\ N e. NN0 /\ (N + 1) e. NN0) /\ (1 <_ M /\ N <_ (N + 1))) -> (M^N) <_ (M^(N + 1)))
2		nnre 6016	. . . . . . 7 |- (M e. NN -> M e. RR)
3	2	adantr 389	. . . . . 6 |- ((M e. NN /\ N e. NN0) -> M e. RR)
4		pm3.27 321	. . . . . 6 |- ((M e. NN /\ N e. NN0) -> N e. NN0)
5		peano2nn0 6234	. . . . . . 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 822	. . . . 5 |- ((M e. NN /\ N e. NN0) -> (M e. RR /\ N e. NN0 /\ (N + 1) e. NN0))
8		nnge1 6030	. . . . . 6 |- (M e. NN -> 1 <_ M)
9		letrp1 5900	. . . . . . 7 |- ((N e. RR /\ N e. RR /\ N <_ N) -> N <_ (N + 1))
10		nn0re 6218	. . . . . . 7 |- (N e. NN0 -> N e. RR)
11		leid 5620	. . . . . . . 8 |- (N e. RR -> N <_ N)
12	10, 11	syl 10	. . . . . . 7 |- (N e. NN0 -> N <_ N)
13	9, 10, 10, 12	syl3anc 861	. . . . . 6 |- (N e. NN0 -> N <_ (N + 1))
14	8, 13	anim12i 331	. . . . 5 |- ((M e. NN /\ N e. NN0) -> (1 <_ M /\ N <_ (N + 1)))
15	1, 7, 14	sylanc 473	. . . 4 |- ((M e. NN /\ N e. NN0) -> (M^N) <_ (M^(N + 1)))
16		faclbnd 7068	. . . . 5 |- ((M e. NN0 /\ N e. NN0) -> (M^(N + 1)) <_ ((M^M) x. (!` N)))
17		nnnn0 6216	. . . . 5 |- (M e. NN -> M e. NN0)
18	16, 17	sylan 450	. . . 4 |- ((M e. NN /\ N e. NN0) -> (M^(N + 1)) <_ ((M^M) x. (!` N)))
19		letr 5614	. . . . . 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		reexpcl 6703	. . . . . . 7 |- ((M e. RR /\ N e. NN0) -> (M^N) e. RR)
21		nn0re 6218	. . . . . . 7 |- (M e. NN0 -> M e. RR)
22	20, 21	sylan 450	. . . . . 6 |- ((M e. NN0 /\ N e. NN0) -> (M^N) e. RR)
23		reexpcl 6703	. . . . . . 7 |- ((M e. RR /\ (N + 1) e. NN0) -> (M^(N + 1)) e. RR)
24	23, 21, 5	syl2an 456	. . . . . 6 |- ((M e. NN0 /\ N e. NN0) -> (M^(N + 1)) e. RR)
25		remulcl 5393	. . . . . . 7 |- (((M^M) e. RR /\ (!` N) e. RR) -> ((M^M) x. (!` N)) e. RR)
26		reexpcl 6703	. . . . . . . 8 |- ((M e. RR /\ M e. NN0) -> (M^M) e. RR)
27	21, 26	mpancom 708	. . . . . . 7 |- (M e. NN0 -> (M^M) e. RR)
28		faccl 7063	. . . . . . . 8 |- (N e. NN0 -> (!` N) e. NN)
29		nnre 6016	. . . . . . . 8 |- ((!` N) e. NN -> (!` N) e. RR)
30	28, 29	syl 10	. . . . . . 7 |- (N e. NN0 -> (!` N) e. RR)
31	25, 27, 30	syl2an 456	. . . . . 6 |- ((M e. NN0 /\ N e. NN0) -> ((M^M) x. (!` N)) e. RR)
32	19, 22, 24, 31	syl3anc 861	. . . . 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 450	. . . 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 706	. . 3 |- ((M e. NN /\ N e. NN0) -> (M^N) <_ ((M^M) x. (!` N)))
35		elnn0 6211	. . . . . . 7 |- (N e. NN0 <-> (N e. NN \/ N = 0))
36		0exp 6713	. . . . . . . . 9 |- (N e. NN -> (0^N) = 0)
37		0re 5529	. . . . . . . . . 10 |- 0 e. RR
38		1re 5524	. . . . . . . . . 10 |- 1 e. RR
39		lt01 5769	. . . . . . . . . 10 |- 0 < 1
40	37, 38, 39	ltleii 5670	. . . . . . . . 9 |- 0 <_ 1
41	36, 40	syl6eqbr 2702	. . . . . . . 8 |- (N e. NN -> (0^N) <_ 1)
42		opreq2 4045	. . . . . . . . 9 |- (N = 0 -> (0^N) = (0^0))
43		0cn 5417	. . . . . . . . . . 11 |- 0 e. CC
44		exp0 6694	. . . . . . . . . . 11 |- (0 e. CC -> (0^0) = 1)
45	43, 44	ax-mp 7	. . . . . . . . . 10 |- (0^0) = 1
46	38	leidi 5699	. . . . . . . . . 10 |- 1 <_ 1
47	45, 46	eqbrtri 2684	. . . . . . . . 9 |- (0^0) <_ 1
48	42, 47	syl6eqbr 2702	. . . . . . . 8 |- (N = 0 -> (0^N) <_ 1)
49	41, 48	jaoi 339	. . . . . . 7 |- ((N e. NN \/ N = 0) -> (0^N) <_ 1)
50	35, 49	sylbi 197	. . . . . 6 |- (N e. NN0 -> (0^N) <_ 1)
51		1nn 6021	. . . . . . . . 9 |- 1 e. NN
52		nnmulcl 6028	. . . . . . . . 9 |- ((1 e. NN /\ (!` N) e. NN) -> (1 x. (!` N)) e. NN)
53	51, 52	mpan 698	. . . . . . . 8 |- ((!` N) e. NN -> (1 x. (!` N)) e. NN)
54	28, 53	syl 10	. . . . . . 7 |- (N e. NN0 -> (1 x. (!` N)) e. NN)
55		nnge1 6030	. . . . . . 7 |- ((1 x. (!` N)) e. NN -> 1 <_ (1 x. (!` N)))
56	54, 55	syl 10	. . . . . 6 |- (N e. NN0 -> 1 <_ (1 x. (!` N)))
57		letr 5614	. . . . . . . 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 907	. . . . . . 7 |- (((0^N) e. RR /\ (1 x. (!` N)) e. RR) -> (((0^N) <_ 1 /\ 1 <_ (1 x. (!` N))) -> (0^N) <_ (1 x. (!` N))))
59		reexpcl 6703	. . . . . . . 8 |- ((0 e. RR /\ N e. NN0) -> (0^N) e. RR)
60	37, 59	mpan 698	. . . . . . 7 |- (N e. NN0 -> (0^N) e. RR)
61		remulcl 5393	. . . . . . . . 9 |- ((1 e. RR /\ (!` N) e. RR) -> (1 x. (!` N)) e. RR)
62	38, 61	mpan 698	. . . . . . . 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 473	. . . . . 6 |- (N e. NN0 -> (((0^N) <_ 1 /\ 1 <_ (1 x. (!` N))) -> (0^N) <_ (1 x. (!` N))))
65	50, 56, 64	mp2and 706	. . . . 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 4044	. . . . . 6 |- (M = 0 -> (M^N) = (0^N))
68		opreq12 4046	. . . . . . . . 9 |- ((M = 0 /\ M = 0) -> (M^M) = (0^0))
69	68	anidms 435	. . . . . . . 8 |- (M = 0 -> (M^M) = (0^0))
70	69, 45	syl6eq 1560	. . . . . . 7 |- (M = 0 -> (M^M) = 1)
71	70	opreq1d 4051	. . . . . 6 |- (M = 0 -> ((M^M) x. (!` N)) = (1 x. (!` N)))
72	67, 71	breq12d 2681	. . . . 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 194	. . 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 6211	. 2 |- (M e. NN0 <-> (M e. NN \/ M = 0))
77	75, 76	sylanb 451	1 |- ((M e. NN0 /\ N e. NN0) -> (M^N) <_ ((M^M) x. (!` N)))

Syntax hints:   -> wi 3   <-> wb 144   \/ wo 220   /\ wa 221   /\ w3a 778   = wceq 988   e. wcel 990   class class class wbr 2669  ` cfv 3237  (class class class)co 4039  CCcc 5321  RRcr 5322  0cc0 5323  1c1 5324   + caddc 5326   x. cmul 5328   <_ cle 5384  NNcn 5385  NN0cn0 5386  ^cexp 6691  !cfa 7054

This theorem is referenced by:  faclbnd4lem4 7074

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 994  ax-gen 995  ax-8 996  ax-9 997  ax-10 998  ax-11 999  ax-12 1000  ax-13 1001  ax-14 1002  ax-17