Step | Hyp | Ref
| Expression |
1 | | itgabsnc.1 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΄) β π΅ β π) |
2 | | itgabsnc.2 |
. . . . . . . . . . . 12
β’ (π β (π₯ β π΄ β¦ π΅) β
πΏ1) |
3 | 1, 2 | itgcl 25151 |
. . . . . . . . . . 11
β’ (π β β«π΄π΅ dπ₯ β β) |
4 | 3 | cjcld 15082 |
. . . . . . . . . 10
β’ (π β (βββ«π΄π΅ dπ₯) β β) |
5 | | iblmbf 25135 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β π΄ β¦ π΅) β πΏ1 β (π₯ β π΄ β¦ π΅) β MblFn) |
6 | 2, 5 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β (π₯ β π΄ β¦ π΅) β MblFn) |
7 | 6, 1 | mbfmptcl 25003 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β π΄) β π΅ β β) |
8 | 7 | ralrimiva 3144 |
. . . . . . . . . . . 12
β’ (π β βπ₯ β π΄ π΅ β β) |
9 | | nfv 1918 |
. . . . . . . . . . . . 13
β’
β²π¦ π΅ β β |
10 | | nfcsb1v 3881 |
. . . . . . . . . . . . . 14
β’
β²π₯β¦π¦ / π₯β¦π΅ |
11 | 10 | nfel1 2924 |
. . . . . . . . . . . . 13
β’
β²π₯β¦π¦ / π₯β¦π΅ β β |
12 | | csbeq1a 3870 |
. . . . . . . . . . . . . 14
β’ (π₯ = π¦ β π΅ = β¦π¦ / π₯β¦π΅) |
13 | 12 | eleq1d 2823 |
. . . . . . . . . . . . 13
β’ (π₯ = π¦ β (π΅ β β β β¦π¦ / π₯β¦π΅ β β)) |
14 | 9, 11, 13 | cbvralw 3290 |
. . . . . . . . . . . 12
β’
(βπ₯ β
π΄ π΅ β β β βπ¦ β π΄ β¦π¦ / π₯β¦π΅ β β) |
15 | 8, 14 | sylib 217 |
. . . . . . . . . . 11
β’ (π β βπ¦ β π΄ β¦π¦ / π₯β¦π΅ β β) |
16 | 15 | r19.21bi 3235 |
. . . . . . . . . 10
β’ ((π β§ π¦ β π΄) β β¦π¦ / π₯β¦π΅ β β) |
17 | | nfcv 2908 |
. . . . . . . . . . . 12
β’
β²π¦π΅ |
18 | 17, 10, 12 | cbvmpt 5217 |
. . . . . . . . . . 11
β’ (π₯ β π΄ β¦ π΅) = (π¦ β π΄ β¦ β¦π¦ / π₯β¦π΅) |
19 | 18, 2 | eqeltrrid 2843 |
. . . . . . . . . 10
β’ (π β (π¦ β π΄ β¦ β¦π¦ / π₯β¦π΅) β
πΏ1) |
20 | | itgabsnc.m2 |
. . . . . . . . . 10
β’ (π β (π¦ β π΄ β¦ ((βββ«π΄π΅ dπ₯) Β· β¦π¦ / π₯β¦π΅)) β MblFn) |
21 | 4, 16, 19, 20 | iblmulc2nc 36146 |
. . . . . . . . 9
β’ (π β (π¦ β π΄ β¦ ((βββ«π΄π΅ dπ₯) Β· β¦π¦ / π₯β¦π΅)) β
πΏ1) |
22 | 4 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β π΄) β (βββ«π΄π΅ dπ₯) β β) |
23 | 22, 16 | mulcld 11176 |
. . . . . . . . . 10
β’ ((π β§ π¦ β π΄) β ((βββ«π΄π΅ dπ₯) Β· β¦π¦ / π₯β¦π΅) β β) |
24 | 23 | iblcn 25166 |
. . . . . . . . 9
β’ (π β ((π¦ β π΄ β¦ ((βββ«π΄π΅ dπ₯) Β· β¦π¦ / π₯β¦π΅)) β πΏ1 β
((π¦ β π΄ β¦
(ββ((βββ«π΄π΅ dπ₯) Β· β¦π¦ / π₯β¦π΅))) β πΏ1 β§
(π¦ β π΄ β¦
(ββ((βββ«π΄π΅ dπ₯) Β· β¦π¦ / π₯β¦π΅))) β
πΏ1))) |
25 | 21, 24 | mpbid 231 |
. . . . . . . 8
β’ (π β ((π¦ β π΄ β¦
(ββ((βββ«π΄π΅ dπ₯) Β· β¦π¦ / π₯β¦π΅))) β πΏ1 β§
(π¦ β π΄ β¦
(ββ((βββ«π΄π΅ dπ₯) Β· β¦π¦ / π₯β¦π΅))) β
πΏ1)) |
26 | 25 | simpld 496 |
. . . . . . 7
β’ (π β (π¦ β π΄ β¦
(ββ((βββ«π΄π΅ dπ₯) Β· β¦π¦ / π₯β¦π΅))) β
πΏ1) |
27 | 22, 16 | absmuld 15340 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β π΄) β
(absβ((βββ«π΄π΅ dπ₯) Β· β¦π¦ / π₯β¦π΅)) = ((absβ(βββ«π΄π΅ dπ₯)) Β· (absββ¦π¦ / π₯β¦π΅))) |
28 | 27 | mpteq2dva 5206 |
. . . . . . . . . 10
β’ (π β (π¦ β π΄ β¦
(absβ((βββ«π΄π΅ dπ₯) Β· β¦π¦ / π₯β¦π΅))) = (π¦ β π΄ β¦
((absβ(βββ«π΄π΅ dπ₯)) Β· (absββ¦π¦ / π₯β¦π΅)))) |
29 | 6, 1 | mbfdm2 25004 |
. . . . . . . . . . 11
β’ (π β π΄ β dom vol) |
30 | 22 | abscld 15322 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β π΄) β
(absβ(βββ«π΄π΅ dπ₯)) β β) |
31 | 16 | abscld 15322 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β π΄) β (absββ¦π¦ / π₯β¦π΅) β β) |
32 | | fconstmpt 5695 |
. . . . . . . . . . . 12
β’ (π΄ Γ
{(absβ(βββ«π΄π΅ dπ₯))}) = (π¦ β π΄ β¦
(absβ(βββ«π΄π΅ dπ₯))) |
33 | 32 | a1i 11 |
. . . . . . . . . . 11
β’ (π β (π΄ Γ
{(absβ(βββ«π΄π΅ dπ₯))}) = (π¦ β π΄ β¦
(absβ(βββ«π΄π΅ dπ₯)))) |
34 | | nfcv 2908 |
. . . . . . . . . . . . 13
β’
β²π¦(absβπ΅) |
35 | | nfcv 2908 |
. . . . . . . . . . . . . 14
β’
β²π₯abs |
36 | 35, 10 | nffv 6853 |
. . . . . . . . . . . . 13
β’
β²π₯(absββ¦π¦ / π₯β¦π΅) |
37 | 12 | fveq2d 6847 |
. . . . . . . . . . . . 13
β’ (π₯ = π¦ β (absβπ΅) = (absββ¦π¦ / π₯β¦π΅)) |
38 | 34, 36, 37 | cbvmpt 5217 |
. . . . . . . . . . . 12
β’ (π₯ β π΄ β¦ (absβπ΅)) = (π¦ β π΄ β¦ (absββ¦π¦ / π₯β¦π΅)) |
39 | 38 | a1i 11 |
. . . . . . . . . . 11
β’ (π β (π₯ β π΄ β¦ (absβπ΅)) = (π¦ β π΄ β¦ (absββ¦π¦ / π₯β¦π΅))) |
40 | 29, 30, 31, 33, 39 | offval2 7638 |
. . . . . . . . . 10
β’ (π β ((π΄ Γ
{(absβ(βββ«π΄π΅ dπ₯))}) βf Β· (π₯ β π΄ β¦ (absβπ΅))) = (π¦ β π΄ β¦
((absβ(βββ«π΄π΅ dπ₯)) Β· (absββ¦π¦ / π₯β¦π΅)))) |
41 | 28, 40 | eqtr4d 2780 |
. . . . . . . . 9
β’ (π β (π¦ β π΄ β¦
(absβ((βββ«π΄π΅ dπ₯) Β· β¦π¦ / π₯β¦π΅))) = ((π΄ Γ
{(absβ(βββ«π΄π΅ dπ₯))}) βf Β· (π₯ β π΄ β¦ (absβπ΅)))) |
42 | | itgabsnc.m1 |
. . . . . . . . . 10
β’ (π β (π₯ β π΄ β¦ (absβπ΅)) β MblFn) |
43 | 4 | abscld 15322 |
. . . . . . . . . 10
β’ (π β
(absβ(βββ«π΄π΅ dπ₯)) β β) |
44 | 7 | abscld 15322 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΄) β (absβπ΅) β β) |
45 | 44 | recnd 11184 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΄) β (absβπ΅) β β) |
46 | 45 | fmpttd 7064 |
. . . . . . . . . 10
β’ (π β (π₯ β π΄ β¦ (absβπ΅)):π΄βΆβ) |
47 | 42, 43, 46 | mbfmulc2re 25015 |
. . . . . . . . 9
β’ (π β ((π΄ Γ
{(absβ(βββ«π΄π΅ dπ₯))}) βf Β· (π₯ β π΄ β¦ (absβπ΅))) β MblFn) |
48 | 41, 47 | eqeltrd 2838 |
. . . . . . . 8
β’ (π β (π¦ β π΄ β¦
(absβ((βββ«π΄π΅ dπ₯) Β· β¦π¦ / π₯β¦π΅))) β MblFn) |
49 | 23, 21, 48 | iblabsnc 36145 |
. . . . . . 7
β’ (π β (π¦ β π΄ β¦
(absβ((βββ«π΄π΅ dπ₯) Β· β¦π¦ / π₯β¦π΅))) β
πΏ1) |
50 | 23 | recld 15080 |
. . . . . . 7
β’ ((π β§ π¦ β π΄) β
(ββ((βββ«π΄π΅ dπ₯) Β· β¦π¦ / π₯β¦π΅)) β β) |
51 | 23 | abscld 15322 |
. . . . . . 7
β’ ((π β§ π¦ β π΄) β
(absβ((βββ«π΄π΅ dπ₯) Β· β¦π¦ / π₯β¦π΅)) β β) |
52 | 23 | releabsd 15337 |
. . . . . . 7
β’ ((π β§ π¦ β π΄) β
(ββ((βββ«π΄π΅ dπ₯) Β· β¦π¦ / π₯β¦π΅)) β€
(absβ((βββ«π΄π΅ dπ₯) Β· β¦π¦ / π₯β¦π΅))) |
53 | 26, 49, 50, 51, 52 | itgle 25177 |
. . . . . 6
β’ (π β β«π΄(ββ((βββ«π΄π΅ dπ₯) Β· β¦π¦ / π₯β¦π΅)) dπ¦ β€ β«π΄(absβ((βββ«π΄π΅ dπ₯) Β· β¦π¦ / π₯β¦π΅)) dπ¦) |
54 | 3 | abscld 15322 |
. . . . . . . . 9
β’ (π β (absββ«π΄π΅ dπ₯) β β) |
55 | 54 | recnd 11184 |
. . . . . . . 8
β’ (π β (absββ«π΄π΅ dπ₯) β β) |
56 | 55 | sqvald 14049 |
. . . . . . 7
β’ (π β ((absββ«π΄π΅ dπ₯)β2) = ((absββ«π΄π΅ dπ₯) Β· (absββ«π΄π΅ dπ₯))) |
57 | 3 | absvalsqd 15328 |
. . . . . . . . . 10
β’ (π β ((absββ«π΄π΅ dπ₯)β2) = (β«π΄π΅ dπ₯ Β· (βββ«π΄π΅ dπ₯))) |
58 | 3, 4 | mulcomd 11177 |
. . . . . . . . . 10
β’ (π β (β«π΄π΅ dπ₯ Β· (βββ«π΄π΅ dπ₯)) = ((βββ«π΄π΅ dπ₯) Β· β«π΄π΅ dπ₯)) |
59 | 12, 17, 10 | cbvitg 25143 |
. . . . . . . . . . . 12
β’
β«π΄π΅ dπ₯ = β«π΄β¦π¦ / π₯β¦π΅ dπ¦ |
60 | 59 | oveq2i 7369 |
. . . . . . . . . . 11
β’
((βββ«π΄π΅ dπ₯) Β· β«π΄π΅ dπ₯) = ((βββ«π΄π΅ dπ₯) Β· β«π΄β¦π¦ / π₯β¦π΅ dπ¦) |
61 | 4, 16, 19, 20 | itgmulc2nc 36149 |
. . . . . . . . . . 11
β’ (π β
((βββ«π΄π΅ dπ₯) Β· β«π΄β¦π¦ / π₯β¦π΅ dπ¦) = β«π΄((βββ«π΄π΅ dπ₯) Β· β¦π¦ / π₯β¦π΅) dπ¦) |
62 | 60, 61 | eqtrid 2789 |
. . . . . . . . . 10
β’ (π β
((βββ«π΄π΅ dπ₯) Β· β«π΄π΅ dπ₯) = β«π΄((βββ«π΄π΅ dπ₯) Β· β¦π¦ / π₯β¦π΅) dπ¦) |
63 | 57, 58, 62 | 3eqtrd 2781 |
. . . . . . . . 9
β’ (π β ((absββ«π΄π΅ dπ₯)β2) = β«π΄((βββ«π΄π΅ dπ₯) Β· β¦π¦ / π₯β¦π΅) dπ¦) |
64 | 63 | fveq2d 6847 |
. . . . . . . 8
β’ (π β
(ββ((absββ«π΄π΅ dπ₯)β2)) = (βββ«π΄((βββ«π΄π΅ dπ₯) Β· β¦π¦ / π₯β¦π΅) dπ¦)) |
65 | 54 | resqcld 14031 |
. . . . . . . . 9
β’ (π β ((absββ«π΄π΅ dπ₯)β2) β β) |
66 | 65 | rered 15110 |
. . . . . . . 8
β’ (π β
(ββ((absββ«π΄π΅ dπ₯)β2)) = ((absββ«π΄π΅ dπ₯)β2)) |
67 | | ovexd 7393 |
. . . . . . . . 9
β’ ((π β§ π¦ β π΄) β ((βββ«π΄π΅ dπ₯) Β· β¦π¦ / π₯β¦π΅) β V) |
68 | 67, 21 | itgre 25168 |
. . . . . . . 8
β’ (π β (βββ«π΄((βββ«π΄π΅ dπ₯) Β· β¦π¦ / π₯β¦π΅) dπ¦) = β«π΄(ββ((βββ«π΄π΅ dπ₯) Β· β¦π¦ / π₯β¦π΅)) dπ¦) |
69 | 64, 66, 68 | 3eqtr3d 2785 |
. . . . . . 7
β’ (π β ((absββ«π΄π΅ dπ₯)β2) = β«π΄(ββ((βββ«π΄π΅ dπ₯) Β· β¦π¦ / π₯β¦π΅)) dπ¦) |
70 | 56, 69 | eqtr3d 2779 |
. . . . . 6
β’ (π β ((absββ«π΄π΅ dπ₯) Β· (absββ«π΄π΅ dπ₯)) = β«π΄(ββ((βββ«π΄π΅ dπ₯) Β· β¦π¦ / π₯β¦π΅)) dπ¦) |
71 | 37, 34, 36 | cbvitg 25143 |
. . . . . . . 8
β’
β«π΄(absβπ΅) dπ₯ = β«π΄(absββ¦π¦ / π₯β¦π΅) dπ¦ |
72 | 71 | oveq2i 7369 |
. . . . . . 7
β’
((absββ«π΄π΅ dπ₯) Β· β«π΄(absβπ΅) dπ₯) = ((absββ«π΄π΅ dπ₯) Β· β«π΄(absββ¦π¦ / π₯β¦π΅) dπ¦) |
73 | 1, 2, 42 | iblabsnc 36145 |
. . . . . . . . . 10
β’ (π β (π₯ β π΄ β¦ (absβπ΅)) β
πΏ1) |
74 | 38, 73 | eqeltrrid 2843 |
. . . . . . . . 9
β’ (π β (π¦ β π΄ β¦ (absββ¦π¦ / π₯β¦π΅)) β
πΏ1) |
75 | 54 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β π΄) β (absββ«π΄π΅ dπ₯) β β) |
76 | | fconstmpt 5695 |
. . . . . . . . . . . 12
β’ (π΄ Γ {(absββ«π΄π΅ dπ₯)}) = (π¦ β π΄ β¦ (absββ«π΄π΅ dπ₯)) |
77 | 76 | a1i 11 |
. . . . . . . . . . 11
β’ (π β (π΄ Γ {(absββ«π΄π΅ dπ₯)}) = (π¦ β π΄ β¦ (absββ«π΄π΅ dπ₯))) |
78 | 29, 75, 31, 77, 39 | offval2 7638 |
. . . . . . . . . 10
β’ (π β ((π΄ Γ {(absββ«π΄π΅ dπ₯)}) βf Β· (π₯ β π΄ β¦ (absβπ΅))) = (π¦ β π΄ β¦ ((absββ«π΄π΅ dπ₯) Β· (absββ¦π¦ / π₯β¦π΅)))) |
79 | 42, 54, 46 | mbfmulc2re 25015 |
. . . . . . . . . 10
β’ (π β ((π΄ Γ {(absββ«π΄π΅ dπ₯)}) βf Β· (π₯ β π΄ β¦ (absβπ΅))) β MblFn) |
80 | 78, 79 | eqeltrrd 2839 |
. . . . . . . . 9
β’ (π β (π¦ β π΄ β¦ ((absββ«π΄π΅ dπ₯) Β· (absββ¦π¦ / π₯β¦π΅))) β MblFn) |
81 | 55, 31, 74, 80 | itgmulc2nc 36149 |
. . . . . . . 8
β’ (π β ((absββ«π΄π΅ dπ₯) Β· β«π΄(absββ¦π¦ / π₯β¦π΅) dπ¦) = β«π΄((absββ«π΄π΅ dπ₯) Β· (absββ¦π¦ / π₯β¦π΅)) dπ¦) |
82 | 3 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β π΄) β β«π΄π΅ dπ₯ β β) |
83 | 82 | abscjd 15336 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β π΄) β
(absβ(βββ«π΄π΅ dπ₯)) = (absββ«π΄π΅ dπ₯)) |
84 | 83 | oveq1d 7373 |
. . . . . . . . . 10
β’ ((π β§ π¦ β π΄) β
((absβ(βββ«π΄π΅ dπ₯)) Β· (absββ¦π¦ / π₯β¦π΅)) = ((absββ«π΄π΅ dπ₯) Β· (absββ¦π¦ / π₯β¦π΅))) |
85 | 27, 84 | eqtrd 2777 |
. . . . . . . . 9
β’ ((π β§ π¦ β π΄) β
(absβ((βββ«π΄π΅ dπ₯) Β· β¦π¦ / π₯β¦π΅)) = ((absββ«π΄π΅ dπ₯) Β· (absββ¦π¦ / π₯β¦π΅))) |
86 | 85 | itgeq2dv 25149 |
. . . . . . . 8
β’ (π β β«π΄(absβ((βββ«π΄π΅ dπ₯) Β· β¦π¦ / π₯β¦π΅)) dπ¦ = β«π΄((absββ«π΄π΅ dπ₯) Β· (absββ¦π¦ / π₯β¦π΅)) dπ¦) |
87 | 81, 86 | eqtr4d 2780 |
. . . . . . 7
β’ (π β ((absββ«π΄π΅ dπ₯) Β· β«π΄(absββ¦π¦ / π₯β¦π΅) dπ¦) = β«π΄(absβ((βββ«π΄π΅ dπ₯) Β· β¦π¦ / π₯β¦π΅)) dπ¦) |
88 | 72, 87 | eqtrid 2789 |
. . . . . 6
β’ (π β ((absββ«π΄π΅ dπ₯) Β· β«π΄(absβπ΅) dπ₯) = β«π΄(absβ((βββ«π΄π΅ dπ₯) Β· β¦π¦ / π₯β¦π΅)) dπ¦) |
89 | 53, 70, 88 | 3brtr4d 5138 |
. . . . 5
β’ (π β ((absββ«π΄π΅ dπ₯) Β· (absββ«π΄π΅ dπ₯)) β€ ((absββ«π΄π΅ dπ₯) Β· β«π΄(absβπ΅) dπ₯)) |
90 | 89 | adantr 482 |
. . . 4
β’ ((π β§ 0 <
(absββ«π΄π΅ dπ₯)) β ((absββ«π΄π΅ dπ₯) Β· (absββ«π΄π΅ dπ₯)) β€ ((absββ«π΄π΅ dπ₯) Β· β«π΄(absβπ΅) dπ₯)) |
91 | 54 | adantr 482 |
. . . . 5
β’ ((π β§ 0 <
(absββ«π΄π΅ dπ₯)) β (absββ«π΄π΅ dπ₯) β β) |
92 | 44, 73 | itgrecl 25165 |
. . . . . 6
β’ (π β β«π΄(absβπ΅) dπ₯ β β) |
93 | 92 | adantr 482 |
. . . . 5
β’ ((π β§ 0 <
(absββ«π΄π΅ dπ₯)) β β«π΄(absβπ΅) dπ₯ β β) |
94 | | simpr 486 |
. . . . 5
β’ ((π β§ 0 <
(absββ«π΄π΅ dπ₯)) β 0 < (absββ«π΄π΅ dπ₯)) |
95 | | lemul2 12009 |
. . . . 5
β’
(((absββ«π΄π΅ dπ₯) β β β§ β«π΄(absβπ΅) dπ₯ β β β§ ((absββ«π΄π΅ dπ₯) β β β§ 0 <
(absββ«π΄π΅ dπ₯))) β ((absββ«π΄π΅ dπ₯) β€ β«π΄(absβπ΅) dπ₯ β ((absββ«π΄π΅ dπ₯) Β· (absββ«π΄π΅ dπ₯)) β€ ((absββ«π΄π΅ dπ₯) Β· β«π΄(absβπ΅) dπ₯))) |
96 | 91, 93, 91, 94, 95 | syl112anc 1375 |
. . . 4
β’ ((π β§ 0 <
(absββ«π΄π΅ dπ₯)) β ((absββ«π΄π΅ dπ₯) β€ β«π΄(absβπ΅) dπ₯ β ((absββ«π΄π΅ dπ₯) Β· (absββ«π΄π΅ dπ₯)) β€ ((absββ«π΄π΅ dπ₯) Β· β«π΄(absβπ΅) dπ₯))) |
97 | 90, 96 | mpbird 257 |
. . 3
β’ ((π β§ 0 <
(absββ«π΄π΅ dπ₯)) β (absββ«π΄π΅ dπ₯) β€ β«π΄(absβπ΅) dπ₯) |
98 | 97 | ex 414 |
. 2
β’ (π β (0 <
(absββ«π΄π΅ dπ₯) β (absββ«π΄π΅ dπ₯) β€ β«π΄(absβπ΅) dπ₯)) |
99 | 7 | absge0d 15330 |
. . . 4
β’ ((π β§ π₯ β π΄) β 0 β€ (absβπ΅)) |
100 | 73, 44, 99 | itgge0 25178 |
. . 3
β’ (π β 0 β€ β«π΄(absβπ΅) dπ₯) |
101 | | breq1 5109 |
. . 3
β’ (0 =
(absββ«π΄π΅ dπ₯) β (0 β€ β«π΄(absβπ΅) dπ₯ β (absββ«π΄π΅ dπ₯) β€ β«π΄(absβπ΅) dπ₯)) |
102 | 100, 101 | syl5ibcom 244 |
. 2
β’ (π β (0 = (absββ«π΄π΅ dπ₯) β (absββ«π΄π΅ dπ₯) β€ β«π΄(absβπ΅) dπ₯)) |
103 | 3 | absge0d 15330 |
. . 3
β’ (π β 0 β€
(absββ«π΄π΅ dπ₯)) |
104 | | 0re 11158 |
. . . 4
β’ 0 β
β |
105 | | leloe 11242 |
. . . 4
β’ ((0
β β β§ (absββ«π΄π΅ dπ₯) β β) β (0 β€
(absββ«π΄π΅ dπ₯) β (0 < (absββ«π΄π΅ dπ₯) β¨ 0 = (absββ«π΄π΅ dπ₯)))) |
106 | 104, 54, 105 | sylancr 588 |
. . 3
β’ (π β (0 β€
(absββ«π΄π΅ dπ₯) β (0 < (absββ«π΄π΅ dπ₯) β¨ 0 = (absββ«π΄π΅ dπ₯)))) |
107 | 103, 106 | mpbid 231 |
. 2
β’ (π β (0 <
(absββ«π΄π΅ dπ₯) β¨ 0 = (absββ«π΄π΅ dπ₯))) |
108 | 98, 102, 107 | mpjaod 859 |
1
β’ (π β (absββ«π΄π΅ dπ₯) β€ β«π΄(absβπ΅) dπ₯) |