Step | Hyp | Ref
| Expression |
1 | | divalglemnqt.rd |
. . 3
โข (๐ โ ๐
< ๐ท) |
2 | 1 | adantr 276 |
. 2
โข ((๐ โง ๐ < ๐) โ ๐
< ๐ท) |
3 | | divalglemnqt.d |
. . . . 5
โข (๐ โ ๐ท โ โ) |
4 | 3 | adantr 276 |
. . . 4
โข ((๐ โง ๐ < ๐) โ ๐ท โ โ) |
5 | 4 | nnred 8931 |
. . 3
โข ((๐ โง ๐ < ๐) โ ๐ท โ โ) |
6 | | divalglemnqt.r |
. . . . 5
โข (๐ โ ๐
โ โค) |
7 | 6 | adantr 276 |
. . . 4
โข ((๐ โง ๐ < ๐) โ ๐
โ โค) |
8 | 7 | zred 9374 |
. . 3
โข ((๐ โง ๐ < ๐) โ ๐
โ โ) |
9 | | divalglemnqt.s |
. . . . . . 7
โข (๐ โ ๐ โ โค) |
10 | 9 | adantr 276 |
. . . . . 6
โข ((๐ โง ๐ < ๐) โ ๐ โ โค) |
11 | 10 | zred 9374 |
. . . . 5
โข ((๐ โง ๐ < ๐) โ ๐ โ โ) |
12 | 5, 11 | readdcld 7986 |
. . . 4
โข ((๐ โง ๐ < ๐) โ (๐ท + ๐) โ โ) |
13 | | divalglemnqt.0s |
. . . . . 6
โข (๐ โ 0 โค ๐) |
14 | 13 | adantr 276 |
. . . . 5
โข ((๐ โง ๐ < ๐) โ 0 โค ๐) |
15 | 5, 11 | addge01d 8489 |
. . . . 5
โข ((๐ โง ๐ < ๐) โ (0 โค ๐ โ ๐ท โค (๐ท + ๐))) |
16 | 14, 15 | mpbid 147 |
. . . 4
โข ((๐ โง ๐ < ๐) โ ๐ท โค (๐ท + ๐)) |
17 | | divalglemnqt.q |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โค) |
18 | 17 | adantr 276 |
. . . . . . . . . 10
โข ((๐ โง ๐ < ๐) โ ๐ โ โค) |
19 | 18 | zred 9374 |
. . . . . . . . 9
โข ((๐ โง ๐ < ๐) โ ๐ โ โ) |
20 | 19 | recnd 7985 |
. . . . . . . 8
โข ((๐ โง ๐ < ๐) โ ๐ โ โ) |
21 | 5 | recnd 7985 |
. . . . . . . 8
โข ((๐ โง ๐ < ๐) โ ๐ท โ โ) |
22 | 20, 21 | mulcld 7977 |
. . . . . . 7
โข ((๐ โง ๐ < ๐) โ (๐ ยท ๐ท) โ โ) |
23 | 11 | recnd 7985 |
. . . . . . 7
โข ((๐ โง ๐ < ๐) โ ๐ โ โ) |
24 | 22, 21, 23 | addassd 7979 |
. . . . . 6
โข ((๐ โง ๐ < ๐) โ (((๐ ยท ๐ท) + ๐ท) + ๐) = ((๐ ยท ๐ท) + (๐ท + ๐))) |
25 | 19, 5 | remulcld 7987 |
. . . . . . . . 9
โข ((๐ โง ๐ < ๐) โ (๐ ยท ๐ท) โ โ) |
26 | 25, 5 | readdcld 7986 |
. . . . . . . 8
โข ((๐ โง ๐ < ๐) โ ((๐ ยท ๐ท) + ๐ท) โ โ) |
27 | | divalglemnqt.t |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โค) |
28 | 27 | adantr 276 |
. . . . . . . . . 10
โข ((๐ โง ๐ < ๐) โ ๐ โ โค) |
29 | 28 | zred 9374 |
. . . . . . . . 9
โข ((๐ โง ๐ < ๐) โ ๐ โ โ) |
30 | 29, 5 | remulcld 7987 |
. . . . . . . 8
โข ((๐ โง ๐ < ๐) โ (๐ ยท ๐ท) โ โ) |
31 | 20, 21 | adddirp1d 7983 |
. . . . . . . . 9
โข ((๐ โง ๐ < ๐) โ ((๐ + 1) ยท ๐ท) = ((๐ ยท ๐ท) + ๐ท)) |
32 | | peano2re 8092 |
. . . . . . . . . . 11
โข (๐ โ โ โ (๐ + 1) โ
โ) |
33 | 19, 32 | syl 14 |
. . . . . . . . . 10
โข ((๐ โง ๐ < ๐) โ (๐ + 1) โ โ) |
34 | 4 | nnnn0d 9228 |
. . . . . . . . . . 11
โข ((๐ โง ๐ < ๐) โ ๐ท โ
โ0) |
35 | 34 | nn0ge0d 9231 |
. . . . . . . . . 10
โข ((๐ โง ๐ < ๐) โ 0 โค ๐ท) |
36 | | simpr 110 |
. . . . . . . . . . 11
โข ((๐ โง ๐ < ๐) โ ๐ < ๐) |
37 | | zltp1le 9306 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ โ โค) โ (๐ < ๐ โ (๐ + 1) โค ๐)) |
38 | 17, 28, 37 | syl2an2r 595 |
. . . . . . . . . . 11
โข ((๐ โง ๐ < ๐) โ (๐ < ๐ โ (๐ + 1) โค ๐)) |
39 | 36, 38 | mpbid 147 |
. . . . . . . . . 10
โข ((๐ โง ๐ < ๐) โ (๐ + 1) โค ๐) |
40 | 33, 29, 5, 35, 39 | lemul1ad 8895 |
. . . . . . . . 9
โข ((๐ โง ๐ < ๐) โ ((๐ + 1) ยท ๐ท) โค (๐ ยท ๐ท)) |
41 | 31, 40 | eqbrtrrd 4027 |
. . . . . . . 8
โข ((๐ โง ๐ < ๐) โ ((๐ ยท ๐ท) + ๐ท) โค (๐ ยท ๐ท)) |
42 | 26, 30, 11, 41 | leadd1dd 8515 |
. . . . . . 7
โข ((๐ โง ๐ < ๐) โ (((๐ ยท ๐ท) + ๐ท) + ๐) โค ((๐ ยท ๐ท) + ๐)) |
43 | | divalglemnqt.eq |
. . . . . . . 8
โข (๐ โ ((๐ ยท ๐ท) + ๐
) = ((๐ ยท ๐ท) + ๐)) |
44 | 43 | adantr 276 |
. . . . . . 7
โข ((๐ โง ๐ < ๐) โ ((๐ ยท ๐ท) + ๐
) = ((๐ ยท ๐ท) + ๐)) |
45 | 42, 44 | breqtrrd 4031 |
. . . . . 6
โข ((๐ โง ๐ < ๐) โ (((๐ ยท ๐ท) + ๐ท) + ๐) โค ((๐ ยท ๐ท) + ๐
)) |
46 | 24, 45 | eqbrtrrd 4027 |
. . . . 5
โข ((๐ โง ๐ < ๐) โ ((๐ ยท ๐ท) + (๐ท + ๐)) โค ((๐ ยท ๐ท) + ๐
)) |
47 | 12, 8, 25 | leadd2d 8496 |
. . . . 5
โข ((๐ โง ๐ < ๐) โ ((๐ท + ๐) โค ๐
โ ((๐ ยท ๐ท) + (๐ท + ๐)) โค ((๐ ยท ๐ท) + ๐
))) |
48 | 46, 47 | mpbird 167 |
. . . 4
โข ((๐ โง ๐ < ๐) โ (๐ท + ๐) โค ๐
) |
49 | 5, 12, 8, 16, 48 | letrd 8080 |
. . 3
โข ((๐ โง ๐ < ๐) โ ๐ท โค ๐
) |
50 | 5, 8, 49 | lensymd 8078 |
. 2
โข ((๐ โง ๐ < ๐) โ ยฌ ๐
< ๐ท) |
51 | 2, 50 | pm2.65da 661 |
1
โข (๐ โ ยฌ ๐ < ๐) |