![]() |
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 2778 | . . . 4 ⊢ +∞ = +∞ | |
2 | orc 856 | . . . 4 ⊢ ((𝐴 ∈ ℝ ∧ +∞ = +∞) → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))) | |
3 | 1, 2 | mpan2 681 | . . 3 ⊢ (𝐴 ∈ ℝ → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))) |
4 | 3 | olcd 863 | . 2 ⊢ (𝐴 ∈ ℝ → ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))) |
5 | rexr 10422 | . . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*) | |
6 | pnfxr 10430 | . . 3 ⊢ +∞ ∈ ℝ* | |
7 | ltxr 12260 | . . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))))) | |
8 | 5, 6, 7 | sylancl 580 | . 2 ⊢ (𝐴 ∈ ℝ → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))))) |
9 | 4, 8 | mpbird 249 | 1 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 386 ∨ wo 836 = wceq 1601 ∈ wcel 2107 class class class wbr 4886 ℝcr 10271 <ℝ cltrr 10276 +∞cpnf 10408 -∞cmnf 10409 ℝ*cxr 10410 < clt 10411 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-8 2109 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-sep 5017 ax-nul 5025 ax-pow 5077 ax-pr 5138 ax-un 7226 ax-cnex 10328 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2551 df-eu 2587 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ral 3095 df-rex 3096 df-rab 3099 df-v 3400 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-pw 4381 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4672 df-br 4887 df-opab 4949 df-xp 5361 df-pnf 10413 df-xr 10415 df-ltxr 10416 |
This theorem is referenced by: ltpnfd 12266 0ltpnf 12267 xrlttri 12282 xrlttr 12283 xrrebnd 12311 xrre 12312 qbtwnxr 12343 xrinfmsslem 12450 xrub 12454 supxrunb1 12461 supxrunb2 12462 elioc2 12548 elicc2 12550 ioomax 12560 ioopos 12562 elioopnf 12580 elicopnf 12582 difreicc 12621 hashbnd 13441 hashv01gt1 13450 fprodge0 15126 fprodge1 15128 pcadd 15997 ramubcl 16126 rge0srg 20213 mnfnei 21433 xblss2ps 22614 icopnfcld 22979 iocmnfcld 22980 blcvx 23009 xrtgioo 23017 reconnlem1 23037 xrge0tsms 23045 iccpnfhmeo 23152 ioombl1lem4 23765 icombl1 23767 uniioombllem1 23785 mbfmax 23853 ismbf3d 23858 itg2seq 23946 lhop2 24215 dvfsumlem2 24227 logccv 24846 xrlimcnp 25147 pntleme 25749 upgrfi 26439 topnfbey 27900 isblo3i 28228 htthlem 28346 xlt2addrd 30088 dfrp2 30097 fsumrp0cl 30257 pnfinf 30299 xrge0tsmsd 30347 xrge0slmod 30406 xrge0iifcnv 30577 xrge0iifiso 30579 xrge0iifhom 30581 lmxrge0 30596 esumcst 30723 esumcvgre 30751 voliune 30890 volfiniune 30891 sxbrsigalem0 30931 orvcgteel 31128 dstfrvclim1 31138 itg2addnclem2 34087 asindmre 34120 dvasin 34121 dvacos 34122 rfcnpre3 40125 supxrgere 40457 supxrgelem 40461 xrlexaddrp 40476 infxr 40491 xrpnf 40621 limsupre 40781 limsuppnfdlem 40841 limsuppnflem 40850 liminflelimsupuz 40925 limsupub2 40952 icccncfext 41028 fourierdlem111 41361 fourierdlem113 41363 fouriersw 41375 sge0iunmptlemre 41556 sge0rpcpnf 41562 sge0xaddlem1 41574 meaiuninclem 41621 hoidmvlelem5 41740 ovolval5lem1 41793 pimltpnf 41843 iccpartiltu 42390 itscnhlinecirc02p 43521 |
Copyright terms: Public domain | W3C validator |