Step | Hyp | Ref
| Expression |
1 | | smcn.u |
. . 3
β’ π β NrmCVec |
2 | | smcn.x |
. . . 4
β’ π = (BaseSetβπ) |
3 | | smcn.s |
. . . 4
β’ π = (
Β·π OLD βπ) |
4 | 2, 3 | nvsf 29603 |
. . 3
β’ (π β NrmCVec β π:(β Γ π)βΆπ) |
5 | 1, 4 | ax-mp 5 |
. 2
β’ π:(β Γ π)βΆπ |
6 | | smcn.t |
. . . . . 6
β’ π = (1 / (1 + ((((πβπ¦) + (absβπ₯)) + 1) / π))) |
7 | | 1rp 12924 |
. . . . . . . 8
β’ 1 β
β+ |
8 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π₯ β β β§ π¦ β π) β π¦ β π) |
9 | | smcn.n |
. . . . . . . . . . . . 13
β’ π =
(normCVβπ) |
10 | 2, 9 | nvcl 29645 |
. . . . . . . . . . . 12
β’ ((π β NrmCVec β§ π¦ β π) β (πβπ¦) β β) |
11 | 1, 8, 10 | sylancr 588 |
. . . . . . . . . . 11
β’ ((π₯ β β β§ π¦ β π) β (πβπ¦) β β) |
12 | | abscl 15169 |
. . . . . . . . . . . 12
β’ (π₯ β β β
(absβπ₯) β
β) |
13 | 12 | adantr 482 |
. . . . . . . . . . 11
β’ ((π₯ β β β§ π¦ β π) β (absβπ₯) β β) |
14 | 11, 13 | readdcld 11189 |
. . . . . . . . . 10
β’ ((π₯ β β β§ π¦ β π) β ((πβπ¦) + (absβπ₯)) β β) |
15 | 2, 9 | nvge0 29657 |
. . . . . . . . . . . 12
β’ ((π β NrmCVec β§ π¦ β π) β 0 β€ (πβπ¦)) |
16 | 1, 8, 15 | sylancr 588 |
. . . . . . . . . . 11
β’ ((π₯ β β β§ π¦ β π) β 0 β€ (πβπ¦)) |
17 | | absge0 15178 |
. . . . . . . . . . . 12
β’ (π₯ β β β 0 β€
(absβπ₯)) |
18 | 17 | adantr 482 |
. . . . . . . . . . 11
β’ ((π₯ β β β§ π¦ β π) β 0 β€ (absβπ₯)) |
19 | 11, 13, 16, 18 | addge0d 11736 |
. . . . . . . . . 10
β’ ((π₯ β β β§ π¦ β π) β 0 β€ ((πβπ¦) + (absβπ₯))) |
20 | 14, 19 | ge0p1rpd 12992 |
. . . . . . . . 9
β’ ((π₯ β β β§ π¦ β π) β (((πβπ¦) + (absβπ₯)) + 1) β
β+) |
21 | | rpdivcl 12945 |
. . . . . . . . 9
β’
(((((πβπ¦) + (absβπ₯)) + 1) β
β+ β§ π
β β+) β ((((πβπ¦) + (absβπ₯)) + 1) / π) β
β+) |
22 | 20, 21 | sylan 581 |
. . . . . . . 8
β’ (((π₯ β β β§ π¦ β π) β§ π β β+) β ((((πβπ¦) + (absβπ₯)) + 1) / π) β
β+) |
23 | | rpaddcl 12942 |
. . . . . . . 8
β’ ((1
β β+ β§ ((((πβπ¦) + (absβπ₯)) + 1) / π) β β+) β (1 +
((((πβπ¦) + (absβπ₯)) + 1) / π)) β
β+) |
24 | 7, 22, 23 | sylancr 588 |
. . . . . . 7
β’ (((π₯ β β β§ π¦ β π) β§ π β β+) β (1 +
((((πβπ¦) + (absβπ₯)) + 1) / π)) β
β+) |
25 | 24 | rpreccld 12972 |
. . . . . 6
β’ (((π₯ β β β§ π¦ β π) β§ π β β+) β (1 / (1 +
((((πβπ¦) + (absβπ₯)) + 1) / π))) β
β+) |
26 | 6, 25 | eqeltrid 2838 |
. . . . 5
β’ (((π₯ β β β§ π¦ β π) β§ π β β+) β π β
β+) |
27 | | smcn.c |
. . . . . . . . . . . 12
β’ πΆ = (IndMetβπ) |
28 | 2, 27 | imsmet 29675 |
. . . . . . . . . . 11
β’ (π β NrmCVec β πΆ β (Metβπ)) |
29 | 1, 28 | ax-mp 5 |
. . . . . . . . . 10
β’ πΆ β (Metβπ) |
30 | 29 | a1i 11 |
. . . . . . . . 9
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β πΆ β (Metβπ)) |
31 | 1 | a1i 11 |
. . . . . . . . . 10
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β π β NrmCVec) |
32 | | simplll 774 |
. . . . . . . . . 10
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β π₯ β β) |
33 | | simpllr 775 |
. . . . . . . . . 10
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β π¦ β π) |
34 | 2, 3 | nvscl 29610 |
. . . . . . . . . 10
β’ ((π β NrmCVec β§ π₯ β β β§ π¦ β π) β (π₯ππ¦) β π) |
35 | 31, 32, 33, 34 | syl3anc 1372 |
. . . . . . . . 9
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (π₯ππ¦) β π) |
36 | | simprll 778 |
. . . . . . . . . 10
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β π§ β β) |
37 | | simprlr 779 |
. . . . . . . . . 10
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β π€ β π) |
38 | 2, 3 | nvscl 29610 |
. . . . . . . . . 10
β’ ((π β NrmCVec β§ π§ β β β§ π€ β π) β (π§ππ€) β π) |
39 | 31, 36, 37, 38 | syl3anc 1372 |
. . . . . . . . 9
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (π§ππ€) β π) |
40 | | metcl 23701 |
. . . . . . . . 9
β’ ((πΆ β (Metβπ) β§ (π₯ππ¦) β π β§ (π§ππ€) β π) β ((π₯ππ¦)πΆ(π§ππ€)) β β) |
41 | 30, 35, 39, 40 | syl3anc 1372 |
. . . . . . . 8
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β ((π₯ππ¦)πΆ(π§ππ€)) β β) |
42 | 2, 3 | nvscl 29610 |
. . . . . . . . . . 11
β’ ((π β NrmCVec β§ π§ β β β§ π¦ β π) β (π§ππ¦) β π) |
43 | 31, 36, 33, 42 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (π§ππ¦) β π) |
44 | | metcl 23701 |
. . . . . . . . . 10
β’ ((πΆ β (Metβπ) β§ (π₯ππ¦) β π β§ (π§ππ¦) β π) β ((π₯ππ¦)πΆ(π§ππ¦)) β β) |
45 | 30, 35, 43, 44 | syl3anc 1372 |
. . . . . . . . 9
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β ((π₯ππ¦)πΆ(π§ππ¦)) β β) |
46 | | metcl 23701 |
. . . . . . . . . 10
β’ ((πΆ β (Metβπ) β§ (π§ππ¦) β π β§ (π§ππ€) β π) β ((π§ππ¦)πΆ(π§ππ€)) β β) |
47 | 30, 43, 39, 46 | syl3anc 1372 |
. . . . . . . . 9
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β ((π§ππ¦)πΆ(π§ππ€)) β β) |
48 | 45, 47 | readdcld 11189 |
. . . . . . . 8
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (((π₯ππ¦)πΆ(π§ππ¦)) + ((π§ππ¦)πΆ(π§ππ€))) β β) |
49 | | rpre 12928 |
. . . . . . . . 9
β’ (π β β+
β π β
β) |
50 | 49 | ad2antlr 726 |
. . . . . . . 8
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β π β β) |
51 | | mettri 23721 |
. . . . . . . . 9
β’ ((πΆ β (Metβπ) β§ ((π₯ππ¦) β π β§ (π§ππ€) β π β§ (π§ππ¦) β π)) β ((π₯ππ¦)πΆ(π§ππ€)) β€ (((π₯ππ¦)πΆ(π§ππ¦)) + ((π§ππ¦)πΆ(π§ππ€)))) |
52 | 30, 35, 39, 43, 51 | syl13anc 1373 |
. . . . . . . 8
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β ((π₯ππ¦)πΆ(π§ππ€)) β€ (((π₯ππ¦)πΆ(π§ππ¦)) + ((π§ππ¦)πΆ(π§ππ€)))) |
53 | 1, 33, 10 | sylancr 588 |
. . . . . . . . . . . 12
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (πβπ¦) β β) |
54 | 32 | abscld 15327 |
. . . . . . . . . . . 12
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (absβπ₯) β β) |
55 | 53, 54 | readdcld 11189 |
. . . . . . . . . . 11
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β ((πβπ¦) + (absβπ₯)) β β) |
56 | | peano2re 11333 |
. . . . . . . . . . 11
β’ (((πβπ¦) + (absβπ₯)) β β β (((πβπ¦) + (absβπ₯)) + 1) β β) |
57 | 55, 56 | syl 17 |
. . . . . . . . . 10
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (((πβπ¦) + (absβπ₯)) + 1) β β) |
58 | 26 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β π β
β+) |
59 | 58 | rpred 12962 |
. . . . . . . . . 10
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β π β β) |
60 | 57, 59 | remulcld 11190 |
. . . . . . . . 9
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β ((((πβπ¦) + (absβπ₯)) + 1) Β· π) β β) |
61 | 32, 36 | subcld 11517 |
. . . . . . . . . . . . 13
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (π₯ β π§) β β) |
62 | 61 | abscld 15327 |
. . . . . . . . . . . 12
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (absβ(π₯ β π§)) β β) |
63 | 62, 53 | remulcld 11190 |
. . . . . . . . . . 11
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β ((absβ(π₯ β π§)) Β· (πβπ¦)) β β) |
64 | 36 | abscld 15327 |
. . . . . . . . . . . 12
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (absβπ§) β β) |
65 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’ (
βπ£ βπ) = ( βπ£
βπ) |
66 | 2, 65 | nvmcl 29630 |
. . . . . . . . . . . . . 14
β’ ((π β NrmCVec β§ π¦ β π β§ π€ β π) β (π¦( βπ£ βπ)π€) β π) |
67 | 31, 33, 37, 66 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (π¦( βπ£ βπ)π€) β π) |
68 | 2, 9 | nvcl 29645 |
. . . . . . . . . . . . 13
β’ ((π β NrmCVec β§ (π¦( βπ£
βπ)π€) β π) β (πβ(π¦( βπ£ βπ)π€)) β β) |
69 | 1, 67, 68 | sylancr 588 |
. . . . . . . . . . . 12
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (πβ(π¦( βπ£ βπ)π€)) β β) |
70 | 64, 69 | remulcld 11190 |
. . . . . . . . . . 11
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β ((absβπ§) Β· (πβ(π¦( βπ£ βπ)π€))) β β) |
71 | 53, 59 | remulcld 11190 |
. . . . . . . . . . 11
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β ((πβπ¦) Β· π) β β) |
72 | | peano2re 11333 |
. . . . . . . . . . . . 13
β’
((absβπ₯)
β β β ((absβπ₯) + 1) β β) |
73 | 54, 72 | syl 17 |
. . . . . . . . . . . 12
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β ((absβπ₯) + 1) β β) |
74 | 73, 59 | remulcld 11190 |
. . . . . . . . . . 11
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (((absβπ₯) + 1) Β· π) β β) |
75 | 1, 33, 15 | sylancr 588 |
. . . . . . . . . . . . 13
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β 0 β€ (πβπ¦)) |
76 | 32, 36 | abssubd 15344 |
. . . . . . . . . . . . . 14
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (absβ(π₯ β π§)) = (absβ(π§ β π₯))) |
77 | 36, 32 | subcld 11517 |
. . . . . . . . . . . . . . . 16
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (π§ β π₯) β β) |
78 | 77 | abscld 15327 |
. . . . . . . . . . . . . . 15
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (absβ(π§ β π₯)) β β) |
79 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . 19
β’ (abs
β β ) = (abs β β ) |
80 | 79 | cnmetdval 24150 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯ β β β§ π§ β β) β (π₯(abs β β )π§) = (absβ(π₯ β π§))) |
81 | 32, 36, 80 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (π₯(abs β β )π§) = (absβ(π₯ β π§))) |
82 | 81, 76 | eqtrd 2773 |
. . . . . . . . . . . . . . . 16
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (π₯(abs β β )π§) = (absβ(π§ β π₯))) |
83 | | simprrl 780 |
. . . . . . . . . . . . . . . 16
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (π₯(abs β β )π§) < π) |
84 | 82, 83 | eqbrtrrd 5130 |
. . . . . . . . . . . . . . 15
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (absβ(π§ β π₯)) < π) |
85 | 78, 59, 84 | ltled 11308 |
. . . . . . . . . . . . . 14
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (absβ(π§ β π₯)) β€ π) |
86 | 76, 85 | eqbrtrd 5128 |
. . . . . . . . . . . . 13
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (absβ(π₯ β π§)) β€ π) |
87 | 62, 59, 53, 75, 86 | lemul1ad 12099 |
. . . . . . . . . . . 12
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β ((absβ(π₯ β π§)) Β· (πβπ¦)) β€ (π Β· (πβπ¦))) |
88 | 58 | rpcnd 12964 |
. . . . . . . . . . . . 13
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β π β β) |
89 | 53 | recnd 11188 |
. . . . . . . . . . . . 13
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (πβπ¦) β β) |
90 | 88, 89 | mulcomd 11181 |
. . . . . . . . . . . 12
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (π Β· (πβπ¦)) = ((πβπ¦) Β· π)) |
91 | 87, 90 | breqtrd 5132 |
. . . . . . . . . . 11
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β ((absβ(π₯ β π§)) Β· (πβπ¦)) β€ ((πβπ¦) Β· π)) |
92 | 36 | absge0d 15335 |
. . . . . . . . . . . 12
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β 0 β€ (absβπ§)) |
93 | 2, 9 | nvge0 29657 |
. . . . . . . . . . . . 13
β’ ((π β NrmCVec β§ (π¦( βπ£
βπ)π€) β π) β 0 β€ (πβ(π¦( βπ£ βπ)π€))) |
94 | 1, 67, 93 | sylancr 588 |
. . . . . . . . . . . 12
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β 0 β€ (πβ(π¦( βπ£ βπ)π€))) |
95 | 54, 78 | readdcld 11189 |
. . . . . . . . . . . . 13
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β ((absβπ₯) + (absβ(π§ β π₯))) β β) |
96 | 32, 36 | pncan3d 11520 |
. . . . . . . . . . . . . . 15
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (π₯ + (π§ β π₯)) = π§) |
97 | 96 | fveq2d 6847 |
. . . . . . . . . . . . . 14
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (absβ(π₯ + (π§ β π₯))) = (absβπ§)) |
98 | 32, 77 | abstrid 15347 |
. . . . . . . . . . . . . 14
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (absβ(π₯ + (π§ β π₯))) β€ ((absβπ₯) + (absβ(π§ β π₯)))) |
99 | 97, 98 | eqbrtrrd 5130 |
. . . . . . . . . . . . 13
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (absβπ§) β€ ((absβπ₯) + (absβ(π§ β π₯)))) |
100 | | 1red 11161 |
. . . . . . . . . . . . . 14
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β 1 β
β) |
101 | | 1re 11160 |
. . . . . . . . . . . . . . . . . . 19
β’ 1 β
β |
102 | 22 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β ((((πβπ¦) + (absβπ₯)) + 1) / π) β
β+) |
103 | | ltaddrp 12957 |
. . . . . . . . . . . . . . . . . . 19
β’ ((1
β β β§ ((((πβπ¦) + (absβπ₯)) + 1) / π) β β+) β 1 <
(1 + ((((πβπ¦) + (absβπ₯)) + 1) / π))) |
104 | 101, 102,
103 | sylancr 588 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β 1 < (1 + ((((πβπ¦) + (absβπ₯)) + 1) / π))) |
105 | 24 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (1 + ((((πβπ¦) + (absβπ₯)) + 1) / π)) β
β+) |
106 | 105 | recgt1d 12976 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (1 < (1 + ((((πβπ¦) + (absβπ₯)) + 1) / π)) β (1 / (1 + ((((πβπ¦) + (absβπ₯)) + 1) / π))) < 1)) |
107 | 104, 106 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (1 / (1 + ((((πβπ¦) + (absβπ₯)) + 1) / π))) < 1) |
108 | 6, 107 | eqbrtrid 5141 |
. . . . . . . . . . . . . . . 16
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β π < 1) |
109 | 59, 100, 108 | ltled 11308 |
. . . . . . . . . . . . . . 15
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β π β€ 1) |
110 | 78, 59, 100, 85, 109 | letrd 11317 |
. . . . . . . . . . . . . 14
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (absβ(π§ β π₯)) β€ 1) |
111 | 78, 100, 54, 110 | leadd2dd 11775 |
. . . . . . . . . . . . 13
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β ((absβπ₯) + (absβ(π§ β π₯))) β€ ((absβπ₯) + 1)) |
112 | 64, 95, 73, 99, 111 | letrd 11317 |
. . . . . . . . . . . 12
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (absβπ§) β€ ((absβπ₯) + 1)) |
113 | 2, 65, 9, 27 | imsdval 29670 |
. . . . . . . . . . . . . . 15
β’ ((π β NrmCVec β§ π¦ β π β§ π€ β π) β (π¦πΆπ€) = (πβ(π¦( βπ£ βπ)π€))) |
114 | 31, 33, 37, 113 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (π¦πΆπ€) = (πβ(π¦( βπ£ βπ)π€))) |
115 | | simprrr 781 |
. . . . . . . . . . . . . 14
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (π¦πΆπ€) < π) |
116 | 114, 115 | eqbrtrrd 5130 |
. . . . . . . . . . . . 13
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (πβ(π¦( βπ£ βπ)π€)) < π) |
117 | 69, 59, 116 | ltled 11308 |
. . . . . . . . . . . 12
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (πβ(π¦( βπ£ βπ)π€)) β€ π) |
118 | 64, 73, 69, 59, 92, 94, 112, 117 | lemul12ad 12102 |
. . . . . . . . . . 11
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β ((absβπ§) Β· (πβ(π¦( βπ£ βπ)π€))) β€ (((absβπ₯) + 1) Β· π)) |
119 | 63, 70, 71, 74, 91, 118 | le2addd 11779 |
. . . . . . . . . 10
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (((absβ(π₯ β π§)) Β· (πβπ¦)) + ((absβπ§) Β· (πβ(π¦( βπ£ βπ)π€)))) β€ (((πβπ¦) Β· π) + (((absβπ₯) + 1) Β· π))) |
120 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’ (
+π£ βπ) = ( +π£ βπ) |
121 | 2, 120, 3, 9, 27 | imsdval2 29671 |
. . . . . . . . . . . . 13
β’ ((π β NrmCVec β§ (π₯ππ¦) β π β§ (π§ππ¦) β π) β ((π₯ππ¦)πΆ(π§ππ¦)) = (πβ((π₯ππ¦)( +π£ βπ)(-1π(π§ππ¦))))) |
122 | 31, 35, 43, 121 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β ((π₯ππ¦)πΆ(π§ππ¦)) = (πβ((π₯ππ¦)( +π£ βπ)(-1π(π§ππ¦))))) |
123 | | neg1cn 12272 |
. . . . . . . . . . . . . . . 16
β’ -1 β
β |
124 | | mulcl 11140 |
. . . . . . . . . . . . . . . 16
β’ ((-1
β β β§ π§
β β) β (-1 Β· π§) β β) |
125 | 123, 36, 124 | sylancr 588 |
. . . . . . . . . . . . . . 15
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (-1 Β· π§) β β) |
126 | 2, 120, 3 | nvdir 29615 |
. . . . . . . . . . . . . . 15
β’ ((π β NrmCVec β§ (π₯ β β β§ (-1
Β· π§) β β
β§ π¦ β π)) β ((π₯ + (-1 Β· π§))ππ¦) = ((π₯ππ¦)( +π£ βπ)((-1 Β· π§)ππ¦))) |
127 | 31, 32, 125, 33, 126 | syl13anc 1373 |
. . . . . . . . . . . . . 14
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β ((π₯ + (-1 Β· π§))ππ¦) = ((π₯ππ¦)( +π£ βπ)((-1 Β· π§)ππ¦))) |
128 | 36 | mulm1d 11612 |
. . . . . . . . . . . . . . . . 17
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (-1 Β· π§) = -π§) |
129 | 128 | oveq2d 7374 |
. . . . . . . . . . . . . . . 16
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (π₯ + (-1 Β· π§)) = (π₯ + -π§)) |
130 | 32, 36 | negsubd 11523 |
. . . . . . . . . . . . . . . 16
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (π₯ + -π§) = (π₯ β π§)) |
131 | 129, 130 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (π₯ + (-1 Β· π§)) = (π₯ β π§)) |
132 | 131 | oveq1d 7373 |
. . . . . . . . . . . . . 14
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β ((π₯ + (-1 Β· π§))ππ¦) = ((π₯ β π§)ππ¦)) |
133 | 123 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β -1 β
β) |
134 | 2, 3 | nvsass 29612 |
. . . . . . . . . . . . . . . 16
β’ ((π β NrmCVec β§ (-1 β
β β§ π§ β
β β§ π¦ β
π)) β ((-1 Β·
π§)ππ¦) = (-1π(π§ππ¦))) |
135 | 31, 133, 36, 33, 134 | syl13anc 1373 |
. . . . . . . . . . . . . . 15
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β ((-1 Β· π§)ππ¦) = (-1π(π§ππ¦))) |
136 | 135 | oveq2d 7374 |
. . . . . . . . . . . . . 14
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β ((π₯ππ¦)( +π£ βπ)((-1 Β· π§)ππ¦)) = ((π₯ππ¦)( +π£ βπ)(-1π(π§ππ¦)))) |
137 | 127, 132,
136 | 3eqtr3d 2781 |
. . . . . . . . . . . . 13
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β ((π₯ β π§)ππ¦) = ((π₯ππ¦)( +π£ βπ)(-1π(π§ππ¦)))) |
138 | 137 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (πβ((π₯ β π§)ππ¦)) = (πβ((π₯ππ¦)( +π£ βπ)(-1π(π§ππ¦))))) |
139 | 2, 3, 9 | nvs 29647 |
. . . . . . . . . . . . 13
β’ ((π β NrmCVec β§ (π₯ β π§) β β β§ π¦ β π) β (πβ((π₯ β π§)ππ¦)) = ((absβ(π₯ β π§)) Β· (πβπ¦))) |
140 | 31, 61, 33, 139 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (πβ((π₯ β π§)ππ¦)) = ((absβ(π₯ β π§)) Β· (πβπ¦))) |
141 | 122, 138,
140 | 3eqtr2d 2779 |
. . . . . . . . . . 11
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β ((π₯ππ¦)πΆ(π§ππ¦)) = ((absβ(π₯ β π§)) Β· (πβπ¦))) |
142 | 2, 65, 9, 27 | imsdval 29670 |
. . . . . . . . . . . . 13
β’ ((π β NrmCVec β§ (π§ππ¦) β π β§ (π§ππ€) β π) β ((π§ππ¦)πΆ(π§ππ€)) = (πβ((π§ππ¦)( βπ£ βπ)(π§ππ€)))) |
143 | 31, 43, 39, 142 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β ((π§ππ¦)πΆ(π§ππ€)) = (πβ((π§ππ¦)( βπ£ βπ)(π§ππ€)))) |
144 | 2, 65, 3 | nvmdi 29632 |
. . . . . . . . . . . . . 14
β’ ((π β NrmCVec β§ (π§ β β β§ π¦ β π β§ π€ β π)) β (π§π(π¦( βπ£ βπ)π€)) = ((π§ππ¦)( βπ£ βπ)(π§ππ€))) |
145 | 31, 36, 33, 37, 144 | syl13anc 1373 |
. . . . . . . . . . . . 13
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (π§π(π¦( βπ£ βπ)π€)) = ((π§ππ¦)( βπ£ βπ)(π§ππ€))) |
146 | 145 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (πβ(π§π(π¦( βπ£ βπ)π€))) = (πβ((π§ππ¦)( βπ£ βπ)(π§ππ€)))) |
147 | 2, 3, 9 | nvs 29647 |
. . . . . . . . . . . . 13
β’ ((π β NrmCVec β§ π§ β β β§ (π¦( βπ£
βπ)π€) β π) β (πβ(π§π(π¦( βπ£ βπ)π€))) = ((absβπ§) Β· (πβ(π¦( βπ£ βπ)π€)))) |
148 | 31, 36, 67, 147 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (πβ(π§π(π¦( βπ£ βπ)π€))) = ((absβπ§) Β· (πβ(π¦( βπ£ βπ)π€)))) |
149 | 143, 146,
148 | 3eqtr2d 2779 |
. . . . . . . . . . 11
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β ((π§ππ¦)πΆ(π§ππ€)) = ((absβπ§) Β· (πβ(π¦( βπ£ βπ)π€)))) |
150 | 141, 149 | oveq12d 7376 |
. . . . . . . . . 10
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (((π₯ππ¦)πΆ(π§ππ¦)) + ((π§ππ¦)πΆ(π§ππ€))) = (((absβ(π₯ β π§)) Β· (πβπ¦)) + ((absβπ§) Β· (πβ(π¦( βπ£ βπ)π€))))) |
151 | 54 | recnd 11188 |
. . . . . . . . . . . . 13
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (absβπ₯) β β) |
152 | | 1cnd 11155 |
. . . . . . . . . . . . 13
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β 1 β
β) |
153 | 89, 151, 152 | addassd 11182 |
. . . . . . . . . . . 12
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (((πβπ¦) + (absβπ₯)) + 1) = ((πβπ¦) + ((absβπ₯) + 1))) |
154 | 153 | oveq1d 7373 |
. . . . . . . . . . 11
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β ((((πβπ¦) + (absβπ₯)) + 1) Β· π) = (((πβπ¦) + ((absβπ₯) + 1)) Β· π)) |
155 | 73 | recnd 11188 |
. . . . . . . . . . . 12
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β ((absβπ₯) + 1) β β) |
156 | 89, 155, 88 | adddird 11185 |
. . . . . . . . . . 11
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (((πβπ¦) + ((absβπ₯) + 1)) Β· π) = (((πβπ¦) Β· π) + (((absβπ₯) + 1) Β· π))) |
157 | 154, 156 | eqtrd 2773 |
. . . . . . . . . 10
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β ((((πβπ¦) + (absβπ₯)) + 1) Β· π) = (((πβπ¦) Β· π) + (((absβπ₯) + 1) Β· π))) |
158 | 119, 150,
157 | 3brtr4d 5138 |
. . . . . . . . 9
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (((π₯ππ¦)πΆ(π§ππ¦)) + ((π§ππ¦)πΆ(π§ππ€))) β€ ((((πβπ¦) + (absβπ₯)) + 1) Β· π)) |
159 | 6 | oveq2i 7369 |
. . . . . . . . . . 11
β’ ((((πβπ¦) + (absβπ₯)) + 1) Β· π) = ((((πβπ¦) + (absβπ₯)) + 1) Β· (1 / (1 + ((((πβπ¦) + (absβπ₯)) + 1) / π)))) |
160 | 57 | recnd 11188 |
. . . . . . . . . . . 12
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (((πβπ¦) + (absβπ₯)) + 1) β β) |
161 | 105 | rpcnd 12964 |
. . . . . . . . . . . 12
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (1 + ((((πβπ¦) + (absβπ₯)) + 1) / π)) β β) |
162 | 105 | rpne0d 12967 |
. . . . . . . . . . . 12
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (1 + ((((πβπ¦) + (absβπ₯)) + 1) / π)) β 0) |
163 | 160, 161,
162 | divrecd 11939 |
. . . . . . . . . . 11
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β ((((πβπ¦) + (absβπ₯)) + 1) / (1 + ((((πβπ¦) + (absβπ₯)) + 1) / π))) = ((((πβπ¦) + (absβπ₯)) + 1) Β· (1 / (1 + ((((πβπ¦) + (absβπ₯)) + 1) / π))))) |
164 | 159, 163 | eqtr4id 2792 |
. . . . . . . . . 10
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β ((((πβπ¦) + (absβπ₯)) + 1) Β· π) = ((((πβπ¦) + (absβπ₯)) + 1) / (1 + ((((πβπ¦) + (absβπ₯)) + 1) / π)))) |
165 | | simplr 768 |
. . . . . . . . . . 11
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β π β β+) |
166 | 102 | rpred 12962 |
. . . . . . . . . . . . 13
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β ((((πβπ¦) + (absβπ₯)) + 1) / π) β β) |
167 | 166 | ltp1d 12090 |
. . . . . . . . . . . 12
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β ((((πβπ¦) + (absβπ₯)) + 1) / π) < (((((πβπ¦) + (absβπ₯)) + 1) / π) + 1)) |
168 | 102 | rpcnd 12964 |
. . . . . . . . . . . . 13
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β ((((πβπ¦) + (absβπ₯)) + 1) / π) β β) |
169 | 168, 152 | addcomd 11362 |
. . . . . . . . . . . 12
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (((((πβπ¦) + (absβπ₯)) + 1) / π) + 1) = (1 + ((((πβπ¦) + (absβπ₯)) + 1) / π))) |
170 | 167, 169 | breqtrd 5132 |
. . . . . . . . . . 11
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β ((((πβπ¦) + (absβπ₯)) + 1) / π) < (1 + ((((πβπ¦) + (absβπ₯)) + 1) / π))) |
171 | 57, 165, 105, 170 | ltdiv23d 13029 |
. . . . . . . . . 10
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β ((((πβπ¦) + (absβπ₯)) + 1) / (1 + ((((πβπ¦) + (absβπ₯)) + 1) / π))) < π) |
172 | 164, 171 | eqbrtrd 5128 |
. . . . . . . . 9
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β ((((πβπ¦) + (absβπ₯)) + 1) Β· π) < π) |
173 | 48, 60, 50, 158, 172 | lelttrd 11318 |
. . . . . . . 8
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β (((π₯ππ¦)πΆ(π§ππ¦)) + ((π§ππ¦)πΆ(π§ππ€))) < π) |
174 | 41, 48, 50, 52, 173 | lelttrd 11318 |
. . . . . . 7
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ ((π§ β β β§ π€ β π) β§ ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) β ((π₯ππ¦)πΆ(π§ππ€)) < π) |
175 | 174 | expr 458 |
. . . . . 6
β’ ((((π₯ β β β§ π¦ β π) β§ π β β+) β§ (π§ β β β§ π€ β π)) β (((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π) β ((π₯ππ¦)πΆ(π§ππ€)) < π)) |
176 | 175 | ralrimivva 3194 |
. . . . 5
β’ (((π₯ β β β§ π¦ β π) β§ π β β+) β
βπ§ β β
βπ€ β π (((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π) β ((π₯ππ¦)πΆ(π§ππ€)) < π)) |
177 | | breq2 5110 |
. . . . . . . . 9
β’ (π = π β ((π₯(abs β β )π§) < π β (π₯(abs β β )π§) < π)) |
178 | | breq2 5110 |
. . . . . . . . 9
β’ (π = π β ((π¦πΆπ€) < π β (π¦πΆπ€) < π)) |
179 | 177, 178 | anbi12d 632 |
. . . . . . . 8
β’ (π = π β (((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π ) β ((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π))) |
180 | 179 | imbi1d 342 |
. . . . . . 7
β’ (π = π β ((((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π ) β ((π₯ππ¦)πΆ(π§ππ€)) < π) β (((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π) β ((π₯ππ¦)πΆ(π§ππ€)) < π))) |
181 | 180 | 2ralbidv 3209 |
. . . . . 6
β’ (π = π β (βπ§ β β βπ€ β π (((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π ) β ((π₯ππ¦)πΆ(π§ππ€)) < π) β βπ§ β β βπ€ β π (((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π) β ((π₯ππ¦)πΆ(π§ππ€)) < π))) |
182 | 181 | rspcev 3580 |
. . . . 5
β’ ((π β β+
β§ βπ§ β
β βπ€ β
π (((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π) β ((π₯ππ¦)πΆ(π§ππ€)) < π)) β βπ β β+ βπ§ β β βπ€ β π (((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π ) β ((π₯ππ¦)πΆ(π§ππ€)) < π)) |
183 | 26, 176, 182 | syl2anc 585 |
. . . 4
β’ (((π₯ β β β§ π¦ β π) β§ π β β+) β
βπ β
β+ βπ§ β β βπ€ β π (((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π ) β ((π₯ππ¦)πΆ(π§ππ€)) < π)) |
184 | 183 | ralrimiva 3140 |
. . 3
β’ ((π₯ β β β§ π¦ β π) β βπ β β+ βπ β β+
βπ§ β β
βπ€ β π (((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π ) β ((π₯ππ¦)πΆ(π§ππ€)) < π)) |
185 | 184 | rgen2 3191 |
. 2
β’
βπ₯ β
β βπ¦ β
π βπ β β+
βπ β
β+ βπ§ β β βπ€ β π (((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π ) β ((π₯ππ¦)πΆ(π§ππ€)) < π) |
186 | | cnxmet 24152 |
. . 3
β’ (abs
β β ) β (βMetββ) |
187 | 2, 27 | imsxmet 29676 |
. . . 4
β’ (π β NrmCVec β πΆ β (βMetβπ)) |
188 | 1, 187 | ax-mp 5 |
. . 3
β’ πΆ β (βMetβπ) |
189 | | smcn.k |
. . . . 5
β’ πΎ =
(TopOpenββfld) |
190 | 189 | cnfldtopn 24161 |
. . . 4
β’ πΎ = (MetOpenβ(abs β
β )) |
191 | | smcn.j |
. . . 4
β’ π½ = (MetOpenβπΆ) |
192 | 190, 191,
191 | txmetcn 23920 |
. . 3
β’ (((abs
β β ) β (βMetββ) β§ πΆ β (βMetβπ) β§ πΆ β (βMetβπ)) β (π β ((πΎ Γt π½) Cn π½) β (π:(β Γ π)βΆπ β§ βπ₯ β β βπ¦ β π βπ β β+ βπ β β+
βπ§ β β
βπ€ β π (((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π ) β ((π₯ππ¦)πΆ(π§ππ€)) < π)))) |
193 | 186, 188,
188, 192 | mp3an 1462 |
. 2
β’ (π β ((πΎ Γt π½) Cn π½) β (π:(β Γ π)βΆπ β§ βπ₯ β β βπ¦ β π βπ β β+ βπ β β+
βπ§ β β
βπ€ β π (((π₯(abs β β )π§) < π β§ (π¦πΆπ€) < π ) β ((π₯ππ¦)πΆ(π§ππ€)) < π))) |
194 | 5, 185, 193 | mpbir2an 710 |
1
β’ π β ((πΎ Γt π½) Cn π½) |