Step | Hyp | Ref
| Expression |
1 | | simprl 529 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ๐ต โ โ) |
2 | | peano2re 8095 |
. . . 4
โข (๐ต โ โ โ (๐ต + 1) โ
โ) |
3 | 1, 2 | syl 14 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ต + 1) โ โ) |
4 | | simpll 527 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ๐ด โ โ) |
5 | | 0red 7960 |
. . . . . . 7
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ 0 โ
โ) |
6 | | simprr 531 |
. . . . . . 7
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ 0 โค ๐ต) |
7 | | ltp1 8803 |
. . . . . . . 8
โข (๐ต โ โ โ ๐ต < (๐ต + 1)) |
8 | 1, 7 | syl 14 |
. . . . . . 7
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ๐ต < (๐ต + 1)) |
9 | 5, 1, 3, 6, 8 | lelttrd 8084 |
. . . . . 6
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ 0 < (๐ต + 1)) |
10 | 3, 9 | gt0ap0d 8588 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ต + 1) # 0) |
11 | 4, 3, 10 | redivclapd 8794 |
. . . 4
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ด / (๐ต + 1)) โ โ) |
12 | | simpl 109 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ด โ โ โง 0 โค ๐ด)) |
13 | | divge0 8832 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง ((๐ต + 1) โ โ โง 0
< (๐ต + 1))) โ 0
โค (๐ด / (๐ต + 1))) |
14 | 12, 3, 9, 13 | syl12anc 1236 |
. . . 4
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ 0 โค (๐ด / (๐ต + 1))) |
15 | 11, 14 | jca 306 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ด / (๐ต + 1)) โ โ โง 0 โค (๐ด / (๐ต + 1)))) |
16 | 1, 3, 8 | ltled 8078 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ๐ต โค (๐ต + 1)) |
17 | | lemul2a 8818 |
. . 3
โข (((๐ต โ โ โง (๐ต + 1) โ โ โง
((๐ด / (๐ต + 1)) โ โ โง 0 โค (๐ด / (๐ต + 1)))) โง ๐ต โค (๐ต + 1)) โ ((๐ด / (๐ต + 1)) ยท ๐ต) โค ((๐ด / (๐ต + 1)) ยท (๐ต + 1))) |
18 | 1, 3, 15, 16, 17 | syl31anc 1241 |
. 2
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ด / (๐ต + 1)) ยท ๐ต) โค ((๐ด / (๐ต + 1)) ยท (๐ต + 1))) |
19 | 4 | recnd 7988 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ๐ด โ โ) |
20 | 3 | recnd 7988 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ต + 1) โ โ) |
21 | 19, 20, 10 | divcanap1d 8750 |
. 2
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ด / (๐ต + 1)) ยท (๐ต + 1)) = ๐ด) |
22 | 18, 21 | breqtrd 4031 |
1
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ด / (๐ต + 1)) ยท ๐ต) โค ๐ด) |