Theorem List for Intuitionistic Logic Explorer - 10301-10400 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | zmodcld 10301 |
Closure law for the modulo operation restricted to integers.
(Contributed by Mario Carneiro, 28-May-2016.)
|
|
|
Theorem | zmodfz 10302 |
An integer mod lies
in the first
nonnegative integers.
(Contributed by Jeff Madsen, 17-Jun-2010.)
|
|
|
Theorem | zmodfzo 10303 |
An integer mod lies
in the first
nonnegative integers.
(Contributed by Stefan O'Rear, 6-Sep-2015.)
|
..^ |
|
Theorem | zmodfzp1 10304 |
An integer mod lies
in the first nonnegative integers.
(Contributed by AV, 27-Oct-2018.)
|
|
|
Theorem | modqid 10305 |
Identity law for modulo. (Contributed by Jim Kingdon, 21-Oct-2021.)
|
|
|
Theorem | modqid0 10306 |
A positive real number modulo itself is 0. (Contributed by Jim Kingdon,
21-Oct-2021.)
|
|
|
Theorem | modqid2 10307 |
Identity law for modulo. (Contributed by Jim Kingdon, 21-Oct-2021.)
|
|
|
Theorem | zmodid2 10308 |
Identity law for modulo restricted to integers. (Contributed by Paul
Chapman, 22-Jun-2011.)
|
|
|
Theorem | zmodidfzo 10309 |
Identity law for modulo restricted to integers. (Contributed by AV,
27-Oct-2018.)
|
..^ |
|
Theorem | zmodidfzoimp 10310 |
Identity law for modulo restricted to integers. (Contributed by AV,
27-Oct-2018.)
|
..^
|
|
Theorem | q0mod 10311 |
Special case: 0 modulo a positive real number is 0. (Contributed by Jim
Kingdon, 21-Oct-2021.)
|
|
|
Theorem | q1mod 10312 |
Special case: 1 modulo a real number greater than 1 is 1. (Contributed by
Jim Kingdon, 21-Oct-2021.)
|
|
|
Theorem | modqabs 10313 |
Absorption law for modulo. (Contributed by Jim Kingdon,
21-Oct-2021.)
|
|
|
Theorem | modqabs2 10314 |
Absorption law for modulo. (Contributed by Jim Kingdon, 21-Oct-2021.)
|
|
|
Theorem | modqcyc 10315 |
The modulo operation is periodic. (Contributed by Jim Kingdon,
21-Oct-2021.)
|
|
|
Theorem | modqcyc2 10316 |
The modulo operation is periodic. (Contributed by Jim Kingdon,
21-Oct-2021.)
|
|
|
Theorem | modqadd1 10317 |
Addition property of the modulo operation. (Contributed by Jim Kingdon,
22-Oct-2021.)
|
|
|
Theorem | modqaddabs 10318 |
Absorption law for modulo. (Contributed by Jim Kingdon, 22-Oct-2021.)
|
|
|
Theorem | modqaddmod 10319 |
The sum of a number modulo a modulus and another number equals the sum of
the two numbers modulo the same modulus. (Contributed by Jim Kingdon,
23-Oct-2021.)
|
|
|
Theorem | mulqaddmodid 10320 |
The sum of a positive rational number less than an upper bound and the
product of an integer and the upper bound is the positive rational number
modulo the upper bound. (Contributed by Jim Kingdon, 23-Oct-2021.)
|
|
|
Theorem | mulp1mod1 10321 |
The product of an integer and an integer greater than 1 increased by 1 is
1 modulo the integer greater than 1. (Contributed by AV, 15-Jul-2021.)
|
|
|
Theorem | modqmuladd 10322* |
Decomposition of an integer into a multiple of a modulus and a
remainder. (Contributed by Jim Kingdon, 23-Oct-2021.)
|
|
|
Theorem | modqmuladdim 10323* |
Implication of a decomposition of an integer into a multiple of a
modulus and a remainder. (Contributed by Jim Kingdon, 23-Oct-2021.)
|
|
|
Theorem | modqmuladdnn0 10324* |
Implication of a decomposition of a nonnegative integer into a multiple
of a modulus and a remainder. (Contributed by Jim Kingdon,
23-Oct-2021.)
|
|
|
Theorem | qnegmod 10325 |
The negation of a number modulo a positive number is equal to the
difference of the modulus and the number modulo the modulus. (Contributed
by Jim Kingdon, 24-Oct-2021.)
|
|
|
Theorem | m1modnnsub1 10326 |
Minus one modulo a positive integer is equal to the integer minus one.
(Contributed by AV, 14-Jul-2021.)
|
|
|
Theorem | m1modge3gt1 10327 |
Minus one modulo an integer greater than two is greater than one.
(Contributed by AV, 14-Jul-2021.)
|
|
|
Theorem | addmodid 10328 |
The sum of a positive integer and a nonnegative integer less than the
positive integer is equal to the nonnegative integer modulo the positive
integer. (Contributed by Alexander van der Vekens, 30-Oct-2018.) (Proof
shortened by AV, 5-Jul-2020.)
|
|
|
Theorem | addmodidr 10329 |
The sum of a positive integer and a nonnegative integer less than the
positive integer is equal to the nonnegative integer modulo the positive
integer. (Contributed by AV, 19-Mar-2021.)
|
|
|
Theorem | modqadd2mod 10330 |
The sum of a number modulo a modulus and another number equals the sum of
the two numbers modulo the modulus. (Contributed by Jim Kingdon,
24-Oct-2021.)
|
|
|
Theorem | modqm1p1mod0 10331 |
If a number modulo a modulus equals the modulus decreased by 1, the first
number increased by 1 modulo the modulus equals 0. (Contributed by Jim
Kingdon, 24-Oct-2021.)
|
|
|
Theorem | modqltm1p1mod 10332 |
If a number modulo a modulus is less than the modulus decreased by 1, the
first number increased by 1 modulo the modulus equals the first number
modulo the modulus, increased by 1. (Contributed by Jim Kingdon,
24-Oct-2021.)
|
|
|
Theorem | modqmul1 10333 |
Multiplication property of the modulo operation. Note that the
multiplier
must be an integer. (Contributed by Jim Kingdon,
24-Oct-2021.)
|
|
|
Theorem | modqmul12d 10334 |
Multiplication property of the modulo operation, see theorem 5.2(b) in
[ApostolNT] p. 107. (Contributed by
Jim Kingdon, 24-Oct-2021.)
|
|
|
Theorem | modqnegd 10335 |
Negation property of the modulo operation. (Contributed by Jim Kingdon,
24-Oct-2021.)
|
|
|
Theorem | modqadd12d 10336 |
Additive property of the modulo operation. (Contributed by Jim Kingdon,
25-Oct-2021.)
|
|
|
Theorem | modqsub12d 10337 |
Subtraction property of the modulo operation. (Contributed by Jim
Kingdon, 25-Oct-2021.)
|
|
|
Theorem | modqsubmod 10338 |
The difference of a number modulo a modulus and another number equals the
difference of the two numbers modulo the modulus. (Contributed by Jim
Kingdon, 25-Oct-2021.)
|
|
|
Theorem | modqsubmodmod 10339 |
The difference of a number modulo a modulus and another number modulo the
same modulus equals the difference of the two numbers modulo the modulus.
(Contributed by Jim Kingdon, 25-Oct-2021.)
|
|
|
Theorem | q2txmodxeq0 10340 |
Two times a positive number modulo the number is zero. (Contributed by
Jim Kingdon, 25-Oct-2021.)
|
|
|
Theorem | q2submod 10341 |
If a number is between a modulus and twice the modulus, the first number
modulo the modulus equals the first number minus the modulus.
(Contributed by Jim Kingdon, 25-Oct-2021.)
|
|
|
Theorem | modifeq2int 10342 |
If a nonnegative integer is less than twice a positive integer, the
nonnegative integer modulo the positive integer equals the nonnegative
integer or the nonnegative integer minus the positive integer.
(Contributed by Alexander van der Vekens, 21-May-2018.)
|
|
|
Theorem | modaddmodup 10343 |
The sum of an integer modulo a positive integer and another integer minus
the positive integer equals the sum of the two integers modulo the
positive integer if the other integer is in the upper part of the range
between 0 and the positive integer. (Contributed by AV, 30-Oct-2018.)
|
..^
|
|
Theorem | modaddmodlo 10344 |
The sum of an integer modulo a positive integer and another integer equals
the sum of the two integers modulo the positive integer if the other
integer is in the lower part of the range between 0 and the positive
integer. (Contributed by AV, 30-Oct-2018.)
|
..^
|
|
Theorem | modqmulmod 10345 |
The product of a rational number modulo a modulus and an integer equals
the product of the rational number and the integer modulo the modulus.
(Contributed by Jim Kingdon, 25-Oct-2021.)
|
|
|
Theorem | modqmulmodr 10346 |
The product of an integer and a rational number modulo a modulus equals
the product of the integer and the rational number modulo the modulus.
(Contributed by Jim Kingdon, 26-Oct-2021.)
|
|
|
Theorem | modqaddmulmod 10347 |
The sum of a rational number and the product of a second rational number
modulo a modulus and an integer equals the sum of the rational number and
the product of the other rational number and the integer modulo the
modulus. (Contributed by Jim Kingdon, 26-Oct-2021.)
|
|
|
Theorem | modqdi 10348 |
Distribute multiplication over a modulo operation. (Contributed by Jim
Kingdon, 26-Oct-2021.)
|
|
|
Theorem | modqsubdir 10349 |
Distribute the modulo operation over a subtraction. (Contributed by Jim
Kingdon, 26-Oct-2021.)
|
|
|
Theorem | modqeqmodmin 10350 |
A rational number equals the difference of the rational number and a
modulus modulo the modulus. (Contributed by Jim Kingdon, 26-Oct-2021.)
|
|
|
Theorem | modfzo0difsn 10351* |
For a number within a half-open range of nonnegative integers with one
excluded integer there is a positive integer so that the number is equal
to the sum of the positive integer and the excluded integer modulo the
upper bound of the range. (Contributed by AV, 19-Mar-2021.)
|
..^
..^ ..^ |
|
Theorem | modsumfzodifsn 10352 |
The sum of a number within a half-open range of positive integers is an
element of the corresponding open range of nonnegative integers with one
excluded integer modulo the excluded integer. (Contributed by AV,
19-Mar-2021.)
|
..^
..^
..^ |
|
Theorem | modlteq 10353 |
Two nonnegative integers less than the modulus are equal iff they are
equal modulo the modulus. (Contributed by AV, 14-Mar-2021.)
|
..^ ..^
|
|
Theorem | addmodlteq 10354 |
Two nonnegative integers less than the modulus are equal iff the sums of
these integer with another integer are equal modulo the modulus.
(Contributed by AV, 20-Mar-2021.)
|
..^ ..^
|
|
4.6.3 Miscellaneous theorems about
integers
|
|
Theorem | frec2uz0d 10355* |
The mapping is a
one-to-one mapping from onto upper
integers that will be used to construct a recursive definition
generator. Ordinal natural number 0 maps to complex number
(normally 0 for the upper integers or 1 for the upper integers
), 1 maps to
+ 1, etc. This
theorem shows the value of
at ordinal
natural number zero. (Contributed by Jim Kingdon,
16-May-2020.)
|
frec
|
|
Theorem | frec2uzzd 10356* |
The value of (see frec2uz0d 10355) is an integer. (Contributed by
Jim Kingdon, 16-May-2020.)
|
frec
|
|
Theorem | frec2uzsucd 10357* |
The value of (see frec2uz0d 10355) at a successor. (Contributed by
Jim Kingdon, 16-May-2020.)
|
frec
|
|
Theorem | frec2uzuzd 10358* |
The value (see frec2uz0d 10355) at an ordinal natural number is in
the upper integers. (Contributed by Jim Kingdon, 16-May-2020.)
|
frec
|
|
Theorem | frec2uzltd 10359* |
Less-than relation for (see frec2uz0d 10355). (Contributed by Jim
Kingdon, 16-May-2020.)
|
frec
|
|
Theorem | frec2uzlt2d 10360* |
The mapping (see frec2uz0d 10355) preserves order. (Contributed by
Jim Kingdon, 16-May-2020.)
|
frec
|
|
Theorem | frec2uzrand 10361* |
Range of (see frec2uz0d 10355). (Contributed by Jim Kingdon,
17-May-2020.)
|
frec
|
|
Theorem | frec2uzf1od 10362* |
(see frec2uz0d 10355) is a one-to-one onto mapping. (Contributed
by Jim Kingdon, 17-May-2020.)
|
frec
|
|
Theorem | frec2uzisod 10363* |
(see frec2uz0d 10355) is an isomorphism from natural ordinals to
upper integers. (Contributed by Jim Kingdon, 17-May-2020.)
|
frec
|
|
Theorem | frecuzrdgrrn 10364* |
The function (used in
the definition of the recursive
definition generator on upper integers) yields ordered pairs of
integers and elements of . (Contributed by Jim Kingdon,
28-Mar-2022.)
|
frec
frec |
|
Theorem | frec2uzrdg 10365* |
A helper lemma for the value of a recursive definition generator on
upper integers (typically either or ) with
characteristic function and initial
value .
This lemma shows that evaluating at an element of
gives an ordered pair whose first element is the index (translated
from
to ).
See comment in frec2uz0d 10355
which describes and the index translation. (Contributed by
Jim Kingdon, 24-May-2020.)
|
frec
frec |
|
Theorem | frecuzrdgrcl 10366* |
The function (used in
the definition of the recursive definition
generator on upper integers) is a function defined for all natural
numbers. (Contributed by Jim Kingdon, 1-Apr-2022.)
|
frec
frec
|
|
Theorem | frecuzrdglem 10367* |
A helper lemma for the value of a recursive definition generator on
upper integers. (Contributed by Jim Kingdon, 26-May-2020.)
|
frec
frec
|
|
Theorem | frecuzrdgtcl 10368* |
The recursive definition generator on upper integers is a function.
See comment in frec2uz0d 10355 for the description of as the
mapping from to . (Contributed by Jim
Kingdon, 26-May-2020.)
|
frec
frec
|
|
Theorem | frecuzrdg0 10369* |
Initial value of a recursive definition generator on upper integers.
See comment in frec2uz0d 10355 for the description of as the
mapping from to . (Contributed by Jim
Kingdon, 27-May-2020.)
|
frec
frec
|
|
Theorem | frecuzrdgsuc 10370* |
Successor value of a recursive definition generator on upper
integers. See comment in frec2uz0d 10355 for the description of
as the mapping from to . (Contributed
by Jim Kingdon, 28-May-2020.)
|
frec
frec
|
|
Theorem | frecuzrdgrclt 10371* |
The function (used in
the definition of the recursive definition
generator on upper integers) yields ordered pairs of integers and
elements of .
Similar to frecuzrdgrcl 10366 except that and
need not be
the same. (Contributed by Jim Kingdon,
22-Apr-2022.)
|
frec
|
|
Theorem | frecuzrdgg 10372* |
Lemma for other theorems involving the the recursive definition
generator on upper integers. Evaluating at a natural number
gives an ordered pair whose first element is the mapping of that
natural number via . (Contributed by Jim Kingdon,
23-Apr-2022.)
|
frec
frec |
|
Theorem | frecuzrdgdomlem 10373* |
The domain of the result of the recursive definition generator on
upper integers. (Contributed by Jim Kingdon, 24-Apr-2022.)
|
frec
frec
|
|
Theorem | frecuzrdgdom 10374* |
The domain of the result of the recursive definition generator on
upper integers. (Contributed by Jim Kingdon, 24-Apr-2022.)
|
frec
|
|
Theorem | frecuzrdgfunlem 10375* |
The recursive definition generator on upper integers produces a a
function. (Contributed by Jim Kingdon, 24-Apr-2022.)
|
frec
frec
|
|
Theorem | frecuzrdgfun 10376* |
The recursive definition generator on upper integers produces a a
function. (Contributed by Jim Kingdon, 24-Apr-2022.)
|
frec
|
|
Theorem | frecuzrdgtclt 10377* |
The recursive definition generator on upper integers is a function.
(Contributed by Jim Kingdon, 22-Apr-2022.)
|
frec
|
|
Theorem | frecuzrdg0t 10378* |
Initial value of a recursive definition generator on upper integers.
(Contributed by Jim Kingdon, 28-Apr-2022.)
|
frec
|
|
Theorem | frecuzrdgsuctlem 10379* |
Successor value of a recursive definition generator on upper integers.
See comment in frec2uz0d 10355 for the description of as the mapping
from to
.
(Contributed by Jim Kingdon,
29-Apr-2022.)
|
frec
frec
|
|
Theorem | frecuzrdgsuct 10380* |
Successor value of a recursive definition generator on upper integers.
(Contributed by Jim Kingdon, 29-Apr-2022.)
|
frec
|
|
Theorem | uzenom 10381 |
An upper integer set is denumerable. (Contributed by Mario Carneiro,
15-Oct-2015.)
|
|
|
Theorem | frecfzennn 10382 |
The cardinality of a finite set of sequential integers. (See
frec2uz0d 10355 for a description of the hypothesis.)
(Contributed by Jim
Kingdon, 18-May-2020.)
|
frec
|
|
Theorem | frecfzen2 10383 |
The cardinality of a finite set of sequential integers with arbitrary
endpoints. (Contributed by Jim Kingdon, 18-May-2020.)
|
frec
|
|
Theorem | frechashgf1o 10384 |
maps one-to-one onto . (Contributed by
Jim
Kingdon, 19-May-2020.)
|
frec |
|
Theorem | frec2uzled 10385* |
The mapping (see frec2uz0d 10355) preserves order. (Contributed by
Jim Kingdon, 24-Feb-2022.)
|
frec
|
|
Theorem | fzfig 10386 |
A finite interval of integers is finite. (Contributed by Jim Kingdon,
19-May-2020.)
|
|
|
Theorem | fzfigd 10387 |
Deduction form of fzfig 10386. (Contributed by Jim Kingdon,
21-May-2020.)
|
|
|
Theorem | fzofig 10388 |
Half-open integer sets are finite. (Contributed by Jim Kingdon,
21-May-2020.)
|
..^
|
|
Theorem | nn0ennn 10389 |
The nonnegative integers are equinumerous to the positive integers.
(Contributed by NM, 19-Jul-2004.)
|
|
|
Theorem | nnenom 10390 |
The set of positive integers (as a subset of complex numbers) is
equinumerous to omega (the set of natural numbers as ordinals).
(Contributed by NM, 31-Jul-2004.) (Revised by Mario Carneiro,
15-Sep-2013.)
|
|
|
Theorem | nnct 10391 |
is dominated by
. (Contributed by
Thierry Arnoux,
29-Dec-2016.)
|
|
|
Theorem | uzennn 10392 |
An upper integer set is equinumerous to the set of natural numbers.
(Contributed by Jim Kingdon, 30-Jul-2023.)
|
|
|
Theorem | fnn0nninf 10393* |
A function from
into ℕ∞. (Contributed by Jim Kingdon,
16-Jul-2022.)
|
frec
ℕ∞ |
|
Theorem | fxnn0nninf 10394* |
A function from NN0* into ℕ∞. (Contributed by Jim
Kingdon,
16-Jul-2022.) TODO: use infnninf 7100 instead of infnninfOLD 7101. More
generally, this theorem and most theorems in this section could use an
extended
defined by
frec
and
as in nnnninf2 7103.
|
frec
NN0*ℕ∞ |
|
Theorem | 0tonninf 10395* |
The mapping of zero into ℕ∞ is the sequence of all
zeroes.
(Contributed by Jim Kingdon, 17-Jul-2022.)
|
frec
|
|
Theorem | 1tonninf 10396* |
The mapping of one into ℕ∞ is a sequence which is a one
followed by zeroes. (Contributed by Jim Kingdon, 17-Jul-2022.)
|
frec
|
|
Theorem | inftonninf 10397* |
The mapping of
into ℕ∞ is the sequence of all ones.
(Contributed by Jim Kingdon, 17-Jul-2022.)
|
frec
|
|
4.6.4 Strong induction over upper sets of
integers
|
|
Theorem | uzsinds 10398* |
Strong (or "total") induction principle over an upper set of
integers.
(Contributed by Scott Fenton, 16-May-2014.)
|
|
|
Theorem | nnsinds 10399* |
Strong (or "total") induction principle over the naturals.
(Contributed
by Scott Fenton, 16-May-2014.)
|
|
|
Theorem | nn0sinds 10400* |
Strong (or "total") induction principle over the nonnegative
integers.
(Contributed by Scott Fenton, 16-May-2014.)
|
|