Metamath Proof Explorer

Theorem dchrisum0re

Description: Suppose X is a non-principal Dirichlet character with sum_ n e. NN , X ( n ) / n = 0 . Then X is a real character. Part of Lemma 9.4.4 of Shapiro, p. 382. (Contributed by Mario Carneiro, 5-May-2016)

Ref Expression
Hypotheses rpvmasum.z 
|- Z = ( Z/nZ ` N )
rpvmasum.l 
|- L = ( ZRHom ` Z )
rpvmasum.a 
|- ( ph -> N e. NN )
rpvmasum2.g 
|- G = ( DChr ` N )
rpvmasum2.d 
|- D = ( Base ` G )
rpvmasum2.1 
|- .1. = ( 0g ` G )
rpvmasum2.w 
|- W = { y e. ( D \ { .1. } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 }
dchrisum0.b 
|- ( ph -> X e. W )
Assertion dchrisum0re 
|- ( ph -> X : ( Base ` Z ) --> RR )

Proof

Step Hyp Ref Expression
1 rpvmasum.z 
 |-  Z = ( Z/nZ ` N )
2 rpvmasum.l 
 |-  L = ( ZRHom ` Z )
3 rpvmasum.a 
 |-  ( ph -> N e. NN )
4 rpvmasum2.g 
 |-  G = ( DChr ` N )
5 rpvmasum2.d 
 |-  D = ( Base ` G )
6 rpvmasum2.1 
 |-  .1. = ( 0g ` G )
7 rpvmasum2.w 
 |-  W = { y e. ( D \ { .1. } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 }
8 dchrisum0.b 
 |-  ( ph -> X e. W )
9 eqid 
 |-  ( Base ` Z ) = ( Base ` Z )
10 7 ssrab3 
 |-  W C_ ( D \ { .1. } )
11 10 8 sseldi 
 |-  ( ph -> X e. ( D \ { .1. } ) )
12 11 eldifad 
 |-  ( ph -> X e. D )
13 4 1 5 9 12 dchrf 
 |-  ( ph -> X : ( Base ` Z ) --> CC )
14 13 ffnd 
 |-  ( ph -> X Fn ( Base ` Z ) )
15 13 ffvelrnda 
 |-  ( ( ph /\ x e. ( Base ` Z ) ) -> ( X ` x ) e. CC )
16 fvco3 
 |-  ( ( X : ( Base ` Z ) --> CC /\ x e. ( Base ` Z ) ) -> ( ( * o. X ) ` x ) = ( * ` ( X ` x ) ) )
17 13 16 sylan 
 |-  ( ( ph /\ x e. ( Base ` Z ) ) -> ( ( * o. X ) ` x ) = ( * ` ( X ` x ) ) )
18 logno1 
 |-  -. ( x e. RR+ |-> ( log ` x ) ) e. O(1)
19 1red 
 |-  ( ( ph /\ ( * o. X ) =/= X ) -> 1 e. RR )
20 eqid 
 |-  ( Unit ` Z ) = ( Unit ` Z )
21 3 nnnn0d 
 |-  ( ph -> N e. NN0 )
22 1 zncrng 
 |-  ( N e. NN0 -> Z e. CRing )
23 21 22 syl 
 |-  ( ph -> Z e. CRing )
24 crngring 
 |-  ( Z e. CRing -> Z e. Ring )
25 23 24 syl 
 |-  ( ph -> Z e. Ring )
26 eqid 
 |-  ( 1r ` Z ) = ( 1r ` Z )
27 20 26 1unit 
 |-  ( Z e. Ring -> ( 1r ` Z ) e. ( Unit ` Z ) )
28 25 27 syl 
 |-  ( ph -> ( 1r ` Z ) e. ( Unit ` Z ) )
29 eqid 
 |-  ( `' L " { ( 1r ` Z ) } ) = ( `' L " { ( 1r ` Z ) } )
30 eqidd 
 |-  ( ( ph /\ f e. W ) -> ( 1r ` Z ) = ( 1r ` Z ) )
31 1 2 3 4 5 6 7 20 28 29 30 rpvmasum2 
 |-  ( ph -> ( x e. RR+ |-> ( ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( `' L " { ( 1r ` Z ) } ) ) ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. ( 1 - ( # ` W ) ) ) ) ) e. O(1) )
32 31 adantr 
 |-  ( ( ph /\ ( * o. X ) =/= X ) -> ( x e. RR+ |-> ( ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( `' L " { ( 1r ` Z ) } ) ) ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. ( 1 - ( # ` W ) ) ) ) ) e. O(1) )
33 3 phicld 
 |-  ( ph -> ( phi ` N ) e. NN )
34 33 nnnn0d 
 |-  ( ph -> ( phi ` N ) e. NN0 )
35 34 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> ( phi ` N ) e. NN0 )
36 35 nn0red 
 |-  ( ( ph /\ x e. RR+ ) -> ( phi ` N ) e. RR )
37 fzfid 
 |-  ( ( ph /\ x e. RR+ ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
38 inss1 
 |-  ( ( 1 ... ( |_ ` x ) ) i^i ( `' L " { ( 1r ` Z ) } ) ) C_ ( 1 ... ( |_ ` x ) )
39 ssfi 
 |-  ( ( ( 1 ... ( |_ ` x ) ) e. Fin /\ ( ( 1 ... ( |_ ` x ) ) i^i ( `' L " { ( 1r ` Z ) } ) ) C_ ( 1 ... ( |_ ` x ) ) ) -> ( ( 1 ... ( |_ ` x ) ) i^i ( `' L " { ( 1r ` Z ) } ) ) e. Fin )
40 37 38 39 sylancl 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( 1 ... ( |_ ` x ) ) i^i ( `' L " { ( 1r ` Z ) } ) ) e. Fin )
41 elinel1 
 |-  ( n e. ( ( 1 ... ( |_ ` x ) ) i^i ( `' L " { ( 1r ` Z ) } ) ) -> n e. ( 1 ... ( |_ ` x ) ) )
42 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
43 42 adantl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
44 41 43 sylan2 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( `' L " { ( 1r ` Z ) } ) ) ) -> n e. NN )
45 vmacl 
 |-  ( n e. NN -> ( Lam ` n ) e. RR )
46 nndivre 
 |-  ( ( ( Lam ` n ) e. RR /\ n e. NN ) -> ( ( Lam ` n ) / n ) e. RR )
47 45 46 mpancom 
 |-  ( n e. NN -> ( ( Lam ` n ) / n ) e. RR )
48 44 47 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( `' L " { ( 1r ` Z ) } ) ) ) -> ( ( Lam ` n ) / n ) e. RR )
49 40 48 fsumrecl 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( `' L " { ( 1r ` Z ) } ) ) ( ( Lam ` n ) / n ) e. RR )
50 36 49 remulcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( `' L " { ( 1r ` Z ) } ) ) ( ( Lam ` n ) / n ) ) e. RR )
51 relogcl 
 |-  ( x e. RR+ -> ( log ` x ) e. RR )
52 51 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> ( log ` x ) e. RR )
53 1re 
 |-  1 e. RR
54 4 5 dchrfi 
 |-  ( N e. NN -> D e. Fin )
55 3 54 syl 
 |-  ( ph -> D e. Fin )
56 difss 
 |-  ( D \ { .1. } ) C_ D
57 10 56 sstri 
 |-  W C_ D
58 ssfi 
 |-  ( ( D e. Fin /\ W C_ D ) -> W e. Fin )
59 55 57 58 sylancl 
 |-  ( ph -> W e. Fin )
60 hashcl 
 |-  ( W e. Fin -> ( # ` W ) e. NN0 )
61 59 60 syl 
 |-  ( ph -> ( # ` W ) e. NN0 )
62 61 nn0red 
 |-  ( ph -> ( # ` W ) e. RR )
63 resubcl 
 |-  ( ( 1 e. RR /\ ( # ` W ) e. RR ) -> ( 1 - ( # ` W ) ) e. RR )
64 53 62 63 sylancr 
 |-  ( ph -> ( 1 - ( # ` W ) ) e. RR )
65 64 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> ( 1 - ( # ` W ) ) e. RR )
66 52 65 remulcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) x. ( 1 - ( # ` W ) ) ) e. RR )
67 50 66 resubcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( `' L " { ( 1r ` Z ) } ) ) ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. ( 1 - ( # ` W ) ) ) ) e. RR )
68 67 recnd 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( `' L " { ( 1r ` Z ) } ) ) ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. ( 1 - ( # ` W ) ) ) ) e. CC )
69 68 adantlr 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ x e. RR+ ) -> ( ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( `' L " { ( 1r ` Z ) } ) ) ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. ( 1 - ( # ` W ) ) ) ) e. CC )
70 51 adantl 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ x e. RR+ ) -> ( log ` x ) e. RR )
71 70 recnd 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ x e. RR+ ) -> ( log ` x ) e. CC )
72 51 ad2antrl 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( log ` x ) e. RR )
73 66 ad2ant2r 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( log ` x ) x. ( 1 - ( # ` W ) ) ) e. RR )
74 72 73 readdcld 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( log ` x ) + ( ( log ` x ) x. ( 1 - ( # ` W ) ) ) ) e. RR )
75 0red 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> 0 e. RR )
76 50 ad2ant2r 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( `' L " { ( 1r ` Z ) } ) ) ( ( Lam ` n ) / n ) ) e. RR )
77 2re 
 |-  2 e. RR
78 77 a1i 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> 2 e. RR )
79 62 ad2antrr 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( # ` W ) e. RR )
80 78 79 resubcld 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( 2 - ( # ` W ) ) e. RR )
81 log1 
 |-  ( log ` 1 ) = 0
82 simprr 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> 1 <_ x )
83 1rp 
 |-  1 e. RR+
84 simprl 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> x e. RR+ )
85 logleb 
 |-  ( ( 1 e. RR+ /\ x e. RR+ ) -> ( 1 <_ x <-> ( log ` 1 ) <_ ( log ` x ) ) )
86 83 84 85 sylancr 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( 1 <_ x <-> ( log ` 1 ) <_ ( log ` x ) ) )
87 82 86 mpbid 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( log ` 1 ) <_ ( log ` x ) )
88 81 87 eqbrtrrid 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> 0 <_ ( log ` x ) )
89 59 ad2antrr 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> W e. Fin )
90 eqid 
 |-  ( invg ` G ) = ( invg ` G )
91 4 5 12 90 dchrinv 
 |-  ( ph -> ( ( invg ` G ) ` X ) = ( * o. X ) )
92 4 dchrabl 
 |-  ( N e. NN -> G e. Abel )
93 3 92 syl 
 |-  ( ph -> G e. Abel )
94 ablgrp 
 |-  ( G e. Abel -> G e. Grp )
95 93 94 syl 
 |-  ( ph -> G e. Grp )
96 5 90 grpinvcl 
 |-  ( ( G e. Grp /\ X e. D ) -> ( ( invg ` G ) ` X ) e. D )
97 95 12 96 syl2anc 
 |-  ( ph -> ( ( invg ` G ) ` X ) e. D )
98 91 97 eqeltrrd 
 |-  ( ph -> ( * o. X ) e. D )
99 eldifsni 
 |-  ( X e. ( D \ { .1. } ) -> X =/= .1. )
100 11 99 syl 
 |-  ( ph -> X =/= .1. )
101 5 6 grpidcl 
 |-  ( G e. Grp -> .1. e. D )
102 95 101 syl 
 |-  ( ph -> .1. e. D )
103 5 90 95 12 102 grpinv11 
 |-  ( ph -> ( ( ( invg ` G ) ` X ) = ( ( invg ` G ) ` .1. ) <-> X = .1. ) )
104 103 necon3bid 
 |-  ( ph -> ( ( ( invg ` G ) ` X ) =/= ( ( invg ` G ) ` .1. ) <-> X =/= .1. ) )
105 100 104 mpbird 
 |-  ( ph -> ( ( invg ` G ) ` X ) =/= ( ( invg ` G ) ` .1. ) )
106 6 90 grpinvid 
 |-  ( G e. Grp -> ( ( invg ` G ) ` .1. ) = .1. )
107 95 106 syl 
 |-  ( ph -> ( ( invg ` G ) ` .1. ) = .1. )
108 105 91 107 3netr3d 
 |-  ( ph -> ( * o. X ) =/= .1. )
109 eldifsn 
 |-  ( ( * o. X ) e. ( D \ { .1. } ) <-> ( ( * o. X ) e. D /\ ( * o. X ) =/= .1. ) )
110 98 108 109 sylanbrc 
 |-  ( ph -> ( * o. X ) e. ( D \ { .1. } ) )
111 nnuz 
 |-  NN = ( ZZ>= ` 1 )
112 1zzd 
 |-  ( ph -> 1 e. ZZ )
113 2fveq3 
 |-  ( n = m -> ( X ` ( L ` n ) ) = ( X ` ( L ` m ) ) )
114 id 
 |-  ( n = m -> n = m )
115 113 114 oveq12d 
 |-  ( n = m -> ( ( X ` ( L ` n ) ) / n ) = ( ( X ` ( L ` m ) ) / m ) )
116 115 fveq2d 
 |-  ( n = m -> ( * ` ( ( X ` ( L ` n ) ) / n ) ) = ( * ` ( ( X ` ( L ` m ) ) / m ) ) )
117 eqid 
 |-  ( n e. NN |-> ( * ` ( ( X ` ( L ` n ) ) / n ) ) ) = ( n e. NN |-> ( * ` ( ( X ` ( L ` n ) ) / n ) ) )
118 fvex 
 |-  ( * ` ( ( X ` ( L ` m ) ) / m ) ) e. _V
119 116 117 118 fvmpt 
 |-  ( m e. NN -> ( ( n e. NN |-> ( * ` ( ( X ` ( L ` n ) ) / n ) ) ) ` m ) = ( * ` ( ( X ` ( L ` m ) ) / m ) ) )
120 119 adantl 
 |-  ( ( ph /\ m e. NN ) -> ( ( n e. NN |-> ( * ` ( ( X ` ( L ` n ) ) / n ) ) ) ` m ) = ( * ` ( ( X ` ( L ` m ) ) / m ) ) )
121 nnre 
 |-  ( m e. NN -> m e. RR )
122 121 adantl 
 |-  ( ( ph /\ m e. NN ) -> m e. RR )
123 122 cjred 
 |-  ( ( ph /\ m e. NN ) -> ( * ` m ) = m )
124 123 oveq2d 
 |-  ( ( ph /\ m e. NN ) -> ( ( * ` ( X ` ( L ` m ) ) ) / ( * ` m ) ) = ( ( * ` ( X ` ( L ` m ) ) ) / m ) )
125 13 adantr 
 |-  ( ( ph /\ m e. NN ) -> X : ( Base ` Z ) --> CC )
126 1 9 2 znzrhfo 
 |-  ( N e. NN0 -> L : ZZ -onto-> ( Base ` Z ) )
127 21 126 syl 
 |-  ( ph -> L : ZZ -onto-> ( Base ` Z ) )
128 fof 
 |-  ( L : ZZ -onto-> ( Base ` Z ) -> L : ZZ --> ( Base ` Z ) )
129 127 128 syl 
 |-  ( ph -> L : ZZ --> ( Base ` Z ) )
130 nnz 
 |-  ( m e. NN -> m e. ZZ )
131 ffvelrn 
 |-  ( ( L : ZZ --> ( Base ` Z ) /\ m e. ZZ ) -> ( L ` m ) e. ( Base ` Z ) )
132 129 130 131 syl2an 
 |-  ( ( ph /\ m e. NN ) -> ( L ` m ) e. ( Base ` Z ) )
133 125 132 ffvelrnd 
 |-  ( ( ph /\ m e. NN ) -> ( X ` ( L ` m ) ) e. CC )
134 nncn 
 |-  ( m e. NN -> m e. CC )
135 134 adantl 
 |-  ( ( ph /\ m e. NN ) -> m e. CC )
136 nnne0 
 |-  ( m e. NN -> m =/= 0 )
137 136 adantl 
 |-  ( ( ph /\ m e. NN ) -> m =/= 0 )
138 133 135 137 cjdivd 
 |-  ( ( ph /\ m e. NN ) -> ( * ` ( ( X ` ( L ` m ) ) / m ) ) = ( ( * ` ( X ` ( L ` m ) ) ) / ( * ` m ) ) )
139 fvco3 
 |-  ( ( X : ( Base ` Z ) --> CC /\ ( L ` m ) e. ( Base ` Z ) ) -> ( ( * o. X ) ` ( L ` m ) ) = ( * ` ( X ` ( L ` m ) ) ) )
140 125 132 139 syl2anc 
 |-  ( ( ph /\ m e. NN ) -> ( ( * o. X ) ` ( L ` m ) ) = ( * ` ( X ` ( L ` m ) ) ) )
141 140 oveq1d 
 |-  ( ( ph /\ m e. NN ) -> ( ( ( * o. X ) ` ( L ` m ) ) / m ) = ( ( * ` ( X ` ( L ` m ) ) ) / m ) )
142 124 138 141 3eqtr4d 
 |-  ( ( ph /\ m e. NN ) -> ( * ` ( ( X ` ( L ` m ) ) / m ) ) = ( ( ( * o. X ) ` ( L ` m ) ) / m ) )
143 120 142 eqtrd 
 |-  ( ( ph /\ m e. NN ) -> ( ( n e. NN |-> ( * ` ( ( X ` ( L ` n ) ) / n ) ) ) ` m ) = ( ( ( * o. X ) ` ( L ` m ) ) / m ) )
144 133 cjcld 
 |-  ( ( ph /\ m e. NN ) -> ( * ` ( X ` ( L ` m ) ) ) e. CC )
145 144 135 137 divcld 
 |-  ( ( ph /\ m e. NN ) -> ( ( * ` ( X ` ( L ` m ) ) ) / m ) e. CC )
146 141 145 eqeltrd 
 |-  ( ( ph /\ m e. NN ) -> ( ( ( * o. X ) ` ( L ` m ) ) / m ) e. CC )
147 eqid 
 |-  ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) = ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) )
148 1 2 3 4 5 6 12 100 147 dchrmusumlema 
 |-  ( ph -> E. t E. c e. ( 0 [,) +oo ) ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) )
149 simprrl 
 |-  ( ( ph /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) ) ) -> seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ~~> t )
150 8 adantr 
 |-  ( ( ph /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) ) ) -> X e. W )
151 3 adantr 
 |-  ( ( ph /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) ) ) -> N e. NN )
152 12 adantr 
 |-  ( ( ph /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) ) ) -> X e. D )
153 100 adantr 
 |-  ( ( ph /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) ) ) -> X =/= .1. )
154 simprl 
 |-  ( ( ph /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) ) ) -> c e. ( 0 [,) +oo ) )
155 simprrr 
 |-  ( ( ph /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) ) ) -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) )
156 1 2 151 4 5 6 152 153 147 154 149 155 7 dchrvmaeq0 
 |-  ( ( ph /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) ) ) -> ( X e. W <-> t = 0 ) )
157 150 156 mpbid 
 |-  ( ( ph /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) ) ) -> t = 0 )
158 149 157 breqtrd 
 |-  ( ( ph /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) ) ) -> seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ~~> 0 )
159 158 rexlimdvaa 
 |-  ( ph -> ( E. c e. ( 0 [,) +oo ) ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) -> seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ~~> 0 ) )
160 159 exlimdv 
 |-  ( ph -> ( E. t E. c e. ( 0 [,) +oo ) ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) -> seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ~~> 0 ) )
161 148 160 mpd 
 |-  ( ph -> seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ~~> 0 )
162 seqex 
 |-  seq 1 ( + , ( n e. NN |-> ( * ` ( ( X ` ( L ` n ) ) / n ) ) ) ) e. _V
163 162 a1i 
 |-  ( ph -> seq 1 ( + , ( n e. NN |-> ( * ` ( ( X ` ( L ` n ) ) / n ) ) ) ) e. _V )
164 2fveq3 
 |-  ( a = m -> ( X ` ( L ` a ) ) = ( X ` ( L ` m ) ) )
165 id 
 |-  ( a = m -> a = m )
166 164 165 oveq12d 
 |-  ( a = m -> ( ( X ` ( L ` a ) ) / a ) = ( ( X ` ( L ` m ) ) / m ) )
167 ovex 
 |-  ( ( X ` ( L ` m ) ) / m ) e. _V
168 166 147 167 fvmpt 
 |-  ( m e. NN -> ( ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ` m ) = ( ( X ` ( L ` m ) ) / m ) )
169 168 adantl 
 |-  ( ( ph /\ m e. NN ) -> ( ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ` m ) = ( ( X ` ( L ` m ) ) / m ) )
170 133 135 137 divcld 
 |-  ( ( ph /\ m e. NN ) -> ( ( X ` ( L ` m ) ) / m ) e. CC )
171 169 170 eqeltrd 
 |-  ( ( ph /\ m e. NN ) -> ( ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ` m ) e. CC )
172 111 112 171 serf 
 |-  ( ph -> seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) : NN --> CC )
173 172 ffvelrnda 
 |-  ( ( ph /\ k e. NN ) -> ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ` k ) e. CC )
174 fzfid 
 |-  ( ( ph /\ k e. NN ) -> ( 1 ... k ) e. Fin )
175 simpl 
 |-  ( ( ph /\ k e. NN ) -> ph )
176 elfznn 
 |-  ( m e. ( 1 ... k ) -> m e. NN )
177 175 176 170 syl2an 
 |-  ( ( ( ph /\ k e. NN ) /\ m e. ( 1 ... k ) ) -> ( ( X ` ( L ` m ) ) / m ) e. CC )
178 174 177 fsumcj 
 |-  ( ( ph /\ k e. NN ) -> ( * ` sum_ m e. ( 1 ... k ) ( ( X ` ( L ` m ) ) / m ) ) = sum_ m e. ( 1 ... k ) ( * ` ( ( X ` ( L ` m ) ) / m ) ) )
179 175 176 169 syl2an 
 |-  ( ( ( ph /\ k e. NN ) /\ m e. ( 1 ... k ) ) -> ( ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ` m ) = ( ( X ` ( L ` m ) ) / m ) )
180 simpr 
 |-  ( ( ph /\ k e. NN ) -> k e. NN )
181 180 111 eleqtrdi 
 |-  ( ( ph /\ k e. NN ) -> k e. ( ZZ>= ` 1 ) )
182 179 181 177 fsumser 
 |-  ( ( ph /\ k e. NN ) -> sum_ m e. ( 1 ... k ) ( ( X ` ( L ` m ) ) / m ) = ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ` k ) )
183 182 fveq2d 
 |-  ( ( ph /\ k e. NN ) -> ( * ` sum_ m e. ( 1 ... k ) ( ( X ` ( L ` m ) ) / m ) ) = ( * ` ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ` k ) ) )
184 175 176 120 syl2an 
 |-  ( ( ( ph /\ k e. NN ) /\ m e. ( 1 ... k ) ) -> ( ( n e. NN |-> ( * ` ( ( X ` ( L ` n ) ) / n ) ) ) ` m ) = ( * ` ( ( X ` ( L ` m ) ) / m ) ) )
185 170 cjcld 
 |-  ( ( ph /\ m e. NN ) -> ( * ` ( ( X ` ( L ` m ) ) / m ) ) e. CC )
186 175 176 185 syl2an 
 |-  ( ( ( ph /\ k e. NN ) /\ m e. ( 1 ... k ) ) -> ( * ` ( ( X ` ( L ` m ) ) / m ) ) e. CC )
187 184 181 186 fsumser 
 |-  ( ( ph /\ k e. NN ) -> sum_ m e. ( 1 ... k ) ( * ` ( ( X ` ( L ` m ) ) / m ) ) = ( seq 1 ( + , ( n e. NN |-> ( * ` ( ( X ` ( L ` n ) ) / n ) ) ) ) ` k ) )
188 178 183 187 3eqtr3rd 
 |-  ( ( ph /\ k e. NN ) -> ( seq 1 ( + , ( n e. NN |-> ( * ` ( ( X ` ( L ` n ) ) / n ) ) ) ) ` k ) = ( * ` ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ` k ) ) )
189 111 161 163 112 173 188 climcj 
 |-  ( ph -> seq 1 ( + , ( n e. NN |-> ( * ` ( ( X ` ( L ` n ) ) / n ) ) ) ) ~~> ( * ` 0 ) )
190 cj0 
 |-  ( * ` 0 ) = 0
191 189 190 breqtrdi 
 |-  ( ph -> seq 1 ( + , ( n e. NN |-> ( * ` ( ( X ` ( L ` n ) ) / n ) ) ) ) ~~> 0 )
192 111 112 143 146 191 isumclim 
 |-  ( ph -> sum_ m e. NN ( ( ( * o. X ) ` ( L ` m ) ) / m ) = 0 )
193 fveq1 
 |-  ( y = ( * o. X ) -> ( y ` ( L ` m ) ) = ( ( * o. X ) ` ( L ` m ) ) )
194 193 oveq1d 
 |-  ( y = ( * o. X ) -> ( ( y ` ( L ` m ) ) / m ) = ( ( ( * o. X ) ` ( L ` m ) ) / m ) )
195 194 sumeq2sdv 
 |-  ( y = ( * o. X ) -> sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = sum_ m e. NN ( ( ( * o. X ) ` ( L ` m ) ) / m ) )
196 195 eqeq1d 
 |-  ( y = ( * o. X ) -> ( sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 <-> sum_ m e. NN ( ( ( * o. X ) ` ( L ` m ) ) / m ) = 0 ) )
197 196 7 elrab2 
 |-  ( ( * o. X ) e. W <-> ( ( * o. X ) e. ( D \ { .1. } ) /\ sum_ m e. NN ( ( ( * o. X ) ` ( L ` m ) ) / m ) = 0 ) )
198 110 192 197 sylanbrc 
 |-  ( ph -> ( * o. X ) e. W )
199 198 ad2antrr 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( * o. X ) e. W )
200 8 ad2antrr 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> X e. W )
201 simplr 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( * o. X ) =/= X )
202 89 199 200 201 nehash2 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> 2 <_ ( # ` W ) )
203 suble0 
 |-  ( ( 2 e. RR /\ ( # ` W ) e. RR ) -> ( ( 2 - ( # ` W ) ) <_ 0 <-> 2 <_ ( # ` W ) ) )
204 77 79 203 sylancr 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( 2 - ( # ` W ) ) <_ 0 <-> 2 <_ ( # ` W ) ) )
205 202 204 mpbird 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( 2 - ( # ` W ) ) <_ 0 )
206 80 75 72 88 205 lemul2ad 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( log ` x ) x. ( 2 - ( # ` W ) ) ) <_ ( ( log ` x ) x. 0 ) )
207 df-2 
 |-  2 = ( 1 + 1 )
208 207 oveq1i 
 |-  ( 2 - ( # ` W ) ) = ( ( 1 + 1 ) - ( # ` W ) )
209 1cnd 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> 1 e. CC )
210 79 recnd 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( # ` W ) e. CC )
211 209 209 210 addsubassd 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( 1 + 1 ) - ( # ` W ) ) = ( 1 + ( 1 - ( # ` W ) ) ) )
212 208 211 syl5eq 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( 2 - ( # ` W ) ) = ( 1 + ( 1 - ( # ` W ) ) ) )
213 212 oveq2d 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( log ` x ) x. ( 2 - ( # ` W ) ) ) = ( ( log ` x ) x. ( 1 + ( 1 - ( # ` W ) ) ) ) )
214 71 adantrr 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( log ` x ) e. CC )
215 64 ad2antrr 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( 1 - ( # ` W ) ) e. RR )
216 215 recnd 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( 1 - ( # ` W ) ) e. CC )
217 214 209 216 adddid 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( log ` x ) x. ( 1 + ( 1 - ( # ` W ) ) ) ) = ( ( ( log ` x ) x. 1 ) + ( ( log ` x ) x. ( 1 - ( # ` W ) ) ) ) )
218 214 mulid1d 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( log ` x ) x. 1 ) = ( log ` x ) )
219 218 oveq1d 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( ( log ` x ) x. 1 ) + ( ( log ` x ) x. ( 1 - ( # ` W ) ) ) ) = ( ( log ` x ) + ( ( log ` x ) x. ( 1 - ( # ` W ) ) ) ) )
220 213 217 219 3eqtrd 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( log ` x ) x. ( 2 - ( # ` W ) ) ) = ( ( log ` x ) + ( ( log ` x ) x. ( 1 - ( # ` W ) ) ) ) )
221 214 mul01d 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( log ` x ) x. 0 ) = 0 )
222 206 220 221 3brtr3d 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( log ` x ) + ( ( log ` x ) x. ( 1 - ( # ` W ) ) ) ) <_ 0 )
223 33 nnred 
 |-  ( ph -> ( phi ` N ) e. RR )
224 223 ad2antrr 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( phi ` N ) e. RR )
225 49 ad2ant2r 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( `' L " { ( 1r ` Z ) } ) ) ( ( Lam ` n ) / n ) e. RR )
226 34 ad2antrr 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( phi ` N ) e. NN0 )
227 226 nn0ge0d 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> 0 <_ ( phi ` N ) )
228 44 45 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( `' L " { ( 1r ` Z ) } ) ) ) -> ( Lam ` n ) e. RR )
229 vmage0 
 |-  ( n e. NN -> 0 <_ ( Lam ` n ) )
230 44 229 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( `' L " { ( 1r ` Z ) } ) ) ) -> 0 <_ ( Lam ` n ) )
231 44 nnred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( `' L " { ( 1r ` Z ) } ) ) ) -> n e. RR )
232 44 nngt0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( `' L " { ( 1r ` Z ) } ) ) ) -> 0 < n )
233 divge0 
 |-  ( ( ( ( Lam ` n ) e. RR /\ 0 <_ ( Lam ` n ) ) /\ ( n e. RR /\ 0 < n ) ) -> 0 <_ ( ( Lam ` n ) / n ) )
234 228 230 231 232 233 syl22anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( `' L " { ( 1r ` Z ) } ) ) ) -> 0 <_ ( ( Lam ` n ) / n ) )
235 40 48 234 fsumge0 
 |-  ( ( ph /\ x e. RR+ ) -> 0 <_ sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( `' L " { ( 1r ` Z ) } ) ) ( ( Lam ` n ) / n ) )
236 235 ad2ant2r 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> 0 <_ sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( `' L " { ( 1r ` Z ) } ) ) ( ( Lam ` n ) / n ) )
237 224 225 227 236 mulge0d 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> 0 <_ ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( `' L " { ( 1r ` Z ) } ) ) ( ( Lam ` n ) / n ) ) )
238 74 75 76 222 237 letrd 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( log ` x ) + ( ( log ` x ) x. ( 1 - ( # ` W ) ) ) ) <_ ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( `' L " { ( 1r ` Z ) } ) ) ( ( Lam ` n ) / n ) ) )
239 leaddsub 
 |-  ( ( ( log ` x ) e. RR /\ ( ( log ` x ) x. ( 1 - ( # ` W ) ) ) e. RR /\ ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( `' L " { ( 1r ` Z ) } ) ) ( ( Lam ` n ) / n ) ) e. RR ) -> ( ( ( log ` x ) + ( ( log ` x ) x. ( 1 - ( # ` W ) ) ) ) <_ ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( `' L " { ( 1r ` Z ) } ) ) ( ( Lam ` n ) / n ) ) <-> ( log ` x ) <_ ( ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( `' L " { ( 1r ` Z ) } ) ) ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. ( 1 - ( # ` W ) ) ) ) ) )
240 72 73 76 239 syl3anc 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( ( log ` x ) + ( ( log ` x ) x. ( 1 - ( # ` W ) ) ) ) <_ ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( `' L " { ( 1r ` Z ) } ) ) ( ( Lam ` n ) / n ) ) <-> ( log ` x ) <_ ( ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( `' L " { ( 1r ` Z ) } ) ) ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. ( 1 - ( # ` W ) ) ) ) ) )
241 238 240 mpbid 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( log ` x ) <_ ( ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( `' L " { ( 1r ` Z ) } ) ) ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. ( 1 - ( # ` W ) ) ) ) )
242 72 88 absidd 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( log ` x ) ) = ( log ` x ) )
243 67 ad2ant2r 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( `' L " { ( 1r ` Z ) } ) ) ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. ( 1 - ( # ` W ) ) ) ) e. RR )
244 75 72 243 88 241 letrd 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> 0 <_ ( ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( `' L " { ( 1r ` Z ) } ) ) ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. ( 1 - ( # ` W ) ) ) ) )
245 243 244 absidd 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( `' L " { ( 1r ` Z ) } ) ) ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. ( 1 - ( # ` W ) ) ) ) ) = ( ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( `' L " { ( 1r ` Z ) } ) ) ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. ( 1 - ( # ` W ) ) ) ) )
246 241 242 245 3brtr4d 
 |-  ( ( ( ph /\ ( * o. X ) =/= X ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( log ` x ) ) <_ ( abs ` ( ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i ( `' L " { ( 1r ` Z ) } ) ) ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. ( 1 - ( # ` W ) ) ) ) ) )
247 19 32 69 71 246 o1le 
 |-  ( ( ph /\ ( * o. X ) =/= X ) -> ( x e. RR+ |-> ( log ` x ) ) e. O(1) )
248 247 ex 
 |-  ( ph -> ( ( * o. X ) =/= X -> ( x e. RR+ |-> ( log ` x ) ) e. O(1) ) )
249 248 necon1bd 
 |-  ( ph -> ( -. ( x e. RR+ |-> ( log ` x ) ) e. O(1) -> ( * o. X ) = X ) )
250 18 249 mpi 
 |-  ( ph -> ( * o. X ) = X )
251 250 adantr 
 |-  ( ( ph /\ x e. ( Base ` Z ) ) -> ( * o. X ) = X )
252 251 fveq1d 
 |-  ( ( ph /\ x e. ( Base ` Z ) ) -> ( ( * o. X ) ` x ) = ( X ` x ) )
253 17 252 eqtr3d 
 |-  ( ( ph /\ x e. ( Base ` Z ) ) -> ( * ` ( X ` x ) ) = ( X ` x ) )
254 15 253 cjrebd 
 |-  ( ( ph /\ x e. ( Base ` Z ) ) -> ( X ` x ) e. RR )
255 254 ralrimiva 
 |-  ( ph -> A. x e. ( Base ` Z ) ( X ` x ) e. RR )
256 ffnfv 
 |-  ( X : ( Base ` Z ) --> RR <-> ( X Fn ( Base ` Z ) /\ A. x e. ( Base ` Z ) ( X ` x ) e. RR ) )
257 14 255 256 sylanbrc 
 |-  ( ph -> X : ( Base ` Z ) --> RR )