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 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) )