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 ⊢+∞≠-∞

Proof

Step Hyp Ref Expression
1 pire ⊢π∈ℝ
2 pipos ⊢0<π
3 1 2 gt0ne0ii ⊢π≠0
4 3 nesymi ⊢¬0=π
5 1 renegcli ⊢−π∈ℝ
6 5 rexri ⊢−π∈ℝ*
7 0red ⊢−π∈ℝ*∧π∈ℝ→0∈ℝ
8 lt0neg2 ⊢π∈ℝ→0<π↔−π<0
9 1 8 ax-mp ⊢0<π↔−π<0
10 2 9 mpbi ⊢−π<0
11 10 a1i ⊢−π∈ℝ*∧π∈ℝ→−π<0
12 0re ⊢0∈ℝ
13 12 1 2 ltleii ⊢0≤π
14 13 a1i ⊢−π∈ℝ*∧π∈ℝ→0≤π
15 elioc2 ⊢−π∈ℝ*∧π∈ℝ→0∈−ππ↔0∈ℝ∧−π<0∧0≤π
16 7 11 14 15 mpbir3and ⊢−π∈ℝ*∧π∈ℝ→0∈−ππ
17 6 1 16 mp2an ⊢0∈−ππ
18 simpr ⊢−π∈ℝ*∧π∈ℝ→π∈ℝ
19 5 12 1 lttri ⊢−π<0∧0<π→−π<π
20 10 2 19 mp2an ⊢−π<π
21 20 a1i ⊢−π∈ℝ*∧π∈ℝ→−π<π
22 1 leidi ⊢π≤π
23 22 a1i ⊢−π∈ℝ*∧π∈ℝ→π≤π
24 elioc2 ⊢−π∈ℝ*∧π∈ℝ→π∈−ππ↔π∈ℝ∧−π<π∧π≤π
25 18 21 23 24 mpbir3and ⊢−π∈ℝ*∧π∈ℝ→π∈−ππ
26 6 1 25 mp2an ⊢π∈−ππ
27 bj-inftyexpiinj ⊢0∈−ππ∧π∈−ππ→0=π↔inftyexpi⁡0=inftyexpi⁡π
28 17 26 27 mp2an ⊢0=π↔inftyexpi⁡0=inftyexpi⁡π
29 4 28 mtbi ⊢¬inftyexpi⁡0=inftyexpi⁡π
30 df-bj-minfty ⊢-∞=inftyexpi⁡π
31 30 eqeq2i ⊢inftyexpi⁡0=-∞↔inftyexpi⁡0=inftyexpi⁡π
32 29 31 mtbir ⊢¬inftyexpi⁡0=-∞
33 df-bj-pinfty ⊢+∞=inftyexpi⁡0
34 33 eqeq1i ⊢+∞=-∞↔inftyexpi⁡0=-∞
35 32 34 mtbir ⊢¬+∞=-∞
36 35 neir ⊢+∞≠-∞