HomeHome Intuitionistic Logic Explorer
Theorem List (p. 90 of 94)
< 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 - 8901-9000   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremexpap0i 8901 Integer exponentiation is apart from zero if its mantissa is apart from zero. (Contributed by Jim Kingdon, 10-Jun-2020.)
((A A # 0 𝑁 ℤ) → (A𝑁) # 0)
 
Theoremexpgt0 8902 Nonnegative integer exponentiation with a positive mantissa is positive. (Contributed by NM, 16-Dec-2005.) (Revised by Mario Carneiro, 4-Jun-2014.)
((A 𝑁 0 < A) → 0 < (A𝑁))
 
Theoremexpnegzap 8903 Value of a complex number raised to a negative power. (Contributed by Mario Carneiro, 4-Jun-2014.)
((A A # 0 𝑁 ℤ) → (A↑-𝑁) = (1 / (A𝑁)))
 
Theorem0exp 8904 Value of zero raised to a positive integer power. (Contributed by NM, 19-Aug-2004.)
(𝑁 ℕ → (0↑𝑁) = 0)
 
Theoremexpge0 8905 Nonnegative integer exponentiation with a nonnegative mantissa is nonnegative. (Contributed by NM, 16-Dec-2005.) (Revised by Mario Carneiro, 4-Jun-2014.)
((A 𝑁 0 0 ≤ A) → 0 ≤ (A𝑁))
 
Theoremexpge1 8906 Nonnegative integer exponentiation with a mantissa greater than or equal to 1 is greater than or equal to 1. (Contributed by NM, 21-Feb-2005.) (Revised by Mario Carneiro, 4-Jun-2014.)
((A 𝑁 0 1 ≤ A) → 1 ≤ (A𝑁))
 
Theoremexpgt1 8907 Positive integer exponentiation with a mantissa greater than 1 is greater than 1. (Contributed by NM, 13-Feb-2005.) (Revised by Mario Carneiro, 4-Jun-2014.)
((A 𝑁 1 < A) → 1 < (A𝑁))
 
Theoremmulexp 8908 Positive integer exponentiation of a product. Proposition 10-4.2(c) of [Gleason] p. 135, restricted to nonnegative integer exponents. (Contributed by NM, 13-Feb-2005.)
((A B 𝑁 0) → ((A · B)↑𝑁) = ((A𝑁) · (B𝑁)))
 
Theoremmulexpzap 8909 Integer exponentiation of a product. (Contributed by Jim Kingdon, 10-Jun-2020.)
(((A A # 0) (B B # 0) 𝑁 ℤ) → ((A · B)↑𝑁) = ((A𝑁) · (B𝑁)))
 
Theoremexprecap 8910 Nonnegative integer exponentiation of a reciprocal. (Contributed by Jim Kingdon, 10-Jun-2020.)
((A A # 0 𝑁 ℤ) → ((1 / A)↑𝑁) = (1 / (A𝑁)))
 
Theoremexpadd 8911 Sum of exponents law for nonnegative integer exponentiation. Proposition 10-4.2(a) of [Gleason] p. 135. (Contributed by NM, 30-Nov-2004.)
((A 𝑀 0 𝑁 0) → (A↑(𝑀 + 𝑁)) = ((A𝑀) · (A𝑁)))
 
Theoremexpaddzaplem 8912 Lemma for expaddzap 8913. (Contributed by Jim Kingdon, 10-Jun-2020.)
(((A A # 0) (𝑀 -𝑀 ℕ) 𝑁 0) → (A↑(𝑀 + 𝑁)) = ((A𝑀) · (A𝑁)))
 
Theoremexpaddzap 8913 Sum of exponents law for integer exponentiation. (Contributed by Jim Kingdon, 10-Jun-2020.)
(((A A # 0) (𝑀 𝑁 ℤ)) → (A↑(𝑀 + 𝑁)) = ((A𝑀) · (A𝑁)))
 
Theoremexpmul 8914 Product of exponents law for positive integer exponentiation. Proposition 10-4.2(b) of [Gleason] p. 135, restricted to nonnegative integer exponents. (Contributed by NM, 4-Jan-2006.)
((A 𝑀 0 𝑁 0) → (A↑(𝑀 · 𝑁)) = ((A𝑀)↑𝑁))
 
Theoremexpmulzap 8915 Product of exponents law for integer exponentiation. (Contributed by Jim Kingdon, 11-Jun-2020.)
(((A A # 0) (𝑀 𝑁 ℤ)) → (A↑(𝑀 · 𝑁)) = ((A𝑀)↑𝑁))
 
Theoremexpsubap 8916 Exponent subtraction law for nonnegative integer exponentiation. (Contributed by Jim Kingdon, 11-Jun-2020.)
(((A A # 0) (𝑀 𝑁 ℤ)) → (A↑(𝑀𝑁)) = ((A𝑀) / (A𝑁)))
 
Theoremexpp1zap 8917 Value of a nonzero complex number raised to an integer power plus one. (Contributed by Jim Kingdon, 11-Jun-2020.)
((A A # 0 𝑁 ℤ) → (A↑(𝑁 + 1)) = ((A𝑁) · A))
 
Theoremexpm1ap 8918 Value of a complex number raised to an integer power minus one. (Contributed by Jim Kingdon, 11-Jun-2020.)
((A A # 0 𝑁 ℤ) → (A↑(𝑁 − 1)) = ((A𝑁) / A))
 
Theoremexpdivap 8919 Nonnegative integer exponentiation of a quotient. (Contributed by Jim Kingdon, 11-Jun-2020.)
((A (B B # 0) 𝑁 0) → ((A / B)↑𝑁) = ((A𝑁) / (B𝑁)))
 
Theoremltexp2a 8920 Ordering relationship for exponentiation. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 4-Jun-2014.)
(((A 𝑀 𝑁 ℤ) (1 < A 𝑀 < 𝑁)) → (A𝑀) < (A𝑁))
 
Theoremleexp2a 8921 Weak ordering relationship for exponentiation. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 5-Jun-2014.)
((A 1 ≤ A 𝑁 (ℤ𝑀)) → (A𝑀) ≤ (A𝑁))
 
Theoremleexp2r 8922 Weak ordering relationship for exponentiation. (Contributed by Paul Chapman, 14-Jan-2008.) (Revised by Mario Carneiro, 29-Apr-2014.)
(((A 𝑀 0 𝑁 (ℤ𝑀)) (0 ≤ A A ≤ 1)) → (A𝑁) ≤ (A𝑀))
 
Theoremleexp1a 8923 Weak mantissa ordering relationship for exponentiation. (Contributed by NM, 18-Dec-2005.)
(((A B 𝑁 0) (0 ≤ A AB)) → (A𝑁) ≤ (B𝑁))
 
Theoremexple1 8924 Nonnegative integer exponentiation with a mantissa between 0 and 1 inclusive is less than or equal to 1. (Contributed by Paul Chapman, 29-Dec-2007.) (Revised by Mario Carneiro, 5-Jun-2014.)
(((A 0 ≤ A A ≤ 1) 𝑁 0) → (A𝑁) ≤ 1)
 
Theoremexpubnd 8925 An upper bound on A𝑁 when 2 ≤ A. (Contributed by NM, 19-Dec-2005.)
((A 𝑁 0 2 ≤ A) → (A𝑁) ≤ ((2↑𝑁) · ((A − 1)↑𝑁)))
 
Theoremsqval 8926 Value of the square of a complex number. (Contributed by Raph Levien, 10-Apr-2004.)
(A ℂ → (A↑2) = (A · A))
 
Theoremsqneg 8927 The square of the negative of a number.) (Contributed by NM, 15-Jan-2006.)
(A ℂ → (-A↑2) = (A↑2))
 
Theoremsqsubswap 8928 Swap the order of subtraction in a square. (Contributed by Scott Fenton, 10-Jun-2013.)
((A B ℂ) → ((AB)↑2) = ((BA)↑2))
 
Theoremsqcl 8929 Closure of square. (Contributed by NM, 10-Aug-1999.)
(A ℂ → (A↑2) ℂ)
 
Theoremsqmul 8930 Distribution of square over multiplication. (Contributed by NM, 21-Mar-2008.)
((A B ℂ) → ((A · B)↑2) = ((A↑2) · (B↑2)))
 
Theoremsqeq0 8931 A number is zero iff its square is zero. (Contributed by NM, 11-Mar-2006.)
(A ℂ → ((A↑2) = 0 ↔ A = 0))
 
Theoremsqdivap 8932 Distribution of square over division. (Contributed by Jim Kingdon, 11-Jun-2020.)
((A B B # 0) → ((A / B)↑2) = ((A↑2) / (B↑2)))
 
Theoremsqne0 8933 A number is nonzero iff its square is nonzero. (Contributed by NM, 11-Mar-2006.)
(A ℂ → ((A↑2) ≠ 0 ↔ A ≠ 0))
 
Theoremresqcl 8934 Closure of the square of a real number. (Contributed by NM, 18-Oct-1999.)
(A ℝ → (A↑2) ℝ)
 
Theoremsqgt0ap 8935 The square of a nonzero real is positive. (Contributed by Jim Kingdon, 11-Jun-2020.)
((A A # 0) → 0 < (A↑2))
 
Theoremnnsqcl 8936 The naturals are closed under squaring. (Contributed by Scott Fenton, 29-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
(A ℕ → (A↑2) ℕ)
 
Theoremzsqcl 8937 Integers are closed under squaring. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
(A ℤ → (A↑2) ℤ)
 
Theoremqsqcl 8938 The square of a rational is rational. (Contributed by Stefan O'Rear, 15-Sep-2014.)
(A ℚ → (A↑2) ℚ)
 
Theoremsq11 8939 The square function is one-to-one for nonnegative reals. (Contributed by NM, 8-Apr-2001.) (Proof shortened by Mario Carneiro, 28-May-2016.)
(((A 0 ≤ A) (B 0 ≤ B)) → ((A↑2) = (B↑2) ↔ A = B))
 
Theoremlt2sq 8940 The square function on nonnegative reals is strictly monotonic. (Contributed by NM, 24-Feb-2006.)
(((A 0 ≤ A) (B 0 ≤ B)) → (A < B ↔ (A↑2) < (B↑2)))
 
Theoremle2sq 8941 The square function on nonnegative reals is monotonic. (Contributed by NM, 18-Oct-1999.)
(((A 0 ≤ A) (B 0 ≤ B)) → (AB ↔ (A↑2) ≤ (B↑2)))
 
Theoremle2sq2 8942 The square of a 'less than or equal to' ordering. (Contributed by NM, 21-Mar-2008.)
(((A 0 ≤ A) (B AB)) → (A↑2) ≤ (B↑2))
 
Theoremsqge0 8943 A square of a real is nonnegative. (Contributed by NM, 18-Oct-1999.)
(A ℝ → 0 ≤ (A↑2))
 
Theoremzsqcl2 8944 The square of an integer is a nonnegative integer. (Contributed by Mario Carneiro, 18-Apr-2014.) (Revised by Mario Carneiro, 14-Jul-2014.)
(A ℤ → (A↑2) 0)
 
Theoremsumsqeq0 8945 Two real numbers are equal to 0 iff their Euclidean norm is. (Contributed by NM, 29-Apr-2005.) (Revised by Stefan O'Rear, 5-Oct-2014.) (Proof shortened by Mario Carneiro, 28-May-2016.)
((A B ℝ) → ((A = 0 B = 0) ↔ ((A↑2) + (B↑2)) = 0))
 
Theoremsqvali 8946 Value of square. Inference version. (Contributed by NM, 1-Aug-1999.)
A        (A↑2) = (A · A)
 
Theoremsqcli 8947 Closure of square. (Contributed by NM, 2-Aug-1999.)
A        (A↑2)
 
Theoremsqeq0i 8948 A number is zero iff its square is zero. (Contributed by NM, 2-Oct-1999.)
A        ((A↑2) = 0 ↔ A = 0)
 
Theoremsqmuli 8949 Distribution of square over multiplication. (Contributed by NM, 3-Sep-1999.)
A     &   B        ((A · B)↑2) = ((A↑2) · (B↑2))
 
Theoremsqdivapi 8950 Distribution of square over division. (Contributed by Jim Kingdon, 12-Jun-2020.)
A     &   B     &   B # 0       ((A / B)↑2) = ((A↑2) / (B↑2))
 
Theoremresqcli 8951 Closure of square in reals. (Contributed by NM, 2-Aug-1999.)
A        (A↑2)
 
Theoremsqgt0api 8952 The square of a nonzero real is positive. (Contributed by Jim Kingdon, 12-Jun-2020.)
A        (A # 0 → 0 < (A↑2))
 
Theoremsqge0i 8953 A square of a real is nonnegative. (Contributed by NM, 3-Aug-1999.)
A        0 ≤ (A↑2)
 
Theoremlt2sqi 8954 The square function on nonnegative reals is strictly monotonic. (Contributed by NM, 12-Sep-1999.)
A     &   B        ((0 ≤ A 0 ≤ B) → (A < B ↔ (A↑2) < (B↑2)))
 
Theoremle2sqi 8955 The square function on nonnegative reals is monotonic. (Contributed by NM, 12-Sep-1999.)
A     &   B        ((0 ≤ A 0 ≤ B) → (AB ↔ (A↑2) ≤ (B↑2)))
 
Theoremsq11i 8956 The square function is one-to-one for nonnegative reals. (Contributed by NM, 27-Oct-1999.)
A     &   B        ((0 ≤ A 0 ≤ B) → ((A↑2) = (B↑2) ↔ A = B))
 
Theoremsq0 8957 The square of 0 is 0. (Contributed by NM, 6-Jun-2006.)
(0↑2) = 0
 
Theoremsq0i 8958 If a number is zero, its square is zero. (Contributed by FL, 10-Dec-2006.)
(A = 0 → (A↑2) = 0)
 
Theoremsq0id 8959 If a number is zero, its square is zero. Deduction form of sq0i 8958. Converse of sqeq0d 8993. (Contributed by David Moews, 28-Feb-2017.)
(φA = 0)       (φ → (A↑2) = 0)
 
Theoremsq1 8960 The square of 1 is 1. (Contributed by NM, 22-Aug-1999.)
(1↑2) = 1
 
Theoremneg1sqe1 8961 -1 squared is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
(-1↑2) = 1
 
Theoremsq2 8962 The square of 2 is 4. (Contributed by NM, 22-Aug-1999.)
(2↑2) = 4
 
Theoremsq3 8963 The square of 3 is 9. (Contributed by NM, 26-Apr-2006.)
(3↑2) = 9
 
Theoremcu2 8964 The cube of 2 is 8. (Contributed by NM, 2-Aug-2004.)
(2↑3) = 8
 
Theoremirec 8965 The reciprocal of i. (Contributed by NM, 11-Oct-1999.)
(1 / i) = -i
 
Theoremi2 8966 i squared. (Contributed by NM, 6-May-1999.)
(i↑2) = -1
 
Theoremi3 8967 i cubed. (Contributed by NM, 31-Jan-2007.)
(i↑3) = -i
 
Theoremi4 8968 i to the fourth power. (Contributed by NM, 31-Jan-2007.)
(i↑4) = 1
 
Theoremnnlesq 8969 A positive integer is less than or equal to its square. (Contributed by NM, 15-Sep-1999.) (Revised by Mario Carneiro, 12-Sep-2015.)
(𝑁 ℕ → 𝑁 ≤ (𝑁↑2))
 
Theoremexpnass 8970 A counterexample showing that exponentiation is not associative. (Contributed by Stefan Allan and Gérard Lang, 21-Sep-2010.)
((3↑3)↑3) < (3↑(3↑3))
 
Theoremsubsq 8971 Factor the difference of two squares. (Contributed by NM, 21-Feb-2008.)
((A B ℂ) → ((A↑2) − (B↑2)) = ((A + B) · (AB)))
 
Theoremsubsq2 8972 Express the difference of the squares of two numbers as a polynomial in the difference of the numbers. (Contributed by NM, 21-Feb-2008.)
((A B ℂ) → ((A↑2) − (B↑2)) = (((AB)↑2) + ((2 · B) · (AB))))
 
Theorembinom2i 8973 The square of a binomial. (Contributed by NM, 11-Aug-1999.)
A     &   B        ((A + B)↑2) = (((A↑2) + (2 · (A · B))) + (B↑2))
 
Theoremsubsqi 8974 Factor the difference of two squares. (Contributed by NM, 7-Feb-2005.)
A     &   B        ((A↑2) − (B↑2)) = ((A + B) · (AB))
 
Theorembinom2 8975 The square of a binomial. (Contributed by FL, 10-Dec-2006.)
((A B ℂ) → ((A + B)↑2) = (((A↑2) + (2 · (A · B))) + (B↑2)))
 
Theorembinom21 8976 Special case of binom2 8975 where B = 1. (Contributed by Scott Fenton, 11-May-2014.)
(A ℂ → ((A + 1)↑2) = (((A↑2) + (2 · A)) + 1))
 
Theorembinom2sub 8977 Expand the square of a subtraction. (Contributed by Scott Fenton, 10-Jun-2013.)
((A B ℂ) → ((AB)↑2) = (((A↑2) − (2 · (A · B))) + (B↑2)))
 
Theorembinom2subi 8978 Expand the square of a subtraction. (Contributed by Scott Fenton, 13-Jun-2013.)
A     &   B        ((AB)↑2) = (((A↑2) − (2 · (A · B))) + (B↑2))
 
Theorembinom3 8979 The cube of a binomial. (Contributed by Mario Carneiro, 24-Apr-2015.)
((A B ℂ) → ((A + B)↑3) = (((A↑3) + (3 · ((A↑2) · B))) + ((3 · (A · (B↑2))) + (B↑3))))
 
Theoremzesq 8980 An integer is even iff its square is even. (Contributed by Mario Carneiro, 12-Sep-2015.)
(𝑁 ℤ → ((𝑁 / 2) ℤ ↔ ((𝑁↑2) / 2) ℤ))
 
Theoremnnesq 8981 A positive integer is even iff its square is even. (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 12-Sep-2015.)
(𝑁 ℕ → ((𝑁 / 2) ℕ ↔ ((𝑁↑2) / 2) ℕ))
 
Theorembernneq 8982 Bernoulli's inequality, due to Johan Bernoulli (1667-1748). (Contributed by NM, 21-Feb-2005.)
((A 𝑁 0 -1 ≤ A) → (1 + (A · 𝑁)) ≤ ((1 + A)↑𝑁))
 
Theorembernneq2 8983 Variation of Bernoulli's inequality bernneq 8982. (Contributed by NM, 18-Oct-2007.)
((A 𝑁 0 0 ≤ A) → (((A − 1) · 𝑁) + 1) ≤ (A𝑁))
 
Theorembernneq3 8984 A corollary of bernneq 8982. (Contributed by Mario Carneiro, 11-Mar-2014.)
((𝑃 (ℤ‘2) 𝑁 0) → 𝑁 < (𝑃𝑁))
 
Theoremexpnbnd 8985* Exponentiation with a mantissa greater than 1 has no upper bound. (Contributed by NM, 20-Oct-2007.)
((A B 1 < B) → 𝑘 A < (B𝑘))
 
Theoremexpnlbnd 8986* The reciprocal of exponentiation with a mantissa greater than 1 has no lower bound. (Contributed by NM, 18-Jul-2008.)
((A + B 1 < B) → 𝑘 ℕ (1 / (B𝑘)) < A)
 
Theoremexpnlbnd2 8987* The reciprocal of exponentiation with a mantissa greater than 1 has no lower bound. (Contributed by NM, 18-Jul-2008.) (Proof shortened by Mario Carneiro, 5-Jun-2014.)
((A + B 1 < B) → 𝑗 𝑘 (ℤ𝑗)(1 / (B𝑘)) < A)
 
Theoremexp0d 8988 Value of a complex number raised to the 0th power. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℂ)       (φ → (A↑0) = 1)
 
Theoremexp1d 8989 Value of a complex number raised to the first power. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℂ)       (φ → (A↑1) = A)
 
Theoremexpeq0d 8990 Positive integer exponentiation is 0 iff its mantissa is 0. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℂ)    &   (φ𝑁 ℕ)    &   (φ → (A𝑁) = 0)       (φA = 0)
 
Theoremsqvald 8991 Value of square. Inference version. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℂ)       (φ → (A↑2) = (A · A))
 
Theoremsqcld 8992 Closure of square. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℂ)       (φ → (A↑2) ℂ)
 
Theoremsqeq0d 8993 A number is zero iff its square is zero. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℂ)    &   (φ → (A↑2) = 0)       (φA = 0)
 
Theoremexpcld 8994 Closure law for nonnegative integer exponentiation. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℂ)    &   (φ𝑁 0)       (φ → (A𝑁) ℂ)
 
Theoremexpp1d 8995 Value of a complex number raised to a nonnegative integer power plus one. Part of Definition 10-4.1 of [Gleason] p. 134. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℂ)    &   (φ𝑁 0)       (φ → (A↑(𝑁 + 1)) = ((A𝑁) · A))
 
Theoremexpaddd 8996 Sum of exponents law for nonnegative integer exponentiation. Proposition 10-4.2(a) of [Gleason] p. 135. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℂ)    &   (φ𝑁 0)    &   (φ𝑀 0)       (φ → (A↑(𝑀 + 𝑁)) = ((A𝑀) · (A𝑁)))
 
Theoremexpmuld 8997 Product of exponents law for positive integer exponentiation. Proposition 10-4.2(b) of [Gleason] p. 135, restricted to nonnegative integer exponents. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℂ)    &   (φ𝑁 0)    &   (φ𝑀 0)       (φ → (A↑(𝑀 · 𝑁)) = ((A𝑀)↑𝑁))
 
Theoremsqrecapd 8998 Square of reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.)
(φA ℂ)    &   (φA # 0)       (φ → ((1 / A)↑2) = (1 / (A↑2)))
 
Theoremexpclzapd 8999 Closure law for integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.)
(φA ℂ)    &   (φA # 0)    &   (φ𝑁 ℤ)       (φ → (A𝑁) ℂ)
 
Theoremexpap0d 9000 Nonnegative integer exponentiation is nonzero if its mantissa is nonzero. (Contributed by Jim Kingdon, 12-Jun-2020.)
(φA ℂ)    &   (φA # 0)    &   (φ𝑁 ℤ)       (φ → (A𝑁) # 0)
    < Previous  Next >

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