Metamath Proof Explorer


Theorem 6gbe

Description: 6 is an even Goldbach number. (Contributed by AV, 20-Jul-2020)

Ref Expression
Assertion 6gbe 6GoldbachEven

Proof

Step Hyp Ref Expression
1 6even 6Even
2 3prm 3
3 3odd 3Odd
4 gbpart6 6=3+3
5 3 3 4 3pm3.2i 3Odd3Odd6=3+3
6 eleq1 p=3pOdd3Odd
7 biidd p=3qOddqOdd
8 oveq1 p=3p+q=3+q
9 8 eqeq2d p=36=p+q6=3+q
10 6 7 9 3anbi123d p=3pOddqOdd6=p+q3OddqOdd6=3+q
11 biidd q=33Odd3Odd
12 eleq1 q=3qOdd3Odd
13 oveq2 q=33+q=3+3
14 13 eqeq2d q=36=3+q6=3+3
15 11 12 14 3anbi123d q=33OddqOdd6=3+q3Odd3Odd6=3+3
16 10 15 rspc2ev 333Odd3Odd6=3+3pqpOddqOdd6=p+q
17 2 2 5 16 mp3an pqpOddqOdd6=p+q
18 isgbe 6GoldbachEven6EvenpqpOddqOdd6=p+q
19 1 17 18 mpbir2an 6GoldbachEven