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 |
|
rpvmasum.g |
|- G = ( DChr ` N ) |
5 |
|
rpvmasum.d |
|- D = ( Base ` G ) |
6 |
|
rpvmasum.1 |
|- .1. = ( 0g ` G ) |
7 |
|
dchrisum.b |
|- ( ph -> X e. D ) |
8 |
|
dchrisum.n1 |
|- ( ph -> X =/= .1. ) |
9 |
|
dchrisumn0.f |
|- F = ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) |
10 |
|
oveq2 |
|- ( n = x -> ( 1 / n ) = ( 1 / x ) ) |
11 |
|
1nn |
|- 1 e. NN |
12 |
11
|
a1i |
|- ( ph -> 1 e. NN ) |
13 |
|
rpreccl |
|- ( n e. RR+ -> ( 1 / n ) e. RR+ ) |
14 |
13
|
adantl |
|- ( ( ph /\ n e. RR+ ) -> ( 1 / n ) e. RR+ ) |
15 |
14
|
rpred |
|- ( ( ph /\ n e. RR+ ) -> ( 1 / n ) e. RR ) |
16 |
|
simp3r |
|- ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( 1 <_ n /\ n <_ x ) ) -> n <_ x ) |
17 |
|
rpregt0 |
|- ( n e. RR+ -> ( n e. RR /\ 0 < n ) ) |
18 |
|
rpregt0 |
|- ( x e. RR+ -> ( x e. RR /\ 0 < x ) ) |
19 |
|
lerec |
|- ( ( ( n e. RR /\ 0 < n ) /\ ( x e. RR /\ 0 < x ) ) -> ( n <_ x <-> ( 1 / x ) <_ ( 1 / n ) ) ) |
20 |
17 18 19
|
syl2an |
|- ( ( n e. RR+ /\ x e. RR+ ) -> ( n <_ x <-> ( 1 / x ) <_ ( 1 / n ) ) ) |
21 |
20
|
3ad2ant2 |
|- ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( 1 <_ n /\ n <_ x ) ) -> ( n <_ x <-> ( 1 / x ) <_ ( 1 / n ) ) ) |
22 |
16 21
|
mpbid |
|- ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( 1 <_ n /\ n <_ x ) ) -> ( 1 / x ) <_ ( 1 / n ) ) |
23 |
|
ax-1cn |
|- 1 e. CC |
24 |
|
divrcnv |
|- ( 1 e. CC -> ( n e. RR+ |-> ( 1 / n ) ) ~~>r 0 ) |
25 |
23 24
|
mp1i |
|- ( ph -> ( n e. RR+ |-> ( 1 / n ) ) ~~>r 0 ) |
26 |
|
2fveq3 |
|- ( a = n -> ( X ` ( L ` a ) ) = ( X ` ( L ` n ) ) ) |
27 |
|
oveq2 |
|- ( a = n -> ( 1 / a ) = ( 1 / n ) ) |
28 |
26 27
|
oveq12d |
|- ( a = n -> ( ( X ` ( L ` a ) ) x. ( 1 / a ) ) = ( ( X ` ( L ` n ) ) x. ( 1 / n ) ) ) |
29 |
28
|
cbvmptv |
|- ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / a ) ) ) = ( n e. NN |-> ( ( X ` ( L ` n ) ) x. ( 1 / n ) ) ) |
30 |
1 2 3 4 5 6 7 8 10 12 15 22 25 29
|
dchrisum |
|- ( ph -> E. t E. c e. ( 0 [,) +oo ) ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / a ) ) ) ) ~~> t /\ A. x e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / a ) ) ) ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. ( 1 / x ) ) ) ) |
31 |
7
|
adantr |
|- ( ( ph /\ n e. NN ) -> X e. D ) |
32 |
|
nnz |
|- ( n e. NN -> n e. ZZ ) |
33 |
32
|
adantl |
|- ( ( ph /\ n e. NN ) -> n e. ZZ ) |
34 |
4 1 5 2 31 33
|
dchrzrhcl |
|- ( ( ph /\ n e. NN ) -> ( X ` ( L ` n ) ) e. CC ) |
35 |
|
nncn |
|- ( n e. NN -> n e. CC ) |
36 |
35
|
adantl |
|- ( ( ph /\ n e. NN ) -> n e. CC ) |
37 |
|
nnne0 |
|- ( n e. NN -> n =/= 0 ) |
38 |
37
|
adantl |
|- ( ( ph /\ n e. NN ) -> n =/= 0 ) |
39 |
34 36 38
|
divrecd |
|- ( ( ph /\ n e. NN ) -> ( ( X ` ( L ` n ) ) / n ) = ( ( X ` ( L ` n ) ) x. ( 1 / n ) ) ) |
40 |
39
|
mpteq2dva |
|- ( ph -> ( n e. NN |-> ( ( X ` ( L ` n ) ) / n ) ) = ( n e. NN |-> ( ( X ` ( L ` n ) ) x. ( 1 / n ) ) ) ) |
41 |
|
id |
|- ( a = n -> a = n ) |
42 |
26 41
|
oveq12d |
|- ( a = n -> ( ( X ` ( L ` a ) ) / a ) = ( ( X ` ( L ` n ) ) / n ) ) |
43 |
42
|
cbvmptv |
|- ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) = ( n e. NN |-> ( ( X ` ( L ` n ) ) / n ) ) |
44 |
9 43
|
eqtri |
|- F = ( n e. NN |-> ( ( X ` ( L ` n ) ) / n ) ) |
45 |
40 44 29
|
3eqtr4g |
|- ( ph -> F = ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / a ) ) ) ) |
46 |
45
|
adantr |
|- ( ( ph /\ c e. ( 0 [,) +oo ) ) -> F = ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / a ) ) ) ) |
47 |
46
|
seqeq3d |
|- ( ( ph /\ c e. ( 0 [,) +oo ) ) -> seq 1 ( + , F ) = seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / a ) ) ) ) ) |
48 |
47
|
breq1d |
|- ( ( ph /\ c e. ( 0 [,) +oo ) ) -> ( seq 1 ( + , F ) ~~> t <-> seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / a ) ) ) ) ~~> t ) ) |
49 |
|
2fveq3 |
|- ( y = x -> ( seq 1 ( + , F ) ` ( |_ ` y ) ) = ( seq 1 ( + , F ) ` ( |_ ` x ) ) ) |
50 |
49
|
fvoveq1d |
|- ( y = x -> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - t ) ) = ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) ) |
51 |
|
oveq2 |
|- ( y = x -> ( c / y ) = ( c / x ) ) |
52 |
50 51
|
breq12d |
|- ( y = x -> ( ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) <-> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c / x ) ) ) |
53 |
52
|
cbvralvw |
|- ( A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) <-> A. x e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c / x ) ) |
54 |
45
|
seqeq3d |
|- ( ph -> seq 1 ( + , F ) = seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / a ) ) ) ) ) |
55 |
54
|
fveq1d |
|- ( ph -> ( seq 1 ( + , F ) ` ( |_ ` x ) ) = ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / a ) ) ) ) ` ( |_ ` x ) ) ) |
56 |
55
|
fvoveq1d |
|- ( ph -> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) = ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / a ) ) ) ) ` ( |_ ` x ) ) - t ) ) ) |
57 |
56
|
ad2antrr |
|- ( ( ( ph /\ c e. ( 0 [,) +oo ) ) /\ x e. ( 1 [,) +oo ) ) -> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) = ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / a ) ) ) ) ` ( |_ ` x ) ) - t ) ) ) |
58 |
|
elrege0 |
|- ( c e. ( 0 [,) +oo ) <-> ( c e. RR /\ 0 <_ c ) ) |
59 |
58
|
simplbi |
|- ( c e. ( 0 [,) +oo ) -> c e. RR ) |
60 |
59
|
recnd |
|- ( c e. ( 0 [,) +oo ) -> c e. CC ) |
61 |
60
|
ad2antlr |
|- ( ( ( ph /\ c e. ( 0 [,) +oo ) ) /\ x e. ( 1 [,) +oo ) ) -> c e. CC ) |
62 |
|
1re |
|- 1 e. RR |
63 |
|
elicopnf |
|- ( 1 e. RR -> ( x e. ( 1 [,) +oo ) <-> ( x e. RR /\ 1 <_ x ) ) ) |
64 |
62 63
|
ax-mp |
|- ( x e. ( 1 [,) +oo ) <-> ( x e. RR /\ 1 <_ x ) ) |
65 |
64
|
simplbi |
|- ( x e. ( 1 [,) +oo ) -> x e. RR ) |
66 |
65
|
adantl |
|- ( ( ( ph /\ c e. ( 0 [,) +oo ) ) /\ x e. ( 1 [,) +oo ) ) -> x e. RR ) |
67 |
66
|
recnd |
|- ( ( ( ph /\ c e. ( 0 [,) +oo ) ) /\ x e. ( 1 [,) +oo ) ) -> x e. CC ) |
68 |
|
0red |
|- ( ( ( ph /\ c e. ( 0 [,) +oo ) ) /\ x e. ( 1 [,) +oo ) ) -> 0 e. RR ) |
69 |
|
1red |
|- ( ( ( ph /\ c e. ( 0 [,) +oo ) ) /\ x e. ( 1 [,) +oo ) ) -> 1 e. RR ) |
70 |
|
0lt1 |
|- 0 < 1 |
71 |
70
|
a1i |
|- ( ( ( ph /\ c e. ( 0 [,) +oo ) ) /\ x e. ( 1 [,) +oo ) ) -> 0 < 1 ) |
72 |
64
|
simprbi |
|- ( x e. ( 1 [,) +oo ) -> 1 <_ x ) |
73 |
72
|
adantl |
|- ( ( ( ph /\ c e. ( 0 [,) +oo ) ) /\ x e. ( 1 [,) +oo ) ) -> 1 <_ x ) |
74 |
68 69 66 71 73
|
ltletrd |
|- ( ( ( ph /\ c e. ( 0 [,) +oo ) ) /\ x e. ( 1 [,) +oo ) ) -> 0 < x ) |
75 |
74
|
gt0ne0d |
|- ( ( ( ph /\ c e. ( 0 [,) +oo ) ) /\ x e. ( 1 [,) +oo ) ) -> x =/= 0 ) |
76 |
61 67 75
|
divrecd |
|- ( ( ( ph /\ c e. ( 0 [,) +oo ) ) /\ x e. ( 1 [,) +oo ) ) -> ( c / x ) = ( c x. ( 1 / x ) ) ) |
77 |
57 76
|
breq12d |
|- ( ( ( ph /\ c e. ( 0 [,) +oo ) ) /\ x e. ( 1 [,) +oo ) ) -> ( ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c / x ) <-> ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / a ) ) ) ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. ( 1 / x ) ) ) ) |
78 |
77
|
ralbidva |
|- ( ( ph /\ c e. ( 0 [,) +oo ) ) -> ( A. x e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - t ) ) <_ ( c / x ) <-> A. x e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / a ) ) ) ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. ( 1 / x ) ) ) ) |
79 |
53 78
|
syl5bb |
|- ( ( ph /\ c e. ( 0 [,) +oo ) ) -> ( A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) <-> A. x e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / a ) ) ) ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. ( 1 / x ) ) ) ) |
80 |
48 79
|
anbi12d |
|- ( ( ph /\ c e. ( 0 [,) +oo ) ) -> ( ( seq 1 ( + , F ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) <-> ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / a ) ) ) ) ~~> t /\ A. x e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / a ) ) ) ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. ( 1 / x ) ) ) ) ) |
81 |
80
|
rexbidva |
|- ( ph -> ( E. c e. ( 0 [,) +oo ) ( seq 1 ( + , F ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) <-> E. c e. ( 0 [,) +oo ) ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / a ) ) ) ) ~~> t /\ A. x e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / a ) ) ) ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. ( 1 / x ) ) ) ) ) |
82 |
81
|
exbidv |
|- ( ph -> ( E. t E. c e. ( 0 [,) +oo ) ( seq 1 ( + , F ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) <-> E. t E. c e. ( 0 [,) +oo ) ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / a ) ) ) ) ~~> t /\ A. x e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) x. ( 1 / a ) ) ) ) ` ( |_ ` x ) ) - t ) ) <_ ( c x. ( 1 / x ) ) ) ) ) |
83 |
30 82
|
mpbird |
|- ( ph -> E. t E. c e. ( 0 [,) +oo ) ( seq 1 ( + , F ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) ) |