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 2738 | . . . 4 ⊢ +∞ = +∞ | |
2 | orc 864 | . . . 4 ⊢ ((𝐴 ∈ ℝ ∧ +∞ = +∞) → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))) | |
3 | 1, 2 | mpan2 688 | . . 3 ⊢ (𝐴 ∈ ℝ → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))) |
4 | 3 | olcd 871 | . 2 ⊢ (𝐴 ∈ ℝ → ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))) |
5 | rexr 11021 | . . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*) | |
6 | pnfxr 11029 | . . 3 ⊢ +∞ ∈ ℝ* | |
7 | ltxr 12851 | . . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))))) | |
8 | 5, 6, 7 | sylancl 586 | . 2 ⊢ (𝐴 ∈ ℝ → (𝐴 < +∞ ↔ ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))))) |
9 | 4, 8 | mpbird 256 | 1 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 844 = wceq 1539 ∈ wcel 2106 class class class wbr 5074 ℝcr 10870 <ℝ cltrr 10875 +∞cpnf 11006 -∞cmnf 11007 ℝ*cxr 11008 < clt 11009 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 ax-cnex 10927 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-ral 3069 df-rex 3070 df-rab 3073 df-v 3434 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-br 5075 df-opab 5137 df-xp 5595 df-pnf 11011 df-xr 11013 df-ltxr 11014 |
This theorem is referenced by: ltpnfd 12857 0ltpnf 12858 xrlttri 12873 xrlttr 12874 xrrebnd 12902 xrre 12903 qbtwnxr 12934 xnn0lem1lt 12978 xrinfmsslem 13042 xrub 13046 supxrunb1 13053 supxrunb2 13054 dfrp2 13128 elioc2 13142 elicc2 13144 ioomax 13154 ioopos 13156 elioopnf 13175 elicopnf 13177 difreicc 13216 hashbnd 14050 hashv01gt1 14059 fprodge0 15703 fprodge1 15705 pcadd 16590 ramubcl 16719 rge0srg 20669 mnfnei 22372 icopnfcld 23931 iocmnfcld 23932 xrtgioo 23969 xrge0tsms 23997 ioombl1lem4 24725 icombl1 24727 mbfmax 24813 upgrfi 27461 topnfbey 28833 isblo3i 29163 htthlem 29279 xlt2addrd 31081 fsumrp0cl 31304 xrge0tsmsd 31317 pnfinf 31437 xrge0slmod 31548 xrge0iifcnv 31883 xrge0iifiso 31885 xrge0iifhom 31887 lmxrge0 31902 esumcst 32031 esumcvgre 32059 voliune 32197 volfiniune 32198 sxbrsigalem0 32238 orvcgteel 32434 dstfrvclim1 32444 itg2addnclem2 35829 asindmre 35860 dvasin 35861 dvacos 35862 rfcnpre3 42576 supxrgere 42872 supxrgelem 42876 xrlexaddrp 42891 infxr 42906 xrpnf 43026 limsupre 43182 limsuppnflem 43251 liminflelimsupuz 43326 limsupub2 43353 icccncfext 43428 fourierdlem111 43758 fourierdlem113 43760 fouriersw 43772 sge0iunmptlemre 43953 sge0rpcpnf 43959 sge0xaddlem1 43971 meaiuninclem 44018 hoidmvlelem5 44137 ovolval5lem1 44190 pimltpnf 44241 iccpartiltu 44874 itscnhlinecirc02p 46131 |
Copyright terms: Public domain | W3C validator |