Metamath Proof Explorer

Theorem mogoldbb

Description: If the modern version of the original formulation of the Goldbach conjecture is valid, the (weak) binary Goldbach conjecture also holds. (Contributed by AV, 26-Dec-2021)

Ref Expression
Assertion mogoldbb 
|- ( A. n e. ( ZZ>= ` 6 ) E. p e. Prime E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) -> A. n e. Even ( 2 < n -> E. p e. Prime E. q e. Prime n = ( p + q ) ) )

Proof

Step Hyp Ref Expression
1 nfra1 
 |-  F/ n A. n e. ( ZZ>= ` 6 ) E. p e. Prime E. q e. Prime E. r e. Prime n = ( ( p + q ) + r )
2 eqeq1 
 |-  ( n = m -> ( n = ( ( p + q ) + r ) <-> m = ( ( p + q ) + r ) ) )
3 2 rexbidv 
 |-  ( n = m -> ( E. r e. Prime n = ( ( p + q ) + r ) <-> E. r e. Prime m = ( ( p + q ) + r ) ) )
4 3 2rexbidv 
 |-  ( n = m -> ( E. p e. Prime E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) <-> E. p e. Prime E. q e. Prime E. r e. Prime m = ( ( p + q ) + r ) ) )
5 4 cbvralvw 
 |-  ( A. n e. ( ZZ>= ` 6 ) E. p e. Prime E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) <-> A. m e. ( ZZ>= ` 6 ) E. p e. Prime E. q e. Prime E. r e. Prime m = ( ( p + q ) + r ) )
6 6nn 
 |-  6 e. NN
7 6 nnzi 
 |-  6 e. ZZ
8 7 a1i 
 |-  ( ( n e. Even /\ 2 < n ) -> 6 e. ZZ )
9 evenz 
 |-  ( n e. Even -> n e. ZZ )
10 2z 
 |-  2 e. ZZ
11 10 a1i 
 |-  ( n e. Even -> 2 e. ZZ )
12 9 11 zaddcld 
 |-  ( n e. Even -> ( n + 2 ) e. ZZ )
13 12 adantr 
 |-  ( ( n e. Even /\ 2 < n ) -> ( n + 2 ) e. ZZ )
14 4cn 
 |-  4 e. CC
15 2cn 
 |-  2 e. CC
16 4p2e6 
 |-  ( 4 + 2 ) = 6
17 16 eqcomi 
 |-  6 = ( 4 + 2 )
18 14 15 17 mvrraddi 
 |-  ( 6 - 2 ) = 4
19 2p2e4 
 |-  ( 2 + 2 ) = 4
20 2evenALTV 
 |-  2 e. Even
21 evenltle 
 |-  ( ( n e. Even /\ 2 e. Even /\ 2 < n ) -> ( 2 + 2 ) <_ n )
22 20 21 mp3an2 
 |-  ( ( n e. Even /\ 2 < n ) -> ( 2 + 2 ) <_ n )
23 19 22 eqbrtrrid 
 |-  ( ( n e. Even /\ 2 < n ) -> 4 <_ n )
24 18 23 eqbrtrid 
 |-  ( ( n e. Even /\ 2 < n ) -> ( 6 - 2 ) <_ n )
25 6re 
 |-  6 e. RR
26 25 a1i 
 |-  ( n e. Even -> 6 e. RR )
27 2re 
 |-  2 e. RR
28 27 a1i 
 |-  ( n e. Even -> 2 e. RR )
29 9 zred 
 |-  ( n e. Even -> n e. RR )
30 26 28 29 3jca 
 |-  ( n e. Even -> ( 6 e. RR /\ 2 e. RR /\ n e. RR ) )
31 30 adantr 
 |-  ( ( n e. Even /\ 2 < n ) -> ( 6 e. RR /\ 2 e. RR /\ n e. RR ) )
32 lesubadd 
 |-  ( ( 6 e. RR /\ 2 e. RR /\ n e. RR ) -> ( ( 6 - 2 ) <_ n <-> 6 <_ ( n + 2 ) ) )
33 31 32 syl 
 |-  ( ( n e. Even /\ 2 < n ) -> ( ( 6 - 2 ) <_ n <-> 6 <_ ( n + 2 ) ) )
34 24 33 mpbid 
 |-  ( ( n e. Even /\ 2 < n ) -> 6 <_ ( n + 2 ) )
35 eluz2 
 |-  ( ( n + 2 ) e. ( ZZ>= ` 6 ) <-> ( 6 e. ZZ /\ ( n + 2 ) e. ZZ /\ 6 <_ ( n + 2 ) ) )
36 8 13 34 35 syl3anbrc 
 |-  ( ( n e. Even /\ 2 < n ) -> ( n + 2 ) e. ( ZZ>= ` 6 ) )
37 eqeq1 
 |-  ( m = ( n + 2 ) -> ( m = ( ( p + q ) + r ) <-> ( n + 2 ) = ( ( p + q ) + r ) ) )
38 37 rexbidv 
 |-  ( m = ( n + 2 ) -> ( E. r e. Prime m = ( ( p + q ) + r ) <-> E. r e. Prime ( n + 2 ) = ( ( p + q ) + r ) ) )
39 38 2rexbidv 
 |-  ( m = ( n + 2 ) -> ( E. p e. Prime E. q e. Prime E. r e. Prime m = ( ( p + q ) + r ) <-> E. p e. Prime E. q e. Prime E. r e. Prime ( n + 2 ) = ( ( p + q ) + r ) ) )
40 39 rspcv 
 |-  ( ( n + 2 ) e. ( ZZ>= ` 6 ) -> ( A. m e. ( ZZ>= ` 6 ) E. p e. Prime E. q e. Prime E. r e. Prime m = ( ( p + q ) + r ) -> E. p e. Prime E. q e. Prime E. r e. Prime ( n + 2 ) = ( ( p + q ) + r ) ) )
41 36 40 syl 
 |-  ( ( n e. Even /\ 2 < n ) -> ( A. m e. ( ZZ>= ` 6 ) E. p e. Prime E. q e. Prime E. r e. Prime m = ( ( p + q ) + r ) -> E. p e. Prime E. q e. Prime E. r e. Prime ( n + 2 ) = ( ( p + q ) + r ) ) )
42 5 41 biimtrid 
 |-  ( ( n e. Even /\ 2 < n ) -> ( A. n e. ( ZZ>= ` 6 ) E. p e. Prime E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) -> E. p e. Prime E. q e. Prime E. r e. Prime ( n + 2 ) = ( ( p + q ) + r ) ) )
43 nfv 
 |-  F/ p ( n e. Even /\ 2 < n )
44 nfre1 
 |-  F/ p E. p e. Prime E. q e. Prime n = ( p + q )
45 nfv 
 |-  F/ q ( ( n e. Even /\ 2 < n ) /\ p e. Prime )
46 nfcv 
 |-  F/_ q Prime
47 nfre1 
 |-  F/ q E. q e. Prime n = ( p + q )
48 46 47 nfrexw 
 |-  F/ q E. p e. Prime E. q e. Prime n = ( p + q )
49 simplrl 
 |-  ( ( ( ( n e. Even /\ 2 < n ) /\ ( p e. Prime /\ q e. Prime ) ) /\ r e. Prime ) -> p e. Prime )
50 simplrr 
 |-  ( ( ( ( n e. Even /\ 2 < n ) /\ ( p e. Prime /\ q e. Prime ) ) /\ r e. Prime ) -> q e. Prime )
51 simpr 
 |-  ( ( ( ( n e. Even /\ 2 < n ) /\ ( p e. Prime /\ q e. Prime ) ) /\ r e. Prime ) -> r e. Prime )
52 49 50 51 3jca 
 |-  ( ( ( ( n e. Even /\ 2 < n ) /\ ( p e. Prime /\ q e. Prime ) ) /\ r e. Prime ) -> ( p e. Prime /\ q e. Prime /\ r e. Prime ) )
53 52 adantr 
 |-  ( ( ( ( ( n e. Even /\ 2 < n ) /\ ( p e. Prime /\ q e. Prime ) ) /\ r e. Prime ) /\ ( n + 2 ) = ( ( p + q ) + r ) ) -> ( p e. Prime /\ q e. Prime /\ r e. Prime ) )
54 simp-4l 
 |-  ( ( ( ( ( n e. Even /\ 2 < n ) /\ ( p e. Prime /\ q e. Prime ) ) /\ r e. Prime ) /\ ( n + 2 ) = ( ( p + q ) + r ) ) -> n e. Even )
55 simpr 
 |-  ( ( ( ( ( n e. Even /\ 2 < n ) /\ ( p e. Prime /\ q e. Prime ) ) /\ r e. Prime ) /\ ( n + 2 ) = ( ( p + q ) + r ) ) -> ( n + 2 ) = ( ( p + q ) + r ) )
56 mogoldbblem 
 |-  ( ( ( p e. Prime /\ q e. Prime /\ r e. Prime ) /\ n e. Even /\ ( n + 2 ) = ( ( p + q ) + r ) ) -> E. y e. Prime E. x e. Prime n = ( y + x ) )
57 oveq1 
 |-  ( p = y -> ( p + q ) = ( y + q ) )
58 57 eqeq2d 
 |-  ( p = y -> ( n = ( p + q ) <-> n = ( y + q ) ) )
59 oveq2 
 |-  ( q = x -> ( y + q ) = ( y + x ) )
60 59 eqeq2d 
 |-  ( q = x -> ( n = ( y + q ) <-> n = ( y + x ) ) )
61 58 60 cbvrex2vw 
 |-  ( E. p e. Prime E. q e. Prime n = ( p + q ) <-> E. y e. Prime E. x e. Prime n = ( y + x ) )
62 56 61 sylibr 
 |-  ( ( ( p e. Prime /\ q e. Prime /\ r e. Prime ) /\ n e. Even /\ ( n + 2 ) = ( ( p + q ) + r ) ) -> E. p e. Prime E. q e. Prime n = ( p + q ) )
63 53 54 55 62 syl3anc 
 |-  ( ( ( ( ( n e. Even /\ 2 < n ) /\ ( p e. Prime /\ q e. Prime ) ) /\ r e. Prime ) /\ ( n + 2 ) = ( ( p + q ) + r ) ) -> E. p e. Prime E. q e. Prime n = ( p + q ) )
64 63 rexlimdva2 
 |-  ( ( ( n e. Even /\ 2 < n ) /\ ( p e. Prime /\ q e. Prime ) ) -> ( E. r e. Prime ( n + 2 ) = ( ( p + q ) + r ) -> E. p e. Prime E. q e. Prime n = ( p + q ) ) )
65 64 expr 
 |-  ( ( ( n e. Even /\ 2 < n ) /\ p e. Prime ) -> ( q e. Prime -> ( E. r e. Prime ( n + 2 ) = ( ( p + q ) + r ) -> E. p e. Prime E. q e. Prime n = ( p + q ) ) ) )
66 45 48 65 rexlimd 
 |-  ( ( ( n e. Even /\ 2 < n ) /\ p e. Prime ) -> ( E. q e. Prime E. r e. Prime ( n + 2 ) = ( ( p + q ) + r ) -> E. p e. Prime E. q e. Prime n = ( p + q ) ) )
67 66 ex 
 |-  ( ( n e. Even /\ 2 < n ) -> ( p e. Prime -> ( E. q e. Prime E. r e. Prime ( n + 2 ) = ( ( p + q ) + r ) -> E. p e. Prime E. q e. Prime n = ( p + q ) ) ) )
68 43 44 67 rexlimd 
 |-  ( ( n e. Even /\ 2 < n ) -> ( E. p e. Prime E. q e. Prime E. r e. Prime ( n + 2 ) = ( ( p + q ) + r ) -> E. p e. Prime E. q e. Prime n = ( p + q ) ) )
69 42 68 syldc 
 |-  ( A. n e. ( ZZ>= ` 6 ) E. p e. Prime E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) -> ( ( n e. Even /\ 2 < n ) -> E. p e. Prime E. q e. Prime n = ( p + q ) ) )
70 69 expd 
 |-  ( A. n e. ( ZZ>= ` 6 ) E. p e. Prime E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) -> ( n e. Even -> ( 2 < n -> E. p e. Prime E. q e. Prime n = ( p + q ) ) ) )
71 1 70 ralrimi 
 |-  ( A. n e. ( ZZ>= ` 6 ) E. p e. Prime E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) -> A. n e. Even ( 2 < n -> E. p e. Prime E. q e. Prime n = ( p + q ) ) )