Metamath Proof Explorer

Theorem sgoldbeven3prm

Description: If the binary Goldbach conjecture is valid, then an even integer greater than 5 can be expressed as the sum of three primes: Since ( N - 2 ) is even iff N is even, there would be primes p and q with ( N - 2 ) = ( p + q ) , and therefore N = ( ( p + q ) + 2 ) . (Contributed by AV, 24-Dec-2021)

Ref Expression
Assertion sgoldbeven3prm 
|- ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> ( ( N e. Even /\ 6 <_ N ) -> E. p e. Prime E. q e. Prime E. r e. Prime N = ( ( p + q ) + r ) ) )

Proof

Step Hyp Ref Expression
1 sbgoldbb 
 |-  ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> A. n e. Even ( 2 < n -> E. p e. Prime E. q e. Prime n = ( p + q ) ) )
2 2p2e4 
 |-  ( 2 + 2 ) = 4
3 evenz 
 |-  ( N e. Even -> N e. ZZ )
4 3 zred 
 |-  ( N e. Even -> N e. RR )
5 4lt6 
 |-  4 < 6
6 4re 
 |-  4 e. RR
7 6re 
 |-  6 e. RR
8 ltletr 
 |-  ( ( 4 e. RR /\ 6 e. RR /\ N e. RR ) -> ( ( 4 < 6 /\ 6 <_ N ) -> 4 < N ) )
9 6 7 8 mp3an12 
 |-  ( N e. RR -> ( ( 4 < 6 /\ 6 <_ N ) -> 4 < N ) )
10 5 9 mpani 
 |-  ( N e. RR -> ( 6 <_ N -> 4 < N ) )
11 4 10 syl 
 |-  ( N e. Even -> ( 6 <_ N -> 4 < N ) )
12 11 imp 
 |-  ( ( N e. Even /\ 6 <_ N ) -> 4 < N )
13 2 12 eqbrtrid 
 |-  ( ( N e. Even /\ 6 <_ N ) -> ( 2 + 2 ) < N )
14 2re 
 |-  2 e. RR
15 14 a1i 
 |-  ( ( N e. Even /\ 6 <_ N ) -> 2 e. RR )
16 4 adantr 
 |-  ( ( N e. Even /\ 6 <_ N ) -> N e. RR )
17 15 15 16 ltaddsub2d 
 |-  ( ( N e. Even /\ 6 <_ N ) -> ( ( 2 + 2 ) < N <-> 2 < ( N - 2 ) ) )
18 13 17 mpbid 
 |-  ( ( N e. Even /\ 6 <_ N ) -> 2 < ( N - 2 ) )
19 2evenALTV 
 |-  2 e. Even
20 emee 
 |-  ( ( N e. Even /\ 2 e. Even ) -> ( N - 2 ) e. Even )
21 19 20 mpan2 
 |-  ( N e. Even -> ( N - 2 ) e. Even )
22 breq2 
 |-  ( n = ( N - 2 ) -> ( 2 < n <-> 2 < ( N - 2 ) ) )
23 eqeq1 
 |-  ( n = ( N - 2 ) -> ( n = ( p + q ) <-> ( N - 2 ) = ( p + q ) ) )
24 23 2rexbidv 
 |-  ( n = ( N - 2 ) -> ( E. p e. Prime E. q e. Prime n = ( p + q ) <-> E. p e. Prime E. q e. Prime ( N - 2 ) = ( p + q ) ) )
25 22 24 imbi12d 
 |-  ( n = ( N - 2 ) -> ( ( 2 < n -> E. p e. Prime E. q e. Prime n = ( p + q ) ) <-> ( 2 < ( N - 2 ) -> E. p e. Prime E. q e. Prime ( N - 2 ) = ( p + q ) ) ) )
26 25 rspcv 
 |-  ( ( N - 2 ) e. Even -> ( A. n e. Even ( 2 < n -> E. p e. Prime E. q e. Prime n = ( p + q ) ) -> ( 2 < ( N - 2 ) -> E. p e. Prime E. q e. Prime ( N - 2 ) = ( p + q ) ) ) )
27 2prm 
 |-  2 e. Prime
28 27 a1i 
 |-  ( ( N e. Even /\ ( N - 2 ) = ( p + q ) ) -> 2 e. Prime )
29 oveq2 
 |-  ( r = 2 -> ( ( p + q ) + r ) = ( ( p + q ) + 2 ) )
30 29 eqeq2d 
 |-  ( r = 2 -> ( N = ( ( p + q ) + r ) <-> N = ( ( p + q ) + 2 ) ) )
31 30 adantl 
 |-  ( ( ( N e. Even /\ ( N - 2 ) = ( p + q ) ) /\ r = 2 ) -> ( N = ( ( p + q ) + r ) <-> N = ( ( p + q ) + 2 ) ) )
32 3 zcnd 
 |-  ( N e. Even -> N e. CC )
33 2cnd 
 |-  ( N e. Even -> 2 e. CC )
34 npcan 
 |-  ( ( N e. CC /\ 2 e. CC ) -> ( ( N - 2 ) + 2 ) = N )
35 34 eqcomd 
 |-  ( ( N e. CC /\ 2 e. CC ) -> N = ( ( N - 2 ) + 2 ) )
36 32 33 35 syl2anc 
 |-  ( N e. Even -> N = ( ( N - 2 ) + 2 ) )
37 36 adantr 
 |-  ( ( N e. Even /\ ( N - 2 ) = ( p + q ) ) -> N = ( ( N - 2 ) + 2 ) )
38 simpr 
 |-  ( ( N e. Even /\ ( N - 2 ) = ( p + q ) ) -> ( N - 2 ) = ( p + q ) )
39 38 oveq1d 
 |-  ( ( N e. Even /\ ( N - 2 ) = ( p + q ) ) -> ( ( N - 2 ) + 2 ) = ( ( p + q ) + 2 ) )
40 37 39 eqtrd 
 |-  ( ( N e. Even /\ ( N - 2 ) = ( p + q ) ) -> N = ( ( p + q ) + 2 ) )
41 28 31 40 rspcedvd 
 |-  ( ( N e. Even /\ ( N - 2 ) = ( p + q ) ) -> E. r e. Prime N = ( ( p + q ) + r ) )
42 41 ex 
 |-  ( N e. Even -> ( ( N - 2 ) = ( p + q ) -> E. r e. Prime N = ( ( p + q ) + r ) ) )
43 42 reximdv 
 |-  ( N e. Even -> ( E. q e. Prime ( N - 2 ) = ( p + q ) -> E. q e. Prime E. r e. Prime N = ( ( p + q ) + r ) ) )
44 43 reximdv 
 |-  ( N e. Even -> ( E. p e. Prime E. q e. Prime ( N - 2 ) = ( p + q ) -> E. p e. Prime E. q e. Prime E. r e. Prime N = ( ( p + q ) + r ) ) )
45 44 imim2d 
 |-  ( N e. Even -> ( ( 2 < ( N - 2 ) -> E. p e. Prime E. q e. Prime ( N - 2 ) = ( p + q ) ) -> ( 2 < ( N - 2 ) -> E. p e. Prime E. q e. Prime E. r e. Prime N = ( ( p + q ) + r ) ) ) )
46 26 45 syl9r 
 |-  ( N e. Even -> ( ( N - 2 ) e. Even -> ( A. n e. Even ( 2 < n -> E. p e. Prime E. q e. Prime n = ( p + q ) ) -> ( 2 < ( N - 2 ) -> E. p e. Prime E. q e. Prime E. r e. Prime N = ( ( p + q ) + r ) ) ) ) )
47 21 46 mpd 
 |-  ( N e. Even -> ( A. n e. Even ( 2 < n -> E. p e. Prime E. q e. Prime n = ( p + q ) ) -> ( 2 < ( N - 2 ) -> E. p e. Prime E. q e. Prime E. r e. Prime N = ( ( p + q ) + r ) ) ) )
48 47 adantr 
 |-  ( ( N e. Even /\ 6 <_ N ) -> ( A. n e. Even ( 2 < n -> E. p e. Prime E. q e. Prime n = ( p + q ) ) -> ( 2 < ( N - 2 ) -> E. p e. Prime E. q e. Prime E. r e. Prime N = ( ( p + q ) + r ) ) ) )
49 18 48 mpid 
 |-  ( ( N e. Even /\ 6 <_ N ) -> ( A. n e. Even ( 2 < n -> E. p e. Prime E. q e. Prime n = ( p + q ) ) -> E. p e. Prime E. q e. Prime E. r e. Prime N = ( ( p + q ) + r ) ) )
50 1 49 syl5com 
 |-  ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> ( ( N e. Even /\ 6 <_ N ) -> E. p e. Prime E. q e. Prime E. r e. Prime N = ( ( p + q ) + r ) ) )