| Metamath
Proof Explorer Theorem List (p. 269 of 494) | < Previous Next > | |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | zrtelqelz 26801 | If the 𝑁-th root of an integer 𝐴 is rational, that root is must be an integer. Similar to zsqrtelqelz 16795, generalized to positive integer roots. (Contributed by Steven Nguyen, 6-Apr-2023.) |
| ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑐(1 / 𝑁)) ∈ ℚ) → (𝐴↑𝑐(1 / 𝑁)) ∈ ℤ) | ||
| Theorem | zrtdvds 26802 | A positive integer root divides its integer. (Contributed by Steven Nguyen, 6-Apr-2023.) |
| ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑐(1 / 𝑁)) ∈ ℕ) → (𝐴↑𝑐(1 / 𝑁)) ∥ 𝐴) | ||
| Theorem | rtprmirr 26803 | The root of a prime number is irrational. (Contributed by Steven Nguyen, 6-Apr-2023.) |
| ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (ℤ≥‘2)) → (𝑃↑𝑐(1 / 𝑁)) ∈ (ℝ ∖ ℚ)) | ||
| Theorem | loglesqrt 26804 | An upper bound on the logarithm. (Contributed by Mario Carneiro, 2-May-2016.) (Proof shortened by AV, 2-Aug-2021.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (log‘(𝐴 + 1)) ≤ (√‘𝐴)) | ||
| Theorem | logreclem 26805 | Symmetry of the natural logarithm range by negation. Lemma for logrec 26806. (Contributed by Saveliy Skresanov, 27-Dec-2016.) |
| ⊢ ((𝐴 ∈ ran log ∧ ¬ (ℑ‘𝐴) = π) → -𝐴 ∈ ran log) | ||
| Theorem | logrec 26806 | Logarithm of a reciprocal changes sign. (Contributed by Saveliy Skresanov, 28-Dec-2016.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ (ℑ‘(log‘𝐴)) ≠ π) → (log‘𝐴) = -(log‘(1 / 𝐴))) | ||
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 26831, logbf 26832 and logbfval 26833. | ||
| Syntax | clogb 26807 | Extend class notation to include the logarithm generalized to an arbitrary base. |
| class logb | ||
| Definition | df-logb 26808* | 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 26809 | 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 26810 | General logarithm closure. (Contributed by David A. Wheeler, 17-Jul-2017.) |
| ⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ 𝑋 ∈ (ℂ ∖ {0})) → (𝐵 logb 𝑋) ∈ ℂ) | ||
| Theorem | logbid1 26811 | 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 26812 | The logarithm of 1 to an arbitrary base 𝐵 is 0. Property 1(b) of [Cohen4] p. 361. See log1 26627. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by Thierry Arnoux, 27-Sep-2017.) |
| ⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) → (𝐵 logb 1) = 0) | ||
| Theorem | elogb 26813 | 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 26814 | 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 26815 | Value of the general logarithm with integer base. (Contributed by Thierry Arnoux, 27-Sep-2017.) |
| ⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑋 ∈ ℝ+) → (𝐵 logb 𝑋) = ((log‘𝑋) / (log‘𝐵))) | ||
| Theorem | relogbcl 26816 | 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 26817 | 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 26818 | 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 26819 | 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 26820 | 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 26821 | 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 26822 | 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 26823 | 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 26824 | 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 26825 | Logarithm of a reciprocal changes sign. See logrec 26806. Particular case of Property 3 of [Cohen4] p. 361. (Contributed by Thierry Arnoux, 27-Sep-2017.) |
| ⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝐴 ∈ ℝ+) → (𝐵 logb (1 / 𝐴)) = -(𝐵 logb 𝐴)) | ||
| Theorem | logbleb 26826 | The general logarithm function is monotone/increasing. See logleb 26645. (Contributed by Stefan O'Rear, 19-Oct-2014.) (Revised by AV, 31-May-2020.) |
| ⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ+) → (𝑋 ≤ 𝑌 ↔ (𝐵 logb 𝑋) ≤ (𝐵 logb 𝑌))) | ||
| Theorem | logblt 26827 | The general logarithm function is strictly monotone/increasing. Property 2 of [Cohen4] p. 377. See logltb 26642. (Contributed by Stefan O'Rear, 19-Oct-2014.) (Revised by Thierry Arnoux, 27-Sep-2017.) |
| ⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ+) → (𝑋 < 𝑌 ↔ (𝐵 logb 𝑋) < (𝐵 logb 𝑌))) | ||
| Theorem | relogbcxp 26828 | Identity law for the general logarithm for real numbers. (Contributed by AV, 22-May-2020.) |
| ⊢ ((𝐵 ∈ (ℝ+ ∖ {1}) ∧ 𝑋 ∈ ℝ) → (𝐵 logb (𝐵↑𝑐𝑋)) = 𝑋) | ||
| Theorem | cxplogb 26829 | Identity law for the general logarithm. (Contributed by AV, 22-May-2020.) |
| ⊢ ((𝐵 ∈ (ℂ ∖ {0, 1}) ∧ 𝑋 ∈ (ℂ ∖ {0})) → (𝐵↑𝑐(𝐵 logb 𝑋)) = 𝑋) | ||
| Theorem | relogbcxpb 26830 | The logarithm is the inverse of the exponentiation. Observation in [Cohen4] p. 348. (Contributed by AV, 11-Jun-2020.) |
| ⊢ (((𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ) → ((𝐵 logb 𝑋) = 𝑌 ↔ (𝐵↑𝑐𝑌) = 𝑋)) | ||
| Theorem | logbmpt 26831* | 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 26832 | The general logarithm to a fixed base regarded as function. (Contributed by AV, 11-Jun-2020.) |
| ⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) → (curry logb ‘𝐵):(ℂ ∖ {0})⟶ℂ) | ||
| Theorem | logbfval 26833 | 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 26834 | 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 26835 | 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 | ||
| Theorem | logbgt0b 26836 | The logarithm of a positive real number to a real base greater than 1 is positive iff the number is greater than 1. (Contributed by AV, 29-Dec-2022.) |
| ⊢ ((𝐴 ∈ ℝ+ ∧ (𝐵 ∈ ℝ+ ∧ 1 < 𝐵)) → (0 < (𝐵 logb 𝐴) ↔ 1 < 𝐴)) | ||
| Theorem | logbgcd1irr 26837 | The logarithm of an integer greater than 1 to an integer base greater than 1 is an irrational number if the argument and the base are relatively prime. For example, (2 logb 9) ∈ (ℝ ∖ ℚ) (see 2logb9irr 26838). (Contributed by AV, 29-Dec-2022.) |
| ⊢ ((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2) ∧ (𝑋 gcd 𝐵) = 1) → (𝐵 logb 𝑋) ∈ (ℝ ∖ ℚ)) | ||
| Theorem | 2logb9irr 26838 | Example for logbgcd1irr 26837. The logarithm of nine to base two is irrational. (Contributed by AV, 29-Dec-2022.) |
| ⊢ (2 logb 9) ∈ (ℝ ∖ ℚ) | ||
| Theorem | logbprmirr 26839 | The logarithm of a prime to a different prime base is an irrational number. For example, (2 logb 3) ∈ (ℝ ∖ ℚ) (see 2logb3irr 26840). (Contributed by AV, 31-Dec-2022.) |
| ⊢ ((𝑋 ∈ ℙ ∧ 𝐵 ∈ ℙ ∧ 𝑋 ≠ 𝐵) → (𝐵 logb 𝑋) ∈ (ℝ ∖ ℚ)) | ||
| Theorem | 2logb3irr 26840 | Example for logbprmirr 26839. The logarithm of three to base two is irrational. (Contributed by AV, 31-Dec-2022.) |
| ⊢ (2 logb 3) ∈ (ℝ ∖ ℚ) | ||
| Theorem | 2logb9irrALT 26841 | Alternate proof of 2logb9irr 26838: The logarithm of nine to base two is irrational. (Contributed by AV, 31-Dec-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (2 logb 9) ∈ (ℝ ∖ ℚ) | ||
| Theorem | sqrt2cxp2logb9e3 26842 | The square root of two to the power of the logarithm of nine to base two is three. (√‘2) and (2 logb 9) are irrational numbers (see sqrt2irr0 16287 resp. 2logb9irr 26838), satisfying the statement in 2irrexpqALT 26843. (Contributed by AV, 29-Dec-2022.) |
| ⊢ ((√‘2)↑𝑐(2 logb 9)) = 3 | ||
| Theorem | 2irrexpqALT 26843* | Alternate proof of 2irrexpq 26773: There exist irrational numbers 𝑎 and 𝑏 such that (𝑎↑𝑏) is rational. Statement in the Metamath book, section 1.1.5, footnote 27 on page 17, and the "constructive proof" for theorem 1.2 of [Bauer], p. 483. In contrast to 2irrexpq 26773, this is a constructive proof because it is based on two explicitly named irrational numbers (√‘2) and (2 logb 9), see sqrt2irr0 16287, 2logb9irr 26838 and sqrt2cxp2logb9e3 26842. Therefore, this proof is also acceptable/usable in intuitionistic logic. (Contributed by AV, 23-Dec-2022.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ ∃𝑎 ∈ (ℝ ∖ ℚ)∃𝑏 ∈ (ℝ ∖ ℚ)(𝑎↑𝑐𝑏) ∈ ℚ | ||
| Theorem | angval 26844* | 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 26845* | Cancel a constant multiplier in the angle function. (Contributed by Mario Carneiro, 23-Sep-2014.) |
| ⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥)))) ⇒ ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐶 · 𝐴)𝐹(𝐶 · 𝐵)) = (𝐴𝐹𝐵)) | ||
| Theorem | angneg 26846* | Cancel a negative sign in the angle function. (Contributed by Mario Carneiro, 23-Sep-2014.) |
| ⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥)))) ⇒ ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → (-𝐴𝐹-𝐵) = (𝐴𝐹𝐵)) | ||
| Theorem | angvald 26847* | The (signed) angle between two vectors is the argument of their quotient. Deduction form of angval 26844. (Contributed by David Moews, 28-Feb-2017.) |
| ⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥)))) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ≠ 0) & ⊢ (𝜑 → 𝑌 ∈ ℂ) & ⊢ (𝜑 → 𝑌 ≠ 0) ⇒ ⊢ (𝜑 → (𝑋𝐹𝑌) = (ℑ‘(log‘(𝑌 / 𝑋)))) | ||
| Theorem | angcld 26848* | The (signed) angle between two vectors is in (-π(,]π). Deduction form. (Contributed by David Moews, 28-Feb-2017.) |
| ⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥)))) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ≠ 0) & ⊢ (𝜑 → 𝑌 ∈ ℂ) & ⊢ (𝜑 → 𝑌 ≠ 0) ⇒ ⊢ (𝜑 → (𝑋𝐹𝑌) ∈ (-π(,]π)) | ||
| Theorem | angrteqvd 26849* | 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 26850* | 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 26851* | 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 26852* | Lemma for ang180 26857. Show that the "revolution number" 𝑁 is an integer, using efeq1 26570 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 26853* | Lemma for ang180 26857. 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 26611, 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 26854* | Lemma for ang180 26857. Since ang180lem1 26852 shows that 𝑁 is an integer and ang180lem2 26853 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 26855* | Lemma for ang180 26857. Reduce the statement to one variable. (Contributed by Mario Carneiro, 23-Sep-2014.) |
| ⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥)))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((((1 − 𝐴)𝐹1) + (𝐴𝐹(𝐴 − 1))) + (1𝐹𝐴)) ∈ {-π, π}) | ||
| Theorem | ang180lem5 26856* | Lemma for ang180 26857: Reduce the statement to two variables. (Contributed by Mario Carneiro, 23-Sep-2014.) |
| ⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥)))) ⇒ ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ 𝐴 ≠ 𝐵) → ((((𝐴 − 𝐵)𝐹𝐴) + (𝐵𝐹(𝐵 − 𝐴))) + (𝐴𝐹𝐵)) ∈ {-π, π}) | ||
| Theorem | ang180 26857* | 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 26858 | Lemma for lawcos 26859. 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 26859* | 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 26857), 𝑋 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 26858 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 16183). The Pythagorean theorem pythag 26860 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 26860* | 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 26857), 𝑋 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 26859 to prove this, along with simple trigonometry facts like coshalfpi 26511 and cosneg 16183. (Contributed by David A. Wheeler, 13-Jun-2015.) |
| ⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥)))) & ⊢ 𝑋 = (abs‘(𝐵 − 𝐶)) & ⊢ 𝑌 = (abs‘(𝐴 − 𝐶)) & ⊢ 𝑍 = (abs‘(𝐴 − 𝐵)) & ⊢ 𝑂 = ((𝐵 − 𝐶)𝐹(𝐴 − 𝐶)) ⇒ ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑂 ∈ {(π / 2), -(π / 2)}) → (𝑍↑2) = ((𝑋↑2) + (𝑌↑2))) | ||
| Theorem | isosctrlem1 26861 | Lemma for isosctr 26864. (Contributed by Saveliy Skresanov, 30-Dec-2016.) |
| ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (ℑ‘(log‘(1 − 𝐴))) ≠ π) | ||
| Theorem | isosctrlem2 26862 | Lemma for isosctr 26864. 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 26863* | Lemma for isosctr 26864. 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 26864* | Isosceles triangle theorem. This is Metamath 100 proof #65. (Contributed by Saveliy Skresanov, 1-Jan-2017.) |
| ⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥)))) ⇒ ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵) ∧ (abs‘(𝐴 − 𝐶)) = (abs‘(𝐵 − 𝐶))) → ((𝐶 − 𝐴)𝐹(𝐵 − 𝐴)) = ((𝐴 − 𝐵)𝐹(𝐶 − 𝐵))) | ||
| Theorem | ssscongptld 26865* |
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 26859 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 26866 | Equivalence between two ways of expressing 𝐵 as an affine combination of 𝐴 and 𝐶. (Contributed by David Moews, 28-Feb-2017.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐵 = ((𝐷 · 𝐴) + ((1 − 𝐷) · 𝐶)) ↔ (𝐶 − 𝐵) = (𝐷 · (𝐶 − 𝐴)))) | ||
| Theorem | affineequiv2 26867 | Equivalence between two ways of expressing 𝐵 as an affine combination of 𝐴 and 𝐶. (Contributed by David Moews, 28-Feb-2017.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐵 = ((𝐷 · 𝐴) + ((1 − 𝐷) · 𝐶)) ↔ (𝐵 − 𝐴) = ((1 − 𝐷) · (𝐶 − 𝐴)))) | ||
| Theorem | affineequiv3 26868 | Equivalence between two ways of expressing 𝐴 as an affine combination of 𝐵 and 𝐶. (Contributed by AV, 22-Jan-2023.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 = (((1 − 𝐷) · 𝐵) + (𝐷 · 𝐶)) ↔ (𝐴 − 𝐵) = (𝐷 · (𝐶 − 𝐵)))) | ||
| Theorem | affineequiv4 26869 | Equivalence between two ways of expressing 𝐴 as an affine combination of 𝐵 and 𝐶. (Contributed by AV, 22-Jan-2023.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 = (((1 − 𝐷) · 𝐵) + (𝐷 · 𝐶)) ↔ 𝐴 = ((𝐷 · (𝐶 − 𝐵)) + 𝐵))) | ||
| Theorem | affineequivne 26870 | Equivalence between two ways of expressing 𝐴 as an affine combination of 𝐵 and 𝐶 if 𝐵 and 𝐶 are not equal. (Contributed by AV, 22-Jan-2023.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → (𝐴 = (((1 − 𝐷) · 𝐵) + (𝐷 · 𝐶)) ↔ 𝐷 = ((𝐴 − 𝐵) / (𝐶 − 𝐵)))) | ||
| Theorem | angpieqvdlem 26871 | Equivalence used in the proof of angpieqvd 26874. (Contributed by David Moews, 28-Feb-2017.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐴 ≠ 𝐶) ⇒ ⊢ (𝜑 → (-((𝐶 − 𝐵) / (𝐴 − 𝐵)) ∈ ℝ+ ↔ ((𝐶 − 𝐵) / (𝐶 − 𝐴)) ∈ (0(,)1))) | ||
| Theorem | angpieqvdlem2 26872* | Equivalence used in angpieqvd 26874. (Contributed by David Moews, 28-Feb-2017.) |
| ⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥)))) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → (-((𝐶 − 𝐵) / (𝐴 − 𝐵)) ∈ ℝ+ ↔ ((𝐴 − 𝐵)𝐹(𝐶 − 𝐵)) = π)) | ||
| Theorem | angpined 26873* | If the angle at ABC is π, then 𝐴 is not equal to 𝐶. (Contributed by David Moews, 28-Feb-2017.) |
| ⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥)))) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → (((𝐴 − 𝐵)𝐹(𝐶 − 𝐵)) = π → 𝐴 ≠ 𝐶)) | ||
| Theorem | angpieqvd 26874* | The angle ABC is π iff 𝐵 is a nontrivial convex combination of 𝐴 and 𝐶, i.e., iff 𝐵 is in the interior of the segment AC. (Contributed by David Moews, 28-Feb-2017.) |
| ⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥)))) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → (((𝐴 − 𝐵)𝐹(𝐶 − 𝐵)) = π ↔ ∃𝑤 ∈ (0(,)1)𝐵 = ((𝑤 · 𝐴) + ((1 − 𝑤) · 𝐶)))) | ||
| Theorem | chordthmlem 26875* | If 𝑀 is the midpoint of AB and AQ = BQ, then QMB is a right angle. The proof uses ssscongptld 26865 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 angles. (Contributed by David Moews, 28-Feb-2017.) |
| ⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥)))) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝑄 ∈ ℂ) & ⊢ (𝜑 → 𝑀 = ((𝐴 + 𝐵) / 2)) & ⊢ (𝜑 → (abs‘(𝐴 − 𝑄)) = (abs‘(𝐵 − 𝑄))) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝑄 ≠ 𝑀) ⇒ ⊢ (𝜑 → ((𝑄 − 𝑀)𝐹(𝐵 − 𝑀)) ∈ {(π / 2), -(π / 2)}) | ||
| Theorem | chordthmlem2 26876* | 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 26875, where P = B, and using angrtmuld 26851 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 26877 | 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 26876 and the Pythagorean theorem (pythag 26860) 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 26878 | 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 26879 | If P is on the segment AB and AQ = BQ, then PA · PB = BQ 2 − PQ 2 . This follows from two uses of chordthmlem3 26877 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 26878. (Contributed by David Moews, 28-Feb-2017.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝑄 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ∈ (0[,]1)) & ⊢ (𝜑 → 𝑃 = ((𝑋 · 𝐴) + ((1 − 𝑋) · 𝐵))) & ⊢ (𝜑 → (abs‘(𝐴 − 𝑄)) = (abs‘(𝐵 − 𝑄))) ⇒ ⊢ (𝜑 → ((abs‘(𝑃 − 𝐴)) · (abs‘(𝑃 − 𝐵))) = (((abs‘(𝐵 − 𝑄))↑2) − ((abs‘(𝑃 − 𝑄))↑2))) | ||
| Theorem | chordthm 26880* | 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 26879 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 26881* | 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‘𝑂))) = (√‘((𝑆 · (𝑆 − 𝑋)) · ((𝑆 − 𝑌) · (𝑆 − 𝑍))))) | ||
| Theorem | quad2 26882 | 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 26883 | The quadratic equation. (Contributed by Mario Carneiro, 23-Apr-2015.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝐷 = ((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ⇒ ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0 ↔ (𝑋 = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∨ 𝑋 = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴))))) | ||
| Theorem | 1cubrlem 26884 | 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 26885 | 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 26886 | Lemma for dcubic1 26888 and dcubic2 26887: 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 26887* | Reverse direction of dcubic 26889. 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 26888 | Forward direction of dcubic 26889: 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 26889* | Solutions to the depressed cubic, a special case of cubic 26892. (The definitions of 𝑀, 𝑁, 𝐺, 𝑇 here differ from mcubic 26890 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 26890* | Solutions to a monic cubic equation, a special case of cubic 26892. (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 26891* | 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 26892* | The cubic equation, which gives the roots of an arbitrary (nondegenerate) cubic function. Use rextp 4706 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 26893 | Work out a quartic binomial. (You would think that by this point it would be faster to use binom 15866, 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 26894 | Lemma for dquart 26896. (Contributed by Mario Carneiro, 6-May-2015.) |
| ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝑆 ∈ ℂ) & ⊢ (𝜑 → 𝑀 = ((2 · 𝑆)↑2)) & ⊢ (𝜑 → 𝑀 ≠ 0) & ⊢ (𝜑 → 𝐼 ∈ ℂ) & ⊢ (𝜑 → (𝐼↑2) = ((-(𝑆↑2) − (𝐵 / 2)) + ((𝐶 / 4) / 𝑆))) ⇒ ⊢ (𝜑 → ((((𝑋↑2) + ((𝑀 + 𝐵) / 2)) + ((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / 𝑆)) = 0 ↔ (𝑋 = (-𝑆 + 𝐼) ∨ 𝑋 = (-𝑆 − 𝐼)))) | ||
| Theorem | dquartlem2 26895 | Lemma for dquart 26896. (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 26896 | Solve a depressed quartic equation. To eliminate 𝑆, which is the square root of a solution 𝑀 to the resolvent cubic equation, apply cubic 26892 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 26897 | Closure lemmas for quart 26904. (Contributed by Mario Carneiro, 7-May-2015.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝑃 = (𝐵 − ((3 / 8) · (𝐴↑2)))) & ⊢ (𝜑 → 𝑄 = ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))) & ⊢ (𝜑 → 𝑅 = ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))) ⇒ ⊢ (𝜑 → (𝑃 ∈ ℂ ∧ 𝑄 ∈ ℂ ∧ 𝑅 ∈ ℂ)) | ||
| Theorem | quart1lem 26898 | Lemma for quart1 26899. (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 26899 | 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 26900 | Lemma for quart 26904. (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))))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |