P. 116 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 11501-11600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	crrei 11501	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 11502	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 11503	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 11504	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 11505	Closure law for complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( * ` A ) e. CC )
Theorem	replimd 11506	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 11507	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 11508	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 11509	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 11510	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 11511	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 11512	A number which is nonzero has a complex conjugate which is nonzero. Also see cjap0d 11513 which is similar but for apartness. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> A =/= 0 )   =>    |- ( ph -> ( * ` A ) =/= 0 )
Theorem	cjap0d 11513	A number which is apart from zero has a complex conjugate which is apart from zero. (Contributed by Jim Kingdon, 11-Aug-2021.)
|- ( ph -> A e. CC )   &    |- ( ph -> A # 0 )   =>    |- ( ph -> ( * ` A ) # 0 )
Theorem	recjd 11514	Real part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( Re ` ( * ` A ) ) = ( Re ` A ) )
Theorem	imcjd 11515	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 11516	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 11517	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 11518	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 11519	Real part of negative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( Re ` -u A ) = -u ( Re ` A ) )
Theorem	imnegd 11520	Imaginary part of negative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( Im ` -u A ) = -u ( Im ` A ) )
Theorem	cjnegd 11521	Complex conjugate of negative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( * ` -u A ) = -u ( * ` A ) )
Theorem	addcjd 11522	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 11523	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 11524	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 11525	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 11526	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 11527	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 11528	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 11529	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 11530	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 11531	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 11532	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	cjdivapd 11533	Complex conjugate distributes over division. (Contributed by Jim Kingdon, 15-Jun-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> ( * ` ( A / B ) ) = ( ( * ` A ) / ( * ` B ) ) )
Theorem	rered 11534	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 11535	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 11536	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 11537	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 11538	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	redivapd 11539	Real part of a division. Related to remul2 11438. (Contributed by Jim Kingdon, 15-Jun-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A # 0 )   =>    |- ( ph -> ( Re ` ( B / A ) ) = ( ( Re ` B ) / A ) )
Theorem	imdivapd 11540	Imaginary part of a division. Related to remul2 11438. (Contributed by Jim Kingdon, 15-Jun-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A # 0 )   =>    |- ( ph -> ( Im ` ( B / A ) ) = ( ( Im ` B ) / A ) )
Theorem	crred 11541	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 11542	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 )
Theorem	cnreim 11543	Complex apartness in terms of real and imaginary parts. See also apreim 8783 which is similar but with different notation. (Contributed by Jim Kingdon, 16-Dec-2023.)
|- ( ( A e. CC /\ B e. CC ) -> ( A # B <-> ( ( Re ` A ) # ( Re ` B ) \/ ( Im ` A ) # ( Im ` B ) ) ) )
4.8.3  Sequence convergence
Theorem	caucvgrelemrec 11544*	Two ways to express a reciprocal. (Contributed by Jim Kingdon, 20-Jul-2021.)
|- ( ( A e. RR /\ A # 0 ) -> ( iota_ r e. RR ( A x. r ) = 1 ) = ( 1 / A ) )
Theorem	caucvgrelemcau 11545*	Lemma for caucvgre 11546. Converting the Cauchy condition. (Contributed by Jim Kingdon, 20-Jul-2021.)
|- ( ph -> F : NN --> RR )   &    |- ( ph -> A. n e. NN A. k e. ( ZZ>= ` n ) ( ( F ` n ) < ( ( F ` k ) + ( 1 / n ) ) /\ ( F ` k ) < ( ( F ` n ) + ( 1 / n ) ) ) )   =>    |- ( ph -> A. n e. NN A. k e. NN ( n <RR k -> ( ( F ` n ) <RR ( ( F ` k ) + ( iota_ r e. RR ( n x. r ) = 1 ) ) /\ ( F ` k ) <RR ( ( F ` n ) + ( iota_ r e. RR ( n x. r ) = 1 ) ) ) ) )
Theorem	caucvgre 11546*	Convergence of real sequences. A Cauchy sequence (as defined here, which has a rate of convergence built in) of real numbers converges to a real number. Specifically on rate of convergence, all terms after the nth term must be within 1 / n of the nth term. (Contributed by Jim Kingdon, 19-Jul-2021.)
|- ( ph -> F : NN --> RR )   &    |- ( ph -> A. n e. NN A. k e. ( ZZ>= ` n ) ( ( F ` n ) < ( ( F ` k ) + ( 1 / n ) ) /\ ( F ` k ) < ( ( F ` n ) + ( 1 / n ) ) ) )   =>    |- ( ph -> E. y e. RR A. x e. RR+ E. j e. NN A. i e. ( ZZ>= ` j ) ( ( F ` i ) < ( y + x ) /\ y < ( ( F ` i ) + x ) ) )
Theorem	cvg1nlemcxze 11547	Lemma for cvg1n 11551. Rearranging an expression related to the rate of convergence. (Contributed by Jim Kingdon, 6-Aug-2021.)
|- ( ph -> C e. RR+ )   &    |- ( ph -> X e. RR+ )   &    |- ( ph -> Z e. NN )   &    |- ( ph -> E e. NN )   &    |- ( ph -> A e. NN )   &    |- ( ph -> ( ( ( ( C x. 2 ) / X ) / Z ) + A ) < E )   =>    |- ( ph -> ( C / ( E x. Z ) ) < ( X / 2 ) )
Theorem	cvg1nlemf 11548*	Lemma for cvg1n 11551. The modified sequence G is a sequence. (Contributed by Jim Kingdon, 1-Aug-2021.)
|- ( ph -> F : NN --> RR )   &    |- ( ph -> C e. RR+ )   &    |- ( ph -> A. n e. NN A. k e. ( ZZ>= ` n ) ( ( F ` n ) < ( ( F ` k ) + ( C / n ) ) /\ ( F ` k ) < ( ( F ` n ) + ( C / n ) ) ) )   &    |- G = ( j e. NN |-> ( F ` ( j x. Z ) ) )   &    |- ( ph -> Z e. NN )   &    |- ( ph -> C < Z )   =>    |- ( ph -> G : NN --> RR )
Theorem	cvg1nlemcau 11549*	Lemma for cvg1n 11551. By selecting spaced out terms for the modified sequence G, the terms are within 1 / n (without the constant C). (Contributed by Jim Kingdon, 1-Aug-2021.)
|- ( ph -> F : NN --> RR )   &    |- ( ph -> C e. RR+ )   &    |- ( ph -> A. n e. NN A. k e. ( ZZ>= ` n ) ( ( F ` n ) < ( ( F ` k ) + ( C / n ) ) /\ ( F ` k ) < ( ( F ` n ) + ( C / n ) ) ) )   &    |- G = ( j e. NN |-> ( F ` ( j x. Z ) ) )   &    |- ( ph -> Z e. NN )   &    |- ( ph -> C < Z )   =>    |- ( ph -> A. n e. NN A. k e. ( ZZ>= ` n ) ( ( G ` n ) < ( ( G ` k ) + ( 1 / n ) ) /\ ( G ` k ) < ( ( G ` n ) + ( 1 / n ) ) ) )
Theorem	cvg1nlemres 11550*	Lemma for cvg1n 11551. The original sequence F has a limit (turns out it is the same as the limit of the modified sequence G). (Contributed by Jim Kingdon, 1-Aug-2021.)
|- ( ph -> F : NN --> RR )   &    |- ( ph -> C e. RR+ )   &    |- ( ph -> A. n e. NN A. k e. ( ZZ>= ` n ) ( ( F ` n ) < ( ( F ` k ) + ( C / n ) ) /\ ( F ` k ) < ( ( F ` n ) + ( C / n ) ) ) )   &    |- G = ( j e. NN |-> ( F ` ( j x. Z ) ) )   &    |- ( ph -> Z e. NN )   &    |- ( ph -> C < Z )   =>    |- ( ph -> E. y e. RR A. x e. RR+ E. j e. NN A. i e. ( ZZ>= ` j ) ( ( F ` i ) < ( y + x ) /\ y < ( ( F ` i ) + x ) ) )
Theorem	cvg1n 11551*	Convergence of real sequences. This is a version of caucvgre 11546 with a constant multiplier C on the rate of convergence. That is, all terms after the nth term must be within C / n of the nth term. (Contributed by Jim Kingdon, 1-Aug-2021.)
|- ( ph -> F : NN --> RR )   &    |- ( ph -> C e. RR+ )   &    |- ( ph -> A. n e. NN A. k e. ( ZZ>= ` n ) ( ( F ` n ) < ( ( F ` k ) + ( C / n ) ) /\ ( F ` k ) < ( ( F ` n ) + ( C / n ) ) ) )   =>    |- ( ph -> E. y e. RR A. x e. RR+ E. j e. NN A. i e. ( ZZ>= ` j ) ( ( F ` i ) < ( y + x ) /\ y < ( ( F ` i ) + x ) ) )
Theorem	uzin2 11552	The upper integers are closed under intersection. (Contributed by Mario Carneiro, 24-Dec-2013.)
|- ( ( A e. ran ZZ>= /\ B e. ran ZZ>= ) -> ( A i^i B ) e. ran ZZ>= )
Theorem	rexanuz 11553*	Combine two different upper integer properties into one. (Contributed by Mario Carneiro, 25-Dec-2013.)
|- ( E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ph /\ ps ) <-> ( E. j e. ZZ A. k e. ( ZZ>= ` j ) ph /\ E. j e. ZZ A. k e. ( ZZ>= ` j ) ps ) )
Theorem	rexfiuz 11554*	Combine finitely many different upper integer properties into one. (Contributed by Mario Carneiro, 6-Jun-2014.)
|- ( A e. Fin -> ( E. j e. ZZ A. k e. ( ZZ>= ` j ) A. n e. A ph <-> A. n e. A E. j e. ZZ A. k e. ( ZZ>= ` j ) ph ) )
Theorem	rexuz3 11555*	Restrict the base of the upper integers set to another upper integers set. (Contributed by Mario Carneiro, 26-Dec-2013.)
|- Z = ( ZZ>= ` M )   =>    |- ( M e. ZZ -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ph <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ph ) )
Theorem	rexanuz2 11556*	Combine two different upper integer properties into one. (Contributed by Mario Carneiro, 26-Dec-2013.)
|- Z = ( ZZ>= ` M )   =>    |- ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ph /\ ps ) <-> ( E. j e. Z A. k e. ( ZZ>= ` j ) ph /\ E. j e. Z A. k e. ( ZZ>= ` j ) ps ) )
Theorem	r19.29uz 11557*	A version of 19.29 1668 for upper integer quantifiers. (Contributed by Mario Carneiro, 10-Feb-2014.)
|- Z = ( ZZ>= ` M )   =>    |- ( ( A. k e. Z ph /\ E. j e. Z A. k e. ( ZZ>= ` j ) ps ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ph /\ ps ) )
Theorem	r19.2uz 11558*	A version of r19.2m 3581 for upper integer quantifiers. (Contributed by Mario Carneiro, 15-Feb-2014.)
|- Z = ( ZZ>= ` M )   =>    |- ( E. j e. Z A. k e. ( ZZ>= ` j ) ph -> E. k e. Z ph )
Theorem	recvguniqlem 11559	Lemma for recvguniq 11560. Some of the rearrangements of the expressions. (Contributed by Jim Kingdon, 8-Aug-2021.)
|- ( ph -> F : NN --> RR )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> K e. NN )   &    |- ( ph -> A < ( ( F ` K ) + ( ( A - B ) / 2 ) ) )   &    |- ( ph -> ( F ` K ) < ( B + ( ( A - B ) / 2 ) ) )   =>    |- ( ph -> F. )
Theorem	recvguniq 11560*	Limits are unique. (Contributed by Jim Kingdon, 7-Aug-2021.)
|- ( ph -> F : NN --> RR )   &    |- ( ph -> L e. RR )   &    |- ( ph -> A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) < ( L + x ) /\ L < ( ( F ` k ) + x ) ) )   &    |- ( ph -> M e. RR )   &    |- ( ph -> A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F ` k ) < ( M + x ) /\ M < ( ( F ` k ) + x ) ) )   =>    |- ( ph -> L = M )
4.8.4  Square root; absolute value
Syntax	csqrt 11561	Extend class notation to include square root of a complex number.
class sqr
Syntax	cabs 11562	Extend class notation to include a function for the absolute value (modulus) of a complex number.
class abs
Definition	df-rsqrt 11563*	Define a function whose value is the square root of a nonnegative real number. Defining the square root for complex numbers has one difficult part: choosing between the two roots. The usual way to define a principal square root for all complex numbers relies on excluded middle or something similar. But in the case of a nonnegative real number, we don't have the complications presented for general complex numbers, and we can choose the nonnegative root. (Contributed by Jim Kingdon, 23-Aug-2020.)
|- sqr = ( x e. RR |-> ( iota_ y e. RR ( ( y ^ 2 ) = x /\ 0 <_ y ) ) )
Definition	df-abs 11564	Define the function for the absolute value (modulus) of a complex number. (Contributed by NM, 27-Jul-1999.)
|- abs = ( x e. CC |-> ( sqr ` ( x x. ( * ` x ) ) ) )
Theorem	sqrtrval 11565*	Value of square root function. (Contributed by Jim Kingdon, 23-Aug-2020.)
|- ( A e. RR -> ( sqr ` A ) = ( iota_ x e. RR ( ( x ^ 2 ) = A /\ 0 <_ x ) ) )
Theorem	absval 11566	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 11567	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	sqrt0rlem 11568	Lemma for sqrt0 11569. (Contributed by Jim Kingdon, 26-Aug-2020.)
|- ( ( A e. RR /\ ( ( A ^ 2 ) = 0 /\ 0 <_ A ) ) <-> A = 0 )
Theorem	sqrt0 11569	Square root of zero. (Contributed by Mario Carneiro, 9-Jul-2013.)
|- ( sqr ` 0 ) = 0
Theorem	resqrexlem1arp 11570	Lemma for resqrex 11591. 1 + A is a positive real (expressed in a way that will help apply seqf 10727 and similar theorems). (Contributed by Jim Kingdon, 28-Jul-2021.) (Revised by Jim Kingdon, 16-Oct-2022.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ( ph /\ N e. NN ) -> ( ( NN X. { ( 1 + A ) } ) ` N ) e. RR+ )
Theorem	resqrexlemp1rp 11571*	Lemma for resqrex 11591. Applying the recursion rule yields a positive real (expressed in a way that will help apply seqf 10727 and similar theorems). (Contributed by Jim Kingdon, 28-Jul-2021.) (Revised by Jim Kingdon, 16-Oct-2022.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ( ph /\ ( B e. RR+ /\ C e. RR+ ) ) -> ( B ( y e. RR+ , z e. RR+ |-> ( ( y + ( A / y ) ) / 2 ) ) C ) e. RR+ )
Theorem	resqrexlemf 11572*	Lemma for resqrex 11591. The sequence is a function. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.) (Revised by Jim Kingdon, 16-Oct-2022.)
|- F = seq 1 ( ( y e. RR+ , z e. RR+ |-> ( ( y + ( A / y ) ) / 2 ) ) , ( NN X. { ( 1 + A ) } ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ph -> F : NN --> RR+ )
Theorem	resqrexlemf1 11573*	Lemma for resqrex 11591. Initial value. Although this sequence converges to the square root with any positive initial value, this choice makes various steps in the proof of convergence easier. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.) (Revised by Jim Kingdon, 16-Oct-2022.)
|- F = seq 1 ( ( y e. RR+ , z e. RR+ |-> ( ( y + ( A / y ) ) / 2 ) ) , ( NN X. { ( 1 + A ) } ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ph -> ( F ` 1 ) = ( 1 + A ) )
Theorem	resqrexlemfp1 11574*	Lemma for resqrex 11591. Recursion rule. This sequence is the ancient method for computing square roots, often known as the babylonian method, although known to many ancient cultures. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.)
|- F = seq 1 ( ( y e. RR+ , z e. RR+ |-> ( ( y + ( A / y ) ) / 2 ) ) , ( NN X. { ( 1 + A ) } ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ( ph /\ N e. NN ) -> ( F ` ( N + 1 ) ) = ( ( ( F ` N ) + ( A / ( F ` N ) ) ) / 2 ) )
Theorem	resqrexlemover 11575*	Lemma for resqrex 11591. Each element of the sequence is an overestimate. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.)
|- F = seq 1 ( ( y e. RR+ , z e. RR+ |-> ( ( y + ( A / y ) ) / 2 ) ) , ( NN X. { ( 1 + A ) } ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ( ph /\ N e. NN ) -> A < ( ( F ` N ) ^ 2 ) )
Theorem	resqrexlemdec 11576*	Lemma for resqrex 11591. The sequence is decreasing. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.)
|- F = seq 1 ( ( y e. RR+ , z e. RR+ |-> ( ( y + ( A / y ) ) / 2 ) ) , ( NN X. { ( 1 + A ) } ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ( ph /\ N e. NN ) -> ( F ` ( N + 1 ) ) < ( F ` N ) )
Theorem	resqrexlemdecn 11577*	Lemma for resqrex 11591. The sequence is decreasing. (Contributed by Jim Kingdon, 31-Jul-2021.)
|- F = seq 1 ( ( y e. RR+ , z e. RR+ |-> ( ( y + ( A / y ) ) / 2 ) ) , ( NN X. { ( 1 + A ) } ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> N e. NN )   &    |- ( ph -> M e. NN )   &    |- ( ph -> N < M )   =>    |- ( ph -> ( F ` M ) < ( F ` N ) )
Theorem	resqrexlemlo 11578*	Lemma for resqrex 11591. A (variable) lower bound for each term of the sequence. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.)
|- F = seq 1 ( ( y e. RR+ , z e. RR+ |-> ( ( y + ( A / y ) ) / 2 ) ) , ( NN X. { ( 1 + A ) } ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ( ph /\ N e. NN ) -> ( 1 / ( 2 ^ N ) ) < ( F ` N ) )
Theorem	resqrexlemcalc1 11579*	Lemma for resqrex 11591. Some of the calculations involved in showing that the sequence converges. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.)
|- F = seq 1 ( ( y e. RR+ , z e. RR+ |-> ( ( y + ( A / y ) ) / 2 ) ) , ( NN X. { ( 1 + A ) } ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ( ph /\ N e. NN ) -> ( ( ( F ` ( N + 1 ) ) ^ 2 ) - A ) = ( ( ( ( ( F ` N ) ^ 2 ) - A ) ^ 2 ) / ( 4 x. ( ( F ` N ) ^ 2 ) ) ) )
Theorem	resqrexlemcalc2 11580*	Lemma for resqrex 11591. Some of the calculations involved in showing that the sequence converges. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.)
|- F = seq 1 ( ( y e. RR+ , z e. RR+ |-> ( ( y + ( A / y ) ) / 2 ) ) , ( NN X. { ( 1 + A ) } ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ( ph /\ N e. NN ) -> ( ( ( F ` ( N + 1 ) ) ^ 2 ) - A ) <_ ( ( ( ( F ` N ) ^ 2 ) - A ) / 4 ) )
Theorem	resqrexlemcalc3 11581*	Lemma for resqrex 11591. Some of the calculations involved in showing that the sequence converges. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.)
|- F = seq 1 ( ( y e. RR+ , z e. RR+ |-> ( ( y + ( A / y ) ) / 2 ) ) , ( NN X. { ( 1 + A ) } ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ( ph /\ N e. NN ) -> ( ( ( F ` N ) ^ 2 ) - A ) <_ ( ( ( F ` 1 ) ^ 2 ) / ( 4 ^ ( N - 1 ) ) ) )
Theorem	resqrexlemnmsq 11582*	Lemma for resqrex 11591. The difference between the squares of two terms of the sequence. (Contributed by Mario Carneiro and Jim Kingdon, 30-Jul-2021.)
|- F = seq 1 ( ( y e. RR+ , z e. RR+ |-> ( ( y + ( A / y ) ) / 2 ) ) , ( NN X. { ( 1 + A ) } ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> N e. NN )   &    |- ( ph -> M e. NN )   &    |- ( ph -> N <_ M )   =>    |- ( ph -> ( ( ( F ` N ) ^ 2 ) - ( ( F ` M ) ^ 2 ) ) < ( ( ( F ` 1 ) ^ 2 ) / ( 4 ^ ( N - 1 ) ) ) )
Theorem	resqrexlemnm 11583*	Lemma for resqrex 11591. The difference between two terms of the sequence. (Contributed by Mario Carneiro and Jim Kingdon, 31-Jul-2021.)
|- F = seq 1 ( ( y e. RR+ , z e. RR+ |-> ( ( y + ( A / y ) ) / 2 ) ) , ( NN X. { ( 1 + A ) } ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> N e. NN )   &    |- ( ph -> M e. NN )   &    |- ( ph -> N <_ M )   =>    |- ( ph -> ( ( F ` N ) - ( F ` M ) ) < ( ( ( ( F ` 1 ) ^ 2 ) x. 2 ) / ( 2 ^ ( N - 1 ) ) ) )
Theorem	resqrexlemcvg 11584*	Lemma for resqrex 11591. The sequence has a limit. (Contributed by Jim Kingdon, 6-Aug-2021.)
|- F = seq 1 ( ( y e. RR+ , z e. RR+ |-> ( ( y + ( A / y ) ) / 2 ) ) , ( NN X. { ( 1 + A ) } ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ph -> E. r e. RR A. x e. RR+ E. j e. NN A. i e. ( ZZ>= ` j ) ( ( F ` i ) < ( r + x ) /\ r < ( ( F ` i ) + x ) ) )
Theorem	resqrexlemgt0 11585*	Lemma for resqrex 11591. A limit is nonnegative. (Contributed by Jim Kingdon, 7-Aug-2021.)
|- F = seq 1 ( ( y e. RR+ , z e. RR+ |-> ( ( y + ( A / y ) ) / 2 ) ) , ( NN X. { ( 1 + A ) } ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> L e. RR )   &    |- ( ph -> A. e e. RR+ E. j e. NN A. i e. ( ZZ>= ` j ) ( ( F ` i ) < ( L + e ) /\ L < ( ( F ` i ) + e ) ) )   =>    |- ( ph -> 0 <_ L )
Theorem	resqrexlemoverl 11586*	Lemma for resqrex 11591. Every term in the sequence is an overestimate compared with the limit L. Although this theorem is stated in terms of a particular sequence the proof could be adapted for any decreasing convergent sequence. (Contributed by Jim Kingdon, 9-Aug-2021.)
|- F = seq 1 ( ( y e. RR+ , z e. RR+ |-> ( ( y + ( A / y ) ) / 2 ) ) , ( NN X. { ( 1 + A ) } ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> L e. RR )   &    |- ( ph -> A. e e. RR+ E. j e. NN A. i e. ( ZZ>= ` j ) ( ( F ` i ) < ( L + e ) /\ L < ( ( F ` i ) + e ) ) )   &    |- ( ph -> K e. NN )   =>    |- ( ph -> L <_ ( F ` K ) )
Theorem	resqrexlemglsq 11587*	Lemma for resqrex 11591. The sequence formed by squaring each term of F converges to ( L ^ 2 ). (Contributed by Mario Carneiro and Jim Kingdon, 8-Aug-2021.)
|- F = seq 1 ( ( y e. RR+ , z e. RR+ |-> ( ( y + ( A / y ) ) / 2 ) ) , ( NN X. { ( 1 + A ) } ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> L e. RR )   &    |- ( ph -> A. e e. RR+ E. j e. NN A. i e. ( ZZ>= ` j ) ( ( F ` i ) < ( L + e ) /\ L < ( ( F ` i ) + e ) ) )   &    |- G = ( x e. NN |-> ( ( F ` x ) ^ 2 ) )   =>    |- ( ph -> A. e e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( G ` k ) < ( ( L ^ 2 ) + e ) /\ ( L ^ 2 ) < ( ( G ` k ) + e ) ) )
Theorem	resqrexlemga 11588*	Lemma for resqrex 11591. The sequence formed by squaring each term of F converges to A. (Contributed by Mario Carneiro and Jim Kingdon, 8-Aug-2021.)
|- F = seq 1 ( ( y e. RR+ , z e. RR+ |-> ( ( y + ( A / y ) ) / 2 ) ) , ( NN X. { ( 1 + A ) } ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> L e. RR )   &    |- ( ph -> A. e e. RR+ E. j e. NN A. i e. ( ZZ>= ` j ) ( ( F ` i ) < ( L + e ) /\ L < ( ( F ` i ) + e ) ) )   &    |- G = ( x e. NN |-> ( ( F ` x ) ^ 2 ) )   =>    |- ( ph -> A. e e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( G ` k ) < ( A + e ) /\ A < ( ( G ` k ) + e ) ) )
Theorem	resqrexlemsqa 11589*	Lemma for resqrex 11591. The square of a limit is A. (Contributed by Jim Kingdon, 7-Aug-2021.)
|- F = seq 1 ( ( y e. RR+ , z e. RR+ |-> ( ( y + ( A / y ) ) / 2 ) ) , ( NN X. { ( 1 + A ) } ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> L e. RR )   &    |- ( ph -> A. e e. RR+ E. j e. NN A. i e. ( ZZ>= ` j ) ( ( F ` i ) < ( L + e ) /\ L < ( ( F ` i ) + e ) ) )   =>    |- ( ph -> ( L ^ 2 ) = A )
Theorem	resqrexlemex 11590*	Lemma for resqrex 11591. Existence of square root given a sequence which converges to the square root. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.)
|- F = seq 1 ( ( y e. RR+ , z e. RR+ |-> ( ( y + ( A / y ) ) / 2 ) ) , ( NN X. { ( 1 + A ) } ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ph -> E. x e. RR ( 0 <_ x /\ ( x ^ 2 ) = A ) )
Theorem	resqrex 11591*	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	rsqrmo 11592*	Uniqueness for the square root function. (Contributed by Jim Kingdon, 10-Aug-2021.)
|- ( ( A e. RR /\ 0 <_ A ) -> E* x e. RR ( ( x ^ 2 ) = A /\ 0 <_ x ) )
Theorem	rersqreu 11593*	Existence and uniqueness for the real square root function. (Contributed by Jim Kingdon, 10-Aug-2021.)
|- ( ( A e. RR /\ 0 <_ A ) -> E! x e. RR ( ( x ^ 2 ) = A /\ 0 <_ x ) )
Theorem	resqrtcl 11594	Closure of the square root function. (Contributed by Mario Carneiro, 9-Jul-2013.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( sqr ` A ) e. RR )
Theorem	rersqrtthlem 11595	Lemma for resqrtth 11596. (Contributed by Jim Kingdon, 10-Aug-2021.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( ( ( sqr ` A ) ^ 2 ) = A /\ 0 <_ ( sqr ` A ) ) )
Theorem	resqrtth 11596	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 11597	Square of square root. (Contributed by Mario Carneiro, 10-Jul-2013.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( ( sqr ` A ) x. ( sqr ` A ) ) = A )
Theorem	sqrtge0 11598	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 11599	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 11600	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 ) ) )