MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ntrivcvgfvn0 Structured version   Visualization version   GIF version

Theorem ntrivcvgfvn0 15114
Description: Any value of a product sequence that converges to a nonzero value is itself nonzero. (Contributed by Scott Fenton, 20-Dec-2017.)
Hypotheses
Ref Expression
ntrivcvgfvn0.1 𝑍 = (ℤ𝑀)
ntrivcvgfvn0.2 (𝜑𝑁𝑍)
ntrivcvgfvn0.3 (𝜑 → seq𝑀( · , 𝐹) ⇝ 𝑋)
ntrivcvgfvn0.4 (𝜑𝑋 ≠ 0)
ntrivcvgfvn0.5 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)
Assertion
Ref Expression
ntrivcvgfvn0 (𝜑 → (seq𝑀( · , 𝐹)‘𝑁) ≠ 0)
Distinct variable groups:   𝑘,𝐹   𝜑,𝑘   𝑘,𝑀   𝑘,𝑁   𝑘,𝑍
Allowed substitution hint:   𝑋(𝑘)

Proof of Theorem ntrivcvgfvn0
Dummy variables 𝑚 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ntrivcvgfvn0.4 . 2 (𝜑𝑋 ≠ 0)
2 fclim 14770 . . . . . . . 8 ⇝ :dom ⇝ ⟶ℂ
3 ffun 6345 . . . . . . . 8 ( ⇝ :dom ⇝ ⟶ℂ → Fun ⇝ )
42, 3ax-mp 5 . . . . . . 7 Fun ⇝
5 ntrivcvgfvn0.3 . . . . . . 7 (𝜑 → seq𝑀( · , 𝐹) ⇝ 𝑋)
6 funbrfv 6544 . . . . . . 7 (Fun ⇝ → (seq𝑀( · , 𝐹) ⇝ 𝑋 → ( ⇝ ‘seq𝑀( · , 𝐹)) = 𝑋))
74, 5, 6mpsyl 68 . . . . . 6 (𝜑 → ( ⇝ ‘seq𝑀( · , 𝐹)) = 𝑋)
87adantr 473 . . . . 5 ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → ( ⇝ ‘seq𝑀( · , 𝐹)) = 𝑋)
9 eqid 2773 . . . . . . 7 (ℤ𝑁) = (ℤ𝑁)
10 ntrivcvgfvn0.1 . . . . . . . . . 10 𝑍 = (ℤ𝑀)
11 uzssz 12077 . . . . . . . . . 10 (ℤ𝑀) ⊆ ℤ
1210, 11eqsstri 3886 . . . . . . . . 9 𝑍 ⊆ ℤ
13 ntrivcvgfvn0.2 . . . . . . . . 9 (𝜑𝑁𝑍)
1412, 13sseldi 3851 . . . . . . . 8 (𝜑𝑁 ∈ ℤ)
1514adantr 473 . . . . . . 7 ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → 𝑁 ∈ ℤ)
16 seqex 13185 . . . . . . . 8 seq𝑀( · , 𝐹) ∈ V
1716a1i 11 . . . . . . 7 ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → seq𝑀( · , 𝐹) ∈ V)
18 0cnd 10431 . . . . . . 7 ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → 0 ∈ ℂ)
19 fveqeq2 6506 . . . . . . . . . 10 (𝑚 = 𝑁 → ((seq𝑀( · , 𝐹)‘𝑚) = 0 ↔ (seq𝑀( · , 𝐹)‘𝑁) = 0))
2019imbi2d 333 . . . . . . . . 9 (𝑚 = 𝑁 → (((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → (seq𝑀( · , 𝐹)‘𝑚) = 0) ↔ ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → (seq𝑀( · , 𝐹)‘𝑁) = 0)))
21 fveqeq2 6506 . . . . . . . . . 10 (𝑚 = 𝑛 → ((seq𝑀( · , 𝐹)‘𝑚) = 0 ↔ (seq𝑀( · , 𝐹)‘𝑛) = 0))
2221imbi2d 333 . . . . . . . . 9 (𝑚 = 𝑛 → (((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → (seq𝑀( · , 𝐹)‘𝑚) = 0) ↔ ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → (seq𝑀( · , 𝐹)‘𝑛) = 0)))
23 fveqeq2 6506 . . . . . . . . . 10 (𝑚 = (𝑛 + 1) → ((seq𝑀( · , 𝐹)‘𝑚) = 0 ↔ (seq𝑀( · , 𝐹)‘(𝑛 + 1)) = 0))
2423imbi2d 333 . . . . . . . . 9 (𝑚 = (𝑛 + 1) → (((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → (seq𝑀( · , 𝐹)‘𝑚) = 0) ↔ ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → (seq𝑀( · , 𝐹)‘(𝑛 + 1)) = 0)))
25 fveqeq2 6506 . . . . . . . . . 10 (𝑚 = 𝑘 → ((seq𝑀( · , 𝐹)‘𝑚) = 0 ↔ (seq𝑀( · , 𝐹)‘𝑘) = 0))
2625imbi2d 333 . . . . . . . . 9 (𝑚 = 𝑘 → (((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → (seq𝑀( · , 𝐹)‘𝑚) = 0) ↔ ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → (seq𝑀( · , 𝐹)‘𝑘) = 0)))
27 simpr 477 . . . . . . . . 9 ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → (seq𝑀( · , 𝐹)‘𝑁) = 0)
2813, 10syl6eleq 2871 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ (ℤ𝑀))
29 uztrn 12074 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (ℤ𝑁) ∧ 𝑁 ∈ (ℤ𝑀)) → 𝑛 ∈ (ℤ𝑀))
3028, 29sylan2 584 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (ℤ𝑁) ∧ 𝜑) → 𝑛 ∈ (ℤ𝑀))
31303adant3 1113 . . . . . . . . . . . . . 14 ((𝑛 ∈ (ℤ𝑁) ∧ 𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑛) = 0) → 𝑛 ∈ (ℤ𝑀))
32 seqp1 13198 . . . . . . . . . . . . . 14 (𝑛 ∈ (ℤ𝑀) → (seq𝑀( · , 𝐹)‘(𝑛 + 1)) = ((seq𝑀( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1))))
3331, 32syl 17 . . . . . . . . . . . . 13 ((𝑛 ∈ (ℤ𝑁) ∧ 𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑛) = 0) → (seq𝑀( · , 𝐹)‘(𝑛 + 1)) = ((seq𝑀( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1))))
34 oveq1 6982 . . . . . . . . . . . . . 14 ((seq𝑀( · , 𝐹)‘𝑛) = 0 → ((seq𝑀( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1))) = (0 · (𝐹‘(𝑛 + 1))))
35343ad2ant3 1116 . . . . . . . . . . . . 13 ((𝑛 ∈ (ℤ𝑁) ∧ 𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑛) = 0) → ((seq𝑀( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1))) = (0 · (𝐹‘(𝑛 + 1))))
36 peano2uz 12114 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (ℤ𝑁) → (𝑛 + 1) ∈ (ℤ𝑁))
3710uztrn2 12075 . . . . . . . . . . . . . . . . . 18 ((𝑁𝑍 ∧ (𝑛 + 1) ∈ (ℤ𝑁)) → (𝑛 + 1) ∈ 𝑍)
3813, 36, 37syl2an 587 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ (ℤ𝑁)) → (𝑛 + 1) ∈ 𝑍)
39 ntrivcvgfvn0.5 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)
4039ralrimiva 3127 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∀𝑘𝑍 (𝐹𝑘) ∈ ℂ)
41 fveq2 6497 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = (𝑛 + 1) → (𝐹𝑘) = (𝐹‘(𝑛 + 1)))
4241eleq1d 2845 . . . . . . . . . . . . . . . . . . 19 (𝑘 = (𝑛 + 1) → ((𝐹𝑘) ∈ ℂ ↔ (𝐹‘(𝑛 + 1)) ∈ ℂ))
4342rspcv 3526 . . . . . . . . . . . . . . . . . 18 ((𝑛 + 1) ∈ 𝑍 → (∀𝑘𝑍 (𝐹𝑘) ∈ ℂ → (𝐹‘(𝑛 + 1)) ∈ ℂ))
4440, 43mpan9 499 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑛 + 1) ∈ 𝑍) → (𝐹‘(𝑛 + 1)) ∈ ℂ)
4538, 44syldan 583 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (ℤ𝑁)) → (𝐹‘(𝑛 + 1)) ∈ ℂ)
4645ancoms 451 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (ℤ𝑁) ∧ 𝜑) → (𝐹‘(𝑛 + 1)) ∈ ℂ)
4746mul02d 10637 . . . . . . . . . . . . . 14 ((𝑛 ∈ (ℤ𝑁) ∧ 𝜑) → (0 · (𝐹‘(𝑛 + 1))) = 0)
48473adant3 1113 . . . . . . . . . . . . 13 ((𝑛 ∈ (ℤ𝑁) ∧ 𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑛) = 0) → (0 · (𝐹‘(𝑛 + 1))) = 0)
4933, 35, 483eqtrd 2813 . . . . . . . . . . . 12 ((𝑛 ∈ (ℤ𝑁) ∧ 𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑛) = 0) → (seq𝑀( · , 𝐹)‘(𝑛 + 1)) = 0)
50493exp 1100 . . . . . . . . . . 11 (𝑛 ∈ (ℤ𝑁) → (𝜑 → ((seq𝑀( · , 𝐹)‘𝑛) = 0 → (seq𝑀( · , 𝐹)‘(𝑛 + 1)) = 0)))
5150adantrd 484 . . . . . . . . . 10 (𝑛 ∈ (ℤ𝑁) → ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → ((seq𝑀( · , 𝐹)‘𝑛) = 0 → (seq𝑀( · , 𝐹)‘(𝑛 + 1)) = 0)))
5251a2d 29 . . . . . . . . 9 (𝑛 ∈ (ℤ𝑁) → (((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → (seq𝑀( · , 𝐹)‘𝑛) = 0) → ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → (seq𝑀( · , 𝐹)‘(𝑛 + 1)) = 0)))
5320, 22, 24, 26, 27, 52uzind4i 12123 . . . . . . . 8 (𝑘 ∈ (ℤ𝑁) → ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → (seq𝑀( · , 𝐹)‘𝑘) = 0))
5453impcom 399 . . . . . . 7 (((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) ∧ 𝑘 ∈ (ℤ𝑁)) → (seq𝑀( · , 𝐹)‘𝑘) = 0)
559, 15, 17, 18, 54climconst 14760 . . . . . 6 ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → seq𝑀( · , 𝐹) ⇝ 0)
56 funbrfv 6544 . . . . . 6 (Fun ⇝ → (seq𝑀( · , 𝐹) ⇝ 0 → ( ⇝ ‘seq𝑀( · , 𝐹)) = 0))
574, 55, 56mpsyl 68 . . . . 5 ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → ( ⇝ ‘seq𝑀( · , 𝐹)) = 0)
588, 57eqtr3d 2811 . . . 4 ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → 𝑋 = 0)
5958ex 405 . . 3 (𝜑 → ((seq𝑀( · , 𝐹)‘𝑁) = 0 → 𝑋 = 0))
6059necon3d 2983 . 2 (𝜑 → (𝑋 ≠ 0 → (seq𝑀( · , 𝐹)‘𝑁) ≠ 0))
611, 60mpd 15 1 (𝜑 → (seq𝑀( · , 𝐹)‘𝑁) ≠ 0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 387  w3a 1069   = wceq 1508  wcel 2051  wne 2962  wral 3083  Vcvv 3410   class class class wbr 4926  dom cdm 5404  Fun wfun 6180  wf 6182  cfv 6186  (class class class)co 6975  cc 10332  0cc0 10334  1c1 10335   + caddc 10337   · cmul 10339  cz 11792  cuz 12057  seqcseq 13183  cli 14701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2745  ax-rep 5046  ax-sep 5057  ax-nul 5064  ax-pow 5116  ax-pr 5183  ax-un 7278  ax-inf2 8897  ax-cnex 10390  ax-resscn 10391  ax-1cn 10392  ax-icn 10393  ax-addcl 10394  ax-addrcl 10395  ax-mulcl 10396  ax-mulrcl 10397  ax-mulcom 10398  ax-addass 10399  ax-mulass 10400  ax-distr 10401  ax-i2m1 10402  ax-1ne0 10403  ax-1rid 10404  ax-rnegex 10405  ax-rrecex 10406  ax-cnre 10407  ax-pre-lttri 10408  ax-pre-lttrn 10409  ax-pre-ltadd 10410  ax-pre-mulgt0 10411  ax-pre-sup 10412
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-ne 2963  df-nel 3069  df-ral 3088  df-rex 3089  df-reu 3090  df-rmo 3091  df-rab 3092  df-v 3412  df-sbc 3677  df-csb 3782  df-dif 3827  df-un 3829  df-in 3831  df-ss 3838  df-pss 3840  df-nul 4174  df-if 4346  df-pw 4419  df-sn 4437  df-pr 4439  df-tp 4441  df-op 4443  df-uni 4710  df-iun 4791  df-br 4927  df-opab 4989  df-mpt 5006  df-tr 5028  df-id 5309  df-eprel 5314  df-po 5323  df-so 5324  df-fr 5363  df-we 5365  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-pred 5984  df-ord 6030  df-on 6031  df-lim 6032  df-suc 6033  df-iota 6150  df-fun 6188  df-fn 6189  df-f 6190  df-f1 6191  df-fo 6192  df-f1o 6193  df-fv 6194  df-riota 6936  df-ov 6978  df-oprab 6979  df-mpo 6980  df-om 7396  df-2nd 7501  df-wrecs 7749  df-recs 7811  df-rdg 7849  df-er 8088  df-en 8306  df-dom 8307  df-sdom 8308  df-sup 8700  df-pnf 10475  df-mnf 10476  df-xr 10477  df-ltxr 10478  df-le 10479  df-sub 10671  df-neg 10672  df-div 11098  df-nn 11439  df-2 11502  df-3 11503  df-n0 11707  df-z 11793  df-uz 12058  df-rp 12204  df-seq 13184  df-exp 13244  df-cj 14318  df-re 14319  df-im 14320  df-sqrt 14454  df-abs 14455  df-clim 14705
This theorem is referenced by:  ntrivcvgtail  15115
  Copyright terms: Public domain W3C validator