Theorem List for Intuitionistic Logic Explorer - 8101-8200 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | addrsub 8101 |
Right-subtraction: Subtraction of the right summand from the result of
an addition. (Contributed by BJ, 6-Jun-2019.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) = 𝐶 ↔ 𝐵 = (𝐶 − 𝐴))) |
|
Theorem | subexsub 8102 |
A subtraction law: Exchanging the subtrahend and the result of the
subtraction. (Contributed by BJ, 6-Jun-2019.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 = (𝐶 − 𝐵) ↔ 𝐵 = (𝐶 − 𝐴))) |
|
Theorem | addid0 8103 |
If adding a number to a another number yields the other number, the added
number must be 0. This shows that 0 is the unique (right)
identity of the complex numbers. (Contributed by AV, 17-Jan-2021.)
|
⊢ ((𝑋 ∈ ℂ ∧ 𝑌 ∈ ℂ) → ((𝑋 + 𝑌) = 𝑋 ↔ 𝑌 = 0)) |
|
Theorem | addn0nid 8104 |
Adding a nonzero number to a complex number does not yield the complex
number. (Contributed by AV, 17-Jan-2021.)
|
⊢ ((𝑋 ∈ ℂ ∧ 𝑌 ∈ ℂ ∧ 𝑌 ≠ 0) → (𝑋 + 𝑌) ≠ 𝑋) |
|
Theorem | pnpncand 8105 |
Addition/subtraction cancellation law. (Contributed by Scott Fenton,
14-Dec-2017.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + (𝐵 − 𝐶)) + (𝐶 − 𝐵)) = 𝐴) |
|
Theorem | subeqrev 8106 |
Reverse the order of subtraction in an equality. (Contributed by Scott
Fenton, 8-Jul-2013.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 − 𝐵) = (𝐶 − 𝐷) ↔ (𝐵 − 𝐴) = (𝐷 − 𝐶))) |
|
Theorem | pncan1 8107 |
Cancellation law for addition and subtraction with 1. (Contributed by
Alexander van der Vekens, 3-Oct-2018.)
|
⊢ (𝐴 ∈ ℂ → ((𝐴 + 1) − 1) = 𝐴) |
|
Theorem | npcan1 8108 |
Cancellation law for subtraction and addition with 1. (Contributed by
Alexander van der Vekens, 5-Oct-2018.)
|
⊢ (𝐴 ∈ ℂ → ((𝐴 − 1) + 1) = 𝐴) |
|
Theorem | subeq0bd 8109 |
If two complex numbers are equal, their difference is zero. Consequence
of subeq0ad 8051. Converse of subeq0d 8049. Contrapositive of subne0ad 8052.
(Contributed by David Moews, 28-Feb-2017.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 − 𝐵) = 0) |
|
Theorem | renegcld 8110 |
Closure law for negative of reals. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ)
⇒ ⊢ (𝜑 → -𝐴 ∈ ℝ) |
|
Theorem | resubcld 8111 |
Closure law for subtraction of reals. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ)
⇒ ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℝ) |
|
Theorem | negf1o 8112* |
Negation is an isomorphism of a subset of the real numbers to the
negated elements of the subset. (Contributed by AV, 9-Aug-2020.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ -𝑥) ⇒ ⊢ (𝐴 ⊆ ℝ → 𝐹:𝐴–1-1-onto→{𝑛 ∈ ℝ ∣ -𝑛 ∈ 𝐴}) |
|
4.3.3 Multiplication
|
|
Theorem | kcnktkm1cn 8113 |
k times k minus 1 is a complex number if k is a complex number.
(Contributed by Alexander van der Vekens, 11-Mar-2018.)
|
⊢ (𝐾 ∈ ℂ → (𝐾 · (𝐾 − 1)) ∈
ℂ) |
|
Theorem | muladd 8114 |
Product of two sums. (Contributed by NM, 14-Jan-2006.) (Proof shortened
by Andrew Salmon, 19-Nov-2011.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) · (𝐶 + 𝐷)) = (((𝐴 · 𝐶) + (𝐷 · 𝐵)) + ((𝐴 · 𝐷) + (𝐶 · 𝐵)))) |
|
Theorem | subdi 8115 |
Distribution of multiplication over subtraction. Theorem I.5 of [Apostol]
p. 18. (Contributed by NM, 18-Nov-2004.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 − 𝐶)) = ((𝐴 · 𝐵) − (𝐴 · 𝐶))) |
|
Theorem | subdir 8116 |
Distribution of multiplication over subtraction. Theorem I.5 of [Apostol]
p. 18. (Contributed by NM, 30-Dec-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) · 𝐶) = ((𝐴 · 𝐶) − (𝐵 · 𝐶))) |
|
Theorem | mul02 8117 |
Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed
by NM, 10-Aug-1999.)
|
⊢ (𝐴 ∈ ℂ → (0 · 𝐴) = 0) |
|
Theorem | mul02lem2 8118 |
Zero times a real is zero. Although we prove it as a corollary of
mul02 8117, the name is for consistency with the
Metamath Proof Explorer
which proves it before mul02 8117. (Contributed by Scott Fenton,
3-Jan-2013.)
|
⊢ (𝐴 ∈ ℝ → (0 · 𝐴) = 0) |
|
Theorem | mul01 8119 |
Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed
by NM, 15-May-1999.) (Revised by Scott Fenton, 3-Jan-2013.)
|
⊢ (𝐴 ∈ ℂ → (𝐴 · 0) = 0) |
|
Theorem | mul02i 8120 |
Multiplication by 0. Theorem I.6 of [Apostol]
p. 18. (Contributed by
NM, 23-Nov-1994.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (0 · 𝐴) = 0 |
|
Theorem | mul01i 8121 |
Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed
by NM, 23-Nov-1994.) (Revised by Scott Fenton, 3-Jan-2013.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (𝐴 · 0) = 0 |
|
Theorem | mul02d 8122 |
Multiplication by 0. Theorem I.6 of [Apostol]
p. 18. (Contributed by
Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (0 · 𝐴) = 0) |
|
Theorem | mul01d 8123 |
Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed
by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 · 0) = 0) |
|
Theorem | ine0 8124 |
The imaginary unit i is not zero. (Contributed by NM,
6-May-1999.)
|
⊢ i ≠ 0 |
|
Theorem | mulneg1 8125 |
Product with negative is negative of product. Theorem I.12 of [Apostol]
p. 18. (Contributed by NM, 14-May-1999.) (Proof shortened by Mario
Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 · 𝐵) = -(𝐴 · 𝐵)) |
|
Theorem | mulneg2 8126 |
The product with a negative is the negative of the product. (Contributed
by NM, 30-Jul-2004.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · -𝐵) = -(𝐴 · 𝐵)) |
|
Theorem | mulneg12 8127 |
Swap the negative sign in a product. (Contributed by NM, 30-Jul-2004.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 · 𝐵) = (𝐴 · -𝐵)) |
|
Theorem | mul2neg 8128 |
Product of two negatives. Theorem I.12 of [Apostol] p. 18. (Contributed
by NM, 30-Jul-2004.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 · -𝐵) = (𝐴 · 𝐵)) |
|
Theorem | submul2 8129 |
Convert a subtraction to addition using multiplication by a negative.
(Contributed by NM, 2-Feb-2007.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 − (𝐵 · 𝐶)) = (𝐴 + (𝐵 · -𝐶))) |
|
Theorem | mulm1 8130 |
Product with minus one is negative. (Contributed by NM, 16-Nov-1999.)
|
⊢ (𝐴 ∈ ℂ → (-1 · 𝐴) = -𝐴) |
|
Theorem | mulsub 8131 |
Product of two differences. (Contributed by NM, 14-Jan-2006.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 − 𝐵) · (𝐶 − 𝐷)) = (((𝐴 · 𝐶) + (𝐷 · 𝐵)) − ((𝐴 · 𝐷) + (𝐶 · 𝐵)))) |
|
Theorem | mulsub2 8132 |
Swap the order of subtraction in a multiplication. (Contributed by Scott
Fenton, 24-Jun-2013.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 − 𝐵) · (𝐶 − 𝐷)) = ((𝐵 − 𝐴) · (𝐷 − 𝐶))) |
|
Theorem | mulm1i 8133 |
Product with minus one is negative. (Contributed by NM,
31-Jul-1999.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (-1 · 𝐴) = -𝐴 |
|
Theorem | mulneg1i 8134 |
Product with negative is negative of product. Theorem I.12 of [Apostol]
p. 18. (Contributed by NM, 10-Feb-1995.) (Revised by Mario Carneiro,
27-May-2016.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ (-𝐴 · 𝐵) = -(𝐴 · 𝐵) |
|
Theorem | mulneg2i 8135 |
Product with negative is negative of product. (Contributed by NM,
31-Jul-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ (𝐴 · -𝐵) = -(𝐴 · 𝐵) |
|
Theorem | mul2negi 8136 |
Product of two negatives. Theorem I.12 of [Apostol] p. 18.
(Contributed by NM, 14-Feb-1995.) (Revised by Mario Carneiro,
27-May-2016.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ (-𝐴 · -𝐵) = (𝐴 · 𝐵) |
|
Theorem | subdii 8137 |
Distribution of multiplication over subtraction. Theorem I.5 of
[Apostol] p. 18. (Contributed by NM,
26-Nov-1994.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈
ℂ ⇒ ⊢ (𝐴 · (𝐵 − 𝐶)) = ((𝐴 · 𝐵) − (𝐴 · 𝐶)) |
|
Theorem | subdiri 8138 |
Distribution of multiplication over subtraction. Theorem I.5 of
[Apostol] p. 18. (Contributed by NM,
8-May-1999.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈
ℂ ⇒ ⊢ ((𝐴 − 𝐵) · 𝐶) = ((𝐴 · 𝐶) − (𝐵 · 𝐶)) |
|
Theorem | muladdi 8139 |
Product of two sums. (Contributed by NM, 17-May-1999.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐷 ∈
ℂ ⇒ ⊢ ((𝐴 + 𝐵) · (𝐶 + 𝐷)) = (((𝐴 · 𝐶) + (𝐷 · 𝐵)) + ((𝐴 · 𝐷) + (𝐶 · 𝐵))) |
|
Theorem | mulm1d 8140 |
Product with minus one is negative. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (-1 · 𝐴) = -𝐴) |
|
Theorem | mulneg1d 8141 |
Product with negative is negative of product. Theorem I.12 of [Apostol]
p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (-𝐴 · 𝐵) = -(𝐴 · 𝐵)) |
|
Theorem | mulneg2d 8142 |
Product with negative is negative of product. (Contributed by Mario
Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 · -𝐵) = -(𝐴 · 𝐵)) |
|
Theorem | mul2negd 8143 |
Product of two negatives. Theorem I.12 of [Apostol] p. 18.
(Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (-𝐴 · -𝐵) = (𝐴 · 𝐵)) |
|
Theorem | subdid 8144 |
Distribution of multiplication over subtraction. Theorem I.5 of
[Apostol] p. 18. (Contributed by Mario
Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 · (𝐵 − 𝐶)) = ((𝐴 · 𝐵) − (𝐴 · 𝐶))) |
|
Theorem | subdird 8145 |
Distribution of multiplication over subtraction. Theorem I.5 of
[Apostol] p. 18. (Contributed by Mario
Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) · 𝐶) = ((𝐴 · 𝐶) − (𝐵 · 𝐶))) |
|
Theorem | muladdd 8146 |
Product of two sums. (Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) · (𝐶 + 𝐷)) = (((𝐴 · 𝐶) + (𝐷 · 𝐵)) + ((𝐴 · 𝐷) + (𝐶 · 𝐵)))) |
|
Theorem | mulsubd 8147 |
Product of two differences. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) · (𝐶 − 𝐷)) = (((𝐴 · 𝐶) + (𝐷 · 𝐵)) − ((𝐴 · 𝐷) + (𝐶 · 𝐵)))) |
|
Theorem | mulsubfacd 8148 |
Multiplication followed by the subtraction of a factor. (Contributed by
Alexander van der Vekens, 28-Aug-2018.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) − 𝐵) = ((𝐴 − 1) · 𝐵)) |
|
4.3.4 Ordering on reals (cont.)
|
|
Theorem | ltadd2 8149 |
Addition to both sides of 'less than'. (Contributed by NM,
12-Nov-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐶 + 𝐴) < (𝐶 + 𝐵))) |
|
Theorem | ltadd2i 8150 |
Addition to both sides of 'less than'. (Contributed by NM,
21-Jan-1997.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈
ℝ ⇒ ⊢ (𝐴 < 𝐵 ↔ (𝐶 + 𝐴) < (𝐶 + 𝐵)) |
|
Theorem | ltadd2d 8151 |
Addition to both sides of 'less than'. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ)
⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐶 + 𝐴) < (𝐶 + 𝐵))) |
|
Theorem | ltadd2dd 8152 |
Addition to both sides of 'less than'. (Contributed by Mario
Carneiro, 30-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → (𝐶 + 𝐴) < (𝐶 + 𝐵)) |
|
Theorem | ltletrd 8153 |
Transitive law deduction for 'less than', 'less than or equal to'.
(Contributed by NM, 9-Jan-2006.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵)
& ⊢ (𝜑 → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 < 𝐶) |
|
Theorem | ltaddneg 8154 |
Adding a negative number to another number decreases it. (Contributed by
Glauco Siliprandi, 11-Dec-2019.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 0 ↔ (𝐵 + 𝐴) < 𝐵)) |
|
Theorem | ltaddnegr 8155 |
Adding a negative number to another number decreases it. (Contributed by
AV, 19-Mar-2021.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 0 ↔ (𝐴 + 𝐵) < 𝐵)) |
|
Theorem | lelttrdi 8156 |
If a number is less than another number, and the other number is less
than or equal to a third number, the first number is less than the third
number. (Contributed by Alexander van der Vekens, 24-Mar-2018.)
|
⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) & ⊢ (𝜑 → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 → 𝐴 < 𝐶)) |
|
Theorem | gt0ne0 8157 |
Positive implies nonzero. (Contributed by NM, 3-Oct-1999.) (Proof
shortened by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴) → 𝐴 ≠ 0) |
|
Theorem | lt0ne0 8158 |
A number which is less than zero is not zero. See also lt0ap0 8378 which is
similar but for apartness. (Contributed by Stefan O'Rear,
13-Sep-2014.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < 0) → 𝐴 ≠ 0) |
|
Theorem | ltadd1 8159 |
Addition to both sides of 'less than'. Part of definition 11.2.7(vi) of
[HoTT], p. (varies). (Contributed by NM,
12-Nov-1999.) (Proof shortened
by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 + 𝐶) < (𝐵 + 𝐶))) |
|
Theorem | leadd1 8160 |
Addition to both sides of 'less than or equal to'. Part of definition
11.2.7(vi) of [HoTT], p. (varies).
(Contributed by NM, 18-Oct-1999.)
(Proof shortened by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 + 𝐶) ≤ (𝐵 + 𝐶))) |
|
Theorem | leadd2 8161 |
Addition to both sides of 'less than or equal to'. (Contributed by NM,
26-Oct-1999.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐶 + 𝐴) ≤ (𝐶 + 𝐵))) |
|
Theorem | ltsubadd 8162 |
'Less than' relationship between subtraction and addition. (Contributed
by NM, 21-Jan-1997.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) < 𝐶 ↔ 𝐴 < (𝐶 + 𝐵))) |
|
Theorem | ltsubadd2 8163 |
'Less than' relationship between subtraction and addition. (Contributed
by NM, 21-Jan-1997.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) < 𝐶 ↔ 𝐴 < (𝐵 + 𝐶))) |
|
Theorem | lesubadd 8164 |
'Less than or equal to' relationship between subtraction and addition.
(Contributed by NM, 17-Nov-2004.) (Proof shortened by Mario Carneiro,
27-May-2016.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐶 + 𝐵))) |
|
Theorem | lesubadd2 8165 |
'Less than or equal to' relationship between subtraction and addition.
(Contributed by NM, 10-Aug-1999.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐵 + 𝐶))) |
|
Theorem | ltaddsub 8166 |
'Less than' relationship between addition and subtraction. (Contributed
by NM, 17-Nov-2004.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) < 𝐶 ↔ 𝐴 < (𝐶 − 𝐵))) |
|
Theorem | ltaddsub2 8167 |
'Less than' relationship between addition and subtraction. (Contributed
by NM, 17-Nov-2004.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) < 𝐶 ↔ 𝐵 < (𝐶 − 𝐴))) |
|
Theorem | leaddsub 8168 |
'Less than or equal to' relationship between addition and subtraction.
(Contributed by NM, 6-Apr-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐶 − 𝐵))) |
|
Theorem | leaddsub2 8169 |
'Less than or equal to' relationship between and addition and subtraction.
(Contributed by NM, 6-Apr-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) ≤ 𝐶 ↔ 𝐵 ≤ (𝐶 − 𝐴))) |
|
Theorem | suble 8170 |
Swap subtrahends in an inequality. (Contributed by NM, 29-Sep-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) ≤ 𝐶 ↔ (𝐴 − 𝐶) ≤ 𝐵)) |
|
Theorem | lesub 8171 |
Swap subtrahends in an inequality. (Contributed by NM, 29-Sep-2005.)
(Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ (𝐵 − 𝐶) ↔ 𝐶 ≤ (𝐵 − 𝐴))) |
|
Theorem | ltsub23 8172 |
'Less than' relationship between subtraction and addition. (Contributed
by NM, 4-Oct-1999.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) < 𝐶 ↔ (𝐴 − 𝐶) < 𝐵)) |
|
Theorem | ltsub13 8173 |
'Less than' relationship between subtraction and addition. (Contributed
by NM, 17-Nov-2004.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < (𝐵 − 𝐶) ↔ 𝐶 < (𝐵 − 𝐴))) |
|
Theorem | le2add 8174 |
Adding both sides of two 'less than or equal to' relations. (Contributed
by NM, 17-Apr-2005.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 ≤ 𝐶 ∧ 𝐵 ≤ 𝐷) → (𝐴 + 𝐵) ≤ (𝐶 + 𝐷))) |
|
Theorem | lt2add 8175 |
Adding both sides of two 'less than' relations. Theorem I.25 of [Apostol]
p. 20. (Contributed by NM, 15-Aug-1999.) (Proof shortened by Mario
Carneiro, 27-May-2016.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 < 𝐶 ∧ 𝐵 < 𝐷) → (𝐴 + 𝐵) < (𝐶 + 𝐷))) |
|
Theorem | ltleadd 8176 |
Adding both sides of two orderings. (Contributed by NM, 23-Dec-2007.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 < 𝐶 ∧ 𝐵 ≤ 𝐷) → (𝐴 + 𝐵) < (𝐶 + 𝐷))) |
|
Theorem | leltadd 8177 |
Adding both sides of two orderings. (Contributed by NM, 15-Aug-2008.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 ≤ 𝐶 ∧ 𝐵 < 𝐷) → (𝐴 + 𝐵) < (𝐶 + 𝐷))) |
|
Theorem | addgt0 8178 |
The sum of 2 positive numbers is positive. (Contributed by NM,
1-Jun-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 < 𝐴 ∧ 0 < 𝐵)) → 0 < (𝐴 + 𝐵)) |
|
Theorem | addgegt0 8179 |
The sum of nonnegative and positive numbers is positive. (Contributed by
NM, 28-Dec-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 0 < 𝐵)) → 0 < (𝐴 + 𝐵)) |
|
Theorem | addgtge0 8180 |
The sum of nonnegative and positive numbers is positive. (Contributed by
NM, 28-Dec-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 < 𝐴 ∧ 0 ≤ 𝐵)) → 0 < (𝐴 + 𝐵)) |
|
Theorem | addge0 8181 |
The sum of 2 nonnegative numbers is nonnegative. (Contributed by NM,
17-Mar-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 0 ≤ 𝐵)) → 0 ≤ (𝐴 + 𝐵)) |
|
Theorem | ltaddpos 8182 |
Adding a positive number to another number increases it. (Contributed by
NM, 17-Nov-2004.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < 𝐴 ↔ 𝐵 < (𝐵 + 𝐴))) |
|
Theorem | ltaddpos2 8183 |
Adding a positive number to another number increases it. (Contributed by
NM, 8-Apr-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < 𝐴 ↔ 𝐵 < (𝐴 + 𝐵))) |
|
Theorem | ltsubpos 8184 |
Subtracting a positive number from another number decreases it.
(Contributed by NM, 17-Nov-2004.) (Proof shortened by Andrew Salmon,
19-Nov-2011.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < 𝐴 ↔ (𝐵 − 𝐴) < 𝐵)) |
|
Theorem | posdif 8185 |
Comparison of two numbers whose difference is positive. (Contributed by
NM, 17-Nov-2004.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴))) |
|
Theorem | lesub1 8186 |
Subtraction from both sides of 'less than or equal to'. (Contributed by
NM, 13-May-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 − 𝐶) ≤ (𝐵 − 𝐶))) |
|
Theorem | lesub2 8187 |
Subtraction of both sides of 'less than or equal to'. (Contributed by NM,
29-Sep-2005.) (Revised by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐶 − 𝐵) ≤ (𝐶 − 𝐴))) |
|
Theorem | ltsub1 8188 |
Subtraction from both sides of 'less than'. (Contributed by FL,
3-Jan-2008.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 − 𝐶) < (𝐵 − 𝐶))) |
|
Theorem | ltsub2 8189 |
Subtraction of both sides of 'less than'. (Contributed by NM,
29-Sep-2005.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐶 − 𝐵) < (𝐶 − 𝐴))) |
|
Theorem | lt2sub 8190 |
Subtracting both sides of two 'less than' relations. (Contributed by
Mario Carneiro, 14-Apr-2016.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 < 𝐶 ∧ 𝐷 < 𝐵) → (𝐴 − 𝐵) < (𝐶 − 𝐷))) |
|
Theorem | le2sub 8191 |
Subtracting both sides of two 'less than or equal to' relations.
(Contributed by Mario Carneiro, 14-Apr-2016.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵) → (𝐴 − 𝐵) ≤ (𝐶 − 𝐷))) |
|
Theorem | ltneg 8192 |
Negative of both sides of 'less than'. Theorem I.23 of [Apostol] p. 20.
(Contributed by NM, 27-Aug-1999.) (Proof shortened by Mario Carneiro,
27-May-2016.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ -𝐵 < -𝐴)) |
|
Theorem | ltnegcon1 8193 |
Contraposition of negative in 'less than'. (Contributed by NM,
8-Nov-2004.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (-𝐴 < 𝐵 ↔ -𝐵 < 𝐴)) |
|
Theorem | ltnegcon2 8194 |
Contraposition of negative in 'less than'. (Contributed by Mario
Carneiro, 25-Feb-2015.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < -𝐵 ↔ 𝐵 < -𝐴)) |
|
Theorem | leneg 8195 |
Negative of both sides of 'less than or equal to'. (Contributed by NM,
12-Sep-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ -𝐵 ≤ -𝐴)) |
|
Theorem | lenegcon1 8196 |
Contraposition of negative in 'less than or equal to'. (Contributed by
NM, 10-May-2004.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (-𝐴 ≤ 𝐵 ↔ -𝐵 ≤ 𝐴)) |
|
Theorem | lenegcon2 8197 |
Contraposition of negative in 'less than or equal to'. (Contributed by
NM, 8-Oct-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ -𝐵 ↔ 𝐵 ≤ -𝐴)) |
|
Theorem | lt0neg1 8198 |
Comparison of a number and its negative to zero. Theorem I.23 of
[Apostol] p. 20. (Contributed by NM,
14-May-1999.)
|
⊢ (𝐴 ∈ ℝ → (𝐴 < 0 ↔ 0 < -𝐴)) |
|
Theorem | lt0neg2 8199 |
Comparison of a number and its negative to zero. (Contributed by NM,
10-May-2004.)
|
⊢ (𝐴 ∈ ℝ → (0 < 𝐴 ↔ -𝐴 < 0)) |
|
Theorem | le0neg1 8200 |
Comparison of a number and its negative to zero. (Contributed by NM,
10-May-2004.)
|
⊢ (𝐴 ∈ ℝ → (𝐴 ≤ 0 ↔ 0 ≤ -𝐴)) |