Metamath Proof Explorer


Theorem mogoldbblem

Description: Lemma for mogoldbb . (Contributed by AV, 26-Dec-2021)

Ref Expression
Assertion mogoldbblem ( ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 ∈ Even ∧ ( 𝑁 + 2 ) = ( ( 𝑃 + 𝑄 ) + 𝑅 ) ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑝 + 𝑞 ) )

Proof

Step Hyp Ref Expression
1 2evenALTV 2 ∈ Even
2 epee ( ( 𝑁 ∈ Even ∧ 2 ∈ Even ) → ( 𝑁 + 2 ) ∈ Even )
3 1 2 mpan2 ( 𝑁 ∈ Even → ( 𝑁 + 2 ) ∈ Even )
4 3 3ad2ant2 ( ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 ∈ Even ∧ ( 𝑁 + 2 ) = ( ( 𝑃 + 𝑄 ) + 𝑅 ) ) → ( 𝑁 + 2 ) ∈ Even )
5 simp1 ( ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 ∈ Even ∧ ( 𝑁 + 2 ) = ( ( 𝑃 + 𝑄 ) + 𝑅 ) ) → ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) )
6 simp3 ( ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 ∈ Even ∧ ( 𝑁 + 2 ) = ( ( 𝑃 + 𝑄 ) + 𝑅 ) ) → ( 𝑁 + 2 ) = ( ( 𝑃 + 𝑄 ) + 𝑅 ) )
7 even3prm2 ( ( ( 𝑁 + 2 ) ∈ Even ∧ ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ ( 𝑁 + 2 ) = ( ( 𝑃 + 𝑄 ) + 𝑅 ) ) → ( 𝑃 = 2 ∨ 𝑄 = 2 ∨ 𝑅 = 2 ) )
8 4 5 6 7 syl3anc ( ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 ∈ Even ∧ ( 𝑁 + 2 ) = ( ( 𝑃 + 𝑄 ) + 𝑅 ) ) → ( 𝑃 = 2 ∨ 𝑄 = 2 ∨ 𝑅 = 2 ) )
9 oveq1 ( 𝑃 = 2 → ( 𝑃 + 𝑄 ) = ( 2 + 𝑄 ) )
10 9 oveq1d ( 𝑃 = 2 → ( ( 𝑃 + 𝑄 ) + 𝑅 ) = ( ( 2 + 𝑄 ) + 𝑅 ) )
11 10 eqeq2d ( 𝑃 = 2 → ( ( 𝑁 + 2 ) = ( ( 𝑃 + 𝑄 ) + 𝑅 ) ↔ ( 𝑁 + 2 ) = ( ( 2 + 𝑄 ) + 𝑅 ) ) )
12 2cnd ( ( 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) → 2 ∈ ℂ )
13 prmz ( 𝑄 ∈ ℙ → 𝑄 ∈ ℤ )
14 13 zcnd ( 𝑄 ∈ ℙ → 𝑄 ∈ ℂ )
15 14 adantr ( ( 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) → 𝑄 ∈ ℂ )
16 prmz ( 𝑅 ∈ ℙ → 𝑅 ∈ ℤ )
17 16 zcnd ( 𝑅 ∈ ℙ → 𝑅 ∈ ℂ )
18 17 adantl ( ( 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) → 𝑅 ∈ ℂ )
19 simp1 ( ( 2 ∈ ℂ ∧ 𝑄 ∈ ℂ ∧ 𝑅 ∈ ℂ ) → 2 ∈ ℂ )
20 addcl ( ( 𝑄 ∈ ℂ ∧ 𝑅 ∈ ℂ ) → ( 𝑄 + 𝑅 ) ∈ ℂ )
21 20 3adant1 ( ( 2 ∈ ℂ ∧ 𝑄 ∈ ℂ ∧ 𝑅 ∈ ℂ ) → ( 𝑄 + 𝑅 ) ∈ ℂ )
22 addass ( ( 2 ∈ ℂ ∧ 𝑄 ∈ ℂ ∧ 𝑅 ∈ ℂ ) → ( ( 2 + 𝑄 ) + 𝑅 ) = ( 2 + ( 𝑄 + 𝑅 ) ) )
23 19 21 22 comraddd ( ( 2 ∈ ℂ ∧ 𝑄 ∈ ℂ ∧ 𝑅 ∈ ℂ ) → ( ( 2 + 𝑄 ) + 𝑅 ) = ( ( 𝑄 + 𝑅 ) + 2 ) )
24 12 15 18 23 syl3anc ( ( 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) → ( ( 2 + 𝑄 ) + 𝑅 ) = ( ( 𝑄 + 𝑅 ) + 2 ) )
25 24 eqeq2d ( ( 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) → ( ( 𝑁 + 2 ) = ( ( 2 + 𝑄 ) + 𝑅 ) ↔ ( 𝑁 + 2 ) = ( ( 𝑄 + 𝑅 ) + 2 ) ) )
26 25 adantr ( ( ( 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 ∈ Even ) → ( ( 𝑁 + 2 ) = ( ( 2 + 𝑄 ) + 𝑅 ) ↔ ( 𝑁 + 2 ) = ( ( 𝑄 + 𝑅 ) + 2 ) ) )
27 evenz ( 𝑁 ∈ Even → 𝑁 ∈ ℤ )
28 27 zcnd ( 𝑁 ∈ Even → 𝑁 ∈ ℂ )
29 28 adantl ( ( ( 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 ∈ Even ) → 𝑁 ∈ ℂ )
30 zaddcl ( ( 𝑄 ∈ ℤ ∧ 𝑅 ∈ ℤ ) → ( 𝑄 + 𝑅 ) ∈ ℤ )
31 13 16 30 syl2an ( ( 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) → ( 𝑄 + 𝑅 ) ∈ ℤ )
32 31 zcnd ( ( 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) → ( 𝑄 + 𝑅 ) ∈ ℂ )
33 32 adantr ( ( ( 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 ∈ Even ) → ( 𝑄 + 𝑅 ) ∈ ℂ )
34 2cnd ( ( ( 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 ∈ Even ) → 2 ∈ ℂ )
35 29 33 34 addcan2d ( ( ( 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 ∈ Even ) → ( ( 𝑁 + 2 ) = ( ( 𝑄 + 𝑅 ) + 2 ) ↔ 𝑁 = ( 𝑄 + 𝑅 ) ) )
36 26 35 bitrd ( ( ( 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 ∈ Even ) → ( ( 𝑁 + 2 ) = ( ( 2 + 𝑄 ) + 𝑅 ) ↔ 𝑁 = ( 𝑄 + 𝑅 ) ) )
37 simpll ( ( ( 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 = ( 𝑄 + 𝑅 ) ) → 𝑄 ∈ ℙ )
38 oveq1 ( 𝑝 = 𝑄 → ( 𝑝 + 𝑞 ) = ( 𝑄 + 𝑞 ) )
39 38 eqeq2d ( 𝑝 = 𝑄 → ( 𝑁 = ( 𝑝 + 𝑞 ) ↔ 𝑁 = ( 𝑄 + 𝑞 ) ) )
40 39 rexbidv ( 𝑝 = 𝑄 → ( ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑝 + 𝑞 ) ↔ ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑄 + 𝑞 ) ) )
41 40 adantl ( ( ( ( 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 = ( 𝑄 + 𝑅 ) ) ∧ 𝑝 = 𝑄 ) → ( ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑝 + 𝑞 ) ↔ ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑄 + 𝑞 ) ) )
42 simplr ( ( ( 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 = ( 𝑄 + 𝑅 ) ) → 𝑅 ∈ ℙ )
43 simpr ( ( ( 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 = ( 𝑄 + 𝑅 ) ) → 𝑁 = ( 𝑄 + 𝑅 ) )
44 oveq2 ( 𝑞 = 𝑅 → ( 𝑄 + 𝑞 ) = ( 𝑄 + 𝑅 ) )
45 44 eqcomd ( 𝑞 = 𝑅 → ( 𝑄 + 𝑅 ) = ( 𝑄 + 𝑞 ) )
46 43 45 sylan9eq ( ( ( ( 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 = ( 𝑄 + 𝑅 ) ) ∧ 𝑞 = 𝑅 ) → 𝑁 = ( 𝑄 + 𝑞 ) )
47 42 46 rspcedeq2vd ( ( ( 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 = ( 𝑄 + 𝑅 ) ) → ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑄 + 𝑞 ) )
48 37 41 47 rspcedvd ( ( ( 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 = ( 𝑄 + 𝑅 ) ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑝 + 𝑞 ) )
49 48 ex ( ( 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) → ( 𝑁 = ( 𝑄 + 𝑅 ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑝 + 𝑞 ) ) )
50 49 adantr ( ( ( 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 ∈ Even ) → ( 𝑁 = ( 𝑄 + 𝑅 ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑝 + 𝑞 ) ) )
51 36 50 sylbid ( ( ( 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 ∈ Even ) → ( ( 𝑁 + 2 ) = ( ( 2 + 𝑄 ) + 𝑅 ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑝 + 𝑞 ) ) )
52 51 com12 ( ( 𝑁 + 2 ) = ( ( 2 + 𝑄 ) + 𝑅 ) → ( ( ( 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 ∈ Even ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑝 + 𝑞 ) ) )
53 11 52 syl6bi ( 𝑃 = 2 → ( ( 𝑁 + 2 ) = ( ( 𝑃 + 𝑄 ) + 𝑅 ) → ( ( ( 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 ∈ Even ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑝 + 𝑞 ) ) ) )
54 53 com13 ( ( ( 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 ∈ Even ) → ( ( 𝑁 + 2 ) = ( ( 𝑃 + 𝑄 ) + 𝑅 ) → ( 𝑃 = 2 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑝 + 𝑞 ) ) ) )
55 54 ex ( ( 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) → ( 𝑁 ∈ Even → ( ( 𝑁 + 2 ) = ( ( 𝑃 + 𝑄 ) + 𝑅 ) → ( 𝑃 = 2 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑝 + 𝑞 ) ) ) ) )
56 55 3adant1 ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) → ( 𝑁 ∈ Even → ( ( 𝑁 + 2 ) = ( ( 𝑃 + 𝑄 ) + 𝑅 ) → ( 𝑃 = 2 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑝 + 𝑞 ) ) ) ) )
57 56 3imp ( ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 ∈ Even ∧ ( 𝑁 + 2 ) = ( ( 𝑃 + 𝑄 ) + 𝑅 ) ) → ( 𝑃 = 2 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑝 + 𝑞 ) ) )
58 57 com12 ( 𝑃 = 2 → ( ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 ∈ Even ∧ ( 𝑁 + 2 ) = ( ( 𝑃 + 𝑄 ) + 𝑅 ) ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑝 + 𝑞 ) ) )
59 oveq2 ( 𝑄 = 2 → ( 𝑃 + 𝑄 ) = ( 𝑃 + 2 ) )
60 59 oveq1d ( 𝑄 = 2 → ( ( 𝑃 + 𝑄 ) + 𝑅 ) = ( ( 𝑃 + 2 ) + 𝑅 ) )
61 60 eqeq2d ( 𝑄 = 2 → ( ( 𝑁 + 2 ) = ( ( 𝑃 + 𝑄 ) + 𝑅 ) ↔ ( 𝑁 + 2 ) = ( ( 𝑃 + 2 ) + 𝑅 ) ) )
62 prmz ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
63 62 zcnd ( 𝑃 ∈ ℙ → 𝑃 ∈ ℂ )
64 63 adantr ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℙ ) → 𝑃 ∈ ℂ )
65 2cnd ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℙ ) → 2 ∈ ℂ )
66 17 adantl ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℙ ) → 𝑅 ∈ ℂ )
67 64 65 66 3jca ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℙ ) → ( 𝑃 ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝑅 ∈ ℂ ) )
68 67 adantr ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 ∈ Even ) → ( 𝑃 ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝑅 ∈ ℂ ) )
69 add32 ( ( 𝑃 ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝑅 ∈ ℂ ) → ( ( 𝑃 + 2 ) + 𝑅 ) = ( ( 𝑃 + 𝑅 ) + 2 ) )
70 68 69 syl ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 ∈ Even ) → ( ( 𝑃 + 2 ) + 𝑅 ) = ( ( 𝑃 + 𝑅 ) + 2 ) )
71 70 eqeq2d ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 ∈ Even ) → ( ( 𝑁 + 2 ) = ( ( 𝑃 + 2 ) + 𝑅 ) ↔ ( 𝑁 + 2 ) = ( ( 𝑃 + 𝑅 ) + 2 ) ) )
72 28 adantl ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 ∈ Even ) → 𝑁 ∈ ℂ )
73 zaddcl ( ( 𝑃 ∈ ℤ ∧ 𝑅 ∈ ℤ ) → ( 𝑃 + 𝑅 ) ∈ ℤ )
74 62 16 73 syl2an ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℙ ) → ( 𝑃 + 𝑅 ) ∈ ℤ )
75 74 zcnd ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℙ ) → ( 𝑃 + 𝑅 ) ∈ ℂ )
76 75 adantr ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 ∈ Even ) → ( 𝑃 + 𝑅 ) ∈ ℂ )
77 2cnd ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 ∈ Even ) → 2 ∈ ℂ )
78 72 76 77 addcan2d ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 ∈ Even ) → ( ( 𝑁 + 2 ) = ( ( 𝑃 + 𝑅 ) + 2 ) ↔ 𝑁 = ( 𝑃 + 𝑅 ) ) )
79 71 78 bitrd ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 ∈ Even ) → ( ( 𝑁 + 2 ) = ( ( 𝑃 + 2 ) + 𝑅 ) ↔ 𝑁 = ( 𝑃 + 𝑅 ) ) )
80 simpll ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 = ( 𝑃 + 𝑅 ) ) → 𝑃 ∈ ℙ )
81 oveq1 ( 𝑝 = 𝑃 → ( 𝑝 + 𝑞 ) = ( 𝑃 + 𝑞 ) )
82 81 eqeq2d ( 𝑝 = 𝑃 → ( 𝑁 = ( 𝑝 + 𝑞 ) ↔ 𝑁 = ( 𝑃 + 𝑞 ) ) )
83 82 rexbidv ( 𝑝 = 𝑃 → ( ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑝 + 𝑞 ) ↔ ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑃 + 𝑞 ) ) )
84 83 adantl ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 = ( 𝑃 + 𝑅 ) ) ∧ 𝑝 = 𝑃 ) → ( ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑝 + 𝑞 ) ↔ ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑃 + 𝑞 ) ) )
85 simplr ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 = ( 𝑃 + 𝑅 ) ) → 𝑅 ∈ ℙ )
86 simpr ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 = ( 𝑃 + 𝑅 ) ) → 𝑁 = ( 𝑃 + 𝑅 ) )
87 oveq2 ( 𝑞 = 𝑅 → ( 𝑃 + 𝑞 ) = ( 𝑃 + 𝑅 ) )
88 87 eqcomd ( 𝑞 = 𝑅 → ( 𝑃 + 𝑅 ) = ( 𝑃 + 𝑞 ) )
89 86 88 sylan9eq ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 = ( 𝑃 + 𝑅 ) ) ∧ 𝑞 = 𝑅 ) → 𝑁 = ( 𝑃 + 𝑞 ) )
90 85 89 rspcedeq2vd ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 = ( 𝑃 + 𝑅 ) ) → ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑃 + 𝑞 ) )
91 80 84 90 rspcedvd ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 = ( 𝑃 + 𝑅 ) ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑝 + 𝑞 ) )
92 91 ex ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℙ ) → ( 𝑁 = ( 𝑃 + 𝑅 ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑝 + 𝑞 ) ) )
93 92 adantr ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 ∈ Even ) → ( 𝑁 = ( 𝑃 + 𝑅 ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑝 + 𝑞 ) ) )
94 79 93 sylbid ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 ∈ Even ) → ( ( 𝑁 + 2 ) = ( ( 𝑃 + 2 ) + 𝑅 ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑝 + 𝑞 ) ) )
95 94 com12 ( ( 𝑁 + 2 ) = ( ( 𝑃 + 2 ) + 𝑅 ) → ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 ∈ Even ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑝 + 𝑞 ) ) )
96 61 95 syl6bi ( 𝑄 = 2 → ( ( 𝑁 + 2 ) = ( ( 𝑃 + 𝑄 ) + 𝑅 ) → ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 ∈ Even ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑝 + 𝑞 ) ) ) )
97 96 com13 ( ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 ∈ Even ) → ( ( 𝑁 + 2 ) = ( ( 𝑃 + 𝑄 ) + 𝑅 ) → ( 𝑄 = 2 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑝 + 𝑞 ) ) ) )
98 97 ex ( ( 𝑃 ∈ ℙ ∧ 𝑅 ∈ ℙ ) → ( 𝑁 ∈ Even → ( ( 𝑁 + 2 ) = ( ( 𝑃 + 𝑄 ) + 𝑅 ) → ( 𝑄 = 2 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑝 + 𝑞 ) ) ) ) )
99 98 3adant2 ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) → ( 𝑁 ∈ Even → ( ( 𝑁 + 2 ) = ( ( 𝑃 + 𝑄 ) + 𝑅 ) → ( 𝑄 = 2 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑝 + 𝑞 ) ) ) ) )
100 99 3imp ( ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 ∈ Even ∧ ( 𝑁 + 2 ) = ( ( 𝑃 + 𝑄 ) + 𝑅 ) ) → ( 𝑄 = 2 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑝 + 𝑞 ) ) )
101 100 com12 ( 𝑄 = 2 → ( ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 ∈ Even ∧ ( 𝑁 + 2 ) = ( ( 𝑃 + 𝑄 ) + 𝑅 ) ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑝 + 𝑞 ) ) )
102 oveq2 ( 𝑅 = 2 → ( ( 𝑃 + 𝑄 ) + 𝑅 ) = ( ( 𝑃 + 𝑄 ) + 2 ) )
103 102 eqeq2d ( 𝑅 = 2 → ( ( 𝑁 + 2 ) = ( ( 𝑃 + 𝑄 ) + 𝑅 ) ↔ ( 𝑁 + 2 ) = ( ( 𝑃 + 𝑄 ) + 2 ) ) )
104 28 adantl ( ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) ∧ 𝑁 ∈ Even ) → 𝑁 ∈ ℂ )
105 zaddcl ( ( 𝑃 ∈ ℤ ∧ 𝑄 ∈ ℤ ) → ( 𝑃 + 𝑄 ) ∈ ℤ )
106 62 13 105 syl2an ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) → ( 𝑃 + 𝑄 ) ∈ ℤ )
107 106 zcnd ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) → ( 𝑃 + 𝑄 ) ∈ ℂ )
108 107 adantr ( ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) ∧ 𝑁 ∈ Even ) → ( 𝑃 + 𝑄 ) ∈ ℂ )
109 2cnd ( ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) ∧ 𝑁 ∈ Even ) → 2 ∈ ℂ )
110 104 108 109 addcan2d ( ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) ∧ 𝑁 ∈ Even ) → ( ( 𝑁 + 2 ) = ( ( 𝑃 + 𝑄 ) + 2 ) ↔ 𝑁 = ( 𝑃 + 𝑄 ) ) )
111 simpll ( ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) ∧ 𝑁 = ( 𝑃 + 𝑄 ) ) → 𝑃 ∈ ℙ )
112 83 adantl ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) ∧ 𝑁 = ( 𝑃 + 𝑄 ) ) ∧ 𝑝 = 𝑃 ) → ( ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑝 + 𝑞 ) ↔ ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑃 + 𝑞 ) ) )
113 simplr ( ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) ∧ 𝑁 = ( 𝑃 + 𝑄 ) ) → 𝑄 ∈ ℙ )
114 simpr ( ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) ∧ 𝑁 = ( 𝑃 + 𝑄 ) ) → 𝑁 = ( 𝑃 + 𝑄 ) )
115 oveq2 ( 𝑞 = 𝑄 → ( 𝑃 + 𝑞 ) = ( 𝑃 + 𝑄 ) )
116 115 eqcomd ( 𝑞 = 𝑄 → ( 𝑃 + 𝑄 ) = ( 𝑃 + 𝑞 ) )
117 114 116 sylan9eq ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) ∧ 𝑁 = ( 𝑃 + 𝑄 ) ) ∧ 𝑞 = 𝑄 ) → 𝑁 = ( 𝑃 + 𝑞 ) )
118 113 117 rspcedeq2vd ( ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) ∧ 𝑁 = ( 𝑃 + 𝑄 ) ) → ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑃 + 𝑞 ) )
119 111 112 118 rspcedvd ( ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) ∧ 𝑁 = ( 𝑃 + 𝑄 ) ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑝 + 𝑞 ) )
120 119 ex ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) → ( 𝑁 = ( 𝑃 + 𝑄 ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑝 + 𝑞 ) ) )
121 120 adantr ( ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) ∧ 𝑁 ∈ Even ) → ( 𝑁 = ( 𝑃 + 𝑄 ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑝 + 𝑞 ) ) )
122 110 121 sylbid ( ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) ∧ 𝑁 ∈ Even ) → ( ( 𝑁 + 2 ) = ( ( 𝑃 + 𝑄 ) + 2 ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑝 + 𝑞 ) ) )
123 122 com12 ( ( 𝑁 + 2 ) = ( ( 𝑃 + 𝑄 ) + 2 ) → ( ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) ∧ 𝑁 ∈ Even ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑝 + 𝑞 ) ) )
124 103 123 syl6bi ( 𝑅 = 2 → ( ( 𝑁 + 2 ) = ( ( 𝑃 + 𝑄 ) + 𝑅 ) → ( ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) ∧ 𝑁 ∈ Even ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑝 + 𝑞 ) ) ) )
125 124 com13 ( ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) ∧ 𝑁 ∈ Even ) → ( ( 𝑁 + 2 ) = ( ( 𝑃 + 𝑄 ) + 𝑅 ) → ( 𝑅 = 2 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑝 + 𝑞 ) ) ) )
126 125 ex ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ) → ( 𝑁 ∈ Even → ( ( 𝑁 + 2 ) = ( ( 𝑃 + 𝑄 ) + 𝑅 ) → ( 𝑅 = 2 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑝 + 𝑞 ) ) ) ) )
127 126 3adant3 ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) → ( 𝑁 ∈ Even → ( ( 𝑁 + 2 ) = ( ( 𝑃 + 𝑄 ) + 𝑅 ) → ( 𝑅 = 2 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑝 + 𝑞 ) ) ) ) )
128 127 3imp ( ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 ∈ Even ∧ ( 𝑁 + 2 ) = ( ( 𝑃 + 𝑄 ) + 𝑅 ) ) → ( 𝑅 = 2 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑝 + 𝑞 ) ) )
129 128 com12 ( 𝑅 = 2 → ( ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 ∈ Even ∧ ( 𝑁 + 2 ) = ( ( 𝑃 + 𝑄 ) + 𝑅 ) ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑝 + 𝑞 ) ) )
130 58 101 129 3jaoi ( ( 𝑃 = 2 ∨ 𝑄 = 2 ∨ 𝑅 = 2 ) → ( ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 ∈ Even ∧ ( 𝑁 + 2 ) = ( ( 𝑃 + 𝑄 ) + 𝑅 ) ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑝 + 𝑞 ) ) )
131 8 130 mpcom ( ( ( 𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ ) ∧ 𝑁 ∈ Even ∧ ( 𝑁 + 2 ) = ( ( 𝑃 + 𝑄 ) + 𝑅 ) ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑝 + 𝑞 ) )