Theorem List for Intuitionistic Logic Explorer - 9901-10000 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | resqrexlemcalc2 9901* |
Lemma for resqrex 9912. 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 9902* |
Lemma for resqrex 9912. 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 9903* |
Lemma for resqrex 9912. 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 9904* |
Lemma for resqrex 9912. 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 9905* |
Lemma for resqrex 9912. The sequence has a limit. (Contributed by
Jim
Kingdon, 6-Aug-2021.)
|
⊢ 𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+
↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}),
ℝ+)
& ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) ⇒ ⊢ (𝜑 → ∃𝑟 ∈ ℝ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑖 ∈
(ℤ≥‘𝑗)((𝐹‘𝑖) < (𝑟 + 𝑥) ∧ 𝑟 < ((𝐹‘𝑖) + 𝑥))) |
|
Theorem | resqrexlemgt0 9906* |
Lemma for resqrex 9912. A limit is nonnegative. (Contributed by
Jim
Kingdon, 7-Aug-2021.)
|
⊢ 𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+
↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}),
ℝ+)
& ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴)
& ⊢ (𝜑 → 𝐿 ∈ ℝ) & ⊢ (𝜑 → ∀𝑒 ∈ ℝ+
∃𝑗 ∈ ℕ
∀𝑖 ∈
(ℤ≥‘𝑗)((𝐹‘𝑖) < (𝐿 + 𝑒) ∧ 𝐿 < ((𝐹‘𝑖) + 𝑒))) ⇒ ⊢ (𝜑 → 0 ≤ 𝐿) |
|
Theorem | resqrexlemoverl 9907* |
Lemma for resqrex 9912. 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 9908* |
Lemma for resqrex 9912. 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 9909* |
Lemma for resqrex 9912. 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 9910* |
Lemma for resqrex 9912. The square of a limit is 𝐴.
(Contributed by Jim Kingdon, 7-Aug-2021.)
|
⊢ 𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+
↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}),
ℝ+)
& ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴)
& ⊢ (𝜑 → 𝐿 ∈ ℝ) & ⊢ (𝜑 → ∀𝑒 ∈ ℝ+
∃𝑗 ∈ ℕ
∀𝑖 ∈
(ℤ≥‘𝑗)((𝐹‘𝑖) < (𝐿 + 𝑒) ∧ 𝐿 < ((𝐹‘𝑖) + 𝑒))) ⇒ ⊢ (𝜑 → (𝐿↑2) = 𝐴) |
|
Theorem | resqrexlemex 9911* |
Lemma for resqrex 9912. 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 9912* |
Existence of a square root for positive reals. (Contributed by Mario
Carneiro, 9-Jul-2013.)
|
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ∃𝑥 ∈ ℝ (0 ≤ 𝑥 ∧ (𝑥↑2) = 𝐴)) |
|
Theorem | rsqrmo 9913* |
Uniqueness for the square root function. (Contributed by Jim Kingdon,
10-Aug-2021.)
|
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ∃*𝑥 ∈ ℝ ((𝑥↑2) = 𝐴 ∧ 0 ≤ 𝑥)) |
|
Theorem | rersqreu 9914* |
Existence and uniqueness for the real square root function.
(Contributed by Jim Kingdon, 10-Aug-2021.)
|
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ∃!𝑥 ∈ ℝ ((𝑥↑2) = 𝐴 ∧ 0 ≤ 𝑥)) |
|
Theorem | resqrtcl 9915 |
Closure of the square root function. (Contributed by Mario Carneiro,
9-Jul-2013.)
|
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (√‘𝐴) ∈
ℝ) |
|
Theorem | rersqrtthlem 9916 |
Lemma for resqrtth 9917. (Contributed by Jim Kingdon, 10-Aug-2021.)
|
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (((√‘𝐴)↑2) = 𝐴 ∧ 0 ≤ (√‘𝐴))) |
|
Theorem | resqrtth 9917 |
Square root theorem over the reals. Theorem I.35 of [Apostol] p. 29.
(Contributed by Mario Carneiro, 9-Jul-2013.)
|
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ((√‘𝐴)↑2) = 𝐴) |
|
Theorem | remsqsqrt 9918 |
Square of square root. (Contributed by Mario Carneiro, 10-Jul-2013.)
|
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ((√‘𝐴) · (√‘𝐴)) = 𝐴) |
|
Theorem | sqrtge0 9919 |
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 9920 |
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 9921 |
Square root distributes over multiplication. (Contributed by NM,
30-Jul-1999.) (Revised by Mario Carneiro, 29-May-2016.)
|
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (√‘(𝐴 · 𝐵)) = ((√‘𝐴) · (√‘𝐵))) |
|
Theorem | sqrtle 9922 |
Square root is monotonic. (Contributed by NM, 17-Mar-2005.) (Proof
shortened by Mario Carneiro, 29-May-2016.)
|
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 ≤ 𝐵 ↔ (√‘𝐴) ≤ (√‘𝐵))) |
|
Theorem | sqrtlt 9923 |
Square root is strictly monotonic. Closed form of sqrtlti 10023.
(Contributed by Scott Fenton, 17-Apr-2014.) (Proof shortened by Mario
Carneiro, 29-May-2016.)
|
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 < 𝐵 ↔ (√‘𝐴) < (√‘𝐵))) |
|
Theorem | sqrt11ap 9924 |
Analogue to sqrt11 9925 but for apartness. (Contributed by Jim
Kingdon,
11-Aug-2021.)
|
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((√‘𝐴) # (√‘𝐵) ↔ 𝐴 # 𝐵)) |
|
Theorem | sqrt11 9925 |
The square root function is one-to-one. Also see sqrt11ap 9924 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 9926 |
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 9927 |
The square root of a positive real is a positive real. (Contributed by
NM, 22-Feb-2008.)
|
⊢ (𝐴 ∈ ℝ+ →
(√‘𝐴) ∈
ℝ+) |
|
Theorem | sqrtdiv 9928 |
Square root distributes over division. (Contributed by Mario Carneiro,
5-May-2016.)
|
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℝ+) →
(√‘(𝐴 / 𝐵)) = ((√‘𝐴) / (√‘𝐵))) |
|
Theorem | sqrtsq2 9929 |
Relationship between square root and squares. (Contributed by NM,
31-Jul-1999.) (Revised by Mario Carneiro, 29-May-2016.)
|
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((√‘𝐴) = 𝐵 ↔ 𝐴 = (𝐵↑2))) |
|
Theorem | sqrtsq 9930 |
Square root of square. (Contributed by NM, 14-Jan-2006.) (Revised by
Mario Carneiro, 29-May-2016.)
|
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (√‘(𝐴↑2)) = 𝐴) |
|
Theorem | sqrtmsq 9931 |
Square root of square. (Contributed by NM, 2-Aug-1999.) (Revised by
Mario Carneiro, 29-May-2016.)
|
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (√‘(𝐴 · 𝐴)) = 𝐴) |
|
Theorem | sqrt1 9932 |
The square root of 1 is 1. (Contributed by NM, 31-Jul-1999.)
|
⊢ (√‘1) = 1 |
|
Theorem | sqrt4 9933 |
The square root of 4 is 2. (Contributed by NM, 3-Aug-1999.)
|
⊢ (√‘4) = 2 |
|
Theorem | sqrt9 9934 |
The square root of 9 is 3. (Contributed by NM, 11-May-2004.)
|
⊢ (√‘9) = 3 |
|
Theorem | sqrt2gt1lt2 9935 |
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 9936 |
Absolute value of negative. (Contributed by NM, 27-Feb-2005.)
|
⊢ (𝐴 ∈ ℂ → (abs‘-𝐴) = (abs‘𝐴)) |
|
Theorem | abscl 9937 |
Real closure of absolute value. (Contributed by NM, 3-Oct-1999.)
|
⊢ (𝐴 ∈ ℂ → (abs‘𝐴) ∈
ℝ) |
|
Theorem | abscj 9938 |
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 9939 |
Square of value of absolute value function. (Contributed by NM,
16-Jan-2006.)
|
⊢ (𝐴 ∈ ℂ → ((abs‘𝐴)↑2) = (𝐴 · (∗‘𝐴))) |
|
Theorem | absvalsq2 9940 |
Square of value of absolute value function. (Contributed by NM,
1-Feb-2007.)
|
⊢ (𝐴 ∈ ℂ → ((abs‘𝐴)↑2) =
(((ℜ‘𝐴)↑2)
+ ((ℑ‘𝐴)↑2))) |
|
Theorem | sqabsadd 9941 |
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 9942 |
Square of absolute value of difference. (Contributed by NM,
21-Jan-2007.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((abs‘(𝐴 − 𝐵))↑2) = ((((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) − (2 ·
(ℜ‘(𝐴 ·
(∗‘𝐵)))))) |
|
Theorem | absval2 9943 |
Value of absolute value function. Definition 10.36 of [Gleason] p. 133.
(Contributed by NM, 17-Mar-2005.)
|
⊢ (𝐴 ∈ ℂ → (abs‘𝐴) =
(√‘(((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)))) |
|
Theorem | abs0 9944 |
The absolute value of 0. (Contributed by NM, 26-Mar-2005.) (Revised by
Mario Carneiro, 29-May-2016.)
|
⊢ (abs‘0) = 0 |
|
Theorem | absi 9945 |
The absolute value of the imaginary unit. (Contributed by NM,
26-Mar-2005.)
|
⊢ (abs‘i) = 1 |
|
Theorem | absge0 9946 |
Absolute value is nonnegative. (Contributed by NM, 20-Nov-2004.)
(Revised by Mario Carneiro, 29-May-2016.)
|
⊢ (𝐴 ∈ ℂ → 0 ≤
(abs‘𝐴)) |
|
Theorem | absrpclap 9947 |
The absolute value of a number apart from zero is a positive real.
(Contributed by Jim Kingdon, 11-Aug-2021.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (abs‘𝐴) ∈
ℝ+) |
|
Theorem | abs00ap 9948 |
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 9949 |
Strong extensionality for absolute value. (Contributed by Jim Kingdon,
12-Aug-2021.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((abs‘𝐴) # (abs‘𝐵) → 𝐴 # 𝐵)) |
|
Theorem | abs00 9950 |
The absolute value of a number is zero iff the number is zero. Also see
abs00ap 9948 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 9951 |
A complex number is zero iff its absolute value is zero. Deduction form
of abs00 9950. (Contributed by David Moews, 28-Feb-2017.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → ((abs‘𝐴) = 0 ↔ 𝐴 = 0)) |
|
Theorem | abs00bd 9952 |
If a complex number is zero, its absolute value is zero. (Contributed
by David Moews, 28-Feb-2017.)
|
⊢ (𝜑 → 𝐴 = 0) ⇒ ⊢ (𝜑 → (abs‘𝐴) = 0) |
|
Theorem | absreimsq 9953 |
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 9954 |
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 9955 |
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 9956 |
Absolute value distributes over division. (Contributed by Jim Kingdon,
11-Aug-2021.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → (abs‘(𝐴 / 𝐵)) = ((abs‘𝐴) / (abs‘𝐵))) |
|
Theorem | absid 9957 |
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 9958 |
The absolute value of 1. Common special case. (Contributed by David A.
Wheeler, 16-Jul-2016.)
|
⊢ (abs‘1) = 1 |
|
Theorem | absnid 9959 |
A negative number is the negative of its own absolute value. (Contributed
by NM, 27-Feb-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≤ 0) → (abs‘𝐴) = -𝐴) |
|
Theorem | leabs 9960 |
A real number is less than or equal to its absolute value. (Contributed
by NM, 27-Feb-2005.)
|
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ (abs‘𝐴)) |
|
Theorem | qabsor 9961 |
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 9962 |
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 9963 |
Absolute value of a real number. (Contributed by NM, 17-Mar-2005.)
|
⊢ (𝐴 ∈ ℝ → (abs‘𝐴) = (√‘(𝐴↑2))) |
|
Theorem | absresq 9964 |
Square of the absolute value of a real number. (Contributed by NM,
16-Jan-2006.)
|
⊢ (𝐴 ∈ ℝ → ((abs‘𝐴)↑2) = (𝐴↑2)) |
|
Theorem | absexp 9965 |
Absolute value of positive integer exponentiation. (Contributed by NM,
5-Jan-2006.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) →
(abs‘(𝐴↑𝑁)) = ((abs‘𝐴)↑𝑁)) |
|
Theorem | absexpzap 9966 |
Absolute value of integer exponentiation. (Contributed by Jim Kingdon,
11-Aug-2021.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℤ) → (abs‘(𝐴↑𝑁)) = ((abs‘𝐴)↑𝑁)) |
|
Theorem | abssq 9967 |
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 9968 |
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 9969 |
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 9970 |
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 9971 |
The absolute value of an integer is a nonnegative integer. (Contributed
by NM, 27-Feb-2005.)
|
⊢ (𝐴 ∈ ℤ → (abs‘𝐴) ∈
ℕ0) |
|
Theorem | zabscl 9972 |
The absolute value of an integer is an integer. (Contributed by Stefan
O'Rear, 24-Sep-2014.)
|
⊢ (𝐴 ∈ ℤ → (abs‘𝐴) ∈
ℤ) |
|
Theorem | ltabs 9973 |
A number which is less than its absolute value is negative. (Contributed
by Jim Kingdon, 12-Aug-2021.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < (abs‘𝐴)) → 𝐴 < 0) |
|
Theorem | abslt 9974 |
Absolute value and 'less than' relation. (Contributed by NM, 6-Apr-2005.)
(Revised by Mario Carneiro, 29-May-2016.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((abs‘𝐴) < 𝐵 ↔ (-𝐵 < 𝐴 ∧ 𝐴 < 𝐵))) |
|
Theorem | absle 9975 |
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 9976 |
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 9977 |
If the absolute value of a complex number is less than a real, its
difference from the real is nonzero. See also abssubap0 9976 which is the
same with not equal changed to apart. (Contributed by NM, 2-Nov-2007.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ ∧ (abs‘𝐴) < 𝐵) → (𝐵 − 𝐴) ≠ 0) |
|
Theorem | absdiflt 9978 |
The absolute value of a difference and 'less than' relation. (Contributed
by Paul Chapman, 18-Sep-2007.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((abs‘(𝐴 − 𝐵)) < 𝐶 ↔ ((𝐵 − 𝐶) < 𝐴 ∧ 𝐴 < (𝐵 + 𝐶)))) |
|
Theorem | absdifle 9979 |
The absolute value of a difference and 'less than or equal to' relation.
(Contributed by Paul Chapman, 18-Sep-2007.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((abs‘(𝐴 − 𝐵)) ≤ 𝐶 ↔ ((𝐵 − 𝐶) ≤ 𝐴 ∧ 𝐴 ≤ (𝐵 + 𝐶)))) |
|
Theorem | elicc4abs 9980 |
Membership in a symmetric closed real interval. (Contributed by Stefan
O'Rear, 16-Nov-2014.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶 ∈ ((𝐴 − 𝐵)[,](𝐴 + 𝐵)) ↔ (abs‘(𝐶 − 𝐴)) ≤ 𝐵)) |
|
Theorem | lenegsq 9981 |
Comparison to a nonnegative number based on comparison to squares.
(Contributed by NM, 16-Jan-2006.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) → ((𝐴 ≤ 𝐵 ∧ -𝐴 ≤ 𝐵) ↔ (𝐴↑2) ≤ (𝐵↑2))) |
|
Theorem | releabs 9982 |
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‘𝐴)) |
|
Theorem | recvalap 9983 |
Reciprocal expressed with a real denominator. (Contributed by Jim
Kingdon, 13-Aug-2021.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (1 / 𝐴) = ((∗‘𝐴) / ((abs‘𝐴)↑2))) |
|
Theorem | absidm 9984 |
The absolute value function is idempotent. (Contributed by NM,
20-Nov-2004.)
|
⊢ (𝐴 ∈ ℂ →
(abs‘(abs‘𝐴))
= (abs‘𝐴)) |
|
Theorem | absgt0ap 9985 |
The absolute value of a number apart from zero is positive. (Contributed
by Jim Kingdon, 13-Aug-2021.)
|
⊢ (𝐴 ∈ ℂ → (𝐴 # 0 ↔ 0 < (abs‘𝐴))) |
|
Theorem | nnabscl 9986 |
The absolute value of a nonzero integer is a positive integer.
(Contributed by Paul Chapman, 21-Mar-2011.) (Proof shortened by Andrew
Salmon, 25-May-2011.)
|
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (abs‘𝑁) ∈
ℕ) |
|
Theorem | abssub 9987 |
Swapping order of subtraction doesn't change the absolute value.
(Contributed by NM, 1-Oct-1999.) (Proof shortened by Mario Carneiro,
29-May-2016.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (abs‘(𝐴 − 𝐵)) = (abs‘(𝐵 − 𝐴))) |
|
Theorem | abssubge0 9988 |
Absolute value of a nonnegative difference. (Contributed by NM,
14-Feb-2008.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (abs‘(𝐵 − 𝐴)) = (𝐵 − 𝐴)) |
|
Theorem | abssuble0 9989 |
Absolute value of a nonpositive difference. (Contributed by FL,
3-Jan-2008.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (abs‘(𝐴 − 𝐵)) = (𝐵 − 𝐴)) |
|
Theorem | abstri 9990 |
Triangle inequality for absolute value. Proposition 10-3.7(h) of
[Gleason] p. 133. (Contributed by NM,
7-Mar-2005.) (Proof shortened by
Mario Carneiro, 29-May-2016.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (abs‘(𝐴 + 𝐵)) ≤ ((abs‘𝐴) + (abs‘𝐵))) |
|
Theorem | abs3dif 9991 |
Absolute value of differences around common element. (Contributed by FL,
9-Oct-2006.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (abs‘(𝐴 − 𝐵)) ≤ ((abs‘(𝐴 − 𝐶)) + (abs‘(𝐶 − 𝐵)))) |
|
Theorem | abs2dif 9992 |
Difference of absolute values. (Contributed by Paul Chapman,
7-Sep-2007.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((abs‘𝐴) − (abs‘𝐵)) ≤ (abs‘(𝐴 − 𝐵))) |
|
Theorem | abs2dif2 9993 |
Difference of absolute values. (Contributed by Mario Carneiro,
14-Apr-2016.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (abs‘(𝐴 − 𝐵)) ≤ ((abs‘𝐴) + (abs‘𝐵))) |
|
Theorem | abs2difabs 9994 |
Absolute value of difference of absolute values. (Contributed by Paul
Chapman, 7-Sep-2007.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) →
(abs‘((abs‘𝐴)
− (abs‘𝐵)))
≤ (abs‘(𝐴 −
𝐵))) |
|
Theorem | recan 9995* |
Cancellation law involving the real part of a complex number.
(Contributed by NM, 12-May-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (∀𝑥 ∈ ℂ
(ℜ‘(𝑥 ·
𝐴)) = (ℜ‘(𝑥 · 𝐵)) ↔ 𝐴 = 𝐵)) |
|
Theorem | absf 9996 |
Mapping domain and codomain of the absolute value function.
(Contributed by NM, 30-Aug-2007.) (Revised by Mario Carneiro,
7-Nov-2013.)
|
⊢ abs:ℂ⟶ℝ |
|
Theorem | abs3lem 9997 |
Lemma involving absolute value of differences. (Contributed by NM,
2-Oct-1999.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℝ)) →
(((abs‘(𝐴 −
𝐶)) < (𝐷 / 2) ∧ (abs‘(𝐶 − 𝐵)) < (𝐷 / 2)) → (abs‘(𝐴 − 𝐵)) < 𝐷)) |
|
Theorem | fzomaxdiflem 9998 |
Lemma for fzomaxdif 9999. (Contributed by Stefan O'Rear, 6-Sep-2015.)
|
⊢ (((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) ∧ 𝐴 ≤ 𝐵) → (abs‘(𝐵 − 𝐴)) ∈ (0..^(𝐷 − 𝐶))) |
|
Theorem | fzomaxdif 9999 |
A bound on the separation of two points in a half-open range.
(Contributed by Stefan O'Rear, 6-Sep-2015.)
|
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → (abs‘(𝐴 − 𝐵)) ∈ (0..^(𝐷 − 𝐶))) |
|
Theorem | cau3lem 10000* |
Lemma for cau3 10001. (Contributed by Mario Carneiro,
15-Feb-2014.)
(Revised by Mario Carneiro, 1-May-2014.)
|
⊢ 𝑍 ⊆ ℤ & ⊢ (𝜏 → 𝜓)
& ⊢ ((𝐹‘𝑘) = (𝐹‘𝑗) → (𝜓 ↔ 𝜒)) & ⊢ ((𝐹‘𝑘) = (𝐹‘𝑚) → (𝜓 ↔ 𝜃)) & ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → (𝐺‘((𝐹‘𝑗)𝐷(𝐹‘𝑘))) = (𝐺‘((𝐹‘𝑘)𝐷(𝐹‘𝑗)))) & ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜒) → (𝐺‘((𝐹‘𝑚)𝐷(𝐹‘𝑗))) = (𝐺‘((𝐹‘𝑗)𝐷(𝐹‘𝑚)))) & ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃) ∧ (𝜒 ∧ 𝑥 ∈ ℝ)) → (((𝐺‘((𝐹‘𝑘)𝐷(𝐹‘𝑗))) < (𝑥 / 2) ∧ (𝐺‘((𝐹‘𝑗)𝐷(𝐹‘𝑚))) < (𝑥 / 2)) → (𝐺‘((𝐹‘𝑘)𝐷(𝐹‘𝑚))) < 𝑥)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝜏 ∧ (𝐺‘((𝐹‘𝑘)𝐷(𝐹‘𝑗))) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝜏 ∧ ∀𝑚 ∈ (ℤ≥‘𝑘)(𝐺‘((𝐹‘𝑘)𝐷(𝐹‘𝑚))) < 𝑥))) |