Metamath Proof Explorer


Theorem pcqcl

Description: Closure of the general prime count function. (Contributed by Mario Carneiro, 23-Feb-2014)

Ref Expression
Assertion pcqcl P N N 0 P pCnt N

Proof

Step Hyp Ref Expression
1 simprl P N N 0 N
2 elq N x y N = x y
3 1 2 sylib P N N 0 x y N = x y
4 nncn y y
5 nnne0 y y 0
6 4 5 div0d y 0 y = 0
7 6 ad2antll P x y 0 y = 0
8 oveq1 x = 0 x y = 0 y
9 8 eqeq1d x = 0 x y = 0 0 y = 0
10 7 9 syl5ibrcom P x y x = 0 x y = 0
11 10 necon3d P x y x y 0 x 0
12 an32 x y x 0 x x 0 y
13 pcdiv P x x 0 y P pCnt x y = P pCnt x P pCnt y
14 pczcl P x x 0 P pCnt x 0
15 14 nn0zd P x x 0 P pCnt x
16 15 3adant3 P x x 0 y P pCnt x
17 nnz y y
18 17 5 jca y y y 0
19 pczcl P y y 0 P pCnt y 0
20 19 nn0zd P y y 0 P pCnt y
21 18 20 sylan2 P y P pCnt y
22 21 3adant2 P x x 0 y P pCnt y
23 16 22 zsubcld P x x 0 y P pCnt x P pCnt y
24 13 23 eqeltrd P x x 0 y P pCnt x y
25 24 3expb P x x 0 y P pCnt x y
26 12 25 sylan2b P x y x 0 P pCnt x y
27 26 expr P x y x 0 P pCnt x y
28 11 27 syld P x y x y 0 P pCnt x y
29 neeq1 N = x y N 0 x y 0
30 oveq2 N = x y P pCnt N = P pCnt x y
31 30 eleq1d N = x y P pCnt N P pCnt x y
32 29 31 imbi12d N = x y N 0 P pCnt N x y 0 P pCnt x y
33 28 32 syl5ibrcom P x y N = x y N 0 P pCnt N
34 33 com23 P x y N 0 N = x y P pCnt N
35 34 impancom P N 0 x y N = x y P pCnt N
36 35 adantrl P N N 0 x y N = x y P pCnt N
37 36 rexlimdvv P N N 0 x y N = x y P pCnt N
38 3 37 mpd P N N 0 P pCnt N