Theorem List for Intuitionistic Logic Explorer - 12301-12400 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | pcndvds2 12301 |
The remainder after dividing out all factors of 𝑃 is not divisible
by 𝑃. (Contributed by Mario Carneiro,
23-Feb-2014.)
|
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → ¬ 𝑃 ∥ (𝑁 / (𝑃↑(𝑃 pCnt 𝑁)))) |
|
Theorem | pcdvdsb 12302 |
𝑃↑𝐴 divides 𝑁 if and only if 𝐴 is at
most the count of
𝑃. (Contributed by Mario Carneiro,
3-Oct-2014.)
|
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0) → (𝐴 ≤ (𝑃 pCnt 𝑁) ↔ (𝑃↑𝐴) ∥ 𝑁)) |
|
Theorem | pcelnn 12303 |
There are a positive number of powers of a prime 𝑃 in 𝑁 iff
𝑃
divides 𝑁. (Contributed by Mario Carneiro,
23-Feb-2014.)
|
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → ((𝑃 pCnt 𝑁) ∈ ℕ ↔ 𝑃 ∥ 𝑁)) |
|
Theorem | pceq0 12304 |
There are zero powers of a prime 𝑃 in 𝑁 iff 𝑃 does
not divide
𝑁. (Contributed by Mario Carneiro,
23-Feb-2014.)
|
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → ((𝑃 pCnt 𝑁) = 0 ↔ ¬ 𝑃 ∥ 𝑁)) |
|
Theorem | pcidlem 12305 |
The prime count of a prime power. (Contributed by Mario Carneiro,
12-Mar-2014.)
|
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0) → (𝑃 pCnt (𝑃↑𝐴)) = 𝐴) |
|
Theorem | pcid 12306 |
The prime count of a prime power. (Contributed by Mario Carneiro,
9-Sep-2014.)
|
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (𝑃 pCnt (𝑃↑𝐴)) = 𝐴) |
|
Theorem | pcneg 12307 |
The prime count of a negative number. (Contributed by Mario Carneiro,
13-Mar-2014.)
|
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℚ) → (𝑃 pCnt -𝐴) = (𝑃 pCnt 𝐴)) |
|
Theorem | pcabs 12308 |
The prime count of an absolute value. (Contributed by Mario Carneiro,
13-Mar-2014.)
|
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℚ) → (𝑃 pCnt (abs‘𝐴)) = (𝑃 pCnt 𝐴)) |
|
Theorem | pcdvdstr 12309 |
The prime count increases under the divisibility relation. (Contributed
by Mario Carneiro, 13-Mar-2014.)
|
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵)) |
|
Theorem | pcgcd1 12310 |
The prime count of a GCD is the minimum of the prime counts of the
arguments. (Contributed by Mario Carneiro, 3-Oct-2014.)
|
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵)) → (𝑃 pCnt (𝐴 gcd 𝐵)) = (𝑃 pCnt 𝐴)) |
|
Theorem | pcgcd 12311 |
The prime count of a GCD is the minimum of the prime counts of the
arguments. (Contributed by Mario Carneiro, 3-Oct-2014.)
|
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑃 pCnt (𝐴 gcd 𝐵)) = if((𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵), (𝑃 pCnt 𝐴), (𝑃 pCnt 𝐵))) |
|
Theorem | pc2dvds 12312* |
A characterization of divisibility in terms of prime count.
(Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by Mario
Carneiro, 3-Oct-2014.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 ∥ 𝐵 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵))) |
|
Theorem | pc11 12313* |
The prime count function, viewed as a function from ℕ to
(ℕ ↑𝑚 ℙ), is
one-to-one. (Contributed by Mario Carneiro,
23-Feb-2014.)
|
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0)
→ (𝐴 = 𝐵 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) = (𝑝 pCnt 𝐵))) |
|
Theorem | pcz 12314* |
The prime count function can be used as an indicator that a given
rational number is an integer. (Contributed by Mario Carneiro,
23-Feb-2014.)
|
⊢ (𝐴 ∈ ℚ → (𝐴 ∈ ℤ ↔ ∀𝑝 ∈ ℙ 0 ≤ (𝑝 pCnt 𝐴))) |
|
Theorem | pcprmpw2 12315* |
Self-referential expression for a prime power. (Contributed by Mario
Carneiro, 16-Jan-2015.)
|
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) → (∃𝑛 ∈ ℕ0
𝐴 ∥ (𝑃↑𝑛) ↔ 𝐴 = (𝑃↑(𝑃 pCnt 𝐴)))) |
|
Theorem | pcprmpw 12316* |
Self-referential expression for a prime power. (Contributed by Mario
Carneiro, 16-Jan-2015.)
|
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) → (∃𝑛 ∈ ℕ0
𝐴 = (𝑃↑𝑛) ↔ 𝐴 = (𝑃↑(𝑃 pCnt 𝐴)))) |
|
Theorem | dvdsprmpweq 12317* |
If a positive integer divides a prime power, it is a prime power.
(Contributed by AV, 25-Jul-2021.)
|
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (𝐴 ∥ (𝑃↑𝑁) → ∃𝑛 ∈ ℕ0 𝐴 = (𝑃↑𝑛))) |
|
Theorem | dvdsprmpweqnn 12318* |
If an integer greater than 1 divides a prime power, it is a (proper)
prime power. (Contributed by AV, 13-Aug-2021.)
|
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ (ℤ≥‘2)
∧ 𝑁 ∈
ℕ0) → (𝐴 ∥ (𝑃↑𝑁) → ∃𝑛 ∈ ℕ 𝐴 = (𝑃↑𝑛))) |
|
Theorem | dvdsprmpweqle 12319* |
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 12320 |
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 12321 |
Lemma for pcadd 12322. 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 12322 |
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 12323 |
Closure for the prime power map. (Contributed by Mario Carneiro,
12-Mar-2014.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑𝐴), 1)) & ⊢ (𝜑 → ∀𝑛 ∈ ℙ 𝐴 ∈
ℕ0) ⇒ ⊢ (𝜑 → (𝐹:ℕ⟶ℕ ∧ seq1(
· , 𝐹):ℕ⟶ℕ)) |
|
Theorem | pcmpt 12324* |
Construct a function with given prime count characteristics.
(Contributed by Mario Carneiro, 12-Mar-2014.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑𝐴), 1)) & ⊢ (𝜑 → ∀𝑛 ∈ ℙ 𝐴 ∈
ℕ0)
& ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝑛 = 𝑃 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝑃 pCnt (seq1( · , 𝐹)‘𝑁)) = if(𝑃 ≤ 𝑁, 𝐵, 0)) |
|
Theorem | pcmpt2 12325* |
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 12326 |
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 12327* |
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 12328* |
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 12329 |
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 12330 |
Lemma for pcfac 12331. (Contributed by Mario Carneiro,
20-May-2014.)
|
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈
(ℤ≥‘𝑁) ∧ 𝑃 ∈ ℙ) →
(⌊‘(𝑁 / (𝑃↑𝑀))) = 0) |
|
Theorem | pcfac 12331* |
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 12332* |
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 12333 |
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 12334 |
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 12335* |
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 12336 |
A relation involving divisibility by a prime power. (Contributed by
Mario Carneiro, 2-Mar-2014.)
|
⊢ (((𝐾 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) ∧ (𝐷 ∥ (𝐾 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝐾 · (𝑃↑(𝑁 − 1))))) → (𝑃↑𝑁) ∥ 𝐷) |
|
Theorem | pockthlem 12337 |
Lemma for pockthg 12338. (Contributed by Mario Carneiro,
2-Mar-2014.)
|
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐵 < 𝐴)
& ⊢ (𝜑 → 𝑁 = ((𝐴 · 𝐵) + 1)) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑃 ∥ 𝑁)
& ⊢ (𝜑 → 𝑄 ∈ ℙ) & ⊢ (𝜑 → (𝑄 pCnt 𝐴) ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℤ) & ⊢ (𝜑 → ((𝐶↑(𝑁 − 1)) mod 𝑁) = 1) & ⊢ (𝜑 → (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁) = 1) ⇒ ⊢ (𝜑 → (𝑄 pCnt 𝐴) ≤ (𝑄 pCnt (𝑃 − 1))) |
|
Theorem | pockthg 12338* |
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 12339 |
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 12338 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 12340* |
Lemma for infpn 12342. 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 12341* |
Lemma for infpn 12342. For any positive integer 𝑁, there
exists a
prime number 𝑗 greater than 𝑁. (Contributed by NM,
5-May-2005.)
|
⊢ 𝐾 = ((!‘𝑁) + 1) ⇒ ⊢ (𝑁 ∈ ℕ → ∃𝑗 ∈ ℕ (𝑁 < 𝑗 ∧ ∀𝑘 ∈ ℕ ((𝑗 / 𝑘) ∈ ℕ → (𝑘 = 1 ∨ 𝑘 = 𝑗)))) |
|
Theorem | infpn 12342* |
There exist infinitely many prime numbers: for any positive integer
𝑁, there exists a prime number 𝑗 greater
than 𝑁. (See
infpn2 12440 for the equinumerosity version.)
(Contributed by NM,
1-Jun-2006.)
|
⊢ (𝑁 ∈ ℕ → ∃𝑗 ∈ ℕ (𝑁 < 𝑗 ∧ ∀𝑘 ∈ ℕ ((𝑗 / 𝑘) ∈ ℕ → (𝑘 = 1 ∨ 𝑘 = 𝑗)))) |
|
Theorem | prmunb 12343* |
The primes are unbounded. (Contributed by Paul Chapman,
28-Nov-2012.)
|
⊢ (𝑁 ∈ ℕ → ∃𝑝 ∈ ℙ 𝑁 < 𝑝) |
|
5.2.11 Fundamental theorem of
arithmetic
|
|
Theorem | 1arithlem1 12344* |
Lemma for 1arith 12348. (Contributed by Mario Carneiro,
30-May-2014.)
|
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛))) ⇒ ⊢ (𝑁 ∈ ℕ → (𝑀‘𝑁) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑁))) |
|
Theorem | 1arithlem2 12345* |
Lemma for 1arith 12348. (Contributed by Mario Carneiro,
30-May-2014.)
|
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛))) ⇒ ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → ((𝑀‘𝑁)‘𝑃) = (𝑃 pCnt 𝑁)) |
|
Theorem | 1arithlem3 12346* |
Lemma for 1arith 12348. (Contributed by Mario Carneiro,
30-May-2014.)
|
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛))) ⇒ ⊢ (𝑁 ∈ ℕ → (𝑀‘𝑁):ℙ⟶ℕ0) |
|
Theorem | 1arithlem4 12347* |
Lemma for 1arith 12348. (Contributed by Mario Carneiro,
30-May-2014.)
|
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛))) & ⊢ 𝐺 = (𝑦 ∈ ℕ ↦ if(𝑦 ∈ ℙ, (𝑦↑(𝐹‘𝑦)), 1)) & ⊢ (𝜑 → 𝐹:ℙ⟶ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ ((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑁 ≤ 𝑞)) → (𝐹‘𝑞) = 0) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℕ 𝐹 = (𝑀‘𝑥)) |
|
Theorem | 1arith 12348* |
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 12349* |
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 12350 |
Extend class notation with the set of gaussian integers.
|
class ℤ[i] |
|
Definition | df-gz 12351 |
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 12352 |
Elementhood in the gaussian integers. (Contributed by Mario Carneiro,
14-Jul-2014.)
|
⊢ (𝐴 ∈ ℤ[i] ↔ (𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
ℤ ∧ (ℑ‘𝐴) ∈ ℤ)) |
|
Theorem | gzcn 12353 |
A gaussian integer is a complex number. (Contributed by Mario Carneiro,
14-Jul-2014.)
|
⊢ (𝐴 ∈ ℤ[i] → 𝐴 ∈ ℂ) |
|
Theorem | zgz 12354 |
An integer is a gaussian integer. (Contributed by Mario Carneiro,
14-Jul-2014.)
|
⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℤ[i]) |
|
Theorem | igz 12355 |
i is a gaussian integer. (Contributed by Mario
Carneiro,
14-Jul-2014.)
|
⊢ i ∈ ℤ[i] |
|
Theorem | gznegcl 12356 |
The gaussian integers are closed under negation. (Contributed by Mario
Carneiro, 14-Jul-2014.)
|
⊢ (𝐴 ∈ ℤ[i] → -𝐴 ∈
ℤ[i]) |
|
Theorem | gzcjcl 12357 |
The gaussian integers are closed under conjugation. (Contributed by Mario
Carneiro, 14-Jul-2014.)
|
⊢ (𝐴 ∈ ℤ[i] →
(∗‘𝐴) ∈
ℤ[i]) |
|
Theorem | gzaddcl 12358 |
The gaussian integers are closed under addition. (Contributed by Mario
Carneiro, 14-Jul-2014.)
|
⊢ ((𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i]) → (𝐴 + 𝐵) ∈ ℤ[i]) |
|
Theorem | gzmulcl 12359 |
The gaussian integers are closed under multiplication. (Contributed by
Mario Carneiro, 14-Jul-2014.)
|
⊢ ((𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i]) → (𝐴 · 𝐵) ∈ ℤ[i]) |
|
Theorem | gzreim 12360 |
Construct a gaussian integer from real and imaginary parts. (Contributed
by Mario Carneiro, 16-Jul-2014.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 + (i · 𝐵)) ∈ ℤ[i]) |
|
Theorem | gzsubcl 12361 |
The gaussian integers are closed under subtraction. (Contributed by Mario
Carneiro, 14-Jul-2014.)
|
⊢ ((𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i]) → (𝐴 − 𝐵) ∈ ℤ[i]) |
|
Theorem | gzabssqcl 12362 |
The squared norm of a gaussian integer is an integer. (Contributed by
Mario Carneiro, 16-Jul-2014.)
|
⊢ (𝐴 ∈ ℤ[i] → ((abs‘𝐴)↑2) ∈
ℕ0) |
|
Theorem | 4sqlem5 12363 |
Lemma for 4sq (not yet proved here). (Contributed by Mario Carneiro,
15-Jul-2014.)
|
⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) ⇒ ⊢ (𝜑 → (𝐵 ∈ ℤ ∧ ((𝐴 − 𝐵) / 𝑀) ∈ ℤ)) |
|
Theorem | 4sqlem6 12364 |
Lemma for 4sq (not yet proved here) . (Contributed by Mario Carneiro,
15-Jul-2014.)
|
⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) ⇒ ⊢ (𝜑 → (-(𝑀 / 2) ≤ 𝐵 ∧ 𝐵 < (𝑀 / 2))) |
|
Theorem | 4sqlem7 12365 |
Lemma for 4sq (not yet proved here) . (Contributed by Mario Carneiro,
15-Jul-2014.)
|
⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) ⇒ ⊢ (𝜑 → (𝐵↑2) ≤ (((𝑀↑2) / 2) / 2)) |
|
Theorem | 4sqlem8 12366 |
Lemma for 4sq (not yet proved here) . (Contributed by Mario Carneiro,
15-Jul-2014.)
|
⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) ⇒ ⊢ (𝜑 → 𝑀 ∥ ((𝐴↑2) − (𝐵↑2))) |
|
Theorem | 4sqlem9 12367 |
Lemma for 4sq (not yet proved here) . (Contributed by Mario Carneiro,
15-Jul-2014.)
|
⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) & ⊢ ((𝜑 ∧ 𝜓) → (𝐵↑2) = 0)
⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝑀↑2) ∥ (𝐴↑2)) |
|
Theorem | 4sqlem10 12368 |
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 12369* |
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 12370* |
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 12371* |
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 12372* |
Lemma for 4sqlem4 12373. (Contributed by Mario Carneiro,
14-Jul-2014.)
|
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))} ⇒ ⊢ ((𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i]) →
(((abs‘𝐴)↑2) +
((abs‘𝐵)↑2))
∈ 𝑆) |
|
Theorem | 4sqlem4 12373* |
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 12374* |
Lemma for mul4sq 12375: 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 12375* |
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 12374. (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 12376 |
There are as many odd positive integers as there are positive integers.
(Contributed by Jim Kingdon, 11-May-2022.)
|
⊢ {𝑧 ∈ ℕ ∣ ¬ 2 ∥
𝑧} ≈
ℕ |
|
Theorem | evenennn 12377 |
There are as many even positive integers as there are positive integers.
(Contributed by Jim Kingdon, 12-May-2022.)
|
⊢ {𝑧 ∈ ℕ ∣ 2 ∥ 𝑧} ≈
ℕ |
|
Theorem | xpnnen 12378 |
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 12379 |
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 12380 |
The cartesian product of two sets dominated by ω
is dominated by
ω. (Contributed by Thierry Arnoux,
24-Sep-2017.)
|
⊢ ((𝐴 ≼ ω ∧ 𝐵 ≼ ω) → (𝐴 × 𝐵) ≼ ω) |
|
Theorem | unennn 12381 |
The union of two disjoint countably infinite sets is countably infinite.
(Contributed by Jim Kingdon, 13-May-2022.)
|
⊢ ((𝐴 ≈ ℕ ∧ 𝐵 ≈ ℕ ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐴 ∪ 𝐵) ≈ ℕ) |
|
Theorem | znnen 12382 |
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 12383* |
Lemma for ennnfone 12409. A direct consequence of fidcenumlemrk 6947.
(Contributed by Jim Kingdon, 15-Jul-2023.)
|
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)
& ⊢ (𝜑 → 𝐹:ω–onto→𝐴)
& ⊢ (𝜑 → 𝑃 ∈ ω)
⇒ ⊢ (𝜑 → DECID (𝐹‘𝑃) ∈ (𝐹 “ 𝑃)) |
|
Theorem | ennnfonelemk 12384* |
Lemma for ennnfone 12409. (Contributed by Jim Kingdon, 15-Jul-2023.)
|
⊢ (𝜑 → 𝐹:ω–onto→𝐴)
& ⊢ (𝜑 → 𝐾 ∈ ω) & ⊢ (𝜑 → 𝑁 ∈ ω) & ⊢ (𝜑 → ∀𝑗 ∈ suc 𝑁(𝐹‘𝐾) ≠ (𝐹‘𝑗)) ⇒ ⊢ (𝜑 → 𝑁 ∈ 𝐾) |
|
Theorem | ennnfonelemj0 12385* |
Lemma for ennnfone 12409. 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 12386* |
Lemma for ennnfone 12409. 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 12387* |
Lemma for ennnfone 12409. 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 12388* |
Lemma for ennnfone 12409. (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 12389* |
Lemma for ennnfone 12409. 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 12390* |
Lemma for ennnfone 12409. 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 12391* |
Lemma for ennnfone 12409. 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 12392* |
Lemma for ennnfone 12409. 𝐻 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 12393* |
Lemma for ennnfone 12409. 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 12394* |
Lemma for ennnfone 12409. 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 12395* |
Lemma for ennnfone 12409. 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 12396* |
Lemma for ennnfone 12409. 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 12397* |
Lemma for ennnfone 12409. 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 12398* |
Lemma for ennnfone 12409. 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 12399* |
Lemma for ennnfone 12409. 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 12400* |
Lemma for ennnfone 12409. A consequence of ennnfonelemss 12394.
(Contributed by Jim Kingdon, 16-Jul-2023.)
|
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)
& ⊢ (𝜑 → 𝐹:ω–onto→𝐴)
& ⊢ (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹‘𝑘) ≠ (𝐹‘𝑗))
& ⊢ 𝐺 = (𝑥 ∈ (𝐴 ↑pm ω), 𝑦 ∈ ω ↦
if((𝐹‘𝑦) ∈ (𝐹 “ 𝑦), 𝑥, (𝑥 ∪ {〈dom 𝑥, (𝐹‘𝑦)〉}))) & ⊢ 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) & ⊢ 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (◡𝑁‘(𝑥 − 1)))) & ⊢ 𝐻 = seq0(𝐺, 𝐽)
& ⊢ (𝜑 → 𝑋 ∈ ran 𝐻)
& ⊢ (𝜑 → 𝑌 ∈ ran 𝐻) ⇒ ⊢ (𝜑 → (𝑋 ⊆ 𝑌 ∨ 𝑌 ⊆ 𝑋)) |