Metamath Proof Explorer

Theorem tgoldbachgtde

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

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 ssidd 
 |-  ( ph -> NN C_ NN )
14 10 12 13 reprfi2 
 |-  ( ph -> ( NN ( repr ` 3 ) N ) e. Fin )
15 diffi 
 |-  ( ( NN ( repr ` 3 ) N ) e. Fin -> ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) e. Fin )
16 14 15 syl 
 |-  ( ph -> ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) e. Fin )
17 difssd 
 |-  ( ph -> ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) C_ ( NN ( repr ` 3 ) N ) )
18 17 sselda 
 |-  ( ( ph /\ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ) -> n e. ( NN ( repr ` 3 ) N ) )
19 vmaf 
 |-  Lam : NN --> RR
20 19 a1i 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> Lam : NN --> RR )
21 ssidd 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> NN C_ NN )
22 10 nn0zd 
 |-  ( ph -> N e. ZZ )
23 22 adantr 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> N e. ZZ )
24 11 a1i 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> 3 e. NN0 )
25 simpr 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> n e. ( NN ( repr ` 3 ) N ) )
26 21 23 24 25 reprf 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> n : ( 0 ..^ 3 ) --> NN )
27 c0ex 
 |-  0 e. _V
28 27 tpid1 
 |-  0 e. { 0 , 1 , 2 }
29 fzo0to3tp 
 |-  ( 0 ..^ 3 ) = { 0 , 1 , 2 }
30 28 29 eleqtrri 
 |-  0 e. ( 0 ..^ 3 )
31 30 a1i 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> 0 e. ( 0 ..^ 3 ) )
32 26 31 ffvelcdmd 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ( n ` 0 ) e. NN )
33 20 32 ffvelcdmd 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ( Lam ` ( n ` 0 ) ) e. RR )
34 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
35 fss 
 |-  ( ( H : NN --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ RR ) -> H : NN --> RR )
36 4 34 35 sylancl 
 |-  ( ph -> H : NN --> RR )
37 36 adantr 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> H : NN --> RR )
38 37 32 ffvelcdmd 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ( H ` ( n ` 0 ) ) e. RR )
39 33 38 remulcld 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ( ( Lam ` ( n ` 0 ) ) x. ( H ` ( n ` 0 ) ) ) e. RR )
40 1eltp012 
 |-  1 e. { 0 , 1 , 2 }
41 40 29 eleqtrri 
 |-  1 e. ( 0 ..^ 3 )
42 41 a1i 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> 1 e. ( 0 ..^ 3 ) )
43 26 42 ffvelcdmd 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ( n ` 1 ) e. NN )
44 20 43 ffvelcdmd 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ( Lam ` ( n ` 1 ) ) e. RR )
45 fss 
 |-  ( ( K : NN --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ RR ) -> K : NN --> RR )
46 5 34 45 sylancl 
 |-  ( ph -> K : NN --> RR )
47 46 adantr 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> K : NN --> RR )
48 47 43 ffvelcdmd 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ( K ` ( n ` 1 ) ) e. RR )
49 44 48 remulcld 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ( ( Lam ` ( n ` 1 ) ) x. ( K ` ( n ` 1 ) ) ) e. RR )
50 2ex 
 |-  2 e. _V
51 50 tpid3 
 |-  2 e. { 0 , 1 , 2 }
52 51 29 eleqtrri 
 |-  2 e. ( 0 ..^ 3 )
53 52 a1i 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> 2 e. ( 0 ..^ 3 ) )
54 26 53 ffvelcdmd 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ( n ` 2 ) e. NN )
55 20 54 ffvelcdmd 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ( Lam ` ( n ` 2 ) ) e. RR )
56 47 54 ffvelcdmd 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ( K ` ( n ` 2 ) ) e. RR )
57 55 56 remulcld 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ( ( Lam ` ( n ` 2 ) ) x. ( K ` ( n ` 2 ) ) ) e. RR )
58 49 57 remulcld 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ( ( ( Lam ` ( n ` 1 ) ) x. ( K ` ( n ` 1 ) ) ) x. ( ( Lam ` ( n ` 2 ) ) x. ( K ` ( n ` 2 ) ) ) ) e. RR )
59 39 58 remulcld 
 |-  ( ( ph /\ n e. ( NN ( 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 ) ) ) ) ) e. RR )
60 18 59 syldan 
 |-  ( ( ph /\ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( 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 ) ) ) ) ) e. RR )
61 16 60 fsumrecl 
 |-  ( ph -> sum_ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( 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 ) ) ) ) ) e. RR )
62 0nn0 
 |-  0 e. NN0
63 qssre 
 |-  QQ C_ RR
64 4nn0 
 |-  4 e. NN0
65 2nn0 
 |-  2 e. NN0
66 nn0ssq 
 |-  NN0 C_ QQ
67 8nn0 
 |-  8 e. NN0
68 66 67 sselii 
 |-  8 e. QQ
69 64 68 dp2clq 
 |-  _ 4 8 e. QQ
70 65 69 dp2clq 
 |-  _ 2 _ 4 8 e. QQ
71 65 70 dp2clq 
 |-  _ 2 _ 2 _ 4 8 e. QQ
72 64 71 dp2clq 
 |-  _ 4 _ 2 _ 2 _ 4 8 e. QQ
73 62 72 dp2clq 
 |-  _ 0 _ 4 _ 2 _ 2 _ 4 8 e. QQ
74 62 73 dp2clq 
 |-  _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 e. QQ
75 62 74 dp2clq 
 |-  _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 e. QQ
76 63 75 sselii 
 |-  _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 e. RR
77 dpcl 
 |-  ( ( 0 e. NN0 /\ _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 e. RR ) -> ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) e. RR )
78 62 76 77 mp2an 
 |-  ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) e. RR
79 78 a1i 
 |-  ( ph -> ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) e. RR )
80 9 nnred 
 |-  ( ph -> N e. RR )
81 80 resqcld 
 |-  ( ph -> ( N ^ 2 ) e. RR )
82 79 81 remulcld 
 |-  ( ph -> ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( N ^ 2 ) ) e. RR )
83 14 59 fsumrecl 
 |-  ( ph -> sum_ n e. ( NN ( 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 ) ) ) ) ) e. RR )
84 7nn0 
 |-  7 e. NN0
85 11 69 dp2clq 
 |-  _ 3 _ 4 8 e. QQ
86 63 85 sselii 
 |-  _ 3 _ 4 8 e. RR
87 dpcl 
 |-  ( ( 7 e. NN0 /\ _ 3 _ 4 8 e. RR ) -> ( 7 . _ 3 _ 4 8 ) e. RR )
88 84 86 87 mp2an 
 |-  ( 7 . _ 3 _ 4 8 ) e. RR
89 88 a1i 
 |-  ( ph -> ( 7 . _ 3 _ 4 8 ) e. RR )
90 9 nnrpd 
 |-  ( ph -> N e. RR+ )
91 90 relogcld 
 |-  ( ph -> ( log ` N ) e. RR )
92 10 nn0ge0d 
 |-  ( ph -> 0 <_ N )
93 80 92 resqrtcld 
 |-  ( ph -> ( sqrt ` N ) e. RR )
94 90 sqrtgt0d 
 |-  ( ph -> 0 < ( sqrt ` N ) )
95 94 gt0ne0d 
 |-  ( ph -> ( sqrt ` N ) =/= 0 )
96 91 93 95 redivcld 
 |-  ( ph -> ( ( log ` N ) / ( sqrt ` N ) ) e. RR )
97 89 96 remulcld 
 |-  ( ph -> ( ( 7 . _ 3 _ 4 8 ) x. ( ( log ` N ) / ( sqrt ` N ) ) ) e. RR )
98 97 81 remulcld 
 |-  ( ph -> ( ( ( 7 . _ 3 _ 4 8 ) x. ( ( log ` N ) / ( sqrt ` N ) ) ) x. ( N ^ 2 ) ) e. RR )
99 1 9 3 4 5 6 7 hgt750leme 
 |-  ( ph -> sum_ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( 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 ) ) ) ) ) <_ ( ( ( 7 . _ 3 _ 4 8 ) x. ( ( log ` N ) / ( sqrt ` N ) ) ) x. ( N ^ 2 ) ) )
100 2z 
 |-  2 e. ZZ
101 100 a1i 
 |-  ( ph -> 2 e. ZZ )
102 90 101 rpexpcld 
 |-  ( ph -> ( N ^ 2 ) e. RR+ )
103 hgt750lem 
 |-  ( ( N e. NN0 /\ ( ; 1 0 ^ ; 2 7 ) <_ N ) -> ( ( 7 . _ 3 _ 4 8 ) x. ( ( log ` N ) / ( sqrt ` N ) ) ) < ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) )
104 10 3 103 syl2anc 
 |-  ( ph -> ( ( 7 . _ 3 _ 4 8 ) x. ( ( log ` N ) / ( sqrt ` N ) ) ) < ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) )
105 97 79 102 104 ltmul1dd 
 |-  ( ph -> ( ( ( 7 . _ 3 _ 4 8 ) x. ( ( log ` N ) / ( sqrt ` N ) ) ) x. ( N ^ 2 ) ) < ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( N ^ 2 ) ) )
106 61 98 82 99 105 lelttrd 
 |-  ( ph -> sum_ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( 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 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( N ^ 2 ) ) )
107 36 46 10 circlemethhgt 
 |-  ( ph -> sum_ n e. ( NN ( 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 ) ) ) ) ) = 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 )
108 8 107 breqtrrd 
 |-  ( ph -> ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( N ^ 2 ) ) <_ sum_ n e. ( NN ( 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 ) ) ) ) ) )
109 61 82 83 106 108 ltletrd 
 |-  ( ph -> sum_ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( 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. ( NN ( 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 ) ) ) ) ) )
110 61 83 posdifd 
 |-  ( ph -> ( sum_ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( 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. ( NN ( 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 < ( sum_ n e. ( NN ( 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. ( ( NN ( repr ` 3 ) N ) \ ( ( 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 ) ) ) ) ) ) ) )
111 109 110 mpbid 
 |-  ( ph -> 0 < ( sum_ n e. ( NN ( 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. ( ( NN ( repr ` 3 ) N ) \ ( ( 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 ) ) ) ) ) ) )
112 inss2 
 |-  ( O i^i Prime ) C_ Prime
113 prmssnn 
 |-  Prime C_ NN
114 112 113 sstri 
 |-  ( O i^i Prime ) C_ NN
115 114 a1i 
 |-  ( ph -> ( O i^i Prime ) C_ NN )
116 13 22 12 115 reprss 
 |-  ( ph -> ( ( O i^i Prime ) ( repr ` 3 ) N ) C_ ( NN ( repr ` 3 ) N ) )
117 14 116 ssfid 
 |-  ( ph -> ( ( O i^i Prime ) ( repr ` 3 ) N ) e. Fin )
118 116 sselda 
 |-  ( ( ph /\ n e. ( ( O i^i Prime ) ( repr ` 3 ) N ) ) -> n e. ( NN ( repr ` 3 ) N ) )
119 59 recnd 
 |-  ( ( ph /\ n e. ( NN ( 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 ) ) ) ) ) e. CC )
120 118 119 syldan 
 |-  ( ( ph /\ 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 ) ) ) ) ) e. CC )
121 117 120 fsumcl 
 |-  ( 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 ) ) ) ) ) e. CC )
122 61 recnd 
 |-  ( ph -> sum_ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( 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 ) ) ) ) ) e. CC )
123 disjdif 
 |-  ( ( ( O i^i Prime ) ( repr ` 3 ) N ) i^i ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ) = (/)
124 123 a1i 
 |-  ( ph -> ( ( ( O i^i Prime ) ( repr ` 3 ) N ) i^i ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ) = (/) )
125 undif 
 |-  ( ( ( O i^i Prime ) ( repr ` 3 ) N ) C_ ( NN ( repr ` 3 ) N ) <-> ( ( ( O i^i Prime ) ( repr ` 3 ) N ) u. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ) = ( NN ( repr ` 3 ) N ) )
126 116 125 sylib 
 |-  ( ph -> ( ( ( O i^i Prime ) ( repr ` 3 ) N ) u. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ) = ( NN ( repr ` 3 ) N ) )
127 126 eqcomd 
 |-  ( ph -> ( NN ( repr ` 3 ) N ) = ( ( ( O i^i Prime ) ( repr ` 3 ) N ) u. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ) )
128 124 127 14 119 fsumsplit 
 |-  ( ph -> sum_ n e. ( NN ( 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. ( ( 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. ( ( NN ( repr ` 3 ) N ) \ ( ( 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 ) ) ) ) ) ) )
129 121 122 128 mvrraddd 
 |-  ( ph -> ( sum_ n e. ( NN ( 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. ( ( NN ( repr ` 3 ) N ) \ ( ( 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. ( ( 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 ) ) ) ) ) )
130 111 129 breqtrd 
 |-  ( 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 ) ) ) ) ) )