![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mnflt | Structured version Visualization version GIF version |
Description: Minus infinity is less than any (finite) real. (Contributed by NM, 14-Oct-2005.) |
Ref | Expression |
---|---|
mnflt | ⊢ (𝐴 ∈ ℝ → -∞ < 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2793 | . . . 4 ⊢ -∞ = -∞ | |
2 | olc 863 | . . . 4 ⊢ ((-∞ = -∞ ∧ 𝐴 ∈ ℝ) → ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ))) | |
3 | 1, 2 | mpan 686 | . . 3 ⊢ (𝐴 ∈ ℝ → ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ))) |
4 | 3 | olcd 869 | . 2 ⊢ (𝐴 ∈ ℝ → ((((-∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ -∞ <ℝ 𝐴) ∨ (-∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ)))) |
5 | mnfxr 10534 | . . 3 ⊢ -∞ ∈ ℝ* | |
6 | rexr 10522 | . . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*) | |
7 | ltxr 12349 | . . 3 ⊢ ((-∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ*) → (-∞ < 𝐴 ↔ ((((-∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ -∞ <ℝ 𝐴) ∨ (-∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ))))) | |
8 | 5, 6, 7 | sylancr 587 | . 2 ⊢ (𝐴 ∈ ℝ → (-∞ < 𝐴 ↔ ((((-∞ ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ -∞ <ℝ 𝐴) ∨ (-∞ = -∞ ∧ 𝐴 = +∞)) ∨ ((-∞ ∈ ℝ ∧ 𝐴 = +∞) ∨ (-∞ = -∞ ∧ 𝐴 ∈ ℝ))))) |
9 | 4, 8 | mpbird 258 | 1 ⊢ (𝐴 ∈ ℝ → -∞ < 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 ∨ wo 842 = wceq 1520 ∈ wcel 2079 class class class wbr 4956 ℝcr 10371 <ℝ cltrr 10376 +∞cpnf 10507 -∞cmnf 10508 ℝ*cxr 10509 < clt 10510 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1775 ax-4 1789 ax-5 1886 ax-6 1945 ax-7 1990 ax-8 2081 ax-9 2089 ax-10 2110 ax-11 2124 ax-12 2139 ax-13 2342 ax-ext 2767 ax-sep 5088 ax-nul 5095 ax-pow 5150 ax-pr 5214 ax-un 7310 ax-cnex 10428 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1080 df-tru 1523 df-ex 1760 df-nf 1764 df-sb 2041 df-mo 2574 df-eu 2610 df-clab 2774 df-cleq 2786 df-clel 2861 df-nfc 2933 df-ral 3108 df-rex 3109 df-rab 3112 df-v 3434 df-dif 3857 df-un 3859 df-in 3861 df-ss 3869 df-nul 4207 df-if 4376 df-pw 4449 df-sn 4467 df-pr 4469 df-op 4473 df-uni 4740 df-br 4957 df-opab 5019 df-xp 5441 df-pnf 10512 df-mnf 10513 df-xr 10514 df-ltxr 10515 |
This theorem is referenced by: mnfltd 12358 mnflt0 12359 mnfltxr 12361 xrlttri 12371 xrlttr 12372 xrrebnd 12400 xrre3 12403 qbtwnxr 12432 xrsupsslem 12539 xrub 12544 elico2 12639 elicc2 12640 ioomax 12650 elioomnf 12671 difreicc 12709 icopnfcld 23047 iocmnfcld 23048 xrtgioo 23085 bndth 23233 mbfmax 23921 itg2seq 24014 ellogdm 24891 esumcvgsum 30920 dya2iocbrsiga 31106 dya2icobrsiga 31107 orvclteel 31303 iooelexlt 34120 itg2addnclem 34420 asindmre 34454 dvasin 34455 dvacos 34456 rfcnpre4 40782 infrpge 41113 infxr 41129 infxrunb2 41130 infleinflem2 41133 icccncfext 41665 fourierdlem113 42000 fouriersw 42012 iccpartigtl 43019 |
Copyright terms: Public domain | W3C validator |