Step | Hyp | Ref
| Expression |
1 | | cncfioobd.a |
. . 3
β’ (π β π΄ β β) |
2 | | cncfioobd.b |
. . 3
β’ (π β π΅ β β) |
3 | | nfv 1918 |
. . . 4
β’
β²π§π |
4 | | eqid 2733 |
. . . 4
β’ (π§ β (π΄[,]π΅) β¦ if(π§ = π΄, π
, if(π§ = π΅, πΏ, (πΉβπ§)))) = (π§ β (π΄[,]π΅) β¦ if(π§ = π΄, π
, if(π§ = π΅, πΏ, (πΉβπ§)))) |
5 | | cncfioobd.f |
. . . 4
β’ (π β πΉ β ((π΄(,)π΅)βcnββ)) |
6 | | cncfioobd.l |
. . . 4
β’ (π β πΏ β (πΉ limβ π΅)) |
7 | | cncfioobd.r |
. . . 4
β’ (π β π
β (πΉ limβ π΄)) |
8 | 3, 4, 1, 2, 5, 6, 7 | cncfiooicc 44225 |
. . 3
β’ (π β (π§ β (π΄[,]π΅) β¦ if(π§ = π΄, π
, if(π§ = π΅, πΏ, (πΉβπ§)))) β ((π΄[,]π΅)βcnββ)) |
9 | | cniccbdd 24848 |
. . 3
β’ ((π΄ β β β§ π΅ β β β§ (π§ β (π΄[,]π΅) β¦ if(π§ = π΄, π
, if(π§ = π΅, πΏ, (πΉβπ§)))) β ((π΄[,]π΅)βcnββ)) β βπ₯ β β βπ¦ β (π΄[,]π΅)(absβ((π§ β (π΄[,]π΅) β¦ if(π§ = π΄, π
, if(π§ = π΅, πΏ, (πΉβπ§))))βπ¦)) β€ π₯) |
10 | 1, 2, 8, 9 | syl3anc 1372 |
. 2
β’ (π β βπ₯ β β βπ¦ β (π΄[,]π΅)(absβ((π§ β (π΄[,]π΅) β¦ if(π§ = π΄, π
, if(π§ = π΅, πΏ, (πΉβπ§))))βπ¦)) β€ π₯) |
11 | | nfv 1918 |
. . . . . 6
β’
β²π¦(π β§ π₯ β β) |
12 | | nfra1 3266 |
. . . . . 6
β’
β²π¦βπ¦ β (π΄[,]π΅)(absβ((π§ β (π΄[,]π΅) β¦ if(π§ = π΄, π
, if(π§ = π΅, πΏ, (πΉβπ§))))βπ¦)) β€ π₯ |
13 | 11, 12 | nfan 1903 |
. . . . 5
β’
β²π¦((π β§ π₯ β β) β§ βπ¦ β (π΄[,]π΅)(absβ((π§ β (π΄[,]π΅) β¦ if(π§ = π΄, π
, if(π§ = π΅, πΏ, (πΉβπ§))))βπ¦)) β€ π₯) |
14 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (π΄(,)π΅)) β π¦ β (π΄(,)π΅)) |
15 | | cncff 24279 |
. . . . . . . . . . . . . . . 16
β’ (πΉ β ((π΄(,)π΅)βcnββ) β πΉ:(π΄(,)π΅)βΆβ) |
16 | 5, 15 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β πΉ:(π΄(,)π΅)βΆβ) |
17 | 16 | fdmd 6683 |
. . . . . . . . . . . . . 14
β’ (π β dom πΉ = (π΄(,)π΅)) |
18 | 17 | eqcomd 2739 |
. . . . . . . . . . . . 13
β’ (π β (π΄(,)π΅) = dom πΉ) |
19 | 18 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (π΄(,)π΅)) β (π΄(,)π΅) = dom πΉ) |
20 | 14, 19 | eleqtrd 2836 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β (π΄(,)π΅)) β π¦ β dom πΉ) |
21 | 1 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β dom πΉ) β π΄ β β) |
22 | 2 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β dom πΉ) β π΅ β β) |
23 | 16 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β dom πΉ) β πΉ:(π΄(,)π΅)βΆβ) |
24 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β dom πΉ) β π¦ β dom πΉ) |
25 | 17 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β dom πΉ) β dom πΉ = (π΄(,)π΅)) |
26 | 24, 25 | eleqtrd 2836 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β dom πΉ) β π¦ β (π΄(,)π΅)) |
27 | 21, 22, 23, 4, 26 | cncfioobdlem 44227 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β dom πΉ) β ((π§ β (π΄[,]π΅) β¦ if(π§ = π΄, π
, if(π§ = π΅, πΏ, (πΉβπ§))))βπ¦) = (πΉβπ¦)) |
28 | 20, 27 | syldan 592 |
. . . . . . . . . 10
β’ ((π β§ π¦ β (π΄(,)π΅)) β ((π§ β (π΄[,]π΅) β¦ if(π§ = π΄, π
, if(π§ = π΅, πΏ, (πΉβπ§))))βπ¦) = (πΉβπ¦)) |
29 | 28 | eqcomd 2739 |
. . . . . . . . 9
β’ ((π β§ π¦ β (π΄(,)π΅)) β (πΉβπ¦) = ((π§ β (π΄[,]π΅) β¦ if(π§ = π΄, π
, if(π§ = π΅, πΏ, (πΉβπ§))))βπ¦)) |
30 | 29 | fveq2d 6850 |
. . . . . . . 8
β’ ((π β§ π¦ β (π΄(,)π΅)) β (absβ(πΉβπ¦)) = (absβ((π§ β (π΄[,]π΅) β¦ if(π§ = π΄, π
, if(π§ = π΅, πΏ, (πΉβπ§))))βπ¦))) |
31 | 30 | ad4ant14 751 |
. . . . . . 7
β’ ((((π β§ π₯ β β) β§ βπ¦ β (π΄[,]π΅)(absβ((π§ β (π΄[,]π΅) β¦ if(π§ = π΄, π
, if(π§ = π΅, πΏ, (πΉβπ§))))βπ¦)) β€ π₯) β§ π¦ β (π΄(,)π΅)) β (absβ(πΉβπ¦)) = (absβ((π§ β (π΄[,]π΅) β¦ if(π§ = π΄, π
, if(π§ = π΅, πΏ, (πΉβπ§))))βπ¦))) |
32 | | simplr 768 |
. . . . . . . 8
β’ ((((π β§ π₯ β β) β§ βπ¦ β (π΄[,]π΅)(absβ((π§ β (π΄[,]π΅) β¦ if(π§ = π΄, π
, if(π§ = π΅, πΏ, (πΉβπ§))))βπ¦)) β€ π₯) β§ π¦ β (π΄(,)π΅)) β βπ¦ β (π΄[,]π΅)(absβ((π§ β (π΄[,]π΅) β¦ if(π§ = π΄, π
, if(π§ = π΅, πΏ, (πΉβπ§))))βπ¦)) β€ π₯) |
33 | | ioossicc 13359 |
. . . . . . . . 9
β’ (π΄(,)π΅) β (π΄[,]π΅) |
34 | | simpr 486 |
. . . . . . . . 9
β’ ((((π β§ π₯ β β) β§ βπ¦ β (π΄[,]π΅)(absβ((π§ β (π΄[,]π΅) β¦ if(π§ = π΄, π
, if(π§ = π΅, πΏ, (πΉβπ§))))βπ¦)) β€ π₯) β§ π¦ β (π΄(,)π΅)) β π¦ β (π΄(,)π΅)) |
35 | 33, 34 | sselid 3946 |
. . . . . . . 8
β’ ((((π β§ π₯ β β) β§ βπ¦ β (π΄[,]π΅)(absβ((π§ β (π΄[,]π΅) β¦ if(π§ = π΄, π
, if(π§ = π΅, πΏ, (πΉβπ§))))βπ¦)) β€ π₯) β§ π¦ β (π΄(,)π΅)) β π¦ β (π΄[,]π΅)) |
36 | | rspa 3230 |
. . . . . . . 8
β’
((βπ¦ β
(π΄[,]π΅)(absβ((π§ β (π΄[,]π΅) β¦ if(π§ = π΄, π
, if(π§ = π΅, πΏ, (πΉβπ§))))βπ¦)) β€ π₯ β§ π¦ β (π΄[,]π΅)) β (absβ((π§ β (π΄[,]π΅) β¦ if(π§ = π΄, π
, if(π§ = π΅, πΏ, (πΉβπ§))))βπ¦)) β€ π₯) |
37 | 32, 35, 36 | syl2anc 585 |
. . . . . . 7
β’ ((((π β§ π₯ β β) β§ βπ¦ β (π΄[,]π΅)(absβ((π§ β (π΄[,]π΅) β¦ if(π§ = π΄, π
, if(π§ = π΅, πΏ, (πΉβπ§))))βπ¦)) β€ π₯) β§ π¦ β (π΄(,)π΅)) β (absβ((π§ β (π΄[,]π΅) β¦ if(π§ = π΄, π
, if(π§ = π΅, πΏ, (πΉβπ§))))βπ¦)) β€ π₯) |
38 | 31, 37 | eqbrtrd 5131 |
. . . . . 6
β’ ((((π β§ π₯ β β) β§ βπ¦ β (π΄[,]π΅)(absβ((π§ β (π΄[,]π΅) β¦ if(π§ = π΄, π
, if(π§ = π΅, πΏ, (πΉβπ§))))βπ¦)) β€ π₯) β§ π¦ β (π΄(,)π΅)) β (absβ(πΉβπ¦)) β€ π₯) |
39 | 38 | ex 414 |
. . . . 5
β’ (((π β§ π₯ β β) β§ βπ¦ β (π΄[,]π΅)(absβ((π§ β (π΄[,]π΅) β¦ if(π§ = π΄, π
, if(π§ = π΅, πΏ, (πΉβπ§))))βπ¦)) β€ π₯) β (π¦ β (π΄(,)π΅) β (absβ(πΉβπ¦)) β€ π₯)) |
40 | 13, 39 | ralrimi 3239 |
. . . 4
β’ (((π β§ π₯ β β) β§ βπ¦ β (π΄[,]π΅)(absβ((π§ β (π΄[,]π΅) β¦ if(π§ = π΄, π
, if(π§ = π΅, πΏ, (πΉβπ§))))βπ¦)) β€ π₯) β βπ¦ β (π΄(,)π΅)(absβ(πΉβπ¦)) β€ π₯) |
41 | 40 | ex 414 |
. . 3
β’ ((π β§ π₯ β β) β (βπ¦ β (π΄[,]π΅)(absβ((π§ β (π΄[,]π΅) β¦ if(π§ = π΄, π
, if(π§ = π΅, πΏ, (πΉβπ§))))βπ¦)) β€ π₯ β βπ¦ β (π΄(,)π΅)(absβ(πΉβπ¦)) β€ π₯)) |
42 | 41 | reximdva 3162 |
. 2
β’ (π β (βπ₯ β β βπ¦ β (π΄[,]π΅)(absβ((π§ β (π΄[,]π΅) β¦ if(π§ = π΄, π
, if(π§ = π΅, πΏ, (πΉβπ§))))βπ¦)) β€ π₯ β βπ₯ β β βπ¦ β (π΄(,)π΅)(absβ(πΉβπ¦)) β€ π₯)) |
43 | 10, 42 | mpd 15 |
1
β’ (π β βπ₯ β β βπ¦ β (π΄(,)π΅)(absβ(πΉβπ¦)) β€ π₯) |