P. 134 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 13301-13400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ipcni 13301	Standard inner product on complex numbers. (Contributed by NM, 2-Oct-1999.)
|- A e. CC   &    |- B e. CC   =>    |- ( Re ` ( A x. ( * ` B ) ) ) = ( ( ( Re ` A ) x. ( Re ` B ) ) + ( ( Im ` A ) x. ( Im ` B ) ) )
Theorem	cjdivi 13302	Complex conjugate distributes over division. (Contributed by NM, 29-Apr-2005.) (Revised by Mario Carneiro, 29-May-2016.)
|- A e. CC   &    |- B e. CC   =>    |- ( B =/= 0 -> ( * ` ( A / B ) ) = ( ( * ` A ) / ( * ` B ) ) )
Theorem	crrei 13303	The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( Re ` ( A + ( _i x. B ) ) ) = A
Theorem	crimi 13304	The imaginary part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( Im ` ( A + ( _i x. B ) ) ) = B
Theorem	recld 13305	The real part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( Re ` A ) e. RR )
Theorem	imcld 13306	The imaginary part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( Im ` A ) e. RR )
Theorem	cjcld 13307	Closure law for complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( * ` A ) e. CC )
Theorem	replimd 13308	Construct a complex number from its real and imaginary parts. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> A = ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) )
Theorem	remimd 13309	Value of the conjugate of a complex number. The value is the real part minus _i times the imaginary part. Definition 10-3.2 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( * ` A ) = ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) )
Theorem	cjcjd 13310	The conjugate of the conjugate is the original complex number. Proposition 10-3.4(e) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( * ` ( * ` A ) ) = A )
Theorem	reim0bd 13311	A number is real iff its imaginary part is 0. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> ( Im ` A ) = 0 )   =>    |- ( ph -> A e. RR )
Theorem	rerebd 13312	A real number equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> ( Re ` A ) = A )   =>    |- ( ph -> A e. RR )
Theorem	cjrebd 13313	A number is real iff it equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> ( * ` A ) = A )   =>    |- ( ph -> A e. RR )
Theorem	cjne0d 13314	A number is nonzero iff its complex conjugate is nonzero. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> A =/= 0 )   =>    |- ( ph -> ( * ` A ) =/= 0 )
Theorem	recjd 13315	Real part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( Re ` ( * ` A ) ) = ( Re ` A ) )
Theorem	imcjd 13316	Imaginary part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( Im ` ( * ` A ) ) = -u ( Im ` A ) )
Theorem	cjmulrcld 13317	A complex number times its conjugate is real. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A x. ( * ` A ) ) e. RR )
Theorem	cjmulvald 13318	A complex number times its conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A x. ( * ` A ) ) = ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) )
Theorem	cjmulge0d 13319	A complex number times its conjugate is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> 0 <_ ( A x. ( * ` A ) ) )
Theorem	renegd 13320	Real part of negative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( Re ` -u A ) = -u ( Re ` A ) )
Theorem	imnegd 13321	Imaginary part of negative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( Im ` -u A ) = -u ( Im ` A ) )
Theorem	cjnegd 13322	Complex conjugate of negative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( * ` -u A ) = -u ( * ` A ) )
Theorem	addcjd 13323	A number plus its conjugate is twice its real part. Compare Proposition 10-3.4(h) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A + ( * ` A ) ) = ( 2 x. ( Re ` A ) ) )
Theorem	cjexpd 13324	Complex conjugate of positive integer exponentiation. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> N e. NN0 )   =>    |- ( ph -> ( * ` ( A ^ N ) ) = ( ( * ` A ) ^ N ) )
Theorem	readdd 13325	Real part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( Re ` ( A + B ) ) = ( ( Re ` A ) + ( Re ` B ) ) )
Theorem	imaddd 13326	Imaginary part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( Im ` ( A + B ) ) = ( ( Im ` A ) + ( Im ` B ) ) )
Theorem	resubd 13327	Real part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( Re ` ( A - B ) ) = ( ( Re ` A ) - ( Re ` B ) ) )
Theorem	imsubd 13328	Imaginary part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( Im ` ( A - B ) ) = ( ( Im ` A ) - ( Im ` B ) ) )
Theorem	remuld 13329	Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( Re ` ( A x. B ) ) = ( ( ( Re ` A ) x. ( Re ` B ) ) - ( ( Im ` A ) x. ( Im ` B ) ) ) )
Theorem	immuld 13330	Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( Im ` ( A x. B ) ) = ( ( ( Re ` A ) x. ( Im ` B ) ) + ( ( Im ` A ) x. ( Re ` B ) ) ) )
Theorem	cjaddd 13331	Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( * ` ( A + B ) ) = ( ( * ` A ) + ( * ` B ) ) )
Theorem	cjmuld 13332	Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( * ` ( A x. B ) ) = ( ( * ` A ) x. ( * ` B ) ) )
Theorem	ipcnd 13333	Standard inner product on complex numbers. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( Re ` ( A x. ( * ` B ) ) ) = ( ( ( Re ` A ) x. ( Re ` B ) ) + ( ( Im ` A ) x. ( Im ` B ) ) ) )
Theorem	cjdivd 13334	Complex conjugate distributes over division. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( * ` ( A / B ) ) = ( ( * ` A ) / ( * ` B ) ) )
Theorem	rered 13335	A real number equals its real part. One direction of Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( Re ` A ) = A )
Theorem	reim0d 13336	The imaginary part of a real number is 0. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( Im ` A ) = 0 )
Theorem	cjred 13337	A real number equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( * ` A ) = A )
Theorem	remul2d 13338	Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( Re ` ( A x. B ) ) = ( A x. ( Re ` B ) ) )
Theorem	immul2d 13339	Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( Im ` ( A x. B ) ) = ( A x. ( Im ` B ) ) )
Theorem	redivd 13340	Real part of a division. Related to remul2 13241. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A =/= 0 )   =>    |- ( ph -> ( Re ` ( B / A ) ) = ( ( Re ` B ) / A ) )
Theorem	imdivd 13341	Imaginary part of a division. Related to remul2 13241. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A =/= 0 )   =>    |- ( ph -> ( Im ` ( B / A ) ) = ( ( Im ` B ) / A ) )
Theorem	crred 13342	The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( Re ` ( A + ( _i x. B ) ) ) = A )
Theorem	crimd 13343	The imaginary part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( Im ` ( A + ( _i x. B ) ) ) = B )
5.9.4  Square root; absolute value
Syntax	csqrt 13344	Extend class notation to include square root of a complex number.
class sqr
Syntax	cabs 13345	Extend class notation to include a function for the absolute value (modulus) of a complex number.
class abs
Definition	df-sqrt 13346*	Define a function whose value is the square root of a complex number. Since ( y ^ 2 ) = x iff ( -u y ^ 2 ) = x, we ensure uniqueness by restricting the range to numbers with positive real part, or numbers with 0 real part and nonnegative imaginary part. A description can be found under "Principal square root of a complex number" at http://en.wikipedia.org/wiki/Square_root. The square root symbol was introduced in 1525 by Christoff Rudolff. See sqrtcl 13472 for its closure, sqrtval 13348 for its value, sqrtth 13475 and sqsqrti 13486 for its relationship to squares, and sqrt11i 13495 for uniqueness. (Contributed by NM, 27-Jul-1999.) (Revised by Mario Carneiro, 8-Jul-2013.)
|- sqr = ( x e. CC |-> ( iota_ y e. CC ( ( y ^ 2 ) = x /\ 0 <_ ( Re ` y ) /\ ( _i x. y ) e/ RR+ ) ) )
Definition	df-abs 13347	Define the function for the absolute value (modulus) of a complex number. See abscli 13505 for its closure and absval 13349 or absval2i 13507 for its value. (Contributed by NM, 27-Jul-1999.)
|- abs = ( x e. CC |-> ( sqr ` ( x x. ( * ` x ) ) ) )
Theorem	sqrtval 13348*	Value of square root function. (Contributed by Mario Carneiro, 8-Jul-2013.)
|- ( A e. CC -> ( sqr ` A ) = ( iota_ x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) ) )
Theorem	absval 13349	The absolute value (modulus) of a complex number. Proposition 10-3.7(a) of [Gleason] p. 133. (Contributed by NM, 27-Jul-1999.) (Revised by Mario Carneiro, 7-Nov-2013.)
|- ( A e. CC -> ( abs ` A ) = ( sqr ` ( A x. ( * ` A ) ) ) )
Theorem	rennim 13350	A real number does not lie on the negative imaginary axis. (Contributed by Mario Carneiro, 8-Jul-2013.)
|- ( A e. RR -> ( _i x. A ) e/ RR+ )
Theorem	cnpart 13351	The specification of restriction to the right half-plane partitions the complex plane without 0 into two disjoint pieces, which are related by a reflection about the origin (under the map x |-> -u x). (Contributed by Mario Carneiro, 8-Jul-2013.)
|- ( ( A e. CC /\ A =/= 0 ) -> ( ( 0 <_ ( Re ` A ) /\ ( _i x. A ) e/ RR+ ) <-> -. ( 0 <_ ( Re ` -u A ) /\ ( _i x. -u A ) e/ RR+ ) ) )
Theorem	sqr0lem 13352	Square root of zero. (Contributed by Mario Carneiro, 9-Jul-2013.)
|- ( ( A e. CC /\ ( ( A ^ 2 ) = 0 /\ 0 <_ ( Re ` A ) /\ ( _i x. A ) e/ RR+ ) ) <-> A = 0 )
Theorem	sqrt0 13353	Square root of zero. (Contributed by Mario Carneiro, 9-Jul-2013.)
|- ( sqr ` 0 ) = 0
Theorem	sqrlem1 13354*	Lemma for 01sqrex 13361. (Contributed by Mario Carneiro, 10-Jul-2013.)
|- S = { x e. RR+ | ( x ^ 2 ) <_ A }   &    |- B = sup ( S , RR , < )   =>    |- ( ( A e. RR+ /\ A <_ 1 ) -> A. y e. S y <_ 1 )
Theorem	sqrlem2 13355*	Lemma for 01sqrex 13361. (Contributed by Mario Carneiro, 10-Jul-2013.)
|- S = { x e. RR+ | ( x ^ 2 ) <_ A }   &    |- B = sup ( S , RR , < )   =>    |- ( ( A e. RR+ /\ A <_ 1 ) -> A e. S )
Theorem	sqrlem3 13356*	Lemma for 01sqrex 13361. (Contributed by Mario Carneiro, 10-Jul-2013.)
|- S = { x e. RR+ | ( x ^ 2 ) <_ A }   &    |- B = sup ( S , RR , < )   =>    |- ( ( A e. RR+ /\ A <_ 1 ) -> ( S C_ RR /\ S =/= (/) /\ E. z e. RR A. y e. S y <_ z ) )
Theorem	sqrlem4 13357*	Lemma for 01sqrex 13361. (Contributed by Mario Carneiro, 10-Jul-2013.)
|- S = { x e. RR+ | ( x ^ 2 ) <_ A }   &    |- B = sup ( S , RR , < )   =>    |- ( ( A e. RR+ /\ A <_ 1 ) -> ( B e. RR+ /\ B <_ 1 ) )
Theorem	sqrlem5 13358*	Lemma for 01sqrex 13361. (Contributed by Mario Carneiro, 10-Jul-2013.)
|- S = { x e. RR+ | ( x ^ 2 ) <_ A }   &    |- B = sup ( S , RR , < )   &    |- T = { y | E. a e. S E. b e. S y = ( a x. b ) }   =>    |- ( ( A e. RR+ /\ A <_ 1 ) -> ( ( T C_ RR /\ T =/= (/) /\ E. v e. RR A. u e. T u <_ v ) /\ ( B ^ 2 ) = sup ( T , RR , < ) ) )
Theorem	sqrlem6 13359*	Lemma for 01sqrex 13361. (Contributed by Mario Carneiro, 10-Jul-2013.)
|- S = { x e. RR+ | ( x ^ 2 ) <_ A }   &    |- B = sup ( S , RR , < )   &    |- T = { y | E. a e. S E. b e. S y = ( a x. b ) }   =>    |- ( ( A e. RR+ /\ A <_ 1 ) -> ( B ^ 2 ) <_ A )
Theorem	sqrlem7 13360*	Lemma for 01sqrex 13361. (Contributed by Mario Carneiro, 10-Jul-2013.)
|- S = { x e. RR+ | ( x ^ 2 ) <_ A }   &    |- B = sup ( S , RR , < )   &    |- T = { y | E. a e. S E. b e. S y = ( a x. b ) }   =>    |- ( ( A e. RR+ /\ A <_ 1 ) -> ( B ^ 2 ) = A )
Theorem	01sqrex 13361*	Existence of a square root for reals in the interval ( 0 , 1 ]. (Contributed by Mario Carneiro, 10-Jul-2013.)
|- ( ( A e. RR+ /\ A <_ 1 ) -> E. x e. RR+ ( x <_ 1 /\ ( x ^ 2 ) = A ) )
Theorem	resqrex 13362*	Existence of a square root for positive reals. (Contributed by Mario Carneiro, 9-Jul-2013.)
|- ( ( A e. RR /\ 0 <_ A ) -> E. x e. RR ( 0 <_ x /\ ( x ^ 2 ) = A ) )
Theorem	sqrmo 13363*	Uniqueness for the square root function. (Contributed by Mario Carneiro, 9-Jul-2013.) (Revised by NM, 17-Jun-2017.)
|- ( A e. CC -> E* x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) )
Theorem	resqreu 13364*	Existence and uniqueness for the real square root function. (Contributed by Mario Carneiro, 9-Jul-2013.)
|- ( ( A e. RR /\ 0 <_ A ) -> E! x e. CC ( ( x ^ 2 ) = A /\ 0 <_ ( Re ` x ) /\ ( _i x. x ) e/ RR+ ) )
Theorem	resqrtcl 13365	Closure of the square root function. (Contributed by Mario Carneiro, 9-Jul-2013.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( sqr ` A ) e. RR )
Theorem	resqrtthlem 13366	Lemma for resqrtth 13367. (Contributed by Mario Carneiro, 9-Jul-2013.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( ( ( sqr ` A ) ^ 2 ) = A /\ 0 <_ ( Re ` ( sqr ` A ) ) /\ ( _i x. ( sqr ` A ) ) e/ RR+ ) )
Theorem	resqrtth 13367	Square root theorem over the reals. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 9-Jul-2013.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( ( sqr ` A ) ^ 2 ) = A )
Theorem	remsqsqrt 13368	Square of square root. (Contributed by Mario Carneiro, 10-Jul-2013.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( ( sqr ` A ) x. ( sqr ` A ) ) = A )
Theorem	sqrtge0 13369	The square root function is nonnegative for nonnegative input. (Contributed by NM, 26-May-1999.) (Revised by Mario Carneiro, 9-Jul-2013.)
|- ( ( A e. RR /\ 0 <_ A ) -> 0 <_ ( sqr ` A ) )
Theorem	sqrtgt0 13370	The square root function is positive for positive input. (Contributed by Mario Carneiro, 10-Jul-2013.) (Revised by Mario Carneiro, 6-Sep-2013.)
|- ( ( A e. RR /\ 0 < A ) -> 0 < ( sqr ` A ) )
Theorem	sqrtmul 13371	Square root distributes over multiplication. (Contributed by NM, 30-Jul-1999.) (Revised by Mario Carneiro, 29-May-2016.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( sqr ` ( A x. B ) ) = ( ( sqr ` A ) x. ( sqr ` B ) ) )
Theorem	sqrtle 13372	Square root is monotonic. (Contributed by NM, 17-Mar-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( A <_ B <-> ( sqr ` A ) <_ ( sqr ` B ) ) )
Theorem	sqrtlt 13373	Square root is strictly monotonic. Closed form of sqrtlti 13500. (Contributed by Scott Fenton, 17-Apr-2014.) (Proof shortened by Mario Carneiro, 29-May-2016.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( A < B <-> ( sqr ` A ) < ( sqr ` B ) ) )
Theorem	sqrt11 13374	The square root function is one-to-one. (Contributed by Scott Fenton, 11-Jun-2013.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( sqr ` A ) = ( sqr ` B ) <-> A = B ) )
Theorem	sqrt00 13375	A square root is zero iff its argument is 0. (Contributed by NM, 27-Jul-1999.) (Proof shortened by Mario Carneiro, 29-May-2016.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( ( sqr ` A ) = 0 <-> A = 0 ) )
Theorem	rpsqrtcl 13376	The square root of a positive real is a positive real. (Contributed by NM, 22-Feb-2008.)
|- ( A e. RR+ -> ( sqr ` A ) e. RR+ )
Theorem	sqrtdiv 13377	Square root distributes over division. (Contributed by Mario Carneiro, 5-May-2016.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ ) -> ( sqr ` ( A / B ) ) = ( ( sqr ` A ) / ( sqr ` B ) ) )
Theorem	sqrtneglem 13378	The square root of a negative number. (Contributed by Mario Carneiro, 9-Jul-2013.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( ( ( _i x. ( sqr ` A ) ) ^ 2 ) = -u A /\ 0 <_ ( Re ` ( _i x. ( sqr ` A ) ) ) /\ ( _i x. ( _i x. ( sqr ` A ) ) ) e/ RR+ ) )
Theorem	sqrtneg 13379	The square root of a negative number. (Contributed by Mario Carneiro, 9-Jul-2013.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( sqr ` -u A ) = ( _i x. ( sqr ` A ) ) )
Theorem	sqrtsq2 13380	Relationship between square root and squares. (Contributed by NM, 31-Jul-1999.) (Revised by Mario Carneiro, 29-May-2016.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( sqr ` A ) = B <-> A = ( B ^ 2 ) ) )
Theorem	sqrtsq 13381	Square root of square. (Contributed by NM, 14-Jan-2006.) (Revised by Mario Carneiro, 29-May-2016.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( sqr ` ( A ^ 2 ) ) = A )
Theorem	sqrtmsq 13382	Square root of square. (Contributed by NM, 2-Aug-1999.) (Revised by Mario Carneiro, 29-May-2016.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( sqr ` ( A x. A ) ) = A )
Theorem	sqrt1 13383	The square root of 1 is 1. (Contributed by NM, 31-Jul-1999.)
|- ( sqr ` 1 ) = 1
Theorem	sqrt4 13384	The square root of 4 is 2. (Contributed by NM, 3-Aug-1999.)
|- ( sqr ` 4 ) = 2
Theorem	sqrt9 13385	The square root of 9 is 3. (Contributed by NM, 11-May-2004.)
|- ( sqr ` 9 ) = 3
Theorem	sqrt2gt1lt2 13386	The square root of 2 is bounded by 1 and 2. (Contributed by Roy F. Longton, 8-Aug-2005.) (Revised by Mario Carneiro, 6-Sep-2013.)
|- ( 1 < ( sqr ` 2 ) /\ ( sqr ` 2 ) < 2 )
Theorem	sqrtm1 13387	The imaginary unit is the square root of negative 1. A lot of people like to call this the "definition" of _i, but the definition of sqr df-sqrt 13346 has already been crafted with _i being mentioned explicitly, and in any case it doesn't make too much sense to define a value based on a function evaluated outside its domain. A more appropriate view is to take ax-i2m1 9632 or i2 12406 as the "definition", and simply postulate the existence of a number satisfying this property. This is the approach we take here. (Contributed by Mario Carneiro, 10-Jul-2013.)
|- _i = ( sqr ` -u 1 )
Theorem	absneg 13388	Absolute value of negative. (Contributed by NM, 27-Feb-2005.)
|- ( A e. CC -> ( abs ` -u A ) = ( abs ` A ) )
Theorem	abscl 13389	Real closure of absolute value. (Contributed by NM, 3-Oct-1999.)
|- ( A e. CC -> ( abs ` A ) e. RR )
Theorem	abscj 13390	The absolute value of a number and its conjugate are the same. Proposition 10-3.7(b) of [Gleason] p. 133. (Contributed by NM, 28-Apr-2005.)
|- ( A e. CC -> ( abs ` ( * ` A ) ) = ( abs ` A ) )
Theorem	absvalsq 13391	Square of value of absolute value function. (Contributed by NM, 16-Jan-2006.)
|- ( A e. CC -> ( ( abs ` A ) ^ 2 ) = ( A x. ( * ` A ) ) )
Theorem	absvalsq2 13392	Square of value of absolute value function. (Contributed by NM, 1-Feb-2007.)
|- ( A e. CC -> ( ( abs ` A ) ^ 2 ) = ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) )
Theorem	sqabsadd 13393	Square of absolute value of sum. Proposition 10-3.7(g) of [Gleason] p. 133. (Contributed by NM, 21-Jan-2007.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( abs ` ( A + B ) ) ^ 2 ) = ( ( ( ( abs ` A ) ^ 2 ) + ( ( abs ` B ) ^ 2 ) ) + ( 2 x. ( Re ` ( A x. ( * ` B ) ) ) ) ) )
Theorem	sqabssub 13394	Square of absolute value of difference. (Contributed by NM, 21-Jan-2007.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( abs ` ( A - B ) ) ^ 2 ) = ( ( ( ( abs ` A ) ^ 2 ) + ( ( abs ` B ) ^ 2 ) ) - ( 2 x. ( Re ` ( A x. ( * ` B ) ) ) ) ) )
Theorem	absval2 13395	Value of absolute value function. Definition 10.36 of [Gleason] p. 133. (Contributed by NM, 17-Mar-2005.)
|- ( A e. CC -> ( abs ` A ) = ( sqr ` ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) ) )
Theorem	abs0 13396	The absolute value of 0. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 29-May-2016.)
|- ( abs ` 0 ) = 0
Theorem	absi 13397	The absolute value of the imaginary unit. (Contributed by NM, 26-Mar-2005.)
|- ( abs ` _i ) = 1
Theorem	absge0 13398	Absolute value is nonnegative. (Contributed by NM, 20-Nov-2004.) (Revised by Mario Carneiro, 29-May-2016.)
|- ( A e. CC -> 0 <_ ( abs ` A ) )
Theorem	absrpcl 13399	The absolute value of a nonzero number is a positive real. (Contributed by FL, 27-Dec-2007.) (Proof shortened by Mario Carneiro, 29-May-2016.)
|- ( ( A e. CC /\ A =/= 0 ) -> ( abs ` A ) e. RR+ )
Theorem	abs00 13400	The absolute value of a number is zero iff the number is zero. Proposition 10-3.7(c) of [Gleason] p. 133. (Contributed by NM, 26-Sep-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.)
|- ( A e. CC -> ( ( abs ` A ) = 0 <-> A = 0 ) )