P. 120 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 11901-12000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	divdiv2 11901	Division by a fraction. (Contributed by NM, 27-Dec-2008.)
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → (𝐴 / (𝐵 / 𝐶)) = ((𝐴 · 𝐶) / 𝐵))
Theorem	recdiv2 11902	Division into a reciprocal. (Contributed by NM, 19-Oct-2007.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → ((1 / 𝐴) / 𝐵) = (1 / (𝐴 · 𝐵)))
Theorem	ddcan 11903	Cancellation in a double division. (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → (𝐴 / (𝐴 / 𝐵)) = 𝐵)
Theorem	divadddiv 11904	Addition of two ratios. Theorem I.13 of [Apostol] p. 18. (Contributed by NM, 1-Aug-2004.) (Revised by Mario Carneiro, 2-May-2016.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → ((𝐴 / 𝐶) + (𝐵 / 𝐷)) = (((𝐴 · 𝐷) + (𝐵 · 𝐶)) / (𝐶 · 𝐷)))
Theorem	divsubdiv 11905	Subtraction of two ratios. (Contributed by Scott Fenton, 22-Apr-2014.) (Revised by Mario Carneiro, 2-May-2016.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → ((𝐴 / 𝐶) − (𝐵 / 𝐷)) = (((𝐴 · 𝐷) − (𝐵 · 𝐶)) / (𝐶 · 𝐷)))
Theorem	conjmul 11906	Two numbers whose reciprocals sum to 1 are called "conjugates" and satisfy this relationship. Equation 5 of [Kreyszig] p. 12. (Contributed by NM, 12-Nov-2006.)
⊢ (((𝑃 ∈ ℂ ∧ 𝑃 ≠ 0) ∧ (𝑄 ∈ ℂ ∧ 𝑄 ≠ 0)) → (((1 / 𝑃) + (1 / 𝑄)) = 1 ↔ ((𝑃 − 1) · (𝑄 − 1)) = 1))
Theorem	rereccl 11907	Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈ ℝ)
Theorem	redivcl 11908	Closure law for division of reals. (Contributed by NM, 27-Sep-1999.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) ∈ ℝ)
Theorem	eqneg 11909	A number equal to its negative is zero. (Contributed by NM, 12-Jul-2005.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ (𝐴 ∈ ℂ → (𝐴 = -𝐴 ↔ 𝐴 = 0))
Theorem	eqnegd 11910	A complex number equals its negative iff it is zero. Deduction form of eqneg 11909. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 = -𝐴 ↔ 𝐴 = 0))
Theorem	eqnegad 11911	If a complex number equals its own negative, it is zero. One-way deduction form of eqneg 11909. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 = -𝐴)    ⇒   ⊢ (𝜑 → 𝐴 = 0)
Theorem	div2neg 11912	Quotient of two negatives. (Contributed by Paul Chapman, 10-Nov-2012.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (-𝐴 / -𝐵) = (𝐴 / 𝐵))
Theorem	divneg2 11913	Move negative sign inside of a division. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → -(𝐴 / 𝐵) = (𝐴 / -𝐵))
Theorem	recclzi 11914	Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 ≠ 0 → (1 / 𝐴) ∈ ℂ)
Theorem	recne0zi 11915	The reciprocal of a nonzero number is nonzero. (Contributed by NM, 14-May-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 ≠ 0 → (1 / 𝐴) ≠ 0)
Theorem	recidzi 11916	Multiplication of a number and its reciprocal. (Contributed by NM, 14-May-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 ≠ 0 → (𝐴 · (1 / 𝐴)) = 1)
Theorem	div1i 11917	A number divided by 1 is itself. (Contributed by NM, 9-Jan-2002.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 / 1) = 𝐴
Theorem	eqnegi 11918	A number equal to its negative is zero. (Contributed by NM, 29-May-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 = -𝐴 ↔ 𝐴 = 0)
Theorem	reccli 11919	Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐴 ≠ 0    ⇒   ⊢ (1 / 𝐴) ∈ ℂ
Theorem	recidi 11920	Multiplication of a number and its reciprocal. (Contributed by NM, 9-Feb-1995.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐴 ≠ 0    ⇒   ⊢ (𝐴 · (1 / 𝐴)) = 1
Theorem	recreci 11921	A number is equal to the reciprocal of its reciprocal. Theorem I.10 of [Apostol] p. 18. (Contributed by NM, 9-Feb-1995.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐴 ≠ 0    ⇒   ⊢ (1 / (1 / 𝐴)) = 𝐴
Theorem	dividi 11922	A number divided by itself is one. (Contributed by NM, 9-Feb-1995.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐴 ≠ 0    ⇒   ⊢ (𝐴 / 𝐴) = 1
Theorem	div0i 11923	Division into zero is zero. (Contributed by NM, 12-Aug-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐴 ≠ 0    ⇒   ⊢ (0 / 𝐴) = 0
Theorem	divclzi 11924	Closure law for division. (Contributed by NM, 7-May-1999.) (Revised by Mario Carneiro, 17-Feb-2014.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐵 ≠ 0 → (𝐴 / 𝐵) ∈ ℂ)
Theorem	divcan1zi 11925	A cancellation law for division. (Contributed by NM, 2-Oct-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐵 ≠ 0 → ((𝐴 / 𝐵) · 𝐵) = 𝐴)
Theorem	divcan2zi 11926	A cancellation law for division. (Contributed by NM, 10-Aug-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐵 ≠ 0 → (𝐵 · (𝐴 / 𝐵)) = 𝐴)
Theorem	divreczi 11927	Relationship between division and reciprocal. Theorem I.9 of [Apostol] p. 18. (Contributed by NM, 11-Oct-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐵 ≠ 0 → (𝐴 / 𝐵) = (𝐴 · (1 / 𝐵)))
Theorem	divcan3zi 11928	A cancellation law for division. (Eliminates a hypothesis of divcan3i 11935 with the weak deduction theorem.) (Contributed by NM, 3-Feb-2004.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐵 ≠ 0 → ((𝐵 · 𝐴) / 𝐵) = 𝐴)
Theorem	divcan4zi 11929	A cancellation law for division. (Contributed by NM, 12-Oct-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐵 ≠ 0 → ((𝐴 · 𝐵) / 𝐵) = 𝐴)
Theorem	rec11i 11930	Reciprocal is one-to-one. (Contributed by NM, 16-Sep-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ ((𝐴 ≠ 0 ∧ 𝐵 ≠ 0) → ((1 / 𝐴) = (1 / 𝐵) ↔ 𝐴 = 𝐵))
Theorem	divcli 11931	Closure law for division. (Contributed by NM, 2-Feb-1995.) (Revised by Mario Carneiro, 17-Feb-2014.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐵 ≠ 0    ⇒   ⊢ (𝐴 / 𝐵) ∈ ℂ
Theorem	divcan2i 11932	A cancellation law for division. (Contributed by NM, 9-Feb-1995.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐵 ≠ 0    ⇒   ⊢ (𝐵 · (𝐴 / 𝐵)) = 𝐴
Theorem	divcan1i 11933	A cancellation law for division. (Contributed by NM, 18-May-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐵 ≠ 0    ⇒   ⊢ ((𝐴 / 𝐵) · 𝐵) = 𝐴
Theorem	divreci 11934	Relationship between division and reciprocal. Theorem I.9 of [Apostol] p. 18. (Contributed by NM, 9-Feb-1995.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐵 ≠ 0    ⇒   ⊢ (𝐴 / 𝐵) = (𝐴 · (1 / 𝐵))
Theorem	divcan3i 11935	A cancellation law for division. (Contributed by NM, 16-Feb-1995.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐵 ≠ 0    ⇒   ⊢ ((𝐵 · 𝐴) / 𝐵) = 𝐴
Theorem	divcan4i 11936	A cancellation law for division. (Contributed by NM, 18-May-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐵 ≠ 0    ⇒   ⊢ ((𝐴 · 𝐵) / 𝐵) = 𝐴
Theorem	divne0i 11937	The ratio of nonzero numbers is nonzero. (Contributed by NM, 9-Feb-1995.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐴 ≠ 0    &   ⊢ 𝐵 ≠ 0    ⇒   ⊢ (𝐴 / 𝐵) ≠ 0
Theorem	rec11ii 11938	Reciprocal is one-to-one. (Contributed by NM, 16-Sep-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐴 ≠ 0    &   ⊢ 𝐵 ≠ 0    ⇒   ⊢ ((1 / 𝐴) = (1 / 𝐵) ↔ 𝐴 = 𝐵)
Theorem	divasszi 11939	An associative law for division. (Contributed by NM, 12-Aug-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ (𝐶 ≠ 0 → ((𝐴 · 𝐵) / 𝐶) = (𝐴 · (𝐵 / 𝐶)))
Theorem	divmulzi 11940	Relationship between division and multiplication. (Contributed by NM, 8-May-1999.) (Revised by Mario Carneiro, 17-Feb-2014.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ (𝐵 ≠ 0 → ((𝐴 / 𝐵) = 𝐶 ↔ (𝐵 · 𝐶) = 𝐴))
Theorem	divdirzi 11941	Distribution of division over addition. (Contributed by NM, 31-Jul-2004.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ (𝐶 ≠ 0 → ((𝐴 + 𝐵) / 𝐶) = ((𝐴 / 𝐶) + (𝐵 / 𝐶)))
Theorem	divdiv23zi 11942	Swap denominators in a division. (Contributed by NM, 15-Sep-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((𝐵 ≠ 0 ∧ 𝐶 ≠ 0) → ((𝐴 / 𝐵) / 𝐶) = ((𝐴 / 𝐶) / 𝐵))
Theorem	divmuli 11943	Relationship between division and multiplication. (Contributed by NM, 2-Feb-1995.) (Revised by Mario Carneiro, 17-Feb-2014.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐵 ≠ 0    ⇒   ⊢ ((𝐴 / 𝐵) = 𝐶 ↔ (𝐵 · 𝐶) = 𝐴)
Theorem	divdiv32i 11944	Swap denominators in a division. (Contributed by NM, 15-Sep-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐵 ≠ 0    &   ⊢ 𝐶 ≠ 0    ⇒   ⊢ ((𝐴 / 𝐵) / 𝐶) = ((𝐴 / 𝐶) / 𝐵)
Theorem	divassi 11945	An associative law for division. (Contributed by NM, 15-Feb-1995.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐶 ≠ 0    ⇒   ⊢ ((𝐴 · 𝐵) / 𝐶) = (𝐴 · (𝐵 / 𝐶))
Theorem	divdiri 11946	Distribution of division over addition. (Contributed by NM, 16-Feb-1995.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐶 ≠ 0    ⇒   ⊢ ((𝐴 + 𝐵) / 𝐶) = ((𝐴 / 𝐶) + (𝐵 / 𝐶))
Theorem	div23i 11947	A commutative/associative law for division. (Contributed by NM, 3-Sep-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐶 ≠ 0    ⇒   ⊢ ((𝐴 · 𝐵) / 𝐶) = ((𝐴 / 𝐶) · 𝐵)
Theorem	div11i 11948	One-to-one relationship for division. (Contributed by NM, 20-Aug-2001.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐶 ≠ 0    ⇒   ⊢ ((𝐴 / 𝐶) = (𝐵 / 𝐶) ↔ 𝐴 = 𝐵)
Theorem	divmuldivi 11949	Multiplication of two ratios. Theorem I.14 of [Apostol] p. 18. (Contributed by NM, 16-Feb-1995.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐷 ∈ ℂ    &   ⊢ 𝐵 ≠ 0    &   ⊢ 𝐷 ≠ 0    ⇒   ⊢ ((𝐴 / 𝐵) · (𝐶 / 𝐷)) = ((𝐴 · 𝐶) / (𝐵 · 𝐷))
Theorem	divmul13i 11950	Swap denominators of two ratios. (Contributed by NM, 6-Aug-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐷 ∈ ℂ    &   ⊢ 𝐵 ≠ 0    &   ⊢ 𝐷 ≠ 0    ⇒   ⊢ ((𝐴 / 𝐵) · (𝐶 / 𝐷)) = ((𝐶 / 𝐵) · (𝐴 / 𝐷))
Theorem	divadddivi 11951	Addition of two ratios. Theorem I.13 of [Apostol] p. 18. (Contributed by NM, 21-Feb-1995.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐷 ∈ ℂ    &   ⊢ 𝐵 ≠ 0    &   ⊢ 𝐷 ≠ 0    ⇒   ⊢ ((𝐴 / 𝐵) + (𝐶 / 𝐷)) = (((𝐴 · 𝐷) + (𝐶 · 𝐵)) / (𝐵 · 𝐷))
Theorem	divdivdivi 11952	Division of two ratios. Theorem I.15 of [Apostol] p. 18. (Contributed by NM, 22-Feb-1995.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐷 ∈ ℂ    &   ⊢ 𝐵 ≠ 0    &   ⊢ 𝐷 ≠ 0    &   ⊢ 𝐶 ≠ 0    ⇒   ⊢ ((𝐴 / 𝐵) / (𝐶 / 𝐷)) = ((𝐴 · 𝐷) / (𝐵 · 𝐶))
Theorem	rerecclzi 11953	Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ (𝐴 ≠ 0 → (1 / 𝐴) ∈ ℝ)
Theorem	rereccli 11954	Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐴 ≠ 0    ⇒   ⊢ (1 / 𝐴) ∈ ℝ
Theorem	redivclzi 11955	Closure law for division of reals. (Contributed by NM, 9-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐵 ≠ 0 → (𝐴 / 𝐵) ∈ ℝ)
Theorem	redivcli 11956	Closure law for division of reals. (Contributed by NM, 9-May-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐵 ≠ 0    ⇒   ⊢ (𝐴 / 𝐵) ∈ ℝ
Theorem	div1d 11957	A number divided by 1 is itself. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 / 1) = 𝐴)
Theorem	reccld 11958	Closure law for reciprocal. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (1 / 𝐴) ∈ ℂ)
Theorem	recne0d 11959	The reciprocal of a nonzero number is nonzero. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (1 / 𝐴) ≠ 0)
Theorem	recidd 11960	Multiplication of a number and its reciprocal. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 · (1 / 𝐴)) = 1)
Theorem	recid2d 11961	Multiplication of a number and its reciprocal. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → ((1 / 𝐴) · 𝐴) = 1)
Theorem	recrecd 11962	A number is equal to the reciprocal of its reciprocal. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (1 / (1 / 𝐴)) = 𝐴)
Theorem	dividd 11963	A number divided by itself is one. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐴) = 1)
Theorem	div0d 11964	Division into zero is zero. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (0 / 𝐴) = 0)
Theorem	divcld 11965	Closure law for division. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℂ)
Theorem	divcan1d 11966	A cancellation law for division. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) · 𝐵) = 𝐴)
Theorem	divcan2d 11967	A cancellation law for division. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐵 · (𝐴 / 𝐵)) = 𝐴)
Theorem	divrecd 11968	Relationship between division and reciprocal. Theorem I.9 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) = (𝐴 · (1 / 𝐵)))
Theorem	divrec2d 11969	Relationship between division and reciprocal. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) = ((1 / 𝐵) · 𝐴))
Theorem	divcan3d 11970	A cancellation law for division. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐵 · 𝐴) / 𝐵) = 𝐴)
Theorem	divcan4d 11971	A cancellation law for division. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) / 𝐵) = 𝐴)
Theorem	diveq0d 11972	A ratio is zero iff the numerator is zero. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → (𝐴 / 𝐵) = 0)    ⇒   ⊢ (𝜑 → 𝐴 = 0)
Theorem	diveq1d 11973	Equality in terms of unit ratio. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → (𝐴 / 𝐵) = 1)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	diveq1ad 11974	The quotient of two complex numbers is one iff they are equal. Deduction form of diveq1 11874. Generalization of diveq1d 11973. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) = 1 ↔ 𝐴 = 𝐵))
Theorem	diveq0ad 11975	A fraction of complex numbers is zero iff its numerator is. Deduction form of diveq0 11854. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) = 0 ↔ 𝐴 = 0))
Theorem	divne1d 11976	If two complex numbers are unequal, their quotient is not one. Contrapositive of diveq1d 11973. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) ≠ 1)
Theorem	divne0bd 11977	A ratio is zero iff the numerator is zero. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 ≠ 0 ↔ (𝐴 / 𝐵) ≠ 0))
Theorem	divnegd 11978	Move negative sign inside of a division. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → -(𝐴 / 𝐵) = (-𝐴 / 𝐵))
Theorem	divneg2d 11979	Move negative sign inside of a division. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → -(𝐴 / 𝐵) = (𝐴 / -𝐵))
Theorem	div2negd 11980	Quotient of two negatives. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (-𝐴 / -𝐵) = (𝐴 / 𝐵))
Theorem	divne0d 11981	The ratio of nonzero numbers is nonzero. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) ≠ 0)
Theorem	recdivd 11982	The reciprocal of a ratio. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (1 / (𝐴 / 𝐵)) = (𝐵 / 𝐴))
Theorem	recdiv2d 11983	Division into a reciprocal. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ((1 / 𝐴) / 𝐵) = (1 / (𝐴 · 𝐵)))
Theorem	divcan6d 11984	Cancellation of inverted fractions. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) · (𝐵 / 𝐴)) = 1)
Theorem	ddcand 11985	Cancellation in a double division. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 / (𝐴 / 𝐵)) = 𝐵)
Theorem	rec11d 11986	Reciprocal is one-to-one. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → (1 / 𝐴) = (1 / 𝐵))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	divmuld 11987	Relationship between division and multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) = 𝐶 ↔ (𝐵 · 𝐶) = 𝐴))
Theorem	div32d 11988	A commutative/associative law for division. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) · 𝐶) = (𝐴 · (𝐶 / 𝐵)))
Theorem	div13d 11989	A commutative/associative law for division. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) · 𝐶) = ((𝐶 / 𝐵) · 𝐴))
Theorem	divdiv32d 11990	Swap denominators in a division. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) / 𝐶) = ((𝐴 / 𝐶) / 𝐵))
Theorem	divcan5d 11991	Cancellation of common factor in a ratio. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐶 · 𝐴) / (𝐶 · 𝐵)) = (𝐴 / 𝐵))
Theorem	divcan5rd 11992	Cancellation of common factor in a ratio. (Contributed by Mario Carneiro, 1-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐶) / (𝐵 · 𝐶)) = (𝐴 / 𝐵))
Theorem	divcan7d 11993	Cancel equal divisors in a division. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐶) / (𝐵 / 𝐶)) = (𝐴 / 𝐵))
Theorem	dmdcand 11994	Cancellation law for division and multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐵 / 𝐶) · (𝐴 / 𝐵)) = (𝐴 / 𝐶))
Theorem	dmdcan2d 11995	Cancellation law for division and multiplication. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) · (𝐵 / 𝐶)) = (𝐴 / 𝐶))
Theorem	divdiv1d 11996	Division into a fraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) / 𝐶) = (𝐴 / (𝐵 · 𝐶)))
Theorem	divdiv2d 11997	Division by a fraction. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 / (𝐵 / 𝐶)) = ((𝐴 · 𝐶) / 𝐵))
Theorem	divmul2d 11998	Relationship between division and multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐶) = 𝐵 ↔ 𝐴 = (𝐶 · 𝐵)))
Theorem	divmul3d 11999	Relationship between division and multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐶) = 𝐵 ↔ 𝐴 = (𝐵 · 𝐶)))
Theorem	divassd 12000	An associative law for division. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) / 𝐶) = (𝐴 · (𝐵 / 𝐶)))