Step | Hyp | Ref
| Expression |
1 | | vdwlem3.b |
. . . . . 6
โข (๐ โ ๐ต โ (1...๐)) |
2 | | elfznn 13530 |
. . . . . 6
โข (๐ต โ (1...๐) โ ๐ต โ โ) |
3 | 1, 2 | syl 17 |
. . . . 5
โข (๐ โ ๐ต โ โ) |
4 | | vdwlem3.w |
. . . . . 6
โข (๐ โ ๐ โ โ) |
5 | | vdwlem3.a |
. . . . . . . . 9
โข (๐ โ ๐ด โ (1...๐)) |
6 | | elfznn 13530 |
. . . . . . . . 9
โข (๐ด โ (1...๐) โ ๐ด โ โ) |
7 | 5, 6 | syl 17 |
. . . . . . . 8
โข (๐ โ ๐ด โ โ) |
8 | | nnm1nn0 12513 |
. . . . . . . 8
โข (๐ด โ โ โ (๐ด โ 1) โ
โ0) |
9 | 7, 8 | syl 17 |
. . . . . . 7
โข (๐ โ (๐ด โ 1) โ
โ0) |
10 | | vdwlem3.v |
. . . . . . 7
โข (๐ โ ๐ โ โ) |
11 | | nn0nnaddcl 12503 |
. . . . . . 7
โข (((๐ด โ 1) โ
โ0 โง ๐
โ โ) โ ((๐ด
โ 1) + ๐) โ
โ) |
12 | 9, 10, 11 | syl2anc 585 |
. . . . . 6
โข (๐ โ ((๐ด โ 1) + ๐) โ โ) |
13 | 4, 12 | nnmulcld 12265 |
. . . . 5
โข (๐ โ (๐ ยท ((๐ด โ 1) + ๐)) โ โ) |
14 | 3, 13 | nnaddcld 12264 |
. . . 4
โข (๐ โ (๐ต + (๐ ยท ((๐ด โ 1) + ๐))) โ โ) |
15 | 14 | nnred 12227 |
. . 3
โข (๐ โ (๐ต + (๐ ยท ((๐ด โ 1) + ๐))) โ โ) |
16 | 7, 10 | nnaddcld 12264 |
. . . . 5
โข (๐ โ (๐ด + ๐) โ โ) |
17 | 4, 16 | nnmulcld 12265 |
. . . 4
โข (๐ โ (๐ ยท (๐ด + ๐)) โ โ) |
18 | 17 | nnred 12227 |
. . 3
โข (๐ โ (๐ ยท (๐ด + ๐)) โ โ) |
19 | | 2nn 12285 |
. . . . . 6
โข 2 โ
โ |
20 | | nnmulcl 12236 |
. . . . . 6
โข ((2
โ โ โง ๐
โ โ) โ (2 ยท ๐) โ โ) |
21 | 19, 10, 20 | sylancr 588 |
. . . . 5
โข (๐ โ (2 ยท ๐) โ
โ) |
22 | 4, 21 | nnmulcld 12265 |
. . . 4
โข (๐ โ (๐ ยท (2 ยท ๐)) โ โ) |
23 | 22 | nnred 12227 |
. . 3
โข (๐ โ (๐ ยท (2 ยท ๐)) โ โ) |
24 | | elfzle2 13505 |
. . . . . 6
โข (๐ต โ (1...๐) โ ๐ต โค ๐) |
25 | 1, 24 | syl 17 |
. . . . 5
โข (๐ โ ๐ต โค ๐) |
26 | | nnre 12219 |
. . . . . . 7
โข (๐ต โ โ โ ๐ต โ
โ) |
27 | | nnre 12219 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โ) |
28 | | nnre 12219 |
. . . . . . 7
โข ((๐ ยท ((๐ด โ 1) + ๐)) โ โ โ (๐ ยท ((๐ด โ 1) + ๐)) โ โ) |
29 | | leadd1 11682 |
. . . . . . 7
โข ((๐ต โ โ โง ๐ โ โ โง (๐ ยท ((๐ด โ 1) + ๐)) โ โ) โ (๐ต โค ๐ โ (๐ต + (๐ ยท ((๐ด โ 1) + ๐))) โค (๐ + (๐ ยท ((๐ด โ 1) + ๐))))) |
30 | 26, 27, 28, 29 | syl3an 1161 |
. . . . . 6
โข ((๐ต โ โ โง ๐ โ โ โง (๐ ยท ((๐ด โ 1) + ๐)) โ โ) โ (๐ต โค ๐ โ (๐ต + (๐ ยท ((๐ด โ 1) + ๐))) โค (๐ + (๐ ยท ((๐ด โ 1) + ๐))))) |
31 | 3, 4, 13, 30 | syl3anc 1372 |
. . . . 5
โข (๐ โ (๐ต โค ๐ โ (๐ต + (๐ ยท ((๐ด โ 1) + ๐))) โค (๐ + (๐ ยท ((๐ด โ 1) + ๐))))) |
32 | 25, 31 | mpbid 231 |
. . . 4
โข (๐ โ (๐ต + (๐ ยท ((๐ด โ 1) + ๐))) โค (๐ + (๐ ยท ((๐ด โ 1) + ๐)))) |
33 | 4 | nncnd 12228 |
. . . . . 6
โข (๐ โ ๐ โ โ) |
34 | | 1cnd 11209 |
. . . . . 6
โข (๐ โ 1 โ
โ) |
35 | 12 | nncnd 12228 |
. . . . . 6
โข (๐ โ ((๐ด โ 1) + ๐) โ โ) |
36 | 33, 34, 35 | adddid 11238 |
. . . . 5
โข (๐ โ (๐ ยท (1 + ((๐ด โ 1) + ๐))) = ((๐ ยท 1) + (๐ ยท ((๐ด โ 1) + ๐)))) |
37 | 9 | nn0cnd 12534 |
. . . . . . . 8
โข (๐ โ (๐ด โ 1) โ โ) |
38 | 10 | nncnd 12228 |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
39 | 34, 37, 38 | addassd 11236 |
. . . . . . 7
โข (๐ โ ((1 + (๐ด โ 1)) + ๐) = (1 + ((๐ด โ 1) + ๐))) |
40 | | ax-1cn 11168 |
. . . . . . . . 9
โข 1 โ
โ |
41 | 7 | nncnd 12228 |
. . . . . . . . 9
โข (๐ โ ๐ด โ โ) |
42 | | pncan3 11468 |
. . . . . . . . 9
โข ((1
โ โ โง ๐ด
โ โ) โ (1 + (๐ด โ 1)) = ๐ด) |
43 | 40, 41, 42 | sylancr 588 |
. . . . . . . 8
โข (๐ โ (1 + (๐ด โ 1)) = ๐ด) |
44 | 43 | oveq1d 7424 |
. . . . . . 7
โข (๐ โ ((1 + (๐ด โ 1)) + ๐) = (๐ด + ๐)) |
45 | 39, 44 | eqtr3d 2775 |
. . . . . 6
โข (๐ โ (1 + ((๐ด โ 1) + ๐)) = (๐ด + ๐)) |
46 | 45 | oveq2d 7425 |
. . . . 5
โข (๐ โ (๐ ยท (1 + ((๐ด โ 1) + ๐))) = (๐ ยท (๐ด + ๐))) |
47 | 33 | mulridd 11231 |
. . . . . 6
โข (๐ โ (๐ ยท 1) = ๐) |
48 | 47 | oveq1d 7424 |
. . . . 5
โข (๐ โ ((๐ ยท 1) + (๐ ยท ((๐ด โ 1) + ๐))) = (๐ + (๐ ยท ((๐ด โ 1) + ๐)))) |
49 | 36, 46, 48 | 3eqtr3d 2781 |
. . . 4
โข (๐ โ (๐ ยท (๐ด + ๐)) = (๐ + (๐ ยท ((๐ด โ 1) + ๐)))) |
50 | 32, 49 | breqtrrd 5177 |
. . 3
โข (๐ โ (๐ต + (๐ ยท ((๐ด โ 1) + ๐))) โค (๐ ยท (๐ด + ๐))) |
51 | 7 | nnred 12227 |
. . . . . 6
โข (๐ โ ๐ด โ โ) |
52 | 10 | nnred 12227 |
. . . . . 6
โข (๐ โ ๐ โ โ) |
53 | | elfzle2 13505 |
. . . . . . 7
โข (๐ด โ (1...๐) โ ๐ด โค ๐) |
54 | 5, 53 | syl 17 |
. . . . . 6
โข (๐ โ ๐ด โค ๐) |
55 | 51, 52, 52, 54 | leadd1dd 11828 |
. . . . 5
โข (๐ โ (๐ด + ๐) โค (๐ + ๐)) |
56 | 38 | 2timesd 12455 |
. . . . 5
โข (๐ โ (2 ยท ๐) = (๐ + ๐)) |
57 | 55, 56 | breqtrrd 5177 |
. . . 4
โข (๐ โ (๐ด + ๐) โค (2 ยท ๐)) |
58 | 16 | nnred 12227 |
. . . . 5
โข (๐ โ (๐ด + ๐) โ โ) |
59 | 21 | nnred 12227 |
. . . . 5
โข (๐ โ (2 ยท ๐) โ
โ) |
60 | 4 | nnred 12227 |
. . . . 5
โข (๐ โ ๐ โ โ) |
61 | 4 | nngt0d 12261 |
. . . . 5
โข (๐ โ 0 < ๐) |
62 | | lemul2 12067 |
. . . . 5
โข (((๐ด + ๐) โ โ โง (2 ยท ๐) โ โ โง (๐ โ โ โง 0 <
๐)) โ ((๐ด + ๐) โค (2 ยท ๐) โ (๐ ยท (๐ด + ๐)) โค (๐ ยท (2 ยท ๐)))) |
63 | 58, 59, 60, 61, 62 | syl112anc 1375 |
. . . 4
โข (๐ โ ((๐ด + ๐) โค (2 ยท ๐) โ (๐ ยท (๐ด + ๐)) โค (๐ ยท (2 ยท ๐)))) |
64 | 57, 63 | mpbid 231 |
. . 3
โข (๐ โ (๐ ยท (๐ด + ๐)) โค (๐ ยท (2 ยท ๐))) |
65 | 15, 18, 23, 50, 64 | letrd 11371 |
. 2
โข (๐ โ (๐ต + (๐ ยท ((๐ด โ 1) + ๐))) โค (๐ ยท (2 ยท ๐))) |
66 | | nnuz 12865 |
. . . 4
โข โ =
(โคโฅโ1) |
67 | 14, 66 | eleqtrdi 2844 |
. . 3
โข (๐ โ (๐ต + (๐ ยท ((๐ด โ 1) + ๐))) โ
(โคโฅโ1)) |
68 | 22 | nnzd 12585 |
. . 3
โข (๐ โ (๐ ยท (2 ยท ๐)) โ โค) |
69 | | elfz5 13493 |
. . 3
โข (((๐ต + (๐ ยท ((๐ด โ 1) + ๐))) โ (โคโฅโ1)
โง (๐ ยท (2
ยท ๐)) โ
โค) โ ((๐ต +
(๐ ยท ((๐ด โ 1) + ๐))) โ (1...(๐ ยท (2 ยท ๐))) โ (๐ต + (๐ ยท ((๐ด โ 1) + ๐))) โค (๐ ยท (2 ยท ๐)))) |
70 | 67, 68, 69 | syl2anc 585 |
. 2
โข (๐ โ ((๐ต + (๐ ยท ((๐ด โ 1) + ๐))) โ (1...(๐ ยท (2 ยท ๐))) โ (๐ต + (๐ ยท ((๐ด โ 1) + ๐))) โค (๐ ยท (2 ยท ๐)))) |
71 | 65, 70 | mpbird 257 |
1
โข (๐ โ (๐ต + (๐ ยท ((๐ด โ 1) + ๐))) โ (1...(๐ ยท (2 ยท ๐)))) |