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 13234

Description: Lemma for trilpo 13236. 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 7012 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 7781	. . . 4
2		trilpolemgt1.f	. . . . 5
3		trilpolemgt1.a	. . . . 5
4	2, 3	trilpolemcl 13230	. . . 4
5	1, 4	resubcld 8143	. . 3
6		trilpolemlt1.a	. . . 4
7	4, 1	posdifd 8294	. . . 4
8	6, 7	mpbid 146	. . 3
9		nnrecl 8975	. . 3 $/\$
10	5, 8, 9	syl2anc 408	. 2
11		elfznn 9834	. . . . . . 7
12	11	ad2antrl 481	. . . . . 6 $/\$ $/\$ $/\$ $/\$
13		simprl 520	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
14	13	fvresd 5446	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
15		simprr 521	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
16	14, 15	eqtr3d 2174	. . . . . 6 $/\$ $/\$ $/\$ $/\$
17	12, 16	jca 304	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
18	17	ex 114	. . . 4 $/\$ $/\$ $/\$ $/\$
19	18	reximdv2 2531	. . 3 $/\$ $/\$
20		2rp 9446	. . . . . . . . . 10
21	20	a1i 9	. . . . . . . . 9 $/\$ $/\$
22		simprl 520	. . . . . . . . . 10 $/\$ $/\$
23	22	nnzd 9172	. . . . . . . . 9 $/\$ $/\$
24	21, 23	rpexpcld 10448	. . . . . . . 8 $/\$ $/\$
25	24	rprecred 9495	. . . . . . 7 $/\$ $/\$
26	22	nnrecred 8767	. . . . . . 7 $/\$ $/\$
27	5	adantr 274	. . . . . . 7 $/\$ $/\$
28		2z 9082	. . . . . . . . . 10
29		uzid 9340	. . . . . . . . . 10
30	28, 29	mp1i 10	. . . . . . . . 9 $/\$ $/\$
31	22	nnnn0d 9030	. . . . . . . . 9 $/\$ $/\$
32		bernneq3 10414	. . . . . . . . 9 $/\$
33	30, 31, 32	syl2anc 408	. . . . . . . 8 $/\$ $/\$
34	22	nnrpd 9482	. . . . . . . . 9 $/\$ $/\$
35	34, 24	ltrecd 9502	. . . . . . . 8 $/\$ $/\$
36	33, 35	mpbid 146	. . . . . . 7 $/\$ $/\$
37		simprr 521	. . . . . . 7 $/\$ $/\$
38	25, 26, 27, 36, 37	lttrd 7888	. . . . . 6 $/\$ $/\$
39	38	adantr 274	. . . . 5 $/\$ $/\$ $/\$
40	27	adantr 274	. . . . . 6 $/\$ $/\$ $/\$
41	25	adantr 274	. . . . . 6 $/\$ $/\$ $/\$
42		1red 7781	. . . . . . 7 $/\$ $/\$ $/\$
43	4	ad2antrr 479	. . . . . . 7 $/\$ $/\$ $/\$
44		0red 7767	. . . . . . . . . 10 $/\$ $/\$ $/\$
45		eqid 2139	. . . . . . . . . . 11
46	22	adantr 274	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
47	46	peano2nnd 8735	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
48	47	nnzd 9172	. . . . . . . . . . 11 $/\$ $/\$ $/\$
49		eluznn 9394	. . . . . . . . . . . . 13 $/\$
50	47, 49	sylan 281	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
51		eqid 2139	. . . . . . . . . . . . 13
52		oveq2 5782	. . . . . . . . . . . . . . 15
53	52	oveq2d 5790	. . . . . . . . . . . . . 14
54		fveq2 5421	. . . . . . . . . . . . . 14
55	53, 54	oveq12d 5792	. . . . . . . . . . . . 13
56		simpr 109	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
57	20	a1i 9	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
58	56	nnzd 9172	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
59	57, 58	rpexpcld 10448	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
60	59	rprecred 9495	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
61		0re 7766	. . . . . . . . . . . . . . . 16
62		1re 7765	. . . . . . . . . . . . . . . 16
63		prssi 3678	. . . . . . . . . . . . . . . 16 $/\$
64	61, 62, 63	mp2an 422	. . . . . . . . . . . . . . 15
65	2	adantr 274	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
66	65	ad2antrr 479	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
67	66, 56	ffvelrnd 5556	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
68	64, 67	sseldi 3095	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
69	60, 68	remulcld 7796	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
70	51, 55, 56, 69	fvmptd3 5514	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
71	50, 70	syldan 280	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
72	50, 69	syldan 280	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
73	65	adantr 274	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
74	73, 51	trilpolemclim 13229	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
75		nnuz 9361	. . . . . . . . . . . . 13
76	69	recnd 7794	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
77	70, 76	eqeltrd 2216	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
78	75, 47, 77	iserex 11108	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
79	74, 78	mpbid 146	. . . . . . . . . . 11 $/\$ $/\$ $/\$
80	45, 48, 71, 72, 79	isumrecl 11198	. . . . . . . . . 10 $/\$ $/\$ $/\$
81		1zzd 9081	. . . . . . . . . . . . 13 $/\$ $/\$
82	81, 23	fzfigd 10204	. . . . . . . . . . . 12 $/\$ $/\$
83	82	adantr 274	. . . . . . . . . . 11 $/\$ $/\$ $/\$
84	20	a1i 9	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
85		elfzelz 9806	. . . . . . . . . . . . . 14
86	85	adantl 275	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
87	84, 86	rpexpcld 10448	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
88	87	rprecred 9495	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
89	83, 88	fsumrecl 11170	. . . . . . . . . 10 $/\$ $/\$ $/\$
90	50, 60	syldan 280	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
91	50, 68	syldan 280	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
92	59	rpreccld 9494	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
93	50, 92	syldan 280	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
94	93	rpge0d 9487	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
95		0le0 8809	. . . . . . . . . . . . . 14
96		simpr 109	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
97	95, 96	breqtrrid 3966	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
98		0le1 8243	. . . . . . . . . . . . . 14
99		simpr 109	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
100	98, 99	breqtrrid 3966	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
101	73	adantr 274	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
102	101, 50	ffvelrnd 5556	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
103		elpri 3550	. . . . . . . . . . . . . 14 $\/$
104	102, 103	syl 14	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $\/$
105	97, 100, 104	mpjaodan 787	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
106	90, 91, 94, 105	mulge0d 8383	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
107	45, 48, 71, 72, 79, 106	isumge0 11199	. . . . . . . . . 10 $/\$ $/\$ $/\$
108	44, 80, 89, 107	leadd2dd 8322	. . . . . . . . 9 $/\$ $/\$ $/\$
109	89	recnd 7794	. . . . . . . . . . 11 $/\$ $/\$ $/\$
110	109	addid1d 7911	. . . . . . . . . 10 $/\$ $/\$ $/\$
111	110	eqcomd 2145	. . . . . . . . 9 $/\$ $/\$ $/\$
112	75, 45, 47, 70, 76, 74	isumsplit 11260	. . . . . . . . . . 11 $/\$ $/\$ $/\$
113	3, 112	syl5eq 2184	. . . . . . . . . 10 $/\$ $/\$ $/\$
114	46	nncnd 8734	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
115		1cnd 7782	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
116	114, 115	pncand 8074	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
117	116	oveq2d 5790	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
118		simpr 109	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
119	118	fvresd 5446	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
120		fveqeq2 5430	. . . . . . . . . . . . . . . 16
121		simplr 519	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
122	120, 121, 118	rspcdva 2794	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
123	119, 122	eqtr3d 2174	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
124	123	oveq2d 5790	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
125	87	rpreccld 9494	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
126	125	rpcnd 9485	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
127	126	mulid1d 7783	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
128	124, 127	eqtrd 2172	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
129	117, 128	sumeq12rdv 11142	. . . . . . . . . . 11 $/\$ $/\$ $/\$
130	129	oveq1d 5789	. . . . . . . . . 10 $/\$ $/\$ $/\$
131	113, 130	eqtrd 2172	. . . . . . . . 9 $/\$ $/\$ $/\$
132	108, 111, 131	3brtr4d 3960	. . . . . . . 8 $/\$ $/\$ $/\$
133		geo2sum 11283	. . . . . . . . . 10 $/\$
134	133	breq1d 3939	. . . . . . . . 9 $/\$
135	46, 115, 134	syl2anc 408	. . . . . . . 8 $/\$ $/\$ $/\$
136	132, 135	mpbid 146	. . . . . . 7 $/\$ $/\$ $/\$
137	42, 41, 43, 136	subled 8310	. . . . . 6 $/\$ $/\$ $/\$
138	40, 41, 137	lensymd 7884	. . . . 5 $/\$ $/\$ $/\$
139	39, 138	pm2.21dd 609	. . . 4 $/\$ $/\$ $/\$
140	139	ex 114	. . 3 $/\$ $/\$
141		fveq1 5420	. . . . . . 7
142	141	eqeq1d 2148	. . . . . 6
143	142	rexbidv 2438	. . . . 5
144	141	eqeq1d 2148	. . . . . 6
145	144	ralbidv 2437	. . . . 5
146	143, 145	orbi12d 782	. . . 4 $\/$ $\/$
147		finomni 7012	. . . . . 6 Omni
148	82, 147	syl 14	. . . . 5 $/\$ $/\$ Omni
149		isomninn 13226	. . . . . 6 Omni Omni $\/$
150	148, 149	syl 14	. . . . 5 $/\$ $/\$ Omni $\/$
151	148, 150	mpbid 146	. . . 4 $/\$ $/\$ $\/$
152		fz1ssnn 9836	. . . . . . 7
153	152	a1i 9	. . . . . 6 $/\$ $/\$
154	65, 153	fssresd 5299	. . . . 5 $/\$ $/\$
155		0red 7767	. . . . . . 7 $/\$ $/\$
156		1red 7781	. . . . . . 7 $/\$ $/\$
157		prexg 4133	. . . . . . 7 $/\$
158	155, 156, 157	syl2anc 408	. . . . . 6 $/\$ $/\$
159	158, 82	elmapd 6556	. . . . 5 $/\$ $/\$
160	154, 159	mpbird 166	. . . 4 $/\$ $/\$
161	146, 151, 160	rspcdva 2794	. . 3 $/\$ $/\$ $\/$
162	19, 140, 161	mpjaod 707	. 2 $/\$ $/\$
163	10, 162	rexlimddv 2554	1

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 103

wb 104 $\/$ wo 697

wceq 1331

wcel 1480

wral 2416

wrex 2417

cvv 2686

wss 3071

cpr 3528 class class class wbr 3929

cmpt 3989

cdm 4539

cres 4541

wf 5119

cfv 5123 (class class class)co 5774

cmap 6542

cfn 6634 Omnicomni 7004

cc 7618

cr 7619

cc0 7620

c1 7621

caddc 7623

cmul 7625

clt 7800

cle 7801

cmin 7933

cdiv 8432

cn 8720

c2 8771

cn0 8977

cz 9054

cuz 9326

crp 9441

cfz 9790

cseq 10218

cexp 10292

cli 11047

csu 11122

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 603 ax-in2 604 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-13 1491 ax-14 1492 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 ax-coll 4043 ax-sep 4046 ax-nul 4054 ax-pow 4098 ax-pr 4131 ax-un 4355 ax-setind 4452 ax-iinf 4502 ax-cnex 7711 ax-resscn 7712 ax-1cn 7713 ax-1re 7714 ax-icn 7715 ax-addcl 7716 ax-addrcl 7717 ax-mulcl 7718 ax-mulrcl 7719 ax-addcom 7720 ax-mulcom 7721 ax-addass 7722 ax-mulass 7723 ax-distr 7724 ax-i2m1 7725 ax-0lt1 7726 ax-1rid 7727 ax-0id 7728 ax-rnegex 7729 ax-precex 7730 ax-cnre 7731 ax-pre-ltirr 7732 ax-pre-ltwlin 7733 ax-pre-lttrn 7734 ax-pre-apti 7735 ax-pre-ltadd 7736 ax-pre-mulgt0 7737 ax-pre-mulext 7738 ax-arch 7739 ax-caucvg 7740

This theorem depends on definitions: df-bi 116 df-dc 820 df-3or 963 df-3an 964 df-tru 1334 df-fal 1337 df-nf 1437 df-sb 1736 df-eu 2002 df-mo 2003 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-ne 2309 df-nel 2404 df-ral 2421 df-rex 2422 df-reu 2423 df-rmo 2424 df-rab 2425 df-v 2688 df-sbc 2910 df-csb 3004 df-dif 3073 df-un 3075 df-in 3077 df-ss 3084 df-nul 3364 df-if 3475 df-pw 3512 df-sn 3533 df-pr 3534 df-op 3536 df-uni 3737 df-int 3772 df-iun 3815 df-br 3930 df-opab 3990 df-mpt 3991 df-tr 4027 df-id 4215 df-po 4218 df-iso 4219 df-iord 4288 df-on 4290 df-ilim 4291 df-suc 4293 df-iom 4505 df-xp 4545 df-rel 4546 df-cnv 4547 df-co 4548 df-dm 4549 df-rn 4550 df-res 4551 df-ima 4552 df-iota 5088 df-fun 5125 df-fn 5126 df-f 5127 df-f1 5128 df-fo 5129 df-f1o 5130 df-fv 5131 df-isom 5132 df-riota 5730 df-ov 5777 df-oprab 5778 df-mpo 5779 df-1st 6038 df-2nd 6039 df-recs 6202 df-irdg 6267 df-frec 6288 df-1o 6313 df-2o 6314 df-oadd 6317 df-er 6429 df-map 6544 df-en 6635 df-dom 6636 df-fin 6637 df-omni 7006 df-pnf 7802 df-mnf 7803 df-xr 7804 df-ltxr 7805 df-le 7806 df-sub 7935 df-neg 7936 df-reap 8337 df-ap 8344 df-div 8433 df-inn 8721 df-2 8779 df-3 8780 df-4 8781 df-n0 8978 df-z 9055 df-uz 9327 df-q 9412 df-rp 9442 df-ico 9677 df-fz 9791 df-fzo 9920 df-seqfrec 10219 df-exp 10293 df-ihash 10522 df-cj 10614 df-re 10615 df-im 10616 df-rsqrt 10770 df-abs 10771 df-clim 11048 df-sumdc 11123

This theorem is referenced by: trilpolemres 13235

W3C validator