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