trilpolemlt1 - Mathbox for Jim Kingdon

	Mathbox for Jim Kingdon		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > Mathboxes > trilpolemlt1		Unicode version

Theorem trilpolemlt1 16645

Description: Lemma for trilpo 16647. The

case. We can use the distance between

and one (that is,

) to find a position in the sequence

where terms after that point will not add up to as much as

. By finomni 7338 we know the terms up to

either contain a zero or are all one. But if they are all one that contradicts the way we constructed

, so we know that the sequence contains a zero. (Contributed by Jim Kingdon, 23-Aug-2023.)

**Hypotheses**
Ref	Expression
trilpolemgt1.f
trilpolemgt1.a
trilpolemlt1.a

**Assertion**
Ref	Expression
trilpolemlt1

Distinct variable groups:

Proof of Theorem trilpolemlt1 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		1red 8193	. . . 4
2		trilpolemgt1.f	. . . . 5
3		trilpolemgt1.a	. . . . 5
4	2, 3	trilpolemcl 16641	. . . 4
5	1, 4	resubcld 8559	. . 3
6		trilpolemlt1.a	. . . 4
7	4, 1	posdifd 8711	. . . 4
8	6, 7	mpbid 147	. . 3
9		nnrecl 9399	. . 3 $/\$
10	5, 8, 9	syl2anc 411	. 2
11		elfznn 10288	. . . . . . 7
12	11	ad2antrl 490	. . . . . 6 $/\$ $/\$ $/\$ $/\$
13		simprl 531	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
14	13	fvresd 5664	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
15		simprr 533	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
16	14, 15	eqtr3d 2266	. . . . . 6 $/\$ $/\$ $/\$ $/\$
17	12, 16	jca 306	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
18	17	ex 115	. . . 4 $/\$ $/\$ $/\$ $/\$
19	18	reximdv2 2631	. . 3 $/\$ $/\$
20		2rp 9892	. . . . . . . . . 10
21	20	a1i 9	. . . . . . . . 9 $/\$ $/\$
22		simprl 531	. . . . . . . . . 10 $/\$ $/\$
23	22	nnzd 9600	. . . . . . . . 9 $/\$ $/\$
24	21, 23	rpexpcld 10958	. . . . . . . 8 $/\$ $/\$
25	24	rprecred 9942	. . . . . . 7 $/\$ $/\$
26	22	nnrecred 9189	. . . . . . 7 $/\$ $/\$
27	5	adantr 276	. . . . . . 7 $/\$ $/\$
28		2z 9506	. . . . . . . . . 10
29		uzid 9769	. . . . . . . . . 10
30	28, 29	mp1i 10	. . . . . . . . 9 $/\$ $/\$
31	22	nnnn0d 9454	. . . . . . . . 9 $/\$ $/\$
32		bernneq3 10923	. . . . . . . . 9 $/\$
33	30, 31, 32	syl2anc 411	. . . . . . . 8 $/\$ $/\$
34	22	nnrpd 9928	. . . . . . . . 9 $/\$ $/\$
35	34, 24	ltrecd 9949	. . . . . . . 8 $/\$ $/\$
36	33, 35	mpbid 147	. . . . . . 7 $/\$ $/\$
37		simprr 533	. . . . . . 7 $/\$ $/\$
38	25, 26, 27, 36, 37	lttrd 8304	. . . . . 6 $/\$ $/\$
39	38	adantr 276	. . . . 5 $/\$ $/\$ $/\$
40	27	adantr 276	. . . . . 6 $/\$ $/\$ $/\$
41	25	adantr 276	. . . . . 6 $/\$ $/\$ $/\$
42		1red 8193	. . . . . . 7 $/\$ $/\$ $/\$
43	4	ad2antrr 488	. . . . . . 7 $/\$ $/\$ $/\$
44		0red 8179	. . . . . . . . . 10 $/\$ $/\$ $/\$
45		eqid 2231	. . . . . . . . . . 11
46	22	adantr 276	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
47	46	peano2nnd 9157	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
48	47	nnzd 9600	. . . . . . . . . . 11 $/\$ $/\$ $/\$
49		eluznn 9833	. . . . . . . . . . . . 13 $/\$
50	47, 49	sylan 283	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
51		eqid 2231	. . . . . . . . . . . . 13
52		oveq2 6025	. . . . . . . . . . . . . . 15
53	52	oveq2d 6033	. . . . . . . . . . . . . 14
54		fveq2 5639	. . . . . . . . . . . . . 14
55	53, 54	oveq12d 6035	. . . . . . . . . . . . 13
56		simpr 110	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
57	20	a1i 9	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
58	56	nnzd 9600	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
59	57, 58	rpexpcld 10958	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
60	59	rprecred 9942	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
61		0re 8178	. . . . . . . . . . . . . . . 16
62		1re 8177	. . . . . . . . . . . . . . . 16
63		prssi 3831	. . . . . . . . . . . . . . . 16 $/\$
64	61, 62, 63	mp2an 426	. . . . . . . . . . . . . . 15
65	2	adantr 276	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
66	65	ad2antrr 488	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
67	66, 56	ffvelcdmd 5783	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
68	64, 67	sselid 3225	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
69	60, 68	remulcld 8209	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
70	51, 55, 56, 69	fvmptd3 5740	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
71	50, 70	syldan 282	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
72	50, 69	syldan 282	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
73	65	adantr 276	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
74	73, 51	trilpolemclim 16640	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
75		nnuz 9791	. . . . . . . . . . . . 13
76	69	recnd 8207	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
77	70, 76	eqeltrd 2308	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
78	75, 47, 77	iserex 11899	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
79	74, 78	mpbid 147	. . . . . . . . . . 11 $/\$ $/\$ $/\$
80	45, 48, 71, 72, 79	isumrecl 11989	. . . . . . . . . 10 $/\$ $/\$ $/\$
81		1zzd 9505	. . . . . . . . . . . . 13 $/\$ $/\$
82	81, 23	fzfigd 10692	. . . . . . . . . . . 12 $/\$ $/\$
83	82	adantr 276	. . . . . . . . . . 11 $/\$ $/\$ $/\$
84	20	a1i 9	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
85		elfzelz 10259	. . . . . . . . . . . . . 14
86	85	adantl 277	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
87	84, 86	rpexpcld 10958	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
88	87	rprecred 9942	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
89	83, 88	fsumrecl 11961	. . . . . . . . . 10 $/\$ $/\$ $/\$
90	50, 60	syldan 282	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
91	50, 68	syldan 282	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
92	59	rpreccld 9941	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
93	50, 92	syldan 282	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
94	93	rpge0d 9934	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
95		0le0 9231	. . . . . . . . . . . . . 14
96		simpr 110	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
97	95, 96	breqtrrid 4126	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
98		0le1 8660	. . . . . . . . . . . . . 14
99		simpr 110	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
100	98, 99	breqtrrid 4126	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
101	73	adantr 276	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
102	101, 50	ffvelcdmd 5783	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
103		elpri 3692	. . . . . . . . . . . . . 14 $\/$
104	102, 103	syl 14	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $\/$
105	97, 100, 104	mpjaodan 805	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
106	90, 91, 94, 105	mulge0d 8800	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
107	45, 48, 71, 72, 79, 106	isumge0 11990	. . . . . . . . . 10 $/\$ $/\$ $/\$
108	44, 80, 89, 107	leadd2dd 8739	. . . . . . . . 9 $/\$ $/\$ $/\$
109	89	recnd 8207	. . . . . . . . . . 11 $/\$ $/\$ $/\$
110	109	addridd 8327	. . . . . . . . . 10 $/\$ $/\$ $/\$
111	110	eqcomd 2237	. . . . . . . . 9 $/\$ $/\$ $/\$
112	75, 45, 47, 70, 76, 74	isumsplit 12051	. . . . . . . . . . 11 $/\$ $/\$ $/\$
113	3, 112	eqtrid 2276	. . . . . . . . . 10 $/\$ $/\$ $/\$
114	46	nncnd 9156	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
115		1cnd 8194	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
116	114, 115	pncand 8490	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
117	116	oveq2d 6033	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
118		simpr 110	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
119	118	fvresd 5664	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
120		fveqeq2 5648	. . . . . . . . . . . . . . . 16
121		simplr 529	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
122	120, 121, 118	rspcdva 2915	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
123	119, 122	eqtr3d 2266	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
124	123	oveq2d 6033	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
125	87	rpreccld 9941	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
126	125	rpcnd 9932	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
127	126	mulridd 8195	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
128	124, 127	eqtrd 2264	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
129	117, 128	sumeq12rdv 11933	. . . . . . . . . . 11 $/\$ $/\$ $/\$
130	129	oveq1d 6032	. . . . . . . . . 10 $/\$ $/\$ $/\$
131	113, 130	eqtrd 2264	. . . . . . . . 9 $/\$ $/\$ $/\$
132	108, 111, 131	3brtr4d 4120	. . . . . . . 8 $/\$ $/\$ $/\$
133		geo2sum 12074	. . . . . . . . . 10 $/\$
134	133	breq1d 4098	. . . . . . . . 9 $/\$
135	46, 115, 134	syl2anc 411	. . . . . . . 8 $/\$ $/\$ $/\$
136	132, 135	mpbid 147	. . . . . . 7 $/\$ $/\$ $/\$
137	42, 41, 43, 136	subled 8727	. . . . . 6 $/\$ $/\$ $/\$
138	40, 41, 137	lensymd 8300	. . . . 5 $/\$ $/\$ $/\$
139	39, 138	pm2.21dd 625	. . . 4 $/\$ $/\$ $/\$
140	139	ex 115	. . 3 $/\$ $/\$
141		fveq1 5638	. . . . . . 7
142	141	eqeq1d 2240	. . . . . 6
143	142	rexbidv 2533	. . . . 5
144	141	eqeq1d 2240	. . . . . 6
145	144	ralbidv 2532	. . . . 5
146	143, 145	orbi12d 800	. . . 4 $\/$ $\/$
147		finomni 7338	. . . . . 6 Omni
148	82, 147	syl 14	. . . . 5 $/\$ $/\$ Omni
149		isomninn 16635	. . . . . 6 Omni Omni $\/$
150	148, 149	syl 14	. . . . 5 $/\$ $/\$ Omni $\/$
151	148, 150	mpbid 147	. . . 4 $/\$ $/\$ $\/$
152		fz1ssnn 10290	. . . . . . 7
153	152	a1i 9	. . . . . 6 $/\$ $/\$
154	65, 153	fssresd 5513	. . . . 5 $/\$ $/\$
155		0red 8179	. . . . . . 7 $/\$ $/\$
156		1red 8193	. . . . . . 7 $/\$ $/\$
157		prexg 4301	. . . . . . 7 $/\$
158	155, 156, 157	syl2anc 411	. . . . . 6 $/\$ $/\$
159	158, 82	elmapd 6830	. . . . 5 $/\$ $/\$
160	154, 159	mpbird 167	. . . 4 $/\$ $/\$
161	146, 151, 160	rspcdva 2915	. . 3 $/\$ $/\$ $\/$
162	19, 140, 161	mpjaod 725	. 2 $/\$ $/\$
163	10, 162	rexlimddv 2655	1

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wb 105 $\/$ wo 715

wceq 1397

wcel 2202

wral 2510

wrex 2511

cvv 2802

wss 3200

cpr 3670 class class class wbr 4088

cmpt 4150

cdm 4725

cres 4727

wf 5322

cfv 5326 (class class class)co 6017

cmap 6816

cfn 6908 Omnicomni 7332

cc 8029

cr 8030

cc0 8031

c1 8032

caddc 8034

cmul 8036

clt 8213

cle 8214

cmin 8349

cdiv 8851

cn 9142

c2 9193

cn0 9401

cz 9478

cuz 9754

crp 9887

cfz 10242

cseq 10708

cexp 10799

cli 11838

csu 11913

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 619 ax-in2 620 ax-io 716 ax-5 1495 ax-7 1496 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-10 1553 ax-11 1554 ax-i12 1555 ax-bndl 1557 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-i5r 1583 ax-13 2204 ax-14 2205 ax-ext 2213 ax-coll 4204 ax-sep 4207 ax-nul 4215 ax-pow 4264 ax-pr 4299 ax-un 4530 ax-setind 4635 ax-iinf 4686 ax-cnex 8122 ax-resscn 8123 ax-1cn 8124 ax-1re 8125 ax-icn 8126 ax-addcl 8127 ax-addrcl 8128 ax-mulcl 8129 ax-mulrcl 8130 ax-addcom 8131 ax-mulcom 8132 ax-addass 8133 ax-mulass 8134 ax-distr 8135 ax-i2m1 8136 ax-0lt1 8137 ax-1rid 8138 ax-0id 8139 ax-rnegex 8140 ax-precex 8141 ax-cnre 8142 ax-pre-ltirr 8143 ax-pre-ltwlin 8144 ax-pre-lttrn 8145 ax-pre-apti 8146 ax-pre-ltadd 8147 ax-pre-mulgt0 8148 ax-pre-mulext 8149 ax-arch 8150 ax-caucvg 8151

This theorem depends on definitions: df-bi 117 df-dc 842 df-3or 1005 df-3an 1006 df-tru 1400 df-fal 1403 df-nf 1509 df-sb 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2363 df-ne 2403 df-nel 2498 df-ral 2515 df-rex 2516 df-reu 2517 df-rmo 2518 df-rab 2519 df-v 2804 df-sbc 3032 df-csb 3128 df-dif 3202 df-un 3204 df-in 3206 df-ss 3213 df-nul 3495 df-if 3606 df-pw 3654 df-sn 3675 df-pr 3676 df-op 3678 df-uni 3894 df-int 3929 df-iun 3972 df-br 4089 df-opab 4151 df-mpt 4152 df-tr 4188 df-id 4390 df-po 4393 df-iso 4394 df-iord 4463 df-on 4465 df-ilim 4466 df-suc 4468 df-iom 4689 df-xp 4731 df-rel 4732 df-cnv 4733 df-co 4734 df-dm 4735 df-rn 4736 df-res 4737 df-ima 4738 df-iota 5286 df-fun 5328 df-fn 5329 df-f 5330 df-f1 5331 df-fo 5332 df-f1o 5333 df-fv 5334 df-isom 5335 df-riota 5970 df-ov 6020 df-oprab 6021 df-mpo 6022 df-1st 6302 df-2nd 6303 df-recs 6470 df-irdg 6535 df-frec 6556 df-1o 6581 df-2o 6582 df-oadd 6585 df-er 6701 df-map 6818 df-en 6909 df-dom 6910 df-fin 6911 df-omni 7333 df-pnf 8215 df-mnf 8216 df-xr 8217 df-ltxr 8218 df-le 8219 df-sub 8351 df-neg 8352 df-reap 8754 df-ap 8761 df-div 8852 df-inn 9143 df-2 9201 df-3 9202 df-4 9203 df-n0 9402 df-z 9479 df-uz 9755 df-q 9853 df-rp 9888 df-ico 10128 df-fz 10243 df-fzo 10377 df-seqfrec 10709 df-exp 10800 df-ihash 11037 df-cj 11402 df-re 11403 df-im 11404 df-rsqrt 11558 df-abs 11559 df-clim 11839 df-sumdc 11914

This theorem is referenced by: trilpolemres 16646 neapmkvlem 16671

W3C validator