Step | Hyp | Ref
| Expression |
1 | | simprl 770 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ๐ต โ โ) |
2 | | peano2re 11336 |
. . . 4
โข (๐ต โ โ โ (๐ต + 1) โ
โ) |
3 | 2 | ad2antrl 727 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ต + 1) โ โ) |
4 | | simpll 766 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ๐ด โ โ) |
5 | | ltp1 12003 |
. . . . . . . . 9
โข (๐ต โ โ โ ๐ต < (๐ต + 1)) |
6 | | 0re 11165 |
. . . . . . . . . . 11
โข 0 โ
โ |
7 | | lelttr 11253 |
. . . . . . . . . . 11
โข ((0
โ โ โง ๐ต
โ โ โง (๐ต +
1) โ โ) โ ((0 โค ๐ต โง ๐ต < (๐ต + 1)) โ 0 < (๐ต + 1))) |
8 | 6, 7 | mp3an1 1449 |
. . . . . . . . . 10
โข ((๐ต โ โ โง (๐ต + 1) โ โ) โ ((0
โค ๐ต โง ๐ต < (๐ต + 1)) โ 0 < (๐ต + 1))) |
9 | 2, 8 | mpdan 686 |
. . . . . . . . 9
โข (๐ต โ โ โ ((0 โค
๐ต โง ๐ต < (๐ต + 1)) โ 0 < (๐ต + 1))) |
10 | 5, 9 | mpan2d 693 |
. . . . . . . 8
โข (๐ต โ โ โ (0 โค
๐ต โ 0 < (๐ต + 1))) |
11 | 10 | imp 408 |
. . . . . . 7
โข ((๐ต โ โ โง 0 โค
๐ต) โ 0 < (๐ต + 1)) |
12 | 11 | gt0ne0d 11727 |
. . . . . 6
โข ((๐ต โ โ โง 0 โค
๐ต) โ (๐ต + 1) โ 0) |
13 | 12 | adantl 483 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ต + 1) โ 0) |
14 | 4, 3, 13 | redivcld 11991 |
. . . 4
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ด / (๐ต + 1)) โ โ) |
15 | 2 | adantr 482 |
. . . . . 6
โข ((๐ต โ โ โง 0 โค
๐ต) โ (๐ต + 1) โ
โ) |
16 | 15, 11 | jca 513 |
. . . . 5
โข ((๐ต โ โ โง 0 โค
๐ต) โ ((๐ต + 1) โ โ โง 0
< (๐ต +
1))) |
17 | | divge0 12032 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง ((๐ต + 1) โ โ โง 0
< (๐ต + 1))) โ 0
โค (๐ด / (๐ต + 1))) |
18 | 16, 17 | sylan2 594 |
. . . 4
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ 0 โค (๐ด / (๐ต + 1))) |
19 | 14, 18 | jca 513 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ด / (๐ต + 1)) โ โ โง 0 โค (๐ด / (๐ต + 1)))) |
20 | | lep1 12004 |
. . . 4
โข (๐ต โ โ โ ๐ต โค (๐ต + 1)) |
21 | 20 | ad2antrl 727 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ๐ต โค (๐ต + 1)) |
22 | | lemul2a 12018 |
. . 3
โข (((๐ต โ โ โง (๐ต + 1) โ โ โง
((๐ด / (๐ต + 1)) โ โ โง 0 โค (๐ด / (๐ต + 1)))) โง ๐ต โค (๐ต + 1)) โ ((๐ด / (๐ต + 1)) ยท ๐ต) โค ((๐ด / (๐ต + 1)) ยท (๐ต + 1))) |
23 | 1, 3, 19, 21, 22 | syl31anc 1374 |
. 2
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ด / (๐ต + 1)) ยท ๐ต) โค ((๐ด / (๐ต + 1)) ยท (๐ต + 1))) |
24 | | recn 11149 |
. . . 4
โข (๐ด โ โ โ ๐ด โ
โ) |
25 | 24 | ad2antrr 725 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ๐ด โ โ) |
26 | 2 | recnd 11191 |
. . . 4
โข (๐ต โ โ โ (๐ต + 1) โ
โ) |
27 | 26 | ad2antrl 727 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ต + 1) โ โ) |
28 | 25, 27, 13 | divcan1d 11940 |
. 2
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ด / (๐ต + 1)) ยท (๐ต + 1)) = ๐ด) |
29 | 23, 28 | breqtrd 5135 |
1
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ด / (๐ต + 1)) ยท ๐ต) โค ๐ด) |