Step | Hyp | Ref
| Expression |
1 | | oveq2 7369 |
. . . . . . . 8
β’ (π = π‘ β (1 β π) = (1 β π‘)) |
2 | 1 | oveq1d 7376 |
. . . . . . 7
β’ (π = π‘ β ((1 β π) Β· (π₯βπ)) = ((1 β π‘) Β· (π₯βπ))) |
3 | | oveq1 7368 |
. . . . . . 7
β’ (π = π‘ β (π Β· (π¦βπ)) = (π‘ Β· (π¦βπ))) |
4 | 2, 3 | oveq12d 7379 |
. . . . . 6
β’ (π = π‘ β (((1 β π) Β· (π₯βπ)) + (π Β· (π¦βπ))) = (((1 β π‘) Β· (π₯βπ)) + (π‘ Β· (π¦βπ)))) |
5 | 4 | eqeq2d 2744 |
. . . . 5
β’ (π = π‘ β ((πβπ) = (((1 β π) Β· (π₯βπ)) + (π Β· (π¦βπ))) β (πβπ) = (((1 β π‘) Β· (π₯βπ)) + (π‘ Β· (π¦βπ))))) |
6 | 5 | ralbidv 3171 |
. . . 4
β’ (π = π‘ β (βπ β (1...π)(πβπ) = (((1 β π) Β· (π₯βπ)) + (π Β· (π¦βπ))) β βπ β (1...π)(πβπ) = (((1 β π‘) Β· (π₯βπ)) + (π‘ Β· (π¦βπ))))) |
7 | 6 | cbvrexvw 3225 |
. . 3
β’
(βπ β
(0[,]1)βπ β
(1...π)(πβπ) = (((1 β π) Β· (π₯βπ)) + (π Β· (π¦βπ))) β βπ‘ β (0[,]1)βπ β (1...π)(πβπ) = (((1 β π‘) Β· (π₯βπ)) + (π‘ Β· (π¦βπ)))) |
8 | | unitssre 13425 |
. . . 4
β’ (0[,]1)
β β |
9 | | ssrexv 4015 |
. . . 4
β’ ((0[,]1)
β β β (βπ‘ β (0[,]1)βπ β (1...π)(πβπ) = (((1 β π‘) Β· (π₯βπ)) + (π‘ Β· (π¦βπ))) β βπ‘ β β βπ β (1...π)(πβπ) = (((1 β π‘) Β· (π₯βπ)) + (π‘ Β· (π¦βπ))))) |
10 | 8, 9 | mp1i 13 |
. . 3
β’ (((π β β β§ π₯ β (β
βm (1...π))
β§ π¦ β ((β
βm (1...π))
β {π₯})) β§ π β (β
βm (1...π))) β (βπ‘ β (0[,]1)βπ β (1...π)(πβπ) = (((1 β π‘) Β· (π₯βπ)) + (π‘ Β· (π¦βπ))) β βπ‘ β β βπ β (1...π)(πβπ) = (((1 β π‘) Β· (π₯βπ)) + (π‘ Β· (π¦βπ))))) |
11 | 7, 10 | biimtrid 241 |
. 2
β’ (((π β β β§ π₯ β (β
βm (1...π))
β§ π¦ β ((β
βm (1...π))
β {π₯})) β§ π β (β
βm (1...π))) β (βπ β (0[,]1)βπ β (1...π)(πβπ) = (((1 β π) Β· (π₯βπ)) + (π Β· (π¦βπ))) β βπ‘ β β βπ β (1...π)(πβπ) = (((1 β π‘) Β· (π₯βπ)) + (π‘ Β· (π¦βπ))))) |
12 | | 0re 11165 |
. . . . . . . 8
β’ 0 β
β |
13 | | 1xr 11222 |
. . . . . . . 8
β’ 1 β
β* |
14 | | elico2 13337 |
. . . . . . . 8
β’ ((0
β β β§ 1 β β*) β (π β (0[,)1) β (π β β β§ 0 β€ π β§ π < 1))) |
15 | 12, 13, 14 | mp2an 691 |
. . . . . . 7
β’ (π β (0[,)1) β (π β β β§ 0 β€
π β§ π < 1)) |
16 | | simp1 1137 |
. . . . . . . 8
β’ ((π β β β§ 0 β€
π β§ π < 1) β π β β) |
17 | | 1red 11164 |
. . . . . . . . 9
β’ ((π β β β§ 0 β€
π β§ π < 1) β 1 β
β) |
18 | 17, 16 | resubcld 11591 |
. . . . . . . 8
β’ ((π β β β§ 0 β€
π β§ π < 1) β (1 β π) β β) |
19 | | 1cnd 11158 |
. . . . . . . . 9
β’ ((π β β β§ 0 β€
π β§ π < 1) β 1 β
β) |
20 | 16 | recnd 11191 |
. . . . . . . . 9
β’ ((π β β β§ 0 β€
π β§ π < 1) β π β β) |
21 | | ltne 11260 |
. . . . . . . . . 10
β’ ((π β β β§ π < 1) β 1 β π) |
22 | 21 | 3adant2 1132 |
. . . . . . . . 9
β’ ((π β β β§ 0 β€
π β§ π < 1) β 1 β π) |
23 | 19, 20, 22 | subne0d 11529 |
. . . . . . . 8
β’ ((π β β β§ 0 β€
π β§ π < 1) β (1 β π) β 0) |
24 | 16, 18, 23 | redivcld 11991 |
. . . . . . 7
β’ ((π β β β§ 0 β€
π β§ π < 1) β (π / (1 β π)) β β) |
25 | 15, 24 | sylbi 216 |
. . . . . 6
β’ (π β (0[,)1) β (π / (1 β π)) β β) |
26 | 25 | ad2antlr 726 |
. . . . 5
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§
βπ β (1...π)(π₯βπ) = (((1 β π) Β· (πβπ)) + (π Β· (π¦βπ)))) β (π / (1 β π)) β β) |
27 | 26 | renegcld 11590 |
. . . 4
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§
βπ β (1...π)(π₯βπ) = (((1 β π) Β· (πβπ)) + (π Β· (π¦βπ)))) β -(π / (1 β π)) β β) |
28 | | oveq2 7369 |
. . . . . . . . 9
β’ (π‘ = -(π / (1 β π)) β (1 β π‘) = (1 β -(π / (1 β π)))) |
29 | 28 | oveq1d 7376 |
. . . . . . . 8
β’ (π‘ = -(π / (1 β π)) β ((1 β π‘) Β· (π₯βπ)) = ((1 β -(π / (1 β π))) Β· (π₯βπ))) |
30 | | oveq1 7368 |
. . . . . . . 8
β’ (π‘ = -(π / (1 β π)) β (π‘ Β· (π¦βπ)) = (-(π / (1 β π)) Β· (π¦βπ))) |
31 | 29, 30 | oveq12d 7379 |
. . . . . . 7
β’ (π‘ = -(π / (1 β π)) β (((1 β π‘) Β· (π₯βπ)) + (π‘ Β· (π¦βπ))) = (((1 β -(π / (1 β π))) Β· (π₯βπ)) + (-(π / (1 β π)) Β· (π¦βπ)))) |
32 | 31 | eqeq2d 2744 |
. . . . . 6
β’ (π‘ = -(π / (1 β π)) β ((πβπ) = (((1 β π‘) Β· (π₯βπ)) + (π‘ Β· (π¦βπ))) β (πβπ) = (((1 β -(π / (1 β π))) Β· (π₯βπ)) + (-(π / (1 β π)) Β· (π¦βπ))))) |
33 | 32 | ralbidv 3171 |
. . . . 5
β’ (π‘ = -(π / (1 β π)) β (βπ β (1...π)(πβπ) = (((1 β π‘) Β· (π₯βπ)) + (π‘ Β· (π¦βπ))) β βπ β (1...π)(πβπ) = (((1 β -(π / (1 β π))) Β· (π₯βπ)) + (-(π / (1 β π)) Β· (π¦βπ))))) |
34 | 33 | adantl 483 |
. . . 4
β’
((((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§
βπ β (1...π)(π₯βπ) = (((1 β π) Β· (πβπ)) + (π Β· (π¦βπ)))) β§ π‘ = -(π / (1 β π))) β (βπ β (1...π)(πβπ) = (((1 β π‘) Β· (π₯βπ)) + (π‘ Β· (π¦βπ))) β βπ β (1...π)(πβπ) = (((1 β -(π / (1 β π))) Β· (π₯βπ)) + (-(π / (1 β π)) Β· (π¦βπ))))) |
35 | | eqcom 2740 |
. . . . . . . 8
β’ ((π₯βπ) = (((1 β π) Β· (πβπ)) + (π Β· (π¦βπ))) β (((1 β π) Β· (πβπ)) + (π Β· (π¦βπ))) = (π₯βπ)) |
36 | | elmapi 8793 |
. . . . . . . . . . . . 13
β’ (π₯ β (β
βm (1...π))
β π₯:(1...π)βΆβ) |
37 | 36 | 3ad2ant2 1135 |
. . . . . . . . . . . 12
β’ ((π β β β§ π₯ β (β
βm (1...π))
β§ π¦ β ((β
βm (1...π))
β {π₯})) β π₯:(1...π)βΆβ) |
38 | 37 | ad2antrr 725 |
. . . . . . . . . . 11
β’ ((((π β β β§ π₯ β (β
βm (1...π))
β§ π¦ β ((β
βm (1...π))
β {π₯})) β§ π β (β
βm (1...π))) β§ π β (0[,)1)) β π₯:(1...π)βΆβ) |
39 | 38 | ffvelcdmda 7039 |
. . . . . . . . . 10
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β (π₯βπ) β β) |
40 | 39 | recnd 11191 |
. . . . . . . . 9
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β (π₯βπ) β β) |
41 | 15, 16 | sylbi 216 |
. . . . . . . . . . . 12
β’ (π β (0[,)1) β π β
β) |
42 | 41 | ad2antlr 726 |
. . . . . . . . . . 11
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β π β β) |
43 | 42 | recnd 11191 |
. . . . . . . . . 10
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β π β β) |
44 | | eldifi 4090 |
. . . . . . . . . . . . . . 15
β’ (π¦ β ((β
βm (1...π))
β {π₯}) β π¦ β (β
βm (1...π))) |
45 | | elmapi 8793 |
. . . . . . . . . . . . . . 15
β’ (π¦ β (β
βm (1...π))
β π¦:(1...π)βΆβ) |
46 | 44, 45 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π¦ β ((β
βm (1...π))
β {π₯}) β π¦:(1...π)βΆβ) |
47 | 46 | 3ad2ant3 1136 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π₯ β (β
βm (1...π))
β§ π¦ β ((β
βm (1...π))
β {π₯})) β π¦:(1...π)βΆβ) |
48 | 47 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ ((((π β β β§ π₯ β (β
βm (1...π))
β§ π¦ β ((β
βm (1...π))
β {π₯})) β§ π β (β
βm (1...π))) β§ π β (0[,)1)) β π¦:(1...π)βΆβ) |
49 | 48 | ffvelcdmda 7039 |
. . . . . . . . . . 11
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β (π¦βπ) β β) |
50 | 49 | recnd 11191 |
. . . . . . . . . 10
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β (π¦βπ) β β) |
51 | 43, 50 | mulcld 11183 |
. . . . . . . . 9
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β (π Β· (π¦βπ)) β β) |
52 | | 1cnd 11158 |
. . . . . . . . . . 11
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β 1 β β) |
53 | 52, 43 | subcld 11520 |
. . . . . . . . . 10
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β (1 β π) β β) |
54 | | elmapi 8793 |
. . . . . . . . . . . . 13
β’ (π β (β
βm (1...π))
β π:(1...π)βΆβ) |
55 | 54 | ad2antlr 726 |
. . . . . . . . . . . 12
β’ ((((π β β β§ π₯ β (β
βm (1...π))
β§ π¦ β ((β
βm (1...π))
β {π₯})) β§ π β (β
βm (1...π))) β§ π β (0[,)1)) β π:(1...π)βΆβ) |
56 | 55 | ffvelcdmda 7039 |
. . . . . . . . . . 11
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β (πβπ) β β) |
57 | 56 | recnd 11191 |
. . . . . . . . . 10
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β (πβπ) β β) |
58 | 53, 57 | mulcld 11183 |
. . . . . . . . 9
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β ((1 β π) Β· (πβπ)) β β) |
59 | 40, 51, 58 | subadd2d 11539 |
. . . . . . . 8
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β (((π₯βπ) β (π Β· (π¦βπ))) = ((1 β π) Β· (πβπ)) β (((1 β π) Β· (πβπ)) + (π Β· (π¦βπ))) = (π₯βπ))) |
60 | 35, 59 | bitr4id 290 |
. . . . . . 7
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β ((π₯βπ) = (((1 β π) Β· (πβπ)) + (π Β· (π¦βπ))) β ((π₯βπ) β (π Β· (π¦βπ))) = ((1 β π) Β· (πβπ)))) |
61 | | eqcom 2740 |
. . . . . . . . 9
β’ (((π₯βπ) β (π Β· (π¦βπ))) = ((1 β π) Β· (πβπ)) β ((1 β π) Β· (πβπ)) = ((π₯βπ) β (π Β· (π¦βπ)))) |
62 | 40, 51 | subcld 11520 |
. . . . . . . . . 10
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β ((π₯βπ) β (π Β· (π¦βπ))) β β) |
63 | 15, 22 | sylbi 216 |
. . . . . . . . . . . 12
β’ (π β (0[,)1) β 1 β
π) |
64 | 63 | ad2antlr 726 |
. . . . . . . . . . 11
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β 1 β π) |
65 | 52, 43, 64 | subne0d 11529 |
. . . . . . . . . 10
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β (1 β π) β 0) |
66 | 62, 53, 57, 65 | divmuld 11961 |
. . . . . . . . 9
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β ((((π₯βπ) β (π Β· (π¦βπ))) / (1 β π)) = (πβπ) β ((1 β π) Β· (πβπ)) = ((π₯βπ) β (π Β· (π¦βπ))))) |
67 | 61, 66 | bitr4id 290 |
. . . . . . . 8
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β (((π₯βπ) β (π Β· (π¦βπ))) = ((1 β π) Β· (πβπ)) β (((π₯βπ) β (π Β· (π¦βπ))) / (1 β π)) = (πβπ))) |
68 | | eqcom 2740 |
. . . . . . . . . 10
β’ ((((π₯βπ) β (π Β· (π¦βπ))) / (1 β π)) = (πβπ) β (πβπ) = (((π₯βπ) β (π Β· (π¦βπ))) / (1 β π))) |
69 | 40, 51, 53, 65 | divsubdird 11978 |
. . . . . . . . . . . 12
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β (((π₯βπ) β (π Β· (π¦βπ))) / (1 β π)) = (((π₯βπ) / (1 β π)) β ((π Β· (π¦βπ)) / (1 β π)))) |
70 | 40, 53, 65 | divrec2d 11943 |
. . . . . . . . . . . . 13
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β ((π₯βπ) / (1 β π)) = ((1 / (1 β π)) Β· (π₯βπ))) |
71 | 43, 50, 53, 65 | div23d 11976 |
. . . . . . . . . . . . 13
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β ((π Β· (π¦βπ)) / (1 β π)) = ((π / (1 β π)) Β· (π¦βπ))) |
72 | 70, 71 | oveq12d 7379 |
. . . . . . . . . . . 12
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β (((π₯βπ) / (1 β π)) β ((π Β· (π¦βπ)) / (1 β π))) = (((1 / (1 β π)) Β· (π₯βπ)) β ((π / (1 β π)) Β· (π¦βπ)))) |
73 | 69, 72 | eqtrd 2773 |
. . . . . . . . . . 11
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β (((π₯βπ) β (π Β· (π¦βπ))) / (1 β π)) = (((1 / (1 β π)) Β· (π₯βπ)) β ((π / (1 β π)) Β· (π¦βπ)))) |
74 | 73 | eqeq2d 2744 |
. . . . . . . . . 10
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β ((πβπ) = (((π₯βπ) β (π Β· (π¦βπ))) / (1 β π)) β (πβπ) = (((1 / (1 β π)) Β· (π₯βπ)) β ((π / (1 β π)) Β· (π¦βπ))))) |
75 | 68, 74 | bitrid 283 |
. . . . . . . . 9
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β ((((π₯βπ) β (π Β· (π¦βπ))) / (1 β π)) = (πβπ) β (πβπ) = (((1 / (1 β π)) Β· (π₯βπ)) β ((π / (1 β π)) Β· (π¦βπ))))) |
76 | 43, 53, 65 | divcld 11939 |
. . . . . . . . . . . . . . 15
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β (π / (1 β π)) β β) |
77 | 76, 50 | mulneg1d 11616 |
. . . . . . . . . . . . . 14
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β (-(π / (1 β π)) Β· (π¦βπ)) = -((π / (1 β π)) Β· (π¦βπ))) |
78 | 77 | eqcomd 2739 |
. . . . . . . . . . . . 13
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β -((π / (1 β π)) Β· (π¦βπ)) = (-(π / (1 β π)) Β· (π¦βπ))) |
79 | 78 | oveq2d 7377 |
. . . . . . . . . . . 12
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β (((1 / (1 β π)) Β· (π₯βπ)) + -((π / (1 β π)) Β· (π¦βπ))) = (((1 / (1 β π)) Β· (π₯βπ)) + (-(π / (1 β π)) Β· (π¦βπ)))) |
80 | 53, 65 | reccld 11932 |
. . . . . . . . . . . . . 14
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β (1 / (1 β π)) β β) |
81 | 80, 40 | mulcld 11183 |
. . . . . . . . . . . . 13
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β ((1 / (1 β π)) Β· (π₯βπ)) β β) |
82 | 76, 50 | mulcld 11183 |
. . . . . . . . . . . . 13
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β ((π / (1 β π)) Β· (π¦βπ)) β β) |
83 | 81, 82 | negsubd 11526 |
. . . . . . . . . . . 12
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β (((1 / (1 β π)) Β· (π₯βπ)) + -((π / (1 β π)) Β· (π¦βπ))) = (((1 / (1 β π)) Β· (π₯βπ)) β ((π / (1 β π)) Β· (π¦βπ)))) |
84 | 52, 76 | subnegd 11527 |
. . . . . . . . . . . . . . . 16
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β (1 β -(π / (1 β π))) = (1 + (π / (1 β π)))) |
85 | | muldivdir 11856 |
. . . . . . . . . . . . . . . . 17
β’ ((1
β β β§ π
β β β§ ((1 β π) β β β§ (1 β π) β 0)) β ((((1 β
π) Β· 1) + π) / (1 β π)) = (1 + (π / (1 β π)))) |
86 | 52, 43, 53, 65, 85 | syl112anc 1375 |
. . . . . . . . . . . . . . . 16
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β ((((1 β π) Β· 1) + π) / (1 β π)) = (1 + (π / (1 β π)))) |
87 | 53 | mulridd 11180 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β ((1 β π) Β· 1) = (1 β π)) |
88 | 87 | oveq1d 7376 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β (((1 β π) Β· 1) + π) = ((1 β π) + π)) |
89 | 52, 43 | npcand 11524 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β ((1 β π) + π) = 1) |
90 | 88, 89 | eqtrd 2773 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β (((1 β π) Β· 1) + π) = 1) |
91 | 90 | oveq1d 7376 |
. . . . . . . . . . . . . . . 16
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β ((((1 β π) Β· 1) + π) / (1 β π)) = (1 / (1 β π))) |
92 | 84, 86, 91 | 3eqtr2d 2779 |
. . . . . . . . . . . . . . 15
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β (1 β -(π / (1 β π))) = (1 / (1 β π))) |
93 | 92 | eqcomd 2739 |
. . . . . . . . . . . . . 14
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β (1 / (1 β π)) = (1 β -(π / (1 β π)))) |
94 | 93 | oveq1d 7376 |
. . . . . . . . . . . . 13
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β ((1 / (1 β π)) Β· (π₯βπ)) = ((1 β -(π / (1 β π))) Β· (π₯βπ))) |
95 | 94 | oveq1d 7376 |
. . . . . . . . . . . 12
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β (((1 / (1 β π)) Β· (π₯βπ)) + (-(π / (1 β π)) Β· (π¦βπ))) = (((1 β -(π / (1 β π))) Β· (π₯βπ)) + (-(π / (1 β π)) Β· (π¦βπ)))) |
96 | 79, 83, 95 | 3eqtr3d 2781 |
. . . . . . . . . . 11
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β (((1 / (1 β π)) Β· (π₯βπ)) β ((π / (1 β π)) Β· (π¦βπ))) = (((1 β -(π / (1 β π))) Β· (π₯βπ)) + (-(π / (1 β π)) Β· (π¦βπ)))) |
97 | 96 | eqeq2d 2744 |
. . . . . . . . . 10
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β ((πβπ) = (((1 / (1 β π)) Β· (π₯βπ)) β ((π / (1 β π)) Β· (π¦βπ))) β (πβπ) = (((1 β -(π / (1 β π))) Β· (π₯βπ)) + (-(π / (1 β π)) Β· (π¦βπ))))) |
98 | 97 | biimpd 228 |
. . . . . . . . 9
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β ((πβπ) = (((1 / (1 β π)) Β· (π₯βπ)) β ((π / (1 β π)) Β· (π¦βπ))) β (πβπ) = (((1 β -(π / (1 β π))) Β· (π₯βπ)) + (-(π / (1 β π)) Β· (π¦βπ))))) |
99 | 75, 98 | sylbid 239 |
. . . . . . . 8
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β ((((π₯βπ) β (π Β· (π¦βπ))) / (1 β π)) = (πβπ) β (πβπ) = (((1 β -(π / (1 β π))) Β· (π₯βπ)) + (-(π / (1 β π)) Β· (π¦βπ))))) |
100 | 67, 99 | sylbid 239 |
. . . . . . 7
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β (((π₯βπ) β (π Β· (π¦βπ))) = ((1 β π) Β· (πβπ)) β (πβπ) = (((1 β -(π / (1 β π))) Β· (π₯βπ)) + (-(π / (1 β π)) Β· (π¦βπ))))) |
101 | 60, 100 | sylbid 239 |
. . . . . 6
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§ π β (1...π)) β ((π₯βπ) = (((1 β π) Β· (πβπ)) + (π Β· (π¦βπ))) β (πβπ) = (((1 β -(π / (1 β π))) Β· (π₯βπ)) + (-(π / (1 β π)) Β· (π¦βπ))))) |
102 | 101 | ralimdva 3161 |
. . . . 5
β’ ((((π β β β§ π₯ β (β
βm (1...π))
β§ π¦ β ((β
βm (1...π))
β {π₯})) β§ π β (β
βm (1...π))) β§ π β (0[,)1)) β (βπ β (1...π)(π₯βπ) = (((1 β π) Β· (πβπ)) + (π Β· (π¦βπ))) β βπ β (1...π)(πβπ) = (((1 β -(π / (1 β π))) Β· (π₯βπ)) + (-(π / (1 β π)) Β· (π¦βπ))))) |
103 | 102 | imp 408 |
. . . 4
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§
βπ β (1...π)(π₯βπ) = (((1 β π) Β· (πβπ)) + (π Β· (π¦βπ)))) β βπ β (1...π)(πβπ) = (((1 β -(π / (1 β π))) Β· (π₯βπ)) + (-(π / (1 β π)) Β· (π¦βπ)))) |
104 | 27, 34, 103 | rspcedvd 3585 |
. . 3
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0[,)1)) β§
βπ β (1...π)(π₯βπ) = (((1 β π) Β· (πβπ)) + (π Β· (π¦βπ)))) β βπ‘ β β βπ β (1...π)(πβπ) = (((1 β π‘) Β· (π₯βπ)) + (π‘ Β· (π¦βπ)))) |
105 | 104 | rexlimdva2 3151 |
. 2
β’ (((π β β β§ π₯ β (β
βm (1...π))
β§ π¦ β ((β
βm (1...π))
β {π₯})) β§ π β (β
βm (1...π))) β (βπ β (0[,)1)βπ β (1...π)(π₯βπ) = (((1 β π) Β· (πβπ)) + (π Β· (π¦βπ))) β βπ‘ β β βπ β (1...π)(πβπ) = (((1 β π‘) Β· (π₯βπ)) + (π‘ Β· (π¦βπ))))) |
106 | | 0xr 11210 |
. . . . . . 7
β’ 0 β
β* |
107 | | 1re 11163 |
. . . . . . 7
β’ 1 β
β |
108 | | elioc2 13336 |
. . . . . . 7
β’ ((0
β β* β§ 1 β β) β (π β (0(,]1) β (π β β β§ 0 < π β§ π β€ 1))) |
109 | 106, 107,
108 | mp2an 691 |
. . . . . 6
β’ (π β (0(,]1) β (π β β β§ 0 <
π β§ π β€ 1)) |
110 | | simp1 1137 |
. . . . . . 7
β’ ((π β β β§ 0 <
π β§ π β€ 1) β π β β) |
111 | | gt0ne0 11628 |
. . . . . . . 8
β’ ((π β β β§ 0 <
π) β π β 0) |
112 | 111 | 3adant3 1133 |
. . . . . . 7
β’ ((π β β β§ 0 <
π β§ π β€ 1) β π β 0) |
113 | 110, 112 | rereccld 11990 |
. . . . . 6
β’ ((π β β β§ 0 <
π β§ π β€ 1) β (1 / π) β β) |
114 | 109, 113 | sylbi 216 |
. . . . 5
β’ (π β (0(,]1) β (1 /
π) β
β) |
115 | 114 | ad2antlr 726 |
. . . 4
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§
βπ β (1...π)(π¦βπ) = (((1 β π) Β· (π₯βπ)) + (π Β· (πβπ)))) β (1 / π) β β) |
116 | | oveq2 7369 |
. . . . . . . . 9
β’ (π‘ = (1 / π) β (1 β π‘) = (1 β (1 / π))) |
117 | 116 | oveq1d 7376 |
. . . . . . . 8
β’ (π‘ = (1 / π) β ((1 β π‘) Β· (π₯βπ)) = ((1 β (1 / π)) Β· (π₯βπ))) |
118 | | oveq1 7368 |
. . . . . . . 8
β’ (π‘ = (1 / π) β (π‘ Β· (π¦βπ)) = ((1 / π) Β· (π¦βπ))) |
119 | 117, 118 | oveq12d 7379 |
. . . . . . 7
β’ (π‘ = (1 / π) β (((1 β π‘) Β· (π₯βπ)) + (π‘ Β· (π¦βπ))) = (((1 β (1 / π)) Β· (π₯βπ)) + ((1 / π) Β· (π¦βπ)))) |
120 | 119 | eqeq2d 2744 |
. . . . . 6
β’ (π‘ = (1 / π) β ((πβπ) = (((1 β π‘) Β· (π₯βπ)) + (π‘ Β· (π¦βπ))) β (πβπ) = (((1 β (1 / π)) Β· (π₯βπ)) + ((1 / π) Β· (π¦βπ))))) |
121 | 120 | ralbidv 3171 |
. . . . 5
β’ (π‘ = (1 / π) β (βπ β (1...π)(πβπ) = (((1 β π‘) Β· (π₯βπ)) + (π‘ Β· (π¦βπ))) β βπ β (1...π)(πβπ) = (((1 β (1 / π)) Β· (π₯βπ)) + ((1 / π) Β· (π¦βπ))))) |
122 | 121 | adantl 483 |
. . . 4
β’
((((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§
βπ β (1...π)(π¦βπ) = (((1 β π) Β· (π₯βπ)) + (π Β· (πβπ)))) β§ π‘ = (1 / π)) β (βπ β (1...π)(πβπ) = (((1 β π‘) Β· (π₯βπ)) + (π‘ Β· (π¦βπ))) β βπ β (1...π)(πβπ) = (((1 β (1 / π)) Β· (π₯βπ)) + ((1 / π) Β· (π¦βπ))))) |
123 | | eqcom 2740 |
. . . . . . . 8
β’ ((π¦βπ) = (((1 β π) Β· (π₯βπ)) + (π Β· (πβπ))) β (((1 β π) Β· (π₯βπ)) + (π Β· (πβπ))) = (π¦βπ)) |
124 | 47 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ ((((π β β β§ π₯ β (β
βm (1...π))
β§ π¦ β ((β
βm (1...π))
β {π₯})) β§ π β (β
βm (1...π))) β§ π β (0(,]1)) β π¦:(1...π)βΆβ) |
125 | 124 | ffvelcdmda 7039 |
. . . . . . . . . . . . 13
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β (π¦βπ) β β) |
126 | 125 | recnd 11191 |
. . . . . . . . . . . 12
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β (π¦βπ) β β) |
127 | | 1cnd 11158 |
. . . . . . . . . . . . . 14
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β 1 β β) |
128 | 109, 110 | sylbi 216 |
. . . . . . . . . . . . . . . 16
β’ (π β (0(,]1) β π β
β) |
129 | 128 | recnd 11191 |
. . . . . . . . . . . . . . 15
β’ (π β (0(,]1) β π β
β) |
130 | 129 | ad2antlr 726 |
. . . . . . . . . . . . . 14
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β π β β) |
131 | 127, 130 | subcld 11520 |
. . . . . . . . . . . . 13
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β (1 β π) β β) |
132 | 37 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ ((((π β β β§ π₯ β (β
βm (1...π))
β§ π¦ β ((β
βm (1...π))
β {π₯})) β§ π β (β
βm (1...π))) β§ π β (0(,]1)) β π₯:(1...π)βΆβ) |
133 | 132 | ffvelcdmda 7039 |
. . . . . . . . . . . . . 14
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β (π₯βπ) β β) |
134 | 133 | recnd 11191 |
. . . . . . . . . . . . 13
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β (π₯βπ) β β) |
135 | 131, 134 | mulcld 11183 |
. . . . . . . . . . . 12
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β ((1 β π) Β· (π₯βπ)) β β) |
136 | 126, 135 | negsubd 11526 |
. . . . . . . . . . 11
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β ((π¦βπ) + -((1 β π) Β· (π₯βπ))) = ((π¦βπ) β ((1 β π) Β· (π₯βπ)))) |
137 | 131, 134 | mulneg1d 11616 |
. . . . . . . . . . . . 13
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β (-(1 β π) Β· (π₯βπ)) = -((1 β π) Β· (π₯βπ))) |
138 | 127, 130 | negsubdi2d 11536 |
. . . . . . . . . . . . . 14
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β -(1 β π) = (π β 1)) |
139 | 138 | oveq1d 7376 |
. . . . . . . . . . . . 13
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β (-(1 β π) Β· (π₯βπ)) = ((π β 1) Β· (π₯βπ))) |
140 | 137, 139 | eqtr3d 2775 |
. . . . . . . . . . . 12
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β -((1 β π) Β· (π₯βπ)) = ((π β 1) Β· (π₯βπ))) |
141 | 140 | oveq2d 7377 |
. . . . . . . . . . 11
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β ((π¦βπ) + -((1 β π) Β· (π₯βπ))) = ((π¦βπ) + ((π β 1) Β· (π₯βπ)))) |
142 | 136, 141 | eqtr3d 2775 |
. . . . . . . . . 10
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β ((π¦βπ) β ((1 β π) Β· (π₯βπ))) = ((π¦βπ) + ((π β 1) Β· (π₯βπ)))) |
143 | 142 | eqeq1d 2735 |
. . . . . . . . 9
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β (((π¦βπ) β ((1 β π) Β· (π₯βπ))) = (π Β· (πβπ)) β ((π¦βπ) + ((π β 1) Β· (π₯βπ))) = (π Β· (πβπ)))) |
144 | 54 | ad2antlr 726 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ π₯ β (β
βm (1...π))
β§ π¦ β ((β
βm (1...π))
β {π₯})) β§ π β (β
βm (1...π))) β§ π β (0(,]1)) β π:(1...π)βΆβ) |
145 | 144 | ffvelcdmda 7039 |
. . . . . . . . . . . 12
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β (πβπ) β β) |
146 | 145 | recnd 11191 |
. . . . . . . . . . 11
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β (πβπ) β β) |
147 | 130, 146 | mulcld 11183 |
. . . . . . . . . 10
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β (π Β· (πβπ)) β β) |
148 | 126, 135,
147 | subaddd 11538 |
. . . . . . . . 9
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β (((π¦βπ) β ((1 β π) Β· (π₯βπ))) = (π Β· (πβπ)) β (((1 β π) Β· (π₯βπ)) + (π Β· (πβπ))) = (π¦βπ))) |
149 | | eqcom 2740 |
. . . . . . . . . . 11
β’ ((((π¦βπ) + ((π β 1) Β· (π₯βπ))) / π) = (πβπ) β (πβπ) = (((π¦βπ) + ((π β 1) Β· (π₯βπ))) / π)) |
150 | 149 | a1i 11 |
. . . . . . . . . 10
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β ((((π¦βπ) + ((π β 1) Β· (π₯βπ))) / π) = (πβπ) β (πβπ) = (((π¦βπ) + ((π β 1) Β· (π₯βπ))) / π))) |
151 | 130, 127 | subcld 11520 |
. . . . . . . . . . . . 13
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β (π β 1) β β) |
152 | 151, 134 | mulcld 11183 |
. . . . . . . . . . . 12
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β ((π β 1) Β· (π₯βπ)) β β) |
153 | 126, 152 | addcld 11182 |
. . . . . . . . . . 11
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β ((π¦βπ) + ((π β 1) Β· (π₯βπ))) β β) |
154 | | elioc1 13315 |
. . . . . . . . . . . . . 14
β’ ((0
β β* β§ 1 β β*) β (π β (0(,]1) β (π β β*
β§ 0 < π β§ π β€ 1))) |
155 | 106, 13, 154 | mp2an 691 |
. . . . . . . . . . . . 13
β’ (π β (0(,]1) β (π β β*
β§ 0 < π β§ π β€ 1)) |
156 | 12 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π β β*
β 0 β β) |
157 | 156 | anim1i 616 |
. . . . . . . . . . . . . . 15
β’ ((π β β*
β§ 0 < π) β (0
β β β§ 0 < π)) |
158 | 157 | 3adant3 1133 |
. . . . . . . . . . . . . 14
β’ ((π β β*
β§ 0 < π β§ π β€ 1) β (0 β
β β§ 0 < π)) |
159 | | ltne 11260 |
. . . . . . . . . . . . . 14
β’ ((0
β β β§ 0 < π) β π β 0) |
160 | 158, 159 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β β*
β§ 0 < π β§ π β€ 1) β π β 0) |
161 | 155, 160 | sylbi 216 |
. . . . . . . . . . . 12
β’ (π β (0(,]1) β π β 0) |
162 | 161 | ad2antlr 726 |
. . . . . . . . . . 11
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β π β 0) |
163 | 153, 146,
130, 162 | divmul2d 11972 |
. . . . . . . . . 10
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β ((((π¦βπ) + ((π β 1) Β· (π₯βπ))) / π) = (πβπ) β ((π¦βπ) + ((π β 1) Β· (π₯βπ))) = (π Β· (πβπ)))) |
164 | 126, 152,
130, 162 | divdird 11977 |
. . . . . . . . . . . 12
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β (((π¦βπ) + ((π β 1) Β· (π₯βπ))) / π) = (((π¦βπ) / π) + (((π β 1) Β· (π₯βπ)) / π))) |
165 | 126, 130,
162 | divrec2d 11943 |
. . . . . . . . . . . . 13
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β ((π¦βπ) / π) = ((1 / π) Β· (π¦βπ))) |
166 | 151, 134,
130, 162 | div23d 11976 |
. . . . . . . . . . . . . 14
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β (((π β 1) Β· (π₯βπ)) / π) = (((π β 1) / π) Β· (π₯βπ))) |
167 | 130, 127,
130, 162 | divsubdird 11978 |
. . . . . . . . . . . . . . 15
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β ((π β 1) / π) = ((π / π) β (1 / π))) |
168 | 167 | oveq1d 7376 |
. . . . . . . . . . . . . 14
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β (((π β 1) / π) Β· (π₯βπ)) = (((π / π) β (1 / π)) Β· (π₯βπ))) |
169 | 166, 168 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β (((π β 1) Β· (π₯βπ)) / π) = (((π / π) β (1 / π)) Β· (π₯βπ))) |
170 | 165, 169 | oveq12d 7379 |
. . . . . . . . . . . 12
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β (((π¦βπ) / π) + (((π β 1) Β· (π₯βπ)) / π)) = (((1 / π) Β· (π¦βπ)) + (((π / π) β (1 / π)) Β· (π₯βπ)))) |
171 | 164, 170 | eqtrd 2773 |
. . . . . . . . . . 11
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β (((π¦βπ) + ((π β 1) Β· (π₯βπ))) / π) = (((1 / π) Β· (π¦βπ)) + (((π / π) β (1 / π)) Β· (π₯βπ)))) |
172 | 171 | eqeq2d 2744 |
. . . . . . . . . 10
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β ((πβπ) = (((π¦βπ) + ((π β 1) Β· (π₯βπ))) / π) β (πβπ) = (((1 / π) Β· (π¦βπ)) + (((π / π) β (1 / π)) Β· (π₯βπ))))) |
173 | 150, 163,
172 | 3bitr3d 309 |
. . . . . . . . 9
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β (((π¦βπ) + ((π β 1) Β· (π₯βπ))) = (π Β· (πβπ)) β (πβπ) = (((1 / π) Β· (π¦βπ)) + (((π / π) β (1 / π)) Β· (π₯βπ))))) |
174 | 143, 148,
173 | 3bitr3d 309 |
. . . . . . . 8
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β ((((1 β π) Β· (π₯βπ)) + (π Β· (πβπ))) = (π¦βπ) β (πβπ) = (((1 / π) Β· (π¦βπ)) + (((π / π) β (1 / π)) Β· (π₯βπ))))) |
175 | 123, 174 | bitrid 283 |
. . . . . . 7
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β ((π¦βπ) = (((1 β π) Β· (π₯βπ)) + (π Β· (πβπ))) β (πβπ) = (((1 / π) Β· (π¦βπ)) + (((π / π) β (1 / π)) Β· (π₯βπ))))) |
176 | 130, 162 | reccld 11932 |
. . . . . . . . . . 11
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β (1 / π) β β) |
177 | 176, 126 | mulcld 11183 |
. . . . . . . . . 10
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β ((1 / π) Β· (π¦βπ)) β β) |
178 | 127, 176 | subcld 11520 |
. . . . . . . . . . 11
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β (1 β (1 / π)) β β) |
179 | 178, 134 | mulcld 11183 |
. . . . . . . . . 10
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β ((1 β (1 / π)) Β· (π₯βπ)) β β) |
180 | 130, 162 | dividd 11937 |
. . . . . . . . . . . . 13
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β (π / π) = 1) |
181 | 180 | oveq1d 7376 |
. . . . . . . . . . . 12
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β ((π / π) β (1 / π)) = (1 β (1 / π))) |
182 | 181 | oveq1d 7376 |
. . . . . . . . . . 11
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β (((π / π) β (1 / π)) Β· (π₯βπ)) = ((1 β (1 / π)) Β· (π₯βπ))) |
183 | 182 | oveq2d 7377 |
. . . . . . . . . 10
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β (((1 / π) Β· (π¦βπ)) + (((π / π) β (1 / π)) Β· (π₯βπ))) = (((1 / π) Β· (π¦βπ)) + ((1 β (1 / π)) Β· (π₯βπ)))) |
184 | 177, 179,
183 | comraddd 11377 |
. . . . . . . . 9
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β (((1 / π) Β· (π¦βπ)) + (((π / π) β (1 / π)) Β· (π₯βπ))) = (((1 β (1 / π)) Β· (π₯βπ)) + ((1 / π) Β· (π¦βπ)))) |
185 | 184 | eqeq2d 2744 |
. . . . . . . 8
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β ((πβπ) = (((1 / π) Β· (π¦βπ)) + (((π / π) β (1 / π)) Β· (π₯βπ))) β (πβπ) = (((1 β (1 / π)) Β· (π₯βπ)) + ((1 / π) Β· (π¦βπ))))) |
186 | 185 | biimpd 228 |
. . . . . . 7
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β ((πβπ) = (((1 / π) Β· (π¦βπ)) + (((π / π) β (1 / π)) Β· (π₯βπ))) β (πβπ) = (((1 β (1 / π)) Β· (π₯βπ)) + ((1 / π) Β· (π¦βπ))))) |
187 | 175, 186 | sylbid 239 |
. . . . . 6
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§ π β (1...π)) β ((π¦βπ) = (((1 β π) Β· (π₯βπ)) + (π Β· (πβπ))) β (πβπ) = (((1 β (1 / π)) Β· (π₯βπ)) + ((1 / π) Β· (π¦βπ))))) |
188 | 187 | ralimdva 3161 |
. . . . 5
β’ ((((π β β β§ π₯ β (β
βm (1...π))
β§ π¦ β ((β
βm (1...π))
β {π₯})) β§ π β (β
βm (1...π))) β§ π β (0(,]1)) β (βπ β (1...π)(π¦βπ) = (((1 β π) Β· (π₯βπ)) + (π Β· (πβπ))) β βπ β (1...π)(πβπ) = (((1 β (1 / π)) Β· (π₯βπ)) + ((1 / π) Β· (π¦βπ))))) |
189 | 188 | imp 408 |
. . . 4
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§
βπ β (1...π)(π¦βπ) = (((1 β π) Β· (π₯βπ)) + (π Β· (πβπ)))) β βπ β (1...π)(πβπ) = (((1 β (1 / π)) Β· (π₯βπ)) + ((1 / π) Β· (π¦βπ)))) |
190 | 115, 122,
189 | rspcedvd 3585 |
. . 3
β’
(((((π β
β β§ π₯ β
(β βm (1...π)) β§ π¦ β ((β βm
(1...π)) β {π₯})) β§ π β (β βm
(1...π))) β§ π β (0(,]1)) β§
βπ β (1...π)(π¦βπ) = (((1 β π) Β· (π₯βπ)) + (π Β· (πβπ)))) β βπ‘ β β βπ β (1...π)(πβπ) = (((1 β π‘) Β· (π₯βπ)) + (π‘ Β· (π¦βπ)))) |
191 | 190 | rexlimdva2 3151 |
. 2
β’ (((π β β β§ π₯ β (β
βm (1...π))
β§ π¦ β ((β
βm (1...π))
β {π₯})) β§ π β (β
βm (1...π))) β (βπ β (0(,]1)βπ β (1...π)(π¦βπ) = (((1 β π) Β· (π₯βπ)) + (π Β· (πβπ))) β βπ‘ β β βπ β (1...π)(πβπ) = (((1 β π‘) Β· (π₯βπ)) + (π‘ Β· (π¦βπ))))) |
192 | 11, 105, 191 | 3jaod 1429 |
1
β’ (((π β β β§ π₯ β (β
βm (1...π))
β§ π¦ β ((β
βm (1...π))
β {π₯})) β§ π β (β
βm (1...π))) β ((βπ β (0[,]1)βπ β (1...π)(πβπ) = (((1 β π) Β· (π₯βπ)) + (π Β· (π¦βπ))) β¨ βπ β (0[,)1)βπ β (1...π)(π₯βπ) = (((1 β π) Β· (πβπ)) + (π Β· (π¦βπ))) β¨ βπ β (0(,]1)βπ β (1...π)(π¦βπ) = (((1 β π) Β· (π₯βπ)) + (π Β· (πβπ)))) β βπ‘ β β βπ β (1...π)(πβπ) = (((1 β π‘) Β· (π₯βπ)) + (π‘ Β· (π¦βπ))))) |