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