Metamath Proof Explorer


Theorem prodrblem2

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

Ref Expression
Hypotheses prodmo.1 F=kifkAB1
prodmo.2 φkAB
prodrb.4 φM
prodrb.5 φN
prodrb.6 φAM
prodrb.7 φAN
Assertion prodrblem2 φNMseqM×FCseqN×FC

Proof

Step Hyp Ref Expression
1 prodmo.1 F=kifkAB1
2 prodmo.2 φkAB
3 prodrb.4 φM
4 prodrb.5 φN
5 prodrb.6 φAM
6 prodrb.7 φAN
7 4 adantr φNMN
8 seqex seqM×FV
9 climres NseqM×FVseqM×FNCseqM×FC
10 7 8 9 sylancl φNMseqM×FNCseqM×FC
11 2 adantlr φNMkAB
12 simpr φNMNM
13 1 11 12 prodrblem φNMANseqM×FN=seqN×F
14 6 13 mpidan φNMseqM×FN=seqN×F
15 14 breq1d φNMseqM×FNCseqN×FC
16 10 15 bitr3d φNMseqM×FCseqN×FC