P. 133 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 13201-13300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cji 13201	The complex conjugate of the imaginary unit. (Contributed by NM, 26-Mar-2005.)
|- ( * ` _i ) = -u _i
Theorem	cjreim 13202	The conjugate of a representation of a complex number in terms of real and imaginary parts. (Contributed by NM, 1-Jul-2005.)
|- ( ( A e. RR /\ B e. RR ) -> ( * ` ( A + ( _i x. B ) ) ) = ( A - ( _i x. B ) ) )
Theorem	cjreim2 13203	The conjugate of the representation of a complex number in terms of real and imaginary parts. (Contributed by NM, 1-Jul-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.)
|- ( ( A e. RR /\ B e. RR ) -> ( * ` ( A - ( _i x. B ) ) ) = ( A + ( _i x. B ) ) )
Theorem	cj11 13204	Complex conjugate is a one-to-one function. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Eric Schmidt, 2-Jul-2009.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( * ` A ) = ( * ` B ) <-> A = B ) )
Theorem	cjne0 13205	A number is nonzero iff its complex conjugate is nonzero. (Contributed by NM, 29-Apr-2005.)
|- ( A e. CC -> ( A =/= 0 <-> ( * ` A ) =/= 0 ) )
Theorem	cjdiv 13206	Complex conjugate distributes over division. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.)
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( * ` ( A / B ) ) = ( ( * ` A ) / ( * ` B ) ) )
Theorem	cnrecnv 13207*	The inverse to the canonical bijection from ( RR X. RR ) to CC from cnref1o 11297. (Contributed by Mario Carneiro, 25-Aug-2014.)
|- F = ( x e. RR , y e. RR |-> ( x + ( _i x. y ) ) )   =>    |- `' F = ( z e. CC |-> <. ( Re ` z ) , ( Im ` z ) >. )
Theorem	sqeqd 13208	A deduction for showing two numbers whose squares are equal are themselves equal. (Contributed by Mario Carneiro, 3-Apr-2015.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> ( A ^ 2 ) = ( B ^ 2 ) )   &    |- ( ph -> 0 <_ ( Re ` A ) )   &    |- ( ph -> 0 <_ ( Re ` B ) )   &    |- ( ( ph /\ ( Re ` A ) = 0 /\ ( Re ` B ) = 0 ) -> A = B )   =>    |- ( ph -> A = B )
Theorem	recli 13209	The real part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.)
|- A e. CC   =>    |- ( Re ` A ) e. RR
Theorem	imcli 13210	The imaginary part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.)
|- A e. CC   =>    |- ( Im ` A ) e. RR
Theorem	cjcli 13211	Closure law for complex conjugate. (Contributed by NM, 11-May-1999.)
|- A e. CC   =>    |- ( * ` A ) e. CC
Theorem	replimi 13212	Construct a complex number from its real and imaginary parts. (Contributed by NM, 1-Oct-1999.)
|- A e. CC   =>    |- A = ( ( Re ` A ) + ( _i x. ( Im ` A ) ) )
Theorem	cjcji 13213	The conjugate of the conjugate is the original complex number. Proposition 10-3.4(e) of [Gleason] p. 133. (Contributed by NM, 11-May-1999.)
|- A e. CC   =>    |- ( * ` ( * ` A ) ) = A
Theorem	reim0bi 13214	A number is real iff its imaginary part is 0. (Contributed by NM, 29-May-1999.)
|- A e. CC   =>    |- ( A e. RR <-> ( Im ` A ) = 0 )
Theorem	rerebi 13215	A real number equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 27-Oct-1999.)
|- A e. CC   =>    |- ( A e. RR <-> ( Re ` A ) = A )
Theorem	cjrebi 13216	A number is real iff it equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 11-Oct-1999.)
|- A e. CC   =>    |- ( A e. RR <-> ( * ` A ) = A )
Theorem	recji 13217	Real part of a complex conjugate. (Contributed by NM, 2-Oct-1999.)
|- A e. CC   =>    |- ( Re ` ( * ` A ) ) = ( Re ` A )
Theorem	imcji 13218	Imaginary part of a complex conjugate. (Contributed by NM, 2-Oct-1999.)
|- A e. CC   =>    |- ( Im ` ( * ` A ) ) = -u ( Im ` A )
Theorem	cjmulrcli 13219	A complex number times its conjugate is real. (Contributed by NM, 11-May-1999.)
|- A e. CC   =>    |- ( A x. ( * ` A ) ) e. RR
Theorem	cjmulvali 13220	A complex number times its conjugate. (Contributed by NM, 2-Oct-1999.)
|- A e. CC   =>    |- ( A x. ( * ` A ) ) = ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) )
Theorem	cjmulge0i 13221	A complex number times its conjugate is nonnegative. (Contributed by NM, 28-May-1999.)
|- A e. CC   =>    |- 0 <_ ( A x. ( * ` A ) )
Theorem	renegi 13222	Real part of negative. (Contributed by NM, 2-Aug-1999.)
|- A e. CC   =>    |- ( Re ` -u A ) = -u ( Re ` A )
Theorem	imnegi 13223	Imaginary part of negative. (Contributed by NM, 2-Aug-1999.)
|- A e. CC   =>    |- ( Im ` -u A ) = -u ( Im ` A )
Theorem	cjnegi 13224	Complex conjugate of negative. (Contributed by NM, 2-Aug-1999.)
|- A e. CC   =>    |- ( * ` -u A ) = -u ( * ` A )
Theorem	addcji 13225	A number plus its conjugate is twice its real part. Compare Proposition 10-3.4(h) of [Gleason] p. 133. (Contributed by NM, 2-Oct-1999.)
|- A e. CC   =>    |- ( A + ( * ` A ) ) = ( 2 x. ( Re ` A ) )
Theorem	readdi 13226	Real part distributes over addition. (Contributed by NM, 28-Jul-1999.)
|- A e. CC   &    |- B e. CC   =>    |- ( Re ` ( A + B ) ) = ( ( Re ` A ) + ( Re ` B ) )
Theorem	imaddi 13227	Imaginary part distributes over addition. (Contributed by NM, 28-Jul-1999.)
|- A e. CC   &    |- B e. CC   =>    |- ( Im ` ( A + B ) ) = ( ( Im ` A ) + ( Im ` B ) )
Theorem	remuli 13228	Real part of a product. (Contributed by NM, 28-Jul-1999.)
|- A e. CC   &    |- B e. CC   =>    |- ( Re ` ( A x. B ) ) = ( ( ( Re ` A ) x. ( Re ` B ) ) - ( ( Im ` A ) x. ( Im ` B ) ) )
Theorem	immuli 13229	Imaginary part of a product. (Contributed by NM, 28-Jul-1999.)
|- A e. CC   &    |- B e. CC   =>    |- ( Im ` ( A x. B ) ) = ( ( ( Re ` A ) x. ( Im ` B ) ) + ( ( Im ` A ) x. ( Re ` B ) ) )
Theorem	cjaddi 13230	Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.)
|- A e. CC   &    |- B e. CC   =>    |- ( * ` ( A + B ) ) = ( ( * ` A ) + ( * ` B ) )
Theorem	cjmuli 13231	Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.)
|- A e. CC   &    |- B e. CC   =>    |- ( * ` ( A x. B ) ) = ( ( * ` A ) x. ( * ` B ) )
Theorem	ipcni 13232	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 13233	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 13234	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 13235	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 13236	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 13237	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 13238	Closure law for complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( * ` A ) e. CC )
Theorem	replimd 13239	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 13240	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 13241	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 13242	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 13243	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 13244	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 13245	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 13246	Real part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( Re ` ( * ` A ) ) = ( Re ` A ) )
Theorem	imcjd 13247	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 13248	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 13249	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 13250	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 13251	Real part of negative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( Re ` -u A ) = -u ( Re ` A ) )
Theorem	imnegd 13252	Imaginary part of negative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( Im ` -u A ) = -u ( Im ` A ) )
Theorem	cjnegd 13253	Complex conjugate of negative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( * ` -u A ) = -u ( * ` A ) )
Theorem	addcjd 13254	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 13255	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 13256	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 13257	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 13258	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 13259	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 13260	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 13261	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 13262	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 13263	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 13264	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 13265	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 13266	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 13267	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 13268	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 13269	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 13270	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 13271	Real part of a division. Related to remul2 13172. (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 13272	Imaginary part of a division. Related to remul2 13172. (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 13273	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 13274	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 13275	Extend class notation to include square root of a complex number.
class sqr
Syntax	cabs 13276	Extend class notation to include a function for the absolute value (modulus) of a complex number.
class abs
Definition	df-sqrt 13277*	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 13403 for its closure, sqrtval 13279 for its value, sqrtth 13406 and sqsqrti 13417 for its relationship to squares, and sqrt11i 13426 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 13278	Define the function for the absolute value (modulus) of a complex number. See abscli 13436 for its closure and absval 13280 or absval2i 13438 for its value. (Contributed by NM, 27-Jul-1999.)
|- abs = ( x e. CC |-> ( sqr ` ( x x. ( * ` x ) ) ) )
Theorem	sqrtval 13279*	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 13280	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 13281	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 13282	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 13283	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 13284	Square root of zero. (Contributed by Mario Carneiro, 9-Jul-2013.)
|- ( sqr ` 0 ) = 0
Theorem	sqrlem1 13285*	Lemma for 01sqrex 13292. (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 13286*	Lemma for 01sqrex 13292. (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 13287*	Lemma for 01sqrex 13292. (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 13288*	Lemma for 01sqrex 13292. (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 13289*	Lemma for 01sqrex 13292. (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 13290*	Lemma for 01sqrex 13292. (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 13291*	Lemma for 01sqrex 13292. (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 13292*	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 13293*	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 13294*	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 13295*	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 13296	Closure of the square root function. (Contributed by Mario Carneiro, 9-Jul-2013.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( sqr ` A ) e. RR )
Theorem	resqrtthlem 13297	Lemma for resqrtth 13298. (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 13298	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 13299	Square of square root. (Contributed by Mario Carneiro, 10-Jul-2013.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( ( sqr ` A ) x. ( sqr ` A ) ) = A )
Theorem	sqrtge0 13300	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 ) )