Metamath Proof Explorer

Theorem wtgoldbnnsum4prm

Description: If the (weak) ternary Goldbach conjecture is valid, then every integer greater than 1 is the sum of at most 4 primes, showing that Schnirelmann's constant would be less than or equal to 4. See corollary 1.1 in Helfgott p. 4. (Contributed by AV, 25-Jul-2020)

Ref Expression
Assertion wtgoldbnnsum4prm 
|- ( A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) -> A. n e. ( ZZ>= ` 2 ) E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 4 /\ 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 biimtrid 
 |-  ( ( 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 nnsum4primesle9 
 |-  ( ( n e. ( ZZ>= ` 2 ) /\ n <_ 8 ) -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 4 /\ 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 <_ 4 /\ n = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
32 31 a1d 
 |-  ( n e. ( 2 ..^ 9 ) -> ( A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 4 /\ n = sum_ k e. ( 1 ... d ) ( f ` k ) ) ) )
33 4nn 
 |-  4 e. NN
34 33 a1i 
 |-  ( ( ( n e. ( ZZ>= ` 9 ) /\ n e. Even ) /\ A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) ) -> 4 e. NN )
35 oveq2 
 |-  ( d = 4 -> ( 1 ... d ) = ( 1 ... 4 ) )
36 35 oveq2d 
 |-  ( d = 4 -> ( Prime ^m ( 1 ... d ) ) = ( Prime ^m ( 1 ... 4 ) ) )
37 breq1 
 |-  ( d = 4 -> ( d <_ 4 <-> 4 <_ 4 ) )
38 35 sumeq1d 
 |-  ( d = 4 -> sum_ k e. ( 1 ... d ) ( f ` k ) = sum_ k e. ( 1 ... 4 ) ( f ` k ) )
39 38 eqeq2d 
 |-  ( d = 4 -> ( n = sum_ k e. ( 1 ... d ) ( f ` k ) <-> n = sum_ k e. ( 1 ... 4 ) ( f ` k ) ) )
40 37 39 anbi12d 
 |-  ( d = 4 -> ( ( d <_ 4 /\ n = sum_ k e. ( 1 ... d ) ( f ` k ) ) <-> ( 4 <_ 4 /\ n = sum_ k e. ( 1 ... 4 ) ( f ` k ) ) ) )
41 36 40 rexeqbidv 
 |-  ( d = 4 -> ( E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 4 /\ n = sum_ k e. ( 1 ... d ) ( f ` k ) ) <-> E. f e. ( Prime ^m ( 1 ... 4 ) ) ( 4 <_ 4 /\ n = sum_ k e. ( 1 ... 4 ) ( f ` k ) ) ) )
42 41 adantl 
 |-  ( ( ( ( n e. ( ZZ>= ` 9 ) /\ n e. Even ) /\ A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) ) /\ d = 4 ) -> ( E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 4 /\ n = sum_ k e. ( 1 ... d ) ( f ` k ) ) <-> E. f e. ( Prime ^m ( 1 ... 4 ) ) ( 4 <_ 4 /\ n = sum_ k e. ( 1 ... 4 ) ( f ` k ) ) ) )
43 4re 
 |-  4 e. RR
44 43 leidi 
 |-  4 <_ 4
45 44 a1i 
 |-  ( ( ( n e. ( ZZ>= ` 9 ) /\ n e. Even ) /\ A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) ) -> 4 <_ 4 )
46 nnsum4primeseven 
 |-  ( A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) -> ( ( n e. ( ZZ>= ` 9 ) /\ n e. Even ) -> E. f e. ( Prime ^m ( 1 ... 4 ) ) n = sum_ k e. ( 1 ... 4 ) ( f ` k ) ) )
47 46 impcom 
 |-  ( ( ( n e. ( ZZ>= ` 9 ) /\ n e. Even ) /\ A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) ) -> E. f e. ( Prime ^m ( 1 ... 4 ) ) n = sum_ k e. ( 1 ... 4 ) ( f ` k ) )
48 r19.42v 
 |-  ( E. f e. ( Prime ^m ( 1 ... 4 ) ) ( 4 <_ 4 /\ n = sum_ k e. ( 1 ... 4 ) ( f ` k ) ) <-> ( 4 <_ 4 /\ E. f e. ( Prime ^m ( 1 ... 4 ) ) n = sum_ k e. ( 1 ... 4 ) ( f ` k ) ) )
49 45 47 48 sylanbrc 
 |-  ( ( ( n e. ( ZZ>= ` 9 ) /\ n e. Even ) /\ A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) ) -> E. f e. ( Prime ^m ( 1 ... 4 ) ) ( 4 <_ 4 /\ n = sum_ k e. ( 1 ... 4 ) ( f ` k ) ) )
50 34 42 49 rspcedvd 
 |-  ( ( ( n e. ( ZZ>= ` 9 ) /\ n e. Even ) /\ A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) ) -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 4 /\ n = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
51 50 ex 
 |-  ( ( n e. ( ZZ>= ` 9 ) /\ n e. Even ) -> ( A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 4 /\ n = sum_ k e. ( 1 ... d ) ( f ` k ) ) ) )
52 3nn 
 |-  3 e. NN
53 52 a1i 
 |-  ( ( ( n e. ( ZZ>= ` 9 ) /\ n e. Odd ) /\ A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) ) -> 3 e. NN )
54 oveq2 
 |-  ( d = 3 -> ( 1 ... d ) = ( 1 ... 3 ) )
55 54 oveq2d 
 |-  ( d = 3 -> ( Prime ^m ( 1 ... d ) ) = ( Prime ^m ( 1 ... 3 ) ) )
56 breq1 
 |-  ( d = 3 -> ( d <_ 4 <-> 3 <_ 4 ) )
57 54 sumeq1d 
 |-  ( d = 3 -> sum_ k e. ( 1 ... d ) ( f ` k ) = sum_ k e. ( 1 ... 3 ) ( f ` k ) )
58 57 eqeq2d 
 |-  ( d = 3 -> ( n = sum_ k e. ( 1 ... d ) ( f ` k ) <-> n = sum_ k e. ( 1 ... 3 ) ( f ` k ) ) )
59 56 58 anbi12d 
 |-  ( d = 3 -> ( ( d <_ 4 /\ n = sum_ k e. ( 1 ... d ) ( f ` k ) ) <-> ( 3 <_ 4 /\ n = sum_ k e. ( 1 ... 3 ) ( f ` k ) ) ) )
60 55 59 rexeqbidv 
 |-  ( d = 3 -> ( E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 4 /\ n = sum_ k e. ( 1 ... d ) ( f ` k ) ) <-> E. f e. ( Prime ^m ( 1 ... 3 ) ) ( 3 <_ 4 /\ n = sum_ k e. ( 1 ... 3 ) ( f ` k ) ) ) )
61 60 adantl 
 |-  ( ( ( ( n e. ( ZZ>= ` 9 ) /\ n e. Odd ) /\ A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) ) /\ d = 3 ) -> ( E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 4 /\ n = sum_ k e. ( 1 ... d ) ( f ` k ) ) <-> E. f e. ( Prime ^m ( 1 ... 3 ) ) ( 3 <_ 4 /\ n = sum_ k e. ( 1 ... 3 ) ( f ` k ) ) ) )
62 3re 
 |-  3 e. RR
63 3lt4 
 |-  3 < 4
64 62 43 63 ltleii 
 |-  3 <_ 4
65 64 a1i 
 |-  ( ( ( n e. ( ZZ>= ` 9 ) /\ n e. Odd ) /\ A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) ) -> 3 <_ 4 )
66 6nn 
 |-  6 e. NN
67 66 nnzi 
 |-  6 e. ZZ
68 6re 
 |-  6 e. RR
69 6lt9 
 |-  6 < 9
70 68 5 69 ltleii 
 |-  6 <_ 9
71 eluzuzle 
 |-  ( ( 6 e. ZZ /\ 6 <_ 9 ) -> ( n e. ( ZZ>= ` 9 ) -> n e. ( ZZ>= ` 6 ) ) )
72 67 70 71 mp2an 
 |-  ( n e. ( ZZ>= ` 9 ) -> n e. ( ZZ>= ` 6 ) )
73 72 anim1i 
 |-  ( ( n e. ( ZZ>= ` 9 ) /\ n e. Odd ) -> ( n e. ( ZZ>= ` 6 ) /\ n e. Odd ) )
74 nnsum4primesodd 
 |-  ( A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) -> ( ( n e. ( ZZ>= ` 6 ) /\ n e. Odd ) -> E. f e. ( Prime ^m ( 1 ... 3 ) ) n = sum_ k e. ( 1 ... 3 ) ( f ` k ) ) )
75 73 74 mpan9 
 |-  ( ( ( n e. ( ZZ>= ` 9 ) /\ n e. Odd ) /\ A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) ) -> E. f e. ( Prime ^m ( 1 ... 3 ) ) n = sum_ k e. ( 1 ... 3 ) ( f ` k ) )
76 r19.42v 
 |-  ( E. f e. ( Prime ^m ( 1 ... 3 ) ) ( 3 <_ 4 /\ n = sum_ k e. ( 1 ... 3 ) ( f ` k ) ) <-> ( 3 <_ 4 /\ E. f e. ( Prime ^m ( 1 ... 3 ) ) n = sum_ k e. ( 1 ... 3 ) ( f ` k ) ) )
77 65 75 76 sylanbrc 
 |-  ( ( ( n e. ( ZZ>= ` 9 ) /\ n e. Odd ) /\ A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) ) -> E. f e. ( Prime ^m ( 1 ... 3 ) ) ( 3 <_ 4 /\ n = sum_ k e. ( 1 ... 3 ) ( f ` k ) ) )
78 53 61 77 rspcedvd 
 |-  ( ( ( n e. ( ZZ>= ` 9 ) /\ n e. Odd ) /\ A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) ) -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 4 /\ n = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
79 78 ex 
 |-  ( ( n e. ( ZZ>= ` 9 ) /\ n e. Odd ) -> ( A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 4 /\ n = sum_ k e. ( 1 ... d ) ( f ` k ) ) ) )
80 eluzelz 
 |-  ( n e. ( ZZ>= ` 9 ) -> n e. ZZ )
81 zeoALTV 
 |-  ( n e. ZZ -> ( n e. Even \/ n e. Odd ) )
82 80 81 syl 
 |-  ( n e. ( ZZ>= ` 9 ) -> ( n e. Even \/ n e. Odd ) )
83 51 79 82 mpjaodan 
 |-  ( n e. ( ZZ>= ` 9 ) -> ( A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 4 /\ n = sum_ k e. ( 1 ... d ) ( f ` k ) ) ) )
84 32 83 jaoi 
 |-  ( ( n e. ( 2 ..^ 9 ) \/ n e. ( ZZ>= ` 9 ) ) -> ( A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 4 /\ n = sum_ k e. ( 1 ... d ) ( f ` k ) ) ) )
85 14 84 sylbi 
 |-  ( n e. ( ZZ>= ` 2 ) -> ( A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 4 /\ n = sum_ k e. ( 1 ... d ) ( f ` k ) ) ) )
86 85 impcom 
 |-  ( ( A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) /\ n e. ( ZZ>= ` 2 ) ) -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 4 /\ n = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
87 86 ralrimiva 
 |-  ( A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) -> A. n e. ( ZZ>= ` 2 ) E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 4 /\ n = sum_ k e. ( 1 ... d ) ( f ` k ) ) )