resqrexlemover - Intuitionistic Logic Explorer

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

Theorem resqrexlemover 11154

Description: Lemma for resqrex 11170. 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 5554	. . . . . 6
2	1	oveq1d 5933	. . . . 5
3	2	breq2d 4041	. . . 4
4	3	imbi2d 230	. . 3
5		fveq2 5554	. . . . . 6
6	5	oveq1d 5933	. . . . 5
7	6	breq2d 4041	. . . 4
8	7	imbi2d 230	. . 3
9		fveq2 5554	. . . . . 6
10	9	oveq1d 5933	. . . . 5
11	10	breq2d 4041	. . . 4
12	11	imbi2d 230	. . 3
13		fveq2 5554	. . . . . 6
14	13	oveq1d 5933	. . . . 5
15	14	breq2d 4041	. . . 4
16	15	imbi2d 230	. . 3
17		resqrexlemex.a	. . . . 5
18	17	resqcld 10770	. . . . . 6
19		2re 9052	. . . . . . . 8
20	19	a1i 9	. . . . . . 7
21	20, 17	remulcld 8050	. . . . . 6
22	18, 21	readdcld 8049	. . . . 5
23		1red 8034	. . . . . 6
24	22, 23	readdcld 8049	. . . . 5
25	17	recnd 8048	. . . . . . . 8
26	25	mulid2d 8038	. . . . . . 7
27		resqrexlemex.agt0	. . . . . . . 8
28		1le2 9190	. . . . . . . . 9
29		lemul1a 8877	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
30	28, 29	mpan2 425	. . . . . . . 8 $/\$ $/\$ $/\$
31	23, 20, 17, 27, 30	syl112anc 1253	. . . . . . 7
32	26, 31	eqbrtrrd 4053	. . . . . 6
33	17	sqge0d 10771	. . . . . . 7
34	21, 18	addge02d 8553	. . . . . . 7
35	33, 34	mpbid 147	. . . . . 6
36	17, 21, 22, 32, 35	letrd 8143	. . . . 5
37	22	ltp1d 8949	. . . . 5
38	17, 22, 24, 36, 37	lelttrd 8144	. . . 4
39		resqrexlemex.seq	. . . . . . . 8
40	39, 17, 27	resqrexlemf1 11152	. . . . . . 7
41		1cnd 8035	. . . . . . . 8
42	41, 25	addcomd 8170	. . . . . . 7
43	40, 42	eqtrd 2226	. . . . . 6
44	43	oveq1d 5933	. . . . 5
45		binom21 10723	. . . . . 6
46	25, 45	syl 14	. . . . 5
47	44, 46	eqtrd 2226	. . . 4
48	38, 47	breqtrrd 4057	. . 3
49	39, 17, 27	resqrexlemf 11151	. . . . . . . . . . . . . 14
50	49	ffvelcdmda 5693	. . . . . . . . . . . . 13 $/\$
51	50	rpred 9762	. . . . . . . . . . . 12 $/\$
52	17	adantr 276	. . . . . . . . . . . . 13 $/\$
53	52, 50	rerpdivcld 9794	. . . . . . . . . . . 12 $/\$
54	51, 53	resubcld 8400	. . . . . . . . . . 11 $/\$
55	54	adantr 276	. . . . . . . . . 10 $/\$ $/\$
56	55	resqcld 10770	. . . . . . . . 9 $/\$ $/\$
57		4re 9059	. . . . . . . . . 10
58	57	a1i 9	. . . . . . . . 9 $/\$ $/\$
59	51	resqcld 10770	. . . . . . . . . . . . . . 15 $/\$
60	59, 52	resubcld 8400	. . . . . . . . . . . . . 14 $/\$
61	60	adantr 276	. . . . . . . . . . . . 13 $/\$ $/\$
62	51	adantr 276	. . . . . . . . . . . . 13 $/\$ $/\$
63	52, 59	posdifd 8551	. . . . . . . . . . . . . 14 $/\$
64	63	biimpa 296	. . . . . . . . . . . . 13 $/\$ $/\$
65	50	rpgt0d 9765	. . . . . . . . . . . . . 14 $/\$
66	65	adantr 276	. . . . . . . . . . . . 13 $/\$ $/\$
67	61, 62, 64, 66	divgt0d 8954	. . . . . . . . . . . 12 $/\$ $/\$
68	51	recnd 8048	. . . . . . . . . . . . . . . 16 $/\$
69	68	sqcld 10742	. . . . . . . . . . . . . . 15 $/\$
70	69	adantr 276	. . . . . . . . . . . . . 14 $/\$ $/\$
71	25	adantr 276	. . . . . . . . . . . . . . 15 $/\$
72	71	adantr 276	. . . . . . . . . . . . . 14 $/\$ $/\$
73	68	adantr 276	. . . . . . . . . . . . . 14 $/\$ $/\$
74	50	rpap0d 9768	. . . . . . . . . . . . . . 15 $/\$ #
75	74	adantr 276	. . . . . . . . . . . . . 14 $/\$ $/\$ #
76	70, 72, 73, 75	divsubdirapd 8849	. . . . . . . . . . . . 13 $/\$ $/\$
77	73	sqvald 10741	. . . . . . . . . . . . . . . 16 $/\$ $/\$
78	77	oveq1d 5933	. . . . . . . . . . . . . . 15 $/\$ $/\$
79	73, 73, 75	divcanap3d 8814	. . . . . . . . . . . . . . 15 $/\$ $/\$
80	78, 79	eqtrd 2226	. . . . . . . . . . . . . 14 $/\$ $/\$
81	80	oveq1d 5933	. . . . . . . . . . . . 13 $/\$ $/\$
82	76, 81	eqtrd 2226	. . . . . . . . . . . 12 $/\$ $/\$
83	67, 82	breqtrd 4055	. . . . . . . . . . 11 $/\$ $/\$
84	55, 83	gt0ap0d 8648	. . . . . . . . . 10 $/\$ $/\$ #
85	55, 84	sqgt0apd 10772	. . . . . . . . 9 $/\$ $/\$
86		4pos 9079	. . . . . . . . . 10
87	86	a1i 9	. . . . . . . . 9 $/\$ $/\$
88	56, 58, 85, 87	divgt0d 8954	. . . . . . . 8 $/\$ $/\$
89	57, 86	gt0ap0ii 8647	. . . . . . . . . . 11 #
90	89	a1i 9	. . . . . . . . . 10 $/\$ $/\$ #
91	56, 58, 90	redivclapd 8854	. . . . . . . . 9 $/\$ $/\$
92	52	adantr 276	. . . . . . . . 9 $/\$ $/\$
93	91, 92	ltaddpos2d 8549	. . . . . . . 8 $/\$ $/\$
94	88, 93	mpbid 147	. . . . . . 7 $/\$ $/\$
95	39, 17, 27	resqrexlemfp1 11153	. . . . . . . . . . . . . 14 $/\$
96	95	oveq1d 5933	. . . . . . . . . . . . 13 $/\$
97	51, 53	readdcld 8049	. . . . . . . . . . . . . . 15 $/\$
98	97	recnd 8048	. . . . . . . . . . . . . 14 $/\$
99		2cnd 9055	. . . . . . . . . . . . . 14 $/\$
100		2ap0 9075	. . . . . . . . . . . . . . 15 #
101	100	a1i 9	. . . . . . . . . . . . . 14 $/\$ #
102	98, 99, 101	sqdivapd 10757	. . . . . . . . . . . . 13 $/\$
103	96, 102	eqtrd 2226	. . . . . . . . . . . 12 $/\$
104		sq2 10706	. . . . . . . . . . . . 13
105	104	oveq2i 5929	. . . . . . . . . . . 12
106	103, 105	eqtrdi 2242	. . . . . . . . . . 11 $/\$
107	71, 68, 74	divcanap2d 8811	. . . . . . . . . . . . . . . . 17 $/\$
108	107	oveq2d 5934	. . . . . . . . . . . . . . . 16 $/\$
109	108	oveq2d 5934	. . . . . . . . . . . . . . 15 $/\$
110	109	oveq1d 5933	. . . . . . . . . . . . . 14 $/\$
111	110	oveq1d 5933	. . . . . . . . . . . . 13 $/\$
112	53	recnd 8048	. . . . . . . . . . . . . . 15 $/\$
113		binom2sub 10724	. . . . . . . . . . . . . . 15 $/\$
114	68, 112, 113	syl2anc 411	. . . . . . . . . . . . . 14 $/\$
115	114	oveq1d 5933	. . . . . . . . . . . . 13 $/\$
116		binom2 10722	. . . . . . . . . . . . . . . 16 $/\$
117	68, 112, 116	syl2anc 411	. . . . . . . . . . . . . . 15 $/\$
118	108	oveq2d 5934	. . . . . . . . . . . . . . . 16 $/\$
119	118	oveq1d 5933	. . . . . . . . . . . . . . 15 $/\$
120	117, 119	eqtrd 2226	. . . . . . . . . . . . . 14 $/\$
121	99, 71	mulcld 8040	. . . . . . . . . . . . . . . . . 18 $/\$
122	121	negcld 8317	. . . . . . . . . . . . . . . . 17 $/\$
123		4cn 9060	. . . . . . . . . . . . . . . . . . 19
124	123	a1i 9	. . . . . . . . . . . . . . . . . 18 $/\$
125	124, 71	mulcld 8040	. . . . . . . . . . . . . . . . 17 $/\$
126	69, 122, 125	addassd 8042	. . . . . . . . . . . . . . . 16 $/\$
127	69, 121	negsubd 8336	. . . . . . . . . . . . . . . . 17 $/\$
128	127	oveq1d 5933	. . . . . . . . . . . . . . . 16 $/\$
129		2cn 9053	. . . . . . . . . . . . . . . . . . . . . 22
130	129	negcli 8287	. . . . . . . . . . . . . . . . . . . . 21
131	130	a1i 9	. . . . . . . . . . . . . . . . . . . 20 $/\$
132	131, 124, 71	adddird 8045	. . . . . . . . . . . . . . . . . . 19 $/\$
133	99, 71	mulneg1d 8430	. . . . . . . . . . . . . . . . . . . 20 $/\$
134	133	oveq1d 5933	. . . . . . . . . . . . . . . . . . 19 $/\$
135	132, 134	eqtrd 2226	. . . . . . . . . . . . . . . . . 18 $/\$
136	130, 129, 129	addassi 8027	. . . . . . . . . . . . . . . . . . . 20
137	129	subidi 8290	. . . . . . . . . . . . . . . . . . . . . . . 24
138	137	negeqi 8213	. . . . . . . . . . . . . . . . . . . . . . 23
139	129, 129	negsubdii 8304	. . . . . . . . . . . . . . . . . . . . . . 23
140		neg0 8265	. . . . . . . . . . . . . . . . . . . . . . 23
141	138, 139, 140	3eqtr3i 2222	. . . . . . . . . . . . . . . . . . . . . 22
142	141	oveq1i 5928	. . . . . . . . . . . . . . . . . . . . 21
143	129	addid2i 8162	. . . . . . . . . . . . . . . . . . . . 21
144	142, 143	eqtri 2214	. . . . . . . . . . . . . . . . . . . 20
145		2p2e4 9109	. . . . . . . . . . . . . . . . . . . . 21
146	145	oveq2i 5929	. . . . . . . . . . . . . . . . . . . 20
147	136, 144, 146	3eqtr3ri 2223	. . . . . . . . . . . . . . . . . . 19
148	147	oveq1i 5928	. . . . . . . . . . . . . . . . . 18
149	135, 148	eqtr3di 2241	. . . . . . . . . . . . . . . . 17 $/\$
150	149	oveq2d 5934	. . . . . . . . . . . . . . . 16 $/\$
151	126, 128, 150	3eqtr3rd 2235	. . . . . . . . . . . . . . 15 $/\$
152	151	oveq1d 5933	. . . . . . . . . . . . . 14 $/\$
153	19	a1i 9	. . . . . . . . . . . . . . . . 17 $/\$
154	153, 52	remulcld 8050	. . . . . . . . . . . . . . . 16 $/\$
155	59, 154	resubcld 8400	. . . . . . . . . . . . . . 15 $/\$
156	57	a1i 9	. . . . . . . . . . . . . . . 16 $/\$
157	156, 52	remulcld 8050	. . . . . . . . . . . . . . 15 $/\$
158	53	resqcld 10770	. . . . . . . . . . . . . . 15 $/\$
159		recn 8005	. . . . . . . . . . . . . . . . 17
160		recn 8005	. . . . . . . . . . . . . . . . 17
161		addcom 8156	. . . . . . . . . . . . . . . . 17 $/\$
162	159, 160, 161	syl2an 289	. . . . . . . . . . . . . . . 16 $/\$
163	162	adantl 277	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
164		recn 8005	. . . . . . . . . . . . . . . . 17
165		addass 8002	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
166	159, 160, 164, 165	syl3an 1291	. . . . . . . . . . . . . . . 16 $/\$ $/\$
167	166	adantl 277	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
168	155, 157, 158, 163, 167	caov32d 6099	. . . . . . . . . . . . . 14 $/\$
169	120, 152, 168	3eqtrd 2230	. . . . . . . . . . . . 13 $/\$
170	111, 115, 169	3eqtr4rd 2237	. . . . . . . . . . . 12 $/\$
171	170	oveq1d 5933	. . . . . . . . . . 11 $/\$
172	106, 171	eqtrd 2226	. . . . . . . . . 10 $/\$
173	68, 112	subcld 8330	. . . . . . . . . . . 12 $/\$
174	173	sqcld 10742	. . . . . . . . . . 11 $/\$
175	89	a1i 9	. . . . . . . . . . 11 $/\$ #
176	174, 125, 124, 175	divdirapd 8848	. . . . . . . . . 10 $/\$
177	71, 124, 175	divcanap3d 8814	. . . . . . . . . . 11 $/\$
178	177	oveq2d 5934	. . . . . . . . . 10 $/\$
179	172, 176, 178	3eqtrd 2230	. . . . . . . . 9 $/\$
180	179	breq2d 4041	. . . . . . . 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 8998	. 2
187	186	impcom 125	1 $/\$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wb 105 $/\$ w3a 980

wceq 1364

wcel 2164

csn 3618 class class class wbr 4029

cxp 4657

cfv 5254 (class class class)co 5918

cmpo 5920

cc 7870

cr 7871

cc0 7872

c1 7873

caddc 7875

cmul 7877

clt 8054

cle 8055

cmin 8190

cneg 8191 # cap 8600

cdiv 8691

cn 8982

c2 9033

c4 9035

crp 9719

cseq 10518

cexp 10609

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 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2166 ax-14 2167 ax-ext 2175 ax-coll 4144 ax-sep 4147 ax-nul 4155 ax-pow 4203 ax-pr 4238 ax-un 4464 ax-setind 4569 ax-iinf 4620 ax-cnex 7963 ax-resscn 7964 ax-1cn 7965 ax-1re 7966 ax-icn 7967 ax-addcl 7968 ax-addrcl 7969 ax-mulcl 7970 ax-mulrcl 7971 ax-addcom 7972 ax-mulcom 7973 ax-addass 7974 ax-mulass 7975 ax-distr 7976 ax-i2m1 7977 ax-0lt1 7978 ax-1rid 7979 ax-0id 7980 ax-rnegex 7981 ax-precex 7982 ax-cnre 7983 ax-pre-ltirr 7984 ax-pre-ltwlin 7985 ax-pre-lttrn 7986 ax-pre-apti 7987 ax-pre-ltadd 7988 ax-pre-mulgt0 7989 ax-pre-mulext 7990

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1472 df-sb 1774 df-eu 2045 df-mo 2046 df-clab 2180 df-cleq 2186 df-clel 2189 df-nfc 2325 df-ne 2365 df-nel 2460 df-ral 2477 df-rex 2478 df-reu 2479 df-rmo 2480 df-rab 2481 df-v 2762 df-sbc 2986 df-csb 3081 df-dif 3155 df-un 3157 df-in 3159 df-ss 3166 df-nul 3447 df-if 3558 df-pw 3603 df-sn 3624 df-pr 3625 df-op 3627 df-uni 3836 df-int 3871 df-iun 3914 df-br 4030 df-opab 4091 df-mpt 4092 df-tr 4128 df-id 4324 df-po 4327 df-iso 4328 df-iord 4397 df-on 4399 df-ilim 4400 df-suc 4402 df-iom 4623 df-xp 4665 df-rel 4666 df-cnv 4667 df-co 4668 df-dm 4669 df-rn 4670 df-res 4671 df-ima 4672 df-iota 5215 df-fun 5256 df-fn 5257 df-f 5258 df-f1 5259 df-fo 5260 df-f1o 5261 df-fv 5262 df-riota 5873 df-ov 5921 df-oprab 5922 df-mpo 5923 df-1st 6193 df-2nd 6194 df-recs 6358 df-frec 6444 df-pnf 8056 df-mnf 8057 df-xr 8058 df-ltxr 8059 df-le 8060 df-sub 8192 df-neg 8193 df-reap 8594 df-ap 8601 df-div 8692 df-inn 8983 df-2 9041 df-3 9042 df-4 9043 df-n0 9241 df-z 9318 df-uz 9593 df-rp 9720 df-seqfrec 10519 df-exp 10610

This theorem is referenced by: resqrexlemdec 11155 resqrexlemcalc2 11159 resqrexlemnmsq 11161 resqrexlemga 11167

W3C validator