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 2823 | . . . 4 ⊢ +∞ = +∞ | |
2 | orc 863 | . . . 4 ⊢ ((𝐴 ∈ ℝ ∧ +∞ = +∞) → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))) | |
3 | 1, 2 | mpan2 689 | . . 3 ⊢ (𝐴 ∈ ℝ → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))) |
4 | 3 | olcd 870 | . 2 ⊢ (𝐴 ∈ ℝ → ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))) |
5 | rexr 10689 | . . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*) | |
6 | pnfxr 10697 | . . 3 ⊢ +∞ ∈ ℝ* | |
7 | ltxr 12513 | . . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))))) | |
8 | 5, 6, 7 | sylancl 588 | . 2 ⊢ (𝐴 ∈ ℝ → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))))) |
9 | 4, 8 | mpbird 259 | 1 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∨ wo 843 = wceq 1537 ∈ wcel 2114 class class class wbr 5068 ℝcr 10538 <ℝ cltrr 10543 +∞cpnf 10674 -∞cmnf 10675 ℝ*cxr 10676 < clt 10677 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 ax-sep 5205 ax-nul 5212 ax-pow 5268 ax-pr 5332 ax-un 7463 ax-cnex 10595 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ral 3145 df-rex 3146 df-rab 3149 df-v 3498 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-nul 4294 df-if 4470 df-pw 4543 df-sn 4570 df-pr 4572 df-op 4576 df-uni 4841 df-br 5069 df-opab 5131 df-xp 5563 df-pnf 10679 df-xr 10681 df-ltxr 10682 |
This theorem is referenced by: ltpnfd 12519 0ltpnf 12520 xrlttri 12535 xrlttr 12536 xrrebnd 12564 xrre 12565 qbtwnxr 12596 xnn0lem1lt 12640 xrinfmsslem 12704 xrub 12708 supxrunb1 12715 supxrunb2 12716 elioc2 12802 elicc2 12804 ioomax 12814 ioopos 12816 elioopnf 12834 elicopnf 12836 difreicc 12873 hashbnd 13699 hashv01gt1 13708 fprodge0 15349 fprodge1 15351 pcadd 16227 ramubcl 16356 rge0srg 20618 mnfnei 21831 icopnfcld 23378 iocmnfcld 23379 xrtgioo 23416 xrge0tsms 23444 ioombl1lem4 24164 icombl1 24166 mbfmax 24252 upgrfi 26878 topnfbey 28250 isblo3i 28580 htthlem 28696 xlt2addrd 30484 dfrp2 30493 fsumrp0cl 30684 xrge0tsmsd 30694 pnfinf 30814 xrge0slmod 30919 xrge0iifcnv 31178 xrge0iifiso 31180 xrge0iifhom 31182 lmxrge0 31197 esumcst 31324 esumcvgre 31352 voliune 31490 volfiniune 31491 sxbrsigalem0 31531 orvcgteel 31727 dstfrvclim1 31737 itg2addnclem2 34946 asindmre 34979 dvasin 34980 dvacos 34981 rfcnpre3 41297 supxrgere 41608 supxrgelem 41612 xrlexaddrp 41627 infxr 41642 xrpnf 41769 limsupre 41929 limsuppnflem 41998 liminflelimsupuz 42073 limsupub2 42100 icccncfext 42177 fourierdlem111 42509 fourierdlem113 42511 fouriersw 42523 sge0iunmptlemre 42704 sge0rpcpnf 42710 sge0xaddlem1 42722 meaiuninclem 42769 hoidmvlelem5 42888 ovolval5lem1 42941 pimltpnf 42991 iccpartiltu 43589 itscnhlinecirc02p 44779 |
Copyright terms: Public domain | W3C validator |