Step | Hyp | Ref
| Expression |
1 | | cvg1nlemcxze.c |
. . . . . . . 8
โข (๐ โ ๐ถ โ
โ+) |
2 | 1 | rpcnd 9698 |
. . . . . . 7
โข (๐ โ ๐ถ โ โ) |
3 | | 2cnd 8992 |
. . . . . . 7
โข (๐ โ 2 โ
โ) |
4 | | cvg1nlemcxze.x |
. . . . . . . 8
โข (๐ โ ๐ โ
โ+) |
5 | 4 | rpcnd 9698 |
. . . . . . 7
โข (๐ โ ๐ โ โ) |
6 | 4 | rpap0d 9702 |
. . . . . . 7
โข (๐ โ ๐ # 0) |
7 | 2, 3, 5, 6 | div23apd 8785 |
. . . . . 6
โข (๐ โ ((๐ถ ยท 2) / ๐) = ((๐ถ / ๐) ยท 2)) |
8 | | 2rp 9658 |
. . . . . . . . . . . . 13
โข 2 โ
โ+ |
9 | 8 | a1i 9 |
. . . . . . . . . . . 12
โข (๐ โ 2 โ
โ+) |
10 | 1, 9 | rpmulcld 9713 |
. . . . . . . . . . 11
โข (๐ โ (๐ถ ยท 2) โ
โ+) |
11 | 10, 4 | rpdivcld 9714 |
. . . . . . . . . 10
โข (๐ โ ((๐ถ ยท 2) / ๐) โ
โ+) |
12 | | cvg1nlemcxze.z |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โ) |
13 | 12 | nnrpd 9694 |
. . . . . . . . . 10
โข (๐ โ ๐ โ
โ+) |
14 | 11, 13 | rpdivcld 9714 |
. . . . . . . . 9
โข (๐ โ (((๐ถ ยท 2) / ๐) / ๐) โ
โ+) |
15 | 14 | rpred 9696 |
. . . . . . . 8
โข (๐ โ (((๐ถ ยท 2) / ๐) / ๐) โ โ) |
16 | | cvg1nlemcxze.a |
. . . . . . . . . 10
โข (๐ โ ๐ด โ โ) |
17 | 16 | nnred 8932 |
. . . . . . . . 9
โข (๐ โ ๐ด โ โ) |
18 | 15, 17 | readdcld 7987 |
. . . . . . . 8
โข (๐ โ ((((๐ถ ยท 2) / ๐) / ๐) + ๐ด) โ โ) |
19 | | cvg1nlemcxze.e |
. . . . . . . . 9
โข (๐ โ ๐ธ โ โ) |
20 | 19 | nnred 8932 |
. . . . . . . 8
โข (๐ โ ๐ธ โ โ) |
21 | 16 | nnrpd 9694 |
. . . . . . . . 9
โข (๐ โ ๐ด โ
โ+) |
22 | 15, 21 | ltaddrpd 9730 |
. . . . . . . 8
โข (๐ โ (((๐ถ ยท 2) / ๐) / ๐) < ((((๐ถ ยท 2) / ๐) / ๐) + ๐ด)) |
23 | | cvg1nlemcxze.1 |
. . . . . . . 8
โข (๐ โ ((((๐ถ ยท 2) / ๐) / ๐) + ๐ด) < ๐ธ) |
24 | 15, 18, 20, 22, 23 | lttrd 8083 |
. . . . . . 7
โข (๐ โ (((๐ถ ยท 2) / ๐) / ๐) < ๐ธ) |
25 | 11 | rpred 9696 |
. . . . . . . 8
โข (๐ โ ((๐ถ ยท 2) / ๐) โ โ) |
26 | 25, 20, 13 | ltdivmul2d 9749 |
. . . . . . 7
โข (๐ โ ((((๐ถ ยท 2) / ๐) / ๐) < ๐ธ โ ((๐ถ ยท 2) / ๐) < (๐ธ ยท ๐))) |
27 | 24, 26 | mpbid 147 |
. . . . . 6
โข (๐ โ ((๐ถ ยท 2) / ๐) < (๐ธ ยท ๐)) |
28 | 7, 27 | eqbrtrrd 4028 |
. . . . 5
โข (๐ โ ((๐ถ / ๐) ยท 2) < (๐ธ ยท ๐)) |
29 | 1 | rpred 9696 |
. . . . . . 7
โข (๐ โ ๐ถ โ โ) |
30 | 29, 4 | rerpdivcld 9728 |
. . . . . 6
โข (๐ โ (๐ถ / ๐) โ โ) |
31 | 19, 12 | nnmulcld 8968 |
. . . . . . 7
โข (๐ โ (๐ธ ยท ๐) โ โ) |
32 | 31 | nnred 8932 |
. . . . . 6
โข (๐ โ (๐ธ ยท ๐) โ โ) |
33 | 30, 32, 9 | ltmuldivd 9744 |
. . . . 5
โข (๐ โ (((๐ถ / ๐) ยท 2) < (๐ธ ยท ๐) โ (๐ถ / ๐) < ((๐ธ ยท ๐) / 2))) |
34 | 28, 33 | mpbid 147 |
. . . 4
โข (๐ โ (๐ถ / ๐) < ((๐ธ ยท ๐) / 2)) |
35 | 29, 9, 32, 4 | lt2mul2divd 9765 |
. . . 4
โข (๐ โ ((๐ถ ยท 2) < ((๐ธ ยท ๐) ยท ๐) โ (๐ถ / ๐) < ((๐ธ ยท ๐) / 2))) |
36 | 34, 35 | mpbird 167 |
. . 3
โข (๐ โ (๐ถ ยท 2) < ((๐ธ ยท ๐) ยท ๐)) |
37 | 31 | nncnd 8933 |
. . . 4
โข (๐ โ (๐ธ ยท ๐) โ โ) |
38 | 37, 5 | mulcomd 7979 |
. . 3
โข (๐ โ ((๐ธ ยท ๐) ยท ๐) = (๐ ยท (๐ธ ยท ๐))) |
39 | 36, 38 | breqtrd 4030 |
. 2
โข (๐ โ (๐ถ ยท 2) < (๐ ยท (๐ธ ยท ๐))) |
40 | 4 | rpred 9696 |
. . 3
โข (๐ โ ๐ โ โ) |
41 | 31 | nnrpd 9694 |
. . 3
โข (๐ โ (๐ธ ยท ๐) โ
โ+) |
42 | 29, 9, 40, 41 | lt2mul2divd 9765 |
. 2
โข (๐ โ ((๐ถ ยท 2) < (๐ ยท (๐ธ ยท ๐)) โ (๐ถ / (๐ธ ยท ๐)) < (๐ / 2))) |
43 | 39, 42 | mpbid 147 |
1
โข (๐ โ (๐ถ / (๐ธ ยท ๐)) < (๐ / 2)) |