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

Metamath Proof Explorer

Theorem prodrb

Description: Rebase the starting point of a product. (Contributed by Scott Fenton, 4-Dec-2017)

Ref Expression
Hypotheses prodmo.1 ⊢ 𝐹 = ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) )
prodmo.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
prodrb.4 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
prodrb.5 ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
prodrb.6 ⊢ ( 𝜑 → 𝐴 ⊆ ( ℤ≥ ‘ 𝑀 ) )
prodrb.7 ⊢ ( 𝜑 → 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) )
Assertion prodrb ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ⇝ 𝐶 ↔ seq 𝑁 ( · , 𝐹 ) ⇝ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 prodmo.1 ⊢ 𝐹 = ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) )
2 prodmo.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
3 prodrb.4 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4 prodrb.5 ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
5 prodrb.6 ⊢ ( 𝜑 → 𝐴 ⊆ ( ℤ≥ ‘ 𝑀 ) )
6 prodrb.7 ⊢ ( 𝜑 → 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) )
7 1 2 3 4 5 6 prodrblem2 ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( seq 𝑀 ( · , 𝐹 ) ⇝ 𝐶 ↔ seq 𝑁 ( · , 𝐹 ) ⇝ 𝐶 ) )
8 1 2 4 3 6 5 prodrblem2 ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( seq 𝑁 ( · , 𝐹 ) ⇝ 𝐶 ↔ seq 𝑀 ( · , 𝐹 ) ⇝ 𝐶 ) )
9 8 bicomd ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( seq 𝑀 ( · , 𝐹 ) ⇝ 𝐶 ↔ seq 𝑁 ( · , 𝐹 ) ⇝ 𝐶 ) )
10 uztric ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∨ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) )
11 3 4 10 syl2anc ⊢ ( 𝜑 → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∨ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) )
12 7 9 11 mpjaodan ⊢ ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ⇝ 𝐶 ↔ seq 𝑁 ( · , 𝐹 ) ⇝ 𝐶 ) )