Metamath Proof Explorer

Theorem gbogbow

Description: A (strong) odd Goldbach number is a weak Goldbach number. (Contributed by AV, 26-Jul-2020)

Ref Expression
Assertion gbogbow 
|- ( Z e. GoldbachOdd -> Z e. GoldbachOddW )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ Z = ( ( p + q ) + r ) ) -> Z = ( ( p + q ) + r ) )
2 1 reximi 
 |-  ( E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ Z = ( ( p + q ) + r ) ) -> E. r e. Prime Z = ( ( p + q ) + r ) )
3 2 reximi 
 |-  ( E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ Z = ( ( p + q ) + r ) ) -> E. q e. Prime E. r e. Prime Z = ( ( p + q ) + r ) )
4 3 reximi 
 |-  ( E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ Z = ( ( p + q ) + r ) ) -> E. p e. Prime E. q e. Prime E. r e. Prime Z = ( ( p + q ) + r ) )
5 4 anim2i 
 |-  ( ( Z e. Odd /\ E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ Z = ( ( p + q ) + r ) ) ) -> ( Z e. Odd /\ E. p e. Prime E. q e. Prime E. r e. Prime Z = ( ( p + q ) + r ) ) )
6 isgbo 
 |-  ( Z e. GoldbachOdd <-> ( Z e. Odd /\ E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ Z = ( ( p + q ) + r ) ) ) )
7 isgbow 
 |-  ( Z e. GoldbachOddW <-> ( Z e. Odd /\ E. p e. Prime E. q e. Prime E. r e. Prime Z = ( ( p + q ) + r ) ) )
8 5 6 7 3imtr4i 
 |-  ( Z e. GoldbachOdd -> Z e. GoldbachOddW )