resqrexlemover - Intuitionistic Logic Explorer

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

Theorem resqrexlemover 11720

Description: Lemma for resqrex 11736. Each element of the sequence is an overestimate. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.)

**Hypotheses**
Ref	Expression
resqrexlemex.seq
resqrexlemex.a
resqrexlemex.agt0

**Assertion**
Ref	Expression
resqrexlemover	$/\$

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

Proof of Theorem resqrexlemover Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 5675	. . . . . 6
2	1	oveq1d 6073	. . . . 5
3	2	breq2d 4126	. . . 4
4	3	imbi2d 230	. . 3
5		fveq2 5675	. . . . . 6
6	5	oveq1d 6073	. . . . 5
7	6	breq2d 4126	. . . 4
8	7	imbi2d 230	. . 3
9		fveq2 5675	. . . . . 6
10	9	oveq1d 6073	. . . . 5
11	10	breq2d 4126	. . . 4
12	11	imbi2d 230	. . 3
13		fveq2 5675	. . . . . 6
14	13	oveq1d 6073	. . . . 5
15	14	breq2d 4126	. . . 4
16	15	imbi2d 230	. . 3
17		resqrexlemex.a	. . . . 5
18	17	resqcld 11086	. . . . . 6
19		2re 9324	. . . . . . . 8
20	19	a1i 9	. . . . . . 7
21	20, 17	remulcld 8320	. . . . . 6
22	18, 21	readdcld 8319	. . . . 5
23		1red 8305	. . . . . 6
24	22, 23	readdcld 8319	. . . . 5
25	17	recnd 8318	. . . . . . . 8
26	25	mullidd 8308	. . . . . . 7
27		resqrexlemex.agt0	. . . . . . . 8
28		1le2 9463	. . . . . . . . 9
29		lemul1a 9149	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
30	28, 29	mpan2 425	. . . . . . . 8 $/\$ $/\$ $/\$
31	23, 20, 17, 27, 30	syl112anc 1278	. . . . . . 7
32	26, 31	eqbrtrrd 4138	. . . . . 6
33	17	sqge0d 11087	. . . . . . 7
34	21, 18	addge02d 8825	. . . . . . 7
35	33, 34	mpbid 147	. . . . . 6
36	17, 21, 22, 32, 35	letrd 8413	. . . . 5
37	22	ltp1d 9221	. . . . 5
38	17, 22, 24, 36, 37	lelttrd 8414	. . . 4
39		resqrexlemex.seq	. . . . . . . 8
40	39, 17, 27	resqrexlemf1 11718	. . . . . . 7
41		1cnd 8306	. . . . . . . 8
42	41, 25	addcomd 8440	. . . . . . 7
43	40, 42	eqtrd 2267	. . . . . 6
44	43	oveq1d 6073	. . . . 5
45		binom21 11038	. . . . . 6
46	25, 45	syl 14	. . . . 5
47	44, 46	eqtrd 2267	. . . 4
48	38, 47	breqtrrd 4142	. . 3
49	39, 17, 27	resqrexlemf 11717	. . . . . . . . . . . . . 14
50	49	ffvelcdmda 5817	. . . . . . . . . . . . 13 $/\$
51	50	rpred 10047	. . . . . . . . . . . 12 $/\$
52	17	adantr 276	. . . . . . . . . . . . 13 $/\$
53	52, 50	rerpdivcld 10079	. . . . . . . . . . . 12 $/\$
54	51, 53	resubcld 8671	. . . . . . . . . . 11 $/\$
55	54	adantr 276	. . . . . . . . . 10 $/\$ $/\$
56	55	resqcld 11086	. . . . . . . . 9 $/\$ $/\$
57		4re 9331	. . . . . . . . . 10
58	57	a1i 9	. . . . . . . . 9 $/\$ $/\$
59	51	resqcld 11086	. . . . . . . . . . . . . . 15 $/\$
60	59, 52	resubcld 8671	. . . . . . . . . . . . . 14 $/\$
61	60	adantr 276	. . . . . . . . . . . . 13 $/\$ $/\$
62	51	adantr 276	. . . . . . . . . . . . 13 $/\$ $/\$
63	52, 59	posdifd 8823	. . . . . . . . . . . . . 14 $/\$
64	63	biimpa 296	. . . . . . . . . . . . 13 $/\$ $/\$
65	50	rpgt0d 10050	. . . . . . . . . . . . . 14 $/\$
66	65	adantr 276	. . . . . . . . . . . . 13 $/\$ $/\$
67	61, 62, 64, 66	divgt0d 9226	. . . . . . . . . . . 12 $/\$ $/\$
68	51	recnd 8318	. . . . . . . . . . . . . . . 16 $/\$
69	68	sqcld 11058	. . . . . . . . . . . . . . 15 $/\$
70	69	adantr 276	. . . . . . . . . . . . . 14 $/\$ $/\$
71	25	adantr 276	. . . . . . . . . . . . . . 15 $/\$
72	71	adantr 276	. . . . . . . . . . . . . 14 $/\$ $/\$
73	68	adantr 276	. . . . . . . . . . . . . 14 $/\$ $/\$
74	50	rpap0d 10053	. . . . . . . . . . . . . . 15 $/\$ #
75	74	adantr 276	. . . . . . . . . . . . . 14 $/\$ $/\$ #
76	70, 72, 73, 75	divsubdirapd 9121	. . . . . . . . . . . . 13 $/\$ $/\$
77	73	sqvald 11057	. . . . . . . . . . . . . . . 16 $/\$ $/\$
78	77	oveq1d 6073	. . . . . . . . . . . . . . 15 $/\$ $/\$
79	73, 73, 75	divcanap3d 9086	. . . . . . . . . . . . . . 15 $/\$ $/\$
80	78, 79	eqtrd 2267	. . . . . . . . . . . . . 14 $/\$ $/\$
81	80	oveq1d 6073	. . . . . . . . . . . . 13 $/\$ $/\$
82	76, 81	eqtrd 2267	. . . . . . . . . . . 12 $/\$ $/\$
83	67, 82	breqtrd 4140	. . . . . . . . . . 11 $/\$ $/\$
84	55, 83	gt0ap0d 8920	. . . . . . . . . 10 $/\$ $/\$ #
85	55, 84	sqgt0apd 11088	. . . . . . . . 9 $/\$ $/\$
86		4pos 9351	. . . . . . . . . 10
87	86	a1i 9	. . . . . . . . 9 $/\$ $/\$
88	56, 58, 85, 87	divgt0d 9226	. . . . . . . 8 $/\$ $/\$
89	57, 86	gt0ap0ii 8919	. . . . . . . . . . 11 #
90	89	a1i 9	. . . . . . . . . 10 $/\$ $/\$ #
91	56, 58, 90	redivclapd 9126	. . . . . . . . 9 $/\$ $/\$
92	52	adantr 276	. . . . . . . . 9 $/\$ $/\$
93	91, 92	ltaddpos2d 8821	. . . . . . . 8 $/\$ $/\$
94	88, 93	mpbid 147	. . . . . . 7 $/\$ $/\$
95	39, 17, 27	resqrexlemfp1 11719	. . . . . . . . . . . . . 14 $/\$
96	95	oveq1d 6073	. . . . . . . . . . . . 13 $/\$
97	51, 53	readdcld 8319	. . . . . . . . . . . . . . 15 $/\$
98	97	recnd 8318	. . . . . . . . . . . . . 14 $/\$
99		2cnd 9327	. . . . . . . . . . . . . 14 $/\$
100		2ap0 9347	. . . . . . . . . . . . . . 15 #
101	100	a1i 9	. . . . . . . . . . . . . 14 $/\$ #
102	98, 99, 101	sqdivapd 11073	. . . . . . . . . . . . 13 $/\$
103	96, 102	eqtrd 2267	. . . . . . . . . . . 12 $/\$
104		sq2 11021	. . . . . . . . . . . . 13
105	104	oveq2i 6069	. . . . . . . . . . . 12
106	103, 105	eqtrdi 2283	. . . . . . . . . . 11 $/\$
107	71, 68, 74	divcanap2d 9083	. . . . . . . . . . . . . . . . 17 $/\$
108	107	oveq2d 6074	. . . . . . . . . . . . . . . 16 $/\$
109	108	oveq2d 6074	. . . . . . . . . . . . . . 15 $/\$
110	109	oveq1d 6073	. . . . . . . . . . . . . 14 $/\$
111	110	oveq1d 6073	. . . . . . . . . . . . 13 $/\$
112	53	recnd 8318	. . . . . . . . . . . . . . 15 $/\$
113		binom2sub 11039	. . . . . . . . . . . . . . 15 $/\$
114	68, 112, 113	syl2anc 411	. . . . . . . . . . . . . 14 $/\$
115	114	oveq1d 6073	. . . . . . . . . . . . 13 $/\$
116		binom2 11037	. . . . . . . . . . . . . . . 16 $/\$
117	68, 112, 116	syl2anc 411	. . . . . . . . . . . . . . 15 $/\$
118	108	oveq2d 6074	. . . . . . . . . . . . . . . 16 $/\$
119	118	oveq1d 6073	. . . . . . . . . . . . . . 15 $/\$
120	117, 119	eqtrd 2267	. . . . . . . . . . . . . 14 $/\$
121	99, 71	mulcld 8310	. . . . . . . . . . . . . . . . . 18 $/\$
122	121	negcld 8587	. . . . . . . . . . . . . . . . 17 $/\$
123		4cn 9332	. . . . . . . . . . . . . . . . . . 19
124	123	a1i 9	. . . . . . . . . . . . . . . . . 18 $/\$
125	124, 71	mulcld 8310	. . . . . . . . . . . . . . . . 17 $/\$
126	69, 122, 125	addassd 8312	. . . . . . . . . . . . . . . 16 $/\$
127	69, 121	negsubd 8606	. . . . . . . . . . . . . . . . 17 $/\$
128	127	oveq1d 6073	. . . . . . . . . . . . . . . 16 $/\$
129		2cn 9325	. . . . . . . . . . . . . . . . . . . . . 22
130	129	negcli 8557	. . . . . . . . . . . . . . . . . . . . 21
131	130	a1i 9	. . . . . . . . . . . . . . . . . . . 20 $/\$
132	131, 124, 71	adddird 8315	. . . . . . . . . . . . . . . . . . 19 $/\$
133	99, 71	mulneg1d 8701	. . . . . . . . . . . . . . . . . . . 20 $/\$
134	133	oveq1d 6073	. . . . . . . . . . . . . . . . . . 19 $/\$
135	132, 134	eqtrd 2267	. . . . . . . . . . . . . . . . . 18 $/\$
136	130, 129, 129	addassi 8298	. . . . . . . . . . . . . . . . . . . 20
137	129	subidi 8560	. . . . . . . . . . . . . . . . . . . . . . . 24
138	137	negeqi 8483	. . . . . . . . . . . . . . . . . . . . . . 23
139	129, 129	negsubdii 8574	. . . . . . . . . . . . . . . . . . . . . . 23
140		neg0 8535	. . . . . . . . . . . . . . . . . . . . . . 23
141	138, 139, 140	3eqtr3i 2263	. . . . . . . . . . . . . . . . . . . . . 22
142	141	oveq1i 6068	. . . . . . . . . . . . . . . . . . . . 21
143	129	addlidi 8432	. . . . . . . . . . . . . . . . . . . . 21
144	142, 143	eqtri 2255	. . . . . . . . . . . . . . . . . . . 20
145		2p2e4 9381	. . . . . . . . . . . . . . . . . . . . 21
146	145	oveq2i 6069	. . . . . . . . . . . . . . . . . . . 20
147	136, 144, 146	3eqtr3ri 2264	. . . . . . . . . . . . . . . . . . 19
148	147	oveq1i 6068	. . . . . . . . . . . . . . . . . 18
149	135, 148	eqtr3di 2282	. . . . . . . . . . . . . . . . 17 $/\$
150	149	oveq2d 6074	. . . . . . . . . . . . . . . 16 $/\$
151	126, 128, 150	3eqtr3rd 2276	. . . . . . . . . . . . . . 15 $/\$
152	151	oveq1d 6073	. . . . . . . . . . . . . 14 $/\$
153	19	a1i 9	. . . . . . . . . . . . . . . . 17 $/\$
154	153, 52	remulcld 8320	. . . . . . . . . . . . . . . 16 $/\$
155	59, 154	resubcld 8671	. . . . . . . . . . . . . . 15 $/\$
156	57	a1i 9	. . . . . . . . . . . . . . . 16 $/\$
157	156, 52	remulcld 8320	. . . . . . . . . . . . . . 15 $/\$
158	53	resqcld 11086	. . . . . . . . . . . . . . 15 $/\$
159		recn 8276	. . . . . . . . . . . . . . . . 17
160		recn 8276	. . . . . . . . . . . . . . . . 17
161		addcom 8426	. . . . . . . . . . . . . . . . 17 $/\$
162	159, 160, 161	syl2an 289	. . . . . . . . . . . . . . . 16 $/\$
163	162	adantl 277	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
164		recn 8276	. . . . . . . . . . . . . . . . 17
165		addass 8273	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
166	159, 160, 164, 165	syl3an 1316	. . . . . . . . . . . . . . . 16 $/\$ $/\$
167	166	adantl 277	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
168	155, 157, 158, 163, 167	caov32d 6243	. . . . . . . . . . . . . 14 $/\$
169	120, 152, 168	3eqtrd 2271	. . . . . . . . . . . . 13 $/\$
170	111, 115, 169	3eqtr4rd 2278	. . . . . . . . . . . 12 $/\$
171	170	oveq1d 6073	. . . . . . . . . . 11 $/\$
172	106, 171	eqtrd 2267	. . . . . . . . . 10 $/\$
173	68, 112	subcld 8600	. . . . . . . . . . . 12 $/\$
174	173	sqcld 11058	. . . . . . . . . . 11 $/\$
175	89	a1i 9	. . . . . . . . . . 11 $/\$ #
176	174, 125, 124, 175	divdirapd 9120	. . . . . . . . . 10 $/\$
177	71, 124, 175	divcanap3d 9086	. . . . . . . . . . 11 $/\$
178	177	oveq2d 6074	. . . . . . . . . 10 $/\$
179	172, 176, 178	3eqtrd 2271	. . . . . . . . 9 $/\$
180	179	breq2d 4126	. . . . . . . 8 $/\$
181	180	adantr 276	. . . . . . 7 $/\$ $/\$
182	94, 181	mpbird 167	. . . . . 6 $/\$ $/\$
183	182	ex 115	. . . . 5 $/\$
184	183	expcom 116	. . . 4
185	184	a2d 26	. . 3
186	4, 8, 12, 16, 48, 185	nnind 9270	. 2
187	186	impcom 125	1 $/\$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wb 105 $/\$ w3a 1005

wceq 1398

wcel 2205

csn 3694 class class class wbr 4114

cxp 4752

cfv 5357 (class class class)co 6058

cmpo 6060

cc 8141

cr 8142

cc0 8143

c1 8144

caddc 8146

cmul 8148

clt 8324

cle 8325

cmin 8460

cneg 8461 # cap 8872

cdiv 8963

cn 9254

c2 9305

c4 9307

crp 10004

cseq 10833

cexp 10924

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 619 ax-in2 620 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2207 ax-14 2208 ax-ext 2216 ax-coll 4230 ax-sep 4233 ax-nul 4241 ax-pow 4292 ax-pr 4327 ax-un 4559 ax-setind 4664 ax-iinf 4715 ax-cnex 8234 ax-resscn 8235 ax-1cn 8236 ax-1re 8237 ax-icn 8238 ax-addcl 8239 ax-addrcl 8240 ax-mulcl 8241 ax-mulrcl 8242 ax-addcom 8243 ax-mulcom 8244 ax-addass 8245 ax-mulass 8246 ax-distr 8247 ax-i2m1 8248 ax-0lt1 8249 ax-1rid 8250 ax-0id 8251 ax-rnegex 8252 ax-precex 8253 ax-cnre 8254 ax-pre-ltirr 8255 ax-pre-ltwlin 8256 ax-pre-lttrn 8257 ax-pre-apti 8258 ax-pre-ltadd 8259 ax-pre-mulgt0 8260 ax-pre-mulext 8261

This theorem depends on definitions: df-bi 117 df-dc 843 df-3or 1006 df-3an 1007 df-tru 1401 df-fal 1404 df-nf 1510 df-sb 1812 df-eu 2085 df-mo 2086 df-clab 2221 df-cleq 2227 df-clel 2230 df-nfc 2375 df-ne 2415 df-nel 2510 df-ral 2527 df-rex 2528 df-reu 2529 df-rmo 2530 df-rab 2531 df-v 2817 df-sbc 3046 df-csb 3142 df-dif 3216 df-un 3218 df-in 3220 df-ss 3227 df-nul 3513 df-if 3625 df-pw 3676 df-sn 3700 df-pr 3701 df-op 3703 df-uni 3920 df-int 3955 df-iun 3998 df-br 4115 df-opab 4177 df-mpt 4178 df-tr 4214 df-id 4419 df-po 4422 df-iso 4423 df-iord 4492 df-on 4494 df-ilim 4495 df-suc 4497 df-iom 4718 df-xp 4760 df-rel 4761 df-cnv 4762 df-co 4763 df-dm 4764 df-rn 4765 df-res 4766 df-ima 4767 df-iota 5317 df-fun 5359 df-fn 5360 df-f 5361 df-f1 5362 df-fo 5363 df-f1o 5364 df-fv 5365 df-riota 6011 df-ov 6061 df-oprab 6062 df-mpo 6063 df-1st 6347 df-2nd 6348 df-recs 6549 df-frec 6635 df-pnf 8326 df-mnf 8327 df-xr 8328 df-ltxr 8329 df-le 8330 df-sub 8462 df-neg 8463 df-reap 8866 df-ap 8873 df-div 8964 df-inn 9255 df-2 9313 df-3 9314 df-4 9315 df-n0 9514 df-z 9595 df-uz 9872 df-rp 10005 df-seqfrec 10834 df-exp 10925

This theorem is referenced by: resqrexlemdec 11721 resqrexlemcalc2 11725 resqrexlemnmsq 11727 resqrexlemga 11733

W3C validator