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

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

   |
|
Theorem | prm23ge5 12284 |
A prime is either 2 or 3 or greater than or equal to 5. (Contributed by
AV, 5-Jul-2021.)
|
 
       |
|
Theorem | pythagtriplem1 12285* |
Lemma for pythagtrip 12303. 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 12286* |
Lemma for pythagtrip 12303. 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 12287 |
Lemma for pythagtrip 12303. 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 12288 |
Lemma for pythagtrip 12303. Show that and are relatively
prime. (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario
Carneiro, 19-Apr-2014.)
|
   
             
       
     |
|
Theorem | pythagtriplem10 12289 |
Lemma for pythagtrip 12303. Show that is
positive. (Contributed
by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro,
19-Apr-2014.)
|
   
                   |
|
Theorem | pythagtriplem6 12290 |
Lemma for pythagtrip 12303. Calculate       .
(Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro,
19-Apr-2014.)
|
   
             
             
   |
|
Theorem | pythagtriplem7 12291 |
Lemma for pythagtrip 12303. Calculate       .
(Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro,
19-Apr-2014.)
|
   
             
             
   |
|
Theorem | pythagtriplem8 12292 |
Lemma for pythagtrip 12303. Show that       is a
positive integer. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised
by Mario Carneiro, 19-Apr-2014.)
|
   
             
             |
|
Theorem | pythagtriplem9 12293 |
Lemma for pythagtrip 12303. Show that       is a
positive integer. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised
by Mario Carneiro, 19-Apr-2014.)
|
   
             
             |
|
Theorem | pythagtriplem11 12294 |
Lemma for pythagtrip 12303. 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 12295 |
Lemma for pythagtrip 12303. Calculate the square of . (Contributed
by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro,
19-Apr-2014.)
|
     
             
             
               |
|
Theorem | pythagtriplem13 12296 |
Lemma for pythagtrip 12303. 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 12297 |
Lemma for pythagtrip 12303. Calculate the square of . (Contributed
by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro,
19-Apr-2014.)
|
     
             
             
               |
|
Theorem | pythagtriplem15 12298 |
Lemma for pythagtrip 12303. Show the relationship between , ,
and .
(Contributed by Scott Fenton, 17-Apr-2014.) (Revised by
Mario Carneiro, 19-Apr-2014.)
|
     
               
             
             
    
            |
|
Theorem | pythagtriplem16 12299 |
Lemma for pythagtrip 12303. Show the relationship between , ,
and .
(Contributed by Scott Fenton, 17-Apr-2014.) (Revised by
Mario Carneiro, 19-Apr-2014.)
|
     
               
             
             
    
      |
|
Theorem | pythagtriplem17 12300 |
Lemma for pythagtrip 12303. Show the relationship between , ,
and .
(Contributed by Scott Fenton, 17-Apr-2014.) (Revised by
Mario Carneiro, 19-Apr-2014.)
|
     
               
             
             
    
            |