Metamath Proof Explorer

Theorem tgoldbachgtda

Description: Lemma for tgoldbachgtd . (Contributed by Thierry Arnoux, 15-Dec-2021)

Ref Expression
Hypotheses tgoldbachgtda.o 
|- O = { z e. ZZ | -. 2 || z }
tgoldbachgtda.n 
|- ( ph -> N e. O )
tgoldbachgtda.0 
|- ( ph -> ( ; 1 0 ^ ; 2 7 ) <_ N )
tgoldbachgtda.h 
|- ( ph -> H : NN --> ( 0 [,) +oo ) )
tgoldbachgtda.k 
|- ( ph -> K : NN --> ( 0 [,) +oo ) )
tgoldbachgtda.1 
|- ( ( ph /\ m e. NN ) -> ( K ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) )
tgoldbachgtda.2 
|- ( ( ph /\ m e. NN ) -> ( H ` m ) <_ ( 1 . _ 4 _ 1 4 ) )
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 )
Assertion tgoldbachgtda 
|- ( ph -> 0 < ( # ` ( ( O i^i Prime ) ( repr ` 3 ) N ) ) )

Proof

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 ) ) )