Metamath Proof Explorer

Theorem sbgoldbm

Description: If the strong binary Goldbach conjecture is valid, the modern version of the original formulation of the Goldbach conjecture also holds: Every integer greater than 5 can be expressed as the sum of three primes. (Contributed by AV, 24-Dec-2021)

Ref Expression
Assertion sbgoldbm 
|- ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> A. n e. ( ZZ>= ` 6 ) E. p e. Prime E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) )

Proof

Step Hyp Ref Expression
1 breq2 
 |-  ( n = m -> ( 4 < n <-> 4 < m ) )
2 eleq1w 
 |-  ( n = m -> ( n e. GoldbachEven <-> m e. GoldbachEven ) )
3 1 2 imbi12d 
 |-  ( n = m -> ( ( 4 < n -> n e. GoldbachEven ) <-> ( 4 < m -> m e. GoldbachEven ) ) )
4 3 cbvralvw 
 |-  ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) <-> A. m e. Even ( 4 < m -> m e. GoldbachEven ) )
5 eluz2 
 |-  ( n e. ( ZZ>= ` 6 ) <-> ( 6 e. ZZ /\ n e. ZZ /\ 6 <_ n ) )
6 zeoALTV 
 |-  ( n e. ZZ -> ( n e. Even \/ n e. Odd ) )
7 sgoldbeven3prm 
 |-  ( A. m e. Even ( 4 < m -> m e. GoldbachEven ) -> ( ( n e. Even /\ 6 <_ n ) -> E. p e. Prime E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) ) )
8 7 expdcom 
 |-  ( n e. Even -> ( 6 <_ n -> ( A. m e. Even ( 4 < m -> m e. GoldbachEven ) -> E. p e. Prime E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) ) ) )
9 sbgoldbwt 
 |-  ( A. m e. Even ( 4 < m -> m e. GoldbachEven ) -> A. n e. Odd ( 5 < n -> n e. GoldbachOddW ) )
10 rspa 
 |-  ( ( A. n e. Odd ( 5 < n -> n e. GoldbachOddW ) /\ n e. Odd ) -> ( 5 < n -> n e. GoldbachOddW ) )
11 df-6 
 |-  6 = ( 5 + 1 )
12 11 breq1i 
 |-  ( 6 <_ n <-> ( 5 + 1 ) <_ n )
13 5nn 
 |-  5 e. NN
14 13 nnzi 
 |-  5 e. ZZ
15 oddz 
 |-  ( n e. Odd -> n e. ZZ )
16 zltp1le 
 |-  ( ( 5 e. ZZ /\ n e. ZZ ) -> ( 5 < n <-> ( 5 + 1 ) <_ n ) )
17 14 15 16 sylancr 
 |-  ( n e. Odd -> ( 5 < n <-> ( 5 + 1 ) <_ n ) )
18 17 biimprd 
 |-  ( n e. Odd -> ( ( 5 + 1 ) <_ n -> 5 < n ) )
19 12 18 biimtrid 
 |-  ( n e. Odd -> ( 6 <_ n -> 5 < n ) )
20 19 imp 
 |-  ( ( n e. Odd /\ 6 <_ n ) -> 5 < n )
21 isgbow 
 |-  ( n e. GoldbachOddW <-> ( n e. Odd /\ E. p e. Prime E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) ) )
22 21 simprbi 
 |-  ( n e. GoldbachOddW -> E. p e. Prime E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) )
23 22 a1i 
 |-  ( ( n e. Odd /\ 6 <_ n ) -> ( n e. GoldbachOddW -> E. p e. Prime E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) ) )
24 20 23 embantd 
 |-  ( ( n e. Odd /\ 6 <_ n ) -> ( ( 5 < n -> n e. GoldbachOddW ) -> E. p e. Prime E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) ) )
25 24 ex 
 |-  ( n e. Odd -> ( 6 <_ n -> ( ( 5 < n -> n e. GoldbachOddW ) -> E. p e. Prime E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) ) ) )
26 25 com23 
 |-  ( n e. Odd -> ( ( 5 < n -> n e. GoldbachOddW ) -> ( 6 <_ n -> E. p e. Prime E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) ) ) )
27 26 adantl 
 |-  ( ( A. n e. Odd ( 5 < n -> n e. GoldbachOddW ) /\ n e. Odd ) -> ( ( 5 < n -> n e. GoldbachOddW ) -> ( 6 <_ n -> E. p e. Prime E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) ) ) )
28 10 27 mpd 
 |-  ( ( A. n e. Odd ( 5 < n -> n e. GoldbachOddW ) /\ n e. Odd ) -> ( 6 <_ n -> E. p e. Prime E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) ) )
29 28 ex 
 |-  ( A. n e. Odd ( 5 < n -> n e. GoldbachOddW ) -> ( n e. Odd -> ( 6 <_ n -> E. p e. Prime E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) ) ) )
30 29 com23 
 |-  ( A. n e. Odd ( 5 < n -> n e. GoldbachOddW ) -> ( 6 <_ n -> ( n e. Odd -> E. p e. Prime E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) ) ) )
31 9 30 syl 
 |-  ( A. m e. Even ( 4 < m -> m e. GoldbachEven ) -> ( 6 <_ n -> ( n e. Odd -> E. p e. Prime E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) ) ) )
32 31 com13 
 |-  ( n e. Odd -> ( 6 <_ n -> ( A. m e. Even ( 4 < m -> m e. GoldbachEven ) -> E. p e. Prime E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) ) ) )
33 8 32 jaoi 
 |-  ( ( n e. Even \/ n e. Odd ) -> ( 6 <_ n -> ( A. m e. Even ( 4 < m -> m e. GoldbachEven ) -> E. p e. Prime E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) ) ) )
34 6 33 syl 
 |-  ( n e. ZZ -> ( 6 <_ n -> ( A. m e. Even ( 4 < m -> m e. GoldbachEven ) -> E. p e. Prime E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) ) ) )
35 34 imp 
 |-  ( ( n e. ZZ /\ 6 <_ n ) -> ( A. m e. Even ( 4 < m -> m e. GoldbachEven ) -> E. p e. Prime E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) ) )
36 35 3adant1 
 |-  ( ( 6 e. ZZ /\ n e. ZZ /\ 6 <_ n ) -> ( A. m e. Even ( 4 < m -> m e. GoldbachEven ) -> E. p e. Prime E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) ) )
37 5 36 sylbi 
 |-  ( n e. ( ZZ>= ` 6 ) -> ( A. m e. Even ( 4 < m -> m e. GoldbachEven ) -> E. p e. Prime E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) ) )
38 37 impcom 
 |-  ( ( A. m e. Even ( 4 < m -> m e. GoldbachEven ) /\ n e. ( ZZ>= ` 6 ) ) -> E. p e. Prime E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) )
39 38 ralrimiva 
 |-  ( A. m e. Even ( 4 < m -> m e. GoldbachEven ) -> A. n e. ( ZZ>= ` 6 ) E. p e. Prime E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) )
40 4 39 sylbi 
 |-  ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> A. n e. ( ZZ>= ` 6 ) E. p e. Prime E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) )