Home | Metamath
Proof Explorer Theorem List (p. 255 of 449) | < 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: | Metamath Proof Explorer
(1-28689) |
Hilbert Space Explorer
(28690-30212) |
Users' Mathboxes
(30213-44900) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | angpieqvdlem2 25401* | Equivalence used in angpieqvd 25403. (Contributed by David Moews, 28-Feb-2017.) |
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥)))) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → (-((𝐶 − 𝐵) / (𝐴 − 𝐵)) ∈ ℝ+ ↔ ((𝐴 − 𝐵)𝐹(𝐶 − 𝐵)) = π)) | ||
Theorem | angpined 25402* | 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 25403* | 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 25404* | If M is the midpoint of AB and AQ = BQ, then QMB is a right angle. The proof uses ssscongptld 25394 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 25405* | 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 25404, where P = B, and using angrtmuld 25380 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 25406 | 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 25405 and the Pythagorean theorem (pythag 25389) 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 25407 | 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 25408 | If P is on the segment AB and AQ = BQ, then PA · PB = BQ 2 − PQ 2 . This follows from two uses of chordthmlem3 25406 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 25407. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝑄 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ∈ (0[,]1)) & ⊢ (𝜑 → 𝑃 = ((𝑋 · 𝐴) + ((1 − 𝑋) · 𝐵))) & ⊢ (𝜑 → (abs‘(𝐴 − 𝑄)) = (abs‘(𝐵 − 𝑄))) ⇒ ⊢ (𝜑 → ((abs‘(𝑃 − 𝐴)) · (abs‘(𝑃 − 𝐵))) = (((abs‘(𝐵 − 𝑄))↑2) − ((abs‘(𝑃 − 𝑄))↑2))) | ||
Theorem | chordthm 25409* | 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 25408 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 25410* | 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 25411 | 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 25412 | The quadratic equation. (Contributed by Mario Carneiro, 23-Apr-2015.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝐷 = ((𝐵↑2) − (4 · (𝐴 · 𝐶)))) ⇒ ⊢ (𝜑 → (((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0 ↔ (𝑋 = ((-𝐵 + (√‘𝐷)) / (2 · 𝐴)) ∨ 𝑋 = ((-𝐵 − (√‘𝐷)) / (2 · 𝐴))))) | ||
Theorem | 1cubrlem 25413 | 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 25414 | 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 25415 | Lemma for dcubic1 25417 and dcubic2 25416: 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 25416* | Reverse direction of dcubic 25418. 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 25417 | Forward direction of dcubic 25418: 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 25418* | Solutions to the depressed cubic, a special case of cubic 25421. (The definitions of 𝑀, 𝑁, 𝐺, 𝑇 here differ from mcubic 25419 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 25419* | Solutions to a monic cubic equation, a special case of cubic 25421. (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 25420* | 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 25421* | The cubic equation, which gives the roots of an arbitrary (nondegenerate) cubic function. Use rextp 4635 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 25422 | Work out a quartic binomial. (You would think that by this point it would be faster to use binom 15179, 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 25423 | Lemma for dquart 25425. (Contributed by Mario Carneiro, 6-May-2015.) |
⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝑆 ∈ ℂ) & ⊢ (𝜑 → 𝑀 = ((2 · 𝑆)↑2)) & ⊢ (𝜑 → 𝑀 ≠ 0) & ⊢ (𝜑 → 𝐼 ∈ ℂ) & ⊢ (𝜑 → (𝐼↑2) = ((-(𝑆↑2) − (𝐵 / 2)) + ((𝐶 / 4) / 𝑆))) ⇒ ⊢ (𝜑 → ((((𝑋↑2) + ((𝑀 + 𝐵) / 2)) + ((((𝑀 / 2) · 𝑋) − (𝐶 / 4)) / 𝑆)) = 0 ↔ (𝑋 = (-𝑆 + 𝐼) ∨ 𝑋 = (-𝑆 − 𝐼)))) | ||
Theorem | dquartlem2 25424 | Lemma for dquart 25425. (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 25425 | Solve a depressed quartic equation. To eliminate 𝑆, which is the square root of a solution 𝑀 to the resolvent cubic equation, apply cubic 25421 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 25426 | Closure lemmas for quart 25433. (Contributed by Mario Carneiro, 7-May-2015.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝑃 = (𝐵 − ((3 / 8) · (𝐴↑2)))) & ⊢ (𝜑 → 𝑄 = ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))) & ⊢ (𝜑 → 𝑅 = ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))) ⇒ ⊢ (𝜑 → (𝑃 ∈ ℂ ∧ 𝑄 ∈ ℂ ∧ 𝑅 ∈ ℂ)) | ||
Theorem | quart1lem 25427 | Lemma for quart1 25428. (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 25428 | 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 25429 | Lemma for quart 25433. (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 25430 | Closure lemmas for quart 25433. (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 25431 | Closure lemmas for quart 25433. (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 25432 | Closure lemmas for quart 25433. (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 25433 | 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 32407) 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 25434 | The arcsine function. |
class arcsin | ||
Syntax | cacos 25435 | The arccosine function. |
class arccos | ||
Syntax | catan 25436 | The arctangent function. |
class arctan | ||
Definition | df-asin 25437 | 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 25438 | Define the arccosine function. See also remarks for df-asin 25437. 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 25439 | Define the arctangent function. See also remarks for df-asin 25437. 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 25440 | The argument to the logarithm in df-asin 25437 is always nonzero. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ ℂ → ((i · 𝐴) + (√‘(1 − (𝐴↑2)))) ≠ 0) | ||
Theorem | asinlem2 25441 | The argument to the logarithm in df-asin 25437 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 25442 | Lemma for asinlem3 25443. (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (ℑ‘𝐴) ≤ 0) → 0 ≤ (ℜ‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) | ||
Theorem | asinlem3 25443 | The argument to the logarithm in df-asin 25437 has nonnegative real part. (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ (𝐴 ∈ ℂ → 0 ≤ (ℜ‘((i · 𝐴) + (√‘(1 − (𝐴↑2)))))) | ||
Theorem | asinf 25444 | Domain and range of the arcsin function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ arcsin:ℂ⟶ℂ | ||
Theorem | asincl 25445 | Closure for the arcsin function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ ℂ → (arcsin‘𝐴) ∈ ℂ) | ||
Theorem | acosf 25446 | Domain and range of the arccos function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ arccos:ℂ⟶ℂ | ||
Theorem | acoscl 25447 | Closure for the arccos function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ ℂ → (arccos‘𝐴) ∈ ℂ) | ||
Theorem | atandm 25448 | 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 25449 | This form of atandm 25448 is a bit more useful for showing that the logarithms in df-atan 25439 are well-defined. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ dom arctan ↔ (𝐴 ∈ ℂ ∧ (1 − (i · 𝐴)) ≠ 0 ∧ (1 + (i · 𝐴)) ≠ 0)) | ||
Theorem | atandm3 25450 | A compact form of atandm 25448. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ dom arctan ↔ (𝐴 ∈ ℂ ∧ (𝐴↑2) ≠ -1)) | ||
Theorem | atandm4 25451 | A compact form of atandm 25448. (Contributed by Mario Carneiro, 3-Apr-2015.) |
⊢ (𝐴 ∈ dom arctan ↔ (𝐴 ∈ ℂ ∧ (1 + (𝐴↑2)) ≠ 0)) | ||
Theorem | atanf 25452 | Domain and range of the arctan function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ arctan:(ℂ ∖ {-i, i})⟶ℂ | ||
Theorem | atancl 25453 | Closure for the arctan function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ dom arctan → (arctan‘𝐴) ∈ ℂ) | ||
Theorem | asinval 25454 | Value of the arcsin function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ ℂ → (arcsin‘𝐴) = (-i · (log‘((i · 𝐴) + (√‘(1 − (𝐴↑2))))))) | ||
Theorem | acosval 25455 | Value of the arccos function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ ℂ → (arccos‘𝐴) = ((π / 2) − (arcsin‘𝐴))) | ||
Theorem | atanval 25456 | 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 25457 | A real number is in the domain of the arctangent function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ ℝ → 𝐴 ∈ dom arctan) | ||
Theorem | asinneg 25458 | The arcsine function is odd. (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ (𝐴 ∈ ℂ → (arcsin‘-𝐴) = -(arcsin‘𝐴)) | ||
Theorem | acosneg 25459 | The negative symmetry relation of the arccosine. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ ℂ → (arccos‘-𝐴) = (π − (arccos‘𝐴))) | ||
Theorem | efiasin 25460 | The exponential of the arcsine function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ ℂ → (exp‘(i · (arcsin‘𝐴))) = ((i · 𝐴) + (√‘(1 − (𝐴↑2))))) | ||
Theorem | sinasin 25461 | 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 25464 is only true under limited circumstances. (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ (𝐴 ∈ ℂ → (sin‘(arcsin‘𝐴)) = 𝐴) | ||
Theorem | cosacos 25462 | The arccosine function is an inverse to cos. (Contributed by Mario Carneiro, 1-Apr-2015.) |
⊢ (𝐴 ∈ ℂ → (cos‘(arccos‘𝐴)) = 𝐴) | ||
Theorem | asinsinlem 25463 | Lemma for asinsin 25464. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → 0 < (ℜ‘(exp‘(i · 𝐴)))) | ||
Theorem | asinsin 25464 | The arcsine function composed with sin is equal to the identity. This plus sinasin 25461 allow us 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 25468). (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (arcsin‘(sin‘𝐴)) = 𝐴) | ||
Theorem | acoscos 25465 | The arccosine function is an inverse to cos. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (0(,)π)) → (arccos‘(cos‘𝐴)) = 𝐴) | ||
Theorem | asin1 25466 | The arcsine of 1 is π / 2. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (arcsin‘1) = (π / 2) | ||
Theorem | acos1 25467 | The arcsine of 1 is π / 2. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (arccos‘1) = 0 | ||
Theorem | reasinsin 25468 | The arcsine function composed with sin is equal to the identity. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ (-(π / 2)[,](π / 2)) → (arcsin‘(sin‘𝐴)) = 𝐴) | ||
Theorem | asinsinb 25469 | Relationship between sine and arcsine. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (ℜ‘𝐵) ∈ (-(π / 2)(,)(π / 2))) → ((arcsin‘𝐴) = 𝐵 ↔ (sin‘𝐵) = 𝐴)) | ||
Theorem | acoscosb 25470 | Relationship between sine and arcsine. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (ℜ‘𝐵) ∈ (0(,)π)) → ((arccos‘𝐴) = 𝐵 ↔ (cos‘𝐵) = 𝐴)) | ||
Theorem | asinbnd 25471 | The arcsine function has range within a vertical strip of the complex plane with real part between -π / 2 and π / 2. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ ℂ → (ℜ‘(arcsin‘𝐴)) ∈ (-(π / 2)[,](π / 2))) | ||
Theorem | acosbnd 25472 | The arccosine function has range within a vertical strip of the complex plane with real part between 0 and π. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ ℂ → (ℜ‘(arccos‘𝐴)) ∈ (0[,]π)) | ||
Theorem | asinrebnd 25473 | Bounds on the arcsine function. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ (-1[,]1) → (arcsin‘𝐴) ∈ (-(π / 2)[,](π / 2))) | ||
Theorem | asinrecl 25474 | The arcsine function is real in its principal domain. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ (-1[,]1) → (arcsin‘𝐴) ∈ ℝ) | ||
Theorem | acosrecl 25475 | The arccosine function is real in its principal domain. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ (-1[,]1) → (arccos‘𝐴) ∈ ℝ) | ||
Theorem | cosasin 25476 | The cosine of the arcsine of 𝐴 is √(1 − 𝐴↑2). (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ ℂ → (cos‘(arcsin‘𝐴)) = (√‘(1 − (𝐴↑2)))) | ||
Theorem | sinacos 25477 | The sine of the arccosine of 𝐴 is √(1 − 𝐴↑2). (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ ℂ → (sin‘(arccos‘𝐴)) = (√‘(1 − (𝐴↑2)))) | ||
Theorem | atandmneg 25478 | The domain of the arctangent function is closed under negatives. (Contributed by Mario Carneiro, 3-Apr-2015.) |
⊢ (𝐴 ∈ dom arctan → -𝐴 ∈ dom arctan) | ||
Theorem | atanneg 25479 | The arctangent function is odd. (Contributed by Mario Carneiro, 3-Apr-2015.) |
⊢ (𝐴 ∈ dom arctan → (arctan‘-𝐴) = -(arctan‘𝐴)) | ||
Theorem | atan0 25480 | The arctangent of zero is zero. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (arctan‘0) = 0 | ||
Theorem | atandmcj 25481 | The arctangent function distributes under conjugation. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ dom arctan → (∗‘𝐴) ∈ dom arctan) | ||
Theorem | atancj 25482 | The arctangent function distributes under conjugation. (The condition that ℜ(𝐴) ≠ 0 is necessary because the branch cuts are chosen so that the negative imaginary line "agrees with" neighboring values with negative real part, while the positive imaginary line agrees with values with positive real part. This makes atanneg 25479 true unconditionally but messes up conjugation symmetry, and it is impossible to have both in a single-valued function. The claim is true on the imaginary line between -1 and 1, though.) (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ≠ 0) → (𝐴 ∈ dom arctan ∧ (∗‘(arctan‘𝐴)) = (arctan‘(∗‘𝐴)))) | ||
Theorem | atanrecl 25483 | The arctangent function is real for all real inputs. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ (𝐴 ∈ ℝ → (arctan‘𝐴) ∈ ℝ) | ||
Theorem | efiatan 25484 | Value of the exponential of an artcangent. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ dom arctan → (exp‘(i · (arctan‘𝐴))) = ((√‘(1 + (i · 𝐴))) / (√‘(1 − (i · 𝐴))))) | ||
Theorem | atanlogaddlem 25485 | Lemma for atanlogadd 25486. (Contributed by Mario Carneiro, 3-Apr-2015.) |
⊢ ((𝐴 ∈ dom arctan ∧ 0 ≤ (ℜ‘𝐴)) → ((log‘(1 + (i · 𝐴))) + (log‘(1 − (i · 𝐴)))) ∈ ran log) | ||
Theorem | atanlogadd 25486 | The rule √(𝑧𝑤) = (√𝑧)(√𝑤) is not always true on the complex numbers, but it is true when the arguments of 𝑧 and 𝑤 sum to within the interval (-π, π], so there are some cases such as this one with 𝑧 = 1 + i𝐴 and 𝑤 = 1 − i𝐴 which are true unconditionally. This result can also be stated as "√(1 + 𝑧) + √(1 − 𝑧) is analytic". (Contributed by Mario Carneiro, 3-Apr-2015.) |
⊢ (𝐴 ∈ dom arctan → ((log‘(1 + (i · 𝐴))) + (log‘(1 − (i · 𝐴)))) ∈ ran log) | ||
Theorem | atanlogsublem 25487 | Lemma for atanlogsub 25488. (Contributed by Mario Carneiro, 4-Apr-2015.) |
⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i · 𝐴))))) ∈ (-π(,)π)) | ||
Theorem | atanlogsub 25488 | A variation on atanlogadd 25486, to show that √(1 + i𝑧) / √(1 − i𝑧) = √((1 + i𝑧) / (1 − i𝑧)) under more limited conditions. (Contributed by Mario Carneiro, 4-Apr-2015.) |
⊢ ((𝐴 ∈ dom arctan ∧ (ℜ‘𝐴) ≠ 0) → ((log‘(1 + (i · 𝐴))) − (log‘(1 − (i · 𝐴)))) ∈ ran log) | ||
Theorem | efiatan2 25489 | Value of the exponential of an artcangent. (Contributed by Mario Carneiro, 3-Apr-2015.) |
⊢ (𝐴 ∈ dom arctan → (exp‘(i · (arctan‘𝐴))) = ((1 + (i · 𝐴)) / (√‘(1 + (𝐴↑2))))) | ||
Theorem | 2efiatan 25490 | Value of the exponential of an artcangent. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ dom arctan → (exp‘(2 · (i · (arctan‘𝐴)))) = (((2 · i) / (𝐴 + i)) − 1)) | ||
Theorem | tanatan 25491 | The arctangent function is an inverse to tan. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (𝐴 ∈ dom arctan → (tan‘(arctan‘𝐴)) = 𝐴) | ||
Theorem | atandmtan 25492 | The tangent function has range contained in the domain of the arctangent. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) ∈ dom arctan) | ||
Theorem | cosatan 25493 | The cosine of an arctangent. (Contributed by Mario Carneiro, 3-Apr-2015.) |
⊢ (𝐴 ∈ dom arctan → (cos‘(arctan‘𝐴)) = (1 / (√‘(1 + (𝐴↑2))))) | ||
Theorem | cosatanne0 25494 | The arctangent function has range contained in the domain of the tangent. (Contributed by Mario Carneiro, 3-Apr-2015.) |
⊢ (𝐴 ∈ dom arctan → (cos‘(arctan‘𝐴)) ≠ 0) | ||
Theorem | atantan 25495 | The arctangent function is an inverse to tan. (Contributed by Mario Carneiro, 5-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (arctan‘(tan‘𝐴)) = 𝐴) | ||
Theorem | atantanb 25496 | Relationship between tangent and arctangent. (Contributed by Mario Carneiro, 5-Apr-2015.) |
⊢ ((𝐴 ∈ dom arctan ∧ 𝐵 ∈ ℂ ∧ (ℜ‘𝐵) ∈ (-(π / 2)(,)(π / 2))) → ((arctan‘𝐴) = 𝐵 ↔ (tan‘𝐵) = 𝐴)) | ||
Theorem | atanbndlem 25497 | Lemma for atanbnd 25498. (Contributed by Mario Carneiro, 5-Apr-2015.) |
⊢ (𝐴 ∈ ℝ+ → (arctan‘𝐴) ∈ (-(π / 2)(,)(π / 2))) | ||
Theorem | atanbnd 25498 | The arctangent function is bounded by π / 2 on the reals. (Contributed by Mario Carneiro, 5-Apr-2015.) |
⊢ (𝐴 ∈ ℝ → (arctan‘𝐴) ∈ (-(π / 2)(,)(π / 2))) | ||
Theorem | atanord 25499 | The arctangent function is strictly increasing. (Contributed by Mario Carneiro, 5-Apr-2015.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ (arctan‘𝐴) < (arctan‘𝐵))) | ||
Theorem | atan1 25500 | The arctangent of 1 is π / 4. (Contributed by Mario Carneiro, 2-Apr-2015.) |
⊢ (arctan‘1) = (π / 4) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |