faclbnd - Intuitionistic Logic Explorer

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

Theorem faclbnd 9765

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 8357	. 2 $\/$
2		oveq1 5550	. . . . . . . 8
3	2	oveq2d 5559	. . . . . . 7
4		fveq2 5209	. . . . . . . 8
5	4	oveq2d 5559	. . . . . . 7
6	3, 5	breq12d 3806	. . . . . 6
7	6	imbi2d 228	. . . . 5
8		oveq1 5550	. . . . . . . 8
9	8	oveq2d 5559	. . . . . . 7
10		fveq2 5209	. . . . . . . 8
11	10	oveq2d 5559	. . . . . . 7
12	9, 11	breq12d 3806	. . . . . 6
13	12	imbi2d 228	. . . . 5
14		oveq1 5550	. . . . . . . 8
15	14	oveq2d 5559	. . . . . . 7
16		fveq2 5209	. . . . . . . 8
17	16	oveq2d 5559	. . . . . . 7
18	15, 17	breq12d 3806	. . . . . 6
19	18	imbi2d 228	. . . . 5
20		oveq1 5550	. . . . . . . 8
21	20	oveq2d 5559	. . . . . . 7
22		fveq2 5209	. . . . . . . 8
23	22	oveq2d 5559	. . . . . . 7
24	21, 23	breq12d 3806	. . . . . 6
25	24	imbi2d 228	. . . . 5
26		nnre 8113	. . . . . . 7
27		nnge1 8129	. . . . . . 7
28		elnnuz 8736	. . . . . . . 8
29	28	biimpi 118	. . . . . . 7
30	26, 27, 29	leexp2ad 9731	. . . . . 6
31		0p1e1 8220	. . . . . . . 8
32	31	oveq2i 5554	. . . . . . 7
33	32	a1i 9	. . . . . 6
34		fac0 9752	. . . . . . . 8
35	34	oveq2i 5554	. . . . . . 7
36		nnnn0 8362	. . . . . . . . . 10
37	26, 36	reexpcld 9719	. . . . . . . . 9
38	37	recnd 7209	. . . . . . . 8
39	38	mulid1d 7198	. . . . . . 7
40	35, 39	syl5eq 2126	. . . . . 6
41	30, 33, 40	3brtr4d 3823	. . . . 5
42	26	ad3antrrr 476	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
43		simpllr 501	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
44		peano2nn0 8395	. . . . . . . . . . . . . . 15
45	43, 44	syl 14	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
46	42, 45	reexpcld 9719	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
47	36	ad3antrrr 476	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
48	42, 47	reexpcld 9719	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
49	43	faccld 9760	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
50	49	nnred 8119	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
51	48, 50	remulcld 7211	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
52		nn0re 8364	. . . . . . . . . . . . . 14
53		peano2re 7311	. . . . . . . . . . . . . 14
54	43, 52, 53	3syl 17	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
55		nngt0 8131	. . . . . . . . . . . . . . . 16
56	55	ad3antrrr 476	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
57		0re 7181	. . . . . . . . . . . . . . . 16
58		ltle 7265	. . . . . . . . . . . . . . . 16 $/\$
59	57, 58	mpan 415	. . . . . . . . . . . . . . 15
60	42, 56, 59	sylc 61	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
61	42, 45, 60	expge0d 9720	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
62		simplr 497	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
63		simprr 499	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
64	46, 51, 42, 54, 61, 60, 62, 63	lemul12ad 8087	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
65	64	anandis 557	. . . . . . . . . . 11 $/\$ $/\$ $/\$
66		nncn 8114	. . . . . . . . . . . . 13
67		expp1 9580	. . . . . . . . . . . . 13 $/\$
68	66, 44, 67	syl2an 283	. . . . . . . . . . . 12 $/\$
69	68	adantr 270	. . . . . . . . . . 11 $/\$ $/\$ $/\$
70		facp1 9754	. . . . . . . . . . . . . . 15
71	70	adantl 271	. . . . . . . . . . . . . 14 $/\$
72	71	oveq2d 5559	. . . . . . . . . . . . 13 $/\$
73	38	adantr 270	. . . . . . . . . . . . . 14 $/\$
74		faccl 9759	. . . . . . . . . . . . . . . 16
75	74	nncnd 8120	. . . . . . . . . . . . . . 15
76	75	adantl 271	. . . . . . . . . . . . . 14 $/\$
77		nn0cn 8365	. . . . . . . . . . . . . . . 16
78		peano2cn 7310	. . . . . . . . . . . . . . . 16
79	77, 78	syl 14	. . . . . . . . . . . . . . 15
80	79	adantl 271	. . . . . . . . . . . . . 14 $/\$
81	73, 76, 80	mulassd 7204	. . . . . . . . . . . . 13 $/\$
82	72, 81	eqtr4d 2117	. . . . . . . . . . . 12 $/\$
83	82	adantr 270	. . . . . . . . . . 11 $/\$ $/\$ $/\$
84	65, 69, 83	3brtr4d 3823	. . . . . . . . . 10 $/\$ $/\$ $/\$
85	84	exp32 357	. . . . . . . . 9 $/\$
86	85	com23 77	. . . . . . . 8 $/\$
87		nn0ltp1le 8494	. . . . . . . . . . 11 $/\$
88	44, 36, 87	syl2anr 284	. . . . . . . . . 10 $/\$
89		peano2nn0 8395	. . . . . . . . . . . . . . 15
90	44, 89	syl 14	. . . . . . . . . . . . . 14
91		reexpcl 9590	. . . . . . . . . . . . . 14 $/\$
92	26, 90, 91	syl2an 283	. . . . . . . . . . . . 13 $/\$
93	92	adantr 270	. . . . . . . . . . . 12 $/\$ $/\$
94	37	ad2antrr 472	. . . . . . . . . . . 12 $/\$ $/\$
95	44	faccld 9760	. . . . . . . . . . . . . . 15
96	95	nnred 8119	. . . . . . . . . . . . . 14
97		remulcl 7163	. . . . . . . . . . . . . 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 8548	. . . . . . . . . . . . . . 15 $/\$ $/\$
105		nnz 8451	. . . . . . . . . . . . . . . 16
106	105	ad2antrr 472	. . . . . . . . . . . . . . 15 $/\$ $/\$
107		eluz 8713	. . . . . . . . . . . . . . 15 $/\$
108	104, 106, 107	syl2anc 403	. . . . . . . . . . . . . 14 $/\$ $/\$
109	102, 108	mpbird 165	. . . . . . . . . . . . 13 $/\$ $/\$
110	100, 101, 109	leexp2ad 9731	. . . . . . . . . . . 12 $/\$ $/\$
111	37, 96	anim12i 331	. . . . . . . . . . . . . 14 $/\$ $/\$
112		nn0re 8364	. . . . . . . . . . . . . . . . 17
113		id 19	. . . . . . . . . . . . . . . . 17
114		nn0ge0 8380	. . . . . . . . . . . . . . . . 17
115	112, 113, 114	expge0d 9720	. . . . . . . . . . . . . . . 16
116	36, 115	syl 14	. . . . . . . . . . . . . . 15
117	95	nnge1d 8148	. . . . . . . . . . . . . . 15
118	116, 117	anim12i 331	. . . . . . . . . . . . . 14 $/\$ $/\$
119		lemulge11 8011	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
120	111, 118, 119	syl2anc 403	. . . . . . . . . . . . 13 $/\$
121	120	adantr 270	. . . . . . . . . . . 12 $/\$ $/\$
122	93, 94, 99, 110, 121	letrd 7300	. . . . . . . . . . 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 8548	. . . . . . . . 9 $/\$
129		zlelttric 8477	. . . . . . . . 9 $/\$ $\/$
130	126, 128, 129	syl2anc 403	. . . . . . . 8 $/\$ $\/$
131	86, 125, 130	mpjaod 671	. . . . . . 7 $/\$
132	131	expcom 114	. . . . . 6
133	132	a2d 26	. . . . 5
134	7, 13, 19, 25, 41, 133	nn0ind 8542	. . . 4
135	134	impcom 123	. . 3 $/\$
136		faccl 9759	. . . . . . . 8
137	136	nnnn0d 8408	. . . . . . 7
138	137	nn0ge0d 8411	. . . . . 6
139		nn0p1nn 8394	. . . . . . 7
140	139	0expd 9718	. . . . . 6
141		0exp0e1 9578	. . . . . . . 8
142	141	oveq1i 5553	. . . . . . 7
143	136	nncnd 8120	. . . . . . . 8
144	143	mulid2d 7199	. . . . . . 7
145	142, 144	syl5eq 2126	. . . . . 6
146	138, 140, 145	3brtr4d 3823	. . . . 5
147		oveq1 5550	. . . . . 6
148		oveq12 5552	. . . . . . . 8 $/\$
149	148	anidms 389	. . . . . . 7
150	149	oveq1d 5558	. . . . . 6
151	147, 150	breq12d 3806	. . . . 5
152	146, 151	syl5ibr 154	. . . 4
153	152	imp 122	. . 3 $/\$
154	135, 153	jaoian 742	. 2 $\/$ $/\$
155	1, 154	sylanb 278	1 $/\$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 102

wb 103 $\/$ wo 662

wceq 1285

wcel 1434 class class class wbr 3793

cfv 4932 (class class class)co 5543

cc 7041

cr 7042

cc0 7043

c1 7044

caddc 7046

cmul 7048

clt 7215

cle 7216

cn 8106

cn0 8355

cz 8432

cuz 8700

cexp 9572

cfa 9749

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 577 ax-in2 578 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-13 1445 ax-14 1446 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2064 ax-coll 3901 ax-sep 3904 ax-nul 3912 ax-pow 3956 ax-pr 3972 ax-un 4196 ax-setind 4288 ax-iinf 4337 ax-cnex 7129 ax-resscn 7130 ax-1cn 7131 ax-1re 7132 ax-icn 7133 ax-addcl 7134 ax-addrcl 7135 ax-mulcl 7136 ax-mulrcl 7137 ax-addcom 7138 ax-mulcom 7139 ax-addass 7140 ax-mulass 7141 ax-distr 7142 ax-i2m1 7143 ax-0lt1 7144 ax-1rid 7145 ax-0id 7146 ax-rnegex 7147 ax-precex 7148 ax-cnre 7149 ax-pre-ltirr 7150 ax-pre-ltwlin 7151 ax-pre-lttrn 7152 ax-pre-apti 7153 ax-pre-ltadd 7154 ax-pre-mulgt0 7155 ax-pre-mulext 7156

This theorem depends on definitions: df-bi 115 df-dc 777 df-3or 921 df-3an 922 df-tru 1288 df-fal 1291 df-nf 1391 df-sb 1687 df-eu 1945 df-mo 1946 df-clab 2069 df-cleq 2075 df-clel 2078 df-nfc 2209 df-ne 2247 df-nel 2341 df-ral 2354 df-rex 2355 df-reu 2356 df-rmo 2357 df-rab 2358 df-v 2604 df-sbc 2817 df-csb 2910 df-dif 2976 df-un 2978 df-in 2980 df-ss 2987 df-nul 3259 df-if 3360 df-pw 3392 df-sn 3412 df-pr 3413 df-op 3415 df-uni 3610 df-int 3645 df-iun 3688 df-br 3794 df-opab 3848 df-mpt 3849 df-tr 3884 df-id 4056 df-po 4059 df-iso 4060 df-iord 4129 df-on 4131 df-ilim 4132 df-suc 4134 df-iom 4340 df-xp 4377 df-rel 4378 df-cnv 4379 df-co 4380 df-dm 4381 df-rn 4382 df-res 4383 df-ima 4384 df-iota 4897 df-fun 4934 df-fn 4935 df-f 4936 df-f1 4937 df-fo 4938 df-f1o 4939 df-fv 4940 df-riota 5499 df-ov 5546 df-oprab 5547 df-mpt2 5548 df-1st 5798 df-2nd 5799 df-recs 5954 df-frec 6040 df-pnf 7217 df-mnf 7218 df-xr 7219 df-ltxr 7220 df-le 7221 df-sub 7348 df-neg 7349 df-reap 7742 df-ap 7749 df-div 7828 df-inn 8107 df-n0 8356 df-z 8433 df-uz 8701 df-rp 8816 df-iseq 9522 df-iexp 9573 df-fac 9750

This theorem is referenced by: faclbnd2 9766 faclbnd3 9767

W3C validator