Metamath Proof Explorer


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 𝑁 ( · , 𝐹 ) ⇝ 𝐶 ) )