Step |
Hyp |
Ref |
Expression |
1 |
|
simpll1 |
|- ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A <_ C /\ C < B ) ) -> A e. RR* ) |
2 |
|
simpll2 |
|- ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A <_ C /\ C < B ) ) -> B e. RR* ) |
3 |
|
simplr1 |
|- ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A <_ C /\ C < B ) ) -> C e. RR* ) |
4 |
|
simplr2 |
|- ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A <_ C /\ C < B ) ) -> D e. RR* ) |
5 |
|
iooin |
|- ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) ) -> ( ( A (,) B ) i^i ( C (,) D ) ) = ( if ( A <_ C , C , A ) (,) if ( B <_ D , B , D ) ) ) |
6 |
1 2 3 4 5
|
syl22anc |
|- ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A <_ C /\ C < B ) ) -> ( ( A (,) B ) i^i ( C (,) D ) ) = ( if ( A <_ C , C , A ) (,) if ( B <_ D , B , D ) ) ) |
7 |
|
simprl |
|- ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A <_ C /\ C < B ) ) -> A <_ C ) |
8 |
7
|
iftrued |
|- ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A <_ C /\ C < B ) ) -> if ( A <_ C , C , A ) = C ) |
9 |
8
|
oveq1d |
|- ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A <_ C /\ C < B ) ) -> ( if ( A <_ C , C , A ) (,) if ( B <_ D , B , D ) ) = ( C (,) if ( B <_ D , B , D ) ) ) |
10 |
|
simprr |
|- ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A <_ C /\ C < B ) ) -> C < B ) |
11 |
|
simplr3 |
|- ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A <_ C /\ C < B ) ) -> C < D ) |
12 |
10 11
|
jca |
|- ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A <_ C /\ C < B ) ) -> ( C < B /\ C < D ) ) |
13 |
|
xrltmin |
|- ( ( C e. RR* /\ B e. RR* /\ D e. RR* ) -> ( C < if ( B <_ D , B , D ) <-> ( C < B /\ C < D ) ) ) |
14 |
3 2 4 13
|
syl3anc |
|- ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A <_ C /\ C < B ) ) -> ( C < if ( B <_ D , B , D ) <-> ( C < B /\ C < D ) ) ) |
15 |
12 14
|
mpbird |
|- ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A <_ C /\ C < B ) ) -> C < if ( B <_ D , B , D ) ) |
16 |
2 4
|
ifcld |
|- ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A <_ C /\ C < B ) ) -> if ( B <_ D , B , D ) e. RR* ) |
17 |
|
ioon0 |
|- ( ( C e. RR* /\ if ( B <_ D , B , D ) e. RR* ) -> ( ( C (,) if ( B <_ D , B , D ) ) =/= (/) <-> C < if ( B <_ D , B , D ) ) ) |
18 |
3 16 17
|
syl2anc |
|- ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A <_ C /\ C < B ) ) -> ( ( C (,) if ( B <_ D , B , D ) ) =/= (/) <-> C < if ( B <_ D , B , D ) ) ) |
19 |
15 18
|
mpbird |
|- ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A <_ C /\ C < B ) ) -> ( C (,) if ( B <_ D , B , D ) ) =/= (/) ) |
20 |
9 19
|
eqnetrd |
|- ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A <_ C /\ C < B ) ) -> ( if ( A <_ C , C , A ) (,) if ( B <_ D , B , D ) ) =/= (/) ) |
21 |
6 20
|
eqnetrd |
|- ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A <_ C /\ C < B ) ) -> ( ( A (,) B ) i^i ( C (,) D ) ) =/= (/) ) |