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

Theorem ntrivcvgfvn0 15683
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 15334 . . . . . . . 8 ⇝ :dom ⇝ ⟶ℂ
3 ffun 6640 . . . . . . . 8 ( ⇝ :dom ⇝ ⟶ℂ → Fun ⇝ )
42, 3ax-mp 5 . . . . . . 7 Fun ⇝
5 ntrivcvgfvn0.3 . . . . . . 7 (𝜑 → seq𝑀( · , 𝐹) ⇝ 𝑋)
6 funbrfv 6859 . . . . . . 7 (Fun ⇝ → (seq𝑀( · , 𝐹) ⇝ 𝑋 → ( ⇝ ‘seq𝑀( · , 𝐹)) = 𝑋))
74, 5, 6mpsyl 68 . . . . . 6 (𝜑 → ( ⇝ ‘seq𝑀( · , 𝐹)) = 𝑋)
87adantr 481 . . . . 5 ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → ( ⇝ ‘seq𝑀( · , 𝐹)) = 𝑋)
9 eqid 2737 . . . . . . 7 (ℤ𝑁) = (ℤ𝑁)
10 ntrivcvgfvn0.1 . . . . . . . . . 10 𝑍 = (ℤ𝑀)
11 uzssz 12676 . . . . . . . . . 10 (ℤ𝑀) ⊆ ℤ
1210, 11eqsstri 3965 . . . . . . . . 9 𝑍 ⊆ ℤ
13 ntrivcvgfvn0.2 . . . . . . . . 9 (𝜑𝑁𝑍)
1412, 13sselid 3929 . . . . . . . 8 (𝜑𝑁 ∈ ℤ)
1514adantr 481 . . . . . . 7 ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → 𝑁 ∈ ℤ)
16 seqex 13796 . . . . . . . 8 seq𝑀( · , 𝐹) ∈ V
1716a1i 11 . . . . . . 7 ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → seq𝑀( · , 𝐹) ∈ V)
18 0cnd 11041 . . . . . . 7 ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → 0 ∈ ℂ)
19 fveqeq2 6820 . . . . . . . . . 10 (𝑚 = 𝑁 → ((seq𝑀( · , 𝐹)‘𝑚) = 0 ↔ (seq𝑀( · , 𝐹)‘𝑁) = 0))
2019imbi2d 340 . . . . . . . . 9 (𝑚 = 𝑁 → (((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → (seq𝑀( · , 𝐹)‘𝑚) = 0) ↔ ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → (seq𝑀( · , 𝐹)‘𝑁) = 0)))
21 fveqeq2 6820 . . . . . . . . . 10 (𝑚 = 𝑛 → ((seq𝑀( · , 𝐹)‘𝑚) = 0 ↔ (seq𝑀( · , 𝐹)‘𝑛) = 0))
2221imbi2d 340 . . . . . . . . 9 (𝑚 = 𝑛 → (((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → (seq𝑀( · , 𝐹)‘𝑚) = 0) ↔ ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → (seq𝑀( · , 𝐹)‘𝑛) = 0)))
23 fveqeq2 6820 . . . . . . . . . 10 (𝑚 = (𝑛 + 1) → ((seq𝑀( · , 𝐹)‘𝑚) = 0 ↔ (seq𝑀( · , 𝐹)‘(𝑛 + 1)) = 0))
2423imbi2d 340 . . . . . . . . 9 (𝑚 = (𝑛 + 1) → (((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → (seq𝑀( · , 𝐹)‘𝑚) = 0) ↔ ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → (seq𝑀( · , 𝐹)‘(𝑛 + 1)) = 0)))
25 fveqeq2 6820 . . . . . . . . . 10 (𝑚 = 𝑘 → ((seq𝑀( · , 𝐹)‘𝑚) = 0 ↔ (seq𝑀( · , 𝐹)‘𝑘) = 0))
2625imbi2d 340 . . . . . . . . 9 (𝑚 = 𝑘 → (((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → (seq𝑀( · , 𝐹)‘𝑚) = 0) ↔ ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → (seq𝑀( · , 𝐹)‘𝑘) = 0)))
27 simpr 485 . . . . . . . . 9 ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → (seq𝑀( · , 𝐹)‘𝑁) = 0)
2813, 10eleqtrdi 2848 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ (ℤ𝑀))
29 uztrn 12673 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (ℤ𝑁) ∧ 𝑁 ∈ (ℤ𝑀)) → 𝑛 ∈ (ℤ𝑀))
3028, 29sylan2 593 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (ℤ𝑁) ∧ 𝜑) → 𝑛 ∈ (ℤ𝑀))
31303adant3 1131 . . . . . . . . . . . . . 14 ((𝑛 ∈ (ℤ𝑁) ∧ 𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑛) = 0) → 𝑛 ∈ (ℤ𝑀))
32 seqp1 13809 . . . . . . . . . . . . . 14 (𝑛 ∈ (ℤ𝑀) → (seq𝑀( · , 𝐹)‘(𝑛 + 1)) = ((seq𝑀( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1))))
3331, 32syl 17 . . . . . . . . . . . . 13 ((𝑛 ∈ (ℤ𝑁) ∧ 𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑛) = 0) → (seq𝑀( · , 𝐹)‘(𝑛 + 1)) = ((seq𝑀( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1))))
34 oveq1 7322 . . . . . . . . . . . . . 14 ((seq𝑀( · , 𝐹)‘𝑛) = 0 → ((seq𝑀( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1))) = (0 · (𝐹‘(𝑛 + 1))))
35343ad2ant3 1134 . . . . . . . . . . . . 13 ((𝑛 ∈ (ℤ𝑁) ∧ 𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑛) = 0) → ((seq𝑀( · , 𝐹)‘𝑛) · (𝐹‘(𝑛 + 1))) = (0 · (𝐹‘(𝑛 + 1))))
36 peano2uz 12714 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (ℤ𝑁) → (𝑛 + 1) ∈ (ℤ𝑁))
3710uztrn2 12674 . . . . . . . . . . . . . . . . . 18 ((𝑁𝑍 ∧ (𝑛 + 1) ∈ (ℤ𝑁)) → (𝑛 + 1) ∈ 𝑍)
3813, 36, 37syl2an 596 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ (ℤ𝑁)) → (𝑛 + 1) ∈ 𝑍)
39 ntrivcvgfvn0.5 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)
4039ralrimiva 3140 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∀𝑘𝑍 (𝐹𝑘) ∈ ℂ)
41 fveq2 6811 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = (𝑛 + 1) → (𝐹𝑘) = (𝐹‘(𝑛 + 1)))
4241eleq1d 2822 . . . . . . . . . . . . . . . . . . 19 (𝑘 = (𝑛 + 1) → ((𝐹𝑘) ∈ ℂ ↔ (𝐹‘(𝑛 + 1)) ∈ ℂ))
4342rspcv 3566 . . . . . . . . . . . . . . . . . 18 ((𝑛 + 1) ∈ 𝑍 → (∀𝑘𝑍 (𝐹𝑘) ∈ ℂ → (𝐹‘(𝑛 + 1)) ∈ ℂ))
4440, 43mpan9 507 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑛 + 1) ∈ 𝑍) → (𝐹‘(𝑛 + 1)) ∈ ℂ)
4538, 44syldan 591 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (ℤ𝑁)) → (𝐹‘(𝑛 + 1)) ∈ ℂ)
4645ancoms 459 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (ℤ𝑁) ∧ 𝜑) → (𝐹‘(𝑛 + 1)) ∈ ℂ)
4746mul02d 11246 . . . . . . . . . . . . . 14 ((𝑛 ∈ (ℤ𝑁) ∧ 𝜑) → (0 · (𝐹‘(𝑛 + 1))) = 0)
48473adant3 1131 . . . . . . . . . . . . 13 ((𝑛 ∈ (ℤ𝑁) ∧ 𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑛) = 0) → (0 · (𝐹‘(𝑛 + 1))) = 0)
4933, 35, 483eqtrd 2781 . . . . . . . . . . . 12 ((𝑛 ∈ (ℤ𝑁) ∧ 𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑛) = 0) → (seq𝑀( · , 𝐹)‘(𝑛 + 1)) = 0)
50493exp 1118 . . . . . . . . . . 11 (𝑛 ∈ (ℤ𝑁) → (𝜑 → ((seq𝑀( · , 𝐹)‘𝑛) = 0 → (seq𝑀( · , 𝐹)‘(𝑛 + 1)) = 0)))
5150adantrd 492 . . . . . . . . . 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 12723 . . . . . . . 8 (𝑘 ∈ (ℤ𝑁) → ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → (seq𝑀( · , 𝐹)‘𝑘) = 0))
5453impcom 408 . . . . . . 7 (((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) ∧ 𝑘 ∈ (ℤ𝑁)) → (seq𝑀( · , 𝐹)‘𝑘) = 0)
559, 15, 17, 18, 54climconst 15324 . . . . . 6 ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → seq𝑀( · , 𝐹) ⇝ 0)
56 funbrfv 6859 . . . . . 6 (Fun ⇝ → (seq𝑀( · , 𝐹) ⇝ 0 → ( ⇝ ‘seq𝑀( · , 𝐹)) = 0))
574, 55, 56mpsyl 68 . . . . 5 ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → ( ⇝ ‘seq𝑀( · , 𝐹)) = 0)
588, 57eqtr3d 2779 . . . 4 ((𝜑 ∧ (seq𝑀( · , 𝐹)‘𝑁) = 0) → 𝑋 = 0)
5958ex 413 . . 3 (𝜑 → ((seq𝑀( · , 𝐹)‘𝑁) = 0 → 𝑋 = 0))
6059necon3d 2962 . 2 (𝜑 → (𝑋 ≠ 0 → (seq𝑀( · , 𝐹)‘𝑁) ≠ 0))
611, 60mpd 15 1 (𝜑 → (seq𝑀( · , 𝐹)‘𝑁) ≠ 0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1086   = wceq 1540  wcel 2105  wne 2941  wral 3062  Vcvv 3441   class class class wbr 5087  dom cdm 5607  Fun wfun 6459  wf 6461  cfv 6465  (class class class)co 7315  cc 10942  0cc0 10944  1c1 10945   + caddc 10947   · cmul 10949  cz 12392  cuz 12655  seqcseq 13794  cli 15265
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-rep 5224  ax-sep 5238  ax-nul 5245  ax-pow 5303  ax-pr 5367  ax-un 7628  ax-inf2 9470  ax-cnex 11000  ax-resscn 11001  ax-1cn 11002  ax-icn 11003  ax-addcl 11004  ax-addrcl 11005  ax-mulcl 11006  ax-mulrcl 11007  ax-mulcom 11008  ax-addass 11009  ax-mulass 11010  ax-distr 11011  ax-i2m1 11012  ax-1ne0 11013  ax-1rid 11014  ax-rnegex 11015  ax-rrecex 11016  ax-cnre 11017  ax-pre-lttri 11018  ax-pre-lttrn 11019  ax-pre-ltadd 11020  ax-pre-mulgt0 11021  ax-pre-sup 11022
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3350  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4851  df-iun 4939  df-br 5088  df-opab 5150  df-mpt 5171  df-tr 5205  df-id 5507  df-eprel 5513  df-po 5521  df-so 5522  df-fr 5562  df-we 5564  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620  df-pred 6224  df-ord 6291  df-on 6292  df-lim 6293  df-suc 6294  df-iota 6417  df-fun 6467  df-fn 6468  df-f 6469  df-f1 6470  df-fo 6471  df-f1o 6472  df-fv 6473  df-riota 7272  df-ov 7318  df-oprab 7319  df-mpo 7320  df-om 7758  df-2nd 7877  df-frecs 8144  df-wrecs 8175  df-recs 8249  df-rdg 8288  df-er 8546  df-en 8782  df-dom 8783  df-sdom 8784  df-sup 9271  df-pnf 11084  df-mnf 11085  df-xr 11086  df-ltxr 11087  df-le 11088  df-sub 11280  df-neg 11281  df-div 11706  df-nn 12047  df-2 12109  df-3 12110  df-n0 12307  df-z 12393  df-uz 12656  df-rp 12804  df-seq 13795  df-exp 13856  df-cj 14882  df-re 14883  df-im 14884  df-sqrt 15018  df-abs 15019  df-clim 15269
This theorem is referenced by:  ntrivcvgtail  15684
  Copyright terms: Public domain W3C validator