![]() |
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 2725 | . . . 4 ⊢ +∞ = +∞ | |
2 | orc 865 | . . . 4 ⊢ ((𝐴 ∈ ℝ ∧ +∞ = +∞) → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))) | |
3 | 1, 2 | mpan2 689 | . . 3 ⊢ (𝐴 ∈ ℝ → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))) |
4 | 3 | olcd 872 | . 2 ⊢ (𝐴 ∈ ℝ → ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))) |
5 | rexr 11297 | . . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*) | |
6 | pnfxr 11305 | . . 3 ⊢ +∞ ∈ ℝ* | |
7 | ltxr 13135 | . . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))))) | |
8 | 5, 6, 7 | sylancl 584 | . 2 ⊢ (𝐴 ∈ ℝ → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))))) |
9 | 4, 8 | mpbird 256 | 1 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 ∨ wo 845 = wceq 1533 ∈ wcel 2098 class class class wbr 5149 ℝcr 11144 <ℝ cltrr 11149 +∞cpnf 11282 -∞cmnf 11283 ℝ*cxr 11284 < clt 11285 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 ax-sep 5300 ax-nul 5307 ax-pow 5365 ax-pr 5429 ax-un 7741 ax-cnex 11201 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-ral 3051 df-rex 3060 df-rab 3419 df-v 3463 df-dif 3947 df-un 3949 df-ss 3961 df-nul 4323 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4910 df-br 5150 df-opab 5212 df-xp 5684 df-pnf 11287 df-xr 11289 df-ltxr 11290 |
This theorem is referenced by: ltpnfd 13141 0ltpnf 13142 xrlttri 13158 xrlttr 13159 xrrebnd 13187 xrre 13188 qbtwnxr 13219 xnn0lem1lt 13263 xrinfmsslem 13327 xrub 13331 supxrunb1 13338 supxrunb2 13339 dfrp2 13413 elioc2 13427 elicc2 13429 ioomax 13439 ioopos 13441 elioopnf 13460 elicopnf 13462 difreicc 13501 hashbnd 14336 hashv01gt1 14345 fprodge0 15978 fprodge1 15980 pcadd 16866 ramubcl 16995 rge0srg 21393 mnfnei 23174 icopnfcld 24733 iocmnfcld 24734 xrtgioo 24771 xrge0tsms 24799 ioombl1lem4 25539 icombl1 25541 mbfmax 25627 upgrfi 28981 topnfbey 30356 isblo3i 30688 htthlem 30804 xlt2addrd 32615 fsumrp0cl 32845 xrge0tsmsd 32866 pnfinf 32988 xrge0slmod 33164 xrge0iifcnv 33667 xrge0iifiso 33669 xrge0iifhom 33671 lmxrge0 33686 esumcst 33815 esumcvgre 33843 voliune 33981 volfiniune 33982 sxbrsigalem0 34024 orvcgteel 34220 dstfrvclim1 34230 itg2addnclem2 37278 asindmre 37309 dvasin 37310 dvacos 37311 rfcnpre3 44539 supxrgere 44855 supxrgelem 44859 xrlexaddrp 44874 infxr 44889 xrpnf 45008 limsupre 45169 limsuppnflem 45238 liminflelimsupuz 45313 limsupub2 45340 icccncfext 45415 fourierdlem111 45745 fourierdlem113 45747 fouriersw 45759 sge0iunmptlemre 45943 sge0rpcpnf 45949 sge0xaddlem1 45961 meaiuninclem 46008 hoidmvlelem5 46127 ovolval5lem1 46180 pimltpnff 46231 iccpartiltu 46901 itscnhlinecirc02p 48046 |
Copyright terms: Public domain | W3C validator |