Step | Hyp | Ref
| Expression |
1 | | refldivcl 13734 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ+)
โ (โโ(๐ด /
๐ต)) โ
โ) |
2 | | peano2re 11333 |
. . . . . 6
โข
((โโ(๐ด /
๐ต)) โ โ โ
((โโ(๐ด / ๐ต)) + 1) โ
โ) |
3 | 1, 2 | syl 17 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ+)
โ ((โโ(๐ด /
๐ต)) + 1) โ
โ) |
4 | 3 | 3adant3 1133 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ+
โง ๐ถ โ โ)
โ ((โโ(๐ด /
๐ต)) + 1) โ
โ) |
5 | 4 | adantr 482 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ+
โง ๐ถ โ โ)
โง ๐ด < (๐ถ โ ๐ต)) โ ((โโ(๐ด / ๐ต)) + 1) โ โ) |
6 | | rerpdivcl 12950 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ+)
โ (๐ด / ๐ต) โ
โ) |
7 | | peano2re 11333 |
. . . . . 6
โข ((๐ด / ๐ต) โ โ โ ((๐ด / ๐ต) + 1) โ โ) |
8 | 6, 7 | syl 17 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ+)
โ ((๐ด / ๐ต) + 1) โ
โ) |
9 | 8 | 3adant3 1133 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ+
โง ๐ถ โ โ)
โ ((๐ด / ๐ต) + 1) โ
โ) |
10 | 9 | adantr 482 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ+
โง ๐ถ โ โ)
โง ๐ด < (๐ถ โ ๐ต)) โ ((๐ด / ๐ต) + 1) โ โ) |
11 | | rerpdivcl 12950 |
. . . . . 6
โข ((๐ถ โ โ โง ๐ต โ โ+)
โ (๐ถ / ๐ต) โ
โ) |
12 | 11 | ancoms 460 |
. . . . 5
โข ((๐ต โ โ+
โง ๐ถ โ โ)
โ (๐ถ / ๐ต) โ
โ) |
13 | 12 | 3adant1 1131 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ+
โง ๐ถ โ โ)
โ (๐ถ / ๐ต) โ
โ) |
14 | 13 | adantr 482 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ+
โง ๐ถ โ โ)
โง ๐ด < (๐ถ โ ๐ต)) โ (๐ถ / ๐ต) โ โ) |
15 | 1 | 3adant3 1133 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ+
โง ๐ถ โ โ)
โ (โโ(๐ด /
๐ต)) โ
โ) |
16 | 15 | adantr 482 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ+
โง ๐ถ โ โ)
โง ๐ด < (๐ถ โ ๐ต)) โ (โโ(๐ด / ๐ต)) โ โ) |
17 | 6 | 3adant3 1133 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ+
โง ๐ถ โ โ)
โ (๐ด / ๐ต) โ
โ) |
18 | 17 | adantr 482 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ+
โง ๐ถ โ โ)
โง ๐ด < (๐ถ โ ๐ต)) โ (๐ด / ๐ต) โ โ) |
19 | | 1red 11161 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ+
โง ๐ถ โ โ)
โง ๐ด < (๐ถ โ ๐ต)) โ 1 โ โ) |
20 | | 3simpa 1149 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ+
โง ๐ถ โ โ)
โ (๐ด โ โ
โง ๐ต โ
โ+)) |
21 | 20 | adantr 482 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ+
โง ๐ถ โ โ)
โง ๐ด < (๐ถ โ ๐ต)) โ (๐ด โ โ โง ๐ต โ
โ+)) |
22 | | fldivle 13742 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ+)
โ (โโ(๐ด /
๐ต)) โค (๐ด / ๐ต)) |
23 | 21, 22 | syl 17 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ+
โง ๐ถ โ โ)
โง ๐ด < (๐ถ โ ๐ต)) โ (โโ(๐ด / ๐ต)) โค (๐ด / ๐ต)) |
24 | 16, 18, 19, 23 | leadd1dd 11774 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ+
โง ๐ถ โ โ)
โง ๐ด < (๐ถ โ ๐ต)) โ ((โโ(๐ด / ๐ต)) + 1) โค ((๐ด / ๐ต) + 1)) |
25 | | rpre 12928 |
. . . . . . 7
โข (๐ต โ โ+
โ ๐ต โ
โ) |
26 | | ltaddsub 11634 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด + ๐ต) < ๐ถ โ ๐ด < (๐ถ โ ๐ต))) |
27 | 25, 26 | syl3an2 1165 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ+
โง ๐ถ โ โ)
โ ((๐ด + ๐ต) < ๐ถ โ ๐ด < (๐ถ โ ๐ต))) |
28 | 27 | biimpar 479 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ+
โง ๐ถ โ โ)
โง ๐ด < (๐ถ โ ๐ต)) โ (๐ด + ๐ต) < ๐ถ) |
29 | | recn 11146 |
. . . . . . . . . 10
โข ((๐ด / ๐ต) โ โ โ (๐ด / ๐ต) โ โ) |
30 | 6, 29 | syl 17 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ+)
โ (๐ด / ๐ต) โ
โ) |
31 | 30 | 3adant3 1133 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ+
โง ๐ถ โ โ)
โ (๐ด / ๐ต) โ
โ) |
32 | | rpcn 12930 |
. . . . . . . . 9
โข (๐ต โ โ+
โ ๐ต โ
โ) |
33 | 32 | 3ad2ant2 1135 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ+
โง ๐ถ โ โ)
โ ๐ต โ
โ) |
34 | | 1cnd 11155 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ+
โง ๐ถ โ โ)
โ 1 โ โ) |
35 | | recn 11146 |
. . . . . . . . . . 11
โข (๐ด โ โ โ ๐ด โ
โ) |
36 | 35 | 3ad2ant1 1134 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ+
โง ๐ถ โ โ)
โ ๐ด โ
โ) |
37 | | rpne0 12936 |
. . . . . . . . . . 11
โข (๐ต โ โ+
โ ๐ต โ
0) |
38 | 37 | 3ad2ant2 1135 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ+
โง ๐ถ โ โ)
โ ๐ต โ
0) |
39 | 36, 33, 38 | divcan1d 11937 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ+
โง ๐ถ โ โ)
โ ((๐ด / ๐ต) ยท ๐ต) = ๐ด) |
40 | 32 | mulid2d 11178 |
. . . . . . . . . 10
โข (๐ต โ โ+
โ (1 ยท ๐ต) =
๐ต) |
41 | 40 | 3ad2ant2 1135 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ+
โง ๐ถ โ โ)
โ (1 ยท ๐ต) =
๐ต) |
42 | 39, 41 | oveq12d 7376 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ+
โง ๐ถ โ โ)
โ (((๐ด / ๐ต) ยท ๐ต) + (1 ยท ๐ต)) = (๐ด + ๐ต)) |
43 | 31, 33, 34, 42 | joinlmuladdmuld 11187 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ+
โง ๐ถ โ โ)
โ (((๐ด / ๐ต) + 1) ยท ๐ต) = (๐ด + ๐ต)) |
44 | | recn 11146 |
. . . . . . . . 9
โข (๐ถ โ โ โ ๐ถ โ
โ) |
45 | 44 | 3ad2ant3 1136 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ+
โง ๐ถ โ โ)
โ ๐ถ โ
โ) |
46 | 45, 33, 38 | divcan1d 11937 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ+
โง ๐ถ โ โ)
โ ((๐ถ / ๐ต) ยท ๐ต) = ๐ถ) |
47 | 43, 46 | breq12d 5119 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ+
โง ๐ถ โ โ)
โ ((((๐ด / ๐ต) + 1) ยท ๐ต) < ((๐ถ / ๐ต) ยท ๐ต) โ (๐ด + ๐ต) < ๐ถ)) |
48 | 47 | adantr 482 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ+
โง ๐ถ โ โ)
โง ๐ด < (๐ถ โ ๐ต)) โ ((((๐ด / ๐ต) + 1) ยท ๐ต) < ((๐ถ / ๐ต) ยท ๐ต) โ (๐ด + ๐ต) < ๐ถ)) |
49 | 28, 48 | mpbird 257 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ+
โง ๐ถ โ โ)
โง ๐ด < (๐ถ โ ๐ต)) โ (((๐ด / ๐ต) + 1) ยท ๐ต) < ((๐ถ / ๐ต) ยท ๐ต)) |
50 | 17, 7 | syl 17 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ+
โง ๐ถ โ โ)
โ ((๐ด / ๐ต) + 1) โ
โ) |
51 | | simp2 1138 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ+
โง ๐ถ โ โ)
โ ๐ต โ
โ+) |
52 | 50, 13, 51 | ltmul1d 13003 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ+
โง ๐ถ โ โ)
โ (((๐ด / ๐ต) + 1) < (๐ถ / ๐ต) โ (((๐ด / ๐ต) + 1) ยท ๐ต) < ((๐ถ / ๐ต) ยท ๐ต))) |
53 | 52 | adantr 482 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ+
โง ๐ถ โ โ)
โง ๐ด < (๐ถ โ ๐ต)) โ (((๐ด / ๐ต) + 1) < (๐ถ / ๐ต) โ (((๐ด / ๐ต) + 1) ยท ๐ต) < ((๐ถ / ๐ต) ยท ๐ต))) |
54 | 49, 53 | mpbird 257 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ+
โง ๐ถ โ โ)
โง ๐ด < (๐ถ โ ๐ต)) โ ((๐ด / ๐ต) + 1) < (๐ถ / ๐ต)) |
55 | 5, 10, 14, 24, 54 | lelttrd 11318 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ+
โง ๐ถ โ โ)
โง ๐ด < (๐ถ โ ๐ต)) โ ((โโ(๐ด / ๐ต)) + 1) < (๐ถ / ๐ต)) |
56 | 55 | ex 414 |
1
โข ((๐ด โ โ โง ๐ต โ โ+
โง ๐ถ โ โ)
โ (๐ด < (๐ถ โ ๐ต) โ ((โโ(๐ด / ๐ต)) + 1) < (๐ถ / ๐ต))) |