P. 244 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 24301-24400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	logrec 24301	Logarithm of a reciprocal changes sign. (Contributed by Saveliy Skresanov, 28-Dec-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ (ℑ‘(log‘𝐴)) ≠ π) → (log‘𝐴) = -(log‘(1 / 𝐴)))
14.3.5  Logarithms to an arbitrary base Define "log using an arbitrary base" function and then prove some of its properties. Note that logb is generalized to an arbitrary base and arbitrary parameter in ℂ, but it doesn't accept infinities as arguments, unlike log. Metamath doesn't care what letters are used to represent classes. Usually classes begin with the letter "A", but here we use "B" and "X" to more clearly distinguish between "base" and "other parameter of log". There are different ways this could be defined in Metamath. The approach used here is intentionally similar to existing 2-parameter Metamath functions (operations): (𝐵 logb 𝑋) where 𝐵 is the base and 𝑋 is the argument of the logarithm function. An alternative would be to support the notational form (( logb ‘𝐵)‘𝑋); that looks a little more like traditional notation. Such a function ( logb ‘𝐵) for a fixed base can be obtained in Metamath (without the need for a new definition) by the curry function: (curry logb ‘𝐵), see logbmpt 24326, logbf 24327 and logbfval 24328.
Syntax	clogb 24302	Extend class notation to include the logarithm generalized to an arbitrary base.
class logb
Definition	df-logb 24303*	Define the logb operator. This is the logarithm generalized to an arbitrary base. It can be used as (𝐵 logb 𝑋) for "log base B of X". In the most common traditional notation, base B is a subscript of "log". The definition is according to Wikipedia "Complex logarithm": https://en.wikipedia.org/wiki/Complex_logarithm#Logarithms_to_other_bases (10-Jun-2020). (Contributed by David A. Wheeler, 21-Jan-2017.)
⊢ logb = (𝑥 ∈ (ℂ ∖ {0, 1}), 𝑦 ∈ (ℂ ∖ {0}) ↦ ((log‘𝑦) / (log‘𝑥)))
Theorem	logbval 24304	Define the value of the logb function, the logarithm generalized to an arbitrary base, when used as infix. Most Metamath statements select variables in order of their use, but to make the order clearer we use "B" for base and "X" for the argument of the logarithm function here. (Contributed by David A. Wheeler, 21-Jan-2017.) (Revised by David A. Wheeler, 16-Jul-2017.)
⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ 𝑋 ∈ (ℂ ∖ {0})) → (𝐵 logb 𝑋) = ((log‘𝑋) / (log‘𝐵)))
Theorem	logbcl 24305	General logarithm closure. (Contributed by David A. Wheeler, 17-Jul-2017.)
⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ 𝑋 ∈ (ℂ ∖ {0})) → (𝐵 logb 𝑋) ∈ ℂ)
Theorem	logbid1 24306	General logarithm is 1 when base and arg match. Property 1(a) of [Cohen4] p. 361. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by David A. Wheeler, 22-Jul-2017.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (𝐴 logb 𝐴) = 1)
Theorem	logb1 24307	The logarithm of 1 to an arbitrary base 𝐵 is 0. Property 1(b) of [Cohen4] p. 361. See log1 24136. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by Thierry Arnoux, 27-Sep-2017.)
⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) → (𝐵 logb 1) = 0)
Theorem	elogb 24308	The general logarithm of a number to the base being Euler's constant is the natural logarithm of the number. Put another way, using e as the base in logb is the same as log. Definition in [Cohen4] p. 352. (Contributed by David A. Wheeler, 17-Oct-2017.) (Revised by David A. Wheeler and AV, 16-Jun-2020.)
⊢ (𝐴 ∈ (ℂ ∖ {0}) → (e logb 𝐴) = (log‘𝐴))
Theorem	logbchbase 24309	Change of base for logarithms. Property in [Cohen4] p. 367. (Contributed by AV, 11-Jun-2020.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) ∧ 𝑋 ∈ (ℂ ∖ {0})) → (𝐴 logb 𝑋) = ((𝐵 logb 𝑋) / (𝐵 logb 𝐴)))
Theorem	relogbval 24310	Value of the general logarithm with integer base. (Contributed by Thierry Arnoux, 27-Sep-2017.)
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑋 ∈ ℝ+) → (𝐵 logb 𝑋) = ((log‘𝑋) / (log‘𝐵)))
Theorem	relogbcl 24311	Closure of the general logarithm with a positive real base on positive reals. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by Thierry Arnoux, 27-Sep-2017.)
⊢ ((𝐵 ∈ ℝ+ ∧ 𝑋 ∈ ℝ+ ∧ 𝐵 ≠ 1) → (𝐵 logb 𝑋) ∈ ℝ)
Theorem	relogbzcl 24312	Closure of the general logarithm with integer base on positive reals. (Contributed by Thierry Arnoux, 27-Sep-2017.) (Proof shortened by AV, 9-Jun-2020.)
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑋 ∈ ℝ+) → (𝐵 logb 𝑋) ∈ ℝ)
Theorem	relogbreexp 24313	Power law for the general logarithm for real powers: The logarithm of a positive real number to the power of a real number is equal to the product of the exponent and the logarithm of the base of the power. Property 4 of [Cohen4] p. 361. (Contributed by AV, 9-Jun-2020.)
⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ 𝐶 ∈ ℝ+ ∧ 𝐸 ∈ ℝ) → (𝐵 logb (𝐶↑𝑐𝐸)) = (𝐸 · (𝐵 logb 𝐶)))
Theorem	relogbzexp 24314	Power law for the general logarithm for integer powers: The logarithm of a positive real number to the power of an integer is equal to the product of the exponent and the logarithm of the base of the power. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by AV, 9-Jun-2020.)
⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ 𝐶 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → (𝐵 logb (𝐶↑𝑁)) = (𝑁 · (𝐵 logb 𝐶)))
Theorem	relogbmul 24315	The logarithm of the product of two positive real numbers is the sum of logarithms. Property 2 of [Cohen4] p. 361. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by AV, 29-May-2020.)
⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ (𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+)) → (𝐵 logb (𝐴 · 𝐶)) = ((𝐵 logb 𝐴) + (𝐵 logb 𝐶)))
Theorem	relogbmulexp 24316	The logarithm of the product of a positive real and a positive real number to the power of a real number is the sum of the logarithm of the first real number and the scaled logarithm of the second real number. (Contributed by AV, 29-May-2020.)
⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ (𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ∧ 𝐸 ∈ ℝ)) → (𝐵 logb (𝐴 · (𝐶↑𝑐𝐸))) = ((𝐵 logb 𝐴) + (𝐸 · (𝐵 logb 𝐶))))
Theorem	relogbdiv 24317	The logarithm of the quotient of two positive real numbers is the difference of logarithms. Property 3 of [Cohen4] p. 361. (Contributed by AV, 29-May-2020.)
⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ (𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+)) → (𝐵 logb (𝐴 / 𝐶)) = ((𝐵 logb 𝐴) − (𝐵 logb 𝐶)))
Theorem	relogbexp 24318	Identity law for general logarithm: the logarithm of a power to the base is the exponent. Property 6 of [Cohen4] p. 361. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by AV, 9-Jun-2020.)
⊢ ((𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ∧ 𝑀 ∈ ℤ) → (𝐵 logb (𝐵↑𝑀)) = 𝑀)
Theorem	nnlogbexp 24319	Identity law for general logarithm with integer base. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by Thierry Arnoux, 27-Sep-2017.)
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ) → (𝐵 logb (𝐵↑𝑀)) = 𝑀)
Theorem	logbrec 24320	Logarithm of a reciprocal changes sign. See logrec 24301. Particular case of Property 3 of [Cohen4] p. 361. (Contributed by Thierry Arnoux, 27-Sep-2017.)
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝐴 ∈ ℝ+) → (𝐵 logb (1 / 𝐴)) = -(𝐵 logb 𝐴))
Theorem	logbleb 24321	The general logarithm function is monotone/increasing. See logleb 24153. (Contributed by Stefan O'Rear, 19-Oct-2014.) (Revised by AV, 31-May-2020.)
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ+) → (𝑋 ≤ 𝑌 ↔ (𝐵 logb 𝑋) ≤ (𝐵 logb 𝑌)))
Theorem	logblt 24322	The general logarithm function is strictly monotone/increasing. Property 2 of [Cohen4] p. 377. See logltb 24150. (Contributed by Stefan O'Rear, 19-Oct-2014.) (Revised by Thierry Arnoux, 27-Sep-2017.)
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ+) → (𝑋 < 𝑌 ↔ (𝐵 logb 𝑋) < (𝐵 logb 𝑌)))
Theorem	relogbcxp 24323	Identity law for the general logarithm for real numbers. (Contributed by AV, 22-May-2020.)
⊢ ((𝐵 ∈ (ℝ+ ∖ {1}) ∧ 𝑋 ∈ ℝ) → (𝐵 logb (𝐵↑𝑐𝑋)) = 𝑋)
Theorem	cxplogb 24324	Identity law for the general logarithm. (Contributed by AV, 22-May-2020.)
⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ 𝑋 ∈ (ℂ ∖ {0})) → (𝐵↑𝑐(𝐵 logb 𝑋)) = 𝑋)
Theorem	relogbcxpb 24325	The logarithm is the inverse of the exponentiation. Observation in [Cohen4] p. 348. (Contributed by AV, 11-Jun-2020.)
⊢ (((𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ) → ((𝐵 logb 𝑋) = 𝑌 ↔ (𝐵↑𝑐𝑌) = 𝑋))
Theorem	logbmpt 24326*	The general logarithm to a fixed base regarded as mapping. (Contributed by AV, 11-Jun-2020.)
⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) → (curry logb ‘𝐵) = (𝑦 ∈ (ℂ ∖ {0}) ↦ ((log‘𝑦) / (log‘𝐵))))
Theorem	logbf 24327	The general logarithm to a fixed base regarded as function. (Contributed by AV, 11-Jun-2020.)
⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) → (curry logb ‘𝐵):(ℂ ∖ {0})⟶ℂ)
Theorem	logbfval 24328	The general logarithm of a complex number to a fixed base. (Contributed by AV, 11-Jun-2020.)
⊢ (((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) ∧ 𝑋 ∈ (ℂ ∖ {0})) → ((curry logb ‘𝐵)‘𝑋) = (𝐵 logb 𝑋))
Theorem	relogbf 24329	The general logarithm to a real base greater than 1 regarded as function restricted to the positive integers. Property in [Cohen4] p. 349. (Contributed by AV, 12-Jun-2020.)
⊢ ((𝐵 ∈ ℝ+ ∧ 1 < 𝐵) → ((curry logb ‘𝐵) ↾ ℝ+):ℝ+⟶ℝ)
Theorem	logblog 24330	The general logarithm to the base being Euler's constant regarded as function is the natural logarithm. (Contributed by AV, 12-Jun-2020.)
⊢ (curry logb ‘e) = log
14.3.6  Theorems of Pythagoras, isosceles triangles, and intersecting chords
Theorem	angval 24331*	Define the angle function, which takes two complex numbers, treated as vectors from the origin, and returns the angle between them, in the range ( − π, π]. To convert from the geometry notation, 𝑚𝐴𝐵𝐶, the measure of the angle with legs 𝐴𝐵, 𝐶𝐵 where 𝐶 is more counterclockwise for positive angles, is represented by ((𝐶 − 𝐵)𝐹(𝐴 − 𝐵)). (Contributed by Mario Carneiro, 23-Sep-2014.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    ⇒   ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → (𝐴𝐹𝐵) = (ℑ‘(log‘(𝐵 / 𝐴))))
Theorem	angcan 24332*	Cancel a constant multiplier in the angle function. (Contributed by Mario Carneiro, 23-Sep-2014.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    ⇒   ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐶 · 𝐴)𝐹(𝐶 · 𝐵)) = (𝐴𝐹𝐵))
Theorem	angneg 24333*	Cancel a negative sign in the angle function. (Contributed by Mario Carneiro, 23-Sep-2014.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    ⇒   ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → (-𝐴𝐹-𝐵) = (𝐴𝐹𝐵))
Theorem	angvald 24334*	The (signed) angle between two vectors is the argument of their quotient. Deduction form of angval 24331. (Contributed by David Moews, 28-Feb-2017.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ≠ 0)    &   ⊢ (𝜑 → 𝑌 ∈ ℂ)    &   ⊢ (𝜑 → 𝑌 ≠ 0)    ⇒   ⊢ (𝜑 → (𝑋𝐹𝑌) = (ℑ‘(log‘(𝑌 / 𝑋))))
Theorem	angcld 24335*	The (signed) angle between two vectors is in (-π(,]π). Deduction form. (Contributed by David Moews, 28-Feb-2017.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ≠ 0)    &   ⊢ (𝜑 → 𝑌 ∈ ℂ)    &   ⊢ (𝜑 → 𝑌 ≠ 0)    ⇒   ⊢ (𝜑 → (𝑋𝐹𝑌) ∈ (-π(,]π))
Theorem	angrteqvd 24336*	Two vectors are at a right angle iff their quotient is purely imaginary. (Contributed by David Moews, 28-Feb-2017.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ≠ 0)    &   ⊢ (𝜑 → 𝑌 ∈ ℂ)    &   ⊢ (𝜑 → 𝑌 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝑋𝐹𝑌) ∈ {(π / 2), -(π / 2)} ↔ (ℜ‘(𝑌 / 𝑋)) = 0))
Theorem	cosangneg2d 24337*	The cosine of the angle between 𝑋 and -𝑌 is the negative of that between 𝑋 and 𝑌. If A, B and C are collinear points, this implies that the cosines of DBA and DBC sum to zero, i.e., that DBA and DBC are supplementary. (Contributed by David Moews, 28-Feb-2017.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ≠ 0)    &   ⊢ (𝜑 → 𝑌 ∈ ℂ)    &   ⊢ (𝜑 → 𝑌 ≠ 0)    ⇒   ⊢ (𝜑 → (cos‘(𝑋𝐹-𝑌)) = -(cos‘(𝑋𝐹𝑌)))
Theorem	angrtmuld 24338*	Perpendicularity of two vectors does not change under rescaling the second. (Contributed by David Moews, 28-Feb-2017.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑌 ∈ ℂ)    &   ⊢ (𝜑 → 𝑍 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ≠ 0)    &   ⊢ (𝜑 → 𝑌 ≠ 0)    &   ⊢ (𝜑 → 𝑍 ≠ 0)    &   ⊢ (𝜑 → (𝑍 / 𝑌) ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝑋𝐹𝑌) ∈ {(π / 2), -(π / 2)} ↔ (𝑋𝐹𝑍) ∈ {(π / 2), -(π / 2)}))
Theorem	ang180lem1 24339*	Lemma for ang180 24344. Show that the "revolution number" 𝑁 is an integer, using efeq1 24079 to show that since the product of the three arguments 𝐴, 1 / (1 − 𝐴), (𝐴 − 1) / 𝐴 is -1, the sum of the logarithms must be an integer multiple of 2πi away from πi = log(-1). (Contributed by Mario Carneiro, 23-Sep-2014.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    &   ⊢ 𝑇 = (((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴))    &   ⊢ 𝑁 = (((𝑇 / i) / (2 · π)) − (1 / 2))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (𝑁 ∈ ℤ ∧ (𝑇 / i) ∈ ℝ))
Theorem	ang180lem2 24340*	Lemma for ang180 24344. Show that the revolution number 𝑁 is strictly between -2 and 1. Both bounds are established by iterating using the bounds on the imaginary part of the logarithm, logimcl 24120, but the resulting bound gives only 𝑁 ≤ 1 for the upper bound. The case 𝑁 = 1 is not ruled out here, but it is in some sense an "edge case" that can only happen under very specific conditions; in particular we show that all the angle arguments 𝐴, 1 / (1 − 𝐴), (𝐴 − 1) / 𝐴 must lie on the negative real axis, which is a contradiction because clearly if 𝐴 is negative then the other two are positive real. (Contributed by Mario Carneiro, 23-Sep-2014.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    &   ⊢ 𝑇 = (((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴))    &   ⊢ 𝑁 = (((𝑇 / i) / (2 · π)) − (1 / 2))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → (-2 < 𝑁 ∧ 𝑁 < 1))
Theorem	ang180lem3 24341*	Lemma for ang180 24344. Since ang180lem1 24339 shows that 𝑁 is an integer and ang180lem2 24340 shows that 𝑁 is strictly between -2 and 1, it follows that 𝑁 ∈ {-1, 0}, and these two cases correspond to the two possible values for 𝑇. (Contributed by Mario Carneiro, 23-Sep-2014.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    &   ⊢ 𝑇 = (((log‘(1 / (1 − 𝐴))) + (log‘((𝐴 − 1) / 𝐴))) + (log‘𝐴))    &   ⊢ 𝑁 = (((𝑇 / i) / (2 · π)) − (1 / 2))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → 𝑇 ∈ {-(i · π), (i · π)})
Theorem	ang180lem4 24342*	Lemma for ang180 24344. Reduce the statement to one variable. (Contributed by Mario Carneiro, 23-Sep-2014.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((((1 − 𝐴)𝐹1) + (𝐴𝐹(𝐴 − 1))) + (1𝐹𝐴)) ∈ {-π, π})
Theorem	ang180lem5 24343*	Lemma for ang180 24344: Reduce the statement to two variables. (Contributed by Mario Carneiro, 23-Sep-2014.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    ⇒   ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ 𝐴 ≠ 𝐵) → ((((𝐴 − 𝐵)𝐹𝐴) + (𝐵𝐹(𝐵 − 𝐴))) + (𝐴𝐹𝐵)) ∈ {-π, π})
Theorem	ang180 24344*	The sum of angles 𝑚𝐴𝐵𝐶 + 𝑚𝐵𝐶𝐴 + 𝑚𝐶𝐴𝐵 in a triangle adds up to either π or -π, i.e. 180 degrees. (The sign is due to the two possible orientations of vertex arrangement and our signed notion of angle). This is Metamath 100 proof #27. (Contributed by Mario Carneiro, 23-Sep-2014.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    ⇒   ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐶)) → ((((𝐶 − 𝐵)𝐹(𝐴 − 𝐵)) + ((𝐴 − 𝐶)𝐹(𝐵 − 𝐶))) + ((𝐵 − 𝐴)𝐹(𝐶 − 𝐴))) ∈ {-π, π})
Theorem	lawcoslem1 24345	Lemma for lawcos 24346. Here we prove the law for a point at the origin and two distinct points U and V, using an expanded version of the signed angle expression on the complex plane. (Contributed by David A. Wheeler, 11-Jun-2015.)
⊢ (𝜑 → 𝑈 ∈ ℂ)    &   ⊢ (𝜑 → 𝑉 ∈ ℂ)    &   ⊢ (𝜑 → 𝑈 ≠ 0)    &   ⊢ (𝜑 → 𝑉 ≠ 0)    ⇒   ⊢ (𝜑 → ((abs‘(𝑈 − 𝑉))↑2) = ((((abs‘𝑈)↑2) + ((abs‘𝑉)↑2)) − (2 · (((abs‘𝑈) · (abs‘𝑉)) · ((ℜ‘(𝑈 / 𝑉)) / (abs‘(𝑈 / 𝑉)))))))
Theorem	lawcos 24346*	Law of cosines (also known as the Al-Kashi theorem or the generalized Pythagorean theorem, or the cosine formula or cosine rule). Given three distinct points A, B, and C, prove a relationship between their segment lengths. This theorem is expressed using the complex number plane as a plane, where 𝐹 is the signed angle construct (as used in ang180 24344), 𝑋 is the distance of line segment BC, 𝑌 is the distance of line segment AC, 𝑍 is the distance of line segment AB, and 𝑂 is the signed angle m/_ BCA on the complex plane. We translate triangle ABC to move C to the origin (C-C), B to U=(B-C), and A to V=(A-C), then use lemma lawcoslem1 24345 to prove this algebraically simpler case. The metamath convention is to use a signed angle; in this case the sign doesn't matter because we use the cosine of the angle (see cosneg 14716). The Pythagorean theorem pythag 24347 is a special case of the law of cosines. The theorem's expression and approach were suggested by Mario Carneiro. This is Metamath 100 proof #94. (Contributed by David A. Wheeler, 12-Jun-2015.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    &   ⊢ 𝑋 = (abs‘(𝐵 − 𝐶))    &   ⊢ 𝑌 = (abs‘(𝐴 − 𝐶))    &   ⊢ 𝑍 = (abs‘(𝐴 − 𝐵))    &   ⊢ 𝑂 = ((𝐵 − 𝐶)𝐹(𝐴 − 𝐶))    ⇒   ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (𝑍↑2) = (((𝑋↑2) + (𝑌↑2)) − (2 · ((𝑋 · 𝑌) · (cos‘𝑂)))))
Theorem	pythag 24347*	Pythagorean theorem. Given three distinct points A, B, and C that form a right triangle (with the right angle at C), prove a relationship between their segment lengths. This theorem is expressed using the complex number plane as a plane, where 𝐹 is the signed angle construct (as used in ang180 24344), 𝑋 is the distance of line segment BC, 𝑌 is the distance of line segment AC, 𝑍 is the distance of line segment AB (the hypotenuse), and 𝑂 is the signed right angle m/_ BCA. We use the law of cosines lawcos 24346 to prove this, along with simple trigonometry facts like coshalfpi 24025 and cosneg 14716. (Contributed by David A. Wheeler, 13-Jun-2015.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    &   ⊢ 𝑋 = (abs‘(𝐵 − 𝐶))    &   ⊢ 𝑌 = (abs‘(𝐴 − 𝐶))    &   ⊢ 𝑍 = (abs‘(𝐴 − 𝐵))    &   ⊢ 𝑂 = ((𝐵 − 𝐶)𝐹(𝐴 − 𝐶))    ⇒   ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑂 ∈ {(π / 2), -(π / 2)}) → (𝑍↑2) = ((𝑋↑2) + (𝑌↑2)))
Theorem	isosctrlem1 24348	Lemma for isosctr 24351. (Contributed by Saveliy Skresanov, 30-Dec-2016.)
⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (ℑ‘(log‘(1 − 𝐴))) ≠ π)
Theorem	isosctrlem2 24349	Lemma for isosctr 24351. Corresponds to the case where one vertex is at 0, another at 1 and the third lies on the unit circle. (Contributed by Saveliy Skresanov, 31-Dec-2016.)
⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (ℑ‘(log‘(1 − 𝐴))) = (ℑ‘(log‘(-𝐴 / (1 − 𝐴)))))
Theorem	isosctrlem3 24350*	Lemma for isosctr 24351. Corresponds to the case where one vertex is at 0. (Contributed by Saveliy Skresanov, 1-Jan-2017.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    ⇒   ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ∧ 𝐴 ≠ 𝐵) ∧ (abs‘𝐴) = (abs‘𝐵)) → (-𝐴𝐹(𝐵 − 𝐴)) = ((𝐴 − 𝐵)𝐹-𝐵))
Theorem	isosctr 24351*	Isosceles triangle theorem. This is Metamath 100 proof #65. (Contributed by Saveliy Skresanov, 1-Jan-2017.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    ⇒   ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵) ∧ (abs‘(𝐴 − 𝐶)) = (abs‘(𝐵 − 𝐶))) → ((𝐶 − 𝐴)𝐹(𝐵 − 𝐴)) = ((𝐴 − 𝐵)𝐹(𝐶 − 𝐵)))
Theorem	ssscongptld 24352*	If two triangles have equal sides, one angle in one triangle has the same cosine as the corresponding angle in the other triangle. This is a partial form of the SSS congruence theorem. This theorem is proven by using lawcos 24346 on both triangles to express one side in terms of the other two, and then equating these expressions and reducing this algebraically to get an equality of cosines of angles. (Contributed by David Moews, 28-Feb-2017.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝐸 ∈ ℂ)    &   ⊢ (𝜑 → 𝐺 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐷 ≠ 𝐸)    &   ⊢ (𝜑 → 𝐸 ≠ 𝐺)    &   ⊢ (𝜑 → (abs‘(𝐴 − 𝐵)) = (abs‘(𝐷 − 𝐸)))    &   ⊢ (𝜑 → (abs‘(𝐵 − 𝐶)) = (abs‘(𝐸 − 𝐺)))    &   ⊢ (𝜑 → (abs‘(𝐶 − 𝐴)) = (abs‘(𝐺 − 𝐷)))    ⇒   ⊢ (𝜑 → (cos‘((𝐴 − 𝐵)𝐹(𝐶 − 𝐵))) = (cos‘((𝐷 − 𝐸)𝐹(𝐺 − 𝐸))))
Theorem	affineequiv 24353	Equivalence between two ways of expressing 𝐵 as an affine combination of 𝐴 and 𝐶. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐵 = ((𝐷 · 𝐴) + ((1 − 𝐷) · 𝐶)) ↔ (𝐶 − 𝐵) = (𝐷 · (𝐶 − 𝐴))))
Theorem	affineequiv2 24354	Equivalence between two ways of expressing 𝐵 as an affine combination of 𝐴 and 𝐶. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐵 = ((𝐷 · 𝐴) + ((1 − 𝐷) · 𝐶)) ↔ (𝐵 − 𝐴) = ((1 − 𝐷) · (𝐶 − 𝐴))))
Theorem	angpieqvdlem 24355	Equivalence used in the proof of angpieqvd 24358. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐶)    ⇒   ⊢ (𝜑 → (-((𝐶 − 𝐵) / (𝐴 − 𝐵)) ∈ ℝ+ ↔ ((𝐶 − 𝐵) / (𝐶 − 𝐴)) ∈ (0(,)1)))
Theorem	angpieqvdlem2 24356*	Equivalence used in angpieqvd 24358. (Contributed by David Moews, 28-Feb-2017.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    ⇒   ⊢ (𝜑 → (-((𝐶 − 𝐵) / (𝐴 − 𝐵)) ∈ ℝ+ ↔ ((𝐴 − 𝐵)𝐹(𝐶 − 𝐵)) = π))
Theorem	angpined 24357*	If the angle at ABC is π, then A is not equal to C. (Contributed by David Moews, 28-Feb-2017.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    ⇒   ⊢ (𝜑 → (((𝐴 − 𝐵)𝐹(𝐶 − 𝐵)) = π → 𝐴 ≠ 𝐶))
Theorem	angpieqvd 24358*	The angle ABC is π iff B is a nontrivial convex combination of A and C, i.e., iff B is in the interior of the segment AC. (Contributed by David Moews, 28-Feb-2017.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    ⇒   ⊢ (𝜑 → (((𝐴 − 𝐵)𝐹(𝐶 − 𝐵)) = π ↔ ∃𝑤 ∈ (0(,)1)𝐵 = ((𝑤 · 𝐴) + ((1 − 𝑤) · 𝐶))))
Theorem	chordthmlem 24359*	If M is the midpoint of AB and AQ = BQ, then QMB is a right angle. The proof uses ssscongptld 24352 to observe that, since AMQ and BMQ have equal sides, the angles QMB and QMA must be equal. Since they are supplementary, both must be right. (Contributed by David Moews, 28-Feb-2017.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝑄 ∈ ℂ)    &   ⊢ (𝜑 → 𝑀 = ((𝐴 + 𝐵) / 2))    &   ⊢ (𝜑 → (abs‘(𝐴 − 𝑄)) = (abs‘(𝐵 − 𝑄)))    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝑄 ≠ 𝑀)    ⇒   ⊢ (𝜑 → ((𝑄 − 𝑀)𝐹(𝐵 − 𝑀)) ∈ {(π / 2), -(π / 2)})
Theorem	chordthmlem2 24360*	If M is the midpoint of AB, AQ = BQ, and P is on the line AB, then QMP is a right angle. This is proven by reduction to the special case chordthmlem 24359, where P = B, and using angrtmuld 24338 to observe that QMP is right iff QMB is. (Contributed by David Moews, 28-Feb-2017.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝑄 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 = ((𝐴 + 𝐵) / 2))    &   ⊢ (𝜑 → 𝑃 = ((𝑋 · 𝐴) + ((1 − 𝑋) · 𝐵)))    &   ⊢ (𝜑 → (abs‘(𝐴 − 𝑄)) = (abs‘(𝐵 − 𝑄)))    &   ⊢ (𝜑 → 𝑃 ≠ 𝑀)    &   ⊢ (𝜑 → 𝑄 ≠ 𝑀)    ⇒   ⊢ (𝜑 → ((𝑄 − 𝑀)𝐹(𝑃 − 𝑀)) ∈ {(π / 2), -(π / 2)})
Theorem	chordthmlem3 24361	If M is the midpoint of AB, AQ = BQ, and P is on the line AB, then PQ 2 = QM 2 + PM 2 . This follows from chordthmlem2 24360 and the Pythagorean theorem (pythag 24347) in the case where P and Q are unequal to M. If either P or Q equals M, the result is trivial. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝑄 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 = ((𝐴 + 𝐵) / 2))    &   ⊢ (𝜑 → 𝑃 = ((𝑋 · 𝐴) + ((1 − 𝑋) · 𝐵)))    &   ⊢ (𝜑 → (abs‘(𝐴 − 𝑄)) = (abs‘(𝐵 − 𝑄)))    ⇒   ⊢ (𝜑 → ((abs‘(𝑃 − 𝑄))↑2) = (((abs‘(𝑄 − 𝑀))↑2) + ((abs‘(𝑃 − 𝑀))↑2)))
Theorem	chordthmlem4 24362	If P is on the segment AB and M is the midpoint of AB, then PA · PB = BM 2 − PM 2 . If all lengths are reexpressed as fractions of AB, this reduces to the identity 𝑋 · (1 − 𝑋) = (1 / 2) 2 − ((1 / 2) − 𝑋) 2 . (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ (0[,]1))    &   ⊢ (𝜑 → 𝑀 = ((𝐴 + 𝐵) / 2))    &   ⊢ (𝜑 → 𝑃 = ((𝑋 · 𝐴) + ((1 − 𝑋) · 𝐵)))    ⇒   ⊢ (𝜑 → ((abs‘(𝑃 − 𝐴)) · (abs‘(𝑃 − 𝐵))) = (((abs‘(𝐵 − 𝑀))↑2) − ((abs‘(𝑃 − 𝑀))↑2)))
Theorem	chordthmlem5 24363	If P is on the segment AB and AQ = BQ, then PA · PB = BQ 2 − PQ 2 . This follows from two uses of chordthmlem3 24361 to show that PQ 2 = QM 2 + PM 2 and BQ 2 = QM 2 + BM 2 , so BQ 2 − PQ 2 = (QM 2 + BM 2 ) − (QM 2 + PM 2 ) = BM 2 − PM 2 , which equals PA · PB by chordthmlem4 24362. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝑄 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ (0[,]1))    &   ⊢ (𝜑 → 𝑃 = ((𝑋 · 𝐴) + ((1 − 𝑋) · 𝐵)))    &   ⊢ (𝜑 → (abs‘(𝐴 − 𝑄)) = (abs‘(𝐵 − 𝑄)))    ⇒   ⊢ (𝜑 → ((abs‘(𝑃 − 𝐴)) · (abs‘(𝑃 − 𝐵))) = (((abs‘(𝐵 − 𝑄))↑2) − ((abs‘(𝑃 − 𝑄))↑2)))
Theorem	chordthm 24364*	The intersecting chords theorem. If points A, B, C, and D lie on a circle (with center Q, say), and the point P is on the interior of the segments AB and CD, then the two products of lengths PA · PB and PC · PD are equal. The Euclidean plane is identified with the complex plane, and the fact that P is on AB and on CD is expressed by the hypothesis that the angles APB and CPD are equal to π. The result is proven by using chordthmlem5 24363 twice to show that PA · PB and PC · PD both equal BQ 2 − PQ 2 . This is similar to the proof of the theorem given in Euclid's Elements, where it is Proposition III.35. This is Metamath 100 proof #55. (Contributed by David Moews, 28-Feb-2017.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝑃 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 𝑃)    &   ⊢ (𝜑 → 𝐵 ≠ 𝑃)    &   ⊢ (𝜑 → 𝐶 ≠ 𝑃)    &   ⊢ (𝜑 → 𝐷 ≠ 𝑃)    &   ⊢ (𝜑 → ((𝐴 − 𝑃)𝐹(𝐵 − 𝑃)) = π)    &   ⊢ (𝜑 → ((𝐶 − 𝑃)𝐹(𝐷 − 𝑃)) = π)    &   ⊢ (𝜑 → 𝑄 ∈ ℂ)    &   ⊢ (𝜑 → (abs‘(𝐴 − 𝑄)) = (abs‘(𝐵 − 𝑄)))    &   ⊢ (𝜑 → (abs‘(𝐴 − 𝑄)) = (abs‘(𝐶 − 𝑄)))    &   ⊢ (𝜑 → (abs‘(𝐴 − 𝑄)) = (abs‘(𝐷 − 𝑄)))    ⇒   ⊢ (𝜑 → ((abs‘(𝑃 − 𝐴)) · (abs‘(𝑃 − 𝐵))) = ((abs‘(𝑃 − 𝐶)) · (abs‘(𝑃 − 𝐷))))
Theorem	heron 24365*	Heron's formula gives the area of a triangle given only the side lengths. If points A, B, C form a triangle, then the area of the triangle, represented here as (1 / 2) · 𝑋 · 𝑌 · abs(sin𝑂), is equal to the square root of 𝑆 · (𝑆 − 𝑋) · (𝑆 − 𝑌) · (𝑆 − 𝑍), where 𝑆 = (𝑋 + 𝑌 + 𝑍) / 2 is half the perimeter of the triangle. Based on work by Jon Pennant. This is Metamath 100 proof #57. (Contributed by Mario Carneiro, 10-Mar-2019.)
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    &   ⊢ 𝑋 = (abs‘(𝐵 − 𝐶))    &   ⊢ 𝑌 = (abs‘(𝐴 − 𝐶))    &   ⊢ 𝑍 = (abs‘(𝐴 − 𝐵))    &   ⊢ 𝑂 = ((𝐵 − 𝐶)𝐹(𝐴 − 𝐶))    &   ⊢ 𝑆 = (((𝑋 + 𝑌) + 𝑍) / 2)    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    ⇒   ⊢ (𝜑 → (((1 / 2) · (𝑋 · 𝑌)) · (abs‘(sin‘𝑂))) = (√‘((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍)))))
14.3.7  Solutions of quadratic, cubic, and quartic equations
Theorem	quad2 24366	The quadratic equation, without specifying the particular branch 𝐷 to the square root. (Contributed by Mario Carneiro, 23-Apr-2015.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → (𝐷↑2) = ((𝐵↑2) − (4 · (𝐴 · 𝐶))))    ⇒   ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0 ↔ (𝑋 = ((-𝐵 + 𝐷) / (2 · 𝐴)) ∨ 𝑋 = ((-𝐵 − 𝐷) / (2 · 𝐴)))))
Theorem	quad 24367	The quadratic equation. (Contributed by Mario Carneiro, 23-Apr-2015.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 = ((𝐵↑2) − (4 · (𝐴 · 𝐶))))    ⇒   ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0 ↔ (𝑋 = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∨ 𝑋 = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴)))))
Theorem	1cubrlem 24368	The cube roots of unity. (Contributed by Mario Carneiro, 23-Apr-2015.)
⊢ ((-1↑𝑐(2 / 3)) = ((-1 + (i · (√‘3))) / 2) ∧ ((-1↑𝑐(2 / 3))↑2) = ((-1 − (i · (√‘3))) / 2))
Theorem	1cubr 24369	The cube roots of unity. (Contributed by Mario Carneiro, 23-Apr-2015.)
⊢ 𝑅 = {1, ((-1 + (i · (√‘3))) / 2), ((-1 − (i · (√‘3))) / 2)}    ⇒   ⊢ (𝐴 ∈ 𝑅 ↔ (𝐴 ∈ ℂ ∧ (𝐴↑3) = 1))
Theorem	dcubic1lem 24370	Lemma for dcubic1 24372 and dcubic2 24371: simplify the cubic equation under the substitution 𝑋 = 𝑈 − 𝑀 / 𝑈. (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ (𝜑 → 𝑃 ∈ ℂ)    &   ⊢ (𝜑 → 𝑄 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑇 ∈ ℂ)    &   ⊢ (𝜑 → (𝑇↑3) = (𝐺 − 𝑁))    &   ⊢ (𝜑 → 𝐺 ∈ ℂ)    &   ⊢ (𝜑 → (𝐺↑2) = ((𝑁↑2) + (𝑀↑3)))    &   ⊢ (𝜑 → 𝑀 = (𝑃 / 3))    &   ⊢ (𝜑 → 𝑁 = (𝑄 / 2))    &   ⊢ (𝜑 → 𝑇 ≠ 0)    &   ⊢ (𝜑 → 𝑈 ∈ ℂ)    &   ⊢ (𝜑 → 𝑈 ≠ 0)    &   ⊢ (𝜑 → 𝑋 = (𝑈 − (𝑀 / 𝑈)))    ⇒   ⊢ (𝜑 → (((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0 ↔ (((𝑈↑3)↑2) + ((𝑄 · (𝑈↑3)) − (𝑀↑3))) = 0))
Theorem	dcubic2 24371*	Reverse direction of dcubic 24373. Given a solution 𝑈 to the "substitution" quadratic equation 𝑋 = 𝑈 − 𝑀 / 𝑈, show that 𝑋 is in the desired form. (Contributed by Mario Carneiro, 25-Apr-2015.)
⊢ (𝜑 → 𝑃 ∈ ℂ)    &   ⊢ (𝜑 → 𝑄 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑇 ∈ ℂ)    &   ⊢ (𝜑 → (𝑇↑3) = (𝐺 − 𝑁))    &   ⊢ (𝜑 → 𝐺 ∈ ℂ)    &   ⊢ (𝜑 → (𝐺↑2) = ((𝑁↑2) + (𝑀↑3)))    &   ⊢ (𝜑 → 𝑀 = (𝑃 / 3))    &   ⊢ (𝜑 → 𝑁 = (𝑄 / 2))    &   ⊢ (𝜑 → 𝑇 ≠ 0)    &   ⊢ (𝜑 → 𝑈 ∈ ℂ)    &   ⊢ (𝜑 → 𝑈 ≠ 0)    &   ⊢ (𝜑 → 𝑋 = (𝑈 − (𝑀 / 𝑈)))    &   ⊢ (𝜑 → ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0)    ⇒   ⊢ (𝜑 → ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇)))))
Theorem	dcubic1 24372	Forward direction of dcubic 24373: the claimed formula produces solutions to the cubic equation. (Contributed by Mario Carneiro, 25-Apr-2015.)
⊢ (𝜑 → 𝑃 ∈ ℂ)    &   ⊢ (𝜑 → 𝑄 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑇 ∈ ℂ)    &   ⊢ (𝜑 → (𝑇↑3) = (𝐺 − 𝑁))    &   ⊢ (𝜑 → 𝐺 ∈ ℂ)    &   ⊢ (𝜑 → (𝐺↑2) = ((𝑁↑2) + (𝑀↑3)))    &   ⊢ (𝜑 → 𝑀 = (𝑃 / 3))    &   ⊢ (𝜑 → 𝑁 = (𝑄 / 2))    &   ⊢ (𝜑 → 𝑇 ≠ 0)    &   ⊢ (𝜑 → 𝑋 = (𝑇 − (𝑀 / 𝑇)))    ⇒   ⊢ (𝜑 → ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0)
Theorem	dcubic 24373*	Solutions to the depressed cubic, a special case of cubic 24376. (The definitions of 𝑀, 𝑁, 𝐺, 𝑇 here differ from mcubic 24374 by scale factors of -9, 54, 54 and -27 respectively, to simplify the algebra and presentation.) (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ (𝜑 → 𝑃 ∈ ℂ)    &   ⊢ (𝜑 → 𝑄 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑇 ∈ ℂ)    &   ⊢ (𝜑 → (𝑇↑3) = (𝐺 − 𝑁))    &   ⊢ (𝜑 → 𝐺 ∈ ℂ)    &   ⊢ (𝜑 → (𝐺↑2) = ((𝑁↑2) + (𝑀↑3)))    &   ⊢ (𝜑 → 𝑀 = (𝑃 / 3))    &   ⊢ (𝜑 → 𝑁 = (𝑄 / 2))    &   ⊢ (𝜑 → 𝑇 ≠ 0)    ⇒   ⊢ (𝜑 → (((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0 ↔ ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))))
Theorem	mcubic 24374*	Solutions to a monic cubic equation, a special case of cubic 24376. (Contributed by Mario Carneiro, 24-Apr-2015.)
⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑇 ∈ ℂ)    &   ⊢ (𝜑 → (𝑇↑3) = ((𝑁 + 𝐺) / 2))    &   ⊢ (𝜑 → 𝐺 ∈ ℂ)    &   ⊢ (𝜑 → (𝐺↑2) = ((𝑁↑2) − (4 · (𝑀↑3))))    &   ⊢ (𝜑 → 𝑀 = ((𝐵↑2) − (3 · 𝐶)))    &   ⊢ (𝜑 → 𝑁 = (((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) + (;27 · 𝐷)))    &   ⊢ (𝜑 → 𝑇 ≠ 0)    ⇒   ⊢ (𝜑 → ((((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)) = 0 ↔ ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3))))
Theorem	cubic2 24375*	The solution to the general cubic equation, for arbitrary choices 𝐺 and 𝑇 of the square and cube roots. (Contributed by Mario Carneiro, 23-Apr-2015.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑇 ∈ ℂ)    &   ⊢ (𝜑 → (𝑇↑3) = ((𝑁 + 𝐺) / 2))    &   ⊢ (𝜑 → 𝐺 ∈ ℂ)    &   ⊢ (𝜑 → (𝐺↑2) = ((𝑁↑2) − (4 · (𝑀↑3))))    &   ⊢ (𝜑 → 𝑀 = ((𝐵↑2) − (3 · (𝐴 · 𝐶))))    &   ⊢ (𝜑 → 𝑁 = (((2 · (𝐵↑3)) − ((9 · 𝐴) · (𝐵 · 𝐶))) + (;27 · ((𝐴↑2) · 𝐷))))    &   ⊢ (𝜑 → 𝑇 ≠ 0)    ⇒   ⊢ (𝜑 → ((((𝐴 · (𝑋↑3)) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)) = 0 ↔ ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / (3 · 𝐴)))))
Theorem	cubic 24376*	The cubic equation, which gives the roots of an arbitrary (nondegenerate) cubic function. Use rextp 4188 to convert the existential quantifier to a triple disjunction. This is Metamath 100 proof #37. (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ 𝑅 = {1, ((-1 + (i · (√‘3))) / 2), ((-1 − (i · (√‘3))) / 2)}    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑇 = (((𝑁 + (√‘𝐺)) / 2)↑𝑐(1 / 3)))    &   ⊢ (𝜑 → 𝐺 = ((𝑁↑2) − (4 · (𝑀↑3))))    &   ⊢ (𝜑 → 𝑀 = ((𝐵↑2) − (3 · (𝐴 · 𝐶))))    &   ⊢ (𝜑 → 𝑁 = (((2 · (𝐵↑3)) − ((9 · 𝐴) · (𝐵 · 𝐶))) + (;27 · ((𝐴↑2) · 𝐷))))    &   ⊢ (𝜑 → 𝑀 ≠ 0)    ⇒   ⊢ (𝜑 → ((((𝐴 · (𝑋↑3)) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)) = 0 ↔ ∃𝑟 ∈ 𝑅 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / (3 · 𝐴))))
Theorem	binom4 24377	Work out a quartic binomial. (You would think that by this point it would be faster to use binom 14401, but it turns out to be just as much work to put it into this form after clearing all the sums and calculating binomial coefficients.) (Contributed by Mario Carneiro, 6-May-2015.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑4) = (((𝐴↑4) + (4 · ((𝐴↑3) · 𝐵))) + ((6 · ((𝐴↑2) · (𝐵↑2))) + ((4 · (𝐴 · (𝐵↑3))) + (𝐵↑4)))))
Theorem	dquartlem1 24378	Lemma for dquart 24380. (Contributed by Mario Carneiro, 6-May-2015.)
⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑆 ∈ ℂ)    &   ⊢ (𝜑 → 𝑀 = ((2 · 𝑆)↑2))    &   ⊢ (𝜑 → 𝑀 ≠ 0)    &   ⊢ (𝜑 → 𝐼 ∈ ℂ)    &   ⊢ (𝜑 → (𝐼↑2) = ((-(𝑆↑2) − (𝐵 / 2)) + ((𝐶 / 4) / 𝑆)))    ⇒   ⊢ (𝜑 → ((((𝑋↑2) + ((𝑀 + 𝐵) / 2)) + ((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / 𝑆)) = 0 ↔ (𝑋 = (-𝑆 + 𝐼) ∨ 𝑋 = (-𝑆 − 𝐼))))
Theorem	dquartlem2 24379	Lemma for dquart 24380. (Contributed by Mario Carneiro, 6-May-2015.)
⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑆 ∈ ℂ)    &   ⊢ (𝜑 → 𝑀 = ((2 · 𝑆)↑2))    &   ⊢ (𝜑 → 𝑀 ≠ 0)    &   ⊢ (𝜑 → 𝐼 ∈ ℂ)    &   ⊢ (𝜑 → (𝐼↑2) = ((-(𝑆↑2) − (𝐵 / 2)) + ((𝐶 / 4) / 𝑆)))    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → (((𝑀↑3) + ((2 · 𝐵) · (𝑀↑2))) + ((((𝐵↑2) − (4 · 𝐷)) · 𝑀) + -(𝐶↑2))) = 0)    ⇒   ⊢ (𝜑 → ((((𝑀 + 𝐵) / 2)↑2) − (((𝐶↑2) / 4) / 𝑀)) = 𝐷)
Theorem	dquart 24380	Solve a depressed quartic equation. To eliminate 𝑆, which is the square root of a solution 𝑀 to the resolvent cubic equation, apply cubic 24376 or one of its variants. (Contributed by Mario Carneiro, 6-May-2015.)
⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑆 ∈ ℂ)    &   ⊢ (𝜑 → 𝑀 = ((2 · 𝑆)↑2))    &   ⊢ (𝜑 → 𝑀 ≠ 0)    &   ⊢ (𝜑 → 𝐼 ∈ ℂ)    &   ⊢ (𝜑 → (𝐼↑2) = ((-(𝑆↑2) − (𝐵 / 2)) + ((𝐶 / 4) / 𝑆)))    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → (((𝑀↑3) + ((2 · 𝐵) · (𝑀↑2))) + ((((𝐵↑2) − (4 · 𝐷)) · 𝑀) + -(𝐶↑2))) = 0)    &   ⊢ (𝜑 → 𝐽 ∈ ℂ)    &   ⊢ (𝜑 → (𝐽↑2) = ((-(𝑆↑2) − (𝐵 / 2)) − ((𝐶 / 4) / 𝑆)))    ⇒   ⊢ (𝜑 → ((((𝑋↑4) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)) = 0 ↔ ((𝑋 = (-𝑆 + 𝐼) ∨ 𝑋 = (-𝑆 − 𝐼)) ∨ (𝑋 = (𝑆 + 𝐽) ∨ 𝑋 = (𝑆 − 𝐽)))))
Theorem	quart1cl 24381	Closure lemmas for quart 24388. (Contributed by Mario Carneiro, 7-May-2015.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝑃 = (𝐵 − ((3 / 8) · (𝐴↑2))))    &   ⊢ (𝜑 → 𝑄 = ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)))    &   ⊢ (𝜑 → 𝑅 = ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))    ⇒   ⊢ (𝜑 → (𝑃 ∈ ℂ ∧ 𝑄 ∈ ℂ ∧ 𝑅 ∈ ℂ))
Theorem	quart1lem 24382	Lemma for quart1 24383. (Contributed by Mario Carneiro, 6-May-2015.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝑃 = (𝐵 − ((3 / 8) · (𝐴↑2))))    &   ⊢ (𝜑 → 𝑄 = ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)))    &   ⊢ (𝜑 → 𝑅 = ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑌 = (𝑋 + (𝐴 / 4)))    ⇒   ⊢ (𝜑 → 𝐷 = ((((𝐴↑4) / ;;256) + (𝑃 · ((𝐴 / 4)↑2))) + ((𝑄 · (𝐴 / 4)) + 𝑅)))
Theorem	quart1 24383	Depress a quartic equation. (Contributed by Mario Carneiro, 6-May-2015.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝑃 = (𝐵 − ((3 / 8) · (𝐴↑2))))    &   ⊢ (𝜑 → 𝑄 = ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)))    &   ⊢ (𝜑 → 𝑅 = ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝑌 = (𝑋 + (𝐴 / 4)))    ⇒   ⊢ (𝜑 → (((𝑋↑4) + (𝐴 · (𝑋↑3))) + ((𝐵 · (𝑋↑2)) + ((𝐶 · 𝑋) + 𝐷))) = (((𝑌↑4) + (𝑃 · (𝑌↑2))) + ((𝑄 · 𝑌) + 𝑅)))
Theorem	quartlem1 24384	Lemma for quart 24388. (Contributed by Mario Carneiro, 6-May-2015.)
⊢ (𝜑 → 𝑃 ∈ ℂ)    &   ⊢ (𝜑 → 𝑄 ∈ ℂ)    &   ⊢ (𝜑 → 𝑅 ∈ ℂ)    &   ⊢ (𝜑 → 𝑈 = ((𝑃↑2) + (;12 · 𝑅)))    &   ⊢ (𝜑 → 𝑉 = ((-(2 · (𝑃↑3)) − (;27 · (𝑄↑2))) + (;72 · (𝑃 · 𝑅))))    ⇒   ⊢ (𝜑 → (𝑈 = (((2 · 𝑃)↑2) − (3 · ((𝑃↑2) − (4 · 𝑅)))) ∧ 𝑉 = (((2 · ((2 · 𝑃)↑3)) − (9 · ((2 · 𝑃) · ((𝑃↑2) − (4 · 𝑅))))) + (;27 · -(𝑄↑2)))))
Theorem	quartlem2 24385	Closure lemmas for quart 24388. (Contributed by Mario Carneiro, 7-May-2015.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝐸 = -(𝐴 / 4))    &   ⊢ (𝜑 → 𝑃 = (𝐵 − ((3 / 8) · (𝐴↑2))))    &   ⊢ (𝜑 → 𝑄 = ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)))    &   ⊢ (𝜑 → 𝑅 = ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))    &   ⊢ (𝜑 → 𝑈 = ((𝑃↑2) + (;12 · 𝑅)))    &   ⊢ (𝜑 → 𝑉 = ((-(2 · (𝑃↑3)) − (;27 · (𝑄↑2))) + (;72 · (𝑃 · 𝑅))))    &   ⊢ (𝜑 → 𝑊 = (√‘((𝑉↑2) − (4 · (𝑈↑3)))))    ⇒   ⊢ (𝜑 → (𝑈 ∈ ℂ ∧ 𝑉 ∈ ℂ ∧ 𝑊 ∈ ℂ))
Theorem	quartlem3 24386	Closure lemmas for quart 24388. (Contributed by Mario Carneiro, 7-May-2015.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝐸 = -(𝐴 / 4))    &   ⊢ (𝜑 → 𝑃 = (𝐵 − ((3 / 8) · (𝐴↑2))))    &   ⊢ (𝜑 → 𝑄 = ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)))    &   ⊢ (𝜑 → 𝑅 = ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))    &   ⊢ (𝜑 → 𝑈 = ((𝑃↑2) + (;12 · 𝑅)))    &   ⊢ (𝜑 → 𝑉 = ((-(2 · (𝑃↑3)) − (;27 · (𝑄↑2))) + (;72 · (𝑃 · 𝑅))))    &   ⊢ (𝜑 → 𝑊 = (√‘((𝑉↑2) − (4 · (𝑈↑3)))))    &   ⊢ (𝜑 → 𝑆 = ((√‘𝑀) / 2))    &   ⊢ (𝜑 → 𝑀 = -((((2 · 𝑃) + 𝑇) + (𝑈 / 𝑇)) / 3))    &   ⊢ (𝜑 → 𝑇 = (((𝑉 + 𝑊) / 2)↑𝑐(1 / 3)))    &   ⊢ (𝜑 → 𝑇 ≠ 0)    ⇒   ⊢ (𝜑 → (𝑆 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑇 ∈ ℂ))
Theorem	quartlem4 24387	Closure lemmas for quart 24388. (Contributed by Mario Carneiro, 7-May-2015.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝐸 = -(𝐴 / 4))    &   ⊢ (𝜑 → 𝑃 = (𝐵 − ((3 / 8) · (𝐴↑2))))    &   ⊢ (𝜑 → 𝑄 = ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)))    &   ⊢ (𝜑 → 𝑅 = ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))    &   ⊢ (𝜑 → 𝑈 = ((𝑃↑2) + (;12 · 𝑅)))    &   ⊢ (𝜑 → 𝑉 = ((-(2 · (𝑃↑3)) − (;27 · (𝑄↑2))) + (;72 · (𝑃 · 𝑅))))    &   ⊢ (𝜑 → 𝑊 = (√‘((𝑉↑2) − (4 · (𝑈↑3)))))    &   ⊢ (𝜑 → 𝑆 = ((√‘𝑀) / 2))    &   ⊢ (𝜑 → 𝑀 = -((((2 · 𝑃) + 𝑇) + (𝑈 / 𝑇)) / 3))    &   ⊢ (𝜑 → 𝑇 = (((𝑉 + 𝑊) / 2)↑𝑐(1 / 3)))    &   ⊢ (𝜑 → 𝑇 ≠ 0)    &   ⊢ (𝜑 → 𝑀 ≠ 0)    &   ⊢ (𝜑 → 𝐼 = (√‘((-(𝑆↑2) − (𝑃 / 2)) + ((𝑄 / 4) / 𝑆))))    &   ⊢ (𝜑 → 𝐽 = (√‘((-(𝑆↑2) − (𝑃 / 2)) − ((𝑄 / 4) / 𝑆))))    ⇒   ⊢ (𝜑 → (𝑆 ≠ 0 ∧ 𝐼 ∈ ℂ ∧ 𝐽 ∈ ℂ))
Theorem	quart 24388	The quartic equation, writing out all roots using square and cube root functions so that only direct substitutions remain, and we can actually claim to have a "quartic equation". Naturally, this theorem is ridiculously long (see quartfull 30401) if all the substitutions are performed. This is Metamath 100 proof #46. (Contributed by Mario Carneiro, 6-May-2015.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝐸 = -(𝐴 / 4))    &   ⊢ (𝜑 → 𝑃 = (𝐵 − ((3 / 8) · (𝐴↑2))))    &   ⊢ (𝜑 → 𝑄 = ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)))    &   ⊢ (𝜑 → 𝑅 = ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))    &   ⊢ (𝜑 → 𝑈 = ((𝑃↑2) + (;12 · 𝑅)))    &   ⊢ (𝜑 → 𝑉 = ((-(2 · (𝑃↑3)) − (;27 · (𝑄↑2))) + (;72 · (𝑃 · 𝑅))))    &   ⊢ (𝜑 → 𝑊 = (√‘((𝑉↑2) − (4 · (𝑈↑3)))))    &   ⊢ (𝜑 → 𝑆 = ((√‘𝑀) / 2))    &   ⊢ (𝜑 → 𝑀 = -((((2 · 𝑃) + 𝑇) + (𝑈 / 𝑇)) / 3))    &   ⊢ (𝜑 → 𝑇 = (((𝑉 + 𝑊) / 2)↑𝑐(1 / 3)))    &   ⊢ (𝜑 → 𝑇 ≠ 0)    &   ⊢ (𝜑 → 𝑀 ≠ 0)    &   ⊢ (𝜑 → 𝐼 = (√‘((-(𝑆↑2) − (𝑃 / 2)) + ((𝑄 / 4) / 𝑆))))    &   ⊢ (𝜑 → 𝐽 = (√‘((-(𝑆↑2) − (𝑃 / 2)) − ((𝑄 / 4) / 𝑆))))    ⇒   ⊢ (𝜑 → ((((𝑋↑4) + (𝐴 · (𝑋↑3))) + ((𝐵 · (𝑋↑2)) + ((𝐶 · 𝑋) + 𝐷))) = 0 ↔ ((𝑋 = ((𝐸 − 𝑆) + 𝐼) ∨ 𝑋 = ((𝐸 − 𝑆) − 𝐼)) ∨ (𝑋 = ((𝐸 + 𝑆) + 𝐽) ∨ 𝑋 = ((𝐸 + 𝑆) − 𝐽)))))
14.3.8  Inverse trigonometric functions
Syntax	casin 24389	The arcsine function.
class arcsin
Syntax	cacos 24390	The arccosine function.
class arccos
Syntax	catan 24391	The arctangent function.
class arctan
Definition	df-asin 24392	Define the arcsine function. Because sin is not a one-to-one function, the literal inverse ◡sin is not a function. Rather than attempt to find the right domain on which to restrict sin in order to get a total function, we just define it in terms of log, which we already know is total (except at 0). There are branch points at -1 and 1 (at which the function is defined), and branch cuts along the real line not between -1 and 1, which is to say (-∞, -1) ∪ (1, +∞). (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ arcsin = (𝑥 ∈ ℂ ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))
Definition	df-acos 24393	Define the arccosine function. See also remarks for df-asin 24392. Since we define arccos in terms of arcsin, it shares the same branch points and cuts, namely (-∞, -1) ∪ (1, +∞). (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ arccos = (𝑥 ∈ ℂ ↦ ((π / 2) − (arcsin‘𝑥)))
Definition	df-atan 24394	Define the arctangent function. See also remarks for df-asin 24392. Unlike arcsin and arccos, this function is not defined everywhere, because tan(𝑧) ≠ ±i for all 𝑧 ∈ ℂ. For all other 𝑧, there is a formula for arctan(𝑧) in terms of log, and we take that as the definition. Branch points are at ±i; branch cuts are on the pure imaginary axis not between -i and i, which is to say {𝑧 ∈ ℂ ∣ (i · 𝑧) ∈ (-∞, -1) ∪ (1, +∞)}. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ arctan = (𝑥 ∈ (ℂ ∖ {-i, i}) ↦ ((i / 2) · ((log‘(1 − (i · 𝑥))) − (log‘(1 + (i · 𝑥))))))
Theorem	asinlem 24395	The argument to the logarithm in df-asin 24392 is always nonzero. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ (𝐴 ∈ ℂ → ((i · 𝐴) + (√‘(1 − (𝐴↑2)))) ≠ 0)
Theorem	asinlem2 24396	The argument to the logarithm in df-asin 24392 has the property that replacing 𝐴 with -𝐴 in the expression gives the reciprocal. (Contributed by Mario Carneiro, 1-Apr-2015.)
⊢ (𝐴 ∈ ℂ → (((i · 𝐴) + (√‘(1 − (𝐴↑2)))) · ((i · -𝐴) + (√‘(1 − (-𝐴↑2))))) = 1)
Theorem	asinlem3a 24397	Lemma for asinlem3 24398. (Contributed by Mario Carneiro, 1-Apr-2015.)
⊢ ((𝐴 ∈ ℂ ∧ (ℑ‘𝐴) ≤ 0) → 0 ≤ (ℜ‘((i · 𝐴) + (√‘(1 − (𝐴↑2))))))
Theorem	asinlem3 24398	The argument to the logarithm in df-asin 24392 has nonnegative real part. (Contributed by Mario Carneiro, 1-Apr-2015.)
⊢ (𝐴 ∈ ℂ → 0 ≤ (ℜ‘((i · 𝐴) + (√‘(1 − (𝐴↑2))))))
Theorem	asinf 24399	Domain and range of the arcsin function. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ arcsin:ℂ⟶ℂ
Theorem	asincl 24400	Closure for the arcsin function. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ (𝐴 ∈ ℂ → (arcsin‘𝐴) ∈ ℂ)