Metamath Proof Explorer

Theorem bgoldbnnsum3prm

Description: If the binary Goldbach conjecture is valid, then every integer greater than 1 is the sum of at most 3 primes, showing that Schnirelmann's constant would be equal to 3. (Contributed by AV, 2-Aug-2020)

Ref Expression
Assertion bgoldbnnsum3prm 
|- ( A. m e. Even ( 4 < m -> m e. GoldbachEven ) -> A. n e. ( ZZ>= ` 2 ) E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ n = sum_ k e. ( 1 ... d ) ( f ` k ) ) )

Proof

Step Hyp Ref Expression
1 2z 
 |-  2 e. ZZ
2 9nn 
 |-  9 e. NN
3 2 nnzi 
 |-  9 e. ZZ
4 2re 
 |-  2 e. RR
5 9re 
 |-  9 e. RR
6 2lt9 
 |-  2 < 9
7 4 5 6 ltleii 
 |-  2 <_ 9
8 eluz2 
 |-  ( 9 e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ 9 e. ZZ /\ 2 <_ 9 ) )
9 1 3 7 8 mpbir3an 
 |-  9 e. ( ZZ>= ` 2 )
10 fzouzsplit 
 |-  ( 9 e. ( ZZ>= ` 2 ) -> ( ZZ>= ` 2 ) = ( ( 2 ..^ 9 ) u. ( ZZ>= ` 9 ) ) )
11 10 eleq2d 
 |-  ( 9 e. ( ZZ>= ` 2 ) -> ( n e. ( ZZ>= ` 2 ) <-> n e. ( ( 2 ..^ 9 ) u. ( ZZ>= ` 9 ) ) ) )
12 9 11 ax-mp 
 |-  ( n e. ( ZZ>= ` 2 ) <-> n e. ( ( 2 ..^ 9 ) u. ( ZZ>= ` 9 ) ) )
13 elun 
 |-  ( n e. ( ( 2 ..^ 9 ) u. ( ZZ>= ` 9 ) ) <-> ( n e. ( 2 ..^ 9 ) \/ n e. ( ZZ>= ` 9 ) ) )
14 12 13 bitri 
 |-  ( n e. ( ZZ>= ` 2 ) <-> ( n e. ( 2 ..^ 9 ) \/ n e. ( ZZ>= ` 9 ) ) )
15 elfzo2 
 |-  ( n e. ( 2 ..^ 9 ) <-> ( n e. ( ZZ>= ` 2 ) /\ 9 e. ZZ /\ n < 9 ) )
16 simp1 
 |-  ( ( n e. ( ZZ>= ` 2 ) /\ 9 e. ZZ /\ n < 9 ) -> n e. ( ZZ>= ` 2 ) )
17 df-9 
 |-  9 = ( 8 + 1 )
18 17 breq2i 
 |-  ( n < 9 <-> n < ( 8 + 1 ) )
19 eluz2nn 
 |-  ( n e. ( ZZ>= ` 2 ) -> n e. NN )
20 8nn 
 |-  8 e. NN
21 19 20 jctir 
 |-  ( n e. ( ZZ>= ` 2 ) -> ( n e. NN /\ 8 e. NN ) )
22 21 adantr 
 |-  ( ( n e. ( ZZ>= ` 2 ) /\ 9 e. ZZ ) -> ( n e. NN /\ 8 e. NN ) )
23 nnleltp1 
 |-  ( ( n e. NN /\ 8 e. NN ) -> ( n <_ 8 <-> n < ( 8 + 1 ) ) )
24 22 23 syl 
 |-  ( ( n e. ( ZZ>= ` 2 ) /\ 9 e. ZZ ) -> ( n <_ 8 <-> n < ( 8 + 1 ) ) )
25 24 biimprd 
 |-  ( ( n e. ( ZZ>= ` 2 ) /\ 9 e. ZZ ) -> ( n < ( 8 + 1 ) -> n <_ 8 ) )
26 18 25 syl5bi 
 |-  ( ( n e. ( ZZ>= ` 2 ) /\ 9 e. ZZ ) -> ( n < 9 -> n <_ 8 ) )
27 26 3impia 
 |-  ( ( n e. ( ZZ>= ` 2 ) /\ 9 e. ZZ /\ n < 9 ) -> n <_ 8 )
28 16 27 jca 
 |-  ( ( n e. ( ZZ>= ` 2 ) /\ 9 e. ZZ /\ n < 9 ) -> ( n e. ( ZZ>= ` 2 ) /\ n <_ 8 ) )
29 15 28 sylbi 
 |-  ( n e. ( 2 ..^ 9 ) -> ( n e. ( ZZ>= ` 2 ) /\ n <_ 8 ) )
30 nnsum3primesle9 
 |-  ( ( n e. ( ZZ>= ` 2 ) /\ n <_ 8 ) -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ n = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
31 29 30 syl 
 |-  ( n e. ( 2 ..^ 9 ) -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ n = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
32 31 a1d 
 |-  ( n e. ( 2 ..^ 9 ) -> ( A. m e. Even ( 4 < m -> m e. GoldbachEven ) -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ n = sum_ k e. ( 1 ... d ) ( f ` k ) ) ) )
33 breq2 
 |-  ( m = n -> ( 4 < m <-> 4 < n ) )
34 eleq1w 
 |-  ( m = n -> ( m e. GoldbachEven <-> n e. GoldbachEven ) )
35 33 34 imbi12d 
 |-  ( m = n -> ( ( 4 < m -> m e. GoldbachEven ) <-> ( 4 < n -> n e. GoldbachEven ) ) )
36 35 rspcv 
 |-  ( n e. Even -> ( A. m e. Even ( 4 < m -> m e. GoldbachEven ) -> ( 4 < n -> n e. GoldbachEven ) ) )
37 4re 
 |-  4 e. RR
38 37 a1i 
 |-  ( n e. ( ZZ>= ` 9 ) -> 4 e. RR )
39 5 a1i 
 |-  ( n e. ( ZZ>= ` 9 ) -> 9 e. RR )
40 eluzelre 
 |-  ( n e. ( ZZ>= ` 9 ) -> n e. RR )
41 38 39 40 3jca 
 |-  ( n e. ( ZZ>= ` 9 ) -> ( 4 e. RR /\ 9 e. RR /\ n e. RR ) )
42 41 adantl 
 |-  ( ( n e. Even /\ n e. ( ZZ>= ` 9 ) ) -> ( 4 e. RR /\ 9 e. RR /\ n e. RR ) )
43 eluzle 
 |-  ( n e. ( ZZ>= ` 9 ) -> 9 <_ n )
44 43 adantl 
 |-  ( ( n e. Even /\ n e. ( ZZ>= ` 9 ) ) -> 9 <_ n )
45 4lt9 
 |-  4 < 9
46 44 45 jctil 
 |-  ( ( n e. Even /\ n e. ( ZZ>= ` 9 ) ) -> ( 4 < 9 /\ 9 <_ n ) )
47 ltletr 
 |-  ( ( 4 e. RR /\ 9 e. RR /\ n e. RR ) -> ( ( 4 < 9 /\ 9 <_ n ) -> 4 < n ) )
48 42 46 47 sylc 
 |-  ( ( n e. Even /\ n e. ( ZZ>= ` 9 ) ) -> 4 < n )
49 pm2.27 
 |-  ( 4 < n -> ( ( 4 < n -> n e. GoldbachEven ) -> n e. GoldbachEven ) )
50 48 49 syl 
 |-  ( ( n e. Even /\ n e. ( ZZ>= ` 9 ) ) -> ( ( 4 < n -> n e. GoldbachEven ) -> n e. GoldbachEven ) )
51 50 ex 
 |-  ( n e. Even -> ( n e. ( ZZ>= ` 9 ) -> ( ( 4 < n -> n e. GoldbachEven ) -> n e. GoldbachEven ) ) )
52 36 51 syl5d 
 |-  ( n e. Even -> ( n e. ( ZZ>= ` 9 ) -> ( A. m e. Even ( 4 < m -> m e. GoldbachEven ) -> n e. GoldbachEven ) ) )
53 52 impcom 
 |-  ( ( n e. ( ZZ>= ` 9 ) /\ n e. Even ) -> ( A. m e. Even ( 4 < m -> m e. GoldbachEven ) -> n e. GoldbachEven ) )
54 nnsum3primesgbe 
 |-  ( n e. GoldbachEven -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ n = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
55 53 54 syl6 
 |-  ( ( n e. ( ZZ>= ` 9 ) /\ n e. Even ) -> ( A. m e. Even ( 4 < m -> m e. GoldbachEven ) -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ n = sum_ k e. ( 1 ... d ) ( f ` k ) ) ) )
56 3nn 
 |-  3 e. NN
57 56 a1i 
 |-  ( ( ( n e. ( ZZ>= ` 9 ) /\ n e. Odd ) /\ A. o e. Odd ( 5 < o -> o e. GoldbachOddW ) ) -> 3 e. NN )
58 oveq2 
 |-  ( d = 3 -> ( 1 ... d ) = ( 1 ... 3 ) )
59 58 oveq2d 
 |-  ( d = 3 -> ( Prime ^m ( 1 ... d ) ) = ( Prime ^m ( 1 ... 3 ) ) )
60 breq1 
 |-  ( d = 3 -> ( d <_ 3 <-> 3 <_ 3 ) )
61 58 sumeq1d 
 |-  ( d = 3 -> sum_ k e. ( 1 ... d ) ( f ` k ) = sum_ k e. ( 1 ... 3 ) ( f ` k ) )
62 61 eqeq2d 
 |-  ( d = 3 -> ( n = sum_ k e. ( 1 ... d ) ( f ` k ) <-> n = sum_ k e. ( 1 ... 3 ) ( f ` k ) ) )
63 60 62 anbi12d 
 |-  ( d = 3 -> ( ( d <_ 3 /\ n = sum_ k e. ( 1 ... d ) ( f ` k ) ) <-> ( 3 <_ 3 /\ n = sum_ k e. ( 1 ... 3 ) ( f ` k ) ) ) )
64 59 63 rexeqbidv 
 |-  ( d = 3 -> ( E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ n = sum_ k e. ( 1 ... d ) ( f ` k ) ) <-> E. f e. ( Prime ^m ( 1 ... 3 ) ) ( 3 <_ 3 /\ n = sum_ k e. ( 1 ... 3 ) ( f ` k ) ) ) )
65 64 adantl 
 |-  ( ( ( ( n e. ( ZZ>= ` 9 ) /\ n e. Odd ) /\ A. o e. Odd ( 5 < o -> o e. GoldbachOddW ) ) /\ d = 3 ) -> ( E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ n = sum_ k e. ( 1 ... d ) ( f ` k ) ) <-> E. f e. ( Prime ^m ( 1 ... 3 ) ) ( 3 <_ 3 /\ n = sum_ k e. ( 1 ... 3 ) ( f ` k ) ) ) )
66 3re 
 |-  3 e. RR
67 66 leidi 
 |-  3 <_ 3
68 67 a1i 
 |-  ( ( ( n e. ( ZZ>= ` 9 ) /\ n e. Odd ) /\ A. o e. Odd ( 5 < o -> o e. GoldbachOddW ) ) -> 3 <_ 3 )
69 6nn 
 |-  6 e. NN
70 69 nnzi 
 |-  6 e. ZZ
71 6re 
 |-  6 e. RR
72 6lt9 
 |-  6 < 9
73 71 5 72 ltleii 
 |-  6 <_ 9
74 eluzuzle 
 |-  ( ( 6 e. ZZ /\ 6 <_ 9 ) -> ( n e. ( ZZ>= ` 9 ) -> n e. ( ZZ>= ` 6 ) ) )
75 70 73 74 mp2an 
 |-  ( n e. ( ZZ>= ` 9 ) -> n e. ( ZZ>= ` 6 ) )
76 75 anim1i 
 |-  ( ( n e. ( ZZ>= ` 9 ) /\ n e. Odd ) -> ( n e. ( ZZ>= ` 6 ) /\ n e. Odd ) )
77 nnsum4primesodd 
 |-  ( A. o e. Odd ( 5 < o -> o e. GoldbachOddW ) -> ( ( n e. ( ZZ>= ` 6 ) /\ n e. Odd ) -> E. f e. ( Prime ^m ( 1 ... 3 ) ) n = sum_ k e. ( 1 ... 3 ) ( f ` k ) ) )
78 76 77 mpan9 
 |-  ( ( ( n e. ( ZZ>= ` 9 ) /\ n e. Odd ) /\ A. o e. Odd ( 5 < o -> o e. GoldbachOddW ) ) -> E. f e. ( Prime ^m ( 1 ... 3 ) ) n = sum_ k e. ( 1 ... 3 ) ( f ` k ) )
79 r19.42v 
 |-  ( E. f e. ( Prime ^m ( 1 ... 3 ) ) ( 3 <_ 3 /\ n = sum_ k e. ( 1 ... 3 ) ( f ` k ) ) <-> ( 3 <_ 3 /\ E. f e. ( Prime ^m ( 1 ... 3 ) ) n = sum_ k e. ( 1 ... 3 ) ( f ` k ) ) )
80 68 78 79 sylanbrc 
 |-  ( ( ( n e. ( ZZ>= ` 9 ) /\ n e. Odd ) /\ A. o e. Odd ( 5 < o -> o e. GoldbachOddW ) ) -> E. f e. ( Prime ^m ( 1 ... 3 ) ) ( 3 <_ 3 /\ n = sum_ k e. ( 1 ... 3 ) ( f ` k ) ) )
81 57 65 80 rspcedvd 
 |-  ( ( ( n e. ( ZZ>= ` 9 ) /\ n e. Odd ) /\ A. o e. Odd ( 5 < o -> o e. GoldbachOddW ) ) -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ n = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
82 81 expcom 
 |-  ( A. o e. Odd ( 5 < o -> o e. GoldbachOddW ) -> ( ( n e. ( ZZ>= ` 9 ) /\ n e. Odd ) -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ n = sum_ k e. ( 1 ... d ) ( f ` k ) ) ) )
83 sbgoldbwt 
 |-  ( A. m e. Even ( 4 < m -> m e. GoldbachEven ) -> A. o e. Odd ( 5 < o -> o e. GoldbachOddW ) )
84 82 83 syl11 
 |-  ( ( n e. ( ZZ>= ` 9 ) /\ n e. Odd ) -> ( A. m e. Even ( 4 < m -> m e. GoldbachEven ) -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ n = sum_ k e. ( 1 ... d ) ( f ` k ) ) ) )
85 eluzelz 
 |-  ( n e. ( ZZ>= ` 9 ) -> n e. ZZ )
86 zeoALTV 
 |-  ( n e. ZZ -> ( n e. Even \/ n e. Odd ) )
87 85 86 syl 
 |-  ( n e. ( ZZ>= ` 9 ) -> ( n e. Even \/ n e. Odd ) )
88 55 84 87 mpjaodan 
 |-  ( n e. ( ZZ>= ` 9 ) -> ( A. m e. Even ( 4 < m -> m e. GoldbachEven ) -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ n = sum_ k e. ( 1 ... d ) ( f ` k ) ) ) )
89 32 88 jaoi 
 |-  ( ( n e. ( 2 ..^ 9 ) \/ n e. ( ZZ>= ` 9 ) ) -> ( A. m e. Even ( 4 < m -> m e. GoldbachEven ) -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ n = sum_ k e. ( 1 ... d ) ( f ` k ) ) ) )
90 14 89 sylbi 
 |-  ( n e. ( ZZ>= ` 2 ) -> ( A. m e. Even ( 4 < m -> m e. GoldbachEven ) -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ n = sum_ k e. ( 1 ... d ) ( f ` k ) ) ) )
91 90 impcom 
 |-  ( ( A. m e. Even ( 4 < m -> m e. GoldbachEven ) /\ n e. ( ZZ>= ` 2 ) ) -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ n = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
92 91 ralrimiva 
 |-  ( A. m e. Even ( 4 < m -> m e. GoldbachEven ) -> A. n e. ( ZZ>= ` 2 ) E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ n = sum_ k e. ( 1 ... d ) ( f ` k ) ) )