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 13119

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 2761	. . . 4 ⊢ -∞ = -∞
2		olc 879	. . . 4 ⊢ ((-∞ = -∞ ∧ 𝐴 ∈ ℝ) → ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))
3	1, 2	mpan 700	. . 3 ⊢ (𝐴 ∈ ℝ → ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))
4	3	olcd 885	. 2 ⊢ (𝐴 ∈ ℝ → ((((-∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ -∞ <_ℝ 𝐴) ∨ (-∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ))))
5		mnfxr 11233	. . 3 ⊢ -∞ ∈ ℝ^*
6		rexr 11222	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ^*)
7		ltxr 13111	. . 3 ⊢ ((-∞ ∈ ℝ^* ∧ 𝐴 ∈ ℝ^*) → (-∞ < 𝐴 ↔ ((((-∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ -∞ <_ℝ 𝐴) ∨ (-∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))))
8	5, 6, 7	sylancr 596	. 2 ⊢ (𝐴 ∈ ℝ → (-∞ < 𝐴 ↔ ((((-∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ -∞ <_ℝ 𝐴) ∨ (-∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))))
9	4, 8	mpbird 259	1 ⊢ (𝐴 ∈ ℝ → -∞ < 𝐴)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 399 ∨ wo 858 = wceq 1559 ∈ wcel 2141 class class class wbr 5097 ℝcr 11066 <_ℝ cltrr 11071 +∞cpnf 11207 -∞cmnf 11208 ℝ^*cxr 11209 < clt 11210

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-ext 2733 ax-sep 5243 ax-pow 5319 ax-pr 5387 ax-un 7713 ax-cnex 11123

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-sb 2090 df-clab 2740 df-cleq 2753 df-clel 2836 df-ral 3076 df-rex 3086 df-rab 3414 df-v 3455 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4863 df-br 5098 df-opab 5160 df-xp 5649 df-pnf 11212 df-mnf 11213 df-xr 11214 df-ltxr 11215

This theorem is referenced by: mnfltd 13120 mnflt0 13121 mnfltxr 13123 xrlttri 13135 xrlttr 13136 xrrebnd 13165 xrre3 13168 qbtwnxr 13197 xrsupsslem 13304 xrub 13309 elico2 13408 elicc2 13409 ioomax 13420 elioomnf 13442 difreicc 13482 icopnfcld 24815 iocmnfcld 24816 xrtgioo 24855 bndth 25008 mbfmax 25699 itg2seq 25792 ellogdm 26692 esumcvgsum 34346 dya2iocbrsiga 34533 dya2icobrsiga 34534 orvclteel 34731 iooelexlt 37817 itg2addnclem 38131 asindmre 38163 dvasin 38164 dvacos 38165 rfcnpre4 45575 infrpge 45888 infxr 45903 infxrunb2 45904 infleinflem2 45907 icccncfext 46422 fouriersw 46766 pimgtmnff 47257 iccpartigtl 47990

W3C validator