Step | Hyp | Ref
| Expression |
1 | | simprl 769 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ๐ต โ โ) |
2 | | peano2re 11386 |
. . . 4
โข (๐ต โ โ โ (๐ต + 1) โ
โ) |
3 | 2 | ad2antrl 726 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ต + 1) โ โ) |
4 | | simpll 765 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ๐ด โ โ) |
5 | | ltp1 12053 |
. . . . . . . . 9
โข (๐ต โ โ โ ๐ต < (๐ต + 1)) |
6 | | 0re 11215 |
. . . . . . . . . . 11
โข 0 โ
โ |
7 | | lelttr 11303 |
. . . . . . . . . . 11
โข ((0
โ โ โง ๐ต
โ โ โง (๐ต +
1) โ โ) โ ((0 โค ๐ต โง ๐ต < (๐ต + 1)) โ 0 < (๐ต + 1))) |
8 | 6, 7 | mp3an1 1448 |
. . . . . . . . . 10
โข ((๐ต โ โ โง (๐ต + 1) โ โ) โ ((0
โค ๐ต โง ๐ต < (๐ต + 1)) โ 0 < (๐ต + 1))) |
9 | 2, 8 | mpdan 685 |
. . . . . . . . 9
โข (๐ต โ โ โ ((0 โค
๐ต โง ๐ต < (๐ต + 1)) โ 0 < (๐ต + 1))) |
10 | 5, 9 | mpan2d 692 |
. . . . . . . 8
โข (๐ต โ โ โ (0 โค
๐ต โ 0 < (๐ต + 1))) |
11 | 10 | imp 407 |
. . . . . . 7
โข ((๐ต โ โ โง 0 โค
๐ต) โ 0 < (๐ต + 1)) |
12 | 11 | gt0ne0d 11777 |
. . . . . 6
โข ((๐ต โ โ โง 0 โค
๐ต) โ (๐ต + 1) โ 0) |
13 | 12 | adantl 482 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ต + 1) โ 0) |
14 | 4, 3, 13 | redivcld 12041 |
. . . 4
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ด / (๐ต + 1)) โ โ) |
15 | 2 | adantr 481 |
. . . . . 6
โข ((๐ต โ โ โง 0 โค
๐ต) โ (๐ต + 1) โ
โ) |
16 | 15, 11 | jca 512 |
. . . . 5
โข ((๐ต โ โ โง 0 โค
๐ต) โ ((๐ต + 1) โ โ โง 0
< (๐ต +
1))) |
17 | | divge0 12082 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง ((๐ต + 1) โ โ โง 0
< (๐ต + 1))) โ 0
โค (๐ด / (๐ต + 1))) |
18 | 16, 17 | sylan2 593 |
. . . 4
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ 0 โค (๐ด / (๐ต + 1))) |
19 | 14, 18 | jca 512 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ด / (๐ต + 1)) โ โ โง 0 โค (๐ด / (๐ต + 1)))) |
20 | | lep1 12054 |
. . . 4
โข (๐ต โ โ โ ๐ต โค (๐ต + 1)) |
21 | 20 | ad2antrl 726 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ๐ต โค (๐ต + 1)) |
22 | | lemul2a 12068 |
. . 3
โข (((๐ต โ โ โง (๐ต + 1) โ โ โง
((๐ด / (๐ต + 1)) โ โ โง 0 โค (๐ด / (๐ต + 1)))) โง ๐ต โค (๐ต + 1)) โ ((๐ด / (๐ต + 1)) ยท ๐ต) โค ((๐ด / (๐ต + 1)) ยท (๐ต + 1))) |
23 | 1, 3, 19, 21, 22 | syl31anc 1373 |
. 2
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ด / (๐ต + 1)) ยท ๐ต) โค ((๐ด / (๐ต + 1)) ยท (๐ต + 1))) |
24 | | recn 11199 |
. . . 4
โข (๐ด โ โ โ ๐ด โ
โ) |
25 | 24 | ad2antrr 724 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ๐ด โ โ) |
26 | 2 | recnd 11241 |
. . . 4
โข (๐ต โ โ โ (๐ต + 1) โ
โ) |
27 | 26 | ad2antrl 726 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ต + 1) โ โ) |
28 | 25, 27, 13 | divcan1d 11990 |
. 2
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ด / (๐ต + 1)) ยท (๐ต + 1)) = ๐ด) |
29 | 23, 28 | breqtrd 5174 |
1
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ด / (๐ต + 1)) ยท ๐ต) โค ๐ด) |