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 1ex 
 |-  1 e. _V
41 40 tpid2 
 |-  1 e. { 0 , 1 , 2 }
42 41 29 eleqtrri 
 |-  1 e. ( 0 ..^ 3 )
43 42 a1i 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> 1 e. ( 0 ..^ 3 ) )
44 26 43 ffvelcdmd 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ( n ` 1 ) e. NN )
45 20 44 ffvelcdmd 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ( Lam ` ( n ` 1 ) ) e. RR )
46 fss 
 |-  ( ( K : NN --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ RR ) -> K : NN --> RR )
47 5 34 46 sylancl 
 |-  ( ph -> K : NN --> RR )
48 47 adantr 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> K : NN --> RR )
49 48 44 ffvelcdmd 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ( K ` ( n ` 1 ) ) e. RR )
50 45 49 remulcld 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ( ( Lam ` ( n ` 1 ) ) x. ( K ` ( n ` 1 ) ) ) e. RR )
51 2ex 
 |-  2 e. _V
52 51 tpid3 
 |-  2 e. { 0 , 1 , 2 }
53 52 29 eleqtrri 
 |-  2 e. ( 0 ..^ 3 )
54 53 a1i 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> 2 e. ( 0 ..^ 3 ) )
55 26 54 ffvelcdmd 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ( n ` 2 ) e. NN )
56 20 55 ffvelcdmd 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ( Lam ` ( n ` 2 ) ) e. RR )
57 48 55 ffvelcdmd 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ( K ` ( n ` 2 ) ) e. RR )
58 56 57 remulcld 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> ( ( Lam ` ( n ` 2 ) ) x. ( K ` ( n ` 2 ) ) ) e. RR )
59 50 58 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 )
60 39 59 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 )
61 18 60 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 )
62 16 61 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 )
63 0nn0 
 |-  0 e. NN0
64 qssre 
 |-  QQ C_ RR
65 4nn0 
 |-  4 e. NN0
66 2nn0 
 |-  2 e. NN0
67 nn0ssq 
 |-  NN0 C_ QQ
68 8nn0 
 |-  8 e. NN0
69 67 68 sselii 
 |-  8 e. QQ
70 65 69 dp2clq 
 |-  _ 4 8 e. QQ
71 66 70 dp2clq 
 |-  _ 2 _ 4 8 e. QQ
72 66 71 dp2clq 
 |-  _ 2 _ 2 _ 4 8 e. QQ
73 65 72 dp2clq 
 |-  _ 4 _ 2 _ 2 _ 4 8 e. QQ
74 63 73 dp2clq 
 |-  _ 0 _ 4 _ 2 _ 2 _ 4 8 e. QQ
75 63 74 dp2clq 
 |-  _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 e. QQ
76 63 75 dp2clq 
 |-  _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 e. QQ
77 64 76 sselii 
 |-  _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 e. RR
78 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 )
79 63 77 78 mp2an 
 |-  ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) e. RR
80 79 a1i 
 |-  ( ph -> ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) e. RR )
81 9 nnred 
 |-  ( ph -> N e. RR )
82 81 resqcld 
 |-  ( ph -> ( N ^ 2 ) e. RR )
83 80 82 remulcld 
 |-  ( ph -> ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( N ^ 2 ) ) e. RR )
84 14 60 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 )
85 7nn0 
 |-  7 e. NN0
86 11 70 dp2clq 
 |-  _ 3 _ 4 8 e. QQ
87 64 86 sselii 
 |-  _ 3 _ 4 8 e. RR
88 dpcl 
 |-  ( ( 7 e. NN0 /\ _ 3 _ 4 8 e. RR ) -> ( 7 . _ 3 _ 4 8 ) e. RR )
89 85 87 88 mp2an 
 |-  ( 7 . _ 3 _ 4 8 ) e. RR
90 89 a1i 
 |-  ( ph -> ( 7 . _ 3 _ 4 8 ) e. RR )
91 9 nnrpd 
 |-  ( ph -> N e. RR+ )
92 91 relogcld 
 |-  ( ph -> ( log ` N ) e. RR )
93 10 nn0ge0d 
 |-  ( ph -> 0 <_ N )
94 81 93 resqrtcld 
 |-  ( ph -> ( sqrt ` N ) e. RR )
95 91 sqrtgt0d 
 |-  ( ph -> 0 < ( sqrt ` N ) )
96 95 gt0ne0d 
 |-  ( ph -> ( sqrt ` N ) =/= 0 )
97 92 94 96 redivcld 
 |-  ( ph -> ( ( log ` N ) / ( sqrt ` N ) ) e. RR )
98 90 97 remulcld 
 |-  ( ph -> ( ( 7 . _ 3 _ 4 8 ) x. ( ( log ` N ) / ( sqrt ` N ) ) ) e. RR )
99 98 82 remulcld 
 |-  ( ph -> ( ( ( 7 . _ 3 _ 4 8 ) x. ( ( log ` N ) / ( sqrt ` N ) ) ) x. ( N ^ 2 ) ) e. RR )
100 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 ) ) )
101 2z 
 |-  2 e. ZZ
102 101 a1i 
 |-  ( ph -> 2 e. ZZ )
103 91 102 rpexpcld 
 |-  ( ph -> ( N ^ 2 ) e. RR+ )
104 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 ) )
105 10 3 104 syl2anc 
 |-  ( ph -> ( ( 7 . _ 3 _ 4 8 ) x. ( ( log ` N ) / ( sqrt ` N ) ) ) < ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) )
106 98 80 103 105 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 ) ) )
107 62 99 83 100 106 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 ) ) )
108 36 47 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 )
109 8 108 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 ) ) ) ) ) )
110 62 83 84 107 109 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 ) ) ) ) ) )
111 62 84 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 ) ) ) ) ) ) ) )
112 110 111 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 ) ) ) ) ) ) )
113 inss2 
 |-  ( O i^i Prime ) C_ Prime
114 prmssnn 
 |-  Prime C_ NN
115 113 114 sstri 
 |-  ( O i^i Prime ) C_ NN
116 115 a1i 
 |-  ( ph -> ( O i^i Prime ) C_ NN )
117 13 22 12 116 reprss 
 |-  ( ph -> ( ( O i^i Prime ) ( repr ` 3 ) N ) C_ ( NN ( repr ` 3 ) N ) )
118 14 117 ssfid 
 |-  ( ph -> ( ( O i^i Prime ) ( repr ` 3 ) N ) e. Fin )
119 117 sselda 
 |-  ( ( ph /\ n e. ( ( O i^i Prime ) ( repr ` 3 ) N ) ) -> n e. ( NN ( repr ` 3 ) N ) )
120 60 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 )
121 119 120 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 )
122 118 121 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 )
123 62 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 )
124 disjdif 
 |-  ( ( ( O i^i Prime ) ( repr ` 3 ) N ) i^i ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ) = (/)
125 124 a1i 
 |-  ( ph -> ( ( ( O i^i Prime ) ( repr ` 3 ) N ) i^i ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ) = (/) )
126 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 ) )
127 117 126 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 ) )
128 127 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 ) ) ) )
129 125 128 14 120 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 ) ) ) ) ) ) )
130 122 123 129 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 ) ) ) ) ) )
131 112 130 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 ) ) ) ) ) )