Step |
Hyp |
Ref |
Expression |
1 |
|
nnsum3primes4 |
|- E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ 4 = sum_ k e. ( 1 ... d ) ( f ` k ) ) |
2 |
|
3lt4 |
|- 3 < 4 |
3 |
|
nnre |
|- ( d e. NN -> d e. RR ) |
4 |
|
3re |
|- 3 e. RR |
5 |
4
|
a1i |
|- ( d e. NN -> 3 e. RR ) |
6 |
|
4re |
|- 4 e. RR |
7 |
6
|
a1i |
|- ( d e. NN -> 4 e. RR ) |
8 |
|
leltletr |
|- ( ( d e. RR /\ 3 e. RR /\ 4 e. RR ) -> ( ( d <_ 3 /\ 3 < 4 ) -> d <_ 4 ) ) |
9 |
3 5 7 8
|
syl3anc |
|- ( d e. NN -> ( ( d <_ 3 /\ 3 < 4 ) -> d <_ 4 ) ) |
10 |
2 9
|
mpan2i |
|- ( d e. NN -> ( d <_ 3 -> d <_ 4 ) ) |
11 |
10
|
anim1d |
|- ( d e. NN -> ( ( d <_ 3 /\ 4 = sum_ k e. ( 1 ... d ) ( f ` k ) ) -> ( d <_ 4 /\ 4 = sum_ k e. ( 1 ... d ) ( f ` k ) ) ) ) |
12 |
11
|
reximdv |
|- ( d e. NN -> ( E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ 4 = sum_ k e. ( 1 ... d ) ( f ` k ) ) -> E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 4 /\ 4 = sum_ k e. ( 1 ... d ) ( f ` k ) ) ) ) |
13 |
12
|
reximia |
|- ( E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ 4 = sum_ k e. ( 1 ... d ) ( f ` k ) ) -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 4 /\ 4 = sum_ k e. ( 1 ... d ) ( f ` k ) ) ) |
14 |
1 13
|
ax-mp |
|- E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 4 /\ 4 = sum_ k e. ( 1 ... d ) ( f ` k ) ) |