Step | Hyp | Ref
| Expression |
1 | | lcmineqlem19.1 |
. 2
โข (๐ โ ๐ โ โ) |
2 | | 2nn 12233 |
. . . . 5
โข 2 โ
โ |
3 | 2 | a1i 11 |
. . . 4
โข (๐ โ 2 โ
โ) |
4 | 3, 1 | nnmulcld 12213 |
. . 3
โข (๐ โ (2 ยท ๐) โ
โ) |
5 | 4 | peano2nnd 12177 |
. 2
โข (๐ โ ((2 ยท ๐) + 1) โ
โ) |
6 | 1 | nnnn0d 12480 |
. . 3
โข (๐ โ ๐ โ
โ0) |
7 | 1 | nnred 12175 |
. . . 4
โข (๐ โ ๐ โ โ) |
8 | | 2re 12234 |
. . . . 5
โข 2 โ
โ |
9 | 8 | a1i 11 |
. . . 4
โข (๐ โ 2 โ
โ) |
10 | 6 | nn0ge0d 12483 |
. . . 4
โข (๐ โ 0 โค ๐) |
11 | 3 | nnge1d 12208 |
. . . 4
โข (๐ โ 1 โค 2) |
12 | 7, 9, 10, 11 | lemulge12d 12100 |
. . 3
โข (๐ โ ๐ โค (2 ยท ๐)) |
13 | 4, 6, 12 | bccl2d 40478 |
. 2
โข (๐ โ ((2 ยท ๐)C๐) โ โ) |
14 | | fz1ssnn 13479 |
. . . 4
โข (1...(2
ยท ๐)) โ
โ |
15 | | fzfi 13884 |
. . . 4
โข (1...(2
ยท ๐)) โ
Fin |
16 | | lcmfnncl 16512 |
. . . 4
โข (((1...(2
ยท ๐)) โ
โ โง (1...(2 ยท ๐)) โ Fin) โ
(lcmโ(1...(2 ยท ๐))) โ โ) |
17 | 14, 15, 16 | mp2an 691 |
. . 3
โข
(lcmโ(1...(2 ยท ๐))) โ โ |
18 | 17 | a1i 11 |
. 2
โข (๐ โ (lcmโ(1...(2
ยท ๐))) โ
โ) |
19 | | fz1ssnn 13479 |
. . . 4
โข (1...((2
ยท ๐) + 1)) โ
โ |
20 | | fzfi 13884 |
. . . 4
โข (1...((2
ยท ๐) + 1)) โ
Fin |
21 | | lcmfnncl 16512 |
. . . 4
โข
(((1...((2 ยท ๐) + 1)) โ โ โง (1...((2
ยท ๐) + 1)) โ
Fin) โ (lcmโ(1...((2 ยท ๐) + 1))) โ โ) |
22 | 19, 20, 21 | mp2an 691 |
. . 3
โข
(lcmโ(1...((2 ยท ๐) + 1))) โ โ |
23 | 22 | a1i 11 |
. 2
โข (๐ โ (lcmโ(1...((2
ยท ๐) + 1))) โ
โ) |
24 | 1, 4, 12 | lcmineqlem16 40530 |
. 2
โข (๐ โ (๐ ยท ((2 ยท ๐)C๐)) โฅ (lcmโ(1...(2
ยท ๐)))) |
25 | 1 | lcmineqlem18 40532 |
. . 3
โข (๐ โ ((๐ + 1) ยท (((2 ยท ๐) + 1)C(๐ + 1))) = (((2 ยท ๐) + 1) ยท ((2 ยท ๐)C๐))) |
26 | 1 | peano2nnd 12177 |
. . . 4
โข (๐ โ (๐ + 1) โ โ) |
27 | 9, 7 | remulcld 11192 |
. . . . 5
โข (๐ โ (2 ยท ๐) โ
โ) |
28 | | 1red 11163 |
. . . . 5
โข (๐ โ 1 โ
โ) |
29 | 7, 27, 28, 12 | leadd1dd 11776 |
. . . 4
โข (๐ โ (๐ + 1) โค ((2 ยท ๐) + 1)) |
30 | 26, 5, 29 | lcmineqlem16 40530 |
. . 3
โข (๐ โ ((๐ + 1) ยท (((2 ยท ๐) + 1)C(๐ + 1))) โฅ (lcmโ(1...((2
ยท ๐) +
1)))) |
31 | 25, 30 | eqbrtrrd 5134 |
. 2
โข (๐ โ (((2 ยท ๐) + 1) ยท ((2 ยท
๐)C๐)) โฅ (lcmโ(1...((2
ยท ๐) +
1)))) |
32 | 18 | nnzd 12533 |
. . . . . 6
โข (๐ โ (lcmโ(1...(2
ยท ๐))) โ
โค) |
33 | 5 | nnzd 12533 |
. . . . . 6
โข (๐ โ ((2 ยท ๐) + 1) โ
โค) |
34 | 32, 33 | jca 513 |
. . . . 5
โข (๐ โ ((lcmโ(1...(2
ยท ๐))) โ
โค โง ((2 ยท ๐) + 1) โ โค)) |
35 | | dvdslcm 16481 |
. . . . 5
โข
(((lcmโ(1...(2 ยท ๐))) โ โค โง ((2 ยท ๐) + 1) โ โค) โ
((lcmโ(1...(2 ยท ๐))) โฅ ((lcmโ(1...(2
ยท ๐))) lcm ((2
ยท ๐) + 1)) โง ((2
ยท ๐) + 1) โฅ
((lcmโ(1...(2 ยท ๐))) lcm ((2 ยท ๐) + 1)))) |
36 | 34, 35 | syl 17 |
. . . 4
โข (๐ โ ((lcmโ(1...(2
ยท ๐))) โฅ
((lcmโ(1...(2 ยท ๐))) lcm ((2 ยท ๐) + 1)) โง ((2 ยท ๐) + 1) โฅ ((lcmโ(1...(2
ยท ๐))) lcm ((2
ยท ๐) +
1)))) |
37 | 36 | simpld 496 |
. . 3
โข (๐ โ (lcmโ(1...(2
ยท ๐))) โฅ
((lcmโ(1...(2 ยท ๐))) lcm ((2 ยท ๐) + 1))) |
38 | 5 | lcmfunnnd 40498 |
. . . 4
โข (๐ โ (lcmโ(1...((2
ยท ๐) + 1))) =
((lcmโ(1...(((2 ยท ๐) + 1) โ 1))) lcm ((2 ยท ๐) + 1))) |
39 | 27 | recnd 11190 |
. . . . . . . 8
โข (๐ โ (2 ยท ๐) โ
โ) |
40 | | 1cnd 11157 |
. . . . . . . 8
โข (๐ โ 1 โ
โ) |
41 | 39, 40 | pncand 11520 |
. . . . . . 7
โข (๐ โ (((2 ยท ๐) + 1) โ 1) = (2 ยท
๐)) |
42 | 41 | oveq2d 7378 |
. . . . . 6
โข (๐ โ (1...(((2 ยท ๐) + 1) โ 1)) = (1...(2
ยท ๐))) |
43 | 42 | fveq2d 6851 |
. . . . 5
โข (๐ โ
(lcmโ(1...(((2 ยท ๐) + 1) โ 1))) =
(lcmโ(1...(2 ยท ๐)))) |
44 | 43 | oveq1d 7377 |
. . . 4
โข (๐ โ
((lcmโ(1...(((2 ยท ๐) + 1) โ 1))) lcm ((2 ยท ๐) + 1)) =
((lcmโ(1...(2 ยท ๐))) lcm ((2 ยท ๐) + 1))) |
45 | 38, 44 | eqtrd 2777 |
. . 3
โข (๐ โ (lcmโ(1...((2
ยท ๐) + 1))) =
((lcmโ(1...(2 ยท ๐))) lcm ((2 ยท ๐) + 1))) |
46 | 37, 45 | breqtrrd 5138 |
. 2
โข (๐ โ (lcmโ(1...(2
ยท ๐))) โฅ
(lcmโ(1...((2 ยท ๐) + 1)))) |
47 | 1 | nnzd 12533 |
. . . . 5
โข (๐ โ ๐ โ โค) |
48 | | 2z 12542 |
. . . . . 6
โข 2 โ
โค |
49 | | 1z 12540 |
. . . . . 6
โข 1 โ
โค |
50 | | gcdaddm 16412 |
. . . . . 6
โข ((2
โ โค โง ๐
โ โค โง 1 โ โค) โ (๐ gcd 1) = (๐ gcd (1 + (2 ยท ๐)))) |
51 | 48, 49, 50 | mp3an13 1453 |
. . . . 5
โข (๐ โ โค โ (๐ gcd 1) = (๐ gcd (1 + (2 ยท ๐)))) |
52 | 47, 51 | syl 17 |
. . . 4
โข (๐ โ (๐ gcd 1) = (๐ gcd (1 + (2 ยท ๐)))) |
53 | 40, 39 | addcomd 11364 |
. . . . 5
โข (๐ โ (1 + (2 ยท ๐)) = ((2 ยท ๐) + 1)) |
54 | 53 | oveq2d 7378 |
. . . 4
โข (๐ โ (๐ gcd (1 + (2 ยท ๐))) = (๐ gcd ((2 ยท ๐) + 1))) |
55 | 52, 54 | eqtrd 2777 |
. . 3
โข (๐ โ (๐ gcd 1) = (๐ gcd ((2 ยท ๐) + 1))) |
56 | | gcd1 16415 |
. . . 4
โข (๐ โ โค โ (๐ gcd 1) = 1) |
57 | 47, 56 | syl 17 |
. . 3
โข (๐ โ (๐ gcd 1) = 1) |
58 | 55, 57 | eqtr3d 2779 |
. 2
โข (๐ โ (๐ gcd ((2 ยท ๐) + 1)) = 1) |
59 | 1, 5, 13, 18, 23, 24, 31, 46, 58 | lcmineqlem14 40528 |
1
โข (๐ โ ((๐ ยท ((2 ยท ๐) + 1)) ยท ((2 ยท ๐)C๐)) โฅ (lcmโ(1...((2
ยท ๐) +
1)))) |