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

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 ⊢ ( 𝑝 = 5 → ( 𝑝 ∈ Odd ↔ 5 ∈ Odd ) )
10 biidd ⊢ ( 𝑝 = 5 → ( 𝑞 ∈ Odd ↔ 𝑞 ∈ Odd ) )
11 oveq1 ⊢ ( 𝑝 = 5 → ( 𝑝 + 𝑞 ) = ( 5 + 𝑞 ) )
12 11 eqeq2d ⊢ ( 𝑝 = 5 → ( 8 = ( 𝑝 + 𝑞 ) ↔ 8 = ( 5 + 𝑞 ) ) )
13 9 10 12 3anbi123d ⊢ ( 𝑝 = 5 → ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 8 = ( 𝑝 + 𝑞 ) ) ↔ ( 5 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 8 = ( 5 + 𝑞 ) ) ) )
14 biidd ⊢ ( 𝑞 = 3 → ( 5 ∈ Odd ↔ 5 ∈ Odd ) )
15 eleq1 ⊢ ( 𝑞 = 3 → ( 𝑞 ∈ Odd ↔ 3 ∈ Odd ) )
16 oveq2 ⊢ ( 𝑞 = 3 → ( 5 + 𝑞 ) = ( 5 + 3 ) )
17 16 eqeq2d ⊢ ( 𝑞 = 3 → ( 8 = ( 5 + 𝑞 ) ↔ 8 = ( 5 + 3 ) ) )
18 14 15 17 3anbi123d ⊢ ( 𝑞 = 3 → ( ( 5 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 8 = ( 5 + 𝑞 ) ) ↔ ( 5 ∈ Odd ∧ 3 ∈ Odd ∧ 8 = ( 5 + 3 ) ) ) )
19 13 18 rspc2ev ⊢ ( ( 5 ∈ ℙ ∧ 3 ∈ ℙ ∧ ( 5 ∈ Odd ∧ 3 ∈ Odd ∧ 8 = ( 5 + 3 ) ) ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 8 = ( 𝑝 + 𝑞 ) ) )
20 2 3 8 19 mp3an ⊢ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 8 = ( 𝑝 + 𝑞 ) )
21 isgbe ⊢ ( 8 ∈ GoldbachEven ↔ ( 8 ∈ Even ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 8 = ( 𝑝 + 𝑞 ) ) ) )
22 1 20 21 mpbir2an ⊢ 8 ∈ GoldbachEven