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

Metamath Proof Explorer

Theorem nltle2tri

Description: Negated extended trichotomy law for 'less than' and 'less than or equal to'. (Contributed by AV, 18-Jul-2020)

Ref Expression
Assertion nltle2tri 
|- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> -. ( A < B /\ B <_ C /\ C <_ A ) )

Proof

Step Hyp Ref Expression
1 xrltletr 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A < B /\ B <_ C ) -> A < C ) )
2 id 
 |-  ( ( ( A < B /\ B <_ C ) -> A < C ) -> ( ( A < B /\ B <_ C ) -> A < C ) )
3 2 impcom 
 |-  ( ( ( A < B /\ B <_ C ) /\ ( ( A < B /\ B <_ C ) -> A < C ) ) -> A < C )
4 xrltnle 
 |-  ( ( A e. RR* /\ C e. RR* ) -> ( A < C <-> -. C <_ A ) )
5 4 3adant2 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( A < C <-> -. C <_ A ) )
6 5 biimpd 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( A < C -> -. C <_ A ) )
7 6 imp 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A < C ) -> -. C <_ A )
8 7 olcd 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A < C ) -> ( -. ( A < B /\ B <_ C ) \/ -. C <_ A ) )
9 8 expcom 
 |-  ( A < C -> ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( -. ( A < B /\ B <_ C ) \/ -. C <_ A ) ) )
10 3 9 syl 
 |-  ( ( ( A < B /\ B <_ C ) /\ ( ( A < B /\ B <_ C ) -> A < C ) ) -> ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( -. ( A < B /\ B <_ C ) \/ -. C <_ A ) ) )
11 10 ex 
 |-  ( ( A < B /\ B <_ C ) -> ( ( ( A < B /\ B <_ C ) -> A < C ) -> ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( -. ( A < B /\ B <_ C ) \/ -. C <_ A ) ) ) )
12 11 com23 
 |-  ( ( A < B /\ B <_ C ) -> ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( ( A < B /\ B <_ C ) -> A < C ) -> ( -. ( A < B /\ B <_ C ) \/ -. C <_ A ) ) ) )
13 12 impd 
 |-  ( ( A < B /\ B <_ C ) -> ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( ( A < B /\ B <_ C ) -> A < C ) ) -> ( -. ( A < B /\ B <_ C ) \/ -. C <_ A ) ) )
14 id 
 |-  ( -. ( A < B /\ B <_ C ) -> -. ( A < B /\ B <_ C ) )
15 14 orcd 
 |-  ( -. ( A < B /\ B <_ C ) -> ( -. ( A < B /\ B <_ C ) \/ -. C <_ A ) )
16 15 a1d 
 |-  ( -. ( A < B /\ B <_ C ) -> ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( ( A < B /\ B <_ C ) -> A < C ) ) -> ( -. ( A < B /\ B <_ C ) \/ -. C <_ A ) ) )
17 13 16 pm2.61i 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( ( A < B /\ B <_ C ) -> A < C ) ) -> ( -. ( A < B /\ B <_ C ) \/ -. C <_ A ) )
18 df-3an 
 |-  ( ( A < B /\ B <_ C /\ C <_ A ) <-> ( ( A < B /\ B <_ C ) /\ C <_ A ) )
19 18 notbii 
 |-  ( -. ( A < B /\ B <_ C /\ C <_ A ) <-> -. ( ( A < B /\ B <_ C ) /\ C <_ A ) )
20 ianor 
 |-  ( -. ( ( A < B /\ B <_ C ) /\ C <_ A ) <-> ( -. ( A < B /\ B <_ C ) \/ -. C <_ A ) )
21 19 20 bitri 
 |-  ( -. ( A < B /\ B <_ C /\ C <_ A ) <-> ( -. ( A < B /\ B <_ C ) \/ -. C <_ A ) )
22 17 21 sylibr 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( ( A < B /\ B <_ C ) -> A < C ) ) -> -. ( A < B /\ B <_ C /\ C <_ A ) )
23 22 ex 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( ( A < B /\ B <_ C ) -> A < C ) -> -. ( A < B /\ B <_ C /\ C <_ A ) ) )
24 1 23 mpd 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> -. ( A < B /\ B <_ C /\ C <_ A ) )