![]() |
Intuitionistic Logic Explorer Theorem List (p. 110 of 149) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cjexp 10901 | Complex conjugate of positive integer exponentiation. (Contributed by NM, 7-Jun-2006.) |
β’ ((π΄ β β β§ π β β0) β (ββ(π΄βπ)) = ((ββπ΄)βπ)) | ||
Theorem | imval2 10902 | The imaginary part of a number in terms of complex conjugate. (Contributed by NM, 30-Apr-2005.) |
β’ (π΄ β β β (ββπ΄) = ((π΄ β (ββπ΄)) / (2 Β· i))) | ||
Theorem | re0 10903 | The real part of zero. (Contributed by NM, 27-Jul-1999.) |
β’ (ββ0) = 0 | ||
Theorem | im0 10904 | The imaginary part of zero. (Contributed by NM, 27-Jul-1999.) |
β’ (ββ0) = 0 | ||
Theorem | re1 10905 | The real part of one. (Contributed by Scott Fenton, 9-Jun-2006.) |
β’ (ββ1) = 1 | ||
Theorem | im1 10906 | The imaginary part of one. (Contributed by Scott Fenton, 9-Jun-2006.) |
β’ (ββ1) = 0 | ||
Theorem | rei 10907 | The real part of i. (Contributed by Scott Fenton, 9-Jun-2006.) |
β’ (ββi) = 0 | ||
Theorem | imi 10908 | The imaginary part of i. (Contributed by Scott Fenton, 9-Jun-2006.) |
β’ (ββi) = 1 | ||
Theorem | cj0 10909 | The conjugate of zero. (Contributed by NM, 27-Jul-1999.) |
β’ (ββ0) = 0 | ||
Theorem | cji 10910 | The complex conjugate of the imaginary unit. (Contributed by NM, 26-Mar-2005.) |
β’ (ββi) = -i | ||
Theorem | cjreim 10911 | The conjugate of a representation of a complex number in terms of real and imaginary parts. (Contributed by NM, 1-Jul-2005.) |
β’ ((π΄ β β β§ π΅ β β) β (ββ(π΄ + (i Β· π΅))) = (π΄ β (i Β· π΅))) | ||
Theorem | cjreim2 10912 | 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.) |
β’ ((π΄ β β β§ π΅ β β) β (ββ(π΄ β (i Β· π΅))) = (π΄ + (i Β· π΅))) | ||
Theorem | cj11 10913 | Complex conjugate is a one-to-one function. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Eric Schmidt, 2-Jul-2009.) |
β’ ((π΄ β β β§ π΅ β β) β ((ββπ΄) = (ββπ΅) β π΄ = π΅)) | ||
Theorem | cjap 10914 | Complex conjugate and apartness. (Contributed by Jim Kingdon, 14-Jun-2020.) |
β’ ((π΄ β β β§ π΅ β β) β ((ββπ΄) # (ββπ΅) β π΄ # π΅)) | ||
Theorem | cjap0 10915 | A number is apart from zero iff its complex conjugate is apart from zero. (Contributed by Jim Kingdon, 14-Jun-2020.) |
β’ (π΄ β β β (π΄ # 0 β (ββπ΄) # 0)) | ||
Theorem | cjne0 10916 | A number is nonzero iff its complex conjugate is nonzero. Also see cjap0 10915 which is similar but for apartness. (Contributed by NM, 29-Apr-2005.) |
β’ (π΄ β β β (π΄ β 0 β (ββπ΄) β 0)) | ||
Theorem | cjdivap 10917 | Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.) |
β’ ((π΄ β β β§ π΅ β β β§ π΅ # 0) β (ββ(π΄ / π΅)) = ((ββπ΄) / (ββπ΅))) | ||
Theorem | cnrecnv 10918* | The inverse to the canonical bijection from (β Γ β) to β from cnref1o 9649. (Contributed by Mario Carneiro, 25-Aug-2014.) |
β’ πΉ = (π₯ β β, π¦ β β β¦ (π₯ + (i Β· π¦))) β β’ β‘πΉ = (π§ β β β¦ β¨(ββπ§), (ββπ§)β©) | ||
Theorem | recli 10919 | The real part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.) |
β’ π΄ β β β β’ (ββπ΄) β β | ||
Theorem | imcli 10920 | The imaginary part of a complex number is real (closure law). (Contributed by NM, 11-May-1999.) |
β’ π΄ β β β β’ (ββπ΄) β β | ||
Theorem | cjcli 10921 | Closure law for complex conjugate. (Contributed by NM, 11-May-1999.) |
β’ π΄ β β β β’ (ββπ΄) β β | ||
Theorem | replimi 10922 | Construct a complex number from its real and imaginary parts. (Contributed by NM, 1-Oct-1999.) |
β’ π΄ β β β β’ π΄ = ((ββπ΄) + (i Β· (ββπ΄))) | ||
Theorem | cjcji 10923 | 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.) |
β’ π΄ β β β β’ (ββ(ββπ΄)) = π΄ | ||
Theorem | reim0bi 10924 | A number is real iff its imaginary part is 0. (Contributed by NM, 29-May-1999.) |
β’ π΄ β β β β’ (π΄ β β β (ββπ΄) = 0) | ||
Theorem | rerebi 10925 | A real number equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 27-Oct-1999.) |
β’ π΄ β β β β’ (π΄ β β β (ββπ΄) = π΄) | ||
Theorem | cjrebi 10926 | 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.) |
β’ π΄ β β β β’ (π΄ β β β (ββπ΄) = π΄) | ||
Theorem | recji 10927 | Real part of a complex conjugate. (Contributed by NM, 2-Oct-1999.) |
β’ π΄ β β β β’ (ββ(ββπ΄)) = (ββπ΄) | ||
Theorem | imcji 10928 | Imaginary part of a complex conjugate. (Contributed by NM, 2-Oct-1999.) |
β’ π΄ β β β β’ (ββ(ββπ΄)) = -(ββπ΄) | ||
Theorem | cjmulrcli 10929 | A complex number times its conjugate is real. (Contributed by NM, 11-May-1999.) |
β’ π΄ β β β β’ (π΄ Β· (ββπ΄)) β β | ||
Theorem | cjmulvali 10930 | A complex number times its conjugate. (Contributed by NM, 2-Oct-1999.) |
β’ π΄ β β β β’ (π΄ Β· (ββπ΄)) = (((ββπ΄)β2) + ((ββπ΄)β2)) | ||
Theorem | cjmulge0i 10931 | A complex number times its conjugate is nonnegative. (Contributed by NM, 28-May-1999.) |
β’ π΄ β β β β’ 0 β€ (π΄ Β· (ββπ΄)) | ||
Theorem | renegi 10932 | Real part of negative. (Contributed by NM, 2-Aug-1999.) |
β’ π΄ β β β β’ (ββ-π΄) = -(ββπ΄) | ||
Theorem | imnegi 10933 | Imaginary part of negative. (Contributed by NM, 2-Aug-1999.) |
β’ π΄ β β β β’ (ββ-π΄) = -(ββπ΄) | ||
Theorem | cjnegi 10934 | Complex conjugate of negative. (Contributed by NM, 2-Aug-1999.) |
β’ π΄ β β β β’ (ββ-π΄) = -(ββπ΄) | ||
Theorem | addcji 10935 | 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.) |
β’ π΄ β β β β’ (π΄ + (ββπ΄)) = (2 Β· (ββπ΄)) | ||
Theorem | readdi 10936 | Real part distributes over addition. (Contributed by NM, 28-Jul-1999.) |
β’ π΄ β β & β’ π΅ β β β β’ (ββ(π΄ + π΅)) = ((ββπ΄) + (ββπ΅)) | ||
Theorem | imaddi 10937 | Imaginary part distributes over addition. (Contributed by NM, 28-Jul-1999.) |
β’ π΄ β β & β’ π΅ β β β β’ (ββ(π΄ + π΅)) = ((ββπ΄) + (ββπ΅)) | ||
Theorem | remuli 10938 | Real part of a product. (Contributed by NM, 28-Jul-1999.) |
β’ π΄ β β & β’ π΅ β β β β’ (ββ(π΄ Β· π΅)) = (((ββπ΄) Β· (ββπ΅)) β ((ββπ΄) Β· (ββπ΅))) | ||
Theorem | immuli 10939 | Imaginary part of a product. (Contributed by NM, 28-Jul-1999.) |
β’ π΄ β β & β’ π΅ β β β β’ (ββ(π΄ Β· π΅)) = (((ββπ΄) Β· (ββπ΅)) + ((ββπ΄) Β· (ββπ΅))) | ||
Theorem | cjaddi 10940 | Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.) |
β’ π΄ β β & β’ π΅ β β β β’ (ββ(π΄ + π΅)) = ((ββπ΄) + (ββπ΅)) | ||
Theorem | cjmuli 10941 | Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.) |
β’ π΄ β β & β’ π΅ β β β β’ (ββ(π΄ Β· π΅)) = ((ββπ΄) Β· (ββπ΅)) | ||
Theorem | ipcni 10942 | Standard inner product on complex numbers. (Contributed by NM, 2-Oct-1999.) |
β’ π΄ β β & β’ π΅ β β β β’ (ββ(π΄ Β· (ββπ΅))) = (((ββπ΄) Β· (ββπ΅)) + ((ββπ΄) Β· (ββπ΅))) | ||
Theorem | cjdivapi 10943 | Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΅ # 0 β (ββ(π΄ / π΅)) = ((ββπ΄) / (ββπ΅))) | ||
Theorem | crrei 10944 | The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.) |
β’ π΄ β β & β’ π΅ β β β β’ (ββ(π΄ + (i Β· π΅))) = π΄ | ||
Theorem | crimi 10945 | The imaginary part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.) |
β’ π΄ β β & β’ π΅ β β β β’ (ββ(π΄ + (i Β· π΅))) = π΅ | ||
Theorem | recld 10946 | The real part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (ββπ΄) β β) | ||
Theorem | imcld 10947 | The imaginary part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (ββπ΄) β β) | ||
Theorem | cjcld 10948 | Closure law for complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (ββπ΄) β β) | ||
Theorem | replimd 10949 | Construct a complex number from its real and imaginary parts. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β π΄ = ((ββπ΄) + (i Β· (ββπ΄)))) | ||
Theorem | remimd 10950 | 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.) |
β’ (π β π΄ β β) β β’ (π β (ββπ΄) = ((ββπ΄) β (i Β· (ββπ΄)))) | ||
Theorem | cjcjd 10951 | 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.) |
β’ (π β π΄ β β) β β’ (π β (ββ(ββπ΄)) = π΄) | ||
Theorem | reim0bd 10952 | A number is real iff its imaginary part is 0. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β (ββπ΄) = 0) β β’ (π β π΄ β β) | ||
Theorem | rerebd 10953 | A real number equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β (ββπ΄) = π΄) β β’ (π β π΄ β β) | ||
Theorem | cjrebd 10954 | 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.) |
β’ (π β π΄ β β) & β’ (π β (ββπ΄) = π΄) β β’ (π β π΄ β β) | ||
Theorem | cjne0d 10955 | A number which is nonzero has a complex conjugate which is nonzero. Also see cjap0d 10956 which is similar but for apartness. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΄ β 0) β β’ (π β (ββπ΄) β 0) | ||
Theorem | cjap0d 10956 | A number which is apart from zero has a complex conjugate which is apart from zero. (Contributed by Jim Kingdon, 11-Aug-2021.) |
β’ (π β π΄ β β) & β’ (π β π΄ # 0) β β’ (π β (ββπ΄) # 0) | ||
Theorem | recjd 10957 | Real part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (ββ(ββπ΄)) = (ββπ΄)) | ||
Theorem | imcjd 10958 | Imaginary part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (ββ(ββπ΄)) = -(ββπ΄)) | ||
Theorem | cjmulrcld 10959 | A complex number times its conjugate is real. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (π΄ Β· (ββπ΄)) β β) | ||
Theorem | cjmulvald 10960 | A complex number times its conjugate. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (π΄ Β· (ββπ΄)) = (((ββπ΄)β2) + ((ββπ΄)β2))) | ||
Theorem | cjmulge0d 10961 | A complex number times its conjugate is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β 0 β€ (π΄ Β· (ββπ΄))) | ||
Theorem | renegd 10962 | Real part of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (ββ-π΄) = -(ββπ΄)) | ||
Theorem | imnegd 10963 | Imaginary part of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (ββ-π΄) = -(ββπ΄)) | ||
Theorem | cjnegd 10964 | Complex conjugate of negative. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (ββ-π΄) = -(ββπ΄)) | ||
Theorem | addcjd 10965 | 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.) |
β’ (π β π΄ β β) β β’ (π β (π΄ + (ββπ΄)) = (2 Β· (ββπ΄))) | ||
Theorem | cjexpd 10966 | Complex conjugate of positive integer exponentiation. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π β β0) β β’ (π β (ββ(π΄βπ)) = ((ββπ΄)βπ)) | ||
Theorem | readdd 10967 | Real part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (ββ(π΄ + π΅)) = ((ββπ΄) + (ββπ΅))) | ||
Theorem | imaddd 10968 | Imaginary part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (ββ(π΄ + π΅)) = ((ββπ΄) + (ββπ΅))) | ||
Theorem | resubd 10969 | Real part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (ββ(π΄ β π΅)) = ((ββπ΄) β (ββπ΅))) | ||
Theorem | imsubd 10970 | Imaginary part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (ββ(π΄ β π΅)) = ((ββπ΄) β (ββπ΅))) | ||
Theorem | remuld 10971 | Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (ββ(π΄ Β· π΅)) = (((ββπ΄) Β· (ββπ΅)) β ((ββπ΄) Β· (ββπ΅)))) | ||
Theorem | immuld 10972 | Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (ββ(π΄ Β· π΅)) = (((ββπ΄) Β· (ββπ΅)) + ((ββπ΄) Β· (ββπ΅)))) | ||
Theorem | cjaddd 10973 | Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (ββ(π΄ + π΅)) = ((ββπ΄) + (ββπ΅))) | ||
Theorem | cjmuld 10974 | Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (ββ(π΄ Β· π΅)) = ((ββπ΄) Β· (ββπ΅))) | ||
Theorem | ipcnd 10975 | Standard inner product on complex numbers. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (ββ(π΄ Β· (ββπ΅))) = (((ββπ΄) Β· (ββπ΅)) + ((ββπ΄) Β· (ββπ΅)))) | ||
Theorem | cjdivapd 10976 | Complex conjugate distributes over division. (Contributed by Jim Kingdon, 15-Jun-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΅ # 0) β β’ (π β (ββ(π΄ / π΅)) = ((ββπ΄) / (ββπ΅))) | ||
Theorem | rered 10977 | 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.) |
β’ (π β π΄ β β) β β’ (π β (ββπ΄) = π΄) | ||
Theorem | reim0d 10978 | The imaginary part of a real number is 0. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (ββπ΄) = 0) | ||
Theorem | cjred 10979 | A real number equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (ββπ΄) = π΄) | ||
Theorem | remul2d 10980 | Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (ββ(π΄ Β· π΅)) = (π΄ Β· (ββπ΅))) | ||
Theorem | immul2d 10981 | Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (ββ(π΄ Β· π΅)) = (π΄ Β· (ββπ΅))) | ||
Theorem | redivapd 10982 | Real part of a division. Related to remul2 10881. (Contributed by Jim Kingdon, 15-Jun-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ # 0) β β’ (π β (ββ(π΅ / π΄)) = ((ββπ΅) / π΄)) | ||
Theorem | imdivapd 10983 | Imaginary part of a division. Related to remul2 10881. (Contributed by Jim Kingdon, 15-Jun-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ # 0) β β’ (π β (ββ(π΅ / π΄)) = ((ββπ΅) / π΄)) | ||
Theorem | crred 10984 | The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (ββ(π΄ + (i Β· π΅))) = π΄) | ||
Theorem | crimd 10985 | The imaginary part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (ββ(π΄ + (i Β· π΅))) = π΅) | ||
Theorem | cnreim 10986 | Complex apartness in terms of real and imaginary parts. See also apreim 8559 which is similar but with different notation. (Contributed by Jim Kingdon, 16-Dec-2023.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ # π΅ β ((ββπ΄) # (ββπ΅) β¨ (ββπ΄) # (ββπ΅)))) | ||
Theorem | caucvgrelemrec 10987* | Two ways to express a reciprocal. (Contributed by Jim Kingdon, 20-Jul-2021.) |
β’ ((π΄ β β β§ π΄ # 0) β (β©π β β (π΄ Β· π) = 1) = (1 / π΄)) | ||
Theorem | caucvgrelemcau 10988* | Lemma for caucvgre 10989. Converting the Cauchy condition. (Contributed by Jim Kingdon, 20-Jul-2021.) |
β’ (π β πΉ:ββΆβ) & β’ (π β βπ β β βπ β (β€β₯βπ)((πΉβπ) < ((πΉβπ) + (1 / π)) β§ (πΉβπ) < ((πΉβπ) + (1 / π)))) β β’ (π β βπ β β βπ β β (π <β π β ((πΉβπ) <β ((πΉβπ) + (β©π β β (π Β· π) = 1)) β§ (πΉβπ) <β ((πΉβπ) + (β©π β β (π Β· π) = 1))))) | ||
Theorem | caucvgre 10989* |
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 / π of the nth term. (Contributed by Jim Kingdon, 19-Jul-2021.) |
β’ (π β πΉ:ββΆβ) & β’ (π β βπ β β βπ β (β€β₯βπ)((πΉβπ) < ((πΉβπ) + (1 / π)) β§ (πΉβπ) < ((πΉβπ) + (1 / π)))) β β’ (π β βπ¦ β β βπ₯ β β+ βπ β β βπ β (β€β₯βπ)((πΉβπ) < (π¦ + π₯) β§ π¦ < ((πΉβπ) + π₯))) | ||
Theorem | cvg1nlemcxze 10990 | Lemma for cvg1n 10994. Rearranging an expression related to the rate of convergence. (Contributed by Jim Kingdon, 6-Aug-2021.) |
β’ (π β πΆ β β+) & β’ (π β π β β+) & β’ (π β π β β) & β’ (π β πΈ β β) & β’ (π β π΄ β β) & β’ (π β ((((πΆ Β· 2) / π) / π) + π΄) < πΈ) β β’ (π β (πΆ / (πΈ Β· π)) < (π / 2)) | ||
Theorem | cvg1nlemf 10991* | Lemma for cvg1n 10994. The modified sequence πΊ is a sequence. (Contributed by Jim Kingdon, 1-Aug-2021.) |
β’ (π β πΉ:ββΆβ) & β’ (π β πΆ β β+) & β’ (π β βπ β β βπ β (β€β₯βπ)((πΉβπ) < ((πΉβπ) + (πΆ / π)) β§ (πΉβπ) < ((πΉβπ) + (πΆ / π)))) & β’ πΊ = (π β β β¦ (πΉβ(π Β· π))) & β’ (π β π β β) & β’ (π β πΆ < π) β β’ (π β πΊ:ββΆβ) | ||
Theorem | cvg1nlemcau 10992* | Lemma for cvg1n 10994. By selecting spaced out terms for the modified sequence πΊ, the terms are within 1 / π (without the constant πΆ). (Contributed by Jim Kingdon, 1-Aug-2021.) |
β’ (π β πΉ:ββΆβ) & β’ (π β πΆ β β+) & β’ (π β βπ β β βπ β (β€β₯βπ)((πΉβπ) < ((πΉβπ) + (πΆ / π)) β§ (πΉβπ) < ((πΉβπ) + (πΆ / π)))) & β’ πΊ = (π β β β¦ (πΉβ(π Β· π))) & β’ (π β π β β) & β’ (π β πΆ < π) β β’ (π β βπ β β βπ β (β€β₯βπ)((πΊβπ) < ((πΊβπ) + (1 / π)) β§ (πΊβπ) < ((πΊβπ) + (1 / π)))) | ||
Theorem | cvg1nlemres 10993* | Lemma for cvg1n 10994. The original sequence πΉ has a limit (turns out it is the same as the limit of the modified sequence πΊ). (Contributed by Jim Kingdon, 1-Aug-2021.) |
β’ (π β πΉ:ββΆβ) & β’ (π β πΆ β β+) & β’ (π β βπ β β βπ β (β€β₯βπ)((πΉβπ) < ((πΉβπ) + (πΆ / π)) β§ (πΉβπ) < ((πΉβπ) + (πΆ / π)))) & β’ πΊ = (π β β β¦ (πΉβ(π Β· π))) & β’ (π β π β β) & β’ (π β πΆ < π) β β’ (π β βπ¦ β β βπ₯ β β+ βπ β β βπ β (β€β₯βπ)((πΉβπ) < (π¦ + π₯) β§ π¦ < ((πΉβπ) + π₯))) | ||
Theorem | cvg1n 10994* |
Convergence of real sequences.
This is a version of caucvgre 10989 with a constant multiplier πΆ on the rate of convergence. That is, all terms after the nth term must be within πΆ / π of the nth term. (Contributed by Jim Kingdon, 1-Aug-2021.) |
β’ (π β πΉ:ββΆβ) & β’ (π β πΆ β β+) & β’ (π β βπ β β βπ β (β€β₯βπ)((πΉβπ) < ((πΉβπ) + (πΆ / π)) β§ (πΉβπ) < ((πΉβπ) + (πΆ / π)))) β β’ (π β βπ¦ β β βπ₯ β β+ βπ β β βπ β (β€β₯βπ)((πΉβπ) < (π¦ + π₯) β§ π¦ < ((πΉβπ) + π₯))) | ||
Theorem | uzin2 10995 | The upper integers are closed under intersection. (Contributed by Mario Carneiro, 24-Dec-2013.) |
β’ ((π΄ β ran β€β₯ β§ π΅ β ran β€β₯) β (π΄ β© π΅) β ran β€β₯) | ||
Theorem | rexanuz 10996* | Combine two different upper integer properties into one. (Contributed by Mario Carneiro, 25-Dec-2013.) |
β’ (βπ β β€ βπ β (β€β₯βπ)(π β§ π) β (βπ β β€ βπ β (β€β₯βπ)π β§ βπ β β€ βπ β (β€β₯βπ)π)) | ||
Theorem | rexfiuz 10997* | Combine finitely many different upper integer properties into one. (Contributed by Mario Carneiro, 6-Jun-2014.) |
β’ (π΄ β Fin β (βπ β β€ βπ β (β€β₯βπ)βπ β π΄ π β βπ β π΄ βπ β β€ βπ β (β€β₯βπ)π)) | ||
Theorem | rexuz3 10998* | Restrict the base of the upper integers set to another upper integers set. (Contributed by Mario Carneiro, 26-Dec-2013.) |
β’ π = (β€β₯βπ) β β’ (π β β€ β (βπ β π βπ β (β€β₯βπ)π β βπ β β€ βπ β (β€β₯βπ)π)) | ||
Theorem | rexanuz2 10999* | Combine two different upper integer properties into one. (Contributed by Mario Carneiro, 26-Dec-2013.) |
β’ π = (β€β₯βπ) β β’ (βπ β π βπ β (β€β₯βπ)(π β§ π) β (βπ β π βπ β (β€β₯βπ)π β§ βπ β π βπ β (β€β₯βπ)π)) | ||
Theorem | r19.29uz 11000* | A version of 19.29 1620 for upper integer quantifiers. (Contributed by Mario Carneiro, 10-Feb-2014.) |
β’ π = (β€β₯βπ) β β’ ((βπ β π π β§ βπ β π βπ β (β€β₯βπ)π) β βπ β π βπ β (β€β₯βπ)(π β§ π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |