resqrexlemover - Intuitionistic Logic Explorer

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

Theorem resqrexlemover 11321

Description: Lemma for resqrex 11337. 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 5576	. . . . . 6
2	1	oveq1d 5959	. . . . 5
3	2	breq2d 4056	. . . 4
4	3	imbi2d 230	. . 3
5		fveq2 5576	. . . . . 6
6	5	oveq1d 5959	. . . . 5
7	6	breq2d 4056	. . . 4
8	7	imbi2d 230	. . 3
9		fveq2 5576	. . . . . 6
10	9	oveq1d 5959	. . . . 5
11	10	breq2d 4056	. . . 4
12	11	imbi2d 230	. . 3
13		fveq2 5576	. . . . . 6
14	13	oveq1d 5959	. . . . 5
15	14	breq2d 4056	. . . 4
16	15	imbi2d 230	. . 3
17		resqrexlemex.a	. . . . 5
18	17	resqcld 10844	. . . . . 6
19		2re 9106	. . . . . . . 8
20	19	a1i 9	. . . . . . 7
21	20, 17	remulcld 8103	. . . . . 6
22	18, 21	readdcld 8102	. . . . 5
23		1red 8087	. . . . . 6
24	22, 23	readdcld 8102	. . . . 5
25	17	recnd 8101	. . . . . . . 8
26	25	mulid2d 8091	. . . . . . 7
27		resqrexlemex.agt0	. . . . . . . 8
28		1le2 9245	. . . . . . . . 9
29		lemul1a 8931	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
30	28, 29	mpan2 425	. . . . . . . 8 $/\$ $/\$ $/\$
31	23, 20, 17, 27, 30	syl112anc 1254	. . . . . . 7
32	26, 31	eqbrtrrd 4068	. . . . . 6
33	17	sqge0d 10845	. . . . . . 7
34	21, 18	addge02d 8607	. . . . . . 7
35	33, 34	mpbid 147	. . . . . 6
36	17, 21, 22, 32, 35	letrd 8196	. . . . 5
37	22	ltp1d 9003	. . . . 5
38	17, 22, 24, 36, 37	lelttrd 8197	. . . 4
39		resqrexlemex.seq	. . . . . . . 8
40	39, 17, 27	resqrexlemf1 11319	. . . . . . 7
41		1cnd 8088	. . . . . . . 8
42	41, 25	addcomd 8223	. . . . . . 7
43	40, 42	eqtrd 2238	. . . . . 6
44	43	oveq1d 5959	. . . . 5
45		binom21 10797	. . . . . 6
46	25, 45	syl 14	. . . . 5
47	44, 46	eqtrd 2238	. . . 4
48	38, 47	breqtrrd 4072	. . 3
49	39, 17, 27	resqrexlemf 11318	. . . . . . . . . . . . . 14
50	49	ffvelcdmda 5715	. . . . . . . . . . . . 13 $/\$
51	50	rpred 9818	. . . . . . . . . . . 12 $/\$
52	17	adantr 276	. . . . . . . . . . . . 13 $/\$
53	52, 50	rerpdivcld 9850	. . . . . . . . . . . 12 $/\$
54	51, 53	resubcld 8453	. . . . . . . . . . 11 $/\$
55	54	adantr 276	. . . . . . . . . 10 $/\$ $/\$
56	55	resqcld 10844	. . . . . . . . 9 $/\$ $/\$
57		4re 9113	. . . . . . . . . 10
58	57	a1i 9	. . . . . . . . 9 $/\$ $/\$
59	51	resqcld 10844	. . . . . . . . . . . . . . 15 $/\$
60	59, 52	resubcld 8453	. . . . . . . . . . . . . 14 $/\$
61	60	adantr 276	. . . . . . . . . . . . 13 $/\$ $/\$
62	51	adantr 276	. . . . . . . . . . . . 13 $/\$ $/\$
63	52, 59	posdifd 8605	. . . . . . . . . . . . . 14 $/\$
64	63	biimpa 296	. . . . . . . . . . . . 13 $/\$ $/\$
65	50	rpgt0d 9821	. . . . . . . . . . . . . 14 $/\$
66	65	adantr 276	. . . . . . . . . . . . 13 $/\$ $/\$
67	61, 62, 64, 66	divgt0d 9008	. . . . . . . . . . . 12 $/\$ $/\$
68	51	recnd 8101	. . . . . . . . . . . . . . . 16 $/\$
69	68	sqcld 10816	. . . . . . . . . . . . . . 15 $/\$
70	69	adantr 276	. . . . . . . . . . . . . 14 $/\$ $/\$
71	25	adantr 276	. . . . . . . . . . . . . . 15 $/\$
72	71	adantr 276	. . . . . . . . . . . . . 14 $/\$ $/\$
73	68	adantr 276	. . . . . . . . . . . . . 14 $/\$ $/\$
74	50	rpap0d 9824	. . . . . . . . . . . . . . 15 $/\$ #
75	74	adantr 276	. . . . . . . . . . . . . 14 $/\$ $/\$ #
76	70, 72, 73, 75	divsubdirapd 8903	. . . . . . . . . . . . 13 $/\$ $/\$
77	73	sqvald 10815	. . . . . . . . . . . . . . . 16 $/\$ $/\$
78	77	oveq1d 5959	. . . . . . . . . . . . . . 15 $/\$ $/\$
79	73, 73, 75	divcanap3d 8868	. . . . . . . . . . . . . . 15 $/\$ $/\$
80	78, 79	eqtrd 2238	. . . . . . . . . . . . . 14 $/\$ $/\$
81	80	oveq1d 5959	. . . . . . . . . . . . 13 $/\$ $/\$
82	76, 81	eqtrd 2238	. . . . . . . . . . . 12 $/\$ $/\$
83	67, 82	breqtrd 4070	. . . . . . . . . . 11 $/\$ $/\$
84	55, 83	gt0ap0d 8702	. . . . . . . . . 10 $/\$ $/\$ #
85	55, 84	sqgt0apd 10846	. . . . . . . . 9 $/\$ $/\$
86		4pos 9133	. . . . . . . . . 10
87	86	a1i 9	. . . . . . . . 9 $/\$ $/\$
88	56, 58, 85, 87	divgt0d 9008	. . . . . . . 8 $/\$ $/\$
89	57, 86	gt0ap0ii 8701	. . . . . . . . . . 11 #
90	89	a1i 9	. . . . . . . . . 10 $/\$ $/\$ #
91	56, 58, 90	redivclapd 8908	. . . . . . . . 9 $/\$ $/\$
92	52	adantr 276	. . . . . . . . 9 $/\$ $/\$
93	91, 92	ltaddpos2d 8603	. . . . . . . 8 $/\$ $/\$
94	88, 93	mpbid 147	. . . . . . 7 $/\$ $/\$
95	39, 17, 27	resqrexlemfp1 11320	. . . . . . . . . . . . . 14 $/\$
96	95	oveq1d 5959	. . . . . . . . . . . . 13 $/\$
97	51, 53	readdcld 8102	. . . . . . . . . . . . . . 15 $/\$
98	97	recnd 8101	. . . . . . . . . . . . . 14 $/\$
99		2cnd 9109	. . . . . . . . . . . . . 14 $/\$
100		2ap0 9129	. . . . . . . . . . . . . . 15 #
101	100	a1i 9	. . . . . . . . . . . . . 14 $/\$ #
102	98, 99, 101	sqdivapd 10831	. . . . . . . . . . . . 13 $/\$
103	96, 102	eqtrd 2238	. . . . . . . . . . . 12 $/\$
104		sq2 10780	. . . . . . . . . . . . 13
105	104	oveq2i 5955	. . . . . . . . . . . 12
106	103, 105	eqtrdi 2254	. . . . . . . . . . 11 $/\$
107	71, 68, 74	divcanap2d 8865	. . . . . . . . . . . . . . . . 17 $/\$
108	107	oveq2d 5960	. . . . . . . . . . . . . . . 16 $/\$
109	108	oveq2d 5960	. . . . . . . . . . . . . . 15 $/\$
110	109	oveq1d 5959	. . . . . . . . . . . . . 14 $/\$
111	110	oveq1d 5959	. . . . . . . . . . . . 13 $/\$
112	53	recnd 8101	. . . . . . . . . . . . . . 15 $/\$
113		binom2sub 10798	. . . . . . . . . . . . . . 15 $/\$
114	68, 112, 113	syl2anc 411	. . . . . . . . . . . . . 14 $/\$
115	114	oveq1d 5959	. . . . . . . . . . . . 13 $/\$
116		binom2 10796	. . . . . . . . . . . . . . . 16 $/\$
117	68, 112, 116	syl2anc 411	. . . . . . . . . . . . . . 15 $/\$
118	108	oveq2d 5960	. . . . . . . . . . . . . . . 16 $/\$
119	118	oveq1d 5959	. . . . . . . . . . . . . . 15 $/\$
120	117, 119	eqtrd 2238	. . . . . . . . . . . . . 14 $/\$
121	99, 71	mulcld 8093	. . . . . . . . . . . . . . . . . 18 $/\$
122	121	negcld 8370	. . . . . . . . . . . . . . . . 17 $/\$
123		4cn 9114	. . . . . . . . . . . . . . . . . . 19
124	123	a1i 9	. . . . . . . . . . . . . . . . . 18 $/\$
125	124, 71	mulcld 8093	. . . . . . . . . . . . . . . . 17 $/\$
126	69, 122, 125	addassd 8095	. . . . . . . . . . . . . . . 16 $/\$
127	69, 121	negsubd 8389	. . . . . . . . . . . . . . . . 17 $/\$
128	127	oveq1d 5959	. . . . . . . . . . . . . . . 16 $/\$
129		2cn 9107	. . . . . . . . . . . . . . . . . . . . . 22
130	129	negcli 8340	. . . . . . . . . . . . . . . . . . . . 21
131	130	a1i 9	. . . . . . . . . . . . . . . . . . . 20 $/\$
132	131, 124, 71	adddird 8098	. . . . . . . . . . . . . . . . . . 19 $/\$
133	99, 71	mulneg1d 8483	. . . . . . . . . . . . . . . . . . . 20 $/\$
134	133	oveq1d 5959	. . . . . . . . . . . . . . . . . . 19 $/\$
135	132, 134	eqtrd 2238	. . . . . . . . . . . . . . . . . 18 $/\$
136	130, 129, 129	addassi 8080	. . . . . . . . . . . . . . . . . . . 20
137	129	subidi 8343	. . . . . . . . . . . . . . . . . . . . . . . 24
138	137	negeqi 8266	. . . . . . . . . . . . . . . . . . . . . . 23
139	129, 129	negsubdii 8357	. . . . . . . . . . . . . . . . . . . . . . 23
140		neg0 8318	. . . . . . . . . . . . . . . . . . . . . . 23
141	138, 139, 140	3eqtr3i 2234	. . . . . . . . . . . . . . . . . . . . . 22
142	141	oveq1i 5954	. . . . . . . . . . . . . . . . . . . . 21
143	129	addlidi 8215	. . . . . . . . . . . . . . . . . . . . 21
144	142, 143	eqtri 2226	. . . . . . . . . . . . . . . . . . . 20
145		2p2e4 9163	. . . . . . . . . . . . . . . . . . . . 21
146	145	oveq2i 5955	. . . . . . . . . . . . . . . . . . . 20
147	136, 144, 146	3eqtr3ri 2235	. . . . . . . . . . . . . . . . . . 19
148	147	oveq1i 5954	. . . . . . . . . . . . . . . . . 18
149	135, 148	eqtr3di 2253	. . . . . . . . . . . . . . . . 17 $/\$
150	149	oveq2d 5960	. . . . . . . . . . . . . . . 16 $/\$
151	126, 128, 150	3eqtr3rd 2247	. . . . . . . . . . . . . . 15 $/\$
152	151	oveq1d 5959	. . . . . . . . . . . . . 14 $/\$
153	19	a1i 9	. . . . . . . . . . . . . . . . 17 $/\$
154	153, 52	remulcld 8103	. . . . . . . . . . . . . . . 16 $/\$
155	59, 154	resubcld 8453	. . . . . . . . . . . . . . 15 $/\$
156	57	a1i 9	. . . . . . . . . . . . . . . 16 $/\$
157	156, 52	remulcld 8103	. . . . . . . . . . . . . . 15 $/\$
158	53	resqcld 10844	. . . . . . . . . . . . . . 15 $/\$
159		recn 8058	. . . . . . . . . . . . . . . . 17
160		recn 8058	. . . . . . . . . . . . . . . . 17
161		addcom 8209	. . . . . . . . . . . . . . . . 17 $/\$
162	159, 160, 161	syl2an 289	. . . . . . . . . . . . . . . 16 $/\$
163	162	adantl 277	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
164		recn 8058	. . . . . . . . . . . . . . . . 17
165		addass 8055	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
166	159, 160, 164, 165	syl3an 1292	. . . . . . . . . . . . . . . 16 $/\$ $/\$
167	166	adantl 277	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
168	155, 157, 158, 163, 167	caov32d 6127	. . . . . . . . . . . . . 14 $/\$
169	120, 152, 168	3eqtrd 2242	. . . . . . . . . . . . 13 $/\$
170	111, 115, 169	3eqtr4rd 2249	. . . . . . . . . . . 12 $/\$
171	170	oveq1d 5959	. . . . . . . . . . 11 $/\$
172	106, 171	eqtrd 2238	. . . . . . . . . 10 $/\$
173	68, 112	subcld 8383	. . . . . . . . . . . 12 $/\$
174	173	sqcld 10816	. . . . . . . . . . 11 $/\$
175	89	a1i 9	. . . . . . . . . . 11 $/\$ #
176	174, 125, 124, 175	divdirapd 8902	. . . . . . . . . 10 $/\$
177	71, 124, 175	divcanap3d 8868	. . . . . . . . . . 11 $/\$
178	177	oveq2d 5960	. . . . . . . . . 10 $/\$
179	172, 176, 178	3eqtrd 2242	. . . . . . . . 9 $/\$
180	179	breq2d 4056	. . . . . . . 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 9052	. 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 4044

cxp 4673

cfv 5271 (class class class)co 5944

cmpo 5946

cc 7923

cr 7924

cc0 7925

c1 7926

caddc 7928

cmul 7930

clt 8107

cle 8108

cmin 8243

cneg 8244 # cap 8654

cdiv 8745

cn 9036

c2 9087

c4 9089

crp 9775

cseq 10592

cexp 10683

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 4159 ax-sep 4162 ax-nul 4170 ax-pow 4218 ax-pr 4253 ax-un 4480 ax-setind 4585 ax-iinf 4636 ax-cnex 8016 ax-resscn 8017 ax-1cn 8018 ax-1re 8019 ax-icn 8020 ax-addcl 8021 ax-addrcl 8022 ax-mulcl 8023 ax-mulrcl 8024 ax-addcom 8025 ax-mulcom 8026 ax-addass 8027 ax-mulass 8028 ax-distr 8029 ax-i2m1 8030 ax-0lt1 8031 ax-1rid 8032 ax-0id 8033 ax-rnegex 8034 ax-precex 8035 ax-cnre 8036 ax-pre-ltirr 8037 ax-pre-ltwlin 8038 ax-pre-lttrn 8039 ax-pre-apti 8040 ax-pre-ltadd 8041 ax-pre-mulgt0 8042 ax-pre-mulext 8043

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 4045 df-opab 4106 df-mpt 4107 df-tr 4143 df-id 4340 df-po 4343 df-iso 4344 df-iord 4413 df-on 4415 df-ilim 4416 df-suc 4418 df-iom 4639 df-xp 4681 df-rel 4682 df-cnv 4683 df-co 4684 df-dm 4685 df-rn 4686 df-res 4687 df-ima 4688 df-iota 5232 df-fun 5273 df-fn 5274 df-f 5275 df-f1 5276 df-fo 5277 df-f1o 5278 df-fv 5279 df-riota 5899 df-ov 5947 df-oprab 5948 df-mpo 5949 df-1st 6226 df-2nd 6227 df-recs 6391 df-frec 6477 df-pnf 8109 df-mnf 8110 df-xr 8111 df-ltxr 8112 df-le 8113 df-sub 8245 df-neg 8246 df-reap 8648 df-ap 8655 df-div 8746 df-inn 9037 df-2 9095 df-3 9096 df-4 9097 df-n0 9296 df-z 9373 df-uz 9649 df-rp 9776 df-seqfrec 10593 df-exp 10684

This theorem is referenced by: resqrexlemdec 11322 resqrexlemcalc2 11326 resqrexlemnmsq 11328 resqrexlemga 11334

W3C validator