Step | Hyp | Ref
| Expression |
1 | | 2re 12234 |
. . . . 5
โข 2 โ
โ |
2 | 1 | a1i 11 |
. . . 4
โข (๐ โ 2 โ
โ) |
3 | | 2nn0 12437 |
. . . . . . 7
โข 2 โ
โ0 |
4 | 3 | a1i 11 |
. . . . . 6
โข (๐ โ 2 โ
โ0) |
5 | | lcmineqlem22.1 |
. . . . . . 7
โข (๐ โ ๐ โ โ) |
6 | 5 | nnnn0d 12480 |
. . . . . 6
โข (๐ โ ๐ โ
โ0) |
7 | 4, 6 | nn0mulcld 12485 |
. . . . 5
โข (๐ โ (2 ยท ๐) โ
โ0) |
8 | | 1nn0 12436 |
. . . . . 6
โข 1 โ
โ0 |
9 | 8 | a1i 11 |
. . . . 5
โข (๐ โ 1 โ
โ0) |
10 | 7, 9 | nn0addcld 12484 |
. . . 4
โข (๐ โ ((2 ยท ๐) + 1) โ
โ0) |
11 | 2, 10 | reexpcld 14075 |
. . 3
โข (๐ โ (2โ((2 ยท ๐) + 1)) โ
โ) |
12 | 7, 4 | nn0addcld 12484 |
. . . 4
โข (๐ โ ((2 ยท ๐) + 2) โ
โ0) |
13 | 2, 12 | reexpcld 14075 |
. . 3
โข (๐ โ (2โ((2 ยท ๐) + 2)) โ
โ) |
14 | | fz1ssnn 13479 |
. . . . . 6
โข (1...((2
ยท ๐) + 1)) โ
โ |
15 | | fzfi 13884 |
. . . . . 6
โข (1...((2
ยท ๐) + 1)) โ
Fin |
16 | | lcmfnncl 16512 |
. . . . . 6
โข
(((1...((2 ยท ๐) + 1)) โ โ โง (1...((2
ยท ๐) + 1)) โ
Fin) โ (lcmโ(1...((2 ยท ๐) + 1))) โ โ) |
17 | 14, 15, 16 | mp2an 691 |
. . . . 5
โข
(lcmโ(1...((2 ยท ๐) + 1))) โ โ |
18 | 17 | a1i 11 |
. . . 4
โข (๐ โ (lcmโ(1...((2
ยท ๐) + 1))) โ
โ) |
19 | 18 | nnred 12175 |
. . 3
โข (๐ โ (lcmโ(1...((2
ยท ๐) + 1))) โ
โ) |
20 | | 1red 11163 |
. . . . 5
โข (๐ โ 1 โ
โ) |
21 | 5 | nnred 12175 |
. . . . . 6
โข (๐ โ ๐ โ โ) |
22 | 2, 21 | remulcld 11192 |
. . . . 5
โข (๐ โ (2 ยท ๐) โ
โ) |
23 | | 1lt2 12331 |
. . . . . . 7
โข 1 <
2 |
24 | 23 | a1i 11 |
. . . . . 6
โข (๐ โ 1 < 2) |
25 | 20, 2, 24 | ltled 11310 |
. . . . 5
โข (๐ โ 1 โค 2) |
26 | 20, 2, 22, 25 | leadd2dd 11777 |
. . . 4
โข (๐ โ ((2 ยท ๐) + 1) โค ((2 ยท ๐) + 2)) |
27 | | 2z 12542 |
. . . . . . . 8
โข 2 โ
โค |
28 | 27 | a1i 11 |
. . . . . . 7
โข (๐ โ 2 โ
โค) |
29 | 5 | nnzd 12533 |
. . . . . . 7
โข (๐ โ ๐ โ โค) |
30 | 28, 29 | zmulcld 12620 |
. . . . . 6
โข (๐ โ (2 ยท ๐) โ
โค) |
31 | 30 | peano2zd 12617 |
. . . . 5
โข (๐ โ ((2 ยท ๐) + 1) โ
โค) |
32 | 30, 28 | zaddcld 12618 |
. . . . 5
โข (๐ โ ((2 ยท ๐) + 2) โ
โค) |
33 | 2, 31, 32, 24 | leexp2d 14162 |
. . . 4
โข (๐ โ (((2 ยท ๐) + 1) โค ((2 ยท ๐) + 2) โ (2โ((2
ยท ๐) + 1)) โค
(2โ((2 ยท ๐) +
2)))) |
34 | 26, 33 | mpbid 231 |
. . 3
โข (๐ โ (2โ((2 ยท ๐) + 1)) โค (2โ((2
ยท ๐) +
2))) |
35 | | lcmineqlem22.2 |
. . . 4
โข (๐ โ 4 โค ๐) |
36 | 5, 35 | lcmineqlem21 40535 |
. . 3
โข (๐ โ (2โ((2 ยท ๐) + 2)) โค
(lcmโ(1...((2 ยท ๐) + 1)))) |
37 | 11, 13, 19, 34, 36 | letrd 11319 |
. 2
โข (๐ โ (2โ((2 ยท ๐) + 1)) โค
(lcmโ(1...((2 ยท ๐) + 1)))) |
38 | | fz1ssnn 13479 |
. . . . . 6
โข (1...((2
ยท ๐) + 2)) โ
โ |
39 | | fzfi 13884 |
. . . . . 6
โข (1...((2
ยท ๐) + 2)) โ
Fin |
40 | | lcmfnncl 16512 |
. . . . . 6
โข
(((1...((2 ยท ๐) + 2)) โ โ โง (1...((2
ยท ๐) + 2)) โ
Fin) โ (lcmโ(1...((2 ยท ๐) + 2))) โ โ) |
41 | 38, 39, 40 | mp2an 691 |
. . . . 5
โข
(lcmโ(1...((2 ยท ๐) + 2))) โ โ |
42 | 41 | a1i 11 |
. . . 4
โข (๐ โ (lcmโ(1...((2
ยท ๐) + 2))) โ
โ) |
43 | 42 | nnred 12175 |
. . 3
โข (๐ โ (lcmโ(1...((2
ยท ๐) + 2))) โ
โ) |
44 | 18 | nnzd 12533 |
. . . . . . . 8
โข (๐ โ (lcmโ(1...((2
ยท ๐) + 1))) โ
โค) |
45 | 44, 32 | jca 513 |
. . . . . . 7
โข (๐ โ
((lcmโ(1...((2 ยท ๐) + 1))) โ โค โง ((2 ยท
๐) + 2) โ
โค)) |
46 | | dvdslcm 16481 |
. . . . . . 7
โข
(((lcmโ(1...((2 ยท ๐) + 1))) โ โค โง ((2 ยท
๐) + 2) โ โค)
โ ((lcmโ(1...((2 ยท ๐) + 1))) โฅ ((lcmโ(1...((2
ยท ๐) + 1))) lcm ((2
ยท ๐) + 2)) โง ((2
ยท ๐) + 2) โฅ
((lcmโ(1...((2 ยท ๐) + 1))) lcm ((2 ยท ๐) + 2)))) |
47 | 45, 46 | syl 17 |
. . . . . 6
โข (๐ โ
((lcmโ(1...((2 ยท ๐) + 1))) โฅ ((lcmโ(1...((2
ยท ๐) + 1))) lcm ((2
ยท ๐) + 2)) โง ((2
ยท ๐) + 2) โฅ
((lcmโ(1...((2 ยท ๐) + 1))) lcm ((2 ยท ๐) + 2)))) |
48 | 47 | simpld 496 |
. . . . 5
โข (๐ โ (lcmโ(1...((2
ยท ๐) + 1))) โฅ
((lcmโ(1...((2 ยท ๐) + 1))) lcm ((2 ยท ๐) + 2))) |
49 | | 2nn 12233 |
. . . . . . . . . 10
โข 2 โ
โ |
50 | 49 | a1i 11 |
. . . . . . . . 9
โข (๐ โ 2 โ
โ) |
51 | 50, 5 | nnmulcld 12213 |
. . . . . . . 8
โข (๐ โ (2 ยท ๐) โ
โ) |
52 | 51, 50 | nnaddcld 12212 |
. . . . . . 7
โข (๐ โ ((2 ยท ๐) + 2) โ
โ) |
53 | 52 | lcmfunnnd 40498 |
. . . . . 6
โข (๐ โ (lcmโ(1...((2
ยท ๐) + 2))) =
((lcmโ(1...(((2 ยท ๐) + 2) โ 1))) lcm ((2 ยท ๐) + 2))) |
54 | 22 | recnd 11190 |
. . . . . . . . . . 11
โข (๐ โ (2 ยท ๐) โ
โ) |
55 | 2 | recnd 11190 |
. . . . . . . . . . 11
โข (๐ โ 2 โ
โ) |
56 | | 1cnd 11157 |
. . . . . . . . . . 11
โข (๐ โ 1 โ
โ) |
57 | 54, 55, 56 | addsubassd 11539 |
. . . . . . . . . 10
โข (๐ โ (((2 ยท ๐) + 2) โ 1) = ((2 ยท
๐) + (2 โ
1))) |
58 | | 2m1e1 12286 |
. . . . . . . . . . 11
โข (2
โ 1) = 1 |
59 | 58 | oveq2i 7373 |
. . . . . . . . . 10
โข ((2
ยท ๐) + (2 โ
1)) = ((2 ยท ๐) +
1) |
60 | 57, 59 | eqtrdi 2793 |
. . . . . . . . 9
โข (๐ โ (((2 ยท ๐) + 2) โ 1) = ((2 ยท
๐) + 1)) |
61 | 60 | oveq2d 7378 |
. . . . . . . 8
โข (๐ โ (1...(((2 ยท ๐) + 2) โ 1)) = (1...((2
ยท ๐) +
1))) |
62 | 61 | fveq2d 6851 |
. . . . . . 7
โข (๐ โ
(lcmโ(1...(((2 ยท ๐) + 2) โ 1))) =
(lcmโ(1...((2 ยท ๐) + 1)))) |
63 | 62 | oveq1d 7377 |
. . . . . 6
โข (๐ โ
((lcmโ(1...(((2 ยท ๐) + 2) โ 1))) lcm ((2 ยท ๐) + 2)) =
((lcmโ(1...((2 ยท ๐) + 1))) lcm ((2 ยท ๐) + 2))) |
64 | 53, 63 | eqtrd 2777 |
. . . . 5
โข (๐ โ (lcmโ(1...((2
ยท ๐) + 2))) =
((lcmโ(1...((2 ยท ๐) + 1))) lcm ((2 ยท ๐) + 2))) |
65 | 48, 64 | breqtrrd 5138 |
. . . 4
โข (๐ โ (lcmโ(1...((2
ยท ๐) + 1))) โฅ
(lcmโ(1...((2 ยท ๐) + 2)))) |
66 | 44, 42 | jca 513 |
. . . . 5
โข (๐ โ
((lcmโ(1...((2 ยท ๐) + 1))) โ โค โง
(lcmโ(1...((2 ยท ๐) + 2))) โ โ)) |
67 | | dvdsle 16199 |
. . . . 5
โข
(((lcmโ(1...((2 ยท ๐) + 1))) โ โค โง
(lcmโ(1...((2 ยท ๐) + 2))) โ โ) โ
((lcmโ(1...((2 ยท ๐) + 1))) โฅ (lcmโ(1...((2
ยท ๐) + 2))) โ
(lcmโ(1...((2 ยท ๐) + 1))) โค (lcmโ(1...((2
ยท ๐) +
2))))) |
68 | 66, 67 | syl 17 |
. . . 4
โข (๐ โ
((lcmโ(1...((2 ยท ๐) + 1))) โฅ (lcmโ(1...((2
ยท ๐) + 2))) โ
(lcmโ(1...((2 ยท ๐) + 1))) โค (lcmโ(1...((2
ยท ๐) +
2))))) |
69 | 65, 68 | mpd 15 |
. . 3
โข (๐ โ (lcmโ(1...((2
ยท ๐) + 1))) โค
(lcmโ(1...((2 ยท ๐) + 2)))) |
70 | 13, 19, 43, 36, 69 | letrd 11319 |
. 2
โข (๐ โ (2โ((2 ยท ๐) + 2)) โค
(lcmโ(1...((2 ยท ๐) + 2)))) |
71 | 37, 70 | jca 513 |
1
โข (๐ โ ((2โ((2 ยท
๐) + 1)) โค
(lcmโ(1...((2 ยท ๐) + 1))) โง (2โ((2 ยท ๐) + 2)) โค
(lcmโ(1...((2 ยท ๐) + 2))))) |