Metamath Proof Explorer

Theorem bj-pinftynminfty

Description: The extended complex numbers pinfty and minfty are different. (Contributed by BJ, 27-Jun-2019)

Ref Expression
Assertion bj-pinftynminfty 
|- pinfty =/= minfty

Proof

Step Hyp Ref Expression
1 pire 
 |-  _pi e. RR
2 pipos 
 |-  0 < _pi
3 1 2 gt0ne0ii 
 |-  _pi =/= 0
4 3 nesymi 
 |-  -. 0 = _pi
5 1 renegcli 
 |-  -u _pi e. RR
6 5 rexri 
 |-  -u _pi e. RR*
7 0red 
 |-  ( ( -u _pi e. RR* /\ _pi e. RR ) -> 0 e. RR )
8 lt0neg2 
 |-  ( _pi e. RR -> ( 0 < _pi <-> -u _pi < 0 ) )
9 1 8 ax-mp 
 |-  ( 0 < _pi <-> -u _pi < 0 )
10 2 9 mpbi 
 |-  -u _pi < 0
11 10 a1i 
 |-  ( ( -u _pi e. RR* /\ _pi e. RR ) -> -u _pi < 0 )
12 0re 
 |-  0 e. RR
13 12 1 2 ltleii 
 |-  0 <_ _pi
14 13 a1i 
 |-  ( ( -u _pi e. RR* /\ _pi e. RR ) -> 0 <_ _pi )
15 elioc2 
 |-  ( ( -u _pi e. RR* /\ _pi e. RR ) -> ( 0 e. ( -u _pi (,] _pi ) <-> ( 0 e. RR /\ -u _pi < 0 /\ 0 <_ _pi ) ) )
16 7 11 14 15 mpbir3and 
 |-  ( ( -u _pi e. RR* /\ _pi e. RR ) -> 0 e. ( -u _pi (,] _pi ) )
17 6 1 16 mp2an 
 |-  0 e. ( -u _pi (,] _pi )
18 simpr 
 |-  ( ( -u _pi e. RR* /\ _pi e. RR ) -> _pi e. RR )
19 5 12 1 lttri 
 |-  ( ( -u _pi < 0 /\ 0 < _pi ) -> -u _pi < _pi )
20 10 2 19 mp2an 
 |-  -u _pi < _pi
21 20 a1i 
 |-  ( ( -u _pi e. RR* /\ _pi e. RR ) -> -u _pi < _pi )
22 1 leidi 
 |-  _pi <_ _pi
23 22 a1i 
 |-  ( ( -u _pi e. RR* /\ _pi e. RR ) -> _pi <_ _pi )
24 elioc2 
 |-  ( ( -u _pi e. RR* /\ _pi e. RR ) -> ( _pi e. ( -u _pi (,] _pi ) <-> ( _pi e. RR /\ -u _pi < _pi /\ _pi <_ _pi ) ) )
25 18 21 23 24 mpbir3and 
 |-  ( ( -u _pi e. RR* /\ _pi e. RR ) -> _pi e. ( -u _pi (,] _pi ) )
26 6 1 25 mp2an 
 |-  _pi e. ( -u _pi (,] _pi )
27 bj-inftyexpiinj 
 |-  ( ( 0 e. ( -u _pi (,] _pi ) /\ _pi e. ( -u _pi (,] _pi ) ) -> ( 0 = _pi <-> ( inftyexpi ` 0 ) = ( inftyexpi ` _pi ) ) )
28 17 26 27 mp2an 
 |-  ( 0 = _pi <-> ( inftyexpi ` 0 ) = ( inftyexpi ` _pi ) )
29 4 28 mtbi 
 |-  -. ( inftyexpi ` 0 ) = ( inftyexpi ` _pi )
30 df-bj-minfty 
 |-  minfty = ( inftyexpi ` _pi )
31 30 eqeq2i 
 |-  ( ( inftyexpi ` 0 ) = minfty <-> ( inftyexpi ` 0 ) = ( inftyexpi ` _pi ) )
32 29 31 mtbir 
 |-  -. ( inftyexpi ` 0 ) = minfty
33 df-bj-pinfty 
 |-  pinfty = ( inftyexpi ` 0 )
34 33 eqeq1i 
 |-  ( pinfty = minfty <-> ( inftyexpi ` 0 ) = minfty )
35 32 34 mtbir 
 |-  -. pinfty = minfty
36 35 neir 
 |-  pinfty =/= minfty