Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
⊢ -∞ = -∞ |
2 |
|
eqid |
⊢ +∞ = +∞ |
3 |
|
olc |
⊢ ( ( -∞ = -∞ ∧ +∞ = +∞ ) → ( ( ( -∞ ∈ ℝ ∧ +∞ ∈ ℝ ) ∧ -∞ <ℝ +∞ ) ∨ ( -∞ = -∞ ∧ +∞ = +∞ ) ) ) |
4 |
1 2 3
|
mp2an |
⊢ ( ( ( -∞ ∈ ℝ ∧ +∞ ∈ ℝ ) ∧ -∞ <ℝ +∞ ) ∨ ( -∞ = -∞ ∧ +∞ = +∞ ) ) |
5 |
4
|
orci |
⊢ ( ( ( ( -∞ ∈ ℝ ∧ +∞ ∈ ℝ ) ∧ -∞ <ℝ +∞ ) ∨ ( -∞ = -∞ ∧ +∞ = +∞ ) ) ∨ ( ( -∞ ∈ ℝ ∧ +∞ = +∞ ) ∨ ( -∞ = -∞ ∧ +∞ ∈ ℝ ) ) ) |
6 |
|
mnfxr |
⊢ -∞ ∈ ℝ* |
7 |
|
pnfxr |
⊢ +∞ ∈ ℝ* |
8 |
|
ltxr |
⊢ ( ( -∞ ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( -∞ < +∞ ↔ ( ( ( ( -∞ ∈ ℝ ∧ +∞ ∈ ℝ ) ∧ -∞ <ℝ +∞ ) ∨ ( -∞ = -∞ ∧ +∞ = +∞ ) ) ∨ ( ( -∞ ∈ ℝ ∧ +∞ = +∞ ) ∨ ( -∞ = -∞ ∧ +∞ ∈ ℝ ) ) ) ) ) |
9 |
6 7 8
|
mp2an |
⊢ ( -∞ < +∞ ↔ ( ( ( ( -∞ ∈ ℝ ∧ +∞ ∈ ℝ ) ∧ -∞ <ℝ +∞ ) ∨ ( -∞ = -∞ ∧ +∞ = +∞ ) ) ∨ ( ( -∞ ∈ ℝ ∧ +∞ = +∞ ) ∨ ( -∞ = -∞ ∧ +∞ ∈ ℝ ) ) ) ) |
10 |
5 9
|
mpbir |
⊢ -∞ < +∞ |