Theorem List for Intuitionistic Logic Explorer - 12301-12400 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | dvdsprmpweqle 12301* |
If a positive integer divides a prime power, it is a prime power with a
smaller exponent. (Contributed by AV, 25-Jul-2021.)
|
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (𝐴 ∥ (𝑃↑𝑁) → ∃𝑛 ∈ ℕ0 (𝑛 ≤ 𝑁 ∧ 𝐴 = (𝑃↑𝑛)))) |
|
Theorem | difsqpwdvds 12302 |
If the difference of two squares is a power of a prime, the prime
divides twice the second squared number. (Contributed by AV,
13-Aug-2021.)
|
⊢ (((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0
∧ (𝐵 + 1) < 𝐴) ∧ (𝐶 ∈ ℙ ∧ 𝐷 ∈ ℕ0)) →
((𝐶↑𝐷) = ((𝐴↑2) − (𝐵↑2)) → 𝐶 ∥ (2 · 𝐵))) |
|
Theorem | pcaddlem 12303 |
Lemma for pcadd 12304. The original numbers 𝐴 and
𝐵
have been
decomposed using the prime count function as (𝑃↑𝑀) · (𝑅 / 𝑆)
where 𝑅, 𝑆 are both not divisible by 𝑃 and
𝑀 =
(𝑃 pCnt 𝐴), and similarly for 𝐵.
(Contributed by Mario
Carneiro, 9-Sep-2014.)
|
⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝐴 = ((𝑃↑𝑀) · (𝑅 / 𝑆))) & ⊢ (𝜑 → 𝐵 = ((𝑃↑𝑁) · (𝑇 / 𝑈))) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → (𝑅 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝑅)) & ⊢ (𝜑 → (𝑆 ∈ ℕ ∧ ¬ 𝑃 ∥ 𝑆)) & ⊢ (𝜑 → (𝑇 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝑇)) & ⊢ (𝜑 → (𝑈 ∈ ℕ ∧ ¬ 𝑃 ∥ 𝑈)) ⇒ ⊢ (𝜑 → 𝑀 ≤ (𝑃 pCnt (𝐴 + 𝐵))) |
|
Theorem | pcadd 12304 |
An inequality for the prime count of a sum. This is the source of the
ultrametric inequality for the p-adic metric. (Contributed by Mario
Carneiro, 9-Sep-2014.)
|
⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝐴 ∈ ℚ) & ⊢ (𝜑 → 𝐵 ∈ ℚ) & ⊢ (𝜑 → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵)) ⇒ ⊢ (𝜑 → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt (𝐴 + 𝐵))) |
|
Theorem | pcmptcl 12305 |
Closure for the prime power map. (Contributed by Mario Carneiro,
12-Mar-2014.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑𝐴), 1)) & ⊢ (𝜑 → ∀𝑛 ∈ ℙ 𝐴 ∈
ℕ0) ⇒ ⊢ (𝜑 → (𝐹:ℕ⟶ℕ ∧ seq1(
· , 𝐹):ℕ⟶ℕ)) |
|
Theorem | pcmpt 12306* |
Construct a function with given prime count characteristics.
(Contributed by Mario Carneiro, 12-Mar-2014.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑𝐴), 1)) & ⊢ (𝜑 → ∀𝑛 ∈ ℙ 𝐴 ∈
ℕ0)
& ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝑛 = 𝑃 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝑃 pCnt (seq1( · , 𝐹)‘𝑁)) = if(𝑃 ≤ 𝑁, 𝐵, 0)) |
|
Theorem | pcmpt2 12307* |
Dividing two prime count maps yields a number with all dividing primes
confined to an interval. (Contributed by Mario Carneiro,
14-Mar-2014.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑𝐴), 1)) & ⊢ (𝜑 → ∀𝑛 ∈ ℙ 𝐴 ∈
ℕ0)
& ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝑛 = 𝑃 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑁))
⇒ ⊢ (𝜑 → (𝑃 pCnt ((seq1( · , 𝐹)‘𝑀) / (seq1( · , 𝐹)‘𝑁))) = if((𝑃 ≤ 𝑀 ∧ ¬ 𝑃 ≤ 𝑁), 𝐵, 0)) |
|
Theorem | pcmptdvds 12308 |
The partial products of the prime power map form a divisibility chain.
(Contributed by Mario Carneiro, 12-Mar-2014.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑𝐴), 1)) & ⊢ (𝜑 → ∀𝑛 ∈ ℙ 𝐴 ∈
ℕ0)
& ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑁))
⇒ ⊢ (𝜑 → (seq1( · , 𝐹)‘𝑁) ∥ (seq1( · , 𝐹)‘𝑀)) |
|
Theorem | pcprod 12309* |
The product of the primes taken to their respective powers reconstructs
the original number. (Contributed by Mario Carneiro, 12-Mar-2014.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt 𝑁)), 1)) ⇒ ⊢ (𝑁 ∈ ℕ → (seq1( · ,
𝐹)‘𝑁) = 𝑁) |
|
Theorem | sumhashdc 12310* |
The sum of 1 over a set is the size of the set. (Contributed by Mario
Carneiro, 8-Mar-2014.) (Revised by Mario Carneiro, 20-May-2014.)
|
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐵 DECID 𝑥 ∈ 𝐴) → Σ𝑘 ∈ 𝐵 if(𝑘 ∈ 𝐴, 1, 0) = (♯‘𝐴)) |
|
Theorem | fldivp1 12311 |
The difference between the floors of adjacent fractions is either 1 or 0.
(Contributed by Mario Carneiro, 8-Mar-2014.)
|
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) →
((⌊‘((𝑀 + 1) /
𝑁)) −
(⌊‘(𝑀 / 𝑁))) = if(𝑁 ∥ (𝑀 + 1), 1, 0)) |
|
Theorem | pcfaclem 12312 |
Lemma for pcfac 12313. (Contributed by Mario Carneiro,
20-May-2014.)
|
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈
(ℤ≥‘𝑁) ∧ 𝑃 ∈ ℙ) →
(⌊‘(𝑁 / (𝑃↑𝑀))) = 0) |
|
Theorem | pcfac 12313* |
Calculate the prime count of a factorial. (Contributed by Mario
Carneiro, 11-Mar-2014.) (Revised by Mario Carneiro, 21-May-2014.)
|
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈
(ℤ≥‘𝑁) ∧ 𝑃 ∈ ℙ) → (𝑃 pCnt (!‘𝑁)) = Σ𝑘 ∈ (1...𝑀)(⌊‘(𝑁 / (𝑃↑𝑘)))) |
|
Theorem | pcbc 12314* |
Calculate the prime count of a binomial coefficient. (Contributed by
Mario Carneiro, 11-Mar-2014.) (Revised by Mario Carneiro,
21-May-2014.)
|
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁) ∧ 𝑃 ∈ ℙ) → (𝑃 pCnt (𝑁C𝐾)) = Σ𝑘 ∈ (1...𝑁)((⌊‘(𝑁 / (𝑃↑𝑘))) − ((⌊‘((𝑁 − 𝐾) / (𝑃↑𝑘))) + (⌊‘(𝐾 / (𝑃↑𝑘)))))) |
|
Theorem | qexpz 12315 |
If a power of a rational number is an integer, then the number is an
integer. (Contributed by Mario Carneiro, 10-Aug-2015.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑁) ∈ ℤ) → 𝐴 ∈ ℤ) |
|
Theorem | expnprm 12316 |
A second or higher power of a rational number is not a prime number. Or
by contraposition, the n-th root of a prime number is not rational.
Suggested by Norm Megill. (Contributed by Mario Carneiro,
10-Aug-2015.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ (ℤ≥‘2))
→ ¬ (𝐴↑𝑁) ∈
ℙ) |
|
Theorem | oddprmdvds 12317* |
Every positive integer which is not a power of two is divisible by an
odd prime number. (Contributed by AV, 6-Aug-2021.)
|
⊢ ((𝐾 ∈ ℕ ∧ ¬ ∃𝑛 ∈ ℕ0
𝐾 = (2↑𝑛)) → ∃𝑝 ∈ (ℙ ∖
{2})𝑝 ∥ 𝐾) |
|
5.2.9 Pocklington's theorem
|
|
Theorem | prmpwdvds 12318 |
A relation involving divisibility by a prime power. (Contributed by
Mario Carneiro, 2-Mar-2014.)
|
⊢ (((𝐾 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) ∧ (𝐷 ∥ (𝐾 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝐾 · (𝑃↑(𝑁 − 1))))) → (𝑃↑𝑁) ∥ 𝐷) |
|
Theorem | pockthlem 12319 |
Lemma for pockthg 12320. (Contributed by Mario Carneiro,
2-Mar-2014.)
|
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐵 < 𝐴)
& ⊢ (𝜑 → 𝑁 = ((𝐴 · 𝐵) + 1)) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑃 ∥ 𝑁)
& ⊢ (𝜑 → 𝑄 ∈ ℙ) & ⊢ (𝜑 → (𝑄 pCnt 𝐴) ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℤ) & ⊢ (𝜑 → ((𝐶↑(𝑁 − 1)) mod 𝑁) = 1) & ⊢ (𝜑 → (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁) = 1) ⇒ ⊢ (𝜑 → (𝑄 pCnt 𝐴) ≤ (𝑄 pCnt (𝑃 − 1))) |
|
Theorem | pockthg 12320* |
The generalized Pocklington's theorem. If 𝑁 − 1 = 𝐴 · 𝐵 where
𝐵
< 𝐴, then 𝑁 is
prime if and only if for every prime factor
𝑝 of 𝐴, there is an 𝑥 such that
𝑥↑(𝑁 − 1) = 1( mod 𝑁) and
gcd (𝑥↑((𝑁 − 1) / 𝑝) − 1, 𝑁) = 1. (Contributed by Mario
Carneiro, 2-Mar-2014.)
|
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐵 < 𝐴)
& ⊢ (𝜑 → 𝑁 = ((𝐴 · 𝐵) + 1)) & ⊢ (𝜑 → ∀𝑝 ∈ ℙ (𝑝 ∥ 𝐴 → ∃𝑥 ∈ ℤ (((𝑥↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝑥↑((𝑁 − 1) / 𝑝)) − 1) gcd 𝑁) = 1))) ⇒ ⊢ (𝜑 → 𝑁 ∈ ℙ) |
|
Theorem | pockthi 12321 |
Pocklington's theorem, which gives a sufficient criterion for a number
𝑁 to be prime. This is the preferred
method for verifying large
primes, being much more efficient to compute than trial division. This
form has been optimized for application to specific large primes; see
pockthg 12320 for a more general closed-form version.
(Contributed by Mario
Carneiro, 2-Mar-2014.)
|
⊢ 𝑃 ∈ ℙ & ⊢ 𝐺 ∈ ℕ & ⊢ 𝑀 = (𝐺 · 𝑃)
& ⊢ 𝑁 = (𝑀 + 1) & ⊢ 𝐷 ∈ ℕ & ⊢ 𝐸 ∈ ℕ & ⊢ 𝐴 ∈ ℕ & ⊢ 𝑀 = (𝐷 · (𝑃↑𝐸)) & ⊢ 𝐷 < (𝑃↑𝐸)
& ⊢ ((𝐴↑𝑀) mod 𝑁) = (1 mod 𝑁)
& ⊢ (((𝐴↑𝐺) − 1) gcd 𝑁) = 1 ⇒ ⊢ 𝑁 ∈ ℙ |
|
5.2.10 Infinite primes theorem
|
|
Theorem | infpnlem1 12322* |
Lemma for infpn 12324. The smallest divisor (greater than 1)
𝑀
of
𝑁!
+ 1 is a prime greater than 𝑁. (Contributed by NM,
5-May-2005.)
|
⊢ 𝐾 = ((!‘𝑁) + 1) ⇒ ⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (((1 < 𝑀 ∧ (𝐾 / 𝑀) ∈ ℕ) ∧ ∀𝑗 ∈ ℕ ((1 < 𝑗 ∧ (𝐾 / 𝑗) ∈ ℕ) → 𝑀 ≤ 𝑗)) → (𝑁 < 𝑀 ∧ ∀𝑗 ∈ ℕ ((𝑀 / 𝑗) ∈ ℕ → (𝑗 = 1 ∨ 𝑗 = 𝑀))))) |
|
Theorem | infpnlem2 12323* |
Lemma for infpn 12324. For any positive integer 𝑁, there
exists a
prime number 𝑗 greater than 𝑁. (Contributed by NM,
5-May-2005.)
|
⊢ 𝐾 = ((!‘𝑁) + 1) ⇒ ⊢ (𝑁 ∈ ℕ → ∃𝑗 ∈ ℕ (𝑁 < 𝑗 ∧ ∀𝑘 ∈ ℕ ((𝑗 / 𝑘) ∈ ℕ → (𝑘 = 1 ∨ 𝑘 = 𝑗)))) |
|
Theorem | infpn 12324* |
There exist infinitely many prime numbers: for any positive integer
𝑁, there exists a prime number 𝑗 greater
than 𝑁. (See
infpn2 12422 for the equinumerosity version.)
(Contributed by NM,
1-Jun-2006.)
|
⊢ (𝑁 ∈ ℕ → ∃𝑗 ∈ ℕ (𝑁 < 𝑗 ∧ ∀𝑘 ∈ ℕ ((𝑗 / 𝑘) ∈ ℕ → (𝑘 = 1 ∨ 𝑘 = 𝑗)))) |
|
Theorem | prmunb 12325* |
The primes are unbounded. (Contributed by Paul Chapman,
28-Nov-2012.)
|
⊢ (𝑁 ∈ ℕ → ∃𝑝 ∈ ℙ 𝑁 < 𝑝) |
|
5.2.11 Fundamental theorem of
arithmetic
|
|
Theorem | 1arithlem1 12326* |
Lemma for 1arith 12330. (Contributed by Mario Carneiro,
30-May-2014.)
|
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛))) ⇒ ⊢ (𝑁 ∈ ℕ → (𝑀‘𝑁) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑁))) |
|
Theorem | 1arithlem2 12327* |
Lemma for 1arith 12330. (Contributed by Mario Carneiro,
30-May-2014.)
|
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛))) ⇒ ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → ((𝑀‘𝑁)‘𝑃) = (𝑃 pCnt 𝑁)) |
|
Theorem | 1arithlem3 12328* |
Lemma for 1arith 12330. (Contributed by Mario Carneiro,
30-May-2014.)
|
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛))) ⇒ ⊢ (𝑁 ∈ ℕ → (𝑀‘𝑁):ℙ⟶ℕ0) |
|
Theorem | 1arithlem4 12329* |
Lemma for 1arith 12330. (Contributed by Mario Carneiro,
30-May-2014.)
|
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛))) & ⊢ 𝐺 = (𝑦 ∈ ℕ ↦ if(𝑦 ∈ ℙ, (𝑦↑(𝐹‘𝑦)), 1)) & ⊢ (𝜑 → 𝐹:ℙ⟶ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ ((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑁 ≤ 𝑞)) → (𝐹‘𝑞) = 0) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℕ 𝐹 = (𝑀‘𝑥)) |
|
Theorem | 1arith 12330* |
Fundamental theorem of arithmetic, where a prime factorization is
represented as a sequence of prime exponents, for which only finitely
many primes have nonzero exponent. The function 𝑀 maps
the set of
positive integers one-to-one onto the set of prime factorizations
𝑅. (Contributed by Paul Chapman,
17-Nov-2012.) (Proof shortened
by Mario Carneiro, 30-May-2014.)
|
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛))) & ⊢ 𝑅 = {𝑒 ∈ (ℕ0
↑𝑚 ℙ) ∣ (◡𝑒 “ ℕ) ∈
Fin} ⇒ ⊢ 𝑀:ℕ–1-1-onto→𝑅 |
|
Theorem | 1arith2 12331* |
Fundamental theorem of arithmetic, where a prime factorization is
represented as a finite monotonic 1-based sequence of primes. Every
positive integer has a unique prime factorization. Theorem 1.10 in
[ApostolNT] p. 17. This is Metamath
100 proof #80. (Contributed by
Paul Chapman, 17-Nov-2012.) (Revised by Mario Carneiro,
30-May-2014.)
|
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛))) & ⊢ 𝑅 = {𝑒 ∈ (ℕ0
↑𝑚 ℙ) ∣ (◡𝑒 “ ℕ) ∈
Fin} ⇒ ⊢ ∀𝑧 ∈ ℕ ∃!𝑔 ∈ 𝑅 (𝑀‘𝑧) = 𝑔 |
|
5.2.12 Lagrange's four-square
theorem
|
|
Syntax | cgz 12332 |
Extend class notation with the set of gaussian integers.
|
class ℤ[i] |
|
Definition | df-gz 12333 |
Define the set of gaussian integers, which are complex numbers whose real
and imaginary parts are integers. (Note that the [i] is actually
part of the symbol token and has no independent meaning.) (Contributed by
Mario Carneiro, 14-Jul-2014.)
|
⊢ ℤ[i] = {𝑥 ∈ ℂ ∣ ((ℜ‘𝑥) ∈ ℤ ∧
(ℑ‘𝑥) ∈
ℤ)} |
|
Theorem | elgz 12334 |
Elementhood in the gaussian integers. (Contributed by Mario Carneiro,
14-Jul-2014.)
|
⊢ (𝐴 ∈ ℤ[i] ↔ (𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
ℤ ∧ (ℑ‘𝐴) ∈ ℤ)) |
|
Theorem | gzcn 12335 |
A gaussian integer is a complex number. (Contributed by Mario Carneiro,
14-Jul-2014.)
|
⊢ (𝐴 ∈ ℤ[i] → 𝐴 ∈ ℂ) |
|
Theorem | zgz 12336 |
An integer is a gaussian integer. (Contributed by Mario Carneiro,
14-Jul-2014.)
|
⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℤ[i]) |
|
Theorem | igz 12337 |
i is a gaussian integer. (Contributed by Mario
Carneiro,
14-Jul-2014.)
|
⊢ i ∈ ℤ[i] |
|
Theorem | gznegcl 12338 |
The gaussian integers are closed under negation. (Contributed by Mario
Carneiro, 14-Jul-2014.)
|
⊢ (𝐴 ∈ ℤ[i] → -𝐴 ∈
ℤ[i]) |
|
Theorem | gzcjcl 12339 |
The gaussian integers are closed under conjugation. (Contributed by Mario
Carneiro, 14-Jul-2014.)
|
⊢ (𝐴 ∈ ℤ[i] →
(∗‘𝐴) ∈
ℤ[i]) |
|
Theorem | gzaddcl 12340 |
The gaussian integers are closed under addition. (Contributed by Mario
Carneiro, 14-Jul-2014.)
|
⊢ ((𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i]) → (𝐴 + 𝐵) ∈ ℤ[i]) |
|
Theorem | gzmulcl 12341 |
The gaussian integers are closed under multiplication. (Contributed by
Mario Carneiro, 14-Jul-2014.)
|
⊢ ((𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i]) → (𝐴 · 𝐵) ∈ ℤ[i]) |
|
Theorem | gzreim 12342 |
Construct a gaussian integer from real and imaginary parts. (Contributed
by Mario Carneiro, 16-Jul-2014.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 + (i · 𝐵)) ∈ ℤ[i]) |
|
Theorem | gzsubcl 12343 |
The gaussian integers are closed under subtraction. (Contributed by Mario
Carneiro, 14-Jul-2014.)
|
⊢ ((𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i]) → (𝐴 − 𝐵) ∈ ℤ[i]) |
|
Theorem | gzabssqcl 12344 |
The squared norm of a gaussian integer is an integer. (Contributed by
Mario Carneiro, 16-Jul-2014.)
|
⊢ (𝐴 ∈ ℤ[i] → ((abs‘𝐴)↑2) ∈
ℕ0) |
|
Theorem | 4sqlem5 12345 |
Lemma for 4sq (not yet proved here). (Contributed by Mario Carneiro,
15-Jul-2014.)
|
⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) ⇒ ⊢ (𝜑 → (𝐵 ∈ ℤ ∧ ((𝐴 − 𝐵) / 𝑀) ∈ ℤ)) |
|
Theorem | 4sqlem6 12346 |
Lemma for 4sq (not yet proved here) . (Contributed by Mario Carneiro,
15-Jul-2014.)
|
⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) ⇒ ⊢ (𝜑 → (-(𝑀 / 2) ≤ 𝐵 ∧ 𝐵 < (𝑀 / 2))) |
|
Theorem | 4sqlem7 12347 |
Lemma for 4sq (not yet proved here) . (Contributed by Mario Carneiro,
15-Jul-2014.)
|
⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) ⇒ ⊢ (𝜑 → (𝐵↑2) ≤ (((𝑀↑2) / 2) / 2)) |
|
Theorem | 4sqlem8 12348 |
Lemma for 4sq (not yet proved here) . (Contributed by Mario Carneiro,
15-Jul-2014.)
|
⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) ⇒ ⊢ (𝜑 → 𝑀 ∥ ((𝐴↑2) − (𝐵↑2))) |
|
Theorem | 4sqlem9 12349 |
Lemma for 4sq (not yet proved here) . (Contributed by Mario Carneiro,
15-Jul-2014.)
|
⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) & ⊢ ((𝜑 ∧ 𝜓) → (𝐵↑2) = 0)
⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝑀↑2) ∥ (𝐴↑2)) |
|
Theorem | 4sqlem10 12350 |
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))) |
|
Theorem | 4sqlem1 12351* |
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 |
|
Theorem | 4sqlem2 12352* |
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)))) |
|
Theorem | 4sqlem3 12353* |
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))) ∈ 𝑆) |
|
Theorem | 4sqlem4a 12354* |
Lemma for 4sqlem4 12355. (Contributed by Mario Carneiro,
14-Jul-2014.)
|
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))} ⇒ ⊢ ((𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i]) →
(((abs‘𝐴)↑2) +
((abs‘𝐵)↑2))
∈ 𝑆) |
|
Theorem | 4sqlem4 12355* |
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))) |
|
Theorem | mul4sqlem 12356* |
Lemma for mul4sq 12357: 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) ⇒ ⊢ (𝜑 → ((𝑋 / 𝑀) · (𝑌 / 𝑀)) ∈ 𝑆) |
|
Theorem | mul4sq 12357* |
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 12356. (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
|
|
Theorem | oddennn 12358 |
There are as many odd positive integers as there are positive integers.
(Contributed by Jim Kingdon, 11-May-2022.)
|
⊢ {𝑧 ∈ ℕ ∣ ¬ 2 ∥
𝑧} ≈
ℕ |
|
Theorem | evenennn 12359 |
There are as many even positive integers as there are positive integers.
(Contributed by Jim Kingdon, 12-May-2022.)
|
⊢ {𝑧 ∈ ℕ ∣ 2 ∥ 𝑧} ≈
ℕ |
|
Theorem | xpnnen 12360 |
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.)
|
⊢ (ℕ × ℕ) ≈
ℕ |
|
Theorem | xpomen 12361 |
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.)
|
⊢ (ω × ω) ≈
ω |
|
Theorem | xpct 12362 |
The cartesian product of two sets dominated by ω
is dominated by
ω. (Contributed by Thierry Arnoux,
24-Sep-2017.)
|
⊢ ((𝐴 ≼ ω ∧ 𝐵 ≼ ω) → (𝐴 × 𝐵) ≼ ω) |
|
Theorem | unennn 12363 |
The union of two disjoint countably infinite sets is countably infinite.
(Contributed by Jim Kingdon, 13-May-2022.)
|
⊢ ((𝐴 ≈ ℕ ∧ 𝐵 ≈ ℕ ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐴 ∪ 𝐵) ≈ ℕ) |
|
Theorem | znnen 12364 |
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.)
|
⊢ ℤ ≈ ℕ |
|
Theorem | ennnfonelemdc 12365* |
Lemma for ennnfone 12391. A direct consequence of fidcenumlemrk 6943.
(Contributed by Jim Kingdon, 15-Jul-2023.)
|
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)
& ⊢ (𝜑 → 𝐹:ω–onto→𝐴)
& ⊢ (𝜑 → 𝑃 ∈ ω)
⇒ ⊢ (𝜑 → DECID (𝐹‘𝑃) ∈ (𝐹 “ 𝑃)) |
|
Theorem | ennnfonelemk 12366* |
Lemma for ennnfone 12391. (Contributed by Jim Kingdon, 15-Jul-2023.)
|
⊢ (𝜑 → 𝐹:ω–onto→𝐴)
& ⊢ (𝜑 → 𝐾 ∈ ω) & ⊢ (𝜑 → 𝑁 ∈ ω) & ⊢ (𝜑 → ∀𝑗 ∈ suc 𝑁(𝐹‘𝐾) ≠ (𝐹‘𝑗)) ⇒ ⊢ (𝜑 → 𝑁 ∈ 𝐾) |
|
Theorem | ennnfonelemj0 12367* |
Lemma for ennnfone 12391. 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 𝑔 ∈
ω}) |
|
Theorem | ennnfonelemjn 12368* |
Lemma for ennnfone 12391. 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))) → (𝐽‘𝑓) ∈
ω) |
|
Theorem | ennnfonelemg 12369* |
Lemma for ennnfone 12391. 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 𝑔 ∈
ω}) |
|
Theorem | ennnfonelemh 12370* |
Lemma for ennnfone 12391. (Contributed by Jim Kingdon, 8-Jul-2023.)
|
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)
& ⊢ (𝜑 → 𝐹:ω–onto→𝐴)
& ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))
& ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦
if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {〈dom 𝑥, (𝐹‘𝑦)〉}))) & ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) & ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1)))) & ⊢ 𝐻 = seq0(𝐺, 𝐽) ⇒ ⊢ (𝜑 → 𝐻:ℕ0⟶(𝐴 ↑pm
ω)) |
|
Theorem | ennnfonelem0 12371* |
Lemma for ennnfone 12391. Initial value. (Contributed by Jim
Kingdon,
15-Jul-2023.)
|
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)
& ⊢ (𝜑 → 𝐹:ω–onto→𝐴)
& ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))
& ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦
if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {〈dom 𝑥, (𝐹‘𝑦)〉}))) & ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) & ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1)))) & ⊢ 𝐻 = seq0(𝐺, 𝐽) ⇒ ⊢ (𝜑 → (𝐻‘0) = ∅) |
|
Theorem | ennnfonelemp1 12372* |
Lemma for ennnfone 12391. 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 (𝐻‘𝑃), (𝐹‘(◡𝑁‘𝑃))〉}))) |
|
Theorem | ennnfonelem1 12373* |
Lemma for ennnfone 12391. Second value. (Contributed by Jim
Kingdon,
19-Jul-2023.)
|
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)
& ⊢ (𝜑 → 𝐹:ω–onto→𝐴)
& ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))
& ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦
if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {〈dom 𝑥, (𝐹‘𝑦)〉}))) & ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) & ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1)))) & ⊢ 𝐻 = seq0(𝐺, 𝐽) ⇒ ⊢ (𝜑 → (𝐻‘1) = {〈∅, (𝐹‘∅)〉}) |
|
Theorem | ennnfonelemom 12374* |
Lemma for ennnfone 12391. 𝐻 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 (𝐻‘𝑃) ∈ ω) |
|
Theorem | ennnfonelemhdmp1 12375* |
Lemma for ennnfone 12391. 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 (𝐻‘𝑃)) |
|
Theorem | ennnfonelemss 12376* |
Lemma for ennnfone 12391. 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))) |
|
Theorem | ennnfoneleminc 12377* |
Lemma for ennnfone 12391. 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) & ⊢ (𝜑 → 𝑃 ≤ 𝑄) ⇒ ⊢ (𝜑 → (𝐻‘𝑃) ⊆ (𝐻‘𝑄)) |
|
Theorem | ennnfonelemkh 12378* |
Lemma for ennnfone 12391. 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 (𝐻‘𝑃) ⊆ (◡𝑁‘𝑃)) |
|
Theorem | ennnfonelemhf1o 12379* |
Lemma for ennnfone 12391. 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→(𝐹 “ (◡𝑁‘𝑃))) |
|
Theorem | ennnfonelemex 12380* |
Lemma for ennnfone 12391. 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 (𝐻‘𝑖)) |
|
Theorem | ennnfonelemhom 12381* |
Lemma for ennnfone 12391. 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 (𝐻‘𝑖)) |
|
Theorem | ennnfonelemrnh 12382* |
Lemma for ennnfone 12391. A consequence of ennnfonelemss 12376.
(Contributed by Jim Kingdon, 16-Jul-2023.)
|
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)
& ⊢ (𝜑 → 𝐹:ω–onto→𝐴)
& ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))
& ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦
if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {〈dom 𝑥, (𝐹‘𝑦)〉}))) & ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) & ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1)))) & ⊢ 𝐻 = seq0(𝐺, 𝐽)
& ⊢ (𝜑 → 𝑋 ∈ ran 𝐻)
& ⊢ (𝜑 → 𝑌 ∈ ran 𝐻) ⇒ ⊢ (𝜑 → (𝑋 ⊆ 𝑌 ∨ 𝑌 ⊆ 𝑋)) |
|
Theorem | ennnfonelemfun 12383* |
Lemma for ennnfone 12391. 𝐿 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 𝐿) |
|
Theorem | ennnfonelemf1 12384* |
Lemma for ennnfone 12391. 𝐿 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→𝐴) |
|
Theorem | ennnfonelemrn 12385* |
Lemma for ennnfone 12391. 𝐿 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 𝐿 = 𝐴) |
|
Theorem | ennnfonelemdm 12386* |
Lemma for ennnfone 12391. 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 𝐿 = ω) |
|
Theorem | ennnfonelemen 12387* |
Lemma for ennnfone 12391. The result. (Contributed by Jim Kingdon,
16-Jul-2023.)
|
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)
& ⊢ (𝜑 → 𝐹:ω–onto→𝐴)
& ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))
& ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦
if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {〈dom 𝑥, (𝐹‘𝑦)〉}))) & ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) & ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1)))) & ⊢ 𝐻 = seq0(𝐺, 𝐽)
& ⊢ 𝐿 = ∪
𝑖 ∈
ℕ0 (𝐻‘𝑖) ⇒ ⊢ (𝜑 → 𝐴 ≈ ℕ) |
|
Theorem | ennnfonelemnn0 12388* |
Lemma for ennnfone 12391. A version of ennnfonelemen 12387 expressed in
terms of ℕ0 instead of ω. (Contributed by Jim Kingdon,
27-Oct-2022.)
|
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)
& ⊢ (𝜑 → 𝐹:ℕ0–onto→𝐴)
& ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 ∃𝑘 ∈ ℕ0
∀𝑗 ∈
(0...𝑛)(𝐹‘𝑘) ≠ (𝐹‘𝑗))
& ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ⇒ ⊢ (𝜑 → 𝐴 ≈ ℕ) |
|
Theorem | ennnfonelemr 12389* |
Lemma for ennnfone 12391. The interesting direction, expressed in
deduction form. (Contributed by Jim Kingdon, 27-Oct-2022.)
|
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)
& ⊢ (𝜑 → 𝐹:ℕ0–onto→𝐴)
& ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 ∃𝑘 ∈ ℕ0
∀𝑗 ∈
(0...𝑛)(𝐹‘𝑘) ≠ (𝐹‘𝑗)) ⇒ ⊢ (𝜑 → 𝐴 ≈ ℕ) |
|
Theorem | ennnfonelemim 12390* |
Lemma for ennnfone 12391. The trivial direction. (Contributed by
Jim
Kingdon, 27-Oct-2022.)
|
⊢ (𝐴 ≈ ℕ → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑓(𝑓:ℕ0–onto→𝐴 ∧ ∀𝑛 ∈ ℕ0 ∃𝑘 ∈ ℕ0
∀𝑗 ∈
(0...𝑛)(𝑓‘𝑘) ≠ (𝑓‘𝑗)))) |
|
Theorem | ennnfone 12391* |
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 𝑓:ℕ0–onto→𝐴 part, as seen in theorems
like ctm 7098), 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 𝑥 = 𝑦 ∧ ∃𝑓(𝑓:ℕ0–onto→𝐴 ∧ ∀𝑛 ∈ ℕ0 ∃𝑘 ∈ ℕ0
∀𝑗 ∈
(0...𝑛)(𝑓‘𝑘) ≠ (𝑓‘𝑗)))) |
|
Theorem | exmidunben 12392* |
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) |
|
Theorem | ctinfomlemom 12393* |
Lemma for ctinfom 12394. Converting between ω and ℕ0.
(Contributed by Jim Kingdon, 10-Aug-2023.)
|
⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) & ⊢ 𝐺 = (𝐹 ∘ ◡𝑁)
& ⊢ (𝜑 → 𝐹:ω–onto→𝐴)
& ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝐹‘𝑘) ∈ (𝐹 “ 𝑛)) ⇒ ⊢ (𝜑 → (𝐺:ℕ0–onto→𝐴 ∧ ∀𝑚 ∈ ℕ0 ∃𝑗 ∈ ℕ0
∀𝑖 ∈
(0...𝑚)(𝐺‘𝑗) ≠ (𝐺‘𝑖))) |
|
Theorem | ctinfom 12394* |
A condition for a set being countably infinite. Restates ennnfone 12391 in
terms of ω and function image. Like ennnfone 12391 the condition can
be summarized as 𝐴 being countable, infinite, and
having decidable
equality. (Contributed by Jim Kingdon, 7-Aug-2023.)
|
⊢ (𝐴 ≈ ℕ ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑓(𝑓:ω–onto→𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓‘𝑘) ∈ (𝑓 “ 𝑛)))) |
|
Theorem | inffinp1 12395* |
An infinite set contains an element not contained in a given finite
subset. (Contributed by Jim Kingdon, 7-Aug-2023.)
|
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)
& ⊢ (𝜑 → ω ≼ 𝐴)
& ⊢ (𝜑 → 𝐵 ⊆ 𝐴)
& ⊢ (𝜑 → 𝐵 ∈ Fin) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵) |
|
Theorem | ctinf 12396* |
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→𝐴 ∧ ω ≼ 𝐴)) |
|
Theorem | qnnen 12397 |
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.)
|
⊢ ℚ ≈ ℕ |
|
Theorem | enctlem 12398* |
Lemma for enct 12399. One direction of the biconditional.
(Contributed by
Jim Kingdon, 23-Dec-2023.)
|
⊢ (𝐴 ≈ 𝐵 → (∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) →
∃𝑔 𝑔:ω–onto→(𝐵 ⊔ 1o))) |
|
Theorem | enct 12399* |
Countability is invariant relative to equinumerosity. (Contributed by
Jim Kingdon, 23-Dec-2023.)
|
⊢ (𝐴 ≈ 𝐵 → (∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) ↔
∃𝑔 𝑔:ω–onto→(𝐵 ⊔ 1o))) |
|
Theorem | ctiunctlemu1st 12400* |
Lemma for ctiunct 12406. (Contributed by Jim Kingdon, 28-Oct-2023.)
|
⊢ (𝜑 → 𝑆 ⊆ ω) & ⊢ (𝜑 → ∀𝑛 ∈ ω
DECID 𝑛
∈ 𝑆) & ⊢ (𝜑 → 𝐹:𝑆–onto→𝐴)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑇 ⊆ ω) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑇)
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺:𝑇–onto→𝐵)
& ⊢ (𝜑 → 𝐽:ω–1-1-onto→(ω × ω)) & ⊢ 𝑈 = {𝑧 ∈ ω ∣ ((1st
‘(𝐽‘𝑧)) ∈ 𝑆 ∧ (2nd ‘(𝐽‘𝑧)) ∈ ⦋(𝐹‘(1st ‘(𝐽‘𝑧))) / 𝑥⦌𝑇)} & ⊢ (𝜑 → 𝑁 ∈ 𝑈) ⇒ ⊢ (𝜑 → (1st ‘(𝐽‘𝑁)) ∈ 𝑆) |