Theorem List for Intuitionistic Logic Explorer - 12301-12400 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | pythagtrip 12301* |
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 12302 |
Extend class notation with the prime count function.
|
 |
|
Definition | df-pc 12303* |
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 12304* |
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 12305* |
Lemma for the prime power pre-function's properties. (Contributed by
Mario Carneiro, 23-Feb-2014.) (Revised by Jim Kingdon,
7-Oct-2024.)
|
              
    |
|
Theorem | pclemdc 12306* |
Lemma for the prime power pre-function's properties. (Contributed by
Jim Kingdon, 8-Oct-2024.)
|
              
 DECID
  |
|
Theorem | pcprecl 12307* |
Closure of the prime power pre-function. (Contributed by Mario
Carneiro, 23-Feb-2014.)
|
                  

       |
|
Theorem | pcprendvds 12308* |
Non-divisibility property of the prime power pre-function.
(Contributed by Mario Carneiro, 23-Feb-2014.)
|
                  
        |
|
Theorem | pcprendvds2 12309* |
Non-divisibility property of the prime power pre-function.
(Contributed by Mario Carneiro, 23-Feb-2014.)
|
                  

       |
|
Theorem | pcpre1 12310* |
Value of the prime power pre-function at 1. (Contributed by Mario
Carneiro, 23-Feb-2014.) (Revised by Mario Carneiro, 26-Apr-2016.)
|
                   |
|
Theorem | pcpremul 12311* |
Multiplicative property of the prime count pre-function. Note that the
primality of
is essential for this property;  
but     
 . Since
this is needed to show uniqueness for the real prime count function
(over ), we
don't bother to define it off the primes.
(Contributed by Mario Carneiro, 23-Feb-2014.)
|
  
                              
  
  

  |
|
Theorem | pceulem 12312* |
Lemma for pceu 12313. (Contributed by Mario Carneiro,
23-Feb-2014.)
|
  
                                          
       
             |
|
Theorem | pceu 12313* |
Uniqueness for the prime power function. (Contributed by Mario
Carneiro, 23-Feb-2014.)
|
  
                          
       |
|
Theorem | pcval 12314* |
The value of the prime power function. (Contributed by Mario Carneiro,
23-Feb-2014.) (Revised by Mario Carneiro, 3-Oct-2014.)
|
  
                           
  


     |
|
Theorem | pczpre 12315* |
Connect the prime count pre-function to the actual prime count function,
when restricted to the integers. (Contributed by Mario Carneiro,
23-Feb-2014.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)
|
  
        
   
   |
|
Theorem | pczcl 12316 |
Closure of the prime power function. (Contributed by Mario Carneiro,
23-Feb-2014.)
|
         |
|
Theorem | pccl 12317 |
Closure of the prime power function. (Contributed by Mario Carneiro,
23-Feb-2014.)
|
       |
|
Theorem | pccld 12318 |
Closure of the prime power function. (Contributed by Mario Carneiro,
29-May-2016.)
|
     
   |
|
Theorem | pcmul 12319 |
Multiplication property of the prime power function. (Contributed by
Mario Carneiro, 23-Feb-2014.)
|
   
   
           |
|
Theorem | pcdiv 12320 |
Division property of the prime power function. (Contributed by Mario
Carneiro, 1-Mar-2014.)
|
   

   
        |
|
Theorem | pcqmul 12321 |
Multiplication property of the prime power function. (Contributed by
Mario Carneiro, 9-Sep-2014.)
|
   
   
           |
|
Theorem | pc0 12322 |
The value of the prime power function at zero. (Contributed by Mario
Carneiro, 3-Oct-2014.)
|
 
   |
|
Theorem | pc1 12323 |
Value of the prime count function at 1. (Contributed by Mario Carneiro,
23-Feb-2014.)
|
 
   |
|
Theorem | pcqcl 12324 |
Closure of the general prime count function. (Contributed by Mario
Carneiro, 23-Feb-2014.)
|
         |
|
Theorem | pcqdiv 12325 |
Division property of the prime power function. (Contributed by Mario
Carneiro, 10-Aug-2015.)
|
   
   
           |
|
Theorem | pcrec 12326 |
Prime power of a reciprocal. (Contributed by Mario Carneiro,
10-Aug-2015.)
|
              |
|
Theorem | pcexp 12327 |
Prime power of an exponential. (Contributed by Mario Carneiro,
10-Aug-2015.)
|
   

     
      |
|
Theorem | pcxnn0cl 12328 |
Extended nonnegative integer closure of the general prime count
function. (Contributed by Jim Kingdon, 13-Oct-2024.)
|
     NN0* |
|
Theorem | pcxcl 12329 |
Extended real closure of the general prime count function. (Contributed
by Mario Carneiro, 3-Oct-2014.)
|
       |
|
Theorem | pcge0 12330 |
The prime count of an integer is greater than or equal to zero.
(Contributed by Mario Carneiro, 3-Oct-2014.)
|
       |
|
Theorem | pczdvds 12331 |
Defining property of the prime count function. (Contributed by Mario
Carneiro, 9-Sep-2014.)
|
             |
|
Theorem | pcdvds 12332 |
Defining property of the prime count function. (Contributed by Mario
Carneiro, 23-Feb-2014.)
|
        
  |
|
Theorem | pczndvds 12333 |
Defining property of the prime count function. (Contributed by Mario
Carneiro, 3-Oct-2014.)
|
               |
|
Theorem | pcndvds 12334 |
Defining property of the prime count function. (Contributed by Mario
Carneiro, 23-Feb-2014.)
|
  
          |
|
Theorem | pczndvds2 12335 |
The remainder after dividing out all factors of is not divisible
by .
(Contributed by Mario Carneiro, 9-Sep-2014.)
|
               |
|
Theorem | pcndvds2 12336 |
The remainder after dividing out all factors of is not divisible
by .
(Contributed by Mario Carneiro, 23-Feb-2014.)
|
  
          |
|
Theorem | pcdvdsb 12337 |
  divides if and only if is at most the count of
. (Contributed
by Mario Carneiro, 3-Oct-2014.)
|
         
   |
|
Theorem | pcelnn 12338 |
There are a positive number of powers of a prime in iff
divides .
(Contributed by Mario Carneiro, 23-Feb-2014.)
|
         |
|
Theorem | pceq0 12339 |
There are zero powers of a prime in iff
does not divide
. (Contributed
by Mario Carneiro, 23-Feb-2014.)
|
     
   |
|
Theorem | pcidlem 12340 |
The prime count of a prime power. (Contributed by Mario Carneiro,
12-Mar-2014.)
|
           |
|
Theorem | pcid 12341 |
The prime count of a prime power. (Contributed by Mario Carneiro,
9-Sep-2014.)
|
           |
|
Theorem | pcneg 12342 |
The prime count of a negative number. (Contributed by Mario Carneiro,
13-Mar-2014.)
|
      
   |
|
Theorem | pcabs 12343 |
The prime count of an absolute value. (Contributed by Mario Carneiro,
13-Mar-2014.)
|
             |
|
Theorem | pcdvdstr 12344 |
The prime count increases under the divisibility relation. (Contributed
by Mario Carneiro, 13-Mar-2014.)
|
  
 
      |
|
Theorem | pcgcd1 12345 |
The prime count of a GCD is the minimum of the prime counts of the
arguments. (Contributed by Mario Carneiro, 3-Oct-2014.)
|
  
  
   
       |
|
Theorem | pcgcd 12346 |
The prime count of a GCD is the minimum of the prime counts of the
arguments. (Contributed by Mario Carneiro, 3-Oct-2014.)
|
         
            |
|
Theorem | pc2dvds 12347* |
A characterization of divisibility in terms of prime count.
(Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by Mario
Carneiro, 3-Oct-2014.)
|
     
      |
|
Theorem | pc11 12348* |
The prime count function, viewed as a function from to
  , is one-to-one. (Contributed by Mario Carneiro,
23-Feb-2014.)
|
            |
|
Theorem | pcz 12349* |
The prime count function can be used as an indicator that a given
rational number is an integer. (Contributed by Mario Carneiro,
23-Feb-2014.)
|
  

    |
|
Theorem | pcprmpw2 12350* |
Self-referential expression for a prime power. (Contributed by Mario
Carneiro, 16-Jan-2015.)
|
        
         |
|
Theorem | pcprmpw 12351* |
Self-referential expression for a prime power. (Contributed by Mario
Carneiro, 16-Jan-2015.)
|
        
         |
|
Theorem | dvdsprmpweq 12352* |
If a positive integer divides a prime power, it is a prime power.
(Contributed by AV, 25-Jul-2021.)
|
        
       |
|
Theorem | dvdsprmpweqnn 12353* |
If an integer greater than 1 divides a prime power, it is a (proper)
prime power. (Contributed by AV, 13-Aug-2021.)
|
     
 
    
       |
|
Theorem | dvdsprmpweqle 12354* |
If a positive integer divides a prime power, it is a prime power with a
smaller exponent. (Contributed by AV, 25-Jul-2021.)
|
        
         |
|
Theorem | difsqpwdvds 12355 |
If the difference of two squares is a power of a prime, the prime
divides twice the second squared number. (Contributed by AV,
13-Aug-2021.)
|
  
     
              
     |
|
Theorem | pcaddlem 12356 |
Lemma for pcadd 12357. The original numbers and have been
decomposed using the prime count function as      
where  are both not divisible by and

 , and similarly for . (Contributed by Mario
Carneiro, 9-Sep-2014.)
|
                      
      
  
             
    |
|
Theorem | pcadd 12357 |
An inequality for the prime count of a sum. This is the source of the
ultrametric inequality for the p-adic metric. (Contributed by Mario
Carneiro, 9-Sep-2014.)
|
         
     
     |
|
Theorem | pcmptcl 12358 |
Closure for the prime power map. (Contributed by Mario Carneiro,
12-Mar-2014.)
|
  
                           |
|
Theorem | pcmpt 12359* |
Construct a function with given prime count characteristics.
(Contributed by Mario Carneiro, 12-Mar-2014.)
|
  
               
 
               |
|
Theorem | pcmpt2 12360* |
Dividing two prime count maps yields a number with all dividing primes
confined to an interval. (Contributed by Mario Carneiro,
14-Mar-2014.)
|
  
               
 
         
              
      |
|
Theorem | pcmptdvds 12361 |
The partial products of the prime power map form a divisibility chain.
(Contributed by Mario Carneiro, 12-Mar-2014.)
|
  
                   
 
            |
|
Theorem | pcprod 12362* |
The product of the primes taken to their respective powers reconstructs
the original number. (Contributed by Mario Carneiro, 12-Mar-2014.)
|
  
                   |
|
Theorem | sumhashdc 12363* |
The sum of 1 over a set is the size of the set. (Contributed by Mario
Carneiro, 8-Mar-2014.) (Revised by Mario Carneiro, 20-May-2014.)
|
 
 DECID        ♯    |
|
Theorem | fldivp1 12364 |
The difference between the floors of adjacent fractions is either 1 or 0.
(Contributed by Mario Carneiro, 8-Mar-2014.)
|
         
           
      |
|
Theorem | pcfaclem 12365 |
Lemma for pcfac 12366. (Contributed by Mario Carneiro,
20-May-2014.)
|
     

            |
|
Theorem | pcfac 12366* |
Calculate the prime count of a factorial. (Contributed by Mario
Carneiro, 11-Mar-2014.) (Revised by Mario Carneiro, 21-May-2014.)
|
     

     
                  |
|
Theorem | pcbc 12367* |
Calculate the prime count of a binomial coefficient. (Contributed by
Mario Carneiro, 11-Mar-2014.) (Revised by Mario Carneiro,
21-May-2014.)
|
     
 
                          
                    |
|
Theorem | qexpz 12368 |
If a power of a rational number is an integer, then the number is an
integer. (Contributed by Mario Carneiro, 10-Aug-2015.)
|
     
   |
|
Theorem | expnprm 12369 |
A second or higher power of a rational number is not a prime number. Or
by contraposition, the n-th root of a prime number is not rational.
Suggested by Norm Megill. (Contributed by Mario Carneiro,
10-Aug-2015.)
|
          
  |
|
Theorem | oddprmdvds 12370* |
Every positive integer which is not a power of two is divisible by an
odd prime number. (Contributed by AV, 6-Aug-2021.)
|
       
 
      |
|
5.2.9 Pocklington's theorem
|
|
Theorem | prmpwdvds 12371 |
A relation involving divisibility by a prime power. (Contributed by
Mario Carneiro, 2-Mar-2014.)
|
    
                        |
|
Theorem | pockthlem 12372 |
Lemma for pockthg 12373. (Contributed by Mario Carneiro,
2-Mar-2014.)
|
         
        
                       
        
     |
|
Theorem | pockthg 12373* |
The generalized Pocklington's theorem. If where
, then is prime if and only if for every prime factor
of , there is an such that
  
   and
         . (Contributed by Mario
Carneiro, 2-Mar-2014.)
|
         
                                 |
|
Theorem | pockthi 12374 |
Pocklington's theorem, which gives a sufficient criterion for a number
to be prime.
This is the preferred method for verifying large
primes, being much more efficient to compute than trial division. This
form has been optimized for application to specific large primes; see
pockthg 12373 for a more general closed-form version.
(Contributed by Mario
Carneiro, 2-Mar-2014.)
|
                               |
|
5.2.10 Infinite primes theorem
|
|
Theorem | infpnlem1 12375* |
Lemma for infpn 12377. The smallest divisor (greater than 1) of
 is a prime greater than . (Contributed by NM,
5-May-2005.)
|
             
         
           |
|
Theorem | infpnlem2 12376* |
Lemma for infpn 12377. For any positive integer , there exists a
prime number
greater than .
(Contributed by NM,
5-May-2005.)
|
        
          |
|
Theorem | infpn 12377* |
There exist infinitely many prime numbers: for any positive integer
, there exists
a prime number greater
than . (See
infpn2 12475 for the equinumerosity version.)
(Contributed by NM,
1-Jun-2006.)
|
  
          |
|
Theorem | prmunb 12378* |
The primes are unbounded. (Contributed by Paul Chapman,
28-Nov-2012.)
|
    |
|
5.2.11 Fundamental theorem of
arithmetic
|
|
Theorem | 1arithlem1 12379* |
Lemma for 1arith 12383. (Contributed by Mario Carneiro,
30-May-2014.)
|
 
    
   
      |
|
Theorem | 1arithlem2 12380* |
Lemma for 1arith 12383. (Contributed by Mario Carneiro,
30-May-2014.)
|
 
              
    |
|
Theorem | 1arithlem3 12381* |
Lemma for 1arith 12383. (Contributed by Mario Carneiro,
30-May-2014.)
|
 
    
          |
|
Theorem | 1arithlem4 12382* |
Lemma for 1arith 12383. (Contributed by Mario Carneiro,
30-May-2014.)
|
 
   
                        

               |
|
Theorem | 1arith 12383* |
Fundamental theorem of arithmetic, where a prime factorization is
represented as a sequence of prime exponents, for which only finitely
many primes have nonzero exponent. The function maps the set of
positive integers one-to-one onto the set of prime factorizations
.
(Contributed by Paul Chapman, 17-Nov-2012.) (Proof shortened
by Mario Carneiro, 30-May-2014.)
|
 
   
              |
|
Theorem | 1arith2 12384* |
Fundamental theorem of arithmetic, where a prime factorization is
represented as a finite monotonic 1-based sequence of primes. Every
positive integer has a unique prime factorization. Theorem 1.10 in
[ApostolNT] p. 17. This is Metamath
100 proof #80. (Contributed by
Paul Chapman, 17-Nov-2012.) (Revised by Mario Carneiro,
30-May-2014.)
|
 
   
          
     |
|
5.2.12 Lagrange's four-square
theorem
|
|
Syntax | cgz 12385 |
Extend class notation with the set of gaussian integers.
|
   ![] ]](rbrack.gif) |
|
Definition | df-gz 12386 |
Define the set of gaussian integers, which are complex numbers whose real
and imaginary parts are integers. (Note that the   is
actually
part of the symbol token and has no independent meaning.) (Contributed by
Mario Carneiro, 14-Jul-2014.)
|
        
   
   |
|
Theorem | elgz 12387 |
Elementhood in the gaussian integers. (Contributed by Mario Carneiro,
14-Jul-2014.)
|
        
   
   |
|
Theorem | gzcn 12388 |
A gaussian integer is a complex number. (Contributed by Mario Carneiro,
14-Jul-2014.)
|
      |
|
Theorem | zgz 12389 |
An integer is a gaussian integer. (Contributed by Mario Carneiro,
14-Jul-2014.)
|
    ![] ]](rbrack.gif)  |
|
Theorem | igz 12390 |
is a gaussian
integer. (Contributed by Mario Carneiro,
14-Jul-2014.)
|
   ![] ]](rbrack.gif) |
|
Theorem | gznegcl 12391 |
The gaussian integers are closed under negation. (Contributed by Mario
Carneiro, 14-Jul-2014.)
|
        ![] ]](rbrack.gif)  |
|
Theorem | gzcjcl 12392 |
The gaussian integers are closed under conjugation. (Contributed by Mario
Carneiro, 14-Jul-2014.)
|
           ![] ]](rbrack.gif)  |
|
Theorem | gzaddcl 12393 |
The gaussian integers are closed under addition. (Contributed by Mario
Carneiro, 14-Jul-2014.)
|
    
   ![] ]](rbrack.gif) 
    ![] ]](rbrack.gif)  |
|
Theorem | gzmulcl 12394 |
The gaussian integers are closed under multiplication. (Contributed by
Mario Carneiro, 14-Jul-2014.)
|
    
   ![] ]](rbrack.gif)      ![] ]](rbrack.gif)  |
|
Theorem | gzreim 12395 |
Construct a gaussian integer from real and imaginary parts. (Contributed
by Mario Carneiro, 16-Jul-2014.)
|
    
 
   ![] ]](rbrack.gif)  |
|
Theorem | gzsubcl 12396 |
The gaussian integers are closed under subtraction. (Contributed by Mario
Carneiro, 14-Jul-2014.)
|
    
   ![] ]](rbrack.gif)      ![] ]](rbrack.gif)  |
|
Theorem | gzabssqcl 12397 |
The squared norm of a gaussian integer is an integer. (Contributed by
Mario Carneiro, 16-Jul-2014.)
|
              |
|
Theorem | 4sqlem5 12398 |
Lemma for 4sq (not yet proved here). (Contributed by Mario Carneiro,
15-Jul-2014.)
|
              
        |
|
Theorem | 4sqlem6 12399 |
Lemma for 4sq (not yet proved here) . (Contributed by Mario Carneiro,
15-Jul-2014.)
|
              
         |
|
Theorem | 4sqlem7 12400 |
Lemma for 4sq (not yet proved here) . (Contributed by Mario Carneiro,
15-Jul-2014.)
|
              
              |