Step | Hyp | Ref
| Expression |
1 | | stoweidlem44.2 |
. . . 4
β’
β²π‘π |
2 | | stoweidlem44.5 |
. . . 4
β’ π = (π‘ β π β¦ ((1 / π) Β· Ξ£π β (1...π)((πΊβπ)βπ‘))) |
3 | | eqid 2733 |
. . . 4
β’ (π‘ β π β¦ Ξ£π β (1...π)((πΊβπ)βπ‘)) = (π‘ β π β¦ Ξ£π β (1...π)((πΊβπ)βπ‘)) |
4 | | eqid 2733 |
. . . 4
β’ (π‘ β π β¦ (1 / π)) = (π‘ β π β¦ (1 / π)) |
5 | | stoweidlem44.6 |
. . . 4
β’ (π β π β β) |
6 | 5 | nnrecred 12212 |
. . . 4
β’ (π β (1 / π) β β) |
7 | | stoweidlem44.7 |
. . . . 5
β’ (π β πΊ:(1...π)βΆπ) |
8 | | stoweidlem44.4 |
. . . . . 6
β’ π = {β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))} |
9 | | ssrab2 4041 |
. . . . . 6
β’ {β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))} β π΄ |
10 | 8, 9 | eqsstri 3982 |
. . . . 5
β’ π β π΄ |
11 | | fss 6689 |
. . . . 5
β’ ((πΊ:(1...π)βΆπ β§ π β π΄) β πΊ:(1...π)βΆπ΄) |
12 | 7, 10, 11 | sylancl 587 |
. . . 4
β’ (π β πΊ:(1...π)βΆπ΄) |
13 | | stoweidlem44.11 |
. . . 4
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) |
14 | | stoweidlem44.12 |
. . . 4
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) |
15 | | stoweidlem44.13 |
. . . 4
β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) |
16 | | stoweidlem44.3 |
. . . . 5
β’ πΎ = (topGenβran
(,)) |
17 | | stoweidlem44.9 |
. . . . 5
β’ π = βͺ
π½ |
18 | | eqid 2733 |
. . . . 5
β’ (π½ Cn πΎ) = (π½ Cn πΎ) |
19 | | stoweidlem44.10 |
. . . . . 6
β’ (π β π΄ β (π½ Cn πΎ)) |
20 | 19 | sselda 3948 |
. . . . 5
β’ ((π β§ π β π΄) β π β (π½ Cn πΎ)) |
21 | 16, 17, 18, 20 | fcnre 43322 |
. . . 4
β’ ((π β§ π β π΄) β π:πβΆβ) |
22 | 1, 2, 3, 4, 5, 6, 12, 13, 14, 15, 21 | stoweidlem32 44363 |
. . 3
β’ (π β π β π΄) |
23 | 8, 2, 5, 7, 21 | stoweidlem38 44369 |
. . . . . 6
β’ ((π β§ π‘ β π) β (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1)) |
24 | 23 | ex 414 |
. . . . 5
β’ (π β (π‘ β π β (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1))) |
25 | 1, 24 | ralrimi 3239 |
. . . 4
β’ (π β βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1)) |
26 | | stoweidlem44.14 |
. . . . 5
β’ (π β π β π) |
27 | 8, 2, 5, 7, 21, 26 | stoweidlem37 44368 |
. . . 4
β’ (π β (πβπ) = 0) |
28 | | stoweidlem44.1 |
. . . . . . . . 9
β’
β²ππ |
29 | | nfv 1918 |
. . . . . . . . 9
β’
β²π π‘ β (π β π) |
30 | 28, 29 | nfan 1903 |
. . . . . . . 8
β’
β²π(π β§ π‘ β (π β π)) |
31 | | nfv 1918 |
. . . . . . . 8
β’
β²π0 < ((1 /
π) Β· Ξ£π β (1...π)((πΊβπ)βπ‘)) |
32 | | stoweidlem44.8 |
. . . . . . . . . 10
β’ (π β βπ‘ β (π β π)βπ β (1...π)0 < ((πΊβπ)βπ‘)) |
33 | 32 | r19.21bi 3233 |
. . . . . . . . 9
β’ ((π β§ π‘ β (π β π)) β βπ β (1...π)0 < ((πΊβπ)βπ‘)) |
34 | | df-rex 3071 |
. . . . . . . . 9
β’
(βπ β
(1...π)0 < ((πΊβπ)βπ‘) β βπ(π β (1...π) β§ 0 < ((πΊβπ)βπ‘))) |
35 | 33, 34 | sylib 217 |
. . . . . . . 8
β’ ((π β§ π‘ β (π β π)) β βπ(π β (1...π) β§ 0 < ((πΊβπ)βπ‘))) |
36 | 6 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π‘ β (π β π)) β§ (π β (1...π) β§ 0 < ((πΊβπ)βπ‘))) β (1 / π) β β) |
37 | | simpll 766 |
. . . . . . . . . 10
β’ (((π β§ π‘ β (π β π)) β§ (π β (1...π) β§ 0 < ((πΊβπ)βπ‘))) β π) |
38 | | eldifi 4090 |
. . . . . . . . . . 11
β’ (π‘ β (π β π) β π‘ β π) |
39 | 38 | ad2antlr 726 |
. . . . . . . . . 10
β’ (((π β§ π‘ β (π β π)) β§ (π β (1...π) β§ 0 < ((πΊβπ)βπ‘))) β π‘ β π) |
40 | | fzfid 13887 |
. . . . . . . . . . 11
β’ ((π β§ π‘ β π) β (1...π) β Fin) |
41 | 8, 7, 21 | stoweidlem15 44346 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (1...π)) β§ π‘ β π) β (((πΊβπ)βπ‘) β β β§ 0 β€ ((πΊβπ)βπ‘) β§ ((πΊβπ)βπ‘) β€ 1)) |
42 | 41 | an32s 651 |
. . . . . . . . . . . 12
β’ (((π β§ π‘ β π) β§ π β (1...π)) β (((πΊβπ)βπ‘) β β β§ 0 β€ ((πΊβπ)βπ‘) β§ ((πΊβπ)βπ‘) β€ 1)) |
43 | 42 | simp1d 1143 |
. . . . . . . . . . 11
β’ (((π β§ π‘ β π) β§ π β (1...π)) β ((πΊβπ)βπ‘) β β) |
44 | 40, 43 | fsumrecl 15627 |
. . . . . . . . . 10
β’ ((π β§ π‘ β π) β Ξ£π β (1...π)((πΊβπ)βπ‘) β β) |
45 | 37, 39, 44 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ π‘ β (π β π)) β§ (π β (1...π) β§ 0 < ((πΊβπ)βπ‘))) β Ξ£π β (1...π)((πΊβπ)βπ‘) β β) |
46 | 5 | nnred 12176 |
. . . . . . . . . . 11
β’ (π β π β β) |
47 | 5 | nngt0d 12210 |
. . . . . . . . . . 11
β’ (π β 0 < π) |
48 | 46, 47 | recgt0d 12097 |
. . . . . . . . . 10
β’ (π β 0 < (1 / π)) |
49 | 48 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π‘ β (π β π)) β§ (π β (1...π) β§ 0 < ((πΊβπ)βπ‘))) β 0 < (1 / π)) |
50 | | 0red 11166 |
. . . . . . . . . . 11
β’ (((π β§ π‘ β (π β π)) β§ (π β (1...π) β§ 0 < ((πΊβπ)βπ‘))) β 0 β β) |
51 | | simprl 770 |
. . . . . . . . . . . . . 14
β’ (((π β§ π‘ β (π β π)) β§ (π β (1...π) β§ 0 < ((πΊβπ)βπ‘))) β π β (1...π)) |
52 | 37, 51, 39 | 3jca 1129 |
. . . . . . . . . . . . 13
β’ (((π β§ π‘ β (π β π)) β§ (π β (1...π) β§ 0 < ((πΊβπ)βπ‘))) β (π β§ π β (1...π) β§ π‘ β π)) |
53 | | snfi 8994 |
. . . . . . . . . . . . . . 15
β’ {π} β Fin |
54 | 53 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (1...π) β§ π‘ β π) β {π} β Fin) |
55 | | simpl1 1192 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (1...π) β§ π‘ β π) β§ π β {π}) β π) |
56 | | simpl3 1194 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (1...π) β§ π‘ β π) β§ π β {π}) β π‘ β π) |
57 | | elsni 4607 |
. . . . . . . . . . . . . . . . 17
β’ (π β {π} β π = π) |
58 | 57 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (1...π) β§ π‘ β π) β§ π β {π}) β π = π) |
59 | | simpl2 1193 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (1...π) β§ π‘ β π) β§ π β {π}) β π β (1...π)) |
60 | 58, 59 | eqeltrd 2834 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (1...π) β§ π‘ β π) β§ π β {π}) β π β (1...π)) |
61 | 55, 56, 60, 43 | syl21anc 837 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (1...π) β§ π‘ β π) β§ π β {π}) β ((πΊβπ)βπ‘) β β) |
62 | 54, 61 | fsumrecl 15627 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...π) β§ π‘ β π) β Ξ£π β {π} ((πΊβπ)βπ‘) β β) |
63 | 52, 62 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ π‘ β (π β π)) β§ (π β (1...π) β§ 0 < ((πΊβπ)βπ‘))) β Ξ£π β {π} ((πΊβπ)βπ‘) β β) |
64 | 50, 63 | readdcld 11192 |
. . . . . . . . . . 11
β’ (((π β§ π‘ β (π β π)) β§ (π β (1...π) β§ 0 < ((πΊβπ)βπ‘))) β (0 + Ξ£π β {π} ((πΊβπ)βπ‘)) β β) |
65 | | fzfi 13886 |
. . . . . . . . . . . . . . 15
β’
(1...π) β
Fin |
66 | | diffi 9129 |
. . . . . . . . . . . . . . 15
β’
((1...π) β Fin
β ((1...π) β
{π}) β
Fin) |
67 | 65, 66 | mp1i 13 |
. . . . . . . . . . . . . 14
β’ ((π β§ π‘ β π) β ((1...π) β {π}) β Fin) |
68 | | eldifi 4090 |
. . . . . . . . . . . . . . 15
β’ (π β ((1...π) β {π}) β π β (1...π)) |
69 | 68, 43 | sylan2 594 |
. . . . . . . . . . . . . 14
β’ (((π β§ π‘ β π) β§ π β ((1...π) β {π})) β ((πΊβπ)βπ‘) β β) |
70 | 67, 69 | fsumrecl 15627 |
. . . . . . . . . . . . 13
β’ ((π β§ π‘ β π) β Ξ£π β ((1...π) β {π})((πΊβπ)βπ‘) β β) |
71 | 37, 39, 70 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π β§ π‘ β (π β π)) β§ (π β (1...π) β§ 0 < ((πΊβπ)βπ‘))) β Ξ£π β ((1...π) β {π})((πΊβπ)βπ‘) β β) |
72 | 71, 63 | readdcld 11192 |
. . . . . . . . . . 11
β’ (((π β§ π‘ β (π β π)) β§ (π β (1...π) β§ 0 < ((πΊβπ)βπ‘))) β (Ξ£π β ((1...π) β {π})((πΊβπ)βπ‘) + Ξ£π β {π} ((πΊβπ)βπ‘)) β β) |
73 | | 00id 11338 |
. . . . . . . . . . . 12
β’ (0 + 0) =
0 |
74 | | simprr 772 |
. . . . . . . . . . . . . 14
β’ (((π β§ π‘ β (π β π)) β§ (π β (1...π) β§ 0 < ((πΊβπ)βπ‘))) β 0 < ((πΊβπ)βπ‘)) |
75 | 8, 7, 21 | stoweidlem15 44346 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (1...π)) β§ π‘ β π) β (((πΊβπ)βπ‘) β β β§ 0 β€ ((πΊβπ)βπ‘) β§ ((πΊβπ)βπ‘) β€ 1)) |
76 | 75 | simp1d 1143 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (1...π)) β§ π‘ β π) β ((πΊβπ)βπ‘) β β) |
77 | 37, 51, 39, 76 | syl21anc 837 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π‘ β (π β π)) β§ (π β (1...π) β§ 0 < ((πΊβπ)βπ‘))) β ((πΊβπ)βπ‘) β β) |
78 | 77 | recnd 11191 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π‘ β (π β π)) β§ (π β (1...π) β§ 0 < ((πΊβπ)βπ‘))) β ((πΊβπ)βπ‘) β β) |
79 | | fveq2 6846 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (πΊβπ) = (πΊβπ)) |
80 | 79 | fveq1d 6848 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ((πΊβπ)βπ‘) = ((πΊβπ)βπ‘)) |
81 | 80 | sumsn 15639 |
. . . . . . . . . . . . . . 15
β’ ((π β (1...π) β§ ((πΊβπ)βπ‘) β β) β Ξ£π β {π} ((πΊβπ)βπ‘) = ((πΊβπ)βπ‘)) |
82 | 51, 78, 81 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((π β§ π‘ β (π β π)) β§ (π β (1...π) β§ 0 < ((πΊβπ)βπ‘))) β Ξ£π β {π} ((πΊβπ)βπ‘) = ((πΊβπ)βπ‘)) |
83 | 74, 82 | breqtrrd 5137 |
. . . . . . . . . . . . 13
β’ (((π β§ π‘ β (π β π)) β§ (π β (1...π) β§ 0 < ((πΊβπ)βπ‘))) β 0 < Ξ£π β {π} ((πΊβπ)βπ‘)) |
84 | 50, 63, 50, 83 | ltadd2dd 11322 |
. . . . . . . . . . . 12
β’ (((π β§ π‘ β (π β π)) β§ (π β (1...π) β§ 0 < ((πΊβπ)βπ‘))) β (0 + 0) < (0 + Ξ£π β {π} ((πΊβπ)βπ‘))) |
85 | 73, 84 | eqbrtrrid 5145 |
. . . . . . . . . . 11
β’ (((π β§ π‘ β (π β π)) β§ (π β (1...π) β§ 0 < ((πΊβπ)βπ‘))) β 0 < (0 + Ξ£π β {π} ((πΊβπ)βπ‘))) |
86 | | 0red 11166 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...π) β§ π‘ β π) β 0 β β) |
87 | 70 | 3adant2 1132 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...π) β§ π‘ β π) β Ξ£π β ((1...π) β {π})((πΊβπ)βπ‘) β β) |
88 | | simpll 766 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π‘ β π) β§ π β ((1...π) β {π})) β π) |
89 | 68 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π‘ β π) β§ π β ((1...π) β {π})) β π β (1...π)) |
90 | | simplr 768 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π‘ β π) β§ π β ((1...π) β {π})) β π‘ β π) |
91 | 88, 89, 90, 41 | syl21anc 837 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π‘ β π) β§ π β ((1...π) β {π})) β (((πΊβπ)βπ‘) β β β§ 0 β€ ((πΊβπ)βπ‘) β§ ((πΊβπ)βπ‘) β€ 1)) |
92 | 91 | simp2d 1144 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π‘ β π) β§ π β ((1...π) β {π})) β 0 β€ ((πΊβπ)βπ‘)) |
93 | 67, 69, 92 | fsumge0 15688 |
. . . . . . . . . . . . . 14
β’ ((π β§ π‘ β π) β 0 β€ Ξ£π β ((1...π) β {π})((πΊβπ)βπ‘)) |
94 | 93 | 3adant2 1132 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...π) β§ π‘ β π) β 0 β€ Ξ£π β ((1...π) β {π})((πΊβπ)βπ‘)) |
95 | 86, 87, 62, 94 | leadd1dd 11777 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...π) β§ π‘ β π) β (0 + Ξ£π β {π} ((πΊβπ)βπ‘)) β€ (Ξ£π β ((1...π) β {π})((πΊβπ)βπ‘) + Ξ£π β {π} ((πΊβπ)βπ‘))) |
96 | 52, 95 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ π‘ β (π β π)) β§ (π β (1...π) β§ 0 < ((πΊβπ)βπ‘))) β (0 + Ξ£π β {π} ((πΊβπ)βπ‘)) β€ (Ξ£π β ((1...π) β {π})((πΊβπ)βπ‘) + Ξ£π β {π} ((πΊβπ)βπ‘))) |
97 | 50, 64, 72, 85, 96 | ltletrd 11323 |
. . . . . . . . . 10
β’ (((π β§ π‘ β (π β π)) β§ (π β (1...π) β§ 0 < ((πΊβπ)βπ‘))) β 0 < (Ξ£π β ((1...π) β {π})((πΊβπ)βπ‘) + Ξ£π β {π} ((πΊβπ)βπ‘))) |
98 | | eldifn 4091 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β ((1...π) β {π}) β Β¬ π₯ β {π}) |
99 | | imnan 401 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β ((1...π) β {π}) β Β¬ π₯ β {π}) β Β¬ (π₯ β ((1...π) β {π}) β§ π₯ β {π})) |
100 | 98, 99 | mpbi 229 |
. . . . . . . . . . . . . . 15
β’ Β¬
(π₯ β ((1...π) β {π}) β§ π₯ β {π}) |
101 | | elin 3930 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (((1...π) β {π}) β© {π}) β (π₯ β ((1...π) β {π}) β§ π₯ β {π})) |
102 | 100, 101 | mtbir 323 |
. . . . . . . . . . . . . 14
β’ Β¬
π₯ β (((1...π) β {π}) β© {π}) |
103 | 102 | nel0 4314 |
. . . . . . . . . . . . 13
β’
(((1...π) β
{π}) β© {π}) = β
|
104 | 103 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...π) β§ π‘ β π) β (((1...π) β {π}) β© {π}) = β
) |
105 | | undif1 4439 |
. . . . . . . . . . . . 13
β’
(((1...π) β
{π}) βͺ {π}) = ((1...π) βͺ {π}) |
106 | | snssi 4772 |
. . . . . . . . . . . . . . 15
β’ (π β (1...π) β {π} β (1...π)) |
107 | 106 | 3ad2ant2 1135 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (1...π) β§ π‘ β π) β {π} β (1...π)) |
108 | | ssequn2 4147 |
. . . . . . . . . . . . . 14
β’ ({π} β (1...π) β ((1...π) βͺ {π}) = (1...π)) |
109 | 107, 108 | sylib 217 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...π) β§ π‘ β π) β ((1...π) βͺ {π}) = (1...π)) |
110 | 105, 109 | eqtr2id 2786 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...π) β§ π‘ β π) β (1...π) = (((1...π) β {π}) βͺ {π})) |
111 | | fzfid 13887 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...π) β§ π‘ β π) β (1...π) β Fin) |
112 | 43 | 3adantl2 1168 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (1...π) β§ π‘ β π) β§ π β (1...π)) β ((πΊβπ)βπ‘) β β) |
113 | 112 | recnd 11191 |
. . . . . . . . . . . 12
β’ (((π β§ π β (1...π) β§ π‘ β π) β§ π β (1...π)) β ((πΊβπ)βπ‘) β β) |
114 | 104, 110,
111, 113 | fsumsplit 15634 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...π) β§ π‘ β π) β Ξ£π β (1...π)((πΊβπ)βπ‘) = (Ξ£π β ((1...π) β {π})((πΊβπ)βπ‘) + Ξ£π β {π} ((πΊβπ)βπ‘))) |
115 | 52, 114 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π‘ β (π β π)) β§ (π β (1...π) β§ 0 < ((πΊβπ)βπ‘))) β Ξ£π β (1...π)((πΊβπ)βπ‘) = (Ξ£π β ((1...π) β {π})((πΊβπ)βπ‘) + Ξ£π β {π} ((πΊβπ)βπ‘))) |
116 | 97, 115 | breqtrrd 5137 |
. . . . . . . . 9
β’ (((π β§ π‘ β (π β π)) β§ (π β (1...π) β§ 0 < ((πΊβπ)βπ‘))) β 0 < Ξ£π β (1...π)((πΊβπ)βπ‘)) |
117 | 36, 45, 49, 116 | mulgt0d 11318 |
. . . . . . . 8
β’ (((π β§ π‘ β (π β π)) β§ (π β (1...π) β§ 0 < ((πΊβπ)βπ‘))) β 0 < ((1 / π) Β· Ξ£π β (1...π)((πΊβπ)βπ‘))) |
118 | 30, 31, 35, 117 | exlimdd 2214 |
. . . . . . 7
β’ ((π β§ π‘ β (π β π)) β 0 < ((1 / π) Β· Ξ£π β (1...π)((πΊβπ)βπ‘))) |
119 | 8, 2, 5, 7, 21 | stoweidlem30 44361 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β (πβπ‘) = ((1 / π) Β· Ξ£π β (1...π)((πΊβπ)βπ‘))) |
120 | 38, 119 | sylan2 594 |
. . . . . . 7
β’ ((π β§ π‘ β (π β π)) β (πβπ‘) = ((1 / π) Β· Ξ£π β (1...π)((πΊβπ)βπ‘))) |
121 | 118, 120 | breqtrrd 5137 |
. . . . . 6
β’ ((π β§ π‘ β (π β π)) β 0 < (πβπ‘)) |
122 | 121 | ex 414 |
. . . . 5
β’ (π β (π‘ β (π β π) β 0 < (πβπ‘))) |
123 | 1, 122 | ralrimi 3239 |
. . . 4
β’ (π β βπ‘ β (π β π)0 < (πβπ‘)) |
124 | 25, 27, 123 | 3jca 1129 |
. . 3
β’ (π β (βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β§ (πβπ) = 0 β§ βπ‘ β (π β π)0 < (πβπ‘))) |
125 | | eleq1 2822 |
. . . . . 6
β’ (π = π β (π β π΄ β π β π΄)) |
126 | | nfmpt1 5217 |
. . . . . . . . . 10
β’
β²π‘(π‘ β π β¦ ((1 / π) Β· Ξ£π β (1...π)((πΊβπ)βπ‘))) |
127 | 2, 126 | nfcxfr 2902 |
. . . . . . . . 9
β’
β²π‘π |
128 | 127 | nfeq2 2921 |
. . . . . . . 8
β’
β²π‘ π = π |
129 | | fveq1 6845 |
. . . . . . . . . 10
β’ (π = π β (πβπ‘) = (πβπ‘)) |
130 | 129 | breq2d 5121 |
. . . . . . . . 9
β’ (π = π β (0 β€ (πβπ‘) β 0 β€ (πβπ‘))) |
131 | 129 | breq1d 5119 |
. . . . . . . . 9
β’ (π = π β ((πβπ‘) β€ 1 β (πβπ‘) β€ 1)) |
132 | 130, 131 | anbi12d 632 |
. . . . . . . 8
β’ (π = π β ((0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1))) |
133 | 128, 132 | ralbid 3255 |
. . . . . . 7
β’ (π = π β (βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1))) |
134 | | fveq1 6845 |
. . . . . . . 8
β’ (π = π β (πβπ) = (πβπ)) |
135 | 134 | eqeq1d 2735 |
. . . . . . 7
β’ (π = π β ((πβπ) = 0 β (πβπ) = 0)) |
136 | 129 | breq2d 5121 |
. . . . . . . 8
β’ (π = π β (0 < (πβπ‘) β 0 < (πβπ‘))) |
137 | 128, 136 | ralbid 3255 |
. . . . . . 7
β’ (π = π β (βπ‘ β (π β π)0 < (πβπ‘) β βπ‘ β (π β π)0 < (πβπ‘))) |
138 | 133, 135,
137 | 3anbi123d 1437 |
. . . . . 6
β’ (π = π β ((βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β§ (πβπ) = 0 β§ βπ‘ β (π β π)0 < (πβπ‘)) β (βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β§ (πβπ) = 0 β§ βπ‘ β (π β π)0 < (πβπ‘)))) |
139 | 125, 138 | anbi12d 632 |
. . . . 5
β’ (π = π β ((π β π΄ β§ (βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β§ (πβπ) = 0 β§ βπ‘ β (π β π)0 < (πβπ‘))) β (π β π΄ β§ (βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β§ (πβπ) = 0 β§ βπ‘ β (π β π)0 < (πβπ‘))))) |
140 | 139 | spcegv 3558 |
. . . 4
β’ (π β π΄ β ((π β π΄ β§ (βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β§ (πβπ) = 0 β§ βπ‘ β (π β π)0 < (πβπ‘))) β βπ(π β π΄ β§ (βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β§ (πβπ) = 0 β§ βπ‘ β (π β π)0 < (πβπ‘))))) |
141 | 22, 140 | syl 17 |
. . 3
β’ (π β ((π β π΄ β§ (βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β§ (πβπ) = 0 β§ βπ‘ β (π β π)0 < (πβπ‘))) β βπ(π β π΄ β§ (βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β§ (πβπ) = 0 β§ βπ‘ β (π β π)0 < (πβπ‘))))) |
142 | 22, 124, 141 | mp2and 698 |
. 2
β’ (π β βπ(π β π΄ β§ (βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β§ (πβπ) = 0 β§ βπ‘ β (π β π)0 < (πβπ‘)))) |
143 | | df-rex 3071 |
. 2
β’
(βπ β
π΄ (βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β§ (πβπ) = 0 β§ βπ‘ β (π β π)0 < (πβπ‘)) β βπ(π β π΄ β§ (βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β§ (πβπ) = 0 β§ βπ‘ β (π β π)0 < (πβπ‘)))) |
144 | 142, 143 | sylibr 233 |
1
β’ (π β βπ β π΄ (βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β§ (πβπ) = 0 β§ βπ‘ β (π β π)0 < (πβπ‘))) |