Metamath Proof Explorer

Theorem 7gbow

Description: 7 is a weak odd Goldbach number. (Contributed by AV, 20-Jul-2020)

Ref Expression
Assertion 7gbow 
|- 7 e. GoldbachOddW

Proof

Step Hyp Ref Expression
1 7odd 
 |-  7 e. Odd
2 2prm 
 |-  2 e. Prime
3 3prm 
 |-  3 e. Prime
4 gbpart7 
 |-  7 = ( ( 2 + 2 ) + 3 )
5 oveq2 
 |-  ( r = 3 -> ( ( 2 + 2 ) + r ) = ( ( 2 + 2 ) + 3 ) )
6 5 rspceeqv 
 |-  ( ( 3 e. Prime /\ 7 = ( ( 2 + 2 ) + 3 ) ) -> E. r e. Prime 7 = ( ( 2 + 2 ) + r ) )
7 3 4 6 mp2an 
 |-  E. r e. Prime 7 = ( ( 2 + 2 ) + r )
8 oveq1 
 |-  ( p = 2 -> ( p + q ) = ( 2 + q ) )
9 8 oveq1d 
 |-  ( p = 2 -> ( ( p + q ) + r ) = ( ( 2 + q ) + r ) )
10 9 eqeq2d 
 |-  ( p = 2 -> ( 7 = ( ( p + q ) + r ) <-> 7 = ( ( 2 + q ) + r ) ) )
11 10 rexbidv 
 |-  ( p = 2 -> ( E. r e. Prime 7 = ( ( p + q ) + r ) <-> E. r e. Prime 7 = ( ( 2 + q ) + r ) ) )
12 oveq2 
 |-  ( q = 2 -> ( 2 + q ) = ( 2 + 2 ) )
13 12 oveq1d 
 |-  ( q = 2 -> ( ( 2 + q ) + r ) = ( ( 2 + 2 ) + r ) )
14 13 eqeq2d 
 |-  ( q = 2 -> ( 7 = ( ( 2 + q ) + r ) <-> 7 = ( ( 2 + 2 ) + r ) ) )
15 14 rexbidv 
 |-  ( q = 2 -> ( E. r e. Prime 7 = ( ( 2 + q ) + r ) <-> E. r e. Prime 7 = ( ( 2 + 2 ) + r ) ) )
16 11 15 rspc2ev 
 |-  ( ( 2 e. Prime /\ 2 e. Prime /\ E. r e. Prime 7 = ( ( 2 + 2 ) + r ) ) -> E. p e. Prime E. q e. Prime E. r e. Prime 7 = ( ( p + q ) + r ) )
17 2 2 7 16 mp3an 
 |-  E. p e. Prime E. q e. Prime E. r e. Prime 7 = ( ( p + q ) + r )
18 isgbow 
 |-  ( 7 e. GoldbachOddW <-> ( 7 e. Odd /\ E. p e. Prime E. q e. Prime E. r e. Prime 7 = ( ( p + q ) + r ) ) )
19 1 17 18 mpbir2an 
 |-  7 e. GoldbachOddW