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 41425 |
. 2
โข (๐ โ ๐น = ฮฃ๐ โ (0...(๐ โ ๐))(((-1โ๐) ยท ((๐ โ ๐)C๐)) ยท โซ(0[,]1)((๐ฅโ(๐ โ 1)) ยท (๐ฅโ๐)) d๐ฅ)) |
6 | | elunitcn 13463 |
. . . . . . . 8
โข (๐ฅ โ (0[,]1) โ ๐ฅ โ
โ) |
7 | 6 | 3ad2ant3 1133 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...(๐ โ ๐)) โง ๐ฅ โ (0[,]1)) โ ๐ฅ โ โ) |
8 | | elfznn0 13612 |
. . . . . . . 8
โข (๐ โ (0...(๐ โ ๐)) โ ๐ โ โ0) |
9 | 8 | 3ad2ant2 1132 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...(๐ โ ๐)) โง ๐ฅ โ (0[,]1)) โ ๐ โ โ0) |
10 | | nnm1nn0 12529 |
. . . . . . . . 9
โข (๐ โ โ โ (๐ โ 1) โ
โ0) |
11 | 3, 10 | syl 17 |
. . . . . . . 8
โข (๐ โ (๐ โ 1) โ
โ0) |
12 | 11 | 3ad2ant1 1131 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...(๐ โ ๐)) โง ๐ฅ โ (0[,]1)) โ (๐ โ 1) โ
โ0) |
13 | 7, 9, 12 | expaddd 14130 |
. . . . . 6
โข ((๐ โง ๐ โ (0...(๐ โ ๐)) โง ๐ฅ โ (0[,]1)) โ (๐ฅโ((๐ โ 1) + ๐)) = ((๐ฅโ(๐ โ 1)) ยท (๐ฅโ๐))) |
14 | 13 | 3expa 1116 |
. . . . 5
โข (((๐ โง ๐ โ (0...(๐ โ ๐))) โง ๐ฅ โ (0[,]1)) โ (๐ฅโ((๐ โ 1) + ๐)) = ((๐ฅโ(๐ โ 1)) ยท (๐ฅโ๐))) |
15 | 14 | itgeq2dv 25685 |
. . . 4
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ โซ(0[,]1)(๐ฅโ((๐ โ 1) + ๐)) d๐ฅ = โซ(0[,]1)((๐ฅโ(๐ โ 1)) ยท (๐ฅโ๐)) d๐ฅ) |
16 | 15 | oveq2d 7430 |
. . 3
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ (((-1โ๐) ยท ((๐ โ ๐)C๐)) ยท โซ(0[,]1)(๐ฅโ((๐ โ 1) + ๐)) d๐ฅ) = (((-1โ๐) ยท ((๐ โ ๐)C๐)) ยท โซ(0[,]1)((๐ฅโ(๐ โ 1)) ยท (๐ฅโ๐)) d๐ฅ)) |
17 | 16 | sumeq2dv 15667 |
. 2
โข (๐ โ ฮฃ๐ โ (0...(๐ โ ๐))(((-1โ๐) ยท ((๐ โ ๐)C๐)) ยท โซ(0[,]1)(๐ฅโ((๐ โ 1) + ๐)) d๐ฅ) = ฮฃ๐ โ (0...(๐ โ ๐))(((-1โ๐) ยท ((๐ โ ๐)C๐)) ยท โซ(0[,]1)((๐ฅโ(๐ โ 1)) ยท (๐ฅโ๐)) d๐ฅ)) |
18 | | 0red 11233 |
. . . . . 6
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ 0 โ
โ) |
19 | | 1red 11231 |
. . . . . 6
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ 1 โ
โ) |
20 | | 0le1 11753 |
. . . . . . 7
โข 0 โค
1 |
21 | 20 | a1i 11 |
. . . . . 6
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ 0 โค 1) |
22 | 11 | adantr 480 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ (๐ โ 1) โ
โ0) |
23 | 8 | adantl 481 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ ๐ โ โ0) |
24 | 22, 23 | nn0addcld 12552 |
. . . . . 6
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ ((๐ โ 1) + ๐) โ
โ0) |
25 | 18, 19, 21, 24 | itgpowd 25959 |
. . . . 5
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ โซ(0[,]1)(๐ฅโ((๐ โ 1) + ๐)) d๐ฅ = (((1โ(((๐ โ 1) + ๐) + 1)) โ (0โ(((๐ โ 1) + ๐) + 1))) / (((๐ โ 1) + ๐) + 1))) |
26 | 3 | nncnd 12244 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ โ) |
27 | 26 | adantr 480 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ ๐ โ โ) |
28 | | 1cnd 11225 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ 1 โ
โ) |
29 | | nn0cn 12498 |
. . . . . . . . . . . . 13
โข (๐ โ โ0
โ ๐ โ
โ) |
30 | 8, 29 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ (0...(๐ โ ๐)) โ ๐ โ โ) |
31 | 30 | adantl 481 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ ๐ โ โ) |
32 | 27, 28, 31 | nppcand 11612 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ (((๐ โ 1) + ๐) + 1) = (๐ + ๐)) |
33 | 32 | oveq2d 7430 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ (1โ(((๐ โ 1) + ๐) + 1)) = (1โ(๐ + ๐))) |
34 | 32 | oveq2d 7430 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ (0โ(((๐ โ 1) + ๐) + 1)) = (0โ(๐ + ๐))) |
35 | 33, 34 | oveq12d 7432 |
. . . . . . . 8
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ ((1โ(((๐ โ 1) + ๐) + 1)) โ (0โ(((๐ โ 1) + ๐) + 1))) = ((1โ(๐ + ๐)) โ (0โ(๐ + ๐)))) |
36 | 3 | adantr 480 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ ๐ โ โ) |
37 | | nnnn0addcl 12518 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐ + ๐) โ
โ) |
38 | 36, 23, 37 | syl2anc 583 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ (๐ + ๐) โ โ) |
39 | 38 | nnzd 12601 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ (๐ + ๐) โ โค) |
40 | | 1exp 14074 |
. . . . . . . . . 10
โข ((๐ + ๐) โ โค โ (1โ(๐ + ๐)) = 1) |
41 | 39, 40 | syl 17 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ (1โ(๐ + ๐)) = 1) |
42 | | 0exp 14080 |
. . . . . . . . . 10
โข ((๐ + ๐) โ โ โ (0โ(๐ + ๐)) = 0) |
43 | 38, 42 | syl 17 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ (0โ(๐ + ๐)) = 0) |
44 | 41, 43 | oveq12d 7432 |
. . . . . . . 8
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ ((1โ(๐ + ๐)) โ (0โ(๐ + ๐))) = (1 โ 0)) |
45 | 35, 44 | eqtrd 2767 |
. . . . . . 7
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ ((1โ(((๐ โ 1) + ๐) + 1)) โ (0โ(((๐ โ 1) + ๐) + 1))) = (1 โ 0)) |
46 | | 1m0e1 12349 |
. . . . . . 7
โข (1
โ 0) = 1 |
47 | 45, 46 | eqtrdi 2783 |
. . . . . 6
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ ((1โ(((๐ โ 1) + ๐) + 1)) โ (0โ(((๐ โ 1) + ๐) + 1))) = 1) |
48 | 47, 32 | oveq12d 7432 |
. . . . 5
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ (((1โ(((๐ โ 1) + ๐) + 1)) โ (0โ(((๐ โ 1) + ๐) + 1))) / (((๐ โ 1) + ๐) + 1)) = (1 / (๐ + ๐))) |
49 | 25, 48 | eqtrd 2767 |
. . . 4
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ โซ(0[,]1)(๐ฅโ((๐ โ 1) + ๐)) d๐ฅ = (1 / (๐ + ๐))) |
50 | 49 | oveq2d 7430 |
. . 3
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ (((-1โ๐) ยท ((๐ โ ๐)C๐)) ยท โซ(0[,]1)(๐ฅโ((๐ โ 1) + ๐)) d๐ฅ) = (((-1โ๐) ยท ((๐ โ ๐)C๐)) ยท (1 / (๐ + ๐)))) |
51 | 50 | sumeq2dv 15667 |
. 2
โข (๐ โ ฮฃ๐ โ (0...(๐ โ ๐))(((-1โ๐) ยท ((๐ โ ๐)C๐)) ยท โซ(0[,]1)(๐ฅโ((๐ โ 1) + ๐)) d๐ฅ) = ฮฃ๐ โ (0...(๐ โ ๐))(((-1โ๐) ยท ((๐ โ ๐)C๐)) ยท (1 / (๐ + ๐)))) |
52 | 5, 17, 51 | 3eqtr2d 2773 |
1
โข (๐ โ ๐น = ฮฃ๐ โ (0...(๐ โ ๐))(((-1โ๐) ยท ((๐ โ ๐)C๐)) ยท (1 / (๐ + ๐)))) |