Step | Hyp | Ref
| Expression |
1 | | simp2 998 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โ ๐ต โ โ) |
2 | | simp1 997 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โ ๐ด โ โ) |
3 | 1, 2 | resubcld 8337 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โ (๐ต โ ๐ด) โ โ) |
4 | | simp3 999 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โ ๐ด < ๐ต) |
5 | 2, 1 | posdifd 8488 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โ (๐ด < ๐ต โ 0 < (๐ต โ ๐ด))) |
6 | 4, 5 | mpbid 147 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โ 0 < (๐ต โ ๐ด)) |
7 | | nnrecl 9173 |
. . 3
โข (((๐ต โ ๐ด) โ โ โง 0 < (๐ต โ ๐ด)) โ โ๐ โ โ (1 / ๐) < (๐ต โ ๐ด)) |
8 | 3, 6, 7 | syl2anc 411 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โ โ๐ โ โ (1 / ๐) < (๐ต โ ๐ด)) |
9 | 2 | adantr 276 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง (๐ โ โ โง (1 / ๐) < (๐ต โ ๐ด))) โ ๐ด โ โ) |
10 | | 2re 8988 |
. . . . . . 7
โข 2 โ
โ |
11 | 10 | a1i 9 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง (๐ โ โ โง (1 / ๐) < (๐ต โ ๐ด))) โ 2 โ
โ) |
12 | | simprl 529 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง (๐ โ โ โง (1 / ๐) < (๐ต โ ๐ด))) โ ๐ โ โ) |
13 | 12 | nnred 8931 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง (๐ โ โ โง (1 / ๐) < (๐ต โ ๐ด))) โ ๐ โ โ) |
14 | 11, 13 | remulcld 7987 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง (๐ โ โ โง (1 / ๐) < (๐ต โ ๐ด))) โ (2 ยท ๐) โ โ) |
15 | 9, 14 | remulcld 7987 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง (๐ โ โ โง (1 / ๐) < (๐ต โ ๐ด))) โ (๐ด ยท (2 ยท ๐)) โ โ) |
16 | | rebtwn2z 10254 |
. . . 4
โข ((๐ด ยท (2 ยท ๐)) โ โ โ
โ๐ โ โค
(๐ < (๐ด ยท (2 ยท ๐)) โง (๐ด ยท (2 ยท ๐)) < (๐ + 2))) |
17 | 15, 16 | syl 14 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง (๐ โ โ โง (1 / ๐) < (๐ต โ ๐ด))) โ โ๐ โ โค (๐ < (๐ด ยท (2 ยท ๐)) โง (๐ด ยท (2 ยท ๐)) < (๐ + 2))) |
18 | | simprl 529 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง (๐ โ โ โง (1 / ๐) < (๐ต โ ๐ด))) โง (๐ โ โค โง (๐ < (๐ด ยท (2 ยท ๐)) โง (๐ด ยท (2 ยท ๐)) < (๐ + 2)))) โ ๐ โ โค) |
19 | | 2z 9280 |
. . . . . . 7
โข 2 โ
โค |
20 | 19 | a1i 9 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง (๐ โ โ โง (1 / ๐) < (๐ต โ ๐ด))) โง (๐ โ โค โง (๐ < (๐ด ยท (2 ยท ๐)) โง (๐ด ยท (2 ยท ๐)) < (๐ + 2)))) โ 2 โ
โค) |
21 | 18, 20 | zaddcld 9378 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง (๐ โ โ โง (1 / ๐) < (๐ต โ ๐ด))) โง (๐ โ โค โง (๐ < (๐ด ยท (2 ยท ๐)) โง (๐ด ยท (2 ยท ๐)) < (๐ + 2)))) โ (๐ + 2) โ โค) |
22 | | 2nn 9079 |
. . . . . . 7
โข 2 โ
โ |
23 | 22 | a1i 9 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง (๐ โ โ โง (1 / ๐) < (๐ต โ ๐ด))) โง (๐ โ โค โง (๐ < (๐ด ยท (2 ยท ๐)) โง (๐ด ยท (2 ยท ๐)) < (๐ + 2)))) โ 2 โ
โ) |
24 | 12 | adantr 276 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง (๐ โ โ โง (1 / ๐) < (๐ต โ ๐ด))) โง (๐ โ โค โง (๐ < (๐ด ยท (2 ยท ๐)) โง (๐ด ยท (2 ยท ๐)) < (๐ + 2)))) โ ๐ โ โ) |
25 | 23, 24 | nnmulcld 8967 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง (๐ โ โ โง (1 / ๐) < (๐ต โ ๐ด))) โง (๐ โ โค โง (๐ < (๐ด ยท (2 ยท ๐)) โง (๐ด ยท (2 ยท ๐)) < (๐ + 2)))) โ (2 ยท ๐) โ
โ) |
26 | | znq 9623 |
. . . . 5
โข (((๐ + 2) โ โค โง (2
ยท ๐) โ โ)
โ ((๐ + 2) / (2
ยท ๐)) โ
โ) |
27 | 21, 25, 26 | syl2anc 411 |
. . . 4
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง (๐ โ โ โง (1 / ๐) < (๐ต โ ๐ด))) โง (๐ โ โค โง (๐ < (๐ด ยท (2 ยท ๐)) โง (๐ด ยท (2 ยท ๐)) < (๐ + 2)))) โ ((๐ + 2) / (2 ยท ๐)) โ โ) |
28 | | simprrr 540 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง (๐ โ โ โง (1 / ๐) < (๐ต โ ๐ด))) โง (๐ โ โค โง (๐ < (๐ด ยท (2 ยท ๐)) โง (๐ด ยท (2 ยท ๐)) < (๐ + 2)))) โ (๐ด ยท (2 ยท ๐)) < (๐ + 2)) |
29 | 9 | adantr 276 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง (๐ โ โ โง (1 / ๐) < (๐ต โ ๐ด))) โง (๐ โ โค โง (๐ < (๐ด ยท (2 ยท ๐)) โง (๐ด ยท (2 ยท ๐)) < (๐ + 2)))) โ ๐ด โ โ) |
30 | 21 | zred 9374 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง (๐ โ โ โง (1 / ๐) < (๐ต โ ๐ด))) โง (๐ โ โค โง (๐ < (๐ด ยท (2 ยท ๐)) โง (๐ด ยท (2 ยท ๐)) < (๐ + 2)))) โ (๐ + 2) โ โ) |
31 | 25 | nnrpd 9693 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง (๐ โ โ โง (1 / ๐) < (๐ต โ ๐ด))) โง (๐ โ โค โง (๐ < (๐ด ยท (2 ยท ๐)) โง (๐ด ยท (2 ยท ๐)) < (๐ + 2)))) โ (2 ยท ๐) โ
โ+) |
32 | 29, 30, 31 | ltmuldivd 9743 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง (๐ โ โ โง (1 / ๐) < (๐ต โ ๐ด))) โง (๐ โ โค โง (๐ < (๐ด ยท (2 ยท ๐)) โง (๐ด ยท (2 ยท ๐)) < (๐ + 2)))) โ ((๐ด ยท (2 ยท ๐)) < (๐ + 2) โ ๐ด < ((๐ + 2) / (2 ยท ๐)))) |
33 | 28, 32 | mpbid 147 |
. . . 4
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง (๐ โ โ โง (1 / ๐) < (๐ต โ ๐ด))) โง (๐ โ โค โง (๐ < (๐ด ยท (2 ยท ๐)) โง (๐ด ยท (2 ยท ๐)) < (๐ + 2)))) โ ๐ด < ((๐ + 2) / (2 ยท ๐))) |
34 | | simpll2 1037 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง (๐ โ โ โง (1 / ๐) < (๐ต โ ๐ด))) โง (๐ โ โค โง (๐ < (๐ด ยท (2 ยท ๐)) โง (๐ด ยท (2 ยท ๐)) < (๐ + 2)))) โ ๐ต โ โ) |
35 | | simprrl 539 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง (๐ โ โ โง (1 / ๐) < (๐ต โ ๐ด))) โง (๐ โ โค โง (๐ < (๐ด ยท (2 ยท ๐)) โง (๐ด ยท (2 ยท ๐)) < (๐ + 2)))) โ ๐ < (๐ด ยท (2 ยท ๐))) |
36 | | simplrr 536 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง (๐ โ โ โง (1 / ๐) < (๐ต โ ๐ด))) โง (๐ โ โค โง (๐ < (๐ด ยท (2 ยท ๐)) โง (๐ด ยท (2 ยท ๐)) < (๐ + 2)))) โ (1 / ๐) < (๐ต โ ๐ด)) |
37 | 18, 24, 29, 34, 35, 36 | qbtwnrelemcalc 10255 |
. . . 4
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง (๐ โ โ โง (1 / ๐) < (๐ต โ ๐ด))) โง (๐ โ โค โง (๐ < (๐ด ยท (2 ยท ๐)) โง (๐ด ยท (2 ยท ๐)) < (๐ + 2)))) โ ((๐ + 2) / (2 ยท ๐)) < ๐ต) |
38 | | breq2 4007 |
. . . . . 6
โข (๐ฅ = ((๐ + 2) / (2 ยท ๐)) โ (๐ด < ๐ฅ โ ๐ด < ((๐ + 2) / (2 ยท ๐)))) |
39 | | breq1 4006 |
. . . . . 6
โข (๐ฅ = ((๐ + 2) / (2 ยท ๐)) โ (๐ฅ < ๐ต โ ((๐ + 2) / (2 ยท ๐)) < ๐ต)) |
40 | 38, 39 | anbi12d 473 |
. . . . 5
โข (๐ฅ = ((๐ + 2) / (2 ยท ๐)) โ ((๐ด < ๐ฅ โง ๐ฅ < ๐ต) โ (๐ด < ((๐ + 2) / (2 ยท ๐)) โง ((๐ + 2) / (2 ยท ๐)) < ๐ต))) |
41 | 40 | rspcev 2841 |
. . . 4
โข ((((๐ + 2) / (2 ยท ๐)) โ โ โง (๐ด < ((๐ + 2) / (2 ยท ๐)) โง ((๐ + 2) / (2 ยท ๐)) < ๐ต)) โ โ๐ฅ โ โ (๐ด < ๐ฅ โง ๐ฅ < ๐ต)) |
42 | 27, 33, 37, 41 | syl12anc 1236 |
. . 3
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง (๐ โ โ โง (1 / ๐) < (๐ต โ ๐ด))) โง (๐ โ โค โง (๐ < (๐ด ยท (2 ยท ๐)) โง (๐ด ยท (2 ยท ๐)) < (๐ + 2)))) โ โ๐ฅ โ โ (๐ด < ๐ฅ โง ๐ฅ < ๐ต)) |
43 | 17, 42 | rexlimddv 2599 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โง (๐ โ โ โง (1 / ๐) < (๐ต โ ๐ด))) โ โ๐ฅ โ โ (๐ด < ๐ฅ โง ๐ฅ < ๐ต)) |
44 | 8, 43 | rexlimddv 2599 |
1
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ด < ๐ต) โ โ๐ฅ โ โ (๐ด < ๐ฅ โง ๐ฅ < ๐ต)) |