Step | Hyp | Ref
| Expression |
1 | | itgcnval.2 |
. . . . . . . 8
โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ
๐ฟ1) |
2 | | iblmbf 25148 |
. . . . . . . 8
โข ((๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1 โ (๐ฅ โ ๐ด โฆ ๐ต) โ MblFn) |
3 | 1, 2 | syl 17 |
. . . . . . 7
โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ MblFn) |
4 | | itgcnval.1 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ ๐) |
5 | 3, 4 | mbfmptcl 25016 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) |
6 | 5 | recld 15086 |
. . . . 5
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ๐ต) โ โ) |
7 | 5 | iblcn 25179 |
. . . . . . 7
โข (๐ โ ((๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1 โ
((๐ฅ โ ๐ด โฆ (โโ๐ต)) โ ๐ฟ1
โง (๐ฅ โ ๐ด โฆ (โโ๐ต)) โ
๐ฟ1))) |
8 | 1, 7 | mpbid 231 |
. . . . . 6
โข (๐ โ ((๐ฅ โ ๐ด โฆ (โโ๐ต)) โ ๐ฟ1 โง (๐ฅ โ ๐ด โฆ (โโ๐ต)) โ
๐ฟ1)) |
9 | 8 | simpld 496 |
. . . . 5
โข (๐ โ (๐ฅ โ ๐ด โฆ (โโ๐ต)) โ
๐ฟ1) |
10 | 6, 9 | itgcl 25164 |
. . . 4
โข (๐ โ โซ๐ด(โโ๐ต) d๐ฅ โ โ) |
11 | | ax-icn 11117 |
. . . . 5
โข i โ
โ |
12 | 5 | imcld 15087 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ๐ต) โ โ) |
13 | 8 | simprd 497 |
. . . . . 6
โข (๐ โ (๐ฅ โ ๐ด โฆ (โโ๐ต)) โ
๐ฟ1) |
14 | 12, 13 | itgcl 25164 |
. . . . 5
โข (๐ โ โซ๐ด(โโ๐ต) d๐ฅ โ โ) |
15 | | mulcl 11142 |
. . . . 5
โข ((i
โ โ โง โซ๐ด(โโ๐ต) d๐ฅ โ โ) โ (i ยท
โซ๐ด(โโ๐ต) d๐ฅ) โ โ) |
16 | 11, 14, 15 | sylancr 588 |
. . . 4
โข (๐ โ (i ยท โซ๐ด(โโ๐ต) d๐ฅ) โ โ) |
17 | 10, 16 | negdid 11532 |
. . 3
โข (๐ โ -(โซ๐ด(โโ๐ต) d๐ฅ + (i ยท โซ๐ด(โโ๐ต) d๐ฅ)) = (-โซ๐ด(โโ๐ต) d๐ฅ + -(i ยท โซ๐ด(โโ๐ต) d๐ฅ))) |
18 | | 0re 11164 |
. . . . . . . 8
โข 0 โ
โ |
19 | | ifcl 4536 |
. . . . . . . 8
โข
(((โโ๐ต)
โ โ โง 0 โ โ) โ if(0 โค (โโ๐ต), (โโ๐ต), 0) โ
โ) |
20 | 6, 18, 19 | sylancl 587 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐ด) โ if(0 โค (โโ๐ต), (โโ๐ต), 0) โ
โ) |
21 | 6 | iblre 25174 |
. . . . . . . . 9
โข (๐ โ ((๐ฅ โ ๐ด โฆ (โโ๐ต)) โ ๐ฟ1 โ
((๐ฅ โ ๐ด โฆ if(0 โค
(โโ๐ต),
(โโ๐ต), 0))
โ ๐ฟ1 โง (๐ฅ โ ๐ด โฆ if(0 โค -(โโ๐ต), -(โโ๐ต), 0)) โ
๐ฟ1))) |
22 | 9, 21 | mpbid 231 |
. . . . . . . 8
โข (๐ โ ((๐ฅ โ ๐ด โฆ if(0 โค (โโ๐ต), (โโ๐ต), 0)) โ
๐ฟ1 โง (๐ฅ โ ๐ด โฆ if(0 โค -(โโ๐ต), -(โโ๐ต), 0)) โ
๐ฟ1)) |
23 | 22 | simpld 496 |
. . . . . . 7
โข (๐ โ (๐ฅ โ ๐ด โฆ if(0 โค (โโ๐ต), (โโ๐ต), 0)) โ
๐ฟ1) |
24 | 20, 23 | itgcl 25164 |
. . . . . 6
โข (๐ โ โซ๐ดif(0 โค (โโ๐ต), (โโ๐ต), 0) d๐ฅ โ โ) |
25 | 6 | renegcld 11589 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ด) โ -(โโ๐ต) โ โ) |
26 | | ifcl 4536 |
. . . . . . . 8
โข
((-(โโ๐ต)
โ โ โง 0 โ โ) โ if(0 โค -(โโ๐ต), -(โโ๐ต), 0) โ
โ) |
27 | 25, 18, 26 | sylancl 587 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐ด) โ if(0 โค -(โโ๐ต), -(โโ๐ต), 0) โ
โ) |
28 | 22 | simprd 497 |
. . . . . . 7
โข (๐ โ (๐ฅ โ ๐ด โฆ if(0 โค -(โโ๐ต), -(โโ๐ต), 0)) โ
๐ฟ1) |
29 | 27, 28 | itgcl 25164 |
. . . . . 6
โข (๐ โ โซ๐ดif(0 โค -(โโ๐ต), -(โโ๐ต), 0) d๐ฅ โ โ) |
30 | 24, 29 | negsubdi2d 11535 |
. . . . 5
โข (๐ โ -(โซ๐ดif(0 โค (โโ๐ต), (โโ๐ต), 0) d๐ฅ โ โซ๐ดif(0 โค -(โโ๐ต), -(โโ๐ต), 0) d๐ฅ) = (โซ๐ดif(0 โค -(โโ๐ต), -(โโ๐ต), 0) d๐ฅ โ โซ๐ดif(0 โค (โโ๐ต), (โโ๐ต), 0) d๐ฅ)) |
31 | 6, 9 | itgreval 25177 |
. . . . . 6
โข (๐ โ โซ๐ด(โโ๐ต) d๐ฅ = (โซ๐ดif(0 โค (โโ๐ต), (โโ๐ต), 0) d๐ฅ โ โซ๐ดif(0 โค -(โโ๐ต), -(โโ๐ต), 0) d๐ฅ)) |
32 | 31 | negeqd 11402 |
. . . . 5
โข (๐ โ -โซ๐ด(โโ๐ต) d๐ฅ = -(โซ๐ดif(0 โค (โโ๐ต), (โโ๐ต), 0) d๐ฅ โ โซ๐ดif(0 โค -(โโ๐ต), -(โโ๐ต), 0) d๐ฅ)) |
33 | 5 | negcld 11506 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ด) โ -๐ต โ โ) |
34 | 33 | recld 15086 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ-๐ต) โ โ) |
35 | 4, 1 | iblneg 25183 |
. . . . . . . . 9
โข (๐ โ (๐ฅ โ ๐ด โฆ -๐ต) โ
๐ฟ1) |
36 | 33 | iblcn 25179 |
. . . . . . . . 9
โข (๐ โ ((๐ฅ โ ๐ด โฆ -๐ต) โ ๐ฟ1 โ
((๐ฅ โ ๐ด โฆ (โโ-๐ต)) โ ๐ฟ1
โง (๐ฅ โ ๐ด โฆ (โโ-๐ต)) โ
๐ฟ1))) |
37 | 35, 36 | mpbid 231 |
. . . . . . . 8
โข (๐ โ ((๐ฅ โ ๐ด โฆ (โโ-๐ต)) โ ๐ฟ1 โง (๐ฅ โ ๐ด โฆ (โโ-๐ต)) โ
๐ฟ1)) |
38 | 37 | simpld 496 |
. . . . . . 7
โข (๐ โ (๐ฅ โ ๐ด โฆ (โโ-๐ต)) โ
๐ฟ1) |
39 | 34, 38 | itgreval 25177 |
. . . . . 6
โข (๐ โ โซ๐ด(โโ-๐ต) d๐ฅ = (โซ๐ดif(0 โค (โโ-๐ต), (โโ-๐ต), 0) d๐ฅ โ โซ๐ดif(0 โค -(โโ-๐ต), -(โโ-๐ต), 0) d๐ฅ)) |
40 | 5 | renegd 15101 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ-๐ต) = -(โโ๐ต)) |
41 | 40 | breq2d 5122 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ ๐ด) โ (0 โค (โโ-๐ต) โ 0 โค
-(โโ๐ต))) |
42 | 41, 40 | ifbieq1d 4515 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ด) โ if(0 โค (โโ-๐ต), (โโ-๐ต), 0) = if(0 โค
-(โโ๐ต),
-(โโ๐ต),
0)) |
43 | 42 | itgeq2dv 25162 |
. . . . . . 7
โข (๐ โ โซ๐ดif(0 โค (โโ-๐ต), (โโ-๐ต), 0) d๐ฅ = โซ๐ดif(0 โค -(โโ๐ต), -(โโ๐ต), 0) d๐ฅ) |
44 | 40 | negeqd 11402 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ ๐ด) โ -(โโ-๐ต) = --(โโ๐ต)) |
45 | 6 | recnd 11190 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ๐ต) โ โ) |
46 | 45 | negnegd 11510 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ ๐ด) โ --(โโ๐ต) = (โโ๐ต)) |
47 | 44, 46 | eqtrd 2777 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ ๐ด) โ -(โโ-๐ต) = (โโ๐ต)) |
48 | 47 | breq2d 5122 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ ๐ด) โ (0 โค -(โโ-๐ต) โ 0 โค
(โโ๐ต))) |
49 | 48, 47 | ifbieq1d 4515 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ด) โ if(0 โค -(โโ-๐ต), -(โโ-๐ต), 0) = if(0 โค
(โโ๐ต),
(โโ๐ต),
0)) |
50 | 49 | itgeq2dv 25162 |
. . . . . . 7
โข (๐ โ โซ๐ดif(0 โค -(โโ-๐ต), -(โโ-๐ต), 0) d๐ฅ = โซ๐ดif(0 โค (โโ๐ต), (โโ๐ต), 0) d๐ฅ) |
51 | 43, 50 | oveq12d 7380 |
. . . . . 6
โข (๐ โ (โซ๐ดif(0 โค (โโ-๐ต), (โโ-๐ต), 0) d๐ฅ โ โซ๐ดif(0 โค -(โโ-๐ต), -(โโ-๐ต), 0) d๐ฅ) = (โซ๐ดif(0 โค -(โโ๐ต), -(โโ๐ต), 0) d๐ฅ โ โซ๐ดif(0 โค (โโ๐ต), (โโ๐ต), 0) d๐ฅ)) |
52 | 39, 51 | eqtrd 2777 |
. . . . 5
โข (๐ โ โซ๐ด(โโ-๐ต) d๐ฅ = (โซ๐ดif(0 โค -(โโ๐ต), -(โโ๐ต), 0) d๐ฅ โ โซ๐ดif(0 โค (โโ๐ต), (โโ๐ต), 0) d๐ฅ)) |
53 | 30, 32, 52 | 3eqtr4d 2787 |
. . . 4
โข (๐ โ -โซ๐ด(โโ๐ต) d๐ฅ = โซ๐ด(โโ-๐ต) d๐ฅ) |
54 | | mulneg2 11599 |
. . . . . 6
โข ((i
โ โ โง โซ๐ด(โโ๐ต) d๐ฅ โ โ) โ (i ยท
-โซ๐ด(โโ๐ต) d๐ฅ) = -(i ยท โซ๐ด(โโ๐ต) d๐ฅ)) |
55 | 11, 14, 54 | sylancr 588 |
. . . . 5
โข (๐ โ (i ยท -โซ๐ด(โโ๐ต) d๐ฅ) = -(i ยท โซ๐ด(โโ๐ต) d๐ฅ)) |
56 | | ifcl 4536 |
. . . . . . . . . . 11
โข
(((โโ๐ต)
โ โ โง 0 โ โ) โ if(0 โค (โโ๐ต), (โโ๐ต), 0) โ
โ) |
57 | 12, 18, 56 | sylancl 587 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ ๐ด) โ if(0 โค (โโ๐ต), (โโ๐ต), 0) โ
โ) |
58 | 12 | iblre 25174 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ฅ โ ๐ด โฆ (โโ๐ต)) โ ๐ฟ1 โ
((๐ฅ โ ๐ด โฆ if(0 โค
(โโ๐ต),
(โโ๐ต), 0))
โ ๐ฟ1 โง (๐ฅ โ ๐ด โฆ if(0 โค -(โโ๐ต), -(โโ๐ต), 0)) โ
๐ฟ1))) |
59 | 13, 58 | mpbid 231 |
. . . . . . . . . . 11
โข (๐ โ ((๐ฅ โ ๐ด โฆ if(0 โค (โโ๐ต), (โโ๐ต), 0)) โ
๐ฟ1 โง (๐ฅ โ ๐ด โฆ if(0 โค -(โโ๐ต), -(โโ๐ต), 0)) โ
๐ฟ1)) |
60 | 59 | simpld 496 |
. . . . . . . . . 10
โข (๐ โ (๐ฅ โ ๐ด โฆ if(0 โค (โโ๐ต), (โโ๐ต), 0)) โ
๐ฟ1) |
61 | 57, 60 | itgcl 25164 |
. . . . . . . . 9
โข (๐ โ โซ๐ดif(0 โค (โโ๐ต), (โโ๐ต), 0) d๐ฅ โ โ) |
62 | 12 | renegcld 11589 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ ๐ด) โ -(โโ๐ต) โ โ) |
63 | | ifcl 4536 |
. . . . . . . . . . 11
โข
((-(โโ๐ต)
โ โ โง 0 โ โ) โ if(0 โค -(โโ๐ต), -(โโ๐ต), 0) โ
โ) |
64 | 62, 18, 63 | sylancl 587 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ ๐ด) โ if(0 โค -(โโ๐ต), -(โโ๐ต), 0) โ
โ) |
65 | 59 | simprd 497 |
. . . . . . . . . 10
โข (๐ โ (๐ฅ โ ๐ด โฆ if(0 โค -(โโ๐ต), -(โโ๐ต), 0)) โ
๐ฟ1) |
66 | 64, 65 | itgcl 25164 |
. . . . . . . . 9
โข (๐ โ โซ๐ดif(0 โค -(โโ๐ต), -(โโ๐ต), 0) d๐ฅ โ โ) |
67 | 61, 66 | negsubdi2d 11535 |
. . . . . . . 8
โข (๐ โ -(โซ๐ดif(0 โค (โโ๐ต), (โโ๐ต), 0) d๐ฅ โ โซ๐ดif(0 โค -(โโ๐ต), -(โโ๐ต), 0) d๐ฅ) = (โซ๐ดif(0 โค -(โโ๐ต), -(โโ๐ต), 0) d๐ฅ โ โซ๐ดif(0 โค (โโ๐ต), (โโ๐ต), 0) d๐ฅ)) |
68 | 5 | imnegd 15102 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ-๐ต) = -(โโ๐ต)) |
69 | 68 | breq2d 5122 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ ๐ด) โ (0 โค (โโ-๐ต) โ 0 โค
-(โโ๐ต))) |
70 | 69, 68 | ifbieq1d 4515 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ ๐ด) โ if(0 โค (โโ-๐ต), (โโ-๐ต), 0) = if(0 โค
-(โโ๐ต),
-(โโ๐ต),
0)) |
71 | 70 | itgeq2dv 25162 |
. . . . . . . . 9
โข (๐ โ โซ๐ดif(0 โค (โโ-๐ต), (โโ-๐ต), 0) d๐ฅ = โซ๐ดif(0 โค -(โโ๐ต), -(โโ๐ต), 0) d๐ฅ) |
72 | 68 | negeqd 11402 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ ๐ด) โ -(โโ-๐ต) = --(โโ๐ต)) |
73 | 12 | recnd 11190 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ๐ต) โ โ) |
74 | 73 | negnegd 11510 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ ๐ด) โ --(โโ๐ต) = (โโ๐ต)) |
75 | 72, 74 | eqtrd 2777 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ ๐ด) โ -(โโ-๐ต) = (โโ๐ต)) |
76 | 75 | breq2d 5122 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ ๐ด) โ (0 โค -(โโ-๐ต) โ 0 โค
(โโ๐ต))) |
77 | 76, 75 | ifbieq1d 4515 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ ๐ด) โ if(0 โค -(โโ-๐ต), -(โโ-๐ต), 0) = if(0 โค
(โโ๐ต),
(โโ๐ต),
0)) |
78 | 77 | itgeq2dv 25162 |
. . . . . . . . 9
โข (๐ โ โซ๐ดif(0 โค -(โโ-๐ต), -(โโ-๐ต), 0) d๐ฅ = โซ๐ดif(0 โค (โโ๐ต), (โโ๐ต), 0) d๐ฅ) |
79 | 71, 78 | oveq12d 7380 |
. . . . . . . 8
โข (๐ โ (โซ๐ดif(0 โค (โโ-๐ต), (โโ-๐ต), 0) d๐ฅ โ โซ๐ดif(0 โค -(โโ-๐ต), -(โโ-๐ต), 0) d๐ฅ) = (โซ๐ดif(0 โค -(โโ๐ต), -(โโ๐ต), 0) d๐ฅ โ โซ๐ดif(0 โค (โโ๐ต), (โโ๐ต), 0) d๐ฅ)) |
80 | 67, 79 | eqtr4d 2780 |
. . . . . . 7
โข (๐ โ -(โซ๐ดif(0 โค (โโ๐ต), (โโ๐ต), 0) d๐ฅ โ โซ๐ดif(0 โค -(โโ๐ต), -(โโ๐ต), 0) d๐ฅ) = (โซ๐ดif(0 โค (โโ-๐ต), (โโ-๐ต), 0) d๐ฅ โ โซ๐ดif(0 โค -(โโ-๐ต), -(โโ-๐ต), 0) d๐ฅ)) |
81 | 12, 13 | itgreval 25177 |
. . . . . . . 8
โข (๐ โ โซ๐ด(โโ๐ต) d๐ฅ = (โซ๐ดif(0 โค (โโ๐ต), (โโ๐ต), 0) d๐ฅ โ โซ๐ดif(0 โค -(โโ๐ต), -(โโ๐ต), 0) d๐ฅ)) |
82 | 81 | negeqd 11402 |
. . . . . . 7
โข (๐ โ -โซ๐ด(โโ๐ต) d๐ฅ = -(โซ๐ดif(0 โค (โโ๐ต), (โโ๐ต), 0) d๐ฅ โ โซ๐ดif(0 โค -(โโ๐ต), -(โโ๐ต), 0) d๐ฅ)) |
83 | 33 | imcld 15087 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ-๐ต) โ โ) |
84 | 37 | simprd 497 |
. . . . . . . 8
โข (๐ โ (๐ฅ โ ๐ด โฆ (โโ-๐ต)) โ
๐ฟ1) |
85 | 83, 84 | itgreval 25177 |
. . . . . . 7
โข (๐ โ โซ๐ด(โโ-๐ต) d๐ฅ = (โซ๐ดif(0 โค (โโ-๐ต), (โโ-๐ต), 0) d๐ฅ โ โซ๐ดif(0 โค -(โโ-๐ต), -(โโ-๐ต), 0) d๐ฅ)) |
86 | 80, 82, 85 | 3eqtr4d 2787 |
. . . . . 6
โข (๐ โ -โซ๐ด(โโ๐ต) d๐ฅ = โซ๐ด(โโ-๐ต) d๐ฅ) |
87 | 86 | oveq2d 7378 |
. . . . 5
โข (๐ โ (i ยท -โซ๐ด(โโ๐ต) d๐ฅ) = (i ยท โซ๐ด(โโ-๐ต) d๐ฅ)) |
88 | 55, 87 | eqtr3d 2779 |
. . . 4
โข (๐ โ -(i ยท โซ๐ด(โโ๐ต) d๐ฅ) = (i ยท โซ๐ด(โโ-๐ต) d๐ฅ)) |
89 | 53, 88 | oveq12d 7380 |
. . 3
โข (๐ โ (-โซ๐ด(โโ๐ต) d๐ฅ + -(i ยท โซ๐ด(โโ๐ต) d๐ฅ)) = (โซ๐ด(โโ-๐ต) d๐ฅ + (i ยท โซ๐ด(โโ-๐ต) d๐ฅ))) |
90 | 17, 89 | eqtrd 2777 |
. 2
โข (๐ โ -(โซ๐ด(โโ๐ต) d๐ฅ + (i ยท โซ๐ด(โโ๐ต) d๐ฅ)) = (โซ๐ด(โโ-๐ต) d๐ฅ + (i ยท โซ๐ด(โโ-๐ต) d๐ฅ))) |
91 | 4, 1 | itgcnval 25180 |
. . 3
โข (๐ โ โซ๐ด๐ต d๐ฅ = (โซ๐ด(โโ๐ต) d๐ฅ + (i ยท โซ๐ด(โโ๐ต) d๐ฅ))) |
92 | 91 | negeqd 11402 |
. 2
โข (๐ โ -โซ๐ด๐ต d๐ฅ = -(โซ๐ด(โโ๐ต) d๐ฅ + (i ยท โซ๐ด(โโ๐ต) d๐ฅ))) |
93 | 33, 35 | itgcnval 25180 |
. 2
โข (๐ โ โซ๐ด-๐ต d๐ฅ = (โซ๐ด(โโ-๐ต) d๐ฅ + (i ยท โซ๐ด(โโ-๐ต) d๐ฅ))) |
94 | 90, 92, 93 | 3eqtr4d 2787 |
1
โข (๐ โ -โซ๐ด๐ต d๐ฅ = โซ๐ด-๐ต d๐ฅ) |