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 13409

Description: Lemma for trilpo 13411. 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 7020 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 7805	. . . 4
2		trilpolemgt1.f	. . . . 5
3		trilpolemgt1.a	. . . . 5
4	2, 3	trilpolemcl 13405	. . . 4
5	1, 4	resubcld 8167	. . 3
6		trilpolemlt1.a	. . . 4
7	4, 1	posdifd 8318	. . . 4
8	6, 7	mpbid 146	. . 3
9		nnrecl 8999	. . 3 $/\$
10	5, 8, 9	syl2anc 409	. 2
11		elfznn 9865	. . . . . . 7
12	11	ad2antrl 482	. . . . . 6 $/\$ $/\$ $/\$ $/\$
13		simprl 521	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
14	13	fvresd 5454	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
15		simprr 522	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
16	14, 15	eqtr3d 2175	. . . . . 6 $/\$ $/\$ $/\$ $/\$
17	12, 16	jca 304	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
18	17	ex 114	. . . 4 $/\$ $/\$ $/\$ $/\$
19	18	reximdv2 2534	. . 3 $/\$ $/\$
20		2rp 9475	. . . . . . . . . 10
21	20	a1i 9	. . . . . . . . 9 $/\$ $/\$
22		simprl 521	. . . . . . . . . 10 $/\$ $/\$
23	22	nnzd 9196	. . . . . . . . 9 $/\$ $/\$
24	21, 23	rpexpcld 10479	. . . . . . . 8 $/\$ $/\$
25	24	rprecred 9525	. . . . . . 7 $/\$ $/\$
26	22	nnrecred 8791	. . . . . . 7 $/\$ $/\$
27	5	adantr 274	. . . . . . 7 $/\$ $/\$
28		2z 9106	. . . . . . . . . 10
29		uzid 9364	. . . . . . . . . 10
30	28, 29	mp1i 10	. . . . . . . . 9 $/\$ $/\$
31	22	nnnn0d 9054	. . . . . . . . 9 $/\$ $/\$
32		bernneq3 10445	. . . . . . . . 9 $/\$
33	30, 31, 32	syl2anc 409	. . . . . . . 8 $/\$ $/\$
34	22	nnrpd 9511	. . . . . . . . 9 $/\$ $/\$
35	34, 24	ltrecd 9532	. . . . . . . 8 $/\$ $/\$
36	33, 35	mpbid 146	. . . . . . 7 $/\$ $/\$
37		simprr 522	. . . . . . 7 $/\$ $/\$
38	25, 26, 27, 36, 37	lttrd 7912	. . . . . 6 $/\$ $/\$
39	38	adantr 274	. . . . 5 $/\$ $/\$ $/\$
40	27	adantr 274	. . . . . 6 $/\$ $/\$ $/\$
41	25	adantr 274	. . . . . 6 $/\$ $/\$ $/\$
42		1red 7805	. . . . . . 7 $/\$ $/\$ $/\$
43	4	ad2antrr 480	. . . . . . 7 $/\$ $/\$ $/\$
44		0red 7791	. . . . . . . . . 10 $/\$ $/\$ $/\$
45		eqid 2140	. . . . . . . . . . 11
46	22	adantr 274	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
47	46	peano2nnd 8759	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
48	47	nnzd 9196	. . . . . . . . . . 11 $/\$ $/\$ $/\$
49		eluznn 9421	. . . . . . . . . . . . 13 $/\$
50	47, 49	sylan 281	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
51		eqid 2140	. . . . . . . . . . . . 13
52		oveq2 5790	. . . . . . . . . . . . . . 15
53	52	oveq2d 5798	. . . . . . . . . . . . . 14
54		fveq2 5429	. . . . . . . . . . . . . 14
55	53, 54	oveq12d 5800	. . . . . . . . . . . . 13
56		simpr 109	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
57	20	a1i 9	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
58	56	nnzd 9196	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
59	57, 58	rpexpcld 10479	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
60	59	rprecred 9525	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
61		0re 7790	. . . . . . . . . . . . . . . 16
62		1re 7789	. . . . . . . . . . . . . . . 16
63		prssi 3686	. . . . . . . . . . . . . . . 16 $/\$
64	61, 62, 63	mp2an 423	. . . . . . . . . . . . . . 15
65	2	adantr 274	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
66	65	ad2antrr 480	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
67	66, 56	ffvelrnd 5564	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
68	64, 67	sseldi 3100	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
69	60, 68	remulcld 7820	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
70	51, 55, 56, 69	fvmptd3 5522	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
71	50, 70	syldan 280	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
72	50, 69	syldan 280	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
73	65	adantr 274	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
74	73, 51	trilpolemclim 13404	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
75		nnuz 9385	. . . . . . . . . . . . 13
76	69	recnd 7818	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
77	70, 76	eqeltrd 2217	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
78	75, 47, 77	iserex 11140	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
79	74, 78	mpbid 146	. . . . . . . . . . 11 $/\$ $/\$ $/\$
80	45, 48, 71, 72, 79	isumrecl 11230	. . . . . . . . . 10 $/\$ $/\$ $/\$
81		1zzd 9105	. . . . . . . . . . . . 13 $/\$ $/\$
82	81, 23	fzfigd 10235	. . . . . . . . . . . 12 $/\$ $/\$
83	82	adantr 274	. . . . . . . . . . 11 $/\$ $/\$ $/\$
84	20	a1i 9	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
85		elfzelz 9837	. . . . . . . . . . . . . 14
86	85	adantl 275	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
87	84, 86	rpexpcld 10479	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
88	87	rprecred 9525	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
89	83, 88	fsumrecl 11202	. . . . . . . . . 10 $/\$ $/\$ $/\$
90	50, 60	syldan 280	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
91	50, 68	syldan 280	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
92	59	rpreccld 9524	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
93	50, 92	syldan 280	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
94	93	rpge0d 9517	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
95		0le0 8833	. . . . . . . . . . . . . 14
96		simpr 109	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
97	95, 96	breqtrrid 3974	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
98		0le1 8267	. . . . . . . . . . . . . 14
99		simpr 109	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
100	98, 99	breqtrrid 3974	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
101	73	adantr 274	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
102	101, 50	ffvelrnd 5564	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
103		elpri 3555	. . . . . . . . . . . . . 14 $\/$
104	102, 103	syl 14	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $\/$
105	97, 100, 104	mpjaodan 788	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
106	90, 91, 94, 105	mulge0d 8407	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
107	45, 48, 71, 72, 79, 106	isumge0 11231	. . . . . . . . . 10 $/\$ $/\$ $/\$
108	44, 80, 89, 107	leadd2dd 8346	. . . . . . . . 9 $/\$ $/\$ $/\$
109	89	recnd 7818	. . . . . . . . . . 11 $/\$ $/\$ $/\$
110	109	addid1d 7935	. . . . . . . . . 10 $/\$ $/\$ $/\$
111	110	eqcomd 2146	. . . . . . . . 9 $/\$ $/\$ $/\$
112	75, 45, 47, 70, 76, 74	isumsplit 11292	. . . . . . . . . . 11 $/\$ $/\$ $/\$
113	3, 112	syl5eq 2185	. . . . . . . . . 10 $/\$ $/\$ $/\$
114	46	nncnd 8758	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
115		1cnd 7806	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
116	114, 115	pncand 8098	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
117	116	oveq2d 5798	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
118		simpr 109	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
119	118	fvresd 5454	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
120		fveqeq2 5438	. . . . . . . . . . . . . . . 16
121		simplr 520	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
122	120, 121, 118	rspcdva 2798	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
123	119, 122	eqtr3d 2175	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
124	123	oveq2d 5798	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
125	87	rpreccld 9524	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
126	125	rpcnd 9515	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
127	126	mulid1d 7807	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
128	124, 127	eqtrd 2173	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
129	117, 128	sumeq12rdv 11174	. . . . . . . . . . 11 $/\$ $/\$ $/\$
130	129	oveq1d 5797	. . . . . . . . . 10 $/\$ $/\$ $/\$
131	113, 130	eqtrd 2173	. . . . . . . . 9 $/\$ $/\$ $/\$
132	108, 111, 131	3brtr4d 3968	. . . . . . . 8 $/\$ $/\$ $/\$
133		geo2sum 11315	. . . . . . . . . 10 $/\$
134	133	breq1d 3947	. . . . . . . . 9 $/\$
135	46, 115, 134	syl2anc 409	. . . . . . . 8 $/\$ $/\$ $/\$
136	132, 135	mpbid 146	. . . . . . 7 $/\$ $/\$ $/\$
137	42, 41, 43, 136	subled 8334	. . . . . 6 $/\$ $/\$ $/\$
138	40, 41, 137	lensymd 7908	. . . . 5 $/\$ $/\$ $/\$
139	39, 138	pm2.21dd 610	. . . 4 $/\$ $/\$ $/\$
140	139	ex 114	. . 3 $/\$ $/\$
141		fveq1 5428	. . . . . . 7
142	141	eqeq1d 2149	. . . . . 6
143	142	rexbidv 2439	. . . . 5
144	141	eqeq1d 2149	. . . . . 6
145	144	ralbidv 2438	. . . . 5
146	143, 145	orbi12d 783	. . . 4 $\/$ $\/$
147		finomni 7020	. . . . . 6 Omni
148	82, 147	syl 14	. . . . 5 $/\$ $/\$ Omni
149		isomninn 13401	. . . . . 6 Omni Omni $\/$
150	148, 149	syl 14	. . . . 5 $/\$ $/\$ Omni $\/$
151	148, 150	mpbid 146	. . . 4 $/\$ $/\$ $\/$
152		fz1ssnn 9867	. . . . . . 7
153	152	a1i 9	. . . . . 6 $/\$ $/\$
154	65, 153	fssresd 5307	. . . . 5 $/\$ $/\$
155		0red 7791	. . . . . . 7 $/\$ $/\$
156		1red 7805	. . . . . . 7 $/\$ $/\$
157		prexg 4141	. . . . . . 7 $/\$
158	155, 156, 157	syl2anc 409	. . . . . 6 $/\$ $/\$
159	158, 82	elmapd 6564	. . . . 5 $/\$ $/\$
160	154, 159	mpbird 166	. . . 4 $/\$ $/\$
161	146, 151, 160	rspcdva 2798	. . 3 $/\$ $/\$ $\/$
162	19, 140, 161	mpjaod 708	. 2 $/\$ $/\$
163	10, 162	rexlimddv 2557	1

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 103

wb 104 $\/$ wo 698

wceq 1332

wcel 1481

wral 2417

wrex 2418

cvv 2689

wss 3076

cpr 3533 class class class wbr 3937

cmpt 3997

cdm 4547

cres 4549

wf 5127

cfv 5131 (class class class)co 5782

cmap 6550

cfn 6642 Omnicomni 7012

cc 7642

cr 7643

cc0 7644

c1 7645

caddc 7647

cmul 7649

clt 7824

cle 7825

cmin 7957

cdiv 8456

cn 8744

c2 8795

cn0 9001

cz 9078

cuz 9350

crp 9470

cfz 9821

cseq 10249

cexp 10323

cli 11079

csu 11154

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 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-10 1484 ax-11 1485 ax-i12 1486 ax-bndl 1487 ax-4 1488 ax-13 1492 ax-14 1493 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 ax-coll 4051 ax-sep 4054 ax-nul 4062 ax-pow 4106 ax-pr 4139 ax-un 4363 ax-setind 4460 ax-iinf 4510 ax-cnex 7735 ax-resscn 7736 ax-1cn 7737 ax-1re 7738 ax-icn 7739 ax-addcl 7740 ax-addrcl 7741 ax-mulcl 7742 ax-mulrcl 7743 ax-addcom 7744 ax-mulcom 7745 ax-addass 7746 ax-mulass 7747 ax-distr 7748 ax-i2m1 7749 ax-0lt1 7750 ax-1rid 7751 ax-0id 7752 ax-rnegex 7753 ax-precex 7754 ax-cnre 7755 ax-pre-ltirr 7756 ax-pre-ltwlin 7757 ax-pre-lttrn 7758 ax-pre-apti 7759 ax-pre-ltadd 7760 ax-pre-mulgt0 7761 ax-pre-mulext 7762 ax-arch 7763 ax-caucvg 7764

This theorem depends on definitions: df-bi 116 df-dc 821 df-3or 964 df-3an 965 df-tru 1335 df-fal 1338 df-nf 1438 df-sb 1737 df-eu 2003 df-mo 2004 df-clab 2127 df-cleq 2133 df-clel 2136 df-nfc 2271 df-ne 2310 df-nel 2405 df-ral 2422 df-rex 2423 df-reu 2424 df-rmo 2425 df-rab 2426 df-v 2691 df-sbc 2914 df-csb 3008 df-dif 3078 df-un 3080 df-in 3082 df-ss 3089 df-nul 3369 df-if 3480 df-pw 3517 df-sn 3538 df-pr 3539 df-op 3541 df-uni 3745 df-int 3780 df-iun 3823 df-br 3938 df-opab 3998 df-mpt 3999 df-tr 4035 df-id 4223 df-po 4226 df-iso 4227 df-iord 4296 df-on 4298 df-ilim 4299 df-suc 4301 df-iom 4513 df-xp 4553 df-rel 4554 df-cnv 4555 df-co 4556 df-dm 4557 df-rn 4558 df-res 4559 df-ima 4560 df-iota 5096 df-fun 5133 df-fn 5134 df-f 5135 df-f1 5136 df-fo 5137 df-f1o 5138 df-fv 5139 df-isom 5140 df-riota 5738 df-ov 5785 df-oprab 5786 df-mpo 5787 df-1st 6046 df-2nd 6047 df-recs 6210 df-irdg 6275 df-frec 6296 df-1o 6321 df-2o 6322 df-oadd 6325 df-er 6437 df-map 6552 df-en 6643 df-dom 6644 df-fin 6645 df-omni 7014 df-pnf 7826 df-mnf 7827 df-xr 7828 df-ltxr 7829 df-le 7830 df-sub 7959 df-neg 7960 df-reap 8361 df-ap 8368 df-div 8457 df-inn 8745 df-2 8803 df-3 8804 df-4 8805 df-n0 9002 df-z 9079 df-uz 9351 df-q 9439 df-rp 9471 df-ico 9707 df-fz 9822 df-fzo 9951 df-seqfrec 10250 df-exp 10324 df-ihash 10554 df-cj 10646 df-re 10647 df-im 10648 df-rsqrt 10802 df-abs 10803 df-clim 11080 df-sumdc 11155

This theorem is referenced by: trilpolemres 13410 neapmkvlem 13424

W3C validator