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 15942

Description: Lemma for trilpo 15944. 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 7241 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 8086	. . . 4
2		trilpolemgt1.f	. . . . 5
3		trilpolemgt1.a	. . . . 5
4	2, 3	trilpolemcl 15938	. . . 4
5	1, 4	resubcld 8452	. . 3
6		trilpolemlt1.a	. . . 4
7	4, 1	posdifd 8604	. . . 4
8	6, 7	mpbid 147	. . 3
9		nnrecl 9292	. . 3 $/\$
10	5, 8, 9	syl2anc 411	. 2
11		elfznn 10175	. . . . . . 7
12	11	ad2antrl 490	. . . . . 6 $/\$ $/\$ $/\$ $/\$
13		simprl 529	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
14	13	fvresd 5600	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
15		simprr 531	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
16	14, 15	eqtr3d 2239	. . . . . 6 $/\$ $/\$ $/\$ $/\$
17	12, 16	jca 306	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
18	17	ex 115	. . . 4 $/\$ $/\$ $/\$ $/\$
19	18	reximdv2 2604	. . 3 $/\$ $/\$
20		2rp 9779	. . . . . . . . . 10
21	20	a1i 9	. . . . . . . . 9 $/\$ $/\$
22		simprl 529	. . . . . . . . . 10 $/\$ $/\$
23	22	nnzd 9493	. . . . . . . . 9 $/\$ $/\$
24	21, 23	rpexpcld 10840	. . . . . . . 8 $/\$ $/\$
25	24	rprecred 9829	. . . . . . 7 $/\$ $/\$
26	22	nnrecred 9082	. . . . . . 7 $/\$ $/\$
27	5	adantr 276	. . . . . . 7 $/\$ $/\$
28		2z 9399	. . . . . . . . . 10
29		uzid 9661	. . . . . . . . . 10
30	28, 29	mp1i 10	. . . . . . . . 9 $/\$ $/\$
31	22	nnnn0d 9347	. . . . . . . . 9 $/\$ $/\$
32		bernneq3 10805	. . . . . . . . 9 $/\$
33	30, 31, 32	syl2anc 411	. . . . . . . 8 $/\$ $/\$
34	22	nnrpd 9815	. . . . . . . . 9 $/\$ $/\$
35	34, 24	ltrecd 9836	. . . . . . . 8 $/\$ $/\$
36	33, 35	mpbid 147	. . . . . . 7 $/\$ $/\$
37		simprr 531	. . . . . . 7 $/\$ $/\$
38	25, 26, 27, 36, 37	lttrd 8197	. . . . . 6 $/\$ $/\$
39	38	adantr 276	. . . . 5 $/\$ $/\$ $/\$
40	27	adantr 276	. . . . . 6 $/\$ $/\$ $/\$
41	25	adantr 276	. . . . . 6 $/\$ $/\$ $/\$
42		1red 8086	. . . . . . 7 $/\$ $/\$ $/\$
43	4	ad2antrr 488	. . . . . . 7 $/\$ $/\$ $/\$
44		0red 8072	. . . . . . . . . 10 $/\$ $/\$ $/\$
45		eqid 2204	. . . . . . . . . . 11
46	22	adantr 276	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
47	46	peano2nnd 9050	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
48	47	nnzd 9493	. . . . . . . . . . 11 $/\$ $/\$ $/\$
49		eluznn 9720	. . . . . . . . . . . . 13 $/\$
50	47, 49	sylan 283	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
51		eqid 2204	. . . . . . . . . . . . 13
52		oveq2 5951	. . . . . . . . . . . . . . 15
53	52	oveq2d 5959	. . . . . . . . . . . . . 14
54		fveq2 5575	. . . . . . . . . . . . . 14
55	53, 54	oveq12d 5961	. . . . . . . . . . . . 13
56		simpr 110	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
57	20	a1i 9	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
58	56	nnzd 9493	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
59	57, 58	rpexpcld 10840	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
60	59	rprecred 9829	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
61		0re 8071	. . . . . . . . . . . . . . . 16
62		1re 8070	. . . . . . . . . . . . . . . 16
63		prssi 3790	. . . . . . . . . . . . . . . 16 $/\$
64	61, 62, 63	mp2an 426	. . . . . . . . . . . . . . 15
65	2	adantr 276	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
66	65	ad2antrr 488	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
67	66, 56	ffvelcdmd 5715	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
68	64, 67	sselid 3190	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
69	60, 68	remulcld 8102	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
70	51, 55, 56, 69	fvmptd3 5672	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
71	50, 70	syldan 282	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
72	50, 69	syldan 282	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
73	65	adantr 276	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
74	73, 51	trilpolemclim 15937	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
75		nnuz 9683	. . . . . . . . . . . . 13
76	69	recnd 8100	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
77	70, 76	eqeltrd 2281	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
78	75, 47, 77	iserex 11621	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
79	74, 78	mpbid 147	. . . . . . . . . . 11 $/\$ $/\$ $/\$
80	45, 48, 71, 72, 79	isumrecl 11711	. . . . . . . . . 10 $/\$ $/\$ $/\$
81		1zzd 9398	. . . . . . . . . . . . 13 $/\$ $/\$
82	81, 23	fzfigd 10574	. . . . . . . . . . . 12 $/\$ $/\$
83	82	adantr 276	. . . . . . . . . . 11 $/\$ $/\$ $/\$
84	20	a1i 9	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
85		elfzelz 10146	. . . . . . . . . . . . . 14
86	85	adantl 277	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
87	84, 86	rpexpcld 10840	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
88	87	rprecred 9829	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
89	83, 88	fsumrecl 11683	. . . . . . . . . 10 $/\$ $/\$ $/\$
90	50, 60	syldan 282	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
91	50, 68	syldan 282	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
92	59	rpreccld 9828	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
93	50, 92	syldan 282	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
94	93	rpge0d 9821	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
95		0le0 9124	. . . . . . . . . . . . . 14
96		simpr 110	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
97	95, 96	breqtrrid 4081	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
98		0le1 8553	. . . . . . . . . . . . . 14
99		simpr 110	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
100	98, 99	breqtrrid 4081	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
101	73	adantr 276	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
102	101, 50	ffvelcdmd 5715	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
103		elpri 3655	. . . . . . . . . . . . . 14 $\/$
104	102, 103	syl 14	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $\/$
105	97, 100, 104	mpjaodan 799	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
106	90, 91, 94, 105	mulge0d 8693	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
107	45, 48, 71, 72, 79, 106	isumge0 11712	. . . . . . . . . 10 $/\$ $/\$ $/\$
108	44, 80, 89, 107	leadd2dd 8632	. . . . . . . . 9 $/\$ $/\$ $/\$
109	89	recnd 8100	. . . . . . . . . . 11 $/\$ $/\$ $/\$
110	109	addridd 8220	. . . . . . . . . 10 $/\$ $/\$ $/\$
111	110	eqcomd 2210	. . . . . . . . 9 $/\$ $/\$ $/\$
112	75, 45, 47, 70, 76, 74	isumsplit 11773	. . . . . . . . . . 11 $/\$ $/\$ $/\$
113	3, 112	eqtrid 2249	. . . . . . . . . 10 $/\$ $/\$ $/\$
114	46	nncnd 9049	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
115		1cnd 8087	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
116	114, 115	pncand 8383	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
117	116	oveq2d 5959	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
118		simpr 110	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
119	118	fvresd 5600	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
120		fveqeq2 5584	. . . . . . . . . . . . . . . 16
121		simplr 528	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
122	120, 121, 118	rspcdva 2881	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
123	119, 122	eqtr3d 2239	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
124	123	oveq2d 5959	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
125	87	rpreccld 9828	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
126	125	rpcnd 9819	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
127	126	mulridd 8088	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
128	124, 127	eqtrd 2237	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
129	117, 128	sumeq12rdv 11655	. . . . . . . . . . 11 $/\$ $/\$ $/\$
130	129	oveq1d 5958	. . . . . . . . . 10 $/\$ $/\$ $/\$
131	113, 130	eqtrd 2237	. . . . . . . . 9 $/\$ $/\$ $/\$
132	108, 111, 131	3brtr4d 4075	. . . . . . . 8 $/\$ $/\$ $/\$
133		geo2sum 11796	. . . . . . . . . 10 $/\$
134	133	breq1d 4053	. . . . . . . . 9 $/\$
135	46, 115, 134	syl2anc 411	. . . . . . . 8 $/\$ $/\$ $/\$
136	132, 135	mpbid 147	. . . . . . 7 $/\$ $/\$ $/\$
137	42, 41, 43, 136	subled 8620	. . . . . 6 $/\$ $/\$ $/\$
138	40, 41, 137	lensymd 8193	. . . . 5 $/\$ $/\$ $/\$
139	39, 138	pm2.21dd 621	. . . 4 $/\$ $/\$ $/\$
140	139	ex 115	. . 3 $/\$ $/\$
141		fveq1 5574	. . . . . . 7
142	141	eqeq1d 2213	. . . . . 6
143	142	rexbidv 2506	. . . . 5
144	141	eqeq1d 2213	. . . . . 6
145	144	ralbidv 2505	. . . . 5
146	143, 145	orbi12d 794	. . . 4 $\/$ $\/$
147		finomni 7241	. . . . . 6 Omni
148	82, 147	syl 14	. . . . 5 $/\$ $/\$ Omni
149		isomninn 15932	. . . . . 6 Omni Omni $\/$
150	148, 149	syl 14	. . . . 5 $/\$ $/\$ Omni $\/$
151	148, 150	mpbid 147	. . . 4 $/\$ $/\$ $\/$
152		fz1ssnn 10177	. . . . . . 7
153	152	a1i 9	. . . . . 6 $/\$ $/\$
154	65, 153	fssresd 5451	. . . . 5 $/\$ $/\$
155		0red 8072	. . . . . . 7 $/\$ $/\$
156		1red 8086	. . . . . . 7 $/\$ $/\$
157		prexg 4254	. . . . . . 7 $/\$
158	155, 156, 157	syl2anc 411	. . . . . 6 $/\$ $/\$
159	158, 82	elmapd 6748	. . . . 5 $/\$ $/\$
160	154, 159	mpbird 167	. . . 4 $/\$ $/\$
161	146, 151, 160	rspcdva 2881	. . 3 $/\$ $/\$ $\/$
162	19, 140, 161	mpjaod 719	. 2 $/\$ $/\$
163	10, 162	rexlimddv 2627	1

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wb 105 $\/$ wo 709

wceq 1372

wcel 2175

wral 2483

wrex 2484

cvv 2771

wss 3165

cpr 3633 class class class wbr 4043

cmpt 4104

cdm 4674

cres 4676

wf 5266

cfv 5270 (class class class)co 5943

cmap 6734

cfn 6826 Omnicomni 7235

cc 7922

cr 7923

cc0 7924

c1 7925

caddc 7927

cmul 7929

clt 8106

cle 8107

cmin 8242

cdiv 8744

cn 9035

c2 9086

cn0 9294

cz 9371

cuz 9647

crp 9774

cfz 10129

cseq 10590

cexp 10681

cli 11560

csu 11635

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 1469 ax-7 1470 ax-gen 1471 ax-ie1 1515 ax-ie2 1516 ax-8 1526 ax-10 1527 ax-11 1528 ax-i12 1529 ax-bndl 1531 ax-4 1532 ax-17 1548 ax-i9 1552 ax-ial 1556 ax-i5r 1557 ax-13 2177 ax-14 2178 ax-ext 2186 ax-coll 4158 ax-sep 4161 ax-nul 4169 ax-pow 4217 ax-pr 4252 ax-un 4479 ax-setind 4584 ax-iinf 4635 ax-cnex 8015 ax-resscn 8016 ax-1cn 8017 ax-1re 8018 ax-icn 8019 ax-addcl 8020 ax-addrcl 8021 ax-mulcl 8022 ax-mulrcl 8023 ax-addcom 8024 ax-mulcom 8025 ax-addass 8026 ax-mulass 8027 ax-distr 8028 ax-i2m1 8029 ax-0lt1 8030 ax-1rid 8031 ax-0id 8032 ax-rnegex 8033 ax-precex 8034 ax-cnre 8035 ax-pre-ltirr 8036 ax-pre-ltwlin 8037 ax-pre-lttrn 8038 ax-pre-apti 8039 ax-pre-ltadd 8040 ax-pre-mulgt0 8041 ax-pre-mulext 8042 ax-arch 8043 ax-caucvg 8044

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 981 df-3an 982 df-tru 1375 df-fal 1378 df-nf 1483 df-sb 1785 df-eu 2056 df-mo 2057 df-clab 2191 df-cleq 2197 df-clel 2200 df-nfc 2336 df-ne 2376 df-nel 2471 df-ral 2488 df-rex 2489 df-reu 2490 df-rmo 2491 df-rab 2492 df-v 2773 df-sbc 2998 df-csb 3093 df-dif 3167 df-un 3169 df-in 3171 df-ss 3178 df-nul 3460 df-if 3571 df-pw 3617 df-sn 3638 df-pr 3639 df-op 3641 df-uni 3850 df-int 3885 df-iun 3928 df-br 4044 df-opab 4105 df-mpt 4106 df-tr 4142 df-id 4339 df-po 4342 df-iso 4343 df-iord 4412 df-on 4414 df-ilim 4415 df-suc 4417 df-iom 4638 df-xp 4680 df-rel 4681 df-cnv 4682 df-co 4683 df-dm 4684 df-rn 4685 df-res 4686 df-ima 4687 df-iota 5231 df-fun 5272 df-fn 5273 df-f 5274 df-f1 5275 df-fo 5276 df-f1o 5277 df-fv 5278 df-isom 5279 df-riota 5898 df-ov 5946 df-oprab 5947 df-mpo 5948 df-1st 6225 df-2nd 6226 df-recs 6390 df-irdg 6455 df-frec 6476 df-1o 6501 df-2o 6502 df-oadd 6505 df-er 6619 df-map 6736 df-en 6827 df-dom 6828 df-fin 6829 df-omni 7236 df-pnf 8108 df-mnf 8109 df-xr 8110 df-ltxr 8111 df-le 8112 df-sub 8244 df-neg 8245 df-reap 8647 df-ap 8654 df-div 8745 df-inn 9036 df-2 9094 df-3 9095 df-4 9096 df-n0 9295 df-z 9372 df-uz 9648 df-q 9740 df-rp 9775 df-ico 10015 df-fz 10130 df-fzo 10264 df-seqfrec 10591 df-exp 10682 df-ihash 10919 df-cj 11124 df-re 11125 df-im 11126 df-rsqrt 11280 df-abs 11281 df-clim 11561 df-sumdc 11636

This theorem is referenced by: trilpolemres 15943 neapmkvlem 15968

W3C validator