Step | Hyp | Ref
| Expression |
1 | | lnopeq0lem1.2 |
. . . 4
โข ๐ด โ โ |
2 | | lnopeq0.1 |
. . . . . 6
โข ๐ โ LinOp |
3 | 2 | lnopfi 30960 |
. . . . 5
โข ๐: โโถ
โ |
4 | 3 | ffvelcdmi 7038 |
. . . 4
โข (๐ด โ โ โ (๐โ๐ด) โ โ) |
5 | 1, 4 | ax-mp 5 |
. . 3
โข (๐โ๐ด) โ โ |
6 | | lnopeq0lem1.3 |
. . 3
โข ๐ต โ โ |
7 | 3 | ffvelcdmi 7038 |
. . . 4
โข (๐ต โ โ โ (๐โ๐ต) โ โ) |
8 | 6, 7 | ax-mp 5 |
. . 3
โข (๐โ๐ต) โ โ |
9 | 5, 6, 8, 1 | polid2i 30148 |
. 2
โข ((๐โ๐ด) ยทih ๐ต) = ((((((๐โ๐ด) +โ (๐โ๐ต)) ยทih
(๐ด +โ
๐ต)) โ (((๐โ๐ด) โโ (๐โ๐ต)) ยทih
(๐ด
โโ ๐ต))) + (i ยท ((((๐โ๐ด) +โ (i
ยทโ (๐โ๐ต))) ยทih
(๐ด +โ (i
ยทโ ๐ต))) โ (((๐โ๐ด) โโ (i
ยทโ (๐โ๐ต))) ยทih
(๐ด
โโ (i ยทโ ๐ต)))))) / 4) |
10 | 2 | lnopaddi 30962 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐โ(๐ด +โ ๐ต)) = ((๐โ๐ด) +โ (๐โ๐ต))) |
11 | 1, 6, 10 | mp2an 691 |
. . . . . 6
โข (๐โ(๐ด +โ ๐ต)) = ((๐โ๐ด) +โ (๐โ๐ต)) |
12 | 11 | oveq1i 7371 |
. . . . 5
โข ((๐โ(๐ด +โ ๐ต)) ยทih
(๐ด +โ
๐ต)) = (((๐โ๐ด) +โ (๐โ๐ต)) ยทih
(๐ด +โ
๐ต)) |
13 | 2 | lnopsubi 30965 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐โ(๐ด โโ ๐ต)) = ((๐โ๐ด) โโ (๐โ๐ต))) |
14 | 1, 6, 13 | mp2an 691 |
. . . . . 6
โข (๐โ(๐ด โโ ๐ต)) = ((๐โ๐ด) โโ (๐โ๐ต)) |
15 | 14 | oveq1i 7371 |
. . . . 5
โข ((๐โ(๐ด โโ ๐ต))
ยทih (๐ด โโ ๐ต)) = (((๐โ๐ด) โโ (๐โ๐ต)) ยทih
(๐ด
โโ ๐ต)) |
16 | 12, 15 | oveq12i 7373 |
. . . 4
โข (((๐โ(๐ด +โ ๐ต)) ยทih
(๐ด +โ
๐ต)) โ ((๐โ(๐ด โโ ๐ต))
ยทih (๐ด โโ ๐ต))) = ((((๐โ๐ด) +โ (๐โ๐ต)) ยทih
(๐ด +โ
๐ต)) โ (((๐โ๐ด) โโ (๐โ๐ต)) ยทih
(๐ด
โโ ๐ต))) |
17 | | ax-icn 11118 |
. . . . . . . 8
โข i โ
โ |
18 | 2 | lnopaddmuli 30964 |
. . . . . . . 8
โข ((i
โ โ โง ๐ด
โ โ โง ๐ต
โ โ) โ (๐โ(๐ด +โ (i
ยทโ ๐ต))) = ((๐โ๐ด) +โ (i
ยทโ (๐โ๐ต)))) |
19 | 17, 1, 6, 18 | mp3an 1462 |
. . . . . . 7
โข (๐โ(๐ด +โ (i
ยทโ ๐ต))) = ((๐โ๐ด) +โ (i
ยทโ (๐โ๐ต))) |
20 | 19 | oveq1i 7371 |
. . . . . 6
โข ((๐โ(๐ด +โ (i
ยทโ ๐ต))) ยทih
(๐ด +โ (i
ยทโ ๐ต))) = (((๐โ๐ด) +โ (i
ยทโ (๐โ๐ต))) ยทih
(๐ด +โ (i
ยทโ ๐ต))) |
21 | 2 | lnopsubmuli 30966 |
. . . . . . . 8
โข ((i
โ โ โง ๐ด
โ โ โง ๐ต
โ โ) โ (๐โ(๐ด โโ (i
ยทโ ๐ต))) = ((๐โ๐ด) โโ (i
ยทโ (๐โ๐ต)))) |
22 | 17, 1, 6, 21 | mp3an 1462 |
. . . . . . 7
โข (๐โ(๐ด โโ (i
ยทโ ๐ต))) = ((๐โ๐ด) โโ (i
ยทโ (๐โ๐ต))) |
23 | 22 | oveq1i 7371 |
. . . . . 6
โข ((๐โ(๐ด โโ (i
ยทโ ๐ต))) ยทih
(๐ด
โโ (i ยทโ ๐ต))) = (((๐โ๐ด) โโ (i
ยทโ (๐โ๐ต))) ยทih
(๐ด
โโ (i ยทโ ๐ต))) |
24 | 20, 23 | oveq12i 7373 |
. . . . 5
โข (((๐โ(๐ด +โ (i
ยทโ ๐ต))) ยทih
(๐ด +โ (i
ยทโ ๐ต))) โ ((๐โ(๐ด โโ (i
ยทโ ๐ต))) ยทih
(๐ด
โโ (i ยทโ ๐ต)))) = ((((๐โ๐ด) +โ (i
ยทโ (๐โ๐ต))) ยทih
(๐ด +โ (i
ยทโ ๐ต))) โ (((๐โ๐ด) โโ (i
ยทโ (๐โ๐ต))) ยทih
(๐ด
โโ (i ยทโ ๐ต)))) |
25 | 24 | oveq2i 7372 |
. . . 4
โข (i
ยท (((๐โ(๐ด +โ (i
ยทโ ๐ต))) ยทih
(๐ด +โ (i
ยทโ ๐ต))) โ ((๐โ(๐ด โโ (i
ยทโ ๐ต))) ยทih
(๐ด
โโ (i ยทโ ๐ต))))) = (i ยท ((((๐โ๐ด) +โ (i
ยทโ (๐โ๐ต))) ยทih
(๐ด +โ (i
ยทโ ๐ต))) โ (((๐โ๐ด) โโ (i
ยทโ (๐โ๐ต))) ยทih
(๐ด
โโ (i ยทโ ๐ต))))) |
26 | 16, 25 | oveq12i 7373 |
. . 3
โข ((((๐โ(๐ด +โ ๐ต)) ยทih
(๐ด +โ
๐ต)) โ ((๐โ(๐ด โโ ๐ต))
ยทih (๐ด โโ ๐ต))) + (i ยท (((๐โ(๐ด +โ (i
ยทโ ๐ต))) ยทih
(๐ด +โ (i
ยทโ ๐ต))) โ ((๐โ(๐ด โโ (i
ยทโ ๐ต))) ยทih
(๐ด
โโ (i ยทโ ๐ต)))))) = (((((๐โ๐ด) +โ (๐โ๐ต)) ยทih
(๐ด +โ
๐ต)) โ (((๐โ๐ด) โโ (๐โ๐ต)) ยทih
(๐ด
โโ ๐ต))) + (i ยท ((((๐โ๐ด) +โ (i
ยทโ (๐โ๐ต))) ยทih
(๐ด +โ (i
ยทโ ๐ต))) โ (((๐โ๐ด) โโ (i
ยทโ (๐โ๐ต))) ยทih
(๐ด
โโ (i ยทโ ๐ต)))))) |
27 | 26 | oveq1i 7371 |
. 2
โข
(((((๐โ(๐ด +โ ๐ต))
ยทih (๐ด +โ ๐ต)) โ ((๐โ(๐ด โโ ๐ต))
ยทih (๐ด โโ ๐ต))) + (i ยท (((๐โ(๐ด +โ (i
ยทโ ๐ต))) ยทih
(๐ด +โ (i
ยทโ ๐ต))) โ ((๐โ(๐ด โโ (i
ยทโ ๐ต))) ยทih
(๐ด
โโ (i ยทโ ๐ต)))))) / 4) = ((((((๐โ๐ด) +โ (๐โ๐ต)) ยทih
(๐ด +โ
๐ต)) โ (((๐โ๐ด) โโ (๐โ๐ต)) ยทih
(๐ด
โโ ๐ต))) + (i ยท ((((๐โ๐ด) +โ (i
ยทโ (๐โ๐ต))) ยทih
(๐ด +โ (i
ยทโ ๐ต))) โ (((๐โ๐ด) โโ (i
ยทโ (๐โ๐ต))) ยทih
(๐ด
โโ (i ยทโ ๐ต)))))) / 4) |
28 | 9, 27 | eqtr4i 2764 |
1
โข ((๐โ๐ด) ยทih ๐ต) = (((((๐โ(๐ด +โ ๐ต)) ยทih
(๐ด +โ
๐ต)) โ ((๐โ(๐ด โโ ๐ต))
ยทih (๐ด โโ ๐ต))) + (i ยท (((๐โ(๐ด +โ (i
ยทโ ๐ต))) ยทih
(๐ด +โ (i
ยทโ ๐ต))) โ ((๐โ(๐ด โโ (i
ยทโ ๐ต))) ยทih
(๐ด
โโ (i ยทโ ๐ต)))))) / 4) |