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