Theorem List for Intuitionistic Logic Explorer - 12101-12200 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | phiprmpw 12101 |
Value of the Euler function at a prime power. Theorem 2.5(a) in
[ApostolNT] p. 28. (Contributed by
Mario Carneiro, 24-Feb-2014.)
|
|
|
Theorem | phiprm 12102 |
Value of the Euler function at a prime. (Contributed by Mario
Carneiro, 28-Feb-2014.)
|
|
|
Theorem | crth 12103* |
The Chinese Remainder Theorem: the function that maps to its
remainder classes and is 1-1 and onto when and
are coprime.
(Contributed by Mario Carneiro, 24-Feb-2014.)
(Proof shortened by Mario Carneiro, 2-May-2016.)
|
..^ ..^ ..^
|
|
Theorem | phimullem 12104* |
Lemma for phimul 12105. (Contributed by Mario Carneiro,
24-Feb-2014.)
|
..^ ..^ ..^
..^
..^
|
|
Theorem | phimul 12105 |
The Euler
function is a multiplicative function, meaning that it
distributes over multiplication at relatively prime arguments. Theorem
2.5(c) in [ApostolNT] p. 28.
(Contributed by Mario Carneiro,
24-Feb-2014.)
|
|
|
Theorem | eulerthlem1 12106* |
Lemma for eulerth 12112. (Contributed by Mario Carneiro,
8-May-2015.)
|
..^
|
|
Theorem | eulerthlemfi 12107* |
Lemma for eulerth 12112. The set is finite. (Contributed by Mario
Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 7-Sep-2024.)
|
..^ |
|
Theorem | eulerthlemrprm 12108* |
Lemma for eulerth 12112. and
are relatively prime.
(Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim
Kingdon, 2-Sep-2024.)
|
..^
|
|
Theorem | eulerthlema 12109* |
Lemma for eulerth 12112. (Contributed by Mario Carneiro,
28-Feb-2014.)
(Revised by Jim Kingdon, 2-Sep-2024.)
|
..^
|
|
Theorem | eulerthlemh 12110* |
Lemma for eulerth 12112. A permutation of .
(Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim
Kingdon, 5-Sep-2024.)
|
..^
|
|
Theorem | eulerthlemth 12111* |
Lemma for eulerth 12112. The result. (Contributed by Mario
Carneiro,
28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.)
|
..^
|
|
Theorem | eulerth 12112 |
Euler's theorem, a generalization of Fermat's little theorem. If
and are
coprime, then (mod ). This
is Metamath 100 proof #10. Also called Euler-Fermat theorem, see
theorem 5.17 in [ApostolNT] p. 113.
(Contributed by Mario Carneiro,
28-Feb-2014.)
|
|
|
Theorem | fermltl 12113 |
Fermat's little theorem. When is prime, (mod )
for any , see
theorem 5.19 in [ApostolNT] p. 114.
(Contributed by
Mario Carneiro, 28-Feb-2014.) (Proof shortened by AV, 19-Mar-2022.)
|
|
|
Theorem | prmdiv 12114 |
Show an explicit expression for the modular inverse of .
(Contributed by Mario Carneiro, 24-Jan-2015.)
|
|
|
Theorem | prmdiveq 12115 |
The modular inverse of is unique. (Contributed
by Mario
Carneiro, 24-Jan-2015.)
|
|
|
Theorem | prmdivdiv 12116 |
The (modular) inverse of the inverse of a number is itself.
(Contributed by Mario Carneiro, 24-Jan-2015.)
|
|
|
Theorem | hashgcdlem 12117* |
A correspondence between elements of specific GCD and relative primes in
a smaller ring. (Contributed by Stefan O'Rear, 12-Sep-2015.)
|
..^
..^
|
|
Theorem | hashgcdeq 12118* |
Number of initial positive integers with specified divisors.
(Contributed by Stefan O'Rear, 12-Sep-2015.)
|
♯ ..^ |
|
Theorem | phisum 12119* |
The divisor sum identity of the totient function. Theorem 2.2 in
[ApostolNT] p. 26. (Contributed by
Stefan O'Rear, 12-Sep-2015.)
|
|
|
Theorem | odzval 12120* |
Value of the order function. This is a function of functions; the inner
argument selects the base (i.e., mod for some , often prime)
and the outer argument selects the integer or equivalence class (if you
want to think about it that way) from the integers mod . In order
to ensure the supremum is well-defined, we only define the expression
when and are coprime. (Contributed
by Mario Carneiro,
23-Feb-2014.) (Revised by AV, 26-Sep-2020.)
|
inf
|
|
Theorem | odzcllem 12121 |
- Lemma for odzcl 12122, showing existence of a recurrent point for
the
exponential. (Contributed by Mario Carneiro, 28-Feb-2014.) (Proof
shortened by AV, 26-Sep-2020.)
|
|
|
Theorem | odzcl 12122 |
The order of a group element is an integer. (Contributed by Mario
Carneiro, 28-Feb-2014.)
|
|
|
Theorem | odzid 12123 |
Any element raised to the power of its order is . (Contributed by
Mario Carneiro, 28-Feb-2014.)
|
|
|
Theorem | odzdvds 12124 |
The only powers of
that are congruent to
are the multiples
of the order of . (Contributed by Mario Carneiro, 28-Feb-2014.)
(Proof shortened by AV, 26-Sep-2020.)
|
|
|
Theorem | odzphi 12125 |
The order of any group element is a divisor of the Euler
function. (Contributed by Mario Carneiro, 28-Feb-2014.)
|
|
|
5.2.6 Arithmetic modulo a prime
number
|
|
Theorem | modprm1div 12126 |
A prime number divides an integer minus 1 iff the integer modulo the prime
number is 1. (Contributed by Alexander van der Vekens, 17-May-2018.)
(Proof shortened by AV, 30-May-2023.)
|
|
|
Theorem | m1dvdsndvds 12127 |
If an integer minus 1 is divisible by a prime number, the integer itself
is not divisible by this prime number. (Contributed by Alexander van der
Vekens, 30-Aug-2018.)
|
|
|
Theorem | modprminv 12128 |
Show an explicit expression for the modular inverse of .
This is an application of prmdiv 12114. (Contributed by Alexander van der
Vekens, 15-May-2018.)
|
|
|
Theorem | modprminveq 12129 |
The modular inverse of is unique. (Contributed
by Alexander
van der Vekens, 17-May-2018.)
|
|
|
Theorem | vfermltl 12130 |
Variant of Fermat's little theorem if is not a multiple of ,
see theorem 5.18 in [ApostolNT] p. 113.
(Contributed by AV, 21-Aug-2020.)
(Proof shortened by AV, 5-Sep-2020.)
|
|
|
Theorem | powm2modprm 12131 |
If an integer minus 1 is divisible by a prime number, then the integer to
the power of the prime number minus 2 is 1 modulo the prime number.
(Contributed by Alexander van der Vekens, 30-Aug-2018.)
|
|
|
Theorem | reumodprminv 12132* |
For any prime number and for any positive integer less than this prime
number, there is a unique modular inverse of this positive integer.
(Contributed by Alexander van der Vekens, 12-May-2018.)
|
..^
|
|
Theorem | modprm0 12133* |
For two positive integers less than a given prime number there is always
a nonnegative integer (less than the given prime number) so that the sum
of one of the two positive integers and the other of the positive
integers multiplied by the nonnegative integer is 0 ( modulo the given
prime number). (Contributed by Alexander van der Vekens,
17-May-2018.)
|
..^
..^
..^ |
|
Theorem | nnnn0modprm0 12134* |
For a positive integer and a nonnegative integer both less than a given
prime number there is always a second nonnegative integer (less than the
given prime number) so that the sum of this second nonnegative integer
multiplied with the positive integer and the first nonnegative integer
is 0 ( modulo the given prime number). (Contributed by Alexander van
der Vekens, 8-Nov-2018.)
|
..^
..^
..^ |
|
Theorem | modprmn0modprm0 12135* |
For an integer not being 0 modulo a given prime number and a nonnegative
integer less than the prime number, there is always a second nonnegative
integer (less than the given prime number) so that the sum of this
second nonnegative integer multiplied with the integer and the first
nonnegative integer is 0 ( modulo the given prime number). (Contributed
by Alexander van der Vekens, 10-Nov-2018.)
|
..^
..^ |
|
5.2.7 Pythagorean Triples
|
|
Theorem | coprimeprodsq 12136 |
If three numbers are coprime, and the square of one is the product of the
other two, then there is a formula for the other two in terms of
and square. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario
Carneiro, 19-Apr-2014.)
|
|
|
Theorem | coprimeprodsq2 12137 |
If three numbers are coprime, and the square of one is the product of the
other two, then there is a formula for the other two in terms of
and square. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by
Mario Carneiro, 19-Apr-2014.)
|
|
|
Theorem | oddprm 12138 |
A prime not equal to is
odd. (Contributed by Mario Carneiro,
4-Feb-2015.) (Proof shortened by AV, 10-Jul-2022.)
|
|
|
Theorem | nnoddn2prm 12139 |
A prime not equal to is
an odd positive integer. (Contributed by
AV, 28-Jun-2021.)
|
|
|
Theorem | oddn2prm 12140 |
A prime not equal to is
odd. (Contributed by AV, 28-Jun-2021.)
|
|
|
Theorem | nnoddn2prmb 12141 |
A number is a prime number not equal to iff it is an odd prime
number. Conversion theorem for two representations of odd primes.
(Contributed by AV, 14-Jul-2021.)
|
|
|
Theorem | prm23lt5 12142 |
A prime less than 5 is either 2 or 3. (Contributed by AV, 5-Jul-2021.)
|
|
|
Theorem | prm23ge5 12143 |
A prime is either 2 or 3 or greater than or equal to 5. (Contributed by
AV, 5-Jul-2021.)
|
|
|
Theorem | pythagtriplem1 12144* |
Lemma for pythagtrip 12162. Prove a weaker version of one direction of
the
theorem. (Contributed by Scott Fenton, 28-Mar-2014.) (Revised by Mario
Carneiro, 19-Apr-2014.)
|
|
|
Theorem | pythagtriplem2 12145* |
Lemma for pythagtrip 12162. Prove the full version of one direction of
the
theorem. (Contributed by Scott Fenton, 28-Mar-2014.) (Revised by Mario
Carneiro, 19-Apr-2014.)
|
|
|
Theorem | pythagtriplem3 12146 |
Lemma for pythagtrip 12162. Show that and are relatively prime
under some conditions. (Contributed by Scott Fenton, 8-Apr-2014.)
(Revised by Mario Carneiro, 19-Apr-2014.)
|
|
|
Theorem | pythagtriplem4 12147 |
Lemma for pythagtrip 12162. Show that and are relatively
prime. (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario
Carneiro, 19-Apr-2014.)
|
|
|
Theorem | pythagtriplem10 12148 |
Lemma for pythagtrip 12162. Show that is
positive. (Contributed
by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro,
19-Apr-2014.)
|
|
|
Theorem | pythagtriplem6 12149 |
Lemma for pythagtrip 12162. Calculate .
(Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro,
19-Apr-2014.)
|
|
|
Theorem | pythagtriplem7 12150 |
Lemma for pythagtrip 12162. Calculate .
(Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro,
19-Apr-2014.)
|
|
|
Theorem | pythagtriplem8 12151 |
Lemma for pythagtrip 12162. Show that is a
positive integer. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised
by Mario Carneiro, 19-Apr-2014.)
|
|
|
Theorem | pythagtriplem9 12152 |
Lemma for pythagtrip 12162. Show that is a
positive integer. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised
by Mario Carneiro, 19-Apr-2014.)
|
|
|
Theorem | pythagtriplem11 12153 |
Lemma for pythagtrip 12162. Show that (which will eventually be
closely related to the in the final statement) is a natural.
(Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro,
19-Apr-2014.)
|
|
|
Theorem | pythagtriplem12 12154 |
Lemma for pythagtrip 12162. Calculate the square of . (Contributed
by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro,
19-Apr-2014.)
|
|
|
Theorem | pythagtriplem13 12155 |
Lemma for pythagtrip 12162. Show that (which will eventually be
closely related to the in the final statement) is a natural.
(Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro,
19-Apr-2014.)
|
|
|
Theorem | pythagtriplem14 12156 |
Lemma for pythagtrip 12162. Calculate the square of . (Contributed
by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro,
19-Apr-2014.)
|
|
|
Theorem | pythagtriplem15 12157 |
Lemma for pythagtrip 12162. Show the relationship between , ,
and .
(Contributed by Scott Fenton, 17-Apr-2014.) (Revised by
Mario Carneiro, 19-Apr-2014.)
|
|
|
Theorem | pythagtriplem16 12158 |
Lemma for pythagtrip 12162. Show the relationship between , ,
and .
(Contributed by Scott Fenton, 17-Apr-2014.) (Revised by
Mario Carneiro, 19-Apr-2014.)
|
|
|
Theorem | pythagtriplem17 12159 |
Lemma for pythagtrip 12162. Show the relationship between , ,
and .
(Contributed by Scott Fenton, 17-Apr-2014.) (Revised by
Mario Carneiro, 19-Apr-2014.)
|
|
|
Theorem | pythagtriplem18 12160* |
Lemma for pythagtrip 12162. Wrap the previous and up in
quantifiers. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by
Mario Carneiro, 19-Apr-2014.)
|
|
|
Theorem | pythagtriplem19 12161* |
Lemma for pythagtrip 12162. Introduce and remove the relative
primality requirement. (Contributed by Scott Fenton, 18-Apr-2014.)
(Revised by Mario Carneiro, 19-Apr-2014.)
|
|
|
Theorem | pythagtrip 12162* |
Parameterize the Pythagorean triples. If , ,
and are
naturals, then they obey the Pythagorean triple formula iff they are
parameterized by three naturals. This proof follows the Isabelle proof
at http://afp.sourceforge.net/entries/Fermat3_4.shtml.
This is
Metamath 100 proof #23. (Contributed by Scott Fenton, 19-Apr-2014.)
|
|
|
5.3 Cardinality of real and complex number
subsets
|
|
5.3.1 Countability of integers and
rationals
|
|
Theorem | oddennn 12163 |
There are as many odd positive integers as there are positive integers.
(Contributed by Jim Kingdon, 11-May-2022.)
|
|
|
Theorem | evenennn 12164 |
There are as many even positive integers as there are positive integers.
(Contributed by Jim Kingdon, 12-May-2022.)
|
|
|
Theorem | xpnnen 12165 |
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 12166 |
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 12167 |
The cartesian product of two sets dominated by is dominated by
.
(Contributed by Thierry Arnoux, 24-Sep-2017.)
|
|
|
Theorem | unennn 12168 |
The union of two disjoint countably infinite sets is countably infinite.
(Contributed by Jim Kingdon, 13-May-2022.)
|
|
|
Theorem | znnen 12169 |
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 12170* |
Lemma for ennnfone 12196. A direct consequence of fidcenumlemrk 6899.
(Contributed by Jim Kingdon, 15-Jul-2023.)
|
DECID
DECID |
|
Theorem | ennnfonelemk 12171* |
Lemma for ennnfone 12196. (Contributed by Jim Kingdon, 15-Jul-2023.)
|
|
|
Theorem | ennnfonelemj0 12172* |
Lemma for ennnfone 12196. Initial state for . (Contributed by Jim
Kingdon, 20-Jul-2023.)
|
DECID
frec
|
|
Theorem | ennnfonelemjn 12173* |
Lemma for ennnfone 12196. Non-initial state for . (Contributed by
Jim Kingdon, 20-Jul-2023.)
|
DECID
frec
|
|
Theorem | ennnfonelemg 12174* |
Lemma for ennnfone 12196. Closure for . (Contributed by Jim
Kingdon, 20-Jul-2023.)
|
DECID
frec
|
|
Theorem | ennnfonelemh 12175* |
Lemma for ennnfone 12196. (Contributed by Jim Kingdon, 8-Jul-2023.)
|
DECID
frec
|
|
Theorem | ennnfonelem0 12176* |
Lemma for ennnfone 12196. Initial value. (Contributed by Jim
Kingdon,
15-Jul-2023.)
|
DECID
frec
|
|
Theorem | ennnfonelemp1 12177* |
Lemma for ennnfone 12196. Value of at a successor. (Contributed
by Jim Kingdon, 23-Jul-2023.)
|
DECID
frec
|
|
Theorem | ennnfonelem1 12178* |
Lemma for ennnfone 12196. Second value. (Contributed by Jim
Kingdon,
19-Jul-2023.)
|
DECID
frec
|
|
Theorem | ennnfonelemom 12179* |
Lemma for ennnfone 12196. yields finite sequences. (Contributed by
Jim Kingdon, 19-Jul-2023.)
|
DECID
frec
|
|
Theorem | ennnfonelemhdmp1 12180* |
Lemma for ennnfone 12196. 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 12181* |
Lemma for ennnfone 12196. We only add elements to as the index
increases. (Contributed by Jim Kingdon, 15-Jul-2023.)
|
DECID
frec
|
|
Theorem | ennnfoneleminc 12182* |
Lemma for ennnfone 12196. We only add elements to as the index
increases. (Contributed by Jim Kingdon, 21-Jul-2023.)
|
DECID
frec
|
|
Theorem | ennnfonelemkh 12183* |
Lemma for ennnfone 12196. 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 12184* |
Lemma for ennnfone 12196. 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 12185* |
Lemma for ennnfone 12196. Extending the sequence to
include an additional element. (Contributed by Jim Kingdon,
19-Jul-2023.)
|
DECID
frec
|
|
Theorem | ennnfonelemhom 12186* |
Lemma for ennnfone 12196. 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 12187* |
Lemma for ennnfone 12196. A consequence of ennnfonelemss 12181.
(Contributed by Jim Kingdon, 16-Jul-2023.)
|
DECID
frec
|
|
Theorem | ennnfonelemfun 12188* |
Lemma for ennnfone 12196. is a function. (Contributed by Jim
Kingdon, 16-Jul-2023.)
|
DECID
frec
|
|
Theorem | ennnfonelemf1 12189* |
Lemma for ennnfone 12196. is one-to-one. (Contributed by Jim
Kingdon, 16-Jul-2023.)
|
DECID
frec
|
|
Theorem | ennnfonelemrn 12190* |
Lemma for ennnfone 12196. is onto . (Contributed by Jim
Kingdon, 16-Jul-2023.)
|
DECID
frec
|
|
Theorem | ennnfonelemdm 12191* |
Lemma for ennnfone 12196. The function is defined everywhere.
(Contributed by Jim Kingdon, 16-Jul-2023.)
|
DECID
frec
|
|
Theorem | ennnfonelemen 12192* |
Lemma for ennnfone 12196. The result. (Contributed by Jim Kingdon,
16-Jul-2023.)
|
DECID
frec
|
|
Theorem | ennnfonelemnn0 12193* |
Lemma for ennnfone 12196. A version of ennnfonelemen 12192 expressed in
terms of instead of . (Contributed by Jim Kingdon,
27-Oct-2022.)
|
DECID
frec |
|
Theorem | ennnfonelemr 12194* |
Lemma for ennnfone 12196. The interesting direction, expressed in
deduction form. (Contributed by Jim Kingdon, 27-Oct-2022.)
|
DECID
|
|
Theorem | ennnfonelemim 12195* |
Lemma for ennnfone 12196. The trivial direction. (Contributed by
Jim
Kingdon, 27-Oct-2022.)
|
DECID
|
|
Theorem | ennnfone 12196* |
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 7054), 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 12197* |
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 12198* |
Lemma for ctinfom 12199. Converting between and .
(Contributed by Jim Kingdon, 10-Aug-2023.)
|
frec
|
|
Theorem | ctinfom 12199* |
A condition for a set being countably infinite. Restates ennnfone 12196 in
terms of
and function image. Like ennnfone 12196 the condition can
be summarized as being countable, infinite, and having decidable
equality. (Contributed by Jim Kingdon, 7-Aug-2023.)
|
DECID |
|
Theorem | inffinp1 12200* |
An infinite set contains an element not contained in a given finite
subset. (Contributed by Jim Kingdon, 7-Aug-2023.)
|
DECID
|