mnflt - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > mnflt		GIF version

Theorem mnflt 10062

Description: Minus infinity is less than any (finite) real. (Contributed by NM, 14-Oct-2005.)

**Assertion**
Ref	Expression
mnflt	⊢ (𝐴 ∈ ℝ → -∞ < 𝐴)

**Proof of Theorem mnflt**
Step	Hyp	Ref	Expression
1		eqid 2231	. . . 4 ⊢ -∞ = -∞
2		olc 719	. . . 4 ⊢ ((-∞ = -∞ ∧ 𝐴 ∈ ℝ) → ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))
3	1, 2	mpan 424	. . 3 ⊢ (𝐴 ∈ ℝ → ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))
4	3	olcd 742	. 2 ⊢ (𝐴 ∈ ℝ → ((((-∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ -∞ <_ℝ 𝐴) ∨ (-∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ))))
5		mnfxr 8278	. . 3 ⊢ -∞ ∈ ℝ^*
6		rexr 8267	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ^*)
7		ltxr 10054	. . 3 ⊢ ((-∞ ∈ ℝ^* ∧ 𝐴 ∈ ℝ^*) → (-∞ < 𝐴 ↔ ((((-∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ -∞ <_ℝ 𝐴) ∨ (-∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))))
8	5, 6, 7	sylancr 414	. 2 ⊢ (𝐴 ∈ ℝ → (-∞ < 𝐴 ↔ ((((-∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ -∞ <_ℝ 𝐴) ∨ (-∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))))
9	4, 8	mpbird 167	1 ⊢ (𝐴 ∈ ℝ → -∞ < 𝐴)

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 716 = wceq 1398 ∈ wcel 2202 class class class wbr 4093 ℝcr 8074 <_ℝ cltrr 8079 +∞cpnf 8253 -∞cmnf 8254 ℝ^*cxr 8255 < clt 8256

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2204 ax-14 2205 ax-ext 2213 ax-sep 4212 ax-pow 4270 ax-pr 4305 ax-un 4536 ax-cnex 8166

This theorem depends on definitions: df-bi 117 df-3an 1007 df-tru 1401 df-nf 1510 df-sb 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2364 df-ral 2516 df-rex 2517 df-v 2805 df-un 3205 df-in 3207 df-ss 3214 df-pw 3658 df-sn 3679 df-pr 3680 df-op 3682 df-uni 3899 df-br 4094 df-opab 4156 df-xp 4737 df-pnf 8258 df-mnf 8259 df-xr 8260 df-ltxr 8261

This theorem is referenced by: mnflt0 10063 mnfltxr 10065 xrlttr 10074 xrltso 10075 xrlttri3 10076 ngtmnft 10096 nmnfgt 10097 xrrebnd 10098 xrre3 10101 xltnegi 10114 xltadd1 10155 xposdif 10161 elico2 10216 elicc2 10217 ioomax 10227 elioomnf 10247 qbtwnxr 10563 tgioo 15348 repiecelem 16740 repiecele0 16741

W3C validator