Theorem List for Intuitionistic Logic Explorer - 7201-7300 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | ltnsym2 7201 |
'Less than' is antisymmetric and irreflexive. (Contributed by NM,
13-Aug-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ¬ (𝐴 < 𝐵 ∧ 𝐵 < 𝐴)) |
|
Theorem | eqle 7202 |
Equality implies 'less than or equal to'. (Contributed by NM,
4-Apr-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 = 𝐵) → 𝐴 ≤ 𝐵) |
|
Theorem | ltnri 7203 |
'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.)
|
⊢ 𝐴 ∈ ℝ
⇒ ⊢ ¬ 𝐴 < 𝐴 |
|
Theorem | eqlei 7204 |
Equality implies 'less than or equal to'. (Contributed by NM,
23-May-1999.) (Revised by Alexander van der Vekens, 20-Mar-2018.)
|
⊢ 𝐴 ∈ ℝ
⇒ ⊢ (𝐴 = 𝐵 → 𝐴 ≤ 𝐵) |
|
Theorem | eqlei2 7205 |
Equality implies 'less than or equal to'. (Contributed by Alexander van
der Vekens, 20-Mar-2018.)
|
⊢ 𝐴 ∈ ℝ
⇒ ⊢ (𝐵 = 𝐴 → 𝐵 ≤ 𝐴) |
|
Theorem | gtneii 7206 |
'Less than' implies not equal. See also gtapii 7732 which is the same
for apartness. (Contributed by Mario Carneiro, 30-Sep-2013.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐴 < 𝐵 ⇒ ⊢ 𝐵 ≠ 𝐴 |
|
Theorem | ltneii 7207 |
'Greater than' implies not equal. (Contributed by Mario Carneiro,
16-Sep-2015.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐴 < 𝐵 ⇒ ⊢ 𝐴 ≠ 𝐵 |
|
Theorem | lttri3i 7208 |
Tightness of real apartness. (Contributed by NM, 14-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ (𝐴 = 𝐵 ↔ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴)) |
|
Theorem | letri3i 7209 |
Tightness of real apartness. (Contributed by NM, 14-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴)) |
|
Theorem | ltnsymi 7210 |
'Less than' is not symmetric. (Contributed by NM, 6-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ (𝐴 < 𝐵 → ¬ 𝐵 < 𝐴) |
|
Theorem | lenlti 7211 |
'Less than or equal to' in terms of 'less than'. (Contributed by NM,
24-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴) |
|
Theorem | ltlei 7212 |
'Less than' implies 'less than or equal to'. (Contributed by NM,
14-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ (𝐴 < 𝐵 → 𝐴 ≤ 𝐵) |
|
Theorem | ltleii 7213 |
'Less than' implies 'less than or equal to' (inference). (Contributed
by NM, 22-Aug-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐴 < 𝐵 ⇒ ⊢ 𝐴 ≤ 𝐵 |
|
Theorem | ltnei 7214 |
'Less than' implies not equal. (Contributed by NM, 28-Jul-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ (𝐴 < 𝐵 → 𝐵 ≠ 𝐴) |
|
Theorem | lttri 7215 |
'Less than' is transitive. Theorem I.17 of [Apostol] p. 20.
(Contributed by NM, 14-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈
ℝ ⇒ ⊢ ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶) |
|
Theorem | lelttri 7216 |
'Less than or equal to', 'less than' transitive law. (Contributed by
NM, 14-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈
ℝ ⇒ ⊢ ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶) |
|
Theorem | ltletri 7217 |
'Less than', 'less than or equal to' transitive law. (Contributed by
NM, 14-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈
ℝ ⇒ ⊢ ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶) |
|
Theorem | letri 7218 |
'Less than or equal to' is transitive. (Contributed by NM,
14-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈
ℝ ⇒ ⊢ ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶) |
|
Theorem | le2tri3i 7219 |
Extended trichotomy law for 'less than or equal to'. (Contributed by
NM, 14-Aug-2000.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈
ℝ ⇒ ⊢ ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ∧ 𝐶 ≤ 𝐴) ↔ (𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ∧ 𝐶 = 𝐴)) |
|
Theorem | mulgt0i 7220 |
The product of two positive numbers is positive. (Contributed by NM,
16-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ ((0 < 𝐴 ∧ 0 < 𝐵) → 0 < (𝐴 · 𝐵)) |
|
Theorem | mulgt0ii 7221 |
The product of two positive numbers is positive. (Contributed by NM,
18-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 0 < 𝐴 & ⊢ 0 < 𝐵 ⇒ ⊢ 0 < (𝐴 · 𝐵) |
|
Theorem | ltnrd 7222 |
'Less than' is irreflexive. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ)
⇒ ⊢ (𝜑 → ¬ 𝐴 < 𝐴) |
|
Theorem | gtned 7223 |
'Less than' implies not equal. See also gtapd 7735 which is the same but
for apartness. (Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐵 ≠ 𝐴) |
|
Theorem | ltned 7224 |
'Greater than' implies not equal. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) |
|
Theorem | lttri3d 7225 |
Tightness of real apartness. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ)
⇒ ⊢ (𝜑 → (𝐴 = 𝐵 ↔ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴))) |
|
Theorem | letri3d 7226 |
Tightness of real apartness. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ)
⇒ ⊢ (𝜑 → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))) |
|
Theorem | lenltd 7227 |
'Less than or equal to' in terms of 'less than'. (Contributed by Mario
Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ)
⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) |
|
Theorem | ltled 7228 |
'Less than' implies 'less than or equal to'. (Contributed by Mario
Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐵) |
|
Theorem | ltnsymd 7229 |
'Less than' implies 'less than or equal to'. (Contributed by Mario
Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐵 < 𝐴) |
|
Theorem | nltled 7230 |
'Not less than ' implies 'less than or equal to'. (Contributed by
Glauco Siliprandi, 11-Dec-2019.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ¬ 𝐵 < 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐵) |
|
Theorem | lensymd 7231 |
'Less than or equal to' implies 'not less than'. (Contributed by
Glauco Siliprandi, 11-Dec-2019.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐵 < 𝐴) |
|
Theorem | mulgt0d 7232 |
The product of two positive numbers is positive. (Contributed by
Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐴)
& ⊢ (𝜑 → 0 < 𝐵) ⇒ ⊢ (𝜑 → 0 < (𝐴 · 𝐵)) |
|
Theorem | letrd 7233 |
Transitive law deduction for 'less than or equal to'. (Contributed by
NM, 20-May-2005.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵)
& ⊢ (𝜑 → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐶) |
|
Theorem | lelttrd 7234 |
Transitive law deduction for 'less than or equal to', 'less than'.
(Contributed by NM, 8-Jan-2006.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵)
& ⊢ (𝜑 → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → 𝐴 < 𝐶) |
|
Theorem | lttrd 7235 |
Transitive law deduction for 'less than'. (Contributed by NM,
9-Jan-2006.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵)
& ⊢ (𝜑 → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → 𝐴 < 𝐶) |
|
Theorem | 0lt1 7236 |
0 is less than 1. Theorem I.21 of [Apostol] p.
20. Part of definition
11.2.7(vi) of [HoTT], p. (varies).
(Contributed by NM, 17-Jan-1997.)
|
⊢ 0 < 1 |
|
3.2.5 Initial properties of the complex
numbers
|
|
Theorem | mul12 7237 |
Commutative/associative law for multiplication. (Contributed by NM,
30-Apr-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶))) |
|
Theorem | mul32 7238 |
Commutative/associative law. (Contributed by NM, 8-Oct-1999.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵)) |
|
Theorem | mul31 7239 |
Commutative/associative law. (Contributed by Scott Fenton,
3-Jan-2013.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = ((𝐶 · 𝐵) · 𝐴)) |
|
Theorem | mul4 7240 |
Rearrangement of 4 factors. (Contributed by NM, 8-Oct-1999.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 · 𝐵) · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · (𝐵 · 𝐷))) |
|
Theorem | muladd11 7241 |
A simple product of sums expansion. (Contributed by NM, 21-Feb-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((1 + 𝐴) · (1 + 𝐵)) = ((1 + 𝐴) + (𝐵 + (𝐴 · 𝐵)))) |
|
Theorem | 1p1times 7242 |
Two times a number. (Contributed by NM, 18-May-1999.) (Revised by Mario
Carneiro, 27-May-2016.)
|
⊢ (𝐴 ∈ ℂ → ((1 + 1) ·
𝐴) = (𝐴 + 𝐴)) |
|
Theorem | peano2cn 7243 |
A theorem for complex numbers analogous the second Peano postulate
peano2 4336. (Contributed by NM, 17-Aug-2005.)
|
⊢ (𝐴 ∈ ℂ → (𝐴 + 1) ∈ ℂ) |
|
Theorem | peano2re 7244 |
A theorem for reals analogous the second Peano postulate peano2 4336.
(Contributed by NM, 5-Jul-2005.)
|
⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ) |
|
Theorem | addcom 7245 |
Addition commutes. (Contributed by Jim Kingdon, 17-Jan-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) |
|
Theorem | addid1 7246 |
0 is an additive identity. (Contributed by Jim
Kingdon,
16-Jan-2020.)
|
⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴) |
|
Theorem | addid2 7247 |
0 is a left identity for addition. (Contributed by
Scott Fenton,
3-Jan-2013.)
|
⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴) |
|
Theorem | readdcan 7248 |
Cancellation law for addition over the reals. (Contributed by Scott
Fenton, 3-Jan-2013.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐶 + 𝐴) = (𝐶 + 𝐵) ↔ 𝐴 = 𝐵)) |
|
Theorem | 00id 7249 |
0 is its own additive identity. (Contributed by Scott
Fenton,
3-Jan-2013.)
|
⊢ (0 + 0) = 0 |
|
Theorem | addid1i 7250 |
0 is an additive identity. (Contributed by NM,
23-Nov-1994.)
(Revised by Scott Fenton, 3-Jan-2013.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (𝐴 + 0) = 𝐴 |
|
Theorem | addid2i 7251 |
0 is a left identity for addition. (Contributed by NM,
3-Jan-2013.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (0 + 𝐴) = 𝐴 |
|
Theorem | addcomi 7252 |
Addition commutes. Based on ideas by Eric Schmidt. (Contributed by
Scott Fenton, 3-Jan-2013.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ (𝐴 + 𝐵) = (𝐵 + 𝐴) |
|
Theorem | addcomli 7253 |
Addition commutes. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ (𝐴 + 𝐵) = 𝐶 ⇒ ⊢ (𝐵 + 𝐴) = 𝐶 |
|
Theorem | mul12i 7254 |
Commutative/associative law that swaps the first two factors in a triple
product. (Contributed by NM, 11-May-1999.) (Proof shortened by Andrew
Salmon, 19-Nov-2011.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈
ℂ ⇒ ⊢ (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶)) |
|
Theorem | mul32i 7255 |
Commutative/associative law that swaps the last two factors in a triple
product. (Contributed by NM, 11-May-1999.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈
ℂ ⇒ ⊢ ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵) |
|
Theorem | mul4i 7256 |
Rearrangement of 4 factors. (Contributed by NM, 16-Feb-1995.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐷 ∈
ℂ ⇒ ⊢ ((𝐴 · 𝐵) · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · (𝐵 · 𝐷)) |
|
Theorem | addid1d 7257 |
0 is an additive identity. (Contributed by Mario
Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 + 0) = 𝐴) |
|
Theorem | addid2d 7258 |
0 is a left identity for addition. (Contributed by
Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (0 + 𝐴) = 𝐴) |
|
Theorem | addcomd 7259 |
Addition commutes. Based on ideas by Eric Schmidt. (Contributed by
Scott Fenton, 3-Jan-2013.) (Revised by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴)) |
|
Theorem | mul12d 7260 |
Commutative/associative law that swaps the first two factors in a triple
product. (Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶))) |
|
Theorem | mul32d 7261 |
Commutative/associative law that swaps the last two factors in a triple
product. (Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵)) |
|
Theorem | mul31d 7262 |
Commutative/associative law. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = ((𝐶 · 𝐵) · 𝐴)) |
|
Theorem | mul4d 7263 |
Rearrangement of 4 factors. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · (𝐵 · 𝐷))) |
|
Theorem | muladd11r 7264 |
A simple product of sums expansion. (Contributed by AV, 30-Jul-2021.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 1) · (𝐵 + 1)) = (((𝐴 · 𝐵) + (𝐴 + 𝐵)) + 1)) |
|
Theorem | comraddd 7265 |
Commute RHS addition, in deduction form. (Contributed by David A.
Wheeler, 11-Oct-2018.)
|
⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐴 = (𝐵 + 𝐶)) ⇒ ⊢ (𝜑 → 𝐴 = (𝐶 + 𝐵)) |
|
3.3 Real and complex numbers - basic
operations
|
|
3.3.1 Addition
|
|
Theorem | add12 7266 |
Commutative/associative law that swaps the first two terms in a triple
sum. (Contributed by NM, 11-May-2004.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 + (𝐵 + 𝐶)) = (𝐵 + (𝐴 + 𝐶))) |
|
Theorem | add32 7267 |
Commutative/associative law that swaps the last two terms in a triple sum.
(Contributed by NM, 13-Nov-1999.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = ((𝐴 + 𝐶) + 𝐵)) |
|
Theorem | add32r 7268 |
Commutative/associative law that swaps the last two terms in a triple sum,
rearranging the parentheses. (Contributed by Paul Chapman,
18-May-2007.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 + (𝐵 + 𝐶)) = ((𝐴 + 𝐶) + 𝐵)) |
|
Theorem | add4 7269 |
Rearrangement of 4 terms in a sum. (Contributed by NM, 13-Nov-1999.)
(Proof shortened by Andrew Salmon, 22-Oct-2011.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + (𝐵 + 𝐷))) |
|
Theorem | add42 7270 |
Rearrangement of 4 terms in a sum. (Contributed by NM, 12-May-2005.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + (𝐷 + 𝐵))) |
|
Theorem | add12i 7271 |
Commutative/associative law that swaps the first two terms in a triple
sum. (Contributed by NM, 21-Jan-1997.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈
ℂ ⇒ ⊢ (𝐴 + (𝐵 + 𝐶)) = (𝐵 + (𝐴 + 𝐶)) |
|
Theorem | add32i 7272 |
Commutative/associative law that swaps the last two terms in a triple
sum. (Contributed by NM, 21-Jan-1997.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈
ℂ ⇒ ⊢ ((𝐴 + 𝐵) + 𝐶) = ((𝐴 + 𝐶) + 𝐵) |
|
Theorem | add4i 7273 |
Rearrangement of 4 terms in a sum. (Contributed by NM, 9-May-1999.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐷 ∈
ℂ ⇒ ⊢ ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + (𝐵 + 𝐷)) |
|
Theorem | add42i 7274 |
Rearrangement of 4 terms in a sum. (Contributed by NM, 22-Aug-1999.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐷 ∈
ℂ ⇒ ⊢ ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + (𝐷 + 𝐵)) |
|
Theorem | add12d 7275 |
Commutative/associative law that swaps the first two terms in a triple
sum. (Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 + (𝐵 + 𝐶)) = (𝐵 + (𝐴 + 𝐶))) |
|
Theorem | add32d 7276 |
Commutative/associative law that swaps the last two terms in a triple
sum. (Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐶) = ((𝐴 + 𝐶) + 𝐵)) |
|
Theorem | add4d 7277 |
Rearrangement of 4 terms in a sum. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + (𝐵 + 𝐷))) |
|
Theorem | add42d 7278 |
Rearrangement of 4 terms in a sum. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + (𝐷 + 𝐵))) |
|
3.3.2 Subtraction
|
|
Syntax | cmin 7279 |
Extend class notation to include subtraction.
|
class − |
|
Syntax | cneg 7280 |
Extend class notation to include unary minus. The symbol - is not a
class by itself but part of a compound class definition. We do this
rather than making it a formal function since it is so commonly used.
Note: We use different symbols for unary minus (-) and subtraction
cmin 7279 (−) to prevent
syntax ambiguity. For example, looking at the
syntax definition co 5532, if we used the same symbol
then "( − 𝐴 − 𝐵) " could mean either
"− 𝐴 " minus "𝐵",
or
it could represent the (meaningless) operation of
classes "− " and "− 𝐵
" connected with "operation" "𝐴".
On the other hand, "(-𝐴 − 𝐵) " is unambiguous.
|
class -𝐴 |
|
Definition | df-sub 7281* |
Define subtraction. Theorem subval 7300 shows its value (and describes how
this definition works), theorem subaddi 7395 relates it to addition, and
theorems subcli 7384 and resubcli 7371 prove its closure laws. (Contributed
by NM, 26-Nov-1994.)
|
⊢ − = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥)) |
|
Definition | df-neg 7282 |
Define the negative of a number (unary minus). We use different symbols
for unary minus (-) and subtraction (−) to prevent syntax
ambiguity. See cneg 7280 for a discussion of this. (Contributed by
NM,
10-Feb-1995.)
|
⊢ -𝐴 = (0 − 𝐴) |
|
Theorem | cnegexlem1 7283 |
Addition cancellation of a real number from two complex numbers. Lemma
for cnegex 7286. (Contributed by Eric Schmidt, 22-May-2007.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) = (𝐴 + 𝐶) ↔ 𝐵 = 𝐶)) |
|
Theorem | cnegexlem2 7284 |
Existence of a real number which produces a real number when multiplied
by i. (Hint: zero is such a number, although we
don't need to
prove that yet). Lemma for cnegex 7286. (Contributed by Eric Schmidt,
22-May-2007.)
|
⊢ ∃𝑦 ∈ ℝ (i · 𝑦) ∈
ℝ |
|
Theorem | cnegexlem3 7285* |
Existence of real number difference. Lemma for cnegex 7286. (Contributed
by Eric Schmidt, 22-May-2007.)
|
⊢ ((𝑏 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ∃𝑐 ∈ ℝ (𝑏 + 𝑐) = 𝑦) |
|
Theorem | cnegex 7286* |
Existence of the negative of a complex number. (Contributed by Eric
Schmidt, 21-May-2007.)
|
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℂ (𝐴 + 𝑥) = 0) |
|
Theorem | cnegex2 7287* |
Existence of a left inverse for addition. (Contributed by Scott Fenton,
3-Jan-2013.)
|
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℂ (𝑥 + 𝐴) = 0) |
|
Theorem | addcan 7288 |
Cancellation law for addition. Theorem I.1 of [Apostol] p. 18.
(Contributed by NM, 22-Nov-1994.) (Proof shortened by Mario Carneiro,
27-May-2016.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) = (𝐴 + 𝐶) ↔ 𝐵 = 𝐶)) |
|
Theorem | addcan2 7289 |
Cancellation law for addition. (Contributed by NM, 30-Jul-2004.)
(Revised by Scott Fenton, 3-Jan-2013.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐶) = (𝐵 + 𝐶) ↔ 𝐴 = 𝐵)) |
|
Theorem | addcani 7290 |
Cancellation law for addition. Theorem I.1 of [Apostol] p. 18.
(Contributed by NM, 27-Oct-1999.) (Revised by Scott Fenton,
3-Jan-2013.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈
ℂ ⇒ ⊢ ((𝐴 + 𝐵) = (𝐴 + 𝐶) ↔ 𝐵 = 𝐶) |
|
Theorem | addcan2i 7291 |
Cancellation law for addition. Theorem I.1 of [Apostol] p. 18.
(Contributed by NM, 14-May-2003.) (Revised by Scott Fenton,
3-Jan-2013.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈
ℂ ⇒ ⊢ ((𝐴 + 𝐶) = (𝐵 + 𝐶) ↔ 𝐴 = 𝐵) |
|
Theorem | addcand 7292 |
Cancellation law for addition. Theorem I.1 of [Apostol] p. 18.
(Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) = (𝐴 + 𝐶) ↔ 𝐵 = 𝐶)) |
|
Theorem | addcan2d 7293 |
Cancellation law for addition. Theorem I.1 of [Apostol] p. 18.
(Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + 𝐶) = (𝐵 + 𝐶) ↔ 𝐴 = 𝐵)) |
|
Theorem | addcanad 7294 |
Cancelling a term on the left-hand side of a sum in an equality.
Consequence of addcand 7292. (Contributed by David Moews,
28-Feb-2017.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐴 + 𝐶)) ⇒ ⊢ (𝜑 → 𝐵 = 𝐶) |
|
Theorem | addcan2ad 7295 |
Cancelling a term on the right-hand side of a sum in an equality.
Consequence of addcan2d 7293. (Contributed by David Moews,
28-Feb-2017.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → (𝐴 + 𝐶) = (𝐵 + 𝐶)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) |
|
Theorem | addneintrd 7296 |
Introducing a term on the left-hand side of a sum in a negated
equality. Contrapositive of addcanad 7294. Consequence of addcand 7292.
(Contributed by David Moews, 28-Feb-2017.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) ≠ (𝐴 + 𝐶)) |
|
Theorem | addneintr2d 7297 |
Introducing a term on the right-hand side of a sum in a negated
equality. Contrapositive of addcan2ad 7295. Consequence of
addcan2d 7293. (Contributed by David Moews, 28-Feb-2017.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 + 𝐶) ≠ (𝐵 + 𝐶)) |
|
Theorem | 0cnALT 7298 |
Alternate proof of 0cn 7111. (Contributed by NM, 19-Feb-2005.) (Revised
by
Mario Carneiro, 27-May-2016.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ 0 ∈ ℂ |
|
Theorem | negeu 7299* |
Existential uniqueness of negatives. Theorem I.2 of [Apostol] p. 18.
(Contributed by NM, 22-Nov-1994.) (Proof shortened by Mario Carneiro,
27-May-2016.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐴 + 𝑥) = 𝐵) |
|
Theorem | subval 7300* |
Value of subtraction, which is the (unique) element 𝑥 such that
𝐵 +
𝑥 = 𝐴. (Contributed by NM, 4-Aug-2007.)
(Revised by Mario
Carneiro, 2-Nov-2013.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) = (℩𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴)) |