Theorem List for Intuitionistic Logic Explorer - 7701-7800 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | xrlenlt 7701 |
'Less than or equal to' expressed in terms of 'less than', for extended
reals. (Contributed by NM, 14-Oct-2005.)
|
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) |
|
Theorem | ltxrlt 7702 |
The standard less-than <ℝ and the
extended real less-than < are
identical when restricted to the non-extended reals ℝ.
(Contributed by NM, 13-Oct-2005.) (Revised by Mario Carneiro,
28-Apr-2015.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 𝐴 <ℝ 𝐵)) |
|
3.2.3 Restate the ordering postulates with
extended real "less than"
|
|
Theorem | axltirr 7703 |
Real number less-than is irreflexive. Axiom for real and complex numbers,
derived from set theory. This restates ax-pre-ltirr 7607 with ordering on
the extended reals. New proofs should use ltnr 7712
instead for naming
consistency. (New usage is discouraged.) (Contributed by Jim Kingdon,
15-Jan-2020.)
|
⊢ (𝐴 ∈ ℝ → ¬ 𝐴 < 𝐴) |
|
Theorem | axltwlin 7704 |
Real number less-than is weakly linear. Axiom for real and complex
numbers, derived from set theory. This restates ax-pre-ltwlin 7608 with
ordering on the extended reals. (Contributed by Jim Kingdon,
15-Jan-2020.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 → (𝐴 < 𝐶 ∨ 𝐶 < 𝐵))) |
|
Theorem | axlttrn 7705 |
Ordering on reals is transitive. Axiom for real and complex numbers,
derived from set theory. This restates ax-pre-lttrn 7609 with ordering on
the extended reals. New proofs should use lttr 7709
instead for naming
consistency. (New usage is discouraged.) (Contributed by NM,
13-Oct-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)) |
|
Theorem | axltadd 7706 |
Ordering property of addition on reals. Axiom for real and complex
numbers, derived from set theory. (This restates ax-pre-ltadd 7611 with
ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 → (𝐶 + 𝐴) < (𝐶 + 𝐵))) |
|
Theorem | axapti 7707 |
Apartness of reals is tight. Axiom for real and complex numbers, derived
from set theory. (This restates ax-pre-apti 7610 with ordering on the
extended reals.) (Contributed by Jim Kingdon, 29-Jan-2020.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ¬ (𝐴 < 𝐵 ∨ 𝐵 < 𝐴)) → 𝐴 = 𝐵) |
|
Theorem | axmulgt0 7708 |
The product of two positive reals is positive. Axiom for real and complex
numbers, derived from set theory. (This restates ax-pre-mulgt0 7612 with
ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 < 𝐴 ∧ 0 < 𝐵) → 0 < (𝐴 · 𝐵))) |
|
3.2.4 Ordering on reals
|
|
Theorem | lttr 7709 |
Alias for axlttrn 7705, for naming consistency with lttri 7739. New proofs
should generally use this instead of ax-pre-lttrn 7609. (Contributed by NM,
10-Mar-2008.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)) |
|
Theorem | mulgt0 7710 |
The product of two positive numbers is positive. (Contributed by NM,
10-Mar-2008.)
|
⊢ (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → 0 < (𝐴 · 𝐵)) |
|
Theorem | lenlt 7711 |
'Less than or equal to' expressed in terms of 'less than'. Part of
definition 11.2.7(vi) of [HoTT], p.
(varies). (Contributed by NM,
13-May-1999.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) |
|
Theorem | ltnr 7712 |
'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.)
|
⊢ (𝐴 ∈ ℝ → ¬ 𝐴 < 𝐴) |
|
Theorem | ltso 7713 |
'Less than' is a strict ordering. (Contributed by NM, 19-Jan-1997.)
|
⊢ < Or ℝ |
|
Theorem | gtso 7714 |
'Greater than' is a strict ordering. (Contributed by JJ, 11-Oct-2018.)
|
⊢ ◡
< Or ℝ |
|
Theorem | lttri3 7715 |
Tightness of real apartness. (Contributed by NM, 5-May-1999.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 = 𝐵 ↔ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴))) |
|
Theorem | letri3 7716 |
Tightness of real apartness. (Contributed by NM, 14-May-1999.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))) |
|
Theorem | ltleletr 7717 |
Transitive law, weaker form of (𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶.
(Contributed by AV, 14-Oct-2018.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶)) |
|
Theorem | letr 7718 |
Transitive law. (Contributed by NM, 12-Nov-1999.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶)) |
|
Theorem | leid 7719 |
'Less than or equal to' is reflexive. (Contributed by NM,
18-Aug-1999.)
|
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ 𝐴) |
|
Theorem | ltne 7720 |
'Less than' implies not equal. See also ltap 8260
which is the same but for
apartness. (Contributed by NM, 9-Oct-1999.) (Revised by Mario Carneiro,
16-Sep-2015.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐵 ≠ 𝐴) |
|
Theorem | ltnsym 7721 |
'Less than' is not symmetric. (Contributed by NM, 8-Jan-2002.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → ¬ 𝐵 < 𝐴)) |
|
Theorem | ltle 7722 |
'Less than' implies 'less than or equal to'. (Contributed by NM,
25-Aug-1999.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵)) |
|
Theorem | lelttr 7723 |
Transitive law. Part of Definition 11.2.7(vi) of [HoTT], p. (varies).
(Contributed by NM, 23-May-1999.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶)) |
|
Theorem | ltletr 7724 |
Transitive law. Part of Definition 11.2.7(vi) of [HoTT], p. (varies).
(Contributed by NM, 25-Aug-1999.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶)) |
|
Theorem | ltnsym2 7725 |
'Less than' is antisymmetric and irreflexive. (Contributed by NM,
13-Aug-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ¬ (𝐴 < 𝐵 ∧ 𝐵 < 𝐴)) |
|
Theorem | eqle 7726 |
Equality implies 'less than or equal to'. (Contributed by NM,
4-Apr-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 = 𝐵) → 𝐴 ≤ 𝐵) |
|
Theorem | ltnri 7727 |
'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.)
|
⊢ 𝐴 ∈ ℝ
⇒ ⊢ ¬ 𝐴 < 𝐴 |
|
Theorem | eqlei 7728 |
Equality implies 'less than or equal to'. (Contributed by NM,
23-May-1999.) (Revised by Alexander van der Vekens, 20-Mar-2018.)
|
⊢ 𝐴 ∈ ℝ
⇒ ⊢ (𝐴 = 𝐵 → 𝐴 ≤ 𝐵) |
|
Theorem | eqlei2 7729 |
Equality implies 'less than or equal to'. (Contributed by Alexander van
der Vekens, 20-Mar-2018.)
|
⊢ 𝐴 ∈ ℝ
⇒ ⊢ (𝐵 = 𝐴 → 𝐵 ≤ 𝐴) |
|
Theorem | gtneii 7730 |
'Less than' implies not equal. See also gtapii 8261 which is the same
for apartness. (Contributed by Mario Carneiro, 30-Sep-2013.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐴 < 𝐵 ⇒ ⊢ 𝐵 ≠ 𝐴 |
|
Theorem | ltneii 7731 |
'Greater than' implies not equal. (Contributed by Mario Carneiro,
16-Sep-2015.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐴 < 𝐵 ⇒ ⊢ 𝐴 ≠ 𝐵 |
|
Theorem | lttri3i 7732 |
Tightness of real apartness. (Contributed by NM, 14-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ (𝐴 = 𝐵 ↔ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴)) |
|
Theorem | letri3i 7733 |
Tightness of real apartness. (Contributed by NM, 14-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴)) |
|
Theorem | ltnsymi 7734 |
'Less than' is not symmetric. (Contributed by NM, 6-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ (𝐴 < 𝐵 → ¬ 𝐵 < 𝐴) |
|
Theorem | lenlti 7735 |
'Less than or equal to' in terms of 'less than'. (Contributed by NM,
24-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴) |
|
Theorem | ltlei 7736 |
'Less than' implies 'less than or equal to'. (Contributed by NM,
14-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ (𝐴 < 𝐵 → 𝐴 ≤ 𝐵) |
|
Theorem | ltleii 7737 |
'Less than' implies 'less than or equal to' (inference). (Contributed
by NM, 22-Aug-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐴 < 𝐵 ⇒ ⊢ 𝐴 ≤ 𝐵 |
|
Theorem | ltnei 7738 |
'Less than' implies not equal. (Contributed by NM, 28-Jul-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ (𝐴 < 𝐵 → 𝐵 ≠ 𝐴) |
|
Theorem | lttri 7739 |
'Less than' is transitive. Theorem I.17 of [Apostol] p. 20.
(Contributed by NM, 14-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈
ℝ ⇒ ⊢ ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶) |
|
Theorem | lelttri 7740 |
'Less than or equal to', 'less than' transitive law. (Contributed by
NM, 14-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈
ℝ ⇒ ⊢ ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶) |
|
Theorem | ltletri 7741 |
'Less than', 'less than or equal to' transitive law. (Contributed by
NM, 14-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈
ℝ ⇒ ⊢ ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶) |
|
Theorem | letri 7742 |
'Less than or equal to' is transitive. (Contributed by NM,
14-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈
ℝ ⇒ ⊢ ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶) |
|
Theorem | le2tri3i 7743 |
Extended trichotomy law for 'less than or equal to'. (Contributed by
NM, 14-Aug-2000.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈
ℝ ⇒ ⊢ ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ∧ 𝐶 ≤ 𝐴) ↔ (𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ∧ 𝐶 = 𝐴)) |
|
Theorem | mulgt0i 7744 |
The product of two positive numbers is positive. (Contributed by NM,
16-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ ((0 < 𝐴 ∧ 0 < 𝐵) → 0 < (𝐴 · 𝐵)) |
|
Theorem | mulgt0ii 7745 |
The product of two positive numbers is positive. (Contributed by NM,
18-May-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 0 < 𝐴 & ⊢ 0 < 𝐵 ⇒ ⊢ 0 < (𝐴 · 𝐵) |
|
Theorem | ltnrd 7746 |
'Less than' is irreflexive. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ)
⇒ ⊢ (𝜑 → ¬ 𝐴 < 𝐴) |
|
Theorem | gtned 7747 |
'Less than' implies not equal. See also gtapd 8264 which is the same but
for apartness. (Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐵 ≠ 𝐴) |
|
Theorem | ltned 7748 |
'Greater than' implies not equal. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) |
|
Theorem | lttri3d 7749 |
Tightness of real apartness. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ)
⇒ ⊢ (𝜑 → (𝐴 = 𝐵 ↔ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴))) |
|
Theorem | letri3d 7750 |
Tightness of real apartness. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ)
⇒ ⊢ (𝜑 → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))) |
|
Theorem | lenltd 7751 |
'Less than or equal to' in terms of 'less than'. (Contributed by Mario
Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ)
⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) |
|
Theorem | ltled 7752 |
'Less than' implies 'less than or equal to'. (Contributed by Mario
Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐵) |
|
Theorem | ltnsymd 7753 |
'Less than' implies 'less than or equal to'. (Contributed by Mario
Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐵 < 𝐴) |
|
Theorem | nltled 7754 |
'Not less than ' implies 'less than or equal to'. (Contributed by
Glauco Siliprandi, 11-Dec-2019.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ¬ 𝐵 < 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐵) |
|
Theorem | lensymd 7755 |
'Less than or equal to' implies 'not less than'. (Contributed by
Glauco Siliprandi, 11-Dec-2019.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐵 < 𝐴) |
|
Theorem | mulgt0d 7756 |
The product of two positive numbers is positive. (Contributed by
Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐴)
& ⊢ (𝜑 → 0 < 𝐵) ⇒ ⊢ (𝜑 → 0 < (𝐴 · 𝐵)) |
|
Theorem | letrd 7757 |
Transitive law deduction for 'less than or equal to'. (Contributed by
NM, 20-May-2005.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵)
& ⊢ (𝜑 → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ≤ 𝐶) |
|
Theorem | lelttrd 7758 |
Transitive law deduction for 'less than or equal to', 'less than'.
(Contributed by NM, 8-Jan-2006.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵)
& ⊢ (𝜑 → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → 𝐴 < 𝐶) |
|
Theorem | lttrd 7759 |
Transitive law deduction for 'less than'. (Contributed by NM,
9-Jan-2006.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵)
& ⊢ (𝜑 → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → 𝐴 < 𝐶) |
|
Theorem | 0lt1 7760 |
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 |
|
Theorem | ltntri 7761 |
Negative trichotomy property for real numbers. It is well known that we
cannot prove real number trichotomy, 𝐴 < 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 < 𝐴. Does
that mean there is a pair of real numbers where none of those hold (that
is, where we can refute each of those three relationships)? Actually, no,
as shown here. This is another example of distinguishing between being
unable to prove something, or being able to refute it. (Contributed by
Jim Kingdon, 13-Aug-2023.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ¬ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐴 = 𝐵 ∧ ¬ 𝐵 < 𝐴)) |
|
3.2.5 Initial properties of the complex
numbers
|
|
Theorem | mul12 7762 |
Commutative/associative law for multiplication. (Contributed by NM,
30-Apr-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶))) |
|
Theorem | mul32 7763 |
Commutative/associative law. (Contributed by NM, 8-Oct-1999.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵)) |
|
Theorem | mul31 7764 |
Commutative/associative law. (Contributed by Scott Fenton,
3-Jan-2013.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = ((𝐶 · 𝐵) · 𝐴)) |
|
Theorem | mul4 7765 |
Rearrangement of 4 factors. (Contributed by NM, 8-Oct-1999.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 · 𝐵) · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · (𝐵 · 𝐷))) |
|
Theorem | muladd11 7766 |
A simple product of sums expansion. (Contributed by NM, 21-Feb-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((1 + 𝐴) · (1 + 𝐵)) = ((1 + 𝐴) + (𝐵 + (𝐴 · 𝐵)))) |
|
Theorem | 1p1times 7767 |
Two times a number. (Contributed by NM, 18-May-1999.) (Revised by Mario
Carneiro, 27-May-2016.)
|
⊢ (𝐴 ∈ ℂ → ((1 + 1) ·
𝐴) = (𝐴 + 𝐴)) |
|
Theorem | peano2cn 7768 |
A theorem for complex numbers analogous the second Peano postulate
peano2 4447. (Contributed by NM, 17-Aug-2005.)
|
⊢ (𝐴 ∈ ℂ → (𝐴 + 1) ∈ ℂ) |
|
Theorem | peano2re 7769 |
A theorem for reals analogous the second Peano postulate peano2 4447.
(Contributed by NM, 5-Jul-2005.)
|
⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ) |
|
Theorem | addcom 7770 |
Addition commutes. (Contributed by Jim Kingdon, 17-Jan-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) |
|
Theorem | addid1 7771 |
0 is an additive identity. (Contributed by Jim
Kingdon,
16-Jan-2020.)
|
⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴) |
|
Theorem | addid2 7772 |
0 is a left identity for addition. (Contributed by
Scott Fenton,
3-Jan-2013.)
|
⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴) |
|
Theorem | readdcan 7773 |
Cancellation law for addition over the reals. (Contributed by Scott
Fenton, 3-Jan-2013.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐶 + 𝐴) = (𝐶 + 𝐵) ↔ 𝐴 = 𝐵)) |
|
Theorem | 00id 7774 |
0 is its own additive identity. (Contributed by Scott
Fenton,
3-Jan-2013.)
|
⊢ (0 + 0) = 0 |
|
Theorem | addid1i 7775 |
0 is an additive identity. (Contributed by NM,
23-Nov-1994.)
(Revised by Scott Fenton, 3-Jan-2013.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (𝐴 + 0) = 𝐴 |
|
Theorem | addid2i 7776 |
0 is a left identity for addition. (Contributed by NM,
3-Jan-2013.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (0 + 𝐴) = 𝐴 |
|
Theorem | addcomi 7777 |
Addition commutes. Based on ideas by Eric Schmidt. (Contributed by
Scott Fenton, 3-Jan-2013.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ (𝐴 + 𝐵) = (𝐵 + 𝐴) |
|
Theorem | addcomli 7778 |
Addition commutes. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ (𝐴 + 𝐵) = 𝐶 ⇒ ⊢ (𝐵 + 𝐴) = 𝐶 |
|
Theorem | mul12i 7779 |
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 7780 |
Commutative/associative law that swaps the last two factors in a triple
product. (Contributed by NM, 11-May-1999.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈
ℂ ⇒ ⊢ ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵) |
|
Theorem | mul4i 7781 |
Rearrangement of 4 factors. (Contributed by NM, 16-Feb-1995.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐷 ∈
ℂ ⇒ ⊢ ((𝐴 · 𝐵) · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · (𝐵 · 𝐷)) |
|
Theorem | addid1d 7782 |
0 is an additive identity. (Contributed by Mario
Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 + 0) = 𝐴) |
|
Theorem | addid2d 7783 |
0 is a left identity for addition. (Contributed by
Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (0 + 𝐴) = 𝐴) |
|
Theorem | addcomd 7784 |
Addition commutes. Based on ideas by Eric Schmidt. (Contributed by
Scott Fenton, 3-Jan-2013.) (Revised by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴)) |
|
Theorem | mul12d 7785 |
Commutative/associative law that swaps the first two factors in a triple
product. (Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶))) |
|
Theorem | mul32d 7786 |
Commutative/associative law that swaps the last two factors in a triple
product. (Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵)) |
|
Theorem | mul31d 7787 |
Commutative/associative law. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = ((𝐶 · 𝐵) · 𝐴)) |
|
Theorem | mul4d 7788 |
Rearrangement of 4 factors. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · (𝐵 · 𝐷))) |
|
Theorem | muladd11r 7789 |
A simple product of sums expansion. (Contributed by AV, 30-Jul-2021.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 1) · (𝐵 + 1)) = (((𝐴 · 𝐵) + (𝐴 + 𝐵)) + 1)) |
|
Theorem | comraddd 7790 |
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 7791 |
Commutative/associative law that swaps the first two terms in a triple
sum. (Contributed by NM, 11-May-2004.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 + (𝐵 + 𝐶)) = (𝐵 + (𝐴 + 𝐶))) |
|
Theorem | add32 7792 |
Commutative/associative law that swaps the last two terms in a triple sum.
(Contributed by NM, 13-Nov-1999.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = ((𝐴 + 𝐶) + 𝐵)) |
|
Theorem | add32r 7793 |
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 7794 |
Rearrangement of 4 terms in a sum. (Contributed by NM, 13-Nov-1999.)
(Proof shortened by Andrew Salmon, 22-Oct-2011.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + (𝐵 + 𝐷))) |
|
Theorem | add42 7795 |
Rearrangement of 4 terms in a sum. (Contributed by NM, 12-May-2005.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + (𝐷 + 𝐵))) |
|
Theorem | add12i 7796 |
Commutative/associative law that swaps the first two terms in a triple
sum. (Contributed by NM, 21-Jan-1997.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈
ℂ ⇒ ⊢ (𝐴 + (𝐵 + 𝐶)) = (𝐵 + (𝐴 + 𝐶)) |
|
Theorem | add32i 7797 |
Commutative/associative law that swaps the last two terms in a triple
sum. (Contributed by NM, 21-Jan-1997.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈
ℂ ⇒ ⊢ ((𝐴 + 𝐵) + 𝐶) = ((𝐴 + 𝐶) + 𝐵) |
|
Theorem | add4i 7798 |
Rearrangement of 4 terms in a sum. (Contributed by NM, 9-May-1999.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐷 ∈
ℂ ⇒ ⊢ ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + (𝐵 + 𝐷)) |
|
Theorem | add42i 7799 |
Rearrangement of 4 terms in a sum. (Contributed by NM, 22-Aug-1999.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐷 ∈
ℂ ⇒ ⊢ ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + (𝐷 + 𝐵)) |
|
Theorem | add12d 7800 |
Commutative/associative law that swaps the first two terms in a triple
sum. (Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 + (𝐵 + 𝐶)) = (𝐵 + (𝐴 + 𝐶))) |