Theorem List for Intuitionistic Logic Explorer - 12201-12300 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | pcpre1 12201* |
Value of the prime power pre-function at 1. (Contributed by Mario
Carneiro, 23-Feb-2014.) (Revised by Mario Carneiro, 26-Apr-2016.)
|
|
|
Theorem | pcpremul 12202* |
Multiplicative property of the prime count pre-function. Note that the
primality of
is essential for this property;
but
. 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.)
|
|
|
Theorem | pceulem 12203* |
Lemma for pceu 12204. (Contributed by Mario Carneiro,
23-Feb-2014.)
|
|
|
Theorem | pceu 12204* |
Uniqueness for the prime power function. (Contributed by Mario
Carneiro, 23-Feb-2014.)
|
|
|
Theorem | pcval 12205* |
The value of the prime power function. (Contributed by Mario Carneiro,
23-Feb-2014.) (Revised by Mario Carneiro, 3-Oct-2014.)
|
|
|
Theorem | pczpre 12206* |
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.)
|
|
|
Theorem | pczcl 12207 |
Closure of the prime power function. (Contributed by Mario Carneiro,
23-Feb-2014.)
|
|
|
Theorem | pccl 12208 |
Closure of the prime power function. (Contributed by Mario Carneiro,
23-Feb-2014.)
|
|
|
Theorem | pccld 12209 |
Closure of the prime power function. (Contributed by Mario Carneiro,
29-May-2016.)
|
|
|
Theorem | pcmul 12210 |
Multiplication property of the prime power function. (Contributed by
Mario Carneiro, 23-Feb-2014.)
|
|
|
Theorem | pcdiv 12211 |
Division property of the prime power function. (Contributed by Mario
Carneiro, 1-Mar-2014.)
|
|
|
Theorem | pcqmul 12212 |
Multiplication property of the prime power function. (Contributed by
Mario Carneiro, 9-Sep-2014.)
|
|
|
Theorem | pc0 12213 |
The value of the prime power function at zero. (Contributed by Mario
Carneiro, 3-Oct-2014.)
|
|
|
Theorem | pc1 12214 |
Value of the prime count function at 1. (Contributed by Mario Carneiro,
23-Feb-2014.)
|
|
|
Theorem | pcqcl 12215 |
Closure of the general prime count function. (Contributed by Mario
Carneiro, 23-Feb-2014.)
|
|
|
Theorem | pcqdiv 12216 |
Division property of the prime power function. (Contributed by Mario
Carneiro, 10-Aug-2015.)
|
|
|
Theorem | pcrec 12217 |
Prime power of a reciprocal. (Contributed by Mario Carneiro,
10-Aug-2015.)
|
|
|
Theorem | pcexp 12218 |
Prime power of an exponential. (Contributed by Mario Carneiro,
10-Aug-2015.)
|
|
|
Theorem | pcxnn0cl 12219 |
Extended nonnegative integer closure of the general prime count
function. (Contributed by Jim Kingdon, 13-Oct-2024.)
|
NN0* |
|
Theorem | pcxcl 12220 |
Extended real closure of the general prime count function. (Contributed
by Mario Carneiro, 3-Oct-2014.)
|
|
|
Theorem | pcge0 12221 |
The prime count of an integer is greater than or equal to zero.
(Contributed by Mario Carneiro, 3-Oct-2014.)
|
|
|
Theorem | pczdvds 12222 |
Defining property of the prime count function. (Contributed by Mario
Carneiro, 9-Sep-2014.)
|
|
|
Theorem | pcdvds 12223 |
Defining property of the prime count function. (Contributed by Mario
Carneiro, 23-Feb-2014.)
|
|
|
Theorem | pczndvds 12224 |
Defining property of the prime count function. (Contributed by Mario
Carneiro, 3-Oct-2014.)
|
|
|
Theorem | pcndvds 12225 |
Defining property of the prime count function. (Contributed by Mario
Carneiro, 23-Feb-2014.)
|
|
|
Theorem | pczndvds2 12226 |
The remainder after dividing out all factors of is not divisible
by .
(Contributed by Mario Carneiro, 9-Sep-2014.)
|
|
|
Theorem | pcndvds2 12227 |
The remainder after dividing out all factors of is not divisible
by .
(Contributed by Mario Carneiro, 23-Feb-2014.)
|
|
|
Theorem | pcdvdsb 12228 |
divides if and only if is at most the count of
. (Contributed
by Mario Carneiro, 3-Oct-2014.)
|
|
|
Theorem | pcelnn 12229 |
There are a positive number of powers of a prime in iff
divides .
(Contributed by Mario Carneiro, 23-Feb-2014.)
|
|
|
Theorem | pceq0 12230 |
There are zero powers of a prime in iff
does not divide
. (Contributed
by Mario Carneiro, 23-Feb-2014.)
|
|
|
Theorem | pcidlem 12231 |
The prime count of a prime power. (Contributed by Mario Carneiro,
12-Mar-2014.)
|
|
|
Theorem | pcid 12232 |
The prime count of a prime power. (Contributed by Mario Carneiro,
9-Sep-2014.)
|
|
|
Theorem | pcneg 12233 |
The prime count of a negative number. (Contributed by Mario Carneiro,
13-Mar-2014.)
|
|
|
Theorem | pcabs 12234 |
The prime count of an absolute value. (Contributed by Mario Carneiro,
13-Mar-2014.)
|
|
|
Theorem | pcdvdstr 12235 |
The prime count increases under the divisibility relation. (Contributed
by Mario Carneiro, 13-Mar-2014.)
|
|
|
Theorem | pcgcd1 12236 |
The prime count of a GCD is the minimum of the prime counts of the
arguments. (Contributed by Mario Carneiro, 3-Oct-2014.)
|
|
|
Theorem | pcgcd 12237 |
The prime count of a GCD is the minimum of the prime counts of the
arguments. (Contributed by Mario Carneiro, 3-Oct-2014.)
|
|
|
Theorem | pc2dvds 12238* |
A characterization of divisibility in terms of prime count.
(Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by Mario
Carneiro, 3-Oct-2014.)
|
|
|
Theorem | pc11 12239* |
The prime count function, viewed as a function from to
, is one-to-one. (Contributed by Mario Carneiro,
23-Feb-2014.)
|
|
|
Theorem | pcz 12240* |
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.)
|
|
|
Theorem | pcprmpw2 12241* |
Self-referential expression for a prime power. (Contributed by Mario
Carneiro, 16-Jan-2015.)
|
|
|
Theorem | pcprmpw 12242* |
Self-referential expression for a prime power. (Contributed by Mario
Carneiro, 16-Jan-2015.)
|
|
|
Theorem | dvdsprmpweq 12243* |
If a positive integer divides a prime power, it is a prime power.
(Contributed by AV, 25-Jul-2021.)
|
|
|
Theorem | dvdsprmpweqnn 12244* |
If an integer greater than 1 divides a prime power, it is a (proper)
prime power. (Contributed by AV, 13-Aug-2021.)
|
|
|
Theorem | dvdsprmpweqle 12245* |
If a positive integer divides a prime power, it is a prime power with a
smaller exponent. (Contributed by AV, 25-Jul-2021.)
|
|
|
Theorem | difsqpwdvds 12246 |
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.)
|
|
|
Theorem | pcaddlem 12247 |
Lemma for pcadd 12248. The original numbers and have been
decomposed using the prime count function as
where are both not divisible by and
, and similarly for . (Contributed by Mario
Carneiro, 9-Sep-2014.)
|
|
|
Theorem | pcadd 12248 |
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.)
|
|
|
Theorem | pcmptcl 12249 |
Closure for the prime power map. (Contributed by Mario Carneiro,
12-Mar-2014.)
|
|
|
Theorem | pcmpt 12250* |
Construct a function with given prime count characteristics.
(Contributed by Mario Carneiro, 12-Mar-2014.)
|
|
|
Theorem | pcmpt2 12251* |
Dividing two prime count maps yields a number with all dividing primes
confined to an interval. (Contributed by Mario Carneiro,
14-Mar-2014.)
|
|
|
Theorem | pcmptdvds 12252 |
The partial products of the prime power map form a divisibility chain.
(Contributed by Mario Carneiro, 12-Mar-2014.)
|
|
|
Theorem | pcprod 12253* |
The product of the primes taken to their respective powers reconstructs
the original number. (Contributed by Mario Carneiro, 12-Mar-2014.)
|
|
|
Theorem | sumhashdc 12254* |
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.)
|
DECID ♯ |
|
Theorem | fldivp1 12255 |
The difference between the floors of adjacent fractions is either 1 or 0.
(Contributed by Mario Carneiro, 8-Mar-2014.)
|
|
|
Theorem | pcfaclem 12256 |
Lemma for pcfac 12257. (Contributed by Mario Carneiro,
20-May-2014.)
|
|
|
Theorem | pcfac 12257* |
Calculate the prime count of a factorial. (Contributed by Mario
Carneiro, 11-Mar-2014.) (Revised by Mario Carneiro, 21-May-2014.)
|
|
|
Theorem | pcbc 12258* |
Calculate the prime count of a binomial coefficient. (Contributed by
Mario Carneiro, 11-Mar-2014.) (Revised by Mario Carneiro,
21-May-2014.)
|
|
|
Theorem | qexpz 12259 |
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 12260 |
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.)
|
|
|
Theorem | oddprmdvds 12261* |
Every positive integer which is not a power of two is divisible by an
odd prime number. (Contributed by AV, 6-Aug-2021.)
|
|
|
5.3 Cardinality of real and complex number
subsets
|
|
5.3.1 Countability of integers and
rationals
|
|
Theorem | oddennn 12262 |
There are as many odd positive integers as there are positive integers.
(Contributed by Jim Kingdon, 11-May-2022.)
|
|
|
Theorem | evenennn 12263 |
There are as many even positive integers as there are positive integers.
(Contributed by Jim Kingdon, 12-May-2022.)
|
|
|
Theorem | xpnnen 12264 |
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 12265 |
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 12266 |
The cartesian product of two sets dominated by is dominated by
.
(Contributed by Thierry Arnoux, 24-Sep-2017.)
|
|
|
Theorem | unennn 12267 |
The union of two disjoint countably infinite sets is countably infinite.
(Contributed by Jim Kingdon, 13-May-2022.)
|
|
|
Theorem | znnen 12268 |
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 12269* |
Lemma for ennnfone 12295. A direct consequence of fidcenumlemrk 6910.
(Contributed by Jim Kingdon, 15-Jul-2023.)
|
DECID
DECID |
|
Theorem | ennnfonelemk 12270* |
Lemma for ennnfone 12295. (Contributed by Jim Kingdon, 15-Jul-2023.)
|
|
|
Theorem | ennnfonelemj0 12271* |
Lemma for ennnfone 12295. Initial state for . (Contributed by Jim
Kingdon, 20-Jul-2023.)
|
DECID
frec
|
|
Theorem | ennnfonelemjn 12272* |
Lemma for ennnfone 12295. Non-initial state for . (Contributed by
Jim Kingdon, 20-Jul-2023.)
|
DECID
frec
|
|
Theorem | ennnfonelemg 12273* |
Lemma for ennnfone 12295. Closure for . (Contributed by Jim
Kingdon, 20-Jul-2023.)
|
DECID
frec
|
|
Theorem | ennnfonelemh 12274* |
Lemma for ennnfone 12295. (Contributed by Jim Kingdon, 8-Jul-2023.)
|
DECID
frec
|
|
Theorem | ennnfonelem0 12275* |
Lemma for ennnfone 12295. Initial value. (Contributed by Jim
Kingdon,
15-Jul-2023.)
|
DECID
frec
|
|
Theorem | ennnfonelemp1 12276* |
Lemma for ennnfone 12295. Value of at a successor. (Contributed
by Jim Kingdon, 23-Jul-2023.)
|
DECID
frec
|
|
Theorem | ennnfonelem1 12277* |
Lemma for ennnfone 12295. Second value. (Contributed by Jim
Kingdon,
19-Jul-2023.)
|
DECID
frec
|
|
Theorem | ennnfonelemom 12278* |
Lemma for ennnfone 12295. yields finite sequences. (Contributed by
Jim Kingdon, 19-Jul-2023.)
|
DECID
frec
|
|
Theorem | ennnfonelemhdmp1 12279* |
Lemma for ennnfone 12295. Domain at a successor where we need to add
an
element to the sequence. (Contributed by Jim Kingdon,
23-Jul-2023.)
|
DECID
frec
|
|
Theorem | ennnfonelemss 12280* |
Lemma for ennnfone 12295. We only add elements to as the index
increases. (Contributed by Jim Kingdon, 15-Jul-2023.)
|
DECID
frec
|
|
Theorem | ennnfoneleminc 12281* |
Lemma for ennnfone 12295. We only add elements to as the index
increases. (Contributed by Jim Kingdon, 21-Jul-2023.)
|
DECID
frec
|
|
Theorem | ennnfonelemkh 12282* |
Lemma for ennnfone 12295. 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
frec
|
|
Theorem | ennnfonelemhf1o 12283* |
Lemma for ennnfone 12295. Each of the functions in is one to one
and onto an image of . (Contributed by Jim Kingdon,
17-Jul-2023.)
|
DECID
frec
|
|
Theorem | ennnfonelemex 12284* |
Lemma for ennnfone 12295. Extending the sequence to
include an additional element. (Contributed by Jim Kingdon,
19-Jul-2023.)
|
DECID
frec
|
|
Theorem | ennnfonelemhom 12285* |
Lemma for ennnfone 12295. The sequences in increase in length
without bound if you go out far enough. (Contributed by Jim Kingdon,
19-Jul-2023.)
|
DECID
frec
|
|
Theorem | ennnfonelemrnh 12286* |
Lemma for ennnfone 12295. A consequence of ennnfonelemss 12280.
(Contributed by Jim Kingdon, 16-Jul-2023.)
|
DECID
frec
|
|
Theorem | ennnfonelemfun 12287* |
Lemma for ennnfone 12295. is a function. (Contributed by Jim
Kingdon, 16-Jul-2023.)
|
DECID
frec
|
|
Theorem | ennnfonelemf1 12288* |
Lemma for ennnfone 12295. is one-to-one. (Contributed by Jim
Kingdon, 16-Jul-2023.)
|
DECID
frec
|
|
Theorem | ennnfonelemrn 12289* |
Lemma for ennnfone 12295. is onto . (Contributed by Jim
Kingdon, 16-Jul-2023.)
|
DECID
frec
|
|
Theorem | ennnfonelemdm 12290* |
Lemma for ennnfone 12295. The function is defined everywhere.
(Contributed by Jim Kingdon, 16-Jul-2023.)
|
DECID
frec
|
|
Theorem | ennnfonelemen 12291* |
Lemma for ennnfone 12295. The result. (Contributed by Jim Kingdon,
16-Jul-2023.)
|
DECID
frec
|
|
Theorem | ennnfonelemnn0 12292* |
Lemma for ennnfone 12295. A version of ennnfonelemen 12291 expressed in
terms of instead of . (Contributed by Jim Kingdon,
27-Oct-2022.)
|
DECID
frec |
|
Theorem | ennnfonelemr 12293* |
Lemma for ennnfone 12295. The interesting direction, expressed in
deduction form. (Contributed by Jim Kingdon, 27-Oct-2022.)
|
DECID
|
|
Theorem | ennnfonelemim 12294* |
Lemma for ennnfone 12295. The trivial direction. (Contributed by
Jim
Kingdon, 27-Oct-2022.)
|
DECID
|
|
Theorem | ennnfone 12295* |
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 part, as seen in theorems
like ctm 7065), 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
|
|
Theorem | exmidunben 12296* |
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 12297* |
Lemma for ctinfom 12298. Converting between and .
(Contributed by Jim Kingdon, 10-Aug-2023.)
|
frec
|
|
Theorem | ctinfom 12298* |
A condition for a set being countably infinite. Restates ennnfone 12295 in
terms of
and function image. Like ennnfone 12295 the condition can
be summarized as being countable, infinite, and having decidable
equality. (Contributed by Jim Kingdon, 7-Aug-2023.)
|
DECID |
|
Theorem | inffinp1 12299* |
An infinite set contains an element not contained in a given finite
subset. (Contributed by Jim Kingdon, 7-Aug-2023.)
|
DECID
|
|
Theorem | ctinf 12300* |
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 |