resqrexlemover - Intuitionistic Logic Explorer

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

Theorem resqrexlemover 11354

Description: Lemma for resqrex 11370. 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 5578	. . . . . 6
2	1	oveq1d 5961	. . . . 5
3	2	breq2d 4057	. . . 4
4	3	imbi2d 230	. . 3
5		fveq2 5578	. . . . . 6
6	5	oveq1d 5961	. . . . 5
7	6	breq2d 4057	. . . 4
8	7	imbi2d 230	. . 3
9		fveq2 5578	. . . . . 6
10	9	oveq1d 5961	. . . . 5
11	10	breq2d 4057	. . . 4
12	11	imbi2d 230	. . 3
13		fveq2 5578	. . . . . 6
14	13	oveq1d 5961	. . . . 5
15	14	breq2d 4057	. . . 4
16	15	imbi2d 230	. . 3
17		resqrexlemex.a	. . . . 5
18	17	resqcld 10846	. . . . . 6
19		2re 9108	. . . . . . . 8
20	19	a1i 9	. . . . . . 7
21	20, 17	remulcld 8105	. . . . . 6
22	18, 21	readdcld 8104	. . . . 5
23		1red 8089	. . . . . 6
24	22, 23	readdcld 8104	. . . . 5
25	17	recnd 8103	. . . . . . . 8
26	25	mulid2d 8093	. . . . . . 7
27		resqrexlemex.agt0	. . . . . . . 8
28		1le2 9247	. . . . . . . . 9
29		lemul1a 8933	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
30	28, 29	mpan2 425	. . . . . . . 8 $/\$ $/\$ $/\$
31	23, 20, 17, 27, 30	syl112anc 1254	. . . . . . 7
32	26, 31	eqbrtrrd 4069	. . . . . 6
33	17	sqge0d 10847	. . . . . . 7
34	21, 18	addge02d 8609	. . . . . . 7
35	33, 34	mpbid 147	. . . . . 6
36	17, 21, 22, 32, 35	letrd 8198	. . . . 5
37	22	ltp1d 9005	. . . . 5
38	17, 22, 24, 36, 37	lelttrd 8199	. . . 4
39		resqrexlemex.seq	. . . . . . . 8
40	39, 17, 27	resqrexlemf1 11352	. . . . . . 7
41		1cnd 8090	. . . . . . . 8
42	41, 25	addcomd 8225	. . . . . . 7
43	40, 42	eqtrd 2238	. . . . . 6
44	43	oveq1d 5961	. . . . 5
45		binom21 10799	. . . . . 6
46	25, 45	syl 14	. . . . 5
47	44, 46	eqtrd 2238	. . . 4
48	38, 47	breqtrrd 4073	. . 3
49	39, 17, 27	resqrexlemf 11351	. . . . . . . . . . . . . 14
50	49	ffvelcdmda 5717	. . . . . . . . . . . . 13 $/\$
51	50	rpred 9820	. . . . . . . . . . . 12 $/\$
52	17	adantr 276	. . . . . . . . . . . . 13 $/\$
53	52, 50	rerpdivcld 9852	. . . . . . . . . . . 12 $/\$
54	51, 53	resubcld 8455	. . . . . . . . . . 11 $/\$
55	54	adantr 276	. . . . . . . . . 10 $/\$ $/\$
56	55	resqcld 10846	. . . . . . . . 9 $/\$ $/\$
57		4re 9115	. . . . . . . . . 10
58	57	a1i 9	. . . . . . . . 9 $/\$ $/\$
59	51	resqcld 10846	. . . . . . . . . . . . . . 15 $/\$
60	59, 52	resubcld 8455	. . . . . . . . . . . . . 14 $/\$
61	60	adantr 276	. . . . . . . . . . . . 13 $/\$ $/\$
62	51	adantr 276	. . . . . . . . . . . . 13 $/\$ $/\$
63	52, 59	posdifd 8607	. . . . . . . . . . . . . 14 $/\$
64	63	biimpa 296	. . . . . . . . . . . . 13 $/\$ $/\$
65	50	rpgt0d 9823	. . . . . . . . . . . . . 14 $/\$
66	65	adantr 276	. . . . . . . . . . . . 13 $/\$ $/\$
67	61, 62, 64, 66	divgt0d 9010	. . . . . . . . . . . 12 $/\$ $/\$
68	51	recnd 8103	. . . . . . . . . . . . . . . 16 $/\$
69	68	sqcld 10818	. . . . . . . . . . . . . . 15 $/\$
70	69	adantr 276	. . . . . . . . . . . . . 14 $/\$ $/\$
71	25	adantr 276	. . . . . . . . . . . . . . 15 $/\$
72	71	adantr 276	. . . . . . . . . . . . . 14 $/\$ $/\$
73	68	adantr 276	. . . . . . . . . . . . . 14 $/\$ $/\$
74	50	rpap0d 9826	. . . . . . . . . . . . . . 15 $/\$ #
75	74	adantr 276	. . . . . . . . . . . . . 14 $/\$ $/\$ #
76	70, 72, 73, 75	divsubdirapd 8905	. . . . . . . . . . . . 13 $/\$ $/\$
77	73	sqvald 10817	. . . . . . . . . . . . . . . 16 $/\$ $/\$
78	77	oveq1d 5961	. . . . . . . . . . . . . . 15 $/\$ $/\$
79	73, 73, 75	divcanap3d 8870	. . . . . . . . . . . . . . 15 $/\$ $/\$
80	78, 79	eqtrd 2238	. . . . . . . . . . . . . 14 $/\$ $/\$
81	80	oveq1d 5961	. . . . . . . . . . . . 13 $/\$ $/\$
82	76, 81	eqtrd 2238	. . . . . . . . . . . 12 $/\$ $/\$
83	67, 82	breqtrd 4071	. . . . . . . . . . 11 $/\$ $/\$
84	55, 83	gt0ap0d 8704	. . . . . . . . . 10 $/\$ $/\$ #
85	55, 84	sqgt0apd 10848	. . . . . . . . 9 $/\$ $/\$
86		4pos 9135	. . . . . . . . . 10
87	86	a1i 9	. . . . . . . . 9 $/\$ $/\$
88	56, 58, 85, 87	divgt0d 9010	. . . . . . . 8 $/\$ $/\$
89	57, 86	gt0ap0ii 8703	. . . . . . . . . . 11 #
90	89	a1i 9	. . . . . . . . . 10 $/\$ $/\$ #
91	56, 58, 90	redivclapd 8910	. . . . . . . . 9 $/\$ $/\$
92	52	adantr 276	. . . . . . . . 9 $/\$ $/\$
93	91, 92	ltaddpos2d 8605	. . . . . . . 8 $/\$ $/\$
94	88, 93	mpbid 147	. . . . . . 7 $/\$ $/\$
95	39, 17, 27	resqrexlemfp1 11353	. . . . . . . . . . . . . 14 $/\$
96	95	oveq1d 5961	. . . . . . . . . . . . 13 $/\$
97	51, 53	readdcld 8104	. . . . . . . . . . . . . . 15 $/\$
98	97	recnd 8103	. . . . . . . . . . . . . 14 $/\$
99		2cnd 9111	. . . . . . . . . . . . . 14 $/\$
100		2ap0 9131	. . . . . . . . . . . . . . 15 #
101	100	a1i 9	. . . . . . . . . . . . . 14 $/\$ #
102	98, 99, 101	sqdivapd 10833	. . . . . . . . . . . . 13 $/\$
103	96, 102	eqtrd 2238	. . . . . . . . . . . 12 $/\$
104		sq2 10782	. . . . . . . . . . . . 13
105	104	oveq2i 5957	. . . . . . . . . . . 12
106	103, 105	eqtrdi 2254	. . . . . . . . . . 11 $/\$
107	71, 68, 74	divcanap2d 8867	. . . . . . . . . . . . . . . . 17 $/\$
108	107	oveq2d 5962	. . . . . . . . . . . . . . . 16 $/\$
109	108	oveq2d 5962	. . . . . . . . . . . . . . 15 $/\$
110	109	oveq1d 5961	. . . . . . . . . . . . . 14 $/\$
111	110	oveq1d 5961	. . . . . . . . . . . . 13 $/\$
112	53	recnd 8103	. . . . . . . . . . . . . . 15 $/\$
113		binom2sub 10800	. . . . . . . . . . . . . . 15 $/\$
114	68, 112, 113	syl2anc 411	. . . . . . . . . . . . . 14 $/\$
115	114	oveq1d 5961	. . . . . . . . . . . . 13 $/\$
116		binom2 10798	. . . . . . . . . . . . . . . 16 $/\$
117	68, 112, 116	syl2anc 411	. . . . . . . . . . . . . . 15 $/\$
118	108	oveq2d 5962	. . . . . . . . . . . . . . . 16 $/\$
119	118	oveq1d 5961	. . . . . . . . . . . . . . 15 $/\$
120	117, 119	eqtrd 2238	. . . . . . . . . . . . . 14 $/\$
121	99, 71	mulcld 8095	. . . . . . . . . . . . . . . . . 18 $/\$
122	121	negcld 8372	. . . . . . . . . . . . . . . . 17 $/\$
123		4cn 9116	. . . . . . . . . . . . . . . . . . 19
124	123	a1i 9	. . . . . . . . . . . . . . . . . 18 $/\$
125	124, 71	mulcld 8095	. . . . . . . . . . . . . . . . 17 $/\$
126	69, 122, 125	addassd 8097	. . . . . . . . . . . . . . . 16 $/\$
127	69, 121	negsubd 8391	. . . . . . . . . . . . . . . . 17 $/\$
128	127	oveq1d 5961	. . . . . . . . . . . . . . . 16 $/\$
129		2cn 9109	. . . . . . . . . . . . . . . . . . . . . 22
130	129	negcli 8342	. . . . . . . . . . . . . . . . . . . . 21
131	130	a1i 9	. . . . . . . . . . . . . . . . . . . 20 $/\$
132	131, 124, 71	adddird 8100	. . . . . . . . . . . . . . . . . . 19 $/\$
133	99, 71	mulneg1d 8485	. . . . . . . . . . . . . . . . . . . 20 $/\$
134	133	oveq1d 5961	. . . . . . . . . . . . . . . . . . 19 $/\$
135	132, 134	eqtrd 2238	. . . . . . . . . . . . . . . . . 18 $/\$
136	130, 129, 129	addassi 8082	. . . . . . . . . . . . . . . . . . . 20
137	129	subidi 8345	. . . . . . . . . . . . . . . . . . . . . . . 24
138	137	negeqi 8268	. . . . . . . . . . . . . . . . . . . . . . 23
139	129, 129	negsubdii 8359	. . . . . . . . . . . . . . . . . . . . . . 23
140		neg0 8320	. . . . . . . . . . . . . . . . . . . . . . 23
141	138, 139, 140	3eqtr3i 2234	. . . . . . . . . . . . . . . . . . . . . 22
142	141	oveq1i 5956	. . . . . . . . . . . . . . . . . . . . 21
143	129	addlidi 8217	. . . . . . . . . . . . . . . . . . . . 21
144	142, 143	eqtri 2226	. . . . . . . . . . . . . . . . . . . 20
145		2p2e4 9165	. . . . . . . . . . . . . . . . . . . . 21
146	145	oveq2i 5957	. . . . . . . . . . . . . . . . . . . 20
147	136, 144, 146	3eqtr3ri 2235	. . . . . . . . . . . . . . . . . . 19
148	147	oveq1i 5956	. . . . . . . . . . . . . . . . . 18
149	135, 148	eqtr3di 2253	. . . . . . . . . . . . . . . . 17 $/\$
150	149	oveq2d 5962	. . . . . . . . . . . . . . . 16 $/\$
151	126, 128, 150	3eqtr3rd 2247	. . . . . . . . . . . . . . 15 $/\$
152	151	oveq1d 5961	. . . . . . . . . . . . . 14 $/\$
153	19	a1i 9	. . . . . . . . . . . . . . . . 17 $/\$
154	153, 52	remulcld 8105	. . . . . . . . . . . . . . . 16 $/\$
155	59, 154	resubcld 8455	. . . . . . . . . . . . . . 15 $/\$
156	57	a1i 9	. . . . . . . . . . . . . . . 16 $/\$
157	156, 52	remulcld 8105	. . . . . . . . . . . . . . 15 $/\$
158	53	resqcld 10846	. . . . . . . . . . . . . . 15 $/\$
159		recn 8060	. . . . . . . . . . . . . . . . 17
160		recn 8060	. . . . . . . . . . . . . . . . 17
161		addcom 8211	. . . . . . . . . . . . . . . . 17 $/\$
162	159, 160, 161	syl2an 289	. . . . . . . . . . . . . . . 16 $/\$
163	162	adantl 277	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
164		recn 8060	. . . . . . . . . . . . . . . . 17
165		addass 8057	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
166	159, 160, 164, 165	syl3an 1292	. . . . . . . . . . . . . . . 16 $/\$ $/\$
167	166	adantl 277	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
168	155, 157, 158, 163, 167	caov32d 6129	. . . . . . . . . . . . . 14 $/\$
169	120, 152, 168	3eqtrd 2242	. . . . . . . . . . . . 13 $/\$
170	111, 115, 169	3eqtr4rd 2249	. . . . . . . . . . . 12 $/\$
171	170	oveq1d 5961	. . . . . . . . . . 11 $/\$
172	106, 171	eqtrd 2238	. . . . . . . . . 10 $/\$
173	68, 112	subcld 8385	. . . . . . . . . . . 12 $/\$
174	173	sqcld 10818	. . . . . . . . . . 11 $/\$
175	89	a1i 9	. . . . . . . . . . 11 $/\$ #
176	174, 125, 124, 175	divdirapd 8904	. . . . . . . . . 10 $/\$
177	71, 124, 175	divcanap3d 8870	. . . . . . . . . . 11 $/\$
178	177	oveq2d 5962	. . . . . . . . . 10 $/\$
179	172, 176, 178	3eqtrd 2242	. . . . . . . . 9 $/\$
180	179	breq2d 4057	. . . . . . . 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 9054	. 2
187	186	impcom 125	1 $/\$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wb 105 $/\$ w3a 981

wceq 1373

wcel 2176

csn 3633 class class class wbr 4045

cxp 4674

cfv 5272 (class class class)co 5946

cmpo 5948

cc 7925

cr 7926

cc0 7927

c1 7928

caddc 7930

cmul 7932

clt 8109

cle 8110

cmin 8245

cneg 8246 # cap 8656

cdiv 8747

cn 9038

c2 9089

c4 9091

crp 9777

cseq 10594

cexp 10685

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 615 ax-in2 616 ax-io 711 ax-5 1470 ax-7 1471 ax-gen 1472 ax-ie1 1516 ax-ie2 1517 ax-8 1527 ax-10 1528 ax-11 1529 ax-i12 1530 ax-bndl 1532 ax-4 1533 ax-17 1549 ax-i9 1553 ax-ial 1557 ax-i5r 1558 ax-13 2178 ax-14 2179 ax-ext 2187 ax-coll 4160 ax-sep 4163 ax-nul 4171 ax-pow 4219 ax-pr 4254 ax-un 4481 ax-setind 4586 ax-iinf 4637 ax-cnex 8018 ax-resscn 8019 ax-1cn 8020 ax-1re 8021 ax-icn 8022 ax-addcl 8023 ax-addrcl 8024 ax-mulcl 8025 ax-mulrcl 8026 ax-addcom 8027 ax-mulcom 8028 ax-addass 8029 ax-mulass 8030 ax-distr 8031 ax-i2m1 8032 ax-0lt1 8033 ax-1rid 8034 ax-0id 8035 ax-rnegex 8036 ax-precex 8037 ax-cnre 8038 ax-pre-ltirr 8039 ax-pre-ltwlin 8040 ax-pre-lttrn 8041 ax-pre-apti 8042 ax-pre-ltadd 8043 ax-pre-mulgt0 8044 ax-pre-mulext 8045

This theorem depends on definitions: df-bi 117 df-dc 837 df-3or 982 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1484 df-sb 1786 df-eu 2057 df-mo 2058 df-clab 2192 df-cleq 2198 df-clel 2201 df-nfc 2337 df-ne 2377 df-nel 2472 df-ral 2489 df-rex 2490 df-reu 2491 df-rmo 2492 df-rab 2493 df-v 2774 df-sbc 2999 df-csb 3094 df-dif 3168 df-un 3170 df-in 3172 df-ss 3179 df-nul 3461 df-if 3572 df-pw 3618 df-sn 3639 df-pr 3640 df-op 3642 df-uni 3851 df-int 3886 df-iun 3929 df-br 4046 df-opab 4107 df-mpt 4108 df-tr 4144 df-id 4341 df-po 4344 df-iso 4345 df-iord 4414 df-on 4416 df-ilim 4417 df-suc 4419 df-iom 4640 df-xp 4682 df-rel 4683 df-cnv 4684 df-co 4685 df-dm 4686 df-rn 4687 df-res 4688 df-ima 4689 df-iota 5233 df-fun 5274 df-fn 5275 df-f 5276 df-f1 5277 df-fo 5278 df-f1o 5279 df-fv 5280 df-riota 5901 df-ov 5949 df-oprab 5950 df-mpo 5951 df-1st 6228 df-2nd 6229 df-recs 6393 df-frec 6479 df-pnf 8111 df-mnf 8112 df-xr 8113 df-ltxr 8114 df-le 8115 df-sub 8247 df-neg 8248 df-reap 8650 df-ap 8657 df-div 8748 df-inn 9039 df-2 9097 df-3 9098 df-4 9099 df-n0 9298 df-z 9375 df-uz 9651 df-rp 9778 df-seqfrec 10595 df-exp 10686

This theorem is referenced by: resqrexlemdec 11355 resqrexlemcalc2 11359 resqrexlemnmsq 11361 resqrexlemga 11367

W3C validator