Step | Hyp | Ref
| Expression |
1 | | dvbsss 25289 |
. . . . . . . 8
β’ dom
(β D πΉ) β
β |
2 | | id 22 |
. . . . . . . . 9
β’ (π₯ β dom πΊ β π₯ β dom πΊ) |
3 | | fperdvper.g |
. . . . . . . . . 10
β’ πΊ = (β D πΉ) |
4 | 3 | dmeqi 5864 |
. . . . . . . . 9
β’ dom πΊ = dom (β D πΉ) |
5 | 2, 4 | eleqtrdi 2844 |
. . . . . . . 8
β’ (π₯ β dom πΊ β π₯ β dom (β D πΉ)) |
6 | 1, 5 | sselid 3946 |
. . . . . . 7
β’ (π₯ β dom πΊ β π₯ β β) |
7 | 6 | adantl 483 |
. . . . . 6
β’ ((π β§ π₯ β dom πΊ) β π₯ β β) |
8 | | fperdvper.t |
. . . . . . 7
β’ (π β π β β) |
9 | 8 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β dom πΊ) β π β β) |
10 | 7, 9 | readdcld 11192 |
. . . . 5
β’ ((π β§ π₯ β dom πΊ) β (π₯ + π) β β) |
11 | | reopn 43614 |
. . . . . . 7
β’ β
β (topGenβran (,)) |
12 | | retop 24148 |
. . . . . . . 8
β’
(topGenβran (,)) β Top |
13 | | ssidd 3971 |
. . . . . . . 8
β’ ((π β§ π₯ β dom πΊ) β β β
β) |
14 | | uniretop 24149 |
. . . . . . . . 9
β’ β =
βͺ (topGenβran (,)) |
15 | 14 | isopn3 22440 |
. . . . . . . 8
β’
(((topGenβran (,)) β Top β§ β β β)
β (β β (topGenβran (,)) β
((intβ(topGenβran (,)))ββ) = β)) |
16 | 12, 13, 15 | sylancr 588 |
. . . . . . 7
β’ ((π β§ π₯ β dom πΊ) β (β β (topGenβran
(,)) β ((intβ(topGenβran (,)))ββ) =
β)) |
17 | 11, 16 | mpbii 232 |
. . . . . 6
β’ ((π β§ π₯ β dom πΊ) β ((intβ(topGenβran
(,)))ββ) = β) |
18 | 17 | eqcomd 2739 |
. . . . 5
β’ ((π β§ π₯ β dom πΊ) β β =
((intβ(topGenβran (,)))ββ)) |
19 | 10, 18 | eleqtrd 2836 |
. . . 4
β’ ((π β§ π₯ β dom πΊ) β (π₯ + π) β ((intβ(topGenβran
(,)))ββ)) |
20 | 5 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π₯ β dom πΊ) β π₯ β dom (β D πΉ)) |
21 | 3 | fveq1i 6847 |
. . . . . . . . . 10
β’ (πΊβπ₯) = ((β D πΉ)βπ₯) |
22 | 21 | eqcomi 2742 |
. . . . . . . . 9
β’ ((β
D πΉ)βπ₯) = (πΊβπ₯) |
23 | 22 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π₯ β dom πΊ) β ((β D πΉ)βπ₯) = (πΊβπ₯)) |
24 | | dvf 25294 |
. . . . . . . . . . . 12
β’ (β
D πΉ):dom (β D πΉ)βΆβ |
25 | | ffun 6675 |
. . . . . . . . . . . 12
β’ ((β
D πΉ):dom (β D πΉ)βΆβ β Fun
(β D πΉ)) |
26 | 24, 25 | ax-mp 5 |
. . . . . . . . . . 11
β’ Fun
(β D πΉ) |
27 | 26 | a1i 11 |
. . . . . . . . . 10
β’ (π β Fun (β D πΉ)) |
28 | | funbrfv2b 6904 |
. . . . . . . . . 10
β’ (Fun
(β D πΉ) β (π₯(β D πΉ)(πΊβπ₯) β (π₯ β dom (β D πΉ) β§ ((β D πΉ)βπ₯) = (πΊβπ₯)))) |
29 | 27, 28 | syl 17 |
. . . . . . . . 9
β’ (π β (π₯(β D πΉ)(πΊβπ₯) β (π₯ β dom (β D πΉ) β§ ((β D πΉ)βπ₯) = (πΊβπ₯)))) |
30 | 29 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β dom πΊ) β (π₯(β D πΉ)(πΊβπ₯) β (π₯ β dom (β D πΉ) β§ ((β D πΉ)βπ₯) = (πΊβπ₯)))) |
31 | 20, 23, 30 | mpbir2and 712 |
. . . . . . 7
β’ ((π β§ π₯ β dom πΊ) β π₯(β D πΉ)(πΊβπ₯)) |
32 | | tgioo4 43901 |
. . . . . . . 8
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
33 | | eqid 2733 |
. . . . . . . 8
β’
(TopOpenββfld) =
(TopOpenββfld) |
34 | | eqid 2733 |
. . . . . . . 8
β’ (π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯))) = (π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯))) |
35 | | ax-resscn 11116 |
. . . . . . . . 9
β’ β
β β |
36 | 35 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π₯ β dom πΊ) β β β
β) |
37 | | fperdvper.f |
. . . . . . . . 9
β’ (π β πΉ:ββΆβ) |
38 | 37 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β dom πΊ) β πΉ:ββΆβ) |
39 | 32, 33, 34, 36, 38, 13 | eldv 25285 |
. . . . . . 7
β’ ((π β§ π₯ β dom πΊ) β (π₯(β D πΉ)(πΊβπ₯) β (π₯ β ((intβ(topGenβran
(,)))ββ) β§ (πΊβπ₯) β ((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯))) limβ π₯)))) |
40 | 31, 39 | mpbid 231 |
. . . . . 6
β’ ((π β§ π₯ β dom πΊ) β (π₯ β ((intβ(topGenβran
(,)))ββ) β§ (πΊβπ₯) β ((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯))) limβ π₯))) |
41 | 40 | simprd 497 |
. . . . 5
β’ ((π β§ π₯ β dom πΊ) β (πΊβπ₯) β ((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯))) limβ π₯)) |
42 | | eqidd 2734 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β (π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π)))) = (π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))) |
43 | | fveq2 6846 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π¦ = π β (πΉβπ¦) = (πΉβπ)) |
44 | 43 | oveq1d 7376 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ = π β ((πΉβπ¦) β (πΉβ(π₯ + π))) = ((πΉβπ) β (πΉβ(π₯ + π)))) |
45 | | oveq1 7368 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ = π β (π¦ β (π₯ + π)) = (π β (π₯ + π))) |
46 | 44, 45 | oveq12d 7379 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ = π β (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))) = (((πΉβπ) β (πΉβ(π₯ + π))) / (π β (π₯ + π)))) |
47 | | eldifi 4090 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (β β {(π₯ + π)}) β π β β) |
48 | 47 | recnd 11191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β (β β {(π₯ + π)}) β π β β) |
49 | 48 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π β (β β {(π₯ + π)})) β π β β) |
50 | 8 | recnd 11191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β π β β) |
51 | 50 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π β (β β {(π₯ + π)})) β π β β) |
52 | 49, 51 | npcand 11524 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π β (β β {(π₯ + π)})) β ((π β π) + π) = π) |
53 | 52 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π β (β β {(π₯ + π)})) β π = ((π β π) + π)) |
54 | 53 | fveq2d 6850 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β (β β {(π₯ + π)})) β (πΉβπ) = (πΉβ((π β π) + π))) |
55 | | ovex 7394 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β π) β V |
56 | 47 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π β (β β {(π₯ + π)})) β π β β) |
57 | 8 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π β (β β {(π₯ + π)})) β π β β) |
58 | 56, 57 | resubcld 11591 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π β (β β {(π₯ + π)})) β (π β π) β β) |
59 | 58 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (π β (β β {(π₯ + π)}) β (π β π) β β)) |
60 | 59 | imdistani 570 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π β (β β {(π₯ + π)})) β (π β§ (π β π) β β)) |
61 | | eleq1 2822 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π₯ = (π β π) β (π₯ β β β (π β π) β β)) |
62 | 61 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π₯ = (π β π) β ((π β§ π₯ β β) β (π β§ (π β π) β β))) |
63 | | fvoveq1 7384 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π₯ = (π β π) β (πΉβ(π₯ + π)) = (πΉβ((π β π) + π))) |
64 | | fveq2 6846 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π₯ = (π β π) β (πΉβπ₯) = (πΉβ(π β π))) |
65 | 63, 64 | eqeq12d 2749 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π₯ = (π β π) β ((πΉβ(π₯ + π)) = (πΉβπ₯) β (πΉβ((π β π) + π)) = (πΉβ(π β π)))) |
66 | 62, 65 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π₯ = (π β π) β (((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) β ((π β§ (π β π) β β) β (πΉβ((π β π) + π)) = (πΉβ(π β π))))) |
67 | | fperdvper.fper |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) |
68 | 66, 67 | vtoclg 3527 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β π) β V β ((π β§ (π β π) β β) β (πΉβ((π β π) + π)) = (πΉβ(π β π)))) |
69 | 55, 60, 68 | mpsyl 68 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β (β β {(π₯ + π)})) β (πΉβ((π β π) + π)) = (πΉβ(π β π))) |
70 | 54, 69 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β (β β {(π₯ + π)})) β (πΉβπ) = (πΉβ(π β π))) |
71 | 70 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β (πΉβπ) = (πΉβ(π β π))) |
72 | | simpll 766 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β π) |
73 | 6 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β π₯ β β) |
74 | 72, 73, 67 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β (πΉβ(π₯ + π)) = (πΉβπ₯)) |
75 | 71, 74 | oveq12d 7379 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β ((πΉβπ) β (πΉβ(π₯ + π))) = ((πΉβ(π β π)) β (πΉβπ₯))) |
76 | 48 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β π β β) |
77 | 72, 50 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β π β β) |
78 | 7 | recnd 11191 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π₯ β dom πΊ) β π₯ β β) |
79 | 78 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β π₯ β β) |
80 | 76, 77, 79 | subsub4d 11551 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β ((π β π) β π₯) = (π β (π + π₯))) |
81 | 77, 79 | addcomd 11365 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β (π + π₯) = (π₯ + π)) |
82 | 81 | oveq2d 7377 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β (π β (π + π₯)) = (π β (π₯ + π))) |
83 | 80, 82 | eqtr2d 2774 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β (π β (π₯ + π)) = ((π β π) β π₯)) |
84 | 75, 83 | oveq12d 7379 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β (((πΉβπ) β (πΉβ(π₯ + π))) / (π β (π₯ + π))) = (((πΉβ(π β π)) β (πΉβπ₯)) / ((π β π) β π₯))) |
85 | 46, 84 | sylan9eqr 2795 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β§ π¦ = π) β (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))) = (((πΉβ(π β π)) β (πΉβπ₯)) / ((π β π) β π₯))) |
86 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β π β (β β {(π₯ + π)})) |
87 | 37 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β (β β {(π₯ + π)})) β πΉ:ββΆβ) |
88 | 87, 58 | ffvelcdmd 7040 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β (β β {(π₯ + π)})) β (πΉβ(π β π)) β β) |
89 | 88 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β (πΉβ(π β π)) β β) |
90 | 38, 7 | ffvelcdmd 7040 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π₯ β dom πΊ) β (πΉβπ₯) β β) |
91 | 90 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β (πΉβπ₯) β β) |
92 | 89, 91 | subcld 11520 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β ((πΉβ(π β π)) β (πΉβπ₯)) β β) |
93 | 76, 77 | subcld 11520 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β (π β π) β β) |
94 | 93, 79 | subcld 11520 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β ((π β π) β π₯) β β) |
95 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β§ (π β π) = π₯) β (π β π) = π₯) |
96 | 48 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β§ (π β π) = π₯) β π β β) |
97 | 77 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β§ (π β π) = π₯) β π β β) |
98 | 79 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β§ (π β π) = π₯) β π₯ β β) |
99 | 96, 97, 98 | subadd2d 11539 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β§ (π β π) = π₯) β ((π β π) = π₯ β (π₯ + π) = π)) |
100 | 95, 99 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β§ (π β π) = π₯) β (π₯ + π) = π) |
101 | 100 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β§ (π β π) = π₯) β π = (π₯ + π)) |
102 | | eldifsni 4754 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (β β {(π₯ + π)}) β π β (π₯ + π)) |
103 | 102 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β§ (π β π) = π₯) β π β (π₯ + π)) |
104 | 103 | neneqd 2945 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β§ (π β π) = π₯) β Β¬ π = (π₯ + π)) |
105 | 101, 104 | pm2.65da 816 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β Β¬ (π β π) = π₯) |
106 | 105 | neqned 2947 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β (π β π) β π₯) |
107 | 93, 79, 106 | subne0d 11529 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β ((π β π) β π₯) β 0) |
108 | 92, 94, 107 | divcld 11939 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β (((πΉβ(π β π)) β (πΉβπ₯)) / ((π β π) β π₯)) β β) |
109 | 42, 85, 86, 108 | fvmptd 6959 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β ((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))βπ) = (((πΉβ(π β π)) β (πΉβπ₯)) / ((π β π) β π₯))) |
110 | 109 | fvoveq1d 7383 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β (absβ(((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))βπ) β π€)) = (absβ((((πΉβ(π β π)) β (πΉβπ₯)) / ((π β π) β π₯)) β π€))) |
111 | 110 | ad4ant13 750 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π₯ β dom πΊ) β§ βπ β (β β {π₯})((π β π₯ β§ (absβ(π β π₯)) < π) β (absβ(((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))βπ) β π€)) < π)) β§ π β (β β {(π₯ + π)})) β§ (π β (π₯ + π) β§ (absβ(π β (π₯ + π))) < π)) β (absβ(((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))βπ) β π€)) = (absβ((((πΉβ(π β π)) β (πΉβπ₯)) / ((π β π) β π₯)) β π€))) |
112 | | neeq1 3003 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (π β π) β (π β π₯ β (π β π) β π₯)) |
113 | | fvoveq1 7384 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (π β π) β (absβ(π β π₯)) = (absβ((π β π) β π₯))) |
114 | 113 | breq1d 5119 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (π β π) β ((absβ(π β π₯)) < π β (absβ((π β π) β π₯)) < π)) |
115 | 112, 114 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (π β π) β ((π β π₯ β§ (absβ(π β π₯)) < π) β ((π β π) β π₯ β§ (absβ((π β π) β π₯)) < π))) |
116 | 115 | imbrov2fvoveq 7386 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (π β π) β (((π β π₯ β§ (absβ(π β π₯)) < π) β (absβ(((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))βπ) β π€)) < π) β (((π β π) β π₯ β§ (absβ((π β π) β π₯)) < π) β (absβ(((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))β(π β π)) β π€)) < π))) |
117 | | simpllr 775 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π₯ β dom πΊ) β§ βπ β (β β {π₯})((π β π₯ β§ (absβ(π β π₯)) < π) β (absβ(((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))βπ) β π€)) < π)) β§ π β (β β {(π₯ + π)})) β§ (absβ(π β (π₯ + π))) < π) β βπ β (β β {π₯})((π β π₯ β§ (absβ(π β π₯)) < π) β (absβ(((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))βπ) β π€)) < π)) |
118 | 47 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ π₯ β dom πΊ) β§ βπ β (β β {π₯})((π β π₯ β§ (absβ(π β π₯)) < π) β (absβ(((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))βπ) β π€)) < π)) β§ π β (β β {(π₯ + π)})) β§ (absβ(π β (π₯ + π))) < π) β π β β) |
119 | 8 | ad4antr 731 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ π₯ β dom πΊ) β§ βπ β (β β {π₯})((π β π₯ β§ (absβ(π β π₯)) < π) β (absβ(((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))βπ) β π€)) < π)) β§ π β (β β {(π₯ + π)})) β§ (absβ(π β (π₯ + π))) < π) β π β β) |
120 | 118, 119 | resubcld 11591 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ π₯ β dom πΊ) β§ βπ β (β β {π₯})((π β π₯ β§ (absβ(π β π₯)) < π) β (absβ(((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))βπ) β π€)) < π)) β§ π β (β β {(π₯ + π)})) β§ (absβ(π β (π₯ + π))) < π) β (π β π) β β) |
121 | | elsni 4607 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β π) β {π₯} β (π β π) = π₯) |
122 | 105, 121 | nsyl 140 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β Β¬ (π β π) β {π₯}) |
123 | 122 | ad4ant13 750 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ π₯ β dom πΊ) β§ βπ β (β β {π₯})((π β π₯ β§ (absβ(π β π₯)) < π) β (absβ(((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))βπ) β π€)) < π)) β§ π β (β β {(π₯ + π)})) β§ (absβ(π β (π₯ + π))) < π) β Β¬ (π β π) β {π₯}) |
124 | 120, 123 | eldifd 3925 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π₯ β dom πΊ) β§ βπ β (β β {π₯})((π β π₯ β§ (absβ(π β π₯)) < π) β (absβ(((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))βπ) β π€)) < π)) β§ π β (β β {(π₯ + π)})) β§ (absβ(π β (π₯ + π))) < π) β (π β π) β (β β {π₯})) |
125 | 116, 117,
124 | rspcdva 3584 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π₯ β dom πΊ) β§ βπ β (β β {π₯})((π β π₯ β§ (absβ(π β π₯)) < π) β (absβ(((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))βπ) β π€)) < π)) β§ π β (β β {(π₯ + π)})) β§ (absβ(π β (π₯ + π))) < π) β (((π β π) β π₯ β§ (absβ((π β π) β π₯)) < π) β (absβ(((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))β(π β π)) β π€)) < π)) |
126 | | eqidd 2734 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β (π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯))) = (π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))) |
127 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β§ π¦ = (π β π)) β π¦ = (π β π)) |
128 | 127 | fveq2d 6850 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β§ π¦ = (π β π)) β (πΉβπ¦) = (πΉβ(π β π))) |
129 | 128 | oveq1d 7376 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β§ π¦ = (π β π)) β ((πΉβπ¦) β (πΉβπ₯)) = ((πΉβ(π β π)) β (πΉβπ₯))) |
130 | 127 | oveq1d 7376 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β§ π¦ = (π β π)) β (π¦ β π₯) = ((π β π) β π₯)) |
131 | 129, 130 | oveq12d 7379 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β§ π¦ = (π β π)) β (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)) = (((πΉβ(π β π)) β (πΉβπ₯)) / ((π β π) β π₯))) |
132 | 47 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β π β β) |
133 | 72, 8 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β π β β) |
134 | 132, 133 | resubcld 11591 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β (π β π) β β) |
135 | 134, 122 | eldifd 3925 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β (π β π) β (β β {π₯})) |
136 | 126, 131,
135, 108 | fvmptd 6959 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β ((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))β(π β π)) = (((πΉβ(π β π)) β (πΉβπ₯)) / ((π β π) β π₯))) |
137 | 136 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β (((πΉβ(π β π)) β (πΉβπ₯)) / ((π β π) β π₯)) = ((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))β(π β π))) |
138 | 137 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β§ (absβ(π β (π₯ + π))) < π) β§ (((π β π) β π₯ β§ (absβ((π β π) β π₯)) < π) β (absβ(((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))β(π β π)) β π€)) < π)) β (((πΉβ(π β π)) β (πΉβπ₯)) / ((π β π) β π₯)) = ((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))β(π β π))) |
139 | 138 | fvoveq1d 7383 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β§ (absβ(π β (π₯ + π))) < π) β§ (((π β π) β π₯ β§ (absβ((π β π) β π₯)) < π) β (absβ(((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))β(π β π)) β π€)) < π)) β (absβ((((πΉβ(π β π)) β (πΉβπ₯)) / ((π β π) β π₯)) β π€)) = (absβ(((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))β(π β π)) β π€))) |
140 | 106 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β§ (absβ(π β (π₯ + π))) < π) β (π β π) β π₯) |
141 | 83 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β ((π β π) β π₯) = (π β (π₯ + π))) |
142 | 141 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β§ (absβ(π β (π₯ + π))) < π) β ((π β π) β π₯) = (π β (π₯ + π))) |
143 | 142 | fveq2d 6850 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β§ (absβ(π β (π₯ + π))) < π) β (absβ((π β π) β π₯)) = (absβ(π β (π₯ + π)))) |
144 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β§ (absβ(π β (π₯ + π))) < π) β (absβ(π β (π₯ + π))) < π) |
145 | 143, 144 | eqbrtrd 5131 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β§ (absβ(π β (π₯ + π))) < π) β (absβ((π β π) β π₯)) < π) |
146 | 140, 145 | jca 513 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β§ (absβ(π β (π₯ + π))) < π) β ((π β π) β π₯ β§ (absβ((π β π) β π₯)) < π)) |
147 | 146 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β§ (absβ(π β (π₯ + π))) < π) β§ (((π β π) β π₯ β§ (absβ((π β π) β π₯)) < π) β (absβ(((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))β(π β π)) β π€)) < π)) β ((π β π) β π₯ β§ (absβ((π β π) β π₯)) < π)) |
148 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β§ (absβ(π β (π₯ + π))) < π) β§ (((π β π) β π₯ β§ (absβ((π β π) β π₯)) < π) β (absβ(((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))β(π β π)) β π€)) < π)) β (((π β π) β π₯ β§ (absβ((π β π) β π₯)) < π) β (absβ(((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))β(π β π)) β π€)) < π)) |
149 | 147, 148 | mpd 15 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β§ (absβ(π β (π₯ + π))) < π) β§ (((π β π) β π₯ β§ (absβ((π β π) β π₯)) < π) β (absβ(((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))β(π β π)) β π€)) < π)) β (absβ(((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))β(π β π)) β π€)) < π) |
150 | 139, 149 | eqbrtrd 5131 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β§ (absβ(π β (π₯ + π))) < π) β§ (((π β π) β π₯ β§ (absβ((π β π) β π₯)) < π) β (absβ(((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))β(π β π)) β π€)) < π)) β (absβ((((πΉβ(π β π)) β (πΉβπ₯)) / ((π β π) β π₯)) β π€)) < π) |
151 | 150 | ex 414 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π₯ β dom πΊ) β§ π β (β β {(π₯ + π)})) β§ (absβ(π β (π₯ + π))) < π) β ((((π β π) β π₯ β§ (absβ((π β π) β π₯)) < π) β (absβ(((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))β(π β π)) β π€)) < π) β (absβ((((πΉβ(π β π)) β (πΉβπ₯)) / ((π β π) β π₯)) β π€)) < π)) |
152 | 151 | adantllr 718 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π₯ β dom πΊ) β§ βπ β (β β {π₯})((π β π₯ β§ (absβ(π β π₯)) < π) β (absβ(((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))βπ) β π€)) < π)) β§ π β (β β {(π₯ + π)})) β§ (absβ(π β (π₯ + π))) < π) β ((((π β π) β π₯ β§ (absβ((π β π) β π₯)) < π) β (absβ(((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))β(π β π)) β π€)) < π) β (absβ((((πΉβ(π β π)) β (πΉβπ₯)) / ((π β π) β π₯)) β π€)) < π)) |
153 | 125, 152 | mpd 15 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π₯ β dom πΊ) β§ βπ β (β β {π₯})((π β π₯ β§ (absβ(π β π₯)) < π) β (absβ(((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))βπ) β π€)) < π)) β§ π β (β β {(π₯ + π)})) β§ (absβ(π β (π₯ + π))) < π) β (absβ((((πΉβ(π β π)) β (πΉβπ₯)) / ((π β π) β π₯)) β π€)) < π) |
154 | 153 | adantrl 715 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π₯ β dom πΊ) β§ βπ β (β β {π₯})((π β π₯ β§ (absβ(π β π₯)) < π) β (absβ(((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))βπ) β π€)) < π)) β§ π β (β β {(π₯ + π)})) β§ (π β (π₯ + π) β§ (absβ(π β (π₯ + π))) < π)) β (absβ((((πΉβ(π β π)) β (πΉβπ₯)) / ((π β π) β π₯)) β π€)) < π) |
155 | 111, 154 | eqbrtrd 5131 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π₯ β dom πΊ) β§ βπ β (β β {π₯})((π β π₯ β§ (absβ(π β π₯)) < π) β (absβ(((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))βπ) β π€)) < π)) β§ π β (β β {(π₯ + π)})) β§ (π β (π₯ + π) β§ (absβ(π β (π₯ + π))) < π)) β (absβ(((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))βπ) β π€)) < π) |
156 | 155 | ex 414 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β dom πΊ) β§ βπ β (β β {π₯})((π β π₯ β§ (absβ(π β π₯)) < π) β (absβ(((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))βπ) β π€)) < π)) β§ π β (β β {(π₯ + π)})) β ((π β (π₯ + π) β§ (absβ(π β (π₯ + π))) < π) β (absβ(((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))βπ) β π€)) < π)) |
157 | 156 | ralrimiva 3140 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β dom πΊ) β§ βπ β (β β {π₯})((π β π₯ β§ (absβ(π β π₯)) < π) β (absβ(((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))βπ) β π€)) < π)) β βπ β (β β {(π₯ + π)})((π β (π₯ + π) β§ (absβ(π β (π₯ + π))) < π) β (absβ(((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))βπ) β π€)) < π)) |
158 | | eqidd 2734 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (β β {π₯}) β (π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯))) = (π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))) |
159 | | fveq2 6846 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π¦ = π β (πΉβπ¦) = (πΉβπ)) |
160 | 159 | oveq1d 7376 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ = π β ((πΉβπ¦) β (πΉβπ₯)) = ((πΉβπ) β (πΉβπ₯))) |
161 | | oveq1 7368 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ = π β (π¦ β π₯) = (π β π₯)) |
162 | 160, 161 | oveq12d 7379 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ = π β (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)) = (((πΉβπ) β (πΉβπ₯)) / (π β π₯))) |
163 | 162 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β (β β {π₯}) β§ π¦ = π) β (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)) = (((πΉβπ) β (πΉβπ₯)) / (π β π₯))) |
164 | | id 22 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (β β {π₯}) β π β (β β {π₯})) |
165 | | ovexd 7396 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (β β {π₯}) β (((πΉβπ) β (πΉβπ₯)) / (π β π₯)) β V) |
166 | 158, 163,
164, 165 | fvmptd 6959 |
. . . . . . . . . . . . . . . . 17
β’ (π β (β β {π₯}) β ((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))βπ) = (((πΉβπ) β (πΉβπ₯)) / (π β π₯))) |
167 | 166 | fvoveq1d 7383 |
. . . . . . . . . . . . . . . 16
β’ (π β (β β {π₯}) β (absβ(((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))βπ) β π€)) = (absβ((((πΉβπ) β (πΉβπ₯)) / (π β π₯)) β π€))) |
168 | 167 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π₯ β dom πΊ) β§ βπ β (β β {(π₯ + π)})((π β (π₯ + π) β§ (absβ(π β (π₯ + π))) < π) β (absβ(((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))βπ) β π€)) < π)) β§ π β (β β {π₯})) β§ (π β π₯ β§ (absβ(π β π₯)) < π)) β (absβ(((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))βπ) β π€)) = (absβ((((πΉβπ) β (πΉβπ₯)) / (π β π₯)) β π€))) |
169 | | simpll 766 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {π₯})) β π) |
170 | | eldifi 4090 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (β β {π₯}) β π β β) |
171 | 170 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {π₯})) β π β β) |
172 | | eleq1 2822 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π₯ = π β (π₯ β β β π β β)) |
173 | 172 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π₯ = π β ((π β§ π₯ β β) β (π β§ π β β))) |
174 | | fvoveq1 7384 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π₯ = π β (πΉβ(π₯ + π)) = (πΉβ(π + π))) |
175 | | fveq2 6846 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π₯ = π β (πΉβπ₯) = (πΉβπ)) |
176 | 174, 175 | eqeq12d 2749 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π₯ = π β ((πΉβ(π₯ + π)) = (πΉβπ₯) β (πΉβ(π + π)) = (πΉβπ))) |
177 | 173, 176 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π₯ = π β (((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) β ((π β§ π β β) β (πΉβ(π + π)) = (πΉβπ)))) |
178 | 177, 67 | chvarvv 2003 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β β) β (πΉβ(π + π)) = (πΉβπ)) |
179 | 178 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β β) β (πΉβπ) = (πΉβ(π + π))) |
180 | 169, 171,
179 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {π₯})) β (πΉβπ) = (πΉβ(π + π))) |
181 | 6 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {π₯})) β π₯ β β) |
182 | 169, 181,
67 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {π₯})) β (πΉβ(π₯ + π)) = (πΉβπ₯)) |
183 | 182 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {π₯})) β (πΉβπ₯) = (πΉβ(π₯ + π))) |
184 | 180, 183 | oveq12d 7379 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {π₯})) β ((πΉβπ) β (πΉβπ₯)) = ((πΉβ(π + π)) β (πΉβ(π₯ + π)))) |
185 | 171 | recnd 11191 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {π₯})) β π β β) |
186 | 78 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {π₯})) β π₯ β β) |
187 | 169, 50 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {π₯})) β π β β) |
188 | 185, 186,
187 | pnpcan2d 11558 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {π₯})) β ((π + π) β (π₯ + π)) = (π β π₯)) |
189 | 188 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {π₯})) β (π β π₯) = ((π + π) β (π₯ + π))) |
190 | 184, 189 | oveq12d 7379 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {π₯})) β (((πΉβπ) β (πΉβπ₯)) / (π β π₯)) = (((πΉβ(π + π)) β (πΉβ(π₯ + π))) / ((π + π) β (π₯ + π)))) |
191 | 190 | fvoveq1d 7383 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {π₯})) β (absβ((((πΉβπ) β (πΉβπ₯)) / (π β π₯)) β π€)) = (absβ((((πΉβ(π + π)) β (πΉβ(π₯ + π))) / ((π + π) β (π₯ + π))) β π€))) |
192 | 191 | ad4ant13 750 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π₯ β dom πΊ) β§ βπ β (β β {(π₯ + π)})((π β (π₯ + π) β§ (absβ(π β (π₯ + π))) < π) β (absβ(((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))βπ) β π€)) < π)) β§ π β (β β {π₯})) β§ (absβ(π β π₯)) < π) β (absβ((((πΉβπ) β (πΉβπ₯)) / (π β π₯)) β π€)) = (absβ((((πΉβ(π + π)) β (πΉβ(π₯ + π))) / ((π + π) β (π₯ + π))) β π€))) |
193 | | neeq1 3003 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (π + π) β (π β (π₯ + π) β (π + π) β (π₯ + π))) |
194 | | fvoveq1 7384 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = (π + π) β (absβ(π β (π₯ + π))) = (absβ((π + π) β (π₯ + π)))) |
195 | 194 | breq1d 5119 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (π + π) β ((absβ(π β (π₯ + π))) < π β (absβ((π + π) β (π₯ + π))) < π)) |
196 | 193, 195 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (π + π) β ((π β (π₯ + π) β§ (absβ(π β (π₯ + π))) < π) β ((π + π) β (π₯ + π) β§ (absβ((π + π) β (π₯ + π))) < π))) |
197 | 196 | imbrov2fvoveq 7386 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (π + π) β (((π β (π₯ + π) β§ (absβ(π β (π₯ + π))) < π) β (absβ(((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))βπ) β π€)) < π) β (((π + π) β (π₯ + π) β§ (absβ((π + π) β (π₯ + π))) < π) β (absβ(((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))β(π + π)) β π€)) < π))) |
198 | | simpllr 775 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ π₯ β dom πΊ) β§ βπ β (β β {(π₯ + π)})((π β (π₯ + π) β§ (absβ(π β (π₯ + π))) < π) β (absβ(((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))βπ) β π€)) < π)) β§ π β (β β {π₯})) β§ (absβ(π β π₯)) < π) β βπ β (β β {(π₯ + π)})((π β (π₯ + π) β§ (absβ(π β (π₯ + π))) < π) β (absβ(((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))βπ) β π€)) < π)) |
199 | 170 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ π₯ β dom πΊ) β§ βπ β (β β {(π₯ + π)})((π β (π₯ + π) β§ (absβ(π β (π₯ + π))) < π) β (absβ(((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))βπ) β π€)) < π)) β§ π β (β β {π₯})) β§ (absβ(π β π₯)) < π) β π β β) |
200 | 8 | ad4antr 731 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ π₯ β dom πΊ) β§ βπ β (β β {(π₯ + π)})((π β (π₯ + π) β§ (absβ(π β (π₯ + π))) < π) β (absβ(((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))βπ) β π€)) < π)) β§ π β (β β {π₯})) β§ (absβ(π β π₯)) < π) β π β β) |
201 | 199, 200 | readdcld 11192 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ π₯ β dom πΊ) β§ βπ β (β β {(π₯ + π)})((π β (π₯ + π) β§ (absβ(π β (π₯ + π))) < π) β (absβ(((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))βπ) β π€)) < π)) β§ π β (β β {π₯})) β§ (absβ(π β π₯)) < π) β (π + π) β β) |
202 | | eldifsni 4754 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (β β {π₯}) β π β π₯) |
203 | 202 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {π₯})) β π β π₯) |
204 | 185, 186,
187, 203 | addneintr2d 11371 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {π₯})) β (π + π) β (π₯ + π)) |
205 | 204 | ad4ant13 750 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ π₯ β dom πΊ) β§ βπ β (β β {(π₯ + π)})((π β (π₯ + π) β§ (absβ(π β (π₯ + π))) < π) β (absβ(((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))βπ) β π€)) < π)) β§ π β (β β {π₯})) β§ (absβ(π β π₯)) < π) β (π + π) β (π₯ + π)) |
206 | | nelsn 4630 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π + π) β (π₯ + π) β Β¬ (π + π) β {(π₯ + π)}) |
207 | 205, 206 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ π₯ β dom πΊ) β§ βπ β (β β {(π₯ + π)})((π β (π₯ + π) β§ (absβ(π β (π₯ + π))) < π) β (absβ(((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))βπ) β π€)) < π)) β§ π β (β β {π₯})) β§ (absβ(π β π₯)) < π) β Β¬ (π + π) β {(π₯ + π)}) |
208 | 201, 207 | eldifd 3925 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ π₯ β dom πΊ) β§ βπ β (β β {(π₯ + π)})((π β (π₯ + π) β§ (absβ(π β (π₯ + π))) < π) β (absβ(((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))βπ) β π€)) < π)) β§ π β (β β {π₯})) β§ (absβ(π β π₯)) < π) β (π + π) β (β β {(π₯ + π)})) |
209 | 197, 198,
208 | rspcdva 3584 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π₯ β dom πΊ) β§ βπ β (β β {(π₯ + π)})((π β (π₯ + π) β§ (absβ(π β (π₯ + π))) < π) β (absβ(((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))βπ) β π€)) < π)) β§ π β (β β {π₯})) β§ (absβ(π β π₯)) < π) β (((π + π) β (π₯ + π) β§ (absβ((π + π) β (π₯ + π))) < π) β (absβ(((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))β(π + π)) β π€)) < π)) |
210 | | eqidd 2734 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {π₯})) β (π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π)))) = (π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))) |
211 | | fveq2 6846 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π¦ = (π + π) β (πΉβπ¦) = (πΉβ(π + π))) |
212 | 211 | oveq1d 7376 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π¦ = (π + π) β ((πΉβπ¦) β (πΉβ(π₯ + π))) = ((πΉβ(π + π)) β (πΉβ(π₯ + π)))) |
213 | | oveq1 7368 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π¦ = (π + π) β (π¦ β (π₯ + π)) = ((π + π) β (π₯ + π))) |
214 | 212, 213 | oveq12d 7379 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π¦ = (π + π) β (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))) = (((πΉβ(π + π)) β (πΉβ(π₯ + π))) / ((π + π) β (π₯ + π)))) |
215 | 214 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π₯ β dom πΊ) β§ π β (β β {π₯})) β§ π¦ = (π + π)) β (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))) = (((πΉβ(π + π)) β (πΉβ(π₯ + π))) / ((π + π) β (π₯ + π)))) |
216 | 169, 8 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {π₯})) β π β β) |
217 | 171, 216 | readdcld 11192 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {π₯})) β (π + π) β β) |
218 | 204, 206 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {π₯})) β Β¬ (π + π) β {(π₯ + π)}) |
219 | 217, 218 | eldifd 3925 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {π₯})) β (π + π) β (β β {(π₯ + π)})) |
220 | | ovexd 7396 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {π₯})) β (((πΉβ(π + π)) β (πΉβ(π₯ + π))) / ((π + π) β (π₯ + π))) β V) |
221 | 210, 215,
219, 220 | fvmptd 6959 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {π₯})) β ((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))β(π + π)) = (((πΉβ(π + π)) β (πΉβ(π₯ + π))) / ((π + π) β (π₯ + π)))) |
222 | 221 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π₯ β dom πΊ) β§ π β (β β {π₯})) β (((πΉβ(π + π)) β (πΉβ(π₯ + π))) / ((π + π) β (π₯ + π))) = ((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))β(π + π))) |
223 | 222 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ π₯ β dom πΊ) β§ π β (β β {π₯})) β§ (absβ(π β π₯)) < π) β§ (((π + π) β (π₯ + π) β§ (absβ((π + π) β (π₯ + π))) < π) β (absβ(((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))β(π + π)) β π€)) < π)) β (((πΉβ(π + π)) β (πΉβ(π₯ + π))) / ((π + π) β (π₯ + π))) = ((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))β(π + π))) |
224 | 223 | fvoveq1d 7383 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ π₯ β dom πΊ) β§ π β (β β {π₯})) β§ (absβ(π β π₯)) < π) β§ (((π + π) β (π₯ + π) β§ (absβ((π + π) β (π₯ + π))) < π) β (absβ(((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))β(π + π)) β π€)) < π)) β (absβ((((πΉβ(π + π)) β (πΉβ(π₯ + π))) / ((π + π) β (π₯ + π))) β π€)) = (absβ(((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))β(π + π)) β π€))) |
225 | 204 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π₯ β dom πΊ) β§ π β (β β {π₯})) β§ (absβ(π β π₯)) < π) β (π + π) β (π₯ + π)) |
226 | 170 | recnd 11191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (β β {π₯}) β π β β) |
227 | 226 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π₯ β dom πΊ) β§ π β (β β {π₯})) β§ (absβ(π β π₯)) < π) β π β β) |
228 | 186 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π₯ β dom πΊ) β§ π β (β β {π₯})) β§ (absβ(π β π₯)) < π) β π₯ β β) |
229 | 187 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π₯ β dom πΊ) β§ π β (β β {π₯})) β§ (absβ(π β π₯)) < π) β π β β) |
230 | 227, 228,
229 | pnpcan2d 11558 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π₯ β dom πΊ) β§ π β (β β {π₯})) β§ (absβ(π β π₯)) < π) β ((π + π) β (π₯ + π)) = (π β π₯)) |
231 | 230 | fveq2d 6850 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π₯ β dom πΊ) β§ π β (β β {π₯})) β§ (absβ(π β π₯)) < π) β (absβ((π + π) β (π₯ + π))) = (absβ(π β π₯))) |
232 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π₯ β dom πΊ) β§ π β (β β {π₯})) β§ (absβ(π β π₯)) < π) β (absβ(π β π₯)) < π) |
233 | 231, 232 | eqbrtrd 5131 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π₯ β dom πΊ) β§ π β (β β {π₯})) β§ (absβ(π β π₯)) < π) β (absβ((π + π) β (π₯ + π))) < π) |
234 | 225, 233 | jca 513 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π₯ β dom πΊ) β§ π β (β β {π₯})) β§ (absβ(π β π₯)) < π) β ((π + π) β (π₯ + π) β§ (absβ((π + π) β (π₯ + π))) < π)) |
235 | 234 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ π₯ β dom πΊ) β§ π β (β β {π₯})) β§ (absβ(π β π₯)) < π) β§ (((π + π) β (π₯ + π) β§ (absβ((π + π) β (π₯ + π))) < π) β (absβ(((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))β(π + π)) β π€)) < π)) β ((π + π) β (π₯ + π) β§ (absβ((π + π) β (π₯ + π))) < π)) |
236 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ π₯ β dom πΊ) β§ π β (β β {π₯})) β§ (absβ(π β π₯)) < π) β§ (((π + π) β (π₯ + π) β§ (absβ((π + π) β (π₯ + π))) < π) β (absβ(((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))β(π + π)) β π€)) < π)) β (((π + π) β (π₯ + π) β§ (absβ((π + π) β (π₯ + π))) < π) β (absβ(((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))β(π + π)) β π€)) < π)) |
237 | 235, 236 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ π₯ β dom πΊ) β§ π β (β β {π₯})) β§ (absβ(π β π₯)) < π) β§ (((π + π) β (π₯ + π) β§ (absβ((π + π) β (π₯ + π))) < π) β (absβ(((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))β(π + π)) β π€)) < π)) β (absβ(((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))β(π + π)) β π€)) < π) |
238 | 224, 237 | eqbrtrd 5131 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ π₯ β dom πΊ) β§ π β (β β {π₯})) β§ (absβ(π β π₯)) < π) β§ (((π + π) β (π₯ + π) β§ (absβ((π + π) β (π₯ + π))) < π) β (absβ(((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))β(π + π)) β π€)) < π)) β (absβ((((πΉβ(π + π)) β (πΉβ(π₯ + π))) / ((π + π) β (π₯ + π))) β π€)) < π) |
239 | 238 | ex 414 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π₯ β dom πΊ) β§ π β (β β {π₯})) β§ (absβ(π β π₯)) < π) β ((((π + π) β (π₯ + π) β§ (absβ((π + π) β (π₯ + π))) < π) β (absβ(((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))β(π + π)) β π€)) < π) β (absβ((((πΉβ(π + π)) β (πΉβ(π₯ + π))) / ((π + π) β (π₯ + π))) β π€)) < π)) |
240 | 239 | adantllr 718 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π₯ β dom πΊ) β§ βπ β (β β {(π₯ + π)})((π β (π₯ + π) β§ (absβ(π β (π₯ + π))) < π) β (absβ(((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))βπ) β π€)) < π)) β§ π β (β β {π₯})) β§ (absβ(π β π₯)) < π) β ((((π + π) β (π₯ + π) β§ (absβ((π + π) β (π₯ + π))) < π) β (absβ(((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))β(π + π)) β π€)) < π) β (absβ((((πΉβ(π + π)) β (πΉβ(π₯ + π))) / ((π + π) β (π₯ + π))) β π€)) < π)) |
241 | 209, 240 | mpd 15 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π₯ β dom πΊ) β§ βπ β (β β {(π₯ + π)})((π β (π₯ + π) β§ (absβ(π β (π₯ + π))) < π) β (absβ(((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))βπ) β π€)) < π)) β§ π β (β β {π₯})) β§ (absβ(π β π₯)) < π) β (absβ((((πΉβ(π + π)) β (πΉβ(π₯ + π))) / ((π + π) β (π₯ + π))) β π€)) < π) |
242 | 192, 241 | eqbrtrd 5131 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π₯ β dom πΊ) β§ βπ β (β β {(π₯ + π)})((π β (π₯ + π) β§ (absβ(π β (π₯ + π))) < π) β (absβ(((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))βπ) β π€)) < π)) β§ π β (β β {π₯})) β§ (absβ(π β π₯)) < π) β (absβ((((πΉβπ) β (πΉβπ₯)) / (π β π₯)) β π€)) < π) |
243 | 242 | adantrl 715 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π₯ β dom πΊ) β§ βπ β (β β {(π₯ + π)})((π β (π₯ + π) β§ (absβ(π β (π₯ + π))) < π) β (absβ(((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))βπ) β π€)) < π)) β§ π β (β β {π₯})) β§ (π β π₯ β§ (absβ(π β π₯)) < π)) β (absβ((((πΉβπ) β (πΉβπ₯)) / (π β π₯)) β π€)) < π) |
244 | 168, 243 | eqbrtrd 5131 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π₯ β dom πΊ) β§ βπ β (β β {(π₯ + π)})((π β (π₯ + π) β§ (absβ(π β (π₯ + π))) < π) β (absβ(((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))βπ) β π€)) < π)) β§ π β (β β {π₯})) β§ (π β π₯ β§ (absβ(π β π₯)) < π)) β (absβ(((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))βπ) β π€)) < π) |
245 | 244 | ex 414 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β dom πΊ) β§ βπ β (β β {(π₯ + π)})((π β (π₯ + π) β§ (absβ(π β (π₯ + π))) < π) β (absβ(((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))βπ) β π€)) < π)) β§ π β (β β {π₯})) β ((π β π₯ β§ (absβ(π β π₯)) < π) β (absβ(((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))βπ) β π€)) < π)) |
246 | 245 | ralrimiva 3140 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β dom πΊ) β§ βπ β (β β {(π₯ + π)})((π β (π₯ + π) β§ (absβ(π β (π₯ + π))) < π) β (absβ(((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))βπ) β π€)) < π)) β βπ β (β β {π₯})((π β π₯ β§ (absβ(π β π₯)) < π) β (absβ(((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))βπ) β π€)) < π)) |
247 | 157, 246 | impbida 800 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β dom πΊ) β (βπ β (β β {π₯})((π β π₯ β§ (absβ(π β π₯)) < π) β (absβ(((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))βπ) β π€)) < π) β βπ β (β β {(π₯ + π)})((π β (π₯ + π) β§ (absβ(π β (π₯ + π))) < π) β (absβ(((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))βπ) β π€)) < π))) |
248 | 247 | rexbidv 3172 |
. . . . . . . . . 10
β’ ((π β§ π₯ β dom πΊ) β (βπ β β+ βπ β (β β {π₯})((π β π₯ β§ (absβ(π β π₯)) < π) β (absβ(((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))βπ) β π€)) < π) β βπ β β+ βπ β (β β {(π₯ + π)})((π β (π₯ + π) β§ (absβ(π β (π₯ + π))) < π) β (absβ(((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))βπ) β π€)) < π))) |
249 | 248 | ralbidv 3171 |
. . . . . . . . 9
β’ ((π β§ π₯ β dom πΊ) β (βπ β β+ βπ β β+
βπ β (β
β {π₯})((π β π₯ β§ (absβ(π β π₯)) < π) β (absβ(((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))βπ) β π€)) < π) β βπ β β+ βπ β β+
βπ β (β
β {(π₯ + π)})((π β (π₯ + π) β§ (absβ(π β (π₯ + π))) < π) β (absβ(((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))βπ) β π€)) < π))) |
250 | 249 | anbi2d 630 |
. . . . . . . 8
β’ ((π β§ π₯ β dom πΊ) β ((π€ β β β§ βπ β β+
βπ β
β+ βπ β (β β {π₯})((π β π₯ β§ (absβ(π β π₯)) < π) β (absβ(((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))βπ) β π€)) < π)) β (π€ β β β§ βπ β β+
βπ β
β+ βπ β (β β {(π₯ + π)})((π β (π₯ + π) β§ (absβ(π β (π₯ + π))) < π) β (absβ(((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))βπ) β π€)) < π)))) |
251 | 38, 36, 7 | dvlem 25283 |
. . . . . . . . . 10
β’ (((π β§ π₯ β dom πΊ) β§ π¦ β (β β {π₯})) β (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)) β β) |
252 | 251 | fmpttd 7067 |
. . . . . . . . 9
β’ ((π β§ π₯ β dom πΊ) β (π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯))):(β β {π₯})βΆβ) |
253 | 36 | ssdifssd 4106 |
. . . . . . . . 9
β’ ((π β§ π₯ β dom πΊ) β (β β {π₯}) β
β) |
254 | 252, 253,
78 | ellimc3 25266 |
. . . . . . . 8
β’ ((π β§ π₯ β dom πΊ) β (π€ β ((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯))) limβ π₯) β (π€ β β β§ βπ β β+
βπ β
β+ βπ β (β β {π₯})((π β π₯ β§ (absβ(π β π₯)) < π) β (absβ(((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯)))βπ) β π€)) < π)))) |
255 | 38, 36, 10 | dvlem 25283 |
. . . . . . . . . 10
β’ (((π β§ π₯ β dom πΊ) β§ π¦ β (β β {(π₯ + π)})) β (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))) β β) |
256 | 255 | fmpttd 7067 |
. . . . . . . . 9
β’ ((π β§ π₯ β dom πΊ) β (π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π)))):(β β {(π₯ + π)})βΆβ) |
257 | 36 | ssdifssd 4106 |
. . . . . . . . 9
β’ ((π β§ π₯ β dom πΊ) β (β β {(π₯ + π)}) β β) |
258 | 10 | recnd 11191 |
. . . . . . . . 9
β’ ((π β§ π₯ β dom πΊ) β (π₯ + π) β β) |
259 | 256, 257,
258 | ellimc3 25266 |
. . . . . . . 8
β’ ((π β§ π₯ β dom πΊ) β (π€ β ((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π)))) limβ (π₯ + π)) β (π€ β β β§ βπ β β+
βπ β
β+ βπ β (β β {(π₯ + π)})((π β (π₯ + π) β§ (absβ(π β (π₯ + π))) < π) β (absβ(((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))))βπ) β π€)) < π)))) |
260 | 250, 254,
259 | 3bitr4d 311 |
. . . . . . 7
β’ ((π β§ π₯ β dom πΊ) β (π€ β ((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯))) limβ π₯) β π€ β ((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π)))) limβ (π₯ + π)))) |
261 | 260 | eqrdv 2731 |
. . . . . 6
β’ ((π β§ π₯ β dom πΊ) β ((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯))) limβ π₯) = ((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π)))) limβ (π₯ + π))) |
262 | | fveq2 6846 |
. . . . . . . . . 10
β’ (π¦ = π§ β (πΉβπ¦) = (πΉβπ§)) |
263 | 262 | oveq1d 7376 |
. . . . . . . . 9
β’ (π¦ = π§ β ((πΉβπ¦) β (πΉβ(π₯ + π))) = ((πΉβπ§) β (πΉβ(π₯ + π)))) |
264 | | oveq1 7368 |
. . . . . . . . 9
β’ (π¦ = π§ β (π¦ β (π₯ + π)) = (π§ β (π₯ + π))) |
265 | 263, 264 | oveq12d 7379 |
. . . . . . . 8
β’ (π¦ = π§ β (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π))) = (((πΉβπ§) β (πΉβ(π₯ + π))) / (π§ β (π₯ + π)))) |
266 | 265 | cbvmptv 5222 |
. . . . . . 7
β’ (π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π)))) = (π§ β (β β {(π₯ + π)}) β¦ (((πΉβπ§) β (πΉβ(π₯ + π))) / (π§ β (π₯ + π)))) |
267 | 266 | oveq1i 7371 |
. . . . . 6
β’ ((π¦ β (β β {(π₯ + π)}) β¦ (((πΉβπ¦) β (πΉβ(π₯ + π))) / (π¦ β (π₯ + π)))) limβ (π₯ + π)) = ((π§ β (β β {(π₯ + π)}) β¦ (((πΉβπ§) β (πΉβ(π₯ + π))) / (π§ β (π₯ + π)))) limβ (π₯ + π)) |
268 | 261, 267 | eqtrdi 2789 |
. . . . 5
β’ ((π β§ π₯ β dom πΊ) β ((π¦ β (β β {π₯}) β¦ (((πΉβπ¦) β (πΉβπ₯)) / (π¦ β π₯))) limβ π₯) = ((π§ β (β β {(π₯ + π)}) β¦ (((πΉβπ§) β (πΉβ(π₯ + π))) / (π§ β (π₯ + π)))) limβ (π₯ + π))) |
269 | 41, 268 | eleqtrd 2836 |
. . . 4
β’ ((π β§ π₯ β dom πΊ) β (πΊβπ₯) β ((π§ β (β β {(π₯ + π)}) β¦ (((πΉβπ§) β (πΉβ(π₯ + π))) / (π§ β (π₯ + π)))) limβ (π₯ + π))) |
270 | | eqid 2733 |
. . . . . 6
β’ (π§ β (β β {(π₯ + π)}) β¦ (((πΉβπ§) β (πΉβ(π₯ + π))) / (π§ β (π₯ + π)))) = (π§ β (β β {(π₯ + π)}) β¦ (((πΉβπ§) β (πΉβ(π₯ + π))) / (π§ β (π₯ + π)))) |
271 | 35 | a1i 11 |
. . . . . 6
β’ (π β β β
β) |
272 | | ssidd 3971 |
. . . . . 6
β’ (π β β β
β) |
273 | 32, 33, 270, 271, 37, 272 | eldv 25285 |
. . . . 5
β’ (π β ((π₯ + π)(β D πΉ)(πΊβπ₯) β ((π₯ + π) β ((intβ(topGenβran
(,)))ββ) β§ (πΊβπ₯) β ((π§ β (β β {(π₯ + π)}) β¦ (((πΉβπ§) β (πΉβ(π₯ + π))) / (π§ β (π₯ + π)))) limβ (π₯ + π))))) |
274 | 273 | adantr 482 |
. . . 4
β’ ((π β§ π₯ β dom πΊ) β ((π₯ + π)(β D πΉ)(πΊβπ₯) β ((π₯ + π) β ((intβ(topGenβran
(,)))ββ) β§ (πΊβπ₯) β ((π§ β (β β {(π₯ + π)}) β¦ (((πΉβπ§) β (πΉβ(π₯ + π))) / (π§ β (π₯ + π)))) limβ (π₯ + π))))) |
275 | 19, 269, 274 | mpbir2and 712 |
. . 3
β’ ((π β§ π₯ β dom πΊ) β (π₯ + π)(β D πΉ)(πΊβπ₯)) |
276 | 3 | a1i 11 |
. . . 4
β’ ((π β§ π₯ β dom πΊ) β πΊ = (β D πΉ)) |
277 | 276 | breqd 5120 |
. . 3
β’ ((π β§ π₯ β dom πΊ) β ((π₯ + π)πΊ(πΊβπ₯) β (π₯ + π)(β D πΉ)(πΊβπ₯))) |
278 | 275, 277 | mpbird 257 |
. 2
β’ ((π β§ π₯ β dom πΊ) β (π₯ + π)πΊ(πΊβπ₯)) |
279 | 3 | a1i 11 |
. . . . . 6
β’ (π β πΊ = (β D πΉ)) |
280 | 279 | funeqd 6527 |
. . . . 5
β’ (π β (Fun πΊ β Fun (β D πΉ))) |
281 | 27, 280 | mpbird 257 |
. . . 4
β’ (π β Fun πΊ) |
282 | 281 | adantr 482 |
. . 3
β’ ((π β§ π₯ β dom πΊ) β Fun πΊ) |
283 | | funbrfv2b 6904 |
. . 3
β’ (Fun
πΊ β ((π₯ + π)πΊ(πΊβπ₯) β ((π₯ + π) β dom πΊ β§ (πΊβ(π₯ + π)) = (πΊβπ₯)))) |
284 | 282, 283 | syl 17 |
. 2
β’ ((π β§ π₯ β dom πΊ) β ((π₯ + π)πΊ(πΊβπ₯) β ((π₯ + π) β dom πΊ β§ (πΊβ(π₯ + π)) = (πΊβπ₯)))) |
285 | 278, 284 | mpbid 231 |
1
β’ ((π β§ π₯ β dom πΊ) β ((π₯ + π) β dom πΊ β§ (πΊβ(π₯ + π)) = (πΊβπ₯))) |