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 2821 | . . . 4 ⊢ +∞ = +∞ | |
2 | orc 863 | . . . 4 ⊢ ((𝐴 ∈ ℝ ∧ +∞ = +∞) → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))) | |
3 | 1, 2 | mpan2 689 | . . 3 ⊢ (𝐴 ∈ ℝ → ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ))) |
4 | 3 | olcd 870 | . 2 ⊢ (𝐴 ∈ ℝ → ((((𝐴 ∈ ℝ ∧ +∞ ∈ ℝ) ∧ 𝐴 <ℝ +∞) ∨ (𝐴 = -∞ ∧ +∞ = +∞)) ∨ ((𝐴 ∈ ℝ ∧ +∞ = +∞) ∨ (𝐴 = -∞ ∧ +∞ ∈ ℝ)))) |
5 | rexr 10681 | . . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*) | |
6 | pnfxr 10689 | . . 3 ⊢ +∞ ∈ ℝ* | |
7 | ltxr 12504 | . . 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 1533 ∈ wcel 2110 class class class wbr 5059 ℝcr 10530 <ℝ cltrr 10535 +∞cpnf 10666 -∞cmnf 10667 ℝ*cxr 10668 < clt 10669 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2156 ax-12 2172 ax-ext 2793 ax-sep 5196 ax-nul 5203 ax-pow 5259 ax-pr 5322 ax-un 7455 ax-cnex 10587 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3497 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4833 df-br 5060 df-opab 5122 df-xp 5556 df-pnf 10671 df-xr 10673 df-ltxr 10674 |
This theorem is referenced by: ltpnfd 12510 0ltpnf 12511 xrlttri 12526 xrlttr 12527 xrrebnd 12555 xrre 12556 qbtwnxr 12587 xnn0lem1lt 12631 xrinfmsslem 12695 xrub 12699 supxrunb1 12706 supxrunb2 12707 elioc2 12793 elicc2 12795 ioomax 12805 ioopos 12807 elioopnf 12825 elicopnf 12827 difreicc 12864 hashbnd 13690 hashv01gt1 13699 fprodge0 15341 fprodge1 15343 pcadd 16219 ramubcl 16348 rge0srg 20610 mnfnei 21823 icopnfcld 23370 iocmnfcld 23371 xrtgioo 23408 xrge0tsms 23436 ioombl1lem4 24156 icombl1 24158 mbfmax 24244 upgrfi 26870 topnfbey 28242 isblo3i 28572 htthlem 28688 xlt2addrd 30476 dfrp2 30485 fsumrp0cl 30677 xrge0tsmsd 30687 pnfinf 30807 xrge0slmod 30912 xrge0iifcnv 31171 xrge0iifiso 31173 xrge0iifhom 31175 lmxrge0 31190 esumcst 31317 esumcvgre 31345 voliune 31483 volfiniune 31484 sxbrsigalem0 31524 orvcgteel 31720 dstfrvclim1 31730 itg2addnclem2 34938 asindmre 34971 dvasin 34972 dvacos 34973 rfcnpre3 41283 supxrgere 41593 supxrgelem 41597 xrlexaddrp 41612 infxr 41627 xrpnf 41754 limsupre 41914 limsuppnfdlem 41974 limsuppnflem 41983 liminflelimsupuz 42058 limsupub2 42085 icccncfext 42162 fourierdlem111 42495 fourierdlem113 42497 fouriersw 42509 sge0iunmptlemre 42690 sge0rpcpnf 42696 sge0xaddlem1 42708 meaiuninclem 42755 hoidmvlelem5 42874 ovolval5lem1 42927 pimltpnf 42977 iccpartiltu 43575 itscnhlinecirc02p 44765 |
Copyright terms: Public domain | W3C validator |