Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  nnsum3primesle9 Structured version   Visualization version   Unicode version
Theorem nnsum3primesle9 41682
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.)
Assertion
Ref Expression
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 ) ) )
Distinct variable group:   N, d, f, k
Proof of Theorem nnsum3primesle9
StepHypRef Expression
1 eluzelre 11698 . . . . 5 |- ( N e. ( ZZ>= ` 2 ) -> N e. RR )
2 8re 11105 . . . . . 6 |- 8 e. RR
32a1i 11 . . . . 5 |- ( N e. ( ZZ>= ` 2 ) -> 8 e. RR )
41, 3leloed 10180 . . . 4 |- ( N e. ( ZZ>= ` 2 ) -> ( N <_ 8 <-> ( N < 8 \/ N = 8 ) ) )
5 eluzelz 11697 . . . . . . . . 9 |- ( N e. ( ZZ>= ` 2 ) -> N e. ZZ )
6 7nn 11190 . . . . . . . . . 10 |- 7 e. NN
76nnzi 11401 . . . . . . . . 9 |- 7 e. ZZ
8 zleltp1 11428 . . . . . . . . 9 |- ( ( N e. ZZ /\ 7 e. ZZ ) -> ( N <_ 7 <-> N < ( 7 + 1 ) ) )
95, 7, 8sylancl 694 . . . . . . . 8 |- ( N e. ( ZZ>= ` 2 ) -> ( N <_ 7 <-> N < ( 7 + 1 ) ) )
10 7re 11103 . . . . . . . . . 10 |- 7 e. RR
1110a1i 11 . . . . . . . . 9 |- ( N e. ( ZZ>= ` 2 ) -> 7 e. RR )
121, 11leloed 10180 . . . . . . . 8 |- ( N e. ( ZZ>= ` 2 ) -> ( N <_ 7 <-> ( N < 7 \/ N = 7 ) ) )
13 7p1e8 11157 . . . . . . . . . 10 |- ( 7 + 1 ) = 8
1413breq2i 4661 . . . . . . . . 9 |- ( N < ( 7 + 1 ) <-> N < 8 )
1514a1i 11 . . . . . . . 8 |- ( N e. ( ZZ>= ` 2 ) -> ( N < ( 7 + 1 ) <-> N < 8 ) )
169, 12, 153bitr3rd 299 . . . . . . 7 |- ( N e. ( ZZ>= ` 2 ) -> ( N < 8 <-> ( N < 7 \/ N = 7 ) ) )
17 6nn 11189 . . . . . . . . . . . 12 |- 6 e. NN
1817nnzi 11401 . . . . . . . . . . 11 |- 6 e. ZZ
19 zleltp1 11428 . . . . . . . . . . 11 |- ( ( N e. ZZ /\ 6 e. ZZ ) -> ( N <_ 6 <-> N < ( 6 + 1 ) ) )
205, 18, 19sylancl 694 . . . . . . . . . 10 |- ( N e. ( ZZ>= ` 2 ) -> ( N <_ 6 <-> N < ( 6 + 1 ) ) )
21 6re 11101 . . . . . . . . . . . 12 |- 6 e. RR
2221a1i 11 . . . . . . . . . . 11 |- ( N e. ( ZZ>= ` 2 ) -> 6 e. RR )
231, 22leloed 10180 . . . . . . . . . 10 |- ( N e. ( ZZ>= ` 2 ) -> ( N <_ 6 <-> ( N < 6 \/ N = 6 ) ) )
24 6p1e7 11156 . . . . . . . . . . . 12 |- ( 6 + 1 ) = 7
2524breq2i 4661 . . . . . . . . . . 11 |- ( N < ( 6 + 1 ) <-> N < 7 )
2625a1i 11 . . . . . . . . . 10 |- ( N e. ( ZZ>= ` 2 ) -> ( N < ( 6 + 1 ) <-> N < 7 ) )
2720, 23, 263bitr3rd 299 . . . . . . . . 9 |- ( N e. ( ZZ>= ` 2 ) -> ( N < 7 <-> ( N < 6 \/ N = 6 ) ) )
28 5nn 11188 . . . . . . . . . . . . . 14 |- 5 e. NN
2928nnzi 11401 . . . . . . . . . . . . 13 |- 5 e. ZZ
30 zleltp1 11428 . . . . . . . . . . . . 13 |- ( ( N e. ZZ /\ 5 e. ZZ ) -> ( N <_ 5 <-> N < ( 5 + 1 ) ) )
315, 29, 30sylancl 694 . . . . . . . . . . . 12 |- ( N e. ( ZZ>= ` 2 ) -> ( N <_ 5 <-> N < ( 5 + 1 ) ) )
32 5re 11099 . . . . . . . . . . . . . 14 |- 5 e. RR
3332a1i 11 . . . . . . . . . . . . 13 |- ( N e. ( ZZ>= ` 2 ) -> 5 e. RR )
341, 33leloed 10180 . . . . . . . . . . . 12 |- ( N e. ( ZZ>= ` 2 ) -> ( N <_ 5 <-> ( N < 5 \/ N = 5 ) ) )
35 5p1e6 11155 . . . . . . . . . . . . . 14 |- ( 5 + 1 ) = 6
3635breq2i 4661 . . . . . . . . . . . . 13 |- ( N < ( 5 + 1 ) <-> N < 6 )
3736a1i 11 . . . . . . . . . . . 12 |- ( N e. ( ZZ>= ` 2 ) -> ( N < ( 5 + 1 ) <-> N < 6 ) )
3831, 34, 373bitr3rd 299 . . . . . . . . . . 11 |- ( N e. ( ZZ>= ` 2 ) -> ( N < 6 <-> ( N < 5 \/ N = 5 ) ) )
39 4z 11411 . . . . . . . . . . . . . . 15 |- 4 e. ZZ
40 zleltp1 11428 . . . . . . . . . . . . . . 15 |- ( ( N e. ZZ /\ 4 e. ZZ ) -> ( N <_ 4 <-> N < ( 4 + 1 ) ) )
415, 39, 40sylancl 694 . . . . . . . . . . . . . 14 |- ( N e. ( ZZ>= ` 2 ) -> ( N <_ 4 <-> N < ( 4 + 1 ) ) )
42 4re 11097 . . . . . . . . . . . . . . . 16 |- 4 e. RR
4342a1i 11 . . . . . . . . . . . . . . 15 |- ( N e. ( ZZ>= ` 2 ) -> 4 e. RR )
441, 43leloed 10180 . . . . . . . . . . . . . 14 |- ( N e. ( ZZ>= ` 2 ) -> ( N <_ 4 <-> ( N < 4 \/ N = 4 ) ) )
45 4p1e5 11154 . . . . . . . . . . . . . . . 16 |- ( 4 + 1 ) = 5
4645breq2i 4661 . . . . . . . . . . . . . . 15 |- ( N < ( 4 + 1 ) <-> N < 5 )
4746a1i 11 . . . . . . . . . . . . . 14 |- ( N e. ( ZZ>= ` 2 ) -> ( N < ( 4 + 1 ) <-> N < 5 ) )
4841, 44, 473bitr3rd 299 . . . . . . . . . . . . 13 |- ( N e. ( ZZ>= ` 2 ) -> ( N < 5 <-> ( N < 4 \/ N = 4 ) ) )
49 3z 11410 . . . . . . . . . . . . . . . . 17 |- 3 e. ZZ
50 zleltp1 11428 . . . . . . . . . . . . . . . . 17 |- ( ( N e. ZZ /\ 3 e. ZZ ) -> ( N <_ 3 <-> N < ( 3 + 1 ) ) )
515, 49, 50sylancl 694 . . . . . . . . . . . . . . . 16 |- ( N e. ( ZZ>= ` 2 ) -> ( N <_ 3 <-> N < ( 3 + 1 ) ) )
52 3re 11094 . . . . . . . . . . . . . . . . . 18 |- 3 e. RR
5352a1i 11 . . . . . . . . . . . . . . . . 17 |- ( N e. ( ZZ>= ` 2 ) -> 3 e. RR )
541, 53leloed 10180 . . . . . . . . . . . . . . . 16 |- ( N e. ( ZZ>= ` 2 ) -> ( N <_ 3 <-> ( N < 3 \/ N = 3 ) ) )
55 3p1e4 11153 . . . . . . . . . . . . . . . . . 18 |- ( 3 + 1 ) = 4
5655breq2i 4661 . . . . . . . . . . . . . . . . 17 |- ( N < ( 3 + 1 ) <-> N < 4 )
5756a1i 11 . . . . . . . . . . . . . . . 16 |- ( N e. ( ZZ>= ` 2 ) -> ( N < ( 3 + 1 ) <-> N < 4 ) )
5851, 54, 573bitr3rd 299 . . . . . . . . . . . . . . 15 |- ( N e. ( ZZ>= ` 2 ) -> ( N < 4 <-> ( N < 3 \/ N = 3 ) ) )
59 eluz2 11693 . . . . . . . . . . . . . . . . 17 |- ( N e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ N e. ZZ /\ 2 <_ N ) )
60 2re 11090 . . . . . . . . . . . . . . . . . . . . . . 23 |- 2 e. RR
6160a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 |- ( N e. ZZ -> 2 e. RR )
62 zre 11381 . . . . . . . . . . . . . . . . . . . . . 22 |- ( N e. ZZ -> N e. RR )
6361, 62leloed 10180 . . . . . . . . . . . . . . . . . . . . 21 |- ( N e. ZZ -> ( 2 <_ N <-> ( 2 < N \/ 2 = N ) ) )
64 3m1e2 11137 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( 3 - 1 ) = 2
6564eqcomi 2631 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- 2 = ( 3 - 1 )
6665breq1i 4660 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( 2 < N <-> ( 3 - 1 ) < N )
67 zlem1lt 11429 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( 3 e. ZZ /\ N e. ZZ ) -> ( 3 <_ N <-> ( 3 - 1 ) < N ) )
6849, 67mpan 706 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( N e. ZZ -> ( 3 <_ N <-> ( 3 - 1 ) < N ) )
6968biimprd 238 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( N e. ZZ -> ( ( 3 - 1 ) < N -> 3 <_ N ) )
7066, 69syl5bi 232 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( N e. ZZ -> ( 2 < N -> 3 <_ N ) )
7152a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( N e. ZZ -> 3 e. RR )
7271, 62lenltd 10183 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( N e. ZZ -> ( 3 <_ N <-> -. N < 3 ) )
73 pm2.21 120 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( -. N < 3 -> ( N < 3 -> N = 2 ) )
7472, 73syl6bi 243 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( N e. ZZ -> ( 3 <_ N -> ( N < 3 -> N = 2 ) ) )
7570, 74syldc 48 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( 2 < N -> ( N e. ZZ -> ( N < 3 -> N = 2 ) ) )
76 eqcom 2629 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( 2 = N <-> N = 2 )
7776biimpi 206 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( 2 = N -> N = 2 )
78772a1d 26 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( 2 = N -> ( N e. ZZ -> ( N < 3 -> N = 2 ) ) )
7975, 78jaoi 394 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 2 < N \/ 2 = N ) -> ( N e. ZZ -> ( N < 3 -> N = 2 ) ) )
8079com12 32 . . . . . . . . . . . . . . . . . . . . 21 |- ( N e. ZZ -> ( ( 2 < N \/ 2 = N ) -> ( N < 3 -> N = 2 ) ) )
8163, 80sylbid 230 . . . . . . . . . . . . . . . . . . . 20 |- ( N e. ZZ -> ( 2 <_ N -> ( N < 3 -> N = 2 ) ) )
8281imp 445 . . . . . . . . . . . . . . . . . . 19 |- ( ( N e. ZZ /\ 2 <_ N ) -> ( N < 3 -> N = 2 ) )
83 2lt3 11195 . . . . . . . . . . . . . . . . . . . 20 |- 2 < 3
84 breq1 4656 . . . . . . . . . . . . . . . . . . . 20 |- ( N = 2 -> ( N < 3 <-> 2 < 3 ) )
8583, 84mpbiri 248 . . . . . . . . . . . . . . . . . . 19 |- ( N = 2 -> N < 3 )
8682, 85impbid1 215 . . . . . . . . . . . . . . . . . 18 |- ( ( N e. ZZ /\ 2 <_ N ) -> ( N < 3 <-> N = 2 ) )
87863adant1 1079 . . . . . . . . . . . . . . . . 17 |- ( ( 2 e. ZZ /\ N e. ZZ /\ 2 <_ N ) -> ( N < 3 <-> N = 2 ) )
8859, 87sylbi 207 . . . . . . . . . . . . . . . 16 |- ( N e. ( ZZ>= ` 2 ) -> ( N < 3 <-> N = 2 ) )
8988orbi1d 739 . . . . . . . . . . . . . . 15 |- ( N e. ( ZZ>= ` 2 ) -> ( ( N < 3 \/ N = 3 ) <-> ( N = 2 \/ N = 3 ) ) )
9058, 89bitrd 268 . . . . . . . . . . . . . 14 |- ( N e. ( ZZ>= ` 2 ) -> ( N < 4 <-> ( N = 2 \/ N = 3 ) ) )
9190orbi1d 739 . . . . . . . . . . . . 13 |- ( N e. ( ZZ>= ` 2 ) -> ( ( N < 4 \/ N = 4 ) <-> ( ( N = 2 \/ N = 3 ) \/ N = 4 ) ) )
9248, 91bitrd 268 . . . . . . . . . . . 12 |- ( N e. ( ZZ>= ` 2 ) -> ( N < 5 <-> ( ( N = 2 \/ N = 3 ) \/ N = 4 ) ) )
9392orbi1d 739 . . . . . . . . . . 11 |- ( N e. ( ZZ>= ` 2 ) -> ( ( N < 5 \/ N = 5 ) <-> ( ( ( N = 2 \/ N = 3 ) \/ N = 4 ) \/ N = 5 ) ) )
9438, 93bitrd 268 . . . . . . . . . 10 |- ( N e. ( ZZ>= ` 2 ) -> ( N < 6 <-> ( ( ( N = 2 \/ N = 3 ) \/ N = 4 ) \/ N = 5 ) ) )
9594orbi1d 739 . . . . . . . . 9 |- ( N e. ( ZZ>= ` 2 ) -> ( ( N < 6 \/ N = 6 ) <-> ( ( ( ( N = 2 \/ N = 3 ) \/ N = 4 ) \/ N = 5 ) \/ N = 6 ) ) )
9627, 95bitrd 268 . . . . . . . 8 |- ( N e. ( ZZ>= ` 2 ) -> ( N < 7 <-> ( ( ( ( N = 2 \/ N = 3 ) \/ N = 4 ) \/ N = 5 ) \/ N = 6 ) ) )
9796orbi1d 739 . . . . . . 7 |- ( N e. ( ZZ>= ` 2 ) -> ( ( N < 7 \/ N = 7 ) <-> ( ( ( ( ( N = 2 \/ N = 3 ) \/ N = 4 ) \/ N = 5 ) \/ N = 6 ) \/ N = 7 ) ) )
9816, 97bitrd 268 . . . . . 6 |- ( N e. ( ZZ>= ` 2 ) -> ( N < 8 <-> ( ( ( ( ( N = 2 \/ N = 3 ) \/ N = 4 ) \/ N = 5 ) \/ N = 6 ) \/ N = 7 ) ) )
9998orbi1d 739 . . . . 5 |- ( N e. ( ZZ>= ` 2 ) -> ( ( N < 8 \/ N = 8 ) <-> ( ( ( ( ( ( N = 2 \/ N = 3 ) \/ N = 4 ) \/ N = 5 ) \/ N = 6 ) \/ N = 7 ) \/ N = 8 ) ) )
10099biimpd 219 . . . 4 |- ( N e. ( ZZ>= ` 2 ) -> ( ( N < 8 \/ N = 8 ) -> ( ( ( ( ( ( N = 2 \/ N = 3 ) \/ N = 4 ) \/ N = 5 ) \/ N = 6 ) \/ N = 7 ) \/ N = 8 ) ) )
1014, 100sylbid 230 . . 3 |- ( N e. ( ZZ>= ` 2 ) -> ( N <_ 8 -> ( ( ( ( ( ( N = 2 \/ N = 3 ) \/ N = 4 ) \/ N = 5 ) \/ N = 6 ) \/ N = 7 ) \/ N = 8 ) ) )
102101imp 445 . 2 |- ( ( N e. ( ZZ>= ` 2 ) /\ N <_ 8 ) -> ( ( ( ( ( ( N = 2 \/ N = 3 ) \/ N = 4 ) \/ N = 5 ) \/ N = 6 ) \/ N = 7 ) \/ N = 8 ) )
103 2prm 15405 . . . . . . . . . 10 |- 2 e. Prime
104 eleq1 2689 . . . . . . . . . 10 |- ( N = 2 -> ( N e. Prime <-> 2 e. Prime ) )
105103, 104mpbiri 248 . . . . . . . . 9 |- ( N = 2 -> N e. Prime )
106 nnsum3primesprm 41678 . . . . . . . . 9 |- ( N e. Prime -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
107105, 106syl 17 . . . . . . . 8 |- ( 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 15406 . . . . . . . . . 10 |- 3 e. Prime
109 eleq1 2689 . . . . . . . . . 10 |- ( N = 3 -> ( N e. Prime <-> 3 e. Prime ) )
110108, 109mpbiri 248 . . . . . . . . 9 |- ( N = 3 -> N e. Prime )
111110, 106syl 17 . . . . . . . 8 |- ( N = 3 -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
112107, 111jaoi 394 . . . . . . 7 |- ( ( 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 41676 . . . . . . . 8 |- E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ 4 = sum_ k e. ( 1 ... d ) ( f ` k ) )
114 eqeq1 2626 . . . . . . . . . 10 |- ( N = 4 -> ( N = sum_ k e. ( 1 ... d ) ( f ` k ) <-> 4 = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
115114anbi2d 740 . . . . . . . . 9 |- ( N = 4 -> ( ( d <_ 3 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) <-> ( d <_ 3 /\ 4 = sum_ k e. ( 1 ... d ) ( f ` k ) ) ) )
1161152rexbidv 3057 . . . . . . . 8 |- ( 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 ) ) ) )
117113, 116mpbiri 248 . . . . . . 7 |- ( N = 4 -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
118112, 117jaoi 394 . . . . . 6 |- ( ( ( 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 15815 . . . . . . . 8 |- 5 e. Prime
120 eleq1 2689 . . . . . . . 8 |- ( N = 5 -> ( N e. Prime <-> 5 e. Prime ) )
121119, 120mpbiri 248 . . . . . . 7 |- ( N = 5 -> N e. Prime )
122121, 106syl 17 . . . . . 6 |- ( N = 5 -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
123118, 122jaoi 394 . . . . 5 |- ( ( ( ( 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 41659 . . . . . . 7 |- 6 e. GoldbachEven
125 eleq1 2689 . . . . . . 7 |- ( N = 6 -> ( N e. GoldbachEven <-> 6 e. GoldbachEven ) )
126124, 125mpbiri 248 . . . . . 6 |- ( N = 6 -> N e. GoldbachEven )
127 nnsum3primesgbe 41680 . . . . . 6 |- ( N e. GoldbachEven -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
128126, 127syl 17 . . . . 5 |- ( N = 6 -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
129123, 128jaoi 394 . . . 4 |- ( ( ( ( ( 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 15817 . . . . . 6 |- 7 e. Prime
131 eleq1 2689 . . . . . 6 |- ( N = 7 -> ( N e. Prime <-> 7 e. Prime ) )
132130, 131mpbiri 248 . . . . 5 |- ( N = 7 -> N e. Prime )
133132, 106syl 17 . . . 4 |- ( N = 7 -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
134129, 133jaoi 394 . . 3 |- ( ( ( ( ( ( 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 41661 . . . . 5 |- 8 e. GoldbachEven
136 eleq1 2689 . . . . 5 |- ( N = 8 -> ( N e. GoldbachEven <-> 8 e. GoldbachEven ) )
137135, 136mpbiri 248 . . . 4 |- ( N = 8 -> N e. GoldbachEven )
138137, 127syl 17 . . 3 |- ( N = 8 -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
139134, 138jaoi 394 . 2 |- ( ( ( ( ( ( ( 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 ) ) )
140102, 139syl 17 1 |- ( ( 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 ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   E.wrex 2913   class class class wbr 4653   ` cfv 5888  (class class class)co 6650   ^m cmap 7857   RRcr 9935   1c1 9937   + caddc 9939   < clt 10074   <_ cle 10075   - cmin 10266   NNcn 11020   2c2 11070   3c3 11071   4c4 11072   5c5 11073   6c6 11074   7c7 11075   8c8 11076   ZZcz 11377   ZZ>=cuz 11687   ...cfz 12326   sum_csu 14416   Primecprime 15385   GoldbachEven cgbe 41633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-oadd 7564  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-sup 8348  df-inf 8349  df-oi 8415  df-card 8765  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-z 11378  df-dec 11494  df-uz 11688  df-rp 11833  df-fz 12327  df-fzo 12466  df-seq 12802  df-exp 12861  df-hash 13118  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-clim 14219  df-sum 14417  df-dvds 14984  df-prm 15386  df-even 41539  df-odd 41540  df-gbe 41636
This theorem is referenced by:  nnsum4primesle9  41683  bgoldbnnsum3prm  41692
  Copyright terms: Public domain W3C validator