Metamath Proof Explorer

Theorem eulerpartlemgc

Description: Lemma for eulerpart . (Contributed by Thierry Arnoux, 9-Aug-2018)

Ref Expression
Hypotheses eulerpartlems.r 
|- R = { f | ( `' f " NN ) e. Fin }
eulerpartlems.s 
|- S = ( f e. ( ( NN0 ^m NN ) i^i R ) |-> sum_ k e. NN ( ( f ` k ) x. k ) )
Assertion eulerpartlemgc 
|- ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ ( t e. NN /\ n e. ( bits ` ( A ` t ) ) ) ) -> ( ( 2 ^ n ) x. t ) <_ ( S ` A ) )

Proof

Step Hyp Ref Expression
1 eulerpartlems.r 
 |-  R = { f | ( `' f " NN ) e. Fin }
2 eulerpartlems.s 
 |-  S = ( f e. ( ( NN0 ^m NN ) i^i R ) |-> sum_ k e. NN ( ( f ` k ) x. k ) )
3 2re 
 |-  2 e. RR
4 3 a1i 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ ( t e. NN /\ n e. ( bits ` ( A ` t ) ) ) ) -> 2 e. RR )
5 bitsss 
 |-  ( bits ` ( A ` t ) ) C_ NN0
6 simprr 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ ( t e. NN /\ n e. ( bits ` ( A ` t ) ) ) ) -> n e. ( bits ` ( A ` t ) ) )
7 5 6 sselid 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ ( t e. NN /\ n e. ( bits ` ( A ` t ) ) ) ) -> n e. NN0 )
8 4 7 reexpcld 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ ( t e. NN /\ n e. ( bits ` ( A ` t ) ) ) ) -> ( 2 ^ n ) e. RR )
9 simprl 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ ( t e. NN /\ n e. ( bits ` ( A ` t ) ) ) ) -> t e. NN )
10 9 nnred 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ ( t e. NN /\ n e. ( bits ` ( A ` t ) ) ) ) -> t e. RR )
11 8 10 remulcld 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ ( t e. NN /\ n e. ( bits ` ( A ` t ) ) ) ) -> ( ( 2 ^ n ) x. t ) e. RR )
12 1 2 eulerpartlemelr 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> ( A : NN --> NN0 /\ ( `' A " NN ) e. Fin ) )
13 12 simpld 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> A : NN --> NN0 )
14 13 ffvelcdmda 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ t e. NN ) -> ( A ` t ) e. NN0 )
15 14 adantrr 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ ( t e. NN /\ n e. ( bits ` ( A ` t ) ) ) ) -> ( A ` t ) e. NN0 )
16 15 nn0red 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ ( t e. NN /\ n e. ( bits ` ( A ` t ) ) ) ) -> ( A ` t ) e. RR )
17 16 10 remulcld 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ ( t e. NN /\ n e. ( bits ` ( A ` t ) ) ) ) -> ( ( A ` t ) x. t ) e. RR )
18 1 2 eulerpartlemsf 
 |-  S : ( ( NN0 ^m NN ) i^i R ) --> NN0
19 18 ffvelcdmi 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> ( S ` A ) e. NN0 )
20 19 adantr 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ ( t e. NN /\ n e. ( bits ` ( A ` t ) ) ) ) -> ( S ` A ) e. NN0 )
21 20 nn0red 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ ( t e. NN /\ n e. ( bits ` ( A ` t ) ) ) ) -> ( S ` A ) e. RR )
22 14 nn0red 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ t e. NN ) -> ( A ` t ) e. RR )
23 22 adantrr 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ ( t e. NN /\ n e. ( bits ` ( A ` t ) ) ) ) -> ( A ` t ) e. RR )
24 9 nnrpd 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ ( t e. NN /\ n e. ( bits ` ( A ` t ) ) ) ) -> t e. RR+ )
25 24 rprege0d 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ ( t e. NN /\ n e. ( bits ` ( A ` t ) ) ) ) -> ( t e. RR /\ 0 <_ t ) )
26 bitsfi 
 |-  ( ( A ` t ) e. NN0 -> ( bits ` ( A ` t ) ) e. Fin )
27 15 26 syl 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ ( t e. NN /\ n e. ( bits ` ( A ` t ) ) ) ) -> ( bits ` ( A ` t ) ) e. Fin )
28 3 a1i 
 |-  ( ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ ( t e. NN /\ n e. ( bits ` ( A ` t ) ) ) ) /\ i e. ( bits ` ( A ` t ) ) ) -> 2 e. RR )
29 5 a1i 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ ( t e. NN /\ n e. ( bits ` ( A ` t ) ) ) ) -> ( bits ` ( A ` t ) ) C_ NN0 )
30 29 sselda 
 |-  ( ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ ( t e. NN /\ n e. ( bits ` ( A ` t ) ) ) ) /\ i e. ( bits ` ( A ` t ) ) ) -> i e. NN0 )
31 28 30 reexpcld 
 |-  ( ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ ( t e. NN /\ n e. ( bits ` ( A ` t ) ) ) ) /\ i e. ( bits ` ( A ` t ) ) ) -> ( 2 ^ i ) e. RR )
32 0le2 
 |-  0 <_ 2
33 32 a1i 
 |-  ( ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ ( t e. NN /\ n e. ( bits ` ( A ` t ) ) ) ) /\ i e. ( bits ` ( A ` t ) ) ) -> 0 <_ 2 )
34 28 30 33 expge0d 
 |-  ( ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ ( t e. NN /\ n e. ( bits ` ( A ` t ) ) ) ) /\ i e. ( bits ` ( A ` t ) ) ) -> 0 <_ ( 2 ^ i ) )
35 6 snssd 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ ( t e. NN /\ n e. ( bits ` ( A ` t ) ) ) ) -> { n } C_ ( bits ` ( A ` t ) ) )
36 27 31 34 35 fsumless 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ ( t e. NN /\ n e. ( bits ` ( A ` t ) ) ) ) -> sum_ i e. { n } ( 2 ^ i ) <_ sum_ i e. ( bits ` ( A ` t ) ) ( 2 ^ i ) )
37 8 recnd 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ ( t e. NN /\ n e. ( bits ` ( A ` t ) ) ) ) -> ( 2 ^ n ) e. CC )
38 oveq2 
 |-  ( i = n -> ( 2 ^ i ) = ( 2 ^ n ) )
39 38 sumsn 
 |-  ( ( n e. ( bits ` ( A ` t ) ) /\ ( 2 ^ n ) e. CC ) -> sum_ i e. { n } ( 2 ^ i ) = ( 2 ^ n ) )
40 6 37 39 syl2anc 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ ( t e. NN /\ n e. ( bits ` ( A ` t ) ) ) ) -> sum_ i e. { n } ( 2 ^ i ) = ( 2 ^ n ) )
41 bitsinv1 
 |-  ( ( A ` t ) e. NN0 -> sum_ i e. ( bits ` ( A ` t ) ) ( 2 ^ i ) = ( A ` t ) )
42 15 41 syl 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ ( t e. NN /\ n e. ( bits ` ( A ` t ) ) ) ) -> sum_ i e. ( bits ` ( A ` t ) ) ( 2 ^ i ) = ( A ` t ) )
43 36 40 42 3brtr3d 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ ( t e. NN /\ n e. ( bits ` ( A ` t ) ) ) ) -> ( 2 ^ n ) <_ ( A ` t ) )
44 lemul1a 
 |-  ( ( ( ( 2 ^ n ) e. RR /\ ( A ` t ) e. RR /\ ( t e. RR /\ 0 <_ t ) ) /\ ( 2 ^ n ) <_ ( A ` t ) ) -> ( ( 2 ^ n ) x. t ) <_ ( ( A ` t ) x. t ) )
45 8 23 25 43 44 syl31anc 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ ( t e. NN /\ n e. ( bits ` ( A ` t ) ) ) ) -> ( ( 2 ^ n ) x. t ) <_ ( ( A ` t ) x. t ) )
46 fzfid 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ t e. ( 1 ... ( S ` A ) ) ) -> ( 1 ... ( S ` A ) ) e. Fin )
47 elfznn 
 |-  ( k e. ( 1 ... ( S ` A ) ) -> k e. NN )
48 ffvelcdm 
 |-  ( ( A : NN --> NN0 /\ k e. NN ) -> ( A ` k ) e. NN0 )
49 13 47 48 syl2an 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( 1 ... ( S ` A ) ) ) -> ( A ` k ) e. NN0 )
50 49 nn0red 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( 1 ... ( S ` A ) ) ) -> ( A ` k ) e. RR )
51 47 adantl 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( 1 ... ( S ` A ) ) ) -> k e. NN )
52 51 nnred 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( 1 ... ( S ` A ) ) ) -> k e. RR )
53 50 52 remulcld 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( 1 ... ( S ` A ) ) ) -> ( ( A ` k ) x. k ) e. RR )
54 53 adantlr 
 |-  ( ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ t e. ( 1 ... ( S ` A ) ) ) /\ k e. ( 1 ... ( S ` A ) ) ) -> ( ( A ` k ) x. k ) e. RR )
55 49 nn0ge0d 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( 1 ... ( S ` A ) ) ) -> 0 <_ ( A ` k ) )
56 0red 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( 1 ... ( S ` A ) ) ) -> 0 e. RR )
57 51 nngt0d 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( 1 ... ( S ` A ) ) ) -> 0 < k )
58 56 52 57 ltled 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( 1 ... ( S ` A ) ) ) -> 0 <_ k )
59 50 52 55 58 mulge0d 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( 1 ... ( S ` A ) ) ) -> 0 <_ ( ( A ` k ) x. k ) )
60 59 adantlr 
 |-  ( ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ t e. ( 1 ... ( S ` A ) ) ) /\ k e. ( 1 ... ( S ` A ) ) ) -> 0 <_ ( ( A ` k ) x. k ) )
61 fveq2 
 |-  ( k = t -> ( A ` k ) = ( A ` t ) )
62 id 
 |-  ( k = t -> k = t )
63 61 62 oveq12d 
 |-  ( k = t -> ( ( A ` k ) x. k ) = ( ( A ` t ) x. t ) )
64 simpr 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ t e. ( 1 ... ( S ` A ) ) ) -> t e. ( 1 ... ( S ` A ) ) )
65 46 54 60 63 64 fsumge1 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ t e. ( 1 ... ( S ` A ) ) ) -> ( ( A ` t ) x. t ) <_ sum_ k e. ( 1 ... ( S ` A ) ) ( ( A ` k ) x. k ) )
66 65 adantlr 
 |-  ( ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ t e. NN ) /\ t e. ( 1 ... ( S ` A ) ) ) -> ( ( A ` t ) x. t ) <_ sum_ k e. ( 1 ... ( S ` A ) ) ( ( A ` k ) x. k ) )
67 eldif 
 |-  ( t e. ( NN \ ( 1 ... ( S ` A ) ) ) <-> ( t e. NN /\ -. t e. ( 1 ... ( S ` A ) ) ) )
68 nndiffz1 
 |-  ( ( S ` A ) e. NN0 -> ( NN \ ( 1 ... ( S ` A ) ) ) = ( ZZ>= ` ( ( S ` A ) + 1 ) ) )
69 68 eleq2d 
 |-  ( ( S ` A ) e. NN0 -> ( t e. ( NN \ ( 1 ... ( S ` A ) ) ) <-> t e. ( ZZ>= ` ( ( S ` A ) + 1 ) ) ) )
70 19 69 syl 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> ( t e. ( NN \ ( 1 ... ( S ` A ) ) ) <-> t e. ( ZZ>= ` ( ( S ` A ) + 1 ) ) ) )
71 70 pm5.32i 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ t e. ( NN \ ( 1 ... ( S ` A ) ) ) ) <-> ( A e. ( ( NN0 ^m NN ) i^i R ) /\ t e. ( ZZ>= ` ( ( S ` A ) + 1 ) ) ) )
72 1 2 eulerpartlems 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ t e. ( ZZ>= ` ( ( S ` A ) + 1 ) ) ) -> ( A ` t ) = 0 )
73 71 72 sylbi 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ t e. ( NN \ ( 1 ... ( S ` A ) ) ) ) -> ( A ` t ) = 0 )
74 73 oveq1d 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ t e. ( NN \ ( 1 ... ( S ` A ) ) ) ) -> ( ( A ` t ) x. t ) = ( 0 x. t ) )
75 simpr 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ t e. ( NN \ ( 1 ... ( S ` A ) ) ) ) -> t e. ( NN \ ( 1 ... ( S ` A ) ) ) )
76 75 eldifad 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ t e. ( NN \ ( 1 ... ( S ` A ) ) ) ) -> t e. NN )
77 76 nncnd 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ t e. ( NN \ ( 1 ... ( S ` A ) ) ) ) -> t e. CC )
78 77 mul02d 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ t e. ( NN \ ( 1 ... ( S ` A ) ) ) ) -> ( 0 x. t ) = 0 )
79 74 78 eqtrd 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ t e. ( NN \ ( 1 ... ( S ` A ) ) ) ) -> ( ( A ` t ) x. t ) = 0 )
80 fzfid 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> ( 1 ... ( S ` A ) ) e. Fin )
81 80 53 59 fsumge0 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> 0 <_ sum_ k e. ( 1 ... ( S ` A ) ) ( ( A ` k ) x. k ) )
82 81 adantr 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ t e. ( NN \ ( 1 ... ( S ` A ) ) ) ) -> 0 <_ sum_ k e. ( 1 ... ( S ` A ) ) ( ( A ` k ) x. k ) )
83 79 82 eqbrtrd 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ t e. ( NN \ ( 1 ... ( S ` A ) ) ) ) -> ( ( A ` t ) x. t ) <_ sum_ k e. ( 1 ... ( S ` A ) ) ( ( A ` k ) x. k ) )
84 67 83 sylan2br 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ ( t e. NN /\ -. t e. ( 1 ... ( S ` A ) ) ) ) -> ( ( A ` t ) x. t ) <_ sum_ k e. ( 1 ... ( S ` A ) ) ( ( A ` k ) x. k ) )
85 84 anassrs 
 |-  ( ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ t e. NN ) /\ -. t e. ( 1 ... ( S ` A ) ) ) -> ( ( A ` t ) x. t ) <_ sum_ k e. ( 1 ... ( S ` A ) ) ( ( A ` k ) x. k ) )
86 66 85 pm2.61dan 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ t e. NN ) -> ( ( A ` t ) x. t ) <_ sum_ k e. ( 1 ... ( S ` A ) ) ( ( A ` k ) x. k ) )
87 1 2 eulerpartlemsv3 
 |-  ( A e. ( ( NN0 ^m NN ) i^i R ) -> ( S ` A ) = sum_ k e. ( 1 ... ( S ` A ) ) ( ( A ` k ) x. k ) )
88 87 adantr 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ t e. NN ) -> ( S ` A ) = sum_ k e. ( 1 ... ( S ` A ) ) ( ( A ` k ) x. k ) )
89 86 88 breqtrrd 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ t e. NN ) -> ( ( A ` t ) x. t ) <_ ( S ` A ) )
90 89 adantrr 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ ( t e. NN /\ n e. ( bits ` ( A ` t ) ) ) ) -> ( ( A ` t ) x. t ) <_ ( S ` A ) )
91 11 17 21 45 90 letrd 
 |-  ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ ( t e. NN /\ n e. ( bits ` ( A ` t ) ) ) ) -> ( ( 2 ^ n ) x. t ) <_ ( S ` A ) )