Theorem List for Intuitionistic Logic Explorer - 7101-7200 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | letr 7101 |
Transitive law. (Contributed by NM, 12-Nov-1999.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶)) |
|
Theorem | leid 7102 |
'Less than or equal to' is reflexive. (Contributed by NM,
18-Aug-1999.)
|
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ 𝐴) |
|
Theorem | ltne 7103 |
'Less than' implies not equal. See also ltap 7622
which is the same but for
apartness. (Contributed by NM, 9-Oct-1999.) (Revised by Mario Carneiro,
16-Sep-2015.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐵 ≠ 𝐴) |
|
Theorem | ltnsym 7104 |
'Less than' is not symmetric. (Contributed by NM, 8-Jan-2002.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → ¬ 𝐵 < 𝐴)) |
|
Theorem | ltle 7105 |
'Less than' implies 'less than or equal to'. (Contributed by NM,
25-Aug-1999.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵)) |
|
Theorem | lelttr 7106 |
Transitive law. Part of Definition 11.2.7(vi) of [HoTT], p. (varies).
(Contributed by NM, 23-May-1999.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)) |
|
Theorem | ltletr 7107 |
Transitive law. Part of Definition 11.2.7(vi) of [HoTT], p. (varies).
(Contributed by NM, 25-Aug-1999.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶)) |
|
Theorem | ltnsym2 7108 |
'Less than' is antisymmetric and irreflexive. (Contributed by NM,
13-Aug-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ¬ (𝐴 < 𝐵 ∧ 𝐵 < 𝐴)) |
|
Theorem | eqle 7109 |
Equality implies 'less than or equal to'. (Contributed by NM,
4-Apr-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 = 𝐵) → 𝐴 ≤ 𝐵) |
|
Theorem | ltnri 7110 |
'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.)
|
⊢ 𝐴 ∈ ℝ
⇒ ⊢ ¬ 𝐴 < 𝐴 |
|
Theorem | eqlei 7111 |
Equality implies 'less than or equal to'. (Contributed by NM,
23-May-1999.) (Revised by Alexander van der Vekens, 20-Mar-2018.)
|
⊢ 𝐴 ∈ ℝ
⇒ ⊢ (𝐴 = 𝐵 → 𝐴 ≤ 𝐵) |
|
Theorem | eqlei2 7112 |
Equality implies 'less than or equal to'. (Contributed by Alexander van
der Vekens, 20-Mar-2018.)
|
⊢ 𝐴 ∈ ℝ
⇒ ⊢ (𝐵 = 𝐴 → 𝐵 ≤ 𝐴) |
|
Theorem | gtneii 7113 |
'Less than' implies not equal. See also gtapii 7623 which is the same
for apartness. (Contributed by Mario Carneiro, 30-Sep-2013.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐴 < 𝐵 ⇒ ⊢ 𝐵 ≠ 𝐴 |
|
Theorem | ltneii 7114 |
'Greater than' implies not equal. (Contributed by Mario Carneiro,
16-Sep-2015.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐴 < 𝐵 ⇒ ⊢ 𝐴 ≠ 𝐵 |
|
Theorem | lttri3i 7115 |
Tightness of real apartness. (Contributed by NM, 14-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ (𝐴 = 𝐵 ↔ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴)) |
|
Theorem | letri3i 7116 |
Tightness of real apartness. (Contributed by NM, 14-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴)) |
|
Theorem | ltnsymi 7117 |
'Less than' is not symmetric. (Contributed by NM, 6-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ (𝐴 < 𝐵 → ¬ 𝐵 < 𝐴) |
|
Theorem | lenlti 7118 |
'Less than or equal to' in terms of 'less than'. (Contributed by NM,
24-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴) |
|
Theorem | ltlei 7119 |
'Less than' implies 'less than or equal to'. (Contributed by NM,
14-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ (𝐴 < 𝐵 → 𝐴 ≤ 𝐵) |
|
Theorem | ltleii 7120 |
'Less than' implies 'less than or equal to' (inference). (Contributed
by NM, 22-Aug-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐴 < 𝐵 ⇒ ⊢ 𝐴 ≤ 𝐵 |
|
Theorem | ltnei 7121 |
'Less than' implies not equal. (Contributed by NM, 28-Jul-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ (𝐴 < 𝐵 → 𝐵 ≠ 𝐴) |
|
Theorem | lttri 7122 |
'Less than' is transitive. Theorem I.17 of [Apostol] p. 20.
(Contributed by NM, 14-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈
ℝ ⇒ ⊢ ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶) |
|
Theorem | lelttri 7123 |
'Less than or equal to', 'less than' transitive law. (Contributed by
NM, 14-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈
ℝ ⇒ ⊢ ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶) |
|
Theorem | ltletri 7124 |
'Less than', 'less than or equal to' transitive law. (Contributed by
NM, 14-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈
ℝ ⇒ ⊢ ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶) |
|
Theorem | letri 7125 |
'Less than or equal to' is transitive. (Contributed by NM,
14-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈
ℝ ⇒ ⊢ ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶) |
|
Theorem | le2tri3i 7126 |
Extended trichotomy law for 'less than or equal to'. (Contributed by
NM, 14-Aug-2000.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈
ℝ ⇒ ⊢ ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ∧ 𝐶 ≤ 𝐴) ↔ (𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ∧ 𝐶 = 𝐴)) |
|
Theorem | mulgt0i 7127 |
The product of two positive numbers is positive. (Contributed by NM,
16-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ ((0 < 𝐴 ∧ 0 < 𝐵) → 0 < (𝐴 · 𝐵)) |
|
Theorem | mulgt0ii 7128 |
The product of two positive numbers is positive. (Contributed by NM,
18-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 0 < 𝐴 & ⊢ 0 < 𝐵 ⇒ ⊢ 0 < (𝐴 · 𝐵) |
|
Theorem | ltnrd 7129 |
'Less than' is irreflexive. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ)
⇒ ⊢ (𝜑 → ¬ 𝐴 < 𝐴) |
|
Theorem | gtned 7130 |
'Less than' implies not equal. See also gtapd 7626 which is the same but
for apartness. (Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐵 ≠ 𝐴) |
|
Theorem | ltned 7131 |
'Greater than' implies not equal. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) |
|
Theorem | lttri3d 7132 |
Tightness of real apartness. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ)
⇒ ⊢ (𝜑 → (𝐴 = 𝐵 ↔ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴))) |
|
Theorem | letri3d 7133 |
Tightness of real apartness. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ)
⇒ ⊢ (𝜑 → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))) |
|
Theorem | lenltd 7134 |
'Less than or equal to' in terms of 'less than'. (Contributed by Mario
Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ)
⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) |
|
Theorem | ltled 7135 |
'Less than' implies 'less than or equal to'. (Contributed by Mario
Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐵) |
|
Theorem | ltnsymd 7136 |
'Less than' implies 'less than or equal to'. (Contributed by Mario
Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐵 < 𝐴) |
|
Theorem | mulgt0d 7137 |
The product of two positive numbers is positive. (Contributed by
Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐴)
& ⊢ (𝜑 → 0 < 𝐵) ⇒ ⊢ (𝜑 → 0 < (𝐴 · 𝐵)) |
|
Theorem | letrd 7138 |
Transitive law deduction for 'less than or equal to'. (Contributed by
NM, 20-May-2005.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵)
& ⊢ (𝜑 → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐶) |
|
Theorem | lelttrd 7139 |
Transitive law deduction for 'less than or equal to', 'less than'.
(Contributed by NM, 8-Jan-2006.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵)
& ⊢ (𝜑 → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → 𝐴 < 𝐶) |
|
Theorem | lttrd 7140 |
Transitive law deduction for 'less than'. (Contributed by NM,
9-Jan-2006.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵)
& ⊢ (𝜑 → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → 𝐴 < 𝐶) |
|
Theorem | 0lt1 7141 |
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 7142 |
Commutative/associative law for multiplication. (Contributed by NM,
30-Apr-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶))) |
|
Theorem | mul32 7143 |
Commutative/associative law. (Contributed by NM, 8-Oct-1999.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵)) |
|
Theorem | mul31 7144 |
Commutative/associative law. (Contributed by Scott Fenton,
3-Jan-2013.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = ((𝐶 · 𝐵) · 𝐴)) |
|
Theorem | mul4 7145 |
Rearrangement of 4 factors. (Contributed by NM, 8-Oct-1999.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 · 𝐵) · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · (𝐵 · 𝐷))) |
|
Theorem | muladd11 7146 |
A simple product of sums expansion. (Contributed by NM, 21-Feb-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((1 + 𝐴) · (1 + 𝐵)) = ((1 + 𝐴) + (𝐵 + (𝐴 · 𝐵)))) |
|
Theorem | 1p1times 7147 |
Two times a number. (Contributed by NM, 18-May-1999.) (Revised by Mario
Carneiro, 27-May-2016.)
|
⊢ (𝐴 ∈ ℂ → ((1 + 1) ·
𝐴) = (𝐴 + 𝐴)) |
|
Theorem | peano2cn 7148 |
A theorem for complex numbers analogous the second Peano postulate
peano2 4318. (Contributed by NM, 17-Aug-2005.)
|
⊢ (𝐴 ∈ ℂ → (𝐴 + 1) ∈ ℂ) |
|
Theorem | peano2re 7149 |
A theorem for reals analogous the second Peano postulate peano2 4318.
(Contributed by NM, 5-Jul-2005.)
|
⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ) |
|
Theorem | addcom 7150 |
Addition commutes. (Contributed by Jim Kingdon, 17-Jan-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) |
|
Theorem | addid1 7151 |
0 is an additive identity. (Contributed by Jim
Kingdon,
16-Jan-2020.)
|
⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴) |
|
Theorem | addid2 7152 |
0 is a left identity for addition. (Contributed by
Scott Fenton,
3-Jan-2013.)
|
⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴) |
|
Theorem | readdcan 7153 |
Cancellation law for addition over the reals. (Contributed by Scott
Fenton, 3-Jan-2013.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐶 + 𝐴) = (𝐶 + 𝐵) ↔ 𝐴 = 𝐵)) |
|
Theorem | 00id 7154 |
0 is its own additive identity. (Contributed by Scott
Fenton,
3-Jan-2013.)
|
⊢ (0 + 0) = 0 |
|
Theorem | addid1i 7155 |
0 is an additive identity. (Contributed by NM,
23-Nov-1994.)
(Revised by Scott Fenton, 3-Jan-2013.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (𝐴 + 0) = 𝐴 |
|
Theorem | addid2i 7156 |
0 is a left identity for addition. (Contributed by NM,
3-Jan-2013.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (0 + 𝐴) = 𝐴 |
|
Theorem | addcomi 7157 |
Addition commutes. Based on ideas by Eric Schmidt. (Contributed by
Scott Fenton, 3-Jan-2013.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ (𝐴 + 𝐵) = (𝐵 + 𝐴) |
|
Theorem | addcomli 7158 |
Addition commutes. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ (𝐴 + 𝐵) = 𝐶 ⇒ ⊢ (𝐵 + 𝐴) = 𝐶 |
|
Theorem | mul12i 7159 |
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 7160 |
Commutative/associative law that swaps the last two factors in a triple
product. (Contributed by NM, 11-May-1999.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈
ℂ ⇒ ⊢ ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵) |
|
Theorem | mul4i 7161 |
Rearrangement of 4 factors. (Contributed by NM, 16-Feb-1995.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐷 ∈
ℂ ⇒ ⊢ ((𝐴 · 𝐵) · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · (𝐵 · 𝐷)) |
|
Theorem | addid1d 7162 |
0 is an additive identity. (Contributed by Mario
Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 + 0) = 𝐴) |
|
Theorem | addid2d 7163 |
0 is a left identity for addition. (Contributed by
Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (0 + 𝐴) = 𝐴) |
|
Theorem | addcomd 7164 |
Addition commutes. Based on ideas by Eric Schmidt. (Contributed by
Scott Fenton, 3-Jan-2013.) (Revised by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴)) |
|
Theorem | mul12d 7165 |
Commutative/associative law that swaps the first two factors in a triple
product. (Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶))) |
|
Theorem | mul32d 7166 |
Commutative/associative law that swaps the last two factors in a triple
product. (Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵)) |
|
Theorem | mul31d 7167 |
Commutative/associative law. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = ((𝐶 · 𝐵) · 𝐴)) |
|
Theorem | mul4d 7168 |
Rearrangement of 4 factors. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · (𝐵 · 𝐷))) |
|
3.3 Real and complex numbers - basic
operations
|
|
3.3.1 Addition
|
|
Theorem | add12 7169 |
Commutative/associative law that swaps the first two terms in a triple
sum. (Contributed by NM, 11-May-2004.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 + (𝐵 + 𝐶)) = (𝐵 + (𝐴 + 𝐶))) |
|
Theorem | add32 7170 |
Commutative/associative law that swaps the last two terms in a triple sum.
(Contributed by NM, 13-Nov-1999.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = ((𝐴 + 𝐶) + 𝐵)) |
|
Theorem | add32r 7171 |
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 7172 |
Rearrangement of 4 terms in a sum. (Contributed by NM, 13-Nov-1999.)
(Proof shortened by Andrew Salmon, 22-Oct-2011.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + (𝐵 + 𝐷))) |
|
Theorem | add42 7173 |
Rearrangement of 4 terms in a sum. (Contributed by NM, 12-May-2005.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + (𝐷 + 𝐵))) |
|
Theorem | add12i 7174 |
Commutative/associative law that swaps the first two terms in a triple
sum. (Contributed by NM, 21-Jan-1997.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈
ℂ ⇒ ⊢ (𝐴 + (𝐵 + 𝐶)) = (𝐵 + (𝐴 + 𝐶)) |
|
Theorem | add32i 7175 |
Commutative/associative law that swaps the last two terms in a triple
sum. (Contributed by NM, 21-Jan-1997.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈
ℂ ⇒ ⊢ ((𝐴 + 𝐵) + 𝐶) = ((𝐴 + 𝐶) + 𝐵) |
|
Theorem | add4i 7176 |
Rearrangement of 4 terms in a sum. (Contributed by NM, 9-May-1999.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐷 ∈
ℂ ⇒ ⊢ ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + (𝐵 + 𝐷)) |
|
Theorem | add42i 7177 |
Rearrangement of 4 terms in a sum. (Contributed by NM, 22-Aug-1999.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐷 ∈
ℂ ⇒ ⊢ ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + (𝐷 + 𝐵)) |
|
Theorem | add12d 7178 |
Commutative/associative law that swaps the first two terms in a triple
sum. (Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 + (𝐵 + 𝐶)) = (𝐵 + (𝐴 + 𝐶))) |
|
Theorem | add32d 7179 |
Commutative/associative law that swaps the last two terms in a triple
sum. (Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐶) = ((𝐴 + 𝐶) + 𝐵)) |
|
Theorem | add4d 7180 |
Rearrangement of 4 terms in a sum. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + (𝐵 + 𝐷))) |
|
Theorem | add42d 7181 |
Rearrangement of 4 terms in a sum. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + (𝐷 + 𝐵))) |
|
3.3.2 Subtraction
|
|
Syntax | cmin 7182 |
Extend class notation to include subtraction.
|
class − |
|
Syntax | cneg 7183 |
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 7182 (−) to prevent
syntax ambiguity. For example, looking at the
syntax definition co 5512, 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 7184* |
Define subtraction. Theorem subval 7203 shows its value (and describes how
this definition works), theorem subaddi 7298 relates it to addition, and
theorems subcli 7287 and resubcli 7274 prove its closure laws. (Contributed
by NM, 26-Nov-1994.)
|
⊢ − = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥)) |
|
Definition | df-neg 7185 |
Define the negative of a number (unary minus). We use different symbols
for unary minus (-) and subtraction (−) to prevent syntax
ambiguity. See cneg 7183 for a discussion of this. (Contributed by
NM,
10-Feb-1995.)
|
⊢ -𝐴 = (0 − 𝐴) |
|
Theorem | cnegexlem1 7186 |
Addition cancellation of a real number from two complex numbers. Lemma
for cnegex 7189. (Contributed by Eric Schmidt, 22-May-2007.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) = (𝐴 + 𝐶) ↔ 𝐵 = 𝐶)) |
|
Theorem | cnegexlem2 7187 |
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 7189. (Contributed by Eric Schmidt,
22-May-2007.)
|
⊢ ∃𝑦 ∈ ℝ (i · 𝑦) ∈
ℝ |
|
Theorem | cnegexlem3 7188* |
Existence of real number difference. Lemma for cnegex 7189. (Contributed
by Eric Schmidt, 22-May-2007.)
|
⊢ ((𝑏 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ∃𝑐 ∈ ℝ (𝑏 + 𝑐) = 𝑦) |
|
Theorem | cnegex 7189* |
Existence of the negative of a complex number. (Contributed by Eric
Schmidt, 21-May-2007.)
|
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℂ (𝐴 + 𝑥) = 0) |
|
Theorem | cnegex2 7190* |
Existence of a left inverse for addition. (Contributed by Scott Fenton,
3-Jan-2013.)
|
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℂ (𝑥 + 𝐴) = 0) |
|
Theorem | addcan 7191 |
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 7192 |
Cancellation law for addition. (Contributed by NM, 30-Jul-2004.)
(Revised by Scott Fenton, 3-Jan-2013.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐶) = (𝐵 + 𝐶) ↔ 𝐴 = 𝐵)) |
|
Theorem | addcani 7193 |
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 7194 |
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 7195 |
Cancellation law for addition. Theorem I.1 of [Apostol] p. 18.
(Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) = (𝐴 + 𝐶) ↔ 𝐵 = 𝐶)) |
|
Theorem | addcan2d 7196 |
Cancellation law for addition. Theorem I.1 of [Apostol] p. 18.
(Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + 𝐶) = (𝐵 + 𝐶) ↔ 𝐴 = 𝐵)) |
|
Theorem | addcanad 7197 |
Cancelling a term on the left-hand side of a sum in an equality.
Consequence of addcand 7195. (Contributed by David Moews,
28-Feb-2017.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐴 + 𝐶)) ⇒ ⊢ (𝜑 → 𝐵 = 𝐶) |
|
Theorem | addcan2ad 7198 |
Cancelling a term on the right-hand side of a sum in an equality.
Consequence of addcan2d 7196. (Contributed by David Moews,
28-Feb-2017.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → (𝐴 + 𝐶) = (𝐵 + 𝐶)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) |
|
Theorem | addneintrd 7199 |
Introducing a term on the left-hand side of a sum in a negated
equality. Contrapositive of addcanad 7197. Consequence of addcand 7195.
(Contributed by David Moews, 28-Feb-2017.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) ≠ (𝐴 + 𝐶)) |
|
Theorem | addneintr2d 7200 |
Introducing a term on the right-hand side of a sum in a negated
equality. Contrapositive of addcan2ad 7198. Consequence of
addcan2d 7196. (Contributed by David Moews, 28-Feb-2017.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 + 𝐶) ≠ (𝐵 + 𝐶)) |