faclbnd - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > faclbnd		Unicode version

Theorem faclbnd 10328

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 8831	. 2 $\/$
2		oveq1 5713	. . . . . . . 8
3	2	oveq2d 5722	. . . . . . 7
4		fveq2 5353	. . . . . . . 8
5	4	oveq2d 5722	. . . . . . 7
6	3, 5	breq12d 3888	. . . . . 6
7	6	imbi2d 229	. . . . 5
8		oveq1 5713	. . . . . . . 8
9	8	oveq2d 5722	. . . . . . 7
10		fveq2 5353	. . . . . . . 8
11	10	oveq2d 5722	. . . . . . 7
12	9, 11	breq12d 3888	. . . . . 6
13	12	imbi2d 229	. . . . 5
14		oveq1 5713	. . . . . . . 8
15	14	oveq2d 5722	. . . . . . 7
16		fveq2 5353	. . . . . . . 8
17	16	oveq2d 5722	. . . . . . 7
18	15, 17	breq12d 3888	. . . . . 6
19	18	imbi2d 229	. . . . 5
20		oveq1 5713	. . . . . . . 8
21	20	oveq2d 5722	. . . . . . 7
22		fveq2 5353	. . . . . . . 8
23	22	oveq2d 5722	. . . . . . 7
24	21, 23	breq12d 3888	. . . . . 6
25	24	imbi2d 229	. . . . 5
26		nnre 8585	. . . . . . 7
27		nnge1 8601	. . . . . . 7
28		elnnuz 9212	. . . . . . . 8
29	28	biimpi 119	. . . . . . 7
30	26, 27, 29	leexp2ad 10294	. . . . . 6
31		0p1e1 8692	. . . . . . . 8
32	31	oveq2i 5717	. . . . . . 7
33	32	a1i 9	. . . . . 6
34		fac0 10315	. . . . . . . 8
35	34	oveq2i 5717	. . . . . . 7
36		nnnn0 8836	. . . . . . . . . 10
37	26, 36	reexpcld 10282	. . . . . . . . 9
38	37	recnd 7666	. . . . . . . 8
39	38	mulid1d 7655	. . . . . . 7
40	35, 39	syl5eq 2144	. . . . . 6
41	30, 33, 40	3brtr4d 3905	. . . . 5
42	26	ad3antrrr 479	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
43		simpllr 504	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
44		peano2nn0 8869	. . . . . . . . . . . . . . 15
45	43, 44	syl 14	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
46	42, 45	reexpcld 10282	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
47	36	ad3antrrr 479	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
48	42, 47	reexpcld 10282	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
49	43	faccld 10323	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
50	49	nnred 8591	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
51	48, 50	remulcld 7668	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
52		nn0re 8838	. . . . . . . . . . . . . 14
53		peano2re 7769	. . . . . . . . . . . . . 14
54	43, 52, 53	3syl 17	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
55		nngt0 8603	. . . . . . . . . . . . . . . 16
56	55	ad3antrrr 479	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
57		0re 7638	. . . . . . . . . . . . . . . 16
58		ltle 7722	. . . . . . . . . . . . . . . 16 $/\$
59	57, 58	mpan 418	. . . . . . . . . . . . . . 15
60	42, 56, 59	sylc 62	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
61	42, 45, 60	expge0d 10283	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
62		simplr 500	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
63		simprr 502	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
64	46, 51, 42, 54, 61, 60, 62, 63	lemul12ad 8558	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
65	64	anandis 562	. . . . . . . . . . 11 $/\$ $/\$ $/\$
66		nncn 8586	. . . . . . . . . . . . 13
67		expp1 10141	. . . . . . . . . . . . 13 $/\$
68	66, 44, 67	syl2an 285	. . . . . . . . . . . 12 $/\$
69	68	adantr 272	. . . . . . . . . . 11 $/\$ $/\$ $/\$
70		facp1 10317	. . . . . . . . . . . . . . 15
71	70	adantl 273	. . . . . . . . . . . . . 14 $/\$
72	71	oveq2d 5722	. . . . . . . . . . . . 13 $/\$
73	38	adantr 272	. . . . . . . . . . . . . 14 $/\$
74		faccl 10322	. . . . . . . . . . . . . . . 16
75	74	nncnd 8592	. . . . . . . . . . . . . . 15
76	75	adantl 273	. . . . . . . . . . . . . 14 $/\$
77		nn0cn 8839	. . . . . . . . . . . . . . . 16
78		peano2cn 7768	. . . . . . . . . . . . . . . 16
79	77, 78	syl 14	. . . . . . . . . . . . . . 15
80	79	adantl 273	. . . . . . . . . . . . . 14 $/\$
81	73, 76, 80	mulassd 7661	. . . . . . . . . . . . 13 $/\$
82	72, 81	eqtr4d 2135	. . . . . . . . . . . 12 $/\$
83	82	adantr 272	. . . . . . . . . . 11 $/\$ $/\$ $/\$
84	65, 69, 83	3brtr4d 3905	. . . . . . . . . 10 $/\$ $/\$ $/\$
85	84	exp32 360	. . . . . . . . 9 $/\$
86	85	com23 78	. . . . . . . 8 $/\$
87		nn0ltp1le 8968	. . . . . . . . . . 11 $/\$
88	44, 36, 87	syl2anr 286	. . . . . . . . . 10 $/\$
89		peano2nn0 8869	. . . . . . . . . . . . . . 15
90	44, 89	syl 14	. . . . . . . . . . . . . 14
91		reexpcl 10151	. . . . . . . . . . . . . 14 $/\$
92	26, 90, 91	syl2an 285	. . . . . . . . . . . . 13 $/\$
93	92	adantr 272	. . . . . . . . . . . 12 $/\$ $/\$
94	37	ad2antrr 475	. . . . . . . . . . . 12 $/\$ $/\$
95	44	faccld 10323	. . . . . . . . . . . . . . 15
96	95	nnred 8591	. . . . . . . . . . . . . 14
97		remulcl 7620	. . . . . . . . . . . . . 14 $/\$
98	37, 96, 97	syl2an 285	. . . . . . . . . . . . 13 $/\$
99	98	adantr 272	. . . . . . . . . . . 12 $/\$ $/\$
100	26	ad2antrr 475	. . . . . . . . . . . . 13 $/\$ $/\$
101	27	ad2antrr 475	. . . . . . . . . . . . 13 $/\$ $/\$
102		simpr 109	. . . . . . . . . . . . . 14 $/\$ $/\$
103	90	ad2antlr 476	. . . . . . . . . . . . . . . 16 $/\$ $/\$
104	103	nn0zd 9023	. . . . . . . . . . . . . . 15 $/\$ $/\$
105		nnz 8925	. . . . . . . . . . . . . . . 16
106	105	ad2antrr 475	. . . . . . . . . . . . . . 15 $/\$ $/\$
107		eluz 9189	. . . . . . . . . . . . . . 15 $/\$
108	104, 106, 107	syl2anc 406	. . . . . . . . . . . . . 14 $/\$ $/\$
109	102, 108	mpbird 166	. . . . . . . . . . . . 13 $/\$ $/\$
110	100, 101, 109	leexp2ad 10294	. . . . . . . . . . . 12 $/\$ $/\$
111	37, 96	anim12i 334	. . . . . . . . . . . . . 14 $/\$ $/\$
112		nn0re 8838	. . . . . . . . . . . . . . . . 17
113		id 19	. . . . . . . . . . . . . . . . 17
114		nn0ge0 8854	. . . . . . . . . . . . . . . . 17
115	112, 113, 114	expge0d 10283	. . . . . . . . . . . . . . . 16
116	36, 115	syl 14	. . . . . . . . . . . . . . 15
117	95	nnge1d 8621	. . . . . . . . . . . . . . 15
118	116, 117	anim12i 334	. . . . . . . . . . . . . 14 $/\$ $/\$
119		lemulge11 8482	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
120	111, 118, 119	syl2anc 406	. . . . . . . . . . . . 13 $/\$
121	120	adantr 272	. . . . . . . . . . . 12 $/\$ $/\$
122	93, 94, 99, 110, 121	letrd 7757	. . . . . . . . . . 11 $/\$ $/\$
123	122	ex 114	. . . . . . . . . 10 $/\$
124	88, 123	sylbid 149	. . . . . . . . 9 $/\$
125	124	a1dd 48	. . . . . . . 8 $/\$
126	105	adantr 272	. . . . . . . . 9 $/\$
127	44	adantl 273	. . . . . . . . . 10 $/\$
128	127	nn0zd 9023	. . . . . . . . 9 $/\$
129		zlelttric 8951	. . . . . . . . 9 $/\$ $\/$
130	126, 128, 129	syl2anc 406	. . . . . . . 8 $/\$ $\/$
131	86, 125, 130	mpjaod 679	. . . . . . 7 $/\$
132	131	expcom 115	. . . . . 6
133	132	a2d 26	. . . . 5
134	7, 13, 19, 25, 41, 133	nn0ind 9017	. . . 4
135	134	impcom 124	. . 3 $/\$
136		faccl 10322	. . . . . . . 8
137	136	nnnn0d 8882	. . . . . . 7
138	137	nn0ge0d 8885	. . . . . 6
139		nn0p1nn 8868	. . . . . . 7
140	139	0expd 10281	. . . . . 6
141		0exp0e1 10139	. . . . . . . 8
142	141	oveq1i 5716	. . . . . . 7
143	136	nncnd 8592	. . . . . . . 8
144	143	mulid2d 7656	. . . . . . 7
145	142, 144	syl5eq 2144	. . . . . 6
146	138, 140, 145	3brtr4d 3905	. . . . 5
147		oveq1 5713	. . . . . 6
148		oveq12 5715	. . . . . . . 8 $/\$
149	148	anidms 392	. . . . . . 7
150	149	oveq1d 5721	. . . . . 6
151	147, 150	breq12d 3888	. . . . 5
152	146, 151	syl5ibr 155	. . . 4
153	152	imp 123	. . 3 $/\$
154	135, 153	jaoian 750	. 2 $\/$ $/\$
155	1, 154	sylanb 280	1 $/\$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 103

wb 104 $\/$ wo 670

wceq 1299

wcel 1448 class class class wbr 3875

cfv 5059 (class class class)co 5706

cc 7498

cr 7499

cc0 7500

c1 7501

caddc 7503

cmul 7505

clt 7672

cle 7673

cn 8578

cn0 8829

cz 8906

cuz 9176

cexp 10133

cfa 10312

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 584 ax-in2 585 ax-io 671 ax-5 1391 ax-7 1392 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-8 1450 ax-10 1451 ax-11 1452 ax-i12 1453 ax-bndl 1454 ax-4 1455 ax-13 1459 ax-14 1460 ax-17 1474 ax-i9 1478 ax-ial 1482 ax-i5r 1483 ax-ext 2082 ax-coll 3983 ax-sep 3986 ax-nul 3994 ax-pow 4038 ax-pr 4069 ax-un 4293 ax-setind 4390 ax-iinf 4440 ax-cnex 7586 ax-resscn 7587 ax-1cn 7588 ax-1re 7589 ax-icn 7590 ax-addcl 7591 ax-addrcl 7592 ax-mulcl 7593 ax-mulrcl 7594 ax-addcom 7595 ax-mulcom 7596 ax-addass 7597 ax-mulass 7598 ax-distr 7599 ax-i2m1 7600 ax-0lt1 7601 ax-1rid 7602 ax-0id 7603 ax-rnegex 7604 ax-precex 7605 ax-cnre 7606 ax-pre-ltirr 7607 ax-pre-ltwlin 7608 ax-pre-lttrn 7609 ax-pre-apti 7610 ax-pre-ltadd 7611 ax-pre-mulgt0 7612 ax-pre-mulext 7613

This theorem depends on definitions: df-bi 116 df-dc 787 df-3or 931 df-3an 932 df-tru 1302 df-fal 1305 df-nf 1405 df-sb 1704 df-eu 1963 df-mo 1964 df-clab 2087 df-cleq 2093 df-clel 2096 df-nfc 2229 df-ne 2268 df-nel 2363 df-ral 2380 df-rex 2381 df-reu 2382 df-rmo 2383 df-rab 2384 df-v 2643 df-sbc 2863 df-csb 2956 df-dif 3023 df-un 3025 df-in 3027 df-ss 3034 df-nul 3311 df-if 3422 df-pw 3459 df-sn 3480 df-pr 3481 df-op 3483 df-uni 3684 df-int 3719 df-iun 3762 df-br 3876 df-opab 3930 df-mpt 3931 df-tr 3967 df-id 4153 df-po 4156 df-iso 4157 df-iord 4226 df-on 4228 df-ilim 4229 df-suc 4231 df-iom 4443 df-xp 4483 df-rel 4484 df-cnv 4485 df-co 4486 df-dm 4487 df-rn 4488 df-res 4489 df-ima 4490 df-iota 5024 df-fun 5061 df-fn 5062 df-f 5063 df-f1 5064 df-fo 5065 df-f1o 5066 df-fv 5067 df-riota 5662 df-ov 5709 df-oprab 5710 df-mpo 5711 df-1st 5969 df-2nd 5970 df-recs 6132 df-frec 6218 df-pnf 7674 df-mnf 7675 df-xr 7676 df-ltxr 7677 df-le 7678 df-sub 7806 df-neg 7807 df-reap 8203 df-ap 8210 df-div 8294 df-inn 8579 df-n0 8830 df-z 8907 df-uz 9177 df-rp 9292 df-seqfrec 10060 df-exp 10134 df-fac 10313

This theorem is referenced by: faclbnd2 10329 faclbnd3 10330

W3C validator