Metamath Proof Explorer

Theorem hgt750leme

Description: An upper bound on the contribution of the non-prime terms in the Statement 7.50 of Helfgott p. 69. (Contributed by Thierry Arnoux, 29-Dec-2021)

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

Proof

Step Hyp Ref Expression
1 hgt750leme.o 
 |-  O = { z e. ZZ | -. 2 || z }
2 hgt750leme.n 
 |-  ( ph -> N e. NN )
3 hgt750leme.0 
 |-  ( ph -> ( ; 1 0 ^ ; 2 7 ) <_ N )
4 hgt750leme.h 
 |-  ( ph -> H : NN --> ( 0 [,) +oo ) )
5 hgt750leme.k 
 |-  ( ph -> K : NN --> ( 0 [,) +oo ) )
6 hgt750leme.1 
 |-  ( ( ph /\ m e. NN ) -> ( K ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) )
7 hgt750leme.2 
 |-  ( ( ph /\ m e. NN ) -> ( H ` m ) <_ ( 1 . _ 4 _ 1 4 ) )
8 2 nnnn0d 
 |-  ( ph -> N e. NN0 )
9 3nn0 
 |-  3 e. NN0
10 9 a1i 
 |-  ( ph -> 3 e. NN0 )
11 ssidd 
 |-  ( ph -> NN C_ NN )
12 8 10 11 reprfi2 
 |-  ( ph -> ( NN ( repr ` 3 ) N ) e. Fin )
13 diffi 
 |-  ( ( NN ( repr ` 3 ) N ) e. Fin -> ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) e. Fin )
14 12 13 syl 
 |-  ( ph -> ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) e. Fin )
15 vmaf 
 |-  Lam : NN --> RR
16 15 a1i 
 |-  ( ( ph /\ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ) -> Lam : NN --> RR )
17 ssidd 
 |-  ( ( ph /\ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ) -> NN C_ NN )
18 2 nnzd 
 |-  ( ph -> N e. ZZ )
19 18 adantr 
 |-  ( ( ph /\ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ) -> N e. ZZ )
20 9 a1i 
 |-  ( ( ph /\ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ) -> 3 e. NN0 )
21 simpr 
 |-  ( ( ph /\ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ) -> n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) )
22 21 eldifad 
 |-  ( ( ph /\ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ) -> n e. ( NN ( repr ` 3 ) N ) )
23 17 19 20 22 reprf 
 |-  ( ( ph /\ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ) -> n : ( 0 ..^ 3 ) --> NN )
24 c0ex 
 |-  0 e. _V
25 24 tpid1 
 |-  0 e. { 0 , 1 , 2 }
26 fzo0to3tp 
 |-  ( 0 ..^ 3 ) = { 0 , 1 , 2 }
27 25 26 eleqtrri 
 |-  0 e. ( 0 ..^ 3 )
28 27 a1i 
 |-  ( ( ph /\ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ) -> 0 e. ( 0 ..^ 3 ) )
29 23 28 ffvelcdmd 
 |-  ( ( ph /\ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ) -> ( n ` 0 ) e. NN )
30 16 29 ffvelcdmd 
 |-  ( ( ph /\ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ) -> ( Lam ` ( n ` 0 ) ) e. RR )
31 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
32 4 adantr 
 |-  ( ( ph /\ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ) -> H : NN --> ( 0 [,) +oo ) )
33 32 29 ffvelcdmd 
 |-  ( ( ph /\ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ) -> ( H ` ( n ` 0 ) ) e. ( 0 [,) +oo ) )
34 31 33 sselid 
 |-  ( ( ph /\ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ) -> ( H ` ( n ` 0 ) ) e. RR )
35 30 34 remulcld 
 |-  ( ( ph /\ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ) -> ( ( Lam ` ( n ` 0 ) ) x. ( H ` ( n ` 0 ) ) ) e. RR )
36 1eltp012 
 |-  1 e. { 0 , 1 , 2 }
37 36 26 eleqtrri 
 |-  1 e. ( 0 ..^ 3 )
38 37 a1i 
 |-  ( ( ph /\ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ) -> 1 e. ( 0 ..^ 3 ) )
39 23 38 ffvelcdmd 
 |-  ( ( ph /\ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ) -> ( n ` 1 ) e. NN )
40 16 39 ffvelcdmd 
 |-  ( ( ph /\ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ) -> ( Lam ` ( n ` 1 ) ) e. RR )
41 5 adantr 
 |-  ( ( ph /\ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ) -> K : NN --> ( 0 [,) +oo ) )
42 41 39 ffvelcdmd 
 |-  ( ( ph /\ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ) -> ( K ` ( n ` 1 ) ) e. ( 0 [,) +oo ) )
43 31 42 sselid 
 |-  ( ( ph /\ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ) -> ( K ` ( n ` 1 ) ) e. RR )
44 40 43 remulcld 
 |-  ( ( ph /\ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ) -> ( ( Lam ` ( n ` 1 ) ) x. ( K ` ( n ` 1 ) ) ) e. RR )
45 2ex 
 |-  2 e. _V
46 45 tpid3 
 |-  2 e. { 0 , 1 , 2 }
47 46 26 eleqtrri 
 |-  2 e. ( 0 ..^ 3 )
48 47 a1i 
 |-  ( ( ph /\ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ) -> 2 e. ( 0 ..^ 3 ) )
49 23 48 ffvelcdmd 
 |-  ( ( ph /\ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ) -> ( n ` 2 ) e. NN )
50 16 49 ffvelcdmd 
 |-  ( ( ph /\ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ) -> ( Lam ` ( n ` 2 ) ) e. RR )
51 41 49 ffvelcdmd 
 |-  ( ( ph /\ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ) -> ( K ` ( n ` 2 ) ) e. ( 0 [,) +oo ) )
52 31 51 sselid 
 |-  ( ( ph /\ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ) -> ( K ` ( n ` 2 ) ) e. RR )
53 50 52 remulcld 
 |-  ( ( ph /\ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ) -> ( ( Lam ` ( n ` 2 ) ) x. ( K ` ( n ` 2 ) ) ) e. RR )
54 44 53 remulcld 
 |-  ( ( ph /\ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ) -> ( ( ( Lam ` ( n ` 1 ) ) x. ( K ` ( n ` 1 ) ) ) x. ( ( Lam ` ( n ` 2 ) ) x. ( K ` ( n ` 2 ) ) ) ) e. RR )
55 35 54 remulcld 
 |-  ( ( 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 )
56 14 55 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 )
57 3re 
 |-  3 e. RR
58 57 a1i 
 |-  ( ph -> 3 e. RR )
59 1nn0 
 |-  1 e. NN0
60 0nn0 
 |-  0 e. NN0
61 7nn0 
 |-  7 e. NN0
62 9nn0 
 |-  9 e. NN0
63 5nn0 
 |-  5 e. NN0
64 5nn 
 |-  5 e. NN
65 nnrp 
 |-  ( 5 e. NN -> 5 e. RR+ )
66 64 65 ax-mp 
 |-  5 e. RR+
67 63 66 rpdp2cl 
 |-  _ 5 5 e. RR+
68 62 67 rpdp2cl 
 |-  _ 9 _ 5 5 e. RR+
69 62 68 rpdp2cl 
 |-  _ 9 _ 9 _ 5 5 e. RR+
70 61 69 rpdp2cl 
 |-  _ 7 _ 9 _ 9 _ 5 5 e. RR+
71 60 70 rpdp2cl 
 |-  _ 0 _ 7 _ 9 _ 9 _ 5 5 e. RR+
72 59 71 rpdpcl 
 |-  ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) e. RR+
73 72 a1i 
 |-  ( ph -> ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) e. RR+ )
74 73 rpred 
 |-  ( ph -> ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) e. RR )
75 74 resqcld 
 |-  ( ph -> ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) e. RR )
76 4nn0 
 |-  4 e. NN0
77 4nn 
 |-  4 e. NN
78 nnrp 
 |-  ( 4 e. NN -> 4 e. RR+ )
79 77 78 ax-mp 
 |-  4 e. RR+
80 59 79 rpdp2cl 
 |-  _ 1 4 e. RR+
81 76 80 rpdp2cl 
 |-  _ 4 _ 1 4 e. RR+
82 59 81 rpdpcl 
 |-  ( 1 . _ 4 _ 1 4 ) e. RR+
83 82 a1i 
 |-  ( ph -> ( 1 . _ 4 _ 1 4 ) e. RR+ )
84 83 rpred 
 |-  ( ph -> ( 1 . _ 4 _ 1 4 ) e. RR )
85 75 84 remulcld 
 |-  ( ph -> ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) e. RR )
86 fveq1 
 |-  ( d = c -> ( d ` 0 ) = ( c ` 0 ) )
87 86 eleq1d 
 |-  ( d = c -> ( ( d ` 0 ) e. ( O i^i Prime ) <-> ( c ` 0 ) e. ( O i^i Prime ) ) )
88 87 notbid 
 |-  ( d = c -> ( -. ( d ` 0 ) e. ( O i^i Prime ) <-> -. ( c ` 0 ) e. ( O i^i Prime ) ) )
89 88 cbvrabv 
 |-  { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } = { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) }
90 89 ssrab3 
 |-  { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } C_ ( NN ( repr ` 3 ) N )
91 ssfi 
 |-  ( ( ( NN ( repr ` 3 ) N ) e. Fin /\ { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } C_ ( NN ( repr ` 3 ) N ) ) -> { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } e. Fin )
92 12 90 91 sylancl 
 |-  ( ph -> { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } e. Fin )
93 15 a1i 
 |-  ( ( ph /\ n e. { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } ) -> Lam : NN --> RR )
94 ssidd 
 |-  ( ( ph /\ n e. { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } ) -> NN C_ NN )
95 18 adantr 
 |-  ( ( ph /\ n e. { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } ) -> N e. ZZ )
96 9 a1i 
 |-  ( ( ph /\ n e. { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } ) -> 3 e. NN0 )
97 90 a1i 
 |-  ( ph -> { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } C_ ( NN ( repr ` 3 ) N ) )
98 97 sselda 
 |-  ( ( ph /\ n e. { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } ) -> n e. ( NN ( repr ` 3 ) N ) )
99 94 95 96 98 reprf 
 |-  ( ( ph /\ n e. { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } ) -> n : ( 0 ..^ 3 ) --> NN )
100 27 a1i 
 |-  ( ( ph /\ n e. { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } ) -> 0 e. ( 0 ..^ 3 ) )
101 99 100 ffvelcdmd 
 |-  ( ( ph /\ n e. { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } ) -> ( n ` 0 ) e. NN )
102 93 101 ffvelcdmd 
 |-  ( ( ph /\ n e. { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } ) -> ( Lam ` ( n ` 0 ) ) e. RR )
103 37 a1i 
 |-  ( ( ph /\ n e. { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } ) -> 1 e. ( 0 ..^ 3 ) )
104 99 103 ffvelcdmd 
 |-  ( ( ph /\ n e. { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } ) -> ( n ` 1 ) e. NN )
105 93 104 ffvelcdmd 
 |-  ( ( ph /\ n e. { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } ) -> ( Lam ` ( n ` 1 ) ) e. RR )
106 47 a1i 
 |-  ( ( ph /\ n e. { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } ) -> 2 e. ( 0 ..^ 3 ) )
107 99 106 ffvelcdmd 
 |-  ( ( ph /\ n e. { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } ) -> ( n ` 2 ) e. NN )
108 93 107 ffvelcdmd 
 |-  ( ( ph /\ n e. { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } ) -> ( Lam ` ( n ` 2 ) ) e. RR )
109 105 108 remulcld 
 |-  ( ( ph /\ n e. { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } ) -> ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) e. RR )
110 102 109 remulcld 
 |-  ( ( ph /\ n e. { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } ) -> ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) e. RR )
111 92 110 fsumrecl 
 |-  ( ph -> sum_ n e. { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) e. RR )
112 85 111 remulcld 
 |-  ( ph -> ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. sum_ n e. { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) e. RR )
113 58 112 remulcld 
 |-  ( ph -> ( 3 x. ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. sum_ n e. { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) ) e. RR )
114 4re 
 |-  4 e. RR
115 8re 
 |-  8 e. RR
116 114 115 pm3.2i 
 |-  ( 4 e. RR /\ 8 e. RR )
117 dp2cl 
 |-  ( ( 4 e. RR /\ 8 e. RR ) -> _ 4 8 e. RR )
118 116 117 ax-mp 
 |-  _ 4 8 e. RR
119 57 118 pm3.2i 
 |-  ( 3 e. RR /\ _ 4 8 e. RR )
120 dp2cl 
 |-  ( ( 3 e. RR /\ _ 4 8 e. RR ) -> _ 3 _ 4 8 e. RR )
121 119 120 ax-mp 
 |-  _ 3 _ 4 8 e. RR
122 dpcl 
 |-  ( ( 7 e. NN0 /\ _ 3 _ 4 8 e. RR ) -> ( 7 . _ 3 _ 4 8 ) e. RR )
123 61 121 122 mp2an 
 |-  ( 7 . _ 3 _ 4 8 ) e. RR
124 123 a1i 
 |-  ( ph -> ( 7 . _ 3 _ 4 8 ) e. RR )
125 2 nnrpd 
 |-  ( ph -> N e. RR+ )
126 125 relogcld 
 |-  ( ph -> ( log ` N ) e. RR )
127 2 nnred 
 |-  ( ph -> N e. RR )
128 125 rpge0d 
 |-  ( ph -> 0 <_ N )
129 127 128 resqrtcld 
 |-  ( ph -> ( sqrt ` N ) e. RR )
130 125 rpsqrtcld 
 |-  ( ph -> ( sqrt ` N ) e. RR+ )
131 130 rpne0d 
 |-  ( ph -> ( sqrt ` N ) =/= 0 )
132 126 129 131 redivcld 
 |-  ( ph -> ( ( log ` N ) / ( sqrt ` N ) ) e. RR )
133 124 132 remulcld 
 |-  ( ph -> ( ( 7 . _ 3 _ 4 8 ) x. ( ( log ` N ) / ( sqrt ` N ) ) ) e. RR )
134 127 resqcld 
 |-  ( ph -> ( N ^ 2 ) e. RR )
135 133 134 remulcld 
 |-  ( ph -> ( ( ( 7 . _ 3 _ 4 8 ) x. ( ( log ` N ) / ( sqrt ` N ) ) ) x. ( N ^ 2 ) ) e. RR )
136 0re 
 |-  0 e. RR
137 7re 
 |-  7 e. RR
138 9re 
 |-  9 e. RR
139 5re 
 |-  5 e. RR
140 139 139 pm3.2i 
 |-  ( 5 e. RR /\ 5 e. RR )
141 dp2cl 
 |-  ( ( 5 e. RR /\ 5 e. RR ) -> _ 5 5 e. RR )
142 140 141 ax-mp 
 |-  _ 5 5 e. RR
143 138 142 pm3.2i 
 |-  ( 9 e. RR /\ _ 5 5 e. RR )
144 dp2cl 
 |-  ( ( 9 e. RR /\ _ 5 5 e. RR ) -> _ 9 _ 5 5 e. RR )
145 143 144 ax-mp 
 |-  _ 9 _ 5 5 e. RR
146 138 145 pm3.2i 
 |-  ( 9 e. RR /\ _ 9 _ 5 5 e. RR )
147 dp2cl 
 |-  ( ( 9 e. RR /\ _ 9 _ 5 5 e. RR ) -> _ 9 _ 9 _ 5 5 e. RR )
148 146 147 ax-mp 
 |-  _ 9 _ 9 _ 5 5 e. RR
149 137 148 pm3.2i 
 |-  ( 7 e. RR /\ _ 9 _ 9 _ 5 5 e. RR )
150 dp2cl 
 |-  ( ( 7 e. RR /\ _ 9 _ 9 _ 5 5 e. RR ) -> _ 7 _ 9 _ 9 _ 5 5 e. RR )
151 149 150 ax-mp 
 |-  _ 7 _ 9 _ 9 _ 5 5 e. RR
152 136 151 pm3.2i 
 |-  ( 0 e. RR /\ _ 7 _ 9 _ 9 _ 5 5 e. RR )
153 dp2cl 
 |-  ( ( 0 e. RR /\ _ 7 _ 9 _ 9 _ 5 5 e. RR ) -> _ 0 _ 7 _ 9 _ 9 _ 5 5 e. RR )
154 152 153 ax-mp 
 |-  _ 0 _ 7 _ 9 _ 9 _ 5 5 e. RR
155 dpcl 
 |-  ( ( 1 e. NN0 /\ _ 0 _ 7 _ 9 _ 9 _ 5 5 e. RR ) -> ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) e. RR )
156 59 154 155 mp2an 
 |-  ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) e. RR
157 156 a1i 
 |-  ( ph -> ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) e. RR )
158 157 resqcld 
 |-  ( ph -> ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) e. RR )
159 1re 
 |-  1 e. RR
160 159 114 pm3.2i 
 |-  ( 1 e. RR /\ 4 e. RR )
161 dp2cl 
 |-  ( ( 1 e. RR /\ 4 e. RR ) -> _ 1 4 e. RR )
162 160 161 ax-mp 
 |-  _ 1 4 e. RR
163 114 162 pm3.2i 
 |-  ( 4 e. RR /\ _ 1 4 e. RR )
164 dp2cl 
 |-  ( ( 4 e. RR /\ _ 1 4 e. RR ) -> _ 4 _ 1 4 e. RR )
165 163 164 ax-mp 
 |-  _ 4 _ 1 4 e. RR
166 dpcl 
 |-  ( ( 1 e. NN0 /\ _ 4 _ 1 4 e. RR ) -> ( 1 . _ 4 _ 1 4 ) e. RR )
167 59 165 166 mp2an 
 |-  ( 1 . _ 4 _ 1 4 ) e. RR
168 167 a1i 
 |-  ( ph -> ( 1 . _ 4 _ 1 4 ) e. RR )
169 158 168 remulcld 
 |-  ( ph -> ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) e. RR )
170 40 50 remulcld 
 |-  ( ( ph /\ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ) -> ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) e. RR )
171 30 170 remulcld 
 |-  ( ( ph /\ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ) -> ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) e. RR )
172 14 171 fsumrecl 
 |-  ( ph -> sum_ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) e. RR )
173 169 172 remulcld 
 |-  ( ph -> ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. sum_ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) e. RR )
174 58 111 remulcld 
 |-  ( ph -> ( 3 x. sum_ n e. { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) e. RR )
175 169 174 remulcld 
 |-  ( ph -> ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( 3 x. sum_ n e. { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) ) e. RR )
176 14 157 168 4 5 29 39 49 6 7 hgt750lemf 
 |-  ( 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 ) ) ) ) ) <_ ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. sum_ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) )
177 2re 
 |-  2 e. RR
178 177 a1i 
 |-  ( ph -> 2 e. RR )
179 10nn0 
 |-  ; 1 0 e. NN0
180 2nn0 
 |-  2 e. NN0
181 180 61 deccl 
 |-  ; 2 7 e. NN0
182 179 181 nn0expcli 
 |-  ( ; 1 0 ^ ; 2 7 ) e. NN0
183 182 nn0rei 
 |-  ( ; 1 0 ^ ; 2 7 ) e. RR
184 183 a1i 
 |-  ( ph -> ( ; 1 0 ^ ; 2 7 ) e. RR )
185 179 numexp1 
 |-  ( ; 1 0 ^ 1 ) = ; 1 0
186 179 nn0rei 
 |-  ; 1 0 e. RR
187 185 186 eqeltri 
 |-  ( ; 1 0 ^ 1 ) e. RR
188 187 a1i 
 |-  ( ph -> ( ; 1 0 ^ 1 ) e. RR )
189 1nn 
 |-  1 e. NN
190 2lt9 
 |-  2 < 9
191 177 138 190 ltleii 
 |-  2 <_ 9
192 189 60 180 191 declei 
 |-  2 <_ ; 1 0
193 192 185 breqtrri 
 |-  2 <_ ( ; 1 0 ^ 1 )
194 193 a1i 
 |-  ( ph -> 2 <_ ( ; 1 0 ^ 1 ) )
195 1z 
 |-  1 e. ZZ
196 181 nn0zi 
 |-  ; 2 7 e. ZZ
197 186 195 196 3pm3.2i 
 |-  ( ; 1 0 e. RR /\ 1 e. ZZ /\ ; 2 7 e. ZZ )
198 1lt10 
 |-  1 < ; 1 0
199 197 198 pm3.2i 
 |-  ( ( ; 1 0 e. RR /\ 1 e. ZZ /\ ; 2 7 e. ZZ ) /\ 1 < ; 1 0 )
200 2nn 
 |-  2 e. NN
201 1lt9 
 |-  1 < 9
202 159 138 201 ltleii 
 |-  1 <_ 9
203 200 61 59 202 declei 
 |-  1 <_ ; 2 7
204 leexp2 
 |-  ( ( ( ; 1 0 e. RR /\ 1 e. ZZ /\ ; 2 7 e. ZZ ) /\ 1 < ; 1 0 ) -> ( 1 <_ ; 2 7 <-> ( ; 1 0 ^ 1 ) <_ ( ; 1 0 ^ ; 2 7 ) ) )
205 204 biimpa 
 |-  ( ( ( ( ; 1 0 e. RR /\ 1 e. ZZ /\ ; 2 7 e. ZZ ) /\ 1 < ; 1 0 ) /\ 1 <_ ; 2 7 ) -> ( ; 1 0 ^ 1 ) <_ ( ; 1 0 ^ ; 2 7 ) )
206 199 203 205 mp2an 
 |-  ( ; 1 0 ^ 1 ) <_ ( ; 1 0 ^ ; 2 7 )
207 206 a1i 
 |-  ( ph -> ( ; 1 0 ^ 1 ) <_ ( ; 1 0 ^ ; 2 7 ) )
208 178 188 184 194 207 letrd 
 |-  ( ph -> 2 <_ ( ; 1 0 ^ ; 2 7 ) )
209 178 184 127 208 3 letrd 
 |-  ( ph -> 2 <_ N )
210 eqid 
 |-  ( e e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } |-> ( e o. if ( a = 0 , ( _I |` ( 0 ..^ 3 ) ) , ( ( pmTrsp ` ( 0 ..^ 3 ) ) ` { a , 0 } ) ) ) ) = ( e e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } |-> ( e o. if ( a = 0 , ( _I |` ( 0 ..^ 3 ) ) , ( ( pmTrsp ` ( 0 ..^ 3 ) ) ` { a , 0 } ) ) ) )
211 1 2 209 89 210 hgt750lema 
 |-  ( ph -> sum_ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) <_ ( 3 x. sum_ n e. { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) )
212 2z 
 |-  2 e. ZZ
213 212 a1i 
 |-  ( ph -> 2 e. ZZ )
214 73 213 rpexpcld 
 |-  ( ph -> ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) e. RR+ )
215 214 83 rpmulcld 
 |-  ( ph -> ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) e. RR+ )
216 172 174 215 lemul2d 
 |-  ( ph -> ( sum_ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) <_ ( 3 x. sum_ n e. { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) <-> ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. sum_ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) <_ ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( 3 x. sum_ n e. { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) ) ) )
217 211 216 mpbid 
 |-  ( ph -> ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. sum_ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) <_ ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( 3 x. sum_ n e. { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) ) )
218 56 173 175 176 217 letrd 
 |-  ( 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 ) ) ) ) ) <_ ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( 3 x. sum_ n e. { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) ) )
219 157 recnd 
 |-  ( ph -> ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) e. CC )
220 219 sqcld 
 |-  ( ph -> ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) e. CC )
221 168 recnd 
 |-  ( ph -> ( 1 . _ 4 _ 1 4 ) e. CC )
222 220 221 mulcld 
 |-  ( ph -> ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) e. CC )
223 3cn 
 |-  3 e. CC
224 223 a1i 
 |-  ( ph -> 3 e. CC )
225 111 recnd 
 |-  ( ph -> sum_ n e. { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) e. CC )
226 222 224 225 mul12d 
 |-  ( ph -> ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( 3 x. sum_ n e. { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) ) = ( 3 x. ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. sum_ n e. { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) ) )
227 218 226 breqtrd 
 |-  ( 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 ) ) ) ) ) <_ ( 3 x. ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. sum_ n e. { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) ) )
228 fzfi 
 |-  ( 1 ... N ) e. Fin
229 diffi 
 |-  ( ( 1 ... N ) e. Fin -> ( ( 1 ... N ) \ Prime ) e. Fin )
230 228 229 ax-mp 
 |-  ( ( 1 ... N ) \ Prime ) e. Fin
231 snfi 
 |-  { 2 } e. Fin
232 unfi 
 |-  ( ( ( ( 1 ... N ) \ Prime ) e. Fin /\ { 2 } e. Fin ) -> ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) e. Fin )
233 230 231 232 mp2an 
 |-  ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) e. Fin
234 233 a1i 
 |-  ( ph -> ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) e. Fin )
235 15 a1i 
 |-  ( ( ph /\ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ) -> Lam : NN --> RR )
236 fz1ssnn 
 |-  ( 1 ... N ) C_ NN
237 236 a1i 
 |-  ( ph -> ( 1 ... N ) C_ NN )
238 237 ssdifssd 
 |-  ( ph -> ( ( 1 ... N ) \ Prime ) C_ NN )
239 200 a1i 
 |-  ( ph -> 2 e. NN )
240 239 snssd 
 |-  ( ph -> { 2 } C_ NN )
241 238 240 unssd 
 |-  ( ph -> ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) C_ NN )
242 241 sselda 
 |-  ( ( ph /\ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ) -> i e. NN )
243 235 242 ffvelcdmd 
 |-  ( ( ph /\ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ) -> ( Lam ` i ) e. RR )
244 234 243 fsumrecl 
 |-  ( ph -> sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( Lam ` i ) e. RR )
245 chpvalz 
 |-  ( N e. ZZ -> ( psi ` N ) = sum_ j e. ( 1 ... N ) ( Lam ` j ) )
246 18 245 syl 
 |-  ( ph -> ( psi ` N ) = sum_ j e. ( 1 ... N ) ( Lam ` j ) )
247 chpf 
 |-  psi : RR --> RR
248 247 a1i 
 |-  ( ph -> psi : RR --> RR )
249 248 127 ffvelcdmd 
 |-  ( ph -> ( psi ` N ) e. RR )
250 246 249 eqeltrrd 
 |-  ( ph -> sum_ j e. ( 1 ... N ) ( Lam ` j ) e. RR )
251 244 250 remulcld 
 |-  ( ph -> ( sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( Lam ` i ) x. sum_ j e. ( 1 ... N ) ( Lam ` j ) ) e. RR )
252 126 251 remulcld 
 |-  ( ph -> ( ( log ` N ) x. ( sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( Lam ` i ) x. sum_ j e. ( 1 ... N ) ( Lam ` j ) ) ) e. RR )
253 85 252 remulcld 
 |-  ( ph -> ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( log ` N ) x. ( sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( Lam ` i ) x. sum_ j e. ( 1 ... N ) ( Lam ` j ) ) ) ) e. RR )
254 58 253 remulcld 
 |-  ( ph -> ( 3 x. ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( log ` N ) x. ( sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( Lam ` i ) x. sum_ j e. ( 1 ... N ) ( Lam ` j ) ) ) ) ) e. RR )
255 1 2 209 89 hgt750lemb 
 |-  ( ph -> sum_ n e. { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) <_ ( ( log ` N ) x. ( sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( Lam ` i ) x. sum_ j e. ( 1 ... N ) ( Lam ` j ) ) ) )
256 111 252 215 lemul2d 
 |-  ( ph -> ( sum_ n e. { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) <_ ( ( log ` N ) x. ( sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( Lam ` i ) x. sum_ j e. ( 1 ... N ) ( Lam ` j ) ) ) <-> ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. sum_ n e. { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) <_ ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( log ` N ) x. ( sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( Lam ` i ) x. sum_ j e. ( 1 ... N ) ( Lam ` j ) ) ) ) ) )
257 255 256 mpbid 
 |-  ( ph -> ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. sum_ n e. { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) <_ ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( log ` N ) x. ( sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( Lam ` i ) x. sum_ j e. ( 1 ... N ) ( Lam ` j ) ) ) ) )
258 3rp 
 |-  3 e. RR+
259 258 a1i 
 |-  ( ph -> 3 e. RR+ )
260 112 253 259 lemul2d 
 |-  ( ph -> ( ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. sum_ n e. { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) <_ ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( log ` N ) x. ( sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( Lam ` i ) x. sum_ j e. ( 1 ... N ) ( Lam ` j ) ) ) ) <-> ( 3 x. ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. sum_ n e. { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) ) <_ ( 3 x. ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( log ` N ) x. ( sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( Lam ` i ) x. sum_ j e. ( 1 ... N ) ( Lam ` j ) ) ) ) ) ) )
261 257 260 mpbid 
 |-  ( ph -> ( 3 x. ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. sum_ n e. { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) ) <_ ( 3 x. ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( log ` N ) x. ( sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( Lam ` i ) x. sum_ j e. ( 1 ... N ) ( Lam ` j ) ) ) ) ) )
262 6re 
 |-  6 e. RR
263 262 57 pm3.2i 
 |-  ( 6 e. RR /\ 3 e. RR )
264 dp2cl 
 |-  ( ( 6 e. RR /\ 3 e. RR ) -> _ 6 3 e. RR )
265 263 264 ax-mp 
 |-  _ 6 3 e. RR
266 177 265 pm3.2i 
 |-  ( 2 e. RR /\ _ 6 3 e. RR )
267 dp2cl 
 |-  ( ( 2 e. RR /\ _ 6 3 e. RR ) -> _ 2 _ 6 3 e. RR )
268 266 267 ax-mp 
 |-  _ 2 _ 6 3 e. RR
269 114 268 pm3.2i 
 |-  ( 4 e. RR /\ _ 2 _ 6 3 e. RR )
270 dp2cl 
 |-  ( ( 4 e. RR /\ _ 2 _ 6 3 e. RR ) -> _ 4 _ 2 _ 6 3 e. RR )
271 269 270 ax-mp 
 |-  _ 4 _ 2 _ 6 3 e. RR
272 dpcl 
 |-  ( ( 1 e. NN0 /\ _ 4 _ 2 _ 6 3 e. RR ) -> ( 1 . _ 4 _ 2 _ 6 3 ) e. RR )
273 59 271 272 mp2an 
 |-  ( 1 . _ 4 _ 2 _ 6 3 ) e. RR
274 273 a1i 
 |-  ( ph -> ( 1 . _ 4 _ 2 _ 6 3 ) e. RR )
275 274 129 remulcld 
 |-  ( ph -> ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( sqrt ` N ) ) e. RR )
276 115 57 pm3.2i 
 |-  ( 8 e. RR /\ 3 e. RR )
277 dp2cl 
 |-  ( ( 8 e. RR /\ 3 e. RR ) -> _ 8 3 e. RR )
278 276 277 ax-mp 
 |-  _ 8 3 e. RR
279 115 278 pm3.2i 
 |-  ( 8 e. RR /\ _ 8 3 e. RR )
280 dp2cl 
 |-  ( ( 8 e. RR /\ _ 8 3 e. RR ) -> _ 8 _ 8 3 e. RR )
281 279 280 ax-mp 
 |-  _ 8 _ 8 3 e. RR
282 57 281 pm3.2i 
 |-  ( 3 e. RR /\ _ 8 _ 8 3 e. RR )
283 dp2cl 
 |-  ( ( 3 e. RR /\ _ 8 _ 8 3 e. RR ) -> _ 3 _ 8 _ 8 3 e. RR )
284 282 283 ax-mp 
 |-  _ 3 _ 8 _ 8 3 e. RR
285 136 284 pm3.2i 
 |-  ( 0 e. RR /\ _ 3 _ 8 _ 8 3 e. RR )
286 dp2cl 
 |-  ( ( 0 e. RR /\ _ 3 _ 8 _ 8 3 e. RR ) -> _ 0 _ 3 _ 8 _ 8 3 e. RR )
287 285 286 ax-mp 
 |-  _ 0 _ 3 _ 8 _ 8 3 e. RR
288 dpcl 
 |-  ( ( 1 e. NN0 /\ _ 0 _ 3 _ 8 _ 8 3 e. RR ) -> ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) e. RR )
289 59 287 288 mp2an 
 |-  ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) e. RR
290 289 a1i 
 |-  ( ph -> ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) e. RR )
291 290 127 remulcld 
 |-  ( ph -> ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) x. N ) e. RR )
292 275 291 remulcld 
 |-  ( ph -> ( ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( sqrt ` N ) ) x. ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) x. N ) ) e. RR )
293 126 292 remulcld 
 |-  ( ph -> ( ( log ` N ) x. ( ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( sqrt ` N ) ) x. ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) x. N ) ) ) e. RR )
294 85 293 remulcld 
 |-  ( ph -> ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( log ` N ) x. ( ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( sqrt ` N ) ) x. ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) x. N ) ) ) ) e. RR )
295 58 294 remulcld 
 |-  ( ph -> ( 3 x. ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( log ` N ) x. ( ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( sqrt ` N ) ) x. ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) x. N ) ) ) ) ) e. RR )
296 vmage0 
 |-  ( i e. NN -> 0 <_ ( Lam ` i ) )
297 242 296 syl 
 |-  ( ( ph /\ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ) -> 0 <_ ( Lam ` i ) )
298 234 243 297 fsumge0 
 |-  ( ph -> 0 <_ sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( Lam ` i ) )
299 2 3 hgt750lemd 
 |-  ( ph -> sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( Lam ` i ) < ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( sqrt ` N ) ) )
300 fzfid 
 |-  ( ph -> ( 1 ... N ) e. Fin )
301 15 a1i 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> Lam : NN --> RR )
302 237 sselda 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> j e. NN )
303 301 302 ffvelcdmd 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( Lam ` j ) e. RR )
304 vmage0 
 |-  ( j e. NN -> 0 <_ ( Lam ` j ) )
305 302 304 syl 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> 0 <_ ( Lam ` j ) )
306 300 303 305 fsumge0 
 |-  ( ph -> 0 <_ sum_ j e. ( 1 ... N ) ( Lam ` j ) )
307 2 hgt750lemc 
 |-  ( ph -> sum_ j e. ( 1 ... N ) ( Lam ` j ) < ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) x. N ) )
308 244 275 250 291 298 299 306 307 ltmul12ad 
 |-  ( ph -> ( sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( Lam ` i ) x. sum_ j e. ( 1 ... N ) ( Lam ` j ) ) < ( ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( sqrt ` N ) ) x. ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) x. N ) ) )
309 251 292 308 ltled 
 |-  ( ph -> ( sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( Lam ` i ) x. sum_ j e. ( 1 ... N ) ( Lam ` j ) ) <_ ( ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( sqrt ` N ) ) x. ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) x. N ) ) )
310 159 a1i 
 |-  ( ph -> 1 e. RR )
311 1lt2 
 |-  1 < 2
312 311 a1i 
 |-  ( ph -> 1 < 2 )
313 310 178 127 312 209 ltletrd 
 |-  ( ph -> 1 < N )
314 127 313 rplogcld 
 |-  ( ph -> ( log ` N ) e. RR+ )
315 251 292 314 lemul2d 
 |-  ( ph -> ( ( sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( Lam ` i ) x. sum_ j e. ( 1 ... N ) ( Lam ` j ) ) <_ ( ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( sqrt ` N ) ) x. ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) x. N ) ) <-> ( ( log ` N ) x. ( sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( Lam ` i ) x. sum_ j e. ( 1 ... N ) ( Lam ` j ) ) ) <_ ( ( log ` N ) x. ( ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( sqrt ` N ) ) x. ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) x. N ) ) ) ) )
316 309 315 mpbid 
 |-  ( ph -> ( ( log ` N ) x. ( sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( Lam ` i ) x. sum_ j e. ( 1 ... N ) ( Lam ` j ) ) ) <_ ( ( log ` N ) x. ( ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( sqrt ` N ) ) x. ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) x. N ) ) ) )
317 252 293 215 lemul2d 
 |-  ( ph -> ( ( ( log ` N ) x. ( sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( Lam ` i ) x. sum_ j e. ( 1 ... N ) ( Lam ` j ) ) ) <_ ( ( log ` N ) x. ( ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( sqrt ` N ) ) x. ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) x. N ) ) ) <-> ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( log ` N ) x. ( sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( Lam ` i ) x. sum_ j e. ( 1 ... N ) ( Lam ` j ) ) ) ) <_ ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( log ` N ) x. ( ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( sqrt ` N ) ) x. ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) x. N ) ) ) ) ) )
318 316 317 mpbid 
 |-  ( ph -> ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( log ` N ) x. ( sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( Lam ` i ) x. sum_ j e. ( 1 ... N ) ( Lam ` j ) ) ) ) <_ ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( log ` N ) x. ( ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( sqrt ` N ) ) x. ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) x. N ) ) ) ) )
319 253 294 259 lemul2d 
 |-  ( ph -> ( ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( log ` N ) x. ( sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( Lam ` i ) x. sum_ j e. ( 1 ... N ) ( Lam ` j ) ) ) ) <_ ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( log ` N ) x. ( ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( sqrt ` N ) ) x. ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) x. N ) ) ) ) <-> ( 3 x. ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( log ` N ) x. ( sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( Lam ` i ) x. sum_ j e. ( 1 ... N ) ( Lam ` j ) ) ) ) ) <_ ( 3 x. ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( log ` N ) x. ( ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( sqrt ` N ) ) x. ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) x. N ) ) ) ) ) ) )
320 318 319 mpbid 
 |-  ( ph -> ( 3 x. ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( log ` N ) x. ( sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( Lam ` i ) x. sum_ j e. ( 1 ... N ) ( Lam ` j ) ) ) ) ) <_ ( 3 x. ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( log ` N ) x. ( ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( sqrt ` N ) ) x. ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) x. N ) ) ) ) ) )
321 156 resqcli 
 |-  ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) e. RR
322 321 167 remulcli 
 |-  ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) e. RR
323 273 289 remulcli 
 |-  ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) e. RR
324 322 323 remulcli 
 |-  ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) e. RR
325 57 324 remulcli 
 |-  ( 3 x. ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) ) e. RR
326 hgt750lem2 
 |-  ( 3 x. ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) ) < ( 7 . _ 3 _ 4 8 )
327 325 123 326 ltleii 
 |-  ( 3 x. ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) ) <_ ( 7 . _ 3 _ 4 8 )
328 325 a1i 
 |-  ( ph -> ( 3 x. ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) ) e. RR )
329 314 130 rpdivcld 
 |-  ( ph -> ( ( log ` N ) / ( sqrt ` N ) ) e. RR+ )
330 125 213 rpexpcld 
 |-  ( ph -> ( N ^ 2 ) e. RR+ )
331 329 330 rpmulcld 
 |-  ( ph -> ( ( ( log ` N ) / ( sqrt ` N ) ) x. ( N ^ 2 ) ) e. RR+ )
332 328 124 331 lemul1d 
 |-  ( ph -> ( ( 3 x. ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) ) <_ ( 7 . _ 3 _ 4 8 ) <-> ( ( 3 x. ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) ) x. ( ( ( log ` N ) / ( sqrt ` N ) ) x. ( N ^ 2 ) ) ) <_ ( ( 7 . _ 3 _ 4 8 ) x. ( ( ( log ` N ) / ( sqrt ` N ) ) x. ( N ^ 2 ) ) ) ) )
333 327 332 mpbii 
 |-  ( ph -> ( ( 3 x. ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) ) x. ( ( ( log ` N ) / ( sqrt ` N ) ) x. ( N ^ 2 ) ) ) <_ ( ( 7 . _ 3 _ 4 8 ) x. ( ( ( log ` N ) / ( sqrt ` N ) ) x. ( N ^ 2 ) ) ) )
334 274 recnd 
 |-  ( ph -> ( 1 . _ 4 _ 2 _ 6 3 ) e. CC )
335 129 recnd 
 |-  ( ph -> ( sqrt ` N ) e. CC )
336 290 recnd 
 |-  ( ph -> ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) e. CC )
337 127 recnd 
 |-  ( ph -> N e. CC )
338 334 335 336 337 mul4d 
 |-  ( ph -> ( ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( sqrt ` N ) ) x. ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) x. N ) ) = ( ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) x. ( ( sqrt ` N ) x. N ) ) )
339 338 oveq2d 
 |-  ( ph -> ( ( log ` N ) x. ( ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( sqrt ` N ) ) x. ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) x. N ) ) ) = ( ( log ` N ) x. ( ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) x. ( ( sqrt ` N ) x. N ) ) ) )
340 126 recnd 
 |-  ( ph -> ( log ` N ) e. CC )
341 334 336 mulcld 
 |-  ( ph -> ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) e. CC )
342 335 337 mulcld 
 |-  ( ph -> ( ( sqrt ` N ) x. N ) e. CC )
343 341 342 mulcld 
 |-  ( ph -> ( ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) x. ( ( sqrt ` N ) x. N ) ) e. CC )
344 340 343 mulcomd 
 |-  ( ph -> ( ( log ` N ) x. ( ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) x. ( ( sqrt ` N ) x. N ) ) ) = ( ( ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) x. ( ( sqrt ` N ) x. N ) ) x. ( log ` N ) ) )
345 339 344 eqtrd 
 |-  ( ph -> ( ( log ` N ) x. ( ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( sqrt ` N ) ) x. ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) x. N ) ) ) = ( ( ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) x. ( ( sqrt ` N ) x. N ) ) x. ( log ` N ) ) )
346 341 342 340 mulassd 
 |-  ( ph -> ( ( ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) x. ( ( sqrt ` N ) x. N ) ) x. ( log ` N ) ) = ( ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) x. ( ( ( sqrt ` N ) x. N ) x. ( log ` N ) ) ) )
347 345 346 eqtrd 
 |-  ( ph -> ( ( log ` N ) x. ( ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( sqrt ` N ) ) x. ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) x. N ) ) ) = ( ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) x. ( ( ( sqrt ` N ) x. N ) x. ( log ` N ) ) ) )
348 347 oveq2d 
 |-  ( ph -> ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( log ` N ) x. ( ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( sqrt ` N ) ) x. ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) x. N ) ) ) ) = ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) x. ( ( ( sqrt ` N ) x. N ) x. ( log ` N ) ) ) ) )
349 85 recnd 
 |-  ( ph -> ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) e. CC )
350 342 340 mulcld 
 |-  ( ph -> ( ( ( sqrt ` N ) x. N ) x. ( log ` N ) ) e. CC )
351 349 341 350 mulassd 
 |-  ( ph -> ( ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) x. ( ( ( sqrt ` N ) x. N ) x. ( log ` N ) ) ) = ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) x. ( ( ( sqrt ` N ) x. N ) x. ( log ` N ) ) ) ) )
352 348 351 eqtr4d 
 |-  ( ph -> ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( log ` N ) x. ( ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( sqrt ` N ) ) x. ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) x. N ) ) ) ) = ( ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) x. ( ( ( sqrt ` N ) x. N ) x. ( log ` N ) ) ) )
353 352 oveq2d 
 |-  ( ph -> ( 3 x. ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( log ` N ) x. ( ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( sqrt ` N ) ) x. ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) x. N ) ) ) ) ) = ( 3 x. ( ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) x. ( ( ( sqrt ` N ) x. N ) x. ( log ` N ) ) ) ) )
354 58 recnd 
 |-  ( ph -> 3 e. CC )
355 349 341 mulcld 
 |-  ( ph -> ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) e. CC )
356 354 355 350 mulassd 
 |-  ( ph -> ( ( 3 x. ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) ) x. ( ( ( sqrt ` N ) x. N ) x. ( log ` N ) ) ) = ( 3 x. ( ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) x. ( ( ( sqrt ` N ) x. N ) x. ( log ` N ) ) ) ) )
357 353 356 eqtr4d 
 |-  ( ph -> ( 3 x. ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( log ` N ) x. ( ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( sqrt ` N ) ) x. ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) x. N ) ) ) ) ) = ( ( 3 x. ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) ) x. ( ( ( sqrt ` N ) x. N ) x. ( log ` N ) ) ) )
358 134 recnd 
 |-  ( ph -> ( N ^ 2 ) e. CC )
359 340 335 358 131 div32d 
 |-  ( ph -> ( ( ( log ` N ) / ( sqrt ` N ) ) x. ( N ^ 2 ) ) = ( ( log ` N ) x. ( ( N ^ 2 ) / ( sqrt ` N ) ) ) )
360 358 335 131 divcld 
 |-  ( ph -> ( ( N ^ 2 ) / ( sqrt ` N ) ) e. CC )
361 340 360 mulcomd 
 |-  ( ph -> ( ( log ` N ) x. ( ( N ^ 2 ) / ( sqrt ` N ) ) ) = ( ( ( N ^ 2 ) / ( sqrt ` N ) ) x. ( log ` N ) ) )
362 337 sqvald 
 |-  ( ph -> ( N ^ 2 ) = ( N x. N ) )
363 362 oveq1d 
 |-  ( ph -> ( ( N ^ 2 ) / ( sqrt ` N ) ) = ( ( N x. N ) / ( sqrt ` N ) ) )
364 337 337 335 131 divassd 
 |-  ( ph -> ( ( N x. N ) / ( sqrt ` N ) ) = ( N x. ( N / ( sqrt ` N ) ) ) )
365 divsqrtid 
 |-  ( N e. RR+ -> ( N / ( sqrt ` N ) ) = ( sqrt ` N ) )
366 125 365 syl 
 |-  ( ph -> ( N / ( sqrt ` N ) ) = ( sqrt ` N ) )
367 366 oveq2d 
 |-  ( ph -> ( N x. ( N / ( sqrt ` N ) ) ) = ( N x. ( sqrt ` N ) ) )
368 363 364 367 3eqtrd 
 |-  ( ph -> ( ( N ^ 2 ) / ( sqrt ` N ) ) = ( N x. ( sqrt ` N ) ) )
369 337 335 mulcomd 
 |-  ( ph -> ( N x. ( sqrt ` N ) ) = ( ( sqrt ` N ) x. N ) )
370 368 369 eqtrd 
 |-  ( ph -> ( ( N ^ 2 ) / ( sqrt ` N ) ) = ( ( sqrt ` N ) x. N ) )
371 370 oveq1d 
 |-  ( ph -> ( ( ( N ^ 2 ) / ( sqrt ` N ) ) x. ( log ` N ) ) = ( ( ( sqrt ` N ) x. N ) x. ( log ` N ) ) )
372 359 361 371 3eqtrrd 
 |-  ( ph -> ( ( ( sqrt ` N ) x. N ) x. ( log ` N ) ) = ( ( ( log ` N ) / ( sqrt ` N ) ) x. ( N ^ 2 ) ) )
373 372 oveq2d 
 |-  ( ph -> ( ( 3 x. ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) ) x. ( ( ( sqrt ` N ) x. N ) x. ( log ` N ) ) ) = ( ( 3 x. ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) ) x. ( ( ( log ` N ) / ( sqrt ` N ) ) x. ( N ^ 2 ) ) ) )
374 357 373 eqtrd 
 |-  ( ph -> ( 3 x. ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( log ` N ) x. ( ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( sqrt ` N ) ) x. ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) x. N ) ) ) ) ) = ( ( 3 x. ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) ) ) ) x. ( ( ( log ` N ) / ( sqrt ` N ) ) x. ( N ^ 2 ) ) ) )
375 124 recnd 
 |-  ( ph -> ( 7 . _ 3 _ 4 8 ) e. CC )
376 132 recnd 
 |-  ( ph -> ( ( log ` N ) / ( sqrt ` N ) ) e. CC )
377 375 376 358 mulassd 
 |-  ( ph -> ( ( ( 7 . _ 3 _ 4 8 ) x. ( ( log ` N ) / ( sqrt ` N ) ) ) x. ( N ^ 2 ) ) = ( ( 7 . _ 3 _ 4 8 ) x. ( ( ( log ` N ) / ( sqrt ` N ) ) x. ( N ^ 2 ) ) ) )
378 333 374 377 3brtr4d 
 |-  ( ph -> ( 3 x. ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( log ` N ) x. ( ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( sqrt ` N ) ) x. ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) x. N ) ) ) ) ) <_ ( ( ( 7 . _ 3 _ 4 8 ) x. ( ( log ` N ) / ( sqrt ` N ) ) ) x. ( N ^ 2 ) ) )
379 254 295 135 320 378 letrd 
 |-  ( ph -> ( 3 x. ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. ( ( log ` N ) x. ( sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( Lam ` i ) x. sum_ j e. ( 1 ... N ) ( Lam ` j ) ) ) ) ) <_ ( ( ( 7 . _ 3 _ 4 8 ) x. ( ( log ` N ) / ( sqrt ` N ) ) ) x. ( N ^ 2 ) ) )
380 113 254 135 261 379 letrd 
 |-  ( ph -> ( 3 x. ( ( ( ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) ^ 2 ) x. ( 1 . _ 4 _ 1 4 ) ) x. sum_ n e. { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) ) <_ ( ( ( 7 . _ 3 _ 4 8 ) x. ( ( log ` N ) / ( sqrt ` N ) ) ) x. ( N ^ 2 ) ) )
381 56 113 135 227 380 letrd 
 |-  ( 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 ) ) )