![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ltpnf | Structured version Visualization version GIF version |
Description: Any (finite) real is less than plus infinity. (Contributed by NM, 14-Oct-2005.) |
Ref | Expression |
---|---|
ltpnf | ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2798 | . . . 4 ⊢ +∞ = +∞ | |
2 | orc 864 | . . . 4 ⊢ ((𝐴 ∈ ℝ ∧ +∞ = +∞) → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))) | |
3 | 1, 2 | mpan2 690 | . . 3 ⊢ (𝐴 ∈ ℝ → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))) |
4 | 3 | olcd 871 | . 2 ⊢ (𝐴 ∈ ℝ → ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))) |
5 | rexr 10676 | . . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*) | |
6 | pnfxr 10684 | . . 3 ⊢ +∞ ∈ ℝ* | |
7 | ltxr 12498 | . . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))))) | |
8 | 5, 6, 7 | sylancl 589 | . 2 ⊢ (𝐴 ∈ ℝ → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))))) |
9 | 4, 8 | mpbird 260 | 1 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∨ wo 844 = wceq 1538 ∈ wcel 2111 class class class wbr 5030 ℝcr 10525 <ℝ cltrr 10530 +∞cpnf 10661 -∞cmnf 10662 ℝ*cxr 10663 < clt 10664 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441 ax-cnex 10582 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ral 3111 df-rex 3112 df-v 3443 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-br 5031 df-opab 5093 df-xp 5525 df-pnf 10666 df-xr 10668 df-ltxr 10669 |
This theorem is referenced by: ltpnfd 12504 0ltpnf 12505 xrlttri 12520 xrlttr 12521 xrrebnd 12549 xrre 12550 qbtwnxr 12581 xnn0lem1lt 12625 xrinfmsslem 12689 xrub 12693 supxrunb1 12700 supxrunb2 12701 elioc2 12788 elicc2 12790 ioomax 12800 ioopos 12802 elioopnf 12821 elicopnf 12823 difreicc 12862 hashbnd 13692 hashv01gt1 13701 fprodge0 15339 fprodge1 15341 pcadd 16215 ramubcl 16344 rge0srg 20162 mnfnei 21826 icopnfcld 23373 iocmnfcld 23374 xrtgioo 23411 xrge0tsms 23439 ioombl1lem4 24165 icombl1 24167 mbfmax 24253 upgrfi 26884 topnfbey 28254 isblo3i 28584 htthlem 28700 xlt2addrd 30508 dfrp2 30517 fsumrp0cl 30729 xrge0tsmsd 30742 pnfinf 30862 xrge0slmod 30968 xrge0iifcnv 31286 xrge0iifiso 31288 xrge0iifhom 31290 lmxrge0 31305 esumcst 31432 esumcvgre 31460 voliune 31598 volfiniune 31599 sxbrsigalem0 31639 orvcgteel 31835 dstfrvclim1 31845 itg2addnclem2 35109 asindmre 35140 dvasin 35141 dvacos 35142 rfcnpre3 41662 supxrgere 41965 supxrgelem 41969 xrlexaddrp 41984 infxr 41999 xrpnf 42125 limsupre 42283 limsuppnflem 42352 liminflelimsupuz 42427 limsupub2 42454 icccncfext 42529 fourierdlem111 42859 fourierdlem113 42861 fouriersw 42873 sge0iunmptlemre 43054 sge0rpcpnf 43060 sge0xaddlem1 43072 meaiuninclem 43119 hoidmvlelem5 43238 ovolval5lem1 43291 pimltpnf 43341 iccpartiltu 43939 itscnhlinecirc02p 45199 |
Copyright terms: Public domain | W3C validator |