This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrdi ⊢ ( 𝑃 = 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 biimtrdi ⊢ ( 𝑄 = 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 biimtrdi ⊢ ( 𝑅 = 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 ) = ( ( 𝑃 + 𝑄 ) + 𝑅 ) ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑁 = ( 𝑝 + 𝑞 ) )