resqrexlemover - Intuitionistic Logic Explorer

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

Theorem resqrexlemover 11699

Description: Lemma for resqrex 11715. 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 5672	. . . . . 6
2	1	oveq1d 6067	. . . . 5
3	2	breq2d 4123	. . . 4
4	3	imbi2d 230	. . 3
5		fveq2 5672	. . . . . 6
6	5	oveq1d 6067	. . . . 5
7	6	breq2d 4123	. . . 4
8	7	imbi2d 230	. . 3
9		fveq2 5672	. . . . . 6
10	9	oveq1d 6067	. . . . 5
11	10	breq2d 4123	. . . 4
12	11	imbi2d 230	. . 3
13		fveq2 5672	. . . . . 6
14	13	oveq1d 6067	. . . . 5
15	14	breq2d 4123	. . . 4
16	15	imbi2d 230	. . 3
17		resqrexlemex.a	. . . . 5
18	17	resqcld 11065	. . . . . 6
19		2re 9309	. . . . . . . 8
20	19	a1i 9	. . . . . . 7
21	20, 17	remulcld 8306	. . . . . 6
22	18, 21	readdcld 8305	. . . . 5
23		1red 8291	. . . . . 6
24	22, 23	readdcld 8305	. . . . 5
25	17	recnd 8304	. . . . . . . 8
26	25	mullidd 8294	. . . . . . 7
27		resqrexlemex.agt0	. . . . . . . 8
28		1le2 9448	. . . . . . . . 9
29		lemul1a 9134	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
30	28, 29	mpan2 425	. . . . . . . 8 $/\$ $/\$ $/\$
31	23, 20, 17, 27, 30	syl112anc 1278	. . . . . . 7
32	26, 31	eqbrtrrd 4135	. . . . . 6
33	17	sqge0d 11066	. . . . . . 7
34	21, 18	addge02d 8810	. . . . . . 7
35	33, 34	mpbid 147	. . . . . 6
36	17, 21, 22, 32, 35	letrd 8399	. . . . 5
37	22	ltp1d 9206	. . . . 5
38	17, 22, 24, 36, 37	lelttrd 8400	. . . 4
39		resqrexlemex.seq	. . . . . . . 8
40	39, 17, 27	resqrexlemf1 11697	. . . . . . 7
41		1cnd 8292	. . . . . . . 8
42	41, 25	addcomd 8426	. . . . . . 7
43	40, 42	eqtrd 2267	. . . . . 6
44	43	oveq1d 6067	. . . . 5
45		binom21 11018	. . . . . 6
46	25, 45	syl 14	. . . . 5
47	44, 46	eqtrd 2267	. . . 4
48	38, 47	breqtrrd 4139	. . 3
49	39, 17, 27	resqrexlemf 11696	. . . . . . . . . . . . . 14
50	49	ffvelcdmda 5814	. . . . . . . . . . . . 13 $/\$
51	50	rpred 10032	. . . . . . . . . . . 12 $/\$
52	17	adantr 276	. . . . . . . . . . . . 13 $/\$
53	52, 50	rerpdivcld 10064	. . . . . . . . . . . 12 $/\$
54	51, 53	resubcld 8656	. . . . . . . . . . 11 $/\$
55	54	adantr 276	. . . . . . . . . 10 $/\$ $/\$
56	55	resqcld 11065	. . . . . . . . 9 $/\$ $/\$
57		4re 9316	. . . . . . . . . 10
58	57	a1i 9	. . . . . . . . 9 $/\$ $/\$
59	51	resqcld 11065	. . . . . . . . . . . . . . 15 $/\$
60	59, 52	resubcld 8656	. . . . . . . . . . . . . 14 $/\$
61	60	adantr 276	. . . . . . . . . . . . 13 $/\$ $/\$
62	51	adantr 276	. . . . . . . . . . . . 13 $/\$ $/\$
63	52, 59	posdifd 8808	. . . . . . . . . . . . . 14 $/\$
64	63	biimpa 296	. . . . . . . . . . . . 13 $/\$ $/\$
65	50	rpgt0d 10035	. . . . . . . . . . . . . 14 $/\$
66	65	adantr 276	. . . . . . . . . . . . 13 $/\$ $/\$
67	61, 62, 64, 66	divgt0d 9211	. . . . . . . . . . . 12 $/\$ $/\$
68	51	recnd 8304	. . . . . . . . . . . . . . . 16 $/\$
69	68	sqcld 11037	. . . . . . . . . . . . . . 15 $/\$
70	69	adantr 276	. . . . . . . . . . . . . 14 $/\$ $/\$
71	25	adantr 276	. . . . . . . . . . . . . . 15 $/\$
72	71	adantr 276	. . . . . . . . . . . . . 14 $/\$ $/\$
73	68	adantr 276	. . . . . . . . . . . . . 14 $/\$ $/\$
74	50	rpap0d 10038	. . . . . . . . . . . . . . 15 $/\$ #
75	74	adantr 276	. . . . . . . . . . . . . 14 $/\$ $/\$ #
76	70, 72, 73, 75	divsubdirapd 9106	. . . . . . . . . . . . 13 $/\$ $/\$
77	73	sqvald 11036	. . . . . . . . . . . . . . . 16 $/\$ $/\$
78	77	oveq1d 6067	. . . . . . . . . . . . . . 15 $/\$ $/\$
79	73, 73, 75	divcanap3d 9071	. . . . . . . . . . . . . . 15 $/\$ $/\$
80	78, 79	eqtrd 2267	. . . . . . . . . . . . . 14 $/\$ $/\$
81	80	oveq1d 6067	. . . . . . . . . . . . 13 $/\$ $/\$
82	76, 81	eqtrd 2267	. . . . . . . . . . . 12 $/\$ $/\$
83	67, 82	breqtrd 4137	. . . . . . . . . . 11 $/\$ $/\$
84	55, 83	gt0ap0d 8905	. . . . . . . . . 10 $/\$ $/\$ #
85	55, 84	sqgt0apd 11067	. . . . . . . . 9 $/\$ $/\$
86		4pos 9336	. . . . . . . . . 10
87	86	a1i 9	. . . . . . . . 9 $/\$ $/\$
88	56, 58, 85, 87	divgt0d 9211	. . . . . . . 8 $/\$ $/\$
89	57, 86	gt0ap0ii 8904	. . . . . . . . . . 11 #
90	89	a1i 9	. . . . . . . . . 10 $/\$ $/\$ #
91	56, 58, 90	redivclapd 9111	. . . . . . . . 9 $/\$ $/\$
92	52	adantr 276	. . . . . . . . 9 $/\$ $/\$
93	91, 92	ltaddpos2d 8806	. . . . . . . 8 $/\$ $/\$
94	88, 93	mpbid 147	. . . . . . 7 $/\$ $/\$
95	39, 17, 27	resqrexlemfp1 11698	. . . . . . . . . . . . . 14 $/\$
96	95	oveq1d 6067	. . . . . . . . . . . . 13 $/\$
97	51, 53	readdcld 8305	. . . . . . . . . . . . . . 15 $/\$
98	97	recnd 8304	. . . . . . . . . . . . . 14 $/\$
99		2cnd 9312	. . . . . . . . . . . . . 14 $/\$
100		2ap0 9332	. . . . . . . . . . . . . . 15 #
101	100	a1i 9	. . . . . . . . . . . . . 14 $/\$ #
102	98, 99, 101	sqdivapd 11052	. . . . . . . . . . . . 13 $/\$
103	96, 102	eqtrd 2267	. . . . . . . . . . . 12 $/\$
104		sq2 11001	. . . . . . . . . . . . 13
105	104	oveq2i 6063	. . . . . . . . . . . 12
106	103, 105	eqtrdi 2283	. . . . . . . . . . 11 $/\$
107	71, 68, 74	divcanap2d 9068	. . . . . . . . . . . . . . . . 17 $/\$
108	107	oveq2d 6068	. . . . . . . . . . . . . . . 16 $/\$
109	108	oveq2d 6068	. . . . . . . . . . . . . . 15 $/\$
110	109	oveq1d 6067	. . . . . . . . . . . . . 14 $/\$
111	110	oveq1d 6067	. . . . . . . . . . . . 13 $/\$
112	53	recnd 8304	. . . . . . . . . . . . . . 15 $/\$
113		binom2sub 11019	. . . . . . . . . . . . . . 15 $/\$
114	68, 112, 113	syl2anc 411	. . . . . . . . . . . . . 14 $/\$
115	114	oveq1d 6067	. . . . . . . . . . . . 13 $/\$
116		binom2 11017	. . . . . . . . . . . . . . . 16 $/\$
117	68, 112, 116	syl2anc 411	. . . . . . . . . . . . . . 15 $/\$
118	108	oveq2d 6068	. . . . . . . . . . . . . . . 16 $/\$
119	118	oveq1d 6067	. . . . . . . . . . . . . . 15 $/\$
120	117, 119	eqtrd 2267	. . . . . . . . . . . . . 14 $/\$
121	99, 71	mulcld 8296	. . . . . . . . . . . . . . . . . 18 $/\$
122	121	negcld 8573	. . . . . . . . . . . . . . . . 17 $/\$
123		4cn 9317	. . . . . . . . . . . . . . . . . . 19
124	123	a1i 9	. . . . . . . . . . . . . . . . . 18 $/\$
125	124, 71	mulcld 8296	. . . . . . . . . . . . . . . . 17 $/\$
126	69, 122, 125	addassd 8298	. . . . . . . . . . . . . . . 16 $/\$
127	69, 121	negsubd 8592	. . . . . . . . . . . . . . . . 17 $/\$
128	127	oveq1d 6067	. . . . . . . . . . . . . . . 16 $/\$
129		2cn 9310	. . . . . . . . . . . . . . . . . . . . . 22
130	129	negcli 8543	. . . . . . . . . . . . . . . . . . . . 21
131	130	a1i 9	. . . . . . . . . . . . . . . . . . . 20 $/\$
132	131, 124, 71	adddird 8301	. . . . . . . . . . . . . . . . . . 19 $/\$
133	99, 71	mulneg1d 8686	. . . . . . . . . . . . . . . . . . . 20 $/\$
134	133	oveq1d 6067	. . . . . . . . . . . . . . . . . . 19 $/\$
135	132, 134	eqtrd 2267	. . . . . . . . . . . . . . . . . 18 $/\$
136	130, 129, 129	addassi 8284	. . . . . . . . . . . . . . . . . . . 20
137	129	subidi 8546	. . . . . . . . . . . . . . . . . . . . . . . 24
138	137	negeqi 8469	. . . . . . . . . . . . . . . . . . . . . . 23
139	129, 129	negsubdii 8560	. . . . . . . . . . . . . . . . . . . . . . 23
140		neg0 8521	. . . . . . . . . . . . . . . . . . . . . . 23
141	138, 139, 140	3eqtr3i 2263	. . . . . . . . . . . . . . . . . . . . . 22
142	141	oveq1i 6062	. . . . . . . . . . . . . . . . . . . . 21
143	129	addlidi 8418	. . . . . . . . . . . . . . . . . . . . 21
144	142, 143	eqtri 2255	. . . . . . . . . . . . . . . . . . . 20
145		2p2e4 9366	. . . . . . . . . . . . . . . . . . . . 21
146	145	oveq2i 6063	. . . . . . . . . . . . . . . . . . . 20
147	136, 144, 146	3eqtr3ri 2264	. . . . . . . . . . . . . . . . . . 19
148	147	oveq1i 6062	. . . . . . . . . . . . . . . . . 18
149	135, 148	eqtr3di 2282	. . . . . . . . . . . . . . . . 17 $/\$
150	149	oveq2d 6068	. . . . . . . . . . . . . . . 16 $/\$
151	126, 128, 150	3eqtr3rd 2276	. . . . . . . . . . . . . . 15 $/\$
152	151	oveq1d 6067	. . . . . . . . . . . . . 14 $/\$
153	19	a1i 9	. . . . . . . . . . . . . . . . 17 $/\$
154	153, 52	remulcld 8306	. . . . . . . . . . . . . . . 16 $/\$
155	59, 154	resubcld 8656	. . . . . . . . . . . . . . 15 $/\$
156	57	a1i 9	. . . . . . . . . . . . . . . 16 $/\$
157	156, 52	remulcld 8306	. . . . . . . . . . . . . . 15 $/\$
158	53	resqcld 11065	. . . . . . . . . . . . . . 15 $/\$
159		recn 8262	. . . . . . . . . . . . . . . . 17
160		recn 8262	. . . . . . . . . . . . . . . . 17
161		addcom 8412	. . . . . . . . . . . . . . . . 17 $/\$
162	159, 160, 161	syl2an 289	. . . . . . . . . . . . . . . 16 $/\$
163	162	adantl 277	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
164		recn 8262	. . . . . . . . . . . . . . . . 17
165		addass 8259	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
166	159, 160, 164, 165	syl3an 1316	. . . . . . . . . . . . . . . 16 $/\$ $/\$
167	166	adantl 277	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
168	155, 157, 158, 163, 167	caov32d 6237	. . . . . . . . . . . . . 14 $/\$
169	120, 152, 168	3eqtrd 2271	. . . . . . . . . . . . 13 $/\$
170	111, 115, 169	3eqtr4rd 2278	. . . . . . . . . . . 12 $/\$
171	170	oveq1d 6067	. . . . . . . . . . 11 $/\$
172	106, 171	eqtrd 2267	. . . . . . . . . 10 $/\$
173	68, 112	subcld 8586	. . . . . . . . . . . 12 $/\$
174	173	sqcld 11037	. . . . . . . . . . 11 $/\$
175	89	a1i 9	. . . . . . . . . . 11 $/\$ #
176	174, 125, 124, 175	divdirapd 9105	. . . . . . . . . 10 $/\$
177	71, 124, 175	divcanap3d 9071	. . . . . . . . . . 11 $/\$
178	177	oveq2d 6068	. . . . . . . . . 10 $/\$
179	172, 176, 178	3eqtrd 2271	. . . . . . . . 9 $/\$
180	179	breq2d 4123	. . . . . . . 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 9255	. 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 3691 class class class wbr 4111

cxp 4749

cfv 5354 (class class class)co 6052

cmpo 6054

cc 8127

cr 8128

cc0 8129

c1 8130

caddc 8132

cmul 8134

clt 8310

cle 8311

cmin 8446

cneg 8447 # cap 8857

cdiv 8948

cn 9239

c2 9290

c4 9292

crp 9989

cseq 10813

cexp 10904

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 4227 ax-sep 4230 ax-nul 4238 ax-pow 4289 ax-pr 4324 ax-un 4556 ax-setind 4661 ax-iinf 4712 ax-cnex 8220 ax-resscn 8221 ax-1cn 8222 ax-1re 8223 ax-icn 8224 ax-addcl 8225 ax-addrcl 8226 ax-mulcl 8227 ax-mulrcl 8228 ax-addcom 8229 ax-mulcom 8230 ax-addass 8231 ax-mulass 8232 ax-distr 8233 ax-i2m1 8234 ax-0lt1 8235 ax-1rid 8236 ax-0id 8237 ax-rnegex 8238 ax-precex 8239 ax-cnre 8240 ax-pre-ltirr 8241 ax-pre-ltwlin 8242 ax-pre-lttrn 8243 ax-pre-apti 8244 ax-pre-ltadd 8245 ax-pre-mulgt0 8246 ax-pre-mulext 8247

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 3045 df-csb 3141 df-dif 3215 df-un 3217 df-in 3219 df-ss 3226 df-nul 3511 df-if 3623 df-pw 3673 df-sn 3697 df-pr 3698 df-op 3700 df-uni 3917 df-int 3952 df-iun 3995 df-br 4112 df-opab 4174 df-mpt 4175 df-tr 4211 df-id 4416 df-po 4419 df-iso 4420 df-iord 4489 df-on 4491 df-ilim 4492 df-suc 4494 df-iom 4715 df-xp 4757 df-rel 4758 df-cnv 4759 df-co 4760 df-dm 4761 df-rn 4762 df-res 4763 df-ima 4764 df-iota 5314 df-fun 5356 df-fn 5357 df-f 5358 df-f1 5359 df-fo 5360 df-f1o 5361 df-fv 5362 df-riota 6005 df-ov 6055 df-oprab 6056 df-mpo 6057 df-1st 6336 df-2nd 6337 df-recs 6538 df-frec 6624 df-pnf 8312 df-mnf 8313 df-xr 8314 df-ltxr 8315 df-le 8316 df-sub 8448 df-neg 8449 df-reap 8851 df-ap 8858 df-div 8949 df-inn 9240 df-2 9298 df-3 9299 df-4 9300 df-n0 9499 df-z 9580 df-uz 9857 df-rp 9990 df-seqfrec 10814 df-exp 10905

This theorem is referenced by: resqrexlemdec 11700 resqrexlemcalc2 11704 resqrexlemnmsq 11706 resqrexlemga 11712

W3C validator