ltaddrp - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > ltaddrp		GIF version

Theorem ltaddrp 10027

Description: Adding a positive number to another number increases it. (Contributed by FL, 27-Dec-2007.)

**Assertion**
Ref	Expression
ltaddrp	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ⁺) → 𝐴 < (𝐴 + 𝐵))

**Proof of Theorem ltaddrp**
Step	Hyp	Ref	Expression
1		elrp 9991	. 2 ⊢ (𝐵 ∈ ℝ⁺ ↔ (𝐵 ∈ ℝ ∧ 0 < 𝐵))
2		ltaddpos 8728	. . . . 5 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (0 < 𝐵 ↔ 𝐴 < (𝐴 + 𝐵)))
3	2	biimpd 144	. . . 4 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (0 < 𝐵 → 𝐴 < (𝐴 + 𝐵)))
4	3	expcom 116	. . 3 ⊢ (𝐴 ∈ ℝ → (𝐵 ∈ ℝ → (0 < 𝐵 → 𝐴 < (𝐴 + 𝐵))))
5	4	imp32 257	. 2 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → 𝐴 < (𝐴 + 𝐵))
6	1, 5	sylan2b 287	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ⁺) → 𝐴 < (𝐴 + 𝐵))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ∈ wcel 2205 class class class wbr 4111 (class class class)co 6052 ℝcr 8128 0cc0 8129 + caddc 8132 < clt 8310 ℝ⁺crp 9989

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 619 ax-in2 620 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2207 ax-14 2208 ax-ext 2216 ax-sep 4230 ax-pow 4289 ax-pr 4324 ax-un 4556 ax-setind 4661 ax-cnex 8220 ax-resscn 8221 ax-1cn 8222 ax-1re 8223 ax-icn 8224 ax-addcl 8225 ax-addrcl 8226 ax-mulcl 8227 ax-addcom 8229 ax-addass 8231 ax-i2m1 8234 ax-0id 8237 ax-rnegex 8238 ax-pre-ltadd 8245

This theorem depends on definitions: df-bi 117 df-3an 1007 df-tru 1401 df-fal 1404 df-nf 1510 df-sb 1812 df-eu 2085 df-mo 2086 df-clab 2221 df-cleq 2227 df-clel 2230 df-nfc 2375 df-ne 2415 df-nel 2510 df-ral 2527 df-rex 2528 df-rab 2531 df-v 2817 df-dif 3215 df-un 3217 df-in 3219 df-ss 3226 df-pw 3673 df-sn 3697 df-pr 3698 df-op 3700 df-uni 3917 df-br 4112 df-opab 4174 df-xp 4757 df-iota 5314 df-fv 5362 df-ov 6055 df-pnf 8312 df-mnf 8313 df-ltxr 8315 df-rp 9990

This theorem is referenced by: ltaddrpd 10066 lswccatn0lsw 11303 qdenre 11891 efgt1 12387 ballotfilem2 13149 perfectlem2 15885

W3C validator