HomeHome Intuitionistic Logic Explorer
Theorem List (p. 120 of 149)
< 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 - 11901-12000   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremopeo 11901 The sum of an odd and an even is odd. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
(((𝐴 ∈ β„€ ∧ Β¬ 2 βˆ₯ 𝐴) ∧ (𝐡 ∈ β„€ ∧ 2 βˆ₯ 𝐡)) β†’ Β¬ 2 βˆ₯ (𝐴 + 𝐡))
 
Theoremomeo 11902 The difference of an odd and an even is odd. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
(((𝐴 ∈ β„€ ∧ Β¬ 2 βˆ₯ 𝐴) ∧ (𝐡 ∈ β„€ ∧ 2 βˆ₯ 𝐡)) β†’ Β¬ 2 βˆ₯ (𝐴 βˆ’ 𝐡))
 
Theoremm1expe 11903 Exponentiation of -1 by an even power. Variant of m1expeven 10566. (Contributed by AV, 25-Jun-2021.)
(2 βˆ₯ 𝑁 β†’ (-1↑𝑁) = 1)
 
Theoremm1expo 11904 Exponentiation of -1 by an odd power. (Contributed by AV, 26-Jun-2021.)
((𝑁 ∈ β„€ ∧ Β¬ 2 βˆ₯ 𝑁) β†’ (-1↑𝑁) = -1)
 
Theoremm1exp1 11905 Exponentiation of negative one is one iff the exponent is even. (Contributed by AV, 20-Jun-2021.)
(𝑁 ∈ β„€ β†’ ((-1↑𝑁) = 1 ↔ 2 βˆ₯ 𝑁))
 
Theoremnn0enne 11906 A positive integer is an even nonnegative integer iff it is an even positive integer. (Contributed by AV, 30-May-2020.)
(𝑁 ∈ β„• β†’ ((𝑁 / 2) ∈ β„•0 ↔ (𝑁 / 2) ∈ β„•))
 
Theoremnn0ehalf 11907 The half of an even nonnegative integer is a nonnegative integer. (Contributed by AV, 22-Jun-2020.) (Revised by AV, 28-Jun-2021.)
((𝑁 ∈ β„•0 ∧ 2 βˆ₯ 𝑁) β†’ (𝑁 / 2) ∈ β„•0)
 
Theoremnnehalf 11908 The half of an even positive integer is a positive integer. (Contributed by AV, 28-Jun-2021.)
((𝑁 ∈ β„• ∧ 2 βˆ₯ 𝑁) β†’ (𝑁 / 2) ∈ β„•)
 
Theoremnn0o1gt2 11909 An odd nonnegative integer is either 1 or greater than 2. (Contributed by AV, 2-Jun-2020.)
((𝑁 ∈ β„•0 ∧ ((𝑁 + 1) / 2) ∈ β„•0) β†’ (𝑁 = 1 ∨ 2 < 𝑁))
 
Theoremnno 11910 An alternate characterization of an odd integer greater than 1. (Contributed by AV, 2-Jun-2020.)
((𝑁 ∈ (β„€β‰₯β€˜2) ∧ ((𝑁 + 1) / 2) ∈ β„•0) β†’ ((𝑁 βˆ’ 1) / 2) ∈ β„•)
 
Theoremnn0o 11911 An alternate characterization of an odd nonnegative integer. (Contributed by AV, 28-May-2020.) (Proof shortened by AV, 2-Jun-2020.)
((𝑁 ∈ β„•0 ∧ ((𝑁 + 1) / 2) ∈ β„•0) β†’ ((𝑁 βˆ’ 1) / 2) ∈ β„•0)
 
Theoremnn0ob 11912 Alternate characterizations of an odd nonnegative integer. (Contributed by AV, 4-Jun-2020.)
(𝑁 ∈ β„•0 β†’ (((𝑁 + 1) / 2) ∈ β„•0 ↔ ((𝑁 βˆ’ 1) / 2) ∈ β„•0))
 
Theoremnn0oddm1d2 11913 A positive integer is odd iff its predecessor divided by 2 is a positive integer. (Contributed by AV, 28-Jun-2021.)
(𝑁 ∈ β„•0 β†’ (Β¬ 2 βˆ₯ 𝑁 ↔ ((𝑁 βˆ’ 1) / 2) ∈ β„•0))
 
Theoremnnoddm1d2 11914 A positive integer is odd iff its successor divided by 2 is a positive integer. (Contributed by AV, 28-Jun-2021.)
(𝑁 ∈ β„• β†’ (Β¬ 2 βˆ₯ 𝑁 ↔ ((𝑁 + 1) / 2) ∈ β„•))
 
Theoremz0even 11915 0 is even. (Contributed by AV, 11-Feb-2020.) (Revised by AV, 23-Jun-2021.)
2 βˆ₯ 0
 
Theoremn2dvds1 11916 2 does not divide 1 (common case). That means 1 is odd. (Contributed by David A. Wheeler, 8-Dec-2018.)
Β¬ 2 βˆ₯ 1
 
Theoremn2dvdsm1 11917 2 does not divide -1. That means -1 is odd. (Contributed by AV, 15-Aug-2021.)
Β¬ 2 βˆ₯ -1
 
Theoremz2even 11918 2 is even. (Contributed by AV, 12-Feb-2020.) (Revised by AV, 23-Jun-2021.)
2 βˆ₯ 2
 
Theoremn2dvds3 11919 2 does not divide 3, i.e. 3 is an odd number. (Contributed by AV, 28-Feb-2021.)
Β¬ 2 βˆ₯ 3
 
Theoremz4even 11920 4 is an even number. (Contributed by AV, 23-Jul-2020.) (Revised by AV, 4-Jul-2021.)
2 βˆ₯ 4
 
Theorem4dvdseven 11921 An integer which is divisible by 4 is an even integer. (Contributed by AV, 4-Jul-2021.)
(4 βˆ₯ 𝑁 β†’ 2 βˆ₯ 𝑁)
 
5.1.3  The division algorithm
 
Theoremdivalglemnn 11922* Lemma for divalg 11928. Existence for a positive denominator. (Contributed by Jim Kingdon, 30-Nov-2021.)
((𝑁 ∈ β„€ ∧ 𝐷 ∈ β„•) β†’ βˆƒπ‘Ÿ ∈ β„€ βˆƒπ‘ž ∈ β„€ (0 ≀ π‘Ÿ ∧ π‘Ÿ < (absβ€˜π·) ∧ 𝑁 = ((π‘ž Β· 𝐷) + π‘Ÿ)))
 
Theoremdivalglemqt 11923 Lemma for divalg 11928. The 𝑄 = 𝑇 case involved in showing uniqueness. (Contributed by Jim Kingdon, 5-Dec-2021.)
(πœ‘ β†’ 𝐷 ∈ β„€)    &   (πœ‘ β†’ 𝑅 ∈ β„€)    &   (πœ‘ β†’ 𝑆 ∈ β„€)    &   (πœ‘ β†’ 𝑄 ∈ β„€)    &   (πœ‘ β†’ 𝑇 ∈ β„€)    &   (πœ‘ β†’ 𝑄 = 𝑇)    &   (πœ‘ β†’ ((𝑄 Β· 𝐷) + 𝑅) = ((𝑇 Β· 𝐷) + 𝑆))    β‡’   (πœ‘ β†’ 𝑅 = 𝑆)
 
Theoremdivalglemnqt 11924 Lemma for divalg 11928. The 𝑄 < 𝑇 case involved in showing uniqueness. (Contributed by Jim Kingdon, 4-Dec-2021.)
(πœ‘ β†’ 𝐷 ∈ β„•)    &   (πœ‘ β†’ 𝑅 ∈ β„€)    &   (πœ‘ β†’ 𝑆 ∈ β„€)    &   (πœ‘ β†’ 𝑄 ∈ β„€)    &   (πœ‘ β†’ 𝑇 ∈ β„€)    &   (πœ‘ β†’ 0 ≀ 𝑆)    &   (πœ‘ β†’ 𝑅 < 𝐷)    &   (πœ‘ β†’ ((𝑄 Β· 𝐷) + 𝑅) = ((𝑇 Β· 𝐷) + 𝑆))    β‡’   (πœ‘ β†’ Β¬ 𝑄 < 𝑇)
 
Theoremdivalglemeunn 11925* Lemma for divalg 11928. Uniqueness for a positive denominator. (Contributed by Jim Kingdon, 4-Dec-2021.)
((𝑁 ∈ β„€ ∧ 𝐷 ∈ β„•) β†’ βˆƒ!π‘Ÿ ∈ β„€ βˆƒπ‘ž ∈ β„€ (0 ≀ π‘Ÿ ∧ π‘Ÿ < (absβ€˜π·) ∧ 𝑁 = ((π‘ž Β· 𝐷) + π‘Ÿ)))
 
Theoremdivalglemex 11926* Lemma for divalg 11928. The quotient and remainder exist. (Contributed by Jim Kingdon, 30-Nov-2021.)
((𝑁 ∈ β„€ ∧ 𝐷 ∈ β„€ ∧ 𝐷 β‰  0) β†’ βˆƒπ‘Ÿ ∈ β„€ βˆƒπ‘ž ∈ β„€ (0 ≀ π‘Ÿ ∧ π‘Ÿ < (absβ€˜π·) ∧ 𝑁 = ((π‘ž Β· 𝐷) + π‘Ÿ)))
 
Theoremdivalglemeuneg 11927* Lemma for divalg 11928. Uniqueness for a negative denominator. (Contributed by Jim Kingdon, 4-Dec-2021.)
((𝑁 ∈ β„€ ∧ 𝐷 ∈ β„€ ∧ 𝐷 < 0) β†’ βˆƒ!π‘Ÿ ∈ β„€ βˆƒπ‘ž ∈ β„€ (0 ≀ π‘Ÿ ∧ π‘Ÿ < (absβ€˜π·) ∧ 𝑁 = ((π‘ž Β· 𝐷) + π‘Ÿ)))
 
Theoremdivalg 11928* The division algorithm (theorem). Dividing an integer 𝑁 by a nonzero integer 𝐷 produces a (unique) quotient π‘ž and a unique remainder 0 ≀ π‘Ÿ < (absβ€˜π·). Theorem 1.14 in [ApostolNT] p. 19. (Contributed by Paul Chapman, 21-Mar-2011.)
((𝑁 ∈ β„€ ∧ 𝐷 ∈ β„€ ∧ 𝐷 β‰  0) β†’ βˆƒ!π‘Ÿ ∈ β„€ βˆƒπ‘ž ∈ β„€ (0 ≀ π‘Ÿ ∧ π‘Ÿ < (absβ€˜π·) ∧ 𝑁 = ((π‘ž Β· 𝐷) + π‘Ÿ)))
 
Theoremdivalgb 11929* Express the division algorithm as stated in divalg 11928 in terms of βˆ₯. (Contributed by Paul Chapman, 31-Mar-2011.)
((𝑁 ∈ β„€ ∧ 𝐷 ∈ β„€ ∧ 𝐷 β‰  0) β†’ (βˆƒ!π‘Ÿ ∈ β„€ βˆƒπ‘ž ∈ β„€ (0 ≀ π‘Ÿ ∧ π‘Ÿ < (absβ€˜π·) ∧ 𝑁 = ((π‘ž Β· 𝐷) + π‘Ÿ)) ↔ βˆƒ!π‘Ÿ ∈ β„•0 (π‘Ÿ < (absβ€˜π·) ∧ 𝐷 βˆ₯ (𝑁 βˆ’ π‘Ÿ))))
 
Theoremdivalg2 11930* The division algorithm (theorem) for a positive divisor. (Contributed by Paul Chapman, 21-Mar-2011.)
((𝑁 ∈ β„€ ∧ 𝐷 ∈ β„•) β†’ βˆƒ!π‘Ÿ ∈ β„•0 (π‘Ÿ < 𝐷 ∧ 𝐷 βˆ₯ (𝑁 βˆ’ π‘Ÿ)))
 
Theoremdivalgmod 11931 The result of the mod operator satisfies the requirements for the remainder 𝑅 in the division algorithm for a positive divisor (compare divalg2 11930 and divalgb 11929). This demonstration theorem justifies the use of mod to yield an explicit remainder from this point forward. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by AV, 21-Aug-2021.)
((𝑁 ∈ β„€ ∧ 𝐷 ∈ β„•) β†’ (𝑅 = (𝑁 mod 𝐷) ↔ (𝑅 ∈ β„•0 ∧ (𝑅 < 𝐷 ∧ 𝐷 βˆ₯ (𝑁 βˆ’ 𝑅)))))
 
Theoremdivalgmodcl 11932 The result of the mod operator satisfies the requirements for the remainder 𝑅 in the division algorithm for a positive divisor. Variant of divalgmod 11931. (Contributed by Stefan O'Rear, 17-Oct-2014.) (Proof shortened by AV, 21-Aug-2021.)
((𝑁 ∈ β„€ ∧ 𝐷 ∈ β„• ∧ 𝑅 ∈ β„•0) β†’ (𝑅 = (𝑁 mod 𝐷) ↔ (𝑅 < 𝐷 ∧ 𝐷 βˆ₯ (𝑁 βˆ’ 𝑅))))
 
Theoremmodremain 11933* The result of the modulo operation is the remainder of the division algorithm. (Contributed by AV, 19-Aug-2021.)
((𝑁 ∈ β„€ ∧ 𝐷 ∈ β„• ∧ (𝑅 ∈ β„•0 ∧ 𝑅 < 𝐷)) β†’ ((𝑁 mod 𝐷) = 𝑅 ↔ βˆƒπ‘§ ∈ β„€ ((𝑧 Β· 𝐷) + 𝑅) = 𝑁))
 
Theoremndvdssub 11934 Corollary of the division algorithm. If an integer 𝐷 greater than 1 divides 𝑁, then it does not divide any of 𝑁 βˆ’ 1, 𝑁 βˆ’ 2... 𝑁 βˆ’ (𝐷 βˆ’ 1). (Contributed by Paul Chapman, 31-Mar-2011.)
((𝑁 ∈ β„€ ∧ 𝐷 ∈ β„• ∧ (𝐾 ∈ β„• ∧ 𝐾 < 𝐷)) β†’ (𝐷 βˆ₯ 𝑁 β†’ Β¬ 𝐷 βˆ₯ (𝑁 βˆ’ 𝐾)))
 
Theoremndvdsadd 11935 Corollary of the division algorithm. If an integer 𝐷 greater than 1 divides 𝑁, then it does not divide any of 𝑁 + 1, 𝑁 + 2... 𝑁 + (𝐷 βˆ’ 1). (Contributed by Paul Chapman, 31-Mar-2011.)
((𝑁 ∈ β„€ ∧ 𝐷 ∈ β„• ∧ (𝐾 ∈ β„• ∧ 𝐾 < 𝐷)) β†’ (𝐷 βˆ₯ 𝑁 β†’ Β¬ 𝐷 βˆ₯ (𝑁 + 𝐾)))
 
Theoremndvdsp1 11936 Special case of ndvdsadd 11935. If an integer 𝐷 greater than 1 divides 𝑁, it does not divide 𝑁 + 1. (Contributed by Paul Chapman, 31-Mar-2011.)
((𝑁 ∈ β„€ ∧ 𝐷 ∈ β„• ∧ 1 < 𝐷) β†’ (𝐷 βˆ₯ 𝑁 β†’ Β¬ 𝐷 βˆ₯ (𝑁 + 1)))
 
Theoremndvdsi 11937 A quick test for non-divisibility. (Contributed by Mario Carneiro, 18-Feb-2014.)
𝐴 ∈ β„•    &   π‘„ ∈ β„•0    &   π‘… ∈ β„•    &   ((𝐴 Β· 𝑄) + 𝑅) = 𝐡    &   π‘… < 𝐴    β‡’    Β¬ 𝐴 βˆ₯ 𝐡
 
Theoremflodddiv4 11938 The floor of an odd integer divided by 4. (Contributed by AV, 17-Jun-2021.)
((𝑀 ∈ β„€ ∧ 𝑁 = ((2 Β· 𝑀) + 1)) β†’ (βŒŠβ€˜(𝑁 / 4)) = if(2 βˆ₯ 𝑀, (𝑀 / 2), ((𝑀 βˆ’ 1) / 2)))
 
Theoremfldivndvdslt 11939 The floor of an integer divided by a nonzero integer not dividing the first integer is less than the integer divided by the positive integer. (Contributed by AV, 4-Jul-2021.)
((𝐾 ∈ β„€ ∧ (𝐿 ∈ β„€ ∧ 𝐿 β‰  0) ∧ Β¬ 𝐿 βˆ₯ 𝐾) β†’ (βŒŠβ€˜(𝐾 / 𝐿)) < (𝐾 / 𝐿))
 
Theoremflodddiv4lt 11940 The floor of an odd number divided by 4 is less than the odd number divided by 4. (Contributed by AV, 4-Jul-2021.)
((𝑁 ∈ β„€ ∧ Β¬ 2 βˆ₯ 𝑁) β†’ (βŒŠβ€˜(𝑁 / 4)) < (𝑁 / 4))
 
Theoremflodddiv4t2lthalf 11941 The floor of an odd number divided by 4, multiplied by 2 is less than the half of the odd number. (Contributed by AV, 4-Jul-2021.)
((𝑁 ∈ β„€ ∧ Β¬ 2 βˆ₯ 𝑁) β†’ ((βŒŠβ€˜(𝑁 / 4)) Β· 2) < (𝑁 / 2))
 
5.1.4  The greatest common divisor operator
 
Syntaxcgcd 11942 Extend the definition of a class to include the greatest common divisor operator.
class gcd
 
Definitiondf-gcd 11943* Define the gcd operator. For example, (-6 gcd 9) = 3 (ex-gcd 14453). (Contributed by Paul Chapman, 21-Mar-2011.)
gcd = (π‘₯ ∈ β„€, 𝑦 ∈ β„€ ↦ if((π‘₯ = 0 ∧ 𝑦 = 0), 0, sup({𝑛 ∈ β„€ ∣ (𝑛 βˆ₯ π‘₯ ∧ 𝑛 βˆ₯ 𝑦)}, ℝ, < )))
 
Theoremgcdmndc 11944 Decidablity lemma used in various proofs related to gcd. (Contributed by Jim Kingdon, 12-Dec-2021.)
((𝑀 ∈ β„€ ∧ 𝑁 ∈ β„€) β†’ DECID (𝑀 = 0 ∧ 𝑁 = 0))
 
Theoremzsupcllemstep 11945* Lemma for zsupcl 11947. Induction step. (Contributed by Jim Kingdon, 7-Dec-2021.)
((πœ‘ ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘€)) β†’ DECID πœ“)    β‡’   (𝐾 ∈ (β„€β‰₯β€˜π‘€) β†’ (((πœ‘ ∧ βˆ€π‘› ∈ (β„€β‰₯β€˜πΎ) Β¬ πœ“) β†’ βˆƒπ‘₯ ∈ β„€ (βˆ€π‘¦ ∈ {𝑛 ∈ β„€ ∣ πœ“} Β¬ π‘₯ < 𝑦 ∧ βˆ€π‘¦ ∈ ℝ (𝑦 < π‘₯ β†’ βˆƒπ‘§ ∈ {𝑛 ∈ β„€ ∣ πœ“}𝑦 < 𝑧))) β†’ ((πœ‘ ∧ βˆ€π‘› ∈ (β„€β‰₯β€˜(𝐾 + 1)) Β¬ πœ“) β†’ βˆƒπ‘₯ ∈ β„€ (βˆ€π‘¦ ∈ {𝑛 ∈ β„€ ∣ πœ“} Β¬ π‘₯ < 𝑦 ∧ βˆ€π‘¦ ∈ ℝ (𝑦 < π‘₯ β†’ βˆƒπ‘§ ∈ {𝑛 ∈ β„€ ∣ πœ“}𝑦 < 𝑧)))))
 
Theoremzsupcllemex 11946* Lemma for zsupcl 11947. Existence of the supremum. (Contributed by Jim Kingdon, 7-Dec-2021.)
(πœ‘ β†’ 𝑀 ∈ β„€)    &   (𝑛 = 𝑀 β†’ (πœ“ ↔ πœ’))    &   (πœ‘ β†’ πœ’)    &   ((πœ‘ ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘€)) β†’ DECID πœ“)    &   (πœ‘ β†’ βˆƒπ‘— ∈ (β„€β‰₯β€˜π‘€)βˆ€π‘› ∈ (β„€β‰₯β€˜π‘—) Β¬ πœ“)    β‡’   (πœ‘ β†’ βˆƒπ‘₯ ∈ β„€ (βˆ€π‘¦ ∈ {𝑛 ∈ β„€ ∣ πœ“} Β¬ π‘₯ < 𝑦 ∧ βˆ€π‘¦ ∈ ℝ (𝑦 < π‘₯ β†’ βˆƒπ‘§ ∈ {𝑛 ∈ β„€ ∣ πœ“}𝑦 < 𝑧)))
 
Theoremzsupcl 11947* Closure of supremum for decidable integer properties. The property which defines the set we are taking the supremum of must (a) be true at 𝑀 (which corresponds to the nonempty condition of classical supremum theorems), (b) decidable at each value after 𝑀, and (c) be false after 𝑗 (which corresponds to the upper bound condition found in classical supremum theorems). (Contributed by Jim Kingdon, 7-Dec-2021.)
(πœ‘ β†’ 𝑀 ∈ β„€)    &   (𝑛 = 𝑀 β†’ (πœ“ ↔ πœ’))    &   (πœ‘ β†’ πœ’)    &   ((πœ‘ ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘€)) β†’ DECID πœ“)    &   (πœ‘ β†’ βˆƒπ‘— ∈ (β„€β‰₯β€˜π‘€)βˆ€π‘› ∈ (β„€β‰₯β€˜π‘—) Β¬ πœ“)    β‡’   (πœ‘ β†’ sup({𝑛 ∈ β„€ ∣ πœ“}, ℝ, < ) ∈ (β„€β‰₯β€˜π‘€))
 
Theoremzssinfcl 11948* The infimum of a set of integers is an element of the set. (Contributed by Jim Kingdon, 16-Jan-2022.)
(πœ‘ β†’ βˆƒπ‘₯ ∈ ℝ (βˆ€π‘¦ ∈ 𝐡 Β¬ 𝑦 < π‘₯ ∧ βˆ€π‘¦ ∈ ℝ (π‘₯ < 𝑦 β†’ βˆƒπ‘§ ∈ 𝐡 𝑧 < 𝑦)))    &   (πœ‘ β†’ 𝐡 βŠ† β„€)    &   (πœ‘ β†’ inf(𝐡, ℝ, < ) ∈ β„€)    β‡’   (πœ‘ β†’ inf(𝐡, ℝ, < ) ∈ 𝐡)
 
Theoreminfssuzex 11949* Existence of the infimum of a subset of an upper set of integers. (Contributed by Jim Kingdon, 13-Jan-2022.)
(πœ‘ β†’ 𝑀 ∈ β„€)    &   π‘† = {𝑛 ∈ (β„€β‰₯β€˜π‘€) ∣ πœ“}    &   (πœ‘ β†’ 𝐴 ∈ 𝑆)    &   ((πœ‘ ∧ 𝑛 ∈ (𝑀...𝐴)) β†’ DECID πœ“)    β‡’   (πœ‘ β†’ βˆƒπ‘₯ ∈ ℝ (βˆ€π‘¦ ∈ 𝑆 Β¬ 𝑦 < π‘₯ ∧ βˆ€π‘¦ ∈ ℝ (π‘₯ < 𝑦 β†’ βˆƒπ‘§ ∈ 𝑆 𝑧 < 𝑦)))
 
Theoreminfssuzledc 11950* The infimum of a subset of an upper set of integers is less than or equal to all members of the subset. (Contributed by Jim Kingdon, 13-Jan-2022.)
(πœ‘ β†’ 𝑀 ∈ β„€)    &   π‘† = {𝑛 ∈ (β„€β‰₯β€˜π‘€) ∣ πœ“}    &   (πœ‘ β†’ 𝐴 ∈ 𝑆)    &   ((πœ‘ ∧ 𝑛 ∈ (𝑀...𝐴)) β†’ DECID πœ“)    β‡’   (πœ‘ β†’ inf(𝑆, ℝ, < ) ≀ 𝐴)
 
Theoreminfssuzcldc 11951* The infimum of a subset of an upper set of integers belongs to the subset. (Contributed by Jim Kingdon, 20-Jan-2022.)
(πœ‘ β†’ 𝑀 ∈ β„€)    &   π‘† = {𝑛 ∈ (β„€β‰₯β€˜π‘€) ∣ πœ“}    &   (πœ‘ β†’ 𝐴 ∈ 𝑆)    &   ((πœ‘ ∧ 𝑛 ∈ (𝑀...𝐴)) β†’ DECID πœ“)    β‡’   (πœ‘ β†’ inf(𝑆, ℝ, < ) ∈ 𝑆)
 
Theoremsuprzubdc 11952* The supremum of a bounded-above decidable set of integers is greater than any member of the set. (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Jim Kingdon, 5-Oct-2024.)
(πœ‘ β†’ 𝐴 βŠ† β„€)    &   (πœ‘ β†’ βˆ€π‘₯ ∈ β„€ DECID π‘₯ ∈ 𝐴)    &   (πœ‘ β†’ βˆƒπ‘₯ ∈ β„€ βˆ€π‘¦ ∈ 𝐴 𝑦 ≀ π‘₯)    &   (πœ‘ β†’ 𝐡 ∈ 𝐴)    β‡’   (πœ‘ β†’ 𝐡 ≀ sup(𝐴, ℝ, < ))
 
Theoremnninfdcex 11953* A decidable set of natural numbers has an infimum. (Contributed by Jim Kingdon, 28-Sep-2024.)
(πœ‘ β†’ 𝐴 βŠ† β„•)    &   (πœ‘ β†’ βˆ€π‘₯ ∈ β„• DECID π‘₯ ∈ 𝐴)    &   (πœ‘ β†’ βˆƒπ‘¦ 𝑦 ∈ 𝐴)    β‡’   (πœ‘ β†’ βˆƒπ‘₯ ∈ ℝ (βˆ€π‘¦ ∈ 𝐴 Β¬ 𝑦 < π‘₯ ∧ βˆ€π‘¦ ∈ ℝ (π‘₯ < 𝑦 β†’ βˆƒπ‘§ ∈ 𝐴 𝑧 < 𝑦)))
 
Theoremzsupssdc 11954* An inhabited decidable bounded subset of integers has a supremum in the set. (The proof does not use ax-pre-suploc 7931.) (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Jim Kingdon, 5-Oct-2024.)
(πœ‘ β†’ 𝐴 βŠ† β„€)    &   (πœ‘ β†’ βˆƒπ‘₯ π‘₯ ∈ 𝐴)    &   (πœ‘ β†’ βˆ€π‘₯ ∈ β„€ DECID π‘₯ ∈ 𝐴)    &   (πœ‘ β†’ βˆƒπ‘₯ ∈ β„€ βˆ€π‘¦ ∈ 𝐴 𝑦 ≀ π‘₯)    β‡’   (πœ‘ β†’ βˆƒπ‘₯ ∈ 𝐴 (βˆ€π‘¦ ∈ 𝐴 Β¬ π‘₯ < 𝑦 ∧ βˆ€π‘¦ ∈ 𝐡 (𝑦 < π‘₯ β†’ βˆƒπ‘§ ∈ 𝐴 𝑦 < 𝑧)))
 
Theoremsuprzcl2dc 11955* The supremum of a bounded-above decidable set of integers is a member of the set. (This theorem avoids ax-pre-suploc 7931.) (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Jim Kingdon, 6-Oct-2024.)
(πœ‘ β†’ 𝐴 βŠ† β„€)    &   (πœ‘ β†’ βˆ€π‘₯ ∈ β„€ DECID π‘₯ ∈ 𝐴)    &   (πœ‘ β†’ βˆƒπ‘₯ ∈ β„€ βˆ€π‘¦ ∈ 𝐴 𝑦 ≀ π‘₯)    &   (πœ‘ β†’ βˆƒπ‘₯ π‘₯ ∈ 𝐴)    β‡’   (πœ‘ β†’ sup(𝐴, ℝ, < ) ∈ 𝐴)
 
Theoremdvdsbnd 11956* There is an upper bound to the divisors of a nonzero integer. (Contributed by Jim Kingdon, 11-Dec-2021.)
((𝐴 ∈ β„€ ∧ 𝐴 β‰  0) β†’ βˆƒπ‘› ∈ β„• βˆ€π‘š ∈ (β„€β‰₯β€˜π‘›) Β¬ π‘š βˆ₯ 𝐴)
 
Theoremgcdsupex 11957* Existence of the supremum used in defining gcd. (Contributed by Jim Kingdon, 12-Dec-2021.)
(((𝑋 ∈ β„€ ∧ π‘Œ ∈ β„€) ∧ Β¬ (𝑋 = 0 ∧ π‘Œ = 0)) β†’ βˆƒπ‘₯ ∈ β„€ (βˆ€π‘¦ ∈ {𝑛 ∈ β„€ ∣ (𝑛 βˆ₯ 𝑋 ∧ 𝑛 βˆ₯ π‘Œ)} Β¬ π‘₯ < 𝑦 ∧ βˆ€π‘¦ ∈ ℝ (𝑦 < π‘₯ β†’ βˆƒπ‘§ ∈ {𝑛 ∈ β„€ ∣ (𝑛 βˆ₯ 𝑋 ∧ 𝑛 βˆ₯ π‘Œ)}𝑦 < 𝑧)))
 
Theoremgcdsupcl 11958* Closure of the supremum used in defining gcd. A lemma for gcdval 11959 and gcdn0cl 11962. (Contributed by Jim Kingdon, 11-Dec-2021.)
(((𝑋 ∈ β„€ ∧ π‘Œ ∈ β„€) ∧ Β¬ (𝑋 = 0 ∧ π‘Œ = 0)) β†’ sup({𝑛 ∈ β„€ ∣ (𝑛 βˆ₯ 𝑋 ∧ 𝑛 βˆ₯ π‘Œ)}, ℝ, < ) ∈ β„•)
 
Theoremgcdval 11959* The value of the gcd operator. (𝑀 gcd 𝑁) is the greatest common divisor of 𝑀 and 𝑁. If 𝑀 and 𝑁 are both 0, the result is defined conventionally as 0. (Contributed by Paul Chapman, 21-Mar-2011.) (Revised by Mario Carneiro, 10-Nov-2013.)
((𝑀 ∈ β„€ ∧ 𝑁 ∈ β„€) β†’ (𝑀 gcd 𝑁) = if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ β„€ ∣ (𝑛 βˆ₯ 𝑀 ∧ 𝑛 βˆ₯ 𝑁)}, ℝ, < )))
 
Theoremgcd0val 11960 The value, by convention, of the gcd operator when both operands are 0. (Contributed by Paul Chapman, 21-Mar-2011.)
(0 gcd 0) = 0
 
Theoremgcdn0val 11961* The value of the gcd operator when at least one operand is nonzero. (Contributed by Paul Chapman, 21-Mar-2011.)
(((𝑀 ∈ β„€ ∧ 𝑁 ∈ β„€) ∧ Β¬ (𝑀 = 0 ∧ 𝑁 = 0)) β†’ (𝑀 gcd 𝑁) = sup({𝑛 ∈ β„€ ∣ (𝑛 βˆ₯ 𝑀 ∧ 𝑛 βˆ₯ 𝑁)}, ℝ, < ))
 
Theoremgcdn0cl 11962 Closure of the gcd operator. (Contributed by Paul Chapman, 21-Mar-2011.)
(((𝑀 ∈ β„€ ∧ 𝑁 ∈ β„€) ∧ Β¬ (𝑀 = 0 ∧ 𝑁 = 0)) β†’ (𝑀 gcd 𝑁) ∈ β„•)
 
Theoremgcddvds 11963 The gcd of two integers divides each of them. (Contributed by Paul Chapman, 21-Mar-2011.)
((𝑀 ∈ β„€ ∧ 𝑁 ∈ β„€) β†’ ((𝑀 gcd 𝑁) βˆ₯ 𝑀 ∧ (𝑀 gcd 𝑁) βˆ₯ 𝑁))
 
Theoremdvdslegcd 11964 An integer which divides both operands of the gcd operator is bounded by it. (Contributed by Paul Chapman, 21-Mar-2011.)
(((𝐾 ∈ β„€ ∧ 𝑀 ∈ β„€ ∧ 𝑁 ∈ β„€) ∧ Β¬ (𝑀 = 0 ∧ 𝑁 = 0)) β†’ ((𝐾 βˆ₯ 𝑀 ∧ 𝐾 βˆ₯ 𝑁) β†’ 𝐾 ≀ (𝑀 gcd 𝑁)))
 
Theoremnndvdslegcd 11965 A positive integer which divides both positive operands of the gcd operator is bounded by it. (Contributed by AV, 9-Aug-2020.)
((𝐾 ∈ β„• ∧ 𝑀 ∈ β„• ∧ 𝑁 ∈ β„•) β†’ ((𝐾 βˆ₯ 𝑀 ∧ 𝐾 βˆ₯ 𝑁) β†’ 𝐾 ≀ (𝑀 gcd 𝑁)))
 
Theoremgcdcl 11966 Closure of the gcd operator. (Contributed by Paul Chapman, 21-Mar-2011.)
((𝑀 ∈ β„€ ∧ 𝑁 ∈ β„€) β†’ (𝑀 gcd 𝑁) ∈ β„•0)
 
Theoremgcdnncl 11967 Closure of the gcd operator. (Contributed by Thierry Arnoux, 2-Feb-2020.)
((𝑀 ∈ β„• ∧ 𝑁 ∈ β„•) β†’ (𝑀 gcd 𝑁) ∈ β„•)
 
Theoremgcdcld 11968 Closure of the gcd operator. (Contributed by Mario Carneiro, 29-May-2016.)
(πœ‘ β†’ 𝑀 ∈ β„€)    &   (πœ‘ β†’ 𝑁 ∈ β„€)    β‡’   (πœ‘ β†’ (𝑀 gcd 𝑁) ∈ β„•0)
 
Theoremgcd2n0cl 11969 Closure of the gcd operator if the second operand is not 0. (Contributed by AV, 10-Jul-2021.)
((𝑀 ∈ β„€ ∧ 𝑁 ∈ β„€ ∧ 𝑁 β‰  0) β†’ (𝑀 gcd 𝑁) ∈ β„•)
 
Theoremzeqzmulgcd 11970* An integer is the product of an integer and the gcd of it and another integer. (Contributed by AV, 11-Jul-2021.)
((𝐴 ∈ β„€ ∧ 𝐡 ∈ β„€) β†’ βˆƒπ‘› ∈ β„€ 𝐴 = (𝑛 Β· (𝐴 gcd 𝐡)))
 
Theoremdivgcdz 11971 An integer divided by the gcd of it and a nonzero integer is an integer. (Contributed by AV, 11-Jul-2021.)
((𝐴 ∈ β„€ ∧ 𝐡 ∈ β„€ ∧ 𝐡 β‰  0) β†’ (𝐴 / (𝐴 gcd 𝐡)) ∈ β„€)
 
Theoremgcdf 11972 Domain and codomain of the gcd operator. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 16-Nov-2013.)
gcd :(β„€ Γ— β„€)βŸΆβ„•0
 
Theoremgcdcom 11973 The gcd operator is commutative. Theorem 1.4(a) in [ApostolNT] p. 16. (Contributed by Paul Chapman, 21-Mar-2011.)
((𝑀 ∈ β„€ ∧ 𝑁 ∈ β„€) β†’ (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀))
 
Theoremgcdcomd 11974 The gcd operator is commutative, deduction version. (Contributed by SN, 24-Aug-2024.)
(πœ‘ β†’ 𝑀 ∈ β„€)    &   (πœ‘ β†’ 𝑁 ∈ β„€)    β‡’   (πœ‘ β†’ (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀))
 
Theoremdivgcdnn 11975 A positive integer divided by the gcd of it and another integer is a positive integer. (Contributed by AV, 10-Jul-2021.)
((𝐴 ∈ β„• ∧ 𝐡 ∈ β„€) β†’ (𝐴 / (𝐴 gcd 𝐡)) ∈ β„•)
 
Theoremdivgcdnnr 11976 A positive integer divided by the gcd of it and another integer is a positive integer. (Contributed by AV, 10-Jul-2021.)
((𝐴 ∈ β„• ∧ 𝐡 ∈ β„€) β†’ (𝐴 / (𝐡 gcd 𝐴)) ∈ β„•)
 
Theoremgcdeq0 11977 The gcd of two integers is zero iff they are both zero. (Contributed by Paul Chapman, 21-Mar-2011.)
((𝑀 ∈ β„€ ∧ 𝑁 ∈ β„€) β†’ ((𝑀 gcd 𝑁) = 0 ↔ (𝑀 = 0 ∧ 𝑁 = 0)))
 
Theoremgcdn0gt0 11978 The gcd of two integers is positive (nonzero) iff they are not both zero. (Contributed by Paul Chapman, 22-Jun-2011.)
((𝑀 ∈ β„€ ∧ 𝑁 ∈ β„€) β†’ (Β¬ (𝑀 = 0 ∧ 𝑁 = 0) ↔ 0 < (𝑀 gcd 𝑁)))
 
Theoremgcd0id 11979 The gcd of 0 and an integer is the integer's absolute value. (Contributed by Paul Chapman, 21-Mar-2011.)
(𝑁 ∈ β„€ β†’ (0 gcd 𝑁) = (absβ€˜π‘))
 
Theoremgcdid0 11980 The gcd of an integer and 0 is the integer's absolute value. Theorem 1.4(d)2 in [ApostolNT] p. 16. (Contributed by Paul Chapman, 31-Mar-2011.)
(𝑁 ∈ β„€ β†’ (𝑁 gcd 0) = (absβ€˜π‘))
 
Theoremnn0gcdid0 11981 The gcd of a nonnegative integer with 0 is itself. (Contributed by Paul Chapman, 31-Mar-2011.)
(𝑁 ∈ β„•0 β†’ (𝑁 gcd 0) = 𝑁)
 
Theoremgcdneg 11982 Negating one operand of the gcd operator does not alter the result. (Contributed by Paul Chapman, 21-Mar-2011.)
((𝑀 ∈ β„€ ∧ 𝑁 ∈ β„€) β†’ (𝑀 gcd -𝑁) = (𝑀 gcd 𝑁))
 
Theoremneggcd 11983 Negating one operand of the gcd operator does not alter the result. (Contributed by Paul Chapman, 22-Jun-2011.)
((𝑀 ∈ β„€ ∧ 𝑁 ∈ β„€) β†’ (-𝑀 gcd 𝑁) = (𝑀 gcd 𝑁))
 
Theoremgcdaddm 11984 Adding a multiple of one operand of the gcd operator to the other does not alter the result. (Contributed by Paul Chapman, 31-Mar-2011.)
((𝐾 ∈ β„€ ∧ 𝑀 ∈ β„€ ∧ 𝑁 ∈ β„€) β†’ (𝑀 gcd 𝑁) = (𝑀 gcd (𝑁 + (𝐾 Β· 𝑀))))
 
Theoremgcdadd 11985 The GCD of two numbers is the same as the GCD of the left and their sum. (Contributed by Scott Fenton, 20-Apr-2014.)
((𝑀 ∈ β„€ ∧ 𝑁 ∈ β„€) β†’ (𝑀 gcd 𝑁) = (𝑀 gcd (𝑁 + 𝑀)))
 
Theoremgcdid 11986 The gcd of a number and itself is its absolute value. (Contributed by Paul Chapman, 31-Mar-2011.)
(𝑁 ∈ β„€ β†’ (𝑁 gcd 𝑁) = (absβ€˜π‘))
 
Theoremgcd1 11987 The gcd of a number with 1 is 1. Theorem 1.4(d)1 in [ApostolNT] p. 16. (Contributed by Mario Carneiro, 19-Feb-2014.)
(𝑀 ∈ β„€ β†’ (𝑀 gcd 1) = 1)
 
Theoremgcdabs 11988 The gcd of two integers is the same as that of their absolute values. (Contributed by Paul Chapman, 31-Mar-2011.)
((𝑀 ∈ β„€ ∧ 𝑁 ∈ β„€) β†’ ((absβ€˜π‘€) gcd (absβ€˜π‘)) = (𝑀 gcd 𝑁))
 
Theoremgcdabs1 11989 gcd of the absolute value of the first operator. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
((𝑁 ∈ β„€ ∧ 𝑀 ∈ β„€) β†’ ((absβ€˜π‘) gcd 𝑀) = (𝑁 gcd 𝑀))
 
Theoremgcdabs2 11990 gcd of the absolute value of the second operator. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
((𝑁 ∈ β„€ ∧ 𝑀 ∈ β„€) β†’ (𝑁 gcd (absβ€˜π‘€)) = (𝑁 gcd 𝑀))
 
Theoremmodgcd 11991 The gcd remains unchanged if one operand is replaced with its remainder modulo the other. (Contributed by Paul Chapman, 31-Mar-2011.)
((𝑀 ∈ β„€ ∧ 𝑁 ∈ β„•) β†’ ((𝑀 mod 𝑁) gcd 𝑁) = (𝑀 gcd 𝑁))
 
Theorem1gcd 11992 The GCD of one and an integer is one. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
(𝑀 ∈ β„€ β†’ (1 gcd 𝑀) = 1)
 
Theoremgcdmultipled 11993 The greatest common divisor of a nonnegative integer 𝑀 and a multiple of it is 𝑀 itself. (Contributed by Rohan Ridenour, 3-Aug-2023.)
(πœ‘ β†’ 𝑀 ∈ β„•0)    &   (πœ‘ β†’ 𝑁 ∈ β„€)    β‡’   (πœ‘ β†’ (𝑀 gcd (𝑁 Β· 𝑀)) = 𝑀)
 
Theoremdvdsgcdidd 11994 The greatest common divisor of a positive integer and another integer it divides is itself. (Contributed by Rohan Ridenour, 3-Aug-2023.)
(πœ‘ β†’ 𝑀 ∈ β„•)    &   (πœ‘ β†’ 𝑁 ∈ β„€)    &   (πœ‘ β†’ 𝑀 βˆ₯ 𝑁)    β‡’   (πœ‘ β†’ (𝑀 gcd 𝑁) = 𝑀)
 
Theorem6gcd4e2 11995 The greatest common divisor of six and four is two. To calculate this gcd, a simple form of Euclid's algorithm is used: (6 gcd 4) = ((4 + 2) gcd 4) = (2 gcd 4) and (2 gcd 4) = (2 gcd (2 + 2)) = (2 gcd 2) = 2. (Contributed by AV, 27-Aug-2020.)
(6 gcd 4) = 2
 
5.1.5  BΓ©zout's identity
 
Theorembezoutlemnewy 11996* Lemma for BΓ©zout's identity. The is-bezout predicate holds for (𝑦 mod π‘Š). (Contributed by Jim Kingdon, 6-Jan-2022.)
(πœ‘ ↔ βˆƒπ‘  ∈ β„€ βˆƒπ‘‘ ∈ β„€ π‘Ÿ = ((𝐴 Β· 𝑠) + (𝐡 Β· 𝑑)))    &   (πœƒ β†’ 𝐴 ∈ β„•0)    &   (πœƒ β†’ 𝐡 ∈ β„•0)    &   (πœƒ β†’ π‘Š ∈ β„•)    &   (πœƒ β†’ [𝑦 / π‘Ÿ]πœ‘)    &   (πœƒ β†’ 𝑦 ∈ β„•0)    &   (πœƒ β†’ [π‘Š / π‘Ÿ]πœ‘)    β‡’   (πœƒ β†’ [(𝑦 mod π‘Š) / π‘Ÿ]πœ‘)
 
Theorembezoutlemstep 11997* Lemma for BΓ©zout's identity. This is the induction step for the proof by induction. (Contributed by Jim Kingdon, 3-Jan-2022.)
(πœ‘ ↔ βˆƒπ‘  ∈ β„€ βˆƒπ‘‘ ∈ β„€ π‘Ÿ = ((𝐴 Β· 𝑠) + (𝐡 Β· 𝑑)))    &   (πœƒ β†’ 𝐴 ∈ β„•0)    &   (πœƒ β†’ 𝐡 ∈ β„•0)    &   (πœƒ β†’ π‘Š ∈ β„•)    &   (πœƒ β†’ [𝑦 / π‘Ÿ]πœ‘)    &   (πœƒ β†’ 𝑦 ∈ β„•0)    &   (πœƒ β†’ [π‘Š / π‘Ÿ]πœ‘)    &   (πœ“ ↔ βˆ€π‘§ ∈ β„•0 (𝑧 βˆ₯ π‘Ÿ β†’ (𝑧 βˆ₯ π‘₯ ∧ 𝑧 βˆ₯ 𝑦)))    &   ((πœƒ ∧ [(𝑦 mod π‘Š) / π‘Ÿ]πœ‘) β†’ βˆƒπ‘Ÿ ∈ β„•0 ([(𝑦 mod π‘Š) / π‘₯][π‘Š / 𝑦]πœ“ ∧ πœ‘))    &   β„²π‘₯πœƒ    &   β„²π‘Ÿπœƒ    β‡’   (πœƒ β†’ βˆƒπ‘Ÿ ∈ β„•0 ([π‘Š / π‘₯]πœ“ ∧ πœ‘))
 
Theorembezoutlemmain 11998* Lemma for BΓ©zout's identity. This is the main result which we prove by induction and which represents the application of the Extended Euclidean algorithm. (Contributed by Jim Kingdon, 30-Dec-2021.)
(πœ‘ ↔ βˆƒπ‘  ∈ β„€ βˆƒπ‘‘ ∈ β„€ π‘Ÿ = ((𝐴 Β· 𝑠) + (𝐡 Β· 𝑑)))    &   (πœ“ ↔ βˆ€π‘§ ∈ β„•0 (𝑧 βˆ₯ π‘Ÿ β†’ (𝑧 βˆ₯ π‘₯ ∧ 𝑧 βˆ₯ 𝑦)))    &   (πœƒ β†’ 𝐴 ∈ β„•0)    &   (πœƒ β†’ 𝐡 ∈ β„•0)    β‡’   (πœƒ β†’ βˆ€π‘₯ ∈ β„•0 ([π‘₯ / π‘Ÿ]πœ‘ β†’ βˆ€π‘¦ ∈ β„•0 ([𝑦 / π‘Ÿ]πœ‘ β†’ βˆƒπ‘Ÿ ∈ β„•0 (πœ“ ∧ πœ‘))))
 
Theorembezoutlema 11999* Lemma for BΓ©zout's identity. The is-bezout condition is satisfied by 𝐴. (Contributed by Jim Kingdon, 30-Dec-2021.)
(πœ‘ ↔ βˆƒπ‘  ∈ β„€ βˆƒπ‘‘ ∈ β„€ π‘Ÿ = ((𝐴 Β· 𝑠) + (𝐡 Β· 𝑑)))    &   (πœƒ β†’ 𝐴 ∈ β„•0)    &   (πœƒ β†’ 𝐡 ∈ β„•0)    β‡’   (πœƒ β†’ [𝐴 / π‘Ÿ]πœ‘)
 
Theorembezoutlemb 12000* Lemma for BΓ©zout's identity. The is-bezout condition is satisfied by 𝐡. (Contributed by Jim Kingdon, 30-Dec-2021.)
(πœ‘ ↔ βˆƒπ‘  ∈ β„€ βˆƒπ‘‘ ∈ β„€ π‘Ÿ = ((𝐴 Β· 𝑠) + (𝐡 Β· 𝑑)))    &   (πœƒ β†’ 𝐴 ∈ β„•0)    &   (πœƒ β†’ 𝐡 ∈ β„•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-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-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14801
  Copyright terms: Public domain < Previous  Next >