P. 239 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 23801-23900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lawcos 23801*	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 F is the signed angle construct (as used in ang180 23799), X is the distance of line segment BC, Y is the distance of line segment AC, Z is the distance of line segment AB, and O 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 23800 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 14256). The Pythagorean theorem pythag 23802 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.)
|- F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )   &    |- X = ( abs ` ( B - C ) )   &    |- Y = ( abs ` ( A - C ) )   &    |- Z = ( abs ` ( A - B ) )   &    |- O = ( ( B - C ) F ( A - C ) )   =>    |- ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) ) -> ( Z ^ 2 ) = ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) - ( 2 x. ( ( X x. Y ) x. ( cos ` O ) ) ) ) )
Theorem	pythag 23802*	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 F is the signed angle construct (as used in ang180 23799), X is the distance of line segment BC, Y is the distance of line segment AC, Z is the distance of line segment AB (the hypotenuse), and O is the signed right angle m/_ BCA. We use the law of cosines lawcos 23801 to prove this, along with simple trigonometry facts like coshalfpi 23480 and cosneg 14256. (Contributed by David A. Wheeler, 13-Jun-2015.)
|- F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )   &    |- X = ( abs ` ( B - C ) )   &    |- Y = ( abs ` ( A - C ) )   &    |- Z = ( abs ` ( A - B ) )   &    |- O = ( ( B - C ) F ( A - C ) )   =>    |- ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C ) /\ O e. { ( pi / 2 ) , -u ( pi / 2 ) } ) -> ( Z ^ 2 ) = ( ( X ^ 2 ) + ( Y ^ 2 ) ) )
Theorem	isosctrlem1 23803	Lemma for isosctr 23806. (Contributed by Saveliy Skresanov, 30-Dec-2016.)
|- ( ( A e. CC /\ ( abs ` A ) = 1 /\ -. 1 = A ) -> ( Im ` ( log ` ( 1 - A ) ) ) =/= pi )
Theorem	isosctrlem2 23804	Lemma for isosctr 23806. 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.)
|- ( ( A e. CC /\ ( abs ` A ) = 1 /\ -. 1 = A ) -> ( Im ` ( log ` ( 1 - A ) ) ) = ( Im ` ( log ` ( -u A / ( 1 - A ) ) ) ) )
Theorem	isosctrlem3 23805*	Lemma for isosctr 23806. Corresponds to the case where one vertex is at 0. (Contributed by Saveliy Skresanov, 1-Jan-2017.)
|- F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )   =>    |- ( ( ( A e. CC /\ B e. CC ) /\ ( A =/= 0 /\ B =/= 0 /\ A =/= B ) /\ ( abs ` A ) = ( abs ` B ) ) -> ( -u A F ( B - A ) ) = ( ( A - B ) F -u B ) )
Theorem	isosctr 23806*	Isosceles triangle theorem. This is Metamath 100 proof #65. (Contributed by Saveliy Skresanov, 1-Jan-2017.)
|- F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )   =>    |- ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= C /\ B =/= C /\ A =/= B ) /\ ( abs ` ( A - C ) ) = ( abs ` ( B - C ) ) ) -> ( ( C - A ) F ( B - A ) ) = ( ( A - B ) F ( C - B ) ) )
Theorem	ssscongptld 23807*	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 23801 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.)
|- F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )   &    |- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   &    |- ( ph -> E e. CC )   &    |- ( ph -> G e. CC )   &    |- ( ph -> A =/= B )   &    |- ( ph -> B =/= C )   &    |- ( ph -> D =/= E )   &    |- ( ph -> E =/= G )   &    |- ( ph -> ( abs ` ( A - B ) ) = ( abs ` ( D - E ) ) )   &    |- ( ph -> ( abs ` ( B - C ) ) = ( abs ` ( E - G ) ) )   &    |- ( ph -> ( abs ` ( C - A ) ) = ( abs ` ( G - D ) ) )   =>    |- ( ph -> ( cos ` ( ( A - B ) F ( C - B ) ) ) = ( cos ` ( ( D - E ) F ( G - E ) ) ) )
Theorem	affineequiv 23808	Equivalence between two ways of expressing B as an affine combination of A and C. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   =>    |- ( ph -> ( B = ( ( D x. A ) + ( ( 1 - D ) x. C ) ) <-> ( C - B ) = ( D x. ( C - A ) ) ) )
Theorem	affineequiv2 23809	Equivalence between two ways of expressing B as an affine combination of A and C. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   =>    |- ( ph -> ( B = ( ( D x. A ) + ( ( 1 - D ) x. C ) ) <-> ( B - A ) = ( ( 1 - D ) x. ( C - A ) ) ) )
Theorem	angpieqvdlem 23810	Equivalence used in the proof of angpieqvd 23813. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> A =/= B )   &    |- ( ph -> A =/= C )   =>    |- ( ph -> ( -u ( ( C - B ) / ( A - B ) ) e. RR+ <-> ( ( C - B ) / ( C - A ) ) e. ( 0 (,) 1 ) ) )
Theorem	angpieqvdlem2 23811*	Equivalence used in angpieqvd 23813. (Contributed by David Moews, 28-Feb-2017.)
|- F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )   &    |- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> A =/= B )   &    |- ( ph -> B =/= C )   =>    |- ( ph -> ( -u ( ( C - B ) / ( A - B ) ) e. RR+ <-> ( ( A - B ) F ( C - B ) ) = pi ) )
Theorem	angpined 23812*	If the angle at ABC is pi, then A is not equal to C. (Contributed by David Moews, 28-Feb-2017.)
|- F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )   &    |- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> A =/= B )   &    |- ( ph -> B =/= C )   =>    |- ( ph -> ( ( ( A - B ) F ( C - B ) ) = pi -> A =/= C ) )
Theorem	angpieqvd 23813*	The angle ABC is pi 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.)
|- F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )   &    |- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> A =/= B )   &    |- ( ph -> B =/= C )   =>    |- ( ph -> ( ( ( A - B ) F ( C - B ) ) = pi <-> E. w e. ( 0 (,) 1 ) B = ( ( w x. A ) + ( ( 1 - w ) x. C ) ) ) )
Theorem	chordthmlem 23814*	If M is the midpoint of AB and AQ = BQ, then QMB is a right angle. The proof uses ssscongptld 23807 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.)
|- F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )   &    |- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> Q e. CC )   &    |- ( ph -> M = ( ( A + B ) / 2 ) )   &    |- ( ph -> ( abs ` ( A - Q ) ) = ( abs ` ( B - Q ) ) )   &    |- ( ph -> A =/= B )   &    |- ( ph -> Q =/= M )   =>    |- ( ph -> ( ( Q - M ) F ( B - M ) ) e. { ( pi / 2 ) , -u ( pi / 2 ) } )
Theorem	chordthmlem2 23815*	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 23814, where P = B, and using angrtmuld 23793 to observe that QMP is right iff QMB is. (Contributed by David Moews, 28-Feb-2017.)
|- F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )   &    |- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> Q e. CC )   &    |- ( ph -> X e. RR )   &    |- ( ph -> M = ( ( A + B ) / 2 ) )   &    |- ( ph -> P = ( ( X x. A ) + ( ( 1 - X ) x. B ) ) )   &    |- ( ph -> ( abs ` ( A - Q ) ) = ( abs ` ( B - Q ) ) )   &    |- ( ph -> P =/= M )   &    |- ( ph -> Q =/= M )   =>    |- ( ph -> ( ( Q - M ) F ( P - M ) ) e. { ( pi / 2 ) , -u ( pi / 2 ) } )
Theorem	chordthmlem3 23816	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 23815 and the Pythagorean theorem (pythag 23802) 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.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> Q e. CC )   &    |- ( ph -> X e. RR )   &    |- ( ph -> M = ( ( A + B ) / 2 ) )   &    |- ( ph -> P = ( ( X x. A ) + ( ( 1 - X ) x. B ) ) )   &    |- ( ph -> ( abs ` ( A - Q ) ) = ( abs ` ( B - Q ) ) )   =>    |- ( ph -> ( ( abs ` ( P - Q ) ) ^ 2 ) = ( ( ( abs ` ( Q - M ) ) ^ 2 ) + ( ( abs ` ( P - M ) ) ^ 2 ) ) )
Theorem	chordthmlem4 23817	If P is on the segment AB and M is the midpoint of AB, then PA x. PB = BM 2 - PM 2 . If all lengths are reexpressed as fractions of AB, this reduces to the identity X x. ( 1 - X ) = ( 1 / 2 ) 2 - ( ( 1 / 2 ) - X ) 2 . (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> X e. ( 0 [,] 1 ) )   &    |- ( ph -> M = ( ( A + B ) / 2 ) )   &    |- ( ph -> P = ( ( X x. A ) + ( ( 1 - X ) x. B ) ) )   =>    |- ( ph -> ( ( abs ` ( P - A ) ) x. ( abs ` ( P - B ) ) ) = ( ( ( abs ` ( B - M ) ) ^ 2 ) - ( ( abs ` ( P - M ) ) ^ 2 ) ) )
Theorem	chordthmlem5 23818	If P is on the segment AB and AQ = BQ, then PA x. PB = BQ 2 - PQ 2 . This follows from two uses of chordthmlem3 23816 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 x. PB by chordthmlem4 23817. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> Q e. CC )   &    |- ( ph -> X e. ( 0 [,] 1 ) )   &    |- ( ph -> P = ( ( X x. A ) + ( ( 1 - X ) x. B ) ) )   &    |- ( ph -> ( abs ` ( A - Q ) ) = ( abs ` ( B - Q ) ) )   =>    |- ( ph -> ( ( abs ` ( P - A ) ) x. ( abs ` ( P - B ) ) ) = ( ( ( abs ` ( B - Q ) ) ^ 2 ) - ( ( abs ` ( P - Q ) ) ^ 2 ) ) )
Theorem	chordthm 23819*	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 x. PB and PC x. 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 pi. The result is proven by using chordthmlem5 23818 twice to show that PA x. PB and PC x. 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.)
|- F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )   &    |- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   &    |- ( ph -> P e. CC )   &    |- ( ph -> A =/= P )   &    |- ( ph -> B =/= P )   &    |- ( ph -> C =/= P )   &    |- ( ph -> D =/= P )   &    |- ( ph -> ( ( A - P ) F ( B - P ) ) = pi )   &    |- ( ph -> ( ( C - P ) F ( D - P ) ) = pi )   &    |- ( ph -> Q e. CC )   &    |- ( ph -> ( abs ` ( A - Q ) ) = ( abs ` ( B - Q ) ) )   &    |- ( ph -> ( abs ` ( A - Q ) ) = ( abs ` ( C - Q ) ) )   &    |- ( ph -> ( abs ` ( A - Q ) ) = ( abs ` ( D - Q ) ) )   =>    |- ( ph -> ( ( abs ` ( P - A ) ) x. ( abs ` ( P - B ) ) ) = ( ( abs ` ( P - C ) ) x. ( abs ` ( P - D ) ) ) )
Theorem	heron 23820*	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 ) x. X x. Y x. abs ( sin O ), is equal to the square root of S x. ( S - X ) x. ( S - Y ) x. ( S - Z ), where S = ( X + Y + Z ) / 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.)
|- F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )   &    |- X = ( abs ` ( B - C ) )   &    |- Y = ( abs ` ( A - C ) )   &    |- Z = ( abs ` ( A - B ) )   &    |- O = ( ( B - C ) F ( A - C ) )   &    |- S = ( ( ( X + Y ) + Z ) / 2 )   &    |- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> A =/= C )   &    |- ( ph -> B =/= C )   =>    |- ( ph -> ( ( ( 1 / 2 ) x. ( X x. Y ) ) x. ( abs ` ( sin ` O ) ) ) = ( sqr ` ( ( S x. ( S - X ) ) x. ( ( S - Y ) x. ( S - Z ) ) ) ) )
14.3.7  Solutions of quadratic, cubic, and quartic equations
Theorem	quad2 23821	The quadratic equation, without specifying the particular branch D to the square root. (Contributed by Mario Carneiro, 23-Apr-2015.)
|- ( ph -> A e. CC )   &    |- ( ph -> A =/= 0 )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> X e. CC )   &    |- ( ph -> D e. CC )   &    |- ( ph -> ( D ^ 2 ) = ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) )   =>    |- ( ph -> ( ( ( A x. ( X ^ 2 ) ) + ( ( B x. X ) + C ) ) = 0 <-> ( X = ( ( -u B + D ) / ( 2 x. A ) ) \/ X = ( ( -u B - D ) / ( 2 x. A ) ) ) ) )
Theorem	quad 23822	The quadratic equation. (Contributed by Mario Carneiro, 23-Apr-2015.)
|- ( ph -> A e. CC )   &    |- ( ph -> A =/= 0 )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> X e. CC )   &    |- ( ph -> D = ( ( B ^ 2 ) - ( 4 x. ( A x. C ) ) ) )   =>    |- ( ph -> ( ( ( A x. ( X ^ 2 ) ) + ( ( B x. X ) + C ) ) = 0 <-> ( X = ( ( -u B + ( sqr ` D ) ) / ( 2 x. A ) ) \/ X = ( ( -u B - ( sqr ` D ) ) / ( 2 x. A ) ) ) ) )
Theorem	1cubrlem 23823	The cube roots of unity. (Contributed by Mario Carneiro, 23-Apr-2015.)
|- ( ( -u 1 ^c ( 2 / 3 ) ) = ( ( -u 1 + ( _i x. ( sqr ` 3 ) ) ) / 2 ) /\ ( ( -u 1 ^c ( 2 / 3 ) ) ^ 2 ) = ( ( -u 1 - ( _i x. ( sqr ` 3 ) ) ) / 2 ) )
Theorem	1cubr 23824	The cube roots of unity. (Contributed by Mario Carneiro, 23-Apr-2015.)
|- R = { 1 , ( ( -u 1 + ( _i x. ( sqr ` 3 ) ) ) / 2 ) , ( ( -u 1 - ( _i x. ( sqr ` 3 ) ) ) / 2 ) }   =>    |- ( A e. R <-> ( A e. CC /\ ( A ^ 3 ) = 1 ) )
Theorem	dcubic1lem 23825	Lemma for dcubic1 23827 and dcubic2 23826: simplify the cubic equation under the substitution X = U - M / U. (Contributed by Mario Carneiro, 26-Apr-2015.)
|- ( ph -> P e. CC )   &    |- ( ph -> Q e. CC )   &    |- ( ph -> X e. CC )   &    |- ( ph -> T e. CC )   &    |- ( ph -> ( T ^ 3 ) = ( G - N ) )   &    |- ( ph -> G e. CC )   &    |- ( ph -> ( G ^ 2 ) = ( ( N ^ 2 ) + ( M ^ 3 ) ) )   &    |- ( ph -> M = ( P / 3 ) )   &    |- ( ph -> N = ( Q / 2 ) )   &    |- ( ph -> T =/= 0 )   &    |- ( ph -> U e. CC )   &    |- ( ph -> U =/= 0 )   &    |- ( ph -> X = ( U - ( M / U ) ) )   =>    |- ( ph -> ( ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 <-> ( ( ( U ^ 3 ) ^ 2 ) + ( ( Q x. ( U ^ 3 ) ) - ( M ^ 3 ) ) ) = 0 ) )
Theorem	dcubic2 23826*	Reverse direction of dcubic 23828. Given a solution U to the "substitution" quadratic equation X = U - M / U, show that X is in the desired form. (Contributed by Mario Carneiro, 25-Apr-2015.)
|- ( ph -> P e. CC )   &    |- ( ph -> Q e. CC )   &    |- ( ph -> X e. CC )   &    |- ( ph -> T e. CC )   &    |- ( ph -> ( T ^ 3 ) = ( G - N ) )   &    |- ( ph -> G e. CC )   &    |- ( ph -> ( G ^ 2 ) = ( ( N ^ 2 ) + ( M ^ 3 ) ) )   &    |- ( ph -> M = ( P / 3 ) )   &    |- ( ph -> N = ( Q / 2 ) )   &    |- ( ph -> T =/= 0 )   &    |- ( ph -> U e. CC )   &    |- ( ph -> U =/= 0 )   &    |- ( ph -> X = ( U - ( M / U ) ) )   &    |- ( ph -> ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 )   =>    |- ( ph -> E. r e. CC ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) )
Theorem	dcubic1 23827	Forward direction of dcubic 23828: the claimed formula produces solutions to the cubic equation. (Contributed by Mario Carneiro, 25-Apr-2015.)
|- ( ph -> P e. CC )   &    |- ( ph -> Q e. CC )   &    |- ( ph -> X e. CC )   &    |- ( ph -> T e. CC )   &    |- ( ph -> ( T ^ 3 ) = ( G - N ) )   &    |- ( ph -> G e. CC )   &    |- ( ph -> ( G ^ 2 ) = ( ( N ^ 2 ) + ( M ^ 3 ) ) )   &    |- ( ph -> M = ( P / 3 ) )   &    |- ( ph -> N = ( Q / 2 ) )   &    |- ( ph -> T =/= 0 )   &    |- ( ph -> X = ( T - ( M / T ) ) )   =>    |- ( ph -> ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 )
Theorem	dcubic 23828*	Solutions to the depressed cubic, a special case of cubic 23831. (The definitions of M , N , G , T here differ from mcubic 23829 by scale factors of -u 9, 5 4, 5 4 and -u 2 7 respectively, to simplify the algebra and presentation.) (Contributed by Mario Carneiro, 26-Apr-2015.)
|- ( ph -> P e. CC )   &    |- ( ph -> Q e. CC )   &    |- ( ph -> X e. CC )   &    |- ( ph -> T e. CC )   &    |- ( ph -> ( T ^ 3 ) = ( G - N ) )   &    |- ( ph -> G e. CC )   &    |- ( ph -> ( G ^ 2 ) = ( ( N ^ 2 ) + ( M ^ 3 ) ) )   &    |- ( ph -> M = ( P / 3 ) )   &    |- ( ph -> N = ( Q / 2 ) )   &    |- ( ph -> T =/= 0 )   =>    |- ( ph -> ( ( ( X ^ 3 ) + ( ( P x. X ) + Q ) ) = 0 <-> E. r e. CC ( ( r ^ 3 ) = 1 /\ X = ( ( r x. T ) - ( M / ( r x. T ) ) ) ) ) )
Theorem	mcubic 23829*	Solutions to a monic cubic equation, a special case of cubic 23831. (Contributed by Mario Carneiro, 24-Apr-2015.)
|- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   &    |- ( ph -> X e. CC )   &    |- ( ph -> T e. CC )   &    |- ( ph -> ( T ^ 3 ) = ( ( N + G ) / 2 ) )   &    |- ( ph -> G e. CC )   &    |- ( ph -> ( G ^ 2 ) = ( ( N ^ 2 ) - ( 4 x. ( M ^ 3 ) ) ) )   &    |- ( ph -> M = ( ( B ^ 2 ) - ( 3 x. C ) ) )   &    |- ( ph -> N = ( ( ( 2 x. ( B ^ 3 ) ) - ( 9 x. ( B x. C ) ) ) + (; 2 7 x. D ) ) )   &    |- ( ph -> T =/= 0 )   =>    |- ( ph -> ( ( ( ( X ^ 3 ) + ( B x. ( X ^ 2 ) ) ) + ( ( C x. X ) + D ) ) = 0 <-> E. r e. CC ( ( r ^ 3 ) = 1 /\ X = -u ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / 3 ) ) ) )
Theorem	cubic2 23830*	The solution to the general cubic equation, for arbitrary choices G and T of the square and cube roots. (Contributed by Mario Carneiro, 23-Apr-2015.)
|- ( ph -> A e. CC )   &    |- ( ph -> A =/= 0 )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   &    |- ( ph -> X e. CC )   &    |- ( ph -> T e. CC )   &    |- ( ph -> ( T ^ 3 ) = ( ( N + G ) / 2 ) )   &    |- ( ph -> G e. CC )   &    |- ( ph -> ( G ^ 2 ) = ( ( N ^ 2 ) - ( 4 x. ( M ^ 3 ) ) ) )   &    |- ( ph -> M = ( ( B ^ 2 ) - ( 3 x. ( A x. C ) ) ) )   &    |- ( ph -> N = ( ( ( 2 x. ( B ^ 3 ) ) - ( ( 9 x. A ) x. ( B x. C ) ) ) + (; 2 7 x. ( ( A ^ 2 ) x. D ) ) ) )   &    |- ( ph -> T =/= 0 )   =>    |- ( ph -> ( ( ( ( A x. ( X ^ 3 ) ) + ( B x. ( X ^ 2 ) ) ) + ( ( C x. X ) + D ) ) = 0 <-> E. r e. CC ( ( r ^ 3 ) = 1 /\ X = -u ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / ( 3 x. A ) ) ) ) )
Theorem	cubic 23831*	The cubic equation, which gives the roots of an arbitrary (nondegenerate) cubic function. Use rextp 4040 to convert the existential quantifier to a triple disjunction. This is Metamath 100 proof #37. (Contributed by Mario Carneiro, 26-Apr-2015.)
|- R = { 1 , ( ( -u 1 + ( _i x. ( sqr ` 3 ) ) ) / 2 ) , ( ( -u 1 - ( _i x. ( sqr ` 3 ) ) ) / 2 ) }   &    |- ( ph -> A e. CC )   &    |- ( ph -> A =/= 0 )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   &    |- ( ph -> X e. CC )   &    |- ( ph -> T = ( ( ( N + ( sqr ` G ) ) / 2 ) ^c ( 1 / 3 ) ) )   &    |- ( ph -> G = ( ( N ^ 2 ) - ( 4 x. ( M ^ 3 ) ) ) )   &    |- ( ph -> M = ( ( B ^ 2 ) - ( 3 x. ( A x. C ) ) ) )   &    |- ( ph -> N = ( ( ( 2 x. ( B ^ 3 ) ) - ( ( 9 x. A ) x. ( B x. C ) ) ) + (; 2 7 x. ( ( A ^ 2 ) x. D ) ) ) )   &    |- ( ph -> M =/= 0 )   =>    |- ( ph -> ( ( ( ( A x. ( X ^ 3 ) ) + ( B x. ( X ^ 2 ) ) ) + ( ( C x. X ) + D ) ) = 0 <-> E. r e. R X = -u ( ( ( B + ( r x. T ) ) + ( M / ( r x. T ) ) ) / ( 3 x. A ) ) ) )
Theorem	binom4 23832	Work out a quartic binomial. (You would think that by this point it would be faster to use binom 13943, 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.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) ^ 4 ) = ( ( ( A ^ 4 ) + ( 4 x. ( ( A ^ 3 ) x. B ) ) ) + ( ( 6 x. ( ( A ^ 2 ) x. ( B ^ 2 ) ) ) + ( ( 4 x. ( A x. ( B ^ 3 ) ) ) + ( B ^ 4 ) ) ) ) )
Theorem	dquartlem1 23833	Lemma for dquart 23835. (Contributed by Mario Carneiro, 6-May-2015.)
|- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> X e. CC )   &    |- ( ph -> S e. CC )   &    |- ( ph -> M = ( ( 2 x. S ) ^ 2 ) )   &    |- ( ph -> M =/= 0 )   &    |- ( ph -> I e. CC )   &    |- ( ph -> ( I ^ 2 ) = ( ( -u ( S ^ 2 ) - ( B / 2 ) ) + ( ( C / 4 ) / S ) ) )   =>    |- ( ph -> ( ( ( ( X ^ 2 ) + ( ( M + B ) / 2 ) ) + ( ( ( ( M / 2 ) x. X ) - ( C / 4 ) ) / S ) ) = 0 <-> ( X = ( -u S + I ) \/ X = ( -u S - I ) ) ) )
Theorem	dquartlem2 23834	Lemma for dquart 23835. (Contributed by Mario Carneiro, 6-May-2015.)
|- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> X e. CC )   &    |- ( ph -> S e. CC )   &    |- ( ph -> M = ( ( 2 x. S ) ^ 2 ) )   &    |- ( ph -> M =/= 0 )   &    |- ( ph -> I e. CC )   &    |- ( ph -> ( I ^ 2 ) = ( ( -u ( S ^ 2 ) - ( B / 2 ) ) + ( ( C / 4 ) / S ) ) )   &    |- ( ph -> D e. CC )   &    |- ( ph -> ( ( ( M ^ 3 ) + ( ( 2 x. B ) x. ( M ^ 2 ) ) ) + ( ( ( ( B ^ 2 ) - ( 4 x. D ) ) x. M ) + -u ( C ^ 2 ) ) ) = 0 )   =>    |- ( ph -> ( ( ( ( M + B ) / 2 ) ^ 2 ) - ( ( ( C ^ 2 ) / 4 ) / M ) ) = D )
Theorem	dquart 23835	Solve a depressed quartic equation. To eliminate S, which is the square root of a solution M to the resolvent cubic equation, apply cubic 23831 or one of its variants. (Contributed by Mario Carneiro, 6-May-2015.)
|- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> X e. CC )   &    |- ( ph -> S e. CC )   &    |- ( ph -> M = ( ( 2 x. S ) ^ 2 ) )   &    |- ( ph -> M =/= 0 )   &    |- ( ph -> I e. CC )   &    |- ( ph -> ( I ^ 2 ) = ( ( -u ( S ^ 2 ) - ( B / 2 ) ) + ( ( C / 4 ) / S ) ) )   &    |- ( ph -> D e. CC )   &    |- ( ph -> ( ( ( M ^ 3 ) + ( ( 2 x. B ) x. ( M ^ 2 ) ) ) + ( ( ( ( B ^ 2 ) - ( 4 x. D ) ) x. M ) + -u ( C ^ 2 ) ) ) = 0 )   &    |- ( ph -> J e. CC )   &    |- ( ph -> ( J ^ 2 ) = ( ( -u ( S ^ 2 ) - ( B / 2 ) ) - ( ( C / 4 ) / S ) ) )   =>    |- ( ph -> ( ( ( ( X ^ 4 ) + ( B x. ( X ^ 2 ) ) ) + ( ( C x. X ) + D ) ) = 0 <-> ( ( X = ( -u S + I ) \/ X = ( -u S - I ) ) \/ ( X = ( S + J ) \/ X = ( S - J ) ) ) ) )
Theorem	quart1cl 23836	Closure lemmas for quart 23843. (Contributed by Mario Carneiro, 7-May-2015.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   &    |- ( ph -> P = ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) )   &    |- ( ph -> Q = ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) )   &    |- ( ph -> R = ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ;; 2 5 6 ) x. ( A ^ 4 ) ) ) ) )   =>    |- ( ph -> ( P e. CC /\ Q e. CC /\ R e. CC ) )
Theorem	quart1lem 23837	Lemma for quart1 23838. (Contributed by Mario Carneiro, 6-May-2015.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   &    |- ( ph -> P = ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) )   &    |- ( ph -> Q = ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) )   &    |- ( ph -> R = ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ;; 2 5 6 ) x. ( A ^ 4 ) ) ) ) )   &    |- ( ph -> X e. CC )   &    |- ( ph -> Y = ( X + ( A / 4 ) ) )   =>    |- ( ph -> D = ( ( ( ( A ^ 4 ) / ;; 2 5 6 ) + ( P x. ( ( A / 4 ) ^ 2 ) ) ) + ( ( Q x. ( A / 4 ) ) + R ) ) )
Theorem	quart1 23838	Depress a quartic equation. (Contributed by Mario Carneiro, 6-May-2015.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   &    |- ( ph -> P = ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) )   &    |- ( ph -> Q = ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) )   &    |- ( ph -> R = ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ;; 2 5 6 ) x. ( A ^ 4 ) ) ) ) )   &    |- ( ph -> X e. CC )   &    |- ( ph -> Y = ( X + ( A / 4 ) ) )   =>    |- ( ph -> ( ( ( X ^ 4 ) + ( A x. ( X ^ 3 ) ) ) + ( ( B x. ( X ^ 2 ) ) + ( ( C x. X ) + D ) ) ) = ( ( ( Y ^ 4 ) + ( P x. ( Y ^ 2 ) ) ) + ( ( Q x. Y ) + R ) ) )
Theorem	quartlem1 23839	Lemma for quart 23843. (Contributed by Mario Carneiro, 6-May-2015.)
|- ( ph -> P e. CC )   &    |- ( ph -> Q e. CC )   &    |- ( ph -> R e. CC )   &    |- ( ph -> U = ( ( P ^ 2 ) + (; 1 2 x. R ) ) )   &    |- ( ph -> V = ( ( -u ( 2 x. ( P ^ 3 ) ) - (; 2 7 x. ( Q ^ 2 ) ) ) + (; 7 2 x. ( P x. R ) ) ) )   =>    |- ( ph -> ( U = ( ( ( 2 x. P ) ^ 2 ) - ( 3 x. ( ( P ^ 2 ) - ( 4 x. R ) ) ) ) /\ V = ( ( ( 2 x. ( ( 2 x. P ) ^ 3 ) ) - ( 9 x. ( ( 2 x. P ) x. ( ( P ^ 2 ) - ( 4 x. R ) ) ) ) ) + (; 2 7 x. -u ( Q ^ 2 ) ) ) ) )
Theorem	quartlem2 23840	Closure lemmas for quart 23843. (Contributed by Mario Carneiro, 7-May-2015.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   &    |- ( ph -> X e. CC )   &    |- ( ph -> E = -u ( A / 4 ) )   &    |- ( ph -> P = ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) )   &    |- ( ph -> Q = ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) )   &    |- ( ph -> R = ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ;; 2 5 6 ) x. ( A ^ 4 ) ) ) ) )   &    |- ( ph -> U = ( ( P ^ 2 ) + (; 1 2 x. R ) ) )   &    |- ( ph -> V = ( ( -u ( 2 x. ( P ^ 3 ) ) - (; 2 7 x. ( Q ^ 2 ) ) ) + (; 7 2 x. ( P x. R ) ) ) )   &    |- ( ph -> W = ( sqr ` ( ( V ^ 2 ) - ( 4 x. ( U ^ 3 ) ) ) ) )   =>    |- ( ph -> ( U e. CC /\ V e. CC /\ W e. CC ) )
Theorem	quartlem3 23841	Closure lemmas for quart 23843. (Contributed by Mario Carneiro, 7-May-2015.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   &    |- ( ph -> X e. CC )   &    |- ( ph -> E = -u ( A / 4 ) )   &    |- ( ph -> P = ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) )   &    |- ( ph -> Q = ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) )   &    |- ( ph -> R = ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ;; 2 5 6 ) x. ( A ^ 4 ) ) ) ) )   &    |- ( ph -> U = ( ( P ^ 2 ) + (; 1 2 x. R ) ) )   &    |- ( ph -> V = ( ( -u ( 2 x. ( P ^ 3 ) ) - (; 2 7 x. ( Q ^ 2 ) ) ) + (; 7 2 x. ( P x. R ) ) ) )   &    |- ( ph -> W = ( sqr ` ( ( V ^ 2 ) - ( 4 x. ( U ^ 3 ) ) ) ) )   &    |- ( ph -> S = ( ( sqr ` M ) / 2 ) )   &    |- ( ph -> M = -u ( ( ( ( 2 x. P ) + T ) + ( U / T ) ) / 3 ) )   &    |- ( ph -> T = ( ( ( V + W ) / 2 ) ^c ( 1 / 3 ) ) )   &    |- ( ph -> T =/= 0 )   =>    |- ( ph -> ( S e. CC /\ M e. CC /\ T e. CC ) )
Theorem	quartlem4 23842	Closure lemmas for quart 23843. (Contributed by Mario Carneiro, 7-May-2015.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   &    |- ( ph -> X e. CC )   &    |- ( ph -> E = -u ( A / 4 ) )   &    |- ( ph -> P = ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) )   &    |- ( ph -> Q = ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) )   &    |- ( ph -> R = ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ;; 2 5 6 ) x. ( A ^ 4 ) ) ) ) )   &    |- ( ph -> U = ( ( P ^ 2 ) + (; 1 2 x. R ) ) )   &    |- ( ph -> V = ( ( -u ( 2 x. ( P ^ 3 ) ) - (; 2 7 x. ( Q ^ 2 ) ) ) + (; 7 2 x. ( P x. R ) ) ) )   &    |- ( ph -> W = ( sqr ` ( ( V ^ 2 ) - ( 4 x. ( U ^ 3 ) ) ) ) )   &    |- ( ph -> S = ( ( sqr ` M ) / 2 ) )   &    |- ( ph -> M = -u ( ( ( ( 2 x. P ) + T ) + ( U / T ) ) / 3 ) )   &    |- ( ph -> T = ( ( ( V + W ) / 2 ) ^c ( 1 / 3 ) ) )   &    |- ( ph -> T =/= 0 )   &    |- ( ph -> M =/= 0 )   &    |- ( ph -> I = ( sqr ` ( ( -u ( S ^ 2 ) - ( P / 2 ) ) + ( ( Q / 4 ) / S ) ) ) )   &    |- ( ph -> J = ( sqr ` ( ( -u ( S ^ 2 ) - ( P / 2 ) ) - ( ( Q / 4 ) / S ) ) ) )   =>    |- ( ph -> ( S =/= 0 /\ I e. CC /\ J e. CC ) )
Theorem	quart 23843	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 29938) if all the substitutions are performed. This is Metamath 100 proof #46. (Contributed by Mario Carneiro, 6-May-2015.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   &    |- ( ph -> X e. CC )   &    |- ( ph -> E = -u ( A / 4 ) )   &    |- ( ph -> P = ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) )   &    |- ( ph -> Q = ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) )   &    |- ( ph -> R = ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ;; 2 5 6 ) x. ( A ^ 4 ) ) ) ) )   &    |- ( ph -> U = ( ( P ^ 2 ) + (; 1 2 x. R ) ) )   &    |- ( ph -> V = ( ( -u ( 2 x. ( P ^ 3 ) ) - (; 2 7 x. ( Q ^ 2 ) ) ) + (; 7 2 x. ( P x. R ) ) ) )   &    |- ( ph -> W = ( sqr ` ( ( V ^ 2 ) - ( 4 x. ( U ^ 3 ) ) ) ) )   &    |- ( ph -> S = ( ( sqr ` M ) / 2 ) )   &    |- ( ph -> M = -u ( ( ( ( 2 x. P ) + T ) + ( U / T ) ) / 3 ) )   &    |- ( ph -> T = ( ( ( V + W ) / 2 ) ^c ( 1 / 3 ) ) )   &    |- ( ph -> T =/= 0 )   &    |- ( ph -> M =/= 0 )   &    |- ( ph -> I = ( sqr ` ( ( -u ( S ^ 2 ) - ( P / 2 ) ) + ( ( Q / 4 ) / S ) ) ) )   &    |- ( ph -> J = ( sqr ` ( ( -u ( S ^ 2 ) - ( P / 2 ) ) - ( ( Q / 4 ) / S ) ) ) )   =>    |- ( ph -> ( ( ( ( X ^ 4 ) + ( A x. ( X ^ 3 ) ) ) + ( ( B x. ( X ^ 2 ) ) + ( ( C x. X ) + D ) ) ) = 0 <-> ( ( X = ( ( E - S ) + I ) \/ X = ( ( E - S ) - I ) ) \/ ( X = ( ( E + S ) + J ) \/ X = ( ( E + S ) - J ) ) ) ) )
14.3.8  Inverse trigonometric functions
Syntax	casin 23844	The arcsine function.
class arcsin
Syntax	cacos 23845	The arccosine function.
class arccos
Syntax	catan 23846	The arctangent function.
class arctan
Definition	df-asin 23847	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 -u 1 and 1 (at which the function is defined), and branch cuts along the real line not between -u 1 and 1, which is to say ( -oo , -u 1 ) u. ( 1 , +oo ). (Contributed by Mario Carneiro, 31-Mar-2015.)
|- arcsin = ( x e. CC |-> ( -u _i x. ( log ` ( ( _i x. x ) + ( sqr ` ( 1 - ( x ^ 2 ) ) ) ) ) ) )
Definition	df-acos 23848	Define the arccosine function. See also remarks for df-asin 23847. Since we define arccos in terms of arcsin, it shares the same branch points and cuts, namely ( -oo , -u 1 ) u. ( 1 , +oo ). (Contributed by Mario Carneiro, 31-Mar-2015.)
|- arccos = ( x e. CC |-> ( ( pi / 2 ) - (arcsin ` x ) ) )
Definition	df-atan 23849	Define the arctangent function. See also remarks for df-asin 23847. Unlike arcsin and arccos, this function is not defined everywhere, because tan ( z ) =/= pm _i for all z e. CC. For all other z, there is a formula for arctan ( z ) in terms of log, and we take that as the definition. Branch points are at pm _i; branch cuts are on the pure imaginary axis not between -u _i and _i, which is to say { z e. CC | ( _i x. z ) e. ( -oo , -u 1 ) u. ( 1 , +oo ) }. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- arctan = ( x e. ( CC \ { -u _i , _i } ) |-> ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) ) )
Theorem	asinlem 23850	The argument to the logarithm in df-asin 23847 is always nonzero. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- ( A e. CC -> ( ( _i x. A ) + ( sqr ` ( 1 - ( A ^ 2 ) ) ) ) =/= 0 )
Theorem	asinlem2 23851	The argument to the logarithm in df-asin 23847 has the property that replacing A with -u A in the expression gives the reciprocal. (Contributed by Mario Carneiro, 1-Apr-2015.)
|- ( A e. CC -> ( ( ( _i x. A ) + ( sqr ` ( 1 - ( A ^ 2 ) ) ) ) x. ( ( _i x. -u A ) + ( sqr ` ( 1 - ( -u A ^ 2 ) ) ) ) ) = 1 )
Theorem	asinlem3a 23852	Lemma for asinlem3 23853. (Contributed by Mario Carneiro, 1-Apr-2015.)
|- ( ( A e. CC /\ ( Im ` A ) <_ 0 ) -> 0 <_ ( Re ` ( ( _i x. A ) + ( sqr ` ( 1 - ( A ^ 2 ) ) ) ) ) )
Theorem	asinlem3 23853	The argument to the logarithm in df-asin 23847 has nonnegative real part. (Contributed by Mario Carneiro, 1-Apr-2015.)
|- ( A e. CC -> 0 <_ ( Re ` ( ( _i x. A ) + ( sqr ` ( 1 - ( A ^ 2 ) ) ) ) ) )
Theorem	asinf 23854	Domain and range of the arcsin function. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- arcsin : CC --> CC
Theorem	asincl 23855	Closure for the arcsin function. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- ( A e. CC -> (arcsin ` A ) e. CC )
Theorem	acosf 23856	Domain and range of the arccos function. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- arccos : CC --> CC
Theorem	acoscl 23857	Closure for the arccos function. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- ( A e. CC -> (arccos ` A ) e. CC )
Theorem	atandm 23858	Since the property is a little lengthy, we abbreviate A e. CC /\ A =/= -u _i /\ A =/= _i as A e. dom arctan. This is the necessary precondition for the definition of arctan to make sense. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- ( A e. dom arctan <-> ( A e. CC /\ A =/= -u _i /\ A =/= _i ) )
Theorem	atandm2 23859	This form of atandm 23858 is a bit more useful for showing that the logarithms in df-atan 23849 are well-defined. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- ( A e. dom arctan <-> ( A e. CC /\ ( 1 - ( _i x. A ) ) =/= 0 /\ ( 1 + ( _i x. A ) ) =/= 0 ) )
Theorem	atandm3 23860	A compact form of atandm 23858. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- ( A e. dom arctan <-> ( A e. CC /\ ( A ^ 2 ) =/= -u 1 ) )
Theorem	atandm4 23861	A compact form of atandm 23858. (Contributed by Mario Carneiro, 3-Apr-2015.)
|- ( A e. dom arctan <-> ( A e. CC /\ ( 1 + ( A ^ 2 ) ) =/= 0 ) )
Theorem	atanf 23862	Domain and range of the arctan function. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- arctan : ( CC \ { -u _i , _i } ) --> CC
Theorem	atancl 23863	Closure for the arctan function. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- ( A e. dom arctan -> (arctan ` A ) e. CC )
Theorem	asinval 23864	Value of the arcsin function. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- ( A e. CC -> (arcsin ` A ) = ( -u _i x. ( log ` ( ( _i x. A ) + ( sqr ` ( 1 - ( A ^ 2 ) ) ) ) ) ) )
Theorem	acosval 23865	Value of the arccos function. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- ( A e. CC -> (arccos ` A ) = ( ( pi / 2 ) - (arcsin ` A ) ) )
Theorem	atanval 23866	Value of the arctan function. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- ( A e. dom arctan -> (arctan ` A ) = ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) )
Theorem	atanre 23867	A real number is in the domain of the arctangent function. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- ( A e. RR -> A e. dom arctan )
Theorem	asinneg 23868	The arcsine function is odd. (Contributed by Mario Carneiro, 1-Apr-2015.)
|- ( A e. CC -> (arcsin ` -u A ) = -u (arcsin ` A ) )
Theorem	acosneg 23869	The negative symmetry relation of the arccosine. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- ( A e. CC -> (arccos ` -u A ) = ( pi - (arccos ` A ) ) )
Theorem	efiasin 23870	The exponential of the arcsine function. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- ( A e. CC -> ( exp ` ( _i x. (arcsin ` A ) ) ) = ( ( _i x. A ) + ( sqr ` ( 1 - ( A ^ 2 ) ) ) ) )
Theorem	sinasin 23871	The arcsine function is an inverse to sin. This is the main property that justifies the notation arcsin or sin ^ -u 1. Because sin is not an injection, the other converse identity asinsin 23874 is only true under limited circumstances. (Contributed by Mario Carneiro, 1-Apr-2015.)
|- ( A e. CC -> ( sin ` (arcsin ` A ) ) = A )
Theorem	cosacos 23872	The arccosine function is an inverse to cos. (Contributed by Mario Carneiro, 1-Apr-2015.)
|- ( A e. CC -> ( cos ` (arccos ` A ) ) = A )
Theorem	asinsinlem 23873	Lemma for asinsin 23874. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- ( ( A e. CC /\ ( Re ` A ) e. ( -u ( pi / 2 ) (,) ( pi / 2 ) ) ) -> 0 < ( Re ` ( exp ` ( _i x. A ) ) ) )
Theorem	asinsin 23874	The arcsine function composed with sin is equal to the identity. This plus sinasin 23871 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 A = ( pi / 2 ) - _i y for nonnegative real y and also symmetrically at A = _i y - ( pi / 2 ). In particular, when restricted to reals this identity extends to the closed interval [ -u ( pi / 2 ) , ( pi / 2 ) ], not just the open interval (see reasinsin 23878). (Contributed by Mario Carneiro, 2-Apr-2015.)
|- ( ( A e. CC /\ ( Re ` A ) e. ( -u ( pi / 2 ) (,) ( pi / 2 ) ) ) -> (arcsin ` ( sin ` A ) ) = A )
Theorem	acoscos 23875	The arccosine function is an inverse to cos. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- ( ( A e. CC /\ ( Re ` A ) e. ( 0 (,) pi ) ) -> (arccos ` ( cos ` A ) ) = A )
Theorem	asin1 23876	The arcsine of 1 is pi / 2. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- (arcsin ` 1 ) = ( pi / 2 )
Theorem	acos1 23877	The arcsine of 1 is pi / 2. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- (arccos ` 1 ) = 0
Theorem	reasinsin 23878	The arcsine function composed with sin is equal to the identity. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- ( A e. ( -u ( pi / 2 ) [,] ( pi / 2 ) ) -> (arcsin ` ( sin ` A ) ) = A )
Theorem	asinsinb 23879	Relationship between sine and arcsine. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- ( ( A e. CC /\ B e. CC /\ ( Re ` B ) e. ( -u ( pi / 2 ) (,) ( pi / 2 ) ) ) -> ( (arcsin ` A ) = B <-> ( sin ` B ) = A ) )
Theorem	acoscosb 23880	Relationship between sine and arcsine. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- ( ( A e. CC /\ B e. CC /\ ( Re ` B ) e. ( 0 (,) pi ) ) -> ( (arccos ` A ) = B <-> ( cos ` B ) = A ) )
Theorem	asinbnd 23881	The arcsine function has range within a vertical strip of the complex plane with real part between -u pi / 2 and pi / 2. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- ( A e. CC -> ( Re ` (arcsin ` A ) ) e. ( -u ( pi / 2 ) [,] ( pi / 2 ) ) )
Theorem	acosbnd 23882	The arccosine function has range within a vertical strip of the complex plane with real part between 0 and pi. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- ( A e. CC -> ( Re ` (arccos ` A ) ) e. ( 0 [,] pi ) )
Theorem	asinrebnd 23883	Bounds on the arcsine function. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- ( A e. ( -u 1 [,] 1 ) -> (arcsin ` A ) e. ( -u ( pi / 2 ) [,] ( pi / 2 ) ) )
Theorem	asinrecl 23884	The arcsine function is real in its principal domain. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- ( A e. ( -u 1 [,] 1 ) -> (arcsin ` A ) e. RR )
Theorem	acosrecl 23885	The arccosine function is real in its principal domain. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- ( A e. ( -u 1 [,] 1 ) -> (arccos ` A ) e. RR )
Theorem	cosasin 23886	The cosine of the arcsine of A is sqr ( 1 - A ^ 2 ). (Contributed by Mario Carneiro, 2-Apr-2015.)
|- ( A e. CC -> ( cos ` (arcsin ` A ) ) = ( sqr ` ( 1 - ( A ^ 2 ) ) ) )
Theorem	sinacos 23887	The sine of the arccosine of A is sqr ( 1 - A ^ 2 ). (Contributed by Mario Carneiro, 2-Apr-2015.)
|- ( A e. CC -> ( sin ` (arccos ` A ) ) = ( sqr ` ( 1 - ( A ^ 2 ) ) ) )
Theorem	atandmneg 23888	The domain of the arctangent function is closed under negatives. (Contributed by Mario Carneiro, 3-Apr-2015.)
|- ( A e. dom arctan -> -u A e. dom arctan )
Theorem	atanneg 23889	The arctangent function is odd. (Contributed by Mario Carneiro, 3-Apr-2015.)
|- ( A e. dom arctan -> (arctan ` -u A ) = -u (arctan ` A ) )
Theorem	atan0 23890	The arctangent of zero is zero. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- (arctan ` 0 ) = 0
Theorem	atandmcj 23891	The arctangent function distributes under conjugation. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- ( A e. dom arctan -> ( * ` A ) e. dom arctan )
Theorem	atancj 23892	The arctangent function distributes under conjugation. (The condition that Re ( A ) =/= 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 23889 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 -u 1 and 1, though.) (Contributed by Mario Carneiro, 31-Mar-2015.)
|- ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( A e. dom arctan /\ ( * ` (arctan ` A ) ) = (arctan ` ( * ` A ) ) ) )
Theorem	atanrecl 23893	The arctangent function is real for all real inputs. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- ( A e. RR -> (arctan ` A ) e. RR )
Theorem	efiatan 23894	Value of the exponential of an artcangent. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- ( A e. dom arctan -> ( exp ` ( _i x. (arctan ` A ) ) ) = ( ( sqr ` ( 1 + ( _i x. A ) ) ) / ( sqr ` ( 1 - ( _i x. A ) ) ) ) )
Theorem	atanlogaddlem 23895	Lemma for atanlogadd 23896. (Contributed by Mario Carneiro, 3-Apr-2015.)
|- ( ( A e. dom arctan /\ 0 <_ ( Re ` A ) ) -> ( ( log ` ( 1 + ( _i x. A ) ) ) + ( log ` ( 1 - ( _i x. A ) ) ) ) e. ran log )
Theorem	atanlogadd 23896	The rule sqr ( z w ) = ( sqr z ) ( sqr w ) is not always true on the complex numbers, but it is true when the arguments of z and w sum to within the interval ( -u pi , pi ], so there are some cases such as this one with z = 1 + _i A and w = 1 - _i A which are true unconditionally. This result can also be stated as " sqr ( 1 + z ) + sqr ( 1 - z ) is analytic". (Contributed by Mario Carneiro, 3-Apr-2015.)
|- ( A e. dom arctan -> ( ( log ` ( 1 + ( _i x. A ) ) ) + ( log ` ( 1 - ( _i x. A ) ) ) ) e. ran log )
Theorem	atanlogsublem 23897	Lemma for atanlogsub 23898. (Contributed by Mario Carneiro, 4-Apr-2015.)
|- ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) e. ( -u pi (,) pi ) )
Theorem	atanlogsub 23898	A variation on atanlogadd 23896, to show that sqr ( 1 + _i z ) / sqr ( 1 - _i z ) = sqr ( ( 1 + _i z ) / ( 1 - _i z ) ) under more limited conditions. (Contributed by Mario Carneiro, 4-Apr-2015.)
|- ( ( A e. dom arctan /\ ( Re ` A ) =/= 0 ) -> ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) e. ran log )
Theorem	efiatan2 23899	Value of the exponential of an artcangent. (Contributed by Mario Carneiro, 3-Apr-2015.)
|- ( A e. dom arctan -> ( exp ` ( _i x. (arctan ` A ) ) ) = ( ( 1 + ( _i x. A ) ) / ( sqr ` ( 1 + ( A ^ 2 ) ) ) ) )
Theorem	2efiatan 23900	Value of the exponential of an artcangent. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- ( A e. dom arctan -> ( exp ` ( 2 x. ( _i x. (arctan ` A ) ) ) ) = ( ( ( 2 x. _i ) / ( A + _i ) ) - 1 ) )