mnflt - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > mnflt		Structured version Visualization version GIF version

Theorem mnflt 13149

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 2763	. . . 4 ⊢ -∞ = -∞
2		olc 881	. . . 4 ⊢ ((-∞ = -∞ ∧ 𝐴 ∈ ℝ) → ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))
3	1, 2	mpan 702	. . 3 ⊢ (𝐴 ∈ ℝ → ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))
4	3	olcd 887	. 2 ⊢ (𝐴 ∈ ℝ → ((((-∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ -∞ <_ℝ 𝐴) ∨ (-∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ))))
5		mnfxr 11267	. . 3 ⊢ -∞ ∈ ℝ^*
6		rexr 11256	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ^*)
7		ltxr 13141	. . 3 ⊢ ((-∞ ∈ ℝ^* ∧ 𝐴 ∈ ℝ^*) → (-∞ < 𝐴 ↔ ((((-∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ -∞ <_ℝ 𝐴) ∨ (-∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))))
8	5, 6, 7	sylancr 598	. 2 ⊢ (𝐴 ∈ ℝ → (-∞ < 𝐴 ↔ ((((-∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ -∞ <_ℝ 𝐴) ∨ (-∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))))
9	4, 8	mpbird 260	1 ⊢ (𝐴 ∈ ℝ → -∞ < 𝐴)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 = wceq 1570 ∈ wcel 2143 class class class wbr 5110 ℝcr 11100 <_ℝ cltrr 11105 +∞cpnf 11241 -∞cmnf 11242 ℝ^*cxr 11243 < clt 11244

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-ext 2735 ax-sep 5258 ax-pow 5338 ax-pr 5406 ax-un 7734 ax-cnex 11157

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-sb 2097 df-clab 2742 df-cleq 2755 df-clel 2838 df-ral 3080 df-rex 3090 df-rab 3417 df-v 3457 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-nul 4288 df-if 4489 df-pw 4565 df-sn 4591 df-pr 4593 df-op 4597 df-uni 4874 df-br 5111 df-opab 5175 df-xp 5669 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249

This theorem is referenced by: mnfltd 13150 mnflt0 13151 mnfltxr 13153 xrlttri 13165 xrlttr 13166 xrrebnd 13195 xrre3 13198 qbtwnxr 13227 xrsupsslem 13334 xrub 13339 elico2 13438 elicc2 13439 ioomax 13450 elioomnf 13472 difreicc 13512 icopnfcld 24905 iocmnfcld 24906 xrtgioo 24945 bndth 25098 mbfmax 25789 itg2seq 25882 ellogdm 26785 esumcvgsum 34459 dya2iocbrsiga 34646 dya2icobrsiga 34647 orvclteel 34844 iooelexlt 37989 itg2addnclem 38303 asindmre 38335 dvasin 38336 dvacos 38337 rfcnpre4 45737 infrpge 46050 infxr 46065 infxrunb2 46066 infleinflem2 46069 icccncfext 46584 fouriersw 46928 pimgtmnff 47419 iccpartigtl 48155

W3C validator