Metamath Proof Explorer

Theorem dchrisumlema

Description: Lemma for dchrisum . Lemma 9.4.1 of Shapiro, p. 377. (Contributed by Mario Carneiro, 2-May-2016)

Ref Expression
Hypotheses rpvmasum.z 
|- Z = ( Z/nZ ` N )
rpvmasum.l 
|- L = ( ZRHom ` Z )
rpvmasum.a 
|- ( ph -> N e. NN )
rpvmasum.g 
|- G = ( DChr ` N )
rpvmasum.d 
|- D = ( Base ` G )
rpvmasum.1 
|- .1. = ( 0g ` G )
dchrisum.b 
|- ( ph -> X e. D )
dchrisum.n1 
|- ( ph -> X =/= .1. )
dchrisum.2 
|- ( n = x -> A = B )
dchrisum.3 
|- ( ph -> M e. NN )
dchrisum.4 
|- ( ( ph /\ n e. RR+ ) -> A e. RR )
dchrisum.5 
|- ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( M <_ n /\ n <_ x ) ) -> B <_ A )
dchrisum.6 
|- ( ph -> ( n e. RR+ |-> A ) ~~>r 0 )
dchrisum.7 
|- F = ( n e. NN |-> ( ( X ` ( L ` n ) ) x. A ) )
Assertion dchrisumlema 
|- ( ph -> ( ( I e. RR+ -> [_ I / n ]_ A e. RR ) /\ ( I e. ( M [,) +oo ) -> 0 <_ [_ I / n ]_ A ) ) )

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 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 dchrisum.2 
 |-  ( n = x -> A = B )
10 dchrisum.3 
 |-  ( ph -> M e. NN )
11 dchrisum.4 
 |-  ( ( ph /\ n e. RR+ ) -> A e. RR )
12 dchrisum.5 
 |-  ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( M <_ n /\ n <_ x ) ) -> B <_ A )
13 dchrisum.6 
 |-  ( ph -> ( n e. RR+ |-> A ) ~~>r 0 )
14 dchrisum.7 
 |-  F = ( n e. NN |-> ( ( X ` ( L ` n ) ) x. A ) )
15 11 ralrimiva 
 |-  ( ph -> A. n e. RR+ A e. RR )
16 nfcsb1v 
 |-  F/_ n [_ I / n ]_ A
17 16 nfel1 
 |-  F/ n [_ I / n ]_ A e. RR
18 csbeq1a 
 |-  ( n = I -> A = [_ I / n ]_ A )
19 18 eleq1d 
 |-  ( n = I -> ( A e. RR <-> [_ I / n ]_ A e. RR ) )
20 17 19 rspc 
 |-  ( I e. RR+ -> ( A. n e. RR+ A e. RR -> [_ I / n ]_ A e. RR ) )
21 15 20 syl5com 
 |-  ( ph -> ( I e. RR+ -> [_ I / n ]_ A e. RR ) )
22 eqid 
 |-  ( ZZ>= ` ( ( |_ ` I ) + 1 ) ) = ( ZZ>= ` ( ( |_ ` I ) + 1 ) )
23 10 nnred 
 |-  ( ph -> M e. RR )
24 elicopnf 
 |-  ( M e. RR -> ( I e. ( M [,) +oo ) <-> ( I e. RR /\ M <_ I ) ) )
25 23 24 syl 
 |-  ( ph -> ( I e. ( M [,) +oo ) <-> ( I e. RR /\ M <_ I ) ) )
26 25 simprbda 
 |-  ( ( ph /\ I e. ( M [,) +oo ) ) -> I e. RR )
27 26 flcld 
 |-  ( ( ph /\ I e. ( M [,) +oo ) ) -> ( |_ ` I ) e. ZZ )
28 27 peano2zd 
 |-  ( ( ph /\ I e. ( M [,) +oo ) ) -> ( ( |_ ` I ) + 1 ) e. ZZ )
29 nnuz 
 |-  NN = ( ZZ>= ` 1 )
30 1zzd 
 |-  ( ph -> 1 e. ZZ )
31 nnrp 
 |-  ( i e. NN -> i e. RR+ )
32 31 ssriv 
 |-  NN C_ RR+
33 eqid 
 |-  ( n e. RR+ |-> A ) = ( n e. RR+ |-> A )
34 33 11 dmmptd 
 |-  ( ph -> dom ( n e. RR+ |-> A ) = RR+ )
35 32 34 sseqtrrid 
 |-  ( ph -> NN C_ dom ( n e. RR+ |-> A ) )
36 29 30 13 35 rlimclim1 
 |-  ( ph -> ( n e. RR+ |-> A ) ~~> 0 )
37 36 adantr 
 |-  ( ( ph /\ I e. ( M [,) +oo ) ) -> ( n e. RR+ |-> A ) ~~> 0 )
38 0red 
 |-  ( ( ph /\ I e. ( M [,) +oo ) ) -> 0 e. RR )
39 23 adantr 
 |-  ( ( ph /\ I e. ( M [,) +oo ) ) -> M e. RR )
40 10 nngt0d 
 |-  ( ph -> 0 < M )
41 40 adantr 
 |-  ( ( ph /\ I e. ( M [,) +oo ) ) -> 0 < M )
42 25 simplbda 
 |-  ( ( ph /\ I e. ( M [,) +oo ) ) -> M <_ I )
43 38 39 26 41 42 ltletrd 
 |-  ( ( ph /\ I e. ( M [,) +oo ) ) -> 0 < I )
44 26 43 elrpd 
 |-  ( ( ph /\ I e. ( M [,) +oo ) ) -> I e. RR+ )
45 15 adantr 
 |-  ( ( ph /\ I e. ( M [,) +oo ) ) -> A. n e. RR+ A e. RR )
46 44 45 20 sylc 
 |-  ( ( ph /\ I e. ( M [,) +oo ) ) -> [_ I / n ]_ A e. RR )
47 46 recnd 
 |-  ( ( ph /\ I e. ( M [,) +oo ) ) -> [_ I / n ]_ A e. CC )
48 ssid 
 |-  ( ZZ>= ` ( ( |_ ` I ) + 1 ) ) C_ ( ZZ>= ` ( ( |_ ` I ) + 1 ) )
49 fvex 
 |-  ( ZZ>= ` ( ( |_ ` I ) + 1 ) ) e. _V
50 48 49 climconst2 
 |-  ( ( [_ I / n ]_ A e. CC /\ ( ( |_ ` I ) + 1 ) e. ZZ ) -> ( ( ZZ>= ` ( ( |_ ` I ) + 1 ) ) X. { [_ I / n ]_ A } ) ~~> [_ I / n ]_ A )
51 47 28 50 syl2anc 
 |-  ( ( ph /\ I e. ( M [,) +oo ) ) -> ( ( ZZ>= ` ( ( |_ ` I ) + 1 ) ) X. { [_ I / n ]_ A } ) ~~> [_ I / n ]_ A )
52 44 rpge0d 
 |-  ( ( ph /\ I e. ( M [,) +oo ) ) -> 0 <_ I )
53 flge0nn0 
 |-  ( ( I e. RR /\ 0 <_ I ) -> ( |_ ` I ) e. NN0 )
54 26 52 53 syl2anc 
 |-  ( ( ph /\ I e. ( M [,) +oo ) ) -> ( |_ ` I ) e. NN0 )
55 nn0p1nn 
 |-  ( ( |_ ` I ) e. NN0 -> ( ( |_ ` I ) + 1 ) e. NN )
56 54 55 syl 
 |-  ( ( ph /\ I e. ( M [,) +oo ) ) -> ( ( |_ ` I ) + 1 ) e. NN )
57 eluznn 
 |-  ( ( ( ( |_ ` I ) + 1 ) e. NN /\ i e. ( ZZ>= ` ( ( |_ ` I ) + 1 ) ) ) -> i e. NN )
58 56 57 sylan 
 |-  ( ( ( ph /\ I e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( ( |_ ` I ) + 1 ) ) ) -> i e. NN )
59 58 nnrpd 
 |-  ( ( ( ph /\ I e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( ( |_ ` I ) + 1 ) ) ) -> i e. RR+ )
60 15 ad2antrr 
 |-  ( ( ( ph /\ I e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( ( |_ ` I ) + 1 ) ) ) -> A. n e. RR+ A e. RR )
61 nfcsb1v 
 |-  F/_ n [_ i / n ]_ A
62 61 nfel1 
 |-  F/ n [_ i / n ]_ A e. RR
63 csbeq1a 
 |-  ( n = i -> A = [_ i / n ]_ A )
64 63 eleq1d 
 |-  ( n = i -> ( A e. RR <-> [_ i / n ]_ A e. RR ) )
65 62 64 rspc 
 |-  ( i e. RR+ -> ( A. n e. RR+ A e. RR -> [_ i / n ]_ A e. RR ) )
66 59 60 65 sylc 
 |-  ( ( ( ph /\ I e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( ( |_ ` I ) + 1 ) ) ) -> [_ i / n ]_ A e. RR )
67 33 fvmpts 
 |-  ( ( i e. RR+ /\ [_ i / n ]_ A e. RR ) -> ( ( n e. RR+ |-> A ) ` i ) = [_ i / n ]_ A )
68 59 66 67 syl2anc 
 |-  ( ( ( ph /\ I e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( ( |_ ` I ) + 1 ) ) ) -> ( ( n e. RR+ |-> A ) ` i ) = [_ i / n ]_ A )
69 68 66 eqeltrd 
 |-  ( ( ( ph /\ I e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( ( |_ ` I ) + 1 ) ) ) -> ( ( n e. RR+ |-> A ) ` i ) e. RR )
70 fvconst2g 
 |-  ( ( [_ I / n ]_ A e. RR /\ i e. ( ZZ>= ` ( ( |_ ` I ) + 1 ) ) ) -> ( ( ( ZZ>= ` ( ( |_ ` I ) + 1 ) ) X. { [_ I / n ]_ A } ) ` i ) = [_ I / n ]_ A )
71 46 70 sylan 
 |-  ( ( ( ph /\ I e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( ( |_ ` I ) + 1 ) ) ) -> ( ( ( ZZ>= ` ( ( |_ ` I ) + 1 ) ) X. { [_ I / n ]_ A } ) ` i ) = [_ I / n ]_ A )
72 46 adantr 
 |-  ( ( ( ph /\ I e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( ( |_ ` I ) + 1 ) ) ) -> [_ I / n ]_ A e. RR )
73 71 72 eqeltrd 
 |-  ( ( ( ph /\ I e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( ( |_ ` I ) + 1 ) ) ) -> ( ( ( ZZ>= ` ( ( |_ ` I ) + 1 ) ) X. { [_ I / n ]_ A } ) ` i ) e. RR )
74 44 adantr 
 |-  ( ( ( ph /\ I e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( ( |_ ` I ) + 1 ) ) ) -> I e. RR+ )
75 12 3expia 
 |-  ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) ) -> ( ( M <_ n /\ n <_ x ) -> B <_ A ) )
76 75 ralrimivva 
 |-  ( ph -> A. n e. RR+ A. x e. RR+ ( ( M <_ n /\ n <_ x ) -> B <_ A ) )
77 76 ad2antrr 
 |-  ( ( ( ph /\ I e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( ( |_ ` I ) + 1 ) ) ) -> A. n e. RR+ A. x e. RR+ ( ( M <_ n /\ n <_ x ) -> B <_ A ) )
78 nfcv 
 |-  F/_ n RR+
79 nfv 
 |-  F/ n ( M <_ I /\ I <_ x )
80 nfcv 
 |-  F/_ n B
81 nfcv 
 |-  F/_ n <_
82 80 81 16 nfbr 
 |-  F/ n B <_ [_ I / n ]_ A
83 79 82 nfim 
 |-  F/ n ( ( M <_ I /\ I <_ x ) -> B <_ [_ I / n ]_ A )
84 78 83 nfralw 
 |-  F/ n A. x e. RR+ ( ( M <_ I /\ I <_ x ) -> B <_ [_ I / n ]_ A )
85 breq2 
 |-  ( n = I -> ( M <_ n <-> M <_ I ) )
86 breq1 
 |-  ( n = I -> ( n <_ x <-> I <_ x ) )
87 85 86 anbi12d 
 |-  ( n = I -> ( ( M <_ n /\ n <_ x ) <-> ( M <_ I /\ I <_ x ) ) )
88 18 breq2d 
 |-  ( n = I -> ( B <_ A <-> B <_ [_ I / n ]_ A ) )
89 87 88 imbi12d 
 |-  ( n = I -> ( ( ( M <_ n /\ n <_ x ) -> B <_ A ) <-> ( ( M <_ I /\ I <_ x ) -> B <_ [_ I / n ]_ A ) ) )
90 89 ralbidv 
 |-  ( n = I -> ( A. x e. RR+ ( ( M <_ n /\ n <_ x ) -> B <_ A ) <-> A. x e. RR+ ( ( M <_ I /\ I <_ x ) -> B <_ [_ I / n ]_ A ) ) )
91 84 90 rspc 
 |-  ( I e. RR+ -> ( A. n e. RR+ A. x e. RR+ ( ( M <_ n /\ n <_ x ) -> B <_ A ) -> A. x e. RR+ ( ( M <_ I /\ I <_ x ) -> B <_ [_ I / n ]_ A ) ) )
92 74 77 91 sylc 
 |-  ( ( ( ph /\ I e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( ( |_ ` I ) + 1 ) ) ) -> A. x e. RR+ ( ( M <_ I /\ I <_ x ) -> B <_ [_ I / n ]_ A ) )
93 42 adantr 
 |-  ( ( ( ph /\ I e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( ( |_ ` I ) + 1 ) ) ) -> M <_ I )
94 26 adantr 
 |-  ( ( ( ph /\ I e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( ( |_ ` I ) + 1 ) ) ) -> I e. RR )
95 reflcl 
 |-  ( I e. RR -> ( |_ ` I ) e. RR )
96 peano2re 
 |-  ( ( |_ ` I ) e. RR -> ( ( |_ ` I ) + 1 ) e. RR )
97 94 95 96 3syl 
 |-  ( ( ( ph /\ I e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( ( |_ ` I ) + 1 ) ) ) -> ( ( |_ ` I ) + 1 ) e. RR )
98 58 nnred 
 |-  ( ( ( ph /\ I e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( ( |_ ` I ) + 1 ) ) ) -> i e. RR )
99 fllep1 
 |-  ( I e. RR -> I <_ ( ( |_ ` I ) + 1 ) )
100 26 99 syl 
 |-  ( ( ph /\ I e. ( M [,) +oo ) ) -> I <_ ( ( |_ ` I ) + 1 ) )
101 100 adantr 
 |-  ( ( ( ph /\ I e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( ( |_ ` I ) + 1 ) ) ) -> I <_ ( ( |_ ` I ) + 1 ) )
102 eluzle 
 |-  ( i e. ( ZZ>= ` ( ( |_ ` I ) + 1 ) ) -> ( ( |_ ` I ) + 1 ) <_ i )
103 102 adantl 
 |-  ( ( ( ph /\ I e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( ( |_ ` I ) + 1 ) ) ) -> ( ( |_ ` I ) + 1 ) <_ i )
104 94 97 98 101 103 letrd 
 |-  ( ( ( ph /\ I e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( ( |_ ` I ) + 1 ) ) ) -> I <_ i )
105 93 104 jca 
 |-  ( ( ( ph /\ I e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( ( |_ ` I ) + 1 ) ) ) -> ( M <_ I /\ I <_ i ) )
106 breq2 
 |-  ( x = i -> ( I <_ x <-> I <_ i ) )
107 106 anbi2d 
 |-  ( x = i -> ( ( M <_ I /\ I <_ x ) <-> ( M <_ I /\ I <_ i ) ) )
108 eqvisset 
 |-  ( x = i -> i e. _V )
109 equtr2 
 |-  ( ( x = i /\ n = i ) -> x = n )
110 9 equcoms 
 |-  ( x = n -> A = B )
111 109 110 syl 
 |-  ( ( x = i /\ n = i ) -> A = B )
112 108 111 csbied 
 |-  ( x = i -> [_ i / n ]_ A = B )
113 112 eqcomd 
 |-  ( x = i -> B = [_ i / n ]_ A )
114 113 breq1d 
 |-  ( x = i -> ( B <_ [_ I / n ]_ A <-> [_ i / n ]_ A <_ [_ I / n ]_ A ) )
115 107 114 imbi12d 
 |-  ( x = i -> ( ( ( M <_ I /\ I <_ x ) -> B <_ [_ I / n ]_ A ) <-> ( ( M <_ I /\ I <_ i ) -> [_ i / n ]_ A <_ [_ I / n ]_ A ) ) )
116 115 rspcv 
 |-  ( i e. RR+ -> ( A. x e. RR+ ( ( M <_ I /\ I <_ x ) -> B <_ [_ I / n ]_ A ) -> ( ( M <_ I /\ I <_ i ) -> [_ i / n ]_ A <_ [_ I / n ]_ A ) ) )
117 59 92 105 116 syl3c 
 |-  ( ( ( ph /\ I e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( ( |_ ` I ) + 1 ) ) ) -> [_ i / n ]_ A <_ [_ I / n ]_ A )
118 117 68 71 3brtr4d 
 |-  ( ( ( ph /\ I e. ( M [,) +oo ) ) /\ i e. ( ZZ>= ` ( ( |_ ` I ) + 1 ) ) ) -> ( ( n e. RR+ |-> A ) ` i ) <_ ( ( ( ZZ>= ` ( ( |_ ` I ) + 1 ) ) X. { [_ I / n ]_ A } ) ` i ) )
119 22 28 37 51 69 73 118 climle 
 |-  ( ( ph /\ I e. ( M [,) +oo ) ) -> 0 <_ [_ I / n ]_ A )
120 119 ex 
 |-  ( ph -> ( I e. ( M [,) +oo ) -> 0 <_ [_ I / n ]_ A ) )
121 21 120 jca 
 |-  ( ph -> ( ( I e. RR+ -> [_ I / n ]_ A e. RR ) /\ ( I e. ( M [,) +oo ) -> 0 <_ [_ I / n ]_ A ) ) )