This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) )