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 syl5bb
 |-  ( 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 )