Step |
Hyp |
Ref |
Expression |
1 |
|
zre |
|- ( N e. ZZ -> N e. RR ) |
2 |
|
chtval |
|- ( N e. RR -> ( theta ` N ) = sum_ n e. ( ( 0 [,] N ) i^i Prime ) ( log ` n ) ) |
3 |
1 2
|
syl |
|- ( N e. ZZ -> ( theta ` N ) = sum_ n e. ( ( 0 [,] N ) i^i Prime ) ( log ` n ) ) |
4 |
|
nnz |
|- ( N e. NN -> N e. ZZ ) |
5 |
|
ppisval |
|- ( N e. RR -> ( ( 0 [,] N ) i^i Prime ) = ( ( 2 ... ( |_ ` N ) ) i^i Prime ) ) |
6 |
1 5
|
syl |
|- ( N e. ZZ -> ( ( 0 [,] N ) i^i Prime ) = ( ( 2 ... ( |_ ` N ) ) i^i Prime ) ) |
7 |
|
flid |
|- ( N e. ZZ -> ( |_ ` N ) = N ) |
8 |
7
|
oveq2d |
|- ( N e. ZZ -> ( 2 ... ( |_ ` N ) ) = ( 2 ... N ) ) |
9 |
8
|
ineq1d |
|- ( N e. ZZ -> ( ( 2 ... ( |_ ` N ) ) i^i Prime ) = ( ( 2 ... N ) i^i Prime ) ) |
10 |
6 9
|
eqtrd |
|- ( N e. ZZ -> ( ( 0 [,] N ) i^i Prime ) = ( ( 2 ... N ) i^i Prime ) ) |
11 |
4 10
|
syl |
|- ( N e. NN -> ( ( 0 [,] N ) i^i Prime ) = ( ( 2 ... N ) i^i Prime ) ) |
12 |
|
2nn |
|- 2 e. NN |
13 |
|
nnuz |
|- NN = ( ZZ>= ` 1 ) |
14 |
12 13
|
eleqtri |
|- 2 e. ( ZZ>= ` 1 ) |
15 |
|
fzss1 |
|- ( 2 e. ( ZZ>= ` 1 ) -> ( 2 ... N ) C_ ( 1 ... N ) ) |
16 |
14 15
|
ax-mp |
|- ( 2 ... N ) C_ ( 1 ... N ) |
17 |
|
ssdif0 |
|- ( ( 2 ... N ) C_ ( 1 ... N ) <-> ( ( 2 ... N ) \ ( 1 ... N ) ) = (/) ) |
18 |
16 17
|
mpbi |
|- ( ( 2 ... N ) \ ( 1 ... N ) ) = (/) |
19 |
18
|
ineq1i |
|- ( ( ( 2 ... N ) \ ( 1 ... N ) ) i^i Prime ) = ( (/) i^i Prime ) |
20 |
|
0in |
|- ( (/) i^i Prime ) = (/) |
21 |
19 20
|
eqtri |
|- ( ( ( 2 ... N ) \ ( 1 ... N ) ) i^i Prime ) = (/) |
22 |
21
|
a1i |
|- ( N e. NN -> ( ( ( 2 ... N ) \ ( 1 ... N ) ) i^i Prime ) = (/) ) |
23 |
13
|
eleq2i |
|- ( N e. NN <-> N e. ( ZZ>= ` 1 ) ) |
24 |
|
fzpred |
|- ( N e. ( ZZ>= ` 1 ) -> ( 1 ... N ) = ( { 1 } u. ( ( 1 + 1 ) ... N ) ) ) |
25 |
23 24
|
sylbi |
|- ( N e. NN -> ( 1 ... N ) = ( { 1 } u. ( ( 1 + 1 ) ... N ) ) ) |
26 |
25
|
eqcomd |
|- ( N e. NN -> ( { 1 } u. ( ( 1 + 1 ) ... N ) ) = ( 1 ... N ) ) |
27 |
|
1p1e2 |
|- ( 1 + 1 ) = 2 |
28 |
27
|
oveq1i |
|- ( ( 1 + 1 ) ... N ) = ( 2 ... N ) |
29 |
28
|
a1i |
|- ( N e. NN -> ( ( 1 + 1 ) ... N ) = ( 2 ... N ) ) |
30 |
26 29
|
difeq12d |
|- ( N e. NN -> ( ( { 1 } u. ( ( 1 + 1 ) ... N ) ) \ ( ( 1 + 1 ) ... N ) ) = ( ( 1 ... N ) \ ( 2 ... N ) ) ) |
31 |
|
difun2 |
|- ( ( { 1 } u. ( ( 1 + 1 ) ... N ) ) \ ( ( 1 + 1 ) ... N ) ) = ( { 1 } \ ( ( 1 + 1 ) ... N ) ) |
32 |
|
fzpreddisj |
|- ( N e. ( ZZ>= ` 1 ) -> ( { 1 } i^i ( ( 1 + 1 ) ... N ) ) = (/) ) |
33 |
23 32
|
sylbi |
|- ( N e. NN -> ( { 1 } i^i ( ( 1 + 1 ) ... N ) ) = (/) ) |
34 |
|
disjdif2 |
|- ( ( { 1 } i^i ( ( 1 + 1 ) ... N ) ) = (/) -> ( { 1 } \ ( ( 1 + 1 ) ... N ) ) = { 1 } ) |
35 |
33 34
|
syl |
|- ( N e. NN -> ( { 1 } \ ( ( 1 + 1 ) ... N ) ) = { 1 } ) |
36 |
31 35
|
syl5eq |
|- ( N e. NN -> ( ( { 1 } u. ( ( 1 + 1 ) ... N ) ) \ ( ( 1 + 1 ) ... N ) ) = { 1 } ) |
37 |
30 36
|
eqtr3d |
|- ( N e. NN -> ( ( 1 ... N ) \ ( 2 ... N ) ) = { 1 } ) |
38 |
37
|
ineq1d |
|- ( N e. NN -> ( ( ( 1 ... N ) \ ( 2 ... N ) ) i^i Prime ) = ( { 1 } i^i Prime ) ) |
39 |
|
incom |
|- ( Prime i^i { 1 } ) = ( { 1 } i^i Prime ) |
40 |
|
1nprm |
|- -. 1 e. Prime |
41 |
|
disjsn |
|- ( ( Prime i^i { 1 } ) = (/) <-> -. 1 e. Prime ) |
42 |
40 41
|
mpbir |
|- ( Prime i^i { 1 } ) = (/) |
43 |
39 42
|
eqtr3i |
|- ( { 1 } i^i Prime ) = (/) |
44 |
38 43
|
eqtrdi |
|- ( N e. NN -> ( ( ( 1 ... N ) \ ( 2 ... N ) ) i^i Prime ) = (/) ) |
45 |
|
difininv |
|- ( ( ( ( ( 2 ... N ) \ ( 1 ... N ) ) i^i Prime ) = (/) /\ ( ( ( 1 ... N ) \ ( 2 ... N ) ) i^i Prime ) = (/) ) -> ( ( 2 ... N ) i^i Prime ) = ( ( 1 ... N ) i^i Prime ) ) |
46 |
22 44 45
|
syl2anc |
|- ( N e. NN -> ( ( 2 ... N ) i^i Prime ) = ( ( 1 ... N ) i^i Prime ) ) |
47 |
11 46
|
eqtrd |
|- ( N e. NN -> ( ( 0 [,] N ) i^i Prime ) = ( ( 1 ... N ) i^i Prime ) ) |
48 |
47
|
adantl |
|- ( ( N e. ZZ /\ N e. NN ) -> ( ( 0 [,] N ) i^i Prime ) = ( ( 1 ... N ) i^i Prime ) ) |
49 |
|
znnnlt1 |
|- ( N e. ZZ -> ( -. N e. NN <-> N < 1 ) ) |
50 |
49
|
biimpa |
|- ( ( N e. ZZ /\ -. N e. NN ) -> N < 1 ) |
51 |
|
incom |
|- ( ( 0 [,] N ) i^i Prime ) = ( Prime i^i ( 0 [,] N ) ) |
52 |
|
isprm3 |
|- ( n e. Prime <-> ( n e. ( ZZ>= ` 2 ) /\ A. i e. ( 2 ... ( n - 1 ) ) -. i || n ) ) |
53 |
52
|
simplbi |
|- ( n e. Prime -> n e. ( ZZ>= ` 2 ) ) |
54 |
53
|
ssriv |
|- Prime C_ ( ZZ>= ` 2 ) |
55 |
12
|
nnzi |
|- 2 e. ZZ |
56 |
|
uzssico |
|- ( 2 e. ZZ -> ( ZZ>= ` 2 ) C_ ( 2 [,) +oo ) ) |
57 |
55 56
|
ax-mp |
|- ( ZZ>= ` 2 ) C_ ( 2 [,) +oo ) |
58 |
54 57
|
sstri |
|- Prime C_ ( 2 [,) +oo ) |
59 |
|
incom |
|- ( ( 0 [,] N ) i^i ( 2 [,) +oo ) ) = ( ( 2 [,) +oo ) i^i ( 0 [,] N ) ) |
60 |
|
0xr |
|- 0 e. RR* |
61 |
60
|
a1i |
|- ( ( N e. ZZ /\ N < 1 ) -> 0 e. RR* ) |
62 |
12
|
nnrei |
|- 2 e. RR |
63 |
62
|
rexri |
|- 2 e. RR* |
64 |
63
|
a1i |
|- ( ( N e. ZZ /\ N < 1 ) -> 2 e. RR* ) |
65 |
|
0le0 |
|- 0 <_ 0 |
66 |
65
|
a1i |
|- ( ( N e. ZZ /\ N < 1 ) -> 0 <_ 0 ) |
67 |
1
|
adantr |
|- ( ( N e. ZZ /\ N < 1 ) -> N e. RR ) |
68 |
|
1red |
|- ( ( N e. ZZ /\ N < 1 ) -> 1 e. RR ) |
69 |
62
|
a1i |
|- ( ( N e. ZZ /\ N < 1 ) -> 2 e. RR ) |
70 |
|
simpr |
|- ( ( N e. ZZ /\ N < 1 ) -> N < 1 ) |
71 |
|
1lt2 |
|- 1 < 2 |
72 |
71
|
a1i |
|- ( ( N e. ZZ /\ N < 1 ) -> 1 < 2 ) |
73 |
67 68 69 70 72
|
lttrd |
|- ( ( N e. ZZ /\ N < 1 ) -> N < 2 ) |
74 |
|
iccssico |
|- ( ( ( 0 e. RR* /\ 2 e. RR* ) /\ ( 0 <_ 0 /\ N < 2 ) ) -> ( 0 [,] N ) C_ ( 0 [,) 2 ) ) |
75 |
61 64 66 73 74
|
syl22anc |
|- ( ( N e. ZZ /\ N < 1 ) -> ( 0 [,] N ) C_ ( 0 [,) 2 ) ) |
76 |
|
pnfxr |
|- +oo e. RR* |
77 |
|
icodisj |
|- ( ( 0 e. RR* /\ 2 e. RR* /\ +oo e. RR* ) -> ( ( 0 [,) 2 ) i^i ( 2 [,) +oo ) ) = (/) ) |
78 |
60 63 76 77
|
mp3an |
|- ( ( 0 [,) 2 ) i^i ( 2 [,) +oo ) ) = (/) |
79 |
|
ssdisj |
|- ( ( ( 0 [,] N ) C_ ( 0 [,) 2 ) /\ ( ( 0 [,) 2 ) i^i ( 2 [,) +oo ) ) = (/) ) -> ( ( 0 [,] N ) i^i ( 2 [,) +oo ) ) = (/) ) |
80 |
75 78 79
|
sylancl |
|- ( ( N e. ZZ /\ N < 1 ) -> ( ( 0 [,] N ) i^i ( 2 [,) +oo ) ) = (/) ) |
81 |
59 80
|
eqtr3id |
|- ( ( N e. ZZ /\ N < 1 ) -> ( ( 2 [,) +oo ) i^i ( 0 [,] N ) ) = (/) ) |
82 |
|
ssdisj |
|- ( ( Prime C_ ( 2 [,) +oo ) /\ ( ( 2 [,) +oo ) i^i ( 0 [,] N ) ) = (/) ) -> ( Prime i^i ( 0 [,] N ) ) = (/) ) |
83 |
58 81 82
|
sylancr |
|- ( ( N e. ZZ /\ N < 1 ) -> ( Prime i^i ( 0 [,] N ) ) = (/) ) |
84 |
51 83
|
syl5eq |
|- ( ( N e. ZZ /\ N < 1 ) -> ( ( 0 [,] N ) i^i Prime ) = (/) ) |
85 |
|
1zzd |
|- ( ( N e. ZZ /\ N < 1 ) -> 1 e. ZZ ) |
86 |
|
simpl |
|- ( ( N e. ZZ /\ N < 1 ) -> N e. ZZ ) |
87 |
|
fzn |
|- ( ( 1 e. ZZ /\ N e. ZZ ) -> ( N < 1 <-> ( 1 ... N ) = (/) ) ) |
88 |
87
|
biimpa |
|- ( ( ( 1 e. ZZ /\ N e. ZZ ) /\ N < 1 ) -> ( 1 ... N ) = (/) ) |
89 |
85 86 70 88
|
syl21anc |
|- ( ( N e. ZZ /\ N < 1 ) -> ( 1 ... N ) = (/) ) |
90 |
89
|
ineq1d |
|- ( ( N e. ZZ /\ N < 1 ) -> ( ( 1 ... N ) i^i Prime ) = ( (/) i^i Prime ) ) |
91 |
90 20
|
eqtrdi |
|- ( ( N e. ZZ /\ N < 1 ) -> ( ( 1 ... N ) i^i Prime ) = (/) ) |
92 |
84 91
|
eqtr4d |
|- ( ( N e. ZZ /\ N < 1 ) -> ( ( 0 [,] N ) i^i Prime ) = ( ( 1 ... N ) i^i Prime ) ) |
93 |
50 92
|
syldan |
|- ( ( N e. ZZ /\ -. N e. NN ) -> ( ( 0 [,] N ) i^i Prime ) = ( ( 1 ... N ) i^i Prime ) ) |
94 |
|
exmidd |
|- ( N e. ZZ -> ( N e. NN \/ -. N e. NN ) ) |
95 |
48 93 94
|
mpjaodan |
|- ( N e. ZZ -> ( ( 0 [,] N ) i^i Prime ) = ( ( 1 ... N ) i^i Prime ) ) |
96 |
95
|
sumeq1d |
|- ( N e. ZZ -> sum_ n e. ( ( 0 [,] N ) i^i Prime ) ( log ` n ) = sum_ n e. ( ( 1 ... N ) i^i Prime ) ( log ` n ) ) |
97 |
3 96
|
eqtrd |
|- ( N e. ZZ -> ( theta ` N ) = sum_ n e. ( ( 1 ... N ) i^i Prime ) ( log ` n ) ) |