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

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