![]() |
Intuitionistic Logic Explorer Theorem List (p. 111 of 148) | < 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 | ||
Syntax | cabs 11001 | Extend class notation to include a function for the absolute value (modulus) of a complex number. |
class abs | ||
Definition | df-rsqrt 11002* |
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 11003 | Define the function for the absolute value (modulus) of a complex number. (Contributed by NM, 27-Jul-1999.) |
⊢ abs = (𝑥 ∈ ℂ ↦ (√‘(𝑥 · (∗‘𝑥)))) | ||
Theorem | sqrtrval 11004* | Value of square root function. (Contributed by Jim Kingdon, 23-Aug-2020.) |
⊢ (𝐴 ∈ ℝ → (√‘𝐴) = (℩𝑥 ∈ ℝ ((𝑥↑2) = 𝐴 ∧ 0 ≤ 𝑥))) | ||
Theorem | absval 11005 | 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 11006 | A real number does not lie on the negative imaginary axis. (Contributed by Mario Carneiro, 8-Jul-2013.) |
⊢ (𝐴 ∈ ℝ → (i · 𝐴) ∉ ℝ+) | ||
Theorem | sqrt0rlem 11007 | Lemma for sqrt0 11008. (Contributed by Jim Kingdon, 26-Aug-2020.) |
⊢ ((𝐴 ∈ ℝ ∧ ((𝐴↑2) = 0 ∧ 0 ≤ 𝐴)) ↔ 𝐴 = 0) | ||
Theorem | sqrt0 11008 | Square root of zero. (Contributed by Mario Carneiro, 9-Jul-2013.) |
⊢ (√‘0) = 0 | ||
Theorem | resqrexlem1arp 11009 | Lemma for resqrex 11030. 1 + 𝐴 is a positive real (expressed in a way that will help apply seqf 10458 and similar theorems). (Contributed by Jim Kingdon, 28-Jul-2021.) (Revised by Jim Kingdon, 16-Oct-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) ⇒ ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → ((ℕ × {(1 + 𝐴)})‘𝑁) ∈ ℝ+) | ||
Theorem | resqrexlemp1rp 11010* | Lemma for resqrex 11030. Applying the recursion rule yields a positive real (expressed in a way that will help apply seqf 10458 and similar theorems). (Contributed by Jim Kingdon, 28-Jul-2021.) (Revised by Jim Kingdon, 16-Oct-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) ⇒ ⊢ ((𝜑 ∧ (𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+)) → (𝐵(𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2))𝐶) ∈ ℝ+) | ||
Theorem | resqrexlemf 11011* | Lemma for resqrex 11030. 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 11012* | Lemma for resqrex 11030. 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 11013* | Lemma for resqrex 11030. 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 11014* | Lemma for resqrex 11030. 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 11015* | Lemma for resqrex 11030. The sequence is decreasing. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.) |
⊢ 𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)})) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) ⇒ ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → (𝐹‘(𝑁 + 1)) < (𝐹‘𝑁)) | ||
Theorem | resqrexlemdecn 11016* | Lemma for resqrex 11030. The sequence is decreasing. (Contributed by Jim Kingdon, 31-Jul-2021.) |
⊢ 𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)})) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 < 𝑀) ⇒ ⊢ (𝜑 → (𝐹‘𝑀) < (𝐹‘𝑁)) | ||
Theorem | resqrexlemlo 11017* | Lemma for resqrex 11030. 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 11018* | Lemma for resqrex 11030. 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 11019* | Lemma for resqrex 11030. 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 11020* | Lemma for resqrex 11030. 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 11021* | Lemma for resqrex 11030. 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 11022* | Lemma for resqrex 11030. 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 11023* | Lemma for resqrex 11030. The sequence has a limit. (Contributed by Jim Kingdon, 6-Aug-2021.) |
⊢ 𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)})) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) ⇒ ⊢ (𝜑 → ∃𝑟 ∈ ℝ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝑟 + 𝑥) ∧ 𝑟 < ((𝐹‘𝑖) + 𝑥))) | ||
Theorem | resqrexlemgt0 11024* | Lemma for resqrex 11030. A limit is nonnegative. (Contributed by Jim Kingdon, 7-Aug-2021.) |
⊢ 𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)})) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐿 ∈ ℝ) & ⊢ (𝜑 → ∀𝑒 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝐿 + 𝑒) ∧ 𝐿 < ((𝐹‘𝑖) + 𝑒))) ⇒ ⊢ (𝜑 → 0 ≤ 𝐿) | ||
Theorem | resqrexlemoverl 11025* | Lemma for resqrex 11030. 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 11026* | Lemma for resqrex 11030. 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 11027* | Lemma for resqrex 11030. 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 11028* | Lemma for resqrex 11030. The square of a limit is 𝐴. (Contributed by Jim Kingdon, 7-Aug-2021.) |
⊢ 𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)})) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐿 ∈ ℝ) & ⊢ (𝜑 → ∀𝑒 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ≥‘𝑗)((𝐹‘𝑖) < (𝐿 + 𝑒) ∧ 𝐿 < ((𝐹‘𝑖) + 𝑒))) ⇒ ⊢ (𝜑 → (𝐿↑2) = 𝐴) | ||
Theorem | resqrexlemex 11029* | Lemma for resqrex 11030. 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 11030* | Existence of a square root for positive reals. (Contributed by Mario Carneiro, 9-Jul-2013.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ∃𝑥 ∈ ℝ (0 ≤ 𝑥 ∧ (𝑥↑2) = 𝐴)) | ||
Theorem | rsqrmo 11031* | Uniqueness for the square root function. (Contributed by Jim Kingdon, 10-Aug-2021.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ∃*𝑥 ∈ ℝ ((𝑥↑2) = 𝐴 ∧ 0 ≤ 𝑥)) | ||
Theorem | rersqreu 11032* | Existence and uniqueness for the real square root function. (Contributed by Jim Kingdon, 10-Aug-2021.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ∃!𝑥 ∈ ℝ ((𝑥↑2) = 𝐴 ∧ 0 ≤ 𝑥)) | ||
Theorem | resqrtcl 11033 | Closure of the square root function. (Contributed by Mario Carneiro, 9-Jul-2013.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (√‘𝐴) ∈ ℝ) | ||
Theorem | rersqrtthlem 11034 | Lemma for resqrtth 11035. (Contributed by Jim Kingdon, 10-Aug-2021.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (((√‘𝐴)↑2) = 𝐴 ∧ 0 ≤ (√‘𝐴))) | ||
Theorem | resqrtth 11035 | Square root theorem over the reals. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 9-Jul-2013.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ((√‘𝐴)↑2) = 𝐴) | ||
Theorem | remsqsqrt 11036 | Square of square root. (Contributed by Mario Carneiro, 10-Jul-2013.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ((√‘𝐴) · (√‘𝐴)) = 𝐴) | ||
Theorem | sqrtge0 11037 | 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 11038 | 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 11039 | Square root distributes over multiplication. (Contributed by NM, 30-Jul-1999.) (Revised by Mario Carneiro, 29-May-2016.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (√‘(𝐴 · 𝐵)) = ((√‘𝐴) · (√‘𝐵))) | ||
Theorem | sqrtle 11040 | Square root is monotonic. (Contributed by NM, 17-Mar-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 ≤ 𝐵 ↔ (√‘𝐴) ≤ (√‘𝐵))) | ||
Theorem | sqrtlt 11041 | Square root is strictly monotonic. Closed form of sqrtlti 11141. (Contributed by Scott Fenton, 17-Apr-2014.) (Proof shortened by Mario Carneiro, 29-May-2016.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 < 𝐵 ↔ (√‘𝐴) < (√‘𝐵))) | ||
Theorem | sqrt11ap 11042 | Analogue to sqrt11 11043 but for apartness. (Contributed by Jim Kingdon, 11-Aug-2021.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((√‘𝐴) # (√‘𝐵) ↔ 𝐴 # 𝐵)) | ||
Theorem | sqrt11 11043 | The square root function is one-to-one. Also see sqrt11ap 11042 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 11044 | 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 11045 | The square root of a positive real is a positive real. (Contributed by NM, 22-Feb-2008.) |
⊢ (𝐴 ∈ ℝ+ → (√‘𝐴) ∈ ℝ+) | ||
Theorem | sqrtdiv 11046 | Square root distributes over division. (Contributed by Mario Carneiro, 5-May-2016.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℝ+) → (√‘(𝐴 / 𝐵)) = ((√‘𝐴) / (√‘𝐵))) | ||
Theorem | sqrtsq2 11047 | Relationship between square root and squares. (Contributed by NM, 31-Jul-1999.) (Revised by Mario Carneiro, 29-May-2016.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((√‘𝐴) = 𝐵 ↔ 𝐴 = (𝐵↑2))) | ||
Theorem | sqrtsq 11048 | Square root of square. (Contributed by NM, 14-Jan-2006.) (Revised by Mario Carneiro, 29-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (√‘(𝐴↑2)) = 𝐴) | ||
Theorem | sqrtmsq 11049 | Square root of square. (Contributed by NM, 2-Aug-1999.) (Revised by Mario Carneiro, 29-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (√‘(𝐴 · 𝐴)) = 𝐴) | ||
Theorem | sqrt1 11050 | The square root of 1 is 1. (Contributed by NM, 31-Jul-1999.) |
⊢ (√‘1) = 1 | ||
Theorem | sqrt4 11051 | The square root of 4 is 2. (Contributed by NM, 3-Aug-1999.) |
⊢ (√‘4) = 2 | ||
Theorem | sqrt9 11052 | The square root of 9 is 3. (Contributed by NM, 11-May-2004.) |
⊢ (√‘9) = 3 | ||
Theorem | sqrt2gt1lt2 11053 | 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 11054 | Absolute value of negative. (Contributed by NM, 27-Feb-2005.) |
⊢ (𝐴 ∈ ℂ → (abs‘-𝐴) = (abs‘𝐴)) | ||
Theorem | abscl 11055 | Real closure of absolute value. (Contributed by NM, 3-Oct-1999.) |
⊢ (𝐴 ∈ ℂ → (abs‘𝐴) ∈ ℝ) | ||
Theorem | abscj 11056 | 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 11057 | Square of value of absolute value function. (Contributed by NM, 16-Jan-2006.) |
⊢ (𝐴 ∈ ℂ → ((abs‘𝐴)↑2) = (𝐴 · (∗‘𝐴))) | ||
Theorem | absvalsq2 11058 | Square of value of absolute value function. (Contributed by NM, 1-Feb-2007.) |
⊢ (𝐴 ∈ ℂ → ((abs‘𝐴)↑2) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2))) | ||
Theorem | sqabsadd 11059 | 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 11060 | Square of absolute value of difference. (Contributed by NM, 21-Jan-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((abs‘(𝐴 − 𝐵))↑2) = ((((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) − (2 · (ℜ‘(𝐴 · (∗‘𝐵)))))) | ||
Theorem | absval2 11061 | Value of absolute value function. Definition 10.36 of [Gleason] p. 133. (Contributed by NM, 17-Mar-2005.) |
⊢ (𝐴 ∈ ℂ → (abs‘𝐴) = (√‘(((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)))) | ||
Theorem | abs0 11062 | The absolute value of 0. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 29-May-2016.) |
⊢ (abs‘0) = 0 | ||
Theorem | absi 11063 | The absolute value of the imaginary unit. (Contributed by NM, 26-Mar-2005.) |
⊢ (abs‘i) = 1 | ||
Theorem | absge0 11064 | Absolute value is nonnegative. (Contributed by NM, 20-Nov-2004.) (Revised by Mario Carneiro, 29-May-2016.) |
⊢ (𝐴 ∈ ℂ → 0 ≤ (abs‘𝐴)) | ||
Theorem | absrpclap 11065 | The absolute value of a number apart from zero is a positive real. (Contributed by Jim Kingdon, 11-Aug-2021.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (abs‘𝐴) ∈ ℝ+) | ||
Theorem | abs00ap 11066 | 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 11067 | Strong extensionality for absolute value. (Contributed by Jim Kingdon, 12-Aug-2021.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((abs‘𝐴) # (abs‘𝐵) → 𝐴 # 𝐵)) | ||
Theorem | abs00 11068 | The absolute value of a number is zero iff the number is zero. Also see abs00ap 11066 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 11069 | A complex number is zero iff its absolute value is zero. Deduction form of abs00 11068. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → ((abs‘𝐴) = 0 ↔ 𝐴 = 0)) | ||
Theorem | abs00bd 11070 | If a complex number is zero, its absolute value is zero. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 = 0) ⇒ ⊢ (𝜑 → (abs‘𝐴) = 0) | ||
Theorem | absreimsq 11071 | 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 11072 | 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 11073 | 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 11074 | Absolute value distributes over division. (Contributed by Jim Kingdon, 11-Aug-2021.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → (abs‘(𝐴 / 𝐵)) = ((abs‘𝐴) / (abs‘𝐵))) | ||
Theorem | absid 11075 | 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 11076 | The absolute value of 1. Common special case. (Contributed by David A. Wheeler, 16-Jul-2016.) |
⊢ (abs‘1) = 1 | ||
Theorem | absnid 11077 | A negative number is the negative of its own absolute value. (Contributed by NM, 27-Feb-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≤ 0) → (abs‘𝐴) = -𝐴) | ||
Theorem | leabs 11078 | A real number is less than or equal to its absolute value. (Contributed by NM, 27-Feb-2005.) |
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ (abs‘𝐴)) | ||
Theorem | qabsor 11079 | 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 11080 | 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 11081 | Absolute value of a real number. (Contributed by NM, 17-Mar-2005.) |
⊢ (𝐴 ∈ ℝ → (abs‘𝐴) = (√‘(𝐴↑2))) | ||
Theorem | absresq 11082 | Square of the absolute value of a real number. (Contributed by NM, 16-Jan-2006.) |
⊢ (𝐴 ∈ ℝ → ((abs‘𝐴)↑2) = (𝐴↑2)) | ||
Theorem | absexp 11083 | Absolute value of positive integer exponentiation. (Contributed by NM, 5-Jan-2006.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (abs‘(𝐴↑𝑁)) = ((abs‘𝐴)↑𝑁)) | ||
Theorem | absexpzap 11084 | Absolute value of integer exponentiation. (Contributed by Jim Kingdon, 11-Aug-2021.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℤ) → (abs‘(𝐴↑𝑁)) = ((abs‘𝐴)↑𝑁)) | ||
Theorem | abssq 11085 | 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 11086 | 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 11087 | 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 11088 | 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 11089 | The absolute value of an integer is a nonnegative integer. (Contributed by NM, 27-Feb-2005.) |
⊢ (𝐴 ∈ ℤ → (abs‘𝐴) ∈ ℕ0) | ||
Theorem | zabscl 11090 | The absolute value of an integer is an integer. (Contributed by Stefan O'Rear, 24-Sep-2014.) |
⊢ (𝐴 ∈ ℤ → (abs‘𝐴) ∈ ℤ) | ||
Theorem | ltabs 11091 | A number which is less than its absolute value is negative. (Contributed by Jim Kingdon, 12-Aug-2021.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < (abs‘𝐴)) → 𝐴 < 0) | ||
Theorem | abslt 11092 | Absolute value and 'less than' relation. (Contributed by NM, 6-Apr-2005.) (Revised by Mario Carneiro, 29-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((abs‘𝐴) < 𝐵 ↔ (-𝐵 < 𝐴 ∧ 𝐴 < 𝐵))) | ||
Theorem | absle 11093 | 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 11094 | 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 11095 | If the absolute value of a complex number is less than a real, its difference from the real is nonzero. See also abssubap0 11094 which is the same with not equal changed to apart. (Contributed by NM, 2-Nov-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ (abs‘𝐴) < 𝐵) → (𝐵 − 𝐴) ≠ 0) | ||
Theorem | absdiflt 11096 | The absolute value of a difference and 'less than' relation. (Contributed by Paul Chapman, 18-Sep-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((abs‘(𝐴 − 𝐵)) < 𝐶 ↔ ((𝐵 − 𝐶) < 𝐴 ∧ 𝐴 < (𝐵 + 𝐶)))) | ||
Theorem | absdifle 11097 | The absolute value of a difference and 'less than or equal to' relation. (Contributed by Paul Chapman, 18-Sep-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((abs‘(𝐴 − 𝐵)) ≤ 𝐶 ↔ ((𝐵 − 𝐶) ≤ 𝐴 ∧ 𝐴 ≤ (𝐵 + 𝐶)))) | ||
Theorem | elicc4abs 11098 | Membership in a symmetric closed real interval. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶 ∈ ((𝐴 − 𝐵)[,](𝐴 + 𝐵)) ↔ (abs‘(𝐶 − 𝐴)) ≤ 𝐵)) | ||
Theorem | lenegsq 11099 | Comparison to a nonnegative number based on comparison to squares. (Contributed by NM, 16-Jan-2006.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) → ((𝐴 ≤ 𝐵 ∧ -𝐴 ≤ 𝐵) ↔ (𝐴↑2) ≤ (𝐵↑2))) | ||
Theorem | releabs 11100 | The real part of a number is less than or equal to its absolute value. Proposition 10-3.7(d) of [Gleason] p. 133. (Contributed by NM, 1-Apr-2005.) |
⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) ≤ (abs‘𝐴)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |