![]() |
Metamath
Proof Explorer Theorem List (p. 262 of 472) | < 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-29689) |
![]() (29690-31212) |
![]() (31213-47147) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sqrt2cxp2logb9e3 26101 | 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 16093 resp. 2logb9irr 26097), satisfying the statement in 2irrexpqALT 26102. (Contributed by AV, 29-Dec-2022.) |
⊢ ((√‘2)↑𝑐(2 logb 9)) = 3 | ||
Theorem | 2irrexpqALT 26102* | Alternate proof of 2irrexpq 26037: 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 26037, this is a constructive proof because it is based on two explicitly named irrational numbers (√‘2) and (2 logb 9), see sqrt2irr0 16093, 2logb9irr 26097 and sqrt2cxp2logb9e3 26101. 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 26103* | 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 26104* | Cancel a constant multiplier in the angle function. (Contributed by Mario Carneiro, 23-Sep-2014.) |
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥)))) ⇒ ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐶 · 𝐴)𝐹(𝐶 · 𝐵)) = (𝐴𝐹𝐵)) | ||
Theorem | angneg 26105* | Cancel a negative sign in the angle function. (Contributed by Mario Carneiro, 23-Sep-2014.) |
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥)))) ⇒ ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → (-𝐴𝐹-𝐵) = (𝐴𝐹𝐵)) | ||
Theorem | angvald 26106* | The (signed) angle between two vectors is the argument of their quotient. Deduction form of angval 26103. (Contributed by David Moews, 28-Feb-2017.) |
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥)))) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ≠ 0) & ⊢ (𝜑 → 𝑌 ∈ ℂ) & ⊢ (𝜑 → 𝑌 ≠ 0) ⇒ ⊢ (𝜑 → (𝑋𝐹𝑌) = (ℑ‘(log‘(𝑌 / 𝑋)))) | ||
Theorem | angcld 26107* | The (signed) angle between two vectors is in (-π(,]π). Deduction form. (Contributed by David Moews, 28-Feb-2017.) |
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥)))) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ≠ 0) & ⊢ (𝜑 → 𝑌 ∈ ℂ) & ⊢ (𝜑 → 𝑌 ≠ 0) ⇒ ⊢ (𝜑 → (𝑋𝐹𝑌) ∈ (-π(,]π)) | ||
Theorem | angrteqvd 26108* | 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 26109* | 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 26110* | 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 26111* | Lemma for ang180 26116. Show that the "revolution number" 𝑁 is an integer, using efeq1 25836 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 26112* | Lemma for ang180 26116. 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 25877, 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 26113* | Lemma for ang180 26116. Since ang180lem1 26111 shows that 𝑁 is an integer and ang180lem2 26112 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 26114* | Lemma for ang180 26116. Reduce the statement to one variable. (Contributed by Mario Carneiro, 23-Sep-2014.) |
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥)))) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1) → ((((1 − 𝐴)𝐹1) + (𝐴𝐹(𝐴 − 1))) + (1𝐹𝐴)) ∈ {-π, π}) | ||
Theorem | ang180lem5 26115* | Lemma for ang180 26116: Reduce the statement to two variables. (Contributed by Mario Carneiro, 23-Sep-2014.) |
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥)))) ⇒ ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ 𝐴 ≠ 𝐵) → ((((𝐴 − 𝐵)𝐹𝐴) + (𝐵𝐹(𝐵 − 𝐴))) + (𝐴𝐹𝐵)) ∈ {-π, π}) | ||
Theorem | ang180 26116* | 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 26117 | Lemma for lawcos 26118. 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 26118* | 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 26116), 𝑋 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 26117 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 15989). The Pythagorean theorem pythag 26119 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 26119* | 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 26116), 𝑋 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 26118 to prove this, along with simple trigonometry facts like coshalfpi 25778 and cosneg 15989. (Contributed by David A. Wheeler, 13-Jun-2015.) |
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥)))) & ⊢ 𝑋 = (abs‘(𝐵 − 𝐶)) & ⊢ 𝑌 = (abs‘(𝐴 − 𝐶)) & ⊢ 𝑍 = (abs‘(𝐴 − 𝐵)) & ⊢ 𝑂 = ((𝐵 − 𝐶)𝐹(𝐴 − 𝐶)) ⇒ ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑂 ∈ {(π / 2), -(π / 2)}) → (𝑍↑2) = ((𝑋↑2) + (𝑌↑2))) | ||
Theorem | isosctrlem1 26120 | Lemma for isosctr 26123. (Contributed by Saveliy Skresanov, 30-Dec-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (ℑ‘(log‘(1 − 𝐴))) ≠ π) | ||
Theorem | isosctrlem2 26121 | Lemma for isosctr 26123. 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 26122* | Lemma for isosctr 26123. 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 26123* | Isosceles triangle theorem. This is Metamath 100 proof #65. (Contributed by Saveliy Skresanov, 1-Jan-2017.) |
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥)))) ⇒ ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐵) ∧ (abs‘(𝐴 − 𝐶)) = (abs‘(𝐵 − 𝐶))) → ((𝐶 − 𝐴)𝐹(𝐵 − 𝐴)) = ((𝐴 − 𝐵)𝐹(𝐶 − 𝐵))) | ||
Theorem | ssscongptld 26124* |
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 26118 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 26125 | Equivalence between two ways of expressing 𝐵 as an affine combination of 𝐴 and 𝐶. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐵 = ((𝐷 · 𝐴) + ((1 − 𝐷) · 𝐶)) ↔ (𝐶 − 𝐵) = (𝐷 · (𝐶 − 𝐴)))) | ||
Theorem | affineequiv2 26126 | Equivalence between two ways of expressing 𝐵 as an affine combination of 𝐴 and 𝐶. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐵 = ((𝐷 · 𝐴) + ((1 − 𝐷) · 𝐶)) ↔ (𝐵 − 𝐴) = ((1 − 𝐷) · (𝐶 − 𝐴)))) | ||
Theorem | affineequiv3 26127 | Equivalence between two ways of expressing 𝐴 as an affine combination of 𝐵 and 𝐶. (Contributed by AV, 22-Jan-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 = (((1 − 𝐷) · 𝐵) + (𝐷 · 𝐶)) ↔ (𝐴 − 𝐵) = (𝐷 · (𝐶 − 𝐵)))) | ||
Theorem | affineequiv4 26128 | Equivalence between two ways of expressing 𝐴 as an affine combination of 𝐵 and 𝐶. (Contributed by AV, 22-Jan-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 = (((1 − 𝐷) · 𝐵) + (𝐷 · 𝐶)) ↔ 𝐴 = ((𝐷 · (𝐶 − 𝐵)) + 𝐵))) | ||
Theorem | affineequivne 26129 | 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 26130 | Equivalence used in the proof of angpieqvd 26133. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐴 ≠ 𝐶) ⇒ ⊢ (𝜑 → (-((𝐶 − 𝐵) / (𝐴 − 𝐵)) ∈ ℝ+ ↔ ((𝐶 − 𝐵) / (𝐶 − 𝐴)) ∈ (0(,)1))) | ||
Theorem | angpieqvdlem2 26131* | Equivalence used in angpieqvd 26133. (Contributed by David Moews, 28-Feb-2017.) |
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥)))) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → (-((𝐶 − 𝐵) / (𝐴 − 𝐵)) ∈ ℝ+ ↔ ((𝐴 − 𝐵)𝐹(𝐶 − 𝐵)) = π)) | ||
Theorem | angpined 26132* | If the angle at ABC is π, then 𝐴 is not equal to 𝐶. (Contributed by David Moews, 28-Feb-2017.) |
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥)))) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → (((𝐴 − 𝐵)𝐹(𝐶 − 𝐵)) = π → 𝐴 ≠ 𝐶)) | ||
Theorem | angpieqvd 26133* | 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 26134* | If 𝑀 is the midpoint of AB and AQ = BQ, then QMB is a right angle. The proof uses ssscongptld 26124 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 26135* | 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 26134, where P = B, and using angrtmuld 26110 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 26136 | 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 26135 and the Pythagorean theorem (pythag 26119) 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 26137 | 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 26138 | If P is on the segment AB and AQ = BQ, then PA · PB = BQ 2 − PQ 2 . This follows from two uses of chordthmlem3 26136 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 26137. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝑄 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ∈ (0[,]1)) & ⊢ (𝜑 → 𝑃 = ((𝑋 · 𝐴) + ((1 − 𝑋) · 𝐵))) & ⊢ (𝜑 → (abs‘(𝐴 − 𝑄)) = (abs‘(𝐵 − 𝑄))) ⇒ ⊢ (𝜑 → ((abs‘(𝑃 − 𝐴)) · (abs‘(𝑃 − 𝐵))) = (((abs‘(𝐵 − 𝑄))↑2) − ((abs‘(𝑃 − 𝑄))↑2))) | ||
Theorem | chordthm 26139* | 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 26138 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 26140* | 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 26141 | 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 26142 | The quadratic equation. (Contributed by Mario Carneiro, 23-Apr-2015.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝐷 = ((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ⇒ ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0 ↔ (𝑋 = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∨ 𝑋 = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴))))) | ||
Theorem | 1cubrlem 26143 | 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 26144 | 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 26145 | Lemma for dcubic1 26147 and dcubic2 26146: 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 26146* | Reverse direction of dcubic 26148. 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 26147 | Forward direction of dcubic 26148: 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 26148* | Solutions to the depressed cubic, a special case of cubic 26151. (The definitions of 𝑀, 𝑁, 𝐺, 𝑇 here differ from mcubic 26149 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 26149* | Solutions to a monic cubic equation, a special case of cubic 26151. (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 26150* | 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 26151* | The cubic equation, which gives the roots of an arbitrary (nondegenerate) cubic function. Use rextp 4666 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 26152 | Work out a quartic binomial. (You would think that by this point it would be faster to use binom 15675, 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 26153 | Lemma for dquart 26155. (Contributed by Mario Carneiro, 6-May-2015.) |
⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝑆 ∈ ℂ) & ⊢ (𝜑 → 𝑀 = ((2 · 𝑆)↑2)) & ⊢ (𝜑 → 𝑀 ≠ 0) & ⊢ (𝜑 → 𝐼 ∈ ℂ) & ⊢ (𝜑 → (𝐼↑2) = ((-(𝑆↑2) − (𝐵 / 2)) + ((𝐶 / 4) / 𝑆))) ⇒ ⊢ (𝜑 → ((((𝑋↑2) + ((𝑀 + 𝐵) / 2)) + ((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / 𝑆)) = 0 ↔ (𝑋 = (-𝑆 + 𝐼) ∨ 𝑋 = (-𝑆 − 𝐼)))) | ||
Theorem | dquartlem2 26154 | Lemma for dquart 26155. (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 26155 | Solve a depressed quartic equation. To eliminate 𝑆, which is the square root of a solution 𝑀 to the resolvent cubic equation, apply cubic 26151 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 26156 | Closure lemmas for quart 26163. (Contributed by Mario Carneiro, 7-May-2015.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝑃 = (𝐵 − ((3 / 8) · (𝐴↑2)))) & ⊢ (𝜑 → 𝑄 = ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))) & ⊢ (𝜑 → 𝑅 = ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))) ⇒ ⊢ (𝜑 → (𝑃 ∈ ℂ ∧ 𝑄 ∈ ℂ ∧ 𝑅 ∈ ℂ)) | ||
Theorem | quart1lem 26157 | Lemma for quart1 26158. (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 26158 | 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 26159 | Lemma for quart 26163. (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 26160 | Closure lemmas for quart 26163. (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 26161 | Closure lemmas for quart 26163. (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 26162 | Closure lemmas for quart 26163. (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 26163 | 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 33563) 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 ↔ ((𝑋 = ((𝐸 − 𝑆) + 𝐼) ∨ 𝑋 = ((𝐸 − 𝑆) − 𝐼)) ∨ (𝑋 = ((𝐸 + 𝑆) + 𝐽) ∨ 𝑋 = ((𝐸 + 𝑆) − 𝐽))))) | ||
Syntax | casin 26164 | The arcsine function. |
class arcsin | ||
Syntax | cacos 26165 | The arccosine function. |
class arccos | ||
Syntax | catan 26166 | The arctangent function. |
class arctan | ||
Definition | df-asin 26167 | 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 26168 | Define the arccosine function. See also remarks for df-asin 26167. 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 26169 | Define the arctangent function. See also remarks for df-asin 26167. 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 26170 | The argument to the logarithm in df-asin 26167 is always nonzero. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ ℂ → ((i · 𝐴) + (√‘(1 − (𝐴↑2)))) ≠ 0) | ||
Theorem | asinlem2 26171 | The argument to the logarithm in df-asin 26167 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 26172 | Lemma for asinlem3 26173. (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (ℑ‘𝐴) ≤ 0) → 0 ≤ (ℜ‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) | ||
Theorem | asinlem3 26173 | The argument to the logarithm in df-asin 26167 has nonnegative real part. (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ (𝐴 ∈ ℂ → 0 ≤ (ℜ‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) | ||
Theorem | asinf 26174 | Domain and codomain of the arcsin function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ arcsin:ℂ⟶ℂ | ||
Theorem | asincl 26175 | Closure for the arcsin function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ ℂ → (arcsin‘𝐴) ∈ ℂ) | ||
Theorem | acosf 26176 | Domain and codoamin of the arccos function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ arccos:ℂ⟶ℂ | ||
Theorem | acoscl 26177 | Closure for the arccos function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ ℂ → (arccos‘𝐴) ∈ ℂ) | ||
Theorem | atandm 26178 | Since the property is a little lengthy, we abbreviate 𝐴 ∈ ℂ ∧ 𝐴 ≠ -i ∧ 𝐴 ≠ i as 𝐴 ∈ dom arctan. This is the necessary precondition for the definition of arctan to make sense. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ dom arctan ↔ (𝐴 ∈ ℂ ∧ 𝐴 ≠ -i ∧ 𝐴 ≠ i)) | ||
Theorem | atandm2 26179 | This form of atandm 26178 is a bit more useful for showing that the logarithms in df-atan 26169 are well-defined. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ dom arctan ↔ (𝐴 ∈ ℂ ∧ (1 − (i · 𝐴)) ≠ 0 ∧ (1 + (i · 𝐴)) ≠ 0)) | ||
Theorem | atandm3 26180 | A compact form of atandm 26178. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ dom arctan ↔ (𝐴 ∈ ℂ ∧ (𝐴↑2) ≠ -1)) | ||
Theorem | atandm4 26181 | A compact form of atandm 26178. (Contributed by Mario Carneiro, 3-Apr-2015.) |
⊢ (𝐴 ∈ dom arctan ↔ (𝐴 ∈ ℂ ∧ (1 + (𝐴↑2)) ≠ 0)) | ||
Theorem | atanf 26182 | Domain and codoamin of the arctan function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ arctan:(ℂ ∖ {-i, i})⟶ℂ | ||
Theorem | atancl 26183 | Closure for the arctan function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ dom arctan → (arctan‘𝐴) ∈ ℂ) | ||
Theorem | asinval 26184 | Value of the arcsin function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ ℂ → (arcsin‘𝐴) = (-i · (log‘((i · 𝐴) + (√‘(1 − (𝐴↑2))))))) | ||
Theorem | acosval 26185 | Value of the arccos function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ ℂ → (arccos‘𝐴) = ((π / 2) − (arcsin‘𝐴))) | ||
Theorem | atanval 26186 | Value of the arctan function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ dom arctan → (arctan‘𝐴) = ((i / 2) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i · 𝐴)))))) | ||
Theorem | atanre 26187 | A real number is in the domain of the arctangent function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ ℝ → 𝐴 ∈ dom arctan) | ||
Theorem | asinneg 26188 | The arcsine function is odd. (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ (𝐴 ∈ ℂ → (arcsin‘-𝐴) = -(arcsin‘𝐴)) | ||
Theorem | acosneg 26189 | The negative symmetry relation of the arccosine. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ ℂ → (arccos‘-𝐴) = (π − (arccos‘𝐴))) | ||
Theorem | efiasin 26190 | The exponential of the arcsine function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ ℂ → (exp‘(i · (arcsin‘𝐴))) = ((i · 𝐴) + (√‘(1 − (𝐴↑2))))) | ||
Theorem | sinasin 26191 | The arcsine function is an inverse to sin. This is the main property that justifies the notation arcsin or sin↑-1. Because sin is not an injection, the other converse identity asinsin 26194 is only true under limited circumstances. (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ (𝐴 ∈ ℂ → (sin‘(arcsin‘𝐴)) = 𝐴) | ||
Theorem | cosacos 26192 | The arccosine function is an inverse to cos. (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ (𝐴 ∈ ℂ → (cos‘(arccos‘𝐴)) = 𝐴) | ||
Theorem | asinsinlem 26193 | Lemma for asinsin 26194. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → 0 < (ℜ‘(exp‘(i · 𝐴)))) | ||
Theorem | asinsin 26194 | The arcsine function composed with sin is equal to the identity. This plus sinasin 26191 allow to view sin and arcsin as inverse operations to each other. For ease of use, we have not defined precisely the correct domain of correctness of this identity; in addition to the main region described here it is also true for some points on the branch cuts, namely when 𝐴 = (π / 2) − i𝑦 for nonnegative real 𝑦 and also symmetrically at 𝐴 = i𝑦 − (π / 2). In particular, when restricted to reals this identity extends to the closed interval [-(π / 2), (π / 2)], not just the open interval (see reasinsin 26198). (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (arcsin‘(sin‘𝐴)) = 𝐴) | ||
Theorem | acoscos 26195 | The arccosine function is an inverse to cos. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (0(,)π)) → (arccos‘(cos‘𝐴)) = 𝐴) | ||
Theorem | asin1 26196 | The arcsine of 1 is π / 2. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (arcsin‘1) = (π / 2) | ||
Theorem | acos1 26197 | The arccosine of 1 is 0. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (arccos‘1) = 0 | ||
Theorem | reasinsin 26198 | The arcsine function composed with sin is equal to the identity. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ (-(π / 2)[,](π / 2)) → (arcsin‘(sin‘𝐴)) = 𝐴) | ||
Theorem | asinsinb 26199 | Relationship between sine and arcsine. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (ℜ‘𝐵) ∈ (-(π / 2)(,)(π / 2))) → ((arcsin‘𝐴) = 𝐵 ↔ (sin‘𝐵) = 𝐴)) | ||
Theorem | acoscosb 26200 | Relationship between cosine and arccosine. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (ℜ‘𝐵) ∈ (0(,)π)) → ((arccos‘𝐴) = 𝐵 ↔ (cos‘𝐵) = 𝐴)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |