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