Metamath Proof Explorer


Theorem 8gbe

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

Ref Expression
Assertion 8gbe 8GoldbachEven

Proof

Step Hyp Ref Expression
1 8even 8Even
2 5prm 5
3 3prm 3
4 5odd 5Odd
5 3odd 3Odd
6 5p3e8 5+3=8
7 6 eqcomi 8=5+3
8 4 5 7 3pm3.2i 5Odd3Odd8=5+3
9 eleq1 p=5pOdd5Odd
10 biidd p=5qOddqOdd
11 oveq1 p=5p+q=5+q
12 11 eqeq2d p=58=p+q8=5+q
13 9 10 12 3anbi123d p=5pOddqOdd8=p+q5OddqOdd8=5+q
14 biidd q=35Odd5Odd
15 eleq1 q=3qOdd3Odd
16 oveq2 q=35+q=5+3
17 16 eqeq2d q=38=5+q8=5+3
18 14 15 17 3anbi123d q=35OddqOdd8=5+q5Odd3Odd8=5+3
19 13 18 rspc2ev 535Odd3Odd8=5+3pqpOddqOdd8=p+q
20 2 3 8 19 mp3an pqpOddqOdd8=p+q
21 isgbe 8GoldbachEven8EvenpqpOddqOdd8=p+q
22 1 20 21 mpbir2an 8GoldbachEven