![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ltaddrp | Structured version Visualization version GIF version |
Description: Adding a positive number to another number increases it. (Contributed by FL, 27-Dec-2007.) |
Ref | Expression |
---|---|
ltaddrp | ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → 𝐴 < (𝐴 + 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elrp 11916 | . 2 ⊢ (𝐵 ∈ ℝ+ ↔ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) | |
2 | ltaddpos 10599 | . . . . 5 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (0 < 𝐵 ↔ 𝐴 < (𝐴 + 𝐵))) | |
3 | 2 | biimpd 219 | . . . 4 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (0 < 𝐵 → 𝐴 < (𝐴 + 𝐵))) |
4 | 3 | expcom 450 | . . 3 ⊢ (𝐴 ∈ ℝ → (𝐵 ∈ ℝ → (0 < 𝐵 → 𝐴 < (𝐴 + 𝐵)))) |
5 | 4 | imp32 448 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → 𝐴 < (𝐴 + 𝐵)) |
6 | 1, 5 | sylan2b 493 | 1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → 𝐴 < (𝐴 + 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∈ wcel 2071 class class class wbr 4728 (class class class)co 6733 ℝcr 10016 0cc0 10017 + caddc 10020 < clt 10155 ℝ+crp 11914 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1818 ax-5 1920 ax-6 1986 ax-7 2022 ax-8 2073 ax-9 2080 ax-10 2100 ax-11 2115 ax-12 2128 ax-13 2323 ax-ext 2672 ax-sep 4857 ax-nul 4865 ax-pow 4916 ax-pr 4979 ax-un 7034 ax-resscn 10074 ax-1cn 10075 ax-icn 10076 ax-addcl 10077 ax-addrcl 10078 ax-mulcl 10079 ax-mulrcl 10080 ax-mulcom 10081 ax-addass 10082 ax-mulass 10083 ax-distr 10084 ax-i2m1 10085 ax-1ne0 10086 ax-1rid 10087 ax-rnegex 10088 ax-rrecex 10089 ax-cnre 10090 ax-pre-lttri 10091 ax-pre-lttrn 10092 ax-pre-ltadd 10093 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1567 df-ex 1786 df-nf 1791 df-sb 1979 df-eu 2543 df-mo 2544 df-clab 2679 df-cleq 2685 df-clel 2688 df-nfc 2823 df-ne 2865 df-nel 2968 df-ral 2987 df-rex 2988 df-rab 2991 df-v 3274 df-sbc 3510 df-csb 3608 df-dif 3651 df-un 3653 df-in 3655 df-ss 3662 df-nul 3992 df-if 4163 df-pw 4236 df-sn 4254 df-pr 4256 df-op 4260 df-uni 4513 df-br 4729 df-opab 4789 df-mpt 4806 df-id 5096 df-po 5107 df-so 5108 df-xp 5192 df-rel 5193 df-cnv 5194 df-co 5195 df-dm 5196 df-rn 5197 df-res 5198 df-ima 5199 df-iota 5932 df-fun 5971 df-fn 5972 df-f 5973 df-f1 5974 df-fo 5975 df-f1o 5976 df-fv 5977 df-ov 6736 df-er 7830 df-en 8041 df-dom 8042 df-sdom 8043 df-pnf 10157 df-mnf 10158 df-ltxr 10160 df-rp 11915 |
This theorem is referenced by: ltaddrpd 11987 lswccatn0lsw 13452 efgt1 14934 efgsfo 18241 efgredlemd 18246 efgredlem 18249 iccntr 22714 reconnlem2 22720 opnreen 22724 minveclem3b 23288 logimul 24448 emcllem2 24811 emcllem4 24813 emcllem6 24815 perfectlem2 25043 bclbnd 25093 pntibndlem1 25366 pntlemd 25371 pntlemc 25372 pntlemr 25379 pntlemp 25387 smcnlem 27750 dp2ltc 29792 dpgti 29812 ballotlem2 30748 poimir 33642 stoweidlem59 40664 perfectALTVlem2 42026 |
Copyright terms: Public domain | W3C validator |