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 15268

Description: Lemma for trilpo 15270. 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 7169 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 8003	. . . 4
2		trilpolemgt1.f	. . . . 5
3		trilpolemgt1.a	. . . . 5
4	2, 3	trilpolemcl 15264	. . . 4
5	1, 4	resubcld 8369	. . 3
6		trilpolemlt1.a	. . . 4
7	4, 1	posdifd 8520	. . . 4
8	6, 7	mpbid 147	. . 3
9		nnrecl 9205	. . 3 $/\$
10	5, 8, 9	syl2anc 411	. 2
11		elfznn 10086	. . . . . . 7
12	11	ad2antrl 490	. . . . . 6 $/\$ $/\$ $/\$ $/\$
13		simprl 529	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
14	13	fvresd 5559	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
15		simprr 531	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
16	14, 15	eqtr3d 2224	. . . . . 6 $/\$ $/\$ $/\$ $/\$
17	12, 16	jca 306	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
18	17	ex 115	. . . 4 $/\$ $/\$ $/\$ $/\$
19	18	reximdv2 2589	. . 3 $/\$ $/\$
20		2rp 9690	. . . . . . . . . 10
21	20	a1i 9	. . . . . . . . 9 $/\$ $/\$
22		simprl 529	. . . . . . . . . 10 $/\$ $/\$
23	22	nnzd 9405	. . . . . . . . 9 $/\$ $/\$
24	21, 23	rpexpcld 10712	. . . . . . . 8 $/\$ $/\$
25	24	rprecred 9740	. . . . . . 7 $/\$ $/\$
26	22	nnrecred 8997	. . . . . . 7 $/\$ $/\$
27	5	adantr 276	. . . . . . 7 $/\$ $/\$
28		2z 9312	. . . . . . . . . 10
29		uzid 9573	. . . . . . . . . 10
30	28, 29	mp1i 10	. . . . . . . . 9 $/\$ $/\$
31	22	nnnn0d 9260	. . . . . . . . 9 $/\$ $/\$
32		bernneq3 10677	. . . . . . . . 9 $/\$
33	30, 31, 32	syl2anc 411	. . . . . . . 8 $/\$ $/\$
34	22	nnrpd 9726	. . . . . . . . 9 $/\$ $/\$
35	34, 24	ltrecd 9747	. . . . . . . 8 $/\$ $/\$
36	33, 35	mpbid 147	. . . . . . 7 $/\$ $/\$
37		simprr 531	. . . . . . 7 $/\$ $/\$
38	25, 26, 27, 36, 37	lttrd 8114	. . . . . 6 $/\$ $/\$
39	38	adantr 276	. . . . 5 $/\$ $/\$ $/\$
40	27	adantr 276	. . . . . 6 $/\$ $/\$ $/\$
41	25	adantr 276	. . . . . 6 $/\$ $/\$ $/\$
42		1red 8003	. . . . . . 7 $/\$ $/\$ $/\$
43	4	ad2antrr 488	. . . . . . 7 $/\$ $/\$ $/\$
44		0red 7989	. . . . . . . . . 10 $/\$ $/\$ $/\$
45		eqid 2189	. . . . . . . . . . 11
46	22	adantr 276	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
47	46	peano2nnd 8965	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
48	47	nnzd 9405	. . . . . . . . . . 11 $/\$ $/\$ $/\$
49		eluznn 9632	. . . . . . . . . . . . 13 $/\$
50	47, 49	sylan 283	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
51		eqid 2189	. . . . . . . . . . . . 13
52		oveq2 5905	. . . . . . . . . . . . . . 15
53	52	oveq2d 5913	. . . . . . . . . . . . . 14
54		fveq2 5534	. . . . . . . . . . . . . 14
55	53, 54	oveq12d 5915	. . . . . . . . . . . . 13
56		simpr 110	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
57	20	a1i 9	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
58	56	nnzd 9405	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
59	57, 58	rpexpcld 10712	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
60	59	rprecred 9740	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
61		0re 7988	. . . . . . . . . . . . . . . 16
62		1re 7987	. . . . . . . . . . . . . . . 16
63		prssi 3765	. . . . . . . . . . . . . . . 16 $/\$
64	61, 62, 63	mp2an 426	. . . . . . . . . . . . . . 15
65	2	adantr 276	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
66	65	ad2antrr 488	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
67	66, 56	ffvelcdmd 5673	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
68	64, 67	sselid 3168	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
69	60, 68	remulcld 8019	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
70	51, 55, 56, 69	fvmptd3 5630	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
71	50, 70	syldan 282	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
72	50, 69	syldan 282	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
73	65	adantr 276	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
74	73, 51	trilpolemclim 15263	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
75		nnuz 9595	. . . . . . . . . . . . 13
76	69	recnd 8017	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
77	70, 76	eqeltrd 2266	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
78	75, 47, 77	iserex 11382	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
79	74, 78	mpbid 147	. . . . . . . . . . 11 $/\$ $/\$ $/\$
80	45, 48, 71, 72, 79	isumrecl 11472	. . . . . . . . . 10 $/\$ $/\$ $/\$
81		1zzd 9311	. . . . . . . . . . . . 13 $/\$ $/\$
82	81, 23	fzfigd 10464	. . . . . . . . . . . 12 $/\$ $/\$
83	82	adantr 276	. . . . . . . . . . 11 $/\$ $/\$ $/\$
84	20	a1i 9	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
85		elfzelz 10057	. . . . . . . . . . . . . 14
86	85	adantl 277	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
87	84, 86	rpexpcld 10712	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
88	87	rprecred 9740	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
89	83, 88	fsumrecl 11444	. . . . . . . . . 10 $/\$ $/\$ $/\$
90	50, 60	syldan 282	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
91	50, 68	syldan 282	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
92	59	rpreccld 9739	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
93	50, 92	syldan 282	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
94	93	rpge0d 9732	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
95		0le0 9039	. . . . . . . . . . . . . 14
96		simpr 110	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
97	95, 96	breqtrrid 4056	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
98		0le1 8469	. . . . . . . . . . . . . 14
99		simpr 110	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
100	98, 99	breqtrrid 4056	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
101	73	adantr 276	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
102	101, 50	ffvelcdmd 5673	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
103		elpri 3630	. . . . . . . . . . . . . 14 $\/$
104	102, 103	syl 14	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $\/$
105	97, 100, 104	mpjaodan 799	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
106	90, 91, 94, 105	mulge0d 8609	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
107	45, 48, 71, 72, 79, 106	isumge0 11473	. . . . . . . . . 10 $/\$ $/\$ $/\$
108	44, 80, 89, 107	leadd2dd 8548	. . . . . . . . 9 $/\$ $/\$ $/\$
109	89	recnd 8017	. . . . . . . . . . 11 $/\$ $/\$ $/\$
110	109	addridd 8137	. . . . . . . . . 10 $/\$ $/\$ $/\$
111	110	eqcomd 2195	. . . . . . . . 9 $/\$ $/\$ $/\$
112	75, 45, 47, 70, 76, 74	isumsplit 11534	. . . . . . . . . . 11 $/\$ $/\$ $/\$
113	3, 112	eqtrid 2234	. . . . . . . . . 10 $/\$ $/\$ $/\$
114	46	nncnd 8964	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
115		1cnd 8004	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
116	114, 115	pncand 8300	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
117	116	oveq2d 5913	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
118		simpr 110	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
119	118	fvresd 5559	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
120		fveqeq2 5543	. . . . . . . . . . . . . . . 16
121		simplr 528	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
122	120, 121, 118	rspcdva 2861	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
123	119, 122	eqtr3d 2224	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
124	123	oveq2d 5913	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
125	87	rpreccld 9739	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
126	125	rpcnd 9730	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
127	126	mulridd 8005	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
128	124, 127	eqtrd 2222	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
129	117, 128	sumeq12rdv 11416	. . . . . . . . . . 11 $/\$ $/\$ $/\$
130	129	oveq1d 5912	. . . . . . . . . 10 $/\$ $/\$ $/\$
131	113, 130	eqtrd 2222	. . . . . . . . 9 $/\$ $/\$ $/\$
132	108, 111, 131	3brtr4d 4050	. . . . . . . 8 $/\$ $/\$ $/\$
133		geo2sum 11557	. . . . . . . . . 10 $/\$
134	133	breq1d 4028	. . . . . . . . 9 $/\$
135	46, 115, 134	syl2anc 411	. . . . . . . 8 $/\$ $/\$ $/\$
136	132, 135	mpbid 147	. . . . . . 7 $/\$ $/\$ $/\$
137	42, 41, 43, 136	subled 8536	. . . . . 6 $/\$ $/\$ $/\$
138	40, 41, 137	lensymd 8110	. . . . 5 $/\$ $/\$ $/\$
139	39, 138	pm2.21dd 621	. . . 4 $/\$ $/\$ $/\$
140	139	ex 115	. . 3 $/\$ $/\$
141		fveq1 5533	. . . . . . 7
142	141	eqeq1d 2198	. . . . . 6
143	142	rexbidv 2491	. . . . 5
144	141	eqeq1d 2198	. . . . . 6
145	144	ralbidv 2490	. . . . 5
146	143, 145	orbi12d 794	. . . 4 $\/$ $\/$
147		finomni 7169	. . . . . 6 Omni
148	82, 147	syl 14	. . . . 5 $/\$ $/\$ Omni
149		isomninn 15258	. . . . . 6 Omni Omni $\/$
150	148, 149	syl 14	. . . . 5 $/\$ $/\$ Omni $\/$
151	148, 150	mpbid 147	. . . 4 $/\$ $/\$ $\/$
152		fz1ssnn 10088	. . . . . . 7
153	152	a1i 9	. . . . . 6 $/\$ $/\$
154	65, 153	fssresd 5411	. . . . 5 $/\$ $/\$
155		0red 7989	. . . . . . 7 $/\$ $/\$
156		1red 8003	. . . . . . 7 $/\$ $/\$
157		prexg 4229	. . . . . . 7 $/\$
158	155, 156, 157	syl2anc 411	. . . . . 6 $/\$ $/\$
159	158, 82	elmapd 6689	. . . . 5 $/\$ $/\$
160	154, 159	mpbird 167	. . . 4 $/\$ $/\$
161	146, 151, 160	rspcdva 2861	. . 3 $/\$ $/\$ $\/$
162	19, 140, 161	mpjaod 719	. 2 $/\$ $/\$
163	10, 162	rexlimddv 2612	1

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wb 105 $\/$ wo 709

wceq 1364

wcel 2160

wral 2468

wrex 2469

cvv 2752

wss 3144

cpr 3608 class class class wbr 4018

cmpt 4079

cdm 4644

cres 4646

wf 5231

cfv 5235 (class class class)co 5897

cmap 6675

cfn 6767 Omnicomni 7163

cc 7840

cr 7841

cc0 7842

c1 7843

caddc 7845

cmul 7847

clt 8023

cle 8024

cmin 8159

cdiv 8660

cn 8950

c2 9001

cn0 9207

cz 9284

cuz 9559

crp 9685

cfz 10040

cseq 10478

cexp 10553

cli 11321

csu 11396

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 2162 ax-14 2163 ax-ext 2171 ax-coll 4133 ax-sep 4136 ax-nul 4144 ax-pow 4192 ax-pr 4227 ax-un 4451 ax-setind 4554 ax-iinf 4605 ax-cnex 7933 ax-resscn 7934 ax-1cn 7935 ax-1re 7936 ax-icn 7937 ax-addcl 7938 ax-addrcl 7939 ax-mulcl 7940 ax-mulrcl 7941 ax-addcom 7942 ax-mulcom 7943 ax-addass 7944 ax-mulass 7945 ax-distr 7946 ax-i2m1 7947 ax-0lt1 7948 ax-1rid 7949 ax-0id 7950 ax-rnegex 7951 ax-precex 7952 ax-cnre 7953 ax-pre-ltirr 7954 ax-pre-ltwlin 7955 ax-pre-lttrn 7956 ax-pre-apti 7957 ax-pre-ltadd 7958 ax-pre-mulgt0 7959 ax-pre-mulext 7960 ax-arch 7961 ax-caucvg 7962

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 2041 df-mo 2042 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-ne 2361 df-nel 2456 df-ral 2473 df-rex 2474 df-reu 2475 df-rmo 2476 df-rab 2477 df-v 2754 df-sbc 2978 df-csb 3073 df-dif 3146 df-un 3148 df-in 3150 df-ss 3157 df-nul 3438 df-if 3550 df-pw 3592 df-sn 3613 df-pr 3614 df-op 3616 df-uni 3825 df-int 3860 df-iun 3903 df-br 4019 df-opab 4080 df-mpt 4081 df-tr 4117 df-id 4311 df-po 4314 df-iso 4315 df-iord 4384 df-on 4386 df-ilim 4387 df-suc 4389 df-iom 4608 df-xp 4650 df-rel 4651 df-cnv 4652 df-co 4653 df-dm 4654 df-rn 4655 df-res 4656 df-ima 4657 df-iota 5196 df-fun 5237 df-fn 5238 df-f 5239 df-f1 5240 df-fo 5241 df-f1o 5242 df-fv 5243 df-isom 5244 df-riota 5852 df-ov 5900 df-oprab 5901 df-mpo 5902 df-1st 6166 df-2nd 6167 df-recs 6331 df-irdg 6396 df-frec 6417 df-1o 6442 df-2o 6443 df-oadd 6446 df-er 6560 df-map 6677 df-en 6768 df-dom 6769 df-fin 6770 df-omni 7164 df-pnf 8025 df-mnf 8026 df-xr 8027 df-ltxr 8028 df-le 8029 df-sub 8161 df-neg 8162 df-reap 8563 df-ap 8570 df-div 8661 df-inn 8951 df-2 9009 df-3 9010 df-4 9011 df-n0 9208 df-z 9285 df-uz 9560 df-q 9652 df-rp 9686 df-ico 9926 df-fz 10041 df-fzo 10175 df-seqfrec 10479 df-exp 10554 df-ihash 10791 df-cj 10886 df-re 10887 df-im 10888 df-rsqrt 11042 df-abs 11043 df-clim 11322 df-sumdc 11397

This theorem is referenced by: trilpolemres 15269 neapmkvlem 15294

W3C validator