ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  pcpremul Unicode version

Theorem pcpremul 12307
Description: Multiplicative property of the prime count pre-function. Note that the primality of  P is essential for this property;  ( 4  pCnt  2
)  =  0 but  ( 4  pCnt 
( 2  x.  2 ) )  =  1  =/=  2  x.  (
4  pCnt  2 )  =  0. Since this is needed to show uniqueness for the real prime count function (over  QQ), we don't bother to define it off the primes. (Contributed by Mario Carneiro, 23-Feb-2014.)
Hypotheses
Ref Expression
pcpremul.1  |-  S  =  sup ( { n  e.  NN0  |  ( P ^ n )  ||  M } ,  RR ,  <  )
pcpremul.2  |-  T  =  sup ( { n  e.  NN0  |  ( P ^ n )  ||  N } ,  RR ,  <  )
pcpremul.3  |-  U  =  sup ( { n  e.  NN0  |  ( P ^ n )  ||  ( M  x.  N
) } ,  RR ,  <  )
Assertion
Ref Expression
pcpremul  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( S  +  T
)  =  U )
Distinct variable groups:    n, M    n, N    P, n
Allowed substitution hints:    S( n)    T( n)    U( n)

Proof of Theorem pcpremul
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssrab2 3252 . . . . . 6  |-  { n  e.  NN0  |  ( P ^ n )  ||  ( M  x.  N
) }  C_  NN0
2 nn0ssz 9285 . . . . . 6  |-  NN0  C_  ZZ
31, 2sstri 3176 . . . . 5  |-  { n  e.  NN0  |  ( P ^ n )  ||  ( M  x.  N
) }  C_  ZZ
43a1i 9 . . . 4  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  ->  { n  e.  NN0  |  ( P ^ n
)  ||  ( M  x.  N ) }  C_  ZZ )
5 prmuz2 12145 . . . . . 6  |-  ( P  e.  Prime  ->  P  e.  ( ZZ>= `  2 )
)
653ad2ant1 1019 . . . . 5  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  ->  P  e.  ( ZZ>= ` 
2 ) )
7 zmulcl 9320 . . . . . . 7  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( M  x.  N
)  e.  ZZ )
87ad2ant2r 509 . . . . . 6  |-  ( ( ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( M  x.  N
)  e.  ZZ )
983adant1 1016 . . . . 5  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( M  x.  N
)  e.  ZZ )
10 simp2l 1024 . . . . . . . 8  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  ->  M  e.  ZZ )
1110zcnd 9390 . . . . . . 7  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  ->  M  e.  CC )
12 simp3l 1026 . . . . . . . 8  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  ->  N  e.  ZZ )
1312zcnd 9390 . . . . . . 7  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  ->  N  e.  CC )
14 simp2r 1025 . . . . . . . 8  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  ->  M  =/=  0 )
15 0zd 9279 . . . . . . . . 9  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
0  e.  ZZ )
16 zapne 9341 . . . . . . . . 9  |-  ( ( M  e.  ZZ  /\  0  e.  ZZ )  ->  ( M #  0  <->  M  =/=  0 ) )
1710, 15, 16syl2anc 411 . . . . . . . 8  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( M #  0  <->  M  =/=  0 ) )
1814, 17mpbird 167 . . . . . . 7  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  ->  M #  0 )
19 simp3r 1027 . . . . . . . 8  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  ->  N  =/=  0 )
20 zapne 9341 . . . . . . . . 9  |-  ( ( N  e.  ZZ  /\  0  e.  ZZ )  ->  ( N #  0  <->  N  =/=  0 ) )
2112, 15, 20syl2anc 411 . . . . . . . 8  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( N #  0  <->  N  =/=  0 ) )
2219, 21mpbird 167 . . . . . . 7  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  ->  N #  0 )
2311, 13, 18, 22mulap0d 8629 . . . . . 6  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( M  x.  N
) #  0 )
24 zapne 9341 . . . . . . 7  |-  ( ( ( M  x.  N
)  e.  ZZ  /\  0  e.  ZZ )  ->  ( ( M  x.  N ) #  0  <->  ( M  x.  N )  =/=  0
) )
259, 15, 24syl2anc 411 . . . . . 6  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( ( M  x.  N ) #  0  <->  ( M  x.  N )  =/=  0
) )
2623, 25mpbid 147 . . . . 5  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( M  x.  N
)  =/=  0 )
27 eqid 2187 . . . . . 6  |-  { n  e.  NN0  |  ( P ^ n )  ||  ( M  x.  N
) }  =  {
n  e.  NN0  | 
( P ^ n
)  ||  ( M  x.  N ) }
2827pclemdc 12302 . . . . 5  |-  ( ( P  e.  ( ZZ>= ` 
2 )  /\  (
( M  x.  N
)  e.  ZZ  /\  ( M  x.  N
)  =/=  0 ) )  ->  A. x  e.  ZZ DECID  x  e.  { n  e.  NN0  |  ( P ^ n )  ||  ( M  x.  N
) } )
296, 9, 26, 28syl12anc 1246 . . . 4  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  ->  A. x  e.  ZZ DECID  x  e.  { n  e.  NN0  |  ( P ^ n
)  ||  ( M  x.  N ) } )
3027pclemub 12301 . . . . 5  |-  ( ( P  e.  ( ZZ>= ` 
2 )  /\  (
( M  x.  N
)  e.  ZZ  /\  ( M  x.  N
)  =/=  0 ) )  ->  E. x  e.  ZZ  A. y  e. 
{ n  e.  NN0  |  ( P ^ n
)  ||  ( M  x.  N ) } y  <_  x )
316, 9, 26, 30syl12anc 1246 . . . 4  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  ->  E. x  e.  ZZ  A. y  e.  { n  e.  NN0  |  ( P ^ n )  ||  ( M  x.  N
) } y  <_  x )
32 oveq2 5896 . . . . . . 7  |-  ( x  =  ( S  +  T )  ->  ( P ^ x )  =  ( P ^ ( S  +  T )
) )
3332breq1d 4025 . . . . . 6  |-  ( x  =  ( S  +  T )  ->  (
( P ^ x
)  ||  ( M  x.  N )  <->  ( P ^ ( S  +  T ) )  ||  ( M  x.  N
) ) )
34 eqid 2187 . . . . . . . . . 10  |-  { n  e.  NN0  |  ( P ^ n )  ||  M }  =  {
n  e.  NN0  | 
( P ^ n
)  ||  M }
35 pcpremul.1 . . . . . . . . . 10  |-  S  =  sup ( { n  e.  NN0  |  ( P ^ n )  ||  M } ,  RR ,  <  )
3634, 35pcprecl 12303 . . . . . . . . 9  |-  ( ( P  e.  ( ZZ>= ` 
2 )  /\  ( M  e.  ZZ  /\  M  =/=  0 ) )  -> 
( S  e.  NN0  /\  ( P ^ S
)  ||  M )
)
376, 10, 14, 36syl12anc 1246 . . . . . . . 8  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( S  e.  NN0  /\  ( P ^ S
)  ||  M )
)
3837simpld 112 . . . . . . 7  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  ->  S  e.  NN0 )
39 eqid 2187 . . . . . . . . . 10  |-  { n  e.  NN0  |  ( P ^ n )  ||  N }  =  {
n  e.  NN0  | 
( P ^ n
)  ||  N }
40 pcpremul.2 . . . . . . . . . 10  |-  T  =  sup ( { n  e.  NN0  |  ( P ^ n )  ||  N } ,  RR ,  <  )
4139, 40pcprecl 12303 . . . . . . . . 9  |-  ( ( P  e.  ( ZZ>= ` 
2 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( T  e.  NN0  /\  ( P ^ T
)  ||  N )
)
426, 12, 19, 41syl12anc 1246 . . . . . . . 8  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( T  e.  NN0  /\  ( P ^ T
)  ||  N )
)
4342simpld 112 . . . . . . 7  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  ->  T  e.  NN0 )
4438, 43nn0addcld 9247 . . . . . 6  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( S  +  T
)  e.  NN0 )
45 prmnn 12124 . . . . . . . . . 10  |-  ( P  e.  Prime  ->  P  e.  NN )
46453ad2ant1 1019 . . . . . . . . 9  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  ->  P  e.  NN )
4746, 44nnexpcld 10690 . . . . . . . 8  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( P ^ ( S  +  T )
)  e.  NN )
4847nnzd 9388 . . . . . . 7  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( P ^ ( S  +  T )
)  e.  ZZ )
4946, 43nnexpcld 10690 . . . . . . . . 9  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( P ^ T
)  e.  NN )
5049nnzd 9388 . . . . . . . 8  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( P ^ T
)  e.  ZZ )
5110, 50zmulcld 9395 . . . . . . 7  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( M  x.  ( P ^ T ) )  e.  ZZ )
5246nncnd 8947 . . . . . . . . 9  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  ->  P  e.  CC )
5352, 43, 38expaddd 10670 . . . . . . . 8  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( P ^ ( S  +  T )
)  =  ( ( P ^ S )  x.  ( P ^ T ) ) )
5437simprd 114 . . . . . . . . 9  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( P ^ S
)  ||  M )
5546, 38nnexpcld 10690 . . . . . . . . . . 11  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( P ^ S
)  e.  NN )
5655nnzd 9388 . . . . . . . . . 10  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( P ^ S
)  e.  ZZ )
57 dvdsmulc 11840 . . . . . . . . . 10  |-  ( ( ( P ^ S
)  e.  ZZ  /\  M  e.  ZZ  /\  ( P ^ T )  e.  ZZ )  ->  (
( P ^ S
)  ||  M  ->  ( ( P ^ S
)  x.  ( P ^ T ) ) 
||  ( M  x.  ( P ^ T ) ) ) )
5856, 10, 50, 57syl3anc 1248 . . . . . . . . 9  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( ( P ^ S )  ||  M  ->  ( ( P ^ S )  x.  ( P ^ T ) ) 
||  ( M  x.  ( P ^ T ) ) ) )
5954, 58mpd 13 . . . . . . . 8  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( ( P ^ S )  x.  ( P ^ T ) ) 
||  ( M  x.  ( P ^ T ) ) )
6053, 59eqbrtrd 4037 . . . . . . 7  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( P ^ ( S  +  T )
)  ||  ( M  x.  ( P ^ T
) ) )
6142simprd 114 . . . . . . . 8  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( P ^ T
)  ||  N )
62 dvdscmul 11839 . . . . . . . . 9  |-  ( ( ( P ^ T
)  e.  ZZ  /\  N  e.  ZZ  /\  M  e.  ZZ )  ->  (
( P ^ T
)  ||  N  ->  ( M  x.  ( P ^ T ) ) 
||  ( M  x.  N ) ) )
6350, 12, 10, 62syl3anc 1248 . . . . . . . 8  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( ( P ^ T )  ||  N  ->  ( M  x.  ( P ^ T ) ) 
||  ( M  x.  N ) ) )
6461, 63mpd 13 . . . . . . 7  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( M  x.  ( P ^ T ) ) 
||  ( M  x.  N ) )
6548, 51, 9, 60, 64dvdstrd 11851 . . . . . 6  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( P ^ ( S  +  T )
)  ||  ( M  x.  N ) )
6633, 44, 65elrabd 2907 . . . . 5  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( S  +  T
)  e.  { x  e.  NN0  |  ( P ^ x )  ||  ( M  x.  N
) } )
67 oveq2 5896 . . . . . . 7  |-  ( x  =  n  ->  ( P ^ x )  =  ( P ^ n
) )
6867breq1d 4025 . . . . . 6  |-  ( x  =  n  ->  (
( P ^ x
)  ||  ( M  x.  N )  <->  ( P ^ n )  ||  ( M  x.  N
) ) )
6968cbvrabv 2748 . . . . 5  |-  { x  e.  NN0  |  ( P ^ x )  ||  ( M  x.  N
) }  =  {
n  e.  NN0  | 
( P ^ n
)  ||  ( M  x.  N ) }
7066, 69eleqtrdi 2280 . . . 4  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( S  +  T
)  e.  { n  e.  NN0  |  ( P ^ n )  ||  ( M  x.  N
) } )
714, 29, 31, 70suprzubdc 11967 . . 3  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( S  +  T
)  <_  sup ( { n  e.  NN0  |  ( P ^ n
)  ||  ( M  x.  N ) } ,  RR ,  <  ) )
72 pcpremul.3 . . 3  |-  U  =  sup ( { n  e.  NN0  |  ( P ^ n )  ||  ( M  x.  N
) } ,  RR ,  <  )
7371, 72breqtrrdi 4057 . 2  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( S  +  T
)  <_  U )
7434, 35pcprendvds2 12305 . . . . . 6  |-  ( ( P  e.  ( ZZ>= ` 
2 )  /\  ( M  e.  ZZ  /\  M  =/=  0 ) )  ->  -.  P  ||  ( M  /  ( P ^ S ) ) )
756, 10, 14, 74syl12anc 1246 . . . . 5  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  ->  -.  P  ||  ( M  /  ( P ^ S ) ) )
7639, 40pcprendvds2 12305 . . . . . 6  |-  ( ( P  e.  ( ZZ>= ` 
2 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  ->  -.  P  ||  ( N  /  ( P ^ T ) ) )
776, 12, 19, 76syl12anc 1246 . . . . 5  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  ->  -.  P  ||  ( N  /  ( P ^ T ) ) )
78 ioran 753 . . . . 5  |-  ( -.  ( P  ||  ( M  /  ( P ^ S ) )  \/  P  ||  ( N  /  ( P ^ T ) ) )  <-> 
( -.  P  ||  ( M  /  ( P ^ S ) )  /\  -.  P  ||  ( N  /  ( P ^ T ) ) ) )
7975, 77, 78sylanbrc 417 . . . 4  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  ->  -.  ( P  ||  ( M  /  ( P ^ S ) )  \/  P  ||  ( N  /  ( P ^ T ) ) ) )
80 simp1 998 . . . . 5  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  ->  P  e.  Prime )
8155nnne0d 8978 . . . . . . 7  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( P ^ S
)  =/=  0 )
82 dvdsval2 11811 . . . . . . 7  |-  ( ( ( P ^ S
)  e.  ZZ  /\  ( P ^ S )  =/=  0  /\  M  e.  ZZ )  ->  (
( P ^ S
)  ||  M  <->  ( M  /  ( P ^ S ) )  e.  ZZ ) )
8356, 81, 10, 82syl3anc 1248 . . . . . 6  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( ( P ^ S )  ||  M  <->  ( M  /  ( P ^ S ) )  e.  ZZ ) )
8454, 83mpbid 147 . . . . 5  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( M  /  ( P ^ S ) )  e.  ZZ )
8549nnne0d 8978 . . . . . . 7  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( P ^ T
)  =/=  0 )
86 dvdsval2 11811 . . . . . . 7  |-  ( ( ( P ^ T
)  e.  ZZ  /\  ( P ^ T )  =/=  0  /\  N  e.  ZZ )  ->  (
( P ^ T
)  ||  N  <->  ( N  /  ( P ^ T ) )  e.  ZZ ) )
8750, 85, 12, 86syl3anc 1248 . . . . . 6  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( ( P ^ T )  ||  N  <->  ( N  /  ( P ^ T ) )  e.  ZZ ) )
8861, 87mpbid 147 . . . . 5  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( N  /  ( P ^ T ) )  e.  ZZ )
89 euclemma 12160 . . . . 5  |-  ( ( P  e.  Prime  /\  ( M  /  ( P ^ S ) )  e.  ZZ  /\  ( N  /  ( P ^ T ) )  e.  ZZ )  ->  ( P  ||  ( ( M  /  ( P ^ S ) )  x.  ( N  /  ( P ^ T ) ) )  <->  ( P  ||  ( M  /  ( P ^ S ) )  \/  P  ||  ( N  /  ( P ^ T ) ) ) ) )
9080, 84, 88, 89syl3anc 1248 . . . 4  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( P  ||  (
( M  /  ( P ^ S ) )  x.  ( N  / 
( P ^ T
) ) )  <->  ( P  ||  ( M  /  ( P ^ S ) )  \/  P  ||  ( N  /  ( P ^ T ) ) ) ) )
9179, 90mtbird 674 . . 3  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  ->  -.  P  ||  ( ( M  /  ( P ^ S ) )  x.  ( N  / 
( P ^ T
) ) ) )
9227, 72pcprecl 12303 . . . . . . 7  |-  ( ( P  e.  ( ZZ>= ` 
2 )  /\  (
( M  x.  N
)  e.  ZZ  /\  ( M  x.  N
)  =/=  0 ) )  ->  ( U  e.  NN0  /\  ( P ^ U )  ||  ( M  x.  N
) ) )
936, 9, 26, 92syl12anc 1246 . . . . . 6  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( U  e.  NN0  /\  ( P ^ U
)  ||  ( M  x.  N ) ) )
9493simpld 112 . . . . 5  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  ->  U  e.  NN0 )
95 nn0ltp1le 9329 . . . . 5  |-  ( ( ( S  +  T
)  e.  NN0  /\  U  e.  NN0 )  -> 
( ( S  +  T )  <  U  <->  ( ( S  +  T
)  +  1 )  <_  U ) )
9644, 94, 95syl2anc 411 . . . 4  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( ( S  +  T )  <  U  <->  ( ( S  +  T
)  +  1 )  <_  U ) )
9746nnzd 9388 . . . . . . 7  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  ->  P  e.  ZZ )
98 peano2nn0 9230 . . . . . . . 8  |-  ( ( S  +  T )  e.  NN0  ->  ( ( S  +  T )  +  1 )  e. 
NN0 )
9944, 98syl 14 . . . . . . 7  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( ( S  +  T )  +  1 )  e.  NN0 )
100 dvdsexp 11881 . . . . . . . 8  |-  ( ( P  e.  ZZ  /\  ( ( S  +  T )  +  1 )  e.  NN0  /\  U  e.  ( ZZ>= `  ( ( S  +  T )  +  1 ) ) )  -> 
( P ^ (
( S  +  T
)  +  1 ) )  ||  ( P ^ U ) )
1011003expia 1206 . . . . . . 7  |-  ( ( P  e.  ZZ  /\  ( ( S  +  T )  +  1 )  e.  NN0 )  ->  ( U  e.  (
ZZ>= `  ( ( S  +  T )  +  1 ) )  -> 
( P ^ (
( S  +  T
)  +  1 ) )  ||  ( P ^ U ) ) )
10297, 99, 101syl2anc 411 . . . . . 6  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( U  e.  (
ZZ>= `  ( ( S  +  T )  +  1 ) )  -> 
( P ^ (
( S  +  T
)  +  1 ) )  ||  ( P ^ U ) ) )
10393simprd 114 . . . . . . 7  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( P ^ U
)  ||  ( M  x.  N ) )
10446, 99nnexpcld 10690 . . . . . . . . 9  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( P ^ (
( S  +  T
)  +  1 ) )  e.  NN )
105104nnzd 9388 . . . . . . . 8  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( P ^ (
( S  +  T
)  +  1 ) )  e.  ZZ )
10646, 94nnexpcld 10690 . . . . . . . . 9  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( P ^ U
)  e.  NN )
107106nnzd 9388 . . . . . . . 8  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( P ^ U
)  e.  ZZ )
108 dvdstr 11849 . . . . . . . 8  |-  ( ( ( P ^ (
( S  +  T
)  +  1 ) )  e.  ZZ  /\  ( P ^ U )  e.  ZZ  /\  ( M  x.  N )  e.  ZZ )  ->  (
( ( P ^
( ( S  +  T )  +  1 ) )  ||  ( P ^ U )  /\  ( P ^ U ) 
||  ( M  x.  N ) )  -> 
( P ^ (
( S  +  T
)  +  1 ) )  ||  ( M  x.  N ) ) )
109105, 107, 9, 108syl3anc 1248 . . . . . . 7  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( ( ( P ^ ( ( S  +  T )  +  1 ) )  ||  ( P ^ U )  /\  ( P ^ U )  ||  ( M  x.  N )
)  ->  ( P ^ ( ( S  +  T )  +  1 ) )  ||  ( M  x.  N
) ) )
110103, 109mpan2d 428 . . . . . 6  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( ( P ^
( ( S  +  T )  +  1 ) )  ||  ( P ^ U )  -> 
( P ^ (
( S  +  T
)  +  1 ) )  ||  ( M  x.  N ) ) )
111102, 110syld 45 . . . . 5  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( U  e.  (
ZZ>= `  ( ( S  +  T )  +  1 ) )  -> 
( P ^ (
( S  +  T
)  +  1 ) )  ||  ( M  x.  N ) ) )
11299nn0zd 9387 . . . . . 6  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( ( S  +  T )  +  1 )  e.  ZZ )
11394nn0zd 9387 . . . . . 6  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  ->  U  e.  ZZ )
114 eluz 9555 . . . . . 6  |-  ( ( ( ( S  +  T )  +  1 )  e.  ZZ  /\  U  e.  ZZ )  ->  ( U  e.  (
ZZ>= `  ( ( S  +  T )  +  1 ) )  <->  ( ( S  +  T )  +  1 )  <_  U ) )
115112, 113, 114syl2anc 411 . . . . 5  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( U  e.  (
ZZ>= `  ( ( S  +  T )  +  1 ) )  <->  ( ( S  +  T )  +  1 )  <_  U ) )
11652, 44expp1d 10669 . . . . . . 7  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( P ^ (
( S  +  T
)  +  1 ) )  =  ( ( P ^ ( S  +  T ) )  x.  P ) )
11711, 13mulcld 7992 . . . . . . . . 9  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( M  x.  N
)  e.  CC )
11847nncnd 8947 . . . . . . . . 9  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( P ^ ( S  +  T )
)  e.  CC )
11947nnap0d 8979 . . . . . . . . 9  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( P ^ ( S  +  T )
) #  0 )
120117, 118, 119divcanap2d 8763 . . . . . . . 8  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( ( P ^
( S  +  T
) )  x.  (
( M  x.  N
)  /  ( P ^ ( S  +  T ) ) ) )  =  ( M  x.  N ) )
12153oveq2d 5904 . . . . . . . . . 10  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( ( M  x.  N )  /  ( P ^ ( S  +  T ) ) )  =  ( ( M  x.  N )  / 
( ( P ^ S )  x.  ( P ^ T ) ) ) )
12255nncnd 8947 . . . . . . . . . . 11  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( P ^ S
)  e.  CC )
12349nncnd 8947 . . . . . . . . . . 11  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( P ^ T
)  e.  CC )
12455nnap0d 8979 . . . . . . . . . . 11  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( P ^ S
) #  0 )
12549nnap0d 8979 . . . . . . . . . . 11  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( P ^ T
) #  0 )
12611, 122, 13, 123, 124, 125divmuldivapd 8803 . . . . . . . . . 10  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( ( M  / 
( P ^ S
) )  x.  ( N  /  ( P ^ T ) ) )  =  ( ( M  x.  N )  / 
( ( P ^ S )  x.  ( P ^ T ) ) ) )
127121, 126eqtr4d 2223 . . . . . . . . 9  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( ( M  x.  N )  /  ( P ^ ( S  +  T ) ) )  =  ( ( M  /  ( P ^ S ) )  x.  ( N  /  ( P ^ T ) ) ) )
128127oveq2d 5904 . . . . . . . 8  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( ( P ^
( S  +  T
) )  x.  (
( M  x.  N
)  /  ( P ^ ( S  +  T ) ) ) )  =  ( ( P ^ ( S  +  T ) )  x.  ( ( M  /  ( P ^ S ) )  x.  ( N  /  ( P ^ T ) ) ) ) )
129120, 128eqtr3d 2222 . . . . . . 7  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( M  x.  N
)  =  ( ( P ^ ( S  +  T ) )  x.  ( ( M  /  ( P ^ S ) )  x.  ( N  /  ( P ^ T ) ) ) ) )
130116, 129breq12d 4028 . . . . . 6  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( ( P ^
( ( S  +  T )  +  1 ) )  ||  ( M  x.  N )  <->  ( ( P ^ ( S  +  T )
)  x.  P ) 
||  ( ( P ^ ( S  +  T ) )  x.  ( ( M  / 
( P ^ S
) )  x.  ( N  /  ( P ^ T ) ) ) ) ) )
13184, 88zmulcld 9395 . . . . . . 7  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( ( M  / 
( P ^ S
) )  x.  ( N  /  ( P ^ T ) ) )  e.  ZZ )
13247nnne0d 8978 . . . . . . 7  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( P ^ ( S  +  T )
)  =/=  0 )
133 dvdscmulr 11841 . . . . . . 7  |-  ( ( P  e.  ZZ  /\  ( ( M  / 
( P ^ S
) )  x.  ( N  /  ( P ^ T ) ) )  e.  ZZ  /\  (
( P ^ ( S  +  T )
)  e.  ZZ  /\  ( P ^ ( S  +  T ) )  =/=  0 ) )  ->  ( ( ( P ^ ( S  +  T ) )  x.  P )  ||  ( ( P ^
( S  +  T
) )  x.  (
( M  /  ( P ^ S ) )  x.  ( N  / 
( P ^ T
) ) ) )  <-> 
P  ||  ( ( M  /  ( P ^ S ) )  x.  ( N  /  ( P ^ T ) ) ) ) )
13497, 131, 48, 132, 133syl112anc 1252 . . . . . 6  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( ( ( P ^ ( S  +  T ) )  x.  P )  ||  (
( P ^ ( S  +  T )
)  x.  ( ( M  /  ( P ^ S ) )  x.  ( N  / 
( P ^ T
) ) ) )  <-> 
P  ||  ( ( M  /  ( P ^ S ) )  x.  ( N  /  ( P ^ T ) ) ) ) )
135130, 134bitrd 188 . . . . 5  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( ( P ^
( ( S  +  T )  +  1 ) )  ||  ( M  x.  N )  <->  P 
||  ( ( M  /  ( P ^ S ) )  x.  ( N  /  ( P ^ T ) ) ) ) )
136111, 115, 1353imtr3d 202 . . . 4  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( ( ( S  +  T )  +  1 )  <_  U  ->  P  ||  ( ( M  /  ( P ^ S ) )  x.  ( N  / 
( P ^ T
) ) ) ) )
13796, 136sylbid 150 . . 3  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( ( S  +  T )  <  U  ->  P  ||  ( ( M  /  ( P ^ S ) )  x.  ( N  / 
( P ^ T
) ) ) ) )
13891, 137mtod 664 . 2  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  ->  -.  ( S  +  T
)  <  U )
13944nn0red 9244 . . 3  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( S  +  T
)  e.  RR )
14094nn0red 9244 . . 3  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  ->  U  e.  RR )
141139, 140eqleltd 8088 . 2  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( ( S  +  T )  =  U  <-> 
( ( S  +  T )  <_  U  /\  -.  ( S  +  T )  <  U
) ) )
14273, 138, 141mpbir2and 945 1  |-  ( ( P  e.  Prime  /\  ( M  e.  ZZ  /\  M  =/=  0 )  /\  ( N  e.  ZZ  /\  N  =/=  0 ) )  -> 
( S  +  T
)  =  U )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 104    <-> wb 105    \/ wo 709  DECID wdc 835    /\ w3a 979    = wceq 1363    e. wcel 2158    =/= wne 2357   A.wral 2465   E.wrex 2466   {crab 2469    C_ wss 3141   class class class wbr 4015   ` cfv 5228  (class class class)co 5888   supcsup 6995   RRcr 7824   0cc0 7825   1c1 7826    + caddc 7828    x. cmul 7830    < clt 8006    <_ cle 8007   # cap 8552    / cdiv 8643   NNcn 8933   2c2 8984   NN0cn0 9190   ZZcz 9267   ZZ>=cuz 9542   ^cexp 10533    || cdvds 11808   Primecprime 12121
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-13 2160  ax-14 2161  ax-ext 2169  ax-coll 4130  ax-sep 4133  ax-nul 4141  ax-pow 4186  ax-pr 4221  ax-un 4445  ax-setind 4548  ax-iinf 4599  ax-cnex 7916  ax-resscn 7917  ax-1cn 7918  ax-1re 7919  ax-icn 7920  ax-addcl 7921  ax-addrcl 7922  ax-mulcl 7923  ax-mulrcl 7924  ax-addcom 7925  ax-mulcom 7926  ax-addass 7927  ax-mulass 7928  ax-distr 7929  ax-i2m1 7930  ax-0lt1 7931  ax-1rid 7932  ax-0id 7933  ax-rnegex 7934  ax-precex 7935  ax-cnre 7936  ax-pre-ltirr 7937  ax-pre-ltwlin 7938  ax-pre-lttrn 7939  ax-pre-apti 7940  ax-pre-ltadd 7941  ax-pre-mulgt0 7942  ax-pre-mulext 7943  ax-arch 7944  ax-caucvg 7945
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 980  df-3an 981  df-tru 1366  df-fal 1369  df-nf 1471  df-sb 1773  df-eu 2039  df-mo 2040  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ne 2358  df-nel 2453  df-ral 2470  df-rex 2471  df-reu 2472  df-rmo 2473  df-rab 2474  df-v 2751  df-sbc 2975  df-csb 3070  df-dif 3143  df-un 3145  df-in 3147  df-ss 3154  df-nul 3435  df-if 3547  df-pw 3589  df-sn 3610  df-pr 3611  df-op 3613  df-uni 3822  df-int 3857  df-iun 3900  df-br 4016  df-opab 4077  df-mpt 4078  df-tr 4114  df-id 4305  df-po 4308  df-iso 4309  df-iord 4378  df-on 4380  df-ilim 4381  df-suc 4383  df-iom 4602  df-xp 4644  df-rel 4645  df-cnv 4646  df-co 4647  df-dm 4648  df-rn 4649  df-res 4650  df-ima 4651  df-iota 5190  df-fun 5230  df-fn 5231  df-f 5232  df-f1 5233  df-fo 5234  df-f1o 5235  df-fv 5236  df-isom 5237  df-riota 5844  df-ov 5891  df-oprab 5892  df-mpo 5893  df-1st 6155  df-2nd 6156  df-recs 6320  df-frec 6406  df-1o 6431  df-2o 6432  df-er 6549  df-en 6755  df-sup 6997  df-inf 6998  df-pnf 8008  df-mnf 8009  df-xr 8010  df-ltxr 8011  df-le 8012  df-sub 8144  df-neg 8145  df-reap 8546  df-ap 8553  df-div 8644  df-inn 8934  df-2 8992  df-3 8993  df-4 8994  df-n0 9191  df-z 9268  df-uz 9543  df-q 9634  df-rp 9668  df-fz 10023  df-fzo 10157  df-fl 10284  df-mod 10337  df-seqfrec 10460  df-exp 10534  df-cj 10865  df-re 10866  df-im 10867  df-rsqrt 11021  df-abs 11022  df-dvds 11809  df-gcd 11958  df-prm 12122
This theorem is referenced by:  pceulem  12308  pcmul  12315
  Copyright terms: Public domain W3C validator