Step | Hyp | Ref
| Expression |
1 | | 2re 8989 |
. . . . 5
โข 2 โ
โ |
2 | 1 | a1i 9 |
. . . 4
โข (๐ โ 2 โ
โ) |
3 | | qbtwnrelemcalc.b |
. . . . . 6
โข (๐ โ ๐ต โ โ) |
4 | | qbtwnrelemcalc.n |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
5 | 4 | nnred 8932 |
. . . . . . 7
โข (๐ โ ๐ โ โ) |
6 | 2, 5 | remulcld 7988 |
. . . . . 6
โข (๐ โ (2 ยท ๐) โ
โ) |
7 | 3, 6 | remulcld 7988 |
. . . . 5
โข (๐ โ (๐ต ยท (2 ยท ๐)) โ โ) |
8 | | qbtwnrelemcalc.a |
. . . . . 6
โข (๐ โ ๐ด โ โ) |
9 | 8, 6 | remulcld 7988 |
. . . . 5
โข (๐ โ (๐ด ยท (2 ยท ๐)) โ โ) |
10 | 7, 9 | resubcld 8338 |
. . . 4
โข (๐ โ ((๐ต ยท (2 ยท ๐)) โ (๐ด ยท (2 ยท ๐))) โ โ) |
11 | | qbtwnrelemcalc.m |
. . . . . 6
โข (๐ โ ๐ โ โค) |
12 | 11 | zred 9375 |
. . . . 5
โข (๐ โ ๐ โ โ) |
13 | 7, 12 | resubcld 8338 |
. . . 4
โข (๐ โ ((๐ต ยท (2 ยท ๐)) โ ๐) โ โ) |
14 | | 2t1e2 9072 |
. . . . . . . . 9
โข (2
ยท 1) = 2 |
15 | 14 | oveq1i 5885 |
. . . . . . . 8
โข ((2
ยท 1) / (2 ยท ๐)) = (2 / (2 ยท ๐)) |
16 | | 1cnd 7973 |
. . . . . . . . 9
โข (๐ โ 1 โ
โ) |
17 | 5 | recnd 7986 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
18 | 2 | recnd 7986 |
. . . . . . . . 9
โข (๐ โ 2 โ
โ) |
19 | 4 | nnap0d 8965 |
. . . . . . . . 9
โข (๐ โ ๐ # 0) |
20 | | 2ap0 9012 |
. . . . . . . . . 10
โข 2 #
0 |
21 | 20 | a1i 9 |
. . . . . . . . 9
โข (๐ โ 2 # 0) |
22 | 16, 17, 18, 19, 21 | divcanap5d 8774 |
. . . . . . . 8
โข (๐ โ ((2 ยท 1) / (2
ยท ๐)) = (1 / ๐)) |
23 | 15, 22 | eqtr3id 2224 |
. . . . . . 7
โข (๐ โ (2 / (2 ยท ๐)) = (1 / ๐)) |
24 | | qbtwnrelemcalc.1n |
. . . . . . 7
โข (๐ โ (1 / ๐) < (๐ต โ ๐ด)) |
25 | 23, 24 | eqbrtrd 4026 |
. . . . . 6
โข (๐ โ (2 / (2 ยท ๐)) < (๐ต โ ๐ด)) |
26 | 3, 8 | resubcld 8338 |
. . . . . . 7
โข (๐ โ (๐ต โ ๐ด) โ โ) |
27 | | 2rp 9658 |
. . . . . . . . 9
โข 2 โ
โ+ |
28 | 27 | a1i 9 |
. . . . . . . 8
โข (๐ โ 2 โ
โ+) |
29 | 4 | nnrpd 9694 |
. . . . . . . 8
โข (๐ โ ๐ โ
โ+) |
30 | 28, 29 | rpmulcld 9713 |
. . . . . . 7
โข (๐ โ (2 ยท ๐) โ
โ+) |
31 | 2, 26, 30 | ltdivmul2d 9749 |
. . . . . 6
โข (๐ โ ((2 / (2 ยท ๐)) < (๐ต โ ๐ด) โ 2 < ((๐ต โ ๐ด) ยท (2 ยท ๐)))) |
32 | 25, 31 | mpbid 147 |
. . . . 5
โข (๐ โ 2 < ((๐ต โ ๐ด) ยท (2 ยท ๐))) |
33 | 3 | recnd 7986 |
. . . . . 6
โข (๐ โ ๐ต โ โ) |
34 | 8 | recnd 7986 |
. . . . . 6
โข (๐ โ ๐ด โ โ) |
35 | 18, 17 | mulcld 7978 |
. . . . . 6
โข (๐ โ (2 ยท ๐) โ
โ) |
36 | 33, 34, 35 | subdird 8372 |
. . . . 5
โข (๐ โ ((๐ต โ ๐ด) ยท (2 ยท ๐)) = ((๐ต ยท (2 ยท ๐)) โ (๐ด ยท (2 ยท ๐)))) |
37 | 32, 36 | breqtrd 4030 |
. . . 4
โข (๐ โ 2 < ((๐ต ยท (2 ยท ๐)) โ (๐ด ยท (2 ยท ๐)))) |
38 | | qbtwnrelemcalc.lt |
. . . . 5
โข (๐ โ ๐ < (๐ด ยท (2 ยท ๐))) |
39 | 12, 9, 7, 38 | ltsub2dd 8515 |
. . . 4
โข (๐ โ ((๐ต ยท (2 ยท ๐)) โ (๐ด ยท (2 ยท ๐))) < ((๐ต ยท (2 ยท ๐)) โ ๐)) |
40 | 2, 10, 13, 37, 39 | lttrd 8083 |
. . 3
โข (๐ โ 2 < ((๐ต ยท (2 ยท ๐)) โ ๐)) |
41 | 12, 2, 7 | ltaddsub2d 8503 |
. . 3
โข (๐ โ ((๐ + 2) < (๐ต ยท (2 ยท ๐)) โ 2 < ((๐ต ยท (2 ยท ๐)) โ ๐))) |
42 | 40, 41 | mpbird 167 |
. 2
โข (๐ โ (๐ + 2) < (๐ต ยท (2 ยท ๐))) |
43 | 12, 2 | readdcld 7987 |
. . 3
โข (๐ โ (๐ + 2) โ โ) |
44 | 43, 3, 30 | ltdivmul2d 9749 |
. 2
โข (๐ โ (((๐ + 2) / (2 ยท ๐)) < ๐ต โ (๐ + 2) < (๐ต ยท (2 ยท ๐)))) |
45 | 42, 44 | mpbird 167 |
1
โข (๐ โ ((๐ + 2) / (2 ยท ๐)) < ๐ต) |