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 2739 | . . . 4 ⊢ +∞ = +∞ | |
2 | orc 866 | . . . 4 ⊢ ((𝐴 ∈ ℝ ∧ +∞ = +∞) → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))) | |
3 | 1, 2 | mpan2 691 | . . 3 ⊢ (𝐴 ∈ ℝ → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))) |
4 | 3 | olcd 873 | . 2 ⊢ (𝐴 ∈ ℝ → ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))) |
5 | rexr 10768 | . . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*) | |
6 | pnfxr 10776 | . . 3 ⊢ +∞ ∈ ℝ* | |
7 | ltxr 12596 | . . 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 846 = wceq 1542 ∈ wcel 2114 class class class wbr 5031 ℝcr 10617 <ℝ cltrr 10622 +∞cpnf 10753 -∞cmnf 10754 ℝ*cxr 10755 < clt 10756 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2711 ax-sep 5168 ax-nul 5175 ax-pow 5233 ax-pr 5297 ax-un 7482 ax-cnex 10674 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-sb 2075 df-clab 2718 df-cleq 2731 df-clel 2812 df-ral 3059 df-rex 3060 df-v 3401 df-dif 3847 df-un 3849 df-in 3851 df-ss 3861 df-nul 4213 df-if 4416 df-pw 4491 df-sn 4518 df-pr 4520 df-op 4524 df-uni 4798 df-br 5032 df-opab 5094 df-xp 5532 df-pnf 10758 df-xr 10760 df-ltxr 10761 |
This theorem is referenced by: ltpnfd 12602 0ltpnf 12603 xrlttri 12618 xrlttr 12619 xrrebnd 12647 xrre 12648 qbtwnxr 12679 xnn0lem1lt 12723 xrinfmsslem 12787 xrub 12791 supxrunb1 12798 supxrunb2 12799 dfrp2 12873 elioc2 12887 elicc2 12889 ioomax 12899 ioopos 12901 elioopnf 12920 elicopnf 12922 difreicc 12961 hashbnd 13791 hashv01gt1 13800 fprodge0 15442 fprodge1 15444 pcadd 16328 ramubcl 16457 rge0srg 20291 mnfnei 21975 icopnfcld 23523 iocmnfcld 23524 xrtgioo 23561 xrge0tsms 23589 ioombl1lem4 24316 icombl1 24318 mbfmax 24404 upgrfi 27039 topnfbey 28409 isblo3i 28739 htthlem 28855 xlt2addrd 30659 fsumrp0cl 30884 xrge0tsmsd 30897 pnfinf 31017 xrge0slmod 31123 xrge0iifcnv 31458 xrge0iifiso 31460 xrge0iifhom 31462 lmxrge0 31477 esumcst 31604 esumcvgre 31632 voliune 31770 volfiniune 31771 sxbrsigalem0 31811 orvcgteel 32007 dstfrvclim1 32017 itg2addnclem2 35475 asindmre 35506 dvasin 35507 dvacos 35508 rfcnpre3 42137 supxrgere 42433 supxrgelem 42437 xrlexaddrp 42452 infxr 42467 xrpnf 42589 limsupre 42747 limsuppnflem 42816 liminflelimsupuz 42891 limsupub2 42918 icccncfext 42993 fourierdlem111 43323 fourierdlem113 43325 fouriersw 43337 sge0iunmptlemre 43518 sge0rpcpnf 43524 sge0xaddlem1 43536 meaiuninclem 43583 hoidmvlelem5 43702 ovolval5lem1 43755 pimltpnf 43805 iccpartiltu 44438 itscnhlinecirc02p 45695 |
Copyright terms: Public domain | W3C validator |