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

Theorem pcaddlem 12279
Description: Lemma for pcadd 12280. The original numbers  A and  B have been decomposed using the prime count function as  ( P ^ M )  x.  ( R  /  S ) where  R ,  S are both not divisible by  P and  M  =  ( P  pCnt  A ), and similarly for  B. (Contributed by Mario Carneiro, 9-Sep-2014.)
Hypotheses
Ref Expression
pcaddlem.1  |-  ( ph  ->  P  e.  Prime )
pcaddlem.2  |-  ( ph  ->  A  =  ( ( P ^ M )  x.  ( R  /  S ) ) )
pcaddlem.3  |-  ( ph  ->  B  =  ( ( P ^ N )  x.  ( T  /  U ) ) )
pcaddlem.4  |-  ( ph  ->  N  e.  ( ZZ>= `  M ) )
pcaddlem.5  |-  ( ph  ->  ( R  e.  ZZ  /\ 
-.  P  ||  R
) )
pcaddlem.6  |-  ( ph  ->  ( S  e.  NN  /\ 
-.  P  ||  S
) )
pcaddlem.7  |-  ( ph  ->  ( T  e.  ZZ  /\ 
-.  P  ||  T
) )
pcaddlem.8  |-  ( ph  ->  ( U  e.  NN  /\ 
-.  P  ||  U
) )
Assertion
Ref Expression
pcaddlem  |-  ( ph  ->  M  <_  ( P  pCnt  ( A  +  B
) ) )

Proof of Theorem pcaddlem
StepHypRef Expression
1 pcaddlem.4 . . . . . . . . 9  |-  ( ph  ->  N  e.  ( ZZ>= `  M ) )
2 eluzel2 9479 . . . . . . . . 9  |-  ( N  e.  ( ZZ>= `  M
)  ->  M  e.  ZZ )
31, 2syl 14 . . . . . . . 8  |-  ( ph  ->  M  e.  ZZ )
43zred 9321 . . . . . . 7  |-  ( ph  ->  M  e.  RR )
54rexrd 7956 . . . . . 6  |-  ( ph  ->  M  e.  RR* )
6 pnfge 9733 . . . . . 6  |-  ( M  e.  RR*  ->  M  <_ +oo )
75, 6syl 14 . . . . 5  |-  ( ph  ->  M  <_ +oo )
8 pcaddlem.1 . . . . . 6  |-  ( ph  ->  P  e.  Prime )
9 pc0 12245 . . . . . 6  |-  ( P  e.  Prime  ->  ( P 
pCnt  0 )  = +oo )
108, 9syl 14 . . . . 5  |-  ( ph  ->  ( P  pCnt  0
)  = +oo )
117, 10breqtrrd 4015 . . . 4  |-  ( ph  ->  M  <_  ( P  pCnt  0 ) )
1211adantr 274 . . 3  |-  ( (
ph  /\  ( A  +  B )  =  0 )  ->  M  <_  ( P  pCnt  0 ) )
13 simpr 109 . . . 4  |-  ( (
ph  /\  ( A  +  B )  =  0 )  ->  ( A  +  B )  =  0 )
1413oveq2d 5866 . . 3  |-  ( (
ph  /\  ( A  +  B )  =  0 )  ->  ( P  pCnt  ( A  +  B
) )  =  ( P  pCnt  0 ) )
1512, 14breqtrrd 4015 . 2  |-  ( (
ph  /\  ( A  +  B )  =  0 )  ->  M  <_  ( P  pCnt  ( A  +  B ) ) )
164adantr 274 . . . 4  |-  ( (
ph  /\  ( A  +  B )  =/=  0
)  ->  M  e.  RR )
17 prmnn 12051 . . . . . . . . . . . . . 14  |-  ( P  e.  Prime  ->  P  e.  NN )
188, 17syl 14 . . . . . . . . . . . . 13  |-  ( ph  ->  P  e.  NN )
1918nncnd 8879 . . . . . . . . . . . 12  |-  ( ph  ->  P  e.  CC )
2018nnap0d 8911 . . . . . . . . . . . 12  |-  ( ph  ->  P #  0 )
21 eluzelz 9483 . . . . . . . . . . . . . 14  |-  ( N  e.  ( ZZ>= `  M
)  ->  N  e.  ZZ )
221, 21syl 14 . . . . . . . . . . . . 13  |-  ( ph  ->  N  e.  ZZ )
2322, 3zsubcld 9326 . . . . . . . . . . . 12  |-  ( ph  ->  ( N  -  M
)  e.  ZZ )
2419, 20, 23expclzapd 10601 . . . . . . . . . . 11  |-  ( ph  ->  ( P ^ ( N  -  M )
)  e.  CC )
25 pcaddlem.7 . . . . . . . . . . . . 13  |-  ( ph  ->  ( T  e.  ZZ  /\ 
-.  P  ||  T
) )
2625simpld 111 . . . . . . . . . . . 12  |-  ( ph  ->  T  e.  ZZ )
2726zcnd 9322 . . . . . . . . . . 11  |-  ( ph  ->  T  e.  CC )
28 pcaddlem.8 . . . . . . . . . . . . 13  |-  ( ph  ->  ( U  e.  NN  /\ 
-.  P  ||  U
) )
2928simpld 111 . . . . . . . . . . . 12  |-  ( ph  ->  U  e.  NN )
3029nncnd 8879 . . . . . . . . . . 11  |-  ( ph  ->  U  e.  CC )
3129nnap0d 8911 . . . . . . . . . . 11  |-  ( ph  ->  U #  0 )
3224, 27, 30, 31divassapd 8730 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( P ^ ( N  -  M ) )  x.  T )  /  U
)  =  ( ( P ^ ( N  -  M ) )  x.  ( T  /  U ) ) )
3332oveq2d 5866 . . . . . . . . 9  |-  ( ph  ->  ( ( R  /  S )  +  ( ( ( P ^
( N  -  M
) )  x.  T
)  /  U ) )  =  ( ( R  /  S )  +  ( ( P ^ ( N  -  M ) )  x.  ( T  /  U
) ) ) )
34 pcaddlem.5 . . . . . . . . . . . 12  |-  ( ph  ->  ( R  e.  ZZ  /\ 
-.  P  ||  R
) )
3534simpld 111 . . . . . . . . . . 11  |-  ( ph  ->  R  e.  ZZ )
3635zcnd 9322 . . . . . . . . . 10  |-  ( ph  ->  R  e.  CC )
3724, 27mulcld 7927 . . . . . . . . . 10  |-  ( ph  ->  ( ( P ^
( N  -  M
) )  x.  T
)  e.  CC )
38 pcaddlem.6 . . . . . . . . . . . . 13  |-  ( ph  ->  ( S  e.  NN  /\ 
-.  P  ||  S
) )
3938simpld 111 . . . . . . . . . . . 12  |-  ( ph  ->  S  e.  NN )
4039nncnd 8879 . . . . . . . . . . 11  |-  ( ph  ->  S  e.  CC )
4139nnap0d 8911 . . . . . . . . . . 11  |-  ( ph  ->  S #  0 )
4240, 41jca 304 . . . . . . . . . 10  |-  ( ph  ->  ( S  e.  CC  /\  S #  0 ) )
4330, 31jca 304 . . . . . . . . . 10  |-  ( ph  ->  ( U  e.  CC  /\  U #  0 ) )
44 divadddivap 8631 . . . . . . . . . 10  |-  ( ( ( R  e.  CC  /\  ( ( P ^
( N  -  M
) )  x.  T
)  e.  CC )  /\  ( ( S  e.  CC  /\  S #  0 )  /\  ( U  e.  CC  /\  U #  0 ) ) )  ->  ( ( R  /  S )  +  ( ( ( P ^ ( N  -  M ) )  x.  T )  /  U
) )  =  ( ( ( R  x.  U )  +  ( ( ( P ^
( N  -  M
) )  x.  T
)  x.  S ) )  /  ( S  x.  U ) ) )
4536, 37, 42, 43, 44syl22anc 1234 . . . . . . . . 9  |-  ( ph  ->  ( ( R  /  S )  +  ( ( ( P ^
( N  -  M
) )  x.  T
)  /  U ) )  =  ( ( ( R  x.  U
)  +  ( ( ( P ^ ( N  -  M )
)  x.  T )  x.  S ) )  /  ( S  x.  U ) ) )
4633, 45eqtr3d 2205 . . . . . . . 8  |-  ( ph  ->  ( ( R  /  S )  +  ( ( P ^ ( N  -  M )
)  x.  ( T  /  U ) ) )  =  ( ( ( R  x.  U
)  +  ( ( ( P ^ ( N  -  M )
)  x.  T )  x.  S ) )  /  ( S  x.  U ) ) )
4746oveq2d 5866 . . . . . . 7  |-  ( ph  ->  ( P  pCnt  (
( R  /  S
)  +  ( ( P ^ ( N  -  M ) )  x.  ( T  /  U ) ) ) )  =  ( P 
pCnt  ( ( ( R  x.  U )  +  ( ( ( P ^ ( N  -  M ) )  x.  T )  x.  S ) )  / 
( S  x.  U
) ) ) )
4847adantr 274 . . . . . 6  |-  ( (
ph  /\  ( A  +  B )  =/=  0
)  ->  ( P  pCnt  ( ( R  /  S )  +  ( ( P ^ ( N  -  M )
)  x.  ( T  /  U ) ) ) )  =  ( P  pCnt  ( (
( R  x.  U
)  +  ( ( ( P ^ ( N  -  M )
)  x.  T )  x.  S ) )  /  ( S  x.  U ) ) ) )
498adantr 274 . . . . . . 7  |-  ( (
ph  /\  ( A  +  B )  =/=  0
)  ->  P  e.  Prime )
5029nnzd 9320 . . . . . . . . . 10  |-  ( ph  ->  U  e.  ZZ )
5135, 50zmulcld 9327 . . . . . . . . 9  |-  ( ph  ->  ( R  x.  U
)  e.  ZZ )
52 uznn0sub 9505 . . . . . . . . . . . . . 14  |-  ( N  e.  ( ZZ>= `  M
)  ->  ( N  -  M )  e.  NN0 )
531, 52syl 14 . . . . . . . . . . . . 13  |-  ( ph  ->  ( N  -  M
)  e.  NN0 )
5418, 53nnexpcld 10618 . . . . . . . . . . . 12  |-  ( ph  ->  ( P ^ ( N  -  M )
)  e.  NN )
5554nnzd 9320 . . . . . . . . . . 11  |-  ( ph  ->  ( P ^ ( N  -  M )
)  e.  ZZ )
5655, 26zmulcld 9327 . . . . . . . . . 10  |-  ( ph  ->  ( ( P ^
( N  -  M
) )  x.  T
)  e.  ZZ )
5739nnzd 9320 . . . . . . . . . 10  |-  ( ph  ->  S  e.  ZZ )
5856, 57zmulcld 9327 . . . . . . . . 9  |-  ( ph  ->  ( ( ( P ^ ( N  -  M ) )  x.  T )  x.  S
)  e.  ZZ )
5951, 58zaddcld 9325 . . . . . . . 8  |-  ( ph  ->  ( ( R  x.  U )  +  ( ( ( P ^
( N  -  M
) )  x.  T
)  x.  S ) )  e.  ZZ )
6059adantr 274 . . . . . . 7  |-  ( (
ph  /\  ( A  +  B )  =/=  0
)  ->  ( ( R  x.  U )  +  ( ( ( P ^ ( N  -  M ) )  x.  T )  x.  S ) )  e.  ZZ )
6119, 20, 3expclzapd 10601 . . . . . . . . . . . . 13  |-  ( ph  ->  ( P ^ M
)  e.  CC )
6261mul01d 8299 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( P ^ M )  x.  0 )  =  0 )
63 oveq2 5858 . . . . . . . . . . . . 13  |-  ( ( ( R  /  S
)  +  ( ( P ^ ( N  -  M ) )  x.  ( T  /  U ) ) )  =  0  ->  (
( P ^ M
)  x.  ( ( R  /  S )  +  ( ( P ^ ( N  -  M ) )  x.  ( T  /  U
) ) ) )  =  ( ( P ^ M )  x.  0 ) )
6463eqeq1d 2179 . . . . . . . . . . . 12  |-  ( ( ( R  /  S
)  +  ( ( P ^ ( N  -  M ) )  x.  ( T  /  U ) ) )  =  0  ->  (
( ( P ^ M )  x.  (
( R  /  S
)  +  ( ( P ^ ( N  -  M ) )  x.  ( T  /  U ) ) ) )  =  0  <->  (
( P ^ M
)  x.  0 )  =  0 ) )
6562, 64syl5ibrcom 156 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( R  /  S )  +  ( ( P ^
( N  -  M
) )  x.  ( T  /  U ) ) )  =  0  -> 
( ( P ^ M )  x.  (
( R  /  S
)  +  ( ( P ^ ( N  -  M ) )  x.  ( T  /  U ) ) ) )  =  0 ) )
6665necon3d 2384 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( P ^ M )  x.  ( ( R  /  S )  +  ( ( P ^ ( N  -  M )
)  x.  ( T  /  U ) ) ) )  =/=  0  ->  ( ( R  /  S )  +  ( ( P ^ ( N  -  M )
)  x.  ( T  /  U ) ) )  =/=  0 ) )
6736, 40, 41divclapd 8694 . . . . . . . . . . . . 13  |-  ( ph  ->  ( R  /  S
)  e.  CC )
6827, 30, 31divclapd 8694 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( T  /  U
)  e.  CC )
6924, 68mulcld 7927 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( P ^
( N  -  M
) )  x.  ( T  /  U ) )  e.  CC )
7061, 67, 69adddid 7931 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( P ^ M )  x.  (
( R  /  S
)  +  ( ( P ^ ( N  -  M ) )  x.  ( T  /  U ) ) ) )  =  ( ( ( P ^ M
)  x.  ( R  /  S ) )  +  ( ( P ^ M )  x.  ( ( P ^
( N  -  M
) )  x.  ( T  /  U ) ) ) ) )
71 pcaddlem.2 . . . . . . . . . . . . 13  |-  ( ph  ->  A  =  ( ( P ^ M )  x.  ( R  /  S ) ) )
72 pcaddlem.3 . . . . . . . . . . . . . 14  |-  ( ph  ->  B  =  ( ( P ^ N )  x.  ( T  /  U ) ) )
733zcnd 9322 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  M  e.  CC )
7422zcnd 9322 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  N  e.  CC )
7573, 74pncan3d 8220 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( M  +  ( N  -  M ) )  =  N )
7675oveq2d 5866 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( P ^ ( M  +  ( N  -  M ) ) )  =  ( P ^ N ) )
77 expaddzap 10507 . . . . . . . . . . . . . . . . 17  |-  ( ( ( P  e.  CC  /\  P #  0 )  /\  ( M  e.  ZZ  /\  ( N  -  M
)  e.  ZZ ) )  ->  ( P ^ ( M  +  ( N  -  M
) ) )  =  ( ( P ^ M )  x.  ( P ^ ( N  -  M ) ) ) )
7819, 20, 3, 23, 77syl22anc 1234 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( P ^ ( M  +  ( N  -  M ) ) )  =  ( ( P ^ M )  x.  ( P ^ ( N  -  M )
) ) )
7976, 78eqtr3d 2205 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( P ^ N
)  =  ( ( P ^ M )  x.  ( P ^
( N  -  M
) ) ) )
8079oveq1d 5865 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( P ^ N )  x.  ( T  /  U ) )  =  ( ( ( P ^ M )  x.  ( P ^
( N  -  M
) ) )  x.  ( T  /  U
) ) )
8161, 24, 68mulassd 7930 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( P ^ M )  x.  ( P ^ ( N  -  M )
) )  x.  ( T  /  U ) )  =  ( ( P ^ M )  x.  ( ( P ^
( N  -  M
) )  x.  ( T  /  U ) ) ) )
8272, 80, 813eqtrd 2207 . . . . . . . . . . . . 13  |-  ( ph  ->  B  =  ( ( P ^ M )  x.  ( ( P ^ ( N  -  M ) )  x.  ( T  /  U
) ) ) )
8371, 82oveq12d 5868 . . . . . . . . . . . 12  |-  ( ph  ->  ( A  +  B
)  =  ( ( ( P ^ M
)  x.  ( R  /  S ) )  +  ( ( P ^ M )  x.  ( ( P ^
( N  -  M
) )  x.  ( T  /  U ) ) ) ) )
8470, 83eqtr4d 2206 . . . . . . . . . . 11  |-  ( ph  ->  ( ( P ^ M )  x.  (
( R  /  S
)  +  ( ( P ^ ( N  -  M ) )  x.  ( T  /  U ) ) ) )  =  ( A  +  B ) )
8584neeq1d 2358 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( P ^ M )  x.  ( ( R  /  S )  +  ( ( P ^ ( N  -  M )
)  x.  ( T  /  U ) ) ) )  =/=  0  <->  ( A  +  B )  =/=  0 ) )
8646neeq1d 2358 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( R  /  S )  +  ( ( P ^
( N  -  M
) )  x.  ( T  /  U ) ) )  =/=  0  <->  (
( ( R  x.  U )  +  ( ( ( P ^
( N  -  M
) )  x.  T
)  x.  S ) )  /  ( S  x.  U ) )  =/=  0 ) )
8766, 85, 863imtr3d 201 . . . . . . . . 9  |-  ( ph  ->  ( ( A  +  B )  =/=  0  ->  ( ( ( R  x.  U )  +  ( ( ( P ^ ( N  -  M ) )  x.  T )  x.  S
) )  /  ( S  x.  U )
)  =/=  0 ) )
8839, 29nnmulcld 8914 . . . . . . . . . . . . 13  |-  ( ph  ->  ( S  x.  U
)  e.  NN )
8988nncnd 8879 . . . . . . . . . . . 12  |-  ( ph  ->  ( S  x.  U
)  e.  CC )
9040, 30, 41, 31mulap0d 8563 . . . . . . . . . . . 12  |-  ( ph  ->  ( S  x.  U
) #  0 )
9189, 90div0apd 8691 . . . . . . . . . . 11  |-  ( ph  ->  ( 0  /  ( S  x.  U )
)  =  0 )
92 oveq1 5857 . . . . . . . . . . . 12  |-  ( ( ( R  x.  U
)  +  ( ( ( P ^ ( N  -  M )
)  x.  T )  x.  S ) )  =  0  ->  (
( ( R  x.  U )  +  ( ( ( P ^
( N  -  M
) )  x.  T
)  x.  S ) )  /  ( S  x.  U ) )  =  ( 0  / 
( S  x.  U
) ) )
9392eqeq1d 2179 . . . . . . . . . . 11  |-  ( ( ( R  x.  U
)  +  ( ( ( P ^ ( N  -  M )
)  x.  T )  x.  S ) )  =  0  ->  (
( ( ( R  x.  U )  +  ( ( ( P ^ ( N  -  M ) )  x.  T )  x.  S
) )  /  ( S  x.  U )
)  =  0  <->  (
0  /  ( S  x.  U ) )  =  0 ) )
9491, 93syl5ibrcom 156 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( R  x.  U )  +  ( ( ( P ^ ( N  -  M ) )  x.  T )  x.  S
) )  =  0  ->  ( ( ( R  x.  U )  +  ( ( ( P ^ ( N  -  M ) )  x.  T )  x.  S ) )  / 
( S  x.  U
) )  =  0 ) )
9594necon3d 2384 . . . . . . . . 9  |-  ( ph  ->  ( ( ( ( R  x.  U )  +  ( ( ( P ^ ( N  -  M ) )  x.  T )  x.  S ) )  / 
( S  x.  U
) )  =/=  0  ->  ( ( R  x.  U )  +  ( ( ( P ^
( N  -  M
) )  x.  T
)  x.  S ) )  =/=  0 ) )
9687, 95syld 45 . . . . . . . 8  |-  ( ph  ->  ( ( A  +  B )  =/=  0  ->  ( ( R  x.  U )  +  ( ( ( P ^
( N  -  M
) )  x.  T
)  x.  S ) )  =/=  0 ) )
9796imp 123 . . . . . . 7  |-  ( (
ph  /\  ( A  +  B )  =/=  0
)  ->  ( ( R  x.  U )  +  ( ( ( P ^ ( N  -  M ) )  x.  T )  x.  S ) )  =/=  0 )
9888adantr 274 . . . . . . 7  |-  ( (
ph  /\  ( A  +  B )  =/=  0
)  ->  ( S  x.  U )  e.  NN )
99 pcdiv 12243 . . . . . . 7  |-  ( ( P  e.  Prime  /\  (
( ( R  x.  U )  +  ( ( ( P ^
( N  -  M
) )  x.  T
)  x.  S ) )  e.  ZZ  /\  ( ( R  x.  U )  +  ( ( ( P ^
( N  -  M
) )  x.  T
)  x.  S ) )  =/=  0 )  /\  ( S  x.  U )  e.  NN )  ->  ( P  pCnt  ( ( ( R  x.  U )  +  ( ( ( P ^
( N  -  M
) )  x.  T
)  x.  S ) )  /  ( S  x.  U ) ) )  =  ( ( P  pCnt  ( ( R  x.  U )  +  ( ( ( P ^ ( N  -  M ) )  x.  T )  x.  S ) ) )  -  ( P  pCnt  ( S  x.  U ) ) ) )
10049, 60, 97, 98, 99syl121anc 1238 . . . . . 6  |-  ( (
ph  /\  ( A  +  B )  =/=  0
)  ->  ( P  pCnt  ( ( ( R  x.  U )  +  ( ( ( P ^ ( N  -  M ) )  x.  T )  x.  S
) )  /  ( S  x.  U )
) )  =  ( ( P  pCnt  (
( R  x.  U
)  +  ( ( ( P ^ ( N  -  M )
)  x.  T )  x.  S ) ) )  -  ( P 
pCnt  ( S  x.  U ) ) ) )
10139nnne0d 8910 . . . . . . . . . . 11  |-  ( ph  ->  S  =/=  0 )
10229nnne0d 8910 . . . . . . . . . . 11  |-  ( ph  ->  U  =/=  0 )
103 pcmul 12242 . . . . . . . . . . 11  |-  ( ( P  e.  Prime  /\  ( S  e.  ZZ  /\  S  =/=  0 )  /\  ( U  e.  ZZ  /\  U  =/=  0 ) )  -> 
( P  pCnt  ( S  x.  U )
)  =  ( ( P  pCnt  S )  +  ( P  pCnt  U ) ) )
1048, 57, 101, 50, 102, 103syl122anc 1242 . . . . . . . . . 10  |-  ( ph  ->  ( P  pCnt  ( S  x.  U )
)  =  ( ( P  pCnt  S )  +  ( P  pCnt  U ) ) )
10538simprd 113 . . . . . . . . . . . . 13  |-  ( ph  ->  -.  P  ||  S
)
106 pceq0 12262 . . . . . . . . . . . . . 14  |-  ( ( P  e.  Prime  /\  S  e.  NN )  ->  (
( P  pCnt  S
)  =  0  <->  -.  P  ||  S ) )
1078, 39, 106syl2anc 409 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( P  pCnt  S )  =  0  <->  -.  P  ||  S ) )
108105, 107mpbird 166 . . . . . . . . . . . 12  |-  ( ph  ->  ( P  pCnt  S
)  =  0 )
10928simprd 113 . . . . . . . . . . . . 13  |-  ( ph  ->  -.  P  ||  U
)
110 pceq0 12262 . . . . . . . . . . . . . 14  |-  ( ( P  e.  Prime  /\  U  e.  NN )  ->  (
( P  pCnt  U
)  =  0  <->  -.  P  ||  U ) )
1118, 29, 110syl2anc 409 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( P  pCnt  U )  =  0  <->  -.  P  ||  U ) )
112109, 111mpbird 166 . . . . . . . . . . . 12  |-  ( ph  ->  ( P  pCnt  U
)  =  0 )
113108, 112oveq12d 5868 . . . . . . . . . . 11  |-  ( ph  ->  ( ( P  pCnt  S )  +  ( P 
pCnt  U ) )  =  ( 0  +  0 ) )
114 00id 8047 . . . . . . . . . . 11  |-  ( 0  +  0 )  =  0
115113, 114eqtrdi 2219 . . . . . . . . . 10  |-  ( ph  ->  ( ( P  pCnt  S )  +  ( P 
pCnt  U ) )  =  0 )
116104, 115eqtrd 2203 . . . . . . . . 9  |-  ( ph  ->  ( P  pCnt  ( S  x.  U )
)  =  0 )
117116oveq2d 5866 . . . . . . . 8  |-  ( ph  ->  ( ( P  pCnt  ( ( R  x.  U
)  +  ( ( ( P ^ ( N  -  M )
)  x.  T )  x.  S ) ) )  -  ( P 
pCnt  ( S  x.  U ) ) )  =  ( ( P 
pCnt  ( ( R  x.  U )  +  ( ( ( P ^ ( N  -  M ) )  x.  T )  x.  S
) ) )  - 
0 ) )
118117adantr 274 . . . . . . 7  |-  ( (
ph  /\  ( A  +  B )  =/=  0
)  ->  ( ( P  pCnt  ( ( R  x.  U )  +  ( ( ( P ^ ( N  -  M ) )  x.  T )  x.  S
) ) )  -  ( P  pCnt  ( S  x.  U ) ) )  =  ( ( P  pCnt  ( ( R  x.  U )  +  ( ( ( P ^ ( N  -  M ) )  x.  T )  x.  S ) ) )  -  0 ) )
119 pczcl 12239 . . . . . . . . . 10  |-  ( ( P  e.  Prime  /\  (
( ( R  x.  U )  +  ( ( ( P ^
( N  -  M
) )  x.  T
)  x.  S ) )  e.  ZZ  /\  ( ( R  x.  U )  +  ( ( ( P ^
( N  -  M
) )  x.  T
)  x.  S ) )  =/=  0 ) )  ->  ( P  pCnt  ( ( R  x.  U )  +  ( ( ( P ^
( N  -  M
) )  x.  T
)  x.  S ) ) )  e.  NN0 )
12049, 60, 97, 119syl12anc 1231 . . . . . . . . 9  |-  ( (
ph  /\  ( A  +  B )  =/=  0
)  ->  ( P  pCnt  ( ( R  x.  U )  +  ( ( ( P ^
( N  -  M
) )  x.  T
)  x.  S ) ) )  e.  NN0 )
121120nn0cnd 9177 . . . . . . . 8  |-  ( (
ph  /\  ( A  +  B )  =/=  0
)  ->  ( P  pCnt  ( ( R  x.  U )  +  ( ( ( P ^
( N  -  M
) )  x.  T
)  x.  S ) ) )  e.  CC )
122121subid1d 8206 . . . . . . 7  |-  ( (
ph  /\  ( A  +  B )  =/=  0
)  ->  ( ( P  pCnt  ( ( R  x.  U )  +  ( ( ( P ^ ( N  -  M ) )  x.  T )  x.  S
) ) )  - 
0 )  =  ( P  pCnt  ( ( R  x.  U )  +  ( ( ( P ^ ( N  -  M ) )  x.  T )  x.  S ) ) ) )
123118, 122eqtrd 2203 . . . . . 6  |-  ( (
ph  /\  ( A  +  B )  =/=  0
)  ->  ( ( P  pCnt  ( ( R  x.  U )  +  ( ( ( P ^ ( N  -  M ) )  x.  T )  x.  S
) ) )  -  ( P  pCnt  ( S  x.  U ) ) )  =  ( P 
pCnt  ( ( R  x.  U )  +  ( ( ( P ^ ( N  -  M ) )  x.  T )  x.  S
) ) ) )
12448, 100, 1233eqtrd 2207 . . . . 5  |-  ( (
ph  /\  ( A  +  B )  =/=  0
)  ->  ( P  pCnt  ( ( R  /  S )  +  ( ( P ^ ( N  -  M )
)  x.  ( T  /  U ) ) ) )  =  ( P  pCnt  ( ( R  x.  U )  +  ( ( ( P ^ ( N  -  M ) )  x.  T )  x.  S ) ) ) )
125124, 120eqeltrd 2247 . . . 4  |-  ( (
ph  /\  ( A  +  B )  =/=  0
)  ->  ( P  pCnt  ( ( R  /  S )  +  ( ( P ^ ( N  -  M )
)  x.  ( T  /  U ) ) ) )  e.  NN0 )
126 nn0addge1 9168 . . . 4  |-  ( ( M  e.  RR  /\  ( P  pCnt  ( ( R  /  S )  +  ( ( P ^ ( N  -  M ) )  x.  ( T  /  U
) ) ) )  e.  NN0 )  ->  M  <_  ( M  +  ( P  pCnt  ( ( R  /  S )  +  ( ( P ^ ( N  -  M ) )  x.  ( T  /  U
) ) ) ) ) )
12716, 125, 126syl2anc 409 . . 3  |-  ( (
ph  /\  ( A  +  B )  =/=  0
)  ->  M  <_  ( M  +  ( P 
pCnt  ( ( R  /  S )  +  ( ( P ^
( N  -  M
) )  x.  ( T  /  U ) ) ) ) ) )
128 nnq 9579 . . . . . . . 8  |-  ( P  e.  NN  ->  P  e.  QQ )
12918, 128syl 14 . . . . . . 7  |-  ( ph  ->  P  e.  QQ )
13018nnne0d 8910 . . . . . . 7  |-  ( ph  ->  P  =/=  0 )
131 qexpclz 10484 . . . . . . 7  |-  ( ( P  e.  QQ  /\  P  =/=  0  /\  M  e.  ZZ )  ->  ( P ^ M )  e.  QQ )
132129, 130, 3, 131syl3anc 1233 . . . . . 6  |-  ( ph  ->  ( P ^ M
)  e.  QQ )
133132adantr 274 . . . . 5  |-  ( (
ph  /\  ( A  +  B )  =/=  0
)  ->  ( P ^ M )  e.  QQ )
13419, 20, 3expap0d 10602 . . . . . . 7  |-  ( ph  ->  ( P ^ M
) #  0 )
135 0z 9210 . . . . . . . . 9  |-  0  e.  ZZ
136 zq 9572 . . . . . . . . 9  |-  ( 0  e.  ZZ  ->  0  e.  QQ )
137135, 136mp1i 10 . . . . . . . 8  |-  ( ph  ->  0  e.  QQ )
138 qapne 9585 . . . . . . . 8  |-  ( ( ( P ^ M
)  e.  QQ  /\  0  e.  QQ )  ->  ( ( P ^ M ) #  0  <->  ( P ^ M )  =/=  0
) )
139132, 137, 138syl2anc 409 . . . . . . 7  |-  ( ph  ->  ( ( P ^ M ) #  0  <->  ( P ^ M )  =/=  0
) )
140134, 139mpbid 146 . . . . . 6  |-  ( ph  ->  ( P ^ M
)  =/=  0 )
141140adantr 274 . . . . 5  |-  ( (
ph  /\  ( A  +  B )  =/=  0
)  ->  ( P ^ M )  =/=  0
)
142 znq 9570 . . . . . . . 8  |-  ( ( R  e.  ZZ  /\  S  e.  NN )  ->  ( R  /  S
)  e.  QQ )
14335, 39, 142syl2anc 409 . . . . . . 7  |-  ( ph  ->  ( R  /  S
)  e.  QQ )
144 qexpclz 10484 . . . . . . . . 9  |-  ( ( P  e.  QQ  /\  P  =/=  0  /\  ( N  -  M )  e.  ZZ )  ->  ( P ^ ( N  -  M ) )  e.  QQ )
145129, 130, 23, 144syl3anc 1233 . . . . . . . 8  |-  ( ph  ->  ( P ^ ( N  -  M )
)  e.  QQ )
146 znq 9570 . . . . . . . . 9  |-  ( ( T  e.  ZZ  /\  U  e.  NN )  ->  ( T  /  U
)  e.  QQ )
14726, 29, 146syl2anc 409 . . . . . . . 8  |-  ( ph  ->  ( T  /  U
)  e.  QQ )
148 qmulcl 9583 . . . . . . . 8  |-  ( ( ( P ^ ( N  -  M )
)  e.  QQ  /\  ( T  /  U
)  e.  QQ )  ->  ( ( P ^ ( N  -  M ) )  x.  ( T  /  U
) )  e.  QQ )
149145, 147, 148syl2anc 409 . . . . . . 7  |-  ( ph  ->  ( ( P ^
( N  -  M
) )  x.  ( T  /  U ) )  e.  QQ )
150 qaddcl 9581 . . . . . . 7  |-  ( ( ( R  /  S
)  e.  QQ  /\  ( ( P ^
( N  -  M
) )  x.  ( T  /  U ) )  e.  QQ )  -> 
( ( R  /  S )  +  ( ( P ^ ( N  -  M )
)  x.  ( T  /  U ) ) )  e.  QQ )
151143, 149, 150syl2anc 409 . . . . . 6  |-  ( ph  ->  ( ( R  /  S )  +  ( ( P ^ ( N  -  M )
)  x.  ( T  /  U ) ) )  e.  QQ )
152151adantr 274 . . . . 5  |-  ( (
ph  /\  ( A  +  B )  =/=  0
)  ->  ( ( R  /  S )  +  ( ( P ^
( N  -  M
) )  x.  ( T  /  U ) ) )  e.  QQ )
15385, 66sylbird 169 . . . . . 6  |-  ( ph  ->  ( ( A  +  B )  =/=  0  ->  ( ( R  /  S )  +  ( ( P ^ ( N  -  M )
)  x.  ( T  /  U ) ) )  =/=  0 ) )
154153imp 123 . . . . 5  |-  ( (
ph  /\  ( A  +  B )  =/=  0
)  ->  ( ( R  /  S )  +  ( ( P ^
( N  -  M
) )  x.  ( T  /  U ) ) )  =/=  0 )
155 pcqmul 12244 . . . . 5  |-  ( ( P  e.  Prime  /\  (
( P ^ M
)  e.  QQ  /\  ( P ^ M )  =/=  0 )  /\  ( ( ( R  /  S )  +  ( ( P ^
( N  -  M
) )  x.  ( T  /  U ) ) )  e.  QQ  /\  ( ( R  /  S )  +  ( ( P ^ ( N  -  M )
)  x.  ( T  /  U ) ) )  =/=  0 ) )  ->  ( P  pCnt  ( ( P ^ M )  x.  (
( R  /  S
)  +  ( ( P ^ ( N  -  M ) )  x.  ( T  /  U ) ) ) ) )  =  ( ( P  pCnt  ( P ^ M ) )  +  ( P  pCnt  ( ( R  /  S
)  +  ( ( P ^ ( N  -  M ) )  x.  ( T  /  U ) ) ) ) ) )
15649, 133, 141, 152, 154, 155syl122anc 1242 . . . 4  |-  ( (
ph  /\  ( A  +  B )  =/=  0
)  ->  ( P  pCnt  ( ( P ^ M )  x.  (
( R  /  S
)  +  ( ( P ^ ( N  -  M ) )  x.  ( T  /  U ) ) ) ) )  =  ( ( P  pCnt  ( P ^ M ) )  +  ( P  pCnt  ( ( R  /  S
)  +  ( ( P ^ ( N  -  M ) )  x.  ( T  /  U ) ) ) ) ) )
15784oveq2d 5866 . . . . 5  |-  ( ph  ->  ( P  pCnt  (
( P ^ M
)  x.  ( ( R  /  S )  +  ( ( P ^ ( N  -  M ) )  x.  ( T  /  U
) ) ) ) )  =  ( P 
pCnt  ( A  +  B ) ) )
158157adantr 274 . . . 4  |-  ( (
ph  /\  ( A  +  B )  =/=  0
)  ->  ( P  pCnt  ( ( P ^ M )  x.  (
( R  /  S
)  +  ( ( P ^ ( N  -  M ) )  x.  ( T  /  U ) ) ) ) )  =  ( P  pCnt  ( A  +  B ) ) )
159 pcid 12264 . . . . . . 7  |-  ( ( P  e.  Prime  /\  M  e.  ZZ )  ->  ( P  pCnt  ( P ^ M ) )  =  M )
1608, 3, 159syl2anc 409 . . . . . 6  |-  ( ph  ->  ( P  pCnt  ( P ^ M ) )  =  M )
161160oveq1d 5865 . . . . 5  |-  ( ph  ->  ( ( P  pCnt  ( P ^ M ) )  +  ( P 
pCnt  ( ( R  /  S )  +  ( ( P ^
( N  -  M
) )  x.  ( T  /  U ) ) ) ) )  =  ( M  +  ( P  pCnt  ( ( R  /  S )  +  ( ( P ^
( N  -  M
) )  x.  ( T  /  U ) ) ) ) ) )
162161adantr 274 . . . 4  |-  ( (
ph  /\  ( A  +  B )  =/=  0
)  ->  ( ( P  pCnt  ( P ^ M ) )  +  ( P  pCnt  (
( R  /  S
)  +  ( ( P ^ ( N  -  M ) )  x.  ( T  /  U ) ) ) ) )  =  ( M  +  ( P 
pCnt  ( ( R  /  S )  +  ( ( P ^
( N  -  M
) )  x.  ( T  /  U ) ) ) ) ) )
163156, 158, 1623eqtr3d 2211 . . 3  |-  ( (
ph  /\  ( A  +  B )  =/=  0
)  ->  ( P  pCnt  ( A  +  B
) )  =  ( M  +  ( P 
pCnt  ( ( R  /  S )  +  ( ( P ^
( N  -  M
) )  x.  ( T  /  U ) ) ) ) ) )
164127, 163breqtrrd 4015 . 2  |-  ( (
ph  /\  ( A  +  B )  =/=  0
)  ->  M  <_  ( P  pCnt  ( A  +  B ) ) )
165 qmulcl 9583 . . . . . . 7  |-  ( ( ( P ^ M
)  e.  QQ  /\  ( R  /  S
)  e.  QQ )  ->  ( ( P ^ M )  x.  ( R  /  S
) )  e.  QQ )
166132, 143, 165syl2anc 409 . . . . . 6  |-  ( ph  ->  ( ( P ^ M )  x.  ( R  /  S ) )  e.  QQ )
16771, 166eqeltrd 2247 . . . . 5  |-  ( ph  ->  A  e.  QQ )
168 qexpclz 10484 . . . . . . . 8  |-  ( ( P  e.  QQ  /\  P  =/=  0  /\  N  e.  ZZ )  ->  ( P ^ N )  e.  QQ )
169129, 130, 22, 168syl3anc 1233 . . . . . . 7  |-  ( ph  ->  ( P ^ N
)  e.  QQ )
170 qmulcl 9583 . . . . . . 7  |-  ( ( ( P ^ N
)  e.  QQ  /\  ( T  /  U
)  e.  QQ )  ->  ( ( P ^ N )  x.  ( T  /  U
) )  e.  QQ )
171169, 147, 170syl2anc 409 . . . . . 6  |-  ( ph  ->  ( ( P ^ N )  x.  ( T  /  U ) )  e.  QQ )
17272, 171eqeltrd 2247 . . . . 5  |-  ( ph  ->  B  e.  QQ )
173 qaddcl 9581 . . . . 5  |-  ( ( A  e.  QQ  /\  B  e.  QQ )  ->  ( A  +  B
)  e.  QQ )
174167, 172, 173syl2anc 409 . . . 4  |-  ( ph  ->  ( A  +  B
)  e.  QQ )
175 qdceq 10190 . . . 4  |-  ( ( ( A  +  B
)  e.  QQ  /\  0  e.  QQ )  -> DECID  ( A  +  B )  =  0 )
176174, 137, 175syl2anc 409 . . 3  |-  ( ph  -> DECID  ( A  +  B )  =  0 )
177 dcne 2351 . . 3  |-  (DECID  ( A  +  B )  =  0  <->  ( ( A  +  B )  =  0  \/  ( A  +  B )  =/=  0 ) )
178176, 177sylib 121 . 2  |-  ( ph  ->  ( ( A  +  B )  =  0  \/  ( A  +  B )  =/=  0
) )
17915, 164, 178mpjaodan 793 1  |-  ( ph  ->  M  <_  ( P  pCnt  ( A  +  B
) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 103    <-> wb 104    \/ wo 703  DECID wdc 829    = wceq 1348    e. wcel 2141    =/= wne 2340   class class class wbr 3987   ` cfv 5196  (class class class)co 5850   CCcc 7759   RRcr 7760   0cc0 7761    + caddc 7764    x. cmul 7766   +oocpnf 7938   RR*cxr 7940    <_ cle 7942    - cmin 8077   # cap 8487    / cdiv 8576   NNcn 8865   NN0cn0 9122   ZZcz 9199   ZZ>=cuz 9474   QQcq 9565   ^cexp 10462    || cdvds 11736   Primecprime 12048    pCnt cpc 12225
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-coll 4102  ax-sep 4105  ax-nul 4113  ax-pow 4158  ax-pr 4192  ax-un 4416  ax-setind 4519  ax-iinf 4570  ax-cnex 7852  ax-resscn 7853  ax-1cn 7854  ax-1re 7855  ax-icn 7856  ax-addcl 7857  ax-addrcl 7858  ax-mulcl 7859  ax-mulrcl 7860  ax-addcom 7861  ax-mulcom 7862  ax-addass 7863  ax-mulass 7864  ax-distr 7865  ax-i2m1 7866  ax-0lt1 7867  ax-1rid 7868  ax-0id 7869  ax-rnegex 7870  ax-precex 7871  ax-cnre 7872  ax-pre-ltirr 7873  ax-pre-ltwlin 7874  ax-pre-lttrn 7875  ax-pre-apti 7876  ax-pre-ltadd 7877  ax-pre-mulgt0 7878  ax-pre-mulext 7879  ax-arch 7880  ax-caucvg 7881
This theorem depends on definitions:  df-bi 116  df-stab 826  df-dc 830  df-3or 974  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-nel 2436  df-ral 2453  df-rex 2454  df-reu 2455  df-rmo 2456  df-rab 2457  df-v 2732  df-sbc 2956  df-csb 3050  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-if 3526  df-pw 3566  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3795  df-int 3830  df-iun 3873  df-br 3988  df-opab 4049  df-mpt 4050  df-tr 4086  df-id 4276  df-po 4279  df-iso 4280  df-iord 4349  df-on 4351  df-ilim 4352  df-suc 4354  df-iom 4573  df-xp 4615  df-rel 4616  df-cnv 4617  df-co 4618  df-dm 4619  df-rn 4620  df-res 4621  df-ima 4622  df-iota 5158  df-fun 5198  df-fn 5199  df-f 5200  df-f1 5201  df-fo 5202  df-f1o 5203  df-fv 5204  df-isom 5205  df-riota 5806  df-ov 5853  df-oprab 5854  df-mpo 5855  df-1st 6116  df-2nd 6117  df-recs 6281  df-frec 6367  df-1o 6392  df-2o 6393  df-er 6509  df-en 6715  df-sup 6957  df-inf 6958  df-pnf 7943  df-mnf 7944  df-xr 7945  df-ltxr 7946  df-le 7947  df-sub 8079  df-neg 8080  df-reap 8481  df-ap 8488  df-div 8577  df-inn 8866  df-2 8924  df-3 8925  df-4 8926  df-n0 9123  df-z 9200  df-uz 9475  df-q 9566  df-rp 9598  df-fz 9953  df-fzo 10086  df-fl 10213  df-mod 10266  df-seqfrec 10389  df-exp 10463  df-cj 10793  df-re 10794  df-im 10795  df-rsqrt 10949  df-abs 10950  df-dvds 11737  df-gcd 11885  df-prm 12049  df-pc 12226
This theorem is referenced by:  pcadd  12280
  Copyright terms: Public domain W3C validator