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 = π ↔ ( +∞ei ‘ 0 ) = ( +∞ei ‘ π ) ) )
28	17 26 27	mp2an	⊢ ( 0 = π ↔ ( +∞ei ‘ 0 ) = ( +∞ei ‘ π ) )
29	4 28	mtbi	⊢ ¬ ( +∞ei ‘ 0 ) = ( +∞ei ‘ π )
30		df-bj-minfty	⊢ -∞ = ( +∞ei ‘ π )
31	30	eqeq2i	⊢ ( ( +∞ei ‘ 0 ) = -∞ ↔ ( +∞ei ‘ 0 ) = ( +∞ei ‘ π ) )
32	29 31	mtbir	⊢ ¬ ( +∞ei ‘ 0 ) = -∞
33		df-bj-pinfty	⊢ +∞ = ( +∞ei ‘ 0 )
34	33	eqeq1i	⊢ ( +∞ = -∞ ↔ ( +∞ei ‘ 0 ) = -∞ )
35	32 34	mtbir	⊢ ¬ +∞ = -∞
36	35	neir	⊢ +∞ ≠ -∞