pellexlem2 - Intuitionistic Logic Explorer

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

Theorem pellexlem2 16242

Description: Lemma for pellex . Arithmetical core of pellexlem3, norm upper bound. (Contributed by Stefan O'Rear, 14-Sep-2014.)

**Assertion**
Ref	Expression
pellexlem2	$/\$ $/\$ $/\$

**Proof of Theorem pellexlem2**
Step	Hyp	Ref	Expression
1		simpl3 1033	. . . . . . . . . 10 $/\$ $/\$ $/\$
2	1	nnred 9327	. . . . . . . . 9 $/\$ $/\$ $/\$
3	2	resqcld 11159	. . . . . . . 8 $/\$ $/\$ $/\$
4	2	sqge0d 11160	. . . . . . . 8 $/\$ $/\$ $/\$
5	3, 4	absidd 11957	. . . . . . 7 $/\$ $/\$ $/\$
6	5	eqcomd 2244	. . . . . 6 $/\$ $/\$ $/\$
7	6	oveq2d 6104	. . . . 5 $/\$ $/\$ $/\$
8		simpl2 1032	. . . . . . . . 9 $/\$ $/\$ $/\$
9	8	nncnd 9328	. . . . . . . 8 $/\$ $/\$ $/\$
10	9	sqcld 11131	. . . . . . 7 $/\$ $/\$ $/\$
11		simpl1 1031	. . . . . . . . 9 $/\$ $/\$ $/\$
12	11	nncnd 9328	. . . . . . . 8 $/\$ $/\$ $/\$
13	1	nncnd 9328	. . . . . . . . 9 $/\$ $/\$ $/\$
14	13	sqcld 11131	. . . . . . . 8 $/\$ $/\$ $/\$
15	12, 14	mulcld 8353	. . . . . . 7 $/\$ $/\$ $/\$
16	10, 15	subcld 8645	. . . . . 6 $/\$ $/\$ $/\$
17	1	nnap0d 9360	. . . . . . 7 $/\$ $/\$ $/\$ #
18		sqap0 11065	. . . . . . . 8 # #
19	18	biimpar 297	. . . . . . 7 $/\$ # #
20	13, 17, 19	syl2anc 415	. . . . . 6 $/\$ $/\$ $/\$ #
21	16, 14, 20	absdivapd 11985	. . . . 5 $/\$ $/\$ $/\$
22	7, 21	eqtr4d 2274	. . . 4 $/\$ $/\$ $/\$
23	22	oveq2d 6104	. . 3 $/\$ $/\$ $/\$
24	16	abscld 11971	. . . . 5 $/\$ $/\$ $/\$
25	24	recnd 8361	. . . 4 $/\$ $/\$ $/\$
26	25, 14, 20	divcanap2d 9131	. . 3 $/\$ $/\$ $/\$
27	10, 15, 14, 20	divsubdirapd 9169	. . . . . 6 $/\$ $/\$ $/\$
28	9, 13, 17	sqdivapd 11146	. . . . . . . 8 $/\$ $/\$ $/\$
29	28	eqcomd 2244	. . . . . . 7 $/\$ $/\$ $/\$
30	11	nnred 9327	. . . . . . . . 9 $/\$ $/\$ $/\$
31	11	nnnn0d 9632	. . . . . . . . . 10 $/\$ $/\$ $/\$
32	31	nn0ge0d 9635	. . . . . . . . 9 $/\$ $/\$ $/\$
33		remsqsqrt 11821	. . . . . . . . 9 $/\$
34	30, 32, 33	syl2anc 415	. . . . . . . 8 $/\$ $/\$ $/\$
35	30, 32	resqrtcld 11953	. . . . . . . . . 10 $/\$ $/\$ $/\$
36	35	recnd 8361	. . . . . . . . 9 $/\$ $/\$ $/\$
37	36	sqvald 11130	. . . . . . . 8 $/\$ $/\$ $/\$
38	12, 14, 20	divcanap4d 9135	. . . . . . . 8 $/\$ $/\$ $/\$
39	34, 37, 38	3eqtr4rd 2282	. . . . . . 7 $/\$ $/\$ $/\$
40	29, 39	oveq12d 6106	. . . . . 6 $/\$ $/\$ $/\$
41	9, 13, 17	divclapd 9129	. . . . . . . 8 $/\$ $/\$ $/\$
42		subsq 11105	. . . . . . . 8 $/\$
43	41, 36, 42	syl2anc 415	. . . . . . 7 $/\$ $/\$ $/\$
44	41, 36	addcld 8352	. . . . . . . 8 $/\$ $/\$ $/\$
45	8	nnred 9327	. . . . . . . . . . 11 $/\$ $/\$ $/\$
46	45, 1	nndivred 9364	. . . . . . . . . 10 $/\$ $/\$ $/\$
47	46, 35	resubcld 8716	. . . . . . . . 9 $/\$ $/\$ $/\$
48	47	recnd 8361	. . . . . . . 8 $/\$ $/\$ $/\$
49	44, 48	mulcomd 8354	. . . . . . 7 $/\$ $/\$ $/\$
50	43, 49	eqtrd 2271	. . . . . 6 $/\$ $/\$ $/\$
51	27, 40, 50	3eqtrd 2275	. . . . 5 $/\$ $/\$ $/\$
52	51	fveq2d 5702	. . . 4 $/\$ $/\$ $/\$
53	52	oveq2d 6104	. . 3 $/\$ $/\$ $/\$
54	23, 26, 53	3eqtr3d 2279	. 2 $/\$ $/\$ $/\$
55	48, 44	absmuld 11984	. . . 4 $/\$ $/\$ $/\$
56	55	oveq2d 6104	. . 3 $/\$ $/\$ $/\$
57	48	abscld 11971	. . . . . 6 $/\$ $/\$ $/\$
58	44	abscld 11971	. . . . . 6 $/\$ $/\$ $/\$
59	57, 58	remulcld 8363	. . . . 5 $/\$ $/\$ $/\$
60	3, 59	remulcld 8363	. . . 4 $/\$ $/\$ $/\$
61		2nn0 9592	. . . . . . . . 9
62	61	nn0negzi 9691	. . . . . . . 8
63	62	a1i 9	. . . . . . 7 $/\$ $/\$ $/\$
64	2, 17, 63	reexpclzapd 11158	. . . . . 6 $/\$ $/\$ $/\$
65	64, 58	remulcld 8363	. . . . 5 $/\$ $/\$ $/\$
66	3, 65	remulcld 8363	. . . 4 $/\$ $/\$ $/\$
67		1red 8348	. . . . 5 $/\$ $/\$ $/\$
68		2re 9384	. . . . . . 7
69	68	a1i 9	. . . . . 6 $/\$ $/\$ $/\$
70	69, 35	remulcld 8363	. . . . 5 $/\$ $/\$ $/\$
71	67, 70	readdcld 8362	. . . 4 $/\$ $/\$ $/\$
72		simpr 110	. . . . . 6 $/\$ $/\$ $/\$
73	46, 35	readdcld 8362	. . . . . . . . 9 $/\$ $/\$ $/\$
74	8	nngt0d 9358	. . . . . . . . . . 11 $/\$ $/\$ $/\$
75	1	nngt0d 9358	. . . . . . . . . . 11 $/\$ $/\$ $/\$
76	45, 2, 74, 75	divgt0d 9274	. . . . . . . . . 10 $/\$ $/\$ $/\$
77	11	nngt0d 9358	. . . . . . . . . . 11 $/\$ $/\$ $/\$
78		sqrtgt0 11823	. . . . . . . . . . 11 $/\$
79	30, 77, 78	syl2anc 415	. . . . . . . . . 10 $/\$ $/\$ $/\$
80	46, 35, 76, 79	addgt0d 8857	. . . . . . . . 9 $/\$ $/\$ $/\$
81	73, 80	gt0ap0d 8966	. . . . . . . 8 $/\$ $/\$ $/\$ #
82		absgt0ap 11889	. . . . . . . . 9 #
83	82	biimpa 296	. . . . . . . 8 $/\$ #
84	44, 81, 83	syl2anc 415	. . . . . . 7 $/\$ $/\$ $/\$
85		ltmul1 8929	. . . . . . 7 $/\$ $/\$ $/\$
86	57, 64, 58, 84, 85	syl112anc 1282	. . . . . 6 $/\$ $/\$ $/\$
87	72, 86	mpbid 147	. . . . 5 $/\$ $/\$ $/\$
88	2, 17	sqgt0apd 11161	. . . . . 6 $/\$ $/\$ $/\$
89		ltmul2 9195	. . . . . 6 $/\$ $/\$ $/\$
90	59, 65, 3, 88, 89	syl112anc 1282	. . . . 5 $/\$ $/\$ $/\$
91	87, 90	mpbid 147	. . . 4 $/\$ $/\$ $/\$
92	13, 17, 63	expclzapd 11138	. . . . . . 7 $/\$ $/\$ $/\$
93	58	recnd 8361	. . . . . . 7 $/\$ $/\$ $/\$
94		mulass 8317	. . . . . . . 8 $/\$ $/\$
95	94	eqcomd 2244	. . . . . . 7 $/\$ $/\$
96	14, 92, 93, 95	syl3anc 1278	. . . . . 6 $/\$ $/\$ $/\$
97	61	a1i 9	. . . . . . . . . 10 $/\$ $/\$ $/\$
98		expnegap0 11006	. . . . . . . . . 10 $/\$ # $/\$
99	13, 17, 97, 98	syl3anc 1278	. . . . . . . . 9 $/\$ $/\$ $/\$
100	99	oveq2d 6104	. . . . . . . 8 $/\$ $/\$ $/\$
101	14, 20	recidapd 9122	. . . . . . . 8 $/\$ $/\$ $/\$
102	100, 101	eqtrd 2271	. . . . . . 7 $/\$ $/\$ $/\$
103	102	oveq1d 6103	. . . . . 6 $/\$ $/\$ $/\$
104	93	mullidd 8351	. . . . . 6 $/\$ $/\$ $/\$
105	96, 103, 104	3eqtrd 2275	. . . . 5 $/\$ $/\$ $/\$
106	41, 36	addcomd 8485	. . . . . . . 8 $/\$ $/\$ $/\$
107		ppncan 8576	. . . . . . . . . 10 $/\$ $/\$
108	107	eqcomd 2244	. . . . . . . . 9 $/\$ $/\$
109	36, 36, 41, 108	syl3anc 1278	. . . . . . . 8 $/\$ $/\$ $/\$
110	36, 36	addcld 8352	. . . . . . . . . 10 $/\$ $/\$ $/\$
111	110, 48	addcomd 8485	. . . . . . . . 9 $/\$ $/\$ $/\$
112		2times 9442	. . . . . . . . . . . 12
113	112	eqcomd 2244	. . . . . . . . . . 11
114	36, 113	syl 14	. . . . . . . . . 10 $/\$ $/\$ $/\$
115	114	oveq2d 6104	. . . . . . . . 9 $/\$ $/\$ $/\$
116	111, 115	eqtrd 2271	. . . . . . . 8 $/\$ $/\$ $/\$
117	106, 109, 116	3eqtrd 2275	. . . . . . 7 $/\$ $/\$ $/\$
118	117	fveq2d 5702	. . . . . 6 $/\$ $/\$ $/\$
119	47, 70	readdcld 8362	. . . . . . . . 9 $/\$ $/\$ $/\$
120	119	recnd 8361	. . . . . . . 8 $/\$ $/\$ $/\$
121	120	abscld 11971	. . . . . . 7 $/\$ $/\$ $/\$
122	70	recnd 8361	. . . . . . . . 9 $/\$ $/\$ $/\$
123	122	abscld 11971	. . . . . . . 8 $/\$ $/\$ $/\$
124	57, 123	readdcld 8362	. . . . . . 7 $/\$ $/\$ $/\$
125	48, 122	abstrid 11986	. . . . . . 7 $/\$ $/\$ $/\$
126		0le2 9404	. . . . . . . . . . . 12
127	126	a1i 9	. . . . . . . . . . 11 $/\$ $/\$ $/\$
128	30, 32	sqrtge0d 11956	. . . . . . . . . . 11 $/\$ $/\$ $/\$
129	69, 35, 127, 128	mulge0d 8958	. . . . . . . . . 10 $/\$ $/\$ $/\$
130	70, 129	absidd 11957	. . . . . . . . 9 $/\$ $/\$ $/\$
131	130	oveq2d 6104	. . . . . . . 8 $/\$ $/\$ $/\$
132	1	nnsqcld 11154	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
133	132	nnge1d 9357	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
134		0lt1 8461	. . . . . . . . . . . . . . . 16
135	134	a1i 9	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
136		lerec 9223	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
137	67, 135, 3, 88, 136	syl22anc 1279	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
138	133, 137	mpbid 147	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
139		1div1e1 9043	. . . . . . . . . . . . 13
140	138, 139	breqtrdi 4172	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
141	99, 140	eqbrtrd 4153	. . . . . . . . . . 11 $/\$ $/\$ $/\$
142	57, 64, 67, 72, 141	ltletrd 8759	. . . . . . . . . 10 $/\$ $/\$ $/\$
143	57, 67, 142	ltled 8453	. . . . . . . . 9 $/\$ $/\$ $/\$
144	57, 67, 70, 143	leadd1dd 8895	. . . . . . . 8 $/\$ $/\$ $/\$
145	131, 144	eqbrtrd 4153	. . . . . . 7 $/\$ $/\$ $/\$
146	121, 124, 71, 125, 145	letrd 8458	. . . . . 6 $/\$ $/\$ $/\$
147	118, 146	eqbrtrd 4153	. . . . 5 $/\$ $/\$ $/\$
148	105, 147	eqbrtrd 4153	. . . 4 $/\$ $/\$ $/\$
149	60, 66, 71, 91, 148	ltletrd 8759	. . 3 $/\$ $/\$ $/\$
150	56, 149	eqbrtrd 4153	. 2 $/\$ $/\$ $/\$
151	54, 150	eqbrtrd 4153	1 $/\$ $/\$ $/\$

Colors of variables: wff set class

This proof depends on syntax axioms:

wi 4 $/\$ wa 104

wb 105 $/\$ w3a 1009

wceq 1402

wcel 2209 class class class wbr 4131

cfv 5380 (class class class)co 6088

cc 8184

cr 8185

cc0 8186

c1 8187

caddc 8189

cmul 8191

clt 8367

cle 8368

cmin 8505

cneg 8506 # cap 8918

cdiv 9011

cn 9314

c2 9365

cn0 9575

cz 9656

cexp 10997

csqrt 11785

cabs 11786

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-coll 4248 ax-sep 4251 ax-nul 4261 ax-pow 4313 ax-pr 4348 ax-un 4580 ax-setind 4686 ax-iinf 4737 ax-cnex 8277 ax-resscn 8278 ax-1cn 8279 ax-1re 8280 ax-icn 8281 ax-addcl 8282 ax-addrcl 8283 ax-mulcl 8284 ax-mulrcl 8285 ax-addcom 8286 ax-mulcom 8287 ax-addass 8288 ax-mulass 8289 ax-distr 8290 ax-i2m1 8291 ax-0lt1 8292 ax-1rid 8293 ax-0id 8294 ax-rnegex 8295 ax-precex 8296 ax-cnre 8297 ax-pre-ltirr 8298 ax-pre-ltwlin 8299 ax-pre-lttrn 8300 ax-pre-apti 8301 ax-pre-ltadd 8302 ax-pre-mulgt0 8303 ax-pre-mulext 8304 ax-arch 8305 ax-caucvg 8306

This proof depends on definitions: df-bi 117 df-dc 847 df-3or 1010 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-nel 2516 df-ral 2533 df-rex 2534 df-reu 2535 df-rmo 2536 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-nul 3521 df-if 3639 df-pw 3690 df-sn 3715 df-pr 3716 df-op 3718 df-uni 3936 df-int 3971 df-iun 4014 df-br 4132 df-opab 4194 df-mpt 4195 df-tr 4232 df-id 4440 df-po 4443 df-iso 4444 df-iord 4513 df-on 4515 df-ilim 4516 df-suc 4518 df-iom 4740 df-xp 4782 df-rel 4783 df-cnv 4784 df-co 4785 df-dm 4786 df-rn 4787 df-res 4788 df-ima 4789 df-iota 5340 df-fun 5382 df-fn 5383 df-f 5384 df-f1 5385 df-fo 5386 df-f1o 5387 df-fv 5388 df-riota 6041 df-ov 6091 df-oprab 6092 df-mpo 6093 df-1st 6378 df-2nd 6379 df-recs 6580 df-frec 6666 df-pnf 8369 df-mnf 8370 df-xr 8371 df-ltxr 8372 df-le 8373 df-sub 8507 df-neg 8508 df-reap 8912 df-ap 8919 df-div 9012 df-inn 9315 df-2 9373 df-3 9374 df-4 9375 df-n0 9576 df-z 9657 df-uz 9939 df-rp 10073 df-seqfrec 10907 df-exp 10998 df-cj 11630 df-re 11631 df-im 11632 df-rsqrt 11787 df-abs 11788

This theorem is used by: pellexlem3 16243

W3C validator