Theorem List for Intuitionistic Logic Explorer - 12201-12300 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | pw2dvds 12201* |
A natural number has a highest power of two which divides it.
(Contributed by Jim Kingdon, 14-Nov-2021.)
|
      
   
 
   |
|
Theorem | pw2dvdseulemle 12202 |
Lemma for pw2dvdseu 12203. Powers of two which do and do not divide a
natural number. (Contributed by Jim Kingdon, 17-Nov-2021.)
|
            
          |
|
Theorem | pw2dvdseu 12203* |
A natural number has a unique highest power of two which divides it.
(Contributed by Jim Kingdon, 16-Nov-2021.)
|
      
   
 
   |
|
Theorem | oddpwdclemxy 12204* |
Lemma for oddpwdc 12209. Another way of stating that decomposing a
natural
number into a power of two and an odd number is unique. (Contributed by
Jim Kingdon, 16-Nov-2021.)
|
   
                                                 |
|
Theorem | oddpwdclemdvds 12205* |
Lemma for oddpwdc 12209. A natural number is divisible by the
highest
power of two which divides it. (Contributed by Jim Kingdon,
17-Nov-2021.)
|
          
     
     |
|
Theorem | oddpwdclemndvds 12206* |
Lemma for oddpwdc 12209. A natural number is not divisible by one
more
than the highest power of two which divides it. (Contributed by Jim
Kingdon, 17-Nov-2021.)
|
                        |
|
Theorem | oddpwdclemodd 12207* |
Lemma for oddpwdc 12209. Removing the powers of two from a natural
number
produces an odd number. (Contributed by Jim Kingdon, 16-Nov-2021.)
|
                        |
|
Theorem | oddpwdclemdc 12208* |
Lemma for oddpwdc 12209. Decomposing a number into odd and even
parts.
(Contributed by Jim Kingdon, 16-Nov-2021.)
|
   
                                                   |
|
Theorem | oddpwdc 12209* |
The function that
decomposes a number into its "odd" and "even"
parts, which is to say the largest power of two and largest odd divisor
of a number, is a bijection from pairs of a nonnegative integer and an
odd number to positive integers. (Contributed by Thierry Arnoux,
15-Aug-2017.)
|
   
              |
|
Theorem | sqpweven 12210* |
The greatest power of two dividing the square of an integer is an even
power of two. (Contributed by Jim Kingdon, 17-Nov-2021.)
|
   
       
               |
|
Theorem | 2sqpwodd 12211* |
The greatest power of two dividing twice the square of an integer is
an odd power of two. (Contributed by Jim Kingdon, 17-Nov-2021.)
|
   
       
                 |
|
Theorem | sqne2sq 12212 |
The square of a natural number can never be equal to two times the
square of a natural number. (Contributed by Jim Kingdon,
17-Nov-2021.)
|
               |
|
Theorem | znege1 12213 |
The absolute value of the difference between two unequal integers is at
least one. (Contributed by Jim Kingdon, 31-Jan-2022.)
|
  
        |
|
Theorem | sqrt2irraplemnn 12214 |
Lemma for sqrt2irrap 12215. The square root of 2 is apart from a
positive
rational expressed as a numerator and denominator. (Contributed by Jim
Kingdon, 2-Oct-2021.)
|
       #     |
|
Theorem | sqrt2irrap 12215 |
The square root of 2 is irrational. That is, for any rational number,
    is apart from it. In the absence of excluded middle,
we can distinguish between this and "the square root of 2 is not
rational" which is sqrt2irr 12197. (Contributed by Jim Kingdon,
2-Oct-2021.)
|
     #   |
|
5.2.4 Properties of the canonical
representation of a rational
|
|
Syntax | cnumer 12216 |
Extend class notation to include canonical numerator function.
|
numer |
|
Syntax | cdenom 12217 |
Extend class notation to include canonical denominator function.
|
denom |
|
Definition | df-numer 12218* |
The canonical numerator of a rational is the numerator of the rational's
reduced fraction representation (no common factors, denominator
positive). (Contributed by Stefan O'Rear, 13-Sep-2014.)
|
numer                    
               |
|
Definition | df-denom 12219* |
The canonical denominator of a rational is the denominator of the
rational's reduced fraction representation (no common factors,
denominator positive). (Contributed by Stefan O'Rear, 13-Sep-2014.)
|
denom                    
               |
|
Theorem | qnumval 12220* |
Value of the canonical numerator function. (Contributed by Stefan
O'Rear, 13-Sep-2014.)
|
 numer      
             
               |
|
Theorem | qdenval 12221* |
Value of the canonical denominator function. (Contributed by Stefan
O'Rear, 13-Sep-2014.)
|
 denom      
             
               |
|
Theorem | qnumdencl 12222 |
Lemma for qnumcl 12223 and qdencl 12224. (Contributed by Stefan O'Rear,
13-Sep-2014.)
|
  numer 
denom     |
|
Theorem | qnumcl 12223 |
The canonical numerator of a rational is an integer. (Contributed by
Stefan O'Rear, 13-Sep-2014.)
|
 numer    |
|
Theorem | qdencl 12224 |
The canonical denominator is a positive integer. (Contributed by Stefan
O'Rear, 13-Sep-2014.)
|
 denom    |
|
Theorem | fnum 12225 |
Canonical numerator defines a function. (Contributed by Stefan O'Rear,
13-Sep-2014.)
|
numer    |
|
Theorem | fden 12226 |
Canonical denominator defines a function. (Contributed by Stefan
O'Rear, 13-Sep-2014.)
|
denom    |
|
Theorem | qnumdenbi 12227 |
Two numbers are the canonical representation of a rational iff they are
coprime and have the right quotient. (Contributed by Stefan O'Rear,
13-Sep-2014.)
|
           numer 
denom      |
|
Theorem | qnumdencoprm 12228 |
The canonical representation of a rational is fully reduced.
(Contributed by Stefan O'Rear, 13-Sep-2014.)
|
  numer  denom  
  |
|
Theorem | qeqnumdivden 12229 |
Recover a rational number from its canonical representation.
(Contributed by Stefan O'Rear, 13-Sep-2014.)
|
  numer  denom     |
|
Theorem | qmuldeneqnum 12230 |
Multiplying a rational by its denominator results in an integer.
(Contributed by Stefan O'Rear, 13-Sep-2014.)
|
  denom   numer    |
|
Theorem | divnumden 12231 |
Calculate the reduced form of a quotient using . (Contributed
by Stefan O'Rear, 13-Sep-2014.)
|
    numer 
      denom   
       |
|
Theorem | divdenle 12232 |
Reducing a quotient never increases the denominator. (Contributed by
Stefan O'Rear, 13-Sep-2014.)
|
   denom      |
|
Theorem | qnumgt0 12233 |
A rational is positive iff its canonical numerator is. (Contributed by
Stefan O'Rear, 15-Sep-2014.)
|
  numer     |
|
Theorem | qgt0numnn 12234 |
A rational is positive iff its canonical numerator is a positive
integer. (Contributed by Stefan O'Rear, 15-Sep-2014.)
|
   numer    |
|
Theorem | nn0gcdsq 12235 |
Squaring commutes with GCD, in particular two coprime numbers have
coprime squares. (Contributed by Stefan O'Rear, 15-Sep-2014.)
|
                     |
|
Theorem | zgcdsq 12236 |
nn0gcdsq 12235 extended to integers by symmetry.
(Contributed by Stefan
O'Rear, 15-Sep-2014.)
|
                     |
|
Theorem | numdensq 12237 |
Squaring a rational squares its canonical components. (Contributed by
Stefan O'Rear, 15-Sep-2014.)
|
  numer       numer    
denom       denom        |
|
Theorem | numsq 12238 |
Square commutes with canonical numerator. (Contributed by Stefan
O'Rear, 15-Sep-2014.)
|
 numer       numer       |
|
Theorem | densq 12239 |
Square commutes with canonical denominator. (Contributed by Stefan
O'Rear, 15-Sep-2014.)
|
 denom       denom       |
|
Theorem | qden1elz 12240 |
A rational is an integer iff it has denominator 1. (Contributed by
Stefan O'Rear, 15-Sep-2014.)
|
  denom 
   |
|
Theorem | nn0sqrtelqelz 12241 |
If a nonnegative integer has a rational square root, that root must be
an integer. (Contributed by Jim Kingdon, 24-May-2022.)
|
     
    
  |
|
Theorem | nonsq 12242 |
Any integer strictly between two adjacent squares has a non-rational
square root. (Contributed by Stefan O'Rear, 15-Sep-2014.)
|
  
                 
  |
|
5.2.5 Euler's theorem
|
|
Syntax | codz 12243 |
Extend class notation with the order function on the class of integers
modulo N.
|
  |
|
Syntax | cphi 12244 |
Extend class notation with the Euler phi function.
|
 |
|
Definition | df-odz 12245* |
Define the order function on the class of integers modulo N.
(Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by AV,
26-Sep-2020.)
|


     inf 
    
       |
|
Definition | df-phi 12246* |
Define the Euler phi function (also called "Euler totient function"),
which counts the number of integers less than and coprime to it,
see definition in [ApostolNT] p. 25.
(Contributed by Mario Carneiro,
23-Feb-2014.)
|
 ♯     
      |
|
Theorem | phivalfi 12247* |
Finiteness of an expression used to define the Euler function.
(Contributed by Jim Kingon, 28-May-2022.)
|
       
   |
|
Theorem | phival 12248* |
Value of the Euler function. (Contributed by Mario Carneiro,
23-Feb-2014.)
|
    
♯     
      |
|
Theorem | phicl2 12249 |
Bounds and closure for the value of the Euler function.
(Contributed by Mario Carneiro, 23-Feb-2014.)
|
    
      |
|
Theorem | phicl 12250 |
Closure for the value of the Euler function. (Contributed by
Mario Carneiro, 28-Feb-2014.)
|
    
  |
|
Theorem | phibndlem 12251* |
Lemma for phibnd 12252. (Contributed by Mario Carneiro,
23-Feb-2014.)
|
     
     
         |
|
Theorem | phibnd 12252 |
A slightly tighter bound on the value of the Euler function.
(Contributed by Mario Carneiro, 23-Feb-2014.)
|
             |
|
Theorem | phicld 12253 |
Closure for the value of the Euler function. (Contributed by
Mario Carneiro, 29-May-2016.)
|
         |
|
Theorem | phi1 12254 |
Value of the Euler function at 1. (Contributed by Mario Carneiro,
23-Feb-2014.)
|
     |
|
Theorem | dfphi2 12255* |
Alternate definition of the Euler function. (Contributed by
Mario Carneiro, 23-Feb-2014.) (Revised by Mario Carneiro,
2-May-2016.)
|
    
♯   ..^       |
|
Theorem | hashdvds 12256* |
The number of numbers in a given residue class in a finite set of
integers. (Contributed by Mario Carneiro, 12-Mar-2014.) (Proof
shortened by Mario Carneiro, 7-Jun-2016.)
|
            
  ♯     
                   
      |
|
Theorem | phiprmpw 12257 |
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 12258 |
Value of the Euler function at a prime. (Contributed by Mario
Carneiro, 28-Feb-2014.)
|
         |
|
Theorem | crth 12259* |
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 12260* |
Lemma for phimul 12261. (Contributed by Mario Carneiro,
24-Feb-2014.)
|
 ..^     ..^  ..^      
       
    ..^   
  ..^   
                         |
|
Theorem | phimul 12261 |
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 12262* |
Lemma for eulerth 12268. (Contributed by Mario Carneiro,
8-May-2015.)
|
 
      ..^            
                      |
|
Theorem | eulerthlemfi 12263* |
Lemma for eulerth 12268. The set is finite. (Contributed by Mario
Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 7-Sep-2024.)
|
 
      ..^       |
|
Theorem | eulerthlemrprm 12264* |
Lemma for eulerth 12268. and
              are relatively prime.
(Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim
Kingdon, 2-Sep-2024.)
|
 
      ..^                  
                  |
|
Theorem | eulerthlema 12265* |
Lemma for eulerth 12268. (Contributed by Mario Carneiro,
28-Feb-2014.)
(Revised by Jim Kingdon, 2-Sep-2024.)
|
 
      ..^                  
                           
                    |
|
Theorem | eulerthlemh 12266* |
Lemma for eulerth 12268. A permutation of         .
(Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim
Kingdon, 5-Sep-2024.)
|
 
      ..^                 
                                            |
|
Theorem | eulerthlemth 12267* |
Lemma for eulerth 12268. The result. (Contributed by Mario
Carneiro,
28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.)
|
 
      ..^                  
        
     |
|
Theorem | eulerth 12268 |
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 12269 |
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 12270 |
Show an explicit expression for the modular inverse of .
(Contributed by Mario Carneiro, 24-Jan-2015.)
|
                         |
|
Theorem | prmdiveq 12271 |
The modular inverse of is unique. (Contributed
by Mario
Carneiro, 24-Jan-2015.)
|
                     
 
   |
|
Theorem | prmdivdiv 12272 |
The (modular) inverse of the inverse of a number is itself.
(Contributed by Mario Carneiro, 24-Jan-2015.)
|
                           |
|
Theorem | hashgcdlem 12273* |
A correspondence between elements of specific GCD and relative primes in
a smaller ring. (Contributed by Stefan O'Rear, 12-Sep-2015.)
|
  ..^    
  
  ..^     
   
       |
|
Theorem | hashgcdeq 12274* |
Number of initial positive integers with specified divisors.
(Contributed by Stefan O'Rear, 12-Sep-2015.)
|
   ♯   ..^                  |
|
Theorem | phisum 12275* |
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 12276* |
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 12277 |
- Lemma for odzcl 12278, 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 12278 |
The order of a group element is an integer. (Contributed by Mario
Carneiro, 28-Feb-2014.)
|
   
         
  |
|
Theorem | odzid 12279 |
Any element raised to the power of its order is . (Contributed by
Mario Carneiro, 28-Feb-2014.)
|
   

                 |
|
Theorem | odzdvds 12280 |
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 12281 |
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 12282 |
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 12283 |
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 12284 |
Show an explicit expression for the modular inverse of .
This is an application of prmdiv 12270. (Contributed by Alexander van der
Vekens, 15-May-2018.)
|
                         |
|
Theorem | modprminveq 12285 |
The modular inverse of is unique. (Contributed
by Alexander
van der Vekens, 17-May-2018.)
|
                       
   |
|
Theorem | vfermltl 12286 |
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 12287 |
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 12288* |
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 12289* |
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 12290* |
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 12291* |
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 12292 |
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 12293 |
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 12294 |
A prime not equal to is
odd. (Contributed by Mario Carneiro,
4-Feb-2015.) (Proof shortened by AV, 10-Jul-2022.)
|
    
      |
|
Theorem | nnoddn2prm 12295 |
A prime not equal to is
an odd positive integer. (Contributed by
AV, 28-Jun-2021.)
|
    
    |
|
Theorem | oddn2prm 12296 |
A prime not equal to is
odd. (Contributed by AV, 28-Jun-2021.)
|
    
  |
|
Theorem | nnoddn2prmb 12297 |
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 12298 |
A prime less than 5 is either 2 or 3. (Contributed by AV, 5-Jul-2021.)
|
  

   |
|
Theorem | prm23ge5 12299 |
A prime is either 2 or 3 or greater than or equal to 5. (Contributed by
AV, 5-Jul-2021.)
|
 
       |
|
Theorem | pythagtriplem1 12300* |
Lemma for pythagtrip 12318. Prove a weaker version of one direction of
the
theorem. (Contributed by Scott Fenton, 28-Mar-2014.) (Revised by Mario
Carneiro, 19-Apr-2014.)
|
    
            
     
                            |