P. 115 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 11401-11500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	re0 11401	The real part of zero. (Contributed by NM, 27-Jul-1999.)
|- ( Re ` 0 ) = 0
Theorem	im0 11402	The imaginary part of zero. (Contributed by NM, 27-Jul-1999.)
|- ( Im ` 0 ) = 0
Theorem	re1 11403	The real part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
|- ( Re ` 1 ) = 1
Theorem	im1 11404	The imaginary part of one. (Contributed by Scott Fenton, 9-Jun-2006.)
|- ( Im ` 1 ) = 0
Theorem	rei 11405	The real part of _i. (Contributed by Scott Fenton, 9-Jun-2006.)
|- ( Re ` _i ) = 0
Theorem	imi 11406	The imaginary part of _i. (Contributed by Scott Fenton, 9-Jun-2006.)
|- ( Im ` _i ) = 1
Theorem	cj0 11407	The conjugate of zero. (Contributed by NM, 27-Jul-1999.)
|- ( * ` 0 ) = 0
Theorem	cji 11408	The complex conjugate of the imaginary unit. (Contributed by NM, 26-Mar-2005.)
|- ( * ` _i ) = -u _i
Theorem	cjreim 11409	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 11410	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 11411	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	cjap 11412	Complex conjugate and apartness. (Contributed by Jim Kingdon, 14-Jun-2020.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( * ` A ) # ( * ` B ) <-> A # B ) )
Theorem	cjap0 11413	A number is apart from zero iff its complex conjugate is apart from zero. (Contributed by Jim Kingdon, 14-Jun-2020.)
|- ( A e. CC -> ( A # 0 <-> ( * ` A ) # 0 ) )
Theorem	cjne0 11414	A number is nonzero iff its complex conjugate is nonzero. Also see cjap0 11413 which is similar but for apartness. (Contributed by NM, 29-Apr-2005.)
|- ( A e. CC -> ( A =/= 0 <-> ( * ` A ) =/= 0 ) )
Theorem	cjdivap 11415	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	cnrecnv 11416*	The inverse to the canonical bijection from ( RR X. RR ) to CC from cnref1o 9842. (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	recli 11417	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 11418	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 11419	Closure law for complex conjugate. (Contributed by NM, 11-May-1999.)
|- A e. CC   =>    |- ( * ` A ) e. CC
Theorem	replimi 11420	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 11421	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 11422	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 11423	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 11424	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 11425	Real part of a complex conjugate. (Contributed by NM, 2-Oct-1999.)
|- A e. CC   =>    |- ( Re ` ( * ` A ) ) = ( Re ` A )
Theorem	imcji 11426	Imaginary part of a complex conjugate. (Contributed by NM, 2-Oct-1999.)
|- A e. CC   =>    |- ( Im ` ( * ` A ) ) = -u ( Im ` A )
Theorem	cjmulrcli 11427	A complex number times its conjugate is real. (Contributed by NM, 11-May-1999.)
|- A e. CC   =>    |- ( A x. ( * ` A ) ) e. RR
Theorem	cjmulvali 11428	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 11429	A complex number times its conjugate is nonnegative. (Contributed by NM, 28-May-1999.)
|- A e. CC   =>    |- 0 <_ ( A x. ( * ` A ) )
Theorem	renegi 11430	Real part of negative. (Contributed by NM, 2-Aug-1999.)
|- A e. CC   =>    |- ( Re ` -u A ) = -u ( Re ` A )
Theorem	imnegi 11431	Imaginary part of negative. (Contributed by NM, 2-Aug-1999.)
|- A e. CC   =>    |- ( Im ` -u A ) = -u ( Im ` A )
Theorem	cjnegi 11432	Complex conjugate of negative. (Contributed by NM, 2-Aug-1999.)
|- A e. CC   =>    |- ( * ` -u A ) = -u ( * ` A )
Theorem	addcji 11433	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 11434	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 11435	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 11436	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 11437	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 11438	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 11439	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 11440	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 11441	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 11442	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 11443	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 11444	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 11445	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 11446	Closure law for complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( * ` A ) e. CC )
Theorem	replimd 11447	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 11448	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 11449	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 11450	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 11451	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 11452	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 11453	A number which is nonzero has a complex conjugate which is nonzero. Also see cjap0d 11454 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 11454	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 11455	Real part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( Re ` ( * ` A ) ) = ( Re ` A ) )
Theorem	imcjd 11456	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 11457	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 11458	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 11459	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 11460	Real part of negative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( Re ` -u A ) = -u ( Re ` A ) )
Theorem	imnegd 11461	Imaginary part of negative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( Im ` -u A ) = -u ( Im ` A ) )
Theorem	cjnegd 11462	Complex conjugate of negative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( * ` -u A ) = -u ( * ` A ) )
Theorem	addcjd 11463	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 11464	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 11465	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 11466	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 11467	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 11468	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 11469	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 11470	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 11471	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 11472	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 11473	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 11474	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 11475	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 11476	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 11477	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 11478	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 11479	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 11480	Real part of a division. Related to remul2 11379. (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 11481	Imaginary part of a division. Related to remul2 11379. (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 11482	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 11483	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 11484	Complex apartness in terms of real and imaginary parts. See also apreim 8746 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 11485*	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 11486*	Lemma for caucvgre 11487. 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 11487*	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 11488	Lemma for cvg1n 11492. 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 11489*	Lemma for cvg1n 11492. 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 11490*	Lemma for cvg1n 11492. 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 11491*	Lemma for cvg1n 11492. 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 11492*	Convergence of real sequences. This is a version of caucvgre 11487 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 11493	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 11494*	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 11495*	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 11496*	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 11497*	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 11498*	A version of 19.29 1666 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 11499*	A version of r19.2m 3578 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 11500	Lemma for recvguniq 11501. 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. )