Step |
Hyp |
Ref |
Expression |
1 |
|
prmnn |
|- ( Q e. Prime -> Q e. NN ) |
2 |
|
nneoALTV |
|- ( Q e. NN -> ( Q e. Even <-> -. Q e. Odd ) ) |
3 |
2
|
bicomd |
|- ( Q e. NN -> ( -. Q e. Odd <-> Q e. Even ) ) |
4 |
1 3
|
syl |
|- ( Q e. Prime -> ( -. Q e. Odd <-> Q e. Even ) ) |
5 |
|
evenprm2 |
|- ( Q e. Prime -> ( Q e. Even <-> Q = 2 ) ) |
6 |
4 5
|
bitrd |
|- ( Q e. Prime -> ( -. Q e. Odd <-> Q = 2 ) ) |
7 |
6
|
adantl |
|- ( ( P e. Prime /\ Q e. Prime ) -> ( -. Q e. Odd <-> Q = 2 ) ) |
8 |
|
oveq2 |
|- ( Q = 2 -> ( P + Q ) = ( P + 2 ) ) |
9 |
8
|
eqeq2d |
|- ( Q = 2 -> ( N = ( P + Q ) <-> N = ( P + 2 ) ) ) |
10 |
9
|
adantl |
|- ( ( P e. Prime /\ Q = 2 ) -> ( N = ( P + Q ) <-> N = ( P + 2 ) ) ) |
11 |
10
|
3anbi3d |
|- ( ( P e. Prime /\ Q = 2 ) -> ( ( N e. Even /\ 4 < N /\ N = ( P + Q ) ) <-> ( N e. Even /\ 4 < N /\ N = ( P + 2 ) ) ) ) |
12 |
|
breq2 |
|- ( N = ( P + 2 ) -> ( 4 < N <-> 4 < ( P + 2 ) ) ) |
13 |
|
eleq1 |
|- ( N = ( P + 2 ) -> ( N e. Even <-> ( P + 2 ) e. Even ) ) |
14 |
12 13
|
anbi12d |
|- ( N = ( P + 2 ) -> ( ( 4 < N /\ N e. Even ) <-> ( 4 < ( P + 2 ) /\ ( P + 2 ) e. Even ) ) ) |
15 |
|
prmz |
|- ( P e. Prime -> P e. ZZ ) |
16 |
|
2evenALTV |
|- 2 e. Even |
17 |
|
evensumeven |
|- ( ( P e. ZZ /\ 2 e. Even ) -> ( P e. Even <-> ( P + 2 ) e. Even ) ) |
18 |
15 16 17
|
sylancl |
|- ( P e. Prime -> ( P e. Even <-> ( P + 2 ) e. Even ) ) |
19 |
|
evenprm2 |
|- ( P e. Prime -> ( P e. Even <-> P = 2 ) ) |
20 |
|
oveq1 |
|- ( P = 2 -> ( P + 2 ) = ( 2 + 2 ) ) |
21 |
|
2p2e4 |
|- ( 2 + 2 ) = 4 |
22 |
20 21
|
eqtrdi |
|- ( P = 2 -> ( P + 2 ) = 4 ) |
23 |
22
|
breq2d |
|- ( P = 2 -> ( 4 < ( P + 2 ) <-> 4 < 4 ) ) |
24 |
|
4re |
|- 4 e. RR |
25 |
24
|
ltnri |
|- -. 4 < 4 |
26 |
25
|
pm2.21i |
|- ( 4 < 4 -> Q e. Odd ) |
27 |
23 26
|
syl6bi |
|- ( P = 2 -> ( 4 < ( P + 2 ) -> Q e. Odd ) ) |
28 |
19 27
|
syl6bi |
|- ( P e. Prime -> ( P e. Even -> ( 4 < ( P + 2 ) -> Q e. Odd ) ) ) |
29 |
18 28
|
sylbird |
|- ( P e. Prime -> ( ( P + 2 ) e. Even -> ( 4 < ( P + 2 ) -> Q e. Odd ) ) ) |
30 |
29
|
com13 |
|- ( 4 < ( P + 2 ) -> ( ( P + 2 ) e. Even -> ( P e. Prime -> Q e. Odd ) ) ) |
31 |
30
|
imp |
|- ( ( 4 < ( P + 2 ) /\ ( P + 2 ) e. Even ) -> ( P e. Prime -> Q e. Odd ) ) |
32 |
14 31
|
syl6bi |
|- ( N = ( P + 2 ) -> ( ( 4 < N /\ N e. Even ) -> ( P e. Prime -> Q e. Odd ) ) ) |
33 |
32
|
expd |
|- ( N = ( P + 2 ) -> ( 4 < N -> ( N e. Even -> ( P e. Prime -> Q e. Odd ) ) ) ) |
34 |
33
|
com13 |
|- ( N e. Even -> ( 4 < N -> ( N = ( P + 2 ) -> ( P e. Prime -> Q e. Odd ) ) ) ) |
35 |
34
|
3imp |
|- ( ( N e. Even /\ 4 < N /\ N = ( P + 2 ) ) -> ( P e. Prime -> Q e. Odd ) ) |
36 |
35
|
com12 |
|- ( P e. Prime -> ( ( N e. Even /\ 4 < N /\ N = ( P + 2 ) ) -> Q e. Odd ) ) |
37 |
36
|
adantr |
|- ( ( P e. Prime /\ Q = 2 ) -> ( ( N e. Even /\ 4 < N /\ N = ( P + 2 ) ) -> Q e. Odd ) ) |
38 |
11 37
|
sylbid |
|- ( ( P e. Prime /\ Q = 2 ) -> ( ( N e. Even /\ 4 < N /\ N = ( P + Q ) ) -> Q e. Odd ) ) |
39 |
38
|
ex |
|- ( P e. Prime -> ( Q = 2 -> ( ( N e. Even /\ 4 < N /\ N = ( P + Q ) ) -> Q e. Odd ) ) ) |
40 |
39
|
adantr |
|- ( ( P e. Prime /\ Q e. Prime ) -> ( Q = 2 -> ( ( N e. Even /\ 4 < N /\ N = ( P + Q ) ) -> Q e. Odd ) ) ) |
41 |
7 40
|
sylbid |
|- ( ( P e. Prime /\ Q e. Prime ) -> ( -. Q e. Odd -> ( ( N e. Even /\ 4 < N /\ N = ( P + Q ) ) -> Q e. Odd ) ) ) |
42 |
|
ax-1 |
|- ( Q e. Odd -> ( ( N e. Even /\ 4 < N /\ N = ( P + Q ) ) -> Q e. Odd ) ) |
43 |
41 42
|
pm2.61d2 |
|- ( ( P e. Prime /\ Q e. Prime ) -> ( ( N e. Even /\ 4 < N /\ N = ( P + Q ) ) -> Q e. Odd ) ) |