Metamath Proof Explorer

Theorem 8gbe

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

Ref Expression
Assertion 8gbe ⊢ 8 ∈ GoldbachEven

Proof

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