Type | Label | Description |
Statement |
|
Theorem | qnumcl 12201 |
The canonical numerator of a rational is an integer. (Contributed by
Stefan O'Rear, 13-Sep-2014.)
|
 numer    |
|
Theorem | qdencl 12202 |
The canonical denominator is a positive integer. (Contributed by Stefan
O'Rear, 13-Sep-2014.)
|
 denom    |
|
Theorem | fnum 12203 |
Canonical numerator defines a function. (Contributed by Stefan O'Rear,
13-Sep-2014.)
|
numer    |
|
Theorem | fden 12204 |
Canonical denominator defines a function. (Contributed by Stefan
O'Rear, 13-Sep-2014.)
|
denom    |
|
Theorem | qnumdenbi 12205 |
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 12206 |
The canonical representation of a rational is fully reduced.
(Contributed by Stefan O'Rear, 13-Sep-2014.)
|
  numer  denom  
  |
|
Theorem | qeqnumdivden 12207 |
Recover a rational number from its canonical representation.
(Contributed by Stefan O'Rear, 13-Sep-2014.)
|
  numer  denom     |
|
Theorem | qmuldeneqnum 12208 |
Multiplying a rational by its denominator results in an integer.
(Contributed by Stefan O'Rear, 13-Sep-2014.)
|
  denom   numer    |
|
Theorem | divnumden 12209 |
Calculate the reduced form of a quotient using . (Contributed
by Stefan O'Rear, 13-Sep-2014.)
|
    numer 
      denom   
       |
|
Theorem | divdenle 12210 |
Reducing a quotient never increases the denominator. (Contributed by
Stefan O'Rear, 13-Sep-2014.)
|
   denom      |
|
Theorem | qnumgt0 12211 |
A rational is positive iff its canonical numerator is. (Contributed by
Stefan O'Rear, 15-Sep-2014.)
|
  numer     |
|
Theorem | qgt0numnn 12212 |
A rational is positive iff its canonical numerator is a positive
integer. (Contributed by Stefan O'Rear, 15-Sep-2014.)
|
   numer    |
|
Theorem | nn0gcdsq 12213 |
Squaring commutes with GCD, in particular two coprime numbers have
coprime squares. (Contributed by Stefan O'Rear, 15-Sep-2014.)
|
                     |
|
Theorem | zgcdsq 12214 |
nn0gcdsq 12213 extended to integers by symmetry.
(Contributed by Stefan
O'Rear, 15-Sep-2014.)
|
                     |
|
Theorem | numdensq 12215 |
Squaring a rational squares its canonical components. (Contributed by
Stefan O'Rear, 15-Sep-2014.)
|
  numer       numer    
denom       denom        |
|
Theorem | numsq 12216 |
Square commutes with canonical numerator. (Contributed by Stefan
O'Rear, 15-Sep-2014.)
|
 numer       numer       |
|
Theorem | densq 12217 |
Square commutes with canonical denominator. (Contributed by Stefan
O'Rear, 15-Sep-2014.)
|
 denom       denom       |
|
Theorem | qden1elz 12218 |
A rational is an integer iff it has denominator 1. (Contributed by
Stefan O'Rear, 15-Sep-2014.)
|
  denom 
   |
|
Theorem | nn0sqrtelqelz 12219 |
If a nonnegative integer has a rational square root, that root must be
an integer. (Contributed by Jim Kingdon, 24-May-2022.)
|
     
    
  |
|
Theorem | nonsq 12220 |
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 12221 |
Extend class notation with the order function on the class of integers
modulo N.
|
  |
|
Syntax | cphi 12222 |
Extend class notation with the Euler phi function.
|
 |
|
Definition | df-odz 12223* |
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 12224* |
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 12225* |
Finiteness of an expression used to define the Euler function.
(Contributed by Jim Kingon, 28-May-2022.)
|
       
   |
|
Theorem | phival 12226* |
Value of the Euler function. (Contributed by Mario Carneiro,
23-Feb-2014.)
|
    
♯     
      |
|
Theorem | phicl2 12227 |
Bounds and closure for the value of the Euler function.
(Contributed by Mario Carneiro, 23-Feb-2014.)
|
    
      |
|
Theorem | phicl 12228 |
Closure for the value of the Euler function. (Contributed by
Mario Carneiro, 28-Feb-2014.)
|
    
  |
|
Theorem | phibndlem 12229* |
Lemma for phibnd 12230. (Contributed by Mario Carneiro,
23-Feb-2014.)
|
     
     
         |
|
Theorem | phibnd 12230 |
A slightly tighter bound on the value of the Euler function.
(Contributed by Mario Carneiro, 23-Feb-2014.)
|
             |
|
Theorem | phicld 12231 |
Closure for the value of the Euler function. (Contributed by
Mario Carneiro, 29-May-2016.)
|
         |
|
Theorem | phi1 12232 |
Value of the Euler function at 1. (Contributed by Mario Carneiro,
23-Feb-2014.)
|
     |
|
Theorem | dfphi2 12233* |
Alternate definition of the Euler function. (Contributed by
Mario Carneiro, 23-Feb-2014.) (Revised by Mario Carneiro,
2-May-2016.)
|
    
♯   ..^       |
|
Theorem | hashdvds 12234* |
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 12235 |
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 12236 |
Value of the Euler function at a prime. (Contributed by Mario
Carneiro, 28-Feb-2014.)
|
         |
|
Theorem | crth 12237* |
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 12238* |
Lemma for phimul 12239. (Contributed by Mario Carneiro,
24-Feb-2014.)
|
 ..^     ..^  ..^      
       
    ..^   
  ..^   
                         |
|
Theorem | phimul 12239 |
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 12240* |
Lemma for eulerth 12246. (Contributed by Mario Carneiro,
8-May-2015.)
|
 
      ..^            
                      |
|
Theorem | eulerthlemfi 12241* |
Lemma for eulerth 12246. The set is finite. (Contributed by Mario
Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 7-Sep-2024.)
|
 
      ..^       |
|
Theorem | eulerthlemrprm 12242* |
Lemma for eulerth 12246. and
              are relatively prime.
(Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim
Kingdon, 2-Sep-2024.)
|
 
      ..^                  
                  |
|
Theorem | eulerthlema 12243* |
Lemma for eulerth 12246. (Contributed by Mario Carneiro,
28-Feb-2014.)
(Revised by Jim Kingdon, 2-Sep-2024.)
|
 
      ..^                  
                           
                    |
|
Theorem | eulerthlemh 12244* |
Lemma for eulerth 12246. A permutation of         .
(Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim
Kingdon, 5-Sep-2024.)
|
 
      ..^                 
                                            |
|
Theorem | eulerthlemth 12245* |
Lemma for eulerth 12246. The result. (Contributed by Mario
Carneiro,
28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.)
|
 
      ..^                  
        
     |
|
Theorem | eulerth 12246 |
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 12247 |
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 12248 |
Show an explicit expression for the modular inverse of .
(Contributed by Mario Carneiro, 24-Jan-2015.)
|
                         |
|
Theorem | prmdiveq 12249 |
The modular inverse of is unique. (Contributed
by Mario
Carneiro, 24-Jan-2015.)
|
                     
 
   |
|
Theorem | prmdivdiv 12250 |
The (modular) inverse of the inverse of a number is itself.
(Contributed by Mario Carneiro, 24-Jan-2015.)
|
                           |
|
Theorem | hashgcdlem 12251* |
A correspondence between elements of specific GCD and relative primes in
a smaller ring. (Contributed by Stefan O'Rear, 12-Sep-2015.)
|
  ..^    
  
  ..^     
   
       |
|
Theorem | hashgcdeq 12252* |
Number of initial positive integers with specified divisors.
(Contributed by Stefan O'Rear, 12-Sep-2015.)
|
   ♯   ..^                  |
|
Theorem | phisum 12253* |
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 12254* |
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 12255 |
- Lemma for odzcl 12256, 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 12256 |
The order of a group element is an integer. (Contributed by Mario
Carneiro, 28-Feb-2014.)
|
   
         
  |
|
Theorem | odzid 12257 |
Any element raised to the power of its order is . (Contributed by
Mario Carneiro, 28-Feb-2014.)
|
   

                 |
|
Theorem | odzdvds 12258 |
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 12259 |
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 12260 |
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 12261 |
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 12262 |
Show an explicit expression for the modular inverse of .
This is an application of prmdiv 12248. (Contributed by Alexander van der
Vekens, 15-May-2018.)
|
                         |
|
Theorem | modprminveq 12263 |
The modular inverse of is unique. (Contributed
by Alexander
van der Vekens, 17-May-2018.)
|
                       
   |
|
Theorem | vfermltl 12264 |
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 12265 |
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 12266* |
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 12267* |
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 12268* |
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 12269* |
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 12270 |
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 12271 |
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 12272 |
A prime not equal to is
odd. (Contributed by Mario Carneiro,
4-Feb-2015.) (Proof shortened by AV, 10-Jul-2022.)
|
    
      |
|
Theorem | nnoddn2prm 12273 |
A prime not equal to is
an odd positive integer. (Contributed by
AV, 28-Jun-2021.)
|
    
    |
|
Theorem | oddn2prm 12274 |
A prime not equal to is
odd. (Contributed by AV, 28-Jun-2021.)
|
    
  |
|
Theorem | nnoddn2prmb 12275 |
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 12276 |
A prime less than 5 is either 2 or 3. (Contributed by AV, 5-Jul-2021.)
|
  

   |
|
Theorem | prm23ge5 12277 |
A prime is either 2 or 3 or greater than or equal to 5. (Contributed by
AV, 5-Jul-2021.)
|
 
       |
|
Theorem | pythagtriplem1 12278* |
Lemma for pythagtrip 12296. 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 12279* |
Lemma for pythagtrip 12296. 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 12280 |
Lemma for pythagtrip 12296. 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 12281 |
Lemma for pythagtrip 12296. Show that and are relatively
prime. (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario
Carneiro, 19-Apr-2014.)
|
   
             
       
     |
|
Theorem | pythagtriplem10 12282 |
Lemma for pythagtrip 12296. Show that is
positive. (Contributed
by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro,
19-Apr-2014.)
|
   
                   |
|
Theorem | pythagtriplem6 12283 |
Lemma for pythagtrip 12296. Calculate       .
(Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro,
19-Apr-2014.)
|
   
             
             
   |
|
Theorem | pythagtriplem7 12284 |
Lemma for pythagtrip 12296. Calculate       .
(Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro,
19-Apr-2014.)
|
   
             
             
   |
|
Theorem | pythagtriplem8 12285 |
Lemma for pythagtrip 12296. Show that       is a
positive integer. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised
by Mario Carneiro, 19-Apr-2014.)
|
   
             
             |
|
Theorem | pythagtriplem9 12286 |
Lemma for pythagtrip 12296. Show that       is a
positive integer. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised
by Mario Carneiro, 19-Apr-2014.)
|
   
             
             |
|
Theorem | pythagtriplem11 12287 |
Lemma for pythagtrip 12296. 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 12288 |
Lemma for pythagtrip 12296. Calculate the square of . (Contributed
by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro,
19-Apr-2014.)
|
     
             
             
               |
|
Theorem | pythagtriplem13 12289 |
Lemma for pythagtrip 12296. 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 12290 |
Lemma for pythagtrip 12296. Calculate the square of . (Contributed
by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro,
19-Apr-2014.)
|
     
             
             
               |
|
Theorem | pythagtriplem15 12291 |
Lemma for pythagtrip 12296. Show the relationship between , ,
and .
(Contributed by Scott Fenton, 17-Apr-2014.) (Revised by
Mario Carneiro, 19-Apr-2014.)
|
     
               
             
             
    
            |
|
Theorem | pythagtriplem16 12292 |
Lemma for pythagtrip 12296. Show the relationship between , ,
and .
(Contributed by Scott Fenton, 17-Apr-2014.) (Revised by
Mario Carneiro, 19-Apr-2014.)
|
     
               
             
             
    
      |
|
Theorem | pythagtriplem17 12293 |
Lemma for pythagtrip 12296. Show the relationship between , ,
and .
(Contributed by Scott Fenton, 17-Apr-2014.) (Revised by
Mario Carneiro, 19-Apr-2014.)
|
     
               
             
             
    
            |
|
Theorem | pythagtriplem18 12294* |
Lemma for pythagtrip 12296. Wrap the previous and up in
quantifiers. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by
Mario Carneiro, 19-Apr-2014.)
|
   
             
     
 
                           |
|
Theorem | pythagtriplem19 12295* |
Lemma for pythagtrip 12296. Introduce and remove the relative
primality requirement. (Contributed by Scott Fenton, 18-Apr-2014.)
(Revised by Mario Carneiro, 19-Apr-2014.)
|
   
             
    
   
                                 |
|
Theorem | pythagtrip 12296* |
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.2.8 The prime count function
|
|
Syntax | cpc 12297 |
Extend class notation with the prime count function.
|
 |
|
Definition | df-pc 12298* |
Define the prime count function, which returns the largest exponent of a
given prime (or other positive integer) that divides the number. For
rational numbers, it returns negative values according to the power of a
prime in the denominator. (Contributed by Mario Carneiro,
23-Feb-2014.)
|
             
             
             |
|
Theorem | pclem0 12299* |
Lemma for the prime power pre-function's properties. (Contributed by
Mario Carneiro, 23-Feb-2014.) (Revised by Jim Kingdon,
7-Oct-2024.)
|
              
  |
|
Theorem | pclemub 12300* |
Lemma for the prime power pre-function's properties. (Contributed by
Mario Carneiro, 23-Feb-2014.) (Revised by Jim Kingdon,
7-Oct-2024.)
|
              
    |