resqrexlemover - Intuitionistic Logic Explorer

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

Theorem resqrexlemover 11021

Description: Lemma for resqrex 11037. 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 5517	. . . . . 6
2	1	oveq1d 5892	. . . . 5
3	2	breq2d 4017	. . . 4
4	3	imbi2d 230	. . 3
5		fveq2 5517	. . . . . 6
6	5	oveq1d 5892	. . . . 5
7	6	breq2d 4017	. . . 4
8	7	imbi2d 230	. . 3
9		fveq2 5517	. . . . . 6
10	9	oveq1d 5892	. . . . 5
11	10	breq2d 4017	. . . 4
12	11	imbi2d 230	. . 3
13		fveq2 5517	. . . . . 6
14	13	oveq1d 5892	. . . . 5
15	14	breq2d 4017	. . . 4
16	15	imbi2d 230	. . 3
17		resqrexlemex.a	. . . . 5
18	17	resqcld 10682	. . . . . 6
19		2re 8991	. . . . . . . 8
20	19	a1i 9	. . . . . . 7
21	20, 17	remulcld 7990	. . . . . 6
22	18, 21	readdcld 7989	. . . . 5
23		1red 7974	. . . . . 6
24	22, 23	readdcld 7989	. . . . 5
25	17	recnd 7988	. . . . . . . 8
26	25	mulid2d 7978	. . . . . . 7
27		resqrexlemex.agt0	. . . . . . . 8
28		1le2 9129	. . . . . . . . 9
29		lemul1a 8817	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
30	28, 29	mpan2 425	. . . . . . . 8 $/\$ $/\$ $/\$
31	23, 20, 17, 27, 30	syl112anc 1242	. . . . . . 7
32	26, 31	eqbrtrrd 4029	. . . . . 6
33	17	sqge0d 10683	. . . . . . 7
34	21, 18	addge02d 8493	. . . . . . 7
35	33, 34	mpbid 147	. . . . . 6
36	17, 21, 22, 32, 35	letrd 8083	. . . . 5
37	22	ltp1d 8889	. . . . 5
38	17, 22, 24, 36, 37	lelttrd 8084	. . . 4
39		resqrexlemex.seq	. . . . . . . 8
40	39, 17, 27	resqrexlemf1 11019	. . . . . . 7
41		1cnd 7975	. . . . . . . 8
42	41, 25	addcomd 8110	. . . . . . 7
43	40, 42	eqtrd 2210	. . . . . 6
44	43	oveq1d 5892	. . . . 5
45		binom21 10635	. . . . . 6
46	25, 45	syl 14	. . . . 5
47	44, 46	eqtrd 2210	. . . 4
48	38, 47	breqtrrd 4033	. . 3
49	39, 17, 27	resqrexlemf 11018	. . . . . . . . . . . . . 14
50	49	ffvelcdmda 5653	. . . . . . . . . . . . 13 $/\$
51	50	rpred 9698	. . . . . . . . . . . 12 $/\$
52	17	adantr 276	. . . . . . . . . . . . 13 $/\$
53	52, 50	rerpdivcld 9730	. . . . . . . . . . . 12 $/\$
54	51, 53	resubcld 8340	. . . . . . . . . . 11 $/\$
55	54	adantr 276	. . . . . . . . . 10 $/\$ $/\$
56	55	resqcld 10682	. . . . . . . . 9 $/\$ $/\$
57		4re 8998	. . . . . . . . . 10
58	57	a1i 9	. . . . . . . . 9 $/\$ $/\$
59	51	resqcld 10682	. . . . . . . . . . . . . . 15 $/\$
60	59, 52	resubcld 8340	. . . . . . . . . . . . . 14 $/\$
61	60	adantr 276	. . . . . . . . . . . . 13 $/\$ $/\$
62	51	adantr 276	. . . . . . . . . . . . 13 $/\$ $/\$
63	52, 59	posdifd 8491	. . . . . . . . . . . . . 14 $/\$
64	63	biimpa 296	. . . . . . . . . . . . 13 $/\$ $/\$
65	50	rpgt0d 9701	. . . . . . . . . . . . . 14 $/\$
66	65	adantr 276	. . . . . . . . . . . . 13 $/\$ $/\$
67	61, 62, 64, 66	divgt0d 8894	. . . . . . . . . . . 12 $/\$ $/\$
68	51	recnd 7988	. . . . . . . . . . . . . . . 16 $/\$
69	68	sqcld 10654	. . . . . . . . . . . . . . 15 $/\$
70	69	adantr 276	. . . . . . . . . . . . . 14 $/\$ $/\$
71	25	adantr 276	. . . . . . . . . . . . . . 15 $/\$
72	71	adantr 276	. . . . . . . . . . . . . 14 $/\$ $/\$
73	68	adantr 276	. . . . . . . . . . . . . 14 $/\$ $/\$
74	50	rpap0d 9704	. . . . . . . . . . . . . . 15 $/\$ #
75	74	adantr 276	. . . . . . . . . . . . . 14 $/\$ $/\$ #
76	70, 72, 73, 75	divsubdirapd 8789	. . . . . . . . . . . . 13 $/\$ $/\$
77	73	sqvald 10653	. . . . . . . . . . . . . . . 16 $/\$ $/\$
78	77	oveq1d 5892	. . . . . . . . . . . . . . 15 $/\$ $/\$
79	73, 73, 75	divcanap3d 8754	. . . . . . . . . . . . . . 15 $/\$ $/\$
80	78, 79	eqtrd 2210	. . . . . . . . . . . . . 14 $/\$ $/\$
81	80	oveq1d 5892	. . . . . . . . . . . . 13 $/\$ $/\$
82	76, 81	eqtrd 2210	. . . . . . . . . . . 12 $/\$ $/\$
83	67, 82	breqtrd 4031	. . . . . . . . . . 11 $/\$ $/\$
84	55, 83	gt0ap0d 8588	. . . . . . . . . 10 $/\$ $/\$ #
85	55, 84	sqgt0apd 10684	. . . . . . . . 9 $/\$ $/\$
86		4pos 9018	. . . . . . . . . 10
87	86	a1i 9	. . . . . . . . 9 $/\$ $/\$
88	56, 58, 85, 87	divgt0d 8894	. . . . . . . 8 $/\$ $/\$
89	57, 86	gt0ap0ii 8587	. . . . . . . . . . 11 #
90	89	a1i 9	. . . . . . . . . 10 $/\$ $/\$ #
91	56, 58, 90	redivclapd 8794	. . . . . . . . 9 $/\$ $/\$
92	52	adantr 276	. . . . . . . . 9 $/\$ $/\$
93	91, 92	ltaddpos2d 8489	. . . . . . . 8 $/\$ $/\$
94	88, 93	mpbid 147	. . . . . . 7 $/\$ $/\$
95	39, 17, 27	resqrexlemfp1 11020	. . . . . . . . . . . . . 14 $/\$
96	95	oveq1d 5892	. . . . . . . . . . . . 13 $/\$
97	51, 53	readdcld 7989	. . . . . . . . . . . . . . 15 $/\$
98	97	recnd 7988	. . . . . . . . . . . . . 14 $/\$
99		2cnd 8994	. . . . . . . . . . . . . 14 $/\$
100		2ap0 9014	. . . . . . . . . . . . . . 15 #
101	100	a1i 9	. . . . . . . . . . . . . 14 $/\$ #
102	98, 99, 101	sqdivapd 10669	. . . . . . . . . . . . 13 $/\$
103	96, 102	eqtrd 2210	. . . . . . . . . . . 12 $/\$
104		sq2 10618	. . . . . . . . . . . . 13
105	104	oveq2i 5888	. . . . . . . . . . . 12
106	103, 105	eqtrdi 2226	. . . . . . . . . . 11 $/\$
107	71, 68, 74	divcanap2d 8751	. . . . . . . . . . . . . . . . 17 $/\$
108	107	oveq2d 5893	. . . . . . . . . . . . . . . 16 $/\$
109	108	oveq2d 5893	. . . . . . . . . . . . . . 15 $/\$
110	109	oveq1d 5892	. . . . . . . . . . . . . 14 $/\$
111	110	oveq1d 5892	. . . . . . . . . . . . 13 $/\$
112	53	recnd 7988	. . . . . . . . . . . . . . 15 $/\$
113		binom2sub 10636	. . . . . . . . . . . . . . 15 $/\$
114	68, 112, 113	syl2anc 411	. . . . . . . . . . . . . 14 $/\$
115	114	oveq1d 5892	. . . . . . . . . . . . 13 $/\$
116		binom2 10634	. . . . . . . . . . . . . . . 16 $/\$
117	68, 112, 116	syl2anc 411	. . . . . . . . . . . . . . 15 $/\$
118	108	oveq2d 5893	. . . . . . . . . . . . . . . 16 $/\$
119	118	oveq1d 5892	. . . . . . . . . . . . . . 15 $/\$
120	117, 119	eqtrd 2210	. . . . . . . . . . . . . 14 $/\$
121	99, 71	mulcld 7980	. . . . . . . . . . . . . . . . . 18 $/\$
122	121	negcld 8257	. . . . . . . . . . . . . . . . 17 $/\$
123		4cn 8999	. . . . . . . . . . . . . . . . . . 19
124	123	a1i 9	. . . . . . . . . . . . . . . . . 18 $/\$
125	124, 71	mulcld 7980	. . . . . . . . . . . . . . . . 17 $/\$
126	69, 122, 125	addassd 7982	. . . . . . . . . . . . . . . 16 $/\$
127	69, 121	negsubd 8276	. . . . . . . . . . . . . . . . 17 $/\$
128	127	oveq1d 5892	. . . . . . . . . . . . . . . 16 $/\$
129		2cn 8992	. . . . . . . . . . . . . . . . . . . . . 22
130	129	negcli 8227	. . . . . . . . . . . . . . . . . . . . 21
131	130	a1i 9	. . . . . . . . . . . . . . . . . . . 20 $/\$
132	131, 124, 71	adddird 7985	. . . . . . . . . . . . . . . . . . 19 $/\$
133	99, 71	mulneg1d 8370	. . . . . . . . . . . . . . . . . . . 20 $/\$
134	133	oveq1d 5892	. . . . . . . . . . . . . . . . . . 19 $/\$
135	132, 134	eqtrd 2210	. . . . . . . . . . . . . . . . . 18 $/\$
136	130, 129, 129	addassi 7967	. . . . . . . . . . . . . . . . . . . 20
137	129	subidi 8230	. . . . . . . . . . . . . . . . . . . . . . . 24
138	137	negeqi 8153	. . . . . . . . . . . . . . . . . . . . . . 23
139	129, 129	negsubdii 8244	. . . . . . . . . . . . . . . . . . . . . . 23
140		neg0 8205	. . . . . . . . . . . . . . . . . . . . . . 23
141	138, 139, 140	3eqtr3i 2206	. . . . . . . . . . . . . . . . . . . . . 22
142	141	oveq1i 5887	. . . . . . . . . . . . . . . . . . . . 21
143	129	addid2i 8102	. . . . . . . . . . . . . . . . . . . . 21
144	142, 143	eqtri 2198	. . . . . . . . . . . . . . . . . . . 20
145		2p2e4 9048	. . . . . . . . . . . . . . . . . . . . 21
146	145	oveq2i 5888	. . . . . . . . . . . . . . . . . . . 20
147	136, 144, 146	3eqtr3ri 2207	. . . . . . . . . . . . . . . . . . 19
148	147	oveq1i 5887	. . . . . . . . . . . . . . . . . 18
149	135, 148	eqtr3di 2225	. . . . . . . . . . . . . . . . 17 $/\$
150	149	oveq2d 5893	. . . . . . . . . . . . . . . 16 $/\$
151	126, 128, 150	3eqtr3rd 2219	. . . . . . . . . . . . . . 15 $/\$
152	151	oveq1d 5892	. . . . . . . . . . . . . 14 $/\$
153	19	a1i 9	. . . . . . . . . . . . . . . . 17 $/\$
154	153, 52	remulcld 7990	. . . . . . . . . . . . . . . 16 $/\$
155	59, 154	resubcld 8340	. . . . . . . . . . . . . . 15 $/\$
156	57	a1i 9	. . . . . . . . . . . . . . . 16 $/\$
157	156, 52	remulcld 7990	. . . . . . . . . . . . . . 15 $/\$
158	53	resqcld 10682	. . . . . . . . . . . . . . 15 $/\$
159		recn 7946	. . . . . . . . . . . . . . . . 17
160		recn 7946	. . . . . . . . . . . . . . . . 17
161		addcom 8096	. . . . . . . . . . . . . . . . 17 $/\$
162	159, 160, 161	syl2an 289	. . . . . . . . . . . . . . . 16 $/\$
163	162	adantl 277	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
164		recn 7946	. . . . . . . . . . . . . . . . 17
165		addass 7943	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
166	159, 160, 164, 165	syl3an 1280	. . . . . . . . . . . . . . . 16 $/\$ $/\$
167	166	adantl 277	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
168	155, 157, 158, 163, 167	caov32d 6057	. . . . . . . . . . . . . 14 $/\$
169	120, 152, 168	3eqtrd 2214	. . . . . . . . . . . . 13 $/\$
170	111, 115, 169	3eqtr4rd 2221	. . . . . . . . . . . 12 $/\$
171	170	oveq1d 5892	. . . . . . . . . . 11 $/\$
172	106, 171	eqtrd 2210	. . . . . . . . . 10 $/\$
173	68, 112	subcld 8270	. . . . . . . . . . . 12 $/\$
174	173	sqcld 10654	. . . . . . . . . . 11 $/\$
175	89	a1i 9	. . . . . . . . . . 11 $/\$ #
176	174, 125, 124, 175	divdirapd 8788	. . . . . . . . . 10 $/\$
177	71, 124, 175	divcanap3d 8754	. . . . . . . . . . 11 $/\$
178	177	oveq2d 5893	. . . . . . . . . 10 $/\$
179	172, 176, 178	3eqtrd 2214	. . . . . . . . 9 $/\$
180	179	breq2d 4017	. . . . . . . 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 8937	. 2
187	186	impcom 125	1 $/\$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wb 105 $/\$ w3a 978

wceq 1353

wcel 2148

csn 3594 class class class wbr 4005

cxp 4626

cfv 5218 (class class class)co 5877

cmpo 5879

cc 7811

cr 7812

cc0 7813

c1 7814

caddc 7816

cmul 7818

clt 7994

cle 7995

cmin 8130

cneg 8131 # cap 8540

cdiv 8631

cn 8921

c2 8972

c4 8974

crp 9655

cseq 10447

cexp 10521

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 614 ax-in2 615 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-13 2150 ax-14 2151 ax-ext 2159 ax-coll 4120 ax-sep 4123 ax-nul 4131 ax-pow 4176 ax-pr 4211 ax-un 4435 ax-setind 4538 ax-iinf 4589 ax-cnex 7904 ax-resscn 7905 ax-1cn 7906 ax-1re 7907 ax-icn 7908 ax-addcl 7909 ax-addrcl 7910 ax-mulcl 7911 ax-mulrcl 7912 ax-addcom 7913 ax-mulcom 7914 ax-addass 7915 ax-mulass 7916 ax-distr 7917 ax-i2m1 7918 ax-0lt1 7919 ax-1rid 7920 ax-0id 7921 ax-rnegex 7922 ax-precex 7923 ax-cnre 7924 ax-pre-ltirr 7925 ax-pre-ltwlin 7926 ax-pre-lttrn 7927 ax-pre-apti 7928 ax-pre-ltadd 7929 ax-pre-mulgt0 7930 ax-pre-mulext 7931

This theorem depends on definitions: df-bi 117 df-dc 835 df-3or 979 df-3an 980 df-tru 1356 df-fal 1359 df-nf 1461 df-sb 1763 df-eu 2029 df-mo 2030 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ne 2348 df-nel 2443 df-ral 2460 df-rex 2461 df-reu 2462 df-rmo 2463 df-rab 2464 df-v 2741 df-sbc 2965 df-csb 3060 df-dif 3133 df-un 3135 df-in 3137 df-ss 3144 df-nul 3425 df-if 3537 df-pw 3579 df-sn 3600 df-pr 3601 df-op 3603 df-uni 3812 df-int 3847 df-iun 3890 df-br 4006 df-opab 4067 df-mpt 4068 df-tr 4104 df-id 4295 df-po 4298 df-iso 4299 df-iord 4368 df-on 4370 df-ilim 4371 df-suc 4373 df-iom 4592 df-xp 4634 df-rel 4635 df-cnv 4636 df-co 4637 df-dm 4638 df-rn 4639 df-res 4640 df-ima 4641 df-iota 5180 df-fun 5220 df-fn 5221 df-f 5222 df-f1 5223 df-fo 5224 df-f1o 5225 df-fv 5226 df-riota 5833 df-ov 5880 df-oprab 5881 df-mpo 5882 df-1st 6143 df-2nd 6144 df-recs 6308 df-frec 6394 df-pnf 7996 df-mnf 7997 df-xr 7998 df-ltxr 7999 df-le 8000 df-sub 8132 df-neg 8133 df-reap 8534 df-ap 8541 df-div 8632 df-inn 8922 df-2 8980 df-3 8981 df-4 8982 df-n0 9179 df-z 9256 df-uz 9531 df-rp 9656 df-seqfrec 10448 df-exp 10522

This theorem is referenced by: resqrexlemdec 11022 resqrexlemcalc2 11026 resqrexlemnmsq 11028 resqrexlemga 11034

W3C validator