resqrexlemover - Intuitionistic Logic Explorer

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

Theorem resqrexlemover 11036

Description: Lemma for resqrex 11052. 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 5529	. . . . . 6
2	1	oveq1d 5905	. . . . 5
3	2	breq2d 4029	. . . 4
4	3	imbi2d 230	. . 3
5		fveq2 5529	. . . . . 6
6	5	oveq1d 5905	. . . . 5
7	6	breq2d 4029	. . . 4
8	7	imbi2d 230	. . 3
9		fveq2 5529	. . . . . 6
10	9	oveq1d 5905	. . . . 5
11	10	breq2d 4029	. . . 4
12	11	imbi2d 230	. . 3
13		fveq2 5529	. . . . . 6
14	13	oveq1d 5905	. . . . 5
15	14	breq2d 4029	. . . 4
16	15	imbi2d 230	. . 3
17		resqrexlemex.a	. . . . 5
18	17	resqcld 10697	. . . . . 6
19		2re 9006	. . . . . . . 8
20	19	a1i 9	. . . . . . 7
21	20, 17	remulcld 8005	. . . . . 6
22	18, 21	readdcld 8004	. . . . 5
23		1red 7989	. . . . . 6
24	22, 23	readdcld 8004	. . . . 5
25	17	recnd 8003	. . . . . . . 8
26	25	mulid2d 7993	. . . . . . 7
27		resqrexlemex.agt0	. . . . . . . 8
28		1le2 9144	. . . . . . . . 9
29		lemul1a 8832	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
30	28, 29	mpan2 425	. . . . . . . 8 $/\$ $/\$ $/\$
31	23, 20, 17, 27, 30	syl112anc 1252	. . . . . . 7
32	26, 31	eqbrtrrd 4041	. . . . . 6
33	17	sqge0d 10698	. . . . . . 7
34	21, 18	addge02d 8508	. . . . . . 7
35	33, 34	mpbid 147	. . . . . 6
36	17, 21, 22, 32, 35	letrd 8098	. . . . 5
37	22	ltp1d 8904	. . . . 5
38	17, 22, 24, 36, 37	lelttrd 8099	. . . 4
39		resqrexlemex.seq	. . . . . . . 8
40	39, 17, 27	resqrexlemf1 11034	. . . . . . 7
41		1cnd 7990	. . . . . . . 8
42	41, 25	addcomd 8125	. . . . . . 7
43	40, 42	eqtrd 2221	. . . . . 6
44	43	oveq1d 5905	. . . . 5
45		binom21 10650	. . . . . 6
46	25, 45	syl 14	. . . . 5
47	44, 46	eqtrd 2221	. . . 4
48	38, 47	breqtrrd 4045	. . 3
49	39, 17, 27	resqrexlemf 11033	. . . . . . . . . . . . . 14
50	49	ffvelcdmda 5666	. . . . . . . . . . . . 13 $/\$
51	50	rpred 9713	. . . . . . . . . . . 12 $/\$
52	17	adantr 276	. . . . . . . . . . . . 13 $/\$
53	52, 50	rerpdivcld 9745	. . . . . . . . . . . 12 $/\$
54	51, 53	resubcld 8355	. . . . . . . . . . 11 $/\$
55	54	adantr 276	. . . . . . . . . 10 $/\$ $/\$
56	55	resqcld 10697	. . . . . . . . 9 $/\$ $/\$
57		4re 9013	. . . . . . . . . 10
58	57	a1i 9	. . . . . . . . 9 $/\$ $/\$
59	51	resqcld 10697	. . . . . . . . . . . . . . 15 $/\$
60	59, 52	resubcld 8355	. . . . . . . . . . . . . 14 $/\$
61	60	adantr 276	. . . . . . . . . . . . 13 $/\$ $/\$
62	51	adantr 276	. . . . . . . . . . . . 13 $/\$ $/\$
63	52, 59	posdifd 8506	. . . . . . . . . . . . . 14 $/\$
64	63	biimpa 296	. . . . . . . . . . . . 13 $/\$ $/\$
65	50	rpgt0d 9716	. . . . . . . . . . . . . 14 $/\$
66	65	adantr 276	. . . . . . . . . . . . 13 $/\$ $/\$
67	61, 62, 64, 66	divgt0d 8909	. . . . . . . . . . . 12 $/\$ $/\$
68	51	recnd 8003	. . . . . . . . . . . . . . . 16 $/\$
69	68	sqcld 10669	. . . . . . . . . . . . . . 15 $/\$
70	69	adantr 276	. . . . . . . . . . . . . 14 $/\$ $/\$
71	25	adantr 276	. . . . . . . . . . . . . . 15 $/\$
72	71	adantr 276	. . . . . . . . . . . . . 14 $/\$ $/\$
73	68	adantr 276	. . . . . . . . . . . . . 14 $/\$ $/\$
74	50	rpap0d 9719	. . . . . . . . . . . . . . 15 $/\$ #
75	74	adantr 276	. . . . . . . . . . . . . 14 $/\$ $/\$ #
76	70, 72, 73, 75	divsubdirapd 8804	. . . . . . . . . . . . 13 $/\$ $/\$
77	73	sqvald 10668	. . . . . . . . . . . . . . . 16 $/\$ $/\$
78	77	oveq1d 5905	. . . . . . . . . . . . . . 15 $/\$ $/\$
79	73, 73, 75	divcanap3d 8769	. . . . . . . . . . . . . . 15 $/\$ $/\$
80	78, 79	eqtrd 2221	. . . . . . . . . . . . . 14 $/\$ $/\$
81	80	oveq1d 5905	. . . . . . . . . . . . 13 $/\$ $/\$
82	76, 81	eqtrd 2221	. . . . . . . . . . . 12 $/\$ $/\$
83	67, 82	breqtrd 4043	. . . . . . . . . . 11 $/\$ $/\$
84	55, 83	gt0ap0d 8603	. . . . . . . . . 10 $/\$ $/\$ #
85	55, 84	sqgt0apd 10699	. . . . . . . . 9 $/\$ $/\$
86		4pos 9033	. . . . . . . . . 10
87	86	a1i 9	. . . . . . . . 9 $/\$ $/\$
88	56, 58, 85, 87	divgt0d 8909	. . . . . . . 8 $/\$ $/\$
89	57, 86	gt0ap0ii 8602	. . . . . . . . . . 11 #
90	89	a1i 9	. . . . . . . . . 10 $/\$ $/\$ #
91	56, 58, 90	redivclapd 8809	. . . . . . . . 9 $/\$ $/\$
92	52	adantr 276	. . . . . . . . 9 $/\$ $/\$
93	91, 92	ltaddpos2d 8504	. . . . . . . 8 $/\$ $/\$
94	88, 93	mpbid 147	. . . . . . 7 $/\$ $/\$
95	39, 17, 27	resqrexlemfp1 11035	. . . . . . . . . . . . . 14 $/\$
96	95	oveq1d 5905	. . . . . . . . . . . . 13 $/\$
97	51, 53	readdcld 8004	. . . . . . . . . . . . . . 15 $/\$
98	97	recnd 8003	. . . . . . . . . . . . . 14 $/\$
99		2cnd 9009	. . . . . . . . . . . . . 14 $/\$
100		2ap0 9029	. . . . . . . . . . . . . . 15 #
101	100	a1i 9	. . . . . . . . . . . . . 14 $/\$ #
102	98, 99, 101	sqdivapd 10684	. . . . . . . . . . . . 13 $/\$
103	96, 102	eqtrd 2221	. . . . . . . . . . . 12 $/\$
104		sq2 10633	. . . . . . . . . . . . 13
105	104	oveq2i 5901	. . . . . . . . . . . 12
106	103, 105	eqtrdi 2237	. . . . . . . . . . 11 $/\$
107	71, 68, 74	divcanap2d 8766	. . . . . . . . . . . . . . . . 17 $/\$
108	107	oveq2d 5906	. . . . . . . . . . . . . . . 16 $/\$
109	108	oveq2d 5906	. . . . . . . . . . . . . . 15 $/\$
110	109	oveq1d 5905	. . . . . . . . . . . . . 14 $/\$
111	110	oveq1d 5905	. . . . . . . . . . . . 13 $/\$
112	53	recnd 8003	. . . . . . . . . . . . . . 15 $/\$
113		binom2sub 10651	. . . . . . . . . . . . . . 15 $/\$
114	68, 112, 113	syl2anc 411	. . . . . . . . . . . . . 14 $/\$
115	114	oveq1d 5905	. . . . . . . . . . . . 13 $/\$
116		binom2 10649	. . . . . . . . . . . . . . . 16 $/\$
117	68, 112, 116	syl2anc 411	. . . . . . . . . . . . . . 15 $/\$
118	108	oveq2d 5906	. . . . . . . . . . . . . . . 16 $/\$
119	118	oveq1d 5905	. . . . . . . . . . . . . . 15 $/\$
120	117, 119	eqtrd 2221	. . . . . . . . . . . . . 14 $/\$
121	99, 71	mulcld 7995	. . . . . . . . . . . . . . . . . 18 $/\$
122	121	negcld 8272	. . . . . . . . . . . . . . . . 17 $/\$
123		4cn 9014	. . . . . . . . . . . . . . . . . . 19
124	123	a1i 9	. . . . . . . . . . . . . . . . . 18 $/\$
125	124, 71	mulcld 7995	. . . . . . . . . . . . . . . . 17 $/\$
126	69, 122, 125	addassd 7997	. . . . . . . . . . . . . . . 16 $/\$
127	69, 121	negsubd 8291	. . . . . . . . . . . . . . . . 17 $/\$
128	127	oveq1d 5905	. . . . . . . . . . . . . . . 16 $/\$
129		2cn 9007	. . . . . . . . . . . . . . . . . . . . . 22
130	129	negcli 8242	. . . . . . . . . . . . . . . . . . . . 21
131	130	a1i 9	. . . . . . . . . . . . . . . . . . . 20 $/\$
132	131, 124, 71	adddird 8000	. . . . . . . . . . . . . . . . . . 19 $/\$
133	99, 71	mulneg1d 8385	. . . . . . . . . . . . . . . . . . . 20 $/\$
134	133	oveq1d 5905	. . . . . . . . . . . . . . . . . . 19 $/\$
135	132, 134	eqtrd 2221	. . . . . . . . . . . . . . . . . 18 $/\$
136	130, 129, 129	addassi 7982	. . . . . . . . . . . . . . . . . . . 20
137	129	subidi 8245	. . . . . . . . . . . . . . . . . . . . . . . 24
138	137	negeqi 8168	. . . . . . . . . . . . . . . . . . . . . . 23
139	129, 129	negsubdii 8259	. . . . . . . . . . . . . . . . . . . . . . 23
140		neg0 8220	. . . . . . . . . . . . . . . . . . . . . . 23
141	138, 139, 140	3eqtr3i 2217	. . . . . . . . . . . . . . . . . . . . . 22
142	141	oveq1i 5900	. . . . . . . . . . . . . . . . . . . . 21
143	129	addid2i 8117	. . . . . . . . . . . . . . . . . . . . 21
144	142, 143	eqtri 2209	. . . . . . . . . . . . . . . . . . . 20
145		2p2e4 9063	. . . . . . . . . . . . . . . . . . . . 21
146	145	oveq2i 5901	. . . . . . . . . . . . . . . . . . . 20
147	136, 144, 146	3eqtr3ri 2218	. . . . . . . . . . . . . . . . . . 19
148	147	oveq1i 5900	. . . . . . . . . . . . . . . . . 18
149	135, 148	eqtr3di 2236	. . . . . . . . . . . . . . . . 17 $/\$
150	149	oveq2d 5906	. . . . . . . . . . . . . . . 16 $/\$
151	126, 128, 150	3eqtr3rd 2230	. . . . . . . . . . . . . . 15 $/\$
152	151	oveq1d 5905	. . . . . . . . . . . . . 14 $/\$
153	19	a1i 9	. . . . . . . . . . . . . . . . 17 $/\$
154	153, 52	remulcld 8005	. . . . . . . . . . . . . . . 16 $/\$
155	59, 154	resubcld 8355	. . . . . . . . . . . . . . 15 $/\$
156	57	a1i 9	. . . . . . . . . . . . . . . 16 $/\$
157	156, 52	remulcld 8005	. . . . . . . . . . . . . . 15 $/\$
158	53	resqcld 10697	. . . . . . . . . . . . . . 15 $/\$
159		recn 7961	. . . . . . . . . . . . . . . . 17
160		recn 7961	. . . . . . . . . . . . . . . . 17
161		addcom 8111	. . . . . . . . . . . . . . . . 17 $/\$
162	159, 160, 161	syl2an 289	. . . . . . . . . . . . . . . 16 $/\$
163	162	adantl 277	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
164		recn 7961	. . . . . . . . . . . . . . . . 17
165		addass 7958	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
166	159, 160, 164, 165	syl3an 1290	. . . . . . . . . . . . . . . 16 $/\$ $/\$
167	166	adantl 277	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
168	155, 157, 158, 163, 167	caov32d 6071	. . . . . . . . . . . . . 14 $/\$
169	120, 152, 168	3eqtrd 2225	. . . . . . . . . . . . 13 $/\$
170	111, 115, 169	3eqtr4rd 2232	. . . . . . . . . . . 12 $/\$
171	170	oveq1d 5905	. . . . . . . . . . 11 $/\$
172	106, 171	eqtrd 2221	. . . . . . . . . 10 $/\$
173	68, 112	subcld 8285	. . . . . . . . . . . 12 $/\$
174	173	sqcld 10669	. . . . . . . . . . 11 $/\$
175	89	a1i 9	. . . . . . . . . . 11 $/\$ #
176	174, 125, 124, 175	divdirapd 8803	. . . . . . . . . 10 $/\$
177	71, 124, 175	divcanap3d 8769	. . . . . . . . . . 11 $/\$
178	177	oveq2d 5906	. . . . . . . . . 10 $/\$
179	172, 176, 178	3eqtrd 2225	. . . . . . . . 9 $/\$
180	179	breq2d 4029	. . . . . . . 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 8952	. 2
187	186	impcom 125	1 $/\$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wb 105 $/\$ w3a 979

wceq 1363

wcel 2159

csn 3606 class class class wbr 4017

cxp 4638

cfv 5230 (class class class)co 5890

cmpo 5892

cc 7826

cr 7827

cc0 7828

c1 7829

caddc 7831

cmul 7833

clt 8009

cle 8010

cmin 8145

cneg 8146 # cap 8555

cdiv 8646

cn 8936

c2 8987

c4 8989

crp 9670

cseq 10462

cexp 10536

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 710 ax-5 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-10 1515 ax-11 1516 ax-i12 1517 ax-bndl 1519 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-13 2161 ax-14 2162 ax-ext 2170 ax-coll 4132 ax-sep 4135 ax-nul 4143 ax-pow 4188 ax-pr 4223 ax-un 4447 ax-setind 4550 ax-iinf 4601 ax-cnex 7919 ax-resscn 7920 ax-1cn 7921 ax-1re 7922 ax-icn 7923 ax-addcl 7924 ax-addrcl 7925 ax-mulcl 7926 ax-mulrcl 7927 ax-addcom 7928 ax-mulcom 7929 ax-addass 7930 ax-mulass 7931 ax-distr 7932 ax-i2m1 7933 ax-0lt1 7934 ax-1rid 7935 ax-0id 7936 ax-rnegex 7937 ax-precex 7938 ax-cnre 7939 ax-pre-ltirr 7940 ax-pre-ltwlin 7941 ax-pre-lttrn 7942 ax-pre-apti 7943 ax-pre-ltadd 7944 ax-pre-mulgt0 7945 ax-pre-mulext 7946

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 980 df-3an 981 df-tru 1366 df-fal 1369 df-nf 1471 df-sb 1773 df-eu 2040 df-mo 2041 df-clab 2175 df-cleq 2181 df-clel 2184 df-nfc 2320 df-ne 2360 df-nel 2455 df-ral 2472 df-rex 2473 df-reu 2474 df-rmo 2475 df-rab 2476 df-v 2753 df-sbc 2977 df-csb 3072 df-dif 3145 df-un 3147 df-in 3149 df-ss 3156 df-nul 3437 df-if 3549 df-pw 3591 df-sn 3612 df-pr 3613 df-op 3615 df-uni 3824 df-int 3859 df-iun 3902 df-br 4018 df-opab 4079 df-mpt 4080 df-tr 4116 df-id 4307 df-po 4310 df-iso 4311 df-iord 4380 df-on 4382 df-ilim 4383 df-suc 4385 df-iom 4604 df-xp 4646 df-rel 4647 df-cnv 4648 df-co 4649 df-dm 4650 df-rn 4651 df-res 4652 df-ima 4653 df-iota 5192 df-fun 5232 df-fn 5233 df-f 5234 df-f1 5235 df-fo 5236 df-f1o 5237 df-fv 5238 df-riota 5846 df-ov 5893 df-oprab 5894 df-mpo 5895 df-1st 6158 df-2nd 6159 df-recs 6323 df-frec 6409 df-pnf 8011 df-mnf 8012 df-xr 8013 df-ltxr 8014 df-le 8015 df-sub 8147 df-neg 8148 df-reap 8549 df-ap 8556 df-div 8647 df-inn 8937 df-2 8995 df-3 8996 df-4 8997 df-n0 9194 df-z 9271 df-uz 9546 df-rp 9671 df-seqfrec 10463 df-exp 10537

This theorem is referenced by: resqrexlemdec 11037 resqrexlemcalc2 11041 resqrexlemnmsq 11043 resqrexlemga 11049

W3C validator