Step | Hyp | Ref
| Expression |
1 | | reex 11201 |
. . . . . . . . . 10
β’ β
β V |
2 | 1 | a1i 11 |
. . . . . . . . 9
β’ (((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β)) β§ β β dom β«1)
β β β V) |
3 | | i1ff 25193 |
. . . . . . . . . . 11
β’ (β β dom β«1
β β:ββΆβ) |
4 | 3 | adantl 483 |
. . . . . . . . . 10
β’ (((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β)) β§ β β dom β«1)
β β:ββΆβ) |
5 | | ressxr 11258 |
. . . . . . . . . 10
β’ β
β β* |
6 | | fss 6735 |
. . . . . . . . . 10
β’ ((β:ββΆβ β§
β β β*) β β:ββΆβ*) |
7 | 4, 5, 6 | sylancl 587 |
. . . . . . . . 9
β’ (((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β)) β§ β β dom β«1)
β β:ββΆβ*) |
8 | | simpll 766 |
. . . . . . . . . 10
β’ (((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β)) β§ β β dom β«1)
β πΉ:ββΆ(0[,]+β)) |
9 | | iccssxr 13407 |
. . . . . . . . . 10
β’
(0[,]+β) β β* |
10 | | fss 6735 |
. . . . . . . . . 10
β’ ((πΉ:ββΆ(0[,]+β)
β§ (0[,]+β) β β*) β πΉ:ββΆβ*) |
11 | 8, 9, 10 | sylancl 587 |
. . . . . . . . 9
β’ (((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β)) β§ β β dom β«1)
β πΉ:ββΆβ*) |
12 | | simplr 768 |
. . . . . . . . . 10
β’ (((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β)) β§ β β dom β«1)
β πΊ:ββΆ(0[,]+β)) |
13 | | fss 6735 |
. . . . . . . . . 10
β’ ((πΊ:ββΆ(0[,]+β)
β§ (0[,]+β) β β*) β πΊ:ββΆβ*) |
14 | 12, 9, 13 | sylancl 587 |
. . . . . . . . 9
β’ (((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β)) β§ β β dom β«1)
β πΊ:ββΆβ*) |
15 | | xrletr 13137 |
. . . . . . . . . 10
β’ ((π₯ β β*
β§ π¦ β
β* β§ π§
β β*) β ((π₯ β€ π¦ β§ π¦ β€ π§) β π₯ β€ π§)) |
16 | 15 | adantl 483 |
. . . . . . . . 9
β’ ((((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β)) β§ β β dom β«1)
β§ (π₯ β
β* β§ π¦
β β* β§ π§ β β*)) β ((π₯ β€ π¦ β§ π¦ β€ π§) β π₯ β€ π§)) |
17 | 2, 7, 11, 14, 16 | caoftrn 7708 |
. . . . . . . 8
β’ (((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β)) β§ β β dom β«1)
β ((β
βr β€ πΉ
β§ πΉ βr
β€ πΊ) β β βr β€ πΊ)) |
18 | | simplr 768 |
. . . . . . . . . 10
β’ (((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β)) β§ (β β dom β«1
β§ β βr
β€ πΊ)) β πΊ:ββΆ(0[,]+β)) |
19 | | simprl 770 |
. . . . . . . . . 10
β’ (((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β)) β§ (β β dom β«1
β§ β βr
β€ πΊ)) β β β dom
β«1) |
20 | | simprr 772 |
. . . . . . . . . 10
β’ (((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β)) β§ (β β dom β«1
β§ β βr
β€ πΊ)) β β βr β€ πΊ) |
21 | | itg2ub 25251 |
. . . . . . . . . 10
β’ ((πΊ:ββΆ(0[,]+β)
β§ β β dom
β«1 β§ β
βr β€ πΊ)
β (β«1ββ) β€ (β«2βπΊ)) |
22 | 18, 19, 20, 21 | syl3anc 1372 |
. . . . . . . . 9
β’ (((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β)) β§ (β β dom β«1
β§ β βr
β€ πΊ)) β
(β«1ββ)
β€ (β«2βπΊ)) |
23 | 22 | expr 458 |
. . . . . . . 8
β’ (((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β)) β§ β β dom β«1)
β (β
βr β€ πΊ
β (β«1ββ) β€ (β«2βπΊ))) |
24 | 17, 23 | syld 47 |
. . . . . . 7
β’ (((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β)) β§ β β dom β«1)
β ((β
βr β€ πΉ
β§ πΉ βr
β€ πΊ) β
(β«1ββ)
β€ (β«2βπΊ))) |
25 | 24 | ancomsd 467 |
. . . . . 6
β’ (((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β)) β§ β β dom β«1)
β ((πΉ
βr β€ πΊ
β§ β βr
β€ πΉ) β
(β«1ββ)
β€ (β«2βπΊ))) |
26 | 25 | exp4b 432 |
. . . . 5
β’ ((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β)) β
(β β dom
β«1 β (πΉ
βr β€ πΊ
β (β
βr β€ πΉ
β (β«1ββ) β€ (β«2βπΊ))))) |
27 | 26 | com23 86 |
. . . 4
β’ ((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β)) β
(πΉ βr β€
πΊ β (β β dom β«1
β (β
βr β€ πΉ
β (β«1ββ) β€ (β«2βπΊ))))) |
28 | 27 | 3impia 1118 |
. . 3
β’ ((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β) β§ πΉ βr β€ πΊ) β (β β dom β«1 β (β βr β€ πΉ β
(β«1ββ)
β€ (β«2βπΊ)))) |
29 | 28 | ralrimiv 3146 |
. 2
β’ ((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β) β§ πΉ βr β€ πΊ) β ββ β dom
β«1(β
βr β€ πΉ
β (β«1ββ) β€ (β«2βπΊ))) |
30 | | simp1 1137 |
. . 3
β’ ((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β) β§ πΉ βr β€ πΊ) β πΉ:ββΆ(0[,]+β)) |
31 | | itg2cl 25250 |
. . . 4
β’ (πΊ:ββΆ(0[,]+β)
β (β«2βπΊ) β
β*) |
32 | 31 | 3ad2ant2 1135 |
. . 3
β’ ((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β) β§ πΉ βr β€ πΊ) β
(β«2βπΊ)
β β*) |
33 | | itg2leub 25252 |
. . 3
β’ ((πΉ:ββΆ(0[,]+β)
β§ (β«2βπΊ) β β*) β
((β«2βπΉ) β€ (β«2βπΊ) β ββ β dom
β«1(β
βr β€ πΉ
β (β«1ββ) β€ (β«2βπΊ)))) |
34 | 30, 32, 33 | syl2anc 585 |
. 2
β’ ((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β) β§ πΉ βr β€ πΊ) β
((β«2βπΉ) β€ (β«2βπΊ) β ββ β dom
β«1(β
βr β€ πΉ
β (β«1ββ) β€ (β«2βπΊ)))) |
35 | 29, 34 | mpbird 257 |
1
β’ ((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β) β§ πΉ βr β€ πΊ) β
(β«2βπΉ)
β€ (β«2βπΊ)) |