Metamath Proof Explorer

Theorem pcpremul

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)

Ref Expression
Hypotheses 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 pcpremul 
|- ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( S + T ) = U )

Proof

Step Hyp Ref Expression
1 pcpremul.1 
 |-  S = sup ( { n e. NN0 | ( P ^ n ) || M } , RR , < )
2 pcpremul.2 
 |-  T = sup ( { n e. NN0 | ( P ^ n ) || N } , RR , < )
3 pcpremul.3 
 |-  U = sup ( { n e. NN0 | ( P ^ n ) || ( M x. N ) } , RR , < )
4 prmuz2 
 |-  ( P e. Prime -> P e. ( ZZ>= ` 2 ) )
5 4 3ad2ant1 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> P e. ( ZZ>= ` 2 ) )
6 zmulcl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M x. N ) e. ZZ )
7 6 ad2ant2r 
 |-  ( ( ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( M x. N ) e. ZZ )
8 7 3adant1 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( M x. N ) e. ZZ )
9 zcn 
 |-  ( M e. ZZ -> M e. CC )
10 9 anim1i 
 |-  ( ( M e. ZZ /\ M =/= 0 ) -> ( M e. CC /\ M =/= 0 ) )
11 zcn 
 |-  ( N e. ZZ -> N e. CC )
12 11 anim1i 
 |-  ( ( N e. ZZ /\ N =/= 0 ) -> ( N e. CC /\ N =/= 0 ) )
13 mulne0 
 |-  ( ( ( M e. CC /\ M =/= 0 ) /\ ( N e. CC /\ N =/= 0 ) ) -> ( M x. N ) =/= 0 )
14 10 12 13 syl2an 
 |-  ( ( ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( M x. N ) =/= 0 )
15 14 3adant1 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( M x. N ) =/= 0 )
16 eqid 
 |-  { n e. NN0 | ( P ^ n ) || ( M x. N ) } = { n e. NN0 | ( P ^ n ) || ( M x. N ) }
17 16 pclem 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( ( M x. N ) e. ZZ /\ ( M x. N ) =/= 0 ) ) -> ( { n e. NN0 | ( P ^ n ) || ( M x. N ) } C_ ZZ /\ { n e. NN0 | ( P ^ n ) || ( M x. N ) } =/= (/) /\ E. x e. ZZ A. y e. { n e. NN0 | ( P ^ n ) || ( M x. N ) } y <_ x ) )
18 5 8 15 17 syl12anc 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( { n e. NN0 | ( P ^ n ) || ( M x. N ) } C_ ZZ /\ { n e. NN0 | ( P ^ n ) || ( M x. N ) } =/= (/) /\ E. x e. ZZ A. y e. { n e. NN0 | ( P ^ n ) || ( M x. N ) } y <_ x ) )
19 18 simp1d 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> { n e. NN0 | ( P ^ n ) || ( M x. N ) } C_ ZZ )
20 18 simp3d 
 |-  ( ( 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 )
21 oveq2 
 |-  ( x = ( S + T ) -> ( P ^ x ) = ( P ^ ( S + T ) ) )
22 21 breq1d 
 |-  ( x = ( S + T ) -> ( ( P ^ x ) || ( M x. N ) <-> ( P ^ ( S + T ) ) || ( M x. N ) ) )
23 simp2l 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> M e. ZZ )
24 simp2r 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> M =/= 0 )
25 eqid 
 |-  { n e. NN0 | ( P ^ n ) || M } = { n e. NN0 | ( P ^ n ) || M }
26 25 1 pcprecl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ M =/= 0 ) ) -> ( S e. NN0 /\ ( P ^ S ) || M ) )
27 5 23 24 26 syl12anc 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( S e. NN0 /\ ( P ^ S ) || M ) )
28 27 simpld 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> S e. NN0 )
29 simp3l 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> N e. ZZ )
30 simp3r 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> N =/= 0 )
31 eqid 
 |-  { n e. NN0 | ( P ^ n ) || N } = { n e. NN0 | ( P ^ n ) || N }
32 31 2 pcprecl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( T e. NN0 /\ ( P ^ T ) || N ) )
33 5 29 30 32 syl12anc 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( T e. NN0 /\ ( P ^ T ) || N ) )
34 33 simpld 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> T e. NN0 )
35 28 34 nn0addcld 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( S + T ) e. NN0 )
36 prmnn 
 |-  ( P e. Prime -> P e. NN )
37 36 3ad2ant1 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> P e. NN )
38 37 35 nnexpcld 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P ^ ( S + T ) ) e. NN )
39 38 nnzd 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P ^ ( S + T ) ) e. ZZ )
40 37 34 nnexpcld 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P ^ T ) e. NN )
41 40 nnzd 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P ^ T ) e. ZZ )
42 23 41 zmulcld 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( M x. ( P ^ T ) ) e. ZZ )
43 37 nncnd 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> P e. CC )
44 43 34 28 expaddd 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P ^ ( S + T ) ) = ( ( P ^ S ) x. ( P ^ T ) ) )
45 27 simprd 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P ^ S ) || M )
46 37 28 nnexpcld 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P ^ S ) e. NN )
47 46 nnzd 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P ^ S ) e. ZZ )
48 dvdsmulc 
 |-  ( ( ( P ^ S ) e. ZZ /\ M e. ZZ /\ ( P ^ T ) e. ZZ ) -> ( ( P ^ S ) || M -> ( ( P ^ S ) x. ( P ^ T ) ) || ( M x. ( P ^ T ) ) ) )
49 47 23 41 48 syl3anc 
 |-  ( ( 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 ) ) ) )
50 45 49 mpd 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( ( P ^ S ) x. ( P ^ T ) ) || ( M x. ( P ^ T ) ) )
51 44 50 eqbrtrd 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P ^ ( S + T ) ) || ( M x. ( P ^ T ) ) )
52 33 simprd 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P ^ T ) || N )
53 dvdscmul 
 |-  ( ( ( P ^ T ) e. ZZ /\ N e. ZZ /\ M e. ZZ ) -> ( ( P ^ T ) || N -> ( M x. ( P ^ T ) ) || ( M x. N ) ) )
54 41 29 23 53 syl3anc 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( ( P ^ T ) || N -> ( M x. ( P ^ T ) ) || ( M x. N ) ) )
55 52 54 mpd 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( M x. ( P ^ T ) ) || ( M x. N ) )
56 39 42 8 51 55 dvdstrd 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P ^ ( S + T ) ) || ( M x. N ) )
57 22 35 56 elrabd 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( S + T ) e. { x e. NN0 | ( P ^ x ) || ( M x. N ) } )
58 oveq2 
 |-  ( x = n -> ( P ^ x ) = ( P ^ n ) )
59 58 breq1d 
 |-  ( x = n -> ( ( P ^ x ) || ( M x. N ) <-> ( P ^ n ) || ( M x. N ) ) )
60 59 cbvrabv 
 |-  { x e. NN0 | ( P ^ x ) || ( M x. N ) } = { n e. NN0 | ( P ^ n ) || ( M x. N ) }
61 57 60 eleqtrdi 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( S + T ) e. { n e. NN0 | ( P ^ n ) || ( M x. N ) } )
62 suprzub 
 |-  ( ( { n e. NN0 | ( P ^ n ) || ( M x. N ) } C_ ZZ /\ E. x e. ZZ A. y e. { n e. NN0 | ( P ^ n ) || ( M x. N ) } y <_ x /\ ( S + T ) e. { n e. NN0 | ( P ^ n ) || ( M x. N ) } ) -> ( S + T ) <_ sup ( { n e. NN0 | ( P ^ n ) || ( M x. N ) } , RR , < ) )
63 19 20 61 62 syl3anc 
 |-  ( ( 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 , < ) )
64 63 3 breqtrrdi 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( S + T ) <_ U )
65 25 1 pcprendvds2 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ M =/= 0 ) ) -> -. P || ( M / ( P ^ S ) ) )
66 5 23 24 65 syl12anc 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> -. P || ( M / ( P ^ S ) ) )
67 31 2 pcprendvds2 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> -. P || ( N / ( P ^ T ) ) )
68 5 29 30 67 syl12anc 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> -. P || ( N / ( P ^ T ) ) )
69 ioran 
 |-  ( -. ( P || ( M / ( P ^ S ) ) \/ P || ( N / ( P ^ T ) ) ) <-> ( -. P || ( M / ( P ^ S ) ) /\ -. P || ( N / ( P ^ T ) ) ) )
70 66 68 69 sylanbrc 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> -. ( P || ( M / ( P ^ S ) ) \/ P || ( N / ( P ^ T ) ) ) )
71 simp1 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> P e. Prime )
72 46 nnne0d 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P ^ S ) =/= 0 )
73 dvdsval2 
 |-  ( ( ( P ^ S ) e. ZZ /\ ( P ^ S ) =/= 0 /\ M e. ZZ ) -> ( ( P ^ S ) || M <-> ( M / ( P ^ S ) ) e. ZZ ) )
74 47 72 23 73 syl3anc 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( ( P ^ S ) || M <-> ( M / ( P ^ S ) ) e. ZZ ) )
75 45 74 mpbid 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( M / ( P ^ S ) ) e. ZZ )
76 40 nnne0d 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P ^ T ) =/= 0 )
77 dvdsval2 
 |-  ( ( ( P ^ T ) e. ZZ /\ ( P ^ T ) =/= 0 /\ N e. ZZ ) -> ( ( P ^ T ) || N <-> ( N / ( P ^ T ) ) e. ZZ ) )
78 41 76 29 77 syl3anc 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( ( P ^ T ) || N <-> ( N / ( P ^ T ) ) e. ZZ ) )
79 52 78 mpbid 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( N / ( P ^ T ) ) e. ZZ )
80 euclemma 
 |-  ( ( 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 ) ) ) ) )
81 71 75 79 80 syl3anc 
 |-  ( ( 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 ) ) ) ) )
82 70 81 mtbird 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> -. P || ( ( M / ( P ^ S ) ) x. ( N / ( P ^ T ) ) ) )
83 16 3 pcprecl 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ ( ( M x. N ) e. ZZ /\ ( M x. N ) =/= 0 ) ) -> ( U e. NN0 /\ ( P ^ U ) || ( M x. N ) ) )
84 5 8 15 83 syl12anc 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( U e. NN0 /\ ( P ^ U ) || ( M x. N ) ) )
85 84 simpld 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> U e. NN0 )
86 nn0ltp1le 
 |-  ( ( ( S + T ) e. NN0 /\ U e. NN0 ) -> ( ( S + T ) < U <-> ( ( S + T ) + 1 ) <_ U ) )
87 35 85 86 syl2anc 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( ( S + T ) < U <-> ( ( S + T ) + 1 ) <_ U ) )
88 37 nnzd 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> P e. ZZ )
89 peano2nn0 
 |-  ( ( S + T ) e. NN0 -> ( ( S + T ) + 1 ) e. NN0 )
90 35 89 syl 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( ( S + T ) + 1 ) e. NN0 )
91 dvdsexp 
 |-  ( ( P e. ZZ /\ ( ( S + T ) + 1 ) e. NN0 /\ U e. ( ZZ>= ` ( ( S + T ) + 1 ) ) ) -> ( P ^ ( ( S + T ) + 1 ) ) || ( P ^ U ) )
92 91 3expia 
 |-  ( ( P e. ZZ /\ ( ( S + T ) + 1 ) e. NN0 ) -> ( U e. ( ZZ>= ` ( ( S + T ) + 1 ) ) -> ( P ^ ( ( S + T ) + 1 ) ) || ( P ^ U ) ) )
93 88 90 92 syl2anc 
 |-  ( ( 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 ) ) )
94 84 simprd 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P ^ U ) || ( M x. N ) )
95 37 90 nnexpcld 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P ^ ( ( S + T ) + 1 ) ) e. NN )
96 95 nnzd 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P ^ ( ( S + T ) + 1 ) ) e. ZZ )
97 37 85 nnexpcld 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P ^ U ) e. NN )
98 97 nnzd 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P ^ U ) e. ZZ )
99 dvdstr 
 |-  ( ( ( 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 ) ) )
100 96 98 8 99 syl3anc 
 |-  ( ( 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 ) ) )
101 94 100 mpan2d 
 |-  ( ( 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 ) ) )
102 93 101 syld 
 |-  ( ( 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 ) ) )
103 90 nn0zd 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( ( S + T ) + 1 ) e. ZZ )
104 85 nn0zd 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> U e. ZZ )
105 eluz 
 |-  ( ( ( ( S + T ) + 1 ) e. ZZ /\ U e. ZZ ) -> ( U e. ( ZZ>= ` ( ( S + T ) + 1 ) ) <-> ( ( S + T ) + 1 ) <_ U ) )
106 103 104 105 syl2anc 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( U e. ( ZZ>= ` ( ( S + T ) + 1 ) ) <-> ( ( S + T ) + 1 ) <_ U ) )
107 43 35 expp1d 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P ^ ( ( S + T ) + 1 ) ) = ( ( P ^ ( S + T ) ) x. P ) )
108 23 zcnd 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> M e. CC )
109 29 zcnd 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> N e. CC )
110 108 109 mulcld 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( M x. N ) e. CC )
111 38 nncnd 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P ^ ( S + T ) ) e. CC )
112 38 nnne0d 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P ^ ( S + T ) ) =/= 0 )
113 110 111 112 divcan2d 
 |-  ( ( 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 ) )
114 44 oveq2d 
 |-  ( ( 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 ) ) ) )
115 46 nncnd 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P ^ S ) e. CC )
116 40 nncnd 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( P ^ T ) e. CC )
117 108 115 109 116 72 76 divmuldivd 
 |-  ( ( 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 ) ) ) )
118 114 117 eqtr4d 
 |-  ( ( 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 ) ) ) )
119 118 oveq2d 
 |-  ( ( 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 ) ) ) ) )
120 113 119 eqtr3d 
 |-  ( ( 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 ) ) ) ) )
121 107 120 breq12d 
 |-  ( ( 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 ) ) ) ) ) )
122 75 79 zmulcld 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( ( M / ( P ^ S ) ) x. ( N / ( P ^ T ) ) ) e. ZZ )
123 dvdscmulr 
 |-  ( ( 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 ) ) ) ) )
124 88 122 39 112 123 syl112anc 
 |-  ( ( 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 ) ) ) ) )
125 121 124 bitrd 
 |-  ( ( 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 ) ) ) ) )
126 102 106 125 3imtr3d 
 |-  ( ( 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 ) ) ) ) )
127 87 126 sylbid 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( ( S + T ) < U -> P || ( ( M / ( P ^ S ) ) x. ( N / ( P ^ T ) ) ) ) )
128 82 127 mtod 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> -. ( S + T ) < U )
129 35 nn0red 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( S + T ) e. RR )
130 85 nn0red 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> U e. RR )
131 129 130 eqleltd 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( ( S + T ) = U <-> ( ( S + T ) <_ U /\ -. ( S + T ) < U ) ) )
132 64 128 131 mpbir2and 
 |-  ( ( P e. Prime /\ ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( S + T ) = U )