HomeHome Intuitionistic Logic Explorer
Theorem List (p. 125 of 153)
< 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 - 12401-12500   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theorem4sqlem8 12401 Lemma for 4sq (not yet proved here) . (Contributed by Mario Carneiro, 15-Jul-2014.)
(𝜑𝐴 ∈ ℤ)    &   (𝜑𝑀 ∈ ℕ)    &   𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))       (𝜑𝑀 ∥ ((𝐴↑2) − (𝐵↑2)))
 
Theorem4sqlem9 12402 Lemma for 4sq (not yet proved here) . (Contributed by Mario Carneiro, 15-Jul-2014.)
(𝜑𝐴 ∈ ℤ)    &   (𝜑𝑀 ∈ ℕ)    &   𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ((𝜑𝜓) → (𝐵↑2) = 0)       ((𝜑𝜓) → (𝑀↑2) ∥ (𝐴↑2))
 
Theorem4sqlem10 12403 Lemma for 4sq (not yet proved here) . (Contributed by Mario Carneiro, 16-Jul-2014.)
(𝜑𝐴 ∈ ℤ)    &   (𝜑𝑀 ∈ ℕ)    &   𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ((𝜑𝜓) → ((((𝑀↑2) / 2) / 2) − (𝐵↑2)) = 0)       ((𝜑𝜓) → (𝑀↑2) ∥ ((𝐴↑2) − (((𝑀↑2) / 2) / 2)))
 
Theorem4sqlem1 12404* Lemma for 4sq (not yet proved here) . The set 𝑆 is the set of all numbers that are expressible as a sum of four squares. Our goal is to show that 𝑆 = ℕ0; here we show one subset direction. (Contributed by Mario Carneiro, 14-Jul-2014.)
𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}       𝑆 ⊆ ℕ0
 
Theorem4sqlem2 12405* Lemma for 4sq (not yet proved here) . Change bound variables in 𝑆. (Contributed by Mario Carneiro, 14-Jul-2014.)
𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}       (𝐴𝑆 ↔ ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ ∃𝑐 ∈ ℤ ∃𝑑 ∈ ℤ 𝐴 = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2))))
 
Theorem4sqlem3 12406* Lemma for 4sq (not yet proved here) . Sufficient condition to be in 𝑆. (Contributed by Mario Carneiro, 14-Jul-2014.)
𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}       (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ)) → (((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))) ∈ 𝑆)
 
Theorem4sqlem4a 12407* Lemma for 4sqlem4 12408. (Contributed by Mario Carneiro, 14-Jul-2014.)
𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}       ((𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i]) → (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) ∈ 𝑆)
 
Theorem4sqlem4 12408* Lemma for 4sq (not yet proved here) . We can express the four-square property more compactly in terms of gaussian integers, because the norms of gaussian integers are exactly sums of two squares. (Contributed by Mario Carneiro, 14-Jul-2014.)
𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}       (𝐴𝑆 ↔ ∃𝑢 ∈ ℤ[i] ∃𝑣 ∈ ℤ[i] 𝐴 = (((abs‘𝑢)↑2) + ((abs‘𝑣)↑2)))
 
Theoremmul4sqlem 12409* Lemma for mul4sq 12410: algebraic manipulations. The extra assumptions involving 𝑀 would let us know not just that the product is a sum of squares, but also that it preserves divisibility by 𝑀. (Contributed by Mario Carneiro, 14-Jul-2014.)
𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    &   (𝜑𝐴 ∈ ℤ[i])    &   (𝜑𝐵 ∈ ℤ[i])    &   (𝜑𝐶 ∈ ℤ[i])    &   (𝜑𝐷 ∈ ℤ[i])    &   𝑋 = (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2))    &   𝑌 = (((abs‘𝐶)↑2) + ((abs‘𝐷)↑2))    &   (𝜑𝑀 ∈ ℕ)    &   (𝜑 → ((𝐴𝐶) / 𝑀) ∈ ℤ[i])    &   (𝜑 → ((𝐵𝐷) / 𝑀) ∈ ℤ[i])    &   (𝜑 → (𝑋 / 𝑀) ∈ ℕ0)       (𝜑 → ((𝑋 / 𝑀) · (𝑌 / 𝑀)) ∈ 𝑆)
 
Theoremmul4sq 12410* Euler's four-square identity: The product of two sums of four squares is also a sum of four squares. This is usually quoted as an explicit formula involving eight real variables; we save some time by working with complex numbers (gaussian integers) instead, so that we only have to work with four variables, and also hiding the actual formula for the product in the proof of mul4sqlem 12409. (For the curious, the explicit formula that is used is ( ∣ 𝑎 ∣ ↑2 + ∣ 𝑏 ∣ ↑2)( ∣ 𝑐 ∣ ↑2 + ∣ 𝑑 ∣ ↑2) = 𝑎∗ · 𝑐 + 𝑏 · 𝑑∗ ∣ ↑2 + ∣ 𝑎∗ · 𝑑𝑏 · 𝑐∗ ∣ ↑2.) (Contributed by Mario Carneiro, 14-Jul-2014.)
𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}       ((𝐴𝑆𝐵𝑆) → (𝐴 · 𝐵) ∈ 𝑆)
 
5.3  Cardinality of real and complex number subsets
 
5.3.1  Countability of integers and rationals
 
Theoremoddennn 12411 There are as many odd positive integers as there are positive integers. (Contributed by Jim Kingdon, 11-May-2022.)
{𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ≈ ℕ
 
Theoremevenennn 12412 There are as many even positive integers as there are positive integers. (Contributed by Jim Kingdon, 12-May-2022.)
{𝑧 ∈ ℕ ∣ 2 ∥ 𝑧} ≈ ℕ
 
Theoremxpnnen 12413 The Cartesian product of the set of positive integers with itself is equinumerous to the set of positive integers. (Contributed by NM, 1-Aug-2004.)
(ℕ × ℕ) ≈ ℕ
 
Theoremxpomen 12414 The Cartesian product of omega (the set of ordinal natural numbers) with itself is equinumerous to omega. Exercise 1 of [Enderton] p. 133. (Contributed by NM, 23-Jul-2004.)
(ω × ω) ≈ ω
 
Theoremxpct 12415 The cartesian product of two sets dominated by ω is dominated by ω. (Contributed by Thierry Arnoux, 24-Sep-2017.)
((𝐴 ≼ ω ∧ 𝐵 ≼ ω) → (𝐴 × 𝐵) ≼ ω)
 
Theoremunennn 12416 The union of two disjoint countably infinite sets is countably infinite. (Contributed by Jim Kingdon, 13-May-2022.)
((𝐴 ≈ ℕ ∧ 𝐵 ≈ ℕ ∧ (𝐴𝐵) = ∅) → (𝐴𝐵) ≈ ℕ)
 
Theoremznnen 12417 The set of integers and the set of positive integers are equinumerous. Corollary 8.1.23 of [AczelRathjen], p. 75. (Contributed by NM, 31-Jul-2004.)
ℤ ≈ ℕ
 
Theoremennnfonelemdc 12418* Lemma for ennnfone 12444. A direct consequence of fidcenumlemrk 6971. (Contributed by Jim Kingdon, 15-Jul-2023.)
(𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)    &   (𝜑𝐹:ω–onto𝐴)    &   (𝜑𝑃 ∈ ω)       (𝜑DECID (𝐹𝑃) ∈ (𝐹𝑃))
 
Theoremennnfonelemk 12419* Lemma for ennnfone 12444. (Contributed by Jim Kingdon, 15-Jul-2023.)
(𝜑𝐹:ω–onto𝐴)    &   (𝜑𝐾 ∈ ω)    &   (𝜑𝑁 ∈ ω)    &   (𝜑 → ∀𝑗 ∈ suc 𝑁(𝐹𝐾) ≠ (𝐹𝑗))       (𝜑𝑁𝐾)
 
Theoremennnfonelemj0 12420* Lemma for ennnfone 12444. Initial state for 𝐽. (Contributed by Jim Kingdon, 20-Jul-2023.)
(𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)    &   (𝜑𝐹:ω–onto𝐴)    &   (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗))    &   𝐺 = (𝑥 ∈ (𝐴pm ω), 𝑦 ∈ ω ↦ if((𝐹𝑦) ∈ (𝐹𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹𝑦)⟩})))    &   𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (𝑁‘(𝑥 − 1))))    &   𝐻 = seq0(𝐺, 𝐽)       (𝜑 → (𝐽‘0) ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω})
 
Theoremennnfonelemjn 12421* Lemma for ennnfone 12444. Non-initial state for 𝐽. (Contributed by Jim Kingdon, 20-Jul-2023.)
(𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)    &   (𝜑𝐹:ω–onto𝐴)    &   (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗))    &   𝐺 = (𝑥 ∈ (𝐴pm ω), 𝑦 ∈ ω ↦ if((𝐹𝑦) ∈ (𝐹𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹𝑦)⟩})))    &   𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (𝑁‘(𝑥 − 1))))    &   𝐻 = seq0(𝐺, 𝐽)       ((𝜑𝑓 ∈ (ℤ‘(0 + 1))) → (𝐽𝑓) ∈ ω)
 
Theoremennnfonelemg 12422* Lemma for ennnfone 12444. Closure for 𝐺. (Contributed by Jim Kingdon, 20-Jul-2023.)
(𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)    &   (𝜑𝐹:ω–onto𝐴)    &   (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗))    &   𝐺 = (𝑥 ∈ (𝐴pm ω), 𝑦 ∈ ω ↦ if((𝐹𝑦) ∈ (𝐹𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹𝑦)⟩})))    &   𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (𝑁‘(𝑥 − 1))))    &   𝐻 = seq0(𝐺, 𝐽)       ((𝜑 ∧ (𝑓 ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω} ∧ 𝑗 ∈ ω)) → (𝑓𝐺𝑗) ∈ {𝑔 ∈ (𝐴pm ω) ∣ dom 𝑔 ∈ ω})
 
Theoremennnfonelemh 12423* Lemma for ennnfone 12444. (Contributed by Jim Kingdon, 8-Jul-2023.)
(𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)    &   (𝜑𝐹:ω–onto𝐴)    &   (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗))    &   𝐺 = (𝑥 ∈ (𝐴pm ω), 𝑦 ∈ ω ↦ if((𝐹𝑦) ∈ (𝐹𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹𝑦)⟩})))    &   𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (𝑁‘(𝑥 − 1))))    &   𝐻 = seq0(𝐺, 𝐽)       (𝜑𝐻:ℕ0⟶(𝐴pm ω))
 
Theoremennnfonelem0 12424* Lemma for ennnfone 12444. Initial value. (Contributed by Jim Kingdon, 15-Jul-2023.)
(𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)    &   (𝜑𝐹:ω–onto𝐴)    &   (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗))    &   𝐺 = (𝑥 ∈ (𝐴pm ω), 𝑦 ∈ ω ↦ if((𝐹𝑦) ∈ (𝐹𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹𝑦)⟩})))    &   𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (𝑁‘(𝑥 − 1))))    &   𝐻 = seq0(𝐺, 𝐽)       (𝜑 → (𝐻‘0) = ∅)
 
Theoremennnfonelemp1 12425* Lemma for ennnfone 12444. Value of 𝐻 at a successor. (Contributed by Jim Kingdon, 23-Jul-2023.)
(𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)    &   (𝜑𝐹:ω–onto𝐴)    &   (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗))    &   𝐺 = (𝑥 ∈ (𝐴pm ω), 𝑦 ∈ ω ↦ if((𝐹𝑦) ∈ (𝐹𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹𝑦)⟩})))    &   𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (𝑁‘(𝑥 − 1))))    &   𝐻 = seq0(𝐺, 𝐽)    &   (𝜑𝑃 ∈ ℕ0)       (𝜑 → (𝐻‘(𝑃 + 1)) = if((𝐹‘(𝑁𝑃)) ∈ (𝐹 “ (𝑁𝑃)), (𝐻𝑃), ((𝐻𝑃) ∪ {⟨dom (𝐻𝑃), (𝐹‘(𝑁𝑃))⟩})))
 
Theoremennnfonelem1 12426* Lemma for ennnfone 12444. Second value. (Contributed by Jim Kingdon, 19-Jul-2023.)
(𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)    &   (𝜑𝐹:ω–onto𝐴)    &   (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗))    &   𝐺 = (𝑥 ∈ (𝐴pm ω), 𝑦 ∈ ω ↦ if((𝐹𝑦) ∈ (𝐹𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹𝑦)⟩})))    &   𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (𝑁‘(𝑥 − 1))))    &   𝐻 = seq0(𝐺, 𝐽)       (𝜑 → (𝐻‘1) = {⟨∅, (𝐹‘∅)⟩})
 
Theoremennnfonelemom 12427* Lemma for ennnfone 12444. 𝐻 yields finite sequences. (Contributed by Jim Kingdon, 19-Jul-2023.)
(𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)    &   (𝜑𝐹:ω–onto𝐴)    &   (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗))    &   𝐺 = (𝑥 ∈ (𝐴pm ω), 𝑦 ∈ ω ↦ if((𝐹𝑦) ∈ (𝐹𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹𝑦)⟩})))    &   𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (𝑁‘(𝑥 − 1))))    &   𝐻 = seq0(𝐺, 𝐽)    &   (𝜑𝑃 ∈ ℕ0)       (𝜑 → dom (𝐻𝑃) ∈ ω)
 
Theoremennnfonelemhdmp1 12428* Lemma for ennnfone 12444. Domain at a successor where we need to add an element to the sequence. (Contributed by Jim Kingdon, 23-Jul-2023.)
(𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)    &   (𝜑𝐹:ω–onto𝐴)    &   (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗))    &   𝐺 = (𝑥 ∈ (𝐴pm ω), 𝑦 ∈ ω ↦ if((𝐹𝑦) ∈ (𝐹𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹𝑦)⟩})))    &   𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (𝑁‘(𝑥 − 1))))    &   𝐻 = seq0(𝐺, 𝐽)    &   (𝜑𝑃 ∈ ℕ0)    &   (𝜑 → ¬ (𝐹‘(𝑁𝑃)) ∈ (𝐹 “ (𝑁𝑃)))       (𝜑 → dom (𝐻‘(𝑃 + 1)) = suc dom (𝐻𝑃))
 
Theoremennnfonelemss 12429* Lemma for ennnfone 12444. We only add elements to 𝐻 as the index increases. (Contributed by Jim Kingdon, 15-Jul-2023.)
(𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)    &   (𝜑𝐹:ω–onto𝐴)    &   (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗))    &   𝐺 = (𝑥 ∈ (𝐴pm ω), 𝑦 ∈ ω ↦ if((𝐹𝑦) ∈ (𝐹𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹𝑦)⟩})))    &   𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (𝑁‘(𝑥 − 1))))    &   𝐻 = seq0(𝐺, 𝐽)    &   (𝜑𝑃 ∈ ℕ0)       (𝜑 → (𝐻𝑃) ⊆ (𝐻‘(𝑃 + 1)))
 
Theoremennnfoneleminc 12430* Lemma for ennnfone 12444. We only add elements to 𝐻 as the index increases. (Contributed by Jim Kingdon, 21-Jul-2023.)
(𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)    &   (𝜑𝐹:ω–onto𝐴)    &   (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗))    &   𝐺 = (𝑥 ∈ (𝐴pm ω), 𝑦 ∈ ω ↦ if((𝐹𝑦) ∈ (𝐹𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹𝑦)⟩})))    &   𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (𝑁‘(𝑥 − 1))))    &   𝐻 = seq0(𝐺, 𝐽)    &   (𝜑𝑃 ∈ ℕ0)    &   (𝜑𝑄 ∈ ℕ0)    &   (𝜑𝑃𝑄)       (𝜑 → (𝐻𝑃) ⊆ (𝐻𝑄))
 
Theoremennnfonelemkh 12431* Lemma for ennnfone 12444. Because we add zero or one entries for each new index, the length of each sequence is no greater than its index. (Contributed by Jim Kingdon, 19-Jul-2023.)
(𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)    &   (𝜑𝐹:ω–onto𝐴)    &   (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗))    &   𝐺 = (𝑥 ∈ (𝐴pm ω), 𝑦 ∈ ω ↦ if((𝐹𝑦) ∈ (𝐹𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹𝑦)⟩})))    &   𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (𝑁‘(𝑥 − 1))))    &   𝐻 = seq0(𝐺, 𝐽)    &   (𝜑𝑃 ∈ ℕ0)       (𝜑 → dom (𝐻𝑃) ⊆ (𝑁𝑃))
 
Theoremennnfonelemhf1o 12432* Lemma for ennnfone 12444. Each of the functions in 𝐻 is one to one and onto an image of 𝐹. (Contributed by Jim Kingdon, 17-Jul-2023.)
(𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)    &   (𝜑𝐹:ω–onto𝐴)    &   (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗))    &   𝐺 = (𝑥 ∈ (𝐴pm ω), 𝑦 ∈ ω ↦ if((𝐹𝑦) ∈ (𝐹𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹𝑦)⟩})))    &   𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (𝑁‘(𝑥 − 1))))    &   𝐻 = seq0(𝐺, 𝐽)    &   (𝜑𝑃 ∈ ℕ0)       (𝜑 → (𝐻𝑃):dom (𝐻𝑃)–1-1-onto→(𝐹 “ (𝑁𝑃)))
 
Theoremennnfonelemex 12433* Lemma for ennnfone 12444. Extending the sequence (𝐻𝑃) to include an additional element. (Contributed by Jim Kingdon, 19-Jul-2023.)
(𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)    &   (𝜑𝐹:ω–onto𝐴)    &   (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗))    &   𝐺 = (𝑥 ∈ (𝐴pm ω), 𝑦 ∈ ω ↦ if((𝐹𝑦) ∈ (𝐹𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹𝑦)⟩})))    &   𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (𝑁‘(𝑥 − 1))))    &   𝐻 = seq0(𝐺, 𝐽)    &   (𝜑𝑃 ∈ ℕ0)       (𝜑 → ∃𝑖 ∈ ℕ0 dom (𝐻𝑃) ∈ dom (𝐻𝑖))
 
Theoremennnfonelemhom 12434* Lemma for ennnfone 12444. The sequences in 𝐻 increase in length without bound if you go out far enough. (Contributed by Jim Kingdon, 19-Jul-2023.)
(𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)    &   (𝜑𝐹:ω–onto𝐴)    &   (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗))    &   𝐺 = (𝑥 ∈ (𝐴pm ω), 𝑦 ∈ ω ↦ if((𝐹𝑦) ∈ (𝐹𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹𝑦)⟩})))    &   𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (𝑁‘(𝑥 − 1))))    &   𝐻 = seq0(𝐺, 𝐽)    &   (𝜑𝑀 ∈ ω)       (𝜑 → ∃𝑖 ∈ ℕ0 𝑀 ∈ dom (𝐻𝑖))
 
Theoremennnfonelemrnh 12435* Lemma for ennnfone 12444. A consequence of ennnfonelemss 12429. (Contributed by Jim Kingdon, 16-Jul-2023.)
(𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)    &   (𝜑𝐹:ω–onto𝐴)    &   (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗))    &   𝐺 = (𝑥 ∈ (𝐴pm ω), 𝑦 ∈ ω ↦ if((𝐹𝑦) ∈ (𝐹𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹𝑦)⟩})))    &   𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (𝑁‘(𝑥 − 1))))    &   𝐻 = seq0(𝐺, 𝐽)    &   (𝜑𝑋 ∈ ran 𝐻)    &   (𝜑𝑌 ∈ ran 𝐻)       (𝜑 → (𝑋𝑌𝑌𝑋))
 
Theoremennnfonelemfun 12436* Lemma for ennnfone 12444. 𝐿 is a function. (Contributed by Jim Kingdon, 16-Jul-2023.)
(𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)    &   (𝜑𝐹:ω–onto𝐴)    &   (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗))    &   𝐺 = (𝑥 ∈ (𝐴pm ω), 𝑦 ∈ ω ↦ if((𝐹𝑦) ∈ (𝐹𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹𝑦)⟩})))    &   𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (𝑁‘(𝑥 − 1))))    &   𝐻 = seq0(𝐺, 𝐽)    &   𝐿 = 𝑖 ∈ ℕ0 (𝐻𝑖)       (𝜑 → Fun 𝐿)
 
Theoremennnfonelemf1 12437* Lemma for ennnfone 12444. 𝐿 is one-to-one. (Contributed by Jim Kingdon, 16-Jul-2023.)
(𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)    &   (𝜑𝐹:ω–onto𝐴)    &   (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗))    &   𝐺 = (𝑥 ∈ (𝐴pm ω), 𝑦 ∈ ω ↦ if((𝐹𝑦) ∈ (𝐹𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹𝑦)⟩})))    &   𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (𝑁‘(𝑥 − 1))))    &   𝐻 = seq0(𝐺, 𝐽)    &   𝐿 = 𝑖 ∈ ℕ0 (𝐻𝑖)       (𝜑𝐿:dom 𝐿1-1𝐴)
 
Theoremennnfonelemrn 12438* Lemma for ennnfone 12444. 𝐿 is onto 𝐴. (Contributed by Jim Kingdon, 16-Jul-2023.)
(𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)    &   (𝜑𝐹:ω–onto𝐴)    &   (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗))    &   𝐺 = (𝑥 ∈ (𝐴pm ω), 𝑦 ∈ ω ↦ if((𝐹𝑦) ∈ (𝐹𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹𝑦)⟩})))    &   𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (𝑁‘(𝑥 − 1))))    &   𝐻 = seq0(𝐺, 𝐽)    &   𝐿 = 𝑖 ∈ ℕ0 (𝐻𝑖)       (𝜑 → ran 𝐿 = 𝐴)
 
Theoremennnfonelemdm 12439* Lemma for ennnfone 12444. The function 𝐿 is defined everywhere. (Contributed by Jim Kingdon, 16-Jul-2023.)
(𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)    &   (𝜑𝐹:ω–onto𝐴)    &   (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗))    &   𝐺 = (𝑥 ∈ (𝐴pm ω), 𝑦 ∈ ω ↦ if((𝐹𝑦) ∈ (𝐹𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹𝑦)⟩})))    &   𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (𝑁‘(𝑥 − 1))))    &   𝐻 = seq0(𝐺, 𝐽)    &   𝐿 = 𝑖 ∈ ℕ0 (𝐻𝑖)       (𝜑 → dom 𝐿 = ω)
 
Theoremennnfonelemen 12440* Lemma for ennnfone 12444. The result. (Contributed by Jim Kingdon, 16-Jul-2023.)
(𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)    &   (𝜑𝐹:ω–onto𝐴)    &   (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗))    &   𝐺 = (𝑥 ∈ (𝐴pm ω), 𝑦 ∈ ω ↦ if((𝐹𝑦) ∈ (𝐹𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹𝑦)⟩})))    &   𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (𝑁‘(𝑥 − 1))))    &   𝐻 = seq0(𝐺, 𝐽)    &   𝐿 = 𝑖 ∈ ℕ0 (𝐻𝑖)       (𝜑𝐴 ≈ ℕ)
 
Theoremennnfonelemnn0 12441* Lemma for ennnfone 12444. A version of ennnfonelemen 12440 expressed in terms of 0 instead of ω. (Contributed by Jim Kingdon, 27-Oct-2022.)
(𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)    &   (𝜑𝐹:ℕ0onto𝐴)    &   (𝜑 → ∀𝑛 ∈ ℕ0𝑘 ∈ ℕ0𝑗 ∈ (0...𝑛)(𝐹𝑘) ≠ (𝐹𝑗))    &   𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)       (𝜑𝐴 ≈ ℕ)
 
Theoremennnfonelemr 12442* Lemma for ennnfone 12444. The interesting direction, expressed in deduction form. (Contributed by Jim Kingdon, 27-Oct-2022.)
(𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)    &   (𝜑𝐹:ℕ0onto𝐴)    &   (𝜑 → ∀𝑛 ∈ ℕ0𝑘 ∈ ℕ0𝑗 ∈ (0...𝑛)(𝐹𝑘) ≠ (𝐹𝑗))       (𝜑𝐴 ≈ ℕ)
 
Theoremennnfonelemim 12443* Lemma for ennnfone 12444. The trivial direction. (Contributed by Jim Kingdon, 27-Oct-2022.)
(𝐴 ≈ ℕ → (∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑓(𝑓:ℕ0onto𝐴 ∧ ∀𝑛 ∈ ℕ0𝑘 ∈ ℕ0𝑗 ∈ (0...𝑛)(𝑓𝑘) ≠ (𝑓𝑗))))
 
Theoremennnfone 12444* A condition for a set being countably infinite. Corollary 8.1.13 of [AczelRathjen], p. 73. Roughly speaking, the condition says that 𝐴 is countable (that's the 𝑓:ℕ0onto𝐴 part, as seen in theorems like ctm 7126), infinite (that's the part about being able to find an element of 𝐴 distinct from any mapping of a natural number via 𝑓), and has decidable equality. (Contributed by Jim Kingdon, 27-Oct-2022.)
(𝐴 ≈ ℕ ↔ (∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑓(𝑓:ℕ0onto𝐴 ∧ ∀𝑛 ∈ ℕ0𝑘 ∈ ℕ0𝑗 ∈ (0...𝑛)(𝑓𝑘) ≠ (𝑓𝑗))))
 
Theoremexmidunben 12445* If any unbounded set of positive integers is equinumerous to , then the Limited Principle of Omniscience (LPO) implies excluded middle. (Contributed by Jim Kingdon, 29-Jul-2023.)
((∀𝑥((𝑥 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛𝑥 𝑚 < 𝑛) → 𝑥 ≈ ℕ) ∧ ω ∈ Omni) → EXMID)
 
Theoremctinfomlemom 12446* Lemma for ctinfom 12447. Converting between ω and 0. (Contributed by Jim Kingdon, 10-Aug-2023.)
𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   𝐺 = (𝐹𝑁)    &   (𝜑𝐹:ω–onto𝐴)    &   (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝐹𝑘) ∈ (𝐹𝑛))       (𝜑 → (𝐺:ℕ0onto𝐴 ∧ ∀𝑚 ∈ ℕ0𝑗 ∈ ℕ0𝑖 ∈ (0...𝑚)(𝐺𝑗) ≠ (𝐺𝑖)))
 
Theoremctinfom 12447* A condition for a set being countably infinite. Restates ennnfone 12444 in terms of ω and function image. Like ennnfone 12444 the condition can be summarized as 𝐴 being countable, infinite, and having decidable equality. (Contributed by Jim Kingdon, 7-Aug-2023.)
(𝐴 ≈ ℕ ↔ (∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑓(𝑓:ω–onto𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓𝑘) ∈ (𝑓𝑛))))
 
Theoreminffinp1 12448* An infinite set contains an element not contained in a given finite subset. (Contributed by Jim Kingdon, 7-Aug-2023.)
(𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)    &   (𝜑 → ω ≼ 𝐴)    &   (𝜑𝐵𝐴)    &   (𝜑𝐵 ∈ Fin)       (𝜑 → ∃𝑥𝐴 ¬ 𝑥𝐵)
 
Theoremctinf 12449* A set is countably infinite if and only if it has decidable equality, is countable, and is infinite. (Contributed by Jim Kingdon, 7-Aug-2023.)
(𝐴 ≈ ℕ ↔ (∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑓 𝑓:ω–onto𝐴 ∧ ω ≼ 𝐴))
 
Theoremqnnen 12450 The rational numbers are countably infinite. Corollary 8.1.23 of [AczelRathjen], p. 75. This is Metamath 100 proof #3. (Contributed by Jim Kingdon, 11-Aug-2023.)
ℚ ≈ ℕ
 
Theoremenctlem 12451* Lemma for enct 12452. One direction of the biconditional. (Contributed by Jim Kingdon, 23-Dec-2023.)
(𝐴𝐵 → (∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) → ∃𝑔 𝑔:ω–onto→(𝐵 ⊔ 1o)))
 
Theoremenct 12452* Countability is invariant relative to equinumerosity. (Contributed by Jim Kingdon, 23-Dec-2023.)
(𝐴𝐵 → (∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) ↔ ∃𝑔 𝑔:ω–onto→(𝐵 ⊔ 1o)))
 
Theoremctiunctlemu1st 12453* Lemma for ctiunct 12459. (Contributed by Jim Kingdon, 28-Oct-2023.)
(𝜑𝑆 ⊆ ω)    &   (𝜑 → ∀𝑛 ∈ ω DECID 𝑛𝑆)    &   (𝜑𝐹:𝑆onto𝐴)    &   ((𝜑𝑥𝐴) → 𝑇 ⊆ ω)    &   ((𝜑𝑥𝐴) → ∀𝑛 ∈ ω DECID 𝑛𝑇)    &   ((𝜑𝑥𝐴) → 𝐺:𝑇onto𝐵)    &   (𝜑𝐽:ω–1-1-onto→(ω × ω))    &   𝑈 = {𝑧 ∈ ω ∣ ((1st ‘(𝐽𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽𝑧)) ∈ (𝐹‘(1st ‘(𝐽𝑧))) / 𝑥𝑇)}    &   (𝜑𝑁𝑈)       (𝜑 → (1st ‘(𝐽𝑁)) ∈ 𝑆)
 
Theoremctiunctlemu2nd 12454* Lemma for ctiunct 12459. (Contributed by Jim Kingdon, 28-Oct-2023.)
(𝜑𝑆 ⊆ ω)    &   (𝜑 → ∀𝑛 ∈ ω DECID 𝑛𝑆)    &   (𝜑𝐹:𝑆onto𝐴)    &   ((𝜑𝑥𝐴) → 𝑇 ⊆ ω)    &   ((𝜑𝑥𝐴) → ∀𝑛 ∈ ω DECID 𝑛𝑇)    &   ((𝜑𝑥𝐴) → 𝐺:𝑇onto𝐵)    &   (𝜑𝐽:ω–1-1-onto→(ω × ω))    &   𝑈 = {𝑧 ∈ ω ∣ ((1st ‘(𝐽𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽𝑧)) ∈ (𝐹‘(1st ‘(𝐽𝑧))) / 𝑥𝑇)}    &   (𝜑𝑁𝑈)       (𝜑 → (2nd ‘(𝐽𝑁)) ∈ (𝐹‘(1st ‘(𝐽𝑁))) / 𝑥𝑇)
 
Theoremctiunctlemuom 12455 Lemma for ctiunct 12459. (Contributed by Jim Kingdon, 28-Oct-2023.)
(𝜑𝑆 ⊆ ω)    &   (𝜑 → ∀𝑛 ∈ ω DECID 𝑛𝑆)    &   (𝜑𝐹:𝑆onto𝐴)    &   ((𝜑𝑥𝐴) → 𝑇 ⊆ ω)    &   ((𝜑𝑥𝐴) → ∀𝑛 ∈ ω DECID 𝑛𝑇)    &   ((𝜑𝑥𝐴) → 𝐺:𝑇onto𝐵)    &   (𝜑𝐽:ω–1-1-onto→(ω × ω))    &   𝑈 = {𝑧 ∈ ω ∣ ((1st ‘(𝐽𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽𝑧)) ∈ (𝐹‘(1st ‘(𝐽𝑧))) / 𝑥𝑇)}       (𝜑𝑈 ⊆ ω)
 
Theoremctiunctlemudc 12456* Lemma for ctiunct 12459. (Contributed by Jim Kingdon, 28-Oct-2023.)
(𝜑𝑆 ⊆ ω)    &   (𝜑 → ∀𝑛 ∈ ω DECID 𝑛𝑆)    &   (𝜑𝐹:𝑆onto𝐴)    &   ((𝜑𝑥𝐴) → 𝑇 ⊆ ω)    &   ((𝜑𝑥𝐴) → ∀𝑛 ∈ ω DECID 𝑛𝑇)    &   ((𝜑𝑥𝐴) → 𝐺:𝑇onto𝐵)    &   (𝜑𝐽:ω–1-1-onto→(ω × ω))    &   𝑈 = {𝑧 ∈ ω ∣ ((1st ‘(𝐽𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽𝑧)) ∈ (𝐹‘(1st ‘(𝐽𝑧))) / 𝑥𝑇)}       (𝜑 → ∀𝑛 ∈ ω DECID 𝑛𝑈)
 
Theoremctiunctlemf 12457* Lemma for ctiunct 12459. (Contributed by Jim Kingdon, 28-Oct-2023.)
(𝜑𝑆 ⊆ ω)    &   (𝜑 → ∀𝑛 ∈ ω DECID 𝑛𝑆)    &   (𝜑𝐹:𝑆onto𝐴)    &   ((𝜑𝑥𝐴) → 𝑇 ⊆ ω)    &   ((𝜑𝑥𝐴) → ∀𝑛 ∈ ω DECID 𝑛𝑇)    &   ((𝜑𝑥𝐴) → 𝐺:𝑇onto𝐵)    &   (𝜑𝐽:ω–1-1-onto→(ω × ω))    &   𝑈 = {𝑧 ∈ ω ∣ ((1st ‘(𝐽𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽𝑧)) ∈ (𝐹‘(1st ‘(𝐽𝑧))) / 𝑥𝑇)}    &   𝐻 = (𝑛𝑈 ↦ ((𝐹‘(1st ‘(𝐽𝑛))) / 𝑥𝐺‘(2nd ‘(𝐽𝑛))))       (𝜑𝐻:𝑈 𝑥𝐴 𝐵)
 
Theoremctiunctlemfo 12458* Lemma for ctiunct 12459. (Contributed by Jim Kingdon, 28-Oct-2023.)
(𝜑𝑆 ⊆ ω)    &   (𝜑 → ∀𝑛 ∈ ω DECID 𝑛𝑆)    &   (𝜑𝐹:𝑆onto𝐴)    &   ((𝜑𝑥𝐴) → 𝑇 ⊆ ω)    &   ((𝜑𝑥𝐴) → ∀𝑛 ∈ ω DECID 𝑛𝑇)    &   ((𝜑𝑥𝐴) → 𝐺:𝑇onto𝐵)    &   (𝜑𝐽:ω–1-1-onto→(ω × ω))    &   𝑈 = {𝑧 ∈ ω ∣ ((1st ‘(𝐽𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽𝑧)) ∈ (𝐹‘(1st ‘(𝐽𝑧))) / 𝑥𝑇)}    &   𝐻 = (𝑛𝑈 ↦ ((𝐹‘(1st ‘(𝐽𝑛))) / 𝑥𝐺‘(2nd ‘(𝐽𝑛))))    &   𝑥𝐻    &   𝑥𝑈       (𝜑𝐻:𝑈onto 𝑥𝐴 𝐵)
 
Theoremctiunct 12459* A sequence of enumerations gives an enumeration of the union. We refer to "sequence of enumerations" rather than "countably many countable sets" because the hypothesis provides more than countability for each 𝐵(𝑥): it refers to 𝐵(𝑥) together with the 𝐺(𝑥) which enumerates it. Theorem 8.1.19 of [AczelRathjen], p. 74.

For "countably many countable sets" the key hypothesis would be (𝜑𝑥𝐴) → ∃𝑔𝑔:ω–onto→(𝐵 ⊔ 1o). This is almost omiunct 12463 (which uses countable choice) although that is for a countably infinite collection not any countable collection.

Compare with the case of two sets instead of countably many, as seen at unct 12461, which says that the union of two countable sets is countable .

The proof proceeds by mapping a natural number to a pair of natural numbers (by xpomen 12414) and using the first number to map to an element 𝑥 of 𝐴 and the second number to map to an element of B(x) . In this way we are able to map to every element of 𝑥𝐴𝐵. Although it would be possible to work directly with countability expressed as 𝐹:ω–onto→(𝐴 ⊔ 1o), we instead use functions from subsets of the natural numbers via ctssdccl 7128 and ctssdc 7130.

(Contributed by Jim Kingdon, 31-Oct-2023.)

(𝜑𝐹:ω–onto→(𝐴 ⊔ 1o))    &   ((𝜑𝑥𝐴) → 𝐺:ω–onto→(𝐵 ⊔ 1o))       (𝜑 → ∃ :ω–onto→( 𝑥𝐴 𝐵 ⊔ 1o))
 
Theoremctiunctal 12460* Variation of ctiunct 12459 which allows 𝑥 to be present in 𝜑. (Contributed by Jim Kingdon, 5-May-2024.)
(𝜑𝐹:ω–onto→(𝐴 ⊔ 1o))    &   (𝜑 → ∀𝑥𝐴 𝐺:ω–onto→(𝐵 ⊔ 1o))       (𝜑 → ∃ :ω–onto→( 𝑥𝐴 𝐵 ⊔ 1o))
 
Theoremunct 12461* The union of two countable sets is countable. Corollary 8.1.20 of [AczelRathjen], p. 75. (Contributed by Jim Kingdon, 1-Nov-2023.)
((∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) ∧ ∃𝑔 𝑔:ω–onto→(𝐵 ⊔ 1o)) → ∃ :ω–onto→((𝐴𝐵) ⊔ 1o))
 
Theoremomctfn 12462* Using countable choice to find a sequence of enumerations for a collection of countable sets. Lemma 8.1.27 of [AczelRathjen], p. 77. (Contributed by Jim Kingdon, 19-Apr-2024.)
(𝜑CCHOICE)    &   ((𝜑𝑥 ∈ ω) → ∃𝑔 𝑔:ω–onto→(𝐵 ⊔ 1o))       (𝜑 → ∃𝑓(𝑓 Fn ω ∧ ∀𝑥 ∈ ω (𝑓𝑥):ω–onto→(𝐵 ⊔ 1o)))
 
Theoremomiunct 12463* The union of a countably infinite collection of countable sets is countable. Theorem 8.1.28 of [AczelRathjen], p. 78. Compare with ctiunct 12459 which has a stronger hypothesis but does not require countable choice. (Contributed by Jim Kingdon, 5-May-2024.)
(𝜑CCHOICE)    &   ((𝜑𝑥 ∈ ω) → ∃𝑔 𝑔:ω–onto→(𝐵 ⊔ 1o))       (𝜑 → ∃ :ω–onto→( 𝑥 ∈ ω 𝐵 ⊔ 1o))
 
Theoremssomct 12464* A decidable subset of ω is countable. (Contributed by Jim Kingdon, 19-Sep-2024.)
((𝐴 ⊆ ω ∧ ∀𝑥 ∈ ω DECID 𝑥𝐴) → ∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o))
 
Theoremssnnctlemct 12465* Lemma for ssnnct 12466. The result. (Contributed by Jim Kingdon, 29-Sep-2024.)
𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 1)       ((𝐴 ⊆ ℕ ∧ ∀𝑥 ∈ ℕ DECID 𝑥𝐴) → ∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o))
 
Theoremssnnct 12466* A decidable subset of is countable. (Contributed by Jim Kingdon, 29-Sep-2024.)
((𝐴 ⊆ ℕ ∧ ∀𝑥 ∈ ℕ DECID 𝑥𝐴) → ∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o))
 
Theoremnninfdclemcl 12467* Lemma for nninfdc 12472. (Contributed by Jim Kingdon, 25-Sep-2024.)
(𝜑𝐴 ⊆ ℕ)    &   (𝜑 → ∀𝑥 ∈ ℕ DECID 𝑥𝐴)    &   (𝜑 → ∀𝑚 ∈ ℕ ∃𝑛𝐴 𝑚 < 𝑛)    &   (𝜑𝑃𝐴)    &   (𝜑𝑄𝐴)       (𝜑 → (𝑃(𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < ))𝑄) ∈ 𝐴)
 
Theoremnninfdclemf 12468* Lemma for nninfdc 12472. A function from the natural numbers into 𝐴. (Contributed by Jim Kingdon, 23-Sep-2024.)
(𝜑𝐴 ⊆ ℕ)    &   (𝜑 → ∀𝑥 ∈ ℕ DECID 𝑥𝐴)    &   (𝜑 → ∀𝑚 ∈ ℕ ∃𝑛𝐴 𝑚 < 𝑛)    &   (𝜑 → (𝐽𝐴 ∧ 1 < 𝐽))    &   𝐹 = seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))       (𝜑𝐹:ℕ⟶𝐴)
 
Theoremnninfdclemp1 12469* Lemma for nninfdc 12472. Each element of the sequence 𝐹 is greater than the previous element. (Contributed by Jim Kingdon, 26-Sep-2024.)
(𝜑𝐴 ⊆ ℕ)    &   (𝜑 → ∀𝑥 ∈ ℕ DECID 𝑥𝐴)    &   (𝜑 → ∀𝑚 ∈ ℕ ∃𝑛𝐴 𝑚 < 𝑛)    &   (𝜑 → (𝐽𝐴 ∧ 1 < 𝐽))    &   𝐹 = seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))    &   (𝜑𝑈 ∈ ℕ)       (𝜑 → (𝐹𝑈) < (𝐹‘(𝑈 + 1)))
 
Theoremnninfdclemlt 12470* Lemma for nninfdc 12472. The function from nninfdclemf 12468 is strictly monotonic. (Contributed by Jim Kingdon, 24-Sep-2024.)
(𝜑𝐴 ⊆ ℕ)    &   (𝜑 → ∀𝑥 ∈ ℕ DECID 𝑥𝐴)    &   (𝜑 → ∀𝑚 ∈ ℕ ∃𝑛𝐴 𝑚 < 𝑛)    &   (𝜑 → (𝐽𝐴 ∧ 1 < 𝐽))    &   𝐹 = seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))    &   (𝜑𝑈 ∈ ℕ)    &   (𝜑𝑉 ∈ ℕ)    &   (𝜑𝑈 < 𝑉)       (𝜑 → (𝐹𝑈) < (𝐹𝑉))
 
Theoremnninfdclemf1 12471* Lemma for nninfdc 12472. The function from nninfdclemf 12468 is one-to-one. (Contributed by Jim Kingdon, 23-Sep-2024.)
(𝜑𝐴 ⊆ ℕ)    &   (𝜑 → ∀𝑥 ∈ ℕ DECID 𝑥𝐴)    &   (𝜑 → ∀𝑚 ∈ ℕ ∃𝑛𝐴 𝑚 < 𝑛)    &   (𝜑 → (𝐽𝐴 ∧ 1 < 𝐽))    &   𝐹 = seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))       (𝜑𝐹:ℕ–1-1𝐴)
 
Theoremnninfdc 12472* An unbounded decidable set of positive integers is infinite. (Contributed by Jim Kingdon, 23-Sep-2024.)
((𝐴 ⊆ ℕ ∧ ∀𝑥 ∈ ℕ DECID 𝑥𝐴 ∧ ∀𝑚 ∈ ℕ ∃𝑛𝐴 𝑚 < 𝑛) → ω ≼ 𝐴)
 
Theoremunbendc 12473* An unbounded decidable set of positive integers is infinite. (Contributed by NM, 5-May-2005.) (Revised by Jim Kingdon, 30-Sep-2024.)
((𝐴 ⊆ ℕ ∧ ∀𝑥 ∈ ℕ DECID 𝑥𝐴 ∧ ∀𝑚 ∈ ℕ ∃𝑛𝐴 𝑚 < 𝑛) → 𝐴 ≈ ℕ)
 
Theoremprminf 12474 There are an infinite number of primes. Theorem 1.7 in [ApostolNT] p. 16. (Contributed by Paul Chapman, 28-Nov-2012.)
ℙ ≈ ℕ
 
Theoreminfpn2 12475* There exist infinitely many prime numbers: the set of all primes 𝑆 is unbounded by infpn 12377, so by unbendc 12473 it is infinite. This is Metamath 100 proof #11. (Contributed by NM, 5-May-2005.)
𝑆 = {𝑛 ∈ ℕ ∣ (1 < 𝑛 ∧ ∀𝑚 ∈ ℕ ((𝑛 / 𝑚) ∈ ℕ → (𝑚 = 1 ∨ 𝑚 = 𝑛)))}       𝑆 ≈ ℕ
 
PART 6  BASIC STRUCTURES
 
6.1  Extensible structures
 
6.1.1  Basic definitions

An "extensible structure" (or "structure" in short, at least in this section) is used to define a specific group, ring, poset, and so on. An extensible structure can contain many components. For example, a group will have at least two components (base set and operation), although it can be further specialized by adding other components such as a multiplicative operation for rings (and still remain a group per our definition). Thus, every ring is also a group. This extensible structure approach allows theorems from more general structures (such as groups) to be reused for more specialized structures (such as rings) without having to reprove anything. Structures are common in mathematics, but in informal (natural language) proofs the details are assumed in ways that we must make explicit.

An extensible structure is implemented as a function (a set of ordered pairs) on a finite (and not necessarily sequential) subset of . The function's argument is the index of a structure component (such as 1 for the base set of a group), and its value is the component (such as the base set). By convention, we normally avoid direct reference to the hard-coded numeric index and instead use structure component extractors such as ndxid 12504 and strslfv 12525. Using extractors makes it easier to change numeric indices and also makes the components' purpose clearer. See the comment of basendx 12535 for more details on numeric indices versus the structure component extractors.

There are many other possible ways to handle structures. We chose this extensible structure approach because this approach (1) results in simpler notation than other approaches we are aware of, and (2) is easier to do proofs with. We cannot use an approach that uses "hidden" arguments; Metamath does not support hidden arguments, and in any case we want nothing hidden. It would be possible to use a categorical approach (e.g., something vaguely similar to Lean's mathlib). However, instances (the chain of proofs that an 𝑋 is a 𝑌 via a bunch of forgetful functors) can cause serious performance problems for automated tooling, and the resulting proofs would be painful to look at directly (in the case of Lean, they are long past the level where people would find it acceptable to look at them directly). Metamath is working under much stricter conditions than this, and it has still managed to achieve about the same level of flexibility through this "extensible structure" approach.

To create a substructure of a given extensible structure, you can simply use the multifunction restriction operator for extensible structures s as defined in df-iress 12488. This can be used to turn statements about rings into statements about subrings, modules into submodules, etc. This definition knows nothing about individual structures and merely truncates the Base set while leaving operators alone. Individual kinds of structures will need to handle this behavior by ignoring operators' values outside the range, defining a function using the base set and applying that, or explicitly truncating the slot before use.

Extensible structures only work well when they represent concrete categories, where there is a "base set", morphisms are functions, and subobjects are subsets with induced operations. In short, they primarily work well for "sets with (some) extra structure". Extensible structures may not suffice for more complicated situations. For example, in manifolds, s would not work. That said, extensible structures are sufficient for many of the structures that set.mm currently considers, and offer a good compromise for a goal-oriented formalization.

 
Syntaxcstr 12476 Extend class notation with the class of structures with components numbered below 𝐴.
class Struct
 
Syntaxcnx 12477 Extend class notation with the structure component index extractor.
class ndx
 
Syntaxcsts 12478 Set components of a structure.
class sSet
 
Syntaxcslot 12479 Extend class notation with the slot function.
class Slot 𝐴
 
Syntaxcbs 12480 Extend class notation with the class of all base set extractors.
class Base
 
Syntaxcress 12481 Extend class notation with the extensible structure builder restriction operator.
class s
 
Definitiondf-struct 12482* Define a structure with components in 𝑀...𝑁. This is not a requirement for groups, posets, etc., but it is a useful assumption for component extraction theorems.

As mentioned in the section header, an "extensible structure should be implemented as a function (a set of ordered pairs)". The current definition, however, is less restrictive: it allows for classes which contain the empty set to be extensible structures. Because of 0nelfun 5249, such classes cannot be functions. Without the empty set, however, a structure must be a function, see structn0fun 12493: 𝐹 Struct 𝑋 → Fun (𝐹 ∖ {∅}).

Allowing an extensible structure to contain the empty set ensures that expressions like {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} are structures without asserting or implying that 𝐴, 𝐵, 𝐶 and 𝐷 are sets (if 𝐴 or 𝐵 is a proper class, then 𝐴, 𝐵⟩ = ∅, see opprc 3814). (Contributed by Mario Carneiro, 29-Aug-2015.)

Struct = {⟨𝑓, 𝑥⟩ ∣ (𝑥 ∈ ( ≤ ∩ (ℕ × ℕ)) ∧ Fun (𝑓 ∖ {∅}) ∧ dom 𝑓 ⊆ (...‘𝑥))}
 
Definitiondf-ndx 12483 Define the structure component index extractor. See Theorem ndxarg 12503 to understand its purpose. The restriction to ensures that ndx is a set. The restriction to some set is necessary since I is a proper class. In principle, we could have chosen or (if we revise all structure component definitions such as df-base 12486) another set such as the set of finite ordinals ω (df-iom 4605). (Contributed by NM, 4-Sep-2011.)
ndx = ( I ↾ ℕ)
 
Definitiondf-slot 12484* Define the slot extractor for extensible structures. The class Slot 𝐴 is a function whose argument can be any set, although it is meaningful only if that set is a member of an extensible structure (such as a partially ordered set or a group).

Note that Slot 𝐴 is implemented as "evaluation at 𝐴". That is, (Slot 𝐴𝑆) is defined to be (𝑆𝐴), where 𝐴 will typically be a small nonzero natural number. Each extensible structure 𝑆 is a function defined on specific natural number "slots", and this function extracts the value at a particular slot.

The special "structure" ndx, defined as the identity function restricted to , can be used to extract the number 𝐴 from a slot, since (Slot 𝐴‘ndx) = 𝐴 (see ndxarg 12503). This is typically used to refer to the number of a slot when defining structures without having to expose the detail of what that number is (for instance, we use the expression (Base‘ndx) in theorems and proofs instead of its value 1).

The class Slot cannot be defined as (𝑥 ∈ V ↦ (𝑓 ∈ V ↦ (𝑓𝑥))) because each Slot 𝐴 is a function on the proper class V so is itself a proper class, and the values of functions are sets (fvex 5550). It is necessary to allow proper classes as values of Slot 𝐴 since for instance the class of all (base sets of) groups is proper. (Contributed by Mario Carneiro, 22-Sep-2015.)

Slot 𝐴 = (𝑥 ∈ V ↦ (𝑥𝐴))
 
Theoremsloteq 12485 Equality theorem for the Slot construction. The converse holds if 𝐴 (or 𝐵) is a set. (Contributed by BJ, 27-Dec-2021.)
(𝐴 = 𝐵 → Slot 𝐴 = Slot 𝐵)
 
Definitiondf-base 12486 Define the base set (also called underlying set, ground set, carrier set, or carrier) extractor for extensible structures. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.)
Base = Slot 1
 
Definitiondf-sets 12487* Set a component of an extensible structure. This function is useful for taking an existing structure and "overriding" one of its components. For example, df-iress 12488 adjusts the base set to match its second argument, which has the effect of making subgroups, subspaces, subrings etc. from the original structures. (Contributed by Mario Carneiro, 1-Dec-2014.)
sSet = (𝑠 ∈ V, 𝑒 ∈ V ↦ ((𝑠 ↾ (V ∖ dom {𝑒})) ∪ {𝑒}))
 
Definitiondf-iress 12488* Define a multifunction restriction operator for extensible structures, which can be used to turn statements about rings into statements about subrings, modules into submodules, etc. This definition knows nothing about individual structures and merely truncates the Base set while leaving operators alone; individual kinds of structures will need to handle this behavior, by ignoring operators' values outside the range, defining a function using the base set and applying that, or explicitly truncating the slot before use.

(Credit for this operator, as well as the 2023 modification for iset.mm, goes to Mario Carneiro.)

(Contributed by Stefan O'Rear, 29-Nov-2014.) (Revised by Jim Kingdon, 7-Oct-2023.)

s = (𝑤 ∈ V, 𝑥 ∈ V ↦ (𝑤 sSet ⟨(Base‘ndx), (𝑥 ∩ (Base‘𝑤))⟩))
 
Theorembrstruct 12489 The structure relation is a relation. (Contributed by Mario Carneiro, 29-Aug-2015.)
Rel Struct
 
Theoremisstruct2im 12490 The property of being a structure with components in (1st𝑋)...(2nd𝑋). (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.)
(𝐹 Struct 𝑋 → (𝑋 ∈ ( ≤ ∩ (ℕ × ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)))
 
Theoremisstruct2r 12491 The property of being a structure with components in (1st𝑋)...(2nd𝑋). (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.)
(((𝑋 ∈ ( ≤ ∩ (ℕ × ℕ)) ∧ Fun (𝐹 ∖ {∅})) ∧ (𝐹𝑉 ∧ dom 𝐹 ⊆ (...‘𝑋))) → 𝐹 Struct 𝑋)
 
Theoremstructex 12492 A structure is a set. (Contributed by AV, 10-Nov-2021.)
(𝐺 Struct 𝑋𝐺 ∈ V)
 
Theoremstructn0fun 12493 A structure without the empty set is a function. (Contributed by AV, 13-Nov-2021.)
(𝐹 Struct 𝑋 → Fun (𝐹 ∖ {∅}))
 
Theoremisstructim 12494 The property of being a structure with components in 𝑀...𝑁. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.)
(𝐹 Struct ⟨𝑀, 𝑁⟩ → ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀𝑁) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (𝑀...𝑁)))
 
Theoremisstructr 12495 The property of being a structure with components in 𝑀...𝑁. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.)
(((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀𝑁) ∧ (Fun (𝐹 ∖ {∅}) ∧ 𝐹𝑉 ∧ dom 𝐹 ⊆ (𝑀...𝑁))) → 𝐹 Struct ⟨𝑀, 𝑁⟩)
 
Theoremstructcnvcnv 12496 Two ways to express the relational part of a structure. (Contributed by Mario Carneiro, 29-Aug-2015.)
(𝐹 Struct 𝑋𝐹 = (𝐹 ∖ {∅}))
 
Theoremstructfung 12497 The converse of the converse of a structure is a function. Closed form of structfun 12498. (Contributed by AV, 12-Nov-2021.)
(𝐹 Struct 𝑋 → Fun 𝐹)
 
Theoremstructfun 12498 Convert between two kinds of structure closure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Proof shortened by AV, 12-Nov-2021.)
𝐹 Struct 𝑋       Fun 𝐹
 
Theoremstructfn 12499 Convert between two kinds of structure closure. (Contributed by Mario Carneiro, 29-Aug-2015.)
𝐹 Struct ⟨𝑀, 𝑁       (Fun 𝐹 ∧ dom 𝐹 ⊆ (1...𝑁))
 
Theoremstrnfvnd 12500 Deduction version of strnfvn 12501. (Contributed by Mario Carneiro, 15-Nov-2014.) (Revised by Jim Kingdon, 19-Jan-2023.)
𝐸 = Slot 𝑁    &   (𝜑𝑆𝑉)    &   (𝜑𝑁 ∈ ℕ)       (𝜑 → (𝐸𝑆) = (𝑆𝑁))
    < 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-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15230
  Copyright terms: Public domain < Previous  Next >