Theorem prodrblem2

Description: Lemma for prodrb . (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	prodrblem2	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 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	4	adantr	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑁 ∈ ℤ )
8		seqex	⊢ seq 𝑀 ( · , 𝐹 ) ∈ V
9		climres	⊢ ( ( 𝑁 ∈ ℤ ∧ seq 𝑀 ( · , 𝐹 ) ∈ V ) → ( ( seq 𝑀 ( · , 𝐹 ) ↾ ( ℤ≥ ‘ 𝑁 ) ) ⇝ 𝐶 ↔ seq 𝑀 ( · , 𝐹 ) ⇝ 𝐶 ) )
10	7 8 9	sylancl	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( seq 𝑀 ( · , 𝐹 ) ↾ ( ℤ≥ ‘ 𝑁 ) ) ⇝ 𝐶 ↔ seq 𝑀 ( · , 𝐹 ) ⇝ 𝐶 ) )
11	2	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
12		simpr	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
13	1 11 12	prodrblem	⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) ) → ( seq 𝑀 ( · , 𝐹 ) ↾ ( ℤ≥ ‘ 𝑁 ) ) = seq 𝑁 ( · , 𝐹 ) )
14	6 13	mpidan	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( seq 𝑀 ( · , 𝐹 ) ↾ ( ℤ≥ ‘ 𝑁 ) ) = seq 𝑁 ( · , 𝐹 ) )
15	14	breq1d	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( seq 𝑀 ( · , 𝐹 ) ↾ ( ℤ≥ ‘ 𝑁 ) ) ⇝ 𝐶 ↔ seq 𝑁 ( · , 𝐹 ) ⇝ 𝐶 ) )
16	10 15	bitr3d	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( seq 𝑀 ( · , 𝐹 ) ⇝ 𝐶 ↔ seq 𝑁 ( · , 𝐹 ) ⇝ 𝐶 ) )