This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ntrivcvgn0

Description: A product that converges to a nonzero value converges non-trivially. (Contributed by Scott Fenton, 18-Dec-2017)

Ref Expression
Hypotheses ntrivcvgn0.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
ntrivcvgn0.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
ntrivcvgn0.3 ⊢ ( 𝜑 → seq 𝑀 ( · , 𝐹 ) ⇝ 𝑋 )
ntrivcvgn0.4 ⊢ ( 𝜑 → 𝑋 ≠ 0 )
Assertion ntrivcvgn0 ( 𝜑 → ∃ 𝑛 ∈ 𝑍 ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) )

Proof

Step Hyp Ref Expression
1 ntrivcvgn0.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 ntrivcvgn0.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 ntrivcvgn0.3 ⊢ ( 𝜑 → seq 𝑀 ( · , 𝐹 ) ⇝ 𝑋 )
4 ntrivcvgn0.4 ⊢ ( 𝜑 → 𝑋 ≠ 0 )
5 2 uzidd ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
6 5 1 eleqtrrdi ⊢ ( 𝜑 → 𝑀 ∈ 𝑍 )
7 climrel ⊢ Rel ⇝
8 7 brrelex2i ⊢ ( seq 𝑀 ( · , 𝐹 ) ⇝ 𝑋 → 𝑋 ∈ V )
9 3 8 syl ⊢ ( 𝜑 → 𝑋 ∈ V )
10 4 3 jca ⊢ ( 𝜑 → ( 𝑋 ≠ 0 ∧ seq 𝑀 ( · , 𝐹 ) ⇝ 𝑋 ) )
11 neeq1 ⊢ ( 𝑦 = 𝑋 → ( 𝑦 ≠ 0 ↔ 𝑋 ≠ 0 ) )
12 breq2 ⊢ ( 𝑦 = 𝑋 → ( seq 𝑀 ( · , 𝐹 ) ⇝ 𝑦 ↔ seq 𝑀 ( · , 𝐹 ) ⇝ 𝑋 ) )
13 11 12 anbi12d ⊢ ( 𝑦 = 𝑋 → ( ( 𝑦 ≠ 0 ∧ seq 𝑀 ( · , 𝐹 ) ⇝ 𝑦 ) ↔ ( 𝑋 ≠ 0 ∧ seq 𝑀 ( · , 𝐹 ) ⇝ 𝑋 ) ) )
14 9 10 13 spcedv ⊢ ( 𝜑 → ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑀 ( · , 𝐹 ) ⇝ 𝑦 ) )
15 seqeq1 ⊢ ( 𝑛 = 𝑀 → seq 𝑛 ( · , 𝐹 ) = seq 𝑀 ( · , 𝐹 ) )
16 15 breq1d ⊢ ( 𝑛 = 𝑀 → ( seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ↔ seq 𝑀 ( · , 𝐹 ) ⇝ 𝑦 ) )
17 16 anbi2d ⊢ ( 𝑛 = 𝑀 → ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ↔ ( 𝑦 ≠ 0 ∧ seq 𝑀 ( · , 𝐹 ) ⇝ 𝑦 ) ) )
18 17 exbidv ⊢ ( 𝑛 = 𝑀 → ( ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ↔ ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑀 ( · , 𝐹 ) ⇝ 𝑦 ) ) )
19 18 rspcev ⊢ ( ( 𝑀 ∈ 𝑍 ∧ ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑀 ( · , 𝐹 ) ⇝ 𝑦 ) ) → ∃ 𝑛 ∈ 𝑍 ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) )
20 6 14 19 syl2anc ⊢ ( 𝜑 → ∃ 𝑛 ∈ 𝑍 ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) )