faclbnd - Intuitionistic Logic Explorer

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

Theorem faclbnd 10114

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 8645	. 2 $\/$
2		oveq1 5641	. . . . . . . 8
3	2	oveq2d 5650	. . . . . . 7
4		fveq2 5289	. . . . . . . 8
5	4	oveq2d 5650	. . . . . . 7
6	3, 5	breq12d 3850	. . . . . 6
7	6	imbi2d 228	. . . . 5
8		oveq1 5641	. . . . . . . 8
9	8	oveq2d 5650	. . . . . . 7
10		fveq2 5289	. . . . . . . 8
11	10	oveq2d 5650	. . . . . . 7
12	9, 11	breq12d 3850	. . . . . 6
13	12	imbi2d 228	. . . . 5
14		oveq1 5641	. . . . . . . 8
15	14	oveq2d 5650	. . . . . . 7
16		fveq2 5289	. . . . . . . 8
17	16	oveq2d 5650	. . . . . . 7
18	15, 17	breq12d 3850	. . . . . 6
19	18	imbi2d 228	. . . . 5
20		oveq1 5641	. . . . . . . 8
21	20	oveq2d 5650	. . . . . . 7
22		fveq2 5289	. . . . . . . 8
23	22	oveq2d 5650	. . . . . . 7
24	21, 23	breq12d 3850	. . . . . 6
25	24	imbi2d 228	. . . . 5
26		nnre 8401	. . . . . . 7
27		nnge1 8417	. . . . . . 7
28		elnnuz 9024	. . . . . . . 8
29	28	biimpi 118	. . . . . . 7
30	26, 27, 29	leexp2ad 10080	. . . . . 6
31		0p1e1 8507	. . . . . . . 8
32	31	oveq2i 5645	. . . . . . 7
33	32	a1i 9	. . . . . 6
34		fac0 10101	. . . . . . . 8
35	34	oveq2i 5645	. . . . . . 7
36		nnnn0 8650	. . . . . . . . . 10
37	26, 36	reexpcld 10068	. . . . . . . . 9
38	37	recnd 7495	. . . . . . . 8
39	38	mulid1d 7484	. . . . . . 7
40	35, 39	syl5eq 2132	. . . . . 6
41	30, 33, 40	3brtr4d 3867	. . . . 5
42	26	ad3antrrr 476	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
43		simpllr 501	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
44		peano2nn0 8683	. . . . . . . . . . . . . . 15
45	43, 44	syl 14	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
46	42, 45	reexpcld 10068	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
47	36	ad3antrrr 476	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
48	42, 47	reexpcld 10068	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
49	43	faccld 10109	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
50	49	nnred 8407	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
51	48, 50	remulcld 7497	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
52		nn0re 8652	. . . . . . . . . . . . . 14
53		peano2re 7597	. . . . . . . . . . . . . 14
54	43, 52, 53	3syl 17	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
55		nngt0 8419	. . . . . . . . . . . . . . . 16
56	55	ad3antrrr 476	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
57		0re 7467	. . . . . . . . . . . . . . . 16
58		ltle 7551	. . . . . . . . . . . . . . . 16 $/\$
59	57, 58	mpan 415	. . . . . . . . . . . . . . 15
60	42, 56, 59	sylc 61	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
61	42, 45, 60	expge0d 10069	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
62		simplr 497	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
63		simprr 499	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
64	46, 51, 42, 54, 61, 60, 62, 63	lemul12ad 8375	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
65	64	anandis 559	. . . . . . . . . . 11 $/\$ $/\$ $/\$
66		nncn 8402	. . . . . . . . . . . . 13
67		expp1 9927	. . . . . . . . . . . . 13 $/\$
68	66, 44, 67	syl2an 283	. . . . . . . . . . . 12 $/\$
69	68	adantr 270	. . . . . . . . . . 11 $/\$ $/\$ $/\$
70		facp1 10103	. . . . . . . . . . . . . . 15
71	70	adantl 271	. . . . . . . . . . . . . 14 $/\$
72	71	oveq2d 5650	. . . . . . . . . . . . 13 $/\$
73	38	adantr 270	. . . . . . . . . . . . . 14 $/\$
74		faccl 10108	. . . . . . . . . . . . . . . 16
75	74	nncnd 8408	. . . . . . . . . . . . . . 15
76	75	adantl 271	. . . . . . . . . . . . . 14 $/\$
77		nn0cn 8653	. . . . . . . . . . . . . . . 16
78		peano2cn 7596	. . . . . . . . . . . . . . . 16
79	77, 78	syl 14	. . . . . . . . . . . . . . 15
80	79	adantl 271	. . . . . . . . . . . . . 14 $/\$
81	73, 76, 80	mulassd 7490	. . . . . . . . . . . . 13 $/\$
82	72, 81	eqtr4d 2123	. . . . . . . . . . . 12 $/\$
83	82	adantr 270	. . . . . . . . . . 11 $/\$ $/\$ $/\$
84	65, 69, 83	3brtr4d 3867	. . . . . . . . . 10 $/\$ $/\$ $/\$
85	84	exp32 357	. . . . . . . . 9 $/\$
86	85	com23 77	. . . . . . . 8 $/\$
87		nn0ltp1le 8782	. . . . . . . . . . 11 $/\$
88	44, 36, 87	syl2anr 284	. . . . . . . . . 10 $/\$
89		peano2nn0 8683	. . . . . . . . . . . . . . 15
90	44, 89	syl 14	. . . . . . . . . . . . . 14
91		reexpcl 9937	. . . . . . . . . . . . . 14 $/\$
92	26, 90, 91	syl2an 283	. . . . . . . . . . . . 13 $/\$
93	92	adantr 270	. . . . . . . . . . . 12 $/\$ $/\$
94	37	ad2antrr 472	. . . . . . . . . . . 12 $/\$ $/\$
95	44	faccld 10109	. . . . . . . . . . . . . . 15
96	95	nnred 8407	. . . . . . . . . . . . . 14
97		remulcl 7449	. . . . . . . . . . . . . 14 $/\$
98	37, 96, 97	syl2an 283	. . . . . . . . . . . . 13 $/\$
99	98	adantr 270	. . . . . . . . . . . 12 $/\$ $/\$
100	26	ad2antrr 472	. . . . . . . . . . . . 13 $/\$ $/\$
101	27	ad2antrr 472	. . . . . . . . . . . . 13 $/\$ $/\$
102		simpr 108	. . . . . . . . . . . . . 14 $/\$ $/\$
103	90	ad2antlr 473	. . . . . . . . . . . . . . . 16 $/\$ $/\$
104	103	nn0zd 8836	. . . . . . . . . . . . . . 15 $/\$ $/\$
105		nnz 8739	. . . . . . . . . . . . . . . 16
106	105	ad2antrr 472	. . . . . . . . . . . . . . 15 $/\$ $/\$
107		eluz 9001	. . . . . . . . . . . . . . 15 $/\$
108	104, 106, 107	syl2anc 403	. . . . . . . . . . . . . 14 $/\$ $/\$
109	102, 108	mpbird 165	. . . . . . . . . . . . 13 $/\$ $/\$
110	100, 101, 109	leexp2ad 10080	. . . . . . . . . . . 12 $/\$ $/\$
111	37, 96	anim12i 331	. . . . . . . . . . . . . 14 $/\$ $/\$
112		nn0re 8652	. . . . . . . . . . . . . . . . 17
113		id 19	. . . . . . . . . . . . . . . . 17
114		nn0ge0 8668	. . . . . . . . . . . . . . . . 17
115	112, 113, 114	expge0d 10069	. . . . . . . . . . . . . . . 16
116	36, 115	syl 14	. . . . . . . . . . . . . . 15
117	95	nnge1d 8436	. . . . . . . . . . . . . . 15
118	116, 117	anim12i 331	. . . . . . . . . . . . . 14 $/\$ $/\$
119		lemulge11 8299	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
120	111, 118, 119	syl2anc 403	. . . . . . . . . . . . 13 $/\$
121	120	adantr 270	. . . . . . . . . . . 12 $/\$ $/\$
122	93, 94, 99, 110, 121	letrd 7586	. . . . . . . . . . 11 $/\$ $/\$
123	122	ex 113	. . . . . . . . . 10 $/\$
124	88, 123	sylbid 148	. . . . . . . . 9 $/\$
125	124	a1dd 47	. . . . . . . 8 $/\$
126	105	adantr 270	. . . . . . . . 9 $/\$
127	44	adantl 271	. . . . . . . . . 10 $/\$
128	127	nn0zd 8836	. . . . . . . . 9 $/\$
129		zlelttric 8765	. . . . . . . . 9 $/\$ $\/$
130	126, 128, 129	syl2anc 403	. . . . . . . 8 $/\$ $\/$
131	86, 125, 130	mpjaod 673	. . . . . . 7 $/\$
132	131	expcom 114	. . . . . 6
133	132	a2d 26	. . . . 5
134	7, 13, 19, 25, 41, 133	nn0ind 8830	. . . 4
135	134	impcom 123	. . 3 $/\$
136		faccl 10108	. . . . . . . 8
137	136	nnnn0d 8696	. . . . . . 7
138	137	nn0ge0d 8699	. . . . . 6
139		nn0p1nn 8682	. . . . . . 7
140	139	0expd 10067	. . . . . 6
141		0exp0e1 9925	. . . . . . . 8
142	141	oveq1i 5644	. . . . . . 7
143	136	nncnd 8408	. . . . . . . 8
144	143	mulid2d 7485	. . . . . . 7
145	142, 144	syl5eq 2132	. . . . . 6
146	138, 140, 145	3brtr4d 3867	. . . . 5
147		oveq1 5641	. . . . . 6
148		oveq12 5643	. . . . . . . 8 $/\$
149	148	anidms 389	. . . . . . 7
150	149	oveq1d 5649	. . . . . 6
151	147, 150	breq12d 3850	. . . . 5
152	146, 151	syl5ibr 154	. . . 4
153	152	imp 122	. . 3 $/\$
154	135, 153	jaoian 744	. 2 $\/$ $/\$
155	1, 154	sylanb 278	1 $/\$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 102

wb 103 $\/$ wo 664

wceq 1289

wcel 1438 class class class wbr 3837

cfv 5002 (class class class)co 5634

cc 7327

cr 7328

cc0 7329

c1 7330

caddc 7332

cmul 7334

clt 7501

cle 7502

cn 8394

cn0 8643

cz 8720

cuz 8988

cexp 9919

cfa 10098

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 579 ax-in2 580 ax-io 665 ax-5 1381 ax-7 1382 ax-gen 1383 ax-ie1 1427 ax-ie2 1428 ax-8 1440 ax-10 1441 ax-11 1442 ax-i12 1443 ax-bndl 1444 ax-4 1445 ax-13 1449 ax-14 1450 ax-17 1464 ax-i9 1468 ax-ial 1472 ax-i5r 1473 ax-ext 2070 ax-coll 3946 ax-sep 3949 ax-nul 3957 ax-pow 4001 ax-pr 4027 ax-un 4251 ax-setind 4343 ax-iinf 4393 ax-cnex 7415 ax-resscn 7416 ax-1cn 7417 ax-1re 7418 ax-icn 7419 ax-addcl 7420 ax-addrcl 7421 ax-mulcl 7422 ax-mulrcl 7423 ax-addcom 7424 ax-mulcom 7425 ax-addass 7426 ax-mulass 7427 ax-distr 7428 ax-i2m1 7429 ax-0lt1 7430 ax-1rid 7431 ax-0id 7432 ax-rnegex 7433 ax-precex 7434 ax-cnre 7435 ax-pre-ltirr 7436 ax-pre-ltwlin 7437 ax-pre-lttrn 7438 ax-pre-apti 7439 ax-pre-ltadd 7440 ax-pre-mulgt0 7441 ax-pre-mulext 7442

This theorem depends on definitions: df-bi 115 df-dc 781 df-3or 925 df-3an 926 df-tru 1292 df-fal 1295 df-nf 1395 df-sb 1693 df-eu 1951 df-mo 1952 df-clab 2075 df-cleq 2081 df-clel 2084 df-nfc 2217 df-ne 2256 df-nel 2351 df-ral 2364 df-rex 2365 df-reu 2366 df-rmo 2367 df-rab 2368 df-v 2621 df-sbc 2839 df-csb 2932 df-dif 2999 df-un 3001 df-in 3003 df-ss 3010 df-nul 3285 df-if 3390 df-pw 3427 df-sn 3447 df-pr 3448 df-op 3450 df-uni 3649 df-int 3684 df-iun 3727 df-br 3838 df-opab 3892 df-mpt 3893 df-tr 3929 df-id 4111 df-po 4114 df-iso 4115 df-iord 4184 df-on 4186 df-ilim 4187 df-suc 4189 df-iom 4396 df-xp 4434 df-rel 4435 df-cnv 4436 df-co 4437 df-dm 4438 df-rn 4439 df-res 4440 df-ima 4441 df-iota 4967 df-fun 5004 df-fn 5005 df-f 5006 df-f1 5007 df-fo 5008 df-f1o 5009 df-fv 5010 df-riota 5590 df-ov 5637 df-oprab 5638 df-mpt2 5639 df-1st 5893 df-2nd 5894 df-recs 6052 df-frec 6138 df-pnf 7503 df-mnf 7504 df-xr 7505 df-ltxr 7506 df-le 7507 df-sub 7634 df-neg 7635 df-reap 8028 df-ap 8035 df-div 8114 df-inn 8395 df-n0 8644 df-z 8721 df-uz 8989 df-rp 9104 df-iseq 9818 df-seq3 9819 df-exp 9920 df-fac 10099

This theorem is referenced by: faclbnd2 10115 faclbnd3 10116

W3C validator