ltaddpos2 - Intuitionistic Logic Explorer

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

Theorem ltaddpos2 8525

Description: Adding a positive number to another number increases it. (Contributed by NM, 8-Apr-2005.)

**Assertion**
Ref	Expression
ltaddpos2	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < 𝐴 ↔ 𝐵 < (𝐴 + 𝐵)))

**Proof of Theorem ltaddpos2**
Step	Hyp	Ref	Expression
1		ltaddpos 8524	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < 𝐴 ↔ 𝐵 < (𝐵 + 𝐴)))
2		recn 8057	. . . 4 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
3		recn 8057	. . . 4 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
4		addcom 8208	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
5	2, 3, 4	syl2an 289	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
6	5	breq2d 4055	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 < (𝐴 + 𝐵) ↔ 𝐵 < (𝐵 + 𝐴)))
7	1, 6	bitr4d 191	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < 𝐴 ↔ 𝐵 < (𝐴 + 𝐵)))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 = wceq 1372 ∈ wcel 2175 class class class wbr 4043 (class class class)co 5943 ℂcc 7922 ℝcr 7923 0cc0 7924 + caddc 7927 < clt 8106

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 615 ax-in2 616 ax-io 710 ax-5 1469 ax-7 1470 ax-gen 1471 ax-ie1 1515 ax-ie2 1516 ax-8 1526 ax-10 1527 ax-11 1528 ax-i12 1529 ax-bndl 1531 ax-4 1532 ax-17 1548 ax-i9 1552 ax-ial 1556 ax-i5r 1557 ax-13 2177 ax-14 2178 ax-ext 2186 ax-sep 4161 ax-pow 4217 ax-pr 4252 ax-un 4479 ax-setind 4584 ax-cnex 8015 ax-resscn 8016 ax-1cn 8017 ax-1re 8018 ax-icn 8019 ax-addcl 8020 ax-addrcl 8021 ax-mulcl 8022 ax-addcom 8024 ax-addass 8026 ax-i2m1 8029 ax-0id 8032 ax-rnegex 8033 ax-pre-ltadd 8040

This theorem depends on definitions: df-bi 117 df-3an 982 df-tru 1375 df-fal 1378 df-nf 1483 df-sb 1785 df-eu 2056 df-mo 2057 df-clab 2191 df-cleq 2197 df-clel 2200 df-nfc 2336 df-ne 2376 df-nel 2471 df-ral 2488 df-rex 2489 df-rab 2492 df-v 2773 df-dif 3167 df-un 3169 df-in 3171 df-ss 3178 df-pw 3617 df-sn 3638 df-pr 3639 df-op 3641 df-uni 3850 df-br 4044 df-opab 4105 df-xp 4680 df-iota 5231 df-fv 5278 df-ov 5946 df-pnf 8108 df-mnf 8109 df-ltxr 8111

This theorem is referenced by: ltaddpos2d 8602 nn1gt1 9069 pockthi 12623

W3C validator