![]() |
Intuitionistic Logic Explorer Theorem List (p. 111 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 | r19.29uz 11001* | A version of 19.29 1620 for upper integer quantifiers. (Contributed by Mario Carneiro, 10-Feb-2014.) |
β’ π = (β€β₯βπ) β β’ ((βπ β π π β§ βπ β π βπ β (β€β₯βπ)π) β βπ β π βπ β (β€β₯βπ)(π β§ π)) | ||
Theorem | r19.2uz 11002* | A version of r19.2m 3510 for upper integer quantifiers. (Contributed by Mario Carneiro, 15-Feb-2014.) |
β’ π = (β€β₯βπ) β β’ (βπ β π βπ β (β€β₯βπ)π β βπ β π π) | ||
Theorem | recvguniqlem 11003 | Lemma for recvguniq 11004. Some of the rearrangements of the expressions. (Contributed by Jim Kingdon, 8-Aug-2021.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΎ β β) & β’ (π β π΄ < ((πΉβπΎ) + ((π΄ β π΅) / 2))) & β’ (π β (πΉβπΎ) < (π΅ + ((π΄ β π΅) / 2))) β β’ (π β β₯) | ||
Theorem | recvguniq 11004* | Limits are unique. (Contributed by Jim Kingdon, 7-Aug-2021.) |
β’ (π β πΉ:ββΆβ) & β’ (π β πΏ β β) & β’ (π β βπ₯ β β+ βπ β β βπ β (β€β₯βπ)((πΉβπ) < (πΏ + π₯) β§ πΏ < ((πΉβπ) + π₯))) & β’ (π β π β β) & β’ (π β βπ₯ β β+ βπ β β βπ β (β€β₯βπ)((πΉβπ) < (π + π₯) β§ π < ((πΉβπ) + π₯))) β β’ (π β πΏ = π) | ||
Syntax | csqrt 11005 | Extend class notation to include square root of a complex number. |
class β | ||
Syntax | cabs 11006 | Extend class notation to include a function for the absolute value (modulus) of a complex number. |
class abs | ||
Definition | df-rsqrt 11007* |
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.) |
β’ β = (π₯ β β β¦ (β©π¦ β β ((π¦β2) = π₯ β§ 0 β€ π¦))) | ||
Definition | df-abs 11008 | Define the function for the absolute value (modulus) of a complex number. (Contributed by NM, 27-Jul-1999.) |
β’ abs = (π₯ β β β¦ (ββ(π₯ Β· (ββπ₯)))) | ||
Theorem | sqrtrval 11009* | Value of square root function. (Contributed by Jim Kingdon, 23-Aug-2020.) |
β’ (π΄ β β β (ββπ΄) = (β©π₯ β β ((π₯β2) = π΄ β§ 0 β€ π₯))) | ||
Theorem | absval 11010 | 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.) |
β’ (π΄ β β β (absβπ΄) = (ββ(π΄ Β· (ββπ΄)))) | ||
Theorem | rennim 11011 | A real number does not lie on the negative imaginary axis. (Contributed by Mario Carneiro, 8-Jul-2013.) |
β’ (π΄ β β β (i Β· π΄) β β+) | ||
Theorem | sqrt0rlem 11012 | Lemma for sqrt0 11013. (Contributed by Jim Kingdon, 26-Aug-2020.) |
β’ ((π΄ β β β§ ((π΄β2) = 0 β§ 0 β€ π΄)) β π΄ = 0) | ||
Theorem | sqrt0 11013 | Square root of zero. (Contributed by Mario Carneiro, 9-Jul-2013.) |
β’ (ββ0) = 0 | ||
Theorem | resqrexlem1arp 11014 | Lemma for resqrex 11035. 1 + π΄ is a positive real (expressed in a way that will help apply seqf 10461 and similar theorems). (Contributed by Jim Kingdon, 28-Jul-2021.) (Revised by Jim Kingdon, 16-Oct-2022.) |
β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) β β’ ((π β§ π β β) β ((β Γ {(1 + π΄)})βπ) β β+) | ||
Theorem | resqrexlemp1rp 11015* | Lemma for resqrex 11035. Applying the recursion rule yields a positive real (expressed in a way that will help apply seqf 10461 and similar theorems). (Contributed by Jim Kingdon, 28-Jul-2021.) (Revised by Jim Kingdon, 16-Oct-2022.) |
β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) β β’ ((π β§ (π΅ β β+ β§ πΆ β β+)) β (π΅(π¦ β β+, π§ β β+ β¦ ((π¦ + (π΄ / π¦)) / 2))πΆ) β β+) | ||
Theorem | resqrexlemf 11016* | Lemma for resqrex 11035. The sequence is a function. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.) (Revised by Jim Kingdon, 16-Oct-2022.) |
β’ πΉ = seq1((π¦ β β+, π§ β β+ β¦ ((π¦ + (π΄ / π¦)) / 2)), (β Γ {(1 + π΄)})) & β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) β β’ (π β πΉ:ββΆβ+) | ||
Theorem | resqrexlemf1 11017* | Lemma for resqrex 11035. 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.) |
β’ πΉ = seq1((π¦ β β+, π§ β β+ β¦ ((π¦ + (π΄ / π¦)) / 2)), (β Γ {(1 + π΄)})) & β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) β β’ (π β (πΉβ1) = (1 + π΄)) | ||
Theorem | resqrexlemfp1 11018* | Lemma for resqrex 11035. 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.) |
β’ πΉ = seq1((π¦ β β+, π§ β β+ β¦ ((π¦ + (π΄ / π¦)) / 2)), (β Γ {(1 + π΄)})) & β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) β β’ ((π β§ π β β) β (πΉβ(π + 1)) = (((πΉβπ) + (π΄ / (πΉβπ))) / 2)) | ||
Theorem | resqrexlemover 11019* | Lemma for resqrex 11035. Each element of the sequence is an overestimate. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.) |
β’ πΉ = seq1((π¦ β β+, π§ β β+ β¦ ((π¦ + (π΄ / π¦)) / 2)), (β Γ {(1 + π΄)})) & β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) β β’ ((π β§ π β β) β π΄ < ((πΉβπ)β2)) | ||
Theorem | resqrexlemdec 11020* | Lemma for resqrex 11035. The sequence is decreasing. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.) |
β’ πΉ = seq1((π¦ β β+, π§ β β+ β¦ ((π¦ + (π΄ / π¦)) / 2)), (β Γ {(1 + π΄)})) & β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) β β’ ((π β§ π β β) β (πΉβ(π + 1)) < (πΉβπ)) | ||
Theorem | resqrexlemdecn 11021* | Lemma for resqrex 11035. The sequence is decreasing. (Contributed by Jim Kingdon, 31-Jul-2021.) |
β’ πΉ = seq1((π¦ β β+, π§ β β+ β¦ ((π¦ + (π΄ / π¦)) / 2)), (β Γ {(1 + π΄)})) & β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β π < π) β β’ (π β (πΉβπ) < (πΉβπ)) | ||
Theorem | resqrexlemlo 11022* | Lemma for resqrex 11035. A (variable) lower bound for each term of the sequence. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.) |
β’ πΉ = seq1((π¦ β β+, π§ β β+ β¦ ((π¦ + (π΄ / π¦)) / 2)), (β Γ {(1 + π΄)})) & β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) β β’ ((π β§ π β β) β (1 / (2βπ)) < (πΉβπ)) | ||
Theorem | resqrexlemcalc1 11023* | Lemma for resqrex 11035. Some of the calculations involved in showing that the sequence converges. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.) |
β’ πΉ = seq1((π¦ β β+, π§ β β+ β¦ ((π¦ + (π΄ / π¦)) / 2)), (β Γ {(1 + π΄)})) & β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) β β’ ((π β§ π β β) β (((πΉβ(π + 1))β2) β π΄) = (((((πΉβπ)β2) β π΄)β2) / (4 Β· ((πΉβπ)β2)))) | ||
Theorem | resqrexlemcalc2 11024* | Lemma for resqrex 11035. Some of the calculations involved in showing that the sequence converges. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.) |
β’ πΉ = seq1((π¦ β β+, π§ β β+ β¦ ((π¦ + (π΄ / π¦)) / 2)), (β Γ {(1 + π΄)})) & β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) β β’ ((π β§ π β β) β (((πΉβ(π + 1))β2) β π΄) β€ ((((πΉβπ)β2) β π΄) / 4)) | ||
Theorem | resqrexlemcalc3 11025* | Lemma for resqrex 11035. Some of the calculations involved in showing that the sequence converges. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.) |
β’ πΉ = seq1((π¦ β β+, π§ β β+ β¦ ((π¦ + (π΄ / π¦)) / 2)), (β Γ {(1 + π΄)})) & β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) β β’ ((π β§ π β β) β (((πΉβπ)β2) β π΄) β€ (((πΉβ1)β2) / (4β(π β 1)))) | ||
Theorem | resqrexlemnmsq 11026* | Lemma for resqrex 11035. The difference between the squares of two terms of the sequence. (Contributed by Mario Carneiro and Jim Kingdon, 30-Jul-2021.) |
β’ πΉ = seq1((π¦ β β+, π§ β β+ β¦ ((π¦ + (π΄ / π¦)) / 2)), (β Γ {(1 + π΄)})) & β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β€ π) β β’ (π β (((πΉβπ)β2) β ((πΉβπ)β2)) < (((πΉβ1)β2) / (4β(π β 1)))) | ||
Theorem | resqrexlemnm 11027* | Lemma for resqrex 11035. The difference between two terms of the sequence. (Contributed by Mario Carneiro and Jim Kingdon, 31-Jul-2021.) |
β’ πΉ = seq1((π¦ β β+, π§ β β+ β¦ ((π¦ + (π΄ / π¦)) / 2)), (β Γ {(1 + π΄)})) & β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β€ π) β β’ (π β ((πΉβπ) β (πΉβπ)) < ((((πΉβ1)β2) Β· 2) / (2β(π β 1)))) | ||
Theorem | resqrexlemcvg 11028* | Lemma for resqrex 11035. The sequence has a limit. (Contributed by Jim Kingdon, 6-Aug-2021.) |
β’ πΉ = seq1((π¦ β β+, π§ β β+ β¦ ((π¦ + (π΄ / π¦)) / 2)), (β Γ {(1 + π΄)})) & β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) β β’ (π β βπ β β βπ₯ β β+ βπ β β βπ β (β€β₯βπ)((πΉβπ) < (π + π₯) β§ π < ((πΉβπ) + π₯))) | ||
Theorem | resqrexlemgt0 11029* | Lemma for resqrex 11035. A limit is nonnegative. (Contributed by Jim Kingdon, 7-Aug-2021.) |
β’ πΉ = seq1((π¦ β β+, π§ β β+ β¦ ((π¦ + (π΄ / π¦)) / 2)), (β Γ {(1 + π΄)})) & β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) & β’ (π β πΏ β β) & β’ (π β βπ β β+ βπ β β βπ β (β€β₯βπ)((πΉβπ) < (πΏ + π) β§ πΏ < ((πΉβπ) + π))) β β’ (π β 0 β€ πΏ) | ||
Theorem | resqrexlemoverl 11030* | Lemma for resqrex 11035. Every term in the sequence is an overestimate compared with the limit πΏ. 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.) |
β’ πΉ = seq1((π¦ β β+, π§ β β+ β¦ ((π¦ + (π΄ / π¦)) / 2)), (β Γ {(1 + π΄)})) & β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) & β’ (π β πΏ β β) & β’ (π β βπ β β+ βπ β β βπ β (β€β₯βπ)((πΉβπ) < (πΏ + π) β§ πΏ < ((πΉβπ) + π))) & β’ (π β πΎ β β) β β’ (π β πΏ β€ (πΉβπΎ)) | ||
Theorem | resqrexlemglsq 11031* | Lemma for resqrex 11035. The sequence formed by squaring each term of πΉ converges to (πΏβ2). (Contributed by Mario Carneiro and Jim Kingdon, 8-Aug-2021.) |
β’ πΉ = seq1((π¦ β β+, π§ β β+ β¦ ((π¦ + (π΄ / π¦)) / 2)), (β Γ {(1 + π΄)})) & β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) & β’ (π β πΏ β β) & β’ (π β βπ β β+ βπ β β βπ β (β€β₯βπ)((πΉβπ) < (πΏ + π) β§ πΏ < ((πΉβπ) + π))) & β’ πΊ = (π₯ β β β¦ ((πΉβπ₯)β2)) β β’ (π β βπ β β+ βπ β β βπ β (β€β₯βπ)((πΊβπ) < ((πΏβ2) + π) β§ (πΏβ2) < ((πΊβπ) + π))) | ||
Theorem | resqrexlemga 11032* | Lemma for resqrex 11035. The sequence formed by squaring each term of πΉ converges to π΄. (Contributed by Mario Carneiro and Jim Kingdon, 8-Aug-2021.) |
β’ πΉ = seq1((π¦ β β+, π§ β β+ β¦ ((π¦ + (π΄ / π¦)) / 2)), (β Γ {(1 + π΄)})) & β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) & β’ (π β πΏ β β) & β’ (π β βπ β β+ βπ β β βπ β (β€β₯βπ)((πΉβπ) < (πΏ + π) β§ πΏ < ((πΉβπ) + π))) & β’ πΊ = (π₯ β β β¦ ((πΉβπ₯)β2)) β β’ (π β βπ β β+ βπ β β βπ β (β€β₯βπ)((πΊβπ) < (π΄ + π) β§ π΄ < ((πΊβπ) + π))) | ||
Theorem | resqrexlemsqa 11033* | Lemma for resqrex 11035. The square of a limit is π΄. (Contributed by Jim Kingdon, 7-Aug-2021.) |
β’ πΉ = seq1((π¦ β β+, π§ β β+ β¦ ((π¦ + (π΄ / π¦)) / 2)), (β Γ {(1 + π΄)})) & β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) & β’ (π β πΏ β β) & β’ (π β βπ β β+ βπ β β βπ β (β€β₯βπ)((πΉβπ) < (πΏ + π) β§ πΏ < ((πΉβπ) + π))) β β’ (π β (πΏβ2) = π΄) | ||
Theorem | resqrexlemex 11034* | Lemma for resqrex 11035. Existence of square root given a sequence which converges to the square root. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.) |
β’ πΉ = seq1((π¦ β β+, π§ β β+ β¦ ((π¦ + (π΄ / π¦)) / 2)), (β Γ {(1 + π΄)})) & β’ (π β π΄ β β) & β’ (π β 0 β€ π΄) β β’ (π β βπ₯ β β (0 β€ π₯ β§ (π₯β2) = π΄)) | ||
Theorem | resqrex 11035* | Existence of a square root for positive reals. (Contributed by Mario Carneiro, 9-Jul-2013.) |
β’ ((π΄ β β β§ 0 β€ π΄) β βπ₯ β β (0 β€ π₯ β§ (π₯β2) = π΄)) | ||
Theorem | rsqrmo 11036* | Uniqueness for the square root function. (Contributed by Jim Kingdon, 10-Aug-2021.) |
β’ ((π΄ β β β§ 0 β€ π΄) β β*π₯ β β ((π₯β2) = π΄ β§ 0 β€ π₯)) | ||
Theorem | rersqreu 11037* | Existence and uniqueness for the real square root function. (Contributed by Jim Kingdon, 10-Aug-2021.) |
β’ ((π΄ β β β§ 0 β€ π΄) β β!π₯ β β ((π₯β2) = π΄ β§ 0 β€ π₯)) | ||
Theorem | resqrtcl 11038 | Closure of the square root function. (Contributed by Mario Carneiro, 9-Jul-2013.) |
β’ ((π΄ β β β§ 0 β€ π΄) β (ββπ΄) β β) | ||
Theorem | rersqrtthlem 11039 | Lemma for resqrtth 11040. (Contributed by Jim Kingdon, 10-Aug-2021.) |
β’ ((π΄ β β β§ 0 β€ π΄) β (((ββπ΄)β2) = π΄ β§ 0 β€ (ββπ΄))) | ||
Theorem | resqrtth 11040 | Square root theorem over the reals. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 9-Jul-2013.) |
β’ ((π΄ β β β§ 0 β€ π΄) β ((ββπ΄)β2) = π΄) | ||
Theorem | remsqsqrt 11041 | Square of square root. (Contributed by Mario Carneiro, 10-Jul-2013.) |
β’ ((π΄ β β β§ 0 β€ π΄) β ((ββπ΄) Β· (ββπ΄)) = π΄) | ||
Theorem | sqrtge0 11042 | The square root function is nonnegative for nonnegative input. (Contributed by NM, 26-May-1999.) (Revised by Mario Carneiro, 9-Jul-2013.) |
β’ ((π΄ β β β§ 0 β€ π΄) β 0 β€ (ββπ΄)) | ||
Theorem | sqrtgt0 11043 | The square root function is positive for positive input. (Contributed by Mario Carneiro, 10-Jul-2013.) (Revised by Mario Carneiro, 6-Sep-2013.) |
β’ ((π΄ β β β§ 0 < π΄) β 0 < (ββπ΄)) | ||
Theorem | sqrtmul 11044 | Square root distributes over multiplication. (Contributed by NM, 30-Jul-1999.) (Revised by Mario Carneiro, 29-May-2016.) |
β’ (((π΄ β β β§ 0 β€ π΄) β§ (π΅ β β β§ 0 β€ π΅)) β (ββ(π΄ Β· π΅)) = ((ββπ΄) Β· (ββπ΅))) | ||
Theorem | sqrtle 11045 | Square root is monotonic. (Contributed by NM, 17-Mar-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
β’ (((π΄ β β β§ 0 β€ π΄) β§ (π΅ β β β§ 0 β€ π΅)) β (π΄ β€ π΅ β (ββπ΄) β€ (ββπ΅))) | ||
Theorem | sqrtlt 11046 | Square root is strictly monotonic. Closed form of sqrtlti 11146. (Contributed by Scott Fenton, 17-Apr-2014.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
β’ (((π΄ β β β§ 0 β€ π΄) β§ (π΅ β β β§ 0 β€ π΅)) β (π΄ < π΅ β (ββπ΄) < (ββπ΅))) | ||
Theorem | sqrt11ap 11047 | Analogue to sqrt11 11048 but for apartness. (Contributed by Jim Kingdon, 11-Aug-2021.) |
β’ (((π΄ β β β§ 0 β€ π΄) β§ (π΅ β β β§ 0 β€ π΅)) β ((ββπ΄) # (ββπ΅) β π΄ # π΅)) | ||
Theorem | sqrt11 11048 | The square root function is one-to-one. Also see sqrt11ap 11047 which would follow easily from this given excluded middle, but which is proved another way without it. (Contributed by Scott Fenton, 11-Jun-2013.) |
β’ (((π΄ β β β§ 0 β€ π΄) β§ (π΅ β β β§ 0 β€ π΅)) β ((ββπ΄) = (ββπ΅) β π΄ = π΅)) | ||
Theorem | sqrt00 11049 | A square root is zero iff its argument is 0. (Contributed by NM, 27-Jul-1999.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
β’ ((π΄ β β β§ 0 β€ π΄) β ((ββπ΄) = 0 β π΄ = 0)) | ||
Theorem | rpsqrtcl 11050 | The square root of a positive real is a positive real. (Contributed by NM, 22-Feb-2008.) |
β’ (π΄ β β+ β (ββπ΄) β β+) | ||
Theorem | sqrtdiv 11051 | Square root distributes over division. (Contributed by Mario Carneiro, 5-May-2016.) |
β’ (((π΄ β β β§ 0 β€ π΄) β§ π΅ β β+) β (ββ(π΄ / π΅)) = ((ββπ΄) / (ββπ΅))) | ||
Theorem | sqrtsq2 11052 | Relationship between square root and squares. (Contributed by NM, 31-Jul-1999.) (Revised by Mario Carneiro, 29-May-2016.) |
β’ (((π΄ β β β§ 0 β€ π΄) β§ (π΅ β β β§ 0 β€ π΅)) β ((ββπ΄) = π΅ β π΄ = (π΅β2))) | ||
Theorem | sqrtsq 11053 | Square root of square. (Contributed by NM, 14-Jan-2006.) (Revised by Mario Carneiro, 29-May-2016.) |
β’ ((π΄ β β β§ 0 β€ π΄) β (ββ(π΄β2)) = π΄) | ||
Theorem | sqrtmsq 11054 | Square root of square. (Contributed by NM, 2-Aug-1999.) (Revised by Mario Carneiro, 29-May-2016.) |
β’ ((π΄ β β β§ 0 β€ π΄) β (ββ(π΄ Β· π΄)) = π΄) | ||
Theorem | sqrt1 11055 | The square root of 1 is 1. (Contributed by NM, 31-Jul-1999.) |
β’ (ββ1) = 1 | ||
Theorem | sqrt4 11056 | The square root of 4 is 2. (Contributed by NM, 3-Aug-1999.) |
β’ (ββ4) = 2 | ||
Theorem | sqrt9 11057 | The square root of 9 is 3. (Contributed by NM, 11-May-2004.) |
β’ (ββ9) = 3 | ||
Theorem | sqrt2gt1lt2 11058 | The square root of 2 is bounded by 1 and 2. (Contributed by Roy F. Longton, 8-Aug-2005.) (Revised by Mario Carneiro, 6-Sep-2013.) |
β’ (1 < (ββ2) β§ (ββ2) < 2) | ||
Theorem | absneg 11059 | Absolute value of negative. (Contributed by NM, 27-Feb-2005.) |
β’ (π΄ β β β (absβ-π΄) = (absβπ΄)) | ||
Theorem | abscl 11060 | Real closure of absolute value. (Contributed by NM, 3-Oct-1999.) |
β’ (π΄ β β β (absβπ΄) β β) | ||
Theorem | abscj 11061 | The absolute value of a number and its conjugate are the same. Proposition 10-3.7(b) of [Gleason] p. 133. (Contributed by NM, 28-Apr-2005.) |
β’ (π΄ β β β (absβ(ββπ΄)) = (absβπ΄)) | ||
Theorem | absvalsq 11062 | Square of value of absolute value function. (Contributed by NM, 16-Jan-2006.) |
β’ (π΄ β β β ((absβπ΄)β2) = (π΄ Β· (ββπ΄))) | ||
Theorem | absvalsq2 11063 | Square of value of absolute value function. (Contributed by NM, 1-Feb-2007.) |
β’ (π΄ β β β ((absβπ΄)β2) = (((ββπ΄)β2) + ((ββπ΄)β2))) | ||
Theorem | sqabsadd 11064 | Square of absolute value of sum. Proposition 10-3.7(g) of [Gleason] p. 133. (Contributed by NM, 21-Jan-2007.) |
β’ ((π΄ β β β§ π΅ β β) β ((absβ(π΄ + π΅))β2) = ((((absβπ΄)β2) + ((absβπ΅)β2)) + (2 Β· (ββ(π΄ Β· (ββπ΅)))))) | ||
Theorem | sqabssub 11065 | Square of absolute value of difference. (Contributed by NM, 21-Jan-2007.) |
β’ ((π΄ β β β§ π΅ β β) β ((absβ(π΄ β π΅))β2) = ((((absβπ΄)β2) + ((absβπ΅)β2)) β (2 Β· (ββ(π΄ Β· (ββπ΅)))))) | ||
Theorem | absval2 11066 | Value of absolute value function. Definition 10.36 of [Gleason] p. 133. (Contributed by NM, 17-Mar-2005.) |
β’ (π΄ β β β (absβπ΄) = (ββ(((ββπ΄)β2) + ((ββπ΄)β2)))) | ||
Theorem | abs0 11067 | The absolute value of 0. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 29-May-2016.) |
β’ (absβ0) = 0 | ||
Theorem | absi 11068 | The absolute value of the imaginary unit. (Contributed by NM, 26-Mar-2005.) |
β’ (absβi) = 1 | ||
Theorem | absge0 11069 | Absolute value is nonnegative. (Contributed by NM, 20-Nov-2004.) (Revised by Mario Carneiro, 29-May-2016.) |
β’ (π΄ β β β 0 β€ (absβπ΄)) | ||
Theorem | absrpclap 11070 | The absolute value of a number apart from zero is a positive real. (Contributed by Jim Kingdon, 11-Aug-2021.) |
β’ ((π΄ β β β§ π΄ # 0) β (absβπ΄) β β+) | ||
Theorem | abs00ap 11071 | The absolute value of a number is apart from zero iff the number is apart from zero. (Contributed by Jim Kingdon, 11-Aug-2021.) |
β’ (π΄ β β β ((absβπ΄) # 0 β π΄ # 0)) | ||
Theorem | absext 11072 | Strong extensionality for absolute value. (Contributed by Jim Kingdon, 12-Aug-2021.) |
β’ ((π΄ β β β§ π΅ β β) β ((absβπ΄) # (absβπ΅) β π΄ # π΅)) | ||
Theorem | abs00 11073 | The absolute value of a number is zero iff the number is zero. Also see abs00ap 11071 which is similar but for apartness. Proposition 10-3.7(c) of [Gleason] p. 133. (Contributed by NM, 26-Sep-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
β’ (π΄ β β β ((absβπ΄) = 0 β π΄ = 0)) | ||
Theorem | abs00ad 11074 | A complex number is zero iff its absolute value is zero. Deduction form of abs00 11073. (Contributed by David Moews, 28-Feb-2017.) |
β’ (π β π΄ β β) β β’ (π β ((absβπ΄) = 0 β π΄ = 0)) | ||
Theorem | abs00bd 11075 | If a complex number is zero, its absolute value is zero. (Contributed by David Moews, 28-Feb-2017.) |
β’ (π β π΄ = 0) β β’ (π β (absβπ΄) = 0) | ||
Theorem | absreimsq 11076 | Square of the absolute value of a number that has been decomposed into real and imaginary parts. (Contributed by NM, 1-Feb-2007.) |
β’ ((π΄ β β β§ π΅ β β) β ((absβ(π΄ + (i Β· π΅)))β2) = ((π΄β2) + (π΅β2))) | ||
Theorem | absreim 11077 | Absolute value of a number that has been decomposed into real and imaginary parts. (Contributed by NM, 14-Jan-2006.) |
β’ ((π΄ β β β§ π΅ β β) β (absβ(π΄ + (i Β· π΅))) = (ββ((π΄β2) + (π΅β2)))) | ||
Theorem | absmul 11078 | Absolute value distributes over multiplication. Proposition 10-3.7(f) of [Gleason] p. 133. (Contributed by NM, 11-Oct-1999.) (Revised by Mario Carneiro, 29-May-2016.) |
β’ ((π΄ β β β§ π΅ β β) β (absβ(π΄ Β· π΅)) = ((absβπ΄) Β· (absβπ΅))) | ||
Theorem | absdivap 11079 | Absolute value distributes over division. (Contributed by Jim Kingdon, 11-Aug-2021.) |
β’ ((π΄ β β β§ π΅ β β β§ π΅ # 0) β (absβ(π΄ / π΅)) = ((absβπ΄) / (absβπ΅))) | ||
Theorem | absid 11080 | A nonnegative number is its own absolute value. (Contributed by NM, 11-Oct-1999.) (Revised by Mario Carneiro, 29-May-2016.) |
β’ ((π΄ β β β§ 0 β€ π΄) β (absβπ΄) = π΄) | ||
Theorem | abs1 11081 | The absolute value of 1. Common special case. (Contributed by David A. Wheeler, 16-Jul-2016.) |
β’ (absβ1) = 1 | ||
Theorem | absnid 11082 | A negative number is the negative of its own absolute value. (Contributed by NM, 27-Feb-2005.) |
β’ ((π΄ β β β§ π΄ β€ 0) β (absβπ΄) = -π΄) | ||
Theorem | leabs 11083 | A real number is less than or equal to its absolute value. (Contributed by NM, 27-Feb-2005.) |
β’ (π΄ β β β π΄ β€ (absβπ΄)) | ||
Theorem | qabsor 11084 | The absolute value of a rational number is either that number or its negative. (Contributed by Jim Kingdon, 8-Nov-2021.) |
β’ (π΄ β β β ((absβπ΄) = π΄ β¨ (absβπ΄) = -π΄)) | ||
Theorem | qabsord 11085 | The absolute value of a rational number is either that number or its negative. (Contributed by Jim Kingdon, 8-Nov-2021.) |
β’ (π β π΄ β β) β β’ (π β ((absβπ΄) = π΄ β¨ (absβπ΄) = -π΄)) | ||
Theorem | absre 11086 | Absolute value of a real number. (Contributed by NM, 17-Mar-2005.) |
β’ (π΄ β β β (absβπ΄) = (ββ(π΄β2))) | ||
Theorem | absresq 11087 | Square of the absolute value of a real number. (Contributed by NM, 16-Jan-2006.) |
β’ (π΄ β β β ((absβπ΄)β2) = (π΄β2)) | ||
Theorem | absexp 11088 | Absolute value of positive integer exponentiation. (Contributed by NM, 5-Jan-2006.) |
β’ ((π΄ β β β§ π β β0) β (absβ(π΄βπ)) = ((absβπ΄)βπ)) | ||
Theorem | absexpzap 11089 | Absolute value of integer exponentiation. (Contributed by Jim Kingdon, 11-Aug-2021.) |
β’ ((π΄ β β β§ π΄ # 0 β§ π β β€) β (absβ(π΄βπ)) = ((absβπ΄)βπ)) | ||
Theorem | abssq 11090 | Square can be moved in and out of absolute value. (Contributed by Scott Fenton, 18-Apr-2014.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
β’ (π΄ β β β ((absβπ΄)β2) = (absβ(π΄β2))) | ||
Theorem | sqabs 11091 | The squares of two reals are equal iff their absolute values are equal. (Contributed by NM, 6-Mar-2009.) |
β’ ((π΄ β β β§ π΅ β β) β ((π΄β2) = (π΅β2) β (absβπ΄) = (absβπ΅))) | ||
Theorem | absrele 11092 | The absolute value of a complex number is greater than or equal to the absolute value of its real part. (Contributed by NM, 1-Apr-2005.) |
β’ (π΄ β β β (absβ(ββπ΄)) β€ (absβπ΄)) | ||
Theorem | absimle 11093 | The absolute value of a complex number is greater than or equal to the absolute value of its imaginary part. (Contributed by NM, 17-Mar-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
β’ (π΄ β β β (absβ(ββπ΄)) β€ (absβπ΄)) | ||
Theorem | nn0abscl 11094 | The absolute value of an integer is a nonnegative integer. (Contributed by NM, 27-Feb-2005.) |
β’ (π΄ β β€ β (absβπ΄) β β0) | ||
Theorem | zabscl 11095 | The absolute value of an integer is an integer. (Contributed by Stefan O'Rear, 24-Sep-2014.) |
β’ (π΄ β β€ β (absβπ΄) β β€) | ||
Theorem | ltabs 11096 | A number which is less than its absolute value is negative. (Contributed by Jim Kingdon, 12-Aug-2021.) |
β’ ((π΄ β β β§ π΄ < (absβπ΄)) β π΄ < 0) | ||
Theorem | abslt 11097 | Absolute value and 'less than' relation. (Contributed by NM, 6-Apr-2005.) (Revised by Mario Carneiro, 29-May-2016.) |
β’ ((π΄ β β β§ π΅ β β) β ((absβπ΄) < π΅ β (-π΅ < π΄ β§ π΄ < π΅))) | ||
Theorem | absle 11098 | Absolute value and 'less than or equal to' relation. (Contributed by NM, 6-Apr-2005.) (Revised by Mario Carneiro, 29-May-2016.) |
β’ ((π΄ β β β§ π΅ β β) β ((absβπ΄) β€ π΅ β (-π΅ β€ π΄ β§ π΄ β€ π΅))) | ||
Theorem | abssubap0 11099 | If the absolute value of a complex number is less than a real, its difference from the real is apart from zero. (Contributed by Jim Kingdon, 12-Aug-2021.) |
β’ ((π΄ β β β§ π΅ β β β§ (absβπ΄) < π΅) β (π΅ β π΄) # 0) | ||
Theorem | abssubne0 11100 | If the absolute value of a complex number is less than a real, its difference from the real is nonzero. See also abssubap0 11099 which is the same with not equal changed to apart. (Contributed by NM, 2-Nov-2007.) |
β’ ((π΄ β β β§ π΅ β β β§ (absβπ΄) < π΅) β (π΅ β π΄) β 0) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |