Step | Hyp | Ref
| Expression |
1 | | elin 3930 |
. . 3
โข (๐ โ (LinFn โฉ ContFn)
โ (๐ โ LinFn
โง ๐ โ
ContFn)) |
2 | | fveq1 6845 |
. . . . . . . 8
โข (๐ = if(๐ โ (LinFn โฉ ContFn), ๐, ( โ ร {0})) โ
(๐โ๐ด) = (if(๐ โ (LinFn โฉ ContFn), ๐, ( โ ร
{0}))โ๐ด)) |
3 | 2 | fveq2d 6850 |
. . . . . . 7
โข (๐ = if(๐ โ (LinFn โฉ ContFn), ๐, ( โ ร {0})) โ
(absโ(๐โ๐ด)) = (absโ(if(๐ โ (LinFn โฉ ContFn),
๐, ( โ ร
{0}))โ๐ด))) |
4 | | fveq2 6846 |
. . . . . . . 8
โข (๐ = if(๐ โ (LinFn โฉ ContFn), ๐, ( โ ร {0})) โ
(normfnโ๐)
= (normfnโif(๐ โ (LinFn โฉ ContFn), ๐, ( โ ร
{0})))) |
5 | 4 | oveq1d 7376 |
. . . . . . 7
โข (๐ = if(๐ โ (LinFn โฉ ContFn), ๐, ( โ ร {0})) โ
((normfnโ๐) ยท
(normโโ๐ด)) = ((normfnโif(๐ โ (LinFn โฉ ContFn),
๐, ( โ ร {0})))
ยท (normโโ๐ด))) |
6 | 3, 5 | breq12d 5122 |
. . . . . 6
โข (๐ = if(๐ โ (LinFn โฉ ContFn), ๐, ( โ ร {0})) โ
((absโ(๐โ๐ด)) โค
((normfnโ๐) ยท
(normโโ๐ด)) โ (absโ(if(๐ โ (LinFn โฉ ContFn), ๐, ( โ ร
{0}))โ๐ด)) โค
((normfnโif(๐ โ (LinFn โฉ ContFn), ๐, ( โ ร {0})))
ยท (normโโ๐ด)))) |
7 | 6 | imbi2d 341 |
. . . . 5
โข (๐ = if(๐ โ (LinFn โฉ ContFn), ๐, ( โ ร {0})) โ
((๐ด โ โ โ
(absโ(๐โ๐ด)) โค
((normfnโ๐) ยท
(normโโ๐ด))) โ (๐ด โ โ โ (absโ(if(๐ โ (LinFn โฉ ContFn),
๐, ( โ ร
{0}))โ๐ด)) โค
((normfnโif(๐ โ (LinFn โฉ ContFn), ๐, ( โ ร {0})))
ยท (normโโ๐ด))))) |
8 | | 0lnfn 30976 |
. . . . . . . . . 10
โข ( โ
ร {0}) โ LinFn |
9 | | 0cnfn 30971 |
. . . . . . . . . 10
โข ( โ
ร {0}) โ ContFn |
10 | | elin 3930 |
. . . . . . . . . 10
โข ((
โ ร {0}) โ (LinFn โฉ ContFn) โ (( โ ร {0})
โ LinFn โง ( โ ร {0}) โ ContFn)) |
11 | 8, 9, 10 | mpbir2an 710 |
. . . . . . . . 9
โข ( โ
ร {0}) โ (LinFn โฉ ContFn) |
12 | 11 | elimel 4559 |
. . . . . . . 8
โข if(๐ โ (LinFn โฉ ContFn),
๐, ( โ ร {0}))
โ (LinFn โฉ ContFn) |
13 | | elin 3930 |
. . . . . . . 8
โข (if(๐ โ (LinFn โฉ ContFn),
๐, ( โ ร {0}))
โ (LinFn โฉ ContFn) โ (if(๐ โ (LinFn โฉ ContFn), ๐, ( โ ร {0})) โ
LinFn โง if(๐ โ
(LinFn โฉ ContFn), ๐, (
โ ร {0})) โ ContFn)) |
14 | 12, 13 | mpbi 229 |
. . . . . . 7
โข (if(๐ โ (LinFn โฉ ContFn),
๐, ( โ ร {0}))
โ LinFn โง if(๐
โ (LinFn โฉ ContFn), ๐, ( โ ร {0})) โ
ContFn) |
15 | 14 | simpli 485 |
. . . . . 6
โข if(๐ โ (LinFn โฉ ContFn),
๐, ( โ ร {0}))
โ LinFn |
16 | 14 | simpri 487 |
. . . . . 6
โข if(๐ โ (LinFn โฉ ContFn),
๐, ( โ ร {0}))
โ ContFn |
17 | 15, 16 | nmcfnlbi 31043 |
. . . . 5
โข (๐ด โ โ โ
(absโ(if(๐ โ
(LinFn โฉ ContFn), ๐, (
โ ร {0}))โ๐ด)) โค ((normfnโif(๐ โ (LinFn โฉ ContFn),
๐, ( โ ร {0})))
ยท (normโโ๐ด))) |
18 | 7, 17 | dedth 4548 |
. . . 4
โข (๐ โ (LinFn โฉ ContFn)
โ (๐ด โ โ
โ (absโ(๐โ๐ด)) โค ((normfnโ๐) ยท
(normโโ๐ด)))) |
19 | 18 | imp 408 |
. . 3
โข ((๐ โ (LinFn โฉ ContFn)
โง ๐ด โ โ)
โ (absโ(๐โ๐ด)) โค ((normfnโ๐) ยท
(normโโ๐ด))) |
20 | 1, 19 | sylanbr 583 |
. 2
โข (((๐ โ LinFn โง ๐ โ ContFn) โง ๐ด โ โ) โ
(absโ(๐โ๐ด)) โค
((normfnโ๐) ยท
(normโโ๐ด))) |
21 | 20 | 3impa 1111 |
1
โข ((๐ โ LinFn โง ๐ โ ContFn โง ๐ด โ โ) โ
(absโ(๐โ๐ด)) โค
((normfnโ๐) ยท
(normโโ๐ด))) |