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 13920

Description: Lemma for trilpo 13922. 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 7104 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 7914	. . . 4
2		trilpolemgt1.f	. . . . 5
3		trilpolemgt1.a	. . . . 5
4	2, 3	trilpolemcl 13916	. . . 4
5	1, 4	resubcld 8279	. . 3
6		trilpolemlt1.a	. . . 4
7	4, 1	posdifd 8430	. . . 4
8	6, 7	mpbid 146	. . 3
9		nnrecl 9112	. . 3 $/\$
10	5, 8, 9	syl2anc 409	. 2
11		elfznn 9989	. . . . . . 7
12	11	ad2antrl 482	. . . . . 6 $/\$ $/\$ $/\$ $/\$
13		simprl 521	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
14	13	fvresd 5511	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
15		simprr 522	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
16	14, 15	eqtr3d 2200	. . . . . 6 $/\$ $/\$ $/\$ $/\$
17	12, 16	jca 304	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
18	17	ex 114	. . . 4 $/\$ $/\$ $/\$ $/\$
19	18	reximdv2 2565	. . 3 $/\$ $/\$
20		2rp 9594	. . . . . . . . . 10
21	20	a1i 9	. . . . . . . . 9 $/\$ $/\$
22		simprl 521	. . . . . . . . . 10 $/\$ $/\$
23	22	nnzd 9312	. . . . . . . . 9 $/\$ $/\$
24	21, 23	rpexpcld 10612	. . . . . . . 8 $/\$ $/\$
25	24	rprecred 9644	. . . . . . 7 $/\$ $/\$
26	22	nnrecred 8904	. . . . . . 7 $/\$ $/\$
27	5	adantr 274	. . . . . . 7 $/\$ $/\$
28		2z 9219	. . . . . . . . . 10
29		uzid 9480	. . . . . . . . . 10
30	28, 29	mp1i 10	. . . . . . . . 9 $/\$ $/\$
31	22	nnnn0d 9167	. . . . . . . . 9 $/\$ $/\$
32		bernneq3 10577	. . . . . . . . 9 $/\$
33	30, 31, 32	syl2anc 409	. . . . . . . 8 $/\$ $/\$
34	22	nnrpd 9630	. . . . . . . . 9 $/\$ $/\$
35	34, 24	ltrecd 9651	. . . . . . . 8 $/\$ $/\$
36	33, 35	mpbid 146	. . . . . . 7 $/\$ $/\$
37		simprr 522	. . . . . . 7 $/\$ $/\$
38	25, 26, 27, 36, 37	lttrd 8024	. . . . . 6 $/\$ $/\$
39	38	adantr 274	. . . . 5 $/\$ $/\$ $/\$
40	27	adantr 274	. . . . . 6 $/\$ $/\$ $/\$
41	25	adantr 274	. . . . . 6 $/\$ $/\$ $/\$
42		1red 7914	. . . . . . 7 $/\$ $/\$ $/\$
43	4	ad2antrr 480	. . . . . . 7 $/\$ $/\$ $/\$
44		0red 7900	. . . . . . . . . 10 $/\$ $/\$ $/\$
45		eqid 2165	. . . . . . . . . . 11
46	22	adantr 274	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
47	46	peano2nnd 8872	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
48	47	nnzd 9312	. . . . . . . . . . 11 $/\$ $/\$ $/\$
49		eluznn 9538	. . . . . . . . . . . . 13 $/\$
50	47, 49	sylan 281	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
51		eqid 2165	. . . . . . . . . . . . 13
52		oveq2 5850	. . . . . . . . . . . . . . 15
53	52	oveq2d 5858	. . . . . . . . . . . . . 14
54		fveq2 5486	. . . . . . . . . . . . . 14
55	53, 54	oveq12d 5860	. . . . . . . . . . . . 13
56		simpr 109	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
57	20	a1i 9	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
58	56	nnzd 9312	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
59	57, 58	rpexpcld 10612	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
60	59	rprecred 9644	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
61		0re 7899	. . . . . . . . . . . . . . . 16
62		1re 7898	. . . . . . . . . . . . . . . 16
63		prssi 3731	. . . . . . . . . . . . . . . 16 $/\$
64	61, 62, 63	mp2an 423	. . . . . . . . . . . . . . 15
65	2	adantr 274	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
66	65	ad2antrr 480	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
67	66, 56	ffvelrnd 5621	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
68	64, 67	sselid 3140	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
69	60, 68	remulcld 7929	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
70	51, 55, 56, 69	fvmptd3 5579	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
71	50, 70	syldan 280	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
72	50, 69	syldan 280	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
73	65	adantr 274	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
74	73, 51	trilpolemclim 13915	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
75		nnuz 9501	. . . . . . . . . . . . 13
76	69	recnd 7927	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
77	70, 76	eqeltrd 2243	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
78	75, 47, 77	iserex 11280	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
79	74, 78	mpbid 146	. . . . . . . . . . 11 $/\$ $/\$ $/\$
80	45, 48, 71, 72, 79	isumrecl 11370	. . . . . . . . . 10 $/\$ $/\$ $/\$
81		1zzd 9218	. . . . . . . . . . . . 13 $/\$ $/\$
82	81, 23	fzfigd 10366	. . . . . . . . . . . 12 $/\$ $/\$
83	82	adantr 274	. . . . . . . . . . 11 $/\$ $/\$ $/\$
84	20	a1i 9	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
85		elfzelz 9960	. . . . . . . . . . . . . 14
86	85	adantl 275	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
87	84, 86	rpexpcld 10612	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
88	87	rprecred 9644	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
89	83, 88	fsumrecl 11342	. . . . . . . . . 10 $/\$ $/\$ $/\$
90	50, 60	syldan 280	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
91	50, 68	syldan 280	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
92	59	rpreccld 9643	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
93	50, 92	syldan 280	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
94	93	rpge0d 9636	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
95		0le0 8946	. . . . . . . . . . . . . 14
96		simpr 109	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
97	95, 96	breqtrrid 4020	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
98		0le1 8379	. . . . . . . . . . . . . 14
99		simpr 109	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
100	98, 99	breqtrrid 4020	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
101	73	adantr 274	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
102	101, 50	ffvelrnd 5621	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
103		elpri 3599	. . . . . . . . . . . . . 14 $\/$
104	102, 103	syl 14	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $\/$
105	97, 100, 104	mpjaodan 788	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
106	90, 91, 94, 105	mulge0d 8519	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
107	45, 48, 71, 72, 79, 106	isumge0 11371	. . . . . . . . . 10 $/\$ $/\$ $/\$
108	44, 80, 89, 107	leadd2dd 8458	. . . . . . . . 9 $/\$ $/\$ $/\$
109	89	recnd 7927	. . . . . . . . . . 11 $/\$ $/\$ $/\$
110	109	addid1d 8047	. . . . . . . . . 10 $/\$ $/\$ $/\$
111	110	eqcomd 2171	. . . . . . . . 9 $/\$ $/\$ $/\$
112	75, 45, 47, 70, 76, 74	isumsplit 11432	. . . . . . . . . . 11 $/\$ $/\$ $/\$
113	3, 112	syl5eq 2211	. . . . . . . . . 10 $/\$ $/\$ $/\$
114	46	nncnd 8871	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
115		1cnd 7915	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
116	114, 115	pncand 8210	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
117	116	oveq2d 5858	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
118		simpr 109	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
119	118	fvresd 5511	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
120		fveqeq2 5495	. . . . . . . . . . . . . . . 16
121		simplr 520	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
122	120, 121, 118	rspcdva 2835	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
123	119, 122	eqtr3d 2200	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
124	123	oveq2d 5858	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
125	87	rpreccld 9643	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
126	125	rpcnd 9634	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
127	126	mulid1d 7916	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
128	124, 127	eqtrd 2198	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
129	117, 128	sumeq12rdv 11314	. . . . . . . . . . 11 $/\$ $/\$ $/\$
130	129	oveq1d 5857	. . . . . . . . . 10 $/\$ $/\$ $/\$
131	113, 130	eqtrd 2198	. . . . . . . . 9 $/\$ $/\$ $/\$
132	108, 111, 131	3brtr4d 4014	. . . . . . . 8 $/\$ $/\$ $/\$
133		geo2sum 11455	. . . . . . . . . 10 $/\$
134	133	breq1d 3992	. . . . . . . . 9 $/\$
135	46, 115, 134	syl2anc 409	. . . . . . . 8 $/\$ $/\$ $/\$
136	132, 135	mpbid 146	. . . . . . 7 $/\$ $/\$ $/\$
137	42, 41, 43, 136	subled 8446	. . . . . 6 $/\$ $/\$ $/\$
138	40, 41, 137	lensymd 8020	. . . . 5 $/\$ $/\$ $/\$
139	39, 138	pm2.21dd 610	. . . 4 $/\$ $/\$ $/\$
140	139	ex 114	. . 3 $/\$ $/\$
141		fveq1 5485	. . . . . . 7
142	141	eqeq1d 2174	. . . . . 6
143	142	rexbidv 2467	. . . . 5
144	141	eqeq1d 2174	. . . . . 6
145	144	ralbidv 2466	. . . . 5
146	143, 145	orbi12d 783	. . . 4 $\/$ $\/$
147		finomni 7104	. . . . . 6 Omni
148	82, 147	syl 14	. . . . 5 $/\$ $/\$ Omni
149		isomninn 13910	. . . . . 6 Omni Omni $\/$
150	148, 149	syl 14	. . . . 5 $/\$ $/\$ Omni $\/$
151	148, 150	mpbid 146	. . . 4 $/\$ $/\$ $\/$
152		fz1ssnn 9991	. . . . . . 7
153	152	a1i 9	. . . . . 6 $/\$ $/\$
154	65, 153	fssresd 5364	. . . . 5 $/\$ $/\$
155		0red 7900	. . . . . . 7 $/\$ $/\$
156		1red 7914	. . . . . . 7 $/\$ $/\$
157		prexg 4189	. . . . . . 7 $/\$
158	155, 156, 157	syl2anc 409	. . . . . 6 $/\$ $/\$
159	158, 82	elmapd 6628	. . . . 5 $/\$ $/\$
160	154, 159	mpbird 166	. . . 4 $/\$ $/\$
161	146, 151, 160	rspcdva 2835	. . 3 $/\$ $/\$ $\/$
162	19, 140, 161	mpjaod 708	. 2 $/\$ $/\$
163	10, 162	rexlimddv 2588	1

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 103

wb 104 $\/$ wo 698

wceq 1343

wcel 2136

wral 2444

wrex 2445

cvv 2726

wss 3116

cpr 3577 class class class wbr 3982

cmpt 4043

cdm 4604

cres 4606

wf 5184

cfv 5188 (class class class)co 5842

cmap 6614

cfn 6706 Omnicomni 7098

cc 7751

cr 7752

cc0 7753

c1 7754

caddc 7756

cmul 7758

clt 7933

cle 7934

cmin 8069

cdiv 8568

cn 8857

c2 8908

cn0 9114

cz 9191

cuz 9466

crp 9589

cfz 9944

cseq 10380

cexp 10454

cli 11219

csu 11294

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1435 ax-7 1436 ax-gen 1437 ax-ie1 1481 ax-ie2 1482 ax-8 1492 ax-10 1493 ax-11 1494 ax-i12 1495 ax-bndl 1497 ax-4 1498 ax-17 1514 ax-i9 1518 ax-ial 1522 ax-i5r 1523 ax-13 2138 ax-14 2139 ax-ext 2147 ax-coll 4097 ax-sep 4100 ax-nul 4108 ax-pow 4153 ax-pr 4187 ax-un 4411 ax-setind 4514 ax-iinf 4565 ax-cnex 7844 ax-resscn 7845 ax-1cn 7846 ax-1re 7847 ax-icn 7848 ax-addcl 7849 ax-addrcl 7850 ax-mulcl 7851 ax-mulrcl 7852 ax-addcom 7853 ax-mulcom 7854 ax-addass 7855 ax-mulass 7856 ax-distr 7857 ax-i2m1 7858 ax-0lt1 7859 ax-1rid 7860 ax-0id 7861 ax-rnegex 7862 ax-precex 7863 ax-cnre 7864 ax-pre-ltirr 7865 ax-pre-ltwlin 7866 ax-pre-lttrn 7867 ax-pre-apti 7868 ax-pre-ltadd 7869 ax-pre-mulgt0 7870 ax-pre-mulext 7871 ax-arch 7872 ax-caucvg 7873

This theorem depends on definitions: df-bi 116 df-dc 825 df-3or 969 df-3an 970 df-tru 1346 df-fal 1349 df-nf 1449 df-sb 1751 df-eu 2017 df-mo 2018 df-clab 2152 df-cleq 2158 df-clel 2161 df-nfc 2297 df-ne 2337 df-nel 2432 df-ral 2449 df-rex 2450 df-reu 2451 df-rmo 2452 df-rab 2453 df-v 2728 df-sbc 2952 df-csb 3046 df-dif 3118 df-un 3120 df-in 3122 df-ss 3129 df-nul 3410 df-if 3521 df-pw 3561 df-sn 3582 df-pr 3583 df-op 3585 df-uni 3790 df-int 3825 df-iun 3868 df-br 3983 df-opab 4044 df-mpt 4045 df-tr 4081 df-id 4271 df-po 4274 df-iso 4275 df-iord 4344 df-on 4346 df-ilim 4347 df-suc 4349 df-iom 4568 df-xp 4610 df-rel 4611 df-cnv 4612 df-co 4613 df-dm 4614 df-rn 4615 df-res 4616 df-ima 4617 df-iota 5153 df-fun 5190 df-fn 5191 df-f 5192 df-f1 5193 df-fo 5194 df-f1o 5195 df-fv 5196 df-isom 5197 df-riota 5798 df-ov 5845 df-oprab 5846 df-mpo 5847 df-1st 6108 df-2nd 6109 df-recs 6273 df-irdg 6338 df-frec 6359 df-1o 6384 df-2o 6385 df-oadd 6388 df-er 6501 df-map 6616 df-en 6707 df-dom 6708 df-fin 6709 df-omni 7099 df-pnf 7935 df-mnf 7936 df-xr 7937 df-ltxr 7938 df-le 7939 df-sub 8071 df-neg 8072 df-reap 8473 df-ap 8480 df-div 8569 df-inn 8858 df-2 8916 df-3 8917 df-4 8918 df-n0 9115 df-z 9192 df-uz 9467 df-q 9558 df-rp 9590 df-ico 9830 df-fz 9945 df-fzo 10078 df-seqfrec 10381 df-exp 10455 df-ihash 10689 df-cj 10784 df-re 10785 df-im 10786 df-rsqrt 10940 df-abs 10941 df-clim 11220 df-sumdc 11295

This theorem is referenced by: trilpolemres 13921 neapmkvlem 13945

W3C validator