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 13256

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 2760	. . . 4 ⊢ -∞ = -∞
2		olc 882	. . . 4 ⊢ ((-∞ = -∞ ∧ 𝐴 ∈ ℝ) → ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))
3	1, 2	mpan 703	. . 3 ⊢ (𝐴 ∈ ℝ → ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))
4	3	olcd 888	. 2 ⊢ (𝐴 ∈ ℝ → ((((-∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ -∞ <_ℝ 𝐴) ∨ (-∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ))))
5		mnfxr 11370	. . 3 ⊢ -∞ ∈ ℝ^*
6		rexr 11359	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ^*)
7		ltxr 13248	. . 3 ⊢ ((-∞ ∈ ℝ^* ∧ 𝐴 ∈ ℝ^*) → (-∞ < 𝐴 ↔ ((((-∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ -∞ <_ℝ 𝐴) ∨ (-∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))))
8	5, 6, 7	sylancr 599	. 2 ⊢ (𝐴 ∈ ℝ → (-∞ < 𝐴 ↔ ((((-∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ -∞ <_ℝ 𝐴) ∨ (-∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))))
9	4, 8	mpbird 260	1 ⊢ (𝐴 ∈ ℝ → -∞ < 𝐴)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 = wceq 1569 ∈ wcel 2144 class class class wbr 5102 ℝcr 11203 <_ℝ cltrr 11208 +∞cpnf 11344 -∞cmnf 11345 ℝ^*cxr 11346 < clt 11347

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-ext 2732 ax-sep 5248 ax-pow 5326 ax-pr 5390 ax-un 7752 ax-cnex 11260

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-sb 2099 df-clab 2739 df-cleq 2752 df-clel 2835 df-ral 3077 df-rex 3087 df-rab 3413 df-v 3452 df-ss 3896 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-br 5103 df-opab 5167 df-xp 5656 df-pnf 11349 df-mnf 11350 df-xr 11351 df-ltxr 11352

This theorem is used by: mnfltd 13257 mnflt0 13258 mnfltxr 13260 xrlttri 13272 xrlttr 13273 xrrebnd 13302 xrre3 13305 qbtwnxr 13334 xrsupsslem 13441 xrub 13446 elico2 13545 elicc2 13546 ioomax 13557 elioomnf 13579 difreicc 13619 icopnfcld 25092 iocmnfcld 25093 xrtgioo 25132 bndth 25285 mbfmax 25976 itg2seq 26069 ellogdm 26973 esumcvgsum 34767 dya2iocbrsiga 34954 dya2icobrsiga 34955 orvclteel 35152 iooelexlt 38379 itg2addnclem 38683 asindmre 38715 dvasin 38716 dvacos 38717 rfcnpre4 46145 infrpge 46457 infxr 46472 infxrunb2 46473 infleinflem2 46476 icccncfext 46991 fouriersw 47335 pimgtmnff 47826 iccpartigtl 48599

W3C validator