Step | Hyp | Ref
| Expression |
1 | | numlt.1 |
. . . . 5
โข ๐ โ โ |
2 | | numlt.2 |
. . . . 5
โข ๐ด โ
โ0 |
3 | | numltc.3 |
. . . . 5
โข ๐ถ โ
โ0 |
4 | | numltc.5 |
. . . . 5
โข ๐ถ < ๐ |
5 | 1, 2, 3, 1, 4 | numlt 9379 |
. . . 4
โข ((๐ ยท ๐ด) + ๐ถ) < ((๐ ยท ๐ด) + ๐) |
6 | 1 | nnrei 8899 |
. . . . . . 7
โข ๐ โ โ |
7 | 6 | recni 7944 |
. . . . . 6
โข ๐ โ โ |
8 | 2 | nn0rei 9158 |
. . . . . . 7
โข ๐ด โ โ |
9 | 8 | recni 7944 |
. . . . . 6
โข ๐ด โ โ |
10 | | ax-1cn 7879 |
. . . . . 6
โข 1 โ
โ |
11 | 7, 9, 10 | adddii 7942 |
. . . . 5
โข (๐ ยท (๐ด + 1)) = ((๐ ยท ๐ด) + (๐ ยท 1)) |
12 | 7 | mulid1i 7934 |
. . . . . 6
โข (๐ ยท 1) = ๐ |
13 | 12 | oveq2i 5876 |
. . . . 5
โข ((๐ ยท ๐ด) + (๐ ยท 1)) = ((๐ ยท ๐ด) + ๐) |
14 | 11, 13 | eqtri 2196 |
. . . 4
โข (๐ ยท (๐ด + 1)) = ((๐ ยท ๐ด) + ๐) |
15 | 5, 14 | breqtrri 4025 |
. . 3
โข ((๐ ยท ๐ด) + ๐ถ) < (๐ ยท (๐ด + 1)) |
16 | | numltc.6 |
. . . . 5
โข ๐ด < ๐ต |
17 | | numlt.3 |
. . . . . 6
โข ๐ต โ
โ0 |
18 | | nn0ltp1le 9286 |
. . . . . 6
โข ((๐ด โ โ0
โง ๐ต โ
โ0) โ (๐ด < ๐ต โ (๐ด + 1) โค ๐ต)) |
19 | 2, 17, 18 | mp2an 426 |
. . . . 5
โข (๐ด < ๐ต โ (๐ด + 1) โค ๐ต) |
20 | 16, 19 | mpbi 145 |
. . . 4
โข (๐ด + 1) โค ๐ต |
21 | 1 | nngt0i 8920 |
. . . . 5
โข 0 <
๐ |
22 | | peano2re 8067 |
. . . . . . 7
โข (๐ด โ โ โ (๐ด + 1) โ
โ) |
23 | 8, 22 | ax-mp 5 |
. . . . . 6
โข (๐ด + 1) โ
โ |
24 | 17 | nn0rei 9158 |
. . . . . 6
โข ๐ต โ โ |
25 | 23, 24, 6 | lemul2i 8853 |
. . . . 5
โข (0 <
๐ โ ((๐ด + 1) โค ๐ต โ (๐ ยท (๐ด + 1)) โค (๐ ยท ๐ต))) |
26 | 21, 25 | ax-mp 5 |
. . . 4
โข ((๐ด + 1) โค ๐ต โ (๐ ยท (๐ด + 1)) โค (๐ ยท ๐ต)) |
27 | 20, 26 | mpbi 145 |
. . 3
โข (๐ ยท (๐ด + 1)) โค (๐ ยท ๐ต) |
28 | 6, 8 | remulcli 7946 |
. . . . 5
โข (๐ ยท ๐ด) โ โ |
29 | 3 | nn0rei 9158 |
. . . . 5
โข ๐ถ โ โ |
30 | 28, 29 | readdcli 7945 |
. . . 4
โข ((๐ ยท ๐ด) + ๐ถ) โ โ |
31 | 6, 23 | remulcli 7946 |
. . . 4
โข (๐ ยท (๐ด + 1)) โ โ |
32 | 6, 24 | remulcli 7946 |
. . . 4
โข (๐ ยท ๐ต) โ โ |
33 | 30, 31, 32 | ltletri 8038 |
. . 3
โข ((((๐ ยท ๐ด) + ๐ถ) < (๐ ยท (๐ด + 1)) โง (๐ ยท (๐ด + 1)) โค (๐ ยท ๐ต)) โ ((๐ ยท ๐ด) + ๐ถ) < (๐ ยท ๐ต)) |
34 | 15, 27, 33 | mp2an 426 |
. 2
โข ((๐ ยท ๐ด) + ๐ถ) < (๐ ยท ๐ต) |
35 | | numltc.4 |
. . 3
โข ๐ท โ
โ0 |
36 | 32, 35 | nn0addge1i 9195 |
. 2
โข (๐ ยท ๐ต) โค ((๐ ยท ๐ต) + ๐ท) |
37 | 35 | nn0rei 9158 |
. . . 4
โข ๐ท โ โ |
38 | 32, 37 | readdcli 7945 |
. . 3
โข ((๐ ยท ๐ต) + ๐ท) โ โ |
39 | 30, 32, 38 | ltletri 8038 |
. 2
โข ((((๐ ยท ๐ด) + ๐ถ) < (๐ ยท ๐ต) โง (๐ ยท ๐ต) โค ((๐ ยท ๐ต) + ๐ท)) โ ((๐ ยท ๐ด) + ๐ถ) < ((๐ ยท ๐ต) + ๐ท)) |
40 | 34, 36, 39 | mp2an 426 |
1
โข ((๐ ยท ๐ด) + ๐ถ) < ((๐ ยท ๐ต) + ๐ท) |