Metamath Proof Explorer

Theorem fsumvma2

Description: Apply fsumvma for the common case of all numbers less than a real number A . (Contributed by Mario Carneiro, 30-Apr-2016)

Ref Expression
Hypotheses fsumvma2.1 
|- ( x = ( p ^ k ) -> B = C )
fsumvma2.2 
|- ( ph -> A e. RR )
fsumvma2.3 
|- ( ( ph /\ x e. ( 1 ... ( |_ ` A ) ) ) -> B e. CC )
fsumvma2.4 
|- ( ( ph /\ ( x e. ( 1 ... ( |_ ` A ) ) /\ ( Lam ` x ) = 0 ) ) -> B = 0 )
Assertion fsumvma2 
|- ( ph -> sum_ x e. ( 1 ... ( |_ ` A ) ) B = sum_ p e. ( ( 0 [,] A ) i^i Prime ) sum_ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) C )

Proof

Step Hyp Ref Expression
1 fsumvma2.1 
 |-  ( x = ( p ^ k ) -> B = C )
2 fsumvma2.2 
 |-  ( ph -> A e. RR )
3 fsumvma2.3 
 |-  ( ( ph /\ x e. ( 1 ... ( |_ ` A ) ) ) -> B e. CC )
4 fsumvma2.4 
 |-  ( ( ph /\ ( x e. ( 1 ... ( |_ ` A ) ) /\ ( Lam ` x ) = 0 ) ) -> B = 0 )
5 fzfid 
 |-  ( ph -> ( 1 ... ( |_ ` A ) ) e. Fin )
6 fz1ssnn 
 |-  ( 1 ... ( |_ ` A ) ) C_ NN
7 6 a1i 
 |-  ( ph -> ( 1 ... ( |_ ` A ) ) C_ NN )
8 ppifi 
 |-  ( A e. RR -> ( ( 0 [,] A ) i^i Prime ) e. Fin )
9 2 8 syl 
 |-  ( ph -> ( ( 0 [,] A ) i^i Prime ) e. Fin )
10 elinel2 
 |-  ( p e. ( ( 0 [,] A ) i^i Prime ) -> p e. Prime )
11 elfznn 
 |-  ( k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) -> k e. NN )
12 10 11 anim12i 
 |-  ( ( p e. ( ( 0 [,] A ) i^i Prime ) /\ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) -> ( p e. Prime /\ k e. NN ) )
13 12 pm4.71ri 
 |-  ( ( p e. ( ( 0 [,] A ) i^i Prime ) /\ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) <-> ( ( p e. Prime /\ k e. NN ) /\ ( p e. ( ( 0 [,] A ) i^i Prime ) /\ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) ) )
14 2 adantr 
 |-  ( ( ph /\ ( p e. Prime /\ k e. NN ) ) -> A e. RR )
15 prmnn 
 |-  ( p e. Prime -> p e. NN )
16 15 ad2antrl 
 |-  ( ( ph /\ ( p e. Prime /\ k e. NN ) ) -> p e. NN )
17 nnnn0 
 |-  ( k e. NN -> k e. NN0 )
18 17 ad2antll 
 |-  ( ( ph /\ ( p e. Prime /\ k e. NN ) ) -> k e. NN0 )
19 16 18 nnexpcld 
 |-  ( ( ph /\ ( p e. Prime /\ k e. NN ) ) -> ( p ^ k ) e. NN )
20 19 nnzd 
 |-  ( ( ph /\ ( p e. Prime /\ k e. NN ) ) -> ( p ^ k ) e. ZZ )
21 flge 
 |-  ( ( A e. RR /\ ( p ^ k ) e. ZZ ) -> ( ( p ^ k ) <_ A <-> ( p ^ k ) <_ ( |_ ` A ) ) )
22 14 20 21 syl2anc 
 |-  ( ( ph /\ ( p e. Prime /\ k e. NN ) ) -> ( ( p ^ k ) <_ A <-> ( p ^ k ) <_ ( |_ ` A ) ) )
23 simplrl 
 |-  ( ( ( ph /\ ( p e. Prime /\ k e. NN ) ) /\ p e. ( 0 [,] A ) ) -> p e. Prime )
24 23 15 syl 
 |-  ( ( ( ph /\ ( p e. Prime /\ k e. NN ) ) /\ p e. ( 0 [,] A ) ) -> p e. NN )
25 24 nnrpd 
 |-  ( ( ( ph /\ ( p e. Prime /\ k e. NN ) ) /\ p e. ( 0 [,] A ) ) -> p e. RR+ )
26 simplrr 
 |-  ( ( ( ph /\ ( p e. Prime /\ k e. NN ) ) /\ p e. ( 0 [,] A ) ) -> k e. NN )
27 26 nnzd 
 |-  ( ( ( ph /\ ( p e. Prime /\ k e. NN ) ) /\ p e. ( 0 [,] A ) ) -> k e. ZZ )
28 relogexp 
 |-  ( ( p e. RR+ /\ k e. ZZ ) -> ( log ` ( p ^ k ) ) = ( k x. ( log ` p ) ) )
29 25 27 28 syl2anc 
 |-  ( ( ( ph /\ ( p e. Prime /\ k e. NN ) ) /\ p e. ( 0 [,] A ) ) -> ( log ` ( p ^ k ) ) = ( k x. ( log ` p ) ) )
30 29 breq1d 
 |-  ( ( ( ph /\ ( p e. Prime /\ k e. NN ) ) /\ p e. ( 0 [,] A ) ) -> ( ( log ` ( p ^ k ) ) <_ ( log ` A ) <-> ( k x. ( log ` p ) ) <_ ( log ` A ) ) )
31 26 nnred 
 |-  ( ( ( ph /\ ( p e. Prime /\ k e. NN ) ) /\ p e. ( 0 [,] A ) ) -> k e. RR )
32 14 adantr 
 |-  ( ( ( ph /\ ( p e. Prime /\ k e. NN ) ) /\ p e. ( 0 [,] A ) ) -> A e. RR )
33 0red 
 |-  ( ( ( ph /\ ( p e. Prime /\ k e. NN ) ) /\ p e. ( 0 [,] A ) ) -> 0 e. RR )
34 16 nnred 
 |-  ( ( ph /\ ( p e. Prime /\ k e. NN ) ) -> p e. RR )
35 34 adantr 
 |-  ( ( ( ph /\ ( p e. Prime /\ k e. NN ) ) /\ p e. ( 0 [,] A ) ) -> p e. RR )
36 24 nngt0d 
 |-  ( ( ( ph /\ ( p e. Prime /\ k e. NN ) ) /\ p e. ( 0 [,] A ) ) -> 0 < p )
37 0red 
 |-  ( ( ph /\ ( p e. Prime /\ k e. NN ) ) -> 0 e. RR )
38 16 nnnn0d 
 |-  ( ( ph /\ ( p e. Prime /\ k e. NN ) ) -> p e. NN0 )
39 38 nn0ge0d 
 |-  ( ( ph /\ ( p e. Prime /\ k e. NN ) ) -> 0 <_ p )
40 elicc2 
 |-  ( ( 0 e. RR /\ A e. RR ) -> ( p e. ( 0 [,] A ) <-> ( p e. RR /\ 0 <_ p /\ p <_ A ) ) )
41 df-3an 
 |-  ( ( p e. RR /\ 0 <_ p /\ p <_ A ) <-> ( ( p e. RR /\ 0 <_ p ) /\ p <_ A ) )
42 40 41 bitrdi 
 |-  ( ( 0 e. RR /\ A e. RR ) -> ( p e. ( 0 [,] A ) <-> ( ( p e. RR /\ 0 <_ p ) /\ p <_ A ) ) )
43 42 baibd 
 |-  ( ( ( 0 e. RR /\ A e. RR ) /\ ( p e. RR /\ 0 <_ p ) ) -> ( p e. ( 0 [,] A ) <-> p <_ A ) )
44 37 14 34 39 43 syl22anc 
 |-  ( ( ph /\ ( p e. Prime /\ k e. NN ) ) -> ( p e. ( 0 [,] A ) <-> p <_ A ) )
45 44 biimpa 
 |-  ( ( ( ph /\ ( p e. Prime /\ k e. NN ) ) /\ p e. ( 0 [,] A ) ) -> p <_ A )
46 33 35 32 36 45 ltletrd 
 |-  ( ( ( ph /\ ( p e. Prime /\ k e. NN ) ) /\ p e. ( 0 [,] A ) ) -> 0 < A )
47 32 46 elrpd 
 |-  ( ( ( ph /\ ( p e. Prime /\ k e. NN ) ) /\ p e. ( 0 [,] A ) ) -> A e. RR+ )
48 47 relogcld 
 |-  ( ( ( ph /\ ( p e. Prime /\ k e. NN ) ) /\ p e. ( 0 [,] A ) ) -> ( log ` A ) e. RR )
49 prmuz2 
 |-  ( p e. Prime -> p e. ( ZZ>= ` 2 ) )
50 eluzelre 
 |-  ( p e. ( ZZ>= ` 2 ) -> p e. RR )
51 eluz2gt1 
 |-  ( p e. ( ZZ>= ` 2 ) -> 1 < p )
52 50 51 rplogcld 
 |-  ( p e. ( ZZ>= ` 2 ) -> ( log ` p ) e. RR+ )
53 23 49 52 3syl 
 |-  ( ( ( ph /\ ( p e. Prime /\ k e. NN ) ) /\ p e. ( 0 [,] A ) ) -> ( log ` p ) e. RR+ )
54 31 48 53 lemuldivd 
 |-  ( ( ( ph /\ ( p e. Prime /\ k e. NN ) ) /\ p e. ( 0 [,] A ) ) -> ( ( k x. ( log ` p ) ) <_ ( log ` A ) <-> k <_ ( ( log ` A ) / ( log ` p ) ) ) )
55 48 53 rerpdivcld 
 |-  ( ( ( ph /\ ( p e. Prime /\ k e. NN ) ) /\ p e. ( 0 [,] A ) ) -> ( ( log ` A ) / ( log ` p ) ) e. RR )
56 flge 
 |-  ( ( ( ( log ` A ) / ( log ` p ) ) e. RR /\ k e. ZZ ) -> ( k <_ ( ( log ` A ) / ( log ` p ) ) <-> k <_ ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) )
57 55 27 56 syl2anc 
 |-  ( ( ( ph /\ ( p e. Prime /\ k e. NN ) ) /\ p e. ( 0 [,] A ) ) -> ( k <_ ( ( log ` A ) / ( log ` p ) ) <-> k <_ ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) )
58 30 54 57 3bitrd 
 |-  ( ( ( ph /\ ( p e. Prime /\ k e. NN ) ) /\ p e. ( 0 [,] A ) ) -> ( ( log ` ( p ^ k ) ) <_ ( log ` A ) <-> k <_ ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) )
59 19 adantr 
 |-  ( ( ( ph /\ ( p e. Prime /\ k e. NN ) ) /\ p e. ( 0 [,] A ) ) -> ( p ^ k ) e. NN )
60 59 nnrpd 
 |-  ( ( ( ph /\ ( p e. Prime /\ k e. NN ) ) /\ p e. ( 0 [,] A ) ) -> ( p ^ k ) e. RR+ )
61 60 47 logled 
 |-  ( ( ( ph /\ ( p e. Prime /\ k e. NN ) ) /\ p e. ( 0 [,] A ) ) -> ( ( p ^ k ) <_ A <-> ( log ` ( p ^ k ) ) <_ ( log ` A ) ) )
62 simprr 
 |-  ( ( ph /\ ( p e. Prime /\ k e. NN ) ) -> k e. NN )
63 nnuz 
 |-  NN = ( ZZ>= ` 1 )
64 62 63 eleqtrdi 
 |-  ( ( ph /\ ( p e. Prime /\ k e. NN ) ) -> k e. ( ZZ>= ` 1 ) )
65 64 adantr 
 |-  ( ( ( ph /\ ( p e. Prime /\ k e. NN ) ) /\ p e. ( 0 [,] A ) ) -> k e. ( ZZ>= ` 1 ) )
66 55 flcld 
 |-  ( ( ( ph /\ ( p e. Prime /\ k e. NN ) ) /\ p e. ( 0 [,] A ) ) -> ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) e. ZZ )
67 elfz5 
 |-  ( ( k e. ( ZZ>= ` 1 ) /\ ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) e. ZZ ) -> ( k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) <-> k <_ ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) )
68 65 66 67 syl2anc 
 |-  ( ( ( ph /\ ( p e. Prime /\ k e. NN ) ) /\ p e. ( 0 [,] A ) ) -> ( k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) <-> k <_ ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) )
69 58 61 68 3bitr4d 
 |-  ( ( ( ph /\ ( p e. Prime /\ k e. NN ) ) /\ p e. ( 0 [,] A ) ) -> ( ( p ^ k ) <_ A <-> k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) )
70 69 pm5.32da 
 |-  ( ( ph /\ ( p e. Prime /\ k e. NN ) ) -> ( ( p e. ( 0 [,] A ) /\ ( p ^ k ) <_ A ) <-> ( p e. ( 0 [,] A ) /\ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) ) )
71 16 nncnd 
 |-  ( ( ph /\ ( p e. Prime /\ k e. NN ) ) -> p e. CC )
72 71 exp1d 
 |-  ( ( ph /\ ( p e. Prime /\ k e. NN ) ) -> ( p ^ 1 ) = p )
73 16 nnge1d 
 |-  ( ( ph /\ ( p e. Prime /\ k e. NN ) ) -> 1 <_ p )
74 34 73 64 leexp2ad 
 |-  ( ( ph /\ ( p e. Prime /\ k e. NN ) ) -> ( p ^ 1 ) <_ ( p ^ k ) )
75 72 74 eqbrtrrd 
 |-  ( ( ph /\ ( p e. Prime /\ k e. NN ) ) -> p <_ ( p ^ k ) )
76 19 nnred 
 |-  ( ( ph /\ ( p e. Prime /\ k e. NN ) ) -> ( p ^ k ) e. RR )
77 letr 
 |-  ( ( p e. RR /\ ( p ^ k ) e. RR /\ A e. RR ) -> ( ( p <_ ( p ^ k ) /\ ( p ^ k ) <_ A ) -> p <_ A ) )
78 34 76 14 77 syl3anc 
 |-  ( ( ph /\ ( p e. Prime /\ k e. NN ) ) -> ( ( p <_ ( p ^ k ) /\ ( p ^ k ) <_ A ) -> p <_ A ) )
79 75 78 mpand 
 |-  ( ( ph /\ ( p e. Prime /\ k e. NN ) ) -> ( ( p ^ k ) <_ A -> p <_ A ) )
80 79 44 sylibrd 
 |-  ( ( ph /\ ( p e. Prime /\ k e. NN ) ) -> ( ( p ^ k ) <_ A -> p e. ( 0 [,] A ) ) )
81 80 pm4.71rd 
 |-  ( ( ph /\ ( p e. Prime /\ k e. NN ) ) -> ( ( p ^ k ) <_ A <-> ( p e. ( 0 [,] A ) /\ ( p ^ k ) <_ A ) ) )
82 elin 
 |-  ( p e. ( ( 0 [,] A ) i^i Prime ) <-> ( p e. ( 0 [,] A ) /\ p e. Prime ) )
83 82 rbaib 
 |-  ( p e. Prime -> ( p e. ( ( 0 [,] A ) i^i Prime ) <-> p e. ( 0 [,] A ) ) )
84 83 ad2antrl 
 |-  ( ( ph /\ ( p e. Prime /\ k e. NN ) ) -> ( p e. ( ( 0 [,] A ) i^i Prime ) <-> p e. ( 0 [,] A ) ) )
85 84 anbi1d 
 |-  ( ( ph /\ ( p e. Prime /\ k e. NN ) ) -> ( ( p e. ( ( 0 [,] A ) i^i Prime ) /\ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) <-> ( p e. ( 0 [,] A ) /\ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) ) )
86 70 81 85 3bitr4rd 
 |-  ( ( ph /\ ( p e. Prime /\ k e. NN ) ) -> ( ( p e. ( ( 0 [,] A ) i^i Prime ) /\ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) <-> ( p ^ k ) <_ A ) )
87 19 63 eleqtrdi 
 |-  ( ( ph /\ ( p e. Prime /\ k e. NN ) ) -> ( p ^ k ) e. ( ZZ>= ` 1 ) )
88 14 flcld 
 |-  ( ( ph /\ ( p e. Prime /\ k e. NN ) ) -> ( |_ ` A ) e. ZZ )
89 elfz5 
 |-  ( ( ( p ^ k ) e. ( ZZ>= ` 1 ) /\ ( |_ ` A ) e. ZZ ) -> ( ( p ^ k ) e. ( 1 ... ( |_ ` A ) ) <-> ( p ^ k ) <_ ( |_ ` A ) ) )
90 87 88 89 syl2anc 
 |-  ( ( ph /\ ( p e. Prime /\ k e. NN ) ) -> ( ( p ^ k ) e. ( 1 ... ( |_ ` A ) ) <-> ( p ^ k ) <_ ( |_ ` A ) ) )
91 22 86 90 3bitr4d 
 |-  ( ( ph /\ ( p e. Prime /\ k e. NN ) ) -> ( ( p e. ( ( 0 [,] A ) i^i Prime ) /\ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) <-> ( p ^ k ) e. ( 1 ... ( |_ ` A ) ) ) )
92 91 pm5.32da 
 |-  ( ph -> ( ( ( p e. Prime /\ k e. NN ) /\ ( p e. ( ( 0 [,] A ) i^i Prime ) /\ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) ) <-> ( ( p e. Prime /\ k e. NN ) /\ ( p ^ k ) e. ( 1 ... ( |_ ` A ) ) ) ) )
93 13 92 bitrid 
 |-  ( ph -> ( ( p e. ( ( 0 [,] A ) i^i Prime ) /\ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) <-> ( ( p e. Prime /\ k e. NN ) /\ ( p ^ k ) e. ( 1 ... ( |_ ` A ) ) ) ) )
94 1 5 7 9 93 3 4 fsumvma 
 |-  ( ph -> sum_ x e. ( 1 ... ( |_ ` A ) ) B = sum_ p e. ( ( 0 [,] A ) i^i Prime ) sum_ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) C )