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