Step | Hyp | Ref
| Expression |
1 | | reex 11200 |
. . . . . . . . . 10
β’ β
β V |
2 | 1 | a1i 11 |
. . . . . . . . 9
β’ (((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β)) β§ β β dom β«1)
β β β V) |
3 | | i1ff 25192 |
. . . . . . . . . . 11
β’ (β β dom β«1
β β:ββΆβ) |
4 | 3 | adantl 482 |
. . . . . . . . . 10
β’ (((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β)) β§ β β dom β«1)
β β:ββΆβ) |
5 | | ressxr 11257 |
. . . . . . . . . 10
β’ β
β β* |
6 | | fss 6734 |
. . . . . . . . . 10
β’ ((β:ββΆβ β§
β β β*) β β:ββΆβ*) |
7 | 4, 5, 6 | sylancl 586 |
. . . . . . . . 9
β’ (((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β)) β§ β β dom β«1)
β β:ββΆβ*) |
8 | | simpll 765 |
. . . . . . . . . 10
β’ (((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β)) β§ β β dom β«1)
β πΉ:ββΆ(0[,]+β)) |
9 | | iccssxr 13406 |
. . . . . . . . . 10
β’
(0[,]+β) β β* |
10 | | fss 6734 |
. . . . . . . . . 10
β’ ((πΉ:ββΆ(0[,]+β)
β§ (0[,]+β) β β*) β πΉ:ββΆβ*) |
11 | 8, 9, 10 | sylancl 586 |
. . . . . . . . 9
β’ (((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β)) β§ β β dom β«1)
β πΉ:ββΆβ*) |
12 | | simplr 767 |
. . . . . . . . . 10
β’ (((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β)) β§ β β dom β«1)
β πΊ:ββΆ(0[,]+β)) |
13 | | fss 6734 |
. . . . . . . . . 10
β’ ((πΊ:ββΆ(0[,]+β)
β§ (0[,]+β) β β*) β πΊ:ββΆβ*) |
14 | 12, 9, 13 | sylancl 586 |
. . . . . . . . 9
β’ (((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β)) β§ β β dom β«1)
β πΊ:ββΆβ*) |
15 | | xrletr 13136 |
. . . . . . . . . 10
β’ ((π₯ β β*
β§ π¦ β
β* β§ π§
β β*) β ((π₯ β€ π¦ β§ π¦ β€ π§) β π₯ β€ π§)) |
16 | 15 | adantl 482 |
. . . . . . . . 9
β’ ((((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β)) β§ β β dom β«1)
β§ (π₯ β
β* β§ π¦
β β* β§ π§ β β*)) β ((π₯ β€ π¦ β§ π¦ β€ π§) β π₯ β€ π§)) |
17 | 2, 7, 11, 14, 16 | caoftrn 7707 |
. . . . . . . 8
β’ (((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β)) β§ β β dom β«1)
β ((β
βr β€ πΉ
β§ πΉ βr
β€ πΊ) β β βr β€ πΊ)) |
18 | | simplr 767 |
. . . . . . . . . 10
β’ (((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β)) β§ (β β dom β«1
β§ β βr
β€ πΊ)) β πΊ:ββΆ(0[,]+β)) |
19 | | simprl 769 |
. . . . . . . . . 10
β’ (((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β)) β§ (β β dom β«1
β§ β βr
β€ πΊ)) β β β dom
β«1) |
20 | | simprr 771 |
. . . . . . . . . 10
β’ (((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β)) β§ (β β dom β«1
β§ β βr
β€ πΊ)) β β βr β€ πΊ) |
21 | | itg2ub 25250 |
. . . . . . . . . 10
β’ ((πΊ:ββΆ(0[,]+β)
β§ β β dom
β«1 β§ β
βr β€ πΊ)
β (β«1ββ) β€ (β«2βπΊ)) |
22 | 18, 19, 20, 21 | syl3anc 1371 |
. . . . . . . . 9
β’ (((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β)) β§ (β β dom β«1
β§ β βr
β€ πΊ)) β
(β«1ββ)
β€ (β«2βπΊ)) |
23 | 22 | expr 457 |
. . . . . . . 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 466 |
. . . . . 6
β’ (((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β)) β§ β β dom β«1)
β ((πΉ
βr β€ πΊ
β§ β βr
β€ πΉ) β
(β«1ββ)
β€ (β«2βπΊ))) |
26 | 25 | exp4b 431 |
. . . . 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 1117 |
. . 3
β’ ((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β) β§ πΉ βr β€ πΊ) β (β β dom β«1 β (β βr β€ πΉ β
(β«1ββ)
β€ (β«2βπΊ)))) |
29 | 28 | ralrimiv 3145 |
. 2
β’ ((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β) β§ πΉ βr β€ πΊ) β ββ β dom
β«1(β
βr β€ πΉ
β (β«1ββ) β€ (β«2βπΊ))) |
30 | | simp1 1136 |
. . 3
β’ ((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β) β§ πΉ βr β€ πΊ) β πΉ:ββΆ(0[,]+β)) |
31 | | itg2cl 25249 |
. . . 4
β’ (πΊ:ββΆ(0[,]+β)
β (β«2βπΊ) β
β*) |
32 | 31 | 3ad2ant2 1134 |
. . 3
β’ ((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β) β§ πΉ βr β€ πΊ) β
(β«2βπΊ)
β β*) |
33 | | itg2leub 25251 |
. . 3
β’ ((πΉ:ββΆ(0[,]+β)
β§ (β«2βπΊ) β β*) β
((β«2βπΉ) β€ (β«2βπΊ) β ββ β dom
β«1(β
βr β€ πΉ
β (β«1ββ) β€ (β«2βπΊ)))) |
34 | 30, 32, 33 | syl2anc 584 |
. 2
β’ ((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β) β§ πΉ βr β€ πΊ) β
((β«2βπΉ) β€ (β«2βπΊ) β ββ β dom
β«1(β
βr β€ πΉ
β (β«1ββ) β€ (β«2βπΊ)))) |
35 | 29, 34 | mpbird 256 |
1
β’ ((πΉ:ββΆ(0[,]+β)
β§ πΊ:ββΆ(0[,]+β) β§ πΉ βr β€ πΊ) β
(β«2βπΉ)
β€ (β«2βπΊ)) |