Theorem climprod1

Description: The limit of a product over one. (Contributed by Scott Fenton, 15-Dec-2017)

	Ref	Expression
Hypotheses	climprod1.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	climprod1.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
Assertion	climprod1	⊢ ( 𝜑 → seq 𝑀 ( · , ( 𝑍 × { 1 } ) ) ⇝ 1 )

Proof

Step	Hyp	Ref	Expression
1		climprod1.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		climprod1.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3	1	prodfclim1	⊢ ( 𝑀 ∈ ℤ → seq 𝑀 ( · , ( 𝑍 × { 1 } ) ) ⇝ 1 )
4	2 3	syl	⊢ ( 𝜑 → seq 𝑀 ( · , ( 𝑍 × { 1 } ) ) ⇝ 1 )