Description: The prime count of a negative number. (Contributed by Mario Carneiro, 13-Mar-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | pcneg | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elq | |
|
2 | zcn | |
|
3 | 2 | ad2antrl | |
4 | nncn | |
|
5 | 4 | ad2antll | |
6 | nnne0 | |
|
7 | 6 | ad2antll | |
8 | 3 5 7 | divnegd | |
9 | 8 | oveq2d | |
10 | neg0 | |
|
11 | simpr | |
|
12 | 11 | negeqd | |
13 | 10 12 11 | 3eqtr4a | |
14 | 13 | oveq1d | |
15 | 14 | oveq2d | |
16 | simpll | |
|
17 | simplrl | |
|
18 | 17 | znegcld | |
19 | simpr | |
|
20 | 2 | negne0bd | |
21 | 17 20 | syl | |
22 | 19 21 | mpbid | |
23 | simplrr | |
|
24 | pcdiv | |
|
25 | 16 18 22 23 24 | syl121anc | |
26 | pcdiv | |
|
27 | 16 17 19 23 26 | syl121anc | |
28 | eqid | |
|
29 | 28 | pczpre | |
30 | 16 18 22 29 | syl12anc | |
31 | eqid | |
|
32 | 31 | pczpre | |
33 | prmz | |
|
34 | zexpcl | |
|
35 | 33 34 | sylan | |
36 | simpl | |
|
37 | dvdsnegb | |
|
38 | 35 36 37 | syl2an | |
39 | 38 | an32s | |
40 | 39 | rabbidva | |
41 | 40 | supeq1d | |
42 | 32 41 | eqtrd | |
43 | 16 17 19 42 | syl12anc | |
44 | 30 43 | eqtr4d | |
45 | 44 | oveq1d | |
46 | 27 45 | eqtr4d | |
47 | 25 46 | eqtr4d | |
48 | 15 47 | pm2.61dane | |
49 | 9 48 | eqtrd | |
50 | negeq | |
|
51 | 50 | oveq2d | |
52 | oveq2 | |
|
53 | 51 52 | eqeq12d | |
54 | 49 53 | syl5ibrcom | |
55 | 54 | rexlimdvva | |
56 | 1 55 | syl5bi | |
57 | 56 | imp | |