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 biimtrid 
 |-  ( 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 biimtrid 
 |-  ( 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 imbitrrdi 
 |-  ( ( 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 ) ) )