Theorem prodrblem2

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

	Ref	Expression
Hypotheses	prodmo.1	|- F = ( k e. ZZ |-> if ( k e. A , B , 1 ) )
	prodmo.2	|- ( ( ph /\ k e. A ) -> B e. CC )
	prodrb.4	|- ( ph -> M e. ZZ )
	prodrb.5	|- ( ph -> N e. ZZ )
	prodrb.6	|- ( ph -> A C_ ( ZZ>= ` M ) )
	prodrb.7	|- ( ph -> A C_ ( ZZ>= ` N ) )
Assertion	prodrblem2	|- ( ( ph /\ N e. ( ZZ>= ` M ) ) -> ( seq M ( x. , F ) ~~> C <-> seq N ( x. , F ) ~~> C ) )

Proof

Step	Hyp	Ref	Expression
1		prodmo.1	|- F = ( k e. ZZ |-> if ( k e. A , B , 1 ) )
2		prodmo.2	|- ( ( ph /\ k e. A ) -> B e. CC )
3		prodrb.4	|- ( ph -> M e. ZZ )
4		prodrb.5	|- ( ph -> N e. ZZ )
5		prodrb.6	|- ( ph -> A C_ ( ZZ>= ` M ) )
6		prodrb.7	|- ( ph -> A C_ ( ZZ>= ` N ) )
7	4	adantr	|- ( ( ph /\ N e. ( ZZ>= ` M ) ) -> N e. ZZ )
8		seqex	|- seq M ( x. , F ) e. _V
9		climres	|- ( ( N e. ZZ /\ seq M ( x. , F ) e. _V ) -> ( ( seq M ( x. , F ) |` ( ZZ>= ` N ) ) ~~> C <-> seq M ( x. , F ) ~~> C ) )
10	7 8 9	sylancl	|- ( ( ph /\ N e. ( ZZ>= ` M ) ) -> ( ( seq M ( x. , F ) |` ( ZZ>= ` N ) ) ~~> C <-> seq M ( x. , F ) ~~> C ) )
11	2	adantlr	|- ( ( ( ph /\ N e. ( ZZ>= ` M ) ) /\ k e. A ) -> B e. CC )
12		simpr	|- ( ( ph /\ N e. ( ZZ>= ` M ) ) -> N e. ( ZZ>= ` M ) )
13	1 11 12	prodrblem	|- ( ( ( ph /\ N e. ( ZZ>= ` M ) ) /\ A C_ ( ZZ>= ` N ) ) -> ( seq M ( x. , F ) |` ( ZZ>= ` N ) ) = seq N ( x. , F ) )
14	6 13	mpidan	|- ( ( ph /\ N e. ( ZZ>= ` M ) ) -> ( seq M ( x. , F ) |` ( ZZ>= ` N ) ) = seq N ( x. , F ) )
15	14	breq1d	|- ( ( ph /\ N e. ( ZZ>= ` M ) ) -> ( ( seq M ( x. , F ) |` ( ZZ>= ` N ) ) ~~> C <-> seq N ( x. , F ) ~~> C ) )
16	10 15	bitr3d	|- ( ( ph /\ N e. ( ZZ>= ` M ) ) -> ( seq M ( x. , F ) ~~> C <-> seq N ( x. , F ) ~~> C ) )