Theorem prodfclim1

Description: The constant one product converges to one. (Contributed by Scott Fenton, 5-Dec-2017)

	Ref	Expression
Hypothesis	prodf1.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
Assertion	prodfclim1	⊢ ( 𝑀 ∈ ℤ → seq 𝑀 ( · , ( 𝑍 × { 1 } ) ) ⇝ 1 )

Proof

Step	Hyp	Ref	Expression
1		prodf1.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2	1	prodf1f	⊢ ( 𝑀 ∈ ℤ → seq 𝑀 ( · , ( 𝑍 × { 1 } ) ) = ( 𝑍 × { 1 } ) )
3		ax-1cn	⊢ 1 ∈ ℂ
4	1	eqimss2i	⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ 𝑍
5	1	fvexi	⊢ 𝑍 ∈ V
6	4 5	climconst2	⊢ ( ( 1 ∈ ℂ ∧ 𝑀 ∈ ℤ ) → ( 𝑍 × { 1 } ) ⇝ 1 )
7	3 6	mpan	⊢ ( 𝑀 ∈ ℤ → ( 𝑍 × { 1 } ) ⇝ 1 )
8	2 7	eqbrtrd	⊢ ( 𝑀 ∈ ℤ → seq 𝑀 ( · , ( 𝑍 × { 1 } ) ) ⇝ 1 )