Step |
Hyp |
Ref |
Expression |
1 |
|
prmnn |
⊢ ( 𝑄 ∈ ℙ → 𝑄 ∈ ℕ ) |
2 |
|
nneoALTV |
⊢ ( 𝑄 ∈ ℕ → ( 𝑄 ∈ Even ↔ ¬ 𝑄 ∈ Odd ) ) |
3 |
2
|
bicomd |
⊢ ( 𝑄 ∈ ℕ → ( ¬ 𝑄 ∈ Odd ↔ 𝑄 ∈ Even ) ) |
4 |
1 3
|
syl |
⊢ ( 𝑄 ∈ ℙ → ( ¬ 𝑄 ∈ Odd ↔ 𝑄 ∈ Even ) ) |
5 |
|
evenprm2 |
⊢ ( 𝑄 ∈ ℙ → ( 𝑄 ∈ Even ↔ 𝑄 = 2 ) ) |
6 |
4 5
|
bitrd |
⊢ ( 𝑄 ∈ ℙ → ( ¬ 𝑄 ∈ Odd ↔ 𝑄 = 2 ) ) |
7 |
6
|
adantl |
⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) → ( ¬ 𝑄 ∈ Odd ↔ 𝑄 = 2 ) ) |
8 |
|
oveq2 |
⊢ ( 𝑄 = 2 → ( 𝑃 + 𝑄 ) = ( 𝑃 + 2 ) ) |
9 |
8
|
eqeq2d |
⊢ ( 𝑄 = 2 → ( 𝑁 = ( 𝑃 + 𝑄 ) ↔ 𝑁 = ( 𝑃 + 2 ) ) ) |
10 |
9
|
adantl |
⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 = 2 ) → ( 𝑁 = ( 𝑃 + 𝑄 ) ↔ 𝑁 = ( 𝑃 + 2 ) ) ) |
11 |
10
|
3anbi3d |
⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 = 2 ) → ( ( 𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = ( 𝑃 + 𝑄 ) ) ↔ ( 𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = ( 𝑃 + 2 ) ) ) ) |
12 |
|
breq2 |
⊢ ( 𝑁 = ( 𝑃 + 2 ) → ( 4 < 𝑁 ↔ 4 < ( 𝑃 + 2 ) ) ) |
13 |
|
eleq1 |
⊢ ( 𝑁 = ( 𝑃 + 2 ) → ( 𝑁 ∈ Even ↔ ( 𝑃 + 2 ) ∈ Even ) ) |
14 |
12 13
|
anbi12d |
⊢ ( 𝑁 = ( 𝑃 + 2 ) → ( ( 4 < 𝑁 ∧ 𝑁 ∈ Even ) ↔ ( 4 < ( 𝑃 + 2 ) ∧ ( 𝑃 + 2 ) ∈ Even ) ) ) |
15 |
|
prmz |
⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ ) |
16 |
|
2evenALTV |
⊢ 2 ∈ Even |
17 |
|
evensumeven |
⊢ ( ( 𝑃 ∈ ℤ ∧ 2 ∈ Even ) → ( 𝑃 ∈ Even ↔ ( 𝑃 + 2 ) ∈ Even ) ) |
18 |
15 16 17
|
sylancl |
⊢ ( 𝑃 ∈ ℙ → ( 𝑃 ∈ Even ↔ ( 𝑃 + 2 ) ∈ Even ) ) |
19 |
|
evenprm2 |
⊢ ( 𝑃 ∈ ℙ → ( 𝑃 ∈ Even ↔ 𝑃 = 2 ) ) |
20 |
|
oveq1 |
⊢ ( 𝑃 = 2 → ( 𝑃 + 2 ) = ( 2 + 2 ) ) |
21 |
|
2p2e4 |
⊢ ( 2 + 2 ) = 4 |
22 |
20 21
|
eqtrdi |
⊢ ( 𝑃 = 2 → ( 𝑃 + 2 ) = 4 ) |
23 |
22
|
breq2d |
⊢ ( 𝑃 = 2 → ( 4 < ( 𝑃 + 2 ) ↔ 4 < 4 ) ) |
24 |
|
4re |
⊢ 4 ∈ ℝ |
25 |
24
|
ltnri |
⊢ ¬ 4 < 4 |
26 |
25
|
pm2.21i |
⊢ ( 4 < 4 → 𝑄 ∈ Odd ) |
27 |
23 26
|
syl6bi |
⊢ ( 𝑃 = 2 → ( 4 < ( 𝑃 + 2 ) → 𝑄 ∈ Odd ) ) |
28 |
19 27
|
syl6bi |
⊢ ( 𝑃 ∈ ℙ → ( 𝑃 ∈ Even → ( 4 < ( 𝑃 + 2 ) → 𝑄 ∈ Odd ) ) ) |
29 |
18 28
|
sylbird |
⊢ ( 𝑃 ∈ ℙ → ( ( 𝑃 + 2 ) ∈ Even → ( 4 < ( 𝑃 + 2 ) → 𝑄 ∈ Odd ) ) ) |
30 |
29
|
com13 |
⊢ ( 4 < ( 𝑃 + 2 ) → ( ( 𝑃 + 2 ) ∈ Even → ( 𝑃 ∈ ℙ → 𝑄 ∈ Odd ) ) ) |
31 |
30
|
imp |
⊢ ( ( 4 < ( 𝑃 + 2 ) ∧ ( 𝑃 + 2 ) ∈ Even ) → ( 𝑃 ∈ ℙ → 𝑄 ∈ Odd ) ) |
32 |
14 31
|
syl6bi |
⊢ ( 𝑁 = ( 𝑃 + 2 ) → ( ( 4 < 𝑁 ∧ 𝑁 ∈ Even ) → ( 𝑃 ∈ ℙ → 𝑄 ∈ Odd ) ) ) |
33 |
32
|
expd |
⊢ ( 𝑁 = ( 𝑃 + 2 ) → ( 4 < 𝑁 → ( 𝑁 ∈ Even → ( 𝑃 ∈ ℙ → 𝑄 ∈ Odd ) ) ) ) |
34 |
33
|
com13 |
⊢ ( 𝑁 ∈ Even → ( 4 < 𝑁 → ( 𝑁 = ( 𝑃 + 2 ) → ( 𝑃 ∈ ℙ → 𝑄 ∈ Odd ) ) ) ) |
35 |
34
|
3imp |
⊢ ( ( 𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = ( 𝑃 + 2 ) ) → ( 𝑃 ∈ ℙ → 𝑄 ∈ Odd ) ) |
36 |
35
|
com12 |
⊢ ( 𝑃 ∈ ℙ → ( ( 𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = ( 𝑃 + 2 ) ) → 𝑄 ∈ Odd ) ) |
37 |
36
|
adantr |
⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 = 2 ) → ( ( 𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = ( 𝑃 + 2 ) ) → 𝑄 ∈ Odd ) ) |
38 |
11 37
|
sylbid |
⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 = 2 ) → ( ( 𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = ( 𝑃 + 𝑄 ) ) → 𝑄 ∈ Odd ) ) |
39 |
38
|
ex |
⊢ ( 𝑃 ∈ ℙ → ( 𝑄 = 2 → ( ( 𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = ( 𝑃 + 𝑄 ) ) → 𝑄 ∈ Odd ) ) ) |
40 |
39
|
adantr |
⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) → ( 𝑄 = 2 → ( ( 𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = ( 𝑃 + 𝑄 ) ) → 𝑄 ∈ Odd ) ) ) |
41 |
7 40
|
sylbid |
⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) → ( ¬ 𝑄 ∈ Odd → ( ( 𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = ( 𝑃 + 𝑄 ) ) → 𝑄 ∈ Odd ) ) ) |
42 |
|
ax-1 |
⊢ ( 𝑄 ∈ Odd → ( ( 𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = ( 𝑃 + 𝑄 ) ) → 𝑄 ∈ Odd ) ) |
43 |
41 42
|
pm2.61d2 |
⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) → ( ( 𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = ( 𝑃 + 𝑄 ) ) → 𝑄 ∈ Odd ) ) |