Mathbox for Jim Kingdon < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  trilpolemlt1 Unicode version

Theorem trilpolemlt1 13045
 Description: Lemma for trilpo 13047. 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 6978 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.
StepHypRef Expression
1 1red 7745 . . . 4
2 trilpolemgt1.f . . . . 5
3 trilpolemgt1.a . . . . 5
42, 3trilpolemcl 13041 . . . 4
51, 4resubcld 8107 . . 3
6 trilpolemlt1.a . . . 4
74, 1posdifd 8257 . . . 4
86, 7mpbid 146 . . 3
9 nnrecl 8926 . . 3
105, 8, 9syl2anc 406 . 2
11 elfznn 9774 . . . . . . 7
1211ad2antrl 479 . . . . . 6
13 simprl 503 . . . . . . . 8
1413fvresd 5412 . . . . . . 7
15 simprr 504 . . . . . . 7
1614, 15eqtr3d 2150 . . . . . 6
1712, 16jca 302 . . . . 5
1817ex 114 . . . 4
1918reximdv2 2506 . . 3
20 2rp 9395 . . . . . . . . . 10
2120a1i 9 . . . . . . . . 9
22 simprl 503 . . . . . . . . . 10
2322nnzd 9123 . . . . . . . . 9
2421, 23rpexpcld 10388 . . . . . . . 8
2524rprecred 9441 . . . . . . 7
2622nnrecred 8724 . . . . . . 7
275adantr 272 . . . . . . 7
28 2z 9033 . . . . . . . . . 10
29 uzid 9289 . . . . . . . . . 10
3028, 29mp1i 10 . . . . . . . . 9
3122nnnn0d 8981 . . . . . . . . 9
32 bernneq3 10354 . . . . . . . . 9
3330, 31, 32syl2anc 406 . . . . . . . 8
3422nnrpd 9428 . . . . . . . . 9
3534, 24ltrecd 9448 . . . . . . . 8
3633, 35mpbid 146 . . . . . . 7
37 simprr 504 . . . . . . 7
3825, 26, 27, 36, 37lttrd 7852 . . . . . 6
3938adantr 272 . . . . 5
4027adantr 272 . . . . . 6
4125adantr 272 . . . . . 6
42 1red 7745 . . . . . . 7
434ad2antrr 477 . . . . . . 7
44 0red 7731 . . . . . . . . . 10
45 eqid 2115 . . . . . . . . . . 11
4622adantr 272 . . . . . . . . . . . . 13
4746peano2nnd 8692 . . . . . . . . . . . 12
4847nnzd 9123 . . . . . . . . . . 11
49 eluznn 9343 . . . . . . . . . . . . 13
5047, 49sylan 279 . . . . . . . . . . . 12
51 eqid 2115 . . . . . . . . . . . . 13
52 oveq2 5748 . . . . . . . . . . . . . . 15
5352oveq2d 5756 . . . . . . . . . . . . . 14
54 fveq2 5387 . . . . . . . . . . . . . 14
5553, 54oveq12d 5758 . . . . . . . . . . . . 13
56 simpr 109 . . . . . . . . . . . . 13
5720a1i 9 . . . . . . . . . . . . . . . 16
5856nnzd 9123 . . . . . . . . . . . . . . . 16
5957, 58rpexpcld 10388 . . . . . . . . . . . . . . 15
6059rprecred 9441 . . . . . . . . . . . . . 14
61 0re 7730 . . . . . . . . . . . . . . . 16
62 1re 7729 . . . . . . . . . . . . . . . 16
63 prssi 3646 . . . . . . . . . . . . . . . 16
6461, 62, 63mp2an 420 . . . . . . . . . . . . . . 15
652adantr 272 . . . . . . . . . . . . . . . . 17
6665ad2antrr 477 . . . . . . . . . . . . . . . 16
6766, 56ffvelrnd 5522 . . . . . . . . . . . . . . 15
6864, 67sseldi 3063 . . . . . . . . . . . . . 14
6960, 68remulcld 7760 . . . . . . . . . . . . 13
7051, 55, 56, 69fvmptd3 5480 . . . . . . . . . . . 12
7150, 70syldan 278 . . . . . . . . . . 11
7250, 69syldan 278 . . . . . . . . . . 11
7365adantr 272 . . . . . . . . . . . . 13
7473, 51trilpolemclim 13040 . . . . . . . . . . . 12
75 nnuz 9310 . . . . . . . . . . . . 13
7669recnd 7758 . . . . . . . . . . . . . 14
7770, 76eqeltrd 2192 . . . . . . . . . . . . 13
7875, 47, 77iserex 11048 . . . . . . . . . . . 12
7974, 78mpbid 146 . . . . . . . . . . 11
8045, 48, 71, 72, 79isumrecl 11138 . . . . . . . . . 10
81 1zzd 9032 . . . . . . . . . . . . 13
8281, 23fzfigd 10144 . . . . . . . . . . . 12
8382adantr 272 . . . . . . . . . . 11
8420a1i 9 . . . . . . . . . . . . 13
85 elfzelz 9746 . . . . . . . . . . . . . 14
8685adantl 273 . . . . . . . . . . . . 13
8784, 86rpexpcld 10388 . . . . . . . . . . . 12
8887rprecred 9441 . . . . . . . . . . 11
8983, 88fsumrecl 11110 . . . . . . . . . 10
9050, 60syldan 278 . . . . . . . . . . . 12
9150, 68syldan 278 . . . . . . . . . . . 12
9259rpreccld 9440 . . . . . . . . . . . . . 14
9350, 92syldan 278 . . . . . . . . . . . . 13
9493rpge0d 9433 . . . . . . . . . . . 12
95 0le0 8766 . . . . . . . . . . . . . 14
96 simpr 109 . . . . . . . . . . . . . 14
9795, 96breqtrrid 3934 . . . . . . . . . . . . 13
98 0le1 8207 . . . . . . . . . . . . . 14
99 simpr 109 . . . . . . . . . . . . . 14
10098, 99breqtrrid 3934 . . . . . . . . . . . . 13
10173adantr 272 . . . . . . . . . . . . . . 15
102101, 50ffvelrnd 5522 . . . . . . . . . . . . . 14
103 elpri 3518 . . . . . . . . . . . . . 14
104102, 103syl 14 . . . . . . . . . . . . 13
10597, 100, 104mpjaodan 770 . . . . . . . . . . . 12
10690, 91, 94, 105mulge0d 8346 . . . . . . . . . . 11
10745, 48, 71, 72, 79, 106isumge0 11139 . . . . . . . . . 10
10844, 80, 89, 107leadd2dd 8285 . . . . . . . . 9
10989recnd 7758 . . . . . . . . . . 11
110109addid1d 7875 . . . . . . . . . 10
111110eqcomd 2121 . . . . . . . . 9
11275, 45, 47, 70, 76, 74isumsplit 11200 . . . . . . . . . . 11
1133, 112syl5eq 2160 . . . . . . . . . 10
11446nncnd 8691 . . . . . . . . . . . . . 14
115 1cnd 7746 . . . . . . . . . . . . . 14
116114, 115pncand 8038 . . . . . . . . . . . . 13
117116oveq2d 5756 . . . . . . . . . . . 12
118 simpr 109 . . . . . . . . . . . . . . . 16
119118fvresd 5412 . . . . . . . . . . . . . . 15
120 fveqeq2 5396 . . . . . . . . . . . . . . . 16
121 simplr 502 . . . . . . . . . . . . . . . 16
122120, 121, 118rspcdva 2766 . . . . . . . . . . . . . . 15
123119, 122eqtr3d 2150 . . . . . . . . . . . . . 14
124123oveq2d 5756 . . . . . . . . . . . . 13
12587rpreccld 9440 . . . . . . . . . . . . . . 15
126125rpcnd 9431 . . . . . . . . . . . . . 14
127126mulid1d 7747 . . . . . . . . . . . . 13
128124, 127eqtrd 2148 . . . . . . . . . . . 12
129117, 128sumeq12rdv 11082 . . . . . . . . . . 11
130129oveq1d 5755 . . . . . . . . . 10
131113, 130eqtrd 2148 . . . . . . . . 9
132108, 111, 1313brtr4d 3928 . . . . . . . 8
133 geo2sum 11223 . . . . . . . . . 10
134133breq1d 3907 . . . . . . . . 9
13546, 115, 134syl2anc 406 . . . . . . . 8
136132, 135mpbid 146 . . . . . . 7
13742, 41, 43, 136subled 8273 . . . . . 6
13840, 41, 137lensymd 7848 . . . . 5
13939, 138pm2.21dd 592 . . . 4
140139ex 114 . . 3
141 fveq1 5386 . . . . . . 7
142141eqeq1d 2124 . . . . . 6
143142rexbidv 2413 . . . . 5
144141eqeq1d 2124 . . . . . 6
145144ralbidv 2412 . . . . 5
146143, 145orbi12d 765 . . . 4
147 finomni 6978 . . . . . 6 Omni
14882, 147syl 14 . . . . 5 Omni
149 isomninn 13037 . . . . . 6 Omni Omni
150148, 149syl 14 . . . . 5 Omni
151148, 150mpbid 146 . . . 4
152 fz1ssnn 9776 . . . . . . 7
153152a1i 9 . . . . . 6
15465, 153fssresd 5267 . . . . 5
155 0red 7731 . . . . . . 7
156 1red 7745 . . . . . . 7
157 prexg 4101 . . . . . . 7
158155, 156, 157syl2anc 406 . . . . . 6
159158, 82elmapd 6522 . . . . 5
160154, 159mpbird 166 . . . 4
161146, 151, 160rspcdva 2766 . . 3
16219, 140, 161mpjaod 690 . 2
16310, 162rexlimddv 2529 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103   wb 104   wo 680   wceq 1314   wcel 1463  wral 2391  wrex 2392  cvv 2658   wss 3039  cpr 3496   class class class wbr 3897   cmpt 3957   cdm 4507   cres 4509  wf 5087  cfv 5091  (class class class)co 5740   cmap 6508  cfn 6600  Omnicomni 6970  cc 7582  cr 7583  cc0 7584  c1 7585   caddc 7587   cmul 7589   clt 7764   cle 7765   cmin 7897   cdiv 8392  cn 8677  c2 8728  cn0 8928  cz 9005  cuz 9275  crp 9390  cfz 9730   cseq 10158  cexp 10232   cli 10987  csu 11062 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 586  ax-in2 587  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-13 1474  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-coll 4011  ax-sep 4014  ax-nul 4022  ax-pow 4066  ax-pr 4099  ax-un 4323  ax-setind 4420  ax-iinf 4470  ax-cnex 7675  ax-resscn 7676  ax-1cn 7677  ax-1re 7678  ax-icn 7679  ax-addcl 7680  ax-addrcl 7681  ax-mulcl 7682  ax-mulrcl 7683  ax-addcom 7684  ax-mulcom 7685  ax-addass 7686  ax-mulass 7687  ax-distr 7688  ax-i2m1 7689  ax-0lt1 7690  ax-1rid 7691  ax-0id 7692  ax-rnegex 7693  ax-precex 7694  ax-cnre 7695  ax-pre-ltirr 7696  ax-pre-ltwlin 7697  ax-pre-lttrn 7698  ax-pre-apti 7699  ax-pre-ltadd 7700  ax-pre-mulgt0 7701  ax-pre-mulext 7702  ax-arch 7703  ax-caucvg 7704 This theorem depends on definitions:  df-bi 116  df-dc 803  df-3or 946  df-3an 947  df-tru 1317  df-fal 1320  df-nf 1420  df-sb 1719  df-eu 1978  df-mo 1979  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-ne 2284  df-nel 2379  df-ral 2396  df-rex 2397  df-reu 2398  df-rmo 2399  df-rab 2400  df-v 2660  df-sbc 2881  df-csb 2974  df-dif 3041  df-un 3043  df-in 3045  df-ss 3052  df-nul 3332  df-if 3443  df-pw 3480  df-sn 3501  df-pr 3502  df-op 3504  df-uni 3705  df-int 3740  df-iun 3783  df-br 3898  df-opab 3958  df-mpt 3959  df-tr 3995  df-id 4183  df-po 4186  df-iso 4187  df-iord 4256  df-on 4258  df-ilim 4259  df-suc 4261  df-iom 4473  df-xp 4513  df-rel 4514  df-cnv 4515  df-co 4516  df-dm 4517  df-rn 4518  df-res 4519  df-ima 4520  df-iota 5056  df-fun 5093  df-fn 5094  df-f 5095  df-f1 5096  df-fo 5097  df-f1o 5098  df-fv 5099  df-isom 5100  df-riota 5696  df-ov 5743  df-oprab 5744  df-mpo 5745  df-1st 6004  df-2nd 6005  df-recs 6168  df-irdg 6233  df-frec 6254  df-1o 6279  df-2o 6280  df-oadd 6283  df-er 6395  df-map 6510  df-en 6601  df-dom 6602  df-fin 6603  df-omni 6972  df-pnf 7766  df-mnf 7767  df-xr 7768  df-ltxr 7769  df-le 7770  df-sub 7899  df-neg 7900  df-reap 8300  df-ap 8307  df-div 8393  df-inn 8678  df-2 8736  df-3 8737  df-4 8738  df-n0 8929  df-z 9006  df-uz 9276  df-q 9361  df-rp 9391  df-ico 9617  df-fz 9731  df-fzo 9860  df-seqfrec 10159  df-exp 10233  df-ihash 10462  df-cj 10554  df-re 10555  df-im 10556  df-rsqrt 10710  df-abs 10711  df-clim 10988  df-sumdc 11063 This theorem is referenced by:  trilpolemres  13046
 Copyright terms: Public domain W3C validator