Metamath Proof Explorer

Theorem nnsum3primesle9

Description: Every integer greater than 1 and less than or equal to 8 is the sum of at most 3 primes. (Contributed by AV, 2-Aug-2020)

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

Proof

Step Hyp Ref Expression
1 eluzelre 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. RR )
2 8re 
 |-  8 e. RR
3 2 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> 8 e. RR )
4 1 3 leloed 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N <_ 8 <-> ( N < 8 \/ N = 8 ) ) )
5 eluzelz 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. ZZ )
6 7nn 
 |-  7 e. NN
7 6 nnzi 
 |-  7 e. ZZ
8 zleltp1 
 |-  ( ( N e. ZZ /\ 7 e. ZZ ) -> ( N <_ 7 <-> N < ( 7 + 1 ) ) )
9 5 7 8 sylancl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N <_ 7 <-> N < ( 7 + 1 ) ) )
10 7re 
 |-  7 e. RR
11 10 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> 7 e. RR )
12 1 11 leloed 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N <_ 7 <-> ( N < 7 \/ N = 7 ) ) )
13 7p1e8 
 |-  ( 7 + 1 ) = 8
14 13 breq2i 
 |-  ( N < ( 7 + 1 ) <-> N < 8 )
15 14 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N < ( 7 + 1 ) <-> N < 8 ) )
16 9 12 15 3bitr3rd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N < 8 <-> ( N < 7 \/ N = 7 ) ) )
17 6nn 
 |-  6 e. NN
18 17 nnzi 
 |-  6 e. ZZ
19 zleltp1 
 |-  ( ( N e. ZZ /\ 6 e. ZZ ) -> ( N <_ 6 <-> N < ( 6 + 1 ) ) )
20 5 18 19 sylancl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N <_ 6 <-> N < ( 6 + 1 ) ) )
21 6re 
 |-  6 e. RR
22 21 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> 6 e. RR )
23 1 22 leloed 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N <_ 6 <-> ( N < 6 \/ N = 6 ) ) )
24 6p1e7 
 |-  ( 6 + 1 ) = 7
25 24 breq2i 
 |-  ( N < ( 6 + 1 ) <-> N < 7 )
26 25 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N < ( 6 + 1 ) <-> N < 7 ) )
27 20 23 26 3bitr3rd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N < 7 <-> ( N < 6 \/ N = 6 ) ) )
28 5nn 
 |-  5 e. NN
29 28 nnzi 
 |-  5 e. ZZ
30 zleltp1 
 |-  ( ( N e. ZZ /\ 5 e. ZZ ) -> ( N <_ 5 <-> N < ( 5 + 1 ) ) )
31 5 29 30 sylancl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N <_ 5 <-> N < ( 5 + 1 ) ) )
32 5re 
 |-  5 e. RR
33 32 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> 5 e. RR )
34 1 33 leloed 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N <_ 5 <-> ( N < 5 \/ N = 5 ) ) )
35 5p1e6 
 |-  ( 5 + 1 ) = 6
36 35 breq2i 
 |-  ( N < ( 5 + 1 ) <-> N < 6 )
37 36 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N < ( 5 + 1 ) <-> N < 6 ) )
38 31 34 37 3bitr3rd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N < 6 <-> ( N < 5 \/ N = 5 ) ) )
39 4z 
 |-  4 e. ZZ
40 zleltp1 
 |-  ( ( N e. ZZ /\ 4 e. ZZ ) -> ( N <_ 4 <-> N < ( 4 + 1 ) ) )
41 5 39 40 sylancl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N <_ 4 <-> N < ( 4 + 1 ) ) )
42 4re 
 |-  4 e. RR
43 42 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> 4 e. RR )
44 1 43 leloed 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N <_ 4 <-> ( N < 4 \/ N = 4 ) ) )
45 4p1e5 
 |-  ( 4 + 1 ) = 5
46 45 breq2i 
 |-  ( N < ( 4 + 1 ) <-> N < 5 )
47 46 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N < ( 4 + 1 ) <-> N < 5 ) )
48 41 44 47 3bitr3rd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N < 5 <-> ( N < 4 \/ N = 4 ) ) )
49 3z 
 |-  3 e. ZZ
50 zleltp1 
 |-  ( ( N e. ZZ /\ 3 e. ZZ ) -> ( N <_ 3 <-> N < ( 3 + 1 ) ) )
51 5 49 50 sylancl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N <_ 3 <-> N < ( 3 + 1 ) ) )
52 3re 
 |-  3 e. RR
53 52 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> 3 e. RR )
54 1 53 leloed 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N <_ 3 <-> ( N < 3 \/ N = 3 ) ) )
55 3p1e4 
 |-  ( 3 + 1 ) = 4
56 55 breq2i 
 |-  ( N < ( 3 + 1 ) <-> N < 4 )
57 56 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N < ( 3 + 1 ) <-> N < 4 ) )
58 51 54 57 3bitr3rd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N < 4 <-> ( N < 3 \/ N = 3 ) ) )
59 eluz2 
 |-  ( N e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ N e. ZZ /\ 2 <_ N ) )
60 2re 
 |-  2 e. RR
61 60 a1i 
 |-  ( N e. ZZ -> 2 e. RR )
62 zre 
 |-  ( N e. ZZ -> N e. RR )
63 61 62 leloed 
 |-  ( N e. ZZ -> ( 2 <_ N <-> ( 2 < N \/ 2 = N ) ) )
64 3m1e2 
 |-  ( 3 - 1 ) = 2
65 64 eqcomi 
 |-  2 = ( 3 - 1 )
66 65 breq1i 
 |-  ( 2 < N <-> ( 3 - 1 ) < N )
67 zlem1lt 
 |-  ( ( 3 e. ZZ /\ N e. ZZ ) -> ( 3 <_ N <-> ( 3 - 1 ) < N ) )
68 49 67 mpan 
 |-  ( N e. ZZ -> ( 3 <_ N <-> ( 3 - 1 ) < N ) )
69 68 biimprd 
 |-  ( N e. ZZ -> ( ( 3 - 1 ) < N -> 3 <_ N ) )
70 66 69 syl5bi 
 |-  ( N e. ZZ -> ( 2 < N -> 3 <_ N ) )
71 52 a1i 
 |-  ( N e. ZZ -> 3 e. RR )
72 71 62 lenltd 
 |-  ( N e. ZZ -> ( 3 <_ N <-> -. N < 3 ) )
73 pm2.21 
 |-  ( -. N < 3 -> ( N < 3 -> N = 2 ) )
74 72 73 syl6bi 
 |-  ( N e. ZZ -> ( 3 <_ N -> ( N < 3 -> N = 2 ) ) )
75 70 74 syldc 
 |-  ( 2 < N -> ( N e. ZZ -> ( N < 3 -> N = 2 ) ) )
76 eqcom 
 |-  ( 2 = N <-> N = 2 )
77 76 biimpi 
 |-  ( 2 = N -> N = 2 )
78 77 2a1d 
 |-  ( 2 = N -> ( N e. ZZ -> ( N < 3 -> N = 2 ) ) )
79 75 78 jaoi 
 |-  ( ( 2 < N \/ 2 = N ) -> ( N e. ZZ -> ( N < 3 -> N = 2 ) ) )
80 79 com12 
 |-  ( N e. ZZ -> ( ( 2 < N \/ 2 = N ) -> ( N < 3 -> N = 2 ) ) )
81 63 80 sylbid 
 |-  ( N e. ZZ -> ( 2 <_ N -> ( N < 3 -> N = 2 ) ) )
82 81 imp 
 |-  ( ( N e. ZZ /\ 2 <_ N ) -> ( N < 3 -> N = 2 ) )
83 2lt3 
 |-  2 < 3
84 breq1 
 |-  ( N = 2 -> ( N < 3 <-> 2 < 3 ) )
85 83 84 mpbiri 
 |-  ( N = 2 -> N < 3 )
86 82 85 impbid1 
 |-  ( ( N e. ZZ /\ 2 <_ N ) -> ( N < 3 <-> N = 2 ) )
87 86 3adant1 
 |-  ( ( 2 e. ZZ /\ N e. ZZ /\ 2 <_ N ) -> ( N < 3 <-> N = 2 ) )
88 59 87 sylbi 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N < 3 <-> N = 2 ) )
89 88 orbi1d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( N < 3 \/ N = 3 ) <-> ( N = 2 \/ N = 3 ) ) )
90 58 89 bitrd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N < 4 <-> ( N = 2 \/ N = 3 ) ) )
91 90 orbi1d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( N < 4 \/ N = 4 ) <-> ( ( N = 2 \/ N = 3 ) \/ N = 4 ) ) )
92 48 91 bitrd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N < 5 <-> ( ( N = 2 \/ N = 3 ) \/ N = 4 ) ) )
93 92 orbi1d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( N < 5 \/ N = 5 ) <-> ( ( ( N = 2 \/ N = 3 ) \/ N = 4 ) \/ N = 5 ) ) )
94 38 93 bitrd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N < 6 <-> ( ( ( N = 2 \/ N = 3 ) \/ N = 4 ) \/ N = 5 ) ) )
95 94 orbi1d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( N < 6 \/ N = 6 ) <-> ( ( ( ( N = 2 \/ N = 3 ) \/ N = 4 ) \/ N = 5 ) \/ N = 6 ) ) )
96 27 95 bitrd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N < 7 <-> ( ( ( ( N = 2 \/ N = 3 ) \/ N = 4 ) \/ N = 5 ) \/ N = 6 ) ) )
97 96 orbi1d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( N < 7 \/ N = 7 ) <-> ( ( ( ( ( N = 2 \/ N = 3 ) \/ N = 4 ) \/ N = 5 ) \/ N = 6 ) \/ N = 7 ) ) )
98 16 97 bitrd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N < 8 <-> ( ( ( ( ( N = 2 \/ N = 3 ) \/ N = 4 ) \/ N = 5 ) \/ N = 6 ) \/ N = 7 ) ) )
99 98 orbi1d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( N < 8 \/ N = 8 ) <-> ( ( ( ( ( ( N = 2 \/ N = 3 ) \/ N = 4 ) \/ N = 5 ) \/ N = 6 ) \/ N = 7 ) \/ N = 8 ) ) )
100 99 biimpd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( N < 8 \/ N = 8 ) -> ( ( ( ( ( ( N = 2 \/ N = 3 ) \/ N = 4 ) \/ N = 5 ) \/ N = 6 ) \/ N = 7 ) \/ N = 8 ) ) )
101 4 100 sylbid 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N <_ 8 -> ( ( ( ( ( ( N = 2 \/ N = 3 ) \/ N = 4 ) \/ N = 5 ) \/ N = 6 ) \/ N = 7 ) \/ N = 8 ) ) )
102 101 imp 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ N <_ 8 ) -> ( ( ( ( ( ( N = 2 \/ N = 3 ) \/ N = 4 ) \/ N = 5 ) \/ N = 6 ) \/ N = 7 ) \/ N = 8 ) )
103 2prm 
 |-  2 e. Prime
104 eleq1 
 |-  ( N = 2 -> ( N e. Prime <-> 2 e. Prime ) )
105 103 104 mpbiri 
 |-  ( N = 2 -> N e. Prime )
106 nnsum3primesprm 
 |-  ( N e. Prime -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
107 105 106 syl 
 |-  ( N = 2 -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
108 3prm 
 |-  3 e. Prime
109 eleq1 
 |-  ( N = 3 -> ( N e. Prime <-> 3 e. Prime ) )
110 108 109 mpbiri 
 |-  ( N = 3 -> N e. Prime )
111 110 106 syl 
 |-  ( N = 3 -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
112 107 111 jaoi 
 |-  ( ( N = 2 \/ N = 3 ) -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
113 nnsum3primes4 
 |-  E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ 4 = sum_ k e. ( 1 ... d ) ( f ` k ) )
114 eqeq1 
 |-  ( N = 4 -> ( N = sum_ k e. ( 1 ... d ) ( f ` k ) <-> 4 = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
115 114 anbi2d 
 |-  ( N = 4 -> ( ( d <_ 3 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) <-> ( d <_ 3 /\ 4 = sum_ k e. ( 1 ... d ) ( f ` k ) ) ) )
116 115 2rexbidv 
 |-  ( N = 4 -> ( E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) <-> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ 4 = sum_ k e. ( 1 ... d ) ( f ` k ) ) ) )
117 113 116 mpbiri 
 |-  ( N = 4 -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
118 112 117 jaoi 
 |-  ( ( ( N = 2 \/ N = 3 ) \/ N = 4 ) -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
119 5prm 
 |-  5 e. Prime
120 eleq1 
 |-  ( N = 5 -> ( N e. Prime <-> 5 e. Prime ) )
121 119 120 mpbiri 
 |-  ( N = 5 -> N e. Prime )
122 121 106 syl 
 |-  ( N = 5 -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
123 118 122 jaoi 
 |-  ( ( ( ( N = 2 \/ N = 3 ) \/ N = 4 ) \/ N = 5 ) -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
124 6gbe 
 |-  6 e. GoldbachEven
125 eleq1 
 |-  ( N = 6 -> ( N e. GoldbachEven <-> 6 e. GoldbachEven ) )
126 124 125 mpbiri 
 |-  ( N = 6 -> N e. GoldbachEven )
127 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 ) ) )
128 126 127 syl 
 |-  ( N = 6 -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
129 123 128 jaoi 
 |-  ( ( ( ( ( N = 2 \/ N = 3 ) \/ N = 4 ) \/ N = 5 ) \/ N = 6 ) -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
130 7prm 
 |-  7 e. Prime
131 eleq1 
 |-  ( N = 7 -> ( N e. Prime <-> 7 e. Prime ) )
132 130 131 mpbiri 
 |-  ( N = 7 -> N e. Prime )
133 132 106 syl 
 |-  ( N = 7 -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
134 129 133 jaoi 
 |-  ( ( ( ( ( ( N = 2 \/ N = 3 ) \/ N = 4 ) \/ N = 5 ) \/ N = 6 ) \/ N = 7 ) -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
135 8gbe 
 |-  8 e. GoldbachEven
136 eleq1 
 |-  ( N = 8 -> ( N e. GoldbachEven <-> 8 e. GoldbachEven ) )
137 135 136 mpbiri 
 |-  ( N = 8 -> N e. GoldbachEven )
138 137 127 syl 
 |-  ( N = 8 -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
139 134 138 jaoi 
 |-  ( ( ( ( ( ( ( N = 2 \/ N = 3 ) \/ N = 4 ) \/ N = 5 ) \/ N = 6 ) \/ N = 7 ) \/ N = 8 ) -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
140 102 139 syl 
 |-  ( ( 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 ) ) )