Metamath Proof Explorer

Theorem prodrblem2

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

Ref Expression
Hypotheses prodmo.1 $⊢ F = k ∈ ℤ ⟼ if k ∈ A B 1$
prodmo.2 $⊢ φ ∧ k ∈ A → B ∈ ℂ$
prodrb.4 $⊢ φ → M ∈ ℤ$
prodrb.5 $⊢ φ → N ∈ ℤ$
prodrb.6 $⊢ φ → A ⊆ ℤ ≥ M$
prodrb.7 $⊢ φ → A ⊆ ℤ ≥ N$
Assertion prodrblem2 $⊢ φ ∧ N ∈ ℤ ≥ M → seq M × F ⇝ C ↔ seq N × F ⇝ C$

Proof

Step Hyp Ref Expression
1 prodmo.1 $⊢ F = k ∈ ℤ ⟼ if k ∈ A B 1$
2 prodmo.2 $⊢ φ ∧ k ∈ A → B ∈ ℂ$
3 prodrb.4 $⊢ φ → M ∈ ℤ$
4 prodrb.5 $⊢ φ → N ∈ ℤ$
5 prodrb.6 $⊢ φ → A ⊆ ℤ ≥ M$
6 prodrb.7 $⊢ φ → A ⊆ ℤ ≥ N$
7 4 adantr $⊢ φ ∧ N ∈ ℤ ≥ M → N ∈ ℤ$
8 seqex $⊢ seq M × F ∈ V$
9 climres $⊢ N ∈ ℤ ∧ seq M × F ∈ V → seq M × F ↾ ℤ ≥ N ⇝ C ↔ seq M × F ⇝ C$
10 7 8 9 sylancl $⊢ φ ∧ N ∈ ℤ ≥ M → seq M × F ↾ ℤ ≥ N ⇝ C ↔ seq M × F ⇝ C$
11 2 adantlr $⊢ φ ∧ N ∈ ℤ ≥ M ∧ k ∈ A → B ∈ ℂ$
12 simpr $⊢ φ ∧ N ∈ ℤ ≥ M → N ∈ ℤ ≥ M$
13 1 11 12 prodrblem $⊢ φ ∧ N ∈ ℤ ≥ M ∧ A ⊆ ℤ ≥ N → seq M × F ↾ ℤ ≥ N = seq N × F$
14 6 13 mpidan $⊢ φ ∧ N ∈ ℤ ≥ M → seq M × F ↾ ℤ ≥ N = seq N × F$
15 14 breq1d $⊢ φ ∧ N ∈ ℤ ≥ M → seq M × F ↾ ℤ ≥ N ⇝ C ↔ seq N × F ⇝ C$
16 10 15 bitr3d $⊢ φ ∧ N ∈ ℤ ≥ M → seq M × F ⇝ C ↔ seq N × F ⇝ C$