Step | Hyp | Ref
| Expression |
1 | | itgabs.1 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ ๐) |
2 | | itgabs.2 |
. . . . . . . . . . . 12
โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ
๐ฟ1) |
3 | 1, 2 | itgcl 25164 |
. . . . . . . . . . 11
โข (๐ โ โซ๐ด๐ต d๐ฅ โ โ) |
4 | 3 | cjcld 15088 |
. . . . . . . . . 10
โข (๐ โ (โโโซ๐ด๐ต d๐ฅ) โ โ) |
5 | | iblmbf 25148 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1 โ (๐ฅ โ ๐ด โฆ ๐ต) โ MblFn) |
6 | 2, 5 | syl 17 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ MblFn) |
7 | 6, 1 | mbfmptcl 25016 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) |
8 | 7 | ralrimiva 3144 |
. . . . . . . . . . . 12
โข (๐ โ โ๐ฅ โ ๐ด ๐ต โ โ) |
9 | | nfv 1918 |
. . . . . . . . . . . . 13
โข
โฒ๐ฆ ๐ต โ โ |
10 | | nfcsb1v 3885 |
. . . . . . . . . . . . . 14
โข
โฒ๐ฅโฆ๐ฆ / ๐ฅโฆ๐ต |
11 | 10 | nfel1 2924 |
. . . . . . . . . . . . 13
โข
โฒ๐ฅโฆ๐ฆ / ๐ฅโฆ๐ต โ โ |
12 | | csbeq1a 3874 |
. . . . . . . . . . . . . 14
โข (๐ฅ = ๐ฆ โ ๐ต = โฆ๐ฆ / ๐ฅโฆ๐ต) |
13 | 12 | eleq1d 2823 |
. . . . . . . . . . . . 13
โข (๐ฅ = ๐ฆ โ (๐ต โ โ โ โฆ๐ฆ / ๐ฅโฆ๐ต โ โ)) |
14 | 9, 11, 13 | cbvralw 3292 |
. . . . . . . . . . . 12
โข
(โ๐ฅ โ
๐ด ๐ต โ โ โ โ๐ฆ โ ๐ด โฆ๐ฆ / ๐ฅโฆ๐ต โ โ) |
15 | 8, 14 | sylib 217 |
. . . . . . . . . . 11
โข (๐ โ โ๐ฆ โ ๐ด โฆ๐ฆ / ๐ฅโฆ๐ต โ โ) |
16 | 15 | r19.21bi 3237 |
. . . . . . . . . 10
โข ((๐ โง ๐ฆ โ ๐ด) โ โฆ๐ฆ / ๐ฅโฆ๐ต โ โ) |
17 | | nfcv 2908 |
. . . . . . . . . . . 12
โข
โฒ๐ฆ๐ต |
18 | 17, 10, 12 | cbvmpt 5221 |
. . . . . . . . . . 11
โข (๐ฅ โ ๐ด โฆ ๐ต) = (๐ฆ โ ๐ด โฆ โฆ๐ฆ / ๐ฅโฆ๐ต) |
19 | 18, 2 | eqeltrrid 2843 |
. . . . . . . . . 10
โข (๐ โ (๐ฆ โ ๐ด โฆ โฆ๐ฆ / ๐ฅโฆ๐ต) โ
๐ฟ1) |
20 | 4, 16, 19 | iblmulc2 25211 |
. . . . . . . . 9
โข (๐ โ (๐ฆ โ ๐ด โฆ ((โโโซ๐ด๐ต d๐ฅ) ยท โฆ๐ฆ / ๐ฅโฆ๐ต)) โ
๐ฟ1) |
21 | 4 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฆ โ ๐ด) โ (โโโซ๐ด๐ต d๐ฅ) โ โ) |
22 | 21, 16 | mulcld 11182 |
. . . . . . . . . 10
โข ((๐ โง ๐ฆ โ ๐ด) โ ((โโโซ๐ด๐ต d๐ฅ) ยท โฆ๐ฆ / ๐ฅโฆ๐ต) โ โ) |
23 | 22 | iblcn 25179 |
. . . . . . . . 9
โข (๐ โ ((๐ฆ โ ๐ด โฆ ((โโโซ๐ด๐ต d๐ฅ) ยท โฆ๐ฆ / ๐ฅโฆ๐ต)) โ ๐ฟ1 โ
((๐ฆ โ ๐ด โฆ
(โโ((โโโซ๐ด๐ต d๐ฅ) ยท โฆ๐ฆ / ๐ฅโฆ๐ต))) โ ๐ฟ1 โง
(๐ฆ โ ๐ด โฆ
(โโ((โโโซ๐ด๐ต d๐ฅ) ยท โฆ๐ฆ / ๐ฅโฆ๐ต))) โ
๐ฟ1))) |
24 | 20, 23 | mpbid 231 |
. . . . . . . 8
โข (๐ โ ((๐ฆ โ ๐ด โฆ
(โโ((โโโซ๐ด๐ต d๐ฅ) ยท โฆ๐ฆ / ๐ฅโฆ๐ต))) โ ๐ฟ1 โง
(๐ฆ โ ๐ด โฆ
(โโ((โโโซ๐ด๐ต d๐ฅ) ยท โฆ๐ฆ / ๐ฅโฆ๐ต))) โ
๐ฟ1)) |
25 | 24 | simpld 496 |
. . . . . . 7
โข (๐ โ (๐ฆ โ ๐ด โฆ
(โโ((โโโซ๐ด๐ต d๐ฅ) ยท โฆ๐ฆ / ๐ฅโฆ๐ต))) โ
๐ฟ1) |
26 | | ovexd 7397 |
. . . . . . . 8
โข ((๐ โง ๐ฆ โ ๐ด) โ ((โโโซ๐ด๐ต d๐ฅ) ยท โฆ๐ฆ / ๐ฅโฆ๐ต) โ V) |
27 | 26, 20 | iblabs 25209 |
. . . . . . 7
โข (๐ โ (๐ฆ โ ๐ด โฆ
(absโ((โโโซ๐ด๐ต d๐ฅ) ยท โฆ๐ฆ / ๐ฅโฆ๐ต))) โ
๐ฟ1) |
28 | 22 | recld 15086 |
. . . . . . 7
โข ((๐ โง ๐ฆ โ ๐ด) โ
(โโ((โโโซ๐ด๐ต d๐ฅ) ยท โฆ๐ฆ / ๐ฅโฆ๐ต)) โ โ) |
29 | 22 | abscld 15328 |
. . . . . . 7
โข ((๐ โง ๐ฆ โ ๐ด) โ
(absโ((โโโซ๐ด๐ต d๐ฅ) ยท โฆ๐ฆ / ๐ฅโฆ๐ต)) โ โ) |
30 | 22 | releabsd 15343 |
. . . . . . 7
โข ((๐ โง ๐ฆ โ ๐ด) โ
(โโ((โโโซ๐ด๐ต d๐ฅ) ยท โฆ๐ฆ / ๐ฅโฆ๐ต)) โค
(absโ((โโโซ๐ด๐ต d๐ฅ) ยท โฆ๐ฆ / ๐ฅโฆ๐ต))) |
31 | 25, 27, 28, 29, 30 | itgle 25190 |
. . . . . 6
โข (๐ โ โซ๐ด(โโ((โโโซ๐ด๐ต d๐ฅ) ยท โฆ๐ฆ / ๐ฅโฆ๐ต)) d๐ฆ โค โซ๐ด(absโ((โโโซ๐ด๐ต d๐ฅ) ยท โฆ๐ฆ / ๐ฅโฆ๐ต)) d๐ฆ) |
32 | 3 | abscld 15328 |
. . . . . . . . 9
โข (๐ โ (absโโซ๐ด๐ต d๐ฅ) โ โ) |
33 | 32 | recnd 11190 |
. . . . . . . 8
โข (๐ โ (absโโซ๐ด๐ต d๐ฅ) โ โ) |
34 | 33 | sqvald 14055 |
. . . . . . 7
โข (๐ โ ((absโโซ๐ด๐ต d๐ฅ)โ2) = ((absโโซ๐ด๐ต d๐ฅ) ยท (absโโซ๐ด๐ต d๐ฅ))) |
35 | 3 | absvalsqd 15334 |
. . . . . . . . . 10
โข (๐ โ ((absโโซ๐ด๐ต d๐ฅ)โ2) = (โซ๐ด๐ต d๐ฅ ยท (โโโซ๐ด๐ต d๐ฅ))) |
36 | 3, 4 | mulcomd 11183 |
. . . . . . . . . 10
โข (๐ โ (โซ๐ด๐ต d๐ฅ ยท (โโโซ๐ด๐ต d๐ฅ)) = ((โโโซ๐ด๐ต d๐ฅ) ยท โซ๐ด๐ต d๐ฅ)) |
37 | 12, 17, 10 | cbvitg 25156 |
. . . . . . . . . . . 12
โข
โซ๐ด๐ต d๐ฅ = โซ๐ดโฆ๐ฆ / ๐ฅโฆ๐ต d๐ฆ |
38 | 37 | oveq2i 7373 |
. . . . . . . . . . 11
โข
((โโโซ๐ด๐ต d๐ฅ) ยท โซ๐ด๐ต d๐ฅ) = ((โโโซ๐ด๐ต d๐ฅ) ยท โซ๐ดโฆ๐ฆ / ๐ฅโฆ๐ต d๐ฆ) |
39 | 4, 16, 19 | itgmulc2 25214 |
. . . . . . . . . . 11
โข (๐ โ
((โโโซ๐ด๐ต d๐ฅ) ยท โซ๐ดโฆ๐ฆ / ๐ฅโฆ๐ต d๐ฆ) = โซ๐ด((โโโซ๐ด๐ต d๐ฅ) ยท โฆ๐ฆ / ๐ฅโฆ๐ต) d๐ฆ) |
40 | 38, 39 | eqtrid 2789 |
. . . . . . . . . 10
โข (๐ โ
((โโโซ๐ด๐ต d๐ฅ) ยท โซ๐ด๐ต d๐ฅ) = โซ๐ด((โโโซ๐ด๐ต d๐ฅ) ยท โฆ๐ฆ / ๐ฅโฆ๐ต) d๐ฆ) |
41 | 35, 36, 40 | 3eqtrd 2781 |
. . . . . . . . 9
โข (๐ โ ((absโโซ๐ด๐ต d๐ฅ)โ2) = โซ๐ด((โโโซ๐ด๐ต d๐ฅ) ยท โฆ๐ฆ / ๐ฅโฆ๐ต) d๐ฆ) |
42 | 41 | fveq2d 6851 |
. . . . . . . 8
โข (๐ โ
(โโ((absโโซ๐ด๐ต d๐ฅ)โ2)) = (โโโซ๐ด((โโโซ๐ด๐ต d๐ฅ) ยท โฆ๐ฆ / ๐ฅโฆ๐ต) d๐ฆ)) |
43 | 32 | resqcld 14037 |
. . . . . . . . 9
โข (๐ โ ((absโโซ๐ด๐ต d๐ฅ)โ2) โ โ) |
44 | 43 | rered 15116 |
. . . . . . . 8
โข (๐ โ
(โโ((absโโซ๐ด๐ต d๐ฅ)โ2)) = ((absโโซ๐ด๐ต d๐ฅ)โ2)) |
45 | 26, 20 | itgre 25181 |
. . . . . . . 8
โข (๐ โ (โโโซ๐ด((โโโซ๐ด๐ต d๐ฅ) ยท โฆ๐ฆ / ๐ฅโฆ๐ต) d๐ฆ) = โซ๐ด(โโ((โโโซ๐ด๐ต d๐ฅ) ยท โฆ๐ฆ / ๐ฅโฆ๐ต)) d๐ฆ) |
46 | 42, 44, 45 | 3eqtr3d 2785 |
. . . . . . 7
โข (๐ โ ((absโโซ๐ด๐ต d๐ฅ)โ2) = โซ๐ด(โโ((โโโซ๐ด๐ต d๐ฅ) ยท โฆ๐ฆ / ๐ฅโฆ๐ต)) d๐ฆ) |
47 | 34, 46 | eqtr3d 2779 |
. . . . . 6
โข (๐ โ ((absโโซ๐ด๐ต d๐ฅ) ยท (absโโซ๐ด๐ต d๐ฅ)) = โซ๐ด(โโ((โโโซ๐ด๐ต d๐ฅ) ยท โฆ๐ฆ / ๐ฅโฆ๐ต)) d๐ฆ) |
48 | 12 | fveq2d 6851 |
. . . . . . . . 9
โข (๐ฅ = ๐ฆ โ (absโ๐ต) = (absโโฆ๐ฆ / ๐ฅโฆ๐ต)) |
49 | | nfcv 2908 |
. . . . . . . . 9
โข
โฒ๐ฆ(absโ๐ต) |
50 | | nfcv 2908 |
. . . . . . . . . 10
โข
โฒ๐ฅabs |
51 | 50, 10 | nffv 6857 |
. . . . . . . . 9
โข
โฒ๐ฅ(absโโฆ๐ฆ / ๐ฅโฆ๐ต) |
52 | 48, 49, 51 | cbvitg 25156 |
. . . . . . . 8
โข
โซ๐ด(absโ๐ต) d๐ฅ = โซ๐ด(absโโฆ๐ฆ / ๐ฅโฆ๐ต) d๐ฆ |
53 | 52 | oveq2i 7373 |
. . . . . . 7
โข
((absโโซ๐ด๐ต d๐ฅ) ยท โซ๐ด(absโ๐ต) d๐ฅ) = ((absโโซ๐ด๐ต d๐ฅ) ยท โซ๐ด(absโโฆ๐ฆ / ๐ฅโฆ๐ต) d๐ฆ) |
54 | 16 | abscld 15328 |
. . . . . . . . 9
โข ((๐ โง ๐ฆ โ ๐ด) โ (absโโฆ๐ฆ / ๐ฅโฆ๐ต) โ โ) |
55 | 16, 19 | iblabs 25209 |
. . . . . . . . 9
โข (๐ โ (๐ฆ โ ๐ด โฆ (absโโฆ๐ฆ / ๐ฅโฆ๐ต)) โ
๐ฟ1) |
56 | 33, 54, 55 | itgmulc2 25214 |
. . . . . . . 8
โข (๐ โ ((absโโซ๐ด๐ต d๐ฅ) ยท โซ๐ด(absโโฆ๐ฆ / ๐ฅโฆ๐ต) d๐ฆ) = โซ๐ด((absโโซ๐ด๐ต d๐ฅ) ยท (absโโฆ๐ฆ / ๐ฅโฆ๐ต)) d๐ฆ) |
57 | 21, 16 | absmuld 15346 |
. . . . . . . . . 10
โข ((๐ โง ๐ฆ โ ๐ด) โ
(absโ((โโโซ๐ด๐ต d๐ฅ) ยท โฆ๐ฆ / ๐ฅโฆ๐ต)) = ((absโ(โโโซ๐ด๐ต d๐ฅ)) ยท (absโโฆ๐ฆ / ๐ฅโฆ๐ต))) |
58 | 3 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฆ โ ๐ด) โ โซ๐ด๐ต d๐ฅ โ โ) |
59 | 58 | abscjd 15342 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฆ โ ๐ด) โ
(absโ(โโโซ๐ด๐ต d๐ฅ)) = (absโโซ๐ด๐ต d๐ฅ)) |
60 | 59 | oveq1d 7377 |
. . . . . . . . . 10
โข ((๐ โง ๐ฆ โ ๐ด) โ
((absโ(โโโซ๐ด๐ต d๐ฅ)) ยท (absโโฆ๐ฆ / ๐ฅโฆ๐ต)) = ((absโโซ๐ด๐ต d๐ฅ) ยท (absโโฆ๐ฆ / ๐ฅโฆ๐ต))) |
61 | 57, 60 | eqtrd 2777 |
. . . . . . . . 9
โข ((๐ โง ๐ฆ โ ๐ด) โ
(absโ((โโโซ๐ด๐ต d๐ฅ) ยท โฆ๐ฆ / ๐ฅโฆ๐ต)) = ((absโโซ๐ด๐ต d๐ฅ) ยท (absโโฆ๐ฆ / ๐ฅโฆ๐ต))) |
62 | 61 | itgeq2dv 25162 |
. . . . . . . 8
โข (๐ โ โซ๐ด(absโ((โโโซ๐ด๐ต d๐ฅ) ยท โฆ๐ฆ / ๐ฅโฆ๐ต)) d๐ฆ = โซ๐ด((absโโซ๐ด๐ต d๐ฅ) ยท (absโโฆ๐ฆ / ๐ฅโฆ๐ต)) d๐ฆ) |
63 | 56, 62 | eqtr4d 2780 |
. . . . . . 7
โข (๐ โ ((absโโซ๐ด๐ต d๐ฅ) ยท โซ๐ด(absโโฆ๐ฆ / ๐ฅโฆ๐ต) d๐ฆ) = โซ๐ด(absโ((โโโซ๐ด๐ต d๐ฅ) ยท โฆ๐ฆ / ๐ฅโฆ๐ต)) d๐ฆ) |
64 | 53, 63 | eqtrid 2789 |
. . . . . 6
โข (๐ โ ((absโโซ๐ด๐ต d๐ฅ) ยท โซ๐ด(absโ๐ต) d๐ฅ) = โซ๐ด(absโ((โโโซ๐ด๐ต d๐ฅ) ยท โฆ๐ฆ / ๐ฅโฆ๐ต)) d๐ฆ) |
65 | 31, 47, 64 | 3brtr4d 5142 |
. . . . 5
โข (๐ โ ((absโโซ๐ด๐ต d๐ฅ) ยท (absโโซ๐ด๐ต d๐ฅ)) โค ((absโโซ๐ด๐ต d๐ฅ) ยท โซ๐ด(absโ๐ต) d๐ฅ)) |
66 | 65 | adantr 482 |
. . . 4
โข ((๐ โง 0 <
(absโโซ๐ด๐ต d๐ฅ)) โ ((absโโซ๐ด๐ต d๐ฅ) ยท (absโโซ๐ด๐ต d๐ฅ)) โค ((absโโซ๐ด๐ต d๐ฅ) ยท โซ๐ด(absโ๐ต) d๐ฅ)) |
67 | 32 | adantr 482 |
. . . . 5
โข ((๐ โง 0 <
(absโโซ๐ด๐ต d๐ฅ)) โ (absโโซ๐ด๐ต d๐ฅ) โ โ) |
68 | 7 | abscld 15328 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐ด) โ (absโ๐ต) โ โ) |
69 | 1, 2 | iblabs 25209 |
. . . . . . 7
โข (๐ โ (๐ฅ โ ๐ด โฆ (absโ๐ต)) โ
๐ฟ1) |
70 | 68, 69 | itgrecl 25178 |
. . . . . 6
โข (๐ โ โซ๐ด(absโ๐ต) d๐ฅ โ โ) |
71 | 70 | adantr 482 |
. . . . 5
โข ((๐ โง 0 <
(absโโซ๐ด๐ต d๐ฅ)) โ โซ๐ด(absโ๐ต) d๐ฅ โ โ) |
72 | | simpr 486 |
. . . . 5
โข ((๐ โง 0 <
(absโโซ๐ด๐ต d๐ฅ)) โ 0 < (absโโซ๐ด๐ต d๐ฅ)) |
73 | | lemul2 12015 |
. . . . 5
โข
(((absโโซ๐ด๐ต d๐ฅ) โ โ โง โซ๐ด(absโ๐ต) d๐ฅ โ โ โง ((absโโซ๐ด๐ต d๐ฅ) โ โ โง 0 <
(absโโซ๐ด๐ต d๐ฅ))) โ ((absโโซ๐ด๐ต d๐ฅ) โค โซ๐ด(absโ๐ต) d๐ฅ โ ((absโโซ๐ด๐ต d๐ฅ) ยท (absโโซ๐ด๐ต d๐ฅ)) โค ((absโโซ๐ด๐ต d๐ฅ) ยท โซ๐ด(absโ๐ต) d๐ฅ))) |
74 | 67, 71, 67, 72, 73 | syl112anc 1375 |
. . . 4
โข ((๐ โง 0 <
(absโโซ๐ด๐ต d๐ฅ)) โ ((absโโซ๐ด๐ต d๐ฅ) โค โซ๐ด(absโ๐ต) d๐ฅ โ ((absโโซ๐ด๐ต d๐ฅ) ยท (absโโซ๐ด๐ต d๐ฅ)) โค ((absโโซ๐ด๐ต d๐ฅ) ยท โซ๐ด(absโ๐ต) d๐ฅ))) |
75 | 66, 74 | mpbird 257 |
. . 3
โข ((๐ โง 0 <
(absโโซ๐ด๐ต d๐ฅ)) โ (absโโซ๐ด๐ต d๐ฅ) โค โซ๐ด(absโ๐ต) d๐ฅ) |
76 | 75 | ex 414 |
. 2
โข (๐ โ (0 <
(absโโซ๐ด๐ต d๐ฅ) โ (absโโซ๐ด๐ต d๐ฅ) โค โซ๐ด(absโ๐ต) d๐ฅ)) |
77 | 7 | absge0d 15336 |
. . . 4
โข ((๐ โง ๐ฅ โ ๐ด) โ 0 โค (absโ๐ต)) |
78 | 69, 68, 77 | itgge0 25191 |
. . 3
โข (๐ โ 0 โค โซ๐ด(absโ๐ต) d๐ฅ) |
79 | | breq1 5113 |
. . 3
โข (0 =
(absโโซ๐ด๐ต d๐ฅ) โ (0 โค โซ๐ด(absโ๐ต) d๐ฅ โ (absโโซ๐ด๐ต d๐ฅ) โค โซ๐ด(absโ๐ต) d๐ฅ)) |
80 | 78, 79 | syl5ibcom 244 |
. 2
โข (๐ โ (0 = (absโโซ๐ด๐ต d๐ฅ) โ (absโโซ๐ด๐ต d๐ฅ) โค โซ๐ด(absโ๐ต) d๐ฅ)) |
81 | 3 | absge0d 15336 |
. . 3
โข (๐ โ 0 โค
(absโโซ๐ด๐ต d๐ฅ)) |
82 | | 0re 11164 |
. . . 4
โข 0 โ
โ |
83 | | leloe 11248 |
. . . 4
โข ((0
โ โ โง (absโโซ๐ด๐ต d๐ฅ) โ โ) โ (0 โค
(absโโซ๐ด๐ต d๐ฅ) โ (0 < (absโโซ๐ด๐ต d๐ฅ) โจ 0 = (absโโซ๐ด๐ต d๐ฅ)))) |
84 | 82, 32, 83 | sylancr 588 |
. . 3
โข (๐ โ (0 โค
(absโโซ๐ด๐ต d๐ฅ) โ (0 < (absโโซ๐ด๐ต d๐ฅ) โจ 0 = (absโโซ๐ด๐ต d๐ฅ)))) |
85 | 81, 84 | mpbid 231 |
. 2
โข (๐ โ (0 <
(absโโซ๐ด๐ต d๐ฅ) โจ 0 = (absโโซ๐ด๐ต d๐ฅ))) |
86 | 76, 80, 85 | mpjaod 859 |
1
โข (๐ โ (absโโซ๐ด๐ต d๐ฅ) โค โซ๐ด(absโ๐ต) d๐ฅ) |