Step | Hyp | Ref
| Expression |
1 | | lcmineqlem3.1 |
. . 3
โข ๐น = โซ(0[,]1)((๐ฅโ(๐ โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ ๐))) d๐ฅ |
2 | | lcmineqlem3.2 |
. . 3
โข (๐ โ ๐ โ โ) |
3 | | lcmineqlem3.3 |
. . 3
โข (๐ โ ๐ โ โ) |
4 | | lcmineqlem3.4 |
. . 3
โข (๐ โ ๐ โค ๐) |
5 | 1, 2, 3, 4 | lcmineqlem2 40516 |
. 2
โข (๐ โ ๐น = ฮฃ๐ โ (0...(๐ โ ๐))(((-1โ๐) ยท ((๐ โ ๐)C๐)) ยท โซ(0[,]1)((๐ฅโ(๐ โ 1)) ยท (๐ฅโ๐)) d๐ฅ)) |
6 | | elunitcn 13392 |
. . . . . . . 8
โข (๐ฅ โ (0[,]1) โ ๐ฅ โ
โ) |
7 | 6 | 3ad2ant3 1136 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...(๐ โ ๐)) โง ๐ฅ โ (0[,]1)) โ ๐ฅ โ โ) |
8 | | elfznn0 13541 |
. . . . . . . 8
โข (๐ โ (0...(๐ โ ๐)) โ ๐ โ โ0) |
9 | 8 | 3ad2ant2 1135 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...(๐ โ ๐)) โง ๐ฅ โ (0[,]1)) โ ๐ โ โ0) |
10 | | nnm1nn0 12461 |
. . . . . . . . 9
โข (๐ โ โ โ (๐ โ 1) โ
โ0) |
11 | 3, 10 | syl 17 |
. . . . . . . 8
โข (๐ โ (๐ โ 1) โ
โ0) |
12 | 11 | 3ad2ant1 1134 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...(๐ โ ๐)) โง ๐ฅ โ (0[,]1)) โ (๐ โ 1) โ
โ0) |
13 | 7, 9, 12 | expaddd 14060 |
. . . . . 6
โข ((๐ โง ๐ โ (0...(๐ โ ๐)) โง ๐ฅ โ (0[,]1)) โ (๐ฅโ((๐ โ 1) + ๐)) = ((๐ฅโ(๐ โ 1)) ยท (๐ฅโ๐))) |
14 | 13 | 3expa 1119 |
. . . . 5
โข (((๐ โง ๐ โ (0...(๐ โ ๐))) โง ๐ฅ โ (0[,]1)) โ (๐ฅโ((๐ โ 1) + ๐)) = ((๐ฅโ(๐ โ 1)) ยท (๐ฅโ๐))) |
15 | 14 | itgeq2dv 25162 |
. . . 4
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ โซ(0[,]1)(๐ฅโ((๐ โ 1) + ๐)) d๐ฅ = โซ(0[,]1)((๐ฅโ(๐ โ 1)) ยท (๐ฅโ๐)) d๐ฅ) |
16 | 15 | oveq2d 7378 |
. . 3
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ (((-1โ๐) ยท ((๐ โ ๐)C๐)) ยท โซ(0[,]1)(๐ฅโ((๐ โ 1) + ๐)) d๐ฅ) = (((-1โ๐) ยท ((๐ โ ๐)C๐)) ยท โซ(0[,]1)((๐ฅโ(๐ โ 1)) ยท (๐ฅโ๐)) d๐ฅ)) |
17 | 16 | sumeq2dv 15595 |
. 2
โข (๐ โ ฮฃ๐ โ (0...(๐ โ ๐))(((-1โ๐) ยท ((๐ โ ๐)C๐)) ยท โซ(0[,]1)(๐ฅโ((๐ โ 1) + ๐)) d๐ฅ) = ฮฃ๐ โ (0...(๐ โ ๐))(((-1โ๐) ยท ((๐ โ ๐)C๐)) ยท โซ(0[,]1)((๐ฅโ(๐ โ 1)) ยท (๐ฅโ๐)) d๐ฅ)) |
18 | | 0red 11165 |
. . . . . 6
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ 0 โ
โ) |
19 | | 1red 11163 |
. . . . . 6
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ 1 โ
โ) |
20 | | 0le1 11685 |
. . . . . . 7
โข 0 โค
1 |
21 | 20 | a1i 11 |
. . . . . 6
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ 0 โค 1) |
22 | 11 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ (๐ โ 1) โ
โ0) |
23 | 8 | adantl 483 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ ๐ โ โ0) |
24 | 22, 23 | nn0addcld 12484 |
. . . . . 6
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ ((๐ โ 1) + ๐) โ
โ0) |
25 | 18, 19, 21, 24 | itgpowd 25430 |
. . . . 5
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ โซ(0[,]1)(๐ฅโ((๐ โ 1) + ๐)) d๐ฅ = (((1โ(((๐ โ 1) + ๐) + 1)) โ (0โ(((๐ โ 1) + ๐) + 1))) / (((๐ โ 1) + ๐) + 1))) |
26 | 3 | nncnd 12176 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ โ) |
27 | 26 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ ๐ โ โ) |
28 | | 1cnd 11157 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ 1 โ
โ) |
29 | | nn0cn 12430 |
. . . . . . . . . . . . 13
โข (๐ โ โ0
โ ๐ โ
โ) |
30 | 8, 29 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ (0...(๐ โ ๐)) โ ๐ โ โ) |
31 | 30 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ ๐ โ โ) |
32 | 27, 28, 31 | nppcand 11544 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ (((๐ โ 1) + ๐) + 1) = (๐ + ๐)) |
33 | 32 | oveq2d 7378 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ (1โ(((๐ โ 1) + ๐) + 1)) = (1โ(๐ + ๐))) |
34 | 32 | oveq2d 7378 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ (0โ(((๐ โ 1) + ๐) + 1)) = (0โ(๐ + ๐))) |
35 | 33, 34 | oveq12d 7380 |
. . . . . . . 8
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ ((1โ(((๐ โ 1) + ๐) + 1)) โ (0โ(((๐ โ 1) + ๐) + 1))) = ((1โ(๐ + ๐)) โ (0โ(๐ + ๐)))) |
36 | 3 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ ๐ โ โ) |
37 | | nnnn0addcl 12450 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐ + ๐) โ
โ) |
38 | 36, 23, 37 | syl2anc 585 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ (๐ + ๐) โ โ) |
39 | 38 | nnzd 12533 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ (๐ + ๐) โ โค) |
40 | | 1exp 14004 |
. . . . . . . . . 10
โข ((๐ + ๐) โ โค โ (1โ(๐ + ๐)) = 1) |
41 | 39, 40 | syl 17 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ (1โ(๐ + ๐)) = 1) |
42 | | 0exp 14010 |
. . . . . . . . . 10
โข ((๐ + ๐) โ โ โ (0โ(๐ + ๐)) = 0) |
43 | 38, 42 | syl 17 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ (0โ(๐ + ๐)) = 0) |
44 | 41, 43 | oveq12d 7380 |
. . . . . . . 8
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ ((1โ(๐ + ๐)) โ (0โ(๐ + ๐))) = (1 โ 0)) |
45 | 35, 44 | eqtrd 2777 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ ((1โ(((๐ โ 1) + ๐) + 1)) โ (0โ(((๐ โ 1) + ๐) + 1))) = (1 โ 0)) |
46 | | 1m0e1 12281 |
. . . . . . 7
โข (1
โ 0) = 1 |
47 | 45, 46 | eqtrdi 2793 |
. . . . . 6
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ ((1โ(((๐ โ 1) + ๐) + 1)) โ (0โ(((๐ โ 1) + ๐) + 1))) = 1) |
48 | 47, 32 | oveq12d 7380 |
. . . . 5
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ (((1โ(((๐ โ 1) + ๐) + 1)) โ (0โ(((๐ โ 1) + ๐) + 1))) / (((๐ โ 1) + ๐) + 1)) = (1 / (๐ + ๐))) |
49 | 25, 48 | eqtrd 2777 |
. . . 4
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ โซ(0[,]1)(๐ฅโ((๐ โ 1) + ๐)) d๐ฅ = (1 / (๐ + ๐))) |
50 | 49 | oveq2d 7378 |
. . 3
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ (((-1โ๐) ยท ((๐ โ ๐)C๐)) ยท โซ(0[,]1)(๐ฅโ((๐ โ 1) + ๐)) d๐ฅ) = (((-1โ๐) ยท ((๐ โ ๐)C๐)) ยท (1 / (๐ + ๐)))) |
51 | 50 | sumeq2dv 15595 |
. 2
โข (๐ โ ฮฃ๐ โ (0...(๐ โ ๐))(((-1โ๐) ยท ((๐ โ ๐)C๐)) ยท โซ(0[,]1)(๐ฅโ((๐ โ 1) + ๐)) d๐ฅ) = ฮฃ๐ โ (0...(๐ โ ๐))(((-1โ๐) ยท ((๐ โ ๐)C๐)) ยท (1 / (๐ + ๐)))) |
52 | 5, 17, 51 | 3eqtr2d 2783 |
1
โข (๐ โ ๐น = ฮฃ๐ โ (0...(๐ โ ๐))(((-1โ๐) ยท ((๐ โ ๐)C๐)) ยท (1 / (๐ + ๐)))) |