Metamath Proof Explorer

Theorem lgamgulmlem5

Description: Lemma for lgamgulm . (Contributed by Mario Carneiro, 3-Jul-2017)

Ref Expression
Hypotheses lgamgulm.r 
|- ( ph -> R e. NN )
lgamgulm.u 
|- U = { x e. CC | ( ( abs ` x ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) ) }
lgamgulm.g 
|- G = ( m e. NN |-> ( z e. U |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) )
lgamgulm.t 
|- T = ( m e. NN |-> if ( ( 2 x. R ) <_ m , ( R x. ( ( 2 x. ( R + 1 ) ) / ( m ^ 2 ) ) ) , ( ( R x. ( log ` ( ( m + 1 ) / m ) ) ) + ( ( log ` ( ( R + 1 ) x. m ) ) + _pi ) ) ) )
Assertion lgamgulmlem5 
|- ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( abs ` ( ( G ` n ) ` y ) ) <_ ( T ` n ) )

Proof

Step Hyp Ref Expression
1 lgamgulm.r 
 |-  ( ph -> R e. NN )
2 lgamgulm.u 
 |-  U = { x e. CC | ( ( abs ` x ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) ) }
3 lgamgulm.g 
 |-  G = ( m e. NN |-> ( z e. U |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) )
4 lgamgulm.t 
 |-  T = ( m e. NN |-> if ( ( 2 x. R ) <_ m , ( R x. ( ( 2 x. ( R + 1 ) ) / ( m ^ 2 ) ) ) , ( ( R x. ( log ` ( ( m + 1 ) / m ) ) ) + ( ( log ` ( ( R + 1 ) x. m ) ) + _pi ) ) ) )
5 breq2 
 |-  ( ( R x. ( ( 2 x. ( R + 1 ) ) / ( n ^ 2 ) ) ) = if ( ( 2 x. R ) <_ n , ( R x. ( ( 2 x. ( R + 1 ) ) / ( n ^ 2 ) ) ) , ( ( R x. ( log ` ( ( n + 1 ) / n ) ) ) + ( ( log ` ( ( R + 1 ) x. n ) ) + _pi ) ) ) -> ( ( abs ` ( ( y x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( y / n ) + 1 ) ) ) ) <_ ( R x. ( ( 2 x. ( R + 1 ) ) / ( n ^ 2 ) ) ) <-> ( abs ` ( ( y x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( y / n ) + 1 ) ) ) ) <_ if ( ( 2 x. R ) <_ n , ( R x. ( ( 2 x. ( R + 1 ) ) / ( n ^ 2 ) ) ) , ( ( R x. ( log ` ( ( n + 1 ) / n ) ) ) + ( ( log ` ( ( R + 1 ) x. n ) ) + _pi ) ) ) ) )
6 breq2 
 |-  ( ( ( R x. ( log ` ( ( n + 1 ) / n ) ) ) + ( ( log ` ( ( R + 1 ) x. n ) ) + _pi ) ) = if ( ( 2 x. R ) <_ n , ( R x. ( ( 2 x. ( R + 1 ) ) / ( n ^ 2 ) ) ) , ( ( R x. ( log ` ( ( n + 1 ) / n ) ) ) + ( ( log ` ( ( R + 1 ) x. n ) ) + _pi ) ) ) -> ( ( abs ` ( ( y x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( y / n ) + 1 ) ) ) ) <_ ( ( R x. ( log ` ( ( n + 1 ) / n ) ) ) + ( ( log ` ( ( R + 1 ) x. n ) ) + _pi ) ) <-> ( abs ` ( ( y x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( y / n ) + 1 ) ) ) ) <_ if ( ( 2 x. R ) <_ n , ( R x. ( ( 2 x. ( R + 1 ) ) / ( n ^ 2 ) ) ) , ( ( R x. ( log ` ( ( n + 1 ) / n ) ) ) + ( ( log ` ( ( R + 1 ) x. n ) ) + _pi ) ) ) ) )
7 1 adantr 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> R e. NN )
8 7 adantr 
 |-  ( ( ( ph /\ ( n e. NN /\ y e. U ) ) /\ ( 2 x. R ) <_ n ) -> R e. NN )
9 fveq2 
 |-  ( x = t -> ( abs ` x ) = ( abs ` t ) )
10 9 breq1d 
 |-  ( x = t -> ( ( abs ` x ) <_ R <-> ( abs ` t ) <_ R ) )
11 fvoveq1 
 |-  ( x = t -> ( abs ` ( x + k ) ) = ( abs ` ( t + k ) ) )
12 11 breq2d 
 |-  ( x = t -> ( ( 1 / R ) <_ ( abs ` ( x + k ) ) <-> ( 1 / R ) <_ ( abs ` ( t + k ) ) ) )
13 12 ralbidv 
 |-  ( x = t -> ( A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) <-> A. k e. NN0 ( 1 / R ) <_ ( abs ` ( t + k ) ) ) )
14 10 13 anbi12d 
 |-  ( x = t -> ( ( ( abs ` x ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) ) <-> ( ( abs ` t ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( t + k ) ) ) ) )
15 14 cbvrabv 
 |-  { x e. CC | ( ( abs ` x ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) ) } = { t e. CC | ( ( abs ` t ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( t + k ) ) ) }
16 2 15 eqtri 
 |-  U = { t e. CC | ( ( abs ` t ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( t + k ) ) ) }
17 simplrl 
 |-  ( ( ( ph /\ ( n e. NN /\ y e. U ) ) /\ ( 2 x. R ) <_ n ) -> n e. NN )
18 simprr 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> y e. U )
19 18 adantr 
 |-  ( ( ( ph /\ ( n e. NN /\ y e. U ) ) /\ ( 2 x. R ) <_ n ) -> y e. U )
20 simpr 
 |-  ( ( ( ph /\ ( n e. NN /\ y e. U ) ) /\ ( 2 x. R ) <_ n ) -> ( 2 x. R ) <_ n )
21 8 16 17 19 20 lgamgulmlem3 
 |-  ( ( ( ph /\ ( n e. NN /\ y e. U ) ) /\ ( 2 x. R ) <_ n ) -> ( abs ` ( ( y x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( y / n ) + 1 ) ) ) ) <_ ( R x. ( ( 2 x. ( R + 1 ) ) / ( n ^ 2 ) ) ) )
22 1 2 lgamgulmlem1 
 |-  ( ph -> U C_ ( CC \ ( ZZ \ NN ) ) )
23 22 adantr 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> U C_ ( CC \ ( ZZ \ NN ) ) )
24 23 18 sseldd 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> y e. ( CC \ ( ZZ \ NN ) ) )
25 24 eldifad 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> y e. CC )
26 simprl 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> n e. NN )
27 26 peano2nnd 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( n + 1 ) e. NN )
28 27 nnrpd 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( n + 1 ) e. RR+ )
29 26 nnrpd 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> n e. RR+ )
30 28 29 rpdivcld 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( ( n + 1 ) / n ) e. RR+ )
31 30 relogcld 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( log ` ( ( n + 1 ) / n ) ) e. RR )
32 31 recnd 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( log ` ( ( n + 1 ) / n ) ) e. CC )
33 25 32 mulcld 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( y x. ( log ` ( ( n + 1 ) / n ) ) ) e. CC )
34 26 nncnd 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> n e. CC )
35 26 nnne0d 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> n =/= 0 )
36 25 34 35 divcld 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( y / n ) e. CC )
37 1cnd 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> 1 e. CC )
38 36 37 addcld 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( ( y / n ) + 1 ) e. CC )
39 24 26 dmgmdivn0 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( ( y / n ) + 1 ) =/= 0 )
40 38 39 logcld 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( log ` ( ( y / n ) + 1 ) ) e. CC )
41 33 40 subcld 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( ( y x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( y / n ) + 1 ) ) ) e. CC )
42 41 abscld 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( abs ` ( ( y x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( y / n ) + 1 ) ) ) ) e. RR )
43 33 abscld 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( abs ` ( y x. ( log ` ( ( n + 1 ) / n ) ) ) ) e. RR )
44 40 abscld 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( abs ` ( log ` ( ( y / n ) + 1 ) ) ) e. RR )
45 43 44 readdcld 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( ( abs ` ( y x. ( log ` ( ( n + 1 ) / n ) ) ) ) + ( abs ` ( log ` ( ( y / n ) + 1 ) ) ) ) e. RR )
46 7 nnred 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> R e. RR )
47 46 31 remulcld 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( R x. ( log ` ( ( n + 1 ) / n ) ) ) e. RR )
48 7 peano2nnd 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( R + 1 ) e. NN )
49 48 nnrpd 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( R + 1 ) e. RR+ )
50 49 29 rpmulcld 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( ( R + 1 ) x. n ) e. RR+ )
51 50 relogcld 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( log ` ( ( R + 1 ) x. n ) ) e. RR )
52 pire 
 |-  _pi e. RR
53 52 a1i 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> _pi e. RR )
54 51 53 readdcld 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( ( log ` ( ( R + 1 ) x. n ) ) + _pi ) e. RR )
55 47 54 readdcld 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( ( R x. ( log ` ( ( n + 1 ) / n ) ) ) + ( ( log ` ( ( R + 1 ) x. n ) ) + _pi ) ) e. RR )
56 33 40 abs2dif2d 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( abs ` ( ( y x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( y / n ) + 1 ) ) ) ) <_ ( ( abs ` ( y x. ( log ` ( ( n + 1 ) / n ) ) ) ) + ( abs ` ( log ` ( ( y / n ) + 1 ) ) ) ) )
57 25 32 absmuld 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( abs ` ( y x. ( log ` ( ( n + 1 ) / n ) ) ) ) = ( ( abs ` y ) x. ( abs ` ( log ` ( ( n + 1 ) / n ) ) ) ) )
58 30 rpred 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( ( n + 1 ) / n ) e. RR )
59 34 mulid2d 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( 1 x. n ) = n )
60 26 nnred 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> n e. RR )
61 60 lep1d 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> n <_ ( n + 1 ) )
62 59 61 eqbrtrd 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( 1 x. n ) <_ ( n + 1 ) )
63 1red 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> 1 e. RR )
64 60 63 readdcld 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( n + 1 ) e. RR )
65 63 64 29 lemuldivd 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( ( 1 x. n ) <_ ( n + 1 ) <-> 1 <_ ( ( n + 1 ) / n ) ) )
66 62 65 mpbid 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> 1 <_ ( ( n + 1 ) / n ) )
67 58 66 logge0d 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> 0 <_ ( log ` ( ( n + 1 ) / n ) ) )
68 31 67 absidd 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( abs ` ( log ` ( ( n + 1 ) / n ) ) ) = ( log ` ( ( n + 1 ) / n ) ) )
69 68 oveq2d 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( ( abs ` y ) x. ( abs ` ( log ` ( ( n + 1 ) / n ) ) ) ) = ( ( abs ` y ) x. ( log ` ( ( n + 1 ) / n ) ) ) )
70 57 69 eqtrd 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( abs ` ( y x. ( log ` ( ( n + 1 ) / n ) ) ) ) = ( ( abs ` y ) x. ( log ` ( ( n + 1 ) / n ) ) ) )
71 25 abscld 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( abs ` y ) e. RR )
72 fveq2 
 |-  ( x = y -> ( abs ` x ) = ( abs ` y ) )
73 72 breq1d 
 |-  ( x = y -> ( ( abs ` x ) <_ R <-> ( abs ` y ) <_ R ) )
74 fvoveq1 
 |-  ( x = y -> ( abs ` ( x + k ) ) = ( abs ` ( y + k ) ) )
75 74 breq2d 
 |-  ( x = y -> ( ( 1 / R ) <_ ( abs ` ( x + k ) ) <-> ( 1 / R ) <_ ( abs ` ( y + k ) ) ) )
76 75 ralbidv 
 |-  ( x = y -> ( A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) <-> A. k e. NN0 ( 1 / R ) <_ ( abs ` ( y + k ) ) ) )
77 73 76 anbi12d 
 |-  ( x = y -> ( ( ( abs ` x ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) ) <-> ( ( abs ` y ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( y + k ) ) ) ) )
78 77 2 elrab2 
 |-  ( y e. U <-> ( y e. CC /\ ( ( abs ` y ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( y + k ) ) ) ) )
79 78 simprbi 
 |-  ( y e. U -> ( ( abs ` y ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( y + k ) ) ) )
80 79 ad2antll 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( ( abs ` y ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( y + k ) ) ) )
81 80 simpld 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( abs ` y ) <_ R )
82 71 46 31 67 81 lemul1ad 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( ( abs ` y ) x. ( log ` ( ( n + 1 ) / n ) ) ) <_ ( R x. ( log ` ( ( n + 1 ) / n ) ) ) )
83 70 82 eqbrtrd 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( abs ` ( y x. ( log ` ( ( n + 1 ) / n ) ) ) ) <_ ( R x. ( log ` ( ( n + 1 ) / n ) ) ) )
84 38 39 absrpcld 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( abs ` ( ( y / n ) + 1 ) ) e. RR+ )
85 84 relogcld 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( log ` ( abs ` ( ( y / n ) + 1 ) ) ) e. RR )
86 85 recnd 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( log ` ( abs ` ( ( y / n ) + 1 ) ) ) e. CC )
87 86 abscld 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( abs ` ( log ` ( abs ` ( ( y / n ) + 1 ) ) ) ) e. RR )
88 87 53 readdcld 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( ( abs ` ( log ` ( abs ` ( ( y / n ) + 1 ) ) ) ) + _pi ) e. RR )
89 abslogle 
 |-  ( ( ( ( y / n ) + 1 ) e. CC /\ ( ( y / n ) + 1 ) =/= 0 ) -> ( abs ` ( log ` ( ( y / n ) + 1 ) ) ) <_ ( ( abs ` ( log ` ( abs ` ( ( y / n ) + 1 ) ) ) ) + _pi ) )
90 38 39 89 syl2anc 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( abs ` ( log ` ( ( y / n ) + 1 ) ) ) <_ ( ( abs ` ( log ` ( abs ` ( ( y / n ) + 1 ) ) ) ) + _pi ) )
91 1rp 
 |-  1 e. RR+
92 relogdiv 
 |-  ( ( 1 e. RR+ /\ ( ( R + 1 ) x. n ) e. RR+ ) -> ( log ` ( 1 / ( ( R + 1 ) x. n ) ) ) = ( ( log ` 1 ) - ( log ` ( ( R + 1 ) x. n ) ) ) )
93 91 50 92 sylancr 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( log ` ( 1 / ( ( R + 1 ) x. n ) ) ) = ( ( log ` 1 ) - ( log ` ( ( R + 1 ) x. n ) ) ) )
94 log1 
 |-  ( log ` 1 ) = 0
95 94 oveq1i 
 |-  ( ( log ` 1 ) - ( log ` ( ( R + 1 ) x. n ) ) ) = ( 0 - ( log ` ( ( R + 1 ) x. n ) ) )
96 df-neg 
 |-  -u ( log ` ( ( R + 1 ) x. n ) ) = ( 0 - ( log ` ( ( R + 1 ) x. n ) ) )
97 95 96 eqtr4i 
 |-  ( ( log ` 1 ) - ( log ` ( ( R + 1 ) x. n ) ) ) = -u ( log ` ( ( R + 1 ) x. n ) )
98 93 97 eqtr2di 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> -u ( log ` ( ( R + 1 ) x. n ) ) = ( log ` ( 1 / ( ( R + 1 ) x. n ) ) ) )
99 48 nnrecred 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( 1 / ( R + 1 ) ) e. RR )
100 25 34 addcld 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( y + n ) e. CC )
101 100 abscld 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( abs ` ( y + n ) ) e. RR )
102 7 nnrecred 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( 1 / R ) e. RR )
103 7 nnrpd 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> R e. RR+ )
104 0le1 
 |-  0 <_ 1
105 104 a1i 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> 0 <_ 1 )
106 46 lep1d 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> R <_ ( R + 1 ) )
107 103 49 63 105 106 lediv2ad 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( 1 / ( R + 1 ) ) <_ ( 1 / R ) )
108 oveq2 
 |-  ( k = n -> ( y + k ) = ( y + n ) )
109 108 fveq2d 
 |-  ( k = n -> ( abs ` ( y + k ) ) = ( abs ` ( y + n ) ) )
110 109 breq2d 
 |-  ( k = n -> ( ( 1 / R ) <_ ( abs ` ( y + k ) ) <-> ( 1 / R ) <_ ( abs ` ( y + n ) ) ) )
111 80 simprd 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> A. k e. NN0 ( 1 / R ) <_ ( abs ` ( y + k ) ) )
112 26 nnnn0d 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> n e. NN0 )
113 110 111 112 rspcdva 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( 1 / R ) <_ ( abs ` ( y + n ) ) )
114 99 102 101 107 113 letrd 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( 1 / ( R + 1 ) ) <_ ( abs ` ( y + n ) ) )
115 99 101 29 114 lediv1dd 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( ( 1 / ( R + 1 ) ) / n ) <_ ( ( abs ` ( y + n ) ) / n ) )
116 48 nncnd 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( R + 1 ) e. CC )
117 48 nnne0d 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( R + 1 ) =/= 0 )
118 116 34 117 35 recdiv2d 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( ( 1 / ( R + 1 ) ) / n ) = ( 1 / ( ( R + 1 ) x. n ) ) )
119 25 34 34 35 divdird 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( ( y + n ) / n ) = ( ( y / n ) + ( n / n ) ) )
120 34 35 dividd 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( n / n ) = 1 )
121 120 oveq2d 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( ( y / n ) + ( n / n ) ) = ( ( y / n ) + 1 ) )
122 119 121 eqtr2d 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( ( y / n ) + 1 ) = ( ( y + n ) / n ) )
123 122 fveq2d 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( abs ` ( ( y / n ) + 1 ) ) = ( abs ` ( ( y + n ) / n ) ) )
124 100 34 35 absdivd 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( abs ` ( ( y + n ) / n ) ) = ( ( abs ` ( y + n ) ) / ( abs ` n ) ) )
125 29 rpge0d 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> 0 <_ n )
126 60 125 absidd 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( abs ` n ) = n )
127 126 oveq2d 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( ( abs ` ( y + n ) ) / ( abs ` n ) ) = ( ( abs ` ( y + n ) ) / n ) )
128 123 124 127 3eqtrrd 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( ( abs ` ( y + n ) ) / n ) = ( abs ` ( ( y / n ) + 1 ) ) )
129 115 118 128 3brtr3d 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( 1 / ( ( R + 1 ) x. n ) ) <_ ( abs ` ( ( y / n ) + 1 ) ) )
130 50 rpreccld 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( 1 / ( ( R + 1 ) x. n ) ) e. RR+ )
131 130 84 logled 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( ( 1 / ( ( R + 1 ) x. n ) ) <_ ( abs ` ( ( y / n ) + 1 ) ) <-> ( log ` ( 1 / ( ( R + 1 ) x. n ) ) ) <_ ( log ` ( abs ` ( ( y / n ) + 1 ) ) ) ) )
132 129 131 mpbid 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( log ` ( 1 / ( ( R + 1 ) x. n ) ) ) <_ ( log ` ( abs ` ( ( y / n ) + 1 ) ) ) )
133 98 132 eqbrtrd 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> -u ( log ` ( ( R + 1 ) x. n ) ) <_ ( log ` ( abs ` ( ( y / n ) + 1 ) ) ) )
134 38 abscld 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( abs ` ( ( y / n ) + 1 ) ) e. RR )
135 46 63 readdcld 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( R + 1 ) e. RR )
136 50 rpred 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( ( R + 1 ) x. n ) e. RR )
137 36 abscld 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( abs ` ( y / n ) ) e. RR )
138 137 63 readdcld 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( ( abs ` ( y / n ) ) + 1 ) e. RR )
139 36 37 abstrid 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( abs ` ( ( y / n ) + 1 ) ) <_ ( ( abs ` ( y / n ) ) + ( abs ` 1 ) ) )
140 abs1 
 |-  ( abs ` 1 ) = 1
141 140 oveq2i 
 |-  ( ( abs ` ( y / n ) ) + ( abs ` 1 ) ) = ( ( abs ` ( y / n ) ) + 1 )
142 139 141 breqtrdi 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( abs ` ( ( y / n ) + 1 ) ) <_ ( ( abs ` ( y / n ) ) + 1 ) )
143 91 a1i 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> 1 e. RR+ )
144 25 absge0d 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> 0 <_ ( abs ` y ) )
145 26 nnge1d 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> 1 <_ n )
146 71 46 143 60 144 81 145 lediv12ad 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( ( abs ` y ) / n ) <_ ( R / 1 ) )
147 25 34 35 absdivd 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( abs ` ( y / n ) ) = ( ( abs ` y ) / ( abs ` n ) ) )
148 126 oveq2d 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( ( abs ` y ) / ( abs ` n ) ) = ( ( abs ` y ) / n ) )
149 147 148 eqtr2d 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( ( abs ` y ) / n ) = ( abs ` ( y / n ) ) )
150 7 nncnd 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> R e. CC )
151 150 div1d 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( R / 1 ) = R )
152 146 149 151 3brtr3d 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( abs ` ( y / n ) ) <_ R )
153 137 46 63 152 leadd1dd 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( ( abs ` ( y / n ) ) + 1 ) <_ ( R + 1 ) )
154 134 138 135 142 153 letrd 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( abs ` ( ( y / n ) + 1 ) ) <_ ( R + 1 ) )
155 49 rpge0d 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> 0 <_ ( R + 1 ) )
156 135 60 155 145 lemulge11d 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( R + 1 ) <_ ( ( R + 1 ) x. n ) )
157 134 135 136 154 156 letrd 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( abs ` ( ( y / n ) + 1 ) ) <_ ( ( R + 1 ) x. n ) )
158 84 50 logled 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( ( abs ` ( ( y / n ) + 1 ) ) <_ ( ( R + 1 ) x. n ) <-> ( log ` ( abs ` ( ( y / n ) + 1 ) ) ) <_ ( log ` ( ( R + 1 ) x. n ) ) ) )
159 157 158 mpbid 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( log ` ( abs ` ( ( y / n ) + 1 ) ) ) <_ ( log ` ( ( R + 1 ) x. n ) ) )
160 85 51 absled 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( ( abs ` ( log ` ( abs ` ( ( y / n ) + 1 ) ) ) ) <_ ( log ` ( ( R + 1 ) x. n ) ) <-> ( -u ( log ` ( ( R + 1 ) x. n ) ) <_ ( log ` ( abs ` ( ( y / n ) + 1 ) ) ) /\ ( log ` ( abs ` ( ( y / n ) + 1 ) ) ) <_ ( log ` ( ( R + 1 ) x. n ) ) ) ) )
161 133 159 160 mpbir2and 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( abs ` ( log ` ( abs ` ( ( y / n ) + 1 ) ) ) ) <_ ( log ` ( ( R + 1 ) x. n ) ) )
162 87 51 53 161 leadd1dd 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( ( abs ` ( log ` ( abs ` ( ( y / n ) + 1 ) ) ) ) + _pi ) <_ ( ( log ` ( ( R + 1 ) x. n ) ) + _pi ) )
163 44 88 54 90 162 letrd 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( abs ` ( log ` ( ( y / n ) + 1 ) ) ) <_ ( ( log ` ( ( R + 1 ) x. n ) ) + _pi ) )
164 43 44 47 54 83 163 le2addd 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( ( abs ` ( y x. ( log ` ( ( n + 1 ) / n ) ) ) ) + ( abs ` ( log ` ( ( y / n ) + 1 ) ) ) ) <_ ( ( R x. ( log ` ( ( n + 1 ) / n ) ) ) + ( ( log ` ( ( R + 1 ) x. n ) ) + _pi ) ) )
165 42 45 55 56 164 letrd 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( abs ` ( ( y x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( y / n ) + 1 ) ) ) ) <_ ( ( R x. ( log ` ( ( n + 1 ) / n ) ) ) + ( ( log ` ( ( R + 1 ) x. n ) ) + _pi ) ) )
166 165 adantr 
 |-  ( ( ( ph /\ ( n e. NN /\ y e. U ) ) /\ -. ( 2 x. R ) <_ n ) -> ( abs ` ( ( y x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( y / n ) + 1 ) ) ) ) <_ ( ( R x. ( log ` ( ( n + 1 ) / n ) ) ) + ( ( log ` ( ( R + 1 ) x. n ) ) + _pi ) ) )
167 5 6 21 166 ifbothda 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( abs ` ( ( y x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( y / n ) + 1 ) ) ) ) <_ if ( ( 2 x. R ) <_ n , ( R x. ( ( 2 x. ( R + 1 ) ) / ( n ^ 2 ) ) ) , ( ( R x. ( log ` ( ( n + 1 ) / n ) ) ) + ( ( log ` ( ( R + 1 ) x. n ) ) + _pi ) ) ) )
168 oveq1 
 |-  ( m = n -> ( m + 1 ) = ( n + 1 ) )
169 id 
 |-  ( m = n -> m = n )
170 168 169 oveq12d 
 |-  ( m = n -> ( ( m + 1 ) / m ) = ( ( n + 1 ) / n ) )
171 170 fveq2d 
 |-  ( m = n -> ( log ` ( ( m + 1 ) / m ) ) = ( log ` ( ( n + 1 ) / n ) ) )
172 171 oveq2d 
 |-  ( m = n -> ( z x. ( log ` ( ( m + 1 ) / m ) ) ) = ( z x. ( log ` ( ( n + 1 ) / n ) ) ) )
173 oveq2 
 |-  ( m = n -> ( z / m ) = ( z / n ) )
174 173 fvoveq1d 
 |-  ( m = n -> ( log ` ( ( z / m ) + 1 ) ) = ( log ` ( ( z / n ) + 1 ) ) )
175 172 174 oveq12d 
 |-  ( m = n -> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) = ( ( z x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( z / n ) + 1 ) ) ) )
176 175 mpteq2dv 
 |-  ( m = n -> ( z e. U |-> ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) ) = ( z e. U |-> ( ( z x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( z / n ) + 1 ) ) ) ) )
177 cnex 
 |-  CC e. _V
178 2 177 rabex2 
 |-  U e. _V
179 178 mptex 
 |-  ( z e. U |-> ( ( z x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( z / n ) + 1 ) ) ) ) e. _V
180 176 3 179 fvmpt 
 |-  ( n e. NN -> ( G ` n ) = ( z e. U |-> ( ( z x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( z / n ) + 1 ) ) ) ) )
181 180 ad2antrl 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( G ` n ) = ( z e. U |-> ( ( z x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( z / n ) + 1 ) ) ) ) )
182 181 fveq1d 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( ( G ` n ) ` y ) = ( ( z e. U |-> ( ( z x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( z / n ) + 1 ) ) ) ) ` y ) )
183 oveq1 
 |-  ( z = y -> ( z x. ( log ` ( ( n + 1 ) / n ) ) ) = ( y x. ( log ` ( ( n + 1 ) / n ) ) ) )
184 oveq1 
 |-  ( z = y -> ( z / n ) = ( y / n ) )
185 184 fvoveq1d 
 |-  ( z = y -> ( log ` ( ( z / n ) + 1 ) ) = ( log ` ( ( y / n ) + 1 ) ) )
186 183 185 oveq12d 
 |-  ( z = y -> ( ( z x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( z / n ) + 1 ) ) ) = ( ( y x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( y / n ) + 1 ) ) ) )
187 eqid 
 |-  ( z e. U |-> ( ( z x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( z / n ) + 1 ) ) ) ) = ( z e. U |-> ( ( z x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( z / n ) + 1 ) ) ) )
188 ovex 
 |-  ( ( y x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( y / n ) + 1 ) ) ) e. _V
189 186 187 188 fvmpt 
 |-  ( y e. U -> ( ( z e. U |-> ( ( z x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( z / n ) + 1 ) ) ) ) ` y ) = ( ( y x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( y / n ) + 1 ) ) ) )
190 189 ad2antll 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( ( z e. U |-> ( ( z x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( z / n ) + 1 ) ) ) ) ` y ) = ( ( y x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( y / n ) + 1 ) ) ) )
191 182 190 eqtrd 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( ( G ` n ) ` y ) = ( ( y x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( y / n ) + 1 ) ) ) )
192 191 fveq2d 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( abs ` ( ( G ` n ) ` y ) ) = ( abs ` ( ( y x. ( log ` ( ( n + 1 ) / n ) ) ) - ( log ` ( ( y / n ) + 1 ) ) ) ) )
193 breq2 
 |-  ( m = n -> ( ( 2 x. R ) <_ m <-> ( 2 x. R ) <_ n ) )
194 oveq1 
 |-  ( m = n -> ( m ^ 2 ) = ( n ^ 2 ) )
195 194 oveq2d 
 |-  ( m = n -> ( ( 2 x. ( R + 1 ) ) / ( m ^ 2 ) ) = ( ( 2 x. ( R + 1 ) ) / ( n ^ 2 ) ) )
196 195 oveq2d 
 |-  ( m = n -> ( R x. ( ( 2 x. ( R + 1 ) ) / ( m ^ 2 ) ) ) = ( R x. ( ( 2 x. ( R + 1 ) ) / ( n ^ 2 ) ) ) )
197 171 oveq2d 
 |-  ( m = n -> ( R x. ( log ` ( ( m + 1 ) / m ) ) ) = ( R x. ( log ` ( ( n + 1 ) / n ) ) ) )
198 oveq2 
 |-  ( m = n -> ( ( R + 1 ) x. m ) = ( ( R + 1 ) x. n ) )
199 198 fveq2d 
 |-  ( m = n -> ( log ` ( ( R + 1 ) x. m ) ) = ( log ` ( ( R + 1 ) x. n ) ) )
200 199 oveq1d 
 |-  ( m = n -> ( ( log ` ( ( R + 1 ) x. m ) ) + _pi ) = ( ( log ` ( ( R + 1 ) x. n ) ) + _pi ) )
201 197 200 oveq12d 
 |-  ( m = n -> ( ( R x. ( log ` ( ( m + 1 ) / m ) ) ) + ( ( log ` ( ( R + 1 ) x. m ) ) + _pi ) ) = ( ( R x. ( log ` ( ( n + 1 ) / n ) ) ) + ( ( log ` ( ( R + 1 ) x. n ) ) + _pi ) ) )
202 193 196 201 ifbieq12d 
 |-  ( m = n -> if ( ( 2 x. R ) <_ m , ( R x. ( ( 2 x. ( R + 1 ) ) / ( m ^ 2 ) ) ) , ( ( R x. ( log ` ( ( m + 1 ) / m ) ) ) + ( ( log ` ( ( R + 1 ) x. m ) ) + _pi ) ) ) = if ( ( 2 x. R ) <_ n , ( R x. ( ( 2 x. ( R + 1 ) ) / ( n ^ 2 ) ) ) , ( ( R x. ( log ` ( ( n + 1 ) / n ) ) ) + ( ( log ` ( ( R + 1 ) x. n ) ) + _pi ) ) ) )
203 ovex 
 |-  ( R x. ( ( 2 x. ( R + 1 ) ) / ( n ^ 2 ) ) ) e. _V
204 ovex 
 |-  ( ( R x. ( log ` ( ( n + 1 ) / n ) ) ) + ( ( log ` ( ( R + 1 ) x. n ) ) + _pi ) ) e. _V
205 203 204 ifex 
 |-  if ( ( 2 x. R ) <_ n , ( R x. ( ( 2 x. ( R + 1 ) ) / ( n ^ 2 ) ) ) , ( ( R x. ( log ` ( ( n + 1 ) / n ) ) ) + ( ( log ` ( ( R + 1 ) x. n ) ) + _pi ) ) ) e. _V
206 202 4 205 fvmpt 
 |-  ( n e. NN -> ( T ` n ) = if ( ( 2 x. R ) <_ n , ( R x. ( ( 2 x. ( R + 1 ) ) / ( n ^ 2 ) ) ) , ( ( R x. ( log ` ( ( n + 1 ) / n ) ) ) + ( ( log ` ( ( R + 1 ) x. n ) ) + _pi ) ) ) )
207 206 ad2antrl 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( T ` n ) = if ( ( 2 x. R ) <_ n , ( R x. ( ( 2 x. ( R + 1 ) ) / ( n ^ 2 ) ) ) , ( ( R x. ( log ` ( ( n + 1 ) / n ) ) ) + ( ( log ` ( ( R + 1 ) x. n ) ) + _pi ) ) ) )
208 167 192 207 3brtr4d 
 |-  ( ( ph /\ ( n e. NN /\ y e. U ) ) -> ( abs ` ( ( G ` n ) ` y ) ) <_ ( T ` n ) )