Theorem List for Intuitionistic Logic Explorer - 12201-12300 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | pcprendvds 12201* |
Non-divisibility property of the prime power pre-function.
(Contributed by Mario Carneiro, 23-Feb-2014.)
|
⊢ 𝐴 = {𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑁}
& ⊢ 𝑆 = sup(𝐴, ℝ, < )
⇒ ⊢ ((𝑃 ∈ (ℤ≥‘2)
∧ (𝑁 ∈ ℤ
∧ 𝑁 ≠ 0)) →
¬ (𝑃↑(𝑆 + 1)) ∥ 𝑁) |
|
Theorem | pcprendvds2 12202* |
Non-divisibility property of the prime power pre-function.
(Contributed by Mario Carneiro, 23-Feb-2014.)
|
⊢ 𝐴 = {𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑁}
& ⊢ 𝑆 = sup(𝐴, ℝ, < )
⇒ ⊢ ((𝑃 ∈ (ℤ≥‘2)
∧ (𝑁 ∈ ℤ
∧ 𝑁 ≠ 0)) →
¬ 𝑃 ∥ (𝑁 / (𝑃↑𝑆))) |
|
Theorem | pcpre1 12203* |
Value of the prime power pre-function at 1. (Contributed by Mario
Carneiro, 23-Feb-2014.) (Revised by Mario Carneiro, 26-Apr-2016.)
|
⊢ 𝐴 = {𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑁}
& ⊢ 𝑆 = sup(𝐴, ℝ, < )
⇒ ⊢ ((𝑃 ∈ (ℤ≥‘2)
∧ 𝑁 = 1) → 𝑆 = 0) |
|
Theorem | pcpremul 12204* |
Multiplicative property of the prime count pre-function. Note that the
primality of 𝑃 is essential for this property;
(4 pCnt 2) = 0
but (4 pCnt (2 · 2)) = 1 ≠ 2 · (4 pCnt
2) = 0. Since
this is needed to show uniqueness for the real prime count function
(over ℚ), we don't bother to define it off
the primes.
(Contributed by Mario Carneiro, 23-Feb-2014.)
|
⊢ 𝑆 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑀}, ℝ, < ) & ⊢ 𝑇 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑁}, ℝ, < ) & ⊢ 𝑈 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ (𝑀 · 𝑁)}, ℝ, <
) ⇒ ⊢ ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑆 + 𝑇) = 𝑈) |
|
Theorem | pceulem 12205* |
Lemma for pceu 12206. (Contributed by Mario Carneiro,
23-Feb-2014.)
|
⊢ 𝑆 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) & ⊢ 𝑇 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < ) & ⊢ 𝑈 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < ) & ⊢ 𝑉 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑡}, ℝ, < ) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑁 ≠ 0) & ⊢ (𝜑 → (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) & ⊢ (𝜑 → 𝑁 = (𝑥 / 𝑦))
& ⊢ (𝜑 → (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℕ)) & ⊢ (𝜑 → 𝑁 = (𝑠 / 𝑡)) ⇒ ⊢ (𝜑 → (𝑆 − 𝑇) = (𝑈 − 𝑉)) |
|
Theorem | pceu 12206* |
Uniqueness for the prime power function. (Contributed by Mario
Carneiro, 23-Feb-2014.)
|
⊢ 𝑆 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) & ⊢ 𝑇 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < )
⇒ ⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℚ ∧ 𝑁 ≠ 0)) → ∃!𝑧∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇))) |
|
Theorem | pcval 12207* |
The value of the prime power function. (Contributed by Mario Carneiro,
23-Feb-2014.) (Revised by Mario Carneiro, 3-Oct-2014.)
|
⊢ 𝑆 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) & ⊢ 𝑇 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < )
⇒ ⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℚ ∧ 𝑁 ≠ 0)) → (𝑃 pCnt 𝑁) = (℩𝑧∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇)))) |
|
Theorem | pczpre 12208* |
Connect the prime count pre-function to the actual prime count function,
when restricted to the integers. (Contributed by Mario Carneiro,
23-Feb-2014.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)
|
⊢ 𝑆 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑁}, ℝ, < )
⇒ ⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃 pCnt 𝑁) = 𝑆) |
|
Theorem | pczcl 12209 |
Closure of the prime power function. (Contributed by Mario Carneiro,
23-Feb-2014.)
|
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃 pCnt 𝑁) ∈
ℕ0) |
|
Theorem | pccl 12210 |
Closure of the prime power function. (Contributed by Mario Carneiro,
23-Feb-2014.)
|
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → (𝑃 pCnt 𝑁) ∈
ℕ0) |
|
Theorem | pccld 12211 |
Closure of the prime power function. (Contributed by Mario Carneiro,
29-May-2016.)
|
⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑁 ∈ ℕ)
⇒ ⊢ (𝜑 → (𝑃 pCnt 𝑁) ∈
ℕ0) |
|
Theorem | pcmul 12212 |
Multiplication property of the prime power function. (Contributed by
Mario Carneiro, 23-Feb-2014.)
|
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝑃 pCnt (𝐴 · 𝐵)) = ((𝑃 pCnt 𝐴) + (𝑃 pCnt 𝐵))) |
|
Theorem | pcdiv 12213 |
Division property of the prime power function. (Contributed by Mario
Carneiro, 1-Mar-2014.)
|
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℕ) → (𝑃 pCnt (𝐴 / 𝐵)) = ((𝑃 pCnt 𝐴) − (𝑃 pCnt 𝐵))) |
|
Theorem | pcqmul 12214 |
Multiplication property of the prime power function. (Contributed by
Mario Carneiro, 9-Sep-2014.)
|
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → (𝑃 pCnt (𝐴 · 𝐵)) = ((𝑃 pCnt 𝐴) + (𝑃 pCnt 𝐵))) |
|
Theorem | pc0 12215 |
The value of the prime power function at zero. (Contributed by Mario
Carneiro, 3-Oct-2014.)
|
⊢ (𝑃 ∈ ℙ → (𝑃 pCnt 0) = +∞) |
|
Theorem | pc1 12216 |
Value of the prime count function at 1. (Contributed by Mario Carneiro,
23-Feb-2014.)
|
⊢ (𝑃 ∈ ℙ → (𝑃 pCnt 1) = 0) |
|
Theorem | pcqcl 12217 |
Closure of the general prime count function. (Contributed by Mario
Carneiro, 23-Feb-2014.)
|
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℚ ∧ 𝑁 ≠ 0)) → (𝑃 pCnt 𝑁) ∈ ℤ) |
|
Theorem | pcqdiv 12218 |
Division property of the prime power function. (Contributed by Mario
Carneiro, 10-Aug-2015.)
|
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → (𝑃 pCnt (𝐴 / 𝐵)) = ((𝑃 pCnt 𝐴) − (𝑃 pCnt 𝐵))) |
|
Theorem | pcrec 12219 |
Prime power of a reciprocal. (Contributed by Mario Carneiro,
10-Aug-2015.)
|
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) → (𝑃 pCnt (1 / 𝐴)) = -(𝑃 pCnt 𝐴)) |
|
Theorem | pcexp 12220 |
Prime power of an exponential. (Contributed by Mario Carneiro,
10-Aug-2015.)
|
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ 𝑁 ∈ ℤ) → (𝑃 pCnt (𝐴↑𝑁)) = (𝑁 · (𝑃 pCnt 𝐴))) |
|
Theorem | pcxnn0cl 12221 |
Extended nonnegative integer closure of the general prime count
function. (Contributed by Jim Kingdon, 13-Oct-2024.)
|
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (𝑃 pCnt 𝑁) ∈
ℕ0*) |
|
Theorem | pcxcl 12222 |
Extended real closure of the general prime count function. (Contributed
by Mario Carneiro, 3-Oct-2014.)
|
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℚ) → (𝑃 pCnt 𝑁) ∈
ℝ*) |
|
Theorem | pcge0 12223 |
The prime count of an integer is greater than or equal to zero.
(Contributed by Mario Carneiro, 3-Oct-2014.)
|
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → 0 ≤ (𝑃 pCnt 𝑁)) |
|
Theorem | pczdvds 12224 |
Defining property of the prime count function. (Contributed by Mario
Carneiro, 9-Sep-2014.)
|
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃↑(𝑃 pCnt 𝑁)) ∥ 𝑁) |
|
Theorem | pcdvds 12225 |
Defining property of the prime count function. (Contributed by Mario
Carneiro, 23-Feb-2014.)
|
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → (𝑃↑(𝑃 pCnt 𝑁)) ∥ 𝑁) |
|
Theorem | pczndvds 12226 |
Defining property of the prime count function. (Contributed by Mario
Carneiro, 3-Oct-2014.)
|
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ¬ (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ 𝑁) |
|
Theorem | pcndvds 12227 |
Defining property of the prime count function. (Contributed by Mario
Carneiro, 23-Feb-2014.)
|
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → ¬ (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ 𝑁) |
|
Theorem | pczndvds2 12228 |
The remainder after dividing out all factors of 𝑃 is not divisible
by 𝑃. (Contributed by Mario Carneiro,
9-Sep-2014.)
|
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ¬ 𝑃 ∥ (𝑁 / (𝑃↑(𝑃 pCnt 𝑁)))) |
|
Theorem | pcndvds2 12229 |
The remainder after dividing out all factors of 𝑃 is not divisible
by 𝑃. (Contributed by Mario Carneiro,
23-Feb-2014.)
|
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → ¬ 𝑃 ∥ (𝑁 / (𝑃↑(𝑃 pCnt 𝑁)))) |
|
Theorem | pcdvdsb 12230 |
𝑃↑𝐴 divides 𝑁 if and only if 𝐴 is at
most the count of
𝑃. (Contributed by Mario Carneiro,
3-Oct-2014.)
|
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0) → (𝐴 ≤ (𝑃 pCnt 𝑁) ↔ (𝑃↑𝐴) ∥ 𝑁)) |
|
Theorem | pcelnn 12231 |
There are a positive number of powers of a prime 𝑃 in 𝑁 iff
𝑃
divides 𝑁. (Contributed by Mario Carneiro,
23-Feb-2014.)
|
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → ((𝑃 pCnt 𝑁) ∈ ℕ ↔ 𝑃 ∥ 𝑁)) |
|
Theorem | pceq0 12232 |
There are zero powers of a prime 𝑃 in 𝑁 iff 𝑃 does
not divide
𝑁. (Contributed by Mario Carneiro,
23-Feb-2014.)
|
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → ((𝑃 pCnt 𝑁) = 0 ↔ ¬ 𝑃 ∥ 𝑁)) |
|
Theorem | pcidlem 12233 |
The prime count of a prime power. (Contributed by Mario Carneiro,
12-Mar-2014.)
|
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0) → (𝑃 pCnt (𝑃↑𝐴)) = 𝐴) |
|
Theorem | pcid 12234 |
The prime count of a prime power. (Contributed by Mario Carneiro,
9-Sep-2014.)
|
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (𝑃 pCnt (𝑃↑𝐴)) = 𝐴) |
|
Theorem | pcneg 12235 |
The prime count of a negative number. (Contributed by Mario Carneiro,
13-Mar-2014.)
|
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℚ) → (𝑃 pCnt -𝐴) = (𝑃 pCnt 𝐴)) |
|
Theorem | pcabs 12236 |
The prime count of an absolute value. (Contributed by Mario Carneiro,
13-Mar-2014.)
|
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℚ) → (𝑃 pCnt (abs‘𝐴)) = (𝑃 pCnt 𝐴)) |
|
Theorem | pcdvdstr 12237 |
The prime count increases under the divisibility relation. (Contributed
by Mario Carneiro, 13-Mar-2014.)
|
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵)) |
|
Theorem | pcgcd1 12238 |
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 12239 |
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 12240* |
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 12241* |
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 12242* |
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 12243* |
Self-referential expression for a prime power. (Contributed by Mario
Carneiro, 16-Jan-2015.)
|
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) → (∃𝑛 ∈ ℕ0
𝐴 ∥ (𝑃↑𝑛) ↔ 𝐴 = (𝑃↑(𝑃 pCnt 𝐴)))) |
|
Theorem | pcprmpw 12244* |
Self-referential expression for a prime power. (Contributed by Mario
Carneiro, 16-Jan-2015.)
|
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) → (∃𝑛 ∈ ℕ0
𝐴 = (𝑃↑𝑛) ↔ 𝐴 = (𝑃↑(𝑃 pCnt 𝐴)))) |
|
Theorem | dvdsprmpweq 12245* |
If a positive integer divides a prime power, it is a prime power.
(Contributed by AV, 25-Jul-2021.)
|
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (𝐴 ∥ (𝑃↑𝑁) → ∃𝑛 ∈ ℕ0 𝐴 = (𝑃↑𝑛))) |
|
Theorem | dvdsprmpweqnn 12246* |
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 12247* |
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 12248 |
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 12249 |
Lemma for pcadd 12250. 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 12250 |
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 12251 |
Closure for the prime power map. (Contributed by Mario Carneiro,
12-Mar-2014.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑𝐴), 1)) & ⊢ (𝜑 → ∀𝑛 ∈ ℙ 𝐴 ∈
ℕ0) ⇒ ⊢ (𝜑 → (𝐹:ℕ⟶ℕ ∧ seq1(
· , 𝐹):ℕ⟶ℕ)) |
|
Theorem | pcmpt 12252* |
Construct a function with given prime count characteristics.
(Contributed by Mario Carneiro, 12-Mar-2014.)
|
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑𝐴), 1)) & ⊢ (𝜑 → ∀𝑛 ∈ ℙ 𝐴 ∈
ℕ0)
& ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝑛 = 𝑃 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝑃 pCnt (seq1( · , 𝐹)‘𝑁)) = if(𝑃 ≤ 𝑁, 𝐵, 0)) |
|
Theorem | pcmpt2 12253* |
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 12254 |
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 12255* |
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 12256* |
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 12257 |
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 12258 |
Lemma for pcfac 12259. (Contributed by Mario Carneiro,
20-May-2014.)
|
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈
(ℤ≥‘𝑁) ∧ 𝑃 ∈ ℙ) →
(⌊‘(𝑁 / (𝑃↑𝑀))) = 0) |
|
Theorem | pcfac 12259* |
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 12260* |
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 12261 |
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 12262 |
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 12263* |
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 12264 |
A relation involving divisibility by a prime power. (Contributed by
Mario Carneiro, 2-Mar-2014.)
|
⊢ (((𝐾 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) ∧ (𝐷 ∥ (𝐾 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝐾 · (𝑃↑(𝑁 − 1))))) → (𝑃↑𝑁) ∥ 𝐷) |
|
Theorem | pockthlem 12265 |
Lemma for pockthg 12266. (Contributed by Mario Carneiro,
2-Mar-2014.)
|
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐵 < 𝐴)
& ⊢ (𝜑 → 𝑁 = ((𝐴 · 𝐵) + 1)) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑃 ∥ 𝑁)
& ⊢ (𝜑 → 𝑄 ∈ ℙ) & ⊢ (𝜑 → (𝑄 pCnt 𝐴) ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℤ) & ⊢ (𝜑 → ((𝐶↑(𝑁 − 1)) mod 𝑁) = 1) & ⊢ (𝜑 → (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁) = 1) ⇒ ⊢ (𝜑 → (𝑄 pCnt 𝐴) ≤ (𝑄 pCnt (𝑃 − 1))) |
|
Theorem | pockthg 12266* |
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 12267 |
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 12266 for a more general closed-form version.
(Contributed by Mario
Carneiro, 2-Mar-2014.)
|
⊢ 𝑃 ∈ ℙ & ⊢ 𝐺 ∈ ℕ & ⊢ 𝑀 = (𝐺 · 𝑃)
& ⊢ 𝑁 = (𝑀 + 1) & ⊢ 𝐷 ∈ ℕ & ⊢ 𝐸 ∈ ℕ & ⊢ 𝐴 ∈ ℕ & ⊢ 𝑀 = (𝐷 · (𝑃↑𝐸)) & ⊢ 𝐷 < (𝑃↑𝐸)
& ⊢ ((𝐴↑𝑀) mod 𝑁) = (1 mod 𝑁)
& ⊢ (((𝐴↑𝐺) − 1) gcd 𝑁) = 1 ⇒ ⊢ 𝑁 ∈ ℙ |
|
5.3 Cardinality of real and complex number
subsets
|
|
5.3.1 Countability of integers and
rationals
|
|
Theorem | oddennn 12268 |
There are as many odd positive integers as there are positive integers.
(Contributed by Jim Kingdon, 11-May-2022.)
|
⊢ {𝑧 ∈ ℕ ∣ ¬ 2 ∥
𝑧} ≈
ℕ |
|
Theorem | evenennn 12269 |
There are as many even positive integers as there are positive integers.
(Contributed by Jim Kingdon, 12-May-2022.)
|
⊢ {𝑧 ∈ ℕ ∣ 2 ∥ 𝑧} ≈
ℕ |
|
Theorem | xpnnen 12270 |
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 12271 |
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 12272 |
The cartesian product of two sets dominated by ω
is dominated by
ω. (Contributed by Thierry Arnoux,
24-Sep-2017.)
|
⊢ ((𝐴 ≼ ω ∧ 𝐵 ≼ ω) → (𝐴 × 𝐵) ≼ ω) |
|
Theorem | unennn 12273 |
The union of two disjoint countably infinite sets is countably infinite.
(Contributed by Jim Kingdon, 13-May-2022.)
|
⊢ ((𝐴 ≈ ℕ ∧ 𝐵 ≈ ℕ ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐴 ∪ 𝐵) ≈ ℕ) |
|
Theorem | znnen 12274 |
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 12275* |
Lemma for ennnfone 12301. A direct consequence of fidcenumlemrk 6910.
(Contributed by Jim Kingdon, 15-Jul-2023.)
|
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)
& ⊢ (𝜑 → 𝐹:ω–onto→𝐴)
& ⊢ (𝜑 → 𝑃 ∈ ω)
⇒ ⊢ (𝜑 → DECID (𝐹‘𝑃) ∈ (𝐹 “ 𝑃)) |
|
Theorem | ennnfonelemk 12276* |
Lemma for ennnfone 12301. (Contributed by Jim Kingdon, 15-Jul-2023.)
|
⊢ (𝜑 → 𝐹:ω–onto→𝐴)
& ⊢ (𝜑 → 𝐾 ∈ ω) & ⊢ (𝜑 → 𝑁 ∈ ω) & ⊢ (𝜑 → ∀𝑗 ∈ suc 𝑁(𝐹‘𝐾) ≠ (𝐹‘𝑗)) ⇒ ⊢ (𝜑 → 𝑁 ∈ 𝐾) |
|
Theorem | ennnfonelemj0 12277* |
Lemma for ennnfone 12301. 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 12278* |
Lemma for ennnfone 12301. 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 12279* |
Lemma for ennnfone 12301. 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 12280* |
Lemma for ennnfone 12301. (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 12281* |
Lemma for ennnfone 12301. 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 12282* |
Lemma for ennnfone 12301. 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 12283* |
Lemma for ennnfone 12301. 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 12284* |
Lemma for ennnfone 12301. 𝐻 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 12285* |
Lemma for ennnfone 12301. 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 12286* |
Lemma for ennnfone 12301. 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 12287* |
Lemma for ennnfone 12301. 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 12288* |
Lemma for ennnfone 12301. 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 12289* |
Lemma for ennnfone 12301. 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 12290* |
Lemma for ennnfone 12301. 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 12291* |
Lemma for ennnfone 12301. 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 12292* |
Lemma for ennnfone 12301. A consequence of ennnfonelemss 12286.
(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 12293* |
Lemma for ennnfone 12301. 𝐿 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 12294* |
Lemma for ennnfone 12301. 𝐿 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 12295* |
Lemma for ennnfone 12301. 𝐿 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 12296* |
Lemma for ennnfone 12301. 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 12297* |
Lemma for ennnfone 12301. 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 12298* |
Lemma for ennnfone 12301. A version of ennnfonelemen 12297 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 12299* |
Lemma for ennnfone 12301. The interesting direction, expressed in
deduction form. (Contributed by Jim Kingdon, 27-Oct-2022.)
|
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦)
& ⊢ (𝜑 → 𝐹:ℕ0–onto→𝐴)
& ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 ∃𝑘 ∈ ℕ0
∀𝑗 ∈
(0...𝑛)(𝐹‘𝑘) ≠ (𝐹‘𝑗)) ⇒ ⊢ (𝜑 → 𝐴 ≈ ℕ) |
|
Theorem | ennnfonelemim 12300* |
Lemma for ennnfone 12301. The trivial direction. (Contributed by
Jim
Kingdon, 27-Oct-2022.)
|
⊢ (𝐴 ≈ ℕ → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑓(𝑓:ℕ0–onto→𝐴 ∧ ∀𝑛 ∈ ℕ0 ∃𝑘 ∈ ℕ0
∀𝑗 ∈
(0...𝑛)(𝑓‘𝑘) ≠ (𝑓‘𝑗)))) |