Step | Hyp | Ref
| Expression |
1 | | dvfsum.s |
. . . 4
β’ π = (π(,)+β) |
2 | | ioossre 13387 |
. . . 4
β’ (π(,)+β) β
β |
3 | 1, 2 | eqsstri 4016 |
. . 3
β’ π β
β |
4 | 3 | a1i 11 |
. 2
β’ (π β π β β) |
5 | | dvfsum.z |
. . . 4
β’ π =
(β€β₯βπ) |
6 | | dvfsum.m |
. . . 4
β’ (π β π β β€) |
7 | | dvfsum.d |
. . . 4
β’ (π β π· β β) |
8 | | dvfsum.md |
. . . 4
β’ (π β π β€ (π· + 1)) |
9 | | dvfsum.t |
. . . 4
β’ (π β π β β) |
10 | | dvfsum.a |
. . . 4
β’ ((π β§ π₯ β π) β π΄ β β) |
11 | | dvfsum.b1 |
. . . 4
β’ ((π β§ π₯ β π) β π΅ β π) |
12 | | dvfsum.b2 |
. . . 4
β’ ((π β§ π₯ β π) β π΅ β β) |
13 | | dvfsum.b3 |
. . . 4
β’ (π β (β D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) |
14 | | dvfsum.c |
. . . 4
β’ (π₯ = π β π΅ = πΆ) |
15 | | dvfsumrlim.g |
. . . 4
β’ πΊ = (π₯ β π β¦ (Ξ£π β (π...(ββπ₯))πΆ β π΄)) |
16 | 1, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15 | dvfsumrlimf 25549 |
. . 3
β’ (π β πΊ:πβΆβ) |
17 | | ax-resscn 11169 |
. . 3
β’ β
β β |
18 | | fss 6734 |
. . 3
β’ ((πΊ:πβΆβ β§ β β
β) β πΊ:πβΆβ) |
19 | 16, 17, 18 | sylancl 586 |
. 2
β’ (π β πΊ:πβΆβ) |
20 | 1 | supeq1i 9444 |
. . 3
β’ sup(π, β*, < ) =
sup((π(,)+β),
β*, < ) |
21 | | ressxr 11260 |
. . . . 5
β’ β
β β* |
22 | 21, 9 | sselid 3980 |
. . . 4
β’ (π β π β
β*) |
23 | 9 | renepnfd 11267 |
. . . 4
β’ (π β π β +β) |
24 | | ioopnfsup 13831 |
. . . 4
β’ ((π β β*
β§ π β +β)
β sup((π(,)+β),
β*, < ) = +β) |
25 | 22, 23, 24 | syl2anc 584 |
. . 3
β’ (π β sup((π(,)+β), β*, < ) =
+β) |
26 | 20, 25 | eqtrid 2784 |
. 2
β’ (π β sup(π, β*, < ) =
+β) |
27 | | dvfsumrlim.k |
. . . 4
β’ (π β (π₯ β π β¦ π΅) βπ
0) |
28 | 11, 27 | rlimmptrcl 15554 |
. . . . . 6
β’ ((π β§ π₯ β π) β π΅ β β) |
29 | 28 | ralrimiva 3146 |
. . . . 5
β’ (π β βπ₯ β π π΅ β β) |
30 | 29, 4 | rlim0 15454 |
. . . 4
β’ (π β ((π₯ β π β¦ π΅) βπ 0 β
βπ β
β+ βπ β β βπ₯ β π (π β€ π₯ β (absβπ΅) < π))) |
31 | 27, 30 | mpbid 231 |
. . 3
β’ (π β βπ β β+ βπ β β βπ₯ β π (π β€ π₯ β (absβπ΅) < π)) |
32 | 3 | a1i 11 |
. . . . . 6
β’ ((π β§ π β β+) β π β
β) |
33 | | peano2re 11389 |
. . . . . . . . 9
β’ (π β β β (π + 1) β
β) |
34 | 9, 33 | syl 17 |
. . . . . . . 8
β’ (π β (π + 1) β β) |
35 | 34, 7 | ifcld 4574 |
. . . . . . 7
β’ (π β if(π· β€ (π + 1), (π + 1), π·) β β) |
36 | 35 | adantr 481 |
. . . . . 6
β’ ((π β§ π β β+) β if(π· β€ (π + 1), (π + 1), π·) β β) |
37 | | rexico 15302 |
. . . . . 6
β’ ((π β β β§ if(π· β€ (π + 1), (π + 1), π·) β β) β (βπ β (if(π· β€ (π + 1), (π + 1), π·)[,)+β)βπ₯ β π (π β€ π₯ β (absβπ΅) < π) β βπ β β βπ₯ β π (π β€ π₯ β (absβπ΅) < π))) |
38 | 32, 36, 37 | syl2anc 584 |
. . . . 5
β’ ((π β§ π β β+) β
(βπ β (if(π· β€ (π + 1), (π + 1), π·)[,)+β)βπ₯ β π (π β€ π₯ β (absβπ΅) < π) β βπ β β βπ₯ β π (π β€ π₯ β (absβπ΅) < π))) |
39 | | elicopnf 13424 |
. . . . . . . . . . . . . 14
β’ (if(π· β€ (π + 1), (π + 1), π·) β β β (π β (if(π· β€ (π + 1), (π + 1), π·)[,)+β) β (π β β β§ if(π· β€ (π + 1), (π + 1), π·) β€ π))) |
40 | 35, 39 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β (π β (if(π· β€ (π + 1), (π + 1), π·)[,)+β) β (π β β β§ if(π· β€ (π + 1), (π + 1), π·) β€ π))) |
41 | 40 | simprbda 499 |
. . . . . . . . . . . 12
β’ ((π β§ π β (if(π· β€ (π + 1), (π + 1), π·)[,)+β)) β π β β) |
42 | 9 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (if(π· β€ (π + 1), (π + 1), π·)[,)+β)) β π β β) |
43 | 42, 33 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (if(π· β€ (π + 1), (π + 1), π·)[,)+β)) β (π + 1) β β) |
44 | 42 | ltp1d 12146 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (if(π· β€ (π + 1), (π + 1), π·)[,)+β)) β π < (π + 1)) |
45 | 40 | simplbda 500 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (if(π· β€ (π + 1), (π + 1), π·)[,)+β)) β if(π· β€ (π + 1), (π + 1), π·) β€ π) |
46 | 7 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (if(π· β€ (π + 1), (π + 1), π·)[,)+β)) β π· β β) |
47 | | maxle 13172 |
. . . . . . . . . . . . . . . 16
β’ ((π· β β β§ (π + 1) β β β§ π β β) β
(if(π· β€ (π + 1), (π + 1), π·) β€ π β (π· β€ π β§ (π + 1) β€ π))) |
48 | 46, 43, 41, 47 | syl3anc 1371 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (if(π· β€ (π + 1), (π + 1), π·)[,)+β)) β (if(π· β€ (π + 1), (π + 1), π·) β€ π β (π· β€ π β§ (π + 1) β€ π))) |
49 | 45, 48 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (if(π· β€ (π + 1), (π + 1), π·)[,)+β)) β (π· β€ π β§ (π + 1) β€ π)) |
50 | 49 | simprd 496 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (if(π· β€ (π + 1), (π + 1), π·)[,)+β)) β (π + 1) β€ π) |
51 | 42, 43, 41, 44, 50 | ltletrd 11376 |
. . . . . . . . . . . 12
β’ ((π β§ π β (if(π· β€ (π + 1), (π + 1), π·)[,)+β)) β π < π) |
52 | 22 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (if(π· β€ (π + 1), (π + 1), π·)[,)+β)) β π β
β*) |
53 | | elioopnf 13422 |
. . . . . . . . . . . . 13
β’ (π β β*
β (π β (π(,)+β) β (π β β β§ π < π))) |
54 | 52, 53 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π β (if(π· β€ (π + 1), (π + 1), π·)[,)+β)) β (π β (π(,)+β) β (π β β β§ π < π))) |
55 | 41, 51, 54 | mpbir2and 711 |
. . . . . . . . . . 11
β’ ((π β§ π β (if(π· β€ (π + 1), (π + 1), π·)[,)+β)) β π β (π(,)+β)) |
56 | 55, 1 | eleqtrrdi 2844 |
. . . . . . . . . 10
β’ ((π β§ π β (if(π· β€ (π + 1), (π + 1), π·)[,)+β)) β π β π) |
57 | 49 | simpld 495 |
. . . . . . . . . 10
β’ ((π β§ π β (if(π· β€ (π + 1), (π + 1), π·)[,)+β)) β π· β€ π) |
58 | 56, 57 | jca 512 |
. . . . . . . . 9
β’ ((π β§ π β (if(π· β€ (π + 1), (π + 1), π·)[,)+β)) β (π β π β§ π· β€ π)) |
59 | 58 | adantlr 713 |
. . . . . . . 8
β’ (((π β§ π β β+) β§ π β (if(π· β€ (π + 1), (π + 1), π·)[,)+β)) β (π β π β§ π· β€ π)) |
60 | | simprrl 779 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π β β+ β§ (π β π β§ π· β€ π))) β π β π) |
61 | 60 | adantrr 715 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ ((π β β+ β§ (π β π β§ π· β€ π)) β§ (π¦ β π β§ π β€ π¦))) β π β π) |
62 | 3, 61 | sselid 3980 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ ((π β β+ β§ (π β π β§ π· β€ π)) β§ (π¦ β π β§ π β€ π¦))) β π β β) |
63 | 62 | leidd 11782 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ ((π β β+ β§ (π β π β§ π· β€ π)) β§ (π¦ β π β§ π β€ π¦))) β π β€ π) |
64 | | nfv 1917 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π₯ π β€ π |
65 | | nfcv 2903 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²π₯abs |
66 | | nfcsb1v 3918 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²π₯β¦π / π₯β¦π΅ |
67 | 65, 66 | nffv 6901 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π₯(absββ¦π / π₯β¦π΅) |
68 | | nfcv 2903 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π₯
< |
69 | | nfcv 2903 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π₯π |
70 | 67, 68, 69 | nfbr 5195 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π₯(absββ¦π / π₯β¦π΅) < π |
71 | 64, 70 | nfim 1899 |
. . . . . . . . . . . . . . . . . 18
β’
β²π₯(π β€ π β (absββ¦π / π₯β¦π΅) < π) |
72 | | breq2 5152 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ = π β (π β€ π₯ β π β€ π)) |
73 | | csbeq1a 3907 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ = π β π΅ = β¦π / π₯β¦π΅) |
74 | 73 | fveq2d 6895 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ = π β (absβπ΅) = (absββ¦π / π₯β¦π΅)) |
75 | 74 | breq1d 5158 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ = π β ((absβπ΅) < π β (absββ¦π / π₯β¦π΅) < π)) |
76 | 72, 75 | imbi12d 344 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π β ((π β€ π₯ β (absβπ΅) < π) β (π β€ π β (absββ¦π / π₯β¦π΅) < π))) |
77 | 71, 76 | rspc 3600 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β (βπ₯ β π (π β€ π₯ β (absβπ΅) < π) β (π β€ π β (absββ¦π / π₯β¦π΅) < π))) |
78 | 61, 77 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ ((π β β+ β§ (π β π β§ π· β€ π)) β§ (π¦ β π β§ π β€ π¦))) β (βπ₯ β π (π β€ π₯ β (absβπ΅) < π) β (π β€ π β (absββ¦π / π₯β¦π΅) < π))) |
79 | 63, 78 | mpid 44 |
. . . . . . . . . . . . . . 15
β’ ((π β§ ((π β β+ β§ (π β π β§ π· β€ π)) β§ (π¦ β π β§ π β€ π¦))) β (βπ₯ β π (π β€ π₯ β (absβπ΅) < π) β (absββ¦π / π₯β¦π΅) < π)) |
80 | 4, 10, 11, 13 | dvmptrecl 25548 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π₯ β π) β π΅ β β) |
81 | 80 | adantrr 715 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ (π₯ β π β§ π· β€ π₯)) β π΅ β β) |
82 | | dvfsumrlim.l |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ (π₯ β π β§ π β π) β§ (π· β€ π₯ β§ π₯ β€ π)) β πΆ β€ π΅) |
83 | 1, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 82, 15, 27 | dvfsumrlimge0 25554 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ (π₯ β π β§ π· β€ π₯)) β 0 β€ π΅) |
84 | | elrege0 13433 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π΅ β (0[,)+β) β
(π΅ β β β§ 0
β€ π΅)) |
85 | 81, 83, 84 | sylanbrc 583 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ (π₯ β π β§ π· β€ π₯)) β π΅ β (0[,)+β)) |
86 | 85 | expr 457 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π₯ β π) β (π· β€ π₯ β π΅ β (0[,)+β))) |
87 | 86 | ralrimiva 3146 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β βπ₯ β π (π· β€ π₯ β π΅ β (0[,)+β))) |
88 | 87 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ ((π β β+ β§ (π β π β§ π· β€ π)) β§ (π¦ β π β§ π β€ π¦))) β βπ₯ β π (π· β€ π₯ β π΅ β (0[,)+β))) |
89 | | simprrr 780 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ (π β β+ β§ (π β π β§ π· β€ π))) β π· β€ π) |
90 | 89 | adantrr 715 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ ((π β β+ β§ (π β π β§ π· β€ π)) β§ (π¦ β π β§ π β€ π¦))) β π· β€ π) |
91 | | nfv 1917 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
β²π₯ π· β€ π |
92 | 66 | nfel1 2919 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
β²π₯β¦π / π₯β¦π΅ β (0[,)+β) |
93 | 91, 92 | nfim 1899 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²π₯(π· β€ π β β¦π / π₯β¦π΅ β (0[,)+β)) |
94 | | breq2 5152 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ = π β (π· β€ π₯ β π· β€ π)) |
95 | 73 | eleq1d 2818 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ = π β (π΅ β (0[,)+β) β
β¦π / π₯β¦π΅ β (0[,)+β))) |
96 | 94, 95 | imbi12d 344 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ = π β ((π· β€ π₯ β π΅ β (0[,)+β)) β (π· β€ π β β¦π / π₯β¦π΅ β (0[,)+β)))) |
97 | 93, 96 | rspc 3600 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π β (βπ₯ β π (π· β€ π₯ β π΅ β (0[,)+β)) β (π· β€ π β β¦π / π₯β¦π΅ β (0[,)+β)))) |
98 | 61, 88, 90, 97 | syl3c 66 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ ((π β β+ β§ (π β π β§ π· β€ π)) β§ (π¦ β π β§ π β€ π¦))) β β¦π / π₯β¦π΅ β (0[,)+β)) |
99 | | elrege0 13433 |
. . . . . . . . . . . . . . . . . . 19
β’
(β¦π /
π₯β¦π΅ β (0[,)+β) β
(β¦π / π₯β¦π΅ β β β§ 0 β€
β¦π / π₯β¦π΅)) |
100 | 98, 99 | sylib 217 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ ((π β β+ β§ (π β π β§ π· β€ π)) β§ (π¦ β π β§ π β€ π¦))) β (β¦π / π₯β¦π΅ β β β§ 0 β€
β¦π / π₯β¦π΅)) |
101 | | absid 15245 |
. . . . . . . . . . . . . . . . . 18
β’
((β¦π /
π₯β¦π΅ β β β§ 0 β€
β¦π / π₯β¦π΅) β (absββ¦π / π₯β¦π΅) = β¦π / π₯β¦π΅) |
102 | 100, 101 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ ((π β β+ β§ (π β π β§ π· β€ π)) β§ (π¦ β π β§ π β€ π¦))) β (absββ¦π / π₯β¦π΅) = β¦π / π₯β¦π΅) |
103 | 102 | breq1d 5158 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ ((π β β+ β§ (π β π β§ π· β€ π)) β§ (π¦ β π β§ π β€ π¦))) β ((absββ¦π / π₯β¦π΅) < π β β¦π / π₯β¦π΅ < π)) |
104 | 6 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ ((π β β+ β§ (π β π β§ π· β€ π)) β§ (π¦ β π β§ π β€ π¦))) β π β β€) |
105 | 7 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ ((π β β+ β§ (π β π β§ π· β€ π)) β§ (π¦ β π β§ π β€ π¦))) β π· β β) |
106 | 8 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ ((π β β+ β§ (π β π β§ π· β€ π)) β§ (π¦ β π β§ π β€ π¦))) β π β€ (π· + 1)) |
107 | 9 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ ((π β β+ β§ (π β π β§ π· β€ π)) β§ (π¦ β π β§ π β€ π¦))) β π β β) |
108 | 10 | adantlr 713 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ ((π β β+ β§ (π β π β§ π· β€ π)) β§ (π¦ β π β§ π β€ π¦))) β§ π₯ β π) β π΄ β β) |
109 | 11 | adantlr 713 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ ((π β β+ β§ (π β π β§ π· β€ π)) β§ (π¦ β π β§ π β€ π¦))) β§ π₯ β π) β π΅ β π) |
110 | 12 | adantlr 713 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ ((π β β+ β§ (π β π β§ π· β€ π)) β§ (π¦ β π β§ π β€ π¦))) β§ π₯ β π) β π΅ β β) |
111 | 13 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ ((π β β+ β§ (π β π β§ π· β€ π)) β§ (π¦ β π β§ π β€ π¦))) β (β D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) |
112 | | pnfxr 11270 |
. . . . . . . . . . . . . . . . . . 19
β’ +β
β β* |
113 | 112 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ ((π β β+ β§ (π β π β§ π· β€ π)) β§ (π¦ β π β§ π β€ π¦))) β +β β
β*) |
114 | | 3simpa 1148 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π· β€ π₯ β§ π₯ β€ π β§ π β€ +β) β (π· β€ π₯ β§ π₯ β€ π)) |
115 | 114, 82 | syl3an3 1165 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π₯ β π β§ π β π) β§ (π· β€ π₯ β§ π₯ β€ π β§ π β€ +β)) β πΆ β€ π΅) |
116 | 115 | 3adant1r 1177 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ ((π β β+ β§ (π β π β§ π· β€ π)) β§ (π¦ β π β§ π β€ π¦))) β§ (π₯ β π β§ π β π) β§ (π· β€ π₯ β§ π₯ β€ π β§ π β€ +β)) β πΆ β€ π΅) |
117 | 83 | 3adantr3 1171 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π₯ β π β§ π· β€ π₯ β§ π₯ β€ +β)) β 0 β€ π΅) |
118 | 117 | adantlr 713 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ ((π β β+ β§ (π β π β§ π· β€ π)) β§ (π¦ β π β§ π β€ π¦))) β§ (π₯ β π β§ π· β€ π₯ β§ π₯ β€ +β)) β 0 β€ π΅) |
119 | | simprrl 779 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ ((π β β+ β§ (π β π β§ π· β€ π)) β§ (π¦ β π β§ π β€ π¦))) β π¦ β π) |
120 | | simprrr 780 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ ((π β β+ β§ (π β π β§ π· β€ π)) β§ (π¦ β π β§ π β€ π¦))) β π β€ π¦) |
121 | 3, 21 | sstri 3991 |
. . . . . . . . . . . . . . . . . . . 20
β’ π β
β* |
122 | 121, 119 | sselid 3980 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ ((π β β+ β§ (π β π β§ π· β€ π)) β§ (π¦ β π β§ π β€ π¦))) β π¦ β β*) |
123 | | pnfge 13112 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ β β*
β π¦ β€
+β) |
124 | 122, 123 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ ((π β β+ β§ (π β π β§ π· β€ π)) β§ (π¦ β π β§ π β€ π¦))) β π¦ β€ +β) |
125 | 1, 5, 104, 105, 106, 107, 108, 109, 110, 111, 14, 113, 116, 15, 118, 61, 119, 90, 120, 124 | dvfsumlem4 25553 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ ((π β β+ β§ (π β π β§ π· β€ π)) β§ (π¦ β π β§ π β€ π¦))) β (absβ((πΊβπ¦) β (πΊβπ))) β€ β¦π / π₯β¦π΅) |
126 | 19 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ ((π β β+ β§ (π β π β§ π· β€ π)) β§ (π¦ β π β§ π β€ π¦))) β πΊ:πβΆβ) |
127 | 126, 119 | ffvelcdmd 7087 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ ((π β β+ β§ (π β π β§ π· β€ π)) β§ (π¦ β π β§ π β€ π¦))) β (πΊβπ¦) β β) |
128 | 126, 61 | ffvelcdmd 7087 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ ((π β β+ β§ (π β π β§ π· β€ π)) β§ (π¦ β π β§ π β€ π¦))) β (πΊβπ) β β) |
129 | 127, 128 | subcld 11573 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ ((π β β+ β§ (π β π β§ π· β€ π)) β§ (π¦ β π β§ π β€ π¦))) β ((πΊβπ¦) β (πΊβπ)) β β) |
130 | 129 | abscld 15385 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ ((π β β+ β§ (π β π β§ π· β€ π)) β§ (π¦ β π β§ π β€ π¦))) β (absβ((πΊβπ¦) β (πΊβπ))) β β) |
131 | 100 | simpld 495 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ ((π β β+ β§ (π β π β§ π· β€ π)) β§ (π¦ β π β§ π β€ π¦))) β β¦π / π₯β¦π΅ β β) |
132 | | simprll 777 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ ((π β β+ β§ (π β π β§ π· β€ π)) β§ (π¦ β π β§ π β€ π¦))) β π β β+) |
133 | 132 | rpred 13018 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ ((π β β+ β§ (π β π β§ π· β€ π)) β§ (π¦ β π β§ π β€ π¦))) β π β β) |
134 | | lelttr 11306 |
. . . . . . . . . . . . . . . . . 18
β’
(((absβ((πΊβπ¦) β (πΊβπ))) β β β§ β¦π / π₯β¦π΅ β β β§ π β β) β (((absβ((πΊβπ¦) β (πΊβπ))) β€ β¦π / π₯β¦π΅ β§ β¦π / π₯β¦π΅ < π) β (absβ((πΊβπ¦) β (πΊβπ))) < π)) |
135 | 130, 131,
133, 134 | syl3anc 1371 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ ((π β β+ β§ (π β π β§ π· β€ π)) β§ (π¦ β π β§ π β€ π¦))) β (((absβ((πΊβπ¦) β (πΊβπ))) β€ β¦π / π₯β¦π΅ β§ β¦π / π₯β¦π΅ < π) β (absβ((πΊβπ¦) β (πΊβπ))) < π)) |
136 | 125, 135 | mpand 693 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ ((π β β+ β§ (π β π β§ π· β€ π)) β§ (π¦ β π β§ π β€ π¦))) β (β¦π / π₯β¦π΅ < π β (absβ((πΊβπ¦) β (πΊβπ))) < π)) |
137 | 103, 136 | sylbid 239 |
. . . . . . . . . . . . . . 15
β’ ((π β§ ((π β β+ β§ (π β π β§ π· β€ π)) β§ (π¦ β π β§ π β€ π¦))) β ((absββ¦π / π₯β¦π΅) < π β (absβ((πΊβπ¦) β (πΊβπ))) < π)) |
138 | 79, 137 | syld 47 |
. . . . . . . . . . . . . 14
β’ ((π β§ ((π β β+ β§ (π β π β§ π· β€ π)) β§ (π¦ β π β§ π β€ π¦))) β (βπ₯ β π (π β€ π₯ β (absβπ΅) < π) β (absβ((πΊβπ¦) β (πΊβπ))) < π)) |
139 | 138 | anassrs 468 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β β+ β§ (π β π β§ π· β€ π))) β§ (π¦ β π β§ π β€ π¦)) β (βπ₯ β π (π β€ π₯ β (absβπ΅) < π) β (absβ((πΊβπ¦) β (πΊβπ))) < π)) |
140 | 139 | expr 457 |
. . . . . . . . . . . 12
β’ (((π β§ (π β β+ β§ (π β π β§ π· β€ π))) β§ π¦ β π) β (π β€ π¦ β (βπ₯ β π (π β€ π₯ β (absβπ΅) < π) β (absβ((πΊβπ¦) β (πΊβπ))) < π))) |
141 | 140 | com23 86 |
. . . . . . . . . . 11
β’ (((π β§ (π β β+ β§ (π β π β§ π· β€ π))) β§ π¦ β π) β (βπ₯ β π (π β€ π₯ β (absβπ΅) < π) β (π β€ π¦ β (absβ((πΊβπ¦) β (πΊβπ))) < π))) |
142 | 141 | ralrimdva 3154 |
. . . . . . . . . 10
β’ ((π β§ (π β β+ β§ (π β π β§ π· β€ π))) β (βπ₯ β π (π β€ π₯ β (absβπ΅) < π) β βπ¦ β π (π β€ π¦ β (absβ((πΊβπ¦) β (πΊβπ))) < π))) |
143 | 142, 60 | jctild 526 |
. . . . . . . . 9
β’ ((π β§ (π β β+ β§ (π β π β§ π· β€ π))) β (βπ₯ β π (π β€ π₯ β (absβπ΅) < π) β (π β π β§ βπ¦ β π (π β€ π¦ β (absβ((πΊβπ¦) β (πΊβπ))) < π)))) |
144 | 143 | anassrs 468 |
. . . . . . . 8
β’ (((π β§ π β β+) β§ (π β π β§ π· β€ π)) β (βπ₯ β π (π β€ π₯ β (absβπ΅) < π) β (π β π β§ βπ¦ β π (π β€ π¦ β (absβ((πΊβπ¦) β (πΊβπ))) < π)))) |
145 | 59, 144 | syldan 591 |
. . . . . . 7
β’ (((π β§ π β β+) β§ π β (if(π· β€ (π + 1), (π + 1), π·)[,)+β)) β (βπ₯ β π (π β€ π₯ β (absβπ΅) < π) β (π β π β§ βπ¦ β π (π β€ π¦ β (absβ((πΊβπ¦) β (πΊβπ))) < π)))) |
146 | 145 | expimpd 454 |
. . . . . 6
β’ ((π β§ π β β+) β ((π β (if(π· β€ (π + 1), (π + 1), π·)[,)+β) β§ βπ₯ β π (π β€ π₯ β (absβπ΅) < π)) β (π β π β§ βπ¦ β π (π β€ π¦ β (absβ((πΊβπ¦) β (πΊβπ))) < π)))) |
147 | 146 | reximdv2 3164 |
. . . . 5
β’ ((π β§ π β β+) β
(βπ β (if(π· β€ (π + 1), (π + 1), π·)[,)+β)βπ₯ β π (π β€ π₯ β (absβπ΅) < π) β βπ β π βπ¦ β π (π β€ π¦ β (absβ((πΊβπ¦) β (πΊβπ))) < π))) |
148 | 38, 147 | sylbird 259 |
. . . 4
β’ ((π β§ π β β+) β
(βπ β β
βπ₯ β π (π β€ π₯ β (absβπ΅) < π) β βπ β π βπ¦ β π (π β€ π¦ β (absβ((πΊβπ¦) β (πΊβπ))) < π))) |
149 | 148 | ralimdva 3167 |
. . 3
β’ (π β (βπ β β+
βπ β β
βπ₯ β π (π β€ π₯ β (absβπ΅) < π) β βπ β β+ βπ β π βπ¦ β π (π β€ π¦ β (absβ((πΊβπ¦) β (πΊβπ))) < π))) |
150 | 31, 149 | mpd 15 |
. 2
β’ (π β βπ β β+ βπ β π βπ¦ β π (π β€ π¦ β (absβ((πΊβπ¦) β (πΊβπ))) < π)) |
151 | 4, 19, 26, 150 | caucvgr 15624 |
1
β’ (π β πΊ β dom βπ
) |