Metamath Proof Explorer

Theorem 6gbe

Description: 6 is an even Goldbach number. (Contributed by AV, 20-Jul-2020)

Ref Expression
Assertion 6gbe ⊢ 6 ∈ GoldbachEven

Proof

Step Hyp Ref Expression
1 6even ⊢ 6 ∈ Even
2 3prm ⊢ 3 ∈ ℙ
3 3odd ⊢ 3 ∈ Odd
4 gbpart6 ⊢ 6 = 3 + 3
5 3 3 4 3pm3.2i ⊢ 3 ∈ Odd ∧ 3 ∈ Odd ∧ 6 = 3 + 3
6 eleq1 ⊢ p = 3 → p ∈ Odd ↔ 3 ∈ Odd
7 biidd ⊢ p = 3 → q ∈ Odd ↔ q ∈ Odd
8 oveq1 ⊢ p = 3 → p + q = 3 + q
9 8 eqeq2d ⊢ p = 3 → 6 = p + q ↔ 6 = 3 + q
10 6 7 9 3anbi123d ⊢ p = 3 → p ∈ Odd ∧ q ∈ Odd ∧ 6 = p + q ↔ 3 ∈ Odd ∧ q ∈ Odd ∧ 6 = 3 + q
11 biidd ⊢ q = 3 → 3 ∈ Odd ↔ 3 ∈ Odd
12 eleq1 ⊢ q = 3 → q ∈ Odd ↔ 3 ∈ Odd
13 oveq2 ⊢ q = 3 → 3 + q = 3 + 3
14 13 eqeq2d ⊢ q = 3 → 6 = 3 + q ↔ 6 = 3 + 3
15 11 12 14 3anbi123d ⊢ q = 3 → 3 ∈ Odd ∧ q ∈ Odd ∧ 6 = 3 + q ↔ 3 ∈ Odd ∧ 3 ∈ Odd ∧ 6 = 3 + 3
16 10 15 rspc2ev ⊢ 3 ∈ ℙ ∧ 3 ∈ ℙ ∧ 3 ∈ Odd ∧ 3 ∈ Odd ∧ 6 = 3 + 3 → ∃ p ∈ ℙ ∃ q ∈ ℙ p ∈ Odd ∧ q ∈ Odd ∧ 6 = p + q
17 2 2 5 16 mp3an ⊢ ∃ p ∈ ℙ ∃ q ∈ ℙ p ∈ Odd ∧ q ∈ Odd ∧ 6 = p + q
18 isgbe ⊢ 6 ∈ GoldbachEven ↔ 6 ∈ Even ∧ ∃ p ∈ ℙ ∃ q ∈ ℙ p ∈ Odd ∧ q ∈ Odd ∧ 6 = p + q
19 1 17 18 mpbir2an ⊢ 6 ∈ GoldbachEven