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

Metamath Proof Explorer

Theorem sbgoldbalt

Description: An alternate (related to the original) formulation of the binary Goldbach conjecture: Every even integer greater than 2 can be expressed as the sum of two primes. (Contributed by AV, 22-Jul-2020)

Ref Expression
Assertion sbgoldbalt ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) ↔ ∀ 𝑛 ∈ Even ( 2 < 𝑛 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) )

Proof

Step Hyp Ref Expression
1 2z ⊢ 2 ∈ ℤ
2 evenz ⊢ ( 𝑛 ∈ Even → 𝑛 ∈ ℤ )
3 zltp1le ⊢ ( ( 2 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 2 < 𝑛 ↔ ( 2 + 1 ) ≤ 𝑛 ) )
4 1 2 3 sylancr ⊢ ( 𝑛 ∈ Even → ( 2 < 𝑛 ↔ ( 2 + 1 ) ≤ 𝑛 ) )
5 2p1e3 ⊢ ( 2 + 1 ) = 3
6 5 breq1i ⊢ ( ( 2 + 1 ) ≤ 𝑛 ↔ 3 ≤ 𝑛 )
7 3re ⊢ 3 ∈ ℝ
8 7 a1i ⊢ ( 𝑛 ∈ Even → 3 ∈ ℝ )
9 2 zred ⊢ ( 𝑛 ∈ Even → 𝑛 ∈ ℝ )
10 8 9 leloed ⊢ ( 𝑛 ∈ Even → ( 3 ≤ 𝑛 ↔ ( 3 < 𝑛 ∨ 3 = 𝑛 ) ) )
11 3z ⊢ 3 ∈ ℤ
12 zltp1le ⊢ ( ( 3 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 3 < 𝑛 ↔ ( 3 + 1 ) ≤ 𝑛 ) )
13 11 2 12 sylancr ⊢ ( 𝑛 ∈ Even → ( 3 < 𝑛 ↔ ( 3 + 1 ) ≤ 𝑛 ) )
14 3p1e4 ⊢ ( 3 + 1 ) = 4
15 14 breq1i ⊢ ( ( 3 + 1 ) ≤ 𝑛 ↔ 4 ≤ 𝑛 )
16 4re ⊢ 4 ∈ ℝ
17 16 a1i ⊢ ( 𝑛 ∈ Even → 4 ∈ ℝ )
18 17 9 leloed ⊢ ( 𝑛 ∈ Even → ( 4 ≤ 𝑛 ↔ ( 4 < 𝑛 ∨ 4 = 𝑛 ) ) )
19 pm3.35 ⊢ ( ( 4 < 𝑛 ∧ ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) ) → 𝑛 ∈ GoldbachEven )
20 isgbe ⊢ ( 𝑛 ∈ GoldbachEven ↔ ( 𝑛 ∈ Even ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
21 simp3 ⊢ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) → 𝑛 = ( 𝑝 + 𝑞 ) )
22 21 a1i ⊢ ( ( ( 𝑛 ∈ Even ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) → ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) → 𝑛 = ( 𝑝 + 𝑞 ) ) )
23 22 reximdva ⊢ ( ( 𝑛 ∈ Even ∧ 𝑝 ∈ ℙ ) → ( ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) → ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) )
24 23 reximdva ⊢ ( 𝑛 ∈ Even → ( ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) )
25 24 imp ⊢ ( ( 𝑛 ∈ Even ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) )
26 20 25 sylbi ⊢ ( 𝑛 ∈ GoldbachEven → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) )
27 26 a1d ⊢ ( 𝑛 ∈ GoldbachEven → ( 𝑛 ∈ Even → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) )
28 19 27 syl ⊢ ( ( 4 < 𝑛 ∧ ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) ) → ( 𝑛 ∈ Even → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) )
29 28 ex ⊢ ( 4 < 𝑛 → ( ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ( 𝑛 ∈ Even → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
30 29 com23 ⊢ ( 4 < 𝑛 → ( 𝑛 ∈ Even → ( ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
31 2prm ⊢ 2 ∈ ℙ
32 2p2e4 ⊢ ( 2 + 2 ) = 4
33 32 eqcomi ⊢ 4 = ( 2 + 2 )
34 rspceov ⊢ ( ( 2 ∈ ℙ ∧ 2 ∈ ℙ ∧ 4 = ( 2 + 2 ) ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 4 = ( 𝑝 + 𝑞 ) )
35 31 31 33 34 mp3an ⊢ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 4 = ( 𝑝 + 𝑞 )
36 eqeq1 ⊢ ( 4 = 𝑛 → ( 4 = ( 𝑝 + 𝑞 ) ↔ 𝑛 = ( 𝑝 + 𝑞 ) ) )
37 36 2rexbidv ⊢ ( 4 = 𝑛 → ( ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 4 = ( 𝑝 + 𝑞 ) ↔ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) )
38 35 37 mpbii ⊢ ( 4 = 𝑛 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) )
39 38 a1d ⊢ ( 4 = 𝑛 → ( ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) )
40 39 a1d ⊢ ( 4 = 𝑛 → ( 𝑛 ∈ Even → ( ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
41 30 40 jaoi ⊢ ( ( 4 < 𝑛 ∨ 4 = 𝑛 ) → ( 𝑛 ∈ Even → ( ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
42 41 com12 ⊢ ( 𝑛 ∈ Even → ( ( 4 < 𝑛 ∨ 4 = 𝑛 ) → ( ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
43 18 42 sylbid ⊢ ( 𝑛 ∈ Even → ( 4 ≤ 𝑛 → ( ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
44 15 43 biimtrid ⊢ ( 𝑛 ∈ Even → ( ( 3 + 1 ) ≤ 𝑛 → ( ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
45 13 44 sylbid ⊢ ( 𝑛 ∈ Even → ( 3 < 𝑛 → ( ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
46 45 com12 ⊢ ( 3 < 𝑛 → ( 𝑛 ∈ Even → ( ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
47 3odd ⊢ 3 ∈ Odd
48 eleq1 ⊢ ( 3 = 𝑛 → ( 3 ∈ Odd ↔ 𝑛 ∈ Odd ) )
49 47 48 mpbii ⊢ ( 3 = 𝑛 → 𝑛 ∈ Odd )
50 oddneven ⊢ ( 𝑛 ∈ Odd → ¬ 𝑛 ∈ Even )
51 49 50 syl ⊢ ( 3 = 𝑛 → ¬ 𝑛 ∈ Even )
52 51 pm2.21d ⊢ ( 3 = 𝑛 → ( 𝑛 ∈ Even → ( ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
53 46 52 jaoi ⊢ ( ( 3 < 𝑛 ∨ 3 = 𝑛 ) → ( 𝑛 ∈ Even → ( ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
54 53 com12 ⊢ ( 𝑛 ∈ Even → ( ( 3 < 𝑛 ∨ 3 = 𝑛 ) → ( ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
55 10 54 sylbid ⊢ ( 𝑛 ∈ Even → ( 3 ≤ 𝑛 → ( ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
56 6 55 biimtrid ⊢ ( 𝑛 ∈ Even → ( ( 2 + 1 ) ≤ 𝑛 → ( ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
57 4 56 sylbid ⊢ ( 𝑛 ∈ Even → ( 2 < 𝑛 → ( ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
58 57 com23 ⊢ ( 𝑛 ∈ Even → ( ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ( 2 < 𝑛 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
59 2lt4 ⊢ 2 < 4
60 2re ⊢ 2 ∈ ℝ
61 60 a1i ⊢ ( 𝑛 ∈ Even → 2 ∈ ℝ )
62 lttr ⊢ ( ( 2 ∈ ℝ ∧ 4 ∈ ℝ ∧ 𝑛 ∈ ℝ ) → ( ( 2 < 4 ∧ 4 < 𝑛 ) → 2 < 𝑛 ) )
63 61 17 9 62 syl3anc ⊢ ( 𝑛 ∈ Even → ( ( 2 < 4 ∧ 4 < 𝑛 ) → 2 < 𝑛 ) )
64 59 63 mpani ⊢ ( 𝑛 ∈ Even → ( 4 < 𝑛 → 2 < 𝑛 ) )
65 64 imp ⊢ ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) → 2 < 𝑛 )
66 simpll ⊢ ( ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) → 𝑛 ∈ Even )
67 simpr ⊢ ( ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℙ )
68 67 anim1i ⊢ ( ( ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) → ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) )
69 68 adantr ⊢ ( ( ( ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) → ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) )
70 simpll ⊢ ( ( ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) → ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) )
71 70 anim1i ⊢ ( ( ( ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) → ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) )
72 df-3an ⊢ ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) ↔ ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) )
73 71 72 sylibr ⊢ ( ( ( ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) → ( 𝑛 ∈ Even ∧ 4 < 𝑛 ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) )
74 sbgoldbaltlem2 ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) → ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) → ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ) ) )
75 69 73 74 sylc ⊢ ( ( ( ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) → ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ) )
76 simpr ⊢ ( ( ( ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) → 𝑛 = ( 𝑝 + 𝑞 ) )
77 df-3an ⊢ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) ↔ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ) ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) )
78 75 76 77 sylanbrc ⊢ ( ( ( ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) → ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) )
79 78 ex ⊢ ( ( ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) → ( 𝑛 = ( 𝑝 + 𝑞 ) → ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
80 79 reximdva ⊢ ( ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) ∧ 𝑝 ∈ ℙ ) → ( ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) → ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
81 80 reximdva ⊢ ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) → ( ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
82 81 imp ⊢ ( ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) )
83 66 82 jca ⊢ ( ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) → ( 𝑛 ∈ Even ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
84 83 ex ⊢ ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) → ( ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) → ( 𝑛 ∈ Even ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑛 = ( 𝑝 + 𝑞 ) ) ) ) )
85 84 20 imbitrrdi ⊢ ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) → ( ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) → 𝑛 ∈ GoldbachEven ) )
86 65 85 embantd ⊢ ( ( 𝑛 ∈ Even ∧ 4 < 𝑛 ) → ( ( 2 < 𝑛 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) → 𝑛 ∈ GoldbachEven ) )
87 86 ex ⊢ ( 𝑛 ∈ Even → ( 4 < 𝑛 → ( ( 2 < 𝑛 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) → 𝑛 ∈ GoldbachEven ) ) )
88 87 com23 ⊢ ( 𝑛 ∈ Even → ( ( 2 < 𝑛 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) → ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) ) )
89 58 88 impbid ⊢ ( 𝑛 ∈ Even → ( ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) ↔ ( 2 < 𝑛 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
90 89 ralbiia ⊢ ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) ↔ ∀ 𝑛 ∈ Even ( 2 < 𝑛 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) )