| Step |
Hyp |
Ref |
Expression |
| 1 |
|
tgoldbachgtda.o |
|- O = { z e. ZZ | -. 2 || z } |
| 2 |
|
tgoldbachgtda.n |
|- ( ph -> N e. O ) |
| 3 |
|
tgoldbachgtda.0 |
|- ( ph -> ( ; 1 0 ^ ; 2 7 ) <_ N ) |
| 4 |
|
tgoldbachgtda.h |
|- ( ph -> H : NN --> ( 0 [,) +oo ) ) |
| 5 |
|
tgoldbachgtda.k |
|- ( ph -> K : NN --> ( 0 [,) +oo ) ) |
| 6 |
|
tgoldbachgtda.1 |
|- ( ( ph /\ m e. NN ) -> ( K ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ) |
| 7 |
|
tgoldbachgtda.2 |
|- ( ( ph /\ m e. NN ) -> ( H ` m ) <_ ( 1 . _ 4 _ 1 4 ) ) |
| 8 |
|
tgoldbachgtda.3 |
|- ( ph -> ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( N ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. H ) vts N ) ` x ) x. ( ( ( ( Lam oF x. K ) vts N ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x ) |
| 9 |
1 2 3
|
tgoldbachgnn |
|- ( ph -> N e. NN ) |
| 10 |
9
|
nnnn0d |
|- ( ph -> N e. NN0 ) |
| 11 |
|
3nn0 |
|- 3 e. NN0 |
| 12 |
11
|
a1i |
|- ( ph -> 3 e. NN0 ) |
| 13 |
|
inss2 |
|- ( O i^i Prime ) C_ Prime |
| 14 |
|
prmssnn |
|- Prime C_ NN |
| 15 |
13 14
|
sstri |
|- ( O i^i Prime ) C_ NN |
| 16 |
15
|
a1i |
|- ( ph -> ( O i^i Prime ) C_ NN ) |
| 17 |
10 12 16
|
reprfi2 |
|- ( ph -> ( ( O i^i Prime ) ( repr ` 3 ) N ) e. Fin ) |
| 18 |
1 2 3 4 5 6 7 8
|
tgoldbachgtde |
|- ( ph -> 0 < sum_ n e. ( ( O i^i Prime ) ( repr ` 3 ) N ) ( ( ( Lam ` ( n ` 0 ) ) x. ( H ` ( n ` 0 ) ) ) x. ( ( ( Lam ` ( n ` 1 ) ) x. ( K ` ( n ` 1 ) ) ) x. ( ( Lam ` ( n ` 2 ) ) x. ( K ` ( n ` 2 ) ) ) ) ) ) |
| 19 |
18
|
gt0ne0d |
|- ( ph -> sum_ n e. ( ( O i^i Prime ) ( repr ` 3 ) N ) ( ( ( Lam ` ( n ` 0 ) ) x. ( H ` ( n ` 0 ) ) ) x. ( ( ( Lam ` ( n ` 1 ) ) x. ( K ` ( n ` 1 ) ) ) x. ( ( Lam ` ( n ` 2 ) ) x. ( K ` ( n ` 2 ) ) ) ) ) =/= 0 ) |
| 20 |
19
|
neneqd |
|- ( ph -> -. sum_ n e. ( ( O i^i Prime ) ( repr ` 3 ) N ) ( ( ( Lam ` ( n ` 0 ) ) x. ( H ` ( n ` 0 ) ) ) x. ( ( ( Lam ` ( n ` 1 ) ) x. ( K ` ( n ` 1 ) ) ) x. ( ( Lam ` ( n ` 2 ) ) x. ( K ` ( n ` 2 ) ) ) ) ) = 0 ) |
| 21 |
|
simpr |
|- ( ( ph /\ ( ( O i^i Prime ) ( repr ` 3 ) N ) = (/) ) -> ( ( O i^i Prime ) ( repr ` 3 ) N ) = (/) ) |
| 22 |
21
|
sumeq1d |
|- ( ( ph /\ ( ( O i^i Prime ) ( repr ` 3 ) N ) = (/) ) -> sum_ n e. ( ( O i^i Prime ) ( repr ` 3 ) N ) ( ( ( Lam ` ( n ` 0 ) ) x. ( H ` ( n ` 0 ) ) ) x. ( ( ( Lam ` ( n ` 1 ) ) x. ( K ` ( n ` 1 ) ) ) x. ( ( Lam ` ( n ` 2 ) ) x. ( K ` ( n ` 2 ) ) ) ) ) = sum_ n e. (/) ( ( ( Lam ` ( n ` 0 ) ) x. ( H ` ( n ` 0 ) ) ) x. ( ( ( Lam ` ( n ` 1 ) ) x. ( K ` ( n ` 1 ) ) ) x. ( ( Lam ` ( n ` 2 ) ) x. ( K ` ( n ` 2 ) ) ) ) ) ) |
| 23 |
|
sum0 |
|- sum_ n e. (/) ( ( ( Lam ` ( n ` 0 ) ) x. ( H ` ( n ` 0 ) ) ) x. ( ( ( Lam ` ( n ` 1 ) ) x. ( K ` ( n ` 1 ) ) ) x. ( ( Lam ` ( n ` 2 ) ) x. ( K ` ( n ` 2 ) ) ) ) ) = 0 |
| 24 |
22 23
|
eqtrdi |
|- ( ( ph /\ ( ( O i^i Prime ) ( repr ` 3 ) N ) = (/) ) -> sum_ n e. ( ( O i^i Prime ) ( repr ` 3 ) N ) ( ( ( Lam ` ( n ` 0 ) ) x. ( H ` ( n ` 0 ) ) ) x. ( ( ( Lam ` ( n ` 1 ) ) x. ( K ` ( n ` 1 ) ) ) x. ( ( Lam ` ( n ` 2 ) ) x. ( K ` ( n ` 2 ) ) ) ) ) = 0 ) |
| 25 |
20 24
|
mtand |
|- ( ph -> -. ( ( O i^i Prime ) ( repr ` 3 ) N ) = (/) ) |
| 26 |
25
|
neqned |
|- ( ph -> ( ( O i^i Prime ) ( repr ` 3 ) N ) =/= (/) ) |
| 27 |
|
hashnncl |
|- ( ( ( O i^i Prime ) ( repr ` 3 ) N ) e. Fin -> ( ( # ` ( ( O i^i Prime ) ( repr ` 3 ) N ) ) e. NN <-> ( ( O i^i Prime ) ( repr ` 3 ) N ) =/= (/) ) ) |
| 28 |
27
|
biimpar |
|- ( ( ( ( O i^i Prime ) ( repr ` 3 ) N ) e. Fin /\ ( ( O i^i Prime ) ( repr ` 3 ) N ) =/= (/) ) -> ( # ` ( ( O i^i Prime ) ( repr ` 3 ) N ) ) e. NN ) |
| 29 |
17 26 28
|
syl2anc |
|- ( ph -> ( # ` ( ( O i^i Prime ) ( repr ` 3 ) N ) ) e. NN ) |
| 30 |
|
nngt0 |
|- ( ( # ` ( ( O i^i Prime ) ( repr ` 3 ) N ) ) e. NN -> 0 < ( # ` ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ) |
| 31 |
29 30
|
syl |
|- ( ph -> 0 < ( # ` ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ) |