Step | Hyp | Ref
| Expression |
1 | | simprr 771 |
. . . . . . 7
β’ ((π β dom β«1
β§ (βπ β
β+ (π§
β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))) β π₯ = (β«1βπ)) |
2 | | itg1cl 25193 |
. . . . . . . 8
β’ (π β dom β«1
β (β«1βπ) β β) |
3 | 2 | adantr 481 |
. . . . . . 7
β’ ((π β dom β«1
β§ (βπ β
β+ (π§
β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))) β
(β«1βπ)
β β) |
4 | 1, 3 | eqeltrd 2833 |
. . . . . 6
β’ ((π β dom β«1
β§ (βπ β
β+ (π§
β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))) β π₯ β β) |
5 | 4 | rexlimiva 3147 |
. . . . 5
β’
(βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ)) β π₯ β β) |
6 | 5 | abssi 4066 |
. . . 4
β’ {π₯ β£ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))} β
β |
7 | 6 | a1i 11 |
. . 3
β’ (π β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))} β
β) |
8 | | i1f0 25195 |
. . . . . 6
β’ (β
Γ {0}) β dom β«1 |
9 | | 3nn 12287 |
. . . . . . . 8
β’ 3 β
β |
10 | | nnrp 12981 |
. . . . . . . 8
β’ (3 β
β β 3 β β+) |
11 | | ne0i 4333 |
. . . . . . . 8
β’ (3 β
β+ β β+ β β
) |
12 | 9, 10, 11 | mp2b 10 |
. . . . . . 7
β’
β+ β β
|
13 | | itg2addnc.f2 |
. . . . . . . . . . . . 13
β’ (π β πΉ:ββΆ(0[,)+β)) |
14 | 13 | ffvelcdmda 7083 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β β) β (πΉβπ§) β (0[,)+β)) |
15 | | elrege0 13427 |
. . . . . . . . . . . 12
β’ ((πΉβπ§) β (0[,)+β) β ((πΉβπ§) β β β§ 0 β€ (πΉβπ§))) |
16 | 14, 15 | sylib 217 |
. . . . . . . . . . 11
β’ ((π β§ π§ β β) β ((πΉβπ§) β β β§ 0 β€ (πΉβπ§))) |
17 | 16 | simprd 496 |
. . . . . . . . . 10
β’ ((π β§ π§ β β) β 0 β€ (πΉβπ§)) |
18 | 17 | ralrimiva 3146 |
. . . . . . . . 9
β’ (π β βπ§ β β 0 β€ (πΉβπ§)) |
19 | | reex 11197 |
. . . . . . . . . . 11
β’ β
β V |
20 | 19 | a1i 11 |
. . . . . . . . . 10
β’ (π β β β
V) |
21 | | c0ex 11204 |
. . . . . . . . . . 11
β’ 0 β
V |
22 | 21 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π§ β β) β 0 β
V) |
23 | | eqidd 2733 |
. . . . . . . . . 10
β’ (π β (π§ β β β¦ 0) = (π§ β β β¦
0)) |
24 | 13 | feqmptd 6957 |
. . . . . . . . . 10
β’ (π β πΉ = (π§ β β β¦ (πΉβπ§))) |
25 | 20, 22, 14, 23, 24 | ofrfval2 7687 |
. . . . . . . . 9
β’ (π β ((π§ β β β¦ 0)
βr β€ πΉ
β βπ§ β
β 0 β€ (πΉβπ§))) |
26 | 18, 25 | mpbird 256 |
. . . . . . . 8
β’ (π β (π§ β β β¦ 0)
βr β€ πΉ) |
27 | 26 | ralrimivw 3150 |
. . . . . . 7
β’ (π β βπ β β+ (π§ β β β¦ 0)
βr β€ πΉ) |
28 | | r19.2z 4493 |
. . . . . . 7
β’
((β+ β β
β§ βπ β β+ (π§ β β β¦ 0)
βr β€ πΉ)
β βπ β
β+ (π§
β β β¦ 0) βr β€ πΉ) |
29 | 12, 27, 28 | sylancr 587 |
. . . . . 6
β’ (π β βπ β β+ (π§ β β β¦ 0)
βr β€ πΉ) |
30 | | fveq2 6888 |
. . . . . . . . . 10
β’ (π = (β Γ {0}) β
(β«1βπ)
= (β«1β(β Γ {0}))) |
31 | | itg10 25196 |
. . . . . . . . . 10
β’
(β«1β(β Γ {0})) = 0 |
32 | 30, 31 | eqtr2di 2789 |
. . . . . . . . 9
β’ (π = (β Γ {0}) β
0 = (β«1βπ)) |
33 | 32 | biantrud 532 |
. . . . . . . 8
β’ (π = (β Γ {0}) β
(βπ β
β+ (π§
β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β (βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ 0 =
(β«1βπ)))) |
34 | | fveq1 6887 |
. . . . . . . . . . . . 13
β’ (π = (β Γ {0}) β
(πβπ§) = ((β Γ {0})βπ§)) |
35 | 21 | fvconst2 7201 |
. . . . . . . . . . . . 13
β’ (π§ β β β ((β
Γ {0})βπ§) =
0) |
36 | 34, 35 | sylan9eq 2792 |
. . . . . . . . . . . 12
β’ ((π = (β Γ {0}) β§
π§ β β) β
(πβπ§) = 0) |
37 | 36 | iftrued 4535 |
. . . . . . . . . . 11
β’ ((π = (β Γ {0}) β§
π§ β β) β
if((πβπ§) = 0, 0, ((πβπ§) + π)) = 0) |
38 | 37 | mpteq2dva 5247 |
. . . . . . . . . 10
β’ (π = (β Γ {0}) β
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) = (π§ β β β¦ 0)) |
39 | 38 | breq1d 5157 |
. . . . . . . . 9
β’ (π = (β Γ {0}) β
((π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β (π§ β β β¦ 0)
βr β€ πΉ)) |
40 | 39 | rexbidv 3178 |
. . . . . . . 8
β’ (π = (β Γ {0}) β
(βπ β
β+ (π§
β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β βπ β β+
(π§ β β β¦
0) βr β€ πΉ)) |
41 | 33, 40 | bitr3d 280 |
. . . . . . 7
β’ (π = (β Γ {0}) β
((βπ β
β+ (π§
β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ 0 =
(β«1βπ)) β βπ β β+ (π§ β β β¦ 0)
βr β€ πΉ)) |
42 | 41 | rspcev 3612 |
. . . . . 6
β’
(((β Γ {0}) β dom β«1 β§ βπ β β+
(π§ β β β¦
0) βr β€ πΉ) β βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ 0 =
(β«1βπ))) |
43 | 8, 29, 42 | sylancr 587 |
. . . . 5
β’ (π β βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ 0 =
(β«1βπ))) |
44 | | eqeq1 2736 |
. . . . . . . 8
β’ (π₯ = 0 β (π₯ = (β«1βπ) β 0 =
(β«1βπ))) |
45 | 44 | anbi2d 629 |
. . . . . . 7
β’ (π₯ = 0 β ((βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ)) β (βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ 0 =
(β«1βπ)))) |
46 | 45 | rexbidv 3178 |
. . . . . 6
β’ (π₯ = 0 β (βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ)) β βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ 0 =
(β«1βπ)))) |
47 | 21, 46 | elab 3667 |
. . . . 5
β’ (0 β
{π₯ β£ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))} β βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ 0 =
(β«1βπ))) |
48 | 43, 47 | sylibr 233 |
. . . 4
β’ (π β 0 β {π₯ β£ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}) |
49 | 48 | ne0d 4334 |
. . 3
β’ (π β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))} β
β
) |
50 | | icossicc 13409 |
. . . . . . 7
β’
(0[,)+β) β (0[,]+β) |
51 | | fss 6731 |
. . . . . . 7
β’ ((πΉ:ββΆ(0[,)+β)
β§ (0[,)+β) β (0[,]+β)) β πΉ:ββΆ(0[,]+β)) |
52 | 50, 51 | mpan2 689 |
. . . . . 6
β’ (πΉ:ββΆ(0[,)+β)
β πΉ:ββΆ(0[,]+β)) |
53 | | eqid 2732 |
. . . . . . 7
β’ {π₯ β£ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))} = {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))} |
54 | 53 | itg2addnclem 36527 |
. . . . . 6
β’ (πΉ:ββΆ(0[,]+β)
β (β«2βπΉ) = sup({π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}, β*, <
)) |
55 | 13, 52, 54 | 3syl 18 |
. . . . 5
β’ (π β
(β«2βπΉ)
= sup({π₯ β£
βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}, β*, <
)) |
56 | | itg2addnc.f3 |
. . . . 5
β’ (π β
(β«2βπΉ)
β β) |
57 | 55, 56 | eqeltrrd 2834 |
. . . 4
β’ (π β sup({π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}, β*, < )
β β) |
58 | | ressxr 11254 |
. . . . . . 7
β’ β
β β* |
59 | 6, 58 | sstri 3990 |
. . . . . 6
β’ {π₯ β£ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))} β
β* |
60 | | supxrub 13299 |
. . . . . 6
β’ (({π₯ β£ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))} β β*
β§ π β {π₯ β£ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}) β π β€ sup({π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}, β*, <
)) |
61 | 59, 60 | mpan 688 |
. . . . 5
β’ (π β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))} β π β€ sup({π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}, β*, <
)) |
62 | 61 | rgen 3063 |
. . . 4
β’
βπ β
{π₯ β£ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}π β€ sup({π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}, β*, <
) |
63 | | brralrspcev 5207 |
. . . 4
β’
((sup({π₯ β£
βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}, β*, < )
β β β§ βπ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}π β€ sup({π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}, β*, <
)) β βπ β
β βπ β
{π₯ β£ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}π β€ π) |
64 | 57, 62, 63 | sylancl 586 |
. . 3
β’ (π β βπ β β βπ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}π β€ π) |
65 | | simprr 771 |
. . . . . . 7
β’ ((π β dom β«1
β§ (βπ β
β+ (π§
β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))) β π₯ = (β«1βπ)) |
66 | | itg1cl 25193 |
. . . . . . . 8
β’ (π β dom β«1
β (β«1βπ) β β) |
67 | 66 | adantr 481 |
. . . . . . 7
β’ ((π β dom β«1
β§ (βπ β
β+ (π§
β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))) β
(β«1βπ)
β β) |
68 | 65, 67 | eqeltrd 2833 |
. . . . . 6
β’ ((π β dom β«1
β§ (βπ β
β+ (π§
β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))) β π₯ β β) |
69 | 68 | rexlimiva 3147 |
. . . . 5
β’
(βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ)) β π₯ β β) |
70 | 69 | abssi 4066 |
. . . 4
β’ {π₯ β£ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))} β
β |
71 | 70 | a1i 11 |
. . 3
β’ (π β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))} β
β) |
72 | | itg2addnc.g2 |
. . . . . . . . . . . . 13
β’ (π β πΊ:ββΆ(0[,)+β)) |
73 | 72 | ffvelcdmda 7083 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β β) β (πΊβπ§) β (0[,)+β)) |
74 | | elrege0 13427 |
. . . . . . . . . . . 12
β’ ((πΊβπ§) β (0[,)+β) β ((πΊβπ§) β β β§ 0 β€ (πΊβπ§))) |
75 | 73, 74 | sylib 217 |
. . . . . . . . . . 11
β’ ((π β§ π§ β β) β ((πΊβπ§) β β β§ 0 β€ (πΊβπ§))) |
76 | 75 | simprd 496 |
. . . . . . . . . 10
β’ ((π β§ π§ β β) β 0 β€ (πΊβπ§)) |
77 | 76 | ralrimiva 3146 |
. . . . . . . . 9
β’ (π β βπ§ β β 0 β€ (πΊβπ§)) |
78 | 72 | feqmptd 6957 |
. . . . . . . . . 10
β’ (π β πΊ = (π§ β β β¦ (πΊβπ§))) |
79 | 20, 22, 73, 23, 78 | ofrfval2 7687 |
. . . . . . . . 9
β’ (π β ((π§ β β β¦ 0)
βr β€ πΊ
β βπ§ β
β 0 β€ (πΊβπ§))) |
80 | 77, 79 | mpbird 256 |
. . . . . . . 8
β’ (π β (π§ β β β¦ 0)
βr β€ πΊ) |
81 | 80 | ralrimivw 3150 |
. . . . . . 7
β’ (π β βπ β β+ (π§ β β β¦ 0)
βr β€ πΊ) |
82 | | r19.2z 4493 |
. . . . . . 7
β’
((β+ β β
β§ βπ β β+ (π§ β β β¦ 0)
βr β€ πΊ)
β βπ β
β+ (π§
β β β¦ 0) βr β€ πΊ) |
83 | 12, 81, 82 | sylancr 587 |
. . . . . 6
β’ (π β βπ β β+ (π§ β β β¦ 0)
βr β€ πΊ) |
84 | | fveq2 6888 |
. . . . . . . . . 10
β’ (π = (β Γ {0}) β
(β«1βπ)
= (β«1β(β Γ {0}))) |
85 | 84, 31 | eqtr2di 2789 |
. . . . . . . . 9
β’ (π = (β Γ {0}) β
0 = (β«1βπ)) |
86 | 85 | biantrud 532 |
. . . . . . . 8
β’ (π = (β Γ {0}) β
(βπ β
β+ (π§
β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β (βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ 0 =
(β«1βπ)))) |
87 | | fveq1 6887 |
. . . . . . . . . . . . 13
β’ (π = (β Γ {0}) β
(πβπ§) = ((β Γ {0})βπ§)) |
88 | 87, 35 | sylan9eq 2792 |
. . . . . . . . . . . 12
β’ ((π = (β Γ {0}) β§
π§ β β) β
(πβπ§) = 0) |
89 | 88 | iftrued 4535 |
. . . . . . . . . . 11
β’ ((π = (β Γ {0}) β§
π§ β β) β
if((πβπ§) = 0, 0, ((πβπ§) + π)) = 0) |
90 | 89 | mpteq2dva 5247 |
. . . . . . . . . 10
β’ (π = (β Γ {0}) β
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) = (π§ β β β¦ 0)) |
91 | 90 | breq1d 5157 |
. . . . . . . . 9
β’ (π = (β Γ {0}) β
((π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β (π§ β β β¦ 0)
βr β€ πΊ)) |
92 | 91 | rexbidv 3178 |
. . . . . . . 8
β’ (π = (β Γ {0}) β
(βπ β
β+ (π§
β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β βπ β β+
(π§ β β β¦
0) βr β€ πΊ)) |
93 | 86, 92 | bitr3d 280 |
. . . . . . 7
β’ (π = (β Γ {0}) β
((βπ β
β+ (π§
β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ 0 =
(β«1βπ)) β βπ β β+ (π§ β β β¦ 0)
βr β€ πΊ)) |
94 | 93 | rspcev 3612 |
. . . . . 6
β’
(((β Γ {0}) β dom β«1 β§ βπ β β+
(π§ β β β¦
0) βr β€ πΊ) β βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ 0 =
(β«1βπ))) |
95 | 8, 83, 94 | sylancr 587 |
. . . . 5
β’ (π β βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ 0 =
(β«1βπ))) |
96 | | eqeq1 2736 |
. . . . . . . 8
β’ (π₯ = 0 β (π₯ = (β«1βπ) β 0 =
(β«1βπ))) |
97 | 96 | anbi2d 629 |
. . . . . . 7
β’ (π₯ = 0 β ((βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ)) β (βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ 0 =
(β«1βπ)))) |
98 | 97 | rexbidv 3178 |
. . . . . 6
β’ (π₯ = 0 β (βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ)) β βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ 0 =
(β«1βπ)))) |
99 | 21, 98 | elab 3667 |
. . . . 5
β’ (0 β
{π₯ β£ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))} β βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ 0 =
(β«1βπ))) |
100 | 95, 99 | sylibr 233 |
. . . 4
β’ (π β 0 β {π₯ β£ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}) |
101 | 100 | ne0d 4334 |
. . 3
β’ (π β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))} β
β
) |
102 | | fss 6731 |
. . . . . . 7
β’ ((πΊ:ββΆ(0[,)+β)
β§ (0[,)+β) β (0[,]+β)) β πΊ:ββΆ(0[,]+β)) |
103 | 50, 102 | mpan2 689 |
. . . . . 6
β’ (πΊ:ββΆ(0[,)+β)
β πΊ:ββΆ(0[,]+β)) |
104 | | eqid 2732 |
. . . . . . 7
β’ {π₯ β£ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))} = {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))} |
105 | 104 | itg2addnclem 36527 |
. . . . . 6
β’ (πΊ:ββΆ(0[,]+β)
β (β«2βπΊ) = sup({π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}, β*, <
)) |
106 | 72, 103, 105 | 3syl 18 |
. . . . 5
β’ (π β
(β«2βπΊ)
= sup({π₯ β£
βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}, β*, <
)) |
107 | | itg2addnc.g3 |
. . . . 5
β’ (π β
(β«2βπΊ)
β β) |
108 | 106, 107 | eqeltrrd 2834 |
. . . 4
β’ (π β sup({π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}, β*, < )
β β) |
109 | 70, 58 | sstri 3990 |
. . . . . 6
β’ {π₯ β£ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))} β
β* |
110 | | supxrub 13299 |
. . . . . 6
β’ (({π₯ β£ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))} β β*
β§ π β {π₯ β£ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}) β π β€ sup({π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}, β*, <
)) |
111 | 109, 110 | mpan 688 |
. . . . 5
β’ (π β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))} β π β€ sup({π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}, β*, <
)) |
112 | 111 | rgen 3063 |
. . . 4
β’
βπ β
{π₯ β£ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π β€ sup({π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}, β*, <
) |
113 | | brralrspcev 5207 |
. . . 4
β’
((sup({π₯ β£
βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}, β*, < )
β β β§ βπ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π β€ sup({π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}, β*, <
)) β βπ β
β βπ β
{π₯ β£ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π β€ π) |
114 | 108, 112,
113 | sylancl 586 |
. . 3
β’ (π β βπ β β βπ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π β€ π) |
115 | | eqid 2732 |
. . 3
β’ {π β£ βπ‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’)} = {π β£ βπ‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’)} |
116 | 7, 49, 64, 71, 101, 114, 115 | supadd 12178 |
. 2
β’ (π β (sup({π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}, β, < ) +
sup({π₯ β£ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}, β, < )) =
sup({π β£ βπ‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’)}, β, < )) |
117 | | supxrre 13302 |
. . . . 5
β’ (({π₯ β£ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))} β β β§ {π₯ β£ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))} β β
β§
βπ β β
βπ β {π₯ β£ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}π β€ π) β sup({π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}, β*, < )
= sup({π₯ β£
βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}, β, <
)) |
118 | 7, 49, 64, 117 | syl3anc 1371 |
. . . 4
β’ (π β sup({π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}, β*, < )
= sup({π₯ β£
βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}, β, <
)) |
119 | 55, 118 | eqtrd 2772 |
. . 3
β’ (π β
(β«2βπΉ)
= sup({π₯ β£
βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}, β, <
)) |
120 | | supxrre 13302 |
. . . . 5
β’ (({π₯ β£ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))} β β β§ {π₯ β£ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))} β β
β§
βπ β β
βπ β {π₯ β£ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π β€ π) β sup({π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}, β*, < )
= sup({π₯ β£
βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}, β, <
)) |
121 | 71, 101, 114, 120 | syl3anc 1371 |
. . . 4
β’ (π β sup({π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}, β*, < )
= sup({π₯ β£
βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}, β, <
)) |
122 | 106, 121 | eqtrd 2772 |
. . 3
β’ (π β
(β«2βπΊ)
= sup({π₯ β£
βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}, β, <
)) |
123 | 119, 122 | oveq12d 7423 |
. 2
β’ (π β
((β«2βπΉ) + (β«2βπΊ)) = (sup({π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}, β, < ) +
sup({π₯ β£ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}, β, <
))) |
124 | | ge0addcl 13433 |
. . . . . . 7
β’ ((π₯ β (0[,)+β) β§
π¦ β (0[,)+β))
β (π₯ + π¦) β
(0[,)+β)) |
125 | 50, 124 | sselid 3979 |
. . . . . 6
β’ ((π₯ β (0[,)+β) β§
π¦ β (0[,)+β))
β (π₯ + π¦) β
(0[,]+β)) |
126 | 125 | adantl 482 |
. . . . 5
β’ ((π β§ (π₯ β (0[,)+β) β§ π¦ β (0[,)+β))) β
(π₯ + π¦) β (0[,]+β)) |
127 | | inidm 4217 |
. . . . 5
β’ (β
β© β) = β |
128 | 126, 13, 72, 20, 20, 127 | off 7684 |
. . . 4
β’ (π β (πΉ βf + πΊ):ββΆ(0[,]+β)) |
129 | | eqid 2732 |
. . . . 5
β’ {π β£ ββ β dom
β«1(βπ¦
β β+ (π§ β β β¦ if((ββπ§) = 0, 0, ((ββπ§) + π¦))) βr β€ (πΉ βf + πΊ) β§ π = (β«1ββ))} = {π β£ ββ β dom β«1(βπ¦ β β+
(π§ β β β¦
if((ββπ§) = 0, 0, ((ββπ§) + π¦))) βr β€ (πΉ βf + πΊ) β§ π = (β«1ββ))} |
130 | 129 | itg2addnclem 36527 |
. . . 4
β’ ((πΉ βf + πΊ):ββΆ(0[,]+β)
β (β«2β(πΉ βf + πΊ)) = sup({π β£ ββ β dom β«1(βπ¦ β β+
(π§ β β β¦
if((ββπ§) = 0, 0, ((ββπ§) + π¦))) βr β€ (πΉ βf + πΊ) β§ π = (β«1ββ))}, β*, <
)) |
131 | 128, 130 | syl 17 |
. . 3
β’ (π β
(β«2β(πΉ
βf + πΊ)) =
sup({π β£ ββ β dom
β«1(βπ¦
β β+ (π§ β β β¦ if((ββπ§) = 0, 0, ((ββπ§) + π¦))) βr β€ (πΉ βf + πΊ) β§ π = (β«1ββ))}, β*, <
)) |
132 | | itg2addnc.f1 |
. . . . . . . 8
β’ (π β πΉ β MblFn) |
133 | 132, 13, 56, 72, 107 | itg2addnclem3 36529 |
. . . . . . 7
β’ (π β (ββ β dom β«1(βπ¦ β β+
(π§ β β β¦
if((ββπ§) = 0, 0, ((ββπ§) + π¦))) βr β€ (πΉ βf + πΊ) β§ π = (β«1ββ)) β βπ‘βπ’(βπ β dom β«1βπ β dom
β«1((βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π‘ = (β«1βπ)) β§ (βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π’ = (β«1βπ))) β§ π = (π‘ + π’)))) |
134 | | simpl 483 |
. . . . . . . . . . . . . 14
β’ ((π β dom β«1
β§ π β dom
β«1) β π
β dom β«1) |
135 | | simpr 485 |
. . . . . . . . . . . . . 14
β’ ((π β dom β«1
β§ π β dom
β«1) β π
β dom β«1) |
136 | 134, 135 | i1fadd 25203 |
. . . . . . . . . . . . 13
β’ ((π β dom β«1
β§ π β dom
β«1) β (π βf + π) β dom
β«1) |
137 | 136 | ad3antlr 729 |
. . . . . . . . . . . 12
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ ((βπ β
β+ (π§
β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π‘ = (β«1βπ)) β§ (βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π’ = (β«1βπ)))) β§ π = (π‘ + π’)) β (π βf + π) β dom
β«1) |
138 | | reeanv 3226 |
. . . . . . . . . . . . . . . . 17
β’
(βπ β
β+ βπ β β+ ((π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ) β (βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ βπ β β+ (π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ)) |
139 | 138 | biimpri 227 |
. . . . . . . . . . . . . . . 16
β’
((βπ β
β+ (π§
β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ βπ β β+ (π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ) β βπ β β+
βπ β
β+ ((π§
β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ)) |
140 | 139 | ad2ant2r 745 |
. . . . . . . . . . . . . . 15
β’
(((βπ β
β+ (π§
β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π‘ = (β«1βπ)) β§ (βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π’ = (β«1βπ))) β βπ β β+
βπ β
β+ ((π§
β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ)) |
141 | | ifcl 4572 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β+
β§ π β
β+) β if(π β€ π, π, π) β
β+) |
142 | 141 | ad2antlr 725 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ ((π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ)) β if(π β€ π, π, π) β
β+) |
143 | | breq1 5150 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (0 =
if((πβπ§) = 0, 0, ((πβπ§) + π)) β (0 β€ (πΉβπ§) β if((πβπ§) = 0, 0, ((πβπ§) + π)) β€ (πΉβπ§))) |
144 | 143 | anbi1d 630 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (0 =
if((πβπ§) = 0, 0, ((πβπ§) + π)) β ((0 β€ (πΉβπ§) β§ if((πβπ§) = 0, 0, ((πβπ§) + π)) β€ (πΊβπ§)) β (if((πβπ§) = 0, 0, ((πβπ§) + π)) β€ (πΉβπ§) β§ if((πβπ§) = 0, 0, ((πβπ§) + π)) β€ (πΊβπ§)))) |
145 | 144 | imbi1d 341 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (0 =
if((πβπ§) = 0, 0, ((πβπ§) + π)) β (((0 β€ (πΉβπ§) β§ if((πβπ§) = 0, 0, ((πβπ§) + π)) β€ (πΊβπ§)) β if(((πβπ§) + (πβπ§)) = 0, 0, (((πβπ§) + (πβπ§)) + if(π β€ π, π, π))) β€ ((πΉβπ§) + (πΊβπ§))) β ((if((πβπ§) = 0, 0, ((πβπ§) + π)) β€ (πΉβπ§) β§ if((πβπ§) = 0, 0, ((πβπ§) + π)) β€ (πΊβπ§)) β if(((πβπ§) + (πβπ§)) = 0, 0, (((πβπ§) + (πβπ§)) + if(π β€ π, π, π))) β€ ((πΉβπ§) + (πΊβπ§))))) |
146 | | breq1 5150 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((πβπ§) + π) = if((πβπ§) = 0, 0, ((πβπ§) + π)) β (((πβπ§) + π) β€ (πΉβπ§) β if((πβπ§) = 0, 0, ((πβπ§) + π)) β€ (πΉβπ§))) |
147 | 146 | anbi1d 630 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((πβπ§) + π) = if((πβπ§) = 0, 0, ((πβπ§) + π)) β ((((πβπ§) + π) β€ (πΉβπ§) β§ if((πβπ§) = 0, 0, ((πβπ§) + π)) β€ (πΊβπ§)) β (if((πβπ§) = 0, 0, ((πβπ§) + π)) β€ (πΉβπ§) β§ if((πβπ§) = 0, 0, ((πβπ§) + π)) β€ (πΊβπ§)))) |
148 | 147 | imbi1d 341 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((πβπ§) + π) = if((πβπ§) = 0, 0, ((πβπ§) + π)) β (((((πβπ§) + π) β€ (πΉβπ§) β§ if((πβπ§) = 0, 0, ((πβπ§) + π)) β€ (πΊβπ§)) β if(((πβπ§) + (πβπ§)) = 0, 0, (((πβπ§) + (πβπ§)) + if(π β€ π, π, π))) β€ ((πΉβπ§) + (πΊβπ§))) β ((if((πβπ§) = 0, 0, ((πβπ§) + π)) β€ (πΉβπ§) β§ if((πβπ§) = 0, 0, ((πβπ§) + π)) β€ (πΊβπ§)) β if(((πβπ§) + (πβπ§)) = 0, 0, (((πβπ§) + (πβπ§)) + if(π β€ π, π, π))) β€ ((πΉβπ§) + (πΊβπ§))))) |
149 | | breq1 5150 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (0 =
if((πβπ§) = 0, 0, ((πβπ§) + π)) β (0 β€ (πΊβπ§) β if((πβπ§) = 0, 0, ((πβπ§) + π)) β€ (πΊβπ§))) |
150 | 149 | anbi2d 629 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (0 =
if((πβπ§) = 0, 0, ((πβπ§) + π)) β ((0 β€ (πΉβπ§) β§ 0 β€ (πΊβπ§)) β (0 β€ (πΉβπ§) β§ if((πβπ§) = 0, 0, ((πβπ§) + π)) β€ (πΊβπ§)))) |
151 | 150 | imbi1d 341 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (0 =
if((πβπ§) = 0, 0, ((πβπ§) + π)) β (((0 β€ (πΉβπ§) β§ 0 β€ (πΊβπ§)) β if(((πβπ§) + (πβπ§)) = 0, 0, (((πβπ§) + (πβπ§)) + if(π β€ π, π, π))) β€ ((πΉβπ§) + (πΊβπ§))) β ((0 β€ (πΉβπ§) β§ if((πβπ§) = 0, 0, ((πβπ§) + π)) β€ (πΊβπ§)) β if(((πβπ§) + (πβπ§)) = 0, 0, (((πβπ§) + (πβπ§)) + if(π β€ π, π, π))) β€ ((πΉβπ§) + (πΊβπ§))))) |
152 | | breq1 5150 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((πβπ§) + π) = if((πβπ§) = 0, 0, ((πβπ§) + π)) β (((πβπ§) + π) β€ (πΊβπ§) β if((πβπ§) = 0, 0, ((πβπ§) + π)) β€ (πΊβπ§))) |
153 | 152 | anbi2d 629 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((πβπ§) + π) = if((πβπ§) = 0, 0, ((πβπ§) + π)) β ((0 β€ (πΉβπ§) β§ ((πβπ§) + π) β€ (πΊβπ§)) β (0 β€ (πΉβπ§) β§ if((πβπ§) = 0, 0, ((πβπ§) + π)) β€ (πΊβπ§)))) |
154 | 153 | imbi1d 341 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((πβπ§) + π) = if((πβπ§) = 0, 0, ((πβπ§) + π)) β (((0 β€ (πΉβπ§) β§ ((πβπ§) + π) β€ (πΊβπ§)) β if(((πβπ§) + (πβπ§)) = 0, 0, (((πβπ§) + (πβπ§)) + if(π β€ π, π, π))) β€ ((πΉβπ§) + (πΊβπ§))) β ((0 β€ (πΉβπ§) β§ if((πβπ§) = 0, 0, ((πβπ§) + π)) β€ (πΊβπ§)) β if(((πβπ§) + (πβπ§)) = 0, 0, (((πβπ§) + (πβπ§)) + if(π β€ π, π, π))) β€ ((πΉβπ§) + (πΊβπ§))))) |
155 | | oveq12 7414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((πβπ§) = 0 β§ (πβπ§) = 0) β ((πβπ§) + (πβπ§)) = (0 + 0)) |
156 | | 00id 11385 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (0 + 0) =
0 |
157 | 155, 156 | eqtrdi 2788 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((πβπ§) = 0 β§ (πβπ§) = 0) β ((πβπ§) + (πβπ§)) = 0) |
158 | 157 | iftrued 4535 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((πβπ§) = 0 β§ (πβπ§) = 0) β if(((πβπ§) + (πβπ§)) = 0, 0, (((πβπ§) + (πβπ§)) + if(π β€ π, π, π))) = 0) |
159 | 158 | adantll 712 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ (πβπ§) = 0) β§ (πβπ§) = 0) β if(((πβπ§) + (πβπ§)) = 0, 0, (((πβπ§) + (πβπ§)) + if(π β€ π, π, π))) = 0) |
160 | | simpll 765 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β π) |
161 | 15 | simplbi 498 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((πΉβπ§) β (0[,)+β) β (πΉβπ§) β β) |
162 | 14, 161 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ π§ β β) β (πΉβπ§) β β) |
163 | 74 | simplbi 498 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((πΊβπ§) β (0[,)+β) β (πΊβπ§) β β) |
164 | 73, 163 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ π§ β β) β (πΊβπ§) β β) |
165 | 162, 164,
17, 76 | addge0d 11786 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π§ β β) β 0 β€ ((πΉβπ§) + (πΊβπ§))) |
166 | 160, 165 | sylan 580 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β 0 β€ ((πΉβπ§) + (πΊβπ§))) |
167 | 166 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ (πβπ§) = 0) β§ (πβπ§) = 0) β 0 β€ ((πΉβπ§) + (πΊβπ§))) |
168 | 159, 167 | eqbrtrd 5169 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ (πβπ§) = 0) β§ (πβπ§) = 0) β if(((πβπ§) + (πβπ§)) = 0, 0, (((πβπ§) + (πβπ§)) + if(π β€ π, π, π))) β€ ((πΉβπ§) + (πΊβπ§))) |
169 | 168 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ (πβπ§) = 0) β§ (πβπ§) = 0) β ((0 β€ (πΉβπ§) β§ 0 β€ (πΊβπ§)) β if(((πβπ§) + (πβπ§)) = 0, 0, (((πβπ§) + (πβπ§)) + if(π β€ π, π, π))) β€ ((πΉβπ§) + (πΊβπ§)))) |
170 | 166 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ (πβπ§) = 0) β§ ((πβπ§) + π) β€ (πΊβπ§)) β 0 β€ ((πΉβπ§) + (πΊβπ§))) |
171 | | oveq1 7412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((πβπ§) = 0 β ((πβπ§) + (πβπ§)) = (0 + (πβπ§))) |
172 | | simplrr 776 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β π β dom
β«1) |
173 | | i1ff 25184 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π β dom β«1
β π:ββΆβ) |
174 | 173 | ffvelcdmda 7083 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π β dom β«1
β§ π§ β β)
β (πβπ§) β
β) |
175 | 172, 174 | sylan 580 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β (πβπ§) β β) |
176 | 175 | recnd 11238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β (πβπ§) β β) |
177 | 176 | addlidd 11411 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β (0 + (πβπ§)) = (πβπ§)) |
178 | 171, 177 | sylan9eqr 2794 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ (πβπ§) = 0) β ((πβπ§) + (πβπ§)) = (πβπ§)) |
179 | 178 | oveq1d 7420 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ (πβπ§) = 0) β (((πβπ§) + (πβπ§)) + if(π β€ π, π, π)) = ((πβπ§) + if(π β€ π, π, π))) |
180 | 179 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ (πβπ§) = 0) β§ ((πβπ§) + π) β€ (πΊβπ§)) β (((πβπ§) + (πβπ§)) + if(π β€ π, π, π)) = ((πβπ§) + if(π β€ π, π, π))) |
181 | 141 | rpred 13012 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π β β+
β§ π β
β+) β if(π β€ π, π, π) β β) |
182 | 181 | ad2antlr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β if(π β€ π, π, π) β β) |
183 | 175, 182 | readdcld 11239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β ((πβπ§) + if(π β€ π, π, π)) β β) |
184 | 183 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ ((πβπ§) + π) β€ (πΊβπ§)) β ((πβπ§) + if(π β€ π, π, π)) β β) |
185 | 160, 164 | sylan 580 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β (πΊβπ§) β β) |
186 | 185 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ ((πβπ§) + π) β€ (πΊβπ§)) β (πΊβπ§) β β) |
187 | 160, 162 | sylan 580 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β (πΉβπ§) β β) |
188 | 187, 185 | readdcld 11239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β ((πΉβπ§) + (πΊβπ§)) β β) |
189 | 188 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ ((πβπ§) + π) β€ (πΊβπ§)) β ((πΉβπ§) + (πΊβπ§)) β β) |
190 | | simplrr 776 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β π β β+) |
191 | 190 | rpred 13012 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β π β β) |
192 | | rpre 12978 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π β β+
β π β
β) |
193 | | rpre 12978 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π β β+
β π β
β) |
194 | | min2 13165 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((π β β β§ π β β) β if(π β€ π, π, π) β€ π) |
195 | 192, 193,
194 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π β β+
β§ π β
β+) β if(π β€ π, π, π) β€ π) |
196 | 195 | ad2antlr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β if(π β€ π, π, π) β€ π) |
197 | 182, 191,
175, 196 | leadd2dd 11825 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β ((πβπ§) + if(π β€ π, π, π)) β€ ((πβπ§) + π)) |
198 | 175, 191 | readdcld 11239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β ((πβπ§) + π) β β) |
199 | | letr 11304 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((((πβπ§) + if(π β€ π, π, π)) β β β§ ((πβπ§) + π) β β β§ (πΊβπ§) β β) β ((((πβπ§) + if(π β€ π, π, π)) β€ ((πβπ§) + π) β§ ((πβπ§) + π) β€ (πΊβπ§)) β ((πβπ§) + if(π β€ π, π, π)) β€ (πΊβπ§))) |
200 | 183, 198,
185, 199 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β ((((πβπ§) + if(π β€ π, π, π)) β€ ((πβπ§) + π) β§ ((πβπ§) + π) β€ (πΊβπ§)) β ((πβπ§) + if(π β€ π, π, π)) β€ (πΊβπ§))) |
201 | 197, 200 | mpand 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β (((πβπ§) + π) β€ (πΊβπ§) β ((πβπ§) + if(π β€ π, π, π)) β€ (πΊβπ§))) |
202 | 201 | imp 407 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ ((πβπ§) + π) β€ (πΊβπ§)) β ((πβπ§) + if(π β€ π, π, π)) β€ (πΊβπ§)) |
203 | 164, 162 | addge02d 11799 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π β§ π§ β β) β (0 β€ (πΉβπ§) β (πΊβπ§) β€ ((πΉβπ§) + (πΊβπ§)))) |
204 | 17, 203 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β§ π§ β β) β (πΊβπ§) β€ ((πΉβπ§) + (πΊβπ§))) |
205 | 160, 204 | sylan 580 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β (πΊβπ§) β€ ((πΉβπ§) + (πΊβπ§))) |
206 | 205 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ ((πβπ§) + π) β€ (πΊβπ§)) β (πΊβπ§) β€ ((πΉβπ§) + (πΊβπ§))) |
207 | 184, 186,
189, 202, 206 | letrd 11367 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ ((πβπ§) + π) β€ (πΊβπ§)) β ((πβπ§) + if(π β€ π, π, π)) β€ ((πΉβπ§) + (πΊβπ§))) |
208 | 207 | adantlr 713 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ (πβπ§) = 0) β§ ((πβπ§) + π) β€ (πΊβπ§)) β ((πβπ§) + if(π β€ π, π, π)) β€ ((πΉβπ§) + (πΊβπ§))) |
209 | 180, 208 | eqbrtrd 5169 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ (πβπ§) = 0) β§ ((πβπ§) + π) β€ (πΊβπ§)) β (((πβπ§) + (πβπ§)) + if(π β€ π, π, π)) β€ ((πΉβπ§) + (πΊβπ§))) |
210 | | breq1 5150 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (0 =
if(((πβπ§) + (πβπ§)) = 0, 0, (((πβπ§) + (πβπ§)) + if(π β€ π, π, π))) β (0 β€ ((πΉβπ§) + (πΊβπ§)) β if(((πβπ§) + (πβπ§)) = 0, 0, (((πβπ§) + (πβπ§)) + if(π β€ π, π, π))) β€ ((πΉβπ§) + (πΊβπ§)))) |
211 | | breq1 5150 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((πβπ§) + (πβπ§)) + if(π β€ π, π, π)) = if(((πβπ§) + (πβπ§)) = 0, 0, (((πβπ§) + (πβπ§)) + if(π β€ π, π, π))) β ((((πβπ§) + (πβπ§)) + if(π β€ π, π, π)) β€ ((πΉβπ§) + (πΊβπ§)) β if(((πβπ§) + (πβπ§)) = 0, 0, (((πβπ§) + (πβπ§)) + if(π β€ π, π, π))) β€ ((πΉβπ§) + (πΊβπ§)))) |
212 | 210, 211 | ifboth 4566 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((0 β€
((πΉβπ§) + (πΊβπ§)) β§ (((πβπ§) + (πβπ§)) + if(π β€ π, π, π)) β€ ((πΉβπ§) + (πΊβπ§))) β if(((πβπ§) + (πβπ§)) = 0, 0, (((πβπ§) + (πβπ§)) + if(π β€ π, π, π))) β€ ((πΉβπ§) + (πΊβπ§))) |
213 | 170, 209,
212 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ (πβπ§) = 0) β§ ((πβπ§) + π) β€ (πΊβπ§)) β if(((πβπ§) + (πβπ§)) = 0, 0, (((πβπ§) + (πβπ§)) + if(π β€ π, π, π))) β€ ((πΉβπ§) + (πΊβπ§))) |
214 | 213 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ (πβπ§) = 0) β (((πβπ§) + π) β€ (πΊβπ§) β if(((πβπ§) + (πβπ§)) = 0, 0, (((πβπ§) + (πβπ§)) + if(π β€ π, π, π))) β€ ((πΉβπ§) + (πΊβπ§)))) |
215 | 214 | adantld 491 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ (πβπ§) = 0) β ((0 β€ (πΉβπ§) β§ ((πβπ§) + π) β€ (πΊβπ§)) β if(((πβπ§) + (πβπ§)) = 0, 0, (((πβπ§) + (πβπ§)) + if(π β€ π, π, π))) β€ ((πΉβπ§) + (πΊβπ§)))) |
216 | 215 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ (πβπ§) = 0) β§ Β¬ (πβπ§) = 0) β ((0 β€ (πΉβπ§) β§ ((πβπ§) + π) β€ (πΊβπ§)) β if(((πβπ§) + (πβπ§)) = 0, 0, (((πβπ§) + (πβπ§)) + if(π β€ π, π, π))) β€ ((πΉβπ§) + (πΊβπ§)))) |
217 | 151, 154,
169, 216 | ifbothda 4565 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ (πβπ§) = 0) β ((0 β€ (πΉβπ§) β§ if((πβπ§) = 0, 0, ((πβπ§) + π)) β€ (πΊβπ§)) β if(((πβπ§) + (πβπ§)) = 0, 0, (((πβπ§) + (πβπ§)) + if(π β€ π, π, π))) β€ ((πΉβπ§) + (πΊβπ§)))) |
218 | 149 | anbi2d 629 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (0 =
if((πβπ§) = 0, 0, ((πβπ§) + π)) β ((((πβπ§) + π) β€ (πΉβπ§) β§ 0 β€ (πΊβπ§)) β (((πβπ§) + π) β€ (πΉβπ§) β§ if((πβπ§) = 0, 0, ((πβπ§) + π)) β€ (πΊβπ§)))) |
219 | 218 | imbi1d 341 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (0 =
if((πβπ§) = 0, 0, ((πβπ§) + π)) β (((((πβπ§) + π) β€ (πΉβπ§) β§ 0 β€ (πΊβπ§)) β if(((πβπ§) + (πβπ§)) = 0, 0, (((πβπ§) + (πβπ§)) + if(π β€ π, π, π))) β€ ((πΉβπ§) + (πΊβπ§))) β ((((πβπ§) + π) β€ (πΉβπ§) β§ if((πβπ§) = 0, 0, ((πβπ§) + π)) β€ (πΊβπ§)) β if(((πβπ§) + (πβπ§)) = 0, 0, (((πβπ§) + (πβπ§)) + if(π β€ π, π, π))) β€ ((πΉβπ§) + (πΊβπ§))))) |
220 | 152 | anbi2d 629 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((πβπ§) + π) = if((πβπ§) = 0, 0, ((πβπ§) + π)) β ((((πβπ§) + π) β€ (πΉβπ§) β§ ((πβπ§) + π) β€ (πΊβπ§)) β (((πβπ§) + π) β€ (πΉβπ§) β§ if((πβπ§) = 0, 0, ((πβπ§) + π)) β€ (πΊβπ§)))) |
221 | 220 | imbi1d 341 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((πβπ§) + π) = if((πβπ§) = 0, 0, ((πβπ§) + π)) β (((((πβπ§) + π) β€ (πΉβπ§) β§ ((πβπ§) + π) β€ (πΊβπ§)) β if(((πβπ§) + (πβπ§)) = 0, 0, (((πβπ§) + (πβπ§)) + if(π β€ π, π, π))) β€ ((πΉβπ§) + (πΊβπ§))) β ((((πβπ§) + π) β€ (πΉβπ§) β§ if((πβπ§) = 0, 0, ((πβπ§) + π)) β€ (πΊβπ§)) β if(((πβπ§) + (πβπ§)) = 0, 0, (((πβπ§) + (πβπ§)) + if(π β€ π, π, π))) β€ ((πΉβπ§) + (πΊβπ§))))) |
222 | 166 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ (πβπ§) = 0) β§ ((πβπ§) + π) β€ (πΉβπ§)) β 0 β€ ((πΉβπ§) + (πΊβπ§))) |
223 | | oveq2 7413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((πβπ§) = 0 β ((πβπ§) + (πβπ§)) = ((πβπ§) + 0)) |
224 | | simplrl 775 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β π β dom
β«1) |
225 | | i1ff 25184 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π β dom β«1
β π:ββΆβ) |
226 | 225 | ffvelcdmda 7083 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π β dom β«1
β§ π§ β β)
β (πβπ§) β
β) |
227 | 224, 226 | sylan 580 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β (πβπ§) β β) |
228 | 227 | recnd 11238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β (πβπ§) β β) |
229 | 228 | addridd 11410 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β ((πβπ§) + 0) = (πβπ§)) |
230 | 223, 229 | sylan9eqr 2794 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ (πβπ§) = 0) β ((πβπ§) + (πβπ§)) = (πβπ§)) |
231 | 230 | oveq1d 7420 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ (πβπ§) = 0) β (((πβπ§) + (πβπ§)) + if(π β€ π, π, π)) = ((πβπ§) + if(π β€ π, π, π))) |
232 | 231 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ (πβπ§) = 0) β§ ((πβπ§) + π) β€ (πΉβπ§)) β (((πβπ§) + (πβπ§)) + if(π β€ π, π, π)) = ((πβπ§) + if(π β€ π, π, π))) |
233 | 227, 182 | readdcld 11239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β ((πβπ§) + if(π β€ π, π, π)) β β) |
234 | 233 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ ((πβπ§) + π) β€ (πΉβπ§)) β ((πβπ§) + if(π β€ π, π, π)) β β) |
235 | 187 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ ((πβπ§) + π) β€ (πΉβπ§)) β (πΉβπ§) β β) |
236 | 188 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ ((πβπ§) + π) β€ (πΉβπ§)) β ((πΉβπ§) + (πΊβπ§)) β β) |
237 | | simplrl 775 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β π β β+) |
238 | 237 | rpred 13012 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β π β β) |
239 | | min1 13164 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((π β β β§ π β β) β if(π β€ π, π, π) β€ π) |
240 | 192, 193,
239 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π β β+
β§ π β
β+) β if(π β€ π, π, π) β€ π) |
241 | 240 | ad2antlr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β if(π β€ π, π, π) β€ π) |
242 | 182, 238,
227, 241 | leadd2dd 11825 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β ((πβπ§) + if(π β€ π, π, π)) β€ ((πβπ§) + π)) |
243 | 227, 238 | readdcld 11239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β ((πβπ§) + π) β β) |
244 | | letr 11304 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((((πβπ§) + if(π β€ π, π, π)) β β β§ ((πβπ§) + π) β β β§ (πΉβπ§) β β) β ((((πβπ§) + if(π β€ π, π, π)) β€ ((πβπ§) + π) β§ ((πβπ§) + π) β€ (πΉβπ§)) β ((πβπ§) + if(π β€ π, π, π)) β€ (πΉβπ§))) |
245 | 233, 243,
187, 244 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β ((((πβπ§) + if(π β€ π, π, π)) β€ ((πβπ§) + π) β§ ((πβπ§) + π) β€ (πΉβπ§)) β ((πβπ§) + if(π β€ π, π, π)) β€ (πΉβπ§))) |
246 | 242, 245 | mpand 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β (((πβπ§) + π) β€ (πΉβπ§) β ((πβπ§) + if(π β€ π, π, π)) β€ (πΉβπ§))) |
247 | 246 | imp 407 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ ((πβπ§) + π) β€ (πΉβπ§)) β ((πβπ§) + if(π β€ π, π, π)) β€ (πΉβπ§)) |
248 | 162, 164 | addge01d 11798 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π β§ π§ β β) β (0 β€ (πΊβπ§) β (πΉβπ§) β€ ((πΉβπ§) + (πΊβπ§)))) |
249 | 76, 248 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β§ π§ β β) β (πΉβπ§) β€ ((πΉβπ§) + (πΊβπ§))) |
250 | 160, 249 | sylan 580 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β (πΉβπ§) β€ ((πΉβπ§) + (πΊβπ§))) |
251 | 250 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ ((πβπ§) + π) β€ (πΉβπ§)) β (πΉβπ§) β€ ((πΉβπ§) + (πΊβπ§))) |
252 | 234, 235,
236, 247, 251 | letrd 11367 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ ((πβπ§) + π) β€ (πΉβπ§)) β ((πβπ§) + if(π β€ π, π, π)) β€ ((πΉβπ§) + (πΊβπ§))) |
253 | 252 | adantlr 713 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ (πβπ§) = 0) β§ ((πβπ§) + π) β€ (πΉβπ§)) β ((πβπ§) + if(π β€ π, π, π)) β€ ((πΉβπ§) + (πΊβπ§))) |
254 | 232, 253 | eqbrtrd 5169 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ (πβπ§) = 0) β§ ((πβπ§) + π) β€ (πΉβπ§)) β (((πβπ§) + (πβπ§)) + if(π β€ π, π, π)) β€ ((πΉβπ§) + (πΊβπ§))) |
255 | 222, 254,
212 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ (πβπ§) = 0) β§ ((πβπ§) + π) β€ (πΉβπ§)) β if(((πβπ§) + (πβπ§)) = 0, 0, (((πβπ§) + (πβπ§)) + if(π β€ π, π, π))) β€ ((πΉβπ§) + (πΊβπ§))) |
256 | 255 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ (πβπ§) = 0) β (((πβπ§) + π) β€ (πΉβπ§) β if(((πβπ§) + (πβπ§)) = 0, 0, (((πβπ§) + (πβπ§)) + if(π β€ π, π, π))) β€ ((πΉβπ§) + (πΊβπ§)))) |
257 | 256 | adantlr 713 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ Β¬ (πβπ§) = 0) β§ (πβπ§) = 0) β (((πβπ§) + π) β€ (πΉβπ§) β if(((πβπ§) + (πβπ§)) = 0, 0, (((πβπ§) + (πβπ§)) + if(π β€ π, π, π))) β€ ((πΉβπ§) + (πΊβπ§)))) |
258 | 257 | adantrd 492 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ Β¬ (πβπ§) = 0) β§ (πβπ§) = 0) β ((((πβπ§) + π) β€ (πΉβπ§) β§ 0 β€ (πΊβπ§)) β if(((πβπ§) + (πβπ§)) = 0, 0, (((πβπ§) + (πβπ§)) + if(π β€ π, π, π))) β€ ((πΉβπ§) + (πΊβπ§)))) |
259 | 166 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ (((πβπ§) + π) β€ (πΉβπ§) β§ ((πβπ§) + π) β€ (πΊβπ§))) β 0 β€ ((πΉβπ§) + (πΊβπ§))) |
260 | 182 | recnd 11238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β if(π β€ π, π, π) β β) |
261 | 228, 176,
260 | addassd 11232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β (((πβπ§) + (πβπ§)) + if(π β€ π, π, π)) = ((πβπ§) + ((πβπ§) + if(π β€ π, π, π)))) |
262 | 261 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ (((πβπ§) + π) β€ (πΉβπ§) β§ ((πβπ§) + π) β€ (πΊβπ§))) β (((πβπ§) + (πβπ§)) + if(π β€ π, π, π)) = ((πβπ§) + ((πβπ§) + if(π β€ π, π, π)))) |
263 | 227, 237 | ltaddrpd 13045 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β (πβπ§) < ((πβπ§) + π)) |
264 | 227, 243,
263 | ltled 11358 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β (πβπ§) β€ ((πβπ§) + π)) |
265 | | letr 11304 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((πβπ§) β β β§ ((πβπ§) + π) β β β§ (πΉβπ§) β β) β (((πβπ§) β€ ((πβπ§) + π) β§ ((πβπ§) + π) β€ (πΉβπ§)) β (πβπ§) β€ (πΉβπ§))) |
266 | 227, 243,
187, 265 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β (((πβπ§) β€ ((πβπ§) + π) β§ ((πβπ§) + π) β€ (πΉβπ§)) β (πβπ§) β€ (πΉβπ§))) |
267 | 264, 266 | mpand 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β (((πβπ§) + π) β€ (πΉβπ§) β (πβπ§) β€ (πΉβπ§))) |
268 | | le2add 11692 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((πβπ§) β β β§ ((πβπ§) + if(π β€ π, π, π)) β β) β§ ((πΉβπ§) β β β§ (πΊβπ§) β β)) β (((πβπ§) β€ (πΉβπ§) β§ ((πβπ§) + if(π β€ π, π, π)) β€ (πΊβπ§)) β ((πβπ§) + ((πβπ§) + if(π β€ π, π, π))) β€ ((πΉβπ§) + (πΊβπ§)))) |
269 | 227, 183,
187, 185, 268 | syl22anc 837 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β (((πβπ§) β€ (πΉβπ§) β§ ((πβπ§) + if(π β€ π, π, π)) β€ (πΊβπ§)) β ((πβπ§) + ((πβπ§) + if(π β€ π, π, π))) β€ ((πΉβπ§) + (πΊβπ§)))) |
270 | 267, 201,
269 | syl2and 608 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β ((((πβπ§) + π) β€ (πΉβπ§) β§ ((πβπ§) + π) β€ (πΊβπ§)) β ((πβπ§) + ((πβπ§) + if(π β€ π, π, π))) β€ ((πΉβπ§) + (πΊβπ§)))) |
271 | 270 | imp 407 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ (((πβπ§) + π) β€ (πΉβπ§) β§ ((πβπ§) + π) β€ (πΊβπ§))) β ((πβπ§) + ((πβπ§) + if(π β€ π, π, π))) β€ ((πΉβπ§) + (πΊβπ§))) |
272 | 262, 271 | eqbrtrd 5169 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ (((πβπ§) + π) β€ (πΉβπ§) β§ ((πβπ§) + π) β€ (πΊβπ§))) β (((πβπ§) + (πβπ§)) + if(π β€ π, π, π)) β€ ((πΉβπ§) + (πΊβπ§))) |
273 | 259, 272,
212 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ (((πβπ§) + π) β€ (πΉβπ§) β§ ((πβπ§) + π) β€ (πΊβπ§))) β if(((πβπ§) + (πβπ§)) = 0, 0, (((πβπ§) + (πβπ§)) + if(π β€ π, π, π))) β€ ((πΉβπ§) + (πΊβπ§))) |
274 | 273 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β ((((πβπ§) + π) β€ (πΉβπ§) β§ ((πβπ§) + π) β€ (πΊβπ§)) β if(((πβπ§) + (πβπ§)) = 0, 0, (((πβπ§) + (πβπ§)) + if(π β€ π, π, π))) β€ ((πΉβπ§) + (πΊβπ§)))) |
275 | 274 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ Β¬ (πβπ§) = 0) β§ Β¬ (πβπ§) = 0) β ((((πβπ§) + π) β€ (πΉβπ§) β§ ((πβπ§) + π) β€ (πΊβπ§)) β if(((πβπ§) + (πβπ§)) = 0, 0, (((πβπ§) + (πβπ§)) + if(π β€ π, π, π))) β€ ((πΉβπ§) + (πΊβπ§)))) |
276 | 219, 221,
258, 275 | ifbothda 4565 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ (π β dom β«1
β§ π β dom
β«1)) β§ (π β β+ β§ π β β+))
β§ π§ β β)
β§ Β¬ (πβπ§) = 0) β ((((πβπ§) + π) β€ (πΉβπ§) β§ if((πβπ§) = 0, 0, ((πβπ§) + π)) β€ (πΊβπ§)) β if(((πβπ§) + (πβπ§)) = 0, 0, (((πβπ§) + (πβπ§)) + if(π β€ π, π, π))) β€ ((πΉβπ§) + (πΊβπ§)))) |
277 | 145, 148,
217, 276 | ifbothda 4565 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β ((if((πβπ§) = 0, 0, ((πβπ§) + π)) β€ (πΉβπ§) β§ if((πβπ§) = 0, 0, ((πβπ§) + π)) β€ (πΊβπ§)) β if(((πβπ§) + (πβπ§)) = 0, 0, (((πβπ§) + (πβπ§)) + if(π β€ π, π, π))) β€ ((πΉβπ§) + (πΊβπ§)))) |
278 | 277 | ralimdva 3167 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β (βπ§ β β (if((πβπ§) = 0, 0, ((πβπ§) + π)) β€ (πΉβπ§) β§ if((πβπ§) = 0, 0, ((πβπ§) + π)) β€ (πΊβπ§)) β βπ§ β β if(((πβπ§) + (πβπ§)) = 0, 0, (((πβπ§) + (πβπ§)) + if(π β€ π, π, π))) β€ ((πΉβπ§) + (πΊβπ§)))) |
279 | | ovex 7438 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((πβπ§) + π) β V |
280 | 21, 279 | ifex 4577 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ if((πβπ§) = 0, 0, ((πβπ§) + π)) β V |
281 | 280 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π§ β β) β if((πβπ§) = 0, 0, ((πβπ§) + π)) β V) |
282 | | eqidd 2733 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) = (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π)))) |
283 | 20, 281, 14, 282, 24 | ofrfval2 7687 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β ((π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β βπ§ β β if((πβπ§) = 0, 0, ((πβπ§) + π)) β€ (πΉβπ§))) |
284 | | ovex 7438 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((πβπ§) + π) β V |
285 | 21, 284 | ifex 4577 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ if((πβπ§) = 0, 0, ((πβπ§) + π)) β V |
286 | 285 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π§ β β) β if((πβπ§) = 0, 0, ((πβπ§) + π)) β V) |
287 | | eqidd 2733 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) = (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π)))) |
288 | 20, 286, 73, 287, 78 | ofrfval2 7687 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β ((π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β βπ§ β β if((πβπ§) = 0, 0, ((πβπ§) + π)) β€ (πΊβπ§))) |
289 | 283, 288 | anbi12d 631 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (((π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ) β (βπ§ β β if((πβπ§) = 0, 0, ((πβπ§) + π)) β€ (πΉβπ§) β§ βπ§ β β if((πβπ§) = 0, 0, ((πβπ§) + π)) β€ (πΊβπ§)))) |
290 | | r19.26 3111 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(βπ§ β
β (if((πβπ§) = 0, 0, ((πβπ§) + π)) β€ (πΉβπ§) β§ if((πβπ§) = 0, 0, ((πβπ§) + π)) β€ (πΊβπ§)) β (βπ§ β β if((πβπ§) = 0, 0, ((πβπ§) + π)) β€ (πΉβπ§) β§ βπ§ β β if((πβπ§) = 0, 0, ((πβπ§) + π)) β€ (πΊβπ§))) |
291 | 289, 290 | bitr4di 288 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (((π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ) β βπ§ β β (if((πβπ§) = 0, 0, ((πβπ§) + π)) β€ (πΉβπ§) β§ if((πβπ§) = 0, 0, ((πβπ§) + π)) β€ (πΊβπ§)))) |
292 | 291 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β (((π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ) β βπ§ β β (if((πβπ§) = 0, 0, ((πβπ§) + π)) β€ (πΉβπ§) β§ if((πβπ§) = 0, 0, ((πβπ§) + π)) β€ (πΊβπ§)))) |
293 | 19 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β β β V) |
294 | | ovex 7438 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((πβπ§) + (πβπ§)) + if(π β€ π, π, π)) β V |
295 | 21, 294 | ifex 4577 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
if(((πβπ§) + (πβπ§)) = 0, 0, (((πβπ§) + (πβπ§)) + if(π β€ π, π, π))) β V |
296 | 295 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β if(((πβπ§) + (πβπ§)) = 0, 0, (((πβπ§) + (πβπ§)) + if(π β€ π, π, π))) β V) |
297 | | ovexd 7440 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β ((πΉβπ§) + (πΊβπ§)) β V) |
298 | 225 | ffnd 6715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β dom β«1
β π Fn
β) |
299 | 298 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β dom β«1
β§ π β dom
β«1) β π
Fn β) |
300 | 299 | ad2antlr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β π Fn β) |
301 | 173 | ffnd 6715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β dom β«1
β π Fn
β) |
302 | 301 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β dom β«1
β§ π β dom
β«1) β π
Fn β) |
303 | 302 | ad2antlr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β π Fn β) |
304 | | eqidd 2733 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β (πβπ§) = (πβπ§)) |
305 | | eqidd 2733 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β (πβπ§) = (πβπ§)) |
306 | 300, 303,
293, 293, 127, 304, 305 | ofval 7677 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β ((π βf + π)βπ§) = ((πβπ§) + (πβπ§))) |
307 | 306 | eqeq1d 2734 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β (((π βf + π)βπ§) = 0 β ((πβπ§) + (πβπ§)) = 0)) |
308 | 306 | oveq1d 7420 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β (((π βf + π)βπ§) + if(π β€ π, π, π)) = (((πβπ§) + (πβπ§)) + if(π β€ π, π, π))) |
309 | 307, 308 | ifbieq2d 4553 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ π§ β β) β if(((π βf + π)βπ§) = 0, 0, (((π βf + π)βπ§) + if(π β€ π, π, π))) = if(((πβπ§) + (πβπ§)) = 0, 0, (((πβπ§) + (πβπ§)) + if(π β€ π, π, π)))) |
310 | 309 | mpteq2dva 5247 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β (π§ β β β¦ if(((π βf + π)βπ§) = 0, 0, (((π βf + π)βπ§) + if(π β€ π, π, π)))) = (π§ β β β¦ if(((πβπ§) + (πβπ§)) = 0, 0, (((πβπ§) + (πβπ§)) + if(π β€ π, π, π))))) |
311 | 13 | ffnd 6715 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β πΉ Fn β) |
312 | 72 | ffnd 6715 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β πΊ Fn β) |
313 | | eqidd 2733 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π§ β β) β (πΉβπ§) = (πΉβπ§)) |
314 | | eqidd 2733 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π§ β β) β (πΊβπ§) = (πΊβπ§)) |
315 | 311, 312,
20, 20, 127, 313, 314 | offval 7675 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (πΉ βf + πΊ) = (π§ β β β¦ ((πΉβπ§) + (πΊβπ§)))) |
316 | 315 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β (πΉ βf + πΊ) = (π§ β β β¦ ((πΉβπ§) + (πΊβπ§)))) |
317 | 293, 296,
297, 310, 316 | ofrfval2 7687 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β ((π§ β β β¦ if(((π βf + π)βπ§) = 0, 0, (((π βf + π)βπ§) + if(π β€ π, π, π)))) βr β€ (πΉ βf + πΊ) β βπ§ β β if(((πβπ§) + (πβπ§)) = 0, 0, (((πβπ§) + (πβπ§)) + if(π β€ π, π, π))) β€ ((πΉβπ§) + (πΊβπ§)))) |
318 | 278, 292,
317 | 3imtr4d 293 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β (((π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ) β (π§ β β β¦ if(((π βf + π)βπ§) = 0, 0, (((π βf + π)βπ§) + if(π β€ π, π, π)))) βr β€ (πΉ βf + πΊ))) |
319 | 318 | imp 407 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ ((π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ)) β (π§ β β β¦ if(((π βf + π)βπ§) = 0, 0, (((π βf + π)βπ§) + if(π β€ π, π, π)))) βr β€ (πΉ βf + πΊ)) |
320 | | oveq2 7413 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π¦ = if(π β€ π, π, π) β (((π βf + π)βπ§) + π¦) = (((π βf + π)βπ§) + if(π β€ π, π, π))) |
321 | 320 | ifeq2d 4547 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π¦ = if(π β€ π, π, π) β if(((π βf + π)βπ§) = 0, 0, (((π βf + π)βπ§) + π¦)) = if(((π βf + π)βπ§) = 0, 0, (((π βf + π)βπ§) + if(π β€ π, π, π)))) |
322 | 321 | mpteq2dv 5249 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ = if(π β€ π, π, π) β (π§ β β β¦ if(((π βf + π)βπ§) = 0, 0, (((π βf + π)βπ§) + π¦))) = (π§ β β β¦ if(((π βf + π)βπ§) = 0, 0, (((π βf + π)βπ§) + if(π β€ π, π, π))))) |
323 | 322 | breq1d 5157 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ = if(π β€ π, π, π) β ((π§ β β β¦ if(((π βf + π)βπ§) = 0, 0, (((π βf + π)βπ§) + π¦))) βr β€ (πΉ βf + πΊ) β (π§ β β β¦ if(((π βf + π)βπ§) = 0, 0, (((π βf + π)βπ§) + if(π β€ π, π, π)))) βr β€ (πΉ βf + πΊ))) |
324 | 323 | rspcev 3612 |
. . . . . . . . . . . . . . . . . 18
β’
((if(π β€ π, π, π) β β+ β§ (π§ β β β¦
if(((π βf
+ π)βπ§) = 0, 0, (((π βf + π)βπ§) + if(π β€ π, π, π)))) βr β€ (πΉ βf + πΊ)) β βπ¦ β β+
(π§ β β β¦
if(((π βf
+ π)βπ§) = 0, 0, (((π βf + π)βπ§) + π¦))) βr β€ (πΉ βf + πΊ)) |
325 | 142, 319,
324 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β§ ((π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ)) β βπ¦ β β+
(π§ β β β¦
if(((π βf
+ π)βπ§) = 0, 0, (((π βf + π)βπ§) + π¦))) βr β€ (πΉ βf + πΊ)) |
326 | 325 | ex 413 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ (π β
β+ β§ π
β β+)) β (((π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ) β βπ¦ β β+
(π§ β β β¦
if(((π βf
+ π)βπ§) = 0, 0, (((π βf + π)βπ§) + π¦))) βr β€ (πΉ βf + πΊ))) |
327 | 326 | rexlimdvva 3211 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β dom β«1 β§ π β dom β«1))
β (βπ β
β+ βπ β β+ ((π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ) β βπ¦ β β+
(π§ β β β¦
if(((π βf
+ π)βπ§) = 0, 0, (((π βf + π)βπ§) + π¦))) βr β€ (πΉ βf + πΊ))) |
328 | 140, 327 | syl5 34 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β dom β«1 β§ π β dom β«1))
β (((βπ β
β+ (π§
β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π‘ = (β«1βπ)) β§ (βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π’ = (β«1βπ))) β βπ¦ β β+
(π§ β β β¦
if(((π βf
+ π)βπ§) = 0, 0, (((π βf + π)βπ§) + π¦))) βr β€ (πΉ βf + πΊ))) |
329 | 328 | a1dd 50 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β dom β«1 β§ π β dom β«1))
β (((βπ β
β+ (π§
β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π‘ = (β«1βπ)) β§ (βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π’ = (β«1βπ))) β (π = (π‘ + π’) β βπ¦ β β+ (π§ β β β¦
if(((π βf
+ π)βπ§) = 0, 0, (((π βf + π)βπ§) + π¦))) βr β€ (πΉ βf + πΊ)))) |
330 | 329 | imp31 418 |
. . . . . . . . . . . 12
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ ((βπ β
β+ (π§
β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π‘ = (β«1βπ)) β§ (βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π’ = (β«1βπ)))) β§ π = (π‘ + π’)) β βπ¦ β β+ (π§ β β β¦
if(((π βf
+ π)βπ§) = 0, 0, (((π βf + π)βπ§) + π¦))) βr β€ (πΉ βf + πΊ)) |
331 | | oveq12 7414 |
. . . . . . . . . . . . . . 15
β’ ((π‘ =
(β«1βπ)
β§ π’ =
(β«1βπ)) β (π‘ + π’) = ((β«1βπ) +
(β«1βπ))) |
332 | 331 | ad2ant2l 744 |
. . . . . . . . . . . . . 14
β’
(((βπ β
β+ (π§
β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π‘ = (β«1βπ)) β§ (βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π’ = (β«1βπ))) β (π‘ + π’) = ((β«1βπ) +
(β«1βπ))) |
333 | 134, 135 | itg1add 25210 |
. . . . . . . . . . . . . . . 16
β’ ((π β dom β«1
β§ π β dom
β«1) β (β«1β(π βf + π)) = ((β«1βπ) +
(β«1βπ))) |
334 | 333 | eqcomd 2738 |
. . . . . . . . . . . . . . 15
β’ ((π β dom β«1
β§ π β dom
β«1) β ((β«1βπ) + (β«1βπ)) =
(β«1β(π
βf + π))) |
335 | 334 | adantl 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β dom β«1 β§ π β dom β«1))
β ((β«1βπ) + (β«1βπ)) =
(β«1β(π
βf + π))) |
336 | 332, 335 | sylan9eqr 2794 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β dom β«1 β§ π β dom β«1))
β§ ((βπ β
β+ (π§
β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π‘ = (β«1βπ)) β§ (βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π’ = (β«1βπ)))) β (π‘ + π’) = (β«1β(π βf + π))) |
337 | | eqtr 2755 |
. . . . . . . . . . . . . 14
β’ ((π = (π‘ + π’) β§ (π‘ + π’) = (β«1β(π βf + π))) β π = (β«1β(π βf + π))) |
338 | 337 | ancoms 459 |
. . . . . . . . . . . . 13
β’ (((π‘ + π’) = (β«1β(π βf + π)) β§ π = (π‘ + π’)) β π = (β«1β(π βf + π))) |
339 | 336, 338 | sylan 580 |
. . . . . . . . . . . 12
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ ((βπ β
β+ (π§
β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π‘ = (β«1βπ)) β§ (βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π’ = (β«1βπ)))) β§ π = (π‘ + π’)) β π = (β«1β(π βf + π))) |
340 | | fveq1 6887 |
. . . . . . . . . . . . . . . . . . 19
β’ (β = (π βf + π) β (ββπ§) = ((π βf + π)βπ§)) |
341 | 340 | eqeq1d 2734 |
. . . . . . . . . . . . . . . . . 18
β’ (β = (π βf + π) β ((ββπ§) = 0 β ((π βf + π)βπ§) = 0)) |
342 | 340 | oveq1d 7420 |
. . . . . . . . . . . . . . . . . 18
β’ (β = (π βf + π) β ((ββπ§) + π¦) = (((π βf + π)βπ§) + π¦)) |
343 | 341, 342 | ifbieq2d 4553 |
. . . . . . . . . . . . . . . . 17
β’ (β = (π βf + π) β if((ββπ§) = 0, 0, ((ββπ§) + π¦)) = if(((π βf + π)βπ§) = 0, 0, (((π βf + π)βπ§) + π¦))) |
344 | 343 | mpteq2dv 5249 |
. . . . . . . . . . . . . . . 16
β’ (β = (π βf + π) β (π§ β β β¦ if((ββπ§) = 0, 0, ((ββπ§) + π¦))) = (π§ β β β¦ if(((π βf + π)βπ§) = 0, 0, (((π βf + π)βπ§) + π¦)))) |
345 | 344 | breq1d 5157 |
. . . . . . . . . . . . . . 15
β’ (β = (π βf + π) β ((π§ β β β¦ if((ββπ§) = 0, 0, ((ββπ§) + π¦))) βr β€ (πΉ βf + πΊ) β (π§ β β β¦ if(((π βf + π)βπ§) = 0, 0, (((π βf + π)βπ§) + π¦))) βr β€ (πΉ βf + πΊ))) |
346 | 345 | rexbidv 3178 |
. . . . . . . . . . . . . 14
β’ (β = (π βf + π) β (βπ¦ β β+ (π§ β β β¦
if((ββπ§) = 0, 0, ((ββπ§) + π¦))) βr β€ (πΉ βf + πΊ) β βπ¦ β β+
(π§ β β β¦
if(((π βf
+ π)βπ§) = 0, 0, (((π βf + π)βπ§) + π¦))) βr β€ (πΉ βf + πΊ))) |
347 | | fveq2 6888 |
. . . . . . . . . . . . . . 15
β’ (β = (π βf + π) β (β«1ββ) =
(β«1β(π
βf + π))) |
348 | 347 | eqeq2d 2743 |
. . . . . . . . . . . . . 14
β’ (β = (π βf + π) β (π = (β«1ββ) β π = (β«1β(π βf + π)))) |
349 | 346, 348 | anbi12d 631 |
. . . . . . . . . . . . 13
β’ (β = (π βf + π) β ((βπ¦ β β+ (π§ β β β¦
if((ββπ§) = 0, 0, ((ββπ§) + π¦))) βr β€ (πΉ βf + πΊ) β§ π = (β«1ββ)) β (βπ¦ β β+
(π§ β β β¦
if(((π βf
+ π)βπ§) = 0, 0, (((π βf + π)βπ§) + π¦))) βr β€ (πΉ βf + πΊ) β§ π = (β«1β(π βf + π))))) |
350 | 349 | rspcev 3612 |
. . . . . . . . . . . 12
β’ (((π βf + π) β dom β«1
β§ (βπ¦ β
β+ (π§
β β β¦ if(((π βf + π)βπ§) = 0, 0, (((π βf + π)βπ§) + π¦))) βr β€ (πΉ βf + πΊ) β§ π = (β«1β(π βf + π)))) β ββ β dom
β«1(βπ¦
β β+ (π§ β β β¦ if((ββπ§) = 0, 0, ((ββπ§) + π¦))) βr β€ (πΉ βf + πΊ) β§ π = (β«1ββ))) |
351 | 137, 330,
339, 350 | syl12anc 835 |
. . . . . . . . . . 11
β’ ((((π β§ (π β dom β«1 β§ π β dom β«1))
β§ ((βπ β
β+ (π§
β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π‘ = (β«1βπ)) β§ (βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π’ = (β«1βπ)))) β§ π = (π‘ + π’)) β ββ β dom β«1(βπ¦ β β+
(π§ β β β¦
if((ββπ§) = 0, 0, ((ββπ§) + π¦))) βr β€ (πΉ βf + πΊ) β§ π = (β«1ββ))) |
352 | 351 | exp31 420 |
. . . . . . . . . 10
β’ ((π β§ (π β dom β«1 β§ π β dom β«1))
β (((βπ β
β+ (π§
β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π‘ = (β«1βπ)) β§ (βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π’ = (β«1βπ))) β (π = (π‘ + π’) β ββ β dom β«1(βπ¦ β β+
(π§ β β β¦
if((ββπ§) = 0, 0, ((ββπ§) + π¦))) βr β€ (πΉ βf + πΊ) β§ π = (β«1ββ))))) |
353 | 352 | rexlimdvva 3211 |
. . . . . . . . 9
β’ (π β (βπ β dom β«1βπ β dom
β«1((βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π‘ = (β«1βπ)) β§ (βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π’ = (β«1βπ))) β (π = (π‘ + π’) β ββ β dom β«1(βπ¦ β β+
(π§ β β β¦
if((ββπ§) = 0, 0, ((ββπ§) + π¦))) βr β€ (πΉ βf + πΊ) β§ π = (β«1ββ))))) |
354 | 353 | impd 411 |
. . . . . . . 8
β’ (π β ((βπ β dom
β«1βπ
β dom β«1((βπ β β+ (π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π‘ = (β«1βπ)) β§ (βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π’ = (β«1βπ))) β§ π = (π‘ + π’)) β ββ β dom β«1(βπ¦ β β+
(π§ β β β¦
if((ββπ§) = 0, 0, ((ββπ§) + π¦))) βr β€ (πΉ βf + πΊ) β§ π = (β«1ββ)))) |
355 | 354 | exlimdvv 1937 |
. . . . . . 7
β’ (π β (βπ‘βπ’(βπ β dom β«1βπ β dom
β«1((βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π‘ = (β«1βπ)) β§ (βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π’ = (β«1βπ))) β§ π = (π‘ + π’)) β ββ β dom β«1(βπ¦ β β+
(π§ β β β¦
if((ββπ§) = 0, 0, ((ββπ§) + π¦))) βr β€ (πΉ βf + πΊ) β§ π = (β«1ββ)))) |
356 | 133, 355 | impbid 211 |
. . . . . 6
β’ (π β (ββ β dom β«1(βπ¦ β β+
(π§ β β β¦
if((ββπ§) = 0, 0, ((ββπ§) + π¦))) βr β€ (πΉ βf + πΊ) β§ π = (β«1ββ)) β βπ‘βπ’(βπ β dom β«1βπ β dom
β«1((βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π‘ = (β«1βπ)) β§ (βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π’ = (β«1βπ))) β§ π = (π‘ + π’)))) |
357 | | eqeq1 2736 |
. . . . . . . . . 10
β’ (π₯ = π‘ β (π₯ = (β«1βπ) β π‘ = (β«1βπ))) |
358 | 357 | anbi2d 629 |
. . . . . . . . 9
β’ (π₯ = π‘ β ((βπ β β+ (π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ)) β (βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π‘ = (β«1βπ)))) |
359 | 358 | rexbidv 3178 |
. . . . . . . 8
β’ (π₯ = π‘ β (βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ)) β βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π‘ = (β«1βπ)))) |
360 | 359 | rexab 3689 |
. . . . . . 7
β’
(βπ‘ β
{π₯ β£ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’) β βπ‘(βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π‘ = (β«1βπ)) β§ βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’))) |
361 | | eqeq1 2736 |
. . . . . . . . . . . . 13
β’ (π₯ = π’ β (π₯ = (β«1βπ) β π’ = (β«1βπ))) |
362 | 361 | anbi2d 629 |
. . . . . . . . . . . 12
β’ (π₯ = π’ β ((βπ β β+ (π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ)) β (βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π’ = (β«1βπ)))) |
363 | 362 | rexbidv 3178 |
. . . . . . . . . . 11
β’ (π₯ = π’ β (βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ)) β βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π’ = (β«1βπ)))) |
364 | 363 | rexab 3689 |
. . . . . . . . . 10
β’
(βπ’ β
{π₯ β£ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’) β βπ’(βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π’ = (β«1βπ)) β§ π = (π‘ + π’))) |
365 | 364 | anbi2i 623 |
. . . . . . . . 9
β’
((βπ β
dom β«1(βπ β β+ (π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π‘ = (β«1βπ)) β§ βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’)) β (βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π‘ = (β«1βπ)) β§ βπ’(βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π’ = (β«1βπ)) β§ π = (π‘ + π’)))) |
366 | | 19.42v 1957 |
. . . . . . . . 9
β’
(βπ’(βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π‘ = (β«1βπ)) β§ (βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π’ = (β«1βπ)) β§ π = (π‘ + π’))) β (βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π‘ = (β«1βπ)) β§ βπ’(βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π’ = (β«1βπ)) β§ π = (π‘ + π’)))) |
367 | | reeanv 3226 |
. . . . . . . . . . . 12
β’
(βπ β dom
β«1βπ
β dom β«1((βπ β β+ (π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π‘ = (β«1βπ)) β§ (βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π’ = (β«1βπ))) β (βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π‘ = (β«1βπ)) β§ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π’ = (β«1βπ)))) |
368 | 367 | anbi1i 624 |
. . . . . . . . . . 11
β’
((βπ β
dom β«1βπ β dom β«1((βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π‘ = (β«1βπ)) β§ (βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π’ = (β«1βπ))) β§ π = (π‘ + π’)) β ((βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π‘ = (β«1βπ)) β§ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π’ = (β«1βπ))) β§ π = (π‘ + π’))) |
369 | | anass 469 |
. . . . . . . . . . 11
β’
(((βπ β
dom β«1(βπ β β+ (π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π‘ = (β«1βπ)) β§ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π’ = (β«1βπ))) β§ π = (π‘ + π’)) β (βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π‘ = (β«1βπ)) β§ (βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π’ = (β«1βπ)) β§ π = (π‘ + π’)))) |
370 | 368, 369 | bitr2i 275 |
. . . . . . . . . 10
β’
((βπ β
dom β«1(βπ β β+ (π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π‘ = (β«1βπ)) β§ (βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π’ = (β«1βπ)) β§ π = (π‘ + π’))) β (βπ β dom β«1βπ β dom
β«1((βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π‘ = (β«1βπ)) β§ (βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π’ = (β«1βπ))) β§ π = (π‘ + π’))) |
371 | 370 | exbii 1850 |
. . . . . . . . 9
β’
(βπ’(βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π‘ = (β«1βπ)) β§ (βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π’ = (β«1βπ)) β§ π = (π‘ + π’))) β βπ’(βπ β dom β«1βπ β dom
β«1((βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π‘ = (β«1βπ)) β§ (βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π’ = (β«1βπ))) β§ π = (π‘ + π’))) |
372 | 365, 366,
371 | 3bitr2i 298 |
. . . . . . . 8
β’
((βπ β
dom β«1(βπ β β+ (π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π‘ = (β«1βπ)) β§ βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’)) β βπ’(βπ β dom β«1βπ β dom
β«1((βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π‘ = (β«1βπ)) β§ (βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π’ = (β«1βπ))) β§ π = (π‘ + π’))) |
373 | 372 | exbii 1850 |
. . . . . . 7
β’
(βπ‘(βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π‘ = (β«1βπ)) β§ βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’)) β βπ‘βπ’(βπ β dom β«1βπ β dom
β«1((βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π‘ = (β«1βπ)) β§ (βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π’ = (β«1βπ))) β§ π = (π‘ + π’))) |
374 | 360, 373 | bitri 274 |
. . . . . 6
β’
(βπ‘ β
{π₯ β£ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’) β βπ‘βπ’(βπ β dom β«1βπ β dom
β«1((βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π‘ = (β«1βπ)) β§ (βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π’ = (β«1βπ))) β§ π = (π‘ + π’))) |
375 | 356, 374 | bitr4di 288 |
. . . . 5
β’ (π β (ββ β dom β«1(βπ¦ β β+
(π§ β β β¦
if((ββπ§) = 0, 0, ((ββπ§) + π¦))) βr β€ (πΉ βf + πΊ) β§ π = (β«1ββ)) β βπ‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’))) |
376 | 375 | abbidv 2801 |
. . . 4
β’ (π β {π β£ ββ β dom β«1(βπ¦ β β+
(π§ β β β¦
if((ββπ§) = 0, 0, ((ββπ§) + π¦))) βr β€ (πΉ βf + πΊ) β§ π = (β«1ββ))} = {π β£ βπ‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’)}) |
377 | 376 | supeq1d 9437 |
. . 3
β’ (π β sup({π β£ ββ β dom β«1(βπ¦ β β+
(π§ β β β¦
if((ββπ§) = 0, 0, ((ββπ§) + π¦))) βr β€ (πΉ βf + πΊ) β§ π = (β«1ββ))}, β*, < )
= sup({π β£
βπ‘ β {π₯ β£ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’)}, β*, <
)) |
378 | | simpr 485 |
. . . . . . . . 9
β’ (((π‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))} β§ π’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}) β§ π = (π‘ + π’)) β π = (π‘ + π’)) |
379 | 6 | sseli 3977 |
. . . . . . . . . . 11
β’ (π‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))} β π‘ β β) |
380 | 379 | ad2antrr 724 |
. . . . . . . . . 10
β’ (((π‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))} β§ π’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}) β§ π = (π‘ + π’)) β π‘ β β) |
381 | 70 | sseli 3977 |
. . . . . . . . . . 11
β’ (π’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))} β π’ β β) |
382 | 381 | ad2antlr 725 |
. . . . . . . . . 10
β’ (((π‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))} β§ π’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}) β§ π = (π‘ + π’)) β π’ β β) |
383 | 380, 382 | readdcld 11239 |
. . . . . . . . 9
β’ (((π‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))} β§ π’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}) β§ π = (π‘ + π’)) β (π‘ + π’) β β) |
384 | 378, 383 | eqeltrd 2833 |
. . . . . . . 8
β’ (((π‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))} β§ π’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}) β§ π = (π‘ + π’)) β π β β) |
385 | 384 | ex 413 |
. . . . . . 7
β’ ((π‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))} β§ π’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}) β (π = (π‘ + π’) β π β β)) |
386 | 385 | rexlimivv 3199 |
. . . . . 6
β’
(βπ‘ β
{π₯ β£ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’) β π β β) |
387 | 386 | abssi 4066 |
. . . . 5
β’ {π β£ βπ‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’)} β β |
388 | 387 | a1i 11 |
. . . 4
β’ (π β {π β£ βπ‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’)} β β) |
389 | 156 | eqcomi 2741 |
. . . . . . . 8
β’ 0 = (0 +
0) |
390 | | rspceov 7452 |
. . . . . . . 8
β’ ((0
β {π₯ β£
βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))} β§ 0 β {π₯ β£ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))} β§ 0 = (0 + 0)) β
βπ‘ β {π₯ β£ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}0 = (π‘ + π’)) |
391 | 389, 390 | mp3an3 1450 |
. . . . . . 7
β’ ((0
β {π₯ β£
βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))} β§ 0 β {π₯ β£ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}) β βπ‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}0 = (π‘ + π’)) |
392 | 48, 100, 391 | syl2anc 584 |
. . . . . 6
β’ (π β βπ‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}0 = (π‘ + π’)) |
393 | | eqeq1 2736 |
. . . . . . . 8
β’ (π = 0 β (π = (π‘ + π’) β 0 = (π‘ + π’))) |
394 | 393 | 2rexbidv 3219 |
. . . . . . 7
β’ (π = 0 β (βπ‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’) β βπ‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}0 = (π‘ + π’))) |
395 | 21, 394 | spcev 3596 |
. . . . . 6
β’
(βπ‘ β
{π₯ β£ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}0 = (π‘ + π’) β βπ βπ‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’)) |
396 | 392, 395 | syl 17 |
. . . . 5
β’ (π β βπ βπ‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’)) |
397 | | abn0 4379 |
. . . . 5
β’ ({π β£ βπ‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’)} β β
β βπ βπ‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’)) |
398 | 396, 397 | sylibr 233 |
. . . 4
β’ (π β {π β£ βπ‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’)} β β
) |
399 | 57, 108 | readdcld 11239 |
. . . . 5
β’ (π β (sup({π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}, β*, < )
+ sup({π₯ β£
βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}, β*, <
)) β β) |
400 | | simpr 485 |
. . . . . . . . 9
β’ (((π β§ (π‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))} β§ π’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))})) β§ π = (π‘ + π’)) β π = (π‘ + π’)) |
401 | 379 | ad2antrl 726 |
. . . . . . . . . . 11
β’ ((π β§ (π‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))} β§ π’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))})) β π‘ β β) |
402 | 381 | ad2antll 727 |
. . . . . . . . . . 11
β’ ((π β§ (π‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))} β§ π’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))})) β π’ β β) |
403 | 57 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ (π‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))} β§ π’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))})) β sup({π₯ β£ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}, β*, < )
β β) |
404 | 108 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ (π‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))} β§ π’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))})) β sup({π₯ β£ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}, β*, < )
β β) |
405 | | supxrub 13299 |
. . . . . . . . . . . . 13
β’ (({π₯ β£ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))} β β*
β§ π‘ β {π₯ β£ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}) β π‘ β€ sup({π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}, β*, <
)) |
406 | 59, 405 | mpan 688 |
. . . . . . . . . . . 12
β’ (π‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))} β π‘ β€ sup({π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}, β*, <
)) |
407 | 406 | ad2antrl 726 |
. . . . . . . . . . 11
β’ ((π β§ (π‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))} β§ π’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))})) β π‘ β€ sup({π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}, β*, <
)) |
408 | | supxrub 13299 |
. . . . . . . . . . . . 13
β’ (({π₯ β£ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))} β β*
β§ π’ β {π₯ β£ βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}) β π’ β€ sup({π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}, β*, <
)) |
409 | 109, 408 | mpan 688 |
. . . . . . . . . . . 12
β’ (π’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))} β π’ β€ sup({π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}, β*, <
)) |
410 | 409 | ad2antll 727 |
. . . . . . . . . . 11
β’ ((π β§ (π‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))} β§ π’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))})) β π’ β€ sup({π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}, β*, <
)) |
411 | 401, 402,
403, 404, 407, 410 | le2addd 11829 |
. . . . . . . . . 10
β’ ((π β§ (π‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))} β§ π’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))})) β (π‘ + π’) β€ (sup({π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}, β*, < )
+ sup({π₯ β£
βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}, β*, <
))) |
412 | 411 | adantr 481 |
. . . . . . . . 9
β’ (((π β§ (π‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))} β§ π’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))})) β§ π = (π‘ + π’)) β (π‘ + π’) β€ (sup({π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}, β*, < )
+ sup({π₯ β£
βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}, β*, <
))) |
413 | 400, 412 | eqbrtrd 5169 |
. . . . . . . 8
β’ (((π β§ (π‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))} β§ π’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))})) β§ π = (π‘ + π’)) β π β€ (sup({π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}, β*, < )
+ sup({π₯ β£
βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}, β*, <
))) |
414 | 413 | ex 413 |
. . . . . . 7
β’ ((π β§ (π‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))} β§ π’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))})) β (π = (π‘ + π’) β π β€ (sup({π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}, β*, < )
+ sup({π₯ β£
βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}, β*, <
)))) |
415 | 414 | rexlimdvva 3211 |
. . . . . 6
β’ (π β (βπ‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’) β π β€ (sup({π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}, β*, < )
+ sup({π₯ β£
βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}, β*, <
)))) |
416 | 415 | alrimiv 1930 |
. . . . 5
β’ (π β βπ(βπ‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’) β π β€ (sup({π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}, β*, < )
+ sup({π₯ β£
βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}, β*, <
)))) |
417 | | breq2 5151 |
. . . . . . . 8
β’ (π = (sup({π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}, β*, < )
+ sup({π₯ β£
βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}, β*, <
)) β (π β€ π β π β€ (sup({π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}, β*, < )
+ sup({π₯ β£
βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}, β*, <
)))) |
418 | 417 | ralbidv 3177 |
. . . . . . 7
β’ (π = (sup({π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}, β*, < )
+ sup({π₯ β£
βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}, β*, <
)) β (βπ β
{π β£ βπ‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’)}π β€ π β βπ β {π β£ βπ‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’)}π β€ (sup({π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}, β*, < )
+ sup({π₯ β£
βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}, β*, <
)))) |
419 | | eqeq1 2736 |
. . . . . . . . 9
β’ (π = π β (π = (π‘ + π’) β π = (π‘ + π’))) |
420 | 419 | 2rexbidv 3219 |
. . . . . . . 8
β’ (π = π β (βπ‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’) β βπ‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’))) |
421 | 420 | ralab 3686 |
. . . . . . 7
β’
(βπ β
{π β£ βπ‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’)}π β€ (sup({π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}, β*, < )
+ sup({π₯ β£
βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}, β*, <
)) β βπ(βπ‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’) β π β€ (sup({π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}, β*, < )
+ sup({π₯ β£
βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}, β*, <
)))) |
422 | 418, 421 | bitrdi 286 |
. . . . . 6
β’ (π = (sup({π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}, β*, < )
+ sup({π₯ β£
βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}, β*, <
)) β (βπ β
{π β£ βπ‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’)}π β€ π β βπ(βπ‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’) β π β€ (sup({π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}, β*, < )
+ sup({π₯ β£
βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}, β*, <
))))) |
423 | 422 | rspcev 3612 |
. . . . 5
β’
(((sup({π₯ β£
βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}, β*, < )
+ sup({π₯ β£
βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}, β*, <
)) β β β§ βπ(βπ‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’) β π β€ (sup({π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}, β*, < )
+ sup({π₯ β£
βπ β dom
β«1(βπ
β β+ (π§ β β β¦ if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}, β*, <
)))) β βπ β
β βπ β
{π β£ βπ‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’)}π β€ π) |
424 | 399, 416,
423 | syl2anc 584 |
. . . 4
β’ (π β βπ β β βπ β {π β£ βπ‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’)}π β€ π) |
425 | | supxrre 13302 |
. . . 4
β’ (({π β£ βπ‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’)} β β β§ {π β£ βπ‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’)} β β
β§ βπ β β βπ β {π β£ βπ‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’)}π β€ π) β sup({π β£ βπ‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’)}, β*, < ) = sup({π β£ βπ‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’)}, β, < )) |
426 | 388, 398,
424, 425 | syl3anc 1371 |
. . 3
β’ (π β sup({π β£ βπ‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’)}, β*, < ) = sup({π β£ βπ‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’)}, β, < )) |
427 | 131, 377,
426 | 3eqtrd 2776 |
. 2
β’ (π β
(β«2β(πΉ
βf + πΊ)) =
sup({π β£ βπ‘ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΉ β§ π₯ = (β«1βπ))}βπ’ β {π₯ β£ βπ β dom β«1(βπ β β+
(π§ β β β¦
if((πβπ§) = 0, 0, ((πβπ§) + π))) βr β€ πΊ β§ π₯ = (β«1βπ))}π = (π‘ + π’)}, β, < )) |
428 | 116, 123,
427 | 3eqtr4rd 2783 |
1
β’ (π β
(β«2β(πΉ
βf + πΊ)) =
((β«2βπΉ) + (β«2βπΊ))) |