Metamath Proof Explorer


Theorem fzass4

Description: Two ways to express a nondecreasing sequence of four integers. (Contributed by Stefan O'Rear, 15-Aug-2015)

Ref Expression
Assertion fzass4
|- ( ( B e. ( A ... D ) /\ C e. ( B ... D ) ) <-> ( B e. ( A ... C ) /\ C e. ( A ... D ) ) )

Proof

Step Hyp Ref Expression
1 simpll
 |-  ( ( ( B e. ( ZZ>= ` A ) /\ D e. ( ZZ>= ` B ) ) /\ ( C e. ( ZZ>= ` B ) /\ D e. ( ZZ>= ` C ) ) ) -> B e. ( ZZ>= ` A ) )
2 simprl
 |-  ( ( ( B e. ( ZZ>= ` A ) /\ D e. ( ZZ>= ` B ) ) /\ ( C e. ( ZZ>= ` B ) /\ D e. ( ZZ>= ` C ) ) ) -> C e. ( ZZ>= ` B ) )
3 1 2 jca
 |-  ( ( ( B e. ( ZZ>= ` A ) /\ D e. ( ZZ>= ` B ) ) /\ ( C e. ( ZZ>= ` B ) /\ D e. ( ZZ>= ` C ) ) ) -> ( B e. ( ZZ>= ` A ) /\ C e. ( ZZ>= ` B ) ) )
4 uztrn
 |-  ( ( C e. ( ZZ>= ` B ) /\ B e. ( ZZ>= ` A ) ) -> C e. ( ZZ>= ` A ) )
5 4 ancoms
 |-  ( ( B e. ( ZZ>= ` A ) /\ C e. ( ZZ>= ` B ) ) -> C e. ( ZZ>= ` A ) )
6 5 ad2ant2r
 |-  ( ( ( B e. ( ZZ>= ` A ) /\ D e. ( ZZ>= ` B ) ) /\ ( C e. ( ZZ>= ` B ) /\ D e. ( ZZ>= ` C ) ) ) -> C e. ( ZZ>= ` A ) )
7 simprr
 |-  ( ( ( B e. ( ZZ>= ` A ) /\ D e. ( ZZ>= ` B ) ) /\ ( C e. ( ZZ>= ` B ) /\ D e. ( ZZ>= ` C ) ) ) -> D e. ( ZZ>= ` C ) )
8 3 6 7 jca32
 |-  ( ( ( B e. ( ZZ>= ` A ) /\ D e. ( ZZ>= ` B ) ) /\ ( C e. ( ZZ>= ` B ) /\ D e. ( ZZ>= ` C ) ) ) -> ( ( B e. ( ZZ>= ` A ) /\ C e. ( ZZ>= ` B ) ) /\ ( C e. ( ZZ>= ` A ) /\ D e. ( ZZ>= ` C ) ) ) )
9 simpll
 |-  ( ( ( B e. ( ZZ>= ` A ) /\ C e. ( ZZ>= ` B ) ) /\ ( C e. ( ZZ>= ` A ) /\ D e. ( ZZ>= ` C ) ) ) -> B e. ( ZZ>= ` A ) )
10 uztrn
 |-  ( ( D e. ( ZZ>= ` C ) /\ C e. ( ZZ>= ` B ) ) -> D e. ( ZZ>= ` B ) )
11 10 ancoms
 |-  ( ( C e. ( ZZ>= ` B ) /\ D e. ( ZZ>= ` C ) ) -> D e. ( ZZ>= ` B ) )
12 11 ad2ant2l
 |-  ( ( ( B e. ( ZZ>= ` A ) /\ C e. ( ZZ>= ` B ) ) /\ ( C e. ( ZZ>= ` A ) /\ D e. ( ZZ>= ` C ) ) ) -> D e. ( ZZ>= ` B ) )
13 9 12 jca
 |-  ( ( ( B e. ( ZZ>= ` A ) /\ C e. ( ZZ>= ` B ) ) /\ ( C e. ( ZZ>= ` A ) /\ D e. ( ZZ>= ` C ) ) ) -> ( B e. ( ZZ>= ` A ) /\ D e. ( ZZ>= ` B ) ) )
14 simplr
 |-  ( ( ( B e. ( ZZ>= ` A ) /\ C e. ( ZZ>= ` B ) ) /\ ( C e. ( ZZ>= ` A ) /\ D e. ( ZZ>= ` C ) ) ) -> C e. ( ZZ>= ` B ) )
15 simprr
 |-  ( ( ( B e. ( ZZ>= ` A ) /\ C e. ( ZZ>= ` B ) ) /\ ( C e. ( ZZ>= ` A ) /\ D e. ( ZZ>= ` C ) ) ) -> D e. ( ZZ>= ` C ) )
16 13 14 15 jca32
 |-  ( ( ( B e. ( ZZ>= ` A ) /\ C e. ( ZZ>= ` B ) ) /\ ( C e. ( ZZ>= ` A ) /\ D e. ( ZZ>= ` C ) ) ) -> ( ( B e. ( ZZ>= ` A ) /\ D e. ( ZZ>= ` B ) ) /\ ( C e. ( ZZ>= ` B ) /\ D e. ( ZZ>= ` C ) ) ) )
17 8 16 impbii
 |-  ( ( ( B e. ( ZZ>= ` A ) /\ D e. ( ZZ>= ` B ) ) /\ ( C e. ( ZZ>= ` B ) /\ D e. ( ZZ>= ` C ) ) ) <-> ( ( B e. ( ZZ>= ` A ) /\ C e. ( ZZ>= ` B ) ) /\ ( C e. ( ZZ>= ` A ) /\ D e. ( ZZ>= ` C ) ) ) )
18 elfzuzb
 |-  ( B e. ( A ... D ) <-> ( B e. ( ZZ>= ` A ) /\ D e. ( ZZ>= ` B ) ) )
19 elfzuzb
 |-  ( C e. ( B ... D ) <-> ( C e. ( ZZ>= ` B ) /\ D e. ( ZZ>= ` C ) ) )
20 18 19 anbi12i
 |-  ( ( B e. ( A ... D ) /\ C e. ( B ... D ) ) <-> ( ( B e. ( ZZ>= ` A ) /\ D e. ( ZZ>= ` B ) ) /\ ( C e. ( ZZ>= ` B ) /\ D e. ( ZZ>= ` C ) ) ) )
21 elfzuzb
 |-  ( B e. ( A ... C ) <-> ( B e. ( ZZ>= ` A ) /\ C e. ( ZZ>= ` B ) ) )
22 elfzuzb
 |-  ( C e. ( A ... D ) <-> ( C e. ( ZZ>= ` A ) /\ D e. ( ZZ>= ` C ) ) )
23 21 22 anbi12i
 |-  ( ( B e. ( A ... C ) /\ C e. ( A ... D ) ) <-> ( ( B e. ( ZZ>= ` A ) /\ C e. ( ZZ>= ` B ) ) /\ ( C e. ( ZZ>= ` A ) /\ D e. ( ZZ>= ` C ) ) ) )
24 17 20 23 3bitr4i
 |-  ( ( B e. ( A ... D ) /\ C e. ( B ... D ) ) <-> ( B e. ( A ... C ) /\ C e. ( A ... D ) ) )