Step | Hyp | Ref
| Expression |
1 | | lcmineqlem13.1 |
. 2
โข ๐น = โซ(0[,]1)((๐ฅโ(๐ โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ ๐))) d๐ฅ |
2 | | lcmineqlem13.2 |
. . . . 5
โข (๐ โ ๐ โ โ) |
3 | 2 | nnzd 12533 |
. . . 4
โข (๐ โ ๐ โ โค) |
4 | | nnge1 12188 |
. . . . 5
โข (๐ โ โ โ 1 โค
๐) |
5 | 2, 4 | syl 17 |
. . . 4
โข (๐ โ 1 โค ๐) |
6 | | lcmineqlem13.4 |
. . . 4
โข (๐ โ ๐ โค ๐) |
7 | 3, 5, 6 | 3jca 1129 |
. . 3
โข (๐ โ (๐ โ โค โง 1 โค ๐ โง ๐ โค ๐)) |
8 | | oveq1 7369 |
. . . . . . . . 9
โข (๐ = 1 โ (๐ โ 1) = (1 โ 1)) |
9 | 8 | oveq2d 7378 |
. . . . . . . 8
โข (๐ = 1 โ (๐ฅโ(๐ โ 1)) = (๐ฅโ(1 โ 1))) |
10 | | oveq2 7370 |
. . . . . . . . 9
โข (๐ = 1 โ (๐ โ ๐) = (๐ โ 1)) |
11 | 10 | oveq2d 7378 |
. . . . . . . 8
โข (๐ = 1 โ ((1 โ ๐ฅ)โ(๐ โ ๐)) = ((1 โ ๐ฅ)โ(๐ โ 1))) |
12 | 9, 11 | oveq12d 7380 |
. . . . . . 7
โข (๐ = 1 โ ((๐ฅโ(๐ โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ ๐))) = ((๐ฅโ(1 โ 1)) ยท ((1 โ
๐ฅ)โ(๐ โ 1)))) |
13 | 12 | adantr 482 |
. . . . . 6
โข ((๐ = 1 โง ๐ฅ โ (0[,]1)) โ ((๐ฅโ(๐ โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ ๐))) = ((๐ฅโ(1 โ 1)) ยท ((1 โ
๐ฅ)โ(๐ โ 1)))) |
14 | 13 | itgeq2dv 25162 |
. . . . 5
โข (๐ = 1 โ โซ(0[,]1)((๐ฅโ(๐ โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ ๐))) d๐ฅ = โซ(0[,]1)((๐ฅโ(1 โ 1)) ยท ((1 โ
๐ฅ)โ(๐ โ 1))) d๐ฅ) |
15 | | id 22 |
. . . . . . 7
โข (๐ = 1 โ ๐ = 1) |
16 | | oveq2 7370 |
. . . . . . 7
โข (๐ = 1 โ (๐C๐) = (๐C1)) |
17 | 15, 16 | oveq12d 7380 |
. . . . . 6
โข (๐ = 1 โ (๐ ยท (๐C๐)) = (1 ยท (๐C1))) |
18 | 17 | oveq2d 7378 |
. . . . 5
โข (๐ = 1 โ (1 / (๐ ยท (๐C๐))) = (1 / (1 ยท (๐C1)))) |
19 | 14, 18 | eqeq12d 2753 |
. . . 4
โข (๐ = 1 โ (โซ(0[,]1)((๐ฅโ(๐ โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ ๐))) d๐ฅ = (1 / (๐ ยท (๐C๐))) โ โซ(0[,]1)((๐ฅโ(1 โ 1)) ยท ((1 โ
๐ฅ)โ(๐ โ 1))) d๐ฅ = (1 / (1 ยท (๐C1))))) |
20 | | oveq1 7369 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ โ 1) = (๐ โ 1)) |
21 | 20 | oveq2d 7378 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ฅโ(๐ โ 1)) = (๐ฅโ(๐ โ 1))) |
22 | | oveq2 7370 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ โ ๐) = (๐ โ ๐)) |
23 | 22 | oveq2d 7378 |
. . . . . . . 8
โข (๐ = ๐ โ ((1 โ ๐ฅ)โ(๐ โ ๐)) = ((1 โ ๐ฅ)โ(๐ โ ๐))) |
24 | 21, 23 | oveq12d 7380 |
. . . . . . 7
โข (๐ = ๐ โ ((๐ฅโ(๐ โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ ๐))) = ((๐ฅโ(๐ โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ ๐)))) |
25 | 24 | adantr 482 |
. . . . . 6
โข ((๐ = ๐ โง ๐ฅ โ (0[,]1)) โ ((๐ฅโ(๐ โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ ๐))) = ((๐ฅโ(๐ โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ ๐)))) |
26 | 25 | itgeq2dv 25162 |
. . . . 5
โข (๐ = ๐ โ โซ(0[,]1)((๐ฅโ(๐ โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ ๐))) d๐ฅ = โซ(0[,]1)((๐ฅโ(๐ โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ ๐))) d๐ฅ) |
27 | | id 22 |
. . . . . . 7
โข (๐ = ๐ โ ๐ = ๐) |
28 | | oveq2 7370 |
. . . . . . 7
โข (๐ = ๐ โ (๐C๐) = (๐C๐)) |
29 | 27, 28 | oveq12d 7380 |
. . . . . 6
โข (๐ = ๐ โ (๐ ยท (๐C๐)) = (๐ ยท (๐C๐))) |
30 | 29 | oveq2d 7378 |
. . . . 5
โข (๐ = ๐ โ (1 / (๐ ยท (๐C๐))) = (1 / (๐ ยท (๐C๐)))) |
31 | 26, 30 | eqeq12d 2753 |
. . . 4
โข (๐ = ๐ โ (โซ(0[,]1)((๐ฅโ(๐ โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ ๐))) d๐ฅ = (1 / (๐ ยท (๐C๐))) โ โซ(0[,]1)((๐ฅโ(๐ โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ ๐))) d๐ฅ = (1 / (๐ ยท (๐C๐))))) |
32 | | oveq1 7369 |
. . . . . . . . 9
โข (๐ = (๐ + 1) โ (๐ โ 1) = ((๐ + 1) โ 1)) |
33 | 32 | oveq2d 7378 |
. . . . . . . 8
โข (๐ = (๐ + 1) โ (๐ฅโ(๐ โ 1)) = (๐ฅโ((๐ + 1) โ 1))) |
34 | | oveq2 7370 |
. . . . . . . . 9
โข (๐ = (๐ + 1) โ (๐ โ ๐) = (๐ โ (๐ + 1))) |
35 | 34 | oveq2d 7378 |
. . . . . . . 8
โข (๐ = (๐ + 1) โ ((1 โ ๐ฅ)โ(๐ โ ๐)) = ((1 โ ๐ฅ)โ(๐ โ (๐ + 1)))) |
36 | 33, 35 | oveq12d 7380 |
. . . . . . 7
โข (๐ = (๐ + 1) โ ((๐ฅโ(๐ โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ ๐))) = ((๐ฅโ((๐ + 1) โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ (๐ + 1))))) |
37 | 36 | adantr 482 |
. . . . . 6
โข ((๐ = (๐ + 1) โง ๐ฅ โ (0[,]1)) โ ((๐ฅโ(๐ โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ ๐))) = ((๐ฅโ((๐ + 1) โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ (๐ + 1))))) |
38 | 37 | itgeq2dv 25162 |
. . . . 5
โข (๐ = (๐ + 1) โ โซ(0[,]1)((๐ฅโ(๐ โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ ๐))) d๐ฅ = โซ(0[,]1)((๐ฅโ((๐ + 1) โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ (๐ + 1)))) d๐ฅ) |
39 | | id 22 |
. . . . . . 7
โข (๐ = (๐ + 1) โ ๐ = (๐ + 1)) |
40 | | oveq2 7370 |
. . . . . . 7
โข (๐ = (๐ + 1) โ (๐C๐) = (๐C(๐ + 1))) |
41 | 39, 40 | oveq12d 7380 |
. . . . . 6
โข (๐ = (๐ + 1) โ (๐ ยท (๐C๐)) = ((๐ + 1) ยท (๐C(๐ + 1)))) |
42 | 41 | oveq2d 7378 |
. . . . 5
โข (๐ = (๐ + 1) โ (1 / (๐ ยท (๐C๐))) = (1 / ((๐ + 1) ยท (๐C(๐ + 1))))) |
43 | 38, 42 | eqeq12d 2753 |
. . . 4
โข (๐ = (๐ + 1) โ (โซ(0[,]1)((๐ฅโ(๐ โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ ๐))) d๐ฅ = (1 / (๐ ยท (๐C๐))) โ โซ(0[,]1)((๐ฅโ((๐ + 1) โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ (๐ + 1)))) d๐ฅ = (1 / ((๐ + 1) ยท (๐C(๐ + 1)))))) |
44 | | oveq1 7369 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ โ 1) = (๐ โ 1)) |
45 | 44 | oveq2d 7378 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ฅโ(๐ โ 1)) = (๐ฅโ(๐ โ 1))) |
46 | | oveq2 7370 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ โ ๐) = (๐ โ ๐)) |
47 | 46 | oveq2d 7378 |
. . . . . . . 8
โข (๐ = ๐ โ ((1 โ ๐ฅ)โ(๐ โ ๐)) = ((1 โ ๐ฅ)โ(๐ โ ๐))) |
48 | 45, 47 | oveq12d 7380 |
. . . . . . 7
โข (๐ = ๐ โ ((๐ฅโ(๐ โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ ๐))) = ((๐ฅโ(๐ โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ ๐)))) |
49 | 48 | adantr 482 |
. . . . . 6
โข ((๐ = ๐ โง ๐ฅ โ (0[,]1)) โ ((๐ฅโ(๐ โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ ๐))) = ((๐ฅโ(๐ โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ ๐)))) |
50 | 49 | itgeq2dv 25162 |
. . . . 5
โข (๐ = ๐ โ โซ(0[,]1)((๐ฅโ(๐ โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ ๐))) d๐ฅ = โซ(0[,]1)((๐ฅโ(๐ โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ ๐))) d๐ฅ) |
51 | | id 22 |
. . . . . . 7
โข (๐ = ๐ โ ๐ = ๐) |
52 | | oveq2 7370 |
. . . . . . 7
โข (๐ = ๐ โ (๐C๐) = (๐C๐)) |
53 | 51, 52 | oveq12d 7380 |
. . . . . 6
โข (๐ = ๐ โ (๐ ยท (๐C๐)) = (๐ ยท (๐C๐))) |
54 | 53 | oveq2d 7378 |
. . . . 5
โข (๐ = ๐ โ (1 / (๐ ยท (๐C๐))) = (1 / (๐ ยท (๐C๐)))) |
55 | 50, 54 | eqeq12d 2753 |
. . . 4
โข (๐ = ๐ โ (โซ(0[,]1)((๐ฅโ(๐ โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ ๐))) d๐ฅ = (1 / (๐ ยท (๐C๐))) โ โซ(0[,]1)((๐ฅโ(๐ โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ ๐))) d๐ฅ = (1 / (๐ ยท (๐C๐))))) |
56 | | lcmineqlem13.3 |
. . . . 5
โข (๐ โ ๐ โ โ) |
57 | 56 | lcmineqlem12 40526 |
. . . 4
โข (๐ โ โซ(0[,]1)((๐ฅโ(1 โ 1)) ยท
((1 โ ๐ฅ)โ(๐ โ 1))) d๐ฅ = (1 / (1 ยท (๐C1)))) |
58 | | elnnz1 12536 |
. . . . . . . . . . 11
โข (๐ โ โ โ (๐ โ โค โง 1 โค
๐)) |
59 | 58 | biimpri 227 |
. . . . . . . . . 10
โข ((๐ โ โค โง 1 โค
๐) โ ๐ โ
โ) |
60 | 59 | 3adant3 1133 |
. . . . . . . . 9
โข ((๐ โ โค โง 1 โค
๐ โง ๐ < ๐) โ ๐ โ โ) |
61 | 60 | adantl 483 |
. . . . . . . 8
โข ((๐ โง (๐ โ โค โง 1 โค ๐ โง ๐ < ๐)) โ ๐ โ โ) |
62 | 56 | adantr 482 |
. . . . . . . 8
โข ((๐ โง (๐ โ โค โง 1 โค ๐ โง ๐ < ๐)) โ ๐ โ โ) |
63 | | simpr3 1197 |
. . . . . . . 8
โข ((๐ โง (๐ โ โค โง 1 โค ๐ โง ๐ < ๐)) โ ๐ < ๐) |
64 | 61, 62, 63 | lcmineqlem10 40524 |
. . . . . . 7
โข ((๐ โง (๐ โ โค โง 1 โค ๐ โง ๐ < ๐)) โ โซ(0[,]1)((๐ฅโ((๐ + 1) โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ (๐ + 1)))) d๐ฅ = ((๐ / (๐ โ ๐)) ยท โซ(0[,]1)((๐ฅโ(๐ โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ ๐))) d๐ฅ)) |
65 | 64 | 3adant3 1133 |
. . . . . 6
โข ((๐ โง (๐ โ โค โง 1 โค ๐ โง ๐ < ๐) โง โซ(0[,]1)((๐ฅโ(๐ โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ ๐))) d๐ฅ = (1 / (๐ ยท (๐C๐)))) โ โซ(0[,]1)((๐ฅโ((๐ + 1) โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ (๐ + 1)))) d๐ฅ = ((๐ / (๐ โ ๐)) ยท โซ(0[,]1)((๐ฅโ(๐ โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ ๐))) d๐ฅ)) |
66 | | oveq2 7370 |
. . . . . . 7
โข
(โซ(0[,]1)((๐ฅโ(๐ โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ ๐))) d๐ฅ = (1 / (๐ ยท (๐C๐))) โ ((๐ / (๐ โ ๐)) ยท โซ(0[,]1)((๐ฅโ(๐ โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ ๐))) d๐ฅ) = ((๐ / (๐ โ ๐)) ยท (1 / (๐ ยท (๐C๐))))) |
67 | 66 | 3ad2ant3 1136 |
. . . . . 6
โข ((๐ โง (๐ โ โค โง 1 โค ๐ โง ๐ < ๐) โง โซ(0[,]1)((๐ฅโ(๐ โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ ๐))) d๐ฅ = (1 / (๐ ยท (๐C๐)))) โ ((๐ / (๐ โ ๐)) ยท โซ(0[,]1)((๐ฅโ(๐ โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ ๐))) d๐ฅ) = ((๐ / (๐ โ ๐)) ยท (1 / (๐ ยท (๐C๐))))) |
68 | 65, 67 | eqtrd 2777 |
. . . . 5
โข ((๐ โง (๐ โ โค โง 1 โค ๐ โง ๐ < ๐) โง โซ(0[,]1)((๐ฅโ(๐ โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ ๐))) d๐ฅ = (1 / (๐ ยท (๐C๐)))) โ โซ(0[,]1)((๐ฅโ((๐ + 1) โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ (๐ + 1)))) d๐ฅ = ((๐ / (๐ โ ๐)) ยท (1 / (๐ ยท (๐C๐))))) |
69 | 61, 62, 63 | lcmineqlem11 40525 |
. . . . . 6
โข ((๐ โง (๐ โ โค โง 1 โค ๐ โง ๐ < ๐)) โ (1 / ((๐ + 1) ยท (๐C(๐ + 1)))) = ((๐ / (๐ โ ๐)) ยท (1 / (๐ ยท (๐C๐))))) |
70 | 69 | 3adant3 1133 |
. . . . 5
โข ((๐ โง (๐ โ โค โง 1 โค ๐ โง ๐ < ๐) โง โซ(0[,]1)((๐ฅโ(๐ โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ ๐))) d๐ฅ = (1 / (๐ ยท (๐C๐)))) โ (1 / ((๐ + 1) ยท (๐C(๐ + 1)))) = ((๐ / (๐ โ ๐)) ยท (1 / (๐ ยท (๐C๐))))) |
71 | 68, 70 | eqtr4d 2780 |
. . . 4
โข ((๐ โง (๐ โ โค โง 1 โค ๐ โง ๐ < ๐) โง โซ(0[,]1)((๐ฅโ(๐ โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ ๐))) d๐ฅ = (1 / (๐ ยท (๐C๐)))) โ โซ(0[,]1)((๐ฅโ((๐ + 1) โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ (๐ + 1)))) d๐ฅ = (1 / ((๐ + 1) ยท (๐C(๐ + 1))))) |
72 | | 1zzd 12541 |
. . . 4
โข (๐ โ 1 โ
โค) |
73 | 56 | nnzd 12533 |
. . . 4
โข (๐ โ ๐ โ โค) |
74 | 56 | nnge1d 12208 |
. . . 4
โข (๐ โ 1 โค ๐) |
75 | 19, 31, 43, 55, 57, 71, 72, 73, 74 | fzindd 12612 |
. . 3
โข ((๐ โง (๐ โ โค โง 1 โค ๐ โง ๐ โค ๐)) โ โซ(0[,]1)((๐ฅโ(๐ โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ ๐))) d๐ฅ = (1 / (๐ ยท (๐C๐)))) |
76 | 7, 75 | mpdan 686 |
. 2
โข (๐ โ โซ(0[,]1)((๐ฅโ(๐ โ 1)) ยท ((1 โ ๐ฅ)โ(๐ โ ๐))) d๐ฅ = (1 / (๐ ยท (๐C๐)))) |
77 | 1, 76 | eqtrid 2789 |
1
โข (๐ โ ๐น = (1 / (๐ ยท (๐C๐)))) |