MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dchrisum0re Structured version   Unicode version

Theorem dchrisum0re 21209
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.)
Hypotheses
Ref Expression
rpvmasum.z  |-  Z  =  (ℤ/n `  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
Ref Expression
dchrisum0re  |-  ( ph  ->  X : ( Base `  Z ) --> RR )
Distinct variable groups:    y, m,  .1.    m, N, y    ph, m    m, Z, y    D, m, y    m, L, y   
m, X, y
Allowed substitution hints:    ph( y)    G( y, m)    W( y, m)

Proof of Theorem dchrisum0re
Dummy variables  k  n  x  f  c 
t  a are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rpvmasum2.g . . . 4  |-  G  =  (DChr `  N )
2 rpvmasum.z . . . 4  |-  Z  =  (ℤ/n `  N )
3 rpvmasum2.d . . . 4  |-  D  =  ( Base `  G
)
4 eqid 2438 . . . 4  |-  ( Base `  Z )  =  (
Base `  Z )
5 rpvmasum2.w . . . . . . 7  |-  W  =  { y  e.  ( D  \  {  .1.  } )  |  sum_ m  e.  NN  ( ( y `
 ( L `  m ) )  /  m )  =  0 }
6 ssrab2 3430 . . . . . . 7  |-  { y  e.  ( D  \  {  .1.  } )  | 
sum_ m  e.  NN  ( ( y `  ( L `  m ) )  /  m )  =  0 }  C_  ( D  \  {  .1.  } )
75, 6eqsstri 3380 . . . . . 6  |-  W  C_  ( D  \  {  .1.  } )
8 dchrisum0.b . . . . . 6  |-  ( ph  ->  X  e.  W )
97, 8sseldi 3348 . . . . 5  |-  ( ph  ->  X  e.  ( D 
\  {  .1.  }
) )
109eldifad 3334 . . . 4  |-  ( ph  ->  X  e.  D )
111, 2, 3, 4, 10dchrf 21028 . . 3  |-  ( ph  ->  X : ( Base `  Z ) --> CC )
12 ffn 5593 . . 3  |-  ( X : ( Base `  Z
) --> CC  ->  X  Fn  ( Base `  Z
) )
1311, 12syl 16 . 2  |-  ( ph  ->  X  Fn  ( Base `  Z ) )
1411ffvelrnda 5872 . . . 4  |-  ( (
ph  /\  x  e.  ( Base `  Z )
)  ->  ( X `  x )  e.  CC )
15 fvco3 5802 . . . . . 6  |-  ( ( X : ( Base `  Z ) --> CC  /\  x  e.  ( Base `  Z ) )  -> 
( ( *  o.  X ) `  x
)  =  ( * `
 ( X `  x ) ) )
1611, 15sylan 459 . . . . 5  |-  ( (
ph  /\  x  e.  ( Base `  Z )
)  ->  ( (
*  o.  X ) `
 x )  =  ( * `  ( X `  x )
) )
17 logno1 20529 . . . . . . . 8  |-  -.  (
x  e.  RR+  |->  ( log `  x ) )  e.  O ( 1 )
18 1re 9092 . . . . . . . . . . . 12  |-  1  e.  RR
1918a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  ( *  o.  X )  =/=  X
)  ->  1  e.  RR )
20 rpvmasum.l . . . . . . . . . . . . 13  |-  L  =  ( ZRHom `  Z
)
21 rpvmasum.a . . . . . . . . . . . . 13  |-  ( ph  ->  N  e.  NN )
22 rpvmasum2.1 . . . . . . . . . . . . 13  |-  .1.  =  ( 0g `  G )
23 eqid 2438 . . . . . . . . . . . . 13  |-  (Unit `  Z )  =  (Unit `  Z )
2421nnnn0d 10276 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  N  e.  NN0 )
252zncrng 16827 . . . . . . . . . . . . . . . 16  |-  ( N  e.  NN0  ->  Z  e. 
CRing )
2624, 25syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  Z  e.  CRing )
27 crngrng 15676 . . . . . . . . . . . . . . 15  |-  ( Z  e.  CRing  ->  Z  e.  Ring )
2826, 27syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  Z  e.  Ring )
29 eqid 2438 . . . . . . . . . . . . . . 15  |-  ( 1r
`  Z )  =  ( 1r `  Z
)
3023, 291unit 15765 . . . . . . . . . . . . . 14  |-  ( Z  e.  Ring  ->  ( 1r
`  Z )  e.  (Unit `  Z )
)
3128, 30syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1r `  Z
)  e.  (Unit `  Z ) )
32 eqid 2438 . . . . . . . . . . . . 13  |-  ( `' L " { ( 1r `  Z ) } )  =  ( `' L " { ( 1r `  Z ) } )
33 eqidd 2439 . . . . . . . . . . . . 13  |-  ( (
ph  /\  f  e.  W )  ->  ( 1r `  Z )  =  ( 1r `  Z
) )
342, 20, 21, 1, 3, 22, 5, 23, 31, 32, 33rpvmasum2 21208 . . . . . . . . . . . 12  |-  ( ph  ->  ( x  e.  RR+  |->  ( ( ( phi `  N )  x.  sum_ n  e.  ( ( 1 ... ( |_ `  x ) )  i^i  ( `' L " { ( 1r `  Z ) } ) ) ( (Λ `  n
)  /  n ) )  -  ( ( log `  x )  x.  ( 1  -  ( # `  W
) ) ) ) )  e.  O ( 1 ) )
3534adantr 453 . . . . . . . . . . 11  |-  ( (
ph  /\  ( *  o.  X )  =/=  X
)  ->  ( x  e.  RR+  |->  ( ( ( phi `  N )  x.  sum_ n  e.  ( ( 1 ... ( |_ `  x ) )  i^i  ( `' L " { ( 1r `  Z ) } ) ) ( (Λ `  n
)  /  n ) )  -  ( ( log `  x )  x.  ( 1  -  ( # `  W
) ) ) ) )  e.  O ( 1 ) )
3621phicld 13163 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( phi `  N
)  e.  NN )
3736nnnn0d 10276 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( phi `  N
)  e.  NN0 )
3837adantr 453 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( phi `  N )  e.  NN0 )
3938nn0red 10277 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( phi `  N )  e.  RR )
40 fzfid 11314 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( 1 ... ( |_ `  x ) )  e. 
Fin )
41 inss1 3563 . . . . . . . . . . . . . . . . 17  |-  ( ( 1 ... ( |_
`  x ) )  i^i  ( `' L " { ( 1r `  Z ) } ) )  C_  ( 1 ... ( |_ `  x ) )
42 ssfi 7331 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 1 ... ( |_ `  x ) )  e.  Fin  /\  (
( 1 ... ( |_ `  x ) )  i^i  ( `' L " { ( 1r `  Z ) } ) )  C_  ( 1 ... ( |_ `  x ) ) )  ->  ( ( 1 ... ( |_ `  x ) )  i^i  ( `' L " { ( 1r `  Z ) } ) )  e.  Fin )
4340, 41, 42sylancl 645 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
1 ... ( |_ `  x ) )  i^i  ( `' L " { ( 1r `  Z ) } ) )  e.  Fin )
4441sseli 3346 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  ( ( 1 ... ( |_ `  x ) )  i^i  ( `' L " { ( 1r `  Z ) } ) )  ->  n  e.  ( 1 ... ( |_ `  x ) ) )
45 elfznn 11082 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  NN )
4645adantl 454 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  NN )
4744, 46sylan2 462 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  ( `' L " { ( 1r `  Z ) } ) ) )  ->  n  e.  NN )
48 vmacl 20903 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  NN  ->  (Λ `  n )  e.  RR )
49 nndivre 10037 . . . . . . . . . . . . . . . . . 18  |-  ( ( (Λ `  n )  e.  RR  /\  n  e.  NN )  ->  (
(Λ `  n )  /  n )  e.  RR )
5048, 49mpancom 652 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  NN  ->  (
(Λ `  n )  /  n )  e.  RR )
5147, 50syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  ( `' L " { ( 1r `  Z ) } ) ) )  ->  ( (Λ `  n
)  /  n )  e.  RR )
5243, 51fsumrecl 12530 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  ( `' L " { ( 1r `  Z ) } ) ) ( (Λ `  n )  /  n )  e.  RR )
5339, 52remulcld 9118 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( phi `  N )  x. 
sum_ n  e.  (
( 1 ... ( |_ `  x ) )  i^i  ( `' L " { ( 1r `  Z ) } ) ) ( (Λ `  n
)  /  n ) )  e.  RR )
54 relogcl 20475 . . . . . . . . . . . . . . . 16  |-  ( x  e.  RR+  ->  ( log `  x )  e.  RR )
5554adantl 454 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( log `  x )  e.  RR )
561, 3dchrfi 21041 . . . . . . . . . . . . . . . . . . . . 21  |-  ( N  e.  NN  ->  D  e.  Fin )
5721, 56syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  D  e.  Fin )
58 difss 3476 . . . . . . . . . . . . . . . . . . . . 21  |-  ( D 
\  {  .1.  }
)  C_  D
597, 58sstri 3359 . . . . . . . . . . . . . . . . . . . 20  |-  W  C_  D
60 ssfi 7331 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( D  e.  Fin  /\  W  C_  D )  ->  W  e.  Fin )
6157, 59, 60sylancl 645 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  W  e.  Fin )
62 hashcl 11641 . . . . . . . . . . . . . . . . . . 19  |-  ( W  e.  Fin  ->  ( # `
 W )  e. 
NN0 )
6361, 62syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( # `  W
)  e.  NN0 )
6463nn0red 10277 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( # `  W
)  e.  RR )
65 resubcl 9367 . . . . . . . . . . . . . . . . 17  |-  ( ( 1  e.  RR  /\  ( # `  W )  e.  RR )  -> 
( 1  -  ( # `
 W ) )  e.  RR )
6618, 64, 65sylancr 646 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( 1  -  ( # `
 W ) )  e.  RR )
6766adantr 453 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( 1  -  ( # `  W
) )  e.  RR )
6855, 67remulcld 9118 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( log `  x )  x.  ( 1  -  ( # `
 W ) ) )  e.  RR )
6953, 68resubcld 9467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
( phi `  N
)  x.  sum_ n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  ( `' L " { ( 1r `  Z ) } ) ) ( (Λ `  n )  /  n ) )  -  ( ( log `  x
)  x.  ( 1  -  ( # `  W
) ) ) )  e.  RR )
7069recnd 9116 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
( phi `  N
)  x.  sum_ n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  ( `' L " { ( 1r `  Z ) } ) ) ( (Λ `  n )  /  n ) )  -  ( ( log `  x
)  x.  ( 1  -  ( # `  W
) ) ) )  e.  CC )
7170adantlr 697 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  x  e.  RR+ )  -> 
( ( ( phi `  N )  x.  sum_ n  e.  ( ( 1 ... ( |_ `  x ) )  i^i  ( `' L " { ( 1r `  Z ) } ) ) ( (Λ `  n
)  /  n ) )  -  ( ( log `  x )  x.  ( 1  -  ( # `  W
) ) ) )  e.  CC )
7254adantl 454 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  x  e.  RR+ )  -> 
( log `  x
)  e.  RR )
7372recnd 9116 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  x  e.  RR+ )  -> 
( log `  x
)  e.  CC )
7454ad2antrl 710 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( log `  x
)  e.  RR )
7568ad2ant2r 729 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( log `  x
)  x.  ( 1  -  ( # `  W
) ) )  e.  RR )
7674, 75readdcld 9117 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( log `  x
)  +  ( ( log `  x )  x.  ( 1  -  ( # `  W
) ) ) )  e.  RR )
77 0re 9093 . . . . . . . . . . . . . . 15  |-  0  e.  RR
7877a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
0  e.  RR )
7953ad2ant2r 729 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( phi `  N )  x.  sum_ n  e.  ( ( 1 ... ( |_ `  x ) )  i^i  ( `' L " { ( 1r `  Z ) } ) ) ( (Λ `  n
)  /  n ) )  e.  RR )
80 2re 10071 . . . . . . . . . . . . . . . . . 18  |-  2  e.  RR
8180a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
2  e.  RR )
8264ad2antrr 708 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( # `  W )  e.  RR )
8381, 82resubcld 9467 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( 2  -  ( # `
 W ) )  e.  RR )
84 log1 20482 . . . . . . . . . . . . . . . . 17  |-  ( log `  1 )  =  0
85 simprr 735 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
1  <_  x )
86 1rp 10618 . . . . . . . . . . . . . . . . . . 19  |-  1  e.  RR+
87 simprl 734 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  x  e.  RR+ )
88 logleb 20500 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 1  e.  RR+  /\  x  e.  RR+ )  ->  (
1  <_  x  <->  ( log `  1 )  <_  ( log `  x ) ) )
8986, 87, 88sylancr 646 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( 1  <_  x  <->  ( log `  1 )  <_  ( log `  x
) ) )
9085, 89mpbid 203 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( log `  1
)  <_  ( log `  x ) )
9184, 90syl5eqbrr 4248 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
0  <_  ( log `  x ) )
92 simplr 733 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( *  o.  X
)  =/=  X )
93 eqid 2438 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( inv g `  G )  =  ( inv g `  G )
941, 3, 10, 93dchrinv 21047 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( ( inv g `  G ) `  X
)  =  ( *  o.  X ) )
951dchrabl 21040 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( N  e.  NN  ->  G  e.  Abel )
9621, 95syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  G  e.  Abel )
97 ablgrp 15419 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( G  e.  Abel  ->  G  e. 
Grp )
9896, 97syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  G  e.  Grp )
993, 93grpinvcl 14852 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( G  e.  Grp  /\  X  e.  D )  ->  ( ( inv g `  G ) `  X
)  e.  D )
10098, 10, 99syl2anc 644 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( ( inv g `  G ) `  X
)  e.  D )
10194, 100eqeltrrd 2513 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( *  o.  X
)  e.  D )
102 eldifsni 3930 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( X  e.  ( D  \  {  .1.  } )  ->  X  =/=  .1.  )
1039, 102syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  X  =/=  .1.  )
1043, 22grpidcl 14835 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( G  e.  Grp  ->  .1.  e.  D )
10598, 104syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  .1.  e.  D )
1063, 93, 98, 10, 105grpinv11 14862 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( ( ( inv g `  G ) `
 X )  =  ( ( inv g `  G ) `  .1.  ) 
<->  X  =  .1.  )
)
107106necon3bid 2638 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( ( ( inv g `  G ) `
 X )  =/=  ( ( inv g `  G ) `  .1.  ) 
<->  X  =/=  .1.  )
)
108103, 107mpbird 225 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( ( inv g `  G ) `  X
)  =/=  ( ( inv g `  G
) `  .1.  )
)
10922, 93grpinvid 14858 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( G  e.  Grp  ->  (
( inv g `  G ) `  .1.  )  =  .1.  )
11098, 109syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( ( inv g `  G ) `  .1.  )  =  .1.  )
111108, 94, 1103netr3d 2629 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( *  o.  X
)  =/=  .1.  )
112 eldifsn 3929 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( *  o.  X )  e.  ( D  \  {  .1.  } )  <->  ( (
*  o.  X )  e.  D  /\  (
*  o.  X )  =/=  .1.  ) )
113101, 111, 112sylanbrc 647 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( *  o.  X
)  e.  ( D 
\  {  .1.  }
) )
114 nnuz 10523 . . . . . . . . . . . . . . . . . . . . . . 23  |-  NN  =  ( ZZ>= `  1 )
115 1z 10313 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  1  e.  ZZ
116115a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  1  e.  ZZ )
117 fveq2 5730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( n  =  m  ->  ( L `  n )  =  ( L `  m ) )
118117fveq2d 5734 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( n  =  m  ->  ( X `  ( L `  n ) )  =  ( X `  ( L `  m )
) )
119 id 21 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( n  =  m  ->  n  =  m )
120118, 119oveq12d 6101 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( n  =  m  ->  (
( X `  ( L `  n )
)  /  n )  =  ( ( X `
 ( L `  m ) )  /  m ) )
121120fveq2d 5734 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( n  =  m  ->  (
* `  ( ( X `  ( L `  n ) )  /  n ) )  =  ( * `  (
( X `  ( L `  m )
)  /  m ) ) )
122 eqid 2438 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( n  e.  NN  |->  ( * `
 ( ( X `
 ( L `  n ) )  /  n ) ) )  =  ( n  e.  NN  |->  ( * `  ( ( X `  ( L `  n ) )  /  n ) ) )
123 fvex 5744 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( * `
 ( ( X `
 ( L `  m ) )  /  m ) )  e. 
_V
124121, 122, 123fvmpt 5808 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( m  e.  NN  ->  (
( n  e.  NN  |->  ( * `  (
( X `  ( L `  n )
)  /  n ) ) ) `  m
)  =  ( * `
 ( ( X `
 ( L `  m ) )  /  m ) ) )
125124adantl 454 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  m  e.  NN )  ->  ( ( n  e.  NN  |->  ( * `  ( ( X `  ( L `
 n ) )  /  n ) ) ) `  m )  =  ( * `  ( ( X `  ( L `  m ) )  /  m ) ) )
126 nnre 10009 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( m  e.  NN  ->  m  e.  RR )
127126adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  m  e.  NN )  ->  m  e.  RR )
128127cjred 12033 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  m  e.  NN )  ->  ( * `
 m )  =  m )
129128oveq2d 6099 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  m  e.  NN )  ->  ( ( * `  ( X `
 ( L `  m ) ) )  /  ( * `  m ) )  =  ( ( * `  ( X `  ( L `
 m ) ) )  /  m ) )
13011adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  m  e.  NN )  ->  X :
( Base `  Z ) --> CC )
1312, 4, 20znzrhfo 16830 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( N  e.  NN0  ->  L : ZZ -onto-> ( Base `  Z
) )
13224, 131syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  L : ZZ -onto-> ( Base `  Z ) )
133 fof 5655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( L : ZZ -onto-> ( Base `  Z )  ->  L : ZZ --> ( Base `  Z
) )
134132, 133syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  L : ZZ --> ( Base `  Z ) )
135 nnz 10305 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( m  e.  NN  ->  m  e.  ZZ )
136 ffvelrn 5870 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( L : ZZ --> ( Base `  Z )  /\  m  e.  ZZ )  ->  ( L `  m )  e.  ( Base `  Z
) )
137134, 135, 136syl2an 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  m  e.  NN )  ->  ( L `
 m )  e.  ( Base `  Z
) )
138130, 137ffvelrnd 5873 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  m  e.  NN )  ->  ( X `
 ( L `  m ) )  e.  CC )
139 nncn 10010 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( m  e.  NN  ->  m  e.  CC )
140139adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  m  e.  NN )  ->  m  e.  CC )
141 nnne0 10034 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( m  e.  NN  ->  m  =/=  0 )
142141adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  m  e.  NN )  ->  m  =/=  0 )
143138, 140, 142cjdivd 12030 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  m  e.  NN )  ->  ( * `
 ( ( X `
 ( L `  m ) )  /  m ) )  =  ( ( * `  ( X `  ( L `
 m ) ) )  /  ( * `
 m ) ) )
144 fvco3 5802 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( X : ( Base `  Z ) --> CC  /\  ( L `  m )  e.  ( Base `  Z
) )  ->  (
( *  o.  X
) `  ( L `  m ) )  =  ( * `  ( X `  ( L `  m ) ) ) )
145130, 137, 144syl2anc 644 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  m  e.  NN )  ->  ( ( *  o.  X ) `
 ( L `  m ) )  =  ( * `  ( X `  ( L `  m ) ) ) )
146145oveq1d 6098 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  m  e.  NN )  ->  ( ( ( *  o.  X
) `  ( L `  m ) )  /  m )  =  ( ( * `  ( X `  ( L `  m ) ) )  /  m ) )
147129, 143, 1463eqtr4d 2480 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  m  e.  NN )  ->  ( * `
 ( ( X `
 ( L `  m ) )  /  m ) )  =  ( ( ( *  o.  X ) `  ( L `  m ) )  /  m ) )
148125, 147eqtrd 2470 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  NN )  ->  ( ( n  e.  NN  |->  ( * `  ( ( X `  ( L `
 n ) )  /  n ) ) ) `  m )  =  ( ( ( *  o.  X ) `
 ( L `  m ) )  /  m ) )
149138cjcld 12003 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  m  e.  NN )  ->  ( * `
 ( X `  ( L `  m ) ) )  e.  CC )
150149, 140, 142divcld 9792 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  m  e.  NN )  ->  ( ( * `  ( X `
 ( L `  m ) ) )  /  m )  e.  CC )
151146, 150eqeltrd 2512 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  NN )  ->  ( ( ( *  o.  X
) `  ( L `  m ) )  /  m )  e.  CC )
152 eqid 2438 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( a  e.  NN  |->  ( ( X `  ( L `
 a ) )  /  a ) )  =  ( a  e.  NN  |->  ( ( X `
 ( L `  a ) )  / 
a ) )
1532, 20, 21, 1, 3, 22, 10, 103, 152dchrmusumlema 21189 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 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 ) ) )
154 simprrl 742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
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 )
1558adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
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 )
15621adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
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 )
15710adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
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 )
158103adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
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.  )
159 simprl 734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
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 ) )
160 simprrr 743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
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 ) )
1612, 20, 156, 1, 3, 22, 157, 158, 152, 159, 154, 160, 5dchrvmaeq0 21200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
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 ) )
162155, 161mpbid 203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
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 )
163154, 162breqtrd 4238 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
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 )
164163rexlimdvaa 2833 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( 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 ) )
165164exlimdv 1647 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 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 ) )
166153, 165mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  seq  1 (  +  ,  ( a  e.  NN  |->  ( ( X `
 ( L `  a ) )  / 
a ) ) )  ~~>  0 )
167 seqex 11327 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  seq  1
(  +  ,  ( n  e.  NN  |->  ( * `  ( ( X `  ( L `
 n ) )  /  n ) ) ) )  e.  _V
168167a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  seq  1 (  +  ,  ( n  e.  NN  |->  ( * `  ( ( X `  ( L `  n ) )  /  n ) ) ) )  e. 
_V )
169 fveq2 5730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( a  =  m  ->  ( L `  a )  =  ( L `  m ) )
170169fveq2d 5734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( a  =  m  ->  ( X `  ( L `  a ) )  =  ( X `  ( L `  m )
) )
171 id 21 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( a  =  m  ->  a  =  m )
172170, 171oveq12d 6101 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( a  =  m  ->  (
( X `  ( L `  a )
)  /  a )  =  ( ( X `
 ( L `  m ) )  /  m ) )
173 ovex 6108 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( X `  ( L `
 m ) )  /  m )  e. 
_V
174172, 152, 173fvmpt 5808 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( m  e.  NN  ->  (
( a  e.  NN  |->  ( ( X `  ( L `  a ) )  /  a ) ) `  m )  =  ( ( X `
 ( L `  m ) )  /  m ) )
175174adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  m  e.  NN )  ->  ( ( a  e.  NN  |->  ( ( X `  ( L `  a )
)  /  a ) ) `  m )  =  ( ( X `
 ( L `  m ) )  /  m ) )
176138, 140, 142divcld 9792 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  m  e.  NN )  ->  ( ( X `  ( L `
 m ) )  /  m )  e.  CC )
177175, 176eqeltrd 2512 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  m  e.  NN )  ->  ( ( a  e.  NN  |->  ( ( X `  ( L `  a )
)  /  a ) ) `  m )  e.  CC )
178114, 116, 177serf 11353 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  seq  1 (  +  ,  ( a  e.  NN  |->  ( ( X `
 ( L `  a ) )  / 
a ) ) ) : NN --> CC )
179178ffvelrnda 5872 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  k  e.  NN )  ->  (  seq  1 (  +  , 
( a  e.  NN  |->  ( ( X `  ( L `  a ) )  /  a ) ) ) `  k
)  e.  CC )
180 fzfid 11314 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  k  e.  NN )  ->  ( 1 ... k )  e. 
Fin )
181 simpl 445 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  k  e.  NN )  ->  ph )
182 elfznn 11082 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( m  e.  ( 1 ... k )  ->  m  e.  NN )
183181, 182, 176syl2an 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  k  e.  NN )  /\  m  e.  ( 1 ... k
) )  ->  (
( X `  ( L `  m )
)  /  m )  e.  CC )
184180, 183fsumcj 12591 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  k  e.  NN )  ->  ( * `
 sum_ m  e.  ( 1 ... k ) ( ( X `  ( L `  m ) )  /  m ) )  =  sum_ m  e.  ( 1 ... k
) ( * `  ( ( X `  ( L `  m ) )  /  m ) ) )
185181, 182, 175syl2an 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  k  e.  NN )  /\  m  e.  ( 1 ... k
) )  ->  (
( a  e.  NN  |->  ( ( X `  ( L `  a ) )  /  a ) ) `  m )  =  ( ( X `
 ( L `  m ) )  /  m ) )
186 simpr 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  NN )
187186, 114syl6eleq 2528 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  ( ZZ>= `  1 )
)
188185, 187, 183fsumser 12526 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  k  e.  NN )  ->  sum_ m  e.  ( 1 ... k
) ( ( X `
 ( L `  m ) )  /  m )  =  (  seq  1 (  +  ,  ( a  e.  NN  |->  ( ( X `
 ( L `  a ) )  / 
a ) ) ) `
 k ) )
189188fveq2d 5734 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  k  e.  NN )  ->  ( * `
 sum_ m  e.  ( 1 ... k ) ( ( X `  ( L `  m ) )  /  m ) )  =  ( * `
 (  seq  1
(  +  ,  ( a  e.  NN  |->  ( ( X `  ( L `  a )
)  /  a ) ) ) `  k
) ) )
190181, 182, 125syl2an 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  k  e.  NN )  /\  m  e.  ( 1 ... k
) )  ->  (
( n  e.  NN  |->  ( * `  (
( X `  ( L `  n )
)  /  n ) ) ) `  m
)  =  ( * `
 ( ( X `
 ( L `  m ) )  /  m ) ) )
191176cjcld 12003 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  m  e.  NN )  ->  ( * `
 ( ( X `
 ( L `  m ) )  /  m ) )  e.  CC )
192181, 182, 191syl2an 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  k  e.  NN )  /\  m  e.  ( 1 ... k
) )  ->  (
* `  ( ( X `  ( L `  m ) )  /  m ) )  e.  CC )
193190, 187, 192fsumser 12526 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  k  e.  NN )  ->  sum_ m  e.  ( 1 ... k
) ( * `  ( ( X `  ( L `  m ) )  /  m ) )  =  (  seq  1 (  +  , 
( n  e.  NN  |->  ( * `  (
( X `  ( L `  n )
)  /  n ) ) ) ) `  k ) )
194184, 189, 1933eqtr3rd 2479 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  k  e.  NN )  ->  (  seq  1 (  +  , 
( n  e.  NN  |->  ( * `  (
( X `  ( L `  n )
)  /  n ) ) ) ) `  k )  =  ( * `  (  seq  1 (  +  , 
( a  e.  NN  |->  ( ( X `  ( L `  a ) )  /  a ) ) ) `  k
) ) )
195114, 166, 168, 116, 179, 194climcj 12400 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  seq  1 (  +  ,  ( n  e.  NN  |->  ( * `  ( ( X `  ( L `  n ) )  /  n ) ) ) )  ~~>  ( * `
 0 ) )
196 cj0 11965 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( * `
 0 )  =  0
197195, 196syl6breq 4253 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  seq  1 (  +  ,  ( n  e.  NN  |->  ( * `  ( ( X `  ( L `  n ) )  /  n ) ) ) )  ~~>  0 )
198114, 116, 148, 151, 197isumclim 12543 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  -> 
sum_ m  e.  NN  ( ( ( *  o.  X ) `  ( L `  m ) )  /  m )  =  0 )
199 fveq1 5729 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  =  ( *  o.  X )  ->  (
y `  ( L `  m ) )  =  ( ( *  o.  X ) `  ( L `  m )
) )
200199oveq1d 6098 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  ( *  o.  X )  ->  (
( y `  ( L `  m )
)  /  m )  =  ( ( ( *  o.  X ) `
 ( L `  m ) )  /  m ) )
201200sumeq2sdv 12500 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  ( *  o.  X )  ->  sum_ m  e.  NN  ( ( y `
 ( L `  m ) )  /  m )  =  sum_ m  e.  NN  ( ( ( *  o.  X
) `  ( L `  m ) )  /  m ) )
202201eqeq1d 2446 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  =  ( *  o.  X )  ->  ( sum_ m  e.  NN  (
( y `  ( L `  m )
)  /  m )  =  0  <->  sum_ m  e.  NN  ( ( ( *  o.  X ) `
 ( L `  m ) )  /  m )  =  0 ) )
203202, 5elrab2 3096 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( *  o.  X )  e.  W  <->  ( (
*  o.  X )  e.  ( D  \  {  .1.  } )  /\  sum_
m  e.  NN  (
( ( *  o.  X ) `  ( L `  m )
)  /  m )  =  0 ) )
204113, 198, 203sylanbrc 647 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( *  o.  X
)  e.  W )
205204ad2antrr 708 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( *  o.  X
)  e.  W )
2068ad2antrr 708 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  X  e.  W )
207 hashprg 11668 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( *  o.  X
)  e.  W  /\  X  e.  W )  ->  ( ( *  o.  X )  =/=  X  <->  (
# `  { (
*  o.  X ) ,  X } )  =  2 ) )
208205, 206, 207syl2anc 644 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( *  o.  X )  =/=  X  <->  (
# `  { (
*  o.  X ) ,  X } )  =  2 ) )
20992, 208mpbid 203 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( # `  { ( *  o.  X ) ,  X } )  =  2 )
21061ad2antrr 708 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  W  e.  Fin )
211 prssi 3956 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( *  o.  X
)  e.  W  /\  X  e.  W )  ->  { ( *  o.  X ) ,  X }  C_  W )
212205, 206, 211syl2anc 644 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  { ( *  o.  X ) ,  X }  C_  W )
213 ssdomg 7155 . . . . . . . . . . . . . . . . . . . 20  |-  ( W  e.  Fin  ->  ( { ( *  o.  X ) ,  X }  C_  W  ->  { ( *  o.  X ) ,  X }  ~<_  W ) )
214210, 212, 213sylc 59 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  { ( *  o.  X ) ,  X }  ~<_  W )
215 hashdomi 11656 . . . . . . . . . . . . . . . . . . 19  |-  ( { ( *  o.  X
) ,  X }  ~<_  W  ->  ( # `  {
( *  o.  X
) ,  X }
)  <_  ( # `  W
) )
216214, 215syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( # `  { ( *  o.  X ) ,  X } )  <_  ( # `  W
) )
217209, 216eqbrtrrd 4236 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
2  <_  ( # `  W
) )
218 suble0 9544 . . . . . . . . . . . . . . . . . 18  |-  ( ( 2  e.  RR  /\  ( # `  W )  e.  RR )  -> 
( ( 2  -  ( # `  W
) )  <_  0  <->  2  <_  ( # `  W
) ) )
21980, 82, 218sylancr 646 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( 2  -  ( # `  W
) )  <_  0  <->  2  <_  ( # `  W
) ) )
220217, 219mpbird 225 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( 2  -  ( # `
 W ) )  <_  0 )
22183, 78, 74, 91, 220lemul2ad 9953 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( log `  x
)  x.  ( 2  -  ( # `  W
) ) )  <_ 
( ( log `  x
)  x.  0 ) )
222 df-2 10060 . . . . . . . . . . . . . . . . . . 19  |-  2  =  ( 1  +  1 )
223222oveq1i 6093 . . . . . . . . . . . . . . . . . 18  |-  ( 2  -  ( # `  W
) )  =  ( ( 1  +  1 )  -  ( # `  W ) )
224 ax-1cn 9050 . . . . . . . . . . . . . . . . . . . 20  |-  1  e.  CC
225224a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
1  e.  CC )
22682recnd 9116 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( # `  W )  e.  CC )
227225, 225, 226addsubassd 9433 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( 1  +  1 )  -  ( # `
 W ) )  =  ( 1  +  ( 1  -  ( # `
 W ) ) ) )
228223, 227syl5eq 2482 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( 2  -  ( # `
 W ) )  =  ( 1  +  ( 1  -  ( # `
 W ) ) ) )
229228oveq2d 6099 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( log `  x
)  x.  ( 2  -  ( # `  W
) ) )  =  ( ( log `  x
)  x.  ( 1  +  ( 1  -  ( # `  W
) ) ) ) )
23073adantrr 699 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( log `  x
)  e.  CC )
23166ad2antrr 708 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( 1  -  ( # `
 W ) )  e.  RR )
232231recnd 9116 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( 1  -  ( # `
 W ) )  e.  CC )
233230, 225, 232adddid 9114 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( log `  x
)  x.  ( 1  +  ( 1  -  ( # `  W
) ) ) )  =  ( ( ( log `  x )  x.  1 )  +  ( ( log `  x
)  x.  ( 1  -  ( # `  W
) ) ) ) )
234230mulid1d 9107 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( log `  x
)  x.  1 )  =  ( log `  x
) )
235234oveq1d 6098 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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
) ) ) ) )
236229, 233, 2353eqtrd 2474 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( log `  x
)  x.  ( 2  -  ( # `  W
) ) )  =  ( ( log `  x
)  +  ( ( log `  x )  x.  ( 1  -  ( # `  W
) ) ) ) )
237230mul01d 9267 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( log `  x
)  x.  0 )  =  0 )
238221, 236, 2373brtr3d 4243 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( log `  x
)  +  ( ( log `  x )  x.  ( 1  -  ( # `  W
) ) ) )  <_  0 )
23936nnred 10017 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( phi `  N
)  e.  RR )
240239ad2antrr 708 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( phi `  N
)  e.  RR )
24152ad2ant2r 729 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  sum_ n  e.  ( ( 1 ... ( |_
`  x ) )  i^i  ( `' L " { ( 1r `  Z ) } ) ) ( (Λ `  n
)  /  n )  e.  RR )
24237ad2antrr 708 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( phi `  N
)  e.  NN0 )
243242nn0ge0d 10279 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
0  <_  ( phi `  N ) )
24447, 48syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  ( `' L " { ( 1r `  Z ) } ) ) )  ->  (Λ `  n )  e.  RR )
245 vmage0 20906 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  NN  ->  0  <_  (Λ `  n )
)
24647, 245syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  ( `' L " { ( 1r `  Z ) } ) ) )  ->  0  <_  (Λ `  n ) )
24747nnred 10017 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  ( `' L " { ( 1r `  Z ) } ) ) )  ->  n  e.  RR )
24847nngt0d 10045 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  ( `' L " { ( 1r `  Z ) } ) ) )  ->  0  <  n
)
249 divge0 9881 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( (Λ `  n
)  e.  RR  /\  0  <_  (Λ `  n )
)  /\  ( n  e.  RR  /\  0  < 
n ) )  -> 
0  <_  ( (Λ `  n )  /  n
) )
250244, 246, 247, 248, 249syl22anc 1186 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  ( `' L " { ( 1r `  Z ) } ) ) )  ->  0  <_  (
(Λ `  n )  /  n ) )
25143, 51, 250fsumge0 12576 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  RR+ )  ->  0  <_  sum_
n  e.  ( ( 1 ... ( |_
`  x ) )  i^i  ( `' L " { ( 1r `  Z ) } ) ) ( (Λ `  n
)  /  n ) )
252251ad2ant2r 729 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
0  <_  sum_ n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  ( `' L " { ( 1r `  Z ) } ) ) ( (Λ `  n )  /  n ) )
253240, 241, 243, 252mulge0d 9605 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
0  <_  ( ( phi `  N )  x. 
sum_ n  e.  (
( 1 ... ( |_ `  x ) )  i^i  ( `' L " { ( 1r `  Z ) } ) ) ( (Λ `  n
)  /  n ) ) )
25476, 78, 79, 238, 253letrd 9229 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) } ) ) ( (Λ `  n
)  /  n ) ) )
255 leaddsub 9506 . . . . . . . . . . . . . 14  |-  ( ( ( log `  x
)  e.  RR  /\  ( ( log `  x
)  x.  ( 1  -  ( # `  W
) ) )  e.  RR  /\  ( ( phi `  N )  x.  sum_ n  e.  ( ( 1 ... ( |_ `  x ) )  i^i  ( `' L " { ( 1r `  Z ) } ) ) ( (Λ `  n
)  /  n ) )  e.  RR )  ->  ( ( ( log `  x )  +  ( ( log `  x )  x.  (
1  -  ( # `  W ) ) ) )  <_  ( ( phi `  N )  x. 
sum_ n  e.  (
( 1 ... ( |_ `  x ) )  i^i  ( `' L " { ( 1r `  Z ) } ) ) ( (Λ `  n
)  /  n ) )  <->  ( log `  x
)  <_  ( (
( phi `  N
)  x.  sum_ n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  ( `' L " { ( 1r `  Z ) } ) ) ( (Λ `  n )  /  n ) )  -  ( ( log `  x
)  x.  ( 1  -  ( # `  W
) ) ) ) ) )
25674, 75, 79, 255syl3anc 1185 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) } ) ) ( (Λ `  n
)  /  n ) )  <->  ( log `  x
)  <_  ( (
( phi `  N
)  x.  sum_ n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  ( `' L " { ( 1r `  Z ) } ) ) ( (Λ `  n )  /  n ) )  -  ( ( log `  x
)  x.  ( 1  -  ( # `  W
) ) ) ) ) )
257254, 256mpbid 203 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( log `  x
)  <_  ( (
( phi `  N
)  x.  sum_ n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  ( `' L " { ( 1r `  Z ) } ) ) ( (Λ `  n )  /  n ) )  -  ( ( log `  x
)  x.  ( 1  -  ( # `  W
) ) ) ) )
25874, 91absidd 12227 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( abs `  ( log `  x ) )  =  ( log `  x
) )
25969ad2ant2r 729 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( ( phi `  N )  x.  sum_ n  e.  ( ( 1 ... ( |_ `  x ) )  i^i  ( `' L " { ( 1r `  Z ) } ) ) ( (Λ `  n
)  /  n ) )  -  ( ( log `  x )  x.  ( 1  -  ( # `  W
) ) ) )  e.  RR )
26078, 74, 259, 91, 257letrd 9229 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
0  <_  ( (
( phi `  N
)  x.  sum_ n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  ( `' L " { ( 1r `  Z ) } ) ) ( (Λ `  n )  /  n ) )  -  ( ( log `  x
)  x.  ( 1  -  ( # `  W
) ) ) ) )
261259, 260absidd 12227 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
*  o.  X )  =/=  X )  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( abs `  (
( ( phi `  N )  x.  sum_ n  e.  ( ( 1 ... ( |_ `  x ) )  i^i  ( `' L " { ( 1r `  Z ) } ) ) ( (Λ `  n
)  /  n ) )  -  ( ( log `  x )  x.  ( 1  -  ( # `  W
) ) ) ) )  =  ( ( ( phi `  N
)  x.  sum_ n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  ( `' L " { ( 1r `  Z ) } ) ) ( (Λ `  n )  /  n ) )  -  ( ( log `  x
)  x.  ( 1  -  ( # `  W
) ) ) ) )
262257, 258, 2613brtr4d 4244 . . . . . . . . . . 11  |-  ( ( ( 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 ) } ) ) ( (Λ `  n
)  /  n ) )  -  ( ( log `  x )  x.  ( 1  -  ( # `  W
) ) ) ) ) )
26319, 35, 71, 73, 262o1le 12448 . . . . . . . . . 10  |-  ( (
ph  /\  ( *  o.  X )  =/=  X
)  ->  ( x  e.  RR+  |->  ( log `  x
) )  e.  O
( 1 ) )
264263ex 425 . . . . . . . . 9  |-  ( ph  ->  ( ( *  o.  X )  =/=  X  ->  ( x  e.  RR+  |->  ( log `  x ) )  e.  O ( 1 ) ) )
265264necon1bd 2674 . . . . . . . 8  |-  ( ph  ->  ( -.  ( x  e.  RR+  |->  ( log `  x ) )  e.  O ( 1 )  ->  ( *  o.  X )  =  X ) )
26617, 265mpi 17 . . . . . . 7  |-  ( ph  ->  ( *  o.  X
)  =  X )
267266adantr 453 . . . . . 6  |-  ( (
ph  /\  x  e.  ( Base `  Z )
)  ->  ( *  o.  X )  =  X )
268267fveq1d 5732 . . . . 5  |-  ( (
ph  /\  x  e.  ( Base `  Z )
)  ->  ( (
*  o.  X ) `
 x )  =  ( X `  x
) )
26916, 268eqtr3d 2472 . . . 4  |-  ( (
ph  /\  x  e.  ( Base `  Z )
)  ->  ( * `  ( X `  x
) )  =  ( X `  x ) )
27014, 269cjrebd 12009 . . 3  |-  ( (
ph  /\  x  e.  ( Base `  Z )
)  ->  ( X `  x )  e.  RR )
271270ralrimiva 2791 . 2  |-  ( ph  ->  A. x  e.  (
Base `  Z )
( X `  x
)  e.  RR )
272 ffnfv 5896 . 2  |-  ( X : ( Base `  Z
) --> RR  <->  ( X  Fn  ( Base `  Z
)  /\  A. x  e.  ( Base `  Z
) ( X `  x )  e.  RR ) )
27313, 271, 272sylanbrc 647 1  |-  ( ph  ->  X : ( Base `  Z ) --> RR )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 178    /\ wa 360   E.wex 1551    = wceq 1653    e. wcel 1726    =/= wne 2601   A.wral 2707   E.wrex 2708   {crab 2711   _Vcvv 2958    \ cdif 3319    i^i cin 3321    C_ wss 3322   {csn 3816   {cpr 3817   class class class wbr 4214    e. cmpt 4268   `'ccnv 4879   "cima 4883    o. ccom 4884    Fn wfn 5451   -->wf 5452   -onto->wfo 5454   ` cfv 5456  (class class class)co 6083    ~<_ cdom 7109   Fincfn 7111   CCcc 8990   RRcr 8991   0cc0 8992   1c1 8993    + caddc 8995    x. cmul 8997    +oocpnf 9119    < clt 9122    <_ cle 9123    - cmin 9293    / cdiv 9679   NNcn 10002   2c2 10051   NN0cn0 10223   ZZcz 10284   ZZ>=cuz 10490   RR+crp 10614   [,)cico 10920   ...cfz 11045   |_cfl 11203    seq cseq 11325   #chash 11620   *ccj 11903   abscabs 12041    ~~> cli 12280   O (
1 )co1 12282   sum_csu 12481   phicphi 13155   Basecbs 13471   0gc0g 13725   Grpcgrp 14687   inv gcminusg 14688   Abelcabel 15415   Ringcrg 15662   CRingccrg 15663   1rcur 15664  Unitcui 15746   ZRHomczrh 16780  ℤ/nczn 16783   logclog 20454  Λcvma 20876  DChrcdchr 21018
This theorem is referenced by:  dchrisum0  21216
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-rep 4322  ax-sep 4332  ax-nul 4340  ax-pow 4379  ax-pr 4405  ax-un 4703  ax-inf2 7598  ax-cnex 9048  ax-resscn 9049  ax-1cn 9050  ax-icn 9051  ax-addcl 9052  ax-addrcl 9053  ax-mulcl 9054  ax-mulrcl 9055  ax-mulcom 9056  ax-addass 9057  ax-mulass 9058  ax-distr 9059  ax-i2m1 9060  ax-1ne0 9061  ax-1rid 9062  ax-rnegex 9063  ax-rrecex 9064  ax-cnre 9065  ax-pre-lttri 9066  ax-pre-lttrn 9067  ax-pre-ltadd 9068  ax-pre-mulgt0 9069  ax-pre-sup 9070  ax-addf 9071  ax-mulf 9072
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-fal 1330  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2712  df-rex 2713  df-reu 2714  df-rmo 2715  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-pss 3338  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-tp 3824  df-op 3825  df-uni 4018  df-int 4053  df-iun 4097  df-iin 4098  df-disj 4185  df-br 4215  df-opab 4269  df-mpt 4270  df-tr 4305  df-eprel 4496  df-id 4500  df-po 4505  df-so 4506  df-fr 4543  df-se 4544  df-we 4545  df-ord 4586  df-on 4587  df-lim 4588  df-suc 4589  df-om 4848  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-iota 5420  df-fun 5458  df-fn 5459  df-f 5460  df-f1 5461  df-fo 5462  df-f1o 5463  df-fv 5464  df-isom 5465  df-ov 6086  df-oprab 6087  df-mpt2 6088  df-of 6307  df-1st 6351  df-2nd 6352  df-tpos 6481  df-rpss 6524  df-riota 6551  df-recs 6635  df-rdg 6670  df-1o 6726  df-2o 6727  df-oadd 6730  df-omul 6731  df-er 6907  df-ec 6909  df-qs 6913  df-map 7022  df-pm 7023  df-ixp 7066  df-en 7112  df-dom 7113  df-sdom 7114  df-fin 7115  df-fi 7418  df-sup 7448  df-oi 7481  df-card 7828  df-acn 7831  df-cda 8050  df-pnf 9124  df-mnf 9125  df-xr 9126  df-ltxr 9127  df-le 9128  df-sub 9295  df-neg 9296  df-div 9680  df-nn 10003  df-2 10060  df-3 10061  df-4 10062  df-5 10063  df-6 10064  df-7 10065  df-8 10066  df-9 10067  df-10 10068  df-n0 10224  df-z 10285  df-dec 10385  df-uz 10491  df-q 10577  df-rp 10615  df-xneg 10712  df-xadd 10713  df-xmul 10714  df-ioo 10922  df-ioc 10923  df-ico 10924  df-icc 10925  df-fz 11046  df-fzo 11138  df-fl 11204  df-mod 11253  df-seq 11326  df-exp 11385  df-fac 11569  df-bc 11596  df-hash 11621  df-word 11725  df-concat 11726  df-s1 11727  df-shft 11884  df-cj 11906  df-re 11907  df-im 11908  df-sqr 12042  df-abs 12043  df-limsup 12267  df-clim 12284  df-rlim 12285  df-o1 12286  df-lo1 12287  df-sum 12482  df-ef 12672  df-e 12673  df-sin 12674  df-cos 12675  df-pi 12677  df-dvds 12855  df-gcd 13009  df-prm 13082  df-phi 13157  df-pc 13213  df-struct 13473  df-ndx 13474  df-slot 13475  df-base 13476  df-sets 13477  df-ress 13478  df-plusg 13544  df-mulr 13545  df-starv 13546  df-sca 13547  df-vsca 13548  df-tset 13550  df-ple 13551  df-ds 13553  df-unif 13554  df-hom 13555  df-cco 13556  df-rest 13652  df-topn 13653  df-topgen 13669  df-pt 13670  df-prds 13673  df-xrs 13728  df-0g 13729  df-gsum 13730  df-qtop 13735  df-imas 13736  df-divs 13737  df-xps 13738  df-mre 13813  df-mrc 13814  df-acs 13816  df-mnd 14692  df-mhm 14740  df-submnd 14741  df-grp 14814  df-minusg 14815  df-sbg 14816  df-mulg 14817  df-subg 14943  df-nsg 14944  df-eqg 14945  df-ghm 15006  df-gim 15048  df-ga 15069  df-cntz 15118  df-oppg 15144  df-od 15169  df-gex 15170  df-pgp 15171  df-lsm 15272  df-pj1 15273  df-cmn 15416  df-abl 15417  df-cyg 15490  df-dprd 15558  df-dpj 15559  df-mgp 15651  df-rng 15665  df-cring 15666  df-ur 15667  df-oppr 15730  df-dvdsr 15748  df-unit 15749  df-invr 15779  df-dvr 15790  df-rnghom 15821  df-drng 15839  df-subrg 15868  df-lmod 15954  df-lss 16011  df-lsp 16050  df-sra 16246  df-rgmod 16247  df-lidl 16248  df-rsp 16249  df-2idl 16305  df-psmet 16696  df-xmet 16697  df-met 16698  df-bl 16699  df-mopn 16700  df-fbas 16701  df-fg 16702  df-cnfld 16706  df-zrh 16784  df-zn 16787  df-top 16965  df-bases 16967  df-topon 16968  df-topsp 16969  df-cld 17085  df-ntr 17086  df-cls 17087  df-nei 17164  df-lp 17202  df-perf 17203  df-cn 17293  df-cnp 17294  df-haus 17381  df-cmp 17452  df-tx 17596  df-hmeo 17789  df-fil 17880  df-fm 17972  df-flim 17973  df-flf 17974  df-xms 18352  df-ms 18353  df-tms 18354  df-cncf 18910  df-0p 19564  df-limc 19755  df-dv 19756  df-ply 20109  df-idp 20110  df-coe 20111  df-dgr 20112  df-quot 20210  df-log 20456  df-cxp 20457  df-em 20833  df-cht 20881  df-vma 20882  df-chp 20883  df-ppi 20884  df-mu 20885  df-dchr 21019
  Copyright terms: Public domain W3C validator