Step | Hyp | Ref
| Expression |
1 | | ffvelcdm 7028 |
. . . . . . . . . 10
β’ ((πΊ:ββΆβ β§
π‘ β β) β
(πΊβπ‘) β β) |
2 | 1 | recnd 11117 |
. . . . . . . . 9
β’ ((πΊ:ββΆβ β§
π‘ β β) β
(πΊβπ‘) β β) |
3 | | i1ff 24962 |
. . . . . . . . . . 11
β’ (πΉ β dom β«1
β πΉ:ββΆβ) |
4 | 3 | ffvelcdmda 7030 |
. . . . . . . . . 10
β’ ((πΉ β dom β«1
β§ π‘ β β)
β (πΉβπ‘) β
β) |
5 | 4 | recnd 11117 |
. . . . . . . . 9
β’ ((πΉ β dom β«1
β§ π‘ β β)
β (πΉβπ‘) β
β) |
6 | | subcl 11334 |
. . . . . . . . 9
β’ (((πΊβπ‘) β β β§ (πΉβπ‘) β β) β ((πΊβπ‘) β (πΉβπ‘)) β β) |
7 | 2, 5, 6 | syl2anr 598 |
. . . . . . . 8
β’ (((πΉ β dom β«1
β§ π‘ β β)
β§ (πΊ:ββΆβ β§ π‘ β β)) β ((πΊβπ‘) β (πΉβπ‘)) β β) |
8 | 7 | anandirs 678 |
. . . . . . 7
β’ (((πΉ β dom β«1
β§ πΊ:ββΆβ) β§ π‘ β β) β ((πΊβπ‘) β (πΉβπ‘)) β β) |
9 | 8 | abscld 15256 |
. . . . . 6
β’ (((πΉ β dom β«1
β§ πΊ:ββΆβ) β§ π‘ β β) β
(absβ((πΊβπ‘) β (πΉβπ‘))) β β) |
10 | 9 | rexrd 11139 |
. . . . 5
β’ (((πΉ β dom β«1
β§ πΊ:ββΆβ) β§ π‘ β β) β
(absβ((πΊβπ‘) β (πΉβπ‘))) β
β*) |
11 | 8 | absge0d 15264 |
. . . . 5
β’ (((πΉ β dom β«1
β§ πΊ:ββΆβ) β§ π‘ β β) β 0 β€
(absβ((πΊβπ‘) β (πΉβπ‘)))) |
12 | | elxrge0 13303 |
. . . . 5
β’
((absβ((πΊβπ‘) β (πΉβπ‘))) β (0[,]+β) β
((absβ((πΊβπ‘) β (πΉβπ‘))) β β* β§ 0 β€
(absβ((πΊβπ‘) β (πΉβπ‘))))) |
13 | 10, 11, 12 | sylanbrc 584 |
. . . 4
β’ (((πΉ β dom β«1
β§ πΊ:ββΆβ) β§ π‘ β β) β
(absβ((πΊβπ‘) β (πΉβπ‘))) β (0[,]+β)) |
14 | 13 | fmpttd 7058 |
. . 3
β’ ((πΉ β dom β«1
β§ πΊ:ββΆβ) β (π‘ β β β¦
(absβ((πΊβπ‘) β (πΉβπ‘)))):ββΆ(0[,]+β)) |
15 | 14 | 3adant2 1132 |
. 2
β’ ((πΉ β dom β«1
β§ πΊ β
πΏ1 β§ πΊ:ββΆβ) β (π‘ β β β¦
(absβ((πΊβπ‘) β (πΉβπ‘)))):ββΆ(0[,]+β)) |
16 | | reex 11076 |
. . . . . . 7
β’ β
β V |
17 | 16 | a1i 11 |
. . . . . 6
β’ ((πΉ β dom β«1
β§ πΊ β
πΏ1 β§ πΊ:ββΆβ) β β
β V) |
18 | | fvexd 6853 |
. . . . . 6
β’ (((πΉ β dom β«1
β§ πΊ β
πΏ1 β§ πΊ:ββΆβ) β§ π‘ β β) β
(absβ(πΊβπ‘)) β V) |
19 | | fvexd 6853 |
. . . . . 6
β’ (((πΉ β dom β«1
β§ πΊ β
πΏ1 β§ πΊ:ββΆβ) β§ π‘ β β) β
(absβ(πΉβπ‘)) β V) |
20 | | eqidd 2739 |
. . . . . 6
β’ ((πΉ β dom β«1
β§ πΊ β
πΏ1 β§ πΊ:ββΆβ) β (π‘ β β β¦
(absβ(πΊβπ‘))) = (π‘ β β β¦ (absβ(πΊβπ‘)))) |
21 | | eqidd 2739 |
. . . . . 6
β’ ((πΉ β dom β«1
β§ πΊ β
πΏ1 β§ πΊ:ββΆβ) β (π‘ β β β¦
(absβ(πΉβπ‘))) = (π‘ β β β¦ (absβ(πΉβπ‘)))) |
22 | 17, 18, 19, 20, 21 | offval2 7628 |
. . . . 5
β’ ((πΉ β dom β«1
β§ πΊ β
πΏ1 β§ πΊ:ββΆβ) β ((π‘ β β β¦
(absβ(πΊβπ‘))) βf + (π‘ β β β¦
(absβ(πΉβπ‘)))) = (π‘ β β β¦ ((absβ(πΊβπ‘)) + (absβ(πΉβπ‘))))) |
23 | 22 | fveq2d 6842 |
. . . 4
β’ ((πΉ β dom β«1
β§ πΊ β
πΏ1 β§ πΊ:ββΆβ) β
(β«2β((π‘ β β β¦ (absβ(πΊβπ‘))) βf + (π‘ β β β¦ (absβ(πΉβπ‘))))) = (β«2β(π‘ β β β¦
((absβ(πΊβπ‘)) + (absβ(πΉβπ‘)))))) |
24 | | id 22 |
. . . . . . . . . 10
β’ (πΊ:ββΆβ β
πΊ:ββΆβ) |
25 | 24 | feqmptd 6906 |
. . . . . . . . 9
β’ (πΊ:ββΆβ β
πΊ = (π‘ β β β¦ (πΊβπ‘))) |
26 | | absf 15157 |
. . . . . . . . . . 11
β’
abs:ββΆβ |
27 | 26 | a1i 11 |
. . . . . . . . . 10
β’ (πΊ:ββΆβ β
abs:ββΆβ) |
28 | 27 | feqmptd 6906 |
. . . . . . . . 9
β’ (πΊ:ββΆβ β
abs = (π₯ β β
β¦ (absβπ₯))) |
29 | | fveq2 6838 |
. . . . . . . . 9
β’ (π₯ = (πΊβπ‘) β (absβπ₯) = (absβ(πΊβπ‘))) |
30 | 2, 25, 28, 29 | fmptco 7070 |
. . . . . . . 8
β’ (πΊ:ββΆβ β
(abs β πΊ) = (π‘ β β β¦
(absβ(πΊβπ‘)))) |
31 | 30 | adantl 483 |
. . . . . . 7
β’ ((πΊ β πΏ1
β§ πΊ:ββΆβ) β (abs β
πΊ) = (π‘ β β β¦ (absβ(πΊβπ‘)))) |
32 | | iblmbf 25054 |
. . . . . . . . 9
β’ (πΊ β πΏ1
β πΊ β
MblFn) |
33 | | ftc1anclem1 36037 |
. . . . . . . . 9
β’ ((πΊ:ββΆβ β§
πΊ β MblFn) β (abs
β πΊ) β
MblFn) |
34 | 32, 33 | sylan2 594 |
. . . . . . . 8
β’ ((πΊ:ββΆβ β§
πΊ β
πΏ1) β (abs β πΊ) β MblFn) |
35 | 34 | ancoms 460 |
. . . . . . 7
β’ ((πΊ β πΏ1
β§ πΊ:ββΆβ) β (abs β
πΊ) β
MblFn) |
36 | 31, 35 | eqeltrrd 2840 |
. . . . . 6
β’ ((πΊ β πΏ1
β§ πΊ:ββΆβ) β (π‘ β β β¦
(absβ(πΊβπ‘))) β
MblFn) |
37 | 36 | 3adant1 1131 |
. . . . 5
β’ ((πΉ β dom β«1
β§ πΊ β
πΏ1 β§ πΊ:ββΆβ) β (π‘ β β β¦
(absβ(πΊβπ‘))) β
MblFn) |
38 | 2 | abscld 15256 |
. . . . . . . 8
β’ ((πΊ:ββΆβ β§
π‘ β β) β
(absβ(πΊβπ‘)) β
β) |
39 | 2 | absge0d 15264 |
. . . . . . . 8
β’ ((πΊ:ββΆβ β§
π‘ β β) β 0
β€ (absβ(πΊβπ‘))) |
40 | | elrege0 13300 |
. . . . . . . 8
β’
((absβ(πΊβπ‘)) β (0[,)+β) β
((absβ(πΊβπ‘)) β β β§ 0 β€
(absβ(πΊβπ‘)))) |
41 | 38, 39, 40 | sylanbrc 584 |
. . . . . . 7
β’ ((πΊ:ββΆβ β§
π‘ β β) β
(absβ(πΊβπ‘)) β
(0[,)+β)) |
42 | 41 | fmpttd 7058 |
. . . . . 6
β’ (πΊ:ββΆβ β
(π‘ β β β¦
(absβ(πΊβπ‘))):ββΆ(0[,)+β)) |
43 | 42 | 3ad2ant3 1136 |
. . . . 5
β’ ((πΉ β dom β«1
β§ πΊ β
πΏ1 β§ πΊ:ββΆβ) β (π‘ β β β¦
(absβ(πΊβπ‘))):ββΆ(0[,)+β)) |
44 | | iftrue 4491 |
. . . . . . . . 9
β’ (π‘ β β β if(π‘ β β,
(absβ(πΊβπ‘)), 0) = (absβ(πΊβπ‘))) |
45 | 44 | mpteq2ia 5207 |
. . . . . . . 8
β’ (π‘ β β β¦ if(π‘ β β,
(absβ(πΊβπ‘)), 0)) = (π‘ β β β¦ (absβ(πΊβπ‘))) |
46 | 45 | fveq2i 6841 |
. . . . . . 7
β’
(β«2β(π‘ β β β¦ if(π‘ β β, (absβ(πΊβπ‘)), 0))) = (β«2β(π‘ β β β¦
(absβ(πΊβπ‘)))) |
47 | 1 | adantll 713 |
. . . . . . . . . 10
β’ (((πΊ β πΏ1
β§ πΊ:ββΆβ) β§ π‘ β β) β (πΊβπ‘) β β) |
48 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((πΊ β πΏ1
β§ πΊ:ββΆβ) β πΊ:ββΆβ) |
49 | 48 | feqmptd 6906 |
. . . . . . . . . . 11
β’ ((πΊ β πΏ1
β§ πΊ:ββΆβ) β πΊ = (π‘ β β β¦ (πΊβπ‘))) |
50 | | simpl 484 |
. . . . . . . . . . 11
β’ ((πΊ β πΏ1
β§ πΊ:ββΆβ) β πΊ β
πΏ1) |
51 | 49, 50 | eqeltrrd 2840 |
. . . . . . . . . 10
β’ ((πΊ β πΏ1
β§ πΊ:ββΆβ) β (π‘ β β β¦ (πΊβπ‘)) β
πΏ1) |
52 | 47, 51, 36 | iblabsnc 36028 |
. . . . . . . . 9
β’ ((πΊ β πΏ1
β§ πΊ:ββΆβ) β (π‘ β β β¦
(absβ(πΊβπ‘))) β
πΏ1) |
53 | 38 | adantll 713 |
. . . . . . . . . 10
β’ (((πΊ β πΏ1
β§ πΊ:ββΆβ) β§ π‘ β β) β
(absβ(πΊβπ‘)) β
β) |
54 | 39 | adantll 713 |
. . . . . . . . . 10
β’ (((πΊ β πΏ1
β§ πΊ:ββΆβ) β§ π‘ β β) β 0 β€
(absβ(πΊβπ‘))) |
55 | 53, 54 | iblpos 25079 |
. . . . . . . . 9
β’ ((πΊ β πΏ1
β§ πΊ:ββΆβ) β ((π‘ β β β¦
(absβ(πΊβπ‘))) β πΏ1
β ((π‘ β β
β¦ (absβ(πΊβπ‘))) β MblFn β§
(β«2β(π‘
β β β¦ if(π‘
β β, (absβ(πΊβπ‘)), 0))) β β))) |
56 | 52, 55 | mpbid 231 |
. . . . . . . 8
β’ ((πΊ β πΏ1
β§ πΊ:ββΆβ) β ((π‘ β β β¦
(absβ(πΊβπ‘))) β MblFn β§
(β«2β(π‘
β β β¦ if(π‘
β β, (absβ(πΊβπ‘)), 0))) β β)) |
57 | 56 | simprd 497 |
. . . . . . 7
β’ ((πΊ β πΏ1
β§ πΊ:ββΆβ) β
(β«2β(π‘
β β β¦ if(π‘
β β, (absβ(πΊβπ‘)), 0))) β β) |
58 | 46, 57 | eqeltrrid 2844 |
. . . . . 6
β’ ((πΊ β πΏ1
β§ πΊ:ββΆβ) β
(β«2β(π‘
β β β¦ (absβ(πΊβπ‘)))) β β) |
59 | 58 | 3adant1 1131 |
. . . . 5
β’ ((πΉ β dom β«1
β§ πΊ β
πΏ1 β§ πΊ:ββΆβ) β
(β«2β(π‘
β β β¦ (absβ(πΊβπ‘)))) β β) |
60 | 5 | abscld 15256 |
. . . . . . . 8
β’ ((πΉ β dom β«1
β§ π‘ β β)
β (absβ(πΉβπ‘)) β β) |
61 | 5 | absge0d 15264 |
. . . . . . . 8
β’ ((πΉ β dom β«1
β§ π‘ β β)
β 0 β€ (absβ(πΉβπ‘))) |
62 | | elrege0 13300 |
. . . . . . . 8
β’
((absβ(πΉβπ‘)) β (0[,)+β) β
((absβ(πΉβπ‘)) β β β§ 0 β€
(absβ(πΉβπ‘)))) |
63 | 60, 61, 62 | sylanbrc 584 |
. . . . . . 7
β’ ((πΉ β dom β«1
β§ π‘ β β)
β (absβ(πΉβπ‘)) β (0[,)+β)) |
64 | 63 | fmpttd 7058 |
. . . . . 6
β’ (πΉ β dom β«1
β (π‘ β β
β¦ (absβ(πΉβπ‘))):ββΆ(0[,)+β)) |
65 | 64 | 3ad2ant1 1134 |
. . . . 5
β’ ((πΉ β dom β«1
β§ πΊ β
πΏ1 β§ πΊ:ββΆβ) β (π‘ β β β¦
(absβ(πΉβπ‘))):ββΆ(0[,)+β)) |
66 | | iftrue 4491 |
. . . . . . . . 9
β’ (π‘ β β β if(π‘ β β,
(absβ(πΉβπ‘)), 0) = (absβ(πΉβπ‘))) |
67 | 66 | mpteq2ia 5207 |
. . . . . . . 8
β’ (π‘ β β β¦ if(π‘ β β,
(absβ(πΉβπ‘)), 0)) = (π‘ β β β¦ (absβ(πΉβπ‘))) |
68 | 67 | fveq2i 6841 |
. . . . . . 7
β’
(β«2β(π‘ β β β¦ if(π‘ β β, (absβ(πΉβπ‘)), 0))) = (β«2β(π‘ β β β¦
(absβ(πΉβπ‘)))) |
69 | 3 | feqmptd 6906 |
. . . . . . . . . . 11
β’ (πΉ β dom β«1
β πΉ = (π‘ β β β¦ (πΉβπ‘))) |
70 | | i1fibl 25094 |
. . . . . . . . . . 11
β’ (πΉ β dom β«1
β πΉ β
πΏ1) |
71 | 69, 70 | eqeltrrd 2840 |
. . . . . . . . . 10
β’ (πΉ β dom β«1
β (π‘ β β
β¦ (πΉβπ‘)) β
πΏ1) |
72 | 26 | a1i 11 |
. . . . . . . . . . . . 13
β’ (πΉ β dom β«1
β abs:ββΆβ) |
73 | 72 | feqmptd 6906 |
. . . . . . . . . . . 12
β’ (πΉ β dom β«1
β abs = (π₯ β
β β¦ (absβπ₯))) |
74 | | fveq2 6838 |
. . . . . . . . . . . 12
β’ (π₯ = (πΉβπ‘) β (absβπ₯) = (absβ(πΉβπ‘))) |
75 | 5, 69, 73, 74 | fmptco 7070 |
. . . . . . . . . . 11
β’ (πΉ β dom β«1
β (abs β πΉ) =
(π‘ β β β¦
(absβ(πΉβπ‘)))) |
76 | | i1fmbf 24961 |
. . . . . . . . . . . 12
β’ (πΉ β dom β«1
β πΉ β
MblFn) |
77 | | ftc1anclem1 36037 |
. . . . . . . . . . . 12
β’ ((πΉ:ββΆβ β§
πΉ β MblFn) β (abs
β πΉ) β
MblFn) |
78 | 3, 76, 77 | syl2anc 585 |
. . . . . . . . . . 11
β’ (πΉ β dom β«1
β (abs β πΉ)
β MblFn) |
79 | 75, 78 | eqeltrrd 2840 |
. . . . . . . . . 10
β’ (πΉ β dom β«1
β (π‘ β β
β¦ (absβ(πΉβπ‘))) β MblFn) |
80 | 4, 71, 79 | iblabsnc 36028 |
. . . . . . . . 9
β’ (πΉ β dom β«1
β (π‘ β β
β¦ (absβ(πΉβπ‘))) β
πΏ1) |
81 | 60, 61 | iblpos 25079 |
. . . . . . . . 9
β’ (πΉ β dom β«1
β ((π‘ β β
β¦ (absβ(πΉβπ‘))) β πΏ1 β
((π‘ β β β¦
(absβ(πΉβπ‘))) β MblFn β§
(β«2β(π‘
β β β¦ if(π‘
β β, (absβ(πΉβπ‘)), 0))) β β))) |
82 | 80, 81 | mpbid 231 |
. . . . . . . 8
β’ (πΉ β dom β«1
β ((π‘ β β
β¦ (absβ(πΉβπ‘))) β MblFn β§
(β«2β(π‘
β β β¦ if(π‘
β β, (absβ(πΉβπ‘)), 0))) β β)) |
83 | 82 | simprd 497 |
. . . . . . 7
β’ (πΉ β dom β«1
β (β«2β(π‘ β β β¦ if(π‘ β β, (absβ(πΉβπ‘)), 0))) β β) |
84 | 68, 83 | eqeltrrid 2844 |
. . . . . 6
β’ (πΉ β dom β«1
β (β«2β(π‘ β β β¦ (absβ(πΉβπ‘)))) β β) |
85 | 84 | 3ad2ant1 1134 |
. . . . 5
β’ ((πΉ β dom β«1
β§ πΊ β
πΏ1 β§ πΊ:ββΆβ) β
(β«2β(π‘
β β β¦ (absβ(πΉβπ‘)))) β β) |
86 | 37, 43, 59, 65, 85 | itg2addnc 36018 |
. . . 4
β’ ((πΉ β dom β«1
β§ πΊ β
πΏ1 β§ πΊ:ββΆβ) β
(β«2β((π‘ β β β¦ (absβ(πΊβπ‘))) βf + (π‘ β β β¦ (absβ(πΉβπ‘))))) = ((β«2β(π‘ β β β¦
(absβ(πΊβπ‘)))) +
(β«2β(π‘
β β β¦ (absβ(πΉβπ‘)))))) |
87 | 23, 86 | eqtr3d 2780 |
. . 3
β’ ((πΉ β dom β«1
β§ πΊ β
πΏ1 β§ πΊ:ββΆβ) β
(β«2β(π‘
β β β¦ ((absβ(πΊβπ‘)) + (absβ(πΉβπ‘))))) = ((β«2β(π‘ β β β¦
(absβ(πΊβπ‘)))) +
(β«2β(π‘
β β β¦ (absβ(πΉβπ‘)))))) |
88 | 59, 85 | readdcld 11118 |
. . 3
β’ ((πΉ β dom β«1
β§ πΊ β
πΏ1 β§ πΊ:ββΆβ) β
((β«2β(π‘ β β β¦ (absβ(πΊβπ‘)))) + (β«2β(π‘ β β β¦
(absβ(πΉβπ‘))))) β
β) |
89 | 87, 88 | eqeltrd 2839 |
. 2
β’ ((πΉ β dom β«1
β§ πΊ β
πΏ1 β§ πΊ:ββΆβ) β
(β«2β(π‘
β β β¦ ((absβ(πΊβπ‘)) + (absβ(πΉβπ‘))))) β β) |
90 | | readdcl 11068 |
. . . . . . . . 9
β’
(((absβ(πΊβπ‘)) β β β§ (absβ(πΉβπ‘)) β β) β ((absβ(πΊβπ‘)) + (absβ(πΉβπ‘))) β β) |
91 | 38, 60, 90 | syl2anr 598 |
. . . . . . . 8
β’ (((πΉ β dom β«1
β§ π‘ β β)
β§ (πΊ:ββΆβ β§ π‘ β β)) β
((absβ(πΊβπ‘)) + (absβ(πΉβπ‘))) β β) |
92 | 91 | anandirs 678 |
. . . . . . 7
β’ (((πΉ β dom β«1
β§ πΊ:ββΆβ) β§ π‘ β β) β
((absβ(πΊβπ‘)) + (absβ(πΉβπ‘))) β β) |
93 | 92 | rexrd 11139 |
. . . . . 6
β’ (((πΉ β dom β«1
β§ πΊ:ββΆβ) β§ π‘ β β) β
((absβ(πΊβπ‘)) + (absβ(πΉβπ‘))) β
β*) |
94 | 38 | adantll 713 |
. . . . . . 7
β’ (((πΉ β dom β«1
β§ πΊ:ββΆβ) β§ π‘ β β) β
(absβ(πΊβπ‘)) β
β) |
95 | 60 | adantlr 714 |
. . . . . . 7
β’ (((πΉ β dom β«1
β§ πΊ:ββΆβ) β§ π‘ β β) β
(absβ(πΉβπ‘)) β
β) |
96 | 39 | adantll 713 |
. . . . . . 7
β’ (((πΉ β dom β«1
β§ πΊ:ββΆβ) β§ π‘ β β) β 0 β€
(absβ(πΊβπ‘))) |
97 | 61 | adantlr 714 |
. . . . . . 7
β’ (((πΉ β dom β«1
β§ πΊ:ββΆβ) β§ π‘ β β) β 0 β€
(absβ(πΉβπ‘))) |
98 | 94, 95, 96, 97 | addge0d 11665 |
. . . . . 6
β’ (((πΉ β dom β«1
β§ πΊ:ββΆβ) β§ π‘ β β) β 0 β€
((absβ(πΊβπ‘)) + (absβ(πΉβπ‘)))) |
99 | | elxrge0 13303 |
. . . . . 6
β’
(((absβ(πΊβπ‘)) + (absβ(πΉβπ‘))) β (0[,]+β) β
(((absβ(πΊβπ‘)) + (absβ(πΉβπ‘))) β β* β§ 0 β€
((absβ(πΊβπ‘)) + (absβ(πΉβπ‘))))) |
100 | 93, 98, 99 | sylanbrc 584 |
. . . . 5
β’ (((πΉ β dom β«1
β§ πΊ:ββΆβ) β§ π‘ β β) β
((absβ(πΊβπ‘)) + (absβ(πΉβπ‘))) β (0[,]+β)) |
101 | 100 | fmpttd 7058 |
. . . 4
β’ ((πΉ β dom β«1
β§ πΊ:ββΆβ) β (π‘ β β β¦
((absβ(πΊβπ‘)) + (absβ(πΉβπ‘)))):ββΆ(0[,]+β)) |
102 | 101 | 3adant2 1132 |
. . 3
β’ ((πΉ β dom β«1
β§ πΊ β
πΏ1 β§ πΊ:ββΆβ) β (π‘ β β β¦
((absβ(πΊβπ‘)) + (absβ(πΉβπ‘)))):ββΆ(0[,]+β)) |
103 | | abs2dif2 15153 |
. . . . . . . 8
β’ (((πΊβπ‘) β β β§ (πΉβπ‘) β β) β (absβ((πΊβπ‘) β (πΉβπ‘))) β€ ((absβ(πΊβπ‘)) + (absβ(πΉβπ‘)))) |
104 | 2, 5, 103 | syl2anr 598 |
. . . . . . 7
β’ (((πΉ β dom β«1
β§ π‘ β β)
β§ (πΊ:ββΆβ β§ π‘ β β)) β
(absβ((πΊβπ‘) β (πΉβπ‘))) β€ ((absβ(πΊβπ‘)) + (absβ(πΉβπ‘)))) |
105 | 104 | anandirs 678 |
. . . . . 6
β’ (((πΉ β dom β«1
β§ πΊ:ββΆβ) β§ π‘ β β) β
(absβ((πΊβπ‘) β (πΉβπ‘))) β€ ((absβ(πΊβπ‘)) + (absβ(πΉβπ‘)))) |
106 | 105 | ralrimiva 3142 |
. . . . 5
β’ ((πΉ β dom β«1
β§ πΊ:ββΆβ) β
βπ‘ β β
(absβ((πΊβπ‘) β (πΉβπ‘))) β€ ((absβ(πΊβπ‘)) + (absβ(πΉβπ‘)))) |
107 | 16 | a1i 11 |
. . . . . 6
β’ ((πΉ β dom β«1
β§ πΊ:ββΆβ) β β
β V) |
108 | | eqidd 2739 |
. . . . . 6
β’ ((πΉ β dom β«1
β§ πΊ:ββΆβ) β (π‘ β β β¦
(absβ((πΊβπ‘) β (πΉβπ‘)))) = (π‘ β β β¦ (absβ((πΊβπ‘) β (πΉβπ‘))))) |
109 | | eqidd 2739 |
. . . . . 6
β’ ((πΉ β dom β«1
β§ πΊ:ββΆβ) β (π‘ β β β¦
((absβ(πΊβπ‘)) + (absβ(πΉβπ‘)))) = (π‘ β β β¦ ((absβ(πΊβπ‘)) + (absβ(πΉβπ‘))))) |
110 | 107, 9, 92, 108, 109 | ofrfval2 7629 |
. . . . 5
β’ ((πΉ β dom β«1
β§ πΊ:ββΆβ) β ((π‘ β β β¦
(absβ((πΊβπ‘) β (πΉβπ‘)))) βr β€ (π‘ β β β¦
((absβ(πΊβπ‘)) + (absβ(πΉβπ‘)))) β βπ‘ β β (absβ((πΊβπ‘) β (πΉβπ‘))) β€ ((absβ(πΊβπ‘)) + (absβ(πΉβπ‘))))) |
111 | 106, 110 | mpbird 257 |
. . . 4
β’ ((πΉ β dom β«1
β§ πΊ:ββΆβ) β (π‘ β β β¦
(absβ((πΊβπ‘) β (πΉβπ‘)))) βr β€ (π‘ β β β¦
((absβ(πΊβπ‘)) + (absβ(πΉβπ‘))))) |
112 | 111 | 3adant2 1132 |
. . 3
β’ ((πΉ β dom β«1
β§ πΊ β
πΏ1 β§ πΊ:ββΆβ) β (π‘ β β β¦
(absβ((πΊβπ‘) β (πΉβπ‘)))) βr β€ (π‘ β β β¦
((absβ(πΊβπ‘)) + (absβ(πΉβπ‘))))) |
113 | | itg2le 25026 |
. . 3
β’ (((π‘ β β β¦
(absβ((πΊβπ‘) β (πΉβπ‘)))):ββΆ(0[,]+β) β§
(π‘ β β β¦
((absβ(πΊβπ‘)) + (absβ(πΉβπ‘)))):ββΆ(0[,]+β) β§
(π‘ β β β¦
(absβ((πΊβπ‘) β (πΉβπ‘)))) βr β€ (π‘ β β β¦
((absβ(πΊβπ‘)) + (absβ(πΉβπ‘))))) β (β«2β(π‘ β β β¦
(absβ((πΊβπ‘) β (πΉβπ‘))))) β€ (β«2β(π‘ β β β¦
((absβ(πΊβπ‘)) + (absβ(πΉβπ‘)))))) |
114 | 15, 102, 112, 113 | syl3anc 1372 |
. 2
β’ ((πΉ β dom β«1
β§ πΊ β
πΏ1 β§ πΊ:ββΆβ) β
(β«2β(π‘
β β β¦ (absβ((πΊβπ‘) β (πΉβπ‘))))) β€ (β«2β(π‘ β β β¦
((absβ(πΊβπ‘)) + (absβ(πΉβπ‘)))))) |
115 | | itg2lecl 25025 |
. 2
β’ (((π‘ β β β¦
(absβ((πΊβπ‘) β (πΉβπ‘)))):ββΆ(0[,]+β) β§
(β«2β(π‘
β β β¦ ((absβ(πΊβπ‘)) + (absβ(πΉβπ‘))))) β β β§
(β«2β(π‘
β β β¦ (absβ((πΊβπ‘) β (πΉβπ‘))))) β€ (β«2β(π‘ β β β¦
((absβ(πΊβπ‘)) + (absβ(πΉβπ‘)))))) β (β«2β(π‘ β β β¦
(absβ((πΊβπ‘) β (πΉβπ‘))))) β β) |
116 | 15, 89, 114, 115 | syl3anc 1372 |
1
β’ ((πΉ β dom β«1
β§ πΊ β
πΏ1 β§ πΊ:ββΆβ) β
(β«2β(π‘
β β β¦ (absβ((πΊβπ‘) β (πΉβπ‘))))) β β) |