 Home Intuitionistic Logic ExplorerTheorem List (p. 95 of 100) < 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 - 9401-9500   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremcjmulge0i 9401 A complex number times its conjugate is nonnegative. (Contributed by NM, 28-May-1999.)
𝐴 ∈ ℂ       0 ≤ (𝐴 · (∗‘𝐴))

Theoremrenegi 9402 Real part of negative. (Contributed by NM, 2-Aug-1999.)
𝐴 ∈ ℂ       (ℜ‘-𝐴) = -(ℜ‘𝐴)

Theoremimnegi 9403 Imaginary part of negative. (Contributed by NM, 2-Aug-1999.)
𝐴 ∈ ℂ       (ℑ‘-𝐴) = -(ℑ‘𝐴)

Theoremcjnegi 9404 Complex conjugate of negative. (Contributed by NM, 2-Aug-1999.)
𝐴 ∈ ℂ       (∗‘-𝐴) = -(∗‘𝐴)

Theoremaddcji 9405 A number plus its conjugate is twice its real part. Compare Proposition 10-3.4(h) of [Gleason] p. 133. (Contributed by NM, 2-Oct-1999.)
𝐴 ∈ ℂ       (𝐴 + (∗‘𝐴)) = (2 · (ℜ‘𝐴))

𝐴 ∈ ℂ    &   𝐵 ∈ ℂ       (ℜ‘(𝐴 + 𝐵)) = ((ℜ‘𝐴) + (ℜ‘𝐵))

𝐴 ∈ ℂ    &   𝐵 ∈ ℂ       (ℑ‘(𝐴 + 𝐵)) = ((ℑ‘𝐴) + (ℑ‘𝐵))

Theoremremuli 9408 Real part of a product. (Contributed by NM, 28-Jul-1999.)
𝐴 ∈ ℂ    &   𝐵 ∈ ℂ       (ℜ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℜ‘𝐵)) − ((ℑ‘𝐴) · (ℑ‘𝐵)))

Theoremimmuli 9409 Imaginary part of a product. (Contributed by NM, 28-Jul-1999.)
𝐴 ∈ ℂ    &   𝐵 ∈ ℂ       (ℑ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℑ‘𝐵)) + ((ℑ‘𝐴) · (ℜ‘𝐵)))

Theoremcjaddi 9410 Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.)
𝐴 ∈ ℂ    &   𝐵 ∈ ℂ       (∗‘(𝐴 + 𝐵)) = ((∗‘𝐴) + (∗‘𝐵))

Theoremcjmuli 9411 Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by NM, 28-Jul-1999.)
𝐴 ∈ ℂ    &   𝐵 ∈ ℂ       (∗‘(𝐴 · 𝐵)) = ((∗‘𝐴) · (∗‘𝐵))

Theoremipcni 9412 Standard inner product on complex numbers. (Contributed by NM, 2-Oct-1999.)
𝐴 ∈ ℂ    &   𝐵 ∈ ℂ       (ℜ‘(𝐴 · (∗‘𝐵))) = (((ℜ‘𝐴) · (ℜ‘𝐵)) + ((ℑ‘𝐴) · (ℑ‘𝐵)))

Theoremcjdivapi 9413 Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.)
𝐴 ∈ ℂ    &   𝐵 ∈ ℂ       (𝐵 # 0 → (∗‘(𝐴 / 𝐵)) = ((∗‘𝐴) / (∗‘𝐵)))

Theoremcrrei 9414 The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.)
𝐴 ∈ ℝ    &   𝐵 ∈ ℝ       (ℜ‘(𝐴 + (i · 𝐵))) = 𝐴

Theoremcrimi 9415 The imaginary part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.)
𝐴 ∈ ℝ    &   𝐵 ∈ ℝ       (ℑ‘(𝐴 + (i · 𝐵))) = 𝐵

Theoremrecld 9416 The real part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)       (𝜑 → (ℜ‘𝐴) ∈ ℝ)

Theoremimcld 9417 The imaginary part of a complex number is real (closure law). (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)       (𝜑 → (ℑ‘𝐴) ∈ ℝ)

Theoremcjcld 9418 Closure law for complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)       (𝜑 → (∗‘𝐴) ∈ ℂ)

Theoremreplimd 9419 Construct a complex number from its real and imaginary parts. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)       (𝜑𝐴 = ((ℜ‘𝐴) + (i · (ℑ‘𝐴))))

Theoremremimd 9420 Value of the conjugate of a complex number. The value is the real part minus i times the imaginary part. Definition 10-3.2 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)       (𝜑 → (∗‘𝐴) = ((ℜ‘𝐴) − (i · (ℑ‘𝐴))))

Theoremcjcjd 9421 The conjugate of the conjugate is the original complex number. Proposition 10-3.4(e) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)       (𝜑 → (∗‘(∗‘𝐴)) = 𝐴)

Theoremreim0bd 9422 A number is real iff its imaginary part is 0. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑 → (ℑ‘𝐴) = 0)       (𝜑𝐴 ∈ ℝ)

Theoremrerebd 9423 A real number equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑 → (ℜ‘𝐴) = 𝐴)       (𝜑𝐴 ∈ ℝ)

Theoremcjrebd 9424 A number is real iff it equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑 → (∗‘𝐴) = 𝐴)       (𝜑𝐴 ∈ ℝ)

Theoremcjne0d 9425 A number which is nonzero has a complex conjugate which is nonzero. Also see cjap0d 9426 which is similar but for apartness. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐴 ≠ 0)       (𝜑 → (∗‘𝐴) ≠ 0)

Theoremcjap0d 9426 A number which is apart from zero has a complex conjugate which is apart from zero. (Contributed by Jim Kingdon, 11-Aug-2021.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐴 # 0)       (𝜑 → (∗‘𝐴) # 0)

Theoremrecjd 9427 Real part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)       (𝜑 → (ℜ‘(∗‘𝐴)) = (ℜ‘𝐴))

Theoremimcjd 9428 Imaginary part of a complex conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)       (𝜑 → (ℑ‘(∗‘𝐴)) = -(ℑ‘𝐴))

Theoremcjmulrcld 9429 A complex number times its conjugate is real. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)       (𝜑 → (𝐴 · (∗‘𝐴)) ∈ ℝ)

Theoremcjmulvald 9430 A complex number times its conjugate. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)       (𝜑 → (𝐴 · (∗‘𝐴)) = (((ℜ‘𝐴)↑2) + ((ℑ‘𝐴)↑2)))

Theoremcjmulge0d 9431 A complex number times its conjugate is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)       (𝜑 → 0 ≤ (𝐴 · (∗‘𝐴)))

Theoremrenegd 9432 Real part of negative. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)       (𝜑 → (ℜ‘-𝐴) = -(ℜ‘𝐴))

Theoremimnegd 9433 Imaginary part of negative. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)       (𝜑 → (ℑ‘-𝐴) = -(ℑ‘𝐴))

Theoremcjnegd 9434 Complex conjugate of negative. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)       (𝜑 → (∗‘-𝐴) = -(∗‘𝐴))

Theoremaddcjd 9435 A number plus its conjugate is twice its real part. Compare Proposition 10-3.4(h) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)       (𝜑 → (𝐴 + (∗‘𝐴)) = (2 · (ℜ‘𝐴)))

Theoremcjexpd 9436 Complex conjugate of positive integer exponentiation. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝑁 ∈ ℕ0)       (𝜑 → (∗‘(𝐴𝑁)) = ((∗‘𝐴)↑𝑁))

Theoremreaddd 9437 Real part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)       (𝜑 → (ℜ‘(𝐴 + 𝐵)) = ((ℜ‘𝐴) + (ℜ‘𝐵)))

Theoremimaddd 9438 Imaginary part distributes over addition. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)       (𝜑 → (ℑ‘(𝐴 + 𝐵)) = ((ℑ‘𝐴) + (ℑ‘𝐵)))

Theoremresubd 9439 Real part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)       (𝜑 → (ℜ‘(𝐴𝐵)) = ((ℜ‘𝐴) − (ℜ‘𝐵)))

Theoremimsubd 9440 Imaginary part distributes over subtraction. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)       (𝜑 → (ℑ‘(𝐴𝐵)) = ((ℑ‘𝐴) − (ℑ‘𝐵)))

Theoremremuld 9441 Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)       (𝜑 → (ℜ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℜ‘𝐵)) − ((ℑ‘𝐴) · (ℑ‘𝐵))))

Theoremimmuld 9442 Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)       (𝜑 → (ℑ‘(𝐴 · 𝐵)) = (((ℜ‘𝐴) · (ℑ‘𝐵)) + ((ℑ‘𝐴) · (ℜ‘𝐵))))

Theoremcjaddd 9443 Complex conjugate distributes over addition. Proposition 10-3.4(a) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)       (𝜑 → (∗‘(𝐴 + 𝐵)) = ((∗‘𝐴) + (∗‘𝐵)))

Theoremcjmuld 9444 Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)       (𝜑 → (∗‘(𝐴 · 𝐵)) = ((∗‘𝐴) · (∗‘𝐵)))

Theoremipcnd 9445 Standard inner product on complex numbers. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)       (𝜑 → (ℜ‘(𝐴 · (∗‘𝐵))) = (((ℜ‘𝐴) · (ℜ‘𝐵)) + ((ℑ‘𝐴) · (ℑ‘𝐵))))

Theoremcjdivapd 9446 Complex conjugate distributes over division. (Contributed by Jim Kingdon, 15-Jun-2020.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)    &   (𝜑𝐵 # 0)       (𝜑 → (∗‘(𝐴 / 𝐵)) = ((∗‘𝐴) / (∗‘𝐵)))

Theoremrered 9447 A real number equals its real part. One direction of Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℝ)       (𝜑 → (ℜ‘𝐴) = 𝐴)

Theoremreim0d 9448 The imaginary part of a real number is 0. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℝ)       (𝜑 → (ℑ‘𝐴) = 0)

Theoremcjred 9449 A real number equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℝ)       (𝜑 → (∗‘𝐴) = 𝐴)

Theoremremul2d 9450 Real part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℂ)       (𝜑 → (ℜ‘(𝐴 · 𝐵)) = (𝐴 · (ℜ‘𝐵)))

Theoremimmul2d 9451 Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℂ)       (𝜑 → (ℑ‘(𝐴 · 𝐵)) = (𝐴 · (ℑ‘𝐵)))

Theoremredivapd 9452 Real part of a division. Related to remul2 9351. (Contributed by Jim Kingdon, 15-Jun-2020.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℂ)    &   (𝜑𝐴 # 0)       (𝜑 → (ℜ‘(𝐵 / 𝐴)) = ((ℜ‘𝐵) / 𝐴))

Theoremimdivapd 9453 Imaginary part of a division. Related to remul2 9351. (Contributed by Jim Kingdon, 15-Jun-2020.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℂ)    &   (𝜑𝐴 # 0)       (𝜑 → (ℑ‘(𝐵 / 𝐴)) = ((ℑ‘𝐵) / 𝐴))

Theoremcrred 9454 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 9455 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.6.3  Sequence convergence

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

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

Theoremcaucvgre 9458* 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 9459 Lemma for cvg1n 9463. Rearranging an expression related to the rate of convergence. (Contributed by Jim Kingdon, 6-Aug-2021.)
(𝜑𝐶 ∈ ℝ+)    &   (𝜑𝑋 ∈ ℝ+)    &   (𝜑𝑍 ∈ ℕ)    &   (𝜑𝐸 ∈ ℕ)    &   (𝜑𝐴 ∈ ℕ)    &   (𝜑 → ((((𝐶 · 2) / 𝑋) / 𝑍) + 𝐴) < 𝐸)       (𝜑 → (𝐶 / (𝐸 · 𝑍)) < (𝑋 / 2))

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

Theoremcvg1nlemcau 9461* Lemma for cvg1n 9463. 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 9462* Lemma for cvg1n 9463. 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 9463* Convergence of real sequences.

This is a version of caucvgre 9458 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 9464 The upper integers are closed under intersection. (Contributed by Mario Carneiro, 24-Dec-2013.)
((𝐴 ∈ ran ℤ𝐵 ∈ ran ℤ) → (𝐴𝐵) ∈ ran ℤ)

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

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

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

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

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

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

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

3.6.4  Square root; absolute value

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

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

Definitiondf-rsqrt 9474* 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 9475 Define the function for the absolute value (modulus) of a complex number. (Contributed by NM, 27-Jul-1999.)
abs = (𝑥 ∈ ℂ ↦ (√‘(𝑥 · (∗‘𝑥))))

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

Theoremabsval 9477 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 9478 A real number does not lie on the negative imaginary axis. (Contributed by Mario Carneiro, 8-Jul-2013.)
(𝐴 ∈ ℝ → (i · 𝐴) ∉ ℝ+)

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

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

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

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

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

Theoremresqrexlemf1 9484* Lemma for resqrex 9502. 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 9485* Lemma for resqrex 9502. 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 9486* Lemma for resqrex 9502. Each element of the sequence is an overestimate. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.)
𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}), ℝ+)    &   (𝜑𝐴 ∈ ℝ)    &   (𝜑 → 0 ≤ 𝐴)       ((𝜑𝑁 ∈ ℕ) → 𝐴 < ((𝐹𝑁)↑2))

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

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

Theoremresqrexlemlo 9489* Lemma for resqrex 9502. 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 9490* Lemma for resqrex 9502. 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 9491* Lemma for resqrex 9502. 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 9492* Lemma for resqrex 9502. 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 9493* Lemma for resqrex 9502. 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 9494* Lemma for resqrex 9502. 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 9495* Lemma for resqrex 9502. The sequence has a limit. (Contributed by Jim Kingdon, 6-Aug-2021.)
𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}), ℝ+)    &   (𝜑𝐴 ∈ ℝ)    &   (𝜑 → 0 ≤ 𝐴)       (𝜑 → ∃𝑟 ∈ ℝ ∀𝑥 ∈ ℝ+𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ𝑗)((𝐹𝑖) < (𝑟 + 𝑥) ∧ 𝑟 < ((𝐹𝑖) + 𝑥)))

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

Theoremresqrexlemoverl 9497* Lemma for resqrex 9502. 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 9498* Lemma for resqrex 9502. 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 9499* Lemma for resqrex 9502. 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 9500* Lemma for resqrex 9502. The square of a limit is 𝐴. (Contributed by Jim Kingdon, 7-Aug-2021.)
𝐹 = seq1((𝑦 ∈ ℝ+, 𝑧 ∈ ℝ+ ↦ ((𝑦 + (𝐴 / 𝑦)) / 2)), (ℕ × {(1 + 𝐴)}), ℝ+)    &   (𝜑𝐴 ∈ ℝ)    &   (𝜑 → 0 ≤ 𝐴)    &   (𝜑𝐿 ∈ ℝ)    &   (𝜑 → ∀𝑒 ∈ ℝ+𝑗 ∈ ℕ ∀𝑖 ∈ (ℤ𝑗)((𝐹𝑖) < (𝐿 + 𝑒) ∧ 𝐿 < ((𝐹𝑖) + 𝑒)))       (𝜑 → (𝐿↑2) = 𝐴)

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-9995
 Copyright terms: Public domain < Previous  Next >