Metamath Proof Explorer

Theorem xrltnr

Description: The extended real 'less than' is irreflexive. (Contributed by NM, 14-Oct-2005)

Ref Expression
Assertion xrltnr 
|- ( A e. RR* -> -. A < A )

Proof

Step Hyp Ref Expression
1 elxr 
 |-  ( A e. RR* <-> ( A e. RR \/ A = +oo \/ A = -oo ) )
2 ltnr 
 |-  ( A e. RR -> -. A < A )
3 pnfnre 
 |-  +oo e/ RR
4 3 neli 
 |-  -. +oo e. RR
5 4 intnan 
 |-  -. ( +oo e. RR /\ +oo e. RR )
6 5 intnanr 
 |-  -. ( ( +oo e. RR /\ +oo e. RR ) /\ +oo
7 pnfnemnf 
 |-  +oo =/= -oo
8 7 neii 
 |-  -. +oo = -oo
9 8 intnanr 
 |-  -. ( +oo = -oo /\ +oo = +oo )
10 6 9 pm3.2ni 
 |-  -. ( ( ( +oo e. RR /\ +oo e. RR ) /\ +oo
11 4 intnanr 
 |-  -. ( +oo e. RR /\ +oo = +oo )
12 4 intnan 
 |-  -. ( +oo = -oo /\ +oo e. RR )
13 11 12 pm3.2ni 
 |-  -. ( ( +oo e. RR /\ +oo = +oo ) \/ ( +oo = -oo /\ +oo e. RR ) )
14 10 13 pm3.2ni 
 |-  -. ( ( ( ( +oo e. RR /\ +oo e. RR ) /\ +oo
15 pnfxr 
 |-  +oo e. RR*
16 ltxr 
 |-  ( ( +oo e. RR* /\ +oo e. RR* ) -> ( +oo < +oo <-> ( ( ( ( +oo e. RR /\ +oo e. RR ) /\ +oo
17 15 15 16 mp2an 
 |-  ( +oo < +oo <-> ( ( ( ( +oo e. RR /\ +oo e. RR ) /\ +oo
18 14 17 mtbir 
 |-  -. +oo < +oo
19 breq12 
 |-  ( ( A = +oo /\ A = +oo ) -> ( A < A <-> +oo < +oo ) )
20 19 anidms 
 |-  ( A = +oo -> ( A < A <-> +oo < +oo ) )
21 18 20 mtbiri 
 |-  ( A = +oo -> -. A < A )
22 mnfnre 
 |-  -oo e/ RR
23 22 neli 
 |-  -. -oo e. RR
24 23 intnan 
 |-  -. ( -oo e. RR /\ -oo e. RR )
25 24 intnanr 
 |-  -. ( ( -oo e. RR /\ -oo e. RR ) /\ -oo
26 7 nesymi 
 |-  -. -oo = +oo
27 26 intnan 
 |-  -. ( -oo = -oo /\ -oo = +oo )
28 25 27 pm3.2ni 
 |-  -. ( ( ( -oo e. RR /\ -oo e. RR ) /\ -oo
29 23 intnanr 
 |-  -. ( -oo e. RR /\ -oo = +oo )
30 23 intnan 
 |-  -. ( -oo = -oo /\ -oo e. RR )
31 29 30 pm3.2ni 
 |-  -. ( ( -oo e. RR /\ -oo = +oo ) \/ ( -oo = -oo /\ -oo e. RR ) )
32 28 31 pm3.2ni 
 |-  -. ( ( ( ( -oo e. RR /\ -oo e. RR ) /\ -oo
33 mnfxr 
 |-  -oo e. RR*
34 ltxr 
 |-  ( ( -oo e. RR* /\ -oo e. RR* ) -> ( -oo < -oo <-> ( ( ( ( -oo e. RR /\ -oo e. RR ) /\ -oo
35 33 33 34 mp2an 
 |-  ( -oo < -oo <-> ( ( ( ( -oo e. RR /\ -oo e. RR ) /\ -oo
36 32 35 mtbir 
 |-  -. -oo < -oo
37 breq12 
 |-  ( ( A = -oo /\ A = -oo ) -> ( A < A <-> -oo < -oo ) )
38 37 anidms 
 |-  ( A = -oo -> ( A < A <-> -oo < -oo ) )
39 36 38 mtbiri 
 |-  ( A = -oo -> -. A < A )
40 2 21 39 3jaoi 
 |-  ( ( A e. RR \/ A = +oo \/ A = -oo ) -> -. A < A )
41 1 40 sylbi 
 |-  ( A e. RR* -> -. A < A )