faclbnd - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > faclbnd		Structured version Unicode version

Theorem faclbnd 12062

Description: A lower bound for the factorial function. (Contributed by NM, 17-Dec-2005.)

**Assertion**
Ref	Expression
faclbnd	$/\$

Proof of Theorem faclbnd Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elnn0 10577	. 2 $\/$
2		oveq1 6097	. . . . . . . 8
3	2	oveq2d 6106	. . . . . . 7
4		fveq2 5688	. . . . . . . 8
5	4	oveq2d 6106	. . . . . . 7
6	3, 5	breq12d 4302	. . . . . 6
7	6	imbi2d 316	. . . . 5
8		oveq1 6097	. . . . . . . 8
9	8	oveq2d 6106	. . . . . . 7
10		fveq2 5688	. . . . . . . 8
11	10	oveq2d 6106	. . . . . . 7
12	9, 11	breq12d 4302	. . . . . 6
13	12	imbi2d 316	. . . . 5
14		oveq1 6097	. . . . . . . 8
15	14	oveq2d 6106	. . . . . . 7
16		fveq2 5688	. . . . . . . 8
17	16	oveq2d 6106	. . . . . . 7
18	15, 17	breq12d 4302	. . . . . 6
19	18	imbi2d 316	. . . . 5
20		oveq1 6097	. . . . . . . 8
21	20	oveq2d 6106	. . . . . . 7
22		fveq2 5688	. . . . . . . 8
23	22	oveq2d 6106	. . . . . . 7
24	21, 23	breq12d 4302	. . . . . 6
25	24	imbi2d 316	. . . . 5
26		nnre 10325	. . . . . . 7
27		nnge1 10344	. . . . . . 7
28		elnnuz 10893	. . . . . . . 8
29	28	biimpi 194	. . . . . . 7
30	26, 27, 29	leexp2ad 12036	. . . . . 6
31		0p1e1 10429	. . . . . . . 8
32	31	oveq2i 6101	. . . . . . 7
33	32	a1i 11	. . . . . 6
34		fac0 12050	. . . . . . . 8
35	34	oveq2i 6101	. . . . . . 7
36		nnnn0 10582	. . . . . . . . . 10
37	26, 36	reexpcld 12021	. . . . . . . . 9
38	37	recnd 9408	. . . . . . . 8
39	38	mulid1d 9399	. . . . . . 7
40	35, 39	syl5eq 2485	. . . . . 6
41	30, 33, 40	3brtr4d 4319	. . . . 5
42	26	ad3antrrr 724	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
43		simpllr 753	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
44		peano2nn0 10616	. . . . . . . . . . . . . . 15
45	43, 44	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
46	42, 45	reexpcld 12021	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
47	36	ad3antrrr 724	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
48	42, 47	reexpcld 12021	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
49		faccl 12057	. . . . . . . . . . . . . . . 16
50	43, 49	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
51	50	nnred 10333	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
52	48, 51	remulcld 9410	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
53		nn0re 10584	. . . . . . . . . . . . . 14
54		peano2re 9538	. . . . . . . . . . . . . 14
55	43, 53, 54	3syl 20	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
56		nngt0 10347	. . . . . . . . . . . . . . . 16
57	56	ad3antrrr 724	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
58		0re 9382	. . . . . . . . . . . . . . . 16
59		ltle 9459	. . . . . . . . . . . . . . . 16 $/\$
60	58, 59	mpan 665	. . . . . . . . . . . . . . 15
61	42, 57, 60	sylc 60	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
62	42, 45, 61	expge0d 12022	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
63		simplr 749	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
64		simprr 751	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
65	46, 52, 42, 55, 62, 61, 63, 64	lemul12ad 10271	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
66	65	anandis 821	. . . . . . . . . . 11 $/\$ $/\$ $/\$
67		nncn 10326	. . . . . . . . . . . . 13
68		expp1 11868	. . . . . . . . . . . . 13 $/\$
69	67, 44, 68	syl2an 474	. . . . . . . . . . . 12 $/\$
70	69	adantr 462	. . . . . . . . . . 11 $/\$ $/\$ $/\$
71		facp1 12052	. . . . . . . . . . . . . . 15
72	71	adantl 463	. . . . . . . . . . . . . 14 $/\$
73	72	oveq2d 6106	. . . . . . . . . . . . 13 $/\$
74	38	adantr 462	. . . . . . . . . . . . . 14 $/\$
75	49	nncnd 10334	. . . . . . . . . . . . . . 15
76	75	adantl 463	. . . . . . . . . . . . . 14 $/\$
77		nn0cn 10585	. . . . . . . . . . . . . . . 16
78		peano2cn 9537	. . . . . . . . . . . . . . . 16
79	77, 78	syl 16	. . . . . . . . . . . . . . 15
80	79	adantl 463	. . . . . . . . . . . . . 14 $/\$
81	74, 76, 80	mulassd 9405	. . . . . . . . . . . . 13 $/\$
82	73, 81	eqtr4d 2476	. . . . . . . . . . . 12 $/\$
83	82	adantr 462	. . . . . . . . . . 11 $/\$ $/\$ $/\$
84	66, 70, 83	3brtr4d 4319	. . . . . . . . . 10 $/\$ $/\$ $/\$
85	84	exp32 602	. . . . . . . . 9 $/\$
86	85	com23 78	. . . . . . . 8 $/\$
87		nn0ltp1le 10698	. . . . . . . . . . 11 $/\$
88	44, 36, 87	syl2anr 475	. . . . . . . . . 10 $/\$
89		peano2nn0 10616	. . . . . . . . . . . . . . 15
90	44, 89	syl 16	. . . . . . . . . . . . . 14
91		reexpcl 11878	. . . . . . . . . . . . . 14 $/\$
92	26, 90, 91	syl2an 474	. . . . . . . . . . . . 13 $/\$
93	92	adantr 462	. . . . . . . . . . . 12 $/\$ $/\$
94	37	ad2antrr 720	. . . . . . . . . . . 12 $/\$ $/\$
95		faccl 12057	. . . . . . . . . . . . . . . 16
96	44, 95	syl 16	. . . . . . . . . . . . . . 15
97	96	nnred 10333	. . . . . . . . . . . . . 14
98		remulcl 9363	. . . . . . . . . . . . . 14 $/\$
99	37, 97, 98	syl2an 474	. . . . . . . . . . . . 13 $/\$
100	99	adantr 462	. . . . . . . . . . . 12 $/\$ $/\$
101	26	ad2antrr 720	. . . . . . . . . . . . 13 $/\$ $/\$
102	27	ad2antrr 720	. . . . . . . . . . . . 13 $/\$ $/\$
103		simpr 458	. . . . . . . . . . . . . 14 $/\$ $/\$
104	90	ad2antlr 721	. . . . . . . . . . . . . . . 16 $/\$ $/\$
105	104	nn0zd 10741	. . . . . . . . . . . . . . 15 $/\$ $/\$
106		nnz 10664	. . . . . . . . . . . . . . . 16
107	106	ad2antrr 720	. . . . . . . . . . . . . . 15 $/\$ $/\$
108		eluz 10870	. . . . . . . . . . . . . . 15 $/\$
109	105, 107, 108	syl2anc 656	. . . . . . . . . . . . . 14 $/\$ $/\$
110	103, 109	mpbird 232	. . . . . . . . . . . . 13 $/\$ $/\$
111	101, 102, 110	leexp2ad 12036	. . . . . . . . . . . 12 $/\$ $/\$
112	37, 97	anim12i 563	. . . . . . . . . . . . . 14 $/\$ $/\$
113		nn0re 10584	. . . . . . . . . . . . . . . . 17
114		id 22	. . . . . . . . . . . . . . . . 17
115		nn0ge0 10601	. . . . . . . . . . . . . . . . 17
116	113, 114, 115	expge0d 12022	. . . . . . . . . . . . . . . 16
117	36, 116	syl 16	. . . . . . . . . . . . . . 15
118	96	nnge1d 10360	. . . . . . . . . . . . . . 15
119	117, 118	anim12i 563	. . . . . . . . . . . . . 14 $/\$ $/\$
120		lemulge11 10187	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
121	112, 119, 120	syl2anc 656	. . . . . . . . . . . . 13 $/\$
122	121	adantr 462	. . . . . . . . . . . 12 $/\$ $/\$
123	93, 94, 100, 111, 122	letrd 9524	. . . . . . . . . . 11 $/\$ $/\$
124	123	ex 434	. . . . . . . . . 10 $/\$
125	88, 124	sylbid 215	. . . . . . . . 9 $/\$
126	125	a1dd 46	. . . . . . . 8 $/\$
127	53, 54	syl 16	. . . . . . . . 9
128		lelttric 9477	. . . . . . . . 9 $/\$ $\/$
129	26, 127, 128	syl2an 474	. . . . . . . 8 $/\$ $\/$
130	86, 126, 129	mpjaod 381	. . . . . . 7 $/\$
131	130	expcom 435	. . . . . 6
132	131	a2d 26	. . . . 5
133	7, 13, 19, 25, 41, 132	nn0ind 10734	. . . 4
134	133	impcom 430	. . 3 $/\$
135		faccl 12057	. . . . . . . 8
136	135	nnnn0d 10632	. . . . . . 7
137	136	nn0ge0d 10635	. . . . . 6
138		nn0p1nn 10615	. . . . . . 7
139	138	0expd 12020	. . . . . 6
140		0exp0e1 11866	. . . . . . . 8
141	140	oveq1i 6100	. . . . . . 7
142	135	nncnd 10334	. . . . . . . 8
143	142	mulid2d 9400	. . . . . . 7
144	141, 143	syl5eq 2485	. . . . . 6
145	137, 139, 144	3brtr4d 4319	. . . . 5
146		oveq1 6097	. . . . . 6
147		oveq12 6099	. . . . . . . 8 $/\$
148	147	anidms 640	. . . . . . 7
149	148	oveq1d 6105	. . . . . 6
150	146, 149	breq12d 4302	. . . . 5
151	145, 150	syl5ibr 221	. . . 4
152	151	imp 429	. . 3 $/\$
153	134, 152	jaoian 777	. 2 $\/$ $/\$
154	1, 153	sylanb 469	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $\/$ wo 368 $/\$ wa 369

wceq 1364

wcel 1761 class class class wbr 4289

cfv 5415 (class class class)co 6090

cc 9276

cr 9277

cc0 9278

c1 9279

caddc 9281

cmul 9283

clt 9414

cle 9415

cn 10318

cn0 10575

cz 10642

cuz 10857

cexp 11861

cfa 12047

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1713 ax-7 1733 ax-8 1763 ax-9 1765 ax-10 1780 ax-11 1785 ax-12 1797 ax-13 1948 ax-ext 2422 ax-sep 4410 ax-nul 4418 ax-pow 4467 ax-pr 4528 ax-un 6371 ax-cnex 9334 ax-resscn 9335 ax-1cn 9336 ax-icn 9337 ax-addcl 9338 ax-addrcl 9339 ax-mulcl 9340 ax-mulrcl 9341 ax-mulcom 9342 ax-addass 9343 ax-mulass 9344 ax-distr 9345 ax-i2m1 9346 ax-1ne0 9347 ax-1rid 9348 ax-rnegex 9349 ax-rrecex 9350 ax-cnre 9351 ax-pre-lttri 9352 ax-pre-lttrn 9353 ax-pre-ltadd 9354 ax-pre-mulgt0 9355

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 961 df-3an 962 df-tru 1367 df-ex 1592 df-nf 1595 df-sb 1706 df-eu 2263 df-mo 2264 df-clab 2428 df-cleq 2434 df-clel 2437 df-nfc 2566 df-ne 2606 df-nel 2607 df-ral 2718 df-rex 2719 df-reu 2720 df-rmo 2721 df-rab 2722 df-v 2972 df-sbc 3184 df-csb 3286 df-dif 3328 df-un 3330 df-in 3332 df-ss 3339 df-pss 3341 df-nul 3635 df-if 3789 df-pw 3859 df-sn 3875 df-pr 3877 df-tp 3879 df-op 3881 df-uni 4089 df-iun 4170 df-br 4290 df-opab 4348 df-mpt 4349 df-tr 4383 df-eprel 4628 df-id 4632 df-po 4637 df-so 4638 df-fr 4675 df-we 4677 df-ord 4718 df-on 4719 df-lim 4720 df-suc 4721 df-xp 4842 df-rel 4843 df-cnv 4844 df-co 4845 df-dm 4846 df-rn 4847 df-res 4848 df-ima 4849 df-iota 5378 df-fun 5417 df-fn 5418 df-f 5419 df-f1 5420 df-fo 5421 df-f1o 5422 df-fv 5423 df-riota 6049 df-ov 6093 df-oprab 6094 df-mpt2 6095 df-om 6476 df-2nd 6577 df-recs 6828 df-rdg 6862 df-er 7097 df-en 7307 df-dom 7308 df-sdom 7309 df-pnf 9416 df-mnf 9417 df-xr 9418 df-ltxr 9419 df-le 9420 df-sub 9593 df-neg 9594 df-div 9990 df-nn 10319 df-n0 10576 df-z 10643 df-uz 10858 df-rp 10988 df-seq 11803 df-exp 11862 df-fac 12048

This theorem is referenced by: faclbnd2 12063 faclbnd3 12064

W3C validator