# Metamath Proof Explorer

## Theorem prodrblem

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

Ref Expression
Hypotheses prodmo.1 ${⊢}{F}=\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)$
prodmo.2 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℂ$
prodrb.3 ${⊢}{\phi }\to {N}\in {ℤ}_{\ge {M}}$
Assertion prodrblem ${⊢}\left({\phi }\wedge {A}\subseteq {ℤ}_{\ge {N}}\right)\to {seq{M}\left(×,{F}\right)↾}_{{ℤ}_{\ge {N}}}=seq{N}\left(×,{F}\right)$

### Proof

Step Hyp Ref Expression
1 prodmo.1 ${⊢}{F}=\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)$
2 prodmo.2 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℂ$
3 prodrb.3 ${⊢}{\phi }\to {N}\in {ℤ}_{\ge {M}}$
4 mulid2 ${⊢}{n}\in ℂ\to 1{n}={n}$
5 4 adantl ${⊢}\left(\left({\phi }\wedge {A}\subseteq {ℤ}_{\ge {N}}\right)\wedge {n}\in ℂ\right)\to 1{n}={n}$
6 1cnd ${⊢}\left({\phi }\wedge {A}\subseteq {ℤ}_{\ge {N}}\right)\to 1\in ℂ$
7 3 adantr ${⊢}\left({\phi }\wedge {A}\subseteq {ℤ}_{\ge {N}}\right)\to {N}\in {ℤ}_{\ge {M}}$
8 iftrue ${⊢}{k}\in {A}\to if\left({k}\in {A},{B},1\right)={B}$
9 8 adantl ${⊢}\left(\left({\phi }\wedge {k}\in ℤ\right)\wedge {k}\in {A}\right)\to if\left({k}\in {A},{B},1\right)={B}$
10 2 adantlr ${⊢}\left(\left({\phi }\wedge {k}\in ℤ\right)\wedge {k}\in {A}\right)\to {B}\in ℂ$
11 9 10 eqeltrd ${⊢}\left(\left({\phi }\wedge {k}\in ℤ\right)\wedge {k}\in {A}\right)\to if\left({k}\in {A},{B},1\right)\in ℂ$
12 11 ex ${⊢}\left({\phi }\wedge {k}\in ℤ\right)\to \left({k}\in {A}\to if\left({k}\in {A},{B},1\right)\in ℂ\right)$
13 iffalse ${⊢}¬{k}\in {A}\to if\left({k}\in {A},{B},1\right)=1$
14 ax-1cn ${⊢}1\in ℂ$
15 13 14 eqeltrdi ${⊢}¬{k}\in {A}\to if\left({k}\in {A},{B},1\right)\in ℂ$
16 12 15 pm2.61d1 ${⊢}\left({\phi }\wedge {k}\in ℤ\right)\to if\left({k}\in {A},{B},1\right)\in ℂ$
17 16 1 fmptd ${⊢}{\phi }\to {F}:ℤ⟶ℂ$
18 uzssz ${⊢}{ℤ}_{\ge {M}}\subseteq ℤ$
19 18 3 sseldi ${⊢}{\phi }\to {N}\in ℤ$
20 17 19 ffvelrnd ${⊢}{\phi }\to {F}\left({N}\right)\in ℂ$
21 20 adantr ${⊢}\left({\phi }\wedge {A}\subseteq {ℤ}_{\ge {N}}\right)\to {F}\left({N}\right)\in ℂ$
22 elfzelz ${⊢}{n}\in \left({M}\dots {N}-1\right)\to {n}\in ℤ$
23 22 adantl ${⊢}\left(\left({\phi }\wedge {A}\subseteq {ℤ}_{\ge {N}}\right)\wedge {n}\in \left({M}\dots {N}-1\right)\right)\to {n}\in ℤ$
24 simplr ${⊢}\left(\left({\phi }\wedge {A}\subseteq {ℤ}_{\ge {N}}\right)\wedge {n}\in \left({M}\dots {N}-1\right)\right)\to {A}\subseteq {ℤ}_{\ge {N}}$
25 19 zcnd ${⊢}{\phi }\to {N}\in ℂ$
26 25 adantr ${⊢}\left({\phi }\wedge {A}\subseteq {ℤ}_{\ge {N}}\right)\to {N}\in ℂ$
27 26 adantr ${⊢}\left(\left({\phi }\wedge {A}\subseteq {ℤ}_{\ge {N}}\right)\wedge {n}\in \left({M}\dots {N}-1\right)\right)\to {N}\in ℂ$
28 1cnd ${⊢}\left(\left({\phi }\wedge {A}\subseteq {ℤ}_{\ge {N}}\right)\wedge {n}\in \left({M}\dots {N}-1\right)\right)\to 1\in ℂ$
29 27 28 npcand ${⊢}\left(\left({\phi }\wedge {A}\subseteq {ℤ}_{\ge {N}}\right)\wedge {n}\in \left({M}\dots {N}-1\right)\right)\to {N}-1+1={N}$
30 29 fveq2d ${⊢}\left(\left({\phi }\wedge {A}\subseteq {ℤ}_{\ge {N}}\right)\wedge {n}\in \left({M}\dots {N}-1\right)\right)\to {ℤ}_{\ge \left({N}-1+1\right)}={ℤ}_{\ge {N}}$
31 24 30 sseqtrrd ${⊢}\left(\left({\phi }\wedge {A}\subseteq {ℤ}_{\ge {N}}\right)\wedge {n}\in \left({M}\dots {N}-1\right)\right)\to {A}\subseteq {ℤ}_{\ge \left({N}-1+1\right)}$
32 fznuz ${⊢}{n}\in \left({M}\dots {N}-1\right)\to ¬{n}\in {ℤ}_{\ge \left({N}-1+1\right)}$
33 32 adantl ${⊢}\left(\left({\phi }\wedge {A}\subseteq {ℤ}_{\ge {N}}\right)\wedge {n}\in \left({M}\dots {N}-1\right)\right)\to ¬{n}\in {ℤ}_{\ge \left({N}-1+1\right)}$
34 31 33 ssneldd ${⊢}\left(\left({\phi }\wedge {A}\subseteq {ℤ}_{\ge {N}}\right)\wedge {n}\in \left({M}\dots {N}-1\right)\right)\to ¬{n}\in {A}$
35 23 34 eldifd ${⊢}\left(\left({\phi }\wedge {A}\subseteq {ℤ}_{\ge {N}}\right)\wedge {n}\in \left({M}\dots {N}-1\right)\right)\to {n}\in \left(ℤ\setminus {A}\right)$
36 fveqeq2 ${⊢}{k}={n}\to \left({F}\left({k}\right)=1↔{F}\left({n}\right)=1\right)$
37 eldifi ${⊢}{k}\in \left(ℤ\setminus {A}\right)\to {k}\in ℤ$
38 eldifn ${⊢}{k}\in \left(ℤ\setminus {A}\right)\to ¬{k}\in {A}$
39 38 13 syl ${⊢}{k}\in \left(ℤ\setminus {A}\right)\to if\left({k}\in {A},{B},1\right)=1$
40 39 14 eqeltrdi ${⊢}{k}\in \left(ℤ\setminus {A}\right)\to if\left({k}\in {A},{B},1\right)\in ℂ$
41 1 fvmpt2 ${⊢}\left({k}\in ℤ\wedge if\left({k}\in {A},{B},1\right)\in ℂ\right)\to {F}\left({k}\right)=if\left({k}\in {A},{B},1\right)$
42 37 40 41 syl2anc ${⊢}{k}\in \left(ℤ\setminus {A}\right)\to {F}\left({k}\right)=if\left({k}\in {A},{B},1\right)$
43 42 39 eqtrd ${⊢}{k}\in \left(ℤ\setminus {A}\right)\to {F}\left({k}\right)=1$
44 36 43 vtoclga ${⊢}{n}\in \left(ℤ\setminus {A}\right)\to {F}\left({n}\right)=1$
45 35 44 syl ${⊢}\left(\left({\phi }\wedge {A}\subseteq {ℤ}_{\ge {N}}\right)\wedge {n}\in \left({M}\dots {N}-1\right)\right)\to {F}\left({n}\right)=1$
46 5 6 7 21 45 seqid ${⊢}\left({\phi }\wedge {A}\subseteq {ℤ}_{\ge {N}}\right)\to {seq{M}\left(×,{F}\right)↾}_{{ℤ}_{\ge {N}}}=seq{N}\left(×,{F}\right)$