Metamath Proof Explorer

Theorem evengpoap3

Description: If the (strong) ternary Goldbach conjecture is valid, then every even integer greater than 10 is the sum of an odd Goldbach number and 3. (Contributed by AV, 27-Jul-2020) (Proof shortened by AV, 15-Sep-2021)

Ref Expression
Assertion evengpoap3 
|- ( A. m e. Odd ( 7 < m -> m e. GoldbachOdd ) -> ( ( N e. ( ZZ>= ` ; 1 2 ) /\ N e. Even ) -> E. o e. GoldbachOdd N = ( o + 3 ) ) )

Proof

Step Hyp Ref Expression
1 3odd 
 |-  3 e. Odd
2 1 a1i 
 |-  ( N e. ( ZZ>= ` ; 1 2 ) -> 3 e. Odd )
3 2 anim1i 
 |-  ( ( N e. ( ZZ>= ` ; 1 2 ) /\ N e. Even ) -> ( 3 e. Odd /\ N e. Even ) )
4 3 ancomd 
 |-  ( ( N e. ( ZZ>= ` ; 1 2 ) /\ 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>= ` ; 1 2 ) /\ N e. Even ) -> ( N - 3 ) e. Odd )
7 breq2 
 |-  ( m = ( N - 3 ) -> ( 7 < m <-> 7 < ( N - 3 ) ) )
8 eleq1 
 |-  ( m = ( N - 3 ) -> ( m e. GoldbachOdd <-> ( N - 3 ) e. GoldbachOdd ) )
9 7 8 imbi12d 
 |-  ( m = ( N - 3 ) -> ( ( 7 < m -> m e. GoldbachOdd ) <-> ( 7 < ( N - 3 ) -> ( N - 3 ) e. GoldbachOdd ) ) )
10 9 adantl 
 |-  ( ( ( N e. ( ZZ>= ` ; 1 2 ) /\ N e. Even ) /\ m = ( N - 3 ) ) -> ( ( 7 < m -> m e. GoldbachOdd ) <-> ( 7 < ( N - 3 ) -> ( N - 3 ) e. GoldbachOdd ) ) )
11 6 10 rspcdv 
 |-  ( ( N e. ( ZZ>= ` ; 1 2 ) /\ N e. Even ) -> ( A. m e. Odd ( 7 < m -> m e. GoldbachOdd ) -> ( 7 < ( N - 3 ) -> ( N - 3 ) e. GoldbachOdd ) ) )
12 eluz2 
 |-  ( N e. ( ZZ>= ` ; 1 2 ) <-> ( ; 1 2 e. ZZ /\ N e. ZZ /\ ; 1 2 <_ N ) )
13 7p3e10 
 |-  ( 7 + 3 ) = ; 1 0
14 1nn0 
 |-  1 e. NN0
15 0nn0 
 |-  0 e. NN0
16 2nn 
 |-  2 e. NN
17 2pos 
 |-  0 < 2
18 14 15 16 17 declt 
 |-  ; 1 0 < ; 1 2
19 13 18 eqbrtri 
 |-  ( 7 + 3 ) < ; 1 2
20 7re 
 |-  7 e. RR
21 3re 
 |-  3 e. RR
22 20 21 readdcli 
 |-  ( 7 + 3 ) e. RR
23 2nn0 
 |-  2 e. NN0
24 14 23 deccl 
 |-  ; 1 2 e. NN0
25 24 nn0rei 
 |-  ; 1 2 e. RR
26 zre 
 |-  ( N e. ZZ -> N e. RR )
27 ltletr 
 |-  ( ( ( 7 + 3 ) e. RR /\ ; 1 2 e. RR /\ N e. RR ) -> ( ( ( 7 + 3 ) < ; 1 2 /\ ; 1 2 <_ N ) -> ( 7 + 3 ) < N ) )
28 22 25 26 27 mp3an12i 
 |-  ( N e. ZZ -> ( ( ( 7 + 3 ) < ; 1 2 /\ ; 1 2 <_ N ) -> ( 7 + 3 ) < N ) )
29 19 28 mpani 
 |-  ( N e. ZZ -> ( ; 1 2 <_ N -> ( 7 + 3 ) < N ) )
30 29 imp 
 |-  ( ( N e. ZZ /\ ; 1 2 <_ N ) -> ( 7 + 3 ) < N )
31 30 3adant1 
 |-  ( ( ; 1 2 e. ZZ /\ N e. ZZ /\ ; 1 2 <_ N ) -> ( 7 + 3 ) < N )
32 20 a1i 
 |-  ( ( ; 1 2 e. ZZ /\ N e. ZZ /\ ; 1 2 <_ N ) -> 7 e. RR )
33 21 a1i 
 |-  ( ( ; 1 2 e. ZZ /\ N e. ZZ /\ ; 1 2 <_ N ) -> 3 e. RR )
34 26 3ad2ant2 
 |-  ( ( ; 1 2 e. ZZ /\ N e. ZZ /\ ; 1 2 <_ N ) -> N e. RR )
35 32 33 34 ltaddsubd 
 |-  ( ( ; 1 2 e. ZZ /\ N e. ZZ /\ ; 1 2 <_ N ) -> ( ( 7 + 3 ) < N <-> 7 < ( N - 3 ) ) )
36 31 35 mpbid 
 |-  ( ( ; 1 2 e. ZZ /\ N e. ZZ /\ ; 1 2 <_ N ) -> 7 < ( N - 3 ) )
37 12 36 sylbi 
 |-  ( N e. ( ZZ>= ` ; 1 2 ) -> 7 < ( N - 3 ) )
38 37 adantr 
 |-  ( ( N e. ( ZZ>= ` ; 1 2 ) /\ N e. Even ) -> 7 < ( N - 3 ) )
39 simpr 
 |-  ( ( ( N e. ( ZZ>= ` ; 1 2 ) /\ N e. Even ) /\ ( N - 3 ) e. GoldbachOdd ) -> ( N - 3 ) e. GoldbachOdd )
40 oveq1 
 |-  ( o = ( N - 3 ) -> ( o + 3 ) = ( ( N - 3 ) + 3 ) )
41 40 eqeq2d 
 |-  ( o = ( N - 3 ) -> ( N = ( o + 3 ) <-> N = ( ( N - 3 ) + 3 ) ) )
42 41 adantl 
 |-  ( ( ( ( N e. ( ZZ>= ` ; 1 2 ) /\ N e. Even ) /\ ( N - 3 ) e. GoldbachOdd ) /\ o = ( N - 3 ) ) -> ( N = ( o + 3 ) <-> N = ( ( N - 3 ) + 3 ) ) )
43 eluzelcn 
 |-  ( N e. ( ZZ>= ` ; 1 2 ) -> N e. CC )
44 3cn 
 |-  3 e. CC
45 43 44 jctir 
 |-  ( N e. ( ZZ>= ` ; 1 2 ) -> ( N e. CC /\ 3 e. CC ) )
46 45 adantr 
 |-  ( ( N e. ( ZZ>= ` ; 1 2 ) /\ N e. Even ) -> ( N e. CC /\ 3 e. CC ) )
47 46 adantr 
 |-  ( ( ( N e. ( ZZ>= ` ; 1 2 ) /\ N e. Even ) /\ ( N - 3 ) e. GoldbachOdd ) -> ( N e. CC /\ 3 e. CC ) )
48 npcan 
 |-  ( ( N e. CC /\ 3 e. CC ) -> ( ( N - 3 ) + 3 ) = N )
49 48 eqcomd 
 |-  ( ( N e. CC /\ 3 e. CC ) -> N = ( ( N - 3 ) + 3 ) )
50 47 49 syl 
 |-  ( ( ( N e. ( ZZ>= ` ; 1 2 ) /\ N e. Even ) /\ ( N - 3 ) e. GoldbachOdd ) -> N = ( ( N - 3 ) + 3 ) )
51 39 42 50 rspcedvd 
 |-  ( ( ( N e. ( ZZ>= ` ; 1 2 ) /\ N e. Even ) /\ ( N - 3 ) e. GoldbachOdd ) -> E. o e. GoldbachOdd N = ( o + 3 ) )
52 51 ex 
 |-  ( ( N e. ( ZZ>= ` ; 1 2 ) /\ N e. Even ) -> ( ( N - 3 ) e. GoldbachOdd -> E. o e. GoldbachOdd N = ( o + 3 ) ) )
53 38 52 embantd 
 |-  ( ( N e. ( ZZ>= ` ; 1 2 ) /\ N e. Even ) -> ( ( 7 < ( N - 3 ) -> ( N - 3 ) e. GoldbachOdd ) -> E. o e. GoldbachOdd N = ( o + 3 ) ) )
54 11 53 syldc 
 |-  ( A. m e. Odd ( 7 < m -> m e. GoldbachOdd ) -> ( ( N e. ( ZZ>= ` ; 1 2 ) /\ N e. Even ) -> E. o e. GoldbachOdd N = ( o + 3 ) ) )