Step | Hyp | Ref
| Expression |
1 | | nn0opthlem1d.1 |
. . . 4
โข (๐ โ ๐ด โ
โ0) |
2 | | 1nn0 9205 |
. . . . 5
โข 1 โ
โ0 |
3 | 2 | a1i 9 |
. . . 4
โข (๐ โ 1 โ
โ0) |
4 | 1, 3 | nn0addcld 9246 |
. . 3
โข (๐ โ (๐ด + 1) โ
โ0) |
5 | | nn0opthlem1d.2 |
. . 3
โข (๐ โ ๐ถ โ
โ0) |
6 | 4, 5 | nn0le2msqd 10712 |
. 2
โข (๐ โ ((๐ด + 1) โค ๐ถ โ ((๐ด + 1) ยท (๐ด + 1)) โค (๐ถ ยท ๐ถ))) |
7 | | nn0ltp1le 9328 |
. . 3
โข ((๐ด โ โ0
โง ๐ถ โ
โ0) โ (๐ด < ๐ถ โ (๐ด + 1) โค ๐ถ)) |
8 | 1, 5, 7 | syl2anc 411 |
. 2
โข (๐ โ (๐ด < ๐ถ โ (๐ด + 1) โค ๐ถ)) |
9 | 1, 1 | nn0mulcld 9247 |
. . . . 5
โข (๐ โ (๐ด ยท ๐ด) โ
โ0) |
10 | | 2nn0 9206 |
. . . . . . 7
โข 2 โ
โ0 |
11 | 10 | a1i 9 |
. . . . . 6
โข (๐ โ 2 โ
โ0) |
12 | 11, 1 | nn0mulcld 9247 |
. . . . 5
โข (๐ โ (2 ยท ๐ด) โ
โ0) |
13 | 9, 12 | nn0addcld 9246 |
. . . 4
โข (๐ โ ((๐ด ยท ๐ด) + (2 ยท ๐ด)) โ
โ0) |
14 | 5, 5 | nn0mulcld 9247 |
. . . 4
โข (๐ โ (๐ถ ยท ๐ถ) โ
โ0) |
15 | | nn0ltp1le 9328 |
. . . 4
โข ((((๐ด ยท ๐ด) + (2 ยท ๐ด)) โ โ0 โง (๐ถ ยท ๐ถ) โ โ0) โ
(((๐ด ยท ๐ด) + (2 ยท ๐ด)) < (๐ถ ยท ๐ถ) โ (((๐ด ยท ๐ด) + (2 ยท ๐ด)) + 1) โค (๐ถ ยท ๐ถ))) |
16 | 13, 14, 15 | syl2anc 411 |
. . 3
โข (๐ โ (((๐ด ยท ๐ด) + (2 ยท ๐ด)) < (๐ถ ยท ๐ถ) โ (((๐ด ยท ๐ด) + (2 ยท ๐ด)) + 1) โค (๐ถ ยท ๐ถ))) |
17 | 1 | nn0cnd 9244 |
. . . . . . 7
โข (๐ โ ๐ด โ โ) |
18 | | 1cnd 7986 |
. . . . . . 7
โข (๐ โ 1 โ
โ) |
19 | | binom2 10645 |
. . . . . . 7
โข ((๐ด โ โ โง 1 โ
โ) โ ((๐ด +
1)โ2) = (((๐ดโ2) +
(2 ยท (๐ด ยท
1))) + (1โ2))) |
20 | 17, 18, 19 | syl2anc 411 |
. . . . . 6
โข (๐ โ ((๐ด + 1)โ2) = (((๐ดโ2) + (2 ยท (๐ด ยท 1))) +
(1โ2))) |
21 | 17, 18 | addcld 7990 |
. . . . . . 7
โข (๐ โ (๐ด + 1) โ โ) |
22 | 21 | sqvald 10664 |
. . . . . 6
โข (๐ โ ((๐ด + 1)โ2) = ((๐ด + 1) ยท (๐ด + 1))) |
23 | 17 | sqvald 10664 |
. . . . . . . 8
โข (๐ โ (๐ดโ2) = (๐ด ยท ๐ด)) |
24 | 23 | oveq1d 5903 |
. . . . . . 7
โข (๐ โ ((๐ดโ2) + (2 ยท (๐ด ยท 1))) = ((๐ด ยท ๐ด) + (2 ยท (๐ด ยท 1)))) |
25 | 18 | sqvald 10664 |
. . . . . . 7
โข (๐ โ (1โ2) = (1 ยท
1)) |
26 | 24, 25 | oveq12d 5906 |
. . . . . 6
โข (๐ โ (((๐ดโ2) + (2 ยท (๐ด ยท 1))) + (1โ2)) = (((๐ด ยท ๐ด) + (2 ยท (๐ด ยท 1))) + (1 ยท
1))) |
27 | 20, 22, 26 | 3eqtr3d 2228 |
. . . . 5
โข (๐ โ ((๐ด + 1) ยท (๐ด + 1)) = (((๐ด ยท ๐ด) + (2 ยท (๐ด ยท 1))) + (1 ยท
1))) |
28 | 17 | mulridd 7987 |
. . . . . . . 8
โข (๐ โ (๐ด ยท 1) = ๐ด) |
29 | 28 | oveq2d 5904 |
. . . . . . 7
โข (๐ โ (2 ยท (๐ด ยท 1)) = (2 ยท
๐ด)) |
30 | 29 | oveq2d 5904 |
. . . . . 6
โข (๐ โ ((๐ด ยท ๐ด) + (2 ยท (๐ด ยท 1))) = ((๐ด ยท ๐ด) + (2 ยท ๐ด))) |
31 | 18 | mulridd 7987 |
. . . . . 6
โข (๐ โ (1 ยท 1) =
1) |
32 | 30, 31 | oveq12d 5906 |
. . . . 5
โข (๐ โ (((๐ด ยท ๐ด) + (2 ยท (๐ด ยท 1))) + (1 ยท 1)) = (((๐ด ยท ๐ด) + (2 ยท ๐ด)) + 1)) |
33 | 27, 32 | eqtrd 2220 |
. . . 4
โข (๐ โ ((๐ด + 1) ยท (๐ด + 1)) = (((๐ด ยท ๐ด) + (2 ยท ๐ด)) + 1)) |
34 | 33 | breq1d 4025 |
. . 3
โข (๐ โ (((๐ด + 1) ยท (๐ด + 1)) โค (๐ถ ยท ๐ถ) โ (((๐ด ยท ๐ด) + (2 ยท ๐ด)) + 1) โค (๐ถ ยท ๐ถ))) |
35 | 16, 34 | bitr4d 191 |
. 2
โข (๐ โ (((๐ด ยท ๐ด) + (2 ยท ๐ด)) < (๐ถ ยท ๐ถ) โ ((๐ด + 1) ยท (๐ด + 1)) โค (๐ถ ยท ๐ถ))) |
36 | 6, 8, 35 | 3bitr4d 220 |
1
โข (๐ โ (๐ด < ๐ถ โ ((๐ด ยท ๐ด) + (2 ยท ๐ด)) < (๐ถ ยท ๐ถ))) |