Metamath Proof Explorer


Theorem sbgoldbalt

Description: An alternate (related to the original) formulation of the binary Goldbach conjecture: Every even integer greater than 2 can be expressed as the sum of two primes. (Contributed by AV, 22-Jul-2020)

Ref Expression
Assertion sbgoldbalt
|- ( 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 ) ) )

Proof

Step Hyp Ref Expression
1 2z
 |-  2 e. ZZ
2 evenz
 |-  ( n e. Even -> n e. ZZ )
3 zltp1le
 |-  ( ( 2 e. ZZ /\ n e. ZZ ) -> ( 2 < n <-> ( 2 + 1 ) <_ n ) )
4 1 2 3 sylancr
 |-  ( n e. Even -> ( 2 < n <-> ( 2 + 1 ) <_ n ) )
5 2p1e3
 |-  ( 2 + 1 ) = 3
6 5 breq1i
 |-  ( ( 2 + 1 ) <_ n <-> 3 <_ n )
7 3re
 |-  3 e. RR
8 7 a1i
 |-  ( n e. Even -> 3 e. RR )
9 2 zred
 |-  ( n e. Even -> n e. RR )
10 8 9 leloed
 |-  ( n e. Even -> ( 3 <_ n <-> ( 3 < n \/ 3 = n ) ) )
11 3z
 |-  3 e. ZZ
12 zltp1le
 |-  ( ( 3 e. ZZ /\ n e. ZZ ) -> ( 3 < n <-> ( 3 + 1 ) <_ n ) )
13 11 2 12 sylancr
 |-  ( n e. Even -> ( 3 < n <-> ( 3 + 1 ) <_ n ) )
14 3p1e4
 |-  ( 3 + 1 ) = 4
15 14 breq1i
 |-  ( ( 3 + 1 ) <_ n <-> 4 <_ n )
16 4re
 |-  4 e. RR
17 16 a1i
 |-  ( n e. Even -> 4 e. RR )
18 17 9 leloed
 |-  ( n e. Even -> ( 4 <_ n <-> ( 4 < n \/ 4 = n ) ) )
19 pm3.35
 |-  ( ( 4 < n /\ ( 4 < n -> n e. GoldbachEven ) ) -> n e. GoldbachEven )
20 isgbe
 |-  ( n e. GoldbachEven <-> ( n e. Even /\ E. p e. Prime E. q e. Prime ( p e. Odd /\ q e. Odd /\ n = ( p + q ) ) ) )
21 simp3
 |-  ( ( p e. Odd /\ q e. Odd /\ n = ( p + q ) ) -> n = ( p + q ) )
22 21 a1i
 |-  ( ( ( n e. Even /\ p e. Prime ) /\ q e. Prime ) -> ( ( p e. Odd /\ q e. Odd /\ n = ( p + q ) ) -> n = ( p + q ) ) )
23 22 reximdva
 |-  ( ( n e. Even /\ p e. Prime ) -> ( E. q e. Prime ( p e. Odd /\ q e. Odd /\ n = ( p + q ) ) -> E. q e. Prime n = ( p + q ) ) )
24 23 reximdva
 |-  ( n e. Even -> ( E. p e. Prime E. q e. Prime ( p e. Odd /\ q e. Odd /\ n = ( p + q ) ) -> E. p e. Prime E. q e. Prime n = ( p + q ) ) )
25 24 imp
 |-  ( ( n e. Even /\ E. p e. Prime E. q e. Prime ( p e. Odd /\ q e. Odd /\ n = ( p + q ) ) ) -> E. p e. Prime E. q e. Prime n = ( p + q ) )
26 20 25 sylbi
 |-  ( n e. GoldbachEven -> E. p e. Prime E. q e. Prime n = ( p + q ) )
27 26 a1d
 |-  ( n e. GoldbachEven -> ( n e. Even -> E. p e. Prime E. q e. Prime n = ( p + q ) ) )
28 19 27 syl
 |-  ( ( 4 < n /\ ( 4 < n -> n e. GoldbachEven ) ) -> ( n e. Even -> E. p e. Prime E. q e. Prime n = ( p + q ) ) )
29 28 ex
 |-  ( 4 < n -> ( ( 4 < n -> n e. GoldbachEven ) -> ( n e. Even -> E. p e. Prime E. q e. Prime n = ( p + q ) ) ) )
30 29 com23
 |-  ( 4 < n -> ( n e. Even -> ( ( 4 < n -> n e. GoldbachEven ) -> E. p e. Prime E. q e. Prime n = ( p + q ) ) ) )
31 2prm
 |-  2 e. Prime
32 2p2e4
 |-  ( 2 + 2 ) = 4
33 32 eqcomi
 |-  4 = ( 2 + 2 )
34 rspceov
 |-  ( ( 2 e. Prime /\ 2 e. Prime /\ 4 = ( 2 + 2 ) ) -> E. p e. Prime E. q e. Prime 4 = ( p + q ) )
35 31 31 33 34 mp3an
 |-  E. p e. Prime E. q e. Prime 4 = ( p + q )
36 eqeq1
 |-  ( 4 = n -> ( 4 = ( p + q ) <-> n = ( p + q ) ) )
37 36 2rexbidv
 |-  ( 4 = n -> ( E. p e. Prime E. q e. Prime 4 = ( p + q ) <-> E. p e. Prime E. q e. Prime n = ( p + q ) ) )
38 35 37 mpbii
 |-  ( 4 = n -> E. p e. Prime E. q e. Prime n = ( p + q ) )
39 38 a1d
 |-  ( 4 = n -> ( ( 4 < n -> n e. GoldbachEven ) -> E. p e. Prime E. q e. Prime n = ( p + q ) ) )
40 39 a1d
 |-  ( 4 = n -> ( n e. Even -> ( ( 4 < n -> n e. GoldbachEven ) -> E. p e. Prime E. q e. Prime n = ( p + q ) ) ) )
41 30 40 jaoi
 |-  ( ( 4 < n \/ 4 = n ) -> ( n e. Even -> ( ( 4 < n -> n e. GoldbachEven ) -> E. p e. Prime E. q e. Prime n = ( p + q ) ) ) )
42 41 com12
 |-  ( n e. Even -> ( ( 4 < n \/ 4 = n ) -> ( ( 4 < n -> n e. GoldbachEven ) -> E. p e. Prime E. q e. Prime n = ( p + q ) ) ) )
43 18 42 sylbid
 |-  ( n e. Even -> ( 4 <_ n -> ( ( 4 < n -> n e. GoldbachEven ) -> E. p e. Prime E. q e. Prime n = ( p + q ) ) ) )
44 15 43 syl5bi
 |-  ( n e. Even -> ( ( 3 + 1 ) <_ n -> ( ( 4 < n -> n e. GoldbachEven ) -> E. p e. Prime E. q e. Prime n = ( p + q ) ) ) )
45 13 44 sylbid
 |-  ( n e. Even -> ( 3 < n -> ( ( 4 < n -> n e. GoldbachEven ) -> E. p e. Prime E. q e. Prime n = ( p + q ) ) ) )
46 45 com12
 |-  ( 3 < n -> ( n e. Even -> ( ( 4 < n -> n e. GoldbachEven ) -> E. p e. Prime E. q e. Prime n = ( p + q ) ) ) )
47 3odd
 |-  3 e. Odd
48 eleq1
 |-  ( 3 = n -> ( 3 e. Odd <-> n e. Odd ) )
49 47 48 mpbii
 |-  ( 3 = n -> n e. Odd )
50 oddneven
 |-  ( n e. Odd -> -. n e. Even )
51 49 50 syl
 |-  ( 3 = n -> -. n e. Even )
52 51 pm2.21d
 |-  ( 3 = n -> ( n e. Even -> ( ( 4 < n -> n e. GoldbachEven ) -> E. p e. Prime E. q e. Prime n = ( p + q ) ) ) )
53 46 52 jaoi
 |-  ( ( 3 < n \/ 3 = n ) -> ( n e. Even -> ( ( 4 < n -> n e. GoldbachEven ) -> E. p e. Prime E. q e. Prime n = ( p + q ) ) ) )
54 53 com12
 |-  ( n e. Even -> ( ( 3 < n \/ 3 = n ) -> ( ( 4 < n -> n e. GoldbachEven ) -> E. p e. Prime E. q e. Prime n = ( p + q ) ) ) )
55 10 54 sylbid
 |-  ( n e. Even -> ( 3 <_ n -> ( ( 4 < n -> n e. GoldbachEven ) -> E. p e. Prime E. q e. Prime n = ( p + q ) ) ) )
56 6 55 syl5bi
 |-  ( n e. Even -> ( ( 2 + 1 ) <_ n -> ( ( 4 < n -> n e. GoldbachEven ) -> E. p e. Prime E. q e. Prime n = ( p + q ) ) ) )
57 4 56 sylbid
 |-  ( n e. Even -> ( 2 < n -> ( ( 4 < n -> n e. GoldbachEven ) -> E. p e. Prime E. q e. Prime n = ( p + q ) ) ) )
58 57 com23
 |-  ( n e. Even -> ( ( 4 < n -> n e. GoldbachEven ) -> ( 2 < n -> E. p e. Prime E. q e. Prime n = ( p + q ) ) ) )
59 2lt4
 |-  2 < 4
60 2re
 |-  2 e. RR
61 60 a1i
 |-  ( n e. Even -> 2 e. RR )
62 lttr
 |-  ( ( 2 e. RR /\ 4 e. RR /\ n e. RR ) -> ( ( 2 < 4 /\ 4 < n ) -> 2 < n ) )
63 61 17 9 62 syl3anc
 |-  ( n e. Even -> ( ( 2 < 4 /\ 4 < n ) -> 2 < n ) )
64 59 63 mpani
 |-  ( n e. Even -> ( 4 < n -> 2 < n ) )
65 64 imp
 |-  ( ( n e. Even /\ 4 < n ) -> 2 < n )
66 simpll
 |-  ( ( ( n e. Even /\ 4 < n ) /\ E. p e. Prime E. q e. Prime n = ( p + q ) ) -> n e. Even )
67 simpr
 |-  ( ( ( n e. Even /\ 4 < n ) /\ p e. Prime ) -> p e. Prime )
68 67 anim1i
 |-  ( ( ( ( n e. Even /\ 4 < n ) /\ p e. Prime ) /\ q e. Prime ) -> ( p e. Prime /\ q e. Prime ) )
69 68 adantr
 |-  ( ( ( ( ( n e. Even /\ 4 < n ) /\ p e. Prime ) /\ q e. Prime ) /\ n = ( p + q ) ) -> ( p e. Prime /\ q e. Prime ) )
70 simpll
 |-  ( ( ( ( n e. Even /\ 4 < n ) /\ p e. Prime ) /\ q e. Prime ) -> ( n e. Even /\ 4 < n ) )
71 70 anim1i
 |-  ( ( ( ( ( n e. Even /\ 4 < n ) /\ p e. Prime ) /\ q e. Prime ) /\ n = ( p + q ) ) -> ( ( n e. Even /\ 4 < n ) /\ n = ( p + q ) ) )
72 df-3an
 |-  ( ( n e. Even /\ 4 < n /\ n = ( p + q ) ) <-> ( ( n e. Even /\ 4 < n ) /\ n = ( p + q ) ) )
73 71 72 sylibr
 |-  ( ( ( ( ( n e. Even /\ 4 < n ) /\ p e. Prime ) /\ q e. Prime ) /\ n = ( p + q ) ) -> ( n e. Even /\ 4 < n /\ n = ( p + q ) ) )
74 sbgoldbaltlem2
 |-  ( ( p e. Prime /\ q e. Prime ) -> ( ( n e. Even /\ 4 < n /\ n = ( p + q ) ) -> ( p e. Odd /\ q e. Odd ) ) )
75 69 73 74 sylc
 |-  ( ( ( ( ( n e. Even /\ 4 < n ) /\ p e. Prime ) /\ q e. Prime ) /\ n = ( p + q ) ) -> ( p e. Odd /\ q e. Odd ) )
76 simpr
 |-  ( ( ( ( ( n e. Even /\ 4 < n ) /\ p e. Prime ) /\ q e. Prime ) /\ n = ( p + q ) ) -> n = ( p + q ) )
77 df-3an
 |-  ( ( p e. Odd /\ q e. Odd /\ n = ( p + q ) ) <-> ( ( p e. Odd /\ q e. Odd ) /\ n = ( p + q ) ) )
78 75 76 77 sylanbrc
 |-  ( ( ( ( ( n e. Even /\ 4 < n ) /\ p e. Prime ) /\ q e. Prime ) /\ n = ( p + q ) ) -> ( p e. Odd /\ q e. Odd /\ n = ( p + q ) ) )
79 78 ex
 |-  ( ( ( ( n e. Even /\ 4 < n ) /\ p e. Prime ) /\ q e. Prime ) -> ( n = ( p + q ) -> ( p e. Odd /\ q e. Odd /\ n = ( p + q ) ) ) )
80 79 reximdva
 |-  ( ( ( n e. Even /\ 4 < n ) /\ p e. Prime ) -> ( E. q e. Prime n = ( p + q ) -> E. q e. Prime ( p e. Odd /\ q e. Odd /\ n = ( p + q ) ) ) )
81 80 reximdva
 |-  ( ( n e. Even /\ 4 < n ) -> ( E. p e. Prime E. q e. Prime n = ( p + q ) -> E. p e. Prime E. q e. Prime ( p e. Odd /\ q e. Odd /\ n = ( p + q ) ) ) )
82 81 imp
 |-  ( ( ( n e. Even /\ 4 < n ) /\ E. p e. Prime E. q e. Prime n = ( p + q ) ) -> E. p e. Prime E. q e. Prime ( p e. Odd /\ q e. Odd /\ n = ( p + q ) ) )
83 66 82 jca
 |-  ( ( ( n e. Even /\ 4 < n ) /\ E. p e. Prime E. q e. Prime n = ( p + q ) ) -> ( n e. Even /\ E. p e. Prime E. q e. Prime ( p e. Odd /\ q e. Odd /\ n = ( p + q ) ) ) )
84 83 ex
 |-  ( ( n e. Even /\ 4 < n ) -> ( E. p e. Prime E. q e. Prime n = ( p + q ) -> ( n e. Even /\ E. p e. Prime E. q e. Prime ( p e. Odd /\ q e. Odd /\ n = ( p + q ) ) ) ) )
85 84 20 syl6ibr
 |-  ( ( n e. Even /\ 4 < n ) -> ( E. p e. Prime E. q e. Prime n = ( p + q ) -> n e. GoldbachEven ) )
86 65 85 embantd
 |-  ( ( n e. Even /\ 4 < n ) -> ( ( 2 < n -> E. p e. Prime E. q e. Prime n = ( p + q ) ) -> n e. GoldbachEven ) )
87 86 ex
 |-  ( n e. Even -> ( 4 < n -> ( ( 2 < n -> E. p e. Prime E. q e. Prime n = ( p + q ) ) -> n e. GoldbachEven ) ) )
88 87 com23
 |-  ( n e. Even -> ( ( 2 < n -> E. p e. Prime E. q e. Prime n = ( p + q ) ) -> ( 4 < n -> n e. GoldbachEven ) ) )
89 58 88 impbid
 |-  ( n e. Even -> ( ( 4 < n -> n e. GoldbachEven ) <-> ( 2 < n -> E. p e. Prime E. q e. Prime n = ( p + q ) ) ) )
90 89 ralbiia
 |-  ( 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 ) ) )