Step | Hyp | Ref
| Expression |
1 | | lcmineqlem6.1 |
. . . . . 6
โข ๐น = โซ(0[,]1)((๐ฅโ(๐ โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ ๐))) d๐ฅ |
2 | | lcmineqlem6.2 |
. . . . . 6
โข (๐ โ ๐ โ โ) |
3 | | lcmineqlem6.3 |
. . . . . 6
โข (๐ โ ๐ โ โ) |
4 | | lcmineqlem6.4 |
. . . . . 6
โข (๐ โ ๐ โค ๐) |
5 | 1, 2, 3, 4 | lcmineqlem3 40517 |
. . . . 5
โข (๐ โ ๐น = ฮฃ๐ โ (0...(๐ โ ๐))(((-1โ๐) ยท ((๐ โ ๐)C๐)) ยท (1 / (๐ + ๐)))) |
6 | 5 | oveq2d 7378 |
. . . 4
โข (๐ โ
((lcmโ(1...๐))
ยท ๐น) =
((lcmโ(1...๐))
ยท ฮฃ๐ โ
(0...(๐ โ ๐))(((-1โ๐) ยท ((๐ โ ๐)C๐)) ยท (1 / (๐ + ๐))))) |
7 | | fzfid 13885 |
. . . . 5
โข (๐ โ (0...(๐ โ ๐)) โ Fin) |
8 | | fz1ssnn 13479 |
. . . . . . . . 9
โข
(1...๐) โ
โ |
9 | | fzfi 13884 |
. . . . . . . . 9
โข
(1...๐) โ
Fin |
10 | 8, 9 | pm3.2i 472 |
. . . . . . . 8
โข
((1...๐) โ
โ โง (1...๐)
โ Fin) |
11 | | lcmfnncl 16512 |
. . . . . . . 8
โข
(((1...๐) โ
โ โง (1...๐)
โ Fin) โ (lcmโ(1...๐)) โ โ) |
12 | 10, 11 | ax-mp 5 |
. . . . . . 7
โข
(lcmโ(1...๐)) โ โ |
13 | 12 | nncni 12170 |
. . . . . 6
โข
(lcmโ(1...๐)) โ โ |
14 | 13 | a1i 11 |
. . . . 5
โข (๐ โ
(lcmโ(1...๐))
โ โ) |
15 | | elfzelz 13448 |
. . . . . . . . . 10
โข (๐ โ (0...(๐ โ ๐)) โ ๐ โ โค) |
16 | | m1expcl 13999 |
. . . . . . . . . 10
โข (๐ โ โค โ
(-1โ๐) โ
โค) |
17 | 15, 16 | syl 17 |
. . . . . . . . 9
โข (๐ โ (0...(๐ โ ๐)) โ (-1โ๐) โ โค) |
18 | 17 | zcnd 12615 |
. . . . . . . 8
โข (๐ โ (0...(๐ โ ๐)) โ (-1โ๐) โ โ) |
19 | 18 | adantl 483 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ (-1โ๐) โ โ) |
20 | | bccl2 14230 |
. . . . . . . . 9
โข (๐ โ (0...(๐ โ ๐)) โ ((๐ โ ๐)C๐) โ โ) |
21 | 20 | nncnd 12176 |
. . . . . . . 8
โข (๐ โ (0...(๐ โ ๐)) โ ((๐ โ ๐)C๐) โ โ) |
22 | 21 | adantl 483 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ ((๐ โ ๐)C๐) โ โ) |
23 | 19, 22 | mulcld 11182 |
. . . . . 6
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ ((-1โ๐) ยท ((๐ โ ๐)C๐)) โ โ) |
24 | 3 | nncnd 12176 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
25 | 24 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ ๐ โ โ) |
26 | 15 | zcnd 12615 |
. . . . . . . . 9
โข (๐ โ (0...(๐ โ ๐)) โ ๐ โ โ) |
27 | 26 | adantl 483 |
. . . . . . . 8
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ ๐ โ โ) |
28 | 25, 27 | addcld 11181 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ (๐ + ๐) โ โ) |
29 | | elfznn0 13541 |
. . . . . . . . . 10
โข (๐ โ (0...(๐ โ ๐)) โ ๐ โ โ0) |
30 | | nnnn0addcl 12450 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐ + ๐) โ
โ) |
31 | 29, 30 | sylan2 594 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ (0...(๐ โ ๐))) โ (๐ + ๐) โ โ) |
32 | 3, 31 | sylan 581 |
. . . . . . . 8
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ (๐ + ๐) โ โ) |
33 | 32 | nnne0d 12210 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ (๐ + ๐) โ 0) |
34 | 28, 33 | reccld 11931 |
. . . . . 6
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ (1 / (๐ + ๐)) โ โ) |
35 | 23, 34 | mulcld 11182 |
. . . . 5
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ (((-1โ๐) ยท ((๐ โ ๐)C๐)) ยท (1 / (๐ + ๐))) โ โ) |
36 | 7, 14, 35 | fsummulc2 15676 |
. . . 4
โข (๐ โ
((lcmโ(1...๐))
ยท ฮฃ๐ โ
(0...(๐ โ ๐))(((-1โ๐) ยท ((๐ โ ๐)C๐)) ยท (1 / (๐ + ๐)))) = ฮฃ๐ โ (0...(๐ โ ๐))((lcmโ(1...๐)) ยท (((-1โ๐) ยท ((๐ โ ๐)C๐)) ยท (1 / (๐ + ๐))))) |
37 | 6, 36 | eqtrd 2777 |
. . 3
โข (๐ โ
((lcmโ(1...๐))
ยท ๐น) = ฮฃ๐ โ (0...(๐ โ ๐))((lcmโ(1...๐)) ยท (((-1โ๐) ยท ((๐ โ ๐)C๐)) ยท (1 / (๐ + ๐))))) |
38 | 13 | a1i 11 |
. . . . 5
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ (lcmโ(1...๐)) โ
โ) |
39 | 38, 23, 28, 33 | lcmineqlem5 40519 |
. . . 4
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ ((lcmโ(1...๐)) ยท (((-1โ๐) ยท ((๐ โ ๐)C๐)) ยท (1 / (๐ + ๐)))) = (((-1โ๐) ยท ((๐ โ ๐)C๐)) ยท ((lcmโ(1...๐)) / (๐ + ๐)))) |
40 | 39 | sumeq2dv 15595 |
. . 3
โข (๐ โ ฮฃ๐ โ (0...(๐ โ ๐))((lcmโ(1...๐)) ยท (((-1โ๐) ยท ((๐ โ ๐)C๐)) ยท (1 / (๐ + ๐)))) = ฮฃ๐ โ (0...(๐ โ ๐))(((-1โ๐) ยท ((๐ โ ๐)C๐)) ยท ((lcmโ(1...๐)) / (๐ + ๐)))) |
41 | 37, 40 | eqtrd 2777 |
. 2
โข (๐ โ
((lcmโ(1...๐))
ยท ๐น) = ฮฃ๐ โ (0...(๐ โ ๐))(((-1โ๐) ยท ((๐ โ ๐)C๐)) ยท ((lcmโ(1...๐)) / (๐ + ๐)))) |
42 | 17 | adantl 483 |
. . . . 5
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ (-1โ๐) โ โค) |
43 | 20 | nnzd 12533 |
. . . . . 6
โข (๐ โ (0...(๐ โ ๐)) โ ((๐ โ ๐)C๐) โ โค) |
44 | 43 | adantl 483 |
. . . . 5
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ ((๐ โ ๐)C๐) โ โค) |
45 | 42, 44 | zmulcld 12620 |
. . . 4
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ ((-1โ๐) ยท ((๐ โ ๐)C๐)) โ โค) |
46 | 2 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ ๐ โ โ) |
47 | 3 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ ๐ โ โ) |
48 | 4 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ ๐ โค ๐) |
49 | | simpr 486 |
. . . . 5
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ ๐ โ (0...(๐ โ ๐))) |
50 | 46, 47, 48, 49 | lcmineqlem4 40518 |
. . . 4
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ ((lcmโ(1...๐)) / (๐ + ๐)) โ โค) |
51 | 45, 50 | zmulcld 12620 |
. . 3
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ (((-1โ๐) ยท ((๐ โ ๐)C๐)) ยท ((lcmโ(1...๐)) / (๐ + ๐))) โ โค) |
52 | 7, 51 | fsumzcl 15627 |
. 2
โข (๐ โ ฮฃ๐ โ (0...(๐ โ ๐))(((-1โ๐) ยท ((๐ โ ๐)C๐)) ยท ((lcmโ(1...๐)) / (๐ + ๐))) โ โค) |
53 | 41, 52 | eqeltrd 2838 |
1
โข (๐ โ
((lcmโ(1...๐))
ยท ๐น) โ
โค) |