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