Metamath Proof Explorer

Theorem sbgoldbwt

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

Ref Expression
Assertion sbgoldbwt 
|- ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) )

Proof

Step Hyp Ref Expression
1 oddz 
 |-  ( m e. Odd -> m e. ZZ )
2 5nn 
 |-  5 e. NN
3 2 nnzi 
 |-  5 e. ZZ
4 zltp1le 
 |-  ( ( 5 e. ZZ /\ m e. ZZ ) -> ( 5 < m <-> ( 5 + 1 ) <_ m ) )
5 3 4 mpan 
 |-  ( m e. ZZ -> ( 5 < m <-> ( 5 + 1 ) <_ m ) )
6 5p1e6 
 |-  ( 5 + 1 ) = 6
7 6 breq1i 
 |-  ( ( 5 + 1 ) <_ m <-> 6 <_ m )
8 6re 
 |-  6 e. RR
9 8 a1i 
 |-  ( m e. ZZ -> 6 e. RR )
10 zre 
 |-  ( m e. ZZ -> m e. RR )
11 9 10 leloed 
 |-  ( m e. ZZ -> ( 6 <_ m <-> ( 6 < m \/ 6 = m ) ) )
12 7 11 bitrid 
 |-  ( m e. ZZ -> ( ( 5 + 1 ) <_ m <-> ( 6 < m \/ 6 = m ) ) )
13 6nn 
 |-  6 e. NN
14 13 nnzi 
 |-  6 e. ZZ
15 zltp1le 
 |-  ( ( 6 e. ZZ /\ m e. ZZ ) -> ( 6 < m <-> ( 6 + 1 ) <_ m ) )
16 14 15 mpan 
 |-  ( m e. ZZ -> ( 6 < m <-> ( 6 + 1 ) <_ m ) )
17 6p1e7 
 |-  ( 6 + 1 ) = 7
18 17 breq1i 
 |-  ( ( 6 + 1 ) <_ m <-> 7 <_ m )
19 7re 
 |-  7 e. RR
20 19 a1i 
 |-  ( m e. ZZ -> 7 e. RR )
21 20 10 leloed 
 |-  ( m e. ZZ -> ( 7 <_ m <-> ( 7 < m \/ 7 = m ) ) )
22 18 21 bitrid 
 |-  ( m e. ZZ -> ( ( 6 + 1 ) <_ m <-> ( 7 < m \/ 7 = m ) ) )
23 simpr 
 |-  ( ( ( 7 < m /\ m e. ZZ ) /\ m e. Odd ) -> m e. Odd )
24 3odd 
 |-  3 e. Odd
25 23 24 jctir 
 |-  ( ( ( 7 < m /\ m e. ZZ ) /\ m e. Odd ) -> ( m e. Odd /\ 3 e. Odd ) )
26 omoeALTV 
 |-  ( ( m e. Odd /\ 3 e. Odd ) -> ( m - 3 ) e. Even )
27 breq2 
 |-  ( n = ( m - 3 ) -> ( 4 < n <-> 4 < ( m - 3 ) ) )
28 eleq1 
 |-  ( n = ( m - 3 ) -> ( n e. GoldbachEven <-> ( m - 3 ) e. GoldbachEven ) )
29 27 28 imbi12d 
 |-  ( n = ( m - 3 ) -> ( ( 4 < n -> n e. GoldbachEven ) <-> ( 4 < ( m - 3 ) -> ( m - 3 ) e. GoldbachEven ) ) )
30 29 rspcv 
 |-  ( ( m - 3 ) e. Even -> ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> ( 4 < ( m - 3 ) -> ( m - 3 ) e. GoldbachEven ) ) )
31 25 26 30 3syl 
 |-  ( ( ( 7 < m /\ m e. ZZ ) /\ m e. Odd ) -> ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> ( 4 < ( m - 3 ) -> ( m - 3 ) e. GoldbachEven ) ) )
32 4p3e7 
 |-  ( 4 + 3 ) = 7
33 32 eqcomi 
 |-  7 = ( 4 + 3 )
34 33 breq1i 
 |-  ( 7 < m <-> ( 4 + 3 ) < m )
35 4re 
 |-  4 e. RR
36 35 a1i 
 |-  ( m e. ZZ -> 4 e. RR )
37 3re 
 |-  3 e. RR
38 37 a1i 
 |-  ( m e. ZZ -> 3 e. RR )
39 ltaddsub 
 |-  ( ( 4 e. RR /\ 3 e. RR /\ m e. RR ) -> ( ( 4 + 3 ) < m <-> 4 < ( m - 3 ) ) )
40 39 biimpd 
 |-  ( ( 4 e. RR /\ 3 e. RR /\ m e. RR ) -> ( ( 4 + 3 ) < m -> 4 < ( m - 3 ) ) )
41 36 38 10 40 syl3anc 
 |-  ( m e. ZZ -> ( ( 4 + 3 ) < m -> 4 < ( m - 3 ) ) )
42 34 41 biimtrid 
 |-  ( m e. ZZ -> ( 7 < m -> 4 < ( m - 3 ) ) )
43 42 impcom 
 |-  ( ( 7 < m /\ m e. ZZ ) -> 4 < ( m - 3 ) )
44 43 adantr 
 |-  ( ( ( 7 < m /\ m e. ZZ ) /\ m e. Odd ) -> 4 < ( m - 3 ) )
45 pm2.27 
 |-  ( 4 < ( m - 3 ) -> ( ( 4 < ( m - 3 ) -> ( m - 3 ) e. GoldbachEven ) -> ( m - 3 ) e. GoldbachEven ) )
46 44 45 syl 
 |-  ( ( ( 7 < m /\ m e. ZZ ) /\ m e. Odd ) -> ( ( 4 < ( m - 3 ) -> ( m - 3 ) e. GoldbachEven ) -> ( m - 3 ) e. GoldbachEven ) )
47 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 ) ) ) )
48 3prm 
 |-  3 e. Prime
49 48 a1i 
 |-  ( m e. ZZ -> 3 e. Prime )
50 zcn 
 |-  ( m e. ZZ -> m e. CC )
51 3cn 
 |-  3 e. CC
52 50 51 jctir 
 |-  ( m e. ZZ -> ( m e. CC /\ 3 e. CC ) )
53 npcan 
 |-  ( ( m e. CC /\ 3 e. CC ) -> ( ( m - 3 ) + 3 ) = m )
54 53 eqcomd 
 |-  ( ( m e. CC /\ 3 e. CC ) -> m = ( ( m - 3 ) + 3 ) )
55 52 54 syl 
 |-  ( m e. ZZ -> m = ( ( m - 3 ) + 3 ) )
56 oveq2 
 |-  ( 3 = r -> ( ( m - 3 ) + 3 ) = ( ( m - 3 ) + r ) )
57 56 eqcoms 
 |-  ( r = 3 -> ( ( m - 3 ) + 3 ) = ( ( m - 3 ) + r ) )
58 55 57 sylan9eq 
 |-  ( ( m e. ZZ /\ r = 3 ) -> m = ( ( m - 3 ) + r ) )
59 49 58 rspcedeq2vd 
 |-  ( m e. ZZ -> E. r e. Prime m = ( ( m - 3 ) + r ) )
60 oveq1 
 |-  ( ( m - 3 ) = ( p + q ) -> ( ( m - 3 ) + r ) = ( ( p + q ) + r ) )
61 60 eqeq2d 
 |-  ( ( m - 3 ) = ( p + q ) -> ( m = ( ( m - 3 ) + r ) <-> m = ( ( p + q ) + r ) ) )
62 61 rexbidv 
 |-  ( ( m - 3 ) = ( p + q ) -> ( E. r e. Prime m = ( ( m - 3 ) + r ) <-> E. r e. Prime m = ( ( p + q ) + r ) ) )
63 59 62 imbitrid 
 |-  ( ( m - 3 ) = ( p + q ) -> ( m e. ZZ -> E. r e. Prime m = ( ( p + q ) + r ) ) )
64 63 3ad2ant3 
 |-  ( ( p e. Odd /\ q e. Odd /\ ( m - 3 ) = ( p + q ) ) -> ( m e. ZZ -> E. r e. Prime m = ( ( p + q ) + r ) ) )
65 64 com12 
 |-  ( m e. ZZ -> ( ( p e. Odd /\ q e. Odd /\ ( m - 3 ) = ( p + q ) ) -> E. r e. Prime m = ( ( p + q ) + r ) ) )
66 65 ad4antlr 
 |-  ( ( ( ( ( 7 < m /\ m e. ZZ ) /\ m e. Odd ) /\ p e. Prime ) /\ q e. Prime ) -> ( ( p e. Odd /\ q e. Odd /\ ( m - 3 ) = ( p + q ) ) -> E. r e. Prime m = ( ( p + q ) + r ) ) )
67 66 reximdva 
 |-  ( ( ( ( 7 < m /\ m e. ZZ ) /\ m e. Odd ) /\ 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 m = ( ( p + q ) + r ) ) )
68 67 reximdva 
 |-  ( ( ( 7 < m /\ m e. ZZ ) /\ m e. Odd ) -> ( 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 m = ( ( p + q ) + r ) ) )
69 68 23 jctild 
 |-  ( ( ( 7 < m /\ m e. ZZ ) /\ m e. Odd ) -> ( 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 m = ( ( p + q ) + r ) ) ) )
70 isgbow 
 |-  ( m e. GoldbachOddW <-> ( m e. Odd /\ E. p e. Prime E. q e. Prime E. r e. Prime m = ( ( p + q ) + r ) ) )
71 69 70 imbitrrdi 
 |-  ( ( ( 7 < m /\ m e. ZZ ) /\ m e. Odd ) -> ( E. p e. Prime E. q e. Prime ( p e. Odd /\ q e. Odd /\ ( m - 3 ) = ( p + q ) ) -> m e. GoldbachOddW ) )
72 71 adantld 
 |-  ( ( ( 7 < m /\ m e. ZZ ) /\ m e. Odd ) -> ( ( ( m - 3 ) e. Even /\ E. p e. Prime E. q e. Prime ( p e. Odd /\ q e. Odd /\ ( m - 3 ) = ( p + q ) ) ) -> m e. GoldbachOddW ) )
73 47 72 biimtrid 
 |-  ( ( ( 7 < m /\ m e. ZZ ) /\ m e. Odd ) -> ( ( m - 3 ) e. GoldbachEven -> m e. GoldbachOddW ) )
74 31 46 73 3syld 
 |-  ( ( ( 7 < m /\ m e. ZZ ) /\ m e. Odd ) -> ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> m e. GoldbachOddW ) )
75 74 ex 
 |-  ( ( 7 < m /\ m e. ZZ ) -> ( m e. Odd -> ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> m e. GoldbachOddW ) ) )
76 75 com23 
 |-  ( ( 7 < m /\ m e. ZZ ) -> ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> ( m e. Odd -> m e. GoldbachOddW ) ) )
77 76 ex 
 |-  ( 7 < m -> ( m e. ZZ -> ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> ( m e. Odd -> m e. GoldbachOddW ) ) ) )
78 7gbow 
 |-  7 e. GoldbachOddW
79 eleq1 
 |-  ( 7 = m -> ( 7 e. GoldbachOddW <-> m e. GoldbachOddW ) )
80 78 79 mpbii 
 |-  ( 7 = m -> m e. GoldbachOddW )
81 80 a1d 
 |-  ( 7 = m -> ( m e. Odd -> m e. GoldbachOddW ) )
82 81 a1d 
 |-  ( 7 = m -> ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> ( m e. Odd -> m e. GoldbachOddW ) ) )
83 82 a1d 
 |-  ( 7 = m -> ( m e. ZZ -> ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> ( m e. Odd -> m e. GoldbachOddW ) ) ) )
84 77 83 jaoi 
 |-  ( ( 7 < m \/ 7 = m ) -> ( m e. ZZ -> ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> ( m e. Odd -> m e. GoldbachOddW ) ) ) )
85 84 com12 
 |-  ( m e. ZZ -> ( ( 7 < m \/ 7 = m ) -> ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> ( m e. Odd -> m e. GoldbachOddW ) ) ) )
86 22 85 sylbid 
 |-  ( m e. ZZ -> ( ( 6 + 1 ) <_ m -> ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> ( m e. Odd -> m e. GoldbachOddW ) ) ) )
87 16 86 sylbid 
 |-  ( m e. ZZ -> ( 6 < m -> ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> ( m e. Odd -> m e. GoldbachOddW ) ) ) )
88 87 com12 
 |-  ( 6 < m -> ( m e. ZZ -> ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> ( m e. Odd -> m e. GoldbachOddW ) ) ) )
89 eleq1 
 |-  ( 6 = m -> ( 6 e. Odd <-> m e. Odd ) )
90 6even 
 |-  6 e. Even
91 evennodd 
 |-  ( 6 e. Even -> -. 6 e. Odd )
92 91 pm2.21d 
 |-  ( 6 e. Even -> ( 6 e. Odd -> m e. GoldbachOddW ) )
93 90 92 ax-mp 
 |-  ( 6 e. Odd -> m e. GoldbachOddW )
94 89 93 biimtrrdi 
 |-  ( 6 = m -> ( m e. Odd -> m e. GoldbachOddW ) )
95 94 a1d 
 |-  ( 6 = m -> ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> ( m e. Odd -> m e. GoldbachOddW ) ) )
96 95 a1d 
 |-  ( 6 = m -> ( m e. ZZ -> ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> ( m e. Odd -> m e. GoldbachOddW ) ) ) )
97 88 96 jaoi 
 |-  ( ( 6 < m \/ 6 = m ) -> ( m e. ZZ -> ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> ( m e. Odd -> m e. GoldbachOddW ) ) ) )
98 97 com12 
 |-  ( m e. ZZ -> ( ( 6 < m \/ 6 = m ) -> ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> ( m e. Odd -> m e. GoldbachOddW ) ) ) )
99 12 98 sylbid 
 |-  ( m e. ZZ -> ( ( 5 + 1 ) <_ m -> ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> ( m e. Odd -> m e. GoldbachOddW ) ) ) )
100 5 99 sylbid 
 |-  ( m e. ZZ -> ( 5 < m -> ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> ( m e. Odd -> m e. GoldbachOddW ) ) ) )
101 100 com24 
 |-  ( m e. ZZ -> ( m e. Odd -> ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> ( 5 < m -> m e. GoldbachOddW ) ) ) )
102 1 101 mpcom 
 |-  ( m e. Odd -> ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> ( 5 < m -> m e. GoldbachOddW ) ) )
103 102 impcom 
 |-  ( ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) /\ m e. Odd ) -> ( 5 < m -> m e. GoldbachOddW ) )
104 103 ralrimiva 
 |-  ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) )