Step | Hyp | Ref
| Expression |
1 | | lcmineqlem1.1 |
. 2
โข ๐น = โซ(0[,]1)((๐ฅโ(๐ โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ ๐))) d๐ฅ |
2 | | elunitcn 13450 |
. . . . 5
โข (๐ฅ โ (0[,]1) โ ๐ฅ โ
โ) |
3 | | ax-1cn 11171 |
. . . . . . . . . 10
โข 1 โ
โ |
4 | | negsub 11513 |
. . . . . . . . . 10
โข ((1
โ โ โง ๐ฅ
โ โ) โ (1 + -๐ฅ) = (1 โ ๐ฅ)) |
5 | 3, 4 | mpan 687 |
. . . . . . . . 9
โข (๐ฅ โ โ โ (1 +
-๐ฅ) = (1 โ ๐ฅ)) |
6 | 5 | oveq1d 7427 |
. . . . . . . 8
โข (๐ฅ โ โ โ ((1 +
-๐ฅ)โ(๐ โ ๐)) = ((1 โ ๐ฅ)โ(๐ โ ๐))) |
7 | 6 | adantl 481 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ โ) โ ((1 + -๐ฅ)โ(๐ โ ๐)) = ((1 โ ๐ฅ)โ(๐ โ ๐))) |
8 | | negcl 11465 |
. . . . . . . . 9
โข (๐ฅ โ โ โ -๐ฅ โ
โ) |
9 | | 1cnd 11214 |
. . . . . . . . . 10
โข (๐ โ 1 โ
โ) |
10 | | lcmineqlem1.4 |
. . . . . . . . . . 11
โข (๐ โ ๐ โค ๐) |
11 | | lcmineqlem1.3 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ โ) |
12 | 11 | nnnn0d 12537 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ
โ0) |
13 | | lcmineqlem1.2 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ โ) |
14 | 13 | nnnn0d 12537 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ
โ0) |
15 | | nn0sub 12527 |
. . . . . . . . . . . 12
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐ โค ๐ โ (๐ โ ๐) โ
โ0)) |
16 | 12, 14, 15 | syl2anc 583 |
. . . . . . . . . . 11
โข (๐ โ (๐ โค ๐ โ (๐ โ ๐) โ
โ0)) |
17 | 10, 16 | mpbid 231 |
. . . . . . . . . 10
โข (๐ โ (๐ โ ๐) โ
โ0) |
18 | | binom 15781 |
. . . . . . . . . . . 12
โข ((1
โ โ โง -๐ฅ
โ โ โง (๐
โ ๐) โ
โ0) โ ((1 + -๐ฅ)โ(๐ โ ๐)) = ฮฃ๐ โ (0...(๐ โ ๐))(((๐ โ ๐)C๐) ยท ((1โ((๐ โ ๐) โ ๐)) ยท (-๐ฅโ๐)))) |
19 | 18 | 3com23 1125 |
. . . . . . . . . . 11
โข ((1
โ โ โง (๐
โ ๐) โ
โ0 โง -๐ฅ โ โ) โ ((1 + -๐ฅ)โ(๐ โ ๐)) = ฮฃ๐ โ (0...(๐ โ ๐))(((๐ โ ๐)C๐) ยท ((1โ((๐ โ ๐) โ ๐)) ยท (-๐ฅโ๐)))) |
20 | 19 | 3expia 1120 |
. . . . . . . . . 10
โข ((1
โ โ โง (๐
โ ๐) โ
โ0) โ (-๐ฅ โ โ โ ((1 + -๐ฅ)โ(๐ โ ๐)) = ฮฃ๐ โ (0...(๐ โ ๐))(((๐ โ ๐)C๐) ยท ((1โ((๐ โ ๐) โ ๐)) ยท (-๐ฅโ๐))))) |
21 | 9, 17, 20 | syl2anc 583 |
. . . . . . . . 9
โข (๐ โ (-๐ฅ โ โ โ ((1 + -๐ฅ)โ(๐ โ ๐)) = ฮฃ๐ โ (0...(๐ โ ๐))(((๐ โ ๐)C๐) ยท ((1โ((๐ โ ๐) โ ๐)) ยท (-๐ฅโ๐))))) |
22 | 8, 21 | syl5 34 |
. . . . . . . 8
โข (๐ โ (๐ฅ โ โ โ ((1 + -๐ฅ)โ(๐ โ ๐)) = ฮฃ๐ โ (0...(๐ โ ๐))(((๐ โ ๐)C๐) ยท ((1โ((๐ โ ๐) โ ๐)) ยท (-๐ฅโ๐))))) |
23 | 22 | imp 406 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ โ) โ ((1 + -๐ฅ)โ(๐ โ ๐)) = ฮฃ๐ โ (0...(๐ โ ๐))(((๐ โ ๐)C๐) ยท ((1โ((๐ โ ๐) โ ๐)) ยท (-๐ฅโ๐)))) |
24 | 7, 23 | eqtr3d 2773 |
. . . . . 6
โข ((๐ โง ๐ฅ โ โ) โ ((1 โ ๐ฅ)โ(๐ โ ๐)) = ฮฃ๐ โ (0...(๐ โ ๐))(((๐ โ ๐)C๐) ยท ((1โ((๐ โ ๐) โ ๐)) ยท (-๐ฅโ๐)))) |
25 | | elfzelz 13506 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (0...(๐ โ ๐)) โ ๐ โ โค) |
26 | 13 | nnzd 12590 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ ๐ โ โค) |
27 | 11 | nnzd 12590 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ ๐ โ โค) |
28 | | zsubcl 12609 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โ ๐) โ โค) |
29 | 26, 27, 28 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (๐ โ ๐) โ โค) |
30 | | zsubcl 12609 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โ ๐) โ โค โง ๐ โ โค) โ ((๐ โ ๐) โ ๐) โ โค) |
31 | 29, 30 | sylan 579 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ โ โค) โ ((๐ โ ๐) โ ๐) โ โค) |
32 | 25, 31 | sylan2 592 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ ((๐ โ ๐) โ ๐) โ โค) |
33 | | 1exp 14062 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โ ๐) โ ๐) โ โค โ (1โ((๐ โ ๐) โ ๐)) = 1) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ (1โ((๐ โ ๐) โ ๐)) = 1) |
35 | 34 | 3adant2 1130 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฅ โ โ โง ๐ โ (0...(๐ โ ๐))) โ (1โ((๐ โ ๐) โ ๐)) = 1) |
36 | 35 | oveq1d 7427 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ฅ โ โ โง ๐ โ (0...(๐ โ ๐))) โ ((1โ((๐ โ ๐) โ ๐)) ยท (-๐ฅโ๐)) = (1 ยท (-๐ฅโ๐))) |
37 | 8 | 3ad2ant2 1133 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ฅ โ โ โง ๐ โ (0...(๐ โ ๐))) โ -๐ฅ โ โ) |
38 | | elfznn0 13599 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (0...(๐ โ ๐)) โ ๐ โ โ0) |
39 | 38 | 3ad2ant3 1134 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ฅ โ โ โง ๐ โ (0...(๐ โ ๐))) โ ๐ โ โ0) |
40 | | expcl 14050 |
. . . . . . . . . . . . . . . 16
โข ((-๐ฅ โ โ โง ๐ โ โ0)
โ (-๐ฅโ๐) โ
โ) |
41 | 37, 39, 40 | syl2anc 583 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฅ โ โ โง ๐ โ (0...(๐ โ ๐))) โ (-๐ฅโ๐) โ โ) |
42 | 41 | mullidd 11237 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ฅ โ โ โง ๐ โ (0...(๐ โ ๐))) โ (1 ยท (-๐ฅโ๐)) = (-๐ฅโ๐)) |
43 | 36, 42 | eqtrd 2771 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ โ โง ๐ โ (0...(๐ โ ๐))) โ ((1โ((๐ โ ๐) โ ๐)) ยท (-๐ฅโ๐)) = (-๐ฅโ๐)) |
44 | | mulm1 11660 |
. . . . . . . . . . . . . . 15
โข (๐ฅ โ โ โ (-1
ยท ๐ฅ) = -๐ฅ) |
45 | 44 | oveq1d 7427 |
. . . . . . . . . . . . . 14
โข (๐ฅ โ โ โ ((-1
ยท ๐ฅ)โ๐) = (-๐ฅโ๐)) |
46 | 45 | 3ad2ant2 1133 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ โ โง ๐ โ (0...(๐ โ ๐))) โ ((-1 ยท ๐ฅ)โ๐) = (-๐ฅโ๐)) |
47 | 43, 46 | eqtr4d 2774 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ โ โง ๐ โ (0...(๐ โ ๐))) โ ((1โ((๐ โ ๐) โ ๐)) ยท (-๐ฅโ๐)) = ((-1 ยท ๐ฅ)โ๐)) |
48 | | neg1cn 12331 |
. . . . . . . . . . . . . . 15
โข -1 โ
โ |
49 | | mulexp 14072 |
. . . . . . . . . . . . . . 15
โข ((-1
โ โ โง ๐ฅ
โ โ โง ๐
โ โ0) โ ((-1 ยท ๐ฅ)โ๐) = ((-1โ๐) ยท (๐ฅโ๐))) |
50 | 48, 49 | mp3an1 1447 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ โ โง ๐ โ โ0)
โ ((-1 ยท ๐ฅ)โ๐) = ((-1โ๐) ยท (๐ฅโ๐))) |
51 | 38, 50 | sylan2 592 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โ โง ๐ โ (0...(๐ โ ๐))) โ ((-1 ยท ๐ฅ)โ๐) = ((-1โ๐) ยท (๐ฅโ๐))) |
52 | 51 | 3adant1 1129 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ โ โง ๐ โ (0...(๐ โ ๐))) โ ((-1 ยท ๐ฅ)โ๐) = ((-1โ๐) ยท (๐ฅโ๐))) |
53 | 47, 52 | eqtrd 2771 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ โ โง ๐ โ (0...(๐ โ ๐))) โ ((1โ((๐ โ ๐) โ ๐)) ยท (-๐ฅโ๐)) = ((-1โ๐) ยท (๐ฅโ๐))) |
54 | 53 | oveq2d 7428 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ โ โง ๐ โ (0...(๐ โ ๐))) โ (((๐ โ ๐)C๐) ยท ((1โ((๐ โ ๐) โ ๐)) ยท (-๐ฅโ๐))) = (((๐ โ ๐)C๐) ยท ((-1โ๐) ยท (๐ฅโ๐)))) |
55 | | bccl 14287 |
. . . . . . . . . . . . . 14
โข (((๐ โ ๐) โ โ0 โง ๐ โ โค) โ ((๐ โ ๐)C๐) โ
โ0) |
56 | 17, 25, 55 | syl2an 595 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (0...(๐ โ ๐))) โ ((๐ โ ๐)C๐) โ
โ0) |
57 | 56 | 3adant2 1130 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ โ โง ๐ โ (0...(๐ โ ๐))) โ ((๐ โ ๐)C๐) โ
โ0) |
58 | 57 | nn0cnd 12539 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ โ โง ๐ โ (0...(๐ โ ๐))) โ ((๐ โ ๐)C๐) โ โ) |
59 | | expcl 14050 |
. . . . . . . . . . . 12
โข ((-1
โ โ โง ๐
โ โ0) โ (-1โ๐) โ โ) |
60 | 48, 39, 59 | sylancr 586 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ โ โง ๐ โ (0...(๐ โ ๐))) โ (-1โ๐) โ โ) |
61 | | expcl 14050 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โ โง ๐ โ โ0)
โ (๐ฅโ๐) โ
โ) |
62 | 38, 61 | sylan2 592 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ โง ๐ โ (0...(๐ โ ๐))) โ (๐ฅโ๐) โ โ) |
63 | 62 | 3adant1 1129 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ โ โง ๐ โ (0...(๐ โ ๐))) โ (๐ฅโ๐) โ โ) |
64 | 58, 60, 63 | mulassd 11242 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ โ โง ๐ โ (0...(๐ โ ๐))) โ ((((๐ โ ๐)C๐) ยท (-1โ๐)) ยท (๐ฅโ๐)) = (((๐ โ ๐)C๐) ยท ((-1โ๐) ยท (๐ฅโ๐)))) |
65 | 54, 64 | eqtr4d 2774 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ โ โง ๐ โ (0...(๐ โ ๐))) โ (((๐ โ ๐)C๐) ยท ((1โ((๐ โ ๐) โ ๐)) ยท (-๐ฅโ๐))) = ((((๐ โ ๐)C๐) ยท (-1โ๐)) ยท (๐ฅโ๐))) |
66 | 58, 60 | mulcomd 11240 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ โ โง ๐ โ (0...(๐ โ ๐))) โ (((๐ โ ๐)C๐) ยท (-1โ๐)) = ((-1โ๐) ยท ((๐ โ ๐)C๐))) |
67 | 66 | oveq1d 7427 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ โ โง ๐ โ (0...(๐ โ ๐))) โ ((((๐ โ ๐)C๐) ยท (-1โ๐)) ยท (๐ฅโ๐)) = (((-1โ๐) ยท ((๐ โ ๐)C๐)) ยท (๐ฅโ๐))) |
68 | 65, 67 | eqtrd 2771 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ โ โง ๐ โ (0...(๐ โ ๐))) โ (((๐ โ ๐)C๐) ยท ((1โ((๐ โ ๐) โ ๐)) ยท (-๐ฅโ๐))) = (((-1โ๐) ยท ((๐ โ ๐)C๐)) ยท (๐ฅโ๐))) |
69 | 68 | 3expa 1117 |
. . . . . . 7
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ (0...(๐ โ ๐))) โ (((๐ โ ๐)C๐) ยท ((1โ((๐ โ ๐) โ ๐)) ยท (-๐ฅโ๐))) = (((-1โ๐) ยท ((๐ โ ๐)C๐)) ยท (๐ฅโ๐))) |
70 | 69 | sumeq2dv 15654 |
. . . . . 6
โข ((๐ โง ๐ฅ โ โ) โ ฮฃ๐ โ (0...(๐ โ ๐))(((๐ โ ๐)C๐) ยท ((1โ((๐ โ ๐) โ ๐)) ยท (-๐ฅโ๐))) = ฮฃ๐ โ (0...(๐ โ ๐))(((-1โ๐) ยท ((๐ โ ๐)C๐)) ยท (๐ฅโ๐))) |
71 | 24, 70 | eqtrd 2771 |
. . . . 5
โข ((๐ โง ๐ฅ โ โ) โ ((1 โ ๐ฅ)โ(๐ โ ๐)) = ฮฃ๐ โ (0...(๐ โ ๐))(((-1โ๐) ยท ((๐ โ ๐)C๐)) ยท (๐ฅโ๐))) |
72 | 2, 71 | sylan2 592 |
. . . 4
โข ((๐ โง ๐ฅ โ (0[,]1)) โ ((1 โ ๐ฅ)โ(๐ โ ๐)) = ฮฃ๐ โ (0...(๐ โ ๐))(((-1โ๐) ยท ((๐ โ ๐)C๐)) ยท (๐ฅโ๐))) |
73 | 72 | oveq2d 7428 |
. . 3
โข ((๐ โง ๐ฅ โ (0[,]1)) โ ((๐ฅโ(๐ โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ ๐))) = ((๐ฅโ(๐ โ 1)) ยท ฮฃ๐ โ (0...(๐ โ ๐))(((-1โ๐) ยท ((๐ โ ๐)C๐)) ยท (๐ฅโ๐)))) |
74 | 73 | itgeq2dv 25532 |
. 2
โข (๐ โ โซ(0[,]1)((๐ฅโ(๐ โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ ๐))) d๐ฅ = โซ(0[,]1)((๐ฅโ(๐ โ 1)) ยท ฮฃ๐ โ (0...(๐ โ ๐))(((-1โ๐) ยท ((๐ โ ๐)C๐)) ยท (๐ฅโ๐))) d๐ฅ) |
75 | 1, 74 | eqtrid 2783 |
1
โข (๐ โ ๐น = โซ(0[,]1)((๐ฅโ(๐ โ 1)) ยท ฮฃ๐ โ (0...(๐ โ ๐))(((-1โ๐) ยท ((๐ โ ๐)C๐)) ยท (๐ฅโ๐))) d๐ฅ) |