Theorem prodrblem

Description: Lemma for prodrb . (Contributed by Scott Fenton, 4-Dec-2017)

	Ref	Expression
Hypotheses	prodmo.1	⊢ 𝐹 = ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) )
	prodmo.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
	prodrb.3	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
Assertion	prodrblem	⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) ) → ( seq 𝑀 ( · , 𝐹 ) ↾ ( ℤ≥ ‘ 𝑁 ) ) = seq 𝑁 ( · , 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		prodmo.1	⊢ 𝐹 = ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) )
2		prodmo.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
3		prodrb.3	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
4		mulid2	⊢ ( 𝑛 ∈ ℂ → ( 1 · 𝑛 ) = 𝑛 )
5	4	adantl	⊢ ( ( ( 𝜑 ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑛 ∈ ℂ ) → ( 1 · 𝑛 ) = 𝑛 )
6		1cnd	⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) ) → 1 ∈ ℂ )
7	3	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
8		iftrue	⊢ ( 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) = 𝐵 )
9	8	adantl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑘 ∈ 𝐴 ) → if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) = 𝐵 )
10	2	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
11	9 10	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑘 ∈ 𝐴 ) → if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ∈ ℂ )
12	11	ex	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ∈ ℂ ) )
13		iffalse	⊢ ( ¬ 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) = 1 )
14		ax-1cn	⊢ 1 ∈ ℂ
15	13 14	eqeltrdi	⊢ ( ¬ 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ∈ ℂ )
16	12 15	pm2.61d1	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ∈ ℂ )
17	16 1	fmptd	⊢ ( 𝜑 → 𝐹 : ℤ ⟶ ℂ )
18		uzssz	⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
19	18 3	sselid	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
20	17 19	ffvelrnd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑁 ) ∈ ℂ )
21	20	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐹 ‘ 𝑁 ) ∈ ℂ )
22		elfzelz	⊢ ( 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) → 𝑛 ∈ ℤ )
23	22	adantl	⊢ ( ( ( 𝜑 ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → 𝑛 ∈ ℤ )
24		simplr	⊢ ( ( ( 𝜑 ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) )
25	19	zcnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
26	25	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ∈ ℂ )
27	26	adantr	⊢ ( ( ( 𝜑 ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ℂ )
28		1cnd	⊢ ( ( ( 𝜑 ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → 1 ∈ ℂ )
29	27 28	npcand	⊢ ( ( ( 𝜑 ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
30	29	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( ℤ≥ ‘ ( ( 𝑁 − 1 ) + 1 ) ) = ( ℤ≥ ‘ 𝑁 ) )
31	24 30	sseqtrrd	⊢ ( ( ( 𝜑 ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → 𝐴 ⊆ ( ℤ≥ ‘ ( ( 𝑁 − 1 ) + 1 ) ) )
32		fznuz	⊢ ( 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) → ¬ 𝑛 ∈ ( ℤ≥ ‘ ( ( 𝑁 − 1 ) + 1 ) ) )
33	32	adantl	⊢ ( ( ( 𝜑 ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ¬ 𝑛 ∈ ( ℤ≥ ‘ ( ( 𝑁 − 1 ) + 1 ) ) )
34	31 33	ssneldd	⊢ ( ( ( 𝜑 ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ¬ 𝑛 ∈ 𝐴 )
35	23 34	eldifd	⊢ ( ( ( 𝜑 ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → 𝑛 ∈ ( ℤ ∖ 𝐴 ) )
36		fveqeq2	⊢ ( 𝑘 = 𝑛 → ( ( 𝐹 ‘ 𝑘 ) = 1 ↔ ( 𝐹 ‘ 𝑛 ) = 1 ) )
37		eldifi	⊢ ( 𝑘 ∈ ( ℤ ∖ 𝐴 ) → 𝑘 ∈ ℤ )
38		eldifn	⊢ ( 𝑘 ∈ ( ℤ ∖ 𝐴 ) → ¬ 𝑘 ∈ 𝐴 )
39	38 13	syl	⊢ ( 𝑘 ∈ ( ℤ ∖ 𝐴 ) → if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) = 1 )
40	39 14	eqeltrdi	⊢ ( 𝑘 ∈ ( ℤ ∖ 𝐴 ) → if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ∈ ℂ )
41	1	fvmpt2	⊢ ( ( 𝑘 ∈ ℤ ∧ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ∈ ℂ ) → ( 𝐹 ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) )
42	37 40 41	syl2anc	⊢ ( 𝑘 ∈ ( ℤ ∖ 𝐴 ) → ( 𝐹 ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) )
43	42 39	eqtrd	⊢ ( 𝑘 ∈ ( ℤ ∖ 𝐴 ) → ( 𝐹 ‘ 𝑘 ) = 1 )
44	36 43	vtoclga	⊢ ( 𝑛 ∈ ( ℤ ∖ 𝐴 ) → ( 𝐹 ‘ 𝑛 ) = 1 )
45	35 44	syl	⊢ ( ( ( 𝜑 ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( 𝐹 ‘ 𝑛 ) = 1 )
46	5 6 7 21 45	seqid	⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) ) → ( seq 𝑀 ( · , 𝐹 ) ↾ ( ℤ≥ ‘ 𝑁 ) ) = seq 𝑁 ( · , 𝐹 ) )