Step | Hyp | Ref
| Expression |
1 | | 0re 11164 |
. . . 4
โข 0 โ
โ |
2 | 1 | ne0ii 4302 |
. . 3
โข โ
โ โ
|
3 | | ral0 4475 |
. . . . 5
โข
โ๐ฅ โ
โ
โ๐ฆ โ
(๐ด[,]๐ต)(absโ((๐นโ๐ฆ) โ (๐นโ๐ฅ))) โค (๐ ยท (absโ(๐ฆ โ ๐ฅ))) |
4 | | c1lip1.a |
. . . . . . . . 9
โข (๐ โ ๐ด โ โ) |
5 | 4 | rexrd 11212 |
. . . . . . . 8
โข (๐ โ ๐ด โ
โ*) |
6 | | c1lip1.b |
. . . . . . . . 9
โข (๐ โ ๐ต โ โ) |
7 | 6 | rexrd 11212 |
. . . . . . . 8
โข (๐ โ ๐ต โ
โ*) |
8 | | icc0 13319 |
. . . . . . . 8
โข ((๐ด โ โ*
โง ๐ต โ
โ*) โ ((๐ด[,]๐ต) = โ
โ ๐ต < ๐ด)) |
9 | 5, 7, 8 | syl2anc 585 |
. . . . . . 7
โข (๐ โ ((๐ด[,]๐ต) = โ
โ ๐ต < ๐ด)) |
10 | 9 | biimpar 479 |
. . . . . 6
โข ((๐ โง ๐ต < ๐ด) โ (๐ด[,]๐ต) = โ
) |
11 | 10 | raleqdv 3316 |
. . . . 5
โข ((๐ โง ๐ต < ๐ด) โ (โ๐ฅ โ (๐ด[,]๐ต)โ๐ฆ โ (๐ด[,]๐ต)(absโ((๐นโ๐ฆ) โ (๐นโ๐ฅ))) โค (๐ ยท (absโ(๐ฆ โ ๐ฅ))) โ โ๐ฅ โ โ
โ๐ฆ โ (๐ด[,]๐ต)(absโ((๐นโ๐ฆ) โ (๐นโ๐ฅ))) โค (๐ ยท (absโ(๐ฆ โ ๐ฅ))))) |
12 | 3, 11 | mpbiri 258 |
. . . 4
โข ((๐ โง ๐ต < ๐ด) โ โ๐ฅ โ (๐ด[,]๐ต)โ๐ฆ โ (๐ด[,]๐ต)(absโ((๐นโ๐ฆ) โ (๐นโ๐ฅ))) โค (๐ ยท (absโ(๐ฆ โ ๐ฅ)))) |
13 | 12 | ralrimivw 3148 |
. . 3
โข ((๐ โง ๐ต < ๐ด) โ โ๐ โ โ โ๐ฅ โ (๐ด[,]๐ต)โ๐ฆ โ (๐ด[,]๐ต)(absโ((๐นโ๐ฆ) โ (๐นโ๐ฅ))) โค (๐ ยท (absโ(๐ฆ โ ๐ฅ)))) |
14 | | r19.2z 4457 |
. . 3
โข ((โ
โ โ
โง โ๐ โ โ โ๐ฅ โ (๐ด[,]๐ต)โ๐ฆ โ (๐ด[,]๐ต)(absโ((๐นโ๐ฆ) โ (๐นโ๐ฅ))) โค (๐ ยท (absโ(๐ฆ โ ๐ฅ)))) โ โ๐ โ โ โ๐ฅ โ (๐ด[,]๐ต)โ๐ฆ โ (๐ด[,]๐ต)(absโ((๐นโ๐ฆ) โ (๐นโ๐ฅ))) โค (๐ ยท (absโ(๐ฆ โ ๐ฅ)))) |
15 | 2, 13, 14 | sylancr 588 |
. 2
โข ((๐ โง ๐ต < ๐ด) โ โ๐ โ โ โ๐ฅ โ (๐ด[,]๐ต)โ๐ฆ โ (๐ด[,]๐ต)(absโ((๐นโ๐ฆ) โ (๐นโ๐ฅ))) โค (๐ ยท (absโ(๐ฆ โ ๐ฅ)))) |
16 | 4 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ด โค ๐ต) โ ๐ด โ โ) |
17 | 6 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ด โค ๐ต) โ ๐ต โ โ) |
18 | | simpr 486 |
. . . . 5
โข ((๐ โง ๐ด โค ๐ต) โ ๐ด โค ๐ต) |
19 | | c1lip1.f |
. . . . . 6
โข (๐ โ ๐น โ (โ โpm
โ)) |
20 | 19 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ด โค ๐ต) โ ๐น โ (โ โpm
โ)) |
21 | | c1lip1.dv |
. . . . . 6
โข (๐ โ ((โ D ๐น) โพ (๐ด[,]๐ต)) โ ((๐ด[,]๐ต)โcnโโ)) |
22 | 21 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ด โค ๐ต) โ ((โ D ๐น) โพ (๐ด[,]๐ต)) โ ((๐ด[,]๐ต)โcnโโ)) |
23 | | c1lip1.cn |
. . . . . 6
โข (๐ โ (๐น โพ (๐ด[,]๐ต)) โ ((๐ด[,]๐ต)โcnโโ)) |
24 | 23 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ด โค ๐ต) โ (๐น โพ (๐ด[,]๐ต)) โ ((๐ด[,]๐ต)โcnโโ)) |
25 | | eqid 2737 |
. . . . 5
โข sup((abs
โ ((โ D ๐น)
โ (๐ด[,]๐ต))), โ, < ) = sup((abs
โ ((โ D ๐น)
โ (๐ด[,]๐ต))), โ, <
) |
26 | 16, 17, 18, 20, 22, 24, 25 | c1liplem1 25376 |
. . . 4
โข ((๐ โง ๐ด โค ๐ต) โ (sup((abs โ ((โ D ๐น) โ (๐ด[,]๐ต))), โ, < ) โ โ โง
โ๐ โ (๐ด[,]๐ต)โ๐ โ (๐ด[,]๐ต)(๐ < ๐ โ (absโ((๐นโ๐) โ (๐นโ๐))) โค (sup((abs โ ((โ D ๐น) โ (๐ด[,]๐ต))), โ, < ) ยท
(absโ(๐ โ ๐)))))) |
27 | | oveq1 7369 |
. . . . . . . 8
โข (๐ = sup((abs โ ((โ D
๐น) โ (๐ด[,]๐ต))), โ, < ) โ (๐ ยท (absโ(๐ โ ๐))) = (sup((abs โ ((โ D ๐น) โ (๐ด[,]๐ต))), โ, < ) ยท
(absโ(๐ โ ๐)))) |
28 | 27 | breq2d 5122 |
. . . . . . 7
โข (๐ = sup((abs โ ((โ D
๐น) โ (๐ด[,]๐ต))), โ, < ) โ
((absโ((๐นโ๐) โ (๐นโ๐))) โค (๐ ยท (absโ(๐ โ ๐))) โ (absโ((๐นโ๐) โ (๐นโ๐))) โค (sup((abs โ ((โ D ๐น) โ (๐ด[,]๐ต))), โ, < ) ยท
(absโ(๐ โ ๐))))) |
29 | 28 | imbi2d 341 |
. . . . . 6
โข (๐ = sup((abs โ ((โ D
๐น) โ (๐ด[,]๐ต))), โ, < ) โ ((๐ < ๐ โ (absโ((๐นโ๐) โ (๐นโ๐))) โค (๐ ยท (absโ(๐ โ ๐)))) โ (๐ < ๐ โ (absโ((๐นโ๐) โ (๐นโ๐))) โค (sup((abs โ ((โ D ๐น) โ (๐ด[,]๐ต))), โ, < ) ยท
(absโ(๐ โ ๐)))))) |
30 | 29 | 2ralbidv 3213 |
. . . . 5
โข (๐ = sup((abs โ ((โ D
๐น) โ (๐ด[,]๐ต))), โ, < ) โ (โ๐ โ (๐ด[,]๐ต)โ๐ โ (๐ด[,]๐ต)(๐ < ๐ โ (absโ((๐นโ๐) โ (๐นโ๐))) โค (๐ ยท (absโ(๐ โ ๐)))) โ โ๐ โ (๐ด[,]๐ต)โ๐ โ (๐ด[,]๐ต)(๐ < ๐ โ (absโ((๐นโ๐) โ (๐นโ๐))) โค (sup((abs โ ((โ D ๐น) โ (๐ด[,]๐ต))), โ, < ) ยท
(absโ(๐ โ ๐)))))) |
31 | 30 | rspcev 3584 |
. . . 4
โข
((sup((abs โ ((โ D ๐น) โ (๐ด[,]๐ต))), โ, < ) โ โ โง
โ๐ โ (๐ด[,]๐ต)โ๐ โ (๐ด[,]๐ต)(๐ < ๐ โ (absโ((๐นโ๐) โ (๐นโ๐))) โค (sup((abs โ ((โ D ๐น) โ (๐ด[,]๐ต))), โ, < ) ยท
(absโ(๐ โ ๐))))) โ โ๐ โ โ โ๐ โ (๐ด[,]๐ต)โ๐ โ (๐ด[,]๐ต)(๐ < ๐ โ (absโ((๐นโ๐) โ (๐นโ๐))) โค (๐ ยท (absโ(๐ โ ๐))))) |
32 | 26, 31 | syl 17 |
. . 3
โข ((๐ โง ๐ด โค ๐ต) โ โ๐ โ โ โ๐ โ (๐ด[,]๐ต)โ๐ โ (๐ด[,]๐ต)(๐ < ๐ โ (absโ((๐นโ๐) โ (๐นโ๐))) โค (๐ ยท (absโ(๐ โ ๐))))) |
33 | | breq1 5113 |
. . . . . . . . . 10
โข (๐ = ๐ฅ โ (๐ < ๐ โ ๐ฅ < ๐)) |
34 | | fveq2 6847 |
. . . . . . . . . . . . 13
โข (๐ = ๐ฅ โ (๐นโ๐) = (๐นโ๐ฅ)) |
35 | 34 | oveq2d 7378 |
. . . . . . . . . . . 12
โข (๐ = ๐ฅ โ ((๐นโ๐) โ (๐นโ๐)) = ((๐นโ๐) โ (๐นโ๐ฅ))) |
36 | 35 | fveq2d 6851 |
. . . . . . . . . . 11
โข (๐ = ๐ฅ โ (absโ((๐นโ๐) โ (๐นโ๐))) = (absโ((๐นโ๐) โ (๐นโ๐ฅ)))) |
37 | | oveq2 7370 |
. . . . . . . . . . . . 13
โข (๐ = ๐ฅ โ (๐ โ ๐) = (๐ โ ๐ฅ)) |
38 | 37 | fveq2d 6851 |
. . . . . . . . . . . 12
โข (๐ = ๐ฅ โ (absโ(๐ โ ๐)) = (absโ(๐ โ ๐ฅ))) |
39 | 38 | oveq2d 7378 |
. . . . . . . . . . 11
โข (๐ = ๐ฅ โ (๐ ยท (absโ(๐ โ ๐))) = (๐ ยท (absโ(๐ โ ๐ฅ)))) |
40 | 36, 39 | breq12d 5123 |
. . . . . . . . . 10
โข (๐ = ๐ฅ โ ((absโ((๐นโ๐) โ (๐นโ๐))) โค (๐ ยท (absโ(๐ โ ๐))) โ (absโ((๐นโ๐) โ (๐นโ๐ฅ))) โค (๐ ยท (absโ(๐ โ ๐ฅ))))) |
41 | 33, 40 | imbi12d 345 |
. . . . . . . . 9
โข (๐ = ๐ฅ โ ((๐ < ๐ โ (absโ((๐นโ๐) โ (๐นโ๐))) โค (๐ ยท (absโ(๐ โ ๐)))) โ (๐ฅ < ๐ โ (absโ((๐นโ๐) โ (๐นโ๐ฅ))) โค (๐ ยท (absโ(๐ โ ๐ฅ)))))) |
42 | | breq2 5114 |
. . . . . . . . . 10
โข (๐ = ๐ฆ โ (๐ฅ < ๐ โ ๐ฅ < ๐ฆ)) |
43 | | fveq2 6847 |
. . . . . . . . . . . 12
โข (๐ = ๐ฆ โ (๐นโ๐) = (๐นโ๐ฆ)) |
44 | 43 | fvoveq1d 7384 |
. . . . . . . . . . 11
โข (๐ = ๐ฆ โ (absโ((๐นโ๐) โ (๐นโ๐ฅ))) = (absโ((๐นโ๐ฆ) โ (๐นโ๐ฅ)))) |
45 | | fvoveq1 7385 |
. . . . . . . . . . . 12
โข (๐ = ๐ฆ โ (absโ(๐ โ ๐ฅ)) = (absโ(๐ฆ โ ๐ฅ))) |
46 | 45 | oveq2d 7378 |
. . . . . . . . . . 11
โข (๐ = ๐ฆ โ (๐ ยท (absโ(๐ โ ๐ฅ))) = (๐ ยท (absโ(๐ฆ โ ๐ฅ)))) |
47 | 44, 46 | breq12d 5123 |
. . . . . . . . . 10
โข (๐ = ๐ฆ โ ((absโ((๐นโ๐) โ (๐นโ๐ฅ))) โค (๐ ยท (absโ(๐ โ ๐ฅ))) โ (absโ((๐นโ๐ฆ) โ (๐นโ๐ฅ))) โค (๐ ยท (absโ(๐ฆ โ ๐ฅ))))) |
48 | 42, 47 | imbi12d 345 |
. . . . . . . . 9
โข (๐ = ๐ฆ โ ((๐ฅ < ๐ โ (absโ((๐นโ๐) โ (๐นโ๐ฅ))) โค (๐ ยท (absโ(๐ โ ๐ฅ)))) โ (๐ฅ < ๐ฆ โ (absโ((๐นโ๐ฆ) โ (๐นโ๐ฅ))) โค (๐ ยท (absโ(๐ฆ โ ๐ฅ)))))) |
49 | 41, 48 | rspc2v 3593 |
. . . . . . . 8
โข ((๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต)) โ (โ๐ โ (๐ด[,]๐ต)โ๐ โ (๐ด[,]๐ต)(๐ < ๐ โ (absโ((๐นโ๐) โ (๐นโ๐))) โค (๐ ยท (absโ(๐ โ ๐)))) โ (๐ฅ < ๐ฆ โ (absโ((๐นโ๐ฆ) โ (๐นโ๐ฅ))) โค (๐ ยท (absโ(๐ฆ โ ๐ฅ)))))) |
50 | 49 | ad2antlr 726 |
. . . . . . 7
โข
(((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โง ๐ฅ < ๐ฆ) โ (โ๐ โ (๐ด[,]๐ต)โ๐ โ (๐ด[,]๐ต)(๐ < ๐ โ (absโ((๐นโ๐) โ (๐นโ๐))) โค (๐ ยท (absโ(๐ โ ๐)))) โ (๐ฅ < ๐ฆ โ (absโ((๐นโ๐ฆ) โ (๐นโ๐ฅ))) โค (๐ ยท (absโ(๐ฆ โ ๐ฅ)))))) |
51 | | pm2.27 42 |
. . . . . . . 8
โข (๐ฅ < ๐ฆ โ ((๐ฅ < ๐ฆ โ (absโ((๐นโ๐ฆ) โ (๐นโ๐ฅ))) โค (๐ ยท (absโ(๐ฆ โ ๐ฅ)))) โ (absโ((๐นโ๐ฆ) โ (๐นโ๐ฅ))) โค (๐ ยท (absโ(๐ฆ โ ๐ฅ))))) |
52 | 51 | adantl 483 |
. . . . . . 7
โข
(((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โง ๐ฅ < ๐ฆ) โ ((๐ฅ < ๐ฆ โ (absโ((๐นโ๐ฆ) โ (๐นโ๐ฅ))) โค (๐ ยท (absโ(๐ฆ โ ๐ฅ)))) โ (absโ((๐นโ๐ฆ) โ (๐นโ๐ฅ))) โค (๐ ยท (absโ(๐ฆ โ ๐ฅ))))) |
53 | 50, 52 | syld 47 |
. . . . . 6
โข
(((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โง ๐ฅ < ๐ฆ) โ (โ๐ โ (๐ด[,]๐ต)โ๐ โ (๐ด[,]๐ต)(๐ < ๐ โ (absโ((๐นโ๐) โ (๐นโ๐))) โค (๐ ยท (absโ(๐ โ ๐)))) โ (absโ((๐นโ๐ฆ) โ (๐นโ๐ฅ))) โค (๐ ยท (absโ(๐ฆ โ ๐ฅ))))) |
54 | | 0le0 12261 |
. . . . . . . . . 10
โข 0 โค
0 |
55 | | fvres 6866 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ โ (๐ด[,]๐ต) โ ((๐น โพ (๐ด[,]๐ต))โ๐ฅ) = (๐นโ๐ฅ)) |
56 | 55 | ad2antrl 727 |
. . . . . . . . . . . . . . 15
โข ((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โ ((๐น โพ (๐ด[,]๐ต))โ๐ฅ) = (๐นโ๐ฅ)) |
57 | | cncff 24272 |
. . . . . . . . . . . . . . . . . 18
โข ((๐น โพ (๐ด[,]๐ต)) โ ((๐ด[,]๐ต)โcnโโ) โ (๐น โพ (๐ด[,]๐ต)):(๐ด[,]๐ต)โถโ) |
58 | 23, 57 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (๐น โพ (๐ด[,]๐ต)):(๐ด[,]๐ต)โถโ) |
59 | 58 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โ (๐น โพ (๐ด[,]๐ต)):(๐ด[,]๐ต)โถโ) |
60 | | simpl 484 |
. . . . . . . . . . . . . . . 16
โข ((๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต)) โ ๐ฅ โ (๐ด[,]๐ต)) |
61 | | ffvelcdm 7037 |
. . . . . . . . . . . . . . . 16
โข (((๐น โพ (๐ด[,]๐ต)):(๐ด[,]๐ต)โถโ โง ๐ฅ โ (๐ด[,]๐ต)) โ ((๐น โพ (๐ด[,]๐ต))โ๐ฅ) โ โ) |
62 | 59, 60, 61 | syl2an 597 |
. . . . . . . . . . . . . . 15
โข ((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โ ((๐น โพ (๐ด[,]๐ต))โ๐ฅ) โ โ) |
63 | 56, 62 | eqeltrrd 2839 |
. . . . . . . . . . . . . 14
โข ((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โ (๐นโ๐ฅ) โ โ) |
64 | 63 | recnd 11190 |
. . . . . . . . . . . . 13
โข ((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โ (๐นโ๐ฅ) โ โ) |
65 | 64 | subidd 11507 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โ ((๐นโ๐ฅ) โ (๐นโ๐ฅ)) = 0) |
66 | 65 | abs00bd 15183 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โ (absโ((๐นโ๐ฅ) โ (๐นโ๐ฅ))) = 0) |
67 | | iccssre 13353 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด[,]๐ต) โ โ) |
68 | 4, 6, 67 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (๐ด[,]๐ต) โ โ) |
69 | 68 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โ (๐ด[,]๐ต) โ โ) |
70 | | simprl 770 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โ ๐ฅ โ (๐ด[,]๐ต)) |
71 | 69, 70 | sseldd 3950 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โ ๐ฅ โ โ) |
72 | 71 | recnd 11190 |
. . . . . . . . . . . . . . 15
โข ((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โ ๐ฅ โ โ) |
73 | 72 | subidd 11507 |
. . . . . . . . . . . . . 14
โข ((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โ (๐ฅ โ ๐ฅ) = 0) |
74 | 73 | abs00bd 15183 |
. . . . . . . . . . . . 13
โข ((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โ (absโ(๐ฅ โ ๐ฅ)) = 0) |
75 | 74 | oveq2d 7378 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โ (๐ ยท (absโ(๐ฅ โ ๐ฅ))) = (๐ ยท 0)) |
76 | | simplr 768 |
. . . . . . . . . . . . . 14
โข ((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โ ๐ โ โ) |
77 | 76 | recnd 11190 |
. . . . . . . . . . . . 13
โข ((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โ ๐ โ โ) |
78 | 77 | mul01d 11361 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โ (๐ ยท 0) = 0) |
79 | 75, 78 | eqtrd 2777 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โ (๐ ยท (absโ(๐ฅ โ ๐ฅ))) = 0) |
80 | 66, 79 | breq12d 5123 |
. . . . . . . . . 10
โข ((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โ ((absโ((๐นโ๐ฅ) โ (๐นโ๐ฅ))) โค (๐ ยท (absโ(๐ฅ โ ๐ฅ))) โ 0 โค 0)) |
81 | 54, 80 | mpbiri 258 |
. . . . . . . . 9
โข ((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โ (absโ((๐นโ๐ฅ) โ (๐นโ๐ฅ))) โค (๐ ยท (absโ(๐ฅ โ ๐ฅ)))) |
82 | | fveq2 6847 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ฆ โ (๐นโ๐ฅ) = (๐นโ๐ฆ)) |
83 | 82 | fvoveq1d 7384 |
. . . . . . . . . 10
โข (๐ฅ = ๐ฆ โ (absโ((๐นโ๐ฅ) โ (๐นโ๐ฅ))) = (absโ((๐นโ๐ฆ) โ (๐นโ๐ฅ)))) |
84 | | fvoveq1 7385 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ฆ โ (absโ(๐ฅ โ ๐ฅ)) = (absโ(๐ฆ โ ๐ฅ))) |
85 | 84 | oveq2d 7378 |
. . . . . . . . . 10
โข (๐ฅ = ๐ฆ โ (๐ ยท (absโ(๐ฅ โ ๐ฅ))) = (๐ ยท (absโ(๐ฆ โ ๐ฅ)))) |
86 | 83, 85 | breq12d 5123 |
. . . . . . . . 9
โข (๐ฅ = ๐ฆ โ ((absโ((๐นโ๐ฅ) โ (๐นโ๐ฅ))) โค (๐ ยท (absโ(๐ฅ โ ๐ฅ))) โ (absโ((๐นโ๐ฆ) โ (๐นโ๐ฅ))) โค (๐ ยท (absโ(๐ฆ โ ๐ฅ))))) |
87 | 81, 86 | syl5ibcom 244 |
. . . . . . . 8
โข ((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โ (๐ฅ = ๐ฆ โ (absโ((๐นโ๐ฆ) โ (๐นโ๐ฅ))) โค (๐ ยท (absโ(๐ฆ โ ๐ฅ))))) |
88 | 87 | imp 408 |
. . . . . . 7
โข
(((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โง ๐ฅ = ๐ฆ) โ (absโ((๐นโ๐ฆ) โ (๐นโ๐ฅ))) โค (๐ ยท (absโ(๐ฆ โ ๐ฅ)))) |
89 | 88 | a1d 25 |
. . . . . 6
โข
(((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โง ๐ฅ = ๐ฆ) โ (โ๐ โ (๐ด[,]๐ต)โ๐ โ (๐ด[,]๐ต)(๐ < ๐ โ (absโ((๐นโ๐) โ (๐นโ๐))) โค (๐ ยท (absโ(๐ โ ๐)))) โ (absโ((๐นโ๐ฆ) โ (๐นโ๐ฅ))) โค (๐ ยท (absโ(๐ฆ โ ๐ฅ))))) |
90 | | breq1 5113 |
. . . . . . . . . . 11
โข (๐ = ๐ฆ โ (๐ < ๐ โ ๐ฆ < ๐)) |
91 | | fveq2 6847 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ฆ โ (๐นโ๐) = (๐นโ๐ฆ)) |
92 | 91 | oveq2d 7378 |
. . . . . . . . . . . . 13
โข (๐ = ๐ฆ โ ((๐นโ๐) โ (๐นโ๐)) = ((๐นโ๐) โ (๐นโ๐ฆ))) |
93 | 92 | fveq2d 6851 |
. . . . . . . . . . . 12
โข (๐ = ๐ฆ โ (absโ((๐นโ๐) โ (๐นโ๐))) = (absโ((๐นโ๐) โ (๐นโ๐ฆ)))) |
94 | | oveq2 7370 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ฆ โ (๐ โ ๐) = (๐ โ ๐ฆ)) |
95 | 94 | fveq2d 6851 |
. . . . . . . . . . . . 13
โข (๐ = ๐ฆ โ (absโ(๐ โ ๐)) = (absโ(๐ โ ๐ฆ))) |
96 | 95 | oveq2d 7378 |
. . . . . . . . . . . 12
โข (๐ = ๐ฆ โ (๐ ยท (absโ(๐ โ ๐))) = (๐ ยท (absโ(๐ โ ๐ฆ)))) |
97 | 93, 96 | breq12d 5123 |
. . . . . . . . . . 11
โข (๐ = ๐ฆ โ ((absโ((๐นโ๐) โ (๐นโ๐))) โค (๐ ยท (absโ(๐ โ ๐))) โ (absโ((๐นโ๐) โ (๐นโ๐ฆ))) โค (๐ ยท (absโ(๐ โ ๐ฆ))))) |
98 | 90, 97 | imbi12d 345 |
. . . . . . . . . 10
โข (๐ = ๐ฆ โ ((๐ < ๐ โ (absโ((๐นโ๐) โ (๐นโ๐))) โค (๐ ยท (absโ(๐ โ ๐)))) โ (๐ฆ < ๐ โ (absโ((๐นโ๐) โ (๐นโ๐ฆ))) โค (๐ ยท (absโ(๐ โ ๐ฆ)))))) |
99 | | breq2 5114 |
. . . . . . . . . . 11
โข (๐ = ๐ฅ โ (๐ฆ < ๐ โ ๐ฆ < ๐ฅ)) |
100 | | fveq2 6847 |
. . . . . . . . . . . . 13
โข (๐ = ๐ฅ โ (๐นโ๐) = (๐นโ๐ฅ)) |
101 | 100 | fvoveq1d 7384 |
. . . . . . . . . . . 12
โข (๐ = ๐ฅ โ (absโ((๐นโ๐) โ (๐นโ๐ฆ))) = (absโ((๐นโ๐ฅ) โ (๐นโ๐ฆ)))) |
102 | | fvoveq1 7385 |
. . . . . . . . . . . . 13
โข (๐ = ๐ฅ โ (absโ(๐ โ ๐ฆ)) = (absโ(๐ฅ โ ๐ฆ))) |
103 | 102 | oveq2d 7378 |
. . . . . . . . . . . 12
โข (๐ = ๐ฅ โ (๐ ยท (absโ(๐ โ ๐ฆ))) = (๐ ยท (absโ(๐ฅ โ ๐ฆ)))) |
104 | 101, 103 | breq12d 5123 |
. . . . . . . . . . 11
โข (๐ = ๐ฅ โ ((absโ((๐นโ๐) โ (๐นโ๐ฆ))) โค (๐ ยท (absโ(๐ โ ๐ฆ))) โ (absโ((๐นโ๐ฅ) โ (๐นโ๐ฆ))) โค (๐ ยท (absโ(๐ฅ โ ๐ฆ))))) |
105 | 99, 104 | imbi12d 345 |
. . . . . . . . . 10
โข (๐ = ๐ฅ โ ((๐ฆ < ๐ โ (absโ((๐นโ๐) โ (๐นโ๐ฆ))) โค (๐ ยท (absโ(๐ โ ๐ฆ)))) โ (๐ฆ < ๐ฅ โ (absโ((๐นโ๐ฅ) โ (๐นโ๐ฆ))) โค (๐ ยท (absโ(๐ฅ โ ๐ฆ)))))) |
106 | 98, 105 | rspc2v 3593 |
. . . . . . . . 9
โข ((๐ฆ โ (๐ด[,]๐ต) โง ๐ฅ โ (๐ด[,]๐ต)) โ (โ๐ โ (๐ด[,]๐ต)โ๐ โ (๐ด[,]๐ต)(๐ < ๐ โ (absโ((๐นโ๐) โ (๐นโ๐))) โค (๐ ยท (absโ(๐ โ ๐)))) โ (๐ฆ < ๐ฅ โ (absโ((๐นโ๐ฅ) โ (๐นโ๐ฆ))) โค (๐ ยท (absโ(๐ฅ โ ๐ฆ)))))) |
107 | 106 | ancoms 460 |
. . . . . . . 8
โข ((๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต)) โ (โ๐ โ (๐ด[,]๐ต)โ๐ โ (๐ด[,]๐ต)(๐ < ๐ โ (absโ((๐นโ๐) โ (๐นโ๐))) โค (๐ ยท (absโ(๐ โ ๐)))) โ (๐ฆ < ๐ฅ โ (absโ((๐นโ๐ฅ) โ (๐นโ๐ฆ))) โค (๐ ยท (absโ(๐ฅ โ ๐ฆ)))))) |
108 | 107 | ad2antlr 726 |
. . . . . . 7
โข
(((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โง ๐ฆ < ๐ฅ) โ (โ๐ โ (๐ด[,]๐ต)โ๐ โ (๐ด[,]๐ต)(๐ < ๐ โ (absโ((๐นโ๐) โ (๐นโ๐))) โค (๐ ยท (absโ(๐ โ ๐)))) โ (๐ฆ < ๐ฅ โ (absโ((๐นโ๐ฅ) โ (๐นโ๐ฆ))) โค (๐ ยท (absโ(๐ฅ โ ๐ฆ)))))) |
109 | | simpr 486 |
. . . . . . . 8
โข
(((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โง ๐ฆ < ๐ฅ) โ ๐ฆ < ๐ฅ) |
110 | | fvres 6866 |
. . . . . . . . . . . . . . 15
โข (๐ฆ โ (๐ด[,]๐ต) โ ((๐น โพ (๐ด[,]๐ต))โ๐ฆ) = (๐นโ๐ฆ)) |
111 | 110 | ad2antll 728 |
. . . . . . . . . . . . . 14
โข ((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โ ((๐น โพ (๐ด[,]๐ต))โ๐ฆ) = (๐นโ๐ฆ)) |
112 | | simpr 486 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต)) โ ๐ฆ โ (๐ด[,]๐ต)) |
113 | | ffvelcdm 7037 |
. . . . . . . . . . . . . . 15
โข (((๐น โพ (๐ด[,]๐ต)):(๐ด[,]๐ต)โถโ โง ๐ฆ โ (๐ด[,]๐ต)) โ ((๐น โพ (๐ด[,]๐ต))โ๐ฆ) โ โ) |
114 | 59, 112, 113 | syl2an 597 |
. . . . . . . . . . . . . 14
โข ((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โ ((๐น โพ (๐ด[,]๐ต))โ๐ฆ) โ โ) |
115 | 111, 114 | eqeltrrd 2839 |
. . . . . . . . . . . . 13
โข ((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โ (๐นโ๐ฆ) โ โ) |
116 | 115 | recnd 11190 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โ (๐นโ๐ฆ) โ โ) |
117 | 64, 116 | abssubd 15345 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โ (absโ((๐นโ๐ฅ) โ (๐นโ๐ฆ))) = (absโ((๐นโ๐ฆ) โ (๐นโ๐ฅ)))) |
118 | 117 | adantr 482 |
. . . . . . . . . 10
โข
(((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โง ๐ฆ < ๐ฅ) โ (absโ((๐นโ๐ฅ) โ (๐นโ๐ฆ))) = (absโ((๐นโ๐ฆ) โ (๐นโ๐ฅ)))) |
119 | 68 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โ (๐ด[,]๐ต) โ โ) |
120 | 119 | sseld 3948 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โ (๐ฅ โ (๐ด[,]๐ต) โ ๐ฅ โ โ)) |
121 | 119 | sseld 3948 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โ (๐ฆ โ (๐ด[,]๐ต) โ ๐ฆ โ โ)) |
122 | 120, 121 | anim12d 610 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โ ((๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต)) โ (๐ฅ โ โ โง ๐ฆ โ โ))) |
123 | 122 | imp 408 |
. . . . . . . . . . . . 13
โข ((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โ (๐ฅ โ โ โง ๐ฆ โ โ)) |
124 | | recn 11148 |
. . . . . . . . . . . . . 14
โข (๐ฅ โ โ โ ๐ฅ โ
โ) |
125 | | recn 11148 |
. . . . . . . . . . . . . 14
โข (๐ฆ โ โ โ ๐ฆ โ
โ) |
126 | | abssub 15218 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ
(absโ(๐ฅ โ ๐ฆ)) = (absโ(๐ฆ โ ๐ฅ))) |
127 | 124, 125,
126 | syl2an 597 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ
(absโ(๐ฅ โ ๐ฆ)) = (absโ(๐ฆ โ ๐ฅ))) |
128 | 123, 127 | syl 17 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โ (absโ(๐ฅ โ ๐ฆ)) = (absโ(๐ฆ โ ๐ฅ))) |
129 | 128 | adantr 482 |
. . . . . . . . . . 11
โข
(((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โง ๐ฆ < ๐ฅ) โ (absโ(๐ฅ โ ๐ฆ)) = (absโ(๐ฆ โ ๐ฅ))) |
130 | 129 | oveq2d 7378 |
. . . . . . . . . 10
โข
(((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โง ๐ฆ < ๐ฅ) โ (๐ ยท (absโ(๐ฅ โ ๐ฆ))) = (๐ ยท (absโ(๐ฆ โ ๐ฅ)))) |
131 | 118, 130 | breq12d 5123 |
. . . . . . . . 9
โข
(((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โง ๐ฆ < ๐ฅ) โ ((absโ((๐นโ๐ฅ) โ (๐นโ๐ฆ))) โค (๐ ยท (absโ(๐ฅ โ ๐ฆ))) โ (absโ((๐นโ๐ฆ) โ (๐นโ๐ฅ))) โค (๐ ยท (absโ(๐ฆ โ ๐ฅ))))) |
132 | 131 | biimpd 228 |
. . . . . . . 8
โข
(((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โง ๐ฆ < ๐ฅ) โ ((absโ((๐นโ๐ฅ) โ (๐นโ๐ฆ))) โค (๐ ยท (absโ(๐ฅ โ ๐ฆ))) โ (absโ((๐นโ๐ฆ) โ (๐นโ๐ฅ))) โค (๐ ยท (absโ(๐ฆ โ ๐ฅ))))) |
133 | 109, 132 | embantd 59 |
. . . . . . 7
โข
(((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โง ๐ฆ < ๐ฅ) โ ((๐ฆ < ๐ฅ โ (absโ((๐นโ๐ฅ) โ (๐นโ๐ฆ))) โค (๐ ยท (absโ(๐ฅ โ ๐ฆ)))) โ (absโ((๐นโ๐ฆ) โ (๐นโ๐ฅ))) โค (๐ ยท (absโ(๐ฆ โ ๐ฅ))))) |
134 | 108, 133 | syld 47 |
. . . . . 6
โข
(((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โง ๐ฆ < ๐ฅ) โ (โ๐ โ (๐ด[,]๐ต)โ๐ โ (๐ด[,]๐ต)(๐ < ๐ โ (absโ((๐นโ๐) โ (๐นโ๐))) โค (๐ ยท (absโ(๐ โ ๐)))) โ (absโ((๐นโ๐ฆ) โ (๐นโ๐ฅ))) โค (๐ ยท (absโ(๐ฆ โ ๐ฅ))))) |
135 | | lttri4 11246 |
. . . . . . 7
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐ฅ < ๐ฆ โจ ๐ฅ = ๐ฆ โจ ๐ฆ < ๐ฅ)) |
136 | 123, 135 | syl 17 |
. . . . . 6
โข ((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โ (๐ฅ < ๐ฆ โจ ๐ฅ = ๐ฆ โจ ๐ฆ < ๐ฅ)) |
137 | 53, 89, 134, 136 | mpjao3dan 1432 |
. . . . 5
โข ((((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โง (๐ฅ โ (๐ด[,]๐ต) โง ๐ฆ โ (๐ด[,]๐ต))) โ (โ๐ โ (๐ด[,]๐ต)โ๐ โ (๐ด[,]๐ต)(๐ < ๐ โ (absโ((๐นโ๐) โ (๐นโ๐))) โค (๐ ยท (absโ(๐ โ ๐)))) โ (absโ((๐นโ๐ฆ) โ (๐นโ๐ฅ))) โค (๐ ยท (absโ(๐ฆ โ ๐ฅ))))) |
138 | 137 | ralrimdvva 3204 |
. . . 4
โข (((๐ โง ๐ด โค ๐ต) โง ๐ โ โ) โ (โ๐ โ (๐ด[,]๐ต)โ๐ โ (๐ด[,]๐ต)(๐ < ๐ โ (absโ((๐นโ๐) โ (๐นโ๐))) โค (๐ ยท (absโ(๐ โ ๐)))) โ โ๐ฅ โ (๐ด[,]๐ต)โ๐ฆ โ (๐ด[,]๐ต)(absโ((๐นโ๐ฆ) โ (๐นโ๐ฅ))) โค (๐ ยท (absโ(๐ฆ โ ๐ฅ))))) |
139 | 138 | reximdva 3166 |
. . 3
โข ((๐ โง ๐ด โค ๐ต) โ (โ๐ โ โ โ๐ โ (๐ด[,]๐ต)โ๐ โ (๐ด[,]๐ต)(๐ < ๐ โ (absโ((๐นโ๐) โ (๐นโ๐))) โค (๐ ยท (absโ(๐ โ ๐)))) โ โ๐ โ โ โ๐ฅ โ (๐ด[,]๐ต)โ๐ฆ โ (๐ด[,]๐ต)(absโ((๐นโ๐ฆ) โ (๐นโ๐ฅ))) โค (๐ ยท (absโ(๐ฆ โ ๐ฅ))))) |
140 | 32, 139 | mpd 15 |
. 2
โข ((๐ โง ๐ด โค ๐ต) โ โ๐ โ โ โ๐ฅ โ (๐ด[,]๐ต)โ๐ฆ โ (๐ด[,]๐ต)(absโ((๐นโ๐ฆ) โ (๐นโ๐ฅ))) โค (๐ ยท (absโ(๐ฆ โ ๐ฅ)))) |
141 | 15, 140, 6, 4 | ltlecasei 11270 |
1
โข (๐ โ โ๐ โ โ โ๐ฅ โ (๐ด[,]๐ต)โ๐ฆ โ (๐ด[,]๐ต)(absโ((๐นโ๐ฆ) โ (๐นโ๐ฅ))) โค (๐ ยท (absโ(๐ฆ โ ๐ฅ)))) |