Theorem List for Intuitionistic Logic Explorer - 8501-8600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | mulext1 8501 |
Left extensionality for complex multiplication. (Contributed by Jim
Kingdon, 22-Feb-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐶) # (𝐵 · 𝐶) → 𝐴 # 𝐵)) |
|
Theorem | mulext2 8502 |
Right extensionality for complex multiplication. (Contributed by Jim
Kingdon, 22-Feb-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐶 · 𝐴) # (𝐶 · 𝐵) → 𝐴 # 𝐵)) |
|
Theorem | mulext 8503 |
Strong extensionality for multiplication. Given excluded middle,
apartness would be equivalent to negated equality and this would follow
readily (for all operations) from oveq12 5845. For us, it is proved a
different way. (Contributed by Jim Kingdon, 23-Feb-2020.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 · 𝐵) # (𝐶 · 𝐷) → (𝐴 # 𝐶 ∨ 𝐵 # 𝐷))) |
|
Theorem | mulap0r 8504 |
A product apart from zero. Lemma 2.13 of [Geuvers], p. 6. (Contributed
by Jim Kingdon, 24-Feb-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐴 · 𝐵) # 0) → (𝐴 # 0 ∧ 𝐵 # 0)) |
|
Theorem | msqge0 8505 |
A square is nonnegative. Lemma 2.35 of [Geuvers], p. 9. (Contributed by
NM, 23-May-2007.) (Revised by Mario Carneiro, 27-May-2016.)
|
⊢ (𝐴 ∈ ℝ → 0 ≤ (𝐴 · 𝐴)) |
|
Theorem | msqge0i 8506 |
A square is nonnegative. (Contributed by NM, 14-May-1999.) (Proof
shortened by Andrew Salmon, 19-Nov-2011.)
|
⊢ 𝐴 ∈ ℝ
⇒ ⊢ 0 ≤ (𝐴 · 𝐴) |
|
Theorem | msqge0d 8507 |
A square is nonnegative. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ)
⇒ ⊢ (𝜑 → 0 ≤ (𝐴 · 𝐴)) |
|
Theorem | mulge0 8508 |
The product of two nonnegative numbers is nonnegative. (Contributed by
NM, 8-Oct-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 0 ≤ (𝐴 · 𝐵)) |
|
Theorem | mulge0i 8509 |
The product of two nonnegative numbers is nonnegative. (Contributed by
NM, 30-Jul-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → 0 ≤ (𝐴 · 𝐵)) |
|
Theorem | mulge0d 8510 |
The product of two nonnegative numbers is nonnegative. (Contributed by
Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴)
& ⊢ (𝜑 → 0 ≤ 𝐵) ⇒ ⊢ (𝜑 → 0 ≤ (𝐴 · 𝐵)) |
|
Theorem | apti 8511 |
Complex apartness is tight. (Contributed by Jim Kingdon,
21-Feb-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 = 𝐵 ↔ ¬ 𝐴 # 𝐵)) |
|
Theorem | apne 8512 |
Apartness implies negated equality. We cannot in general prove the
converse (as shown at neapmkv 13786), which is the whole point of having
separate notations for apartness and negated equality. (Contributed by
Jim Kingdon, 21-Feb-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 # 𝐵 → 𝐴 ≠ 𝐵)) |
|
Theorem | apcon4bid 8513 |
Contrapositive law deduction for apartness. (Contributed by Jim
Kingdon, 31-Jul-2023.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → (𝐴 # 𝐵 ↔ 𝐶 # 𝐷)) ⇒ ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷)) |
|
Theorem | leltap 8514 |
≤ implies 'less than' is 'apart'. (Contributed by
Jim Kingdon,
13-Aug-2021.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (𝐴 < 𝐵 ↔ 𝐵 # 𝐴)) |
|
Theorem | gt0ap0 8515 |
Positive implies apart from zero. (Contributed by Jim Kingdon,
27-Feb-2020.)
|
⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴) → 𝐴 # 0) |
|
Theorem | gt0ap0i 8516 |
Positive means apart from zero (useful for ordering theorems involving
division). (Contributed by Jim Kingdon, 27-Feb-2020.)
|
⊢ 𝐴 ∈ ℝ
⇒ ⊢ (0 < 𝐴 → 𝐴 # 0) |
|
Theorem | gt0ap0ii 8517 |
Positive implies apart from zero. (Contributed by Jim Kingdon,
27-Feb-2020.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 0 < 𝐴 ⇒ ⊢ 𝐴 # 0 |
|
Theorem | gt0ap0d 8518 |
Positive implies apart from zero. Because of the way we define
#, 𝐴 must be an element of ℝ, not just ℝ*.
(Contributed by Jim Kingdon, 27-Feb-2020.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐴) ⇒ ⊢ (𝜑 → 𝐴 # 0) |
|
Theorem | negap0 8519 |
A number is apart from zero iff its negative is apart from zero.
(Contributed by Jim Kingdon, 27-Feb-2020.)
|
⊢ (𝐴 ∈ ℂ → (𝐴 # 0 ↔ -𝐴 # 0)) |
|
Theorem | negap0d 8520 |
The negative of a number apart from zero is apart from zero.
(Contributed by Jim Kingdon, 25-Feb-2024.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 # 0) ⇒ ⊢ (𝜑 → -𝐴 # 0) |
|
Theorem | ltleap 8521 |
Less than in terms of non-strict order and apartness. (Contributed by Jim
Kingdon, 28-Feb-2020.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐴 # 𝐵))) |
|
Theorem | ltap 8522 |
'Less than' implies apart. (Contributed by Jim Kingdon, 12-Aug-2021.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐵 # 𝐴) |
|
Theorem | gtapii 8523 |
'Greater than' implies apart. (Contributed by Jim Kingdon,
12-Aug-2021.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐴 < 𝐵 ⇒ ⊢ 𝐵 # 𝐴 |
|
Theorem | ltapii 8524 |
'Less than' implies apart. (Contributed by Jim Kingdon,
12-Aug-2021.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐴 < 𝐵 ⇒ ⊢ 𝐴 # 𝐵 |
|
Theorem | ltapi 8525 |
'Less than' implies apart. (Contributed by Jim Kingdon,
12-Aug-2021.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ (𝐴 < 𝐵 → 𝐵 # 𝐴) |
|
Theorem | gtapd 8526 |
'Greater than' implies apart. (Contributed by Jim Kingdon,
12-Aug-2021.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐵 # 𝐴) |
|
Theorem | ltapd 8527 |
'Less than' implies apart. (Contributed by Jim Kingdon,
12-Aug-2021.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → 𝐴 # 𝐵) |
|
Theorem | leltapd 8528 |
≤ implies 'less than' is 'apart'. (Contributed by
Jim Kingdon,
13-Aug-2021.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 𝐵 # 𝐴)) |
|
Theorem | ap0gt0 8529 |
A nonnegative number is apart from zero if and only if it is positive.
(Contributed by Jim Kingdon, 11-Aug-2021.)
|
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (𝐴 # 0 ↔ 0 < 𝐴)) |
|
Theorem | ap0gt0d 8530 |
A nonzero nonnegative number is positive. (Contributed by Jim
Kingdon, 11-Aug-2021.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴)
& ⊢ (𝜑 → 𝐴 # 0) ⇒ ⊢ (𝜑 → 0 < 𝐴) |
|
Theorem | apsub1 8531 |
Subtraction respects apartness. Analogue of subcan2 8114 for apartness.
(Contributed by Jim Kingdon, 6-Jan-2022.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 # 𝐵 ↔ (𝐴 − 𝐶) # (𝐵 − 𝐶))) |
|
Theorem | subap0 8532 |
Two numbers being apart is equivalent to their difference being apart from
zero. (Contributed by Jim Kingdon, 25-Dec-2022.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) # 0 ↔ 𝐴 # 𝐵)) |
|
Theorem | subap0d 8533 |
Two numbers apart from each other have difference apart from zero.
(Contributed by Jim Kingdon, 12-Aug-2021.) (Proof shortened by BJ,
15-Aug-2024.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 # 𝐵) ⇒ ⊢ (𝜑 → (𝐴 − 𝐵) # 0) |
|
Theorem | cnstab 8534 |
Equality of complex numbers is stable. Stability here means
¬ ¬ 𝐴 = 𝐵 → 𝐴 = 𝐵 as defined at df-stab 821. This theorem for real
numbers is Proposition 5.2 of [BauerHanson], p. 27. (Contributed by Jim
Kingdon, 1-Aug-2023.) (Proof shortened by BJ, 15-Aug-2024.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → STAB
𝐴 = 𝐵) |
|
Theorem | aprcl 8535 |
Reverse closure for apartness. (Contributed by Jim Kingdon,
19-Dec-2023.)
|
⊢ (𝐴 # 𝐵 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ)) |
|
Theorem | apsscn 8536* |
The points apart from a given point are complex numbers. (Contributed
by Jim Kingdon, 19-Dec-2023.)
|
⊢ {𝑥 ∈ 𝐴 ∣ 𝑥 # 𝐵} ⊆ ℂ |
|
Theorem | lt0ap0 8537 |
A number which is less than zero is apart from zero. (Contributed by Jim
Kingdon, 25-Feb-2024.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < 0) → 𝐴 # 0) |
|
Theorem | lt0ap0d 8538 |
A real number less than zero is apart from zero. Deduction form.
(Contributed by Jim Kingdon, 24-Feb-2024.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 0) ⇒ ⊢ (𝜑 → 𝐴 # 0) |
|
4.3.7 Reciprocals
|
|
Theorem | recextlem1 8539 |
Lemma for recexap 8541. (Contributed by Eric Schmidt, 23-May-2007.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + (i · 𝐵)) · (𝐴 − (i · 𝐵))) = ((𝐴 · 𝐴) + (𝐵 · 𝐵))) |
|
Theorem | recexaplem2 8540 |
Lemma for recexap 8541. (Contributed by Jim Kingdon, 20-Feb-2020.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐴 + (i · 𝐵)) # 0) → ((𝐴 · 𝐴) + (𝐵 · 𝐵)) # 0) |
|
Theorem | recexap 8541* |
Existence of reciprocal of nonzero complex number. (Contributed by Jim
Kingdon, 20-Feb-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → ∃𝑥 ∈ ℂ (𝐴 · 𝑥) = 1) |
|
Theorem | mulap0 8542 |
The product of two numbers apart from zero is apart from zero. Lemma
2.15 of [Geuvers], p. 6. (Contributed
by Jim Kingdon, 22-Feb-2020.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0)) → (𝐴 · 𝐵) # 0) |
|
Theorem | mulap0b 8543 |
The product of two numbers apart from zero is apart from zero.
(Contributed by Jim Kingdon, 24-Feb-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 # 0 ∧ 𝐵 # 0) ↔ (𝐴 · 𝐵) # 0)) |
|
Theorem | mulap0i 8544 |
The product of two numbers apart from zero is apart from zero.
(Contributed by Jim Kingdon, 23-Feb-2020.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐴 # 0 & ⊢ 𝐵 # 0
⇒ ⊢ (𝐴 · 𝐵) # 0 |
|
Theorem | mulap0bd 8545 |
The product of two numbers apart from zero is apart from zero. Exercise
11.11 of [HoTT], p. (varies).
(Contributed by Jim Kingdon,
24-Feb-2020.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 # 0 ∧ 𝐵 # 0) ↔ (𝐴 · 𝐵) # 0)) |
|
Theorem | mulap0d 8546 |
The product of two numbers apart from zero is apart from zero.
(Contributed by Jim Kingdon, 23-Feb-2020.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 # 0) & ⊢ (𝜑 → 𝐵 # 0) ⇒ ⊢ (𝜑 → (𝐴 · 𝐵) # 0) |
|
Theorem | mulap0bad 8547 |
A factor of a complex number apart from zero is apart from zero.
Partial converse of mulap0d 8546 and consequence of mulap0bd 8545.
(Contributed by Jim Kingdon, 24-Feb-2020.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝐴 · 𝐵) # 0) ⇒ ⊢ (𝜑 → 𝐴 # 0) |
|
Theorem | mulap0bbd 8548 |
A factor of a complex number apart from zero is apart from zero.
Partial converse of mulap0d 8546 and consequence of mulap0bd 8545.
(Contributed by Jim Kingdon, 24-Feb-2020.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝐴 · 𝐵) # 0) ⇒ ⊢ (𝜑 → 𝐵 # 0) |
|
Theorem | mulcanapd 8549 |
Cancellation law for multiplication. (Contributed by Jim Kingdon,
21-Feb-2020.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐶 # 0) ⇒ ⊢ (𝜑 → ((𝐶 · 𝐴) = (𝐶 · 𝐵) ↔ 𝐴 = 𝐵)) |
|
Theorem | mulcanap2d 8550 |
Cancellation law for multiplication. (Contributed by Jim Kingdon,
21-Feb-2020.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐶 # 0) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐶) = (𝐵 · 𝐶) ↔ 𝐴 = 𝐵)) |
|
Theorem | mulcanapad 8551 |
Cancellation of a nonzero factor on the left in an equation. One-way
deduction form of mulcanapd 8549. (Contributed by Jim Kingdon,
21-Feb-2020.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐶 # 0) & ⊢ (𝜑 → (𝐶 · 𝐴) = (𝐶 · 𝐵)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) |
|
Theorem | mulcanap2ad 8552 |
Cancellation of a nonzero factor on the right in an equation. One-way
deduction form of mulcanap2d 8550. (Contributed by Jim Kingdon,
21-Feb-2020.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐶 # 0) & ⊢ (𝜑 → (𝐴 · 𝐶) = (𝐵 · 𝐶)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) |
|
Theorem | mulcanap 8553 |
Cancellation law for multiplication (full theorem form). (Contributed by
Jim Kingdon, 21-Feb-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐶 · 𝐴) = (𝐶 · 𝐵) ↔ 𝐴 = 𝐵)) |
|
Theorem | mulcanap2 8554 |
Cancellation law for multiplication. (Contributed by Jim Kingdon,
21-Feb-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐴 · 𝐶) = (𝐵 · 𝐶) ↔ 𝐴 = 𝐵)) |
|
Theorem | mulcanapi 8555 |
Cancellation law for multiplication. (Contributed by Jim Kingdon,
21-Feb-2020.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐶 # 0
⇒ ⊢ ((𝐶 · 𝐴) = (𝐶 · 𝐵) ↔ 𝐴 = 𝐵) |
|
Theorem | muleqadd 8556 |
Property of numbers whose product equals their sum. Equation 5 of
[Kreyszig] p. 12. (Contributed by NM,
13-Nov-2006.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · 𝐵) = (𝐴 + 𝐵) ↔ ((𝐴 − 1) · (𝐵 − 1)) = 1)) |
|
Theorem | receuap 8557* |
Existential uniqueness of reciprocals. (Contributed by Jim Kingdon,
21-Feb-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → ∃!𝑥 ∈ ℂ (𝐵 · 𝑥) = 𝐴) |
|
Theorem | mul0eqap 8558 |
If two numbers are apart from each other and their product is zero, one
of them must be zero. (Contributed by Jim Kingdon, 31-Jul-2023.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 # 𝐵)
& ⊢ (𝜑 → (𝐴 · 𝐵) = 0) ⇒ ⊢ (𝜑 → (𝐴 = 0 ∨ 𝐵 = 0)) |
|
4.3.8 Division
|
|
Syntax | cdiv 8559 |
Extend class notation to include division.
|
class / |
|
Definition | df-div 8560* |
Define division. Theorem divmulap 8562 relates it to multiplication, and
divclap 8565 and redivclap 8618 prove its closure laws. (Contributed by NM,
2-Feb-1995.) Use divvalap 8561 instead. (Revised by Mario Carneiro,
1-Apr-2014.) (New usage is discouraged.)
|
⊢ / = (𝑥 ∈ ℂ, 𝑦 ∈ (ℂ ∖ {0}) ↦
(℩𝑧 ∈
ℂ (𝑦 · 𝑧) = 𝑥)) |
|
Theorem | divvalap 8561* |
Value of division: the (unique) element 𝑥 such that
(𝐵
· 𝑥) = 𝐴. This is meaningful
only when 𝐵 is apart from
zero. (Contributed by Jim Kingdon, 21-Feb-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → (𝐴 / 𝐵) = (℩𝑥 ∈ ℂ (𝐵 · 𝑥) = 𝐴)) |
|
Theorem | divmulap 8562 |
Relationship between division and multiplication. (Contributed by Jim
Kingdon, 22-Feb-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐴 / 𝐶) = 𝐵 ↔ (𝐶 · 𝐵) = 𝐴)) |
|
Theorem | divmulap2 8563 |
Relationship between division and multiplication. (Contributed by Jim
Kingdon, 22-Feb-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐴 / 𝐶) = 𝐵 ↔ 𝐴 = (𝐶 · 𝐵))) |
|
Theorem | divmulap3 8564 |
Relationship between division and multiplication. (Contributed by Jim
Kingdon, 22-Feb-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐴 / 𝐶) = 𝐵 ↔ 𝐴 = (𝐵 · 𝐶))) |
|
Theorem | divclap 8565 |
Closure law for division. (Contributed by Jim Kingdon, 22-Feb-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → (𝐴 / 𝐵) ∈ ℂ) |
|
Theorem | recclap 8566 |
Closure law for reciprocal. (Contributed by Jim Kingdon, 22-Feb-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (1 / 𝐴) ∈ ℂ) |
|
Theorem | divcanap2 8567 |
A cancellation law for division. (Contributed by Jim Kingdon,
22-Feb-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → (𝐵 · (𝐴 / 𝐵)) = 𝐴) |
|
Theorem | divcanap1 8568 |
A cancellation law for division. (Contributed by Jim Kingdon,
22-Feb-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → ((𝐴 / 𝐵) · 𝐵) = 𝐴) |
|
Theorem | diveqap0 8569 |
A ratio is zero iff the numerator is zero. (Contributed by Jim Kingdon,
22-Feb-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → ((𝐴 / 𝐵) = 0 ↔ 𝐴 = 0)) |
|
Theorem | divap0b 8570 |
The ratio of numbers apart from zero is apart from zero. (Contributed by
Jim Kingdon, 22-Feb-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → (𝐴 # 0 ↔ (𝐴 / 𝐵) # 0)) |
|
Theorem | divap0 8571 |
The ratio of numbers apart from zero is apart from zero. (Contributed by
Jim Kingdon, 22-Feb-2020.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0)) → (𝐴 / 𝐵) # 0) |
|
Theorem | recap0 8572 |
The reciprocal of a number apart from zero is apart from zero.
(Contributed by Jim Kingdon, 24-Feb-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (1 / 𝐴) # 0) |
|
Theorem | recidap 8573 |
Multiplication of a number and its reciprocal. (Contributed by Jim
Kingdon, 24-Feb-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (𝐴 · (1 / 𝐴)) = 1) |
|
Theorem | recidap2 8574 |
Multiplication of a number and its reciprocal. (Contributed by Jim
Kingdon, 24-Feb-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → ((1 / 𝐴) · 𝐴) = 1) |
|
Theorem | divrecap 8575 |
Relationship between division and reciprocal. (Contributed by Jim
Kingdon, 24-Feb-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → (𝐴 / 𝐵) = (𝐴 · (1 / 𝐵))) |
|
Theorem | divrecap2 8576 |
Relationship between division and reciprocal. (Contributed by Jim
Kingdon, 25-Feb-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → (𝐴 / 𝐵) = ((1 / 𝐵) · 𝐴)) |
|
Theorem | divassap 8577 |
An associative law for division. (Contributed by Jim Kingdon,
25-Feb-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐴 · 𝐵) / 𝐶) = (𝐴 · (𝐵 / 𝐶))) |
|
Theorem | div23ap 8578 |
A commutative/associative law for division. (Contributed by Jim Kingdon,
25-Feb-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐴 · 𝐵) / 𝐶) = ((𝐴 / 𝐶) · 𝐵)) |
|
Theorem | div32ap 8579 |
A commutative/associative law for division. (Contributed by Jim Kingdon,
25-Feb-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0) ∧ 𝐶 ∈ ℂ) → ((𝐴 / 𝐵) · 𝐶) = (𝐴 · (𝐶 / 𝐵))) |
|
Theorem | div13ap 8580 |
A commutative/associative law for division. (Contributed by Jim Kingdon,
25-Feb-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0) ∧ 𝐶 ∈ ℂ) → ((𝐴 / 𝐵) · 𝐶) = ((𝐶 / 𝐵) · 𝐴)) |
|
Theorem | div12ap 8581 |
A commutative/associative law for division. (Contributed by Jim Kingdon,
25-Feb-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → (𝐴 · (𝐵 / 𝐶)) = (𝐵 · (𝐴 / 𝐶))) |
|
Theorem | divmulassap 8582 |
An associative law for division and multiplication. (Contributed by Jim
Kingdon, 24-Jan-2022.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐷 # 0)) → ((𝐴 · (𝐵 / 𝐷)) · 𝐶) = ((𝐴 · 𝐵) · (𝐶 / 𝐷))) |
|
Theorem | divmulasscomap 8583 |
An associative/commutative law for division and multiplication.
(Contributed by Jim Kingdon, 24-Jan-2022.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐷 # 0)) → ((𝐴 · (𝐵 / 𝐷)) · 𝐶) = (𝐵 · ((𝐴 · 𝐶) / 𝐷))) |
|
Theorem | divdirap 8584 |
Distribution of division over addition. (Contributed by Jim Kingdon,
25-Feb-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐴 + 𝐵) / 𝐶) = ((𝐴 / 𝐶) + (𝐵 / 𝐶))) |
|
Theorem | divcanap3 8585 |
A cancellation law for division. (Contributed by Jim Kingdon,
25-Feb-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → ((𝐵 · 𝐴) / 𝐵) = 𝐴) |
|
Theorem | divcanap4 8586 |
A cancellation law for division. (Contributed by Jim Kingdon,
25-Feb-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → ((𝐴 · 𝐵) / 𝐵) = 𝐴) |
|
Theorem | div11ap 8587 |
One-to-one relationship for division. (Contributed by Jim Kingdon,
25-Feb-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐴 / 𝐶) = (𝐵 / 𝐶) ↔ 𝐴 = 𝐵)) |
|
Theorem | dividap 8588 |
A number divided by itself is one. (Contributed by Jim Kingdon,
25-Feb-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (𝐴 / 𝐴) = 1) |
|
Theorem | div0ap 8589 |
Division into zero is zero. (Contributed by Jim Kingdon, 25-Feb-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (0 / 𝐴) = 0) |
|
Theorem | div1 8590 |
A number divided by 1 is itself. (Contributed by NM, 9-Jan-2002.) (Proof
shortened by Mario Carneiro, 27-May-2016.)
|
⊢ (𝐴 ∈ ℂ → (𝐴 / 1) = 𝐴) |
|
Theorem | 1div1e1 8591 |
1 divided by 1 is 1 (common case). (Contributed by David A. Wheeler,
7-Dec-2018.)
|
⊢ (1 / 1) = 1 |
|
Theorem | diveqap1 8592 |
Equality in terms of unit ratio. (Contributed by Jim Kingdon,
25-Feb-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → ((𝐴 / 𝐵) = 1 ↔ 𝐴 = 𝐵)) |
|
Theorem | divnegap 8593 |
Move negative sign inside of a division. (Contributed by Jim Kingdon,
25-Feb-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → -(𝐴 / 𝐵) = (-𝐴 / 𝐵)) |
|
Theorem | muldivdirap 8594 |
Distribution of division over addition with a multiplication.
(Contributed by Jim Kingdon, 11-Nov-2021.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → (((𝐶 · 𝐴) + 𝐵) / 𝐶) = (𝐴 + (𝐵 / 𝐶))) |
|
Theorem | divsubdirap 8595 |
Distribution of division over subtraction. (Contributed by NM,
4-Mar-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐴 − 𝐵) / 𝐶) = ((𝐴 / 𝐶) − (𝐵 / 𝐶))) |
|
Theorem | recrecap 8596 |
A number is equal to the reciprocal of its reciprocal. (Contributed by
Jim Kingdon, 25-Feb-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (1 / (1 / 𝐴)) = 𝐴) |
|
Theorem | rec11ap 8597 |
Reciprocal is one-to-one. (Contributed by Jim Kingdon, 25-Feb-2020.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0)) → ((1 / 𝐴) = (1 / 𝐵) ↔ 𝐴 = 𝐵)) |
|
Theorem | rec11rap 8598 |
Mutual reciprocals. (Contributed by Jim Kingdon, 25-Feb-2020.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0)) → ((1 / 𝐴) = 𝐵 ↔ (1 / 𝐵) = 𝐴)) |
|
Theorem | divmuldivap 8599 |
Multiplication of two ratios. (Contributed by Jim Kingdon,
25-Feb-2020.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 # 0))) → ((𝐴 / 𝐶) · (𝐵 / 𝐷)) = ((𝐴 · 𝐵) / (𝐶 · 𝐷))) |
|
Theorem | divdivdivap 8600 |
Division of two ratios. Theorem I.15 of [Apostol] p. 18. (Contributed by
Jim Kingdon, 25-Feb-2020.)
|
⊢ (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 # 0))) → ((𝐴 / 𝐵) / (𝐶 / 𝐷)) = ((𝐴 · 𝐷) / (𝐵 · 𝐶))) |