Metamath Proof Explorer

Theorem sbgoldbst

Description: If the strong binary Goldbach conjecture is valid, then the (strong) ternary Goldbach conjecture holds, too. (Contributed by AV, 26-Jul-2020)

Ref Expression
Assertion sbgoldbst 
|- ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> A. m e. Odd ( 7 < m -> m e. GoldbachOdd ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( m e. Odd /\ 7 < m ) -> m e. Odd )
2 3odd 
 |-  3 e. Odd
3 1 2 jctir 
 |-  ( ( m e. Odd /\ 7 < m ) -> ( m e. Odd /\ 3 e. Odd ) )
4 omoeALTV 
 |-  ( ( m e. Odd /\ 3 e. Odd ) -> ( m - 3 ) e. Even )
5 breq2 
 |-  ( n = ( m - 3 ) -> ( 4 < n <-> 4 < ( m - 3 ) ) )
6 eleq1 
 |-  ( n = ( m - 3 ) -> ( n e. GoldbachEven <-> ( m - 3 ) e. GoldbachEven ) )
7 5 6 imbi12d 
 |-  ( n = ( m - 3 ) -> ( ( 4 < n -> n e. GoldbachEven ) <-> ( 4 < ( m - 3 ) -> ( m - 3 ) e. GoldbachEven ) ) )
8 7 rspcv 
 |-  ( ( m - 3 ) e. Even -> ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> ( 4 < ( m - 3 ) -> ( m - 3 ) e. GoldbachEven ) ) )
9 3 4 8 3syl 
 |-  ( ( m e. Odd /\ 7 < m ) -> ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> ( 4 < ( m - 3 ) -> ( m - 3 ) e. GoldbachEven ) ) )
10 4p3e7 
 |-  ( 4 + 3 ) = 7
11 10 breq1i 
 |-  ( ( 4 + 3 ) < m <-> 7 < m )
12 4re 
 |-  4 e. RR
13 12 a1i 
 |-  ( m e. Odd -> 4 e. RR )
14 3re 
 |-  3 e. RR
15 14 a1i 
 |-  ( m e. Odd -> 3 e. RR )
16 oddz 
 |-  ( m e. Odd -> m e. ZZ )
17 16 zred 
 |-  ( m e. Odd -> m e. RR )
18 13 15 17 ltaddsubd 
 |-  ( m e. Odd -> ( ( 4 + 3 ) < m <-> 4 < ( m - 3 ) ) )
19 18 biimpd 
 |-  ( m e. Odd -> ( ( 4 + 3 ) < m -> 4 < ( m - 3 ) ) )
20 11 19 biimtrrid 
 |-  ( m e. Odd -> ( 7 < m -> 4 < ( m - 3 ) ) )
21 20 imp 
 |-  ( ( m e. Odd /\ 7 < m ) -> 4 < ( m - 3 ) )
22 pm2.27 
 |-  ( 4 < ( m - 3 ) -> ( ( 4 < ( m - 3 ) -> ( m - 3 ) e. GoldbachEven ) -> ( m - 3 ) e. GoldbachEven ) )
23 21 22 syl 
 |-  ( ( m e. Odd /\ 7 < m ) -> ( ( 4 < ( m - 3 ) -> ( m - 3 ) e. GoldbachEven ) -> ( m - 3 ) e. GoldbachEven ) )
24 isgbe 
 |-  ( ( m - 3 ) e. GoldbachEven <-> ( ( m - 3 ) e. Even /\ E. p e. Prime E. q e. Prime ( p e. Odd /\ q e. Odd /\ ( m - 3 ) = ( p + q ) ) ) )
25 3prm 
 |-  3 e. Prime
26 25 a1i 
 |-  ( ( ( ( ( m e. Odd /\ 7 < m ) /\ p e. Prime ) /\ q e. Prime ) /\ ( p e. Odd /\ q e. Odd /\ ( m - 3 ) = ( p + q ) ) ) -> 3 e. Prime )
27 eleq1 
 |-  ( r = 3 -> ( r e. Odd <-> 3 e. Odd ) )
28 27 3anbi3d 
 |-  ( r = 3 -> ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) <-> ( p e. Odd /\ q e. Odd /\ 3 e. Odd ) ) )
29 oveq2 
 |-  ( r = 3 -> ( ( p + q ) + r ) = ( ( p + q ) + 3 ) )
30 29 eqeq2d 
 |-  ( r = 3 -> ( m = ( ( p + q ) + r ) <-> m = ( ( p + q ) + 3 ) ) )
31 28 30 anbi12d 
 |-  ( r = 3 -> ( ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ m = ( ( p + q ) + r ) ) <-> ( ( p e. Odd /\ q e. Odd /\ 3 e. Odd ) /\ m = ( ( p + q ) + 3 ) ) ) )
32 31 adantl 
 |-  ( ( ( ( ( ( m e. Odd /\ 7 < m ) /\ p e. Prime ) /\ q e. Prime ) /\ ( p e. Odd /\ q e. Odd /\ ( m - 3 ) = ( p + q ) ) ) /\ r = 3 ) -> ( ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ m = ( ( p + q ) + r ) ) <-> ( ( p e. Odd /\ q e. Odd /\ 3 e. Odd ) /\ m = ( ( p + q ) + 3 ) ) ) )
33 simp1 
 |-  ( ( p e. Odd /\ q e. Odd /\ ( m - 3 ) = ( p + q ) ) -> p e. Odd )
34 simp2 
 |-  ( ( p e. Odd /\ q e. Odd /\ ( m - 3 ) = ( p + q ) ) -> q e. Odd )
35 2 a1i 
 |-  ( ( p e. Odd /\ q e. Odd /\ ( m - 3 ) = ( p + q ) ) -> 3 e. Odd )
36 33 34 35 3jca 
 |-  ( ( p e. Odd /\ q e. Odd /\ ( m - 3 ) = ( p + q ) ) -> ( p e. Odd /\ q e. Odd /\ 3 e. Odd ) )
37 36 adantl 
 |-  ( ( ( ( ( m e. Odd /\ 7 < m ) /\ p e. Prime ) /\ q e. Prime ) /\ ( p e. Odd /\ q e. Odd /\ ( m - 3 ) = ( p + q ) ) ) -> ( p e. Odd /\ q e. Odd /\ 3 e. Odd ) )
38 16 zcnd 
 |-  ( m e. Odd -> m e. CC )
39 38 ad3antrrr 
 |-  ( ( ( ( m e. Odd /\ 7 < m ) /\ p e. Prime ) /\ q e. Prime ) -> m e. CC )
40 3cn 
 |-  3 e. CC
41 40 a1i 
 |-  ( ( ( ( m e. Odd /\ 7 < m ) /\ p e. Prime ) /\ q e. Prime ) -> 3 e. CC )
42 prmz 
 |-  ( p e. Prime -> p e. ZZ )
43 prmz 
 |-  ( q e. Prime -> q e. ZZ )
44 zaddcl 
 |-  ( ( p e. ZZ /\ q e. ZZ ) -> ( p + q ) e. ZZ )
45 42 43 44 syl2an 
 |-  ( ( p e. Prime /\ q e. Prime ) -> ( p + q ) e. ZZ )
46 45 zcnd 
 |-  ( ( p e. Prime /\ q e. Prime ) -> ( p + q ) e. CC )
47 46 adantll 
 |-  ( ( ( ( m e. Odd /\ 7 < m ) /\ p e. Prime ) /\ q e. Prime ) -> ( p + q ) e. CC )
48 39 41 47 subadd2d 
 |-  ( ( ( ( m e. Odd /\ 7 < m ) /\ p e. Prime ) /\ q e. Prime ) -> ( ( m - 3 ) = ( p + q ) <-> ( ( p + q ) + 3 ) = m ) )
49 48 biimpa 
 |-  ( ( ( ( ( m e. Odd /\ 7 < m ) /\ p e. Prime ) /\ q e. Prime ) /\ ( m - 3 ) = ( p + q ) ) -> ( ( p + q ) + 3 ) = m )
50 49 eqcomd 
 |-  ( ( ( ( ( m e. Odd /\ 7 < m ) /\ p e. Prime ) /\ q e. Prime ) /\ ( m - 3 ) = ( p + q ) ) -> m = ( ( p + q ) + 3 ) )
51 50 3ad2antr3 
 |-  ( ( ( ( ( m e. Odd /\ 7 < m ) /\ p e. Prime ) /\ q e. Prime ) /\ ( p e. Odd /\ q e. Odd /\ ( m - 3 ) = ( p + q ) ) ) -> m = ( ( p + q ) + 3 ) )
52 37 51 jca 
 |-  ( ( ( ( ( m e. Odd /\ 7 < m ) /\ p e. Prime ) /\ q e. Prime ) /\ ( p e. Odd /\ q e. Odd /\ ( m - 3 ) = ( p + q ) ) ) -> ( ( p e. Odd /\ q e. Odd /\ 3 e. Odd ) /\ m = ( ( p + q ) + 3 ) ) )
53 26 32 52 rspcedvd 
 |-  ( ( ( ( ( m e. Odd /\ 7 < m ) /\ p e. Prime ) /\ q e. Prime ) /\ ( p e. Odd /\ q e. Odd /\ ( m - 3 ) = ( p + q ) ) ) -> E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ m = ( ( p + q ) + r ) ) )
54 53 ex 
 |-  ( ( ( ( m e. Odd /\ 7 < m ) /\ p e. Prime ) /\ q e. Prime ) -> ( ( p e. Odd /\ q e. Odd /\ ( m - 3 ) = ( p + q ) ) -> E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ m = ( ( p + q ) + r ) ) ) )
55 54 reximdva 
 |-  ( ( ( m e. Odd /\ 7 < m ) /\ p e. Prime ) -> ( E. q e. Prime ( p e. Odd /\ q e. Odd /\ ( m - 3 ) = ( p + q ) ) -> E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ m = ( ( p + q ) + r ) ) ) )
56 55 reximdva 
 |-  ( ( m e. Odd /\ 7 < m ) -> ( E. p e. Prime E. q e. Prime ( p e. Odd /\ q e. Odd /\ ( m - 3 ) = ( p + q ) ) -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ m = ( ( p + q ) + r ) ) ) )
57 56 1 jctild 
 |-  ( ( m e. Odd /\ 7 < m ) -> ( E. p e. Prime E. q e. Prime ( p e. Odd /\ q e. Odd /\ ( m - 3 ) = ( p + q ) ) -> ( m e. Odd /\ E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ m = ( ( p + q ) + r ) ) ) ) )
58 isgbo 
 |-  ( m e. GoldbachOdd <-> ( m e. Odd /\ E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ m = ( ( p + q ) + r ) ) ) )
59 57 58 imbitrrdi 
 |-  ( ( m e. Odd /\ 7 < m ) -> ( E. p e. Prime E. q e. Prime ( p e. Odd /\ q e. Odd /\ ( m - 3 ) = ( p + q ) ) -> m e. GoldbachOdd ) )
60 59 adantld 
 |-  ( ( m e. Odd /\ 7 < m ) -> ( ( ( m - 3 ) e. Even /\ E. p e. Prime E. q e. Prime ( p e. Odd /\ q e. Odd /\ ( m - 3 ) = ( p + q ) ) ) -> m e. GoldbachOdd ) )
61 24 60 biimtrid 
 |-  ( ( m e. Odd /\ 7 < m ) -> ( ( m - 3 ) e. GoldbachEven -> m e. GoldbachOdd ) )
62 9 23 61 3syld 
 |-  ( ( m e. Odd /\ 7 < m ) -> ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> m e. GoldbachOdd ) )
63 62 com12 
 |-  ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> ( ( m e. Odd /\ 7 < m ) -> m e. GoldbachOdd ) )
64 63 expd 
 |-  ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> ( m e. Odd -> ( 7 < m -> m e. GoldbachOdd ) ) )
65 64 ralrimiv 
 |-  ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> A. m e. Odd ( 7 < m -> m e. GoldbachOdd ) )