Metamath Proof Explorer

Theorem evengpop3

Description: If the (weak) ternary Goldbach conjecture is valid, then every even integer greater than 8 is the sum of an odd Goldbach number and 3. (Contributed by AV, 24-Jul-2020)

Ref Expression
Assertion evengpop3 
|- ( A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) -> ( ( N e. ( ZZ>= ` 9 ) /\ N e. Even ) -> E. o e. GoldbachOddW N = ( o + 3 ) ) )

Proof

Step Hyp Ref Expression
1 3odd 
 |-  3 e. Odd
2 1 a1i 
 |-  ( N e. ( ZZ>= ` 9 ) -> 3 e. Odd )
3 2 anim1i 
 |-  ( ( N e. ( ZZ>= ` 9 ) /\ N e. Even ) -> ( 3 e. Odd /\ N e. Even ) )
4 3 ancomd 
 |-  ( ( N e. ( ZZ>= ` 9 ) /\ N e. Even ) -> ( N e. Even /\ 3 e. Odd ) )
5 emoo 
 |-  ( ( N e. Even /\ 3 e. Odd ) -> ( N - 3 ) e. Odd )
6 4 5 syl 
 |-  ( ( N e. ( ZZ>= ` 9 ) /\ N e. Even ) -> ( N - 3 ) e. Odd )
7 breq2 
 |-  ( m = ( N - 3 ) -> ( 5 < m <-> 5 < ( N - 3 ) ) )
8 eleq1 
 |-  ( m = ( N - 3 ) -> ( m e. GoldbachOddW <-> ( N - 3 ) e. GoldbachOddW ) )
9 7 8 imbi12d 
 |-  ( m = ( N - 3 ) -> ( ( 5 < m -> m e. GoldbachOddW ) <-> ( 5 < ( N - 3 ) -> ( N - 3 ) e. GoldbachOddW ) ) )
10 9 adantl 
 |-  ( ( ( N e. ( ZZ>= ` 9 ) /\ N e. Even ) /\ m = ( N - 3 ) ) -> ( ( 5 < m -> m e. GoldbachOddW ) <-> ( 5 < ( N - 3 ) -> ( N - 3 ) e. GoldbachOddW ) ) )
11 6 10 rspcdv 
 |-  ( ( N e. ( ZZ>= ` 9 ) /\ N e. Even ) -> ( A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) -> ( 5 < ( N - 3 ) -> ( N - 3 ) e. GoldbachOddW ) ) )
12 eluz2 
 |-  ( N e. ( ZZ>= ` 9 ) <-> ( 9 e. ZZ /\ N e. ZZ /\ 9 <_ N ) )
13 5p3e8 
 |-  ( 5 + 3 ) = 8
14 8p1e9 
 |-  ( 8 + 1 ) = 9
15 9cn 
 |-  9 e. CC
16 ax-1cn 
 |-  1 e. CC
17 8cn 
 |-  8 e. CC
18 15 16 17 subadd2i 
 |-  ( ( 9 - 1 ) = 8 <-> ( 8 + 1 ) = 9 )
19 14 18 mpbir 
 |-  ( 9 - 1 ) = 8
20 13 19 eqtr4i 
 |-  ( 5 + 3 ) = ( 9 - 1 )
21 zlem1lt 
 |-  ( ( 9 e. ZZ /\ N e. ZZ ) -> ( 9 <_ N <-> ( 9 - 1 ) < N ) )
22 21 biimp3a 
 |-  ( ( 9 e. ZZ /\ N e. ZZ /\ 9 <_ N ) -> ( 9 - 1 ) < N )
23 20 22 eqbrtrid 
 |-  ( ( 9 e. ZZ /\ N e. ZZ /\ 9 <_ N ) -> ( 5 + 3 ) < N )
24 5re 
 |-  5 e. RR
25 24 a1i 
 |-  ( N e. ZZ -> 5 e. RR )
26 3re 
 |-  3 e. RR
27 26 a1i 
 |-  ( N e. ZZ -> 3 e. RR )
28 zre 
 |-  ( N e. ZZ -> N e. RR )
29 25 27 28 3jca 
 |-  ( N e. ZZ -> ( 5 e. RR /\ 3 e. RR /\ N e. RR ) )
30 29 3ad2ant2 
 |-  ( ( 9 e. ZZ /\ N e. ZZ /\ 9 <_ N ) -> ( 5 e. RR /\ 3 e. RR /\ N e. RR ) )
31 ltaddsub 
 |-  ( ( 5 e. RR /\ 3 e. RR /\ N e. RR ) -> ( ( 5 + 3 ) < N <-> 5 < ( N - 3 ) ) )
32 30 31 syl 
 |-  ( ( 9 e. ZZ /\ N e. ZZ /\ 9 <_ N ) -> ( ( 5 + 3 ) < N <-> 5 < ( N - 3 ) ) )
33 23 32 mpbid 
 |-  ( ( 9 e. ZZ /\ N e. ZZ /\ 9 <_ N ) -> 5 < ( N - 3 ) )
34 12 33 sylbi 
 |-  ( N e. ( ZZ>= ` 9 ) -> 5 < ( N - 3 ) )
35 34 adantr 
 |-  ( ( N e. ( ZZ>= ` 9 ) /\ N e. Even ) -> 5 < ( N - 3 ) )
36 simpr 
 |-  ( ( ( N e. ( ZZ>= ` 9 ) /\ N e. Even ) /\ ( N - 3 ) e. GoldbachOddW ) -> ( N - 3 ) e. GoldbachOddW )
37 oveq1 
 |-  ( o = ( N - 3 ) -> ( o + 3 ) = ( ( N - 3 ) + 3 ) )
38 37 eqeq2d 
 |-  ( o = ( N - 3 ) -> ( N = ( o + 3 ) <-> N = ( ( N - 3 ) + 3 ) ) )
39 38 adantl 
 |-  ( ( ( ( N e. ( ZZ>= ` 9 ) /\ N e. Even ) /\ ( N - 3 ) e. GoldbachOddW ) /\ o = ( N - 3 ) ) -> ( N = ( o + 3 ) <-> N = ( ( N - 3 ) + 3 ) ) )
40 eluzelcn 
 |-  ( N e. ( ZZ>= ` 9 ) -> N e. CC )
41 3cn 
 |-  3 e. CC
42 41 a1i 
 |-  ( N e. ( ZZ>= ` 9 ) -> 3 e. CC )
43 40 42 jca 
 |-  ( N e. ( ZZ>= ` 9 ) -> ( N e. CC /\ 3 e. CC ) )
44 43 adantr 
 |-  ( ( N e. ( ZZ>= ` 9 ) /\ N e. Even ) -> ( N e. CC /\ 3 e. CC ) )
45 44 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 9 ) /\ N e. Even ) /\ ( N - 3 ) e. GoldbachOddW ) -> ( N e. CC /\ 3 e. CC ) )
46 npcan 
 |-  ( ( N e. CC /\ 3 e. CC ) -> ( ( N - 3 ) + 3 ) = N )
47 46 eqcomd 
 |-  ( ( N e. CC /\ 3 e. CC ) -> N = ( ( N - 3 ) + 3 ) )
48 45 47 syl 
 |-  ( ( ( N e. ( ZZ>= ` 9 ) /\ N e. Even ) /\ ( N - 3 ) e. GoldbachOddW ) -> N = ( ( N - 3 ) + 3 ) )
49 36 39 48 rspcedvd 
 |-  ( ( ( N e. ( ZZ>= ` 9 ) /\ N e. Even ) /\ ( N - 3 ) e. GoldbachOddW ) -> E. o e. GoldbachOddW N = ( o + 3 ) )
50 49 ex 
 |-  ( ( N e. ( ZZ>= ` 9 ) /\ N e. Even ) -> ( ( N - 3 ) e. GoldbachOddW -> E. o e. GoldbachOddW N = ( o + 3 ) ) )
51 35 50 embantd 
 |-  ( ( N e. ( ZZ>= ` 9 ) /\ N e. Even ) -> ( ( 5 < ( N - 3 ) -> ( N - 3 ) e. GoldbachOddW ) -> E. o e. GoldbachOddW N = ( o + 3 ) ) )
52 11 51 syldc 
 |-  ( A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) -> ( ( N e. ( ZZ>= ` 9 ) /\ N e. Even ) -> E. o e. GoldbachOddW N = ( o + 3 ) ) )