Theorem prodf1f

Description: A one-valued infinite product is equal to the constant one function. (Contributed by Scott Fenton, 5-Dec-2017)

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

Proof

Step	Hyp	Ref	Expression
1		prodf1.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2	1	prodf1	⊢ ( 𝑘 ∈ 𝑍 → ( seq 𝑀 ( · , ( 𝑍 × { 1 } ) ) ‘ 𝑘 ) = 1 )
3		1ex	⊢ 1 ∈ V
4	3	fvconst2	⊢ ( 𝑘 ∈ 𝑍 → ( ( 𝑍 × { 1 } ) ‘ 𝑘 ) = 1 )
5	2 4	eqtr4d	⊢ ( 𝑘 ∈ 𝑍 → ( seq 𝑀 ( · , ( 𝑍 × { 1 } ) ) ‘ 𝑘 ) = ( ( 𝑍 × { 1 } ) ‘ 𝑘 ) )
6	5	rgen	⊢ ∀ 𝑘 ∈ 𝑍 ( seq 𝑀 ( · , ( 𝑍 × { 1 } ) ) ‘ 𝑘 ) = ( ( 𝑍 × { 1 } ) ‘ 𝑘 )
7		seqfn	⊢ ( 𝑀 ∈ ℤ → seq 𝑀 ( · , ( 𝑍 × { 1 } ) ) Fn ( ℤ≥ ‘ 𝑀 ) )
8	1	fneq2i	⊢ ( seq 𝑀 ( · , ( 𝑍 × { 1 } ) ) Fn 𝑍 ↔ seq 𝑀 ( · , ( 𝑍 × { 1 } ) ) Fn ( ℤ≥ ‘ 𝑀 ) )
9	7 8	sylibr	⊢ ( 𝑀 ∈ ℤ → seq 𝑀 ( · , ( 𝑍 × { 1 } ) ) Fn 𝑍 )
10	3	fconst	⊢ ( 𝑍 × { 1 } ) : 𝑍 ⟶ { 1 }
11		ffn	⊢ ( ( 𝑍 × { 1 } ) : 𝑍 ⟶ { 1 } → ( 𝑍 × { 1 } ) Fn 𝑍 )
12	10 11	ax-mp	⊢ ( 𝑍 × { 1 } ) Fn 𝑍
13		eqfnfv	⊢ ( ( seq 𝑀 ( · , ( 𝑍 × { 1 } ) ) Fn 𝑍 ∧ ( 𝑍 × { 1 } ) Fn 𝑍 ) → ( seq 𝑀 ( · , ( 𝑍 × { 1 } ) ) = ( 𝑍 × { 1 } ) ↔ ∀ 𝑘 ∈ 𝑍 ( seq 𝑀 ( · , ( 𝑍 × { 1 } ) ) ‘ 𝑘 ) = ( ( 𝑍 × { 1 } ) ‘ 𝑘 ) ) )
14	9 12 13	sylancl	⊢ ( 𝑀 ∈ ℤ → ( seq 𝑀 ( · , ( 𝑍 × { 1 } ) ) = ( 𝑍 × { 1 } ) ↔ ∀ 𝑘 ∈ 𝑍 ( seq 𝑀 ( · , ( 𝑍 × { 1 } ) ) ‘ 𝑘 ) = ( ( 𝑍 × { 1 } ) ‘ 𝑘 ) ) )
15	6 14	mpbiri	⊢ ( 𝑀 ∈ ℤ → seq 𝑀 ( · , ( 𝑍 × { 1 } ) ) = ( 𝑍 × { 1 } ) )