This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 mullid ⊢ ( 𝑛 ∈ ℂ → ( 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 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑁 ) ∈ ℂ )
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 𝑁 ( · , 𝐹 ) )