Step | Hyp | Ref
| Expression |
1 | | absf 15287 |
. . . . . 6
β’
abs:ββΆβ |
2 | | subf 11463 |
. . . . . 6
β’ β
:(β Γ β)βΆβ |
3 | | fco 6734 |
. . . . . 6
β’
((abs:ββΆβ β§ β :(β Γ
β)βΆβ) β (abs β β ):(β Γ
β)βΆβ) |
4 | 1, 2, 3 | mp2an 689 |
. . . . 5
β’ (abs
β β ):(β Γ β)βΆβ |
5 | | inss2 4224 |
. . . . . . 7
β’ ( β€
β© (β Γ β)) β (β Γ
β) |
6 | | ax-resscn 11166 |
. . . . . . . 8
β’ β
β β |
7 | | xpss12 5684 |
. . . . . . . 8
β’ ((β
β β β§ β β β) β (β Γ β)
β (β Γ β)) |
8 | 6, 6, 7 | mp2an 689 |
. . . . . . 7
β’ (β
Γ β) β (β Γ β) |
9 | 5, 8 | sstri 3986 |
. . . . . 6
β’ ( β€
β© (β Γ β)) β (β Γ
β) |
10 | | fss 6727 |
. . . . . 6
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ ( β€ β© (β Γ β))
β (β Γ β)) β πΉ:ββΆ(β Γ
β)) |
11 | 9, 10 | mpan2 688 |
. . . . 5
β’ (πΉ:ββΆ( β€ β©
(β Γ β)) β πΉ:ββΆ(β Γ
β)) |
12 | | fco 6734 |
. . . . 5
β’ (((abs
β β ):(β Γ β)βΆβ β§ πΉ:ββΆ(β Γ
β)) β ((abs β β ) β πΉ):ββΆβ) |
13 | 4, 11, 12 | sylancr 586 |
. . . 4
β’ (πΉ:ββΆ( β€ β©
(β Γ β)) β ((abs β β ) β πΉ):ββΆβ) |
14 | | ovolfs.1 |
. . . . 5
β’ πΊ = ((abs β β )
β πΉ) |
15 | 14 | feq1i 6701 |
. . . 4
β’ (πΊ:ββΆβ β
((abs β β ) β πΉ):ββΆβ) |
16 | 13, 15 | sylibr 233 |
. . 3
β’ (πΉ:ββΆ( β€ β©
(β Γ β)) β πΊ:ββΆβ) |
17 | 16 | ffnd 6711 |
. 2
β’ (πΉ:ββΆ( β€ β©
(β Γ β)) β πΊ Fn β) |
18 | 16 | ffvelcdmda 7079 |
. . . 4
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π₯ β β) β (πΊβπ₯) β β) |
19 | | ovolfcl 25345 |
. . . . . 6
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π₯ β β) β ((1st
β(πΉβπ₯)) β β β§
(2nd β(πΉβπ₯)) β β β§ (1st
β(πΉβπ₯)) β€ (2nd
β(πΉβπ₯)))) |
20 | | subge0 11728 |
. . . . . . . 8
β’
(((2nd β(πΉβπ₯)) β β β§ (1st
β(πΉβπ₯)) β β) β (0
β€ ((2nd β(πΉβπ₯)) β (1st β(πΉβπ₯))) β (1st β(πΉβπ₯)) β€ (2nd β(πΉβπ₯)))) |
21 | 20 | ancoms 458 |
. . . . . . 7
β’
(((1st β(πΉβπ₯)) β β β§ (2nd
β(πΉβπ₯)) β β) β (0
β€ ((2nd β(πΉβπ₯)) β (1st β(πΉβπ₯))) β (1st β(πΉβπ₯)) β€ (2nd β(πΉβπ₯)))) |
22 | 21 | biimp3ar 1466 |
. . . . . 6
β’
(((1st β(πΉβπ₯)) β β β§ (2nd
β(πΉβπ₯)) β β β§
(1st β(πΉβπ₯)) β€ (2nd β(πΉβπ₯))) β 0 β€ ((2nd
β(πΉβπ₯)) β (1st
β(πΉβπ₯)))) |
23 | 19, 22 | syl 17 |
. . . . 5
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π₯ β β) β 0 β€
((2nd β(πΉβπ₯)) β (1st β(πΉβπ₯)))) |
24 | 14 | ovolfsval 25349 |
. . . . 5
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π₯ β β) β (πΊβπ₯) = ((2nd β(πΉβπ₯)) β (1st β(πΉβπ₯)))) |
25 | 23, 24 | breqtrrd 5169 |
. . . 4
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π₯ β β) β 0 β€ (πΊβπ₯)) |
26 | | elrege0 13434 |
. . . 4
β’ ((πΊβπ₯) β (0[,)+β) β ((πΊβπ₯) β β β§ 0 β€ (πΊβπ₯))) |
27 | 18, 25, 26 | sylanbrc 582 |
. . 3
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π₯ β β) β (πΊβπ₯) β (0[,)+β)) |
28 | 27 | ralrimiva 3140 |
. 2
β’ (πΉ:ββΆ( β€ β©
(β Γ β)) β βπ₯ β β (πΊβπ₯) β (0[,)+β)) |
29 | | ffnfv 7113 |
. 2
β’ (πΊ:ββΆ(0[,)+β)
β (πΊ Fn β β§
βπ₯ β β
(πΊβπ₯) β (0[,)+β))) |
30 | 17, 28, 29 | sylanbrc 582 |
1
β’ (πΉ:ββΆ( β€ β©
(β Γ β)) β πΊ:ββΆ(0[,)+β)) |