Home Intuitionistic Logic ExplorerTheorem List (p. 101 of 110) < Previous  Next > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 10001-10100   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremcrred 10001 The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)       (𝜑 → (ℜ‘(𝐴 + (i · 𝐵))) = 𝐴)

Theoremcrimd 10002 The imaginary part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)       (𝜑 → (ℑ‘(𝐴 + (i · 𝐵))) = 𝐵)

3.7.3  Sequence convergence

Theoremcaucvgrelemrec 10003* Two ways to express a reciprocal. (Contributed by Jim Kingdon, 20-Jul-2021.)
((𝐴 ∈ ℝ ∧ 𝐴 # 0) → (𝑟 ∈ ℝ (𝐴 · 𝑟) = 1) = (1 / 𝐴))

Theoremcaucvgrelemcau 10004* Lemma for caucvgre 10005. Converting the Cauchy condition. (Contributed by Jim Kingdon, 20-Jul-2021.)
(𝜑𝐹:ℕ⟶ℝ)    &   (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ𝑛)((𝐹𝑛) < ((𝐹𝑘) + (1 / 𝑛)) ∧ (𝐹𝑘) < ((𝐹𝑛) + (1 / 𝑛))))       (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ ℕ (𝑛 < 𝑘 → ((𝐹𝑛) < ((𝐹𝑘) + (𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹𝑘) < ((𝐹𝑛) + (𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)))))

Theoremcaucvgre 10005* 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 / 𝑛))))       (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ+𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ𝑗)((𝐹𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹𝑖) + 𝑥)))

Theoremcvg1nlemcxze 10006 Lemma for cvg1n 10010. Rearranging an expression related to the rate of convergence. (Contributed by Jim Kingdon, 6-Aug-2021.)
(𝜑𝐶 ∈ ℝ+)    &   (𝜑𝑋 ∈ ℝ+)    &   (𝜑𝑍 ∈ ℕ)    &   (𝜑𝐸 ∈ ℕ)    &   (𝜑𝐴 ∈ ℕ)    &   (𝜑 → ((((𝐶 · 2) / 𝑋) / 𝑍) + 𝐴) < 𝐸)       (𝜑 → (𝐶 / (𝐸 · 𝑍)) < (𝑋 / 2))

Theoremcvg1nlemf 10007* Lemma for cvg1n 10010. The modified sequence 𝐺 is a sequence. (Contributed by Jim Kingdon, 1-Aug-2021.)
(𝜑𝐹:ℕ⟶ℝ)    &   (𝜑𝐶 ∈ ℝ+)    &   (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ𝑛)((𝐹𝑛) < ((𝐹𝑘) + (𝐶 / 𝑛)) ∧ (𝐹𝑘) < ((𝐹𝑛) + (𝐶 / 𝑛))))    &   𝐺 = (𝑗 ∈ ℕ ↦ (𝐹‘(𝑗 · 𝑍)))    &   (𝜑𝑍 ∈ ℕ)    &   (𝜑𝐶 < 𝑍)       (𝜑𝐺:ℕ⟶ℝ)

Theoremcvg1nlemcau 10008* Lemma for cvg1n 10010. 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 / 𝑛))))

Theoremcvg1nlemres 10009* Lemma for cvg1n 10010. 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.)
(𝜑𝐹:ℕ⟶ℝ)    &   (𝜑𝐶 ∈ ℝ+)    &   (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ𝑛)((𝐹𝑛) < ((𝐹𝑘) + (𝐶 / 𝑛)) ∧ (𝐹𝑘) < ((𝐹𝑛) + (𝐶 / 𝑛))))    &   𝐺 = (𝑗 ∈ ℕ ↦ (𝐹‘(𝑗 · 𝑍)))    &   (𝜑𝑍 ∈ ℕ)    &   (𝜑𝐶 < 𝑍)       (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ+𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ𝑗)((𝐹𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹𝑖) + 𝑥)))

Theoremcvg1n 10010* Convergence of real sequences.

This is a version of caucvgre 10005 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.)

(𝜑𝐹:ℕ⟶ℝ)    &   (𝜑𝐶 ∈ ℝ+)    &   (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ𝑛)((𝐹𝑛) < ((𝐹𝑘) + (𝐶 / 𝑛)) ∧ (𝐹𝑘) < ((𝐹𝑛) + (𝐶 / 𝑛))))       (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ+𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ𝑗)((𝐹𝑖) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹𝑖) + 𝑥)))

Theoremuzin2 10011 The upper integers are closed under intersection. (Contributed by Mario Carneiro, 24-Dec-2013.)
((𝐴 ∈ ran ℤ𝐵 ∈ ran ℤ) → (𝐴𝐵) ∈ ran ℤ)

Theoremrexanuz 10012* Combine two different upper integer properties into one. (Contributed by Mario Carneiro, 25-Dec-2013.)
(∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)(𝜑𝜓) ↔ (∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)𝜑 ∧ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)𝜓))

Theoremrexfiuz 10013* Combine finitely many different upper integer properties into one. (Contributed by Mario Carneiro, 6-Jun-2014.)
(𝐴 ∈ Fin → (∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)∀𝑛𝐴 𝜑 ↔ ∀𝑛𝐴𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)𝜑))

Theoremrexuz3 10014* Restrict the base of the upper integers set to another upper integers set. (Contributed by Mario Carneiro, 26-Dec-2013.)
𝑍 = (ℤ𝑀)       (𝑀 ∈ ℤ → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)𝜑 ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)𝜑))

Theoremrexanuz2 10015* Combine two different upper integer properties into one. (Contributed by Mario Carneiro, 26-Dec-2013.)
𝑍 = (ℤ𝑀)       (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝜑𝜓) ↔ (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)𝜑 ∧ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)𝜓))

Theoremr19.29uz 10016* A version of 19.29 1552 for upper integer quantifiers. (Contributed by Mario Carneiro, 10-Feb-2014.)
𝑍 = (ℤ𝑀)       ((∀𝑘𝑍 𝜑 ∧ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)𝜓) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝜑𝜓))

Theoremr19.2uz 10017* A version of r19.2m 3336 for upper integer quantifiers. (Contributed by Mario Carneiro, 15-Feb-2014.)
𝑍 = (ℤ𝑀)       (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)𝜑 → ∃𝑘𝑍 𝜑)

Theoremrecvguniqlem 10018 Lemma for recvguniq 10019. Some of the rearrangements of the expressions. (Contributed by Jim Kingdon, 8-Aug-2021.)
(𝜑𝐹:ℕ⟶ℝ)    &   (𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐾 ∈ ℕ)    &   (𝜑𝐴 < ((𝐹𝐾) + ((𝐴𝐵) / 2)))    &   (𝜑 → (𝐹𝐾) < (𝐵 + ((𝐴𝐵) / 2)))       (𝜑 → ⊥)

Theoremrecvguniq 10019* Limits are unique. (Contributed by Jim Kingdon, 7-Aug-2021.)
(𝜑𝐹:ℕ⟶ℝ)    &   (𝜑𝐿 ∈ ℝ)    &   (𝜑 → ∀𝑥 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)((𝐹𝑘) < (𝐿 + 𝑥) ∧ 𝐿 < ((𝐹𝑘) + 𝑥)))    &   (𝜑𝑀 ∈ ℝ)    &   (𝜑 → ∀𝑥 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)((𝐹𝑘) < (𝑀 + 𝑥) ∧ 𝑀 < ((𝐹𝑘) + 𝑥)))       (𝜑𝐿 = 𝑀)

3.7.4  Square root; absolute value

Syntaxcsqrt 10020 Extend class notation to include square root of a complex number.
class

Syntaxcabs 10021 Extend class notation to include a function for the absolute value (modulus) of a complex number.
class abs

Definitiondf-rsqrt 10022* 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 ≤ 𝑦)))

Definitiondf-abs 10023 Define the function for the absolute value (modulus) of a complex number. (Contributed by NM, 27-Jul-1999.)
abs = (𝑥 ∈ ℂ ↦ (√‘(𝑥 · (∗‘𝑥))))

Theoremsqrtrval 10024* Value of square root function. (Contributed by Jim Kingdon, 23-Aug-2020.)
(𝐴 ∈ ℝ → (√‘𝐴) = (𝑥 ∈ ℝ ((𝑥↑2) = 𝐴 ∧ 0 ≤ 𝑥)))

Theoremabsval 10025 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‘𝐴) = (√‘(𝐴 · (∗‘𝐴))))

Theoremrennim 10026 A real number does not lie on the negative imaginary axis. (Contributed by Mario Carneiro, 8-Jul-2013.)
(𝐴 ∈ ℝ → (i · 𝐴) ∉ ℝ+)

Theoremsqrt0rlem 10027 Lemma for sqrt0 10028. (Contributed by Jim Kingdon, 26-Aug-2020.)
((𝐴 ∈ ℝ ∧ ((𝐴↑2) = 0 ∧ 0 ≤ 𝐴)) ↔ 𝐴 = 0)

Theoremsqrt0 10028 Square root of zero. (Contributed by Mario Carneiro, 9-Jul-2013.)
(√‘0) = 0

Theoremresqrexlem1arp 10029* Lemma for resqrex 10050. 1 + 𝐴 is a positive real (expressed in a way that will help apply iseqfcl 9535 and similar theorems). (Contributed by Jim Kingdon, 28-Jul-2021.)
𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}), ℝ+)    &   (𝜑𝐴 ∈ ℝ)    &   (𝜑 → 0 ≤ 𝐴)       ((𝜑𝑁 ∈ ℕ) → ((ℕ × {(1 + 𝐴)})‘𝑁) ∈ ℝ+)

Theoremresqrexlemp1rp 10030* Lemma for resqrex 10050. Applying the recursion rule yields a positive real (expressed in a way that will help apply iseqfcl 9535 and similar theorems). (Contributed by Jim Kingdon, 28-Jul-2021.)
𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}), ℝ+)    &   (𝜑𝐴 ∈ ℝ)    &   (𝜑 → 0 ≤ 𝐴)       ((𝜑 ∧ (𝐵 ∈ ℝ+𝐶 ∈ ℝ+)) → (𝐵(𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2))𝐶) ∈ ℝ+)

Theoremresqrexlemf 10031* Lemma for resqrex 10050. The sequence is a function. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.)
𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}), ℝ+)    &   (𝜑𝐴 ∈ ℝ)    &   (𝜑 → 0 ≤ 𝐴)       (𝜑𝐹:ℕ⟶ℝ+)

Theoremresqrexlemf1 10032* Lemma for resqrex 10050. 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.)
𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}), ℝ+)    &   (𝜑𝐴 ∈ ℝ)    &   (𝜑 → 0 ≤ 𝐴)       (𝜑 → (𝐹‘1) = (1 + 𝐴))

Theoremresqrexlemfp1 10033* Lemma for resqrex 10050. 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))

Theoremresqrexlemover 10034* Lemma for resqrex 10050. Each element of the sequence is an overestimate. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.)
𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}), ℝ+)    &   (𝜑𝐴 ∈ ℝ)    &   (𝜑 → 0 ≤ 𝐴)       ((𝜑𝑁 ∈ ℕ) → 𝐴 < ((𝐹𝑁)↑2))

Theoremresqrexlemdec 10035* Lemma for resqrex 10050. The sequence is decreasing. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.)
𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}), ℝ+)    &   (𝜑𝐴 ∈ ℝ)    &   (𝜑 → 0 ≤ 𝐴)       ((𝜑𝑁 ∈ ℕ) → (𝐹‘(𝑁 + 1)) < (𝐹𝑁))

Theoremresqrexlemdecn 10036* Lemma for resqrex 10050. The sequence is decreasing. (Contributed by Jim Kingdon, 31-Jul-2021.)
𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}), ℝ+)    &   (𝜑𝐴 ∈ ℝ)    &   (𝜑 → 0 ≤ 𝐴)    &   (𝜑𝑁 ∈ ℕ)    &   (𝜑𝑀 ∈ ℕ)    &   (𝜑𝑁 < 𝑀)       (𝜑 → (𝐹𝑀) < (𝐹𝑁))

Theoremresqrexlemlo 10037* Lemma for resqrex 10050. 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↑𝑁)) < (𝐹𝑁))

Theoremresqrexlemcalc1 10038* Lemma for resqrex 10050. 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))))

Theoremresqrexlemcalc2 10039* Lemma for resqrex 10050. 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))

Theoremresqrexlemcalc3 10040* Lemma for resqrex 10050. 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))))

Theoremresqrexlemnmsq 10041* Lemma for resqrex 10050. 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))))

Theoremresqrexlemnm 10042* Lemma for resqrex 10050. 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))))

Theoremresqrexlemcvg 10043* Lemma for resqrex 10050. The sequence has a limit. (Contributed by Jim Kingdon, 6-Aug-2021.)
𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}), ℝ+)    &   (𝜑𝐴 ∈ ℝ)    &   (𝜑 → 0 ≤ 𝐴)       (𝜑 → ∃𝑟 ∈ ℝ ∀𝑥 ∈ ℝ+𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ𝑗)((𝐹𝑖) < (𝑟 + 𝑥) ∧ 𝑟 < ((𝐹𝑖) + 𝑥)))

Theoremresqrexlemgt0 10044* Lemma for resqrex 10050. A limit is nonnegative. (Contributed by Jim Kingdon, 7-Aug-2021.)
𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}), ℝ+)    &   (𝜑𝐴 ∈ ℝ)    &   (𝜑 → 0 ≤ 𝐴)    &   (𝜑𝐿 ∈ ℝ)    &   (𝜑 → ∀𝑒 ∈ ℝ+𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ𝑗)((𝐹𝑖) < (𝐿 + 𝑒) ∧ 𝐿 < ((𝐹𝑖) + 𝑒)))       (𝜑 → 0 ≤ 𝐿)

Theoremresqrexlemoverl 10045* Lemma for resqrex 10050. 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 ≤ 𝐴)    &   (𝜑𝐿 ∈ ℝ)    &   (𝜑 → ∀𝑒 ∈ ℝ+𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ𝑗)((𝐹𝑖) < (𝐿 + 𝑒) ∧ 𝐿 < ((𝐹𝑖) + 𝑒)))    &   (𝜑𝐾 ∈ ℕ)       (𝜑𝐿 ≤ (𝐹𝐾))

Theoremresqrexlemglsq 10046* Lemma for resqrex 10050. 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) < ((𝐺𝑘) + 𝑒)))

Theoremresqrexlemga 10047* Lemma for resqrex 10050. 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))       (𝜑 → ∀𝑒 ∈ ℝ+𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ𝑗)((𝐺𝑘) < (𝐴 + 𝑒) ∧ 𝐴 < ((𝐺𝑘) + 𝑒)))

Theoremresqrexlemsqa 10048* Lemma for resqrex 10050. The square of a limit is 𝐴. (Contributed by Jim Kingdon, 7-Aug-2021.)
𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}), ℝ+)    &   (𝜑𝐴 ∈ ℝ)    &   (𝜑 → 0 ≤ 𝐴)    &   (𝜑𝐿 ∈ ℝ)    &   (𝜑 → ∀𝑒 ∈ ℝ+𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ𝑗)((𝐹𝑖) < (𝐿 + 𝑒) ∧ 𝐿 < ((𝐹𝑖) + 𝑒)))       (𝜑 → (𝐿↑2) = 𝐴)

Theoremresqrexlemex 10049* Lemma for resqrex 10050. 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) = 𝐴))

Theoremresqrex 10050* Existence of a square root for positive reals. (Contributed by Mario Carneiro, 9-Jul-2013.)
((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ∃𝑥 ∈ ℝ (0 ≤ 𝑥 ∧ (𝑥↑2) = 𝐴))

Theoremrsqrmo 10051* Uniqueness for the square root function. (Contributed by Jim Kingdon, 10-Aug-2021.)
((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ∃*𝑥 ∈ ℝ ((𝑥↑2) = 𝐴 ∧ 0 ≤ 𝑥))

Theoremrersqreu 10052* Existence and uniqueness for the real square root function. (Contributed by Jim Kingdon, 10-Aug-2021.)
((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ∃!𝑥 ∈ ℝ ((𝑥↑2) = 𝐴 ∧ 0 ≤ 𝑥))

Theoremresqrtcl 10053 Closure of the square root function. (Contributed by Mario Carneiro, 9-Jul-2013.)
((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (√‘𝐴) ∈ ℝ)

Theoremrersqrtthlem 10054 Lemma for resqrtth 10055. (Contributed by Jim Kingdon, 10-Aug-2021.)
((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (((√‘𝐴)↑2) = 𝐴 ∧ 0 ≤ (√‘𝐴)))

Theoremresqrtth 10055 Square root theorem over the reals. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 9-Jul-2013.)
((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ((√‘𝐴)↑2) = 𝐴)

Theoremremsqsqrt 10056 Square of square root. (Contributed by Mario Carneiro, 10-Jul-2013.)
((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → ((√‘𝐴) · (√‘𝐴)) = 𝐴)

Theoremsqrtge0 10057 The square root function is nonnegative for nonnegative input. (Contributed by NM, 26-May-1999.) (Revised by Mario Carneiro, 9-Jul-2013.)
((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → 0 ≤ (√‘𝐴))

Theoremsqrtgt0 10058 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 < (√‘𝐴))

Theoremsqrtmul 10059 Square root distributes over multiplication. (Contributed by NM, 30-Jul-1999.) (Revised by Mario Carneiro, 29-May-2016.)
(((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (√‘(𝐴 · 𝐵)) = ((√‘𝐴) · (√‘𝐵)))

Theoremsqrtle 10060 Square root is monotonic. (Contributed by NM, 17-Mar-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.)
(((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴𝐵 ↔ (√‘𝐴) ≤ (√‘𝐵)))

Theoremsqrtlt 10061 Square root is strictly monotonic. Closed form of sqrtlti 10161. (Contributed by Scott Fenton, 17-Apr-2014.) (Proof shortened by Mario Carneiro, 29-May-2016.)
(((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 < 𝐵 ↔ (√‘𝐴) < (√‘𝐵)))

Theoremsqrt11ap 10062 Analogue to sqrt11 10063 but for apartness. (Contributed by Jim Kingdon, 11-Aug-2021.)
(((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((√‘𝐴) # (√‘𝐵) ↔ 𝐴 # 𝐵))

Theoremsqrt11 10063 The square root function is one-to-one. Also see sqrt11ap 10062 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 ≤ 𝐵)) → ((√‘𝐴) = (√‘𝐵) ↔ 𝐴 = 𝐵))

Theoremsqrt00 10064 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))

Theoremrpsqrtcl 10065 The square root of a positive real is a positive real. (Contributed by NM, 22-Feb-2008.)
(𝐴 ∈ ℝ+ → (√‘𝐴) ∈ ℝ+)

Theoremsqrtdiv 10066 Square root distributes over division. (Contributed by Mario Carneiro, 5-May-2016.)
(((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℝ+) → (√‘(𝐴 / 𝐵)) = ((√‘𝐴) / (√‘𝐵)))

Theoremsqrtsq2 10067 Relationship between square root and squares. (Contributed by NM, 31-Jul-1999.) (Revised by Mario Carneiro, 29-May-2016.)
(((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((√‘𝐴) = 𝐵𝐴 = (𝐵↑2)))

Theoremsqrtsq 10068 Square root of square. (Contributed by NM, 14-Jan-2006.) (Revised by Mario Carneiro, 29-May-2016.)
((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (√‘(𝐴↑2)) = 𝐴)

Theoremsqrtmsq 10069 Square root of square. (Contributed by NM, 2-Aug-1999.) (Revised by Mario Carneiro, 29-May-2016.)
((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (√‘(𝐴 · 𝐴)) = 𝐴)

Theoremsqrt1 10070 The square root of 1 is 1. (Contributed by NM, 31-Jul-1999.)
(√‘1) = 1

Theoremsqrt4 10071 The square root of 4 is 2. (Contributed by NM, 3-Aug-1999.)
(√‘4) = 2

Theoremsqrt9 10072 The square root of 9 is 3. (Contributed by NM, 11-May-2004.)
(√‘9) = 3

Theoremsqrt2gt1lt2 10073 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)

Theoremabsneg 10074 Absolute value of negative. (Contributed by NM, 27-Feb-2005.)
(𝐴 ∈ ℂ → (abs‘-𝐴) = (abs‘𝐴))

Theoremabscl 10075 Real closure of absolute value. (Contributed by NM, 3-Oct-1999.)
(𝐴 ∈ ℂ → (abs‘𝐴) ∈ ℝ)

Theoremabscj 10076 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‘𝐴))

Theoremabsvalsq 10077 Square of value of absolute value function. (Contributed by NM, 16-Jan-2006.)
(𝐴 ∈ ℂ → ((abs‘𝐴)↑2) = (𝐴 · (∗‘𝐴)))

Theoremabsvalsq2 10078 Square of value of absolute value function. (Contributed by NM, 1-Feb-2007.)
(𝐴 ∈ ℂ → ((abs‘𝐴)↑2) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)))

Theoremsqabsadd 10079 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 · (ℜ‘(𝐴 · (∗‘𝐵))))))

Theoremsqabssub 10080 Square of absolute value of difference. (Contributed by NM, 21-Jan-2007.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((abs‘(𝐴𝐵))↑2) = ((((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) − (2 · (ℜ‘(𝐴 · (∗‘𝐵))))))

Theoremabsval2 10081 Value of absolute value function. Definition 10.36 of [Gleason] p. 133. (Contributed by NM, 17-Mar-2005.)
(𝐴 ∈ ℂ → (abs‘𝐴) = (√‘(((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2))))

Theoremabs0 10082 The absolute value of 0. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 29-May-2016.)
(abs‘0) = 0

Theoremabsi 10083 The absolute value of the imaginary unit. (Contributed by NM, 26-Mar-2005.)
(abs‘i) = 1

Theoremabsge0 10084 Absolute value is nonnegative. (Contributed by NM, 20-Nov-2004.) (Revised by Mario Carneiro, 29-May-2016.)
(𝐴 ∈ ℂ → 0 ≤ (abs‘𝐴))

Theoremabsrpclap 10085 The absolute value of a number apart from zero is a positive real. (Contributed by Jim Kingdon, 11-Aug-2021.)
((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (abs‘𝐴) ∈ ℝ+)

Theoremabs00ap 10086 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))

Theoremabsext 10087 Strong extensionality for absolute value. (Contributed by Jim Kingdon, 12-Aug-2021.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((abs‘𝐴) # (abs‘𝐵) → 𝐴 # 𝐵))

Theoremabs00 10088 The absolute value of a number is zero iff the number is zero. Also see abs00ap 10086 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))

Theoremabs00ad 10089 A complex number is zero iff its absolute value is zero. Deduction form of abs00 10088. (Contributed by David Moews, 28-Feb-2017.)
(𝜑𝐴 ∈ ℂ)       (𝜑 → ((abs‘𝐴) = 0 ↔ 𝐴 = 0))

Theoremabs00bd 10090 If a complex number is zero, its absolute value is zero. (Contributed by David Moews, 28-Feb-2017.)
(𝜑𝐴 = 0)       (𝜑 → (abs‘𝐴) = 0)

Theoremabsreimsq 10091 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)))

Theoremabsreim 10092 Absolute value of a number that has been decomposed into real and imaginary parts. (Contributed by NM, 14-Jan-2006.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (abs‘(𝐴 + (i · 𝐵))) = (√‘((𝐴↑2) + (𝐵↑2))))

Theoremabsmul 10093 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‘𝐵)))

Theoremabsdivap 10094 Absolute value distributes over division. (Contributed by Jim Kingdon, 11-Aug-2021.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → (abs‘(𝐴 / 𝐵)) = ((abs‘𝐴) / (abs‘𝐵)))

Theoremabsid 10095 A nonnegative number is its own absolute value. (Contributed by NM, 11-Oct-1999.) (Revised by Mario Carneiro, 29-May-2016.)
((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (abs‘𝐴) = 𝐴)

Theoremabs1 10096 The absolute value of 1. Common special case. (Contributed by David A. Wheeler, 16-Jul-2016.)
(abs‘1) = 1

Theoremabsnid 10097 A negative number is the negative of its own absolute value. (Contributed by NM, 27-Feb-2005.)
((𝐴 ∈ ℝ ∧ 𝐴 ≤ 0) → (abs‘𝐴) = -𝐴)

Theoremleabs 10098 A real number is less than or equal to its absolute value. (Contributed by NM, 27-Feb-2005.)
(𝐴 ∈ ℝ → 𝐴 ≤ (abs‘𝐴))

Theoremqabsor 10099 The absolute value of a rational number is either that number or its negative. (Contributed by Jim Kingdon, 8-Nov-2021.)
(𝐴 ∈ ℚ → ((abs‘𝐴) = 𝐴 ∨ (abs‘𝐴) = -𝐴))

Theoremqabsord 10100 The absolute value of a rational number is either that number or its negative. (Contributed by Jim Kingdon, 8-Nov-2021.)
(𝜑𝐴 ∈ ℚ)       (𝜑 → ((abs‘𝐴) = 𝐴 ∨ (abs‘𝐴) = -𝐴))

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-10953
 Copyright terms: Public domain < Previous  Next >