Step | Hyp | Ref
| Expression |
1 | | o1fsum.2 |
. . 3
β’ (π β (π β β β¦ π΄) β π(1)) |
2 | | nnssre 12164 |
. . . . 5
β’ β
β β |
3 | 2 | a1i 11 |
. . . 4
β’ (π β β β
β) |
4 | | o1fsum.1 |
. . . . 5
β’ ((π β§ π β β) β π΄ β π) |
5 | 4, 1 | o1mptrcl 15512 |
. . . 4
β’ ((π β§ π β β) β π΄ β β) |
6 | | 1red 11163 |
. . . 4
β’ (π β 1 β
β) |
7 | 3, 5, 6 | elo1mpt2 15424 |
. . 3
β’ (π β ((π β β β¦ π΄) β π(1) β βπ β
(1[,)+β)βπ
β β βπ
β β (π β€
π β (absβπ΄) β€ π))) |
8 | 1, 7 | mpbid 231 |
. 2
β’ (π β βπ β (1[,)+β)βπ β β βπ β β (π β€ π β (absβπ΄) β€ π)) |
9 | | rpssre 12929 |
. . . . . 6
β’
β+ β β |
10 | 9 | a1i 11 |
. . . . 5
β’ (((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β β+ β
β) |
11 | | nfcv 2908 |
. . . . . . . 8
β’
β²ππ΄ |
12 | | nfcsb1v 3885 |
. . . . . . . 8
β’
β²πβ¦π / πβ¦π΄ |
13 | | csbeq1a 3874 |
. . . . . . . 8
β’ (π = π β π΄ = β¦π / πβ¦π΄) |
14 | 11, 12, 13 | cbvsumi 15589 |
. . . . . . 7
β’
Ξ£π β
(1...(ββπ₯))π΄ = Ξ£π β (1...(ββπ₯))β¦π / πβ¦π΄ |
15 | | fzfid 13885 |
. . . . . . . 8
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ π₯ β β+) β
(1...(ββπ₯))
β Fin) |
16 | | o1f 15418 |
. . . . . . . . . . . . 13
β’ ((π β β β¦ π΄) β π(1) β
(π β β β¦
π΄):dom (π β β β¦ π΄)βΆβ) |
17 | 1, 16 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (π β β β¦ π΄):dom (π β β β¦ π΄)βΆβ) |
18 | 4 | ralrimiva 3144 |
. . . . . . . . . . . . . 14
β’ (π β βπ β β π΄ β π) |
19 | | dmmptg 6199 |
. . . . . . . . . . . . . 14
β’
(βπ β
β π΄ β π β dom (π β β β¦ π΄) = β) |
20 | 18, 19 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β dom (π β β β¦ π΄) = β) |
21 | 20 | feq2d 6659 |
. . . . . . . . . . . 12
β’ (π β ((π β β β¦ π΄):dom (π β β β¦ π΄)βΆβ β (π β β β¦ π΄):ββΆβ)) |
22 | 17, 21 | mpbid 231 |
. . . . . . . . . . 11
β’ (π β (π β β β¦ π΄):ββΆβ) |
23 | | eqid 2737 |
. . . . . . . . . . . 12
β’ (π β β β¦ π΄) = (π β β β¦ π΄) |
24 | 23 | fmpt 7063 |
. . . . . . . . . . 11
β’
(βπ β
β π΄ β β
β (π β β
β¦ π΄):ββΆβ) |
25 | 22, 24 | sylibr 233 |
. . . . . . . . . 10
β’ (π β βπ β β π΄ β β) |
26 | 25 | ad3antrrr 729 |
. . . . . . . . 9
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ π₯ β β+) β
βπ β β
π΄ β
β) |
27 | | elfznn 13477 |
. . . . . . . . 9
β’ (π β
(1...(ββπ₯))
β π β
β) |
28 | 12 | nfel1 2924 |
. . . . . . . . . . 11
β’
β²πβ¦π / πβ¦π΄ β β |
29 | 13 | eleq1d 2823 |
. . . . . . . . . . 11
β’ (π = π β (π΄ β β β β¦π / πβ¦π΄ β β)) |
30 | 28, 29 | rspc 3572 |
. . . . . . . . . 10
β’ (π β β β
(βπ β β
π΄ β β β
β¦π / πβ¦π΄ β β)) |
31 | 30 | impcom 409 |
. . . . . . . . 9
β’
((βπ β
β π΄ β β
β§ π β β)
β β¦π /
πβ¦π΄ β
β) |
32 | 26, 27, 31 | syl2an 597 |
. . . . . . . 8
β’
(((((π β§ (π β (1[,)+β) β§
π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β β¦π /
πβ¦π΄ β
β) |
33 | 15, 32 | fsumcl 15625 |
. . . . . . 7
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))β¦π / πβ¦π΄ β β) |
34 | 14, 33 | eqeltrid 2842 |
. . . . . 6
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))π΄ β β) |
35 | | rpcn 12932 |
. . . . . . 7
β’ (π₯ β β+
β π₯ β
β) |
36 | 35 | adantl 483 |
. . . . . 6
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ π₯ β β+) β π₯ β
β) |
37 | | rpne0 12938 |
. . . . . . 7
β’ (π₯ β β+
β π₯ β
0) |
38 | 37 | adantl 483 |
. . . . . 6
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ π₯ β β+) β π₯ β 0) |
39 | 34, 36, 38 | divcld 11938 |
. . . . 5
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ π₯ β β+) β
(Ξ£π β
(1...(ββπ₯))π΄ / π₯) β β) |
40 | | simplrl 776 |
. . . . . . 7
β’ (((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β π β (1[,)+β)) |
41 | | 1re 11162 |
. . . . . . . 8
β’ 1 β
β |
42 | | elicopnf 13369 |
. . . . . . . 8
β’ (1 β
β β (π β
(1[,)+β) β (π
β β β§ 1 β€ π))) |
43 | 41, 42 | ax-mp 5 |
. . . . . . 7
β’ (π β (1[,)+β) β
(π β β β§ 1
β€ π)) |
44 | 40, 43 | sylib 217 |
. . . . . 6
β’ (((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β (π β β β§ 1 β€ π)) |
45 | 44 | simpld 496 |
. . . . 5
β’ (((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β π β β) |
46 | | fzfid 13885 |
. . . . . . 7
β’ (((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β (1...(ββπ)) β Fin) |
47 | 25 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β βπ β β π΄ β β) |
48 | | elfznn 13477 |
. . . . . . . . 9
β’ (π β
(1...(ββπ))
β π β
β) |
49 | 47, 48, 31 | syl2an 597 |
. . . . . . . 8
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ π β (1...(ββπ))) β β¦π / πβ¦π΄ β β) |
50 | 49 | abscld 15328 |
. . . . . . 7
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ π β (1...(ββπ))) β
(absββ¦π
/ πβ¦π΄) β
β) |
51 | 46, 50 | fsumrecl 15626 |
. . . . . 6
β’ (((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β Ξ£π β (1...(ββπ))(absββ¦π / πβ¦π΄) β β) |
52 | | simplrr 777 |
. . . . . 6
β’ (((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β π β β) |
53 | 51, 52 | readdcld 11191 |
. . . . 5
β’ (((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β (Ξ£π β (1...(ββπ))(absββ¦π / πβ¦π΄) + π) β β) |
54 | 34, 36, 38 | absdivd 15347 |
. . . . . . . 8
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ π₯ β β+) β
(absβ(Ξ£π β
(1...(ββπ₯))π΄ / π₯)) = ((absβΞ£π β (1...(ββπ₯))π΄) / (absβπ₯))) |
55 | 54 | adantrr 716 |
. . . . . . 7
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β (absβ(Ξ£π β
(1...(ββπ₯))π΄ / π₯)) = ((absβΞ£π β (1...(ββπ₯))π΄) / (absβπ₯))) |
56 | | rprege0 12937 |
. . . . . . . . . 10
β’ (π₯ β β+
β (π₯ β β
β§ 0 β€ π₯)) |
57 | 56 | ad2antrl 727 |
. . . . . . . . 9
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β (π₯ β β β§ 0 β€ π₯)) |
58 | | absid 15188 |
. . . . . . . . 9
β’ ((π₯ β β β§ 0 β€
π₯) β (absβπ₯) = π₯) |
59 | 57, 58 | syl 17 |
. . . . . . . 8
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β (absβπ₯) = π₯) |
60 | 59 | oveq2d 7378 |
. . . . . . 7
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β ((absβΞ£π β
(1...(ββπ₯))π΄) / (absβπ₯)) = ((absβΞ£π β (1...(ββπ₯))π΄) / π₯)) |
61 | 55, 60 | eqtrd 2777 |
. . . . . 6
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β (absβ(Ξ£π β
(1...(ββπ₯))π΄ / π₯)) = ((absβΞ£π β (1...(ββπ₯))π΄) / π₯)) |
62 | 34 | adantrr 716 |
. . . . . . . . 9
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β Ξ£π β (1...(ββπ₯))π΄ β β) |
63 | 62 | abscld 15328 |
. . . . . . . 8
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β (absβΞ£π β
(1...(ββπ₯))π΄) β β) |
64 | | fzfid 13885 |
. . . . . . . . 9
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β (1...(ββπ₯)) β Fin) |
65 | 47, 27, 31 | syl2an 597 |
. . . . . . . . . . 11
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ π β (1...(ββπ₯))) β β¦π / πβ¦π΄ β β) |
66 | 65 | adantlr 714 |
. . . . . . . . . 10
β’
(((((π β§ (π β (1[,)+β) β§
π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β§ π β (1...(ββπ₯))) β β¦π / πβ¦π΄ β β) |
67 | 66 | abscld 15328 |
. . . . . . . . 9
β’
(((((π β§ (π β (1[,)+β) β§
π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β§ π β (1...(ββπ₯))) β
(absββ¦π
/ πβ¦π΄) β
β) |
68 | 64, 67 | fsumrecl 15626 |
. . . . . . . 8
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β Ξ£π β (1...(ββπ₯))(absββ¦π / πβ¦π΄) β β) |
69 | 57 | simpld 496 |
. . . . . . . . 9
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β π₯ β β) |
70 | 51 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β Ξ£π β (1...(ββπ))(absββ¦π / πβ¦π΄) β β) |
71 | 52 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β π β β) |
72 | 70, 71 | readdcld 11191 |
. . . . . . . . 9
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β (Ξ£π β (1...(ββπ))(absββ¦π / πβ¦π΄) + π) β β) |
73 | 69, 72 | remulcld 11192 |
. . . . . . . 8
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β (π₯ Β· (Ξ£π β (1...(ββπ))(absββ¦π / πβ¦π΄) + π)) β β) |
74 | 14 | fveq2i 6850 |
. . . . . . . . 9
β’
(absβΞ£π
β (1...(ββπ₯))π΄) = (absβΞ£π β (1...(ββπ₯))β¦π / πβ¦π΄) |
75 | 64, 66 | fsumabs 15693 |
. . . . . . . . 9
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β (absβΞ£π β
(1...(ββπ₯))β¦π / πβ¦π΄) β€ Ξ£π β (1...(ββπ₯))(absββ¦π / πβ¦π΄)) |
76 | 74, 75 | eqbrtrid 5145 |
. . . . . . . 8
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β (absβΞ£π β
(1...(ββπ₯))π΄) β€ Ξ£π β (1...(ββπ₯))(absββ¦π / πβ¦π΄)) |
77 | | fzfid 13885 |
. . . . . . . . . . 11
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β (((ββπ) + 1)...(ββπ₯)) β Fin) |
78 | | ssun2 4138 |
. . . . . . . . . . . . . 14
β’
(((ββπ)
+ 1)...(ββπ₯))
β ((1...(ββπ)) βͺ (((ββπ) + 1)...(ββπ₯))) |
79 | | flge1nn 13733 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ 1 β€
π) β
(ββπ) β
β) |
80 | 44, 79 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β (ββπ) β β) |
81 | 80 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β (ββπ) β β) |
82 | 81 | nnred 12175 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β (ββπ) β β) |
83 | 45 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β π β β) |
84 | | flle 13711 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β
(ββπ) β€
π) |
85 | 83, 84 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β (ββπ) β€ π) |
86 | | simprr 772 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β π β€ π₯) |
87 | 82, 83, 69, 85, 86 | letrd 11319 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β (ββπ) β€ π₯) |
88 | | fznnfl 13774 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β β β
((ββπ) β
(1...(ββπ₯))
β ((ββπ)
β β β§ (ββπ) β€ π₯))) |
89 | 69, 88 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β ((ββπ) β (1...(ββπ₯)) β ((ββπ) β β β§
(ββπ) β€
π₯))) |
90 | 81, 87, 89 | mpbir2and 712 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β (ββπ) β (1...(ββπ₯))) |
91 | | fzsplit 13474 |
. . . . . . . . . . . . . . 15
β’
((ββπ)
β (1...(ββπ₯)) β (1...(ββπ₯)) = ((1...(ββπ)) βͺ (((ββπ) + 1)...(ββπ₯)))) |
92 | 90, 91 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β (1...(ββπ₯)) = ((1...(ββπ)) βͺ (((ββπ) + 1)...(ββπ₯)))) |
93 | 78, 92 | sseqtrrid 4002 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β (((ββπ) + 1)...(ββπ₯)) β (1...(ββπ₯))) |
94 | 93 | sselda 3949 |
. . . . . . . . . . . 12
β’
(((((π β§ (π β (1[,)+β) β§
π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β§ π β (((ββπ) + 1)...(ββπ₯))) β π β (1...(ββπ₯))) |
95 | 65 | abscld 15328 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ π β (1...(ββπ₯))) β
(absββ¦π
/ πβ¦π΄) β
β) |
96 | 95 | adantlr 714 |
. . . . . . . . . . . 12
β’
(((((π β§ (π β (1[,)+β) β§
π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β§ π β (1...(ββπ₯))) β
(absββ¦π
/ πβ¦π΄) β
β) |
97 | 94, 96 | syldan 592 |
. . . . . . . . . . 11
β’
(((((π β§ (π β (1[,)+β) β§
π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β§ π β (((ββπ) + 1)...(ββπ₯))) β (absββ¦π / πβ¦π΄) β β) |
98 | 77, 97 | fsumrecl 15626 |
. . . . . . . . . 10
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β Ξ£π β (((ββπ) + 1)...(ββπ₯))(absββ¦π / πβ¦π΄) β β) |
99 | 69, 70 | remulcld 11192 |
. . . . . . . . . 10
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β (π₯ Β· Ξ£π β (1...(ββπ))(absββ¦π / πβ¦π΄)) β β) |
100 | 69, 71 | remulcld 11192 |
. . . . . . . . . 10
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β (π₯ Β· π) β β) |
101 | 70 | recnd 11190 |
. . . . . . . . . . . 12
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β Ξ£π β (1...(ββπ))(absββ¦π / πβ¦π΄) β β) |
102 | 101 | mulid2d 11180 |
. . . . . . . . . . 11
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β (1 Β· Ξ£π β
(1...(ββπ))(absββ¦π / πβ¦π΄)) = Ξ£π β (1...(ββπ))(absββ¦π / πβ¦π΄)) |
103 | | 1red 11163 |
. . . . . . . . . . . 12
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β 1 β β) |
104 | 49 | absge0d 15336 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ π β (1...(ββπ))) β 0 β€
(absββ¦π
/ πβ¦π΄)) |
105 | 46, 50, 104 | fsumge0 15687 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β 0 β€ Ξ£π β (1...(ββπ))(absββ¦π / πβ¦π΄)) |
106 | 51, 105 | jca 513 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β (Ξ£π β (1...(ββπ))(absββ¦π / πβ¦π΄) β β β§ 0 β€ Ξ£π β
(1...(ββπ))(absββ¦π / πβ¦π΄))) |
107 | 106 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β (Ξ£π β (1...(ββπ))(absββ¦π / πβ¦π΄) β β β§ 0 β€ Ξ£π β
(1...(ββπ))(absββ¦π / πβ¦π΄))) |
108 | 44 | simprd 497 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β 1 β€ π) |
109 | 108 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β 1 β€ π) |
110 | 103, 83, 69, 109, 86 | letrd 11319 |
. . . . . . . . . . . 12
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β 1 β€ π₯) |
111 | | lemul1a 12016 |
. . . . . . . . . . . 12
β’ (((1
β β β§ π₯
β β β§ (Ξ£π β (1...(ββπ))(absββ¦π / πβ¦π΄) β β β§ 0 β€ Ξ£π β
(1...(ββπ))(absββ¦π / πβ¦π΄))) β§ 1 β€ π₯) β (1 Β· Ξ£π β
(1...(ββπ))(absββ¦π / πβ¦π΄)) β€ (π₯ Β· Ξ£π β (1...(ββπ))(absββ¦π / πβ¦π΄))) |
112 | 103, 69, 107, 110, 111 | syl31anc 1374 |
. . . . . . . . . . 11
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β (1 Β· Ξ£π β
(1...(ββπ))(absββ¦π / πβ¦π΄)) β€ (π₯ Β· Ξ£π β (1...(ββπ))(absββ¦π / πβ¦π΄))) |
113 | 102, 112 | eqbrtrrd 5134 |
. . . . . . . . . 10
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β Ξ£π β (1...(ββπ))(absββ¦π / πβ¦π΄) β€ (π₯ Β· Ξ£π β (1...(ββπ))(absββ¦π / πβ¦π΄))) |
114 | | hashcl 14263 |
. . . . . . . . . . . . 13
β’
((((ββπ)
+ 1)...(ββπ₯))
β Fin β (β―β(((ββπ) + 1)...(ββπ₯))) β
β0) |
115 | | nn0re 12429 |
. . . . . . . . . . . . 13
β’
((β―β(((ββπ) + 1)...(ββπ₯))) β β0 β
(β―β(((ββπ) + 1)...(ββπ₯))) β β) |
116 | 77, 114, 115 | 3syl 18 |
. . . . . . . . . . . 12
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β
(β―β(((ββπ) + 1)...(ββπ₯))) β β) |
117 | 116, 71 | remulcld 11192 |
. . . . . . . . . . 11
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β
((β―β(((ββπ) + 1)...(ββπ₯))) Β· π) β β) |
118 | 71 | adantr 482 |
. . . . . . . . . . . . 13
β’
(((((π β§ (π β (1[,)+β) β§
π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β§ π β (((ββπ) + 1)...(ββπ₯))) β π β β) |
119 | | elfzuz 13444 |
. . . . . . . . . . . . . 14
β’ (π β (((ββπ) + 1)...(ββπ₯)) β π β
(β€β₯β((ββπ) + 1))) |
120 | 81 | peano2nnd 12177 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β ((ββπ) + 1) β β) |
121 | | eluznn 12850 |
. . . . . . . . . . . . . . . 16
β’
((((ββπ)
+ 1) β β β§ π
β (β€β₯β((ββπ) + 1))) β π β β) |
122 | 120, 121 | sylan 581 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ (π β (1[,)+β) β§
π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β§ π β
(β€β₯β((ββπ) + 1))) β π β β) |
123 | | simpllr 775 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ (π β (1[,)+β) β§
π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β§ π β
(β€β₯β((ββπ) + 1))) β βπ β β (π β€ π β (absβπ΄) β€ π)) |
124 | 83 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ (π β (1[,)+β) β§
π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β§ π β
(β€β₯β((ββπ) + 1))) β π β β) |
125 | | reflcl 13708 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β
(ββπ) β
β) |
126 | | peano2re 11335 |
. . . . . . . . . . . . . . . . 17
β’
((ββπ)
β β β ((ββπ) + 1) β β) |
127 | 124, 125,
126 | 3syl 18 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ (π β (1[,)+β) β§
π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β§ π β
(β€β₯β((ββπ) + 1))) β ((ββπ) + 1) β
β) |
128 | 122 | nnred 12175 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ (π β (1[,)+β) β§
π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β§ π β
(β€β₯β((ββπ) + 1))) β π β β) |
129 | | fllep1 13713 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β π β€ ((ββπ) + 1)) |
130 | 124, 129 | syl 17 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ (π β (1[,)+β) β§
π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β§ π β
(β€β₯β((ββπ) + 1))) β π β€ ((ββπ) + 1)) |
131 | | eluzle 12783 |
. . . . . . . . . . . . . . . . 17
β’ (π β
(β€β₯β((ββπ) + 1)) β ((ββπ) + 1) β€ π) |
132 | 131 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ (π β (1[,)+β) β§
π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β§ π β
(β€β₯β((ββπ) + 1))) β ((ββπ) + 1) β€ π) |
133 | 124, 127,
128, 130, 132 | letrd 11319 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ (π β (1[,)+β) β§
π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β§ π β
(β€β₯β((ββπ) + 1))) β π β€ π) |
134 | | nfv 1918 |
. . . . . . . . . . . . . . . . 17
β’
β²π π β€ π |
135 | | nfcv 2908 |
. . . . . . . . . . . . . . . . . . 19
β’
β²πabs |
136 | 135, 12 | nffv 6857 |
. . . . . . . . . . . . . . . . . 18
β’
β²π(absββ¦π / πβ¦π΄) |
137 | | nfcv 2908 |
. . . . . . . . . . . . . . . . . 18
β’
β²π
β€ |
138 | | nfcv 2908 |
. . . . . . . . . . . . . . . . . 18
β’
β²ππ |
139 | 136, 137,
138 | nfbr 5157 |
. . . . . . . . . . . . . . . . 17
β’
β²π(absββ¦π / πβ¦π΄) β€ π |
140 | 134, 139 | nfim 1900 |
. . . . . . . . . . . . . . . 16
β’
β²π(π β€ π β (absββ¦π / πβ¦π΄) β€ π) |
141 | | breq2 5114 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (π β€ π β π β€ π)) |
142 | 13 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (absβπ΄) = (absββ¦π / πβ¦π΄)) |
143 | 142 | breq1d 5120 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β ((absβπ΄) β€ π β (absββ¦π / πβ¦π΄) β€ π)) |
144 | 141, 143 | imbi12d 345 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ((π β€ π β (absβπ΄) β€ π) β (π β€ π β (absββ¦π / πβ¦π΄) β€ π))) |
145 | 140, 144 | rspc 3572 |
. . . . . . . . . . . . . . 15
β’ (π β β β
(βπ β β
(π β€ π β (absβπ΄) β€ π) β (π β€ π β (absββ¦π / πβ¦π΄) β€ π))) |
146 | 122, 123,
133, 145 | syl3c 66 |
. . . . . . . . . . . . . 14
β’
(((((π β§ (π β (1[,)+β) β§
π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β§ π β
(β€β₯β((ββπ) + 1))) β
(absββ¦π
/ πβ¦π΄) β€ π) |
147 | 119, 146 | sylan2 594 |
. . . . . . . . . . . . 13
β’
(((((π β§ (π β (1[,)+β) β§
π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β§ π β (((ββπ) + 1)...(ββπ₯))) β (absββ¦π / πβ¦π΄) β€ π) |
148 | 77, 97, 118, 147 | fsumle 15691 |
. . . . . . . . . . . 12
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β Ξ£π β (((ββπ) + 1)...(ββπ₯))(absββ¦π / πβ¦π΄) β€ Ξ£π β (((ββπ) + 1)...(ββπ₯))π) |
149 | 71 | recnd 11190 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β π β β) |
150 | | fsumconst 15682 |
. . . . . . . . . . . . 13
β’
(((((ββπ) + 1)...(ββπ₯)) β Fin β§ π β β) β Ξ£π β (((ββπ) + 1)...(ββπ₯))π = ((β―β(((ββπ) + 1)...(ββπ₯))) Β· π)) |
151 | 77, 149, 150 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β Ξ£π β (((ββπ) + 1)...(ββπ₯))π = ((β―β(((ββπ) + 1)...(ββπ₯))) Β· π)) |
152 | 148, 151 | breqtrd 5136 |
. . . . . . . . . . 11
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β Ξ£π β (((ββπ) + 1)...(ββπ₯))(absββ¦π / πβ¦π΄) β€
((β―β(((ββπ) + 1)...(ββπ₯))) Β· π)) |
153 | | biidd 262 |
. . . . . . . . . . . . 13
β’ (π = ((ββπ) + 1) β (0 β€ π β 0 β€ π)) |
154 | | 0red 11165 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ (π β (1[,)+β) β§
π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β§ π β
(β€β₯β((ββπ) + 1))) β 0 β
β) |
155 | 47, 30 | mpan9 508 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ π β β) β β¦π / πβ¦π΄ β β) |
156 | 155 | adantlr 714 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ (π β (1[,)+β) β§
π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β§ π β β) β β¦π / πβ¦π΄ β β) |
157 | 122, 156 | syldan 592 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ (π β (1[,)+β) β§
π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β§ π β
(β€β₯β((ββπ) + 1))) β β¦π / πβ¦π΄ β β) |
158 | 157 | abscld 15328 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ (π β (1[,)+β) β§
π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β§ π β
(β€β₯β((ββπ) + 1))) β
(absββ¦π
/ πβ¦π΄) β
β) |
159 | 71 | adantr 482 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ (π β (1[,)+β) β§
π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β§ π β
(β€β₯β((ββπ) + 1))) β π β β) |
160 | 157 | absge0d 15336 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ (π β (1[,)+β) β§
π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β§ π β
(β€β₯β((ββπ) + 1))) β 0 β€
(absββ¦π
/ πβ¦π΄)) |
161 | 154, 158,
159, 160, 146 | letrd 11319 |
. . . . . . . . . . . . . 14
β’
(((((π β§ (π β (1[,)+β) β§
π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β§ π β
(β€β₯β((ββπ) + 1))) β 0 β€ π) |
162 | 161 | ralrimiva 3144 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β βπ β
(β€β₯β((ββπ) + 1))0 β€ π) |
163 | 120 | nnzd 12533 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β ((ββπ) + 1) β β€) |
164 | | uzid 12785 |
. . . . . . . . . . . . . 14
β’
(((ββπ)
+ 1) β β€ β ((ββπ) + 1) β
(β€β₯β((ββπ) + 1))) |
165 | 163, 164 | syl 17 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β ((ββπ) + 1) β
(β€β₯β((ββπ) + 1))) |
166 | 153, 162,
165 | rspcdva 3585 |
. . . . . . . . . . . 12
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β 0 β€ π) |
167 | | reflcl 13708 |
. . . . . . . . . . . . . 14
β’ (π₯ β β β
(ββπ₯) β
β) |
168 | 69, 167 | syl 17 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β (ββπ₯) β β) |
169 | | ssdomg 8947 |
. . . . . . . . . . . . . . . 16
β’
((1...(ββπ₯)) β Fin β ((((ββπ) + 1)...(ββπ₯)) β
(1...(ββπ₯))
β (((ββπ)
+ 1)...(ββπ₯))
βΌ (1...(ββπ₯)))) |
170 | 64, 93, 169 | sylc 65 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β (((ββπ) + 1)...(ββπ₯)) βΌ (1...(ββπ₯))) |
171 | | hashdomi 14287 |
. . . . . . . . . . . . . . 15
β’
((((ββπ)
+ 1)...(ββπ₯))
βΌ (1...(ββπ₯)) β
(β―β(((ββπ) + 1)...(ββπ₯))) β€
(β―β(1...(ββπ₯)))) |
172 | 170, 171 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β
(β―β(((ββπ) + 1)...(ββπ₯))) β€
(β―β(1...(ββπ₯)))) |
173 | | flge0nn0 13732 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β β§ 0 β€
π₯) β
(ββπ₯) β
β0) |
174 | | hashfz1 14253 |
. . . . . . . . . . . . . . 15
β’
((ββπ₯)
β β0 β (β―β(1...(ββπ₯))) = (ββπ₯)) |
175 | 57, 173, 174 | 3syl 18 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β
(β―β(1...(ββπ₯))) = (ββπ₯)) |
176 | 172, 175 | breqtrd 5136 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β
(β―β(((ββπ) + 1)...(ββπ₯))) β€ (ββπ₯)) |
177 | | flle 13711 |
. . . . . . . . . . . . . 14
β’ (π₯ β β β
(ββπ₯) β€
π₯) |
178 | 69, 177 | syl 17 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β (ββπ₯) β€ π₯) |
179 | 116, 168,
69, 176, 178 | letrd 11319 |
. . . . . . . . . . . 12
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β
(β―β(((ββπ) + 1)...(ββπ₯))) β€ π₯) |
180 | 116, 69, 71, 166, 179 | lemul1ad 12101 |
. . . . . . . . . . 11
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β
((β―β(((ββπ) + 1)...(ββπ₯))) Β· π) β€ (π₯ Β· π)) |
181 | 98, 117, 100, 152, 180 | letrd 11319 |
. . . . . . . . . 10
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β Ξ£π β (((ββπ) + 1)...(ββπ₯))(absββ¦π / πβ¦π΄) β€ (π₯ Β· π)) |
182 | 70, 98, 99, 100, 113, 181 | le2addd 11781 |
. . . . . . . . 9
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β (Ξ£π β (1...(ββπ))(absββ¦π / πβ¦π΄) + Ξ£π β (((ββπ) + 1)...(ββπ₯))(absββ¦π / πβ¦π΄)) β€ ((π₯ Β· Ξ£π β (1...(ββπ))(absββ¦π / πβ¦π΄)) + (π₯ Β· π))) |
183 | | ltp1 12002 |
. . . . . . . . . . 11
β’
((ββπ)
β β β (ββπ) < ((ββπ) + 1)) |
184 | | fzdisj 13475 |
. . . . . . . . . . 11
β’
((ββπ)
< ((ββπ) +
1) β ((1...(ββπ)) β© (((ββπ) + 1)...(ββπ₯))) = β
) |
185 | 82, 183, 184 | 3syl 18 |
. . . . . . . . . 10
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β ((1...(ββπ)) β© (((ββπ) + 1)...(ββπ₯))) = β
) |
186 | 96 | recnd 11190 |
. . . . . . . . . 10
β’
(((((π β§ (π β (1[,)+β) β§
π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β§ π β (1...(ββπ₯))) β
(absββ¦π
/ πβ¦π΄) β
β) |
187 | 185, 92, 64, 186 | fsumsplit 15633 |
. . . . . . . . 9
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β Ξ£π β (1...(ββπ₯))(absββ¦π / πβ¦π΄) = (Ξ£π β (1...(ββπ))(absββ¦π / πβ¦π΄) + Ξ£π β (((ββπ) + 1)...(ββπ₯))(absββ¦π / πβ¦π΄))) |
188 | 36 | adantrr 716 |
. . . . . . . . . 10
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β π₯ β β) |
189 | 188, 101,
149 | adddid 11186 |
. . . . . . . . 9
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β (π₯ Β· (Ξ£π β (1...(ββπ))(absββ¦π / πβ¦π΄) + π)) = ((π₯ Β· Ξ£π β (1...(ββπ))(absββ¦π / πβ¦π΄)) + (π₯ Β· π))) |
190 | 182, 187,
189 | 3brtr4d 5142 |
. . . . . . . 8
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β Ξ£π β (1...(ββπ₯))(absββ¦π / πβ¦π΄) β€ (π₯ Β· (Ξ£π β (1...(ββπ))(absββ¦π / πβ¦π΄) + π))) |
191 | 63, 68, 73, 76, 190 | letrd 11319 |
. . . . . . 7
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β (absβΞ£π β
(1...(ββπ₯))π΄) β€ (π₯ Β· (Ξ£π β (1...(ββπ))(absββ¦π / πβ¦π΄) + π))) |
192 | | rpregt0 12936 |
. . . . . . . . 9
β’ (π₯ β β+
β (π₯ β β
β§ 0 < π₯)) |
193 | 192 | ad2antrl 727 |
. . . . . . . 8
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β (π₯ β β β§ 0 < π₯)) |
194 | | ledivmul 12038 |
. . . . . . . 8
β’
(((absβΞ£π β (1...(ββπ₯))π΄) β β β§ (Ξ£π β
(1...(ββπ))(absββ¦π / πβ¦π΄) + π) β β β§ (π₯ β β β§ 0 < π₯)) β
(((absβΞ£π
β (1...(ββπ₯))π΄) / π₯) β€ (Ξ£π β (1...(ββπ))(absββ¦π / πβ¦π΄) + π) β (absβΞ£π β (1...(ββπ₯))π΄) β€ (π₯ Β· (Ξ£π β (1...(ββπ))(absββ¦π / πβ¦π΄) + π)))) |
195 | 63, 72, 193, 194 | syl3anc 1372 |
. . . . . . 7
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β (((absβΞ£π β
(1...(ββπ₯))π΄) / π₯) β€ (Ξ£π β (1...(ββπ))(absββ¦π / πβ¦π΄) + π) β (absβΞ£π β (1...(ββπ₯))π΄) β€ (π₯ Β· (Ξ£π β (1...(ββπ))(absββ¦π / πβ¦π΄) + π)))) |
196 | 191, 195 | mpbird 257 |
. . . . . 6
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β ((absβΞ£π β
(1...(ββπ₯))π΄) / π₯) β€ (Ξ£π β (1...(ββπ))(absββ¦π / πβ¦π΄) + π)) |
197 | 61, 196 | eqbrtrd 5132 |
. . . . 5
β’ ((((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β§ (π₯ β β+ β§ π β€ π₯)) β (absβ(Ξ£π β
(1...(ββπ₯))π΄ / π₯)) β€ (Ξ£π β (1...(ββπ))(absββ¦π / πβ¦π΄) + π)) |
198 | 10, 39, 45, 53, 197 | elo1d 15425 |
. . . 4
β’ (((π β§ (π β (1[,)+β) β§ π β β)) β§
βπ β β
(π β€ π β (absβπ΄) β€ π)) β (π₯ β β+ β¦
(Ξ£π β
(1...(ββπ₯))π΄ / π₯)) β π(1)) |
199 | 198 | ex 414 |
. . 3
β’ ((π β§ (π β (1[,)+β) β§ π β β)) β
(βπ β β
(π β€ π β (absβπ΄) β€ π) β (π₯ β β+ β¦
(Ξ£π β
(1...(ββπ₯))π΄ / π₯)) β π(1))) |
200 | 199 | rexlimdvva 3206 |
. 2
β’ (π β (βπ β (1[,)+β)βπ β β βπ β β (π β€ π β (absβπ΄) β€ π) β (π₯ β β+ β¦
(Ξ£π β
(1...(ββπ₯))π΄ / π₯)) β π(1))) |
201 | 8, 200 | mpd 15 |
1
β’ (π β (π₯ β β+ β¦
(Ξ£π β
(1...(ββπ₯))π΄ / π₯)) β π(1)) |