faclbnd - Intuitionistic Logic Explorer

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

Theorem faclbnd 10654

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 9116	. 2 $\/$
2		oveq1 5849	. . . . . . . 8
3	2	oveq2d 5858	. . . . . . 7
4		fveq2 5486	. . . . . . . 8
5	4	oveq2d 5858	. . . . . . 7
6	3, 5	breq12d 3995	. . . . . 6
7	6	imbi2d 229	. . . . 5
8		oveq1 5849	. . . . . . . 8
9	8	oveq2d 5858	. . . . . . 7
10		fveq2 5486	. . . . . . . 8
11	10	oveq2d 5858	. . . . . . 7
12	9, 11	breq12d 3995	. . . . . 6
13	12	imbi2d 229	. . . . 5
14		oveq1 5849	. . . . . . . 8
15	14	oveq2d 5858	. . . . . . 7
16		fveq2 5486	. . . . . . . 8
17	16	oveq2d 5858	. . . . . . 7
18	15, 17	breq12d 3995	. . . . . 6
19	18	imbi2d 229	. . . . 5
20		oveq1 5849	. . . . . . . 8
21	20	oveq2d 5858	. . . . . . 7
22		fveq2 5486	. . . . . . . 8
23	22	oveq2d 5858	. . . . . . 7
24	21, 23	breq12d 3995	. . . . . 6
25	24	imbi2d 229	. . . . 5
26		nnre 8864	. . . . . . 7
27		nnge1 8880	. . . . . . 7
28		elnnuz 9502	. . . . . . . 8
29	28	biimpi 119	. . . . . . 7
30	26, 27, 29	leexp2ad 10617	. . . . . 6
31		0p1e1 8971	. . . . . . . 8
32	31	oveq2i 5853	. . . . . . 7
33	32	a1i 9	. . . . . 6
34		fac0 10641	. . . . . . . 8
35	34	oveq2i 5853	. . . . . . 7
36		nnnn0 9121	. . . . . . . . . 10
37	26, 36	reexpcld 10605	. . . . . . . . 9
38	37	recnd 7927	. . . . . . . 8
39	38	mulid1d 7916	. . . . . . 7
40	35, 39	syl5eq 2211	. . . . . 6
41	30, 33, 40	3brtr4d 4014	. . . . 5
42	26	ad3antrrr 484	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
43		simpllr 524	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
44		peano2nn0 9154	. . . . . . . . . . . . . . 15
45	43, 44	syl 14	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
46	42, 45	reexpcld 10605	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
47	36	ad3antrrr 484	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
48	42, 47	reexpcld 10605	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
49	43	faccld 10649	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
50	49	nnred 8870	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
51	48, 50	remulcld 7929	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
52		nn0re 9123	. . . . . . . . . . . . . 14
53		peano2re 8034	. . . . . . . . . . . . . 14
54	43, 52, 53	3syl 17	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
55		nngt0 8882	. . . . . . . . . . . . . . . 16
56	55	ad3antrrr 484	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
57		0re 7899	. . . . . . . . . . . . . . . 16
58		ltle 7986	. . . . . . . . . . . . . . . 16 $/\$
59	57, 58	mpan 421	. . . . . . . . . . . . . . 15
60	42, 56, 59	sylc 62	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
61	42, 45, 60	expge0d 10606	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
62		simplr 520	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
63		simprr 522	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
64	46, 51, 42, 54, 61, 60, 62, 63	lemul12ad 8837	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
65	64	anandis 582	. . . . . . . . . . 11 $/\$ $/\$ $/\$
66		nncn 8865	. . . . . . . . . . . . 13
67		expp1 10462	. . . . . . . . . . . . 13 $/\$
68	66, 44, 67	syl2an 287	. . . . . . . . . . . 12 $/\$
69	68	adantr 274	. . . . . . . . . . 11 $/\$ $/\$ $/\$
70		facp1 10643	. . . . . . . . . . . . . . 15
71	70	adantl 275	. . . . . . . . . . . . . 14 $/\$
72	71	oveq2d 5858	. . . . . . . . . . . . 13 $/\$
73	38	adantr 274	. . . . . . . . . . . . . 14 $/\$
74		faccl 10648	. . . . . . . . . . . . . . . 16
75	74	nncnd 8871	. . . . . . . . . . . . . . 15
76	75	adantl 275	. . . . . . . . . . . . . 14 $/\$
77		nn0cn 9124	. . . . . . . . . . . . . . . 16
78		peano2cn 8033	. . . . . . . . . . . . . . . 16
79	77, 78	syl 14	. . . . . . . . . . . . . . 15
80	79	adantl 275	. . . . . . . . . . . . . 14 $/\$
81	73, 76, 80	mulassd 7922	. . . . . . . . . . . . 13 $/\$
82	72, 81	eqtr4d 2201	. . . . . . . . . . . 12 $/\$
83	82	adantr 274	. . . . . . . . . . 11 $/\$ $/\$ $/\$
84	65, 69, 83	3brtr4d 4014	. . . . . . . . . 10 $/\$ $/\$ $/\$
85	84	exp32 363	. . . . . . . . 9 $/\$
86	85	com23 78	. . . . . . . 8 $/\$
87		nn0ltp1le 9253	. . . . . . . . . . 11 $/\$
88	44, 36, 87	syl2anr 288	. . . . . . . . . 10 $/\$
89		peano2nn0 9154	. . . . . . . . . . . . . . 15
90	44, 89	syl 14	. . . . . . . . . . . . . 14
91		reexpcl 10472	. . . . . . . . . . . . . 14 $/\$
92	26, 90, 91	syl2an 287	. . . . . . . . . . . . 13 $/\$
93	92	adantr 274	. . . . . . . . . . . 12 $/\$ $/\$
94	37	ad2antrr 480	. . . . . . . . . . . 12 $/\$ $/\$
95	44	faccld 10649	. . . . . . . . . . . . . . 15
96	95	nnred 8870	. . . . . . . . . . . . . 14
97		remulcl 7881	. . . . . . . . . . . . . 14 $/\$
98	37, 96, 97	syl2an 287	. . . . . . . . . . . . 13 $/\$
99	98	adantr 274	. . . . . . . . . . . 12 $/\$ $/\$
100	26	ad2antrr 480	. . . . . . . . . . . . 13 $/\$ $/\$
101	27	ad2antrr 480	. . . . . . . . . . . . 13 $/\$ $/\$
102		simpr 109	. . . . . . . . . . . . . 14 $/\$ $/\$
103	90	ad2antlr 481	. . . . . . . . . . . . . . . 16 $/\$ $/\$
104	103	nn0zd 9311	. . . . . . . . . . . . . . 15 $/\$ $/\$
105		nnz 9210	. . . . . . . . . . . . . . . 16
106	105	ad2antrr 480	. . . . . . . . . . . . . . 15 $/\$ $/\$
107		eluz 9479	. . . . . . . . . . . . . . 15 $/\$
108	104, 106, 107	syl2anc 409	. . . . . . . . . . . . . 14 $/\$ $/\$
109	102, 108	mpbird 166	. . . . . . . . . . . . 13 $/\$ $/\$
110	100, 101, 109	leexp2ad 10617	. . . . . . . . . . . 12 $/\$ $/\$
111	37, 96	anim12i 336	. . . . . . . . . . . . . 14 $/\$ $/\$
112		nn0re 9123	. . . . . . . . . . . . . . . . 17
113		id 19	. . . . . . . . . . . . . . . . 17
114		nn0ge0 9139	. . . . . . . . . . . . . . . . 17
115	112, 113, 114	expge0d 10606	. . . . . . . . . . . . . . . 16
116	36, 115	syl 14	. . . . . . . . . . . . . . 15
117	95	nnge1d 8900	. . . . . . . . . . . . . . 15
118	116, 117	anim12i 336	. . . . . . . . . . . . . 14 $/\$ $/\$
119		lemulge11 8761	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
120	111, 118, 119	syl2anc 409	. . . . . . . . . . . . 13 $/\$
121	120	adantr 274	. . . . . . . . . . . 12 $/\$ $/\$
122	93, 94, 99, 110, 121	letrd 8022	. . . . . . . . . . 11 $/\$ $/\$
123	122	ex 114	. . . . . . . . . 10 $/\$
124	88, 123	sylbid 149	. . . . . . . . 9 $/\$
125	124	a1dd 48	. . . . . . . 8 $/\$
126	105	adantr 274	. . . . . . . . 9 $/\$
127	44	adantl 275	. . . . . . . . . 10 $/\$
128	127	nn0zd 9311	. . . . . . . . 9 $/\$
129		zlelttric 9236	. . . . . . . . 9 $/\$ $\/$
130	126, 128, 129	syl2anc 409	. . . . . . . 8 $/\$ $\/$
131	86, 125, 130	mpjaod 708	. . . . . . 7 $/\$
132	131	expcom 115	. . . . . 6
133	132	a2d 26	. . . . 5
134	7, 13, 19, 25, 41, 133	nn0ind 9305	. . . 4
135	134	impcom 124	. . 3 $/\$
136		faccl 10648	. . . . . . . 8
137	136	nnnn0d 9167	. . . . . . 7
138	137	nn0ge0d 9170	. . . . . 6
139		nn0p1nn 9153	. . . . . . 7
140	139	0expd 10604	. . . . . 6
141		0exp0e1 10460	. . . . . . . 8
142	141	oveq1i 5852	. . . . . . 7
143	136	nncnd 8871	. . . . . . . 8
144	143	mulid2d 7917	. . . . . . 7
145	142, 144	syl5eq 2211	. . . . . 6
146	138, 140, 145	3brtr4d 4014	. . . . 5
147		oveq1 5849	. . . . . 6
148		oveq12 5851	. . . . . . . 8 $/\$
149	148	anidms 395	. . . . . . 7
150	149	oveq1d 5857	. . . . . 6
151	147, 150	breq12d 3995	. . . . 5
152	146, 151	syl5ibr 155	. . . 4
153	152	imp 123	. . 3 $/\$
154	135, 153	jaoian 785	. 2 $\/$ $/\$
155	1, 154	sylanb 282	1 $/\$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 103

wb 104 $\/$ wo 698

wceq 1343

wcel 2136 class class class wbr 3982

cfv 5188 (class class class)co 5842

cc 7751

cr 7752

cc0 7753

c1 7754

caddc 7756

cmul 7758

clt 7933

cle 7934

cn 8857

cn0 9114

cz 9191

cuz 9466

cexp 10454

cfa 10638

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1435 ax-7 1436 ax-gen 1437 ax-ie1 1481 ax-ie2 1482 ax-8 1492 ax-10 1493 ax-11 1494 ax-i12 1495 ax-bndl 1497 ax-4 1498 ax-17 1514 ax-i9 1518 ax-ial 1522 ax-i5r 1523 ax-13 2138 ax-14 2139 ax-ext 2147 ax-coll 4097 ax-sep 4100 ax-nul 4108 ax-pow 4153 ax-pr 4187 ax-un 4411 ax-setind 4514 ax-iinf 4565 ax-cnex 7844 ax-resscn 7845 ax-1cn 7846 ax-1re 7847 ax-icn 7848 ax-addcl 7849 ax-addrcl 7850 ax-mulcl 7851 ax-mulrcl 7852 ax-addcom 7853 ax-mulcom 7854 ax-addass 7855 ax-mulass 7856 ax-distr 7857 ax-i2m1 7858 ax-0lt1 7859 ax-1rid 7860 ax-0id 7861 ax-rnegex 7862 ax-precex 7863 ax-cnre 7864 ax-pre-ltirr 7865 ax-pre-ltwlin 7866 ax-pre-lttrn 7867 ax-pre-apti 7868 ax-pre-ltadd 7869 ax-pre-mulgt0 7870 ax-pre-mulext 7871

This theorem depends on definitions: df-bi 116 df-dc 825 df-3or 969 df-3an 970 df-tru 1346 df-fal 1349 df-nf 1449 df-sb 1751 df-eu 2017 df-mo 2018 df-clab 2152 df-cleq 2158 df-clel 2161 df-nfc 2297 df-ne 2337 df-nel 2432 df-ral 2449 df-rex 2450 df-reu 2451 df-rmo 2452 df-rab 2453 df-v 2728 df-sbc 2952 df-csb 3046 df-dif 3118 df-un 3120 df-in 3122 df-ss 3129 df-nul 3410 df-if 3521 df-pw 3561 df-sn 3582 df-pr 3583 df-op 3585 df-uni 3790 df-int 3825 df-iun 3868 df-br 3983 df-opab 4044 df-mpt 4045 df-tr 4081 df-id 4271 df-po 4274 df-iso 4275 df-iord 4344 df-on 4346 df-ilim 4347 df-suc 4349 df-iom 4568 df-xp 4610 df-rel 4611 df-cnv 4612 df-co 4613 df-dm 4614 df-rn 4615 df-res 4616 df-ima 4617 df-iota 5153 df-fun 5190 df-fn 5191 df-f 5192 df-f1 5193 df-fo 5194 df-f1o 5195 df-fv 5196 df-riota 5798 df-ov 5845 df-oprab 5846 df-mpo 5847 df-1st 6108 df-2nd 6109 df-recs 6273 df-frec 6359 df-pnf 7935 df-mnf 7936 df-xr 7937 df-ltxr 7938 df-le 7939 df-sub 8071 df-neg 8072 df-reap 8473 df-ap 8480 df-div 8569 df-inn 8858 df-n0 9115 df-z 9192 df-uz 9467 df-rp 9590 df-seqfrec 10381 df-exp 10455 df-fac 10639

This theorem is referenced by: faclbnd2 10655 faclbnd3 10656

W3C validator