P. 112 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 11101-11200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	recji 11101	Real part of a complex conjugate. (Contributed by NM, 2-Oct-1999.)
|- A e. CC   =>    |- ( Re ` ( * ` A ) ) = ( Re ` A )
Theorem	imcji 11102	Imaginary part of a complex conjugate. (Contributed by NM, 2-Oct-1999.)
|- A e. CC   =>    |- ( Im ` ( * ` A ) ) = -u ( Im ` A )
Theorem	cjmulrcli 11103	A complex number times its conjugate is real. (Contributed by NM, 11-May-1999.)
|- A e. CC   =>    |- ( A x. ( * ` A ) ) e. RR
Theorem	cjmulvali 11104	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 11105	A complex number times its conjugate is nonnegative. (Contributed by NM, 28-May-1999.)
|- A e. CC   =>    |- 0 <_ ( A x. ( * ` A ) )
Theorem	renegi 11106	Real part of negative. (Contributed by NM, 2-Aug-1999.)
|- A e. CC   =>    |- ( Re ` -u A ) = -u ( Re ` A )
Theorem	imnegi 11107	Imaginary part of negative. (Contributed by NM, 2-Aug-1999.)
|- A e. CC   =>    |- ( Im ` -u A ) = -u ( Im ` A )
Theorem	cjnegi 11108	Complex conjugate of negative. (Contributed by NM, 2-Aug-1999.)
|- A e. CC   =>    |- ( * ` -u A ) = -u ( * ` A )
Theorem	addcji 11109	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 11110	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 11111	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 11112	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 11113	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 11114	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 11115	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 11116	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	cjdivapi 11117	Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.)
|- A e. CC   &    |- B e. CC   =>    |- ( B # 0 -> ( * ` ( A / B ) ) = ( ( * ` A ) / ( * ` B ) ) )
Theorem	crrei 11118	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 11119	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 11120	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 11121	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 11122	Closure law for complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( * ` A ) e. CC )
Theorem	replimd 11123	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 11124	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 11125	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 11126	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 11127	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 11128	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 11129	A number which is nonzero has a complex conjugate which is nonzero. Also see cjap0d 11130 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 11130	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 11131	Real part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( Re ` ( * ` A ) ) = ( Re ` A ) )
Theorem	imcjd 11132	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 11133	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 11134	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 11135	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 11136	Real part of negative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( Re ` -u A ) = -u ( Re ` A ) )
Theorem	imnegd 11137	Imaginary part of negative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( Im ` -u A ) = -u ( Im ` A ) )
Theorem	cjnegd 11138	Complex conjugate of negative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( * ` -u A ) = -u ( * ` A ) )
Theorem	addcjd 11139	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 11140	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 11141	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 11142	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 11143	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 11144	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 11145	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 11146	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 11147	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 11148	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 11149	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 11150	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 11151	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 11152	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 11153	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 11154	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 11155	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 11156	Real part of a division. Related to remul2 11055. (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 11157	Imaginary part of a division. Related to remul2 11055. (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 11158	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 11159	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 11160	Complex apartness in terms of real and imaginary parts. See also apreim 8647 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 11161*	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 11162*	Lemma for caucvgre 11163. 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 11163*	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 11164	Lemma for cvg1n 11168. 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 11165*	Lemma for cvg1n 11168. 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 11166*	Lemma for cvg1n 11168. 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 11167*	Lemma for cvg1n 11168. 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 11168*	Convergence of real sequences. This is a version of caucvgre 11163 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 11169	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 11170*	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 11171*	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 11172*	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 11173*	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 11174*	A version of 19.29 1634 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 11175*	A version of r19.2m 3538 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 11176	Lemma for recvguniq 11177. 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 11177*	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 11178	Extend class notation to include square root of a complex number.
class sqr
Syntax	cabs 11179	Extend class notation to include a function for the absolute value (modulus) of a complex number.
class abs
Definition	df-rsqrt 11180*	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 11181	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 11182*	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 11183	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 11184	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 11185	Lemma for sqrt0 11186. (Contributed by Jim Kingdon, 26-Aug-2020.)
|- ( ( A e. RR /\ ( ( A ^ 2 ) = 0 /\ 0 <_ A ) ) <-> A = 0 )
Theorem	sqrt0 11186	Square root of zero. (Contributed by Mario Carneiro, 9-Jul-2013.)
|- ( sqr ` 0 ) = 0
Theorem	resqrexlem1arp 11187	Lemma for resqrex 11208. 1 + A is a positive real (expressed in a way that will help apply seqf 10573 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 11188*	Lemma for resqrex 11208. Applying the recursion rule yields a positive real (expressed in a way that will help apply seqf 10573 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 11189*	Lemma for resqrex 11208. 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 11190*	Lemma for resqrex 11208. 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 11191*	Lemma for resqrex 11208. 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 11192*	Lemma for resqrex 11208. 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 11193*	Lemma for resqrex 11208. 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 11194*	Lemma for resqrex 11208. 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 11195*	Lemma for resqrex 11208. 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 11196*	Lemma for resqrex 11208. 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 11197*	Lemma for resqrex 11208. 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 11198*	Lemma for resqrex 11208. 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 11199*	Lemma for resqrex 11208. 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 11200*	Lemma for resqrex 11208. 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 ) ) ) )