Step | Hyp | Ref
| Expression |
1 | | stoweidlem59.8 |
. . . . . . . . . 10
β’ π = {π¦ β π΄ β£ βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1)} |
2 | | nfrab1 3425 |
. . . . . . . . . 10
β’
β²π¦{π¦ β π΄ β£ βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1)} |
3 | 1, 2 | nfcxfr 2904 |
. . . . . . . . 9
β’
β²π¦π |
4 | | nfcv 2906 |
. . . . . . . . 9
β’
β²π§π |
5 | | nfv 1918 |
. . . . . . . . 9
β’
β²π§(βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘)) |
6 | | nfv 1918 |
. . . . . . . . 9
β’
β²π¦(βπ‘ β (π·βπ)(π§βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π§βπ‘)) |
7 | | fveq1 6837 |
. . . . . . . . . . . 12
β’ (π¦ = π§ β (π¦βπ‘) = (π§βπ‘)) |
8 | 7 | breq1d 5114 |
. . . . . . . . . . 11
β’ (π¦ = π§ β ((π¦βπ‘) < (πΈ / π) β (π§βπ‘) < (πΈ / π))) |
9 | 8 | ralbidv 3173 |
. . . . . . . . . 10
β’ (π¦ = π§ β (βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π) β βπ‘ β (π·βπ)(π§βπ‘) < (πΈ / π))) |
10 | 7 | breq2d 5116 |
. . . . . . . . . . 11
β’ (π¦ = π§ β ((1 β (πΈ / π)) < (π¦βπ‘) β (1 β (πΈ / π)) < (π§βπ‘))) |
11 | 10 | ralbidv 3173 |
. . . . . . . . . 10
β’ (π¦ = π§ β (βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘) β βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π§βπ‘))) |
12 | 9, 11 | anbi12d 632 |
. . . . . . . . 9
β’ (π¦ = π§ β ((βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘)) β (βπ‘ β (π·βπ)(π§βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π§βπ‘)))) |
13 | 3, 4, 5, 6, 12 | cbvrabw 3438 |
. . . . . . . 8
β’ {π¦ β π β£ (βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘))} = {π§ β π β£ (βπ‘ β (π·βπ)(π§βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π§βπ‘))} |
14 | | ovexd 7385 |
. . . . . . . . . 10
β’ (π β (π½ Cn πΎ) β V) |
15 | | stoweidlem59.11 |
. . . . . . . . . . 11
β’ (π β π΄ β πΆ) |
16 | | stoweidlem59.5 |
. . . . . . . . . . 11
β’ πΆ = (π½ Cn πΎ) |
17 | 15, 16 | sseqtrdi 3993 |
. . . . . . . . . 10
β’ (π β π΄ β (π½ Cn πΎ)) |
18 | 14, 17 | ssexd 5280 |
. . . . . . . . 9
β’ (π β π΄ β V) |
19 | 1, 18 | rabexd 5289 |
. . . . . . . 8
β’ (π β π β V) |
20 | 13, 19 | rabexd 5289 |
. . . . . . 7
β’ (π β {π¦ β π β£ (βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘))} β V) |
21 | 20 | ralrimivw 3146 |
. . . . . 6
β’ (π β βπ β (0...π){π¦ β π β£ (βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘))} β V) |
22 | | stoweidlem59.9 |
. . . . . . 7
β’ π» = (π β (0...π) β¦ {π¦ β π β£ (βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘))}) |
23 | 22 | fnmpt 6637 |
. . . . . 6
β’
(βπ β
(0...π){π¦ β π β£ (βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘))} β V β π» Fn (0...π)) |
24 | 21, 23 | syl 17 |
. . . . 5
β’ (π β π» Fn (0...π)) |
25 | | fzfi 13806 |
. . . . 5
β’
(0...π) β
Fin |
26 | | fnfi 9059 |
. . . . 5
β’ ((π» Fn (0...π) β§ (0...π) β Fin) β π» β Fin) |
27 | 24, 25, 26 | sylancl 587 |
. . . 4
β’ (π β π» β Fin) |
28 | | rnfi 9213 |
. . . 4
β’ (π» β Fin β ran π» β Fin) |
29 | 27, 28 | syl 17 |
. . 3
β’ (π β ran π» β Fin) |
30 | | fnchoice 42967 |
. . 3
β’ (ran
π» β Fin β
ββ(β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) |
31 | 29, 30 | syl 17 |
. 2
β’ (π β ββ(β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) |
32 | | simprl 770 |
. . . . 5
β’ ((π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) β β Fn ran π») |
33 | | ovex 7383 |
. . . . . . . 8
β’
(0...π) β
V |
34 | 33 | mptex 7168 |
. . . . . . 7
β’ (π β (0...π) β¦ {π¦ β π β£ (βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘))}) β V |
35 | 22, 34 | eqeltri 2835 |
. . . . . 6
β’ π» β V |
36 | 35 | rnex 7840 |
. . . . 5
β’ ran π» β V |
37 | | fnex 7162 |
. . . . 5
β’ ((β Fn ran π» β§ ran π» β V) β β β V) |
38 | 32, 36, 37 | sylancl 587 |
. . . 4
β’ ((π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) β β β V) |
39 | | coexg 7857 |
. . . 4
β’ ((β β V β§ π» β V) β (β β π») β V) |
40 | 38, 35, 39 | sylancl 587 |
. . 3
β’ ((π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) β (β β π») β V) |
41 | | dffn3 6677 |
. . . . . . 7
β’ (β Fn ran π» β β:ran π»βΆran β) |
42 | 32, 41 | sylib 217 |
. . . . . 6
β’ ((π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) β β:ran π»βΆran β) |
43 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π€π |
44 | | nfv 1918 |
. . . . . . . . . . 11
β’
β²π€ β Fn ran π» |
45 | | nfra1 3266 |
. . . . . . . . . . 11
β’
β²π€βπ€ β ran π»(π€ β β
β (ββπ€) β π€) |
46 | 44, 45 | nfan 1903 |
. . . . . . . . . 10
β’
β²π€(β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€)) |
47 | 43, 46 | nfan 1903 |
. . . . . . . . 9
β’
β²π€(π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) |
48 | | simplrr 777 |
. . . . . . . . . . 11
β’ (((π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) β§ π€ β ran π») β βπ€ β ran π»(π€ β β
β (ββπ€) β π€)) |
49 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) β§ π€ β ran π») β π€ β ran π») |
50 | | fvelrnb 6899 |
. . . . . . . . . . . . . . . 16
β’ (π» Fn (0...π) β (π€ β ran π» β βπ β (0...π)(π»βπ) = π€)) |
51 | | nfv 1918 |
. . . . . . . . . . . . . . . . 17
β’
β²π(π»βπ) = π€ |
52 | | nfmpt1 5212 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π(π β (0...π) β¦ {π¦ β π β£ (βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘))}) |
53 | 22, 52 | nfcxfr 2904 |
. . . . . . . . . . . . . . . . . . 19
β’
β²ππ» |
54 | | nfcv 2906 |
. . . . . . . . . . . . . . . . . . 19
β’
β²ππ |
55 | 53, 54 | nffv 6848 |
. . . . . . . . . . . . . . . . . 18
β’
β²π(π»βπ) |
56 | | nfcv 2906 |
. . . . . . . . . . . . . . . . . 18
β’
β²ππ€ |
57 | 55, 56 | nfeq 2919 |
. . . . . . . . . . . . . . . . 17
β’
β²π(π»βπ) = π€ |
58 | | fveq2 6838 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (π»βπ) = (π»βπ)) |
59 | 58 | eqeq1d 2740 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β ((π»βπ) = π€ β (π»βπ) = π€)) |
60 | 51, 57, 59 | cbvrexw 3289 |
. . . . . . . . . . . . . . . 16
β’
(βπ β
(0...π)(π»βπ) = π€ β βπ β (0...π)(π»βπ) = π€) |
61 | 50, 60 | bitr4di 289 |
. . . . . . . . . . . . . . 15
β’ (π» Fn (0...π) β (π€ β ran π» β βπ β (0...π)(π»βπ) = π€)) |
62 | 24, 61 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β (π€ β ran π» β βπ β (0...π)(π»βπ) = π€)) |
63 | 62 | biimpa 478 |
. . . . . . . . . . . . 13
β’ ((π β§ π€ β ran π») β βπ β (0...π)(π»βπ) = π€) |
64 | | simp3 1139 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (0...π) β§ (π»βπ) = π€) β (π»βπ) = π€) |
65 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β (0...π)) β π β (0...π)) |
66 | 20 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β (0...π)) β {π¦ β π β£ (βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘))} β V) |
67 | 22 | fvmpt2 6955 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (0...π) β§ {π¦ β π β£ (βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘))} β V) β (π»βπ) = {π¦ β π β£ (βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘))}) |
68 | 65, 66, 67 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (0...π)) β (π»βπ) = {π¦ β π β£ (βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘))}) |
69 | | stoweidlem59.6 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ π· = (π β (0...π) β¦ {π‘ β π β£ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)}) |
70 | | nfcv 2906 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
β²π‘(0...π) |
71 | | nfrab1 3425 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
β²π‘{π‘ β π β£ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)} |
72 | 70, 71 | nfmpt 5211 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
β²π‘(π β (0...π) β¦ {π‘ β π β£ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)}) |
73 | 69, 72 | nfcxfr 2904 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β²π‘π· |
74 | | nfcv 2906 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β²π‘π |
75 | 73, 74 | nffv 6848 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β²π‘(π·βπ) |
76 | | nfcv 2906 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β²π‘π |
77 | | stoweidlem59.7 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ π΅ = (π β (0...π) β¦ {π‘ β π β£ ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ‘)}) |
78 | | nfrab1 3425 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
β²π‘{π‘ β π β£ ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ‘)} |
79 | 70, 78 | nfmpt 5211 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
β²π‘(π β (0...π) β¦ {π‘ β π β£ ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ‘)}) |
80 | 77, 79 | nfcxfr 2904 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
β²π‘π΅ |
81 | 80, 74 | nffv 6848 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β²π‘(π΅βπ) |
82 | 76, 81 | nfdif 4084 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β²π‘(π β (π΅βπ)) |
83 | | stoweidlem59.2 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β²π‘π |
84 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β²π‘ π β (0...π) |
85 | 83, 84 | nfan 1903 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β²π‘(π β§ π β (0...π)) |
86 | | stoweidlem59.3 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ πΎ = (topGenβran
(,)) |
87 | | stoweidlem59.4 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ π = βͺ
π½ |
88 | | stoweidlem59.10 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β π½ β Comp) |
89 | 88 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β (0...π)) β π½ β Comp) |
90 | 15 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β (0...π)) β π΄ β πΆ) |
91 | | stoweidlem59.12 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) |
92 | 91 | 3adant1r 1178 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π β (0...π)) β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) |
93 | | stoweidlem59.13 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) |
94 | 93 | 3adant1r 1178 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π β (0...π)) β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) |
95 | | stoweidlem59.14 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π¦ β β) β (π‘ β π β¦ π¦) β π΄) |
96 | 95 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π β (0...π)) β§ π¦ β β) β (π‘ β π β¦ π¦) β π΄) |
97 | | stoweidlem59.15 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘)) |
98 | 97 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π β (0...π)) β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘)) |
99 | 88 | uniexd 7670 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β βͺ π½
β V) |
100 | 87, 99 | eqeltrid 2843 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β π β V) |
101 | 100 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π β (0...π)) β π β V) |
102 | | rabexg 5287 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β V β {π‘ β π β£ ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ‘)} β V) |
103 | 101, 102 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π β (0...π)) β {π‘ β π β£ ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ‘)} β V) |
104 | 77 | fvmpt2 6955 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β (0...π) β§ {π‘ β π β£ ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ‘)} β V) β (π΅βπ) = {π‘ β π β£ ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ‘)}) |
105 | 65, 103, 104 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π β (0...π)) β (π΅βπ) = {π‘ β π β£ ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ‘)}) |
106 | | stoweidlem59.1 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
β²π‘πΉ |
107 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ {π‘ β π β£ ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ‘)} = {π‘ β π β£ ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ‘)} |
108 | | elfzelz 13370 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β (0...π) β π β β€) |
109 | 108 | zred 12540 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (0...π) β π β β) |
110 | | 3re 12167 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ 3 β
β |
111 | | 3ne0 12193 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ 3 β
0 |
112 | 110, 111 | rereccli 11854 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (1 / 3)
β β |
113 | | readdcl 11068 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β β β§ (1 / 3)
β β) β (π +
(1 / 3)) β β) |
114 | 109, 112,
113 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β (0...π) β (π + (1 / 3)) β β) |
115 | 114 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π β (0...π)) β (π + (1 / 3)) β β) |
116 | | stoweidlem59.17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β πΈ β
β+) |
117 | 116 | rpred 12886 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β πΈ β β) |
118 | 117 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π β (0...π)) β πΈ β β) |
119 | 115, 118 | remulcld 11119 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π β (0...π)) β ((π + (1 / 3)) Β· πΈ) β β) |
120 | | stoweidlem59.16 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β πΉ β πΆ) |
121 | 120, 16 | eleqtrdi 2849 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β πΉ β (π½ Cn πΎ)) |
122 | 121 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π β (0...π)) β πΉ β (π½ Cn πΎ)) |
123 | 106, 86, 87, 107, 119, 122 | rfcnpre3 42971 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π β (0...π)) β {π‘ β π β£ ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ‘)} β (Clsdβπ½)) |
124 | 105, 123 | eqeltrd 2839 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β (0...π)) β (π΅βπ) β (Clsdβπ½)) |
125 | | rabexg 5287 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β V β {π‘ β π β£ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)} β V) |
126 | 101, 125 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π β (0...π)) β {π‘ β π β£ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)} β V) |
127 | 69 | fvmpt2 6955 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β (0...π) β§ {π‘ β π β£ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)} β V) β (π·βπ) = {π‘ β π β£ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)}) |
128 | 65, 126, 127 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π β (0...π)) β (π·βπ) = {π‘ β π β£ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)}) |
129 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ {π‘ β π β£ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)} = {π‘ β π β£ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)} |
130 | | resubcl 11399 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β β β§ (1 / 3)
β β) β (π
β (1 / 3)) β β) |
131 | 109, 112,
130 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β (0...π) β (π β (1 / 3)) β
β) |
132 | 131 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π β (0...π)) β (π β (1 / 3)) β
β) |
133 | 132, 118 | remulcld 11119 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π β (0...π)) β ((π β (1 / 3)) Β· πΈ) β β) |
134 | 106, 86, 87, 129, 133, 122 | rfcnpre4 42972 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π β (0...π)) β {π‘ β π β£ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)} β (Clsdβπ½)) |
135 | 128, 134 | eqeltrd 2839 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β (0...π)) β (π·βπ) β (Clsdβπ½)) |
136 | 133 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π β§ π β (0...π)) β§ π‘ β (π΅βπ)) β ((π β (1 / 3)) Β· πΈ) β β) |
137 | 119 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π β§ π β (0...π)) β§ π‘ β (π΅βπ)) β ((π + (1 / 3)) Β· πΈ) β β) |
138 | 86, 87, 16, 120 | fcnre 42963 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π β πΉ:πβΆβ) |
139 | 138 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((π β§ π β (0...π)) β§ π‘ β (π΅βπ)) β πΉ:πβΆβ) |
140 | | ssrab2 4036 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ {π‘ β π β£ ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ‘)} β π |
141 | 105, 140 | eqsstrdi 3997 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π β§ π β (0...π)) β (π΅βπ) β π) |
142 | 141 | sselda 3943 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((π β§ π β (0...π)) β§ π‘ β (π΅βπ)) β π‘ β π) |
143 | 139, 142 | ffvelcdmd 7031 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π β§ π β (0...π)) β§ π‘ β (π΅βπ)) β (πΉβπ‘) β β) |
144 | 112, 130 | mpan2 690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π β β β (π β (1 / 3)) β
β) |
145 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π β β β π β
β) |
146 | 112, 113 | mpan2 690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π β β β (π + (1 / 3)) β
β) |
147 | | 3pos 12192 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ 0 <
3 |
148 | 110, 147 | recgt0ii 11995 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ 0 < (1
/ 3) |
149 | 112, 148 | elrpii 12847 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (1 / 3)
β β+ |
150 | | ltsubrp 12880 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((π β β β§ (1 / 3)
β β+) β (π β (1 / 3)) < π) |
151 | 149, 150 | mpan2 690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π β β β (π β (1 / 3)) < π) |
152 | | ltaddrp 12881 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((π β β β§ (1 / 3)
β β+) β π < (π + (1 / 3))) |
153 | 149, 152 | mpan2 690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π β β β π < (π + (1 / 3))) |
154 | 144, 145,
146, 151, 153 | lttrd 11250 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π β β β (π β (1 / 3)) < (π + (1 / 3))) |
155 | 109, 154 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π β (0...π) β (π β (1 / 3)) < (π + (1 / 3))) |
156 | 155 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π β§ π β (0...π)) β (π β (1 / 3)) < (π + (1 / 3))) |
157 | 116 | rpregt0d 12892 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π β (πΈ β β β§ 0 < πΈ)) |
158 | 157 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π β§ π β (0...π)) β (πΈ β β β§ 0 < πΈ)) |
159 | | ltmul1 11939 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (((π β (1 / 3)) β β
β§ (π + (1 / 3)) β
β β§ (πΈ β
β β§ 0 < πΈ))
β ((π β (1 / 3))
< (π + (1 / 3)) β
((π β (1 / 3))
Β· πΈ) < ((π + (1 / 3)) Β· πΈ))) |
160 | 132, 115,
158, 159 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π β§ π β (0...π)) β ((π β (1 / 3)) < (π + (1 / 3)) β ((π β (1 / 3)) Β· πΈ) < ((π + (1 / 3)) Β· πΈ))) |
161 | 156, 160 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β§ π β (0...π)) β ((π β (1 / 3)) Β· πΈ) < ((π + (1 / 3)) Β· πΈ)) |
162 | 161 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π β§ π β (0...π)) β§ π‘ β (π΅βπ)) β ((π β (1 / 3)) Β· πΈ) < ((π + (1 / 3)) Β· πΈ)) |
163 | 105 | eleq2d 2824 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π β§ π β (0...π)) β (π‘ β (π΅βπ) β π‘ β {π‘ β π β£ ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ‘)})) |
164 | 163 | biimpa 478 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((π β§ π β (0...π)) β§ π‘ β (π΅βπ)) β π‘ β {π‘ β π β£ ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ‘)}) |
165 | | rabid 3426 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π‘ β {π‘ β π β£ ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ‘)} β (π‘ β π β§ ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ‘))) |
166 | 164, 165 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((π β§ π β (0...π)) β§ π‘ β (π΅βπ)) β (π‘ β π β§ ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ‘))) |
167 | 166 | simprd 497 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π β§ π β (0...π)) β§ π‘ β (π΅βπ)) β ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ‘)) |
168 | 136, 137,
143, 162, 167 | ltletrd 11249 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β§ π β (0...π)) β§ π‘ β (π΅βπ)) β ((π β (1 / 3)) Β· πΈ) < (πΉβπ‘)) |
169 | 136, 143 | ltnled 11236 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β§ π β (0...π)) β§ π‘ β (π΅βπ)) β (((π β (1 / 3)) Β· πΈ) < (πΉβπ‘) β Β¬ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ))) |
170 | 168, 169 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ π β (0...π)) β§ π‘ β (π΅βπ)) β Β¬ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)) |
171 | 170 | intnand 490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ π β (0...π)) β§ π‘ β (π΅βπ)) β Β¬ (π‘ β π β§ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ))) |
172 | | rabid 3426 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π‘ β {π‘ β π β£ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)} β (π‘ β π β§ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ))) |
173 | 171, 172 | sylnibr 329 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ π β (0...π)) β§ π‘ β (π΅βπ)) β Β¬ π‘ β {π‘ β π β£ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)}) |
174 | 128 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ π β (0...π)) β§ π‘ β (π΅βπ)) β (π·βπ) = {π‘ β π β£ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)}) |
175 | 173, 174 | neleqtrrd 2861 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π β (0...π)) β§ π‘ β (π΅βπ)) β Β¬ π‘ β (π·βπ)) |
176 | 175 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π β (0...π)) β (π‘ β (π΅βπ) β Β¬ π‘ β (π·βπ))) |
177 | 85, 176 | ralrimi 3239 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π β (0...π)) β βπ‘ β (π΅βπ) Β¬ π‘ β (π·βπ)) |
178 | | disj 4406 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π΅βπ) β© (π·βπ)) = β
β βπ β (π΅βπ) Β¬ π β (π·βπ)) |
179 | | nfcv 2906 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
β²π(π΅βπ) |
180 | 75 | nfcri 2893 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
β²π‘ π β (π·βπ) |
181 | 180 | nfn 1861 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
β²π‘ Β¬ π β (π·βπ) |
182 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
β²π Β¬ π‘ β (π·βπ) |
183 | | eleq1 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π = π‘ β (π β (π·βπ) β π‘ β (π·βπ))) |
184 | 183 | notbid 318 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π = π‘ β (Β¬ π β (π·βπ) β Β¬ π‘ β (π·βπ))) |
185 | 179, 81, 181, 182, 184 | cbvralfw 3286 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(βπ β
(π΅βπ) Β¬ π β (π·βπ) β βπ‘ β (π΅βπ) Β¬ π‘ β (π·βπ)) |
186 | 178, 185 | bitri 275 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π΅βπ) β© (π·βπ)) = β
β βπ‘ β (π΅βπ) Β¬ π‘ β (π·βπ)) |
187 | 177, 186 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β (0...π)) β ((π΅βπ) β© (π·βπ)) = β
) |
188 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (π΅βπ)) = (π β (π΅βπ)) |
189 | | stoweidlem59.19 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β π β β) |
190 | 189 | nnrpd 12884 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β π β
β+) |
191 | 116, 190 | rpdivcld 12903 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (πΈ / π) β
β+) |
192 | 191 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β (0...π)) β (πΈ / π) β
β+) |
193 | 117, 189 | nndivred 12141 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (πΈ / π) β β) |
194 | 112 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (1 / 3) β
β) |
195 | 189 | nnge1d 12135 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β 1 β€ π) |
196 | | 1re 11089 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ 1 β
β |
197 | | 0lt1 11611 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ 0 <
1 |
198 | 196, 197 | pm3.2i 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (1 β
β β§ 0 < 1) |
199 | 198 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (1 β β β§ 0
< 1)) |
200 | 189 | nnred 12102 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β π β β) |
201 | 189 | nngt0d 12136 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β 0 < π) |
202 | | lediv2 11979 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((1
β β β§ 0 < 1) β§ (π β β β§ 0 < π) β§ (πΈ β β β§ 0 < πΈ)) β (1 β€ π β (πΈ / π) β€ (πΈ / 1))) |
203 | 199, 200,
201, 157, 202 | syl121anc 1376 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β (1 β€ π β (πΈ / π) β€ (πΈ / 1))) |
204 | 195, 203 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (πΈ / π) β€ (πΈ / 1)) |
205 | 116 | rpcnd 12888 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β πΈ β β) |
206 | 205 | div1d 11857 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (πΈ / 1) = πΈ) |
207 | 204, 206 | breqtrd 5130 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (πΈ / π) β€ πΈ) |
208 | | stoweidlem59.18 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β πΈ < (1 / 3)) |
209 | 193, 117,
194, 207, 208 | lelttrd 11247 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (πΈ / π) < (1 / 3)) |
210 | 209 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β (0...π)) β (πΈ / π) < (1 / 3)) |
211 | 75, 82, 85, 86, 87, 16, 89, 90, 92, 94, 96, 98, 124, 135, 187, 188, 192, 210 | stoweidlem58 44009 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β (0...π)) β βπ₯ β π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β (π·βπ)(π₯βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π₯βπ‘))) |
212 | | df-rex 3073 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(βπ₯ β
π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β (π·βπ)(π₯βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π₯βπ‘)) β βπ₯(π₯ β π΄ β§ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β (π·βπ)(π₯βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π₯βπ‘)))) |
213 | 211, 212 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β (0...π)) β βπ₯(π₯ β π΄ β§ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β (π·βπ)(π₯βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π₯βπ‘)))) |
214 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π β (0...π)) β§ (π₯ β π΄ β§ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β (π·βπ)(π₯βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π₯βπ‘)))) β π₯ β π΄) |
215 | | simprr1 1222 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π β (0...π)) β§ (π₯ β π΄ β§ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β (π·βπ)(π₯βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π₯βπ‘)))) β βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1)) |
216 | | fveq1 6837 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π¦ = π₯ β (π¦βπ‘) = (π₯βπ‘)) |
217 | 216 | breq2d 5116 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π¦ = π₯ β (0 β€ (π¦βπ‘) β 0 β€ (π₯βπ‘))) |
218 | 216 | breq1d 5114 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π¦ = π₯ β ((π¦βπ‘) β€ 1 β (π₯βπ‘) β€ 1)) |
219 | 217, 218 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π¦ = π₯ β ((0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1) β (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1))) |
220 | 219 | ralbidv 3173 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π¦ = π₯ β (βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1) β βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1))) |
221 | 220, 1 | elrab2 3647 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π₯ β π β (π₯ β π΄ β§ βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1))) |
222 | 214, 215,
221 | sylanbrc 584 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π β (0...π)) β§ (π₯ β π΄ β§ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β (π·βπ)(π₯βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π₯βπ‘)))) β π₯ β π) |
223 | | simprr2 1223 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π β (0...π)) β§ (π₯ β π΄ β§ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β (π·βπ)(π₯βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π₯βπ‘)))) β βπ‘ β (π·βπ)(π₯βπ‘) < (πΈ / π)) |
224 | | simprr3 1224 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π β (0...π)) β§ (π₯ β π΄ β§ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β (π·βπ)(π₯βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π₯βπ‘)))) β βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π₯βπ‘)) |
225 | 223, 224 | jca 513 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π β (0...π)) β§ (π₯ β π΄ β§ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β (π·βπ)(π₯βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π₯βπ‘)))) β (βπ‘ β (π·βπ)(π₯βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π₯βπ‘))) |
226 | | nfcv 2906 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
β²π¦π₯ |
227 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
β²π¦(βπ‘ β (π·βπ)(π₯βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π₯βπ‘)) |
228 | 216 | breq1d 5114 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π¦ = π₯ β ((π¦βπ‘) < (πΈ / π) β (π₯βπ‘) < (πΈ / π))) |
229 | 228 | ralbidv 3173 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π¦ = π₯ β (βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π) β βπ‘ β (π·βπ)(π₯βπ‘) < (πΈ / π))) |
230 | 216 | breq2d 5116 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π¦ = π₯ β ((1 β (πΈ / π)) < (π¦βπ‘) β (1 β (πΈ / π)) < (π₯βπ‘))) |
231 | 230 | ralbidv 3173 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π¦ = π₯ β (βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘) β βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π₯βπ‘))) |
232 | 229, 231 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π¦ = π₯ β ((βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘)) β (βπ‘ β (π·βπ)(π₯βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π₯βπ‘)))) |
233 | 226, 3, 227, 232 | elrabf 3640 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π₯ β {π¦ β π β£ (βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘))} β (π₯ β π β§ (βπ‘ β (π·βπ)(π₯βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π₯βπ‘)))) |
234 | 222, 225,
233 | sylanbrc 584 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π β (0...π)) β§ (π₯ β π΄ β§ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β (π·βπ)(π₯βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π₯βπ‘)))) β π₯ β {π¦ β π β£ (βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘))}) |
235 | 234 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β (0...π)) β ((π₯ β π΄ β§ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β (π·βπ)(π₯βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π₯βπ‘))) β π₯ β {π¦ β π β£ (βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘))})) |
236 | 235 | eximdv 1921 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β (0...π)) β (βπ₯(π₯ β π΄ β§ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β (π·βπ)(π₯βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π₯βπ‘))) β βπ₯ π₯ β {π¦ β π β£ (βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘))})) |
237 | 213, 236 | mpd 15 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β (0...π)) β βπ₯ π₯ β {π¦ β π β£ (βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘))}) |
238 | | ne0i 4293 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ β {π¦ β π β£ (βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘))} β {π¦ β π β£ (βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘))} β β
) |
239 | 238 | exlimiv 1934 |
. . . . . . . . . . . . . . . . . . . 20
β’
(βπ₯ π₯ β {π¦ β π β£ (βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘))} β {π¦ β π β£ (βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘))} β β
) |
240 | 237, 239 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (0...π)) β {π¦ β π β£ (βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘))} β β
) |
241 | 68, 240 | eqnetrd 3010 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (0...π)) β (π»βπ) β β
) |
242 | 241 | 3adant3 1133 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (0...π) β§ (π»βπ) = π€) β (π»βπ) β β
) |
243 | 64, 242 | eqnetrrd 3011 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0...π) β§ (π»βπ) = π€) β π€ β β
) |
244 | 243 | 3exp 1120 |
. . . . . . . . . . . . . . 15
β’ (π β (π β (0...π) β ((π»βπ) = π€ β π€ β β
))) |
245 | 244 | rexlimdv 3149 |
. . . . . . . . . . . . . 14
β’ (π β (βπ β (0...π)(π»βπ) = π€ β π€ β β
)) |
246 | 245 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π€ β ran π») β (βπ β (0...π)(π»βπ) = π€ β π€ β β
)) |
247 | 63, 246 | mpd 15 |
. . . . . . . . . . . 12
β’ ((π β§ π€ β ran π») β π€ β β
) |
248 | 247 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) β§ π€ β ran π») β π€ β β
) |
249 | | rsp 3229 |
. . . . . . . . . . 11
β’
(βπ€ β
ran π»(π€ β β
β (ββπ€) β π€) β (π€ β ran π» β (π€ β β
β (ββπ€) β π€))) |
250 | 48, 49, 248, 249 | syl3c 66 |
. . . . . . . . . 10
β’ (((π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) β§ π€ β ran π») β (ββπ€) β π€) |
251 | 250 | ex 414 |
. . . . . . . . 9
β’ ((π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) β (π€ β ran π» β (ββπ€) β π€)) |
252 | 47, 251 | ralrimi 3239 |
. . . . . . . 8
β’ ((π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) β βπ€ β ran π»(ββπ€) β π€) |
253 | | chfnrn 6995 |
. . . . . . . 8
β’ ((β Fn ran π» β§ βπ€ β ran π»(ββπ€) β π€) β ran β β βͺ ran
π») |
254 | 32, 252, 253 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) β ran β β βͺ ran
π») |
255 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π¦π |
256 | | nfcv 2906 |
. . . . . . . . . . . 12
β’
β²π¦β |
257 | | nfcv 2906 |
. . . . . . . . . . . . . . 15
β’
β²π¦(0...π) |
258 | | nfrab1 3425 |
. . . . . . . . . . . . . . 15
β’
β²π¦{π¦ β π β£ (βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘))} |
259 | 257, 258 | nfmpt 5211 |
. . . . . . . . . . . . . 14
β’
β²π¦(π β (0...π) β¦ {π¦ β π β£ (βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘))}) |
260 | 22, 259 | nfcxfr 2904 |
. . . . . . . . . . . . 13
β’
β²π¦π» |
261 | 260 | nfrn 5904 |
. . . . . . . . . . . 12
β’
β²π¦ran
π» |
262 | 256, 261 | nffn 6597 |
. . . . . . . . . . 11
β’
β²π¦ β Fn ran π» |
263 | | nfv 1918 |
. . . . . . . . . . . 12
β’
β²π¦(π€ β β
β (ββπ€) β π€) |
264 | 261, 263 | nfralw 3293 |
. . . . . . . . . . 11
β’
β²π¦βπ€ β ran π»(π€ β β
β (ββπ€) β π€) |
265 | 262, 264 | nfan 1903 |
. . . . . . . . . 10
β’
β²π¦(β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€)) |
266 | 255, 265 | nfan 1903 |
. . . . . . . . 9
β’
β²π¦(π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) |
267 | 261 | nfuni 4871 |
. . . . . . . . 9
β’
β²π¦βͺ ran π» |
268 | | fnunirn 7196 |
. . . . . . . . . . . . . . 15
β’ (π» Fn (0...π) β (π¦ β βͺ ran
π» β βπ§ β (0...π)π¦ β (π»βπ§))) |
269 | | nfcv 2906 |
. . . . . . . . . . . . . . . . . 18
β’
β²ππ§ |
270 | 53, 269 | nffv 6848 |
. . . . . . . . . . . . . . . . 17
β’
β²π(π»βπ§) |
271 | 270 | nfcri 2893 |
. . . . . . . . . . . . . . . 16
β’
β²π π¦ β (π»βπ§) |
272 | | nfv 1918 |
. . . . . . . . . . . . . . . 16
β’
β²π§ π¦ β (π»βπ) |
273 | | fveq2 6838 |
. . . . . . . . . . . . . . . . 17
β’ (π§ = π β (π»βπ§) = (π»βπ)) |
274 | 273 | eleq2d 2824 |
. . . . . . . . . . . . . . . 16
β’ (π§ = π β (π¦ β (π»βπ§) β π¦ β (π»βπ))) |
275 | 271, 272,
274 | cbvrexw 3289 |
. . . . . . . . . . . . . . 15
β’
(βπ§ β
(0...π)π¦ β (π»βπ§) β βπ β (0...π)π¦ β (π»βπ)) |
276 | 268, 275 | bitrdi 287 |
. . . . . . . . . . . . . 14
β’ (π» Fn (0...π) β (π¦ β βͺ ran
π» β βπ β (0...π)π¦ β (π»βπ))) |
277 | 24, 276 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β (π¦ β βͺ ran
π» β βπ β (0...π)π¦ β (π»βπ))) |
278 | 277 | biimpa 478 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β βͺ ran
π») β βπ β (0...π)π¦ β (π»βπ)) |
279 | | nfv 1918 |
. . . . . . . . . . . . . 14
β’
β²ππ |
280 | 53 | nfrn 5904 |
. . . . . . . . . . . . . . . 16
β’
β²πran
π» |
281 | 280 | nfuni 4871 |
. . . . . . . . . . . . . . 15
β’
β²πβͺ ran π» |
282 | 281 | nfcri 2893 |
. . . . . . . . . . . . . 14
β’
β²π π¦ β βͺ ran π» |
283 | 279, 282 | nfan 1903 |
. . . . . . . . . . . . 13
β’
β²π(π β§ π¦ β βͺ ran
π») |
284 | | nfv 1918 |
. . . . . . . . . . . . 13
β’
β²π π¦ β π |
285 | | simp1l 1198 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π¦ β βͺ ran
π») β§ π β (0...π) β§ π¦ β (π»βπ)) β π) |
286 | | simp2 1138 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π¦ β βͺ ran
π») β§ π β (0...π) β§ π¦ β (π»βπ)) β π β (0...π)) |
287 | | simp3 1139 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π¦ β βͺ ran
π») β§ π β (0...π) β§ π¦ β (π»βπ)) β π¦ β (π»βπ)) |
288 | 68 | eleq2d 2824 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (0...π)) β (π¦ β (π»βπ) β π¦ β {π¦ β π β£ (βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘))})) |
289 | 288 | biimpa 478 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0...π)) β§ π¦ β (π»βπ)) β π¦ β {π¦ β π β£ (βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘))}) |
290 | | rabid 3426 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ β {π¦ β π β£ (βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘))} β (π¦ β π β§ (βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘)))) |
291 | 289, 290 | sylib 217 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0...π)) β§ π¦ β (π»βπ)) β (π¦ β π β§ (βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘)))) |
292 | 291 | simpld 496 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0...π)) β§ π¦ β (π»βπ)) β π¦ β π) |
293 | 285, 286,
287, 292 | syl21anc 837 |
. . . . . . . . . . . . . 14
β’ (((π β§ π¦ β βͺ ran
π») β§ π β (0...π) β§ π¦ β (π»βπ)) β π¦ β π) |
294 | 293 | 3exp 1120 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β βͺ ran
π») β (π β (0...π) β (π¦ β (π»βπ) β π¦ β π))) |
295 | 283, 284,
294 | rexlimd 3248 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β βͺ ran
π») β (βπ β (0...π)π¦ β (π»βπ) β π¦ β π)) |
296 | 278, 295 | mpd 15 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β βͺ ran
π») β π¦ β π) |
297 | 296 | adantlr 714 |
. . . . . . . . . 10
β’ (((π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) β§ π¦ β βͺ ran
π») β π¦ β π) |
298 | 297 | ex 414 |
. . . . . . . . 9
β’ ((π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) β (π¦ β βͺ ran
π» β π¦ β π)) |
299 | 266, 267,
3, 298 | ssrd 3948 |
. . . . . . . 8
β’ ((π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) β βͺ ran
π» β π) |
300 | | ssrab2 4036 |
. . . . . . . . 9
β’ {π¦ β π΄ β£ βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1)} β π΄ |
301 | 1, 300 | eqsstri 3977 |
. . . . . . . 8
β’ π β π΄ |
302 | 299, 301 | sstrdi 3955 |
. . . . . . 7
β’ ((π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) β βͺ ran
π» β π΄) |
303 | 254, 302 | sstrd 3953 |
. . . . . 6
β’ ((π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) β ran β β π΄) |
304 | 42, 303 | fssd 6682 |
. . . . 5
β’ ((π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) β β:ran π»βΆπ΄) |
305 | | dffn3 6677 |
. . . . . . 7
β’ (π» Fn (0...π) β π»:(0...π)βΆran π») |
306 | 24, 305 | sylib 217 |
. . . . . 6
β’ (π β π»:(0...π)βΆran π») |
307 | 306 | adantr 482 |
. . . . 5
β’ ((π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) β π»:(0...π)βΆran π») |
308 | | fco 6688 |
. . . . 5
β’ ((β:ran π»βΆπ΄ β§ π»:(0...π)βΆran π») β (β β π»):(0...π)βΆπ΄) |
309 | 304, 307,
308 | syl2anc 585 |
. . . 4
β’ ((π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) β (β β π»):(0...π)βΆπ΄) |
310 | | nfcv 2906 |
. . . . . . . 8
β’
β²πβ |
311 | 310, 280 | nffn 6597 |
. . . . . . 7
β’
β²π β Fn ran π» |
312 | | nfv 1918 |
. . . . . . . 8
β’
β²π(π€ β β
β (ββπ€) β π€) |
313 | 280, 312 | nfralw 3293 |
. . . . . . 7
β’
β²πβπ€ β ran π»(π€ β β
β (ββπ€) β π€) |
314 | 311, 313 | nfan 1903 |
. . . . . 6
β’
β²π(β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€)) |
315 | 279, 314 | nfan 1903 |
. . . . 5
β’
β²π(π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) |
316 | | simpll 766 |
. . . . . . . . . 10
β’ (((π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) β§ π β (0...π)) β π) |
317 | | simpr 486 |
. . . . . . . . . 10
β’ (((π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) β§ π β (0...π)) β π β (0...π)) |
318 | 24 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) β§ π β (0...π)) β π» Fn (0...π)) |
319 | | fvco2 6934 |
. . . . . . . . . . . 12
β’ ((π» Fn (0...π) β§ π β (0...π)) β ((β β π»)βπ) = (ββ(π»βπ))) |
320 | 318, 319 | sylancom 589 |
. . . . . . . . . . 11
β’ (((π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) β§ π β (0...π)) β ((β β π»)βπ) = (ββ(π»βπ))) |
321 | | simplrr 777 |
. . . . . . . . . . . . 13
β’ (((π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) β§ π β (0...π)) β βπ€ β ran π»(π€ β β
β (ββπ€) β π€)) |
322 | | fnfun 6598 |
. . . . . . . . . . . . . . . 16
β’ (π» Fn (0...π) β Fun π») |
323 | 24, 322 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β Fun π») |
324 | 323 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) β§ π β (0...π)) β Fun π») |
325 | 24 | fndmd 6603 |
. . . . . . . . . . . . . . . . 17
β’ (π β dom π» = (0...π)) |
326 | 325 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0...π)) β dom π» = (0...π)) |
327 | 65, 326 | eleqtrrd 2842 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0...π)) β π β dom π») |
328 | 327 | adantlr 714 |
. . . . . . . . . . . . . 14
β’ (((π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) β§ π β (0...π)) β π β dom π») |
329 | | fvelrn 7023 |
. . . . . . . . . . . . . 14
β’ ((Fun
π» β§ π β dom π») β (π»βπ) β ran π») |
330 | 324, 328,
329 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) β§ π β (0...π)) β (π»βπ) β ran π») |
331 | 321, 330 | jca 513 |
. . . . . . . . . . . 12
β’ (((π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) β§ π β (0...π)) β (βπ€ β ran π»(π€ β β
β (ββπ€) β π€) β§ (π»βπ) β ran π»)) |
332 | 241 | adantlr 714 |
. . . . . . . . . . . 12
β’ (((π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) β§ π β (0...π)) β (π»βπ) β β
) |
333 | | neeq1 3005 |
. . . . . . . . . . . . . 14
β’ (π€ = (π»βπ) β (π€ β β
β (π»βπ) β β
)) |
334 | | fveq2 6838 |
. . . . . . . . . . . . . . 15
β’ (π€ = (π»βπ) β (ββπ€) = (ββ(π»βπ))) |
335 | | id 22 |
. . . . . . . . . . . . . . 15
β’ (π€ = (π»βπ) β π€ = (π»βπ)) |
336 | 334, 335 | eleq12d 2833 |
. . . . . . . . . . . . . 14
β’ (π€ = (π»βπ) β ((ββπ€) β π€ β (ββ(π»βπ)) β (π»βπ))) |
337 | 333, 336 | imbi12d 345 |
. . . . . . . . . . . . 13
β’ (π€ = (π»βπ) β ((π€ β β
β (ββπ€) β π€) β ((π»βπ) β β
β (ββ(π»βπ)) β (π»βπ)))) |
338 | 337 | rspccva 3579 |
. . . . . . . . . . . 12
β’
((βπ€ β
ran π»(π€ β β
β (ββπ€) β π€) β§ (π»βπ) β ran π») β ((π»βπ) β β
β (ββ(π»βπ)) β (π»βπ))) |
339 | 331, 332,
338 | sylc 65 |
. . . . . . . . . . 11
β’ (((π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) β§ π β (0...π)) β (ββ(π»βπ)) β (π»βπ)) |
340 | 320, 339 | eqeltrd 2839 |
. . . . . . . . . 10
β’ (((π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) β§ π β (0...π)) β ((β β π»)βπ) β (π»βπ)) |
341 | 256, 260 | nfco 5818 |
. . . . . . . . . . . . 13
β’
β²π¦(β β π») |
342 | | nfcv 2906 |
. . . . . . . . . . . . 13
β’
β²π¦π |
343 | 341, 342 | nffv 6848 |
. . . . . . . . . . . 12
β’
β²π¦((β β π»)βπ) |
344 | | nfv 1918 |
. . . . . . . . . . . . . 14
β’
β²π¦(π β§ π β (0...π)) |
345 | 260, 342 | nffv 6848 |
. . . . . . . . . . . . . . 15
β’
β²π¦(π»βπ) |
346 | 343, 345 | nfel 2920 |
. . . . . . . . . . . . . 14
β’
β²π¦((β β π»)βπ) β (π»βπ) |
347 | 344, 346 | nfan 1903 |
. . . . . . . . . . . . 13
β’
β²π¦((π β§ π β (0...π)) β§ ((β β π»)βπ) β (π»βπ)) |
348 | 343, 3 | nfel 2920 |
. . . . . . . . . . . . 13
β’
β²π¦((β β π»)βπ) β π |
349 | 347, 348 | nfim 1900 |
. . . . . . . . . . . 12
β’
β²π¦(((π β§ π β (0...π)) β§ ((β β π»)βπ) β (π»βπ)) β ((β β π»)βπ) β π) |
350 | | eleq1 2826 |
. . . . . . . . . . . . . 14
β’ (π¦ = ((β β π»)βπ) β (π¦ β (π»βπ) β ((β β π»)βπ) β (π»βπ))) |
351 | 350 | anbi2d 630 |
. . . . . . . . . . . . 13
β’ (π¦ = ((β β π»)βπ) β (((π β§ π β (0...π)) β§ π¦ β (π»βπ)) β ((π β§ π β (0...π)) β§ ((β β π»)βπ) β (π»βπ)))) |
352 | | eleq1 2826 |
. . . . . . . . . . . . 13
β’ (π¦ = ((β β π»)βπ) β (π¦ β π β ((β β π»)βπ) β π)) |
353 | 351, 352 | imbi12d 345 |
. . . . . . . . . . . 12
β’ (π¦ = ((β β π»)βπ) β ((((π β§ π β (0...π)) β§ π¦ β (π»βπ)) β π¦ β π) β (((π β§ π β (0...π)) β§ ((β β π»)βπ) β (π»βπ)) β ((β β π»)βπ) β π))) |
354 | 343, 349,
353, 292 | vtoclgf 3522 |
. . . . . . . . . . 11
β’ (((β β π»)βπ) β (π»βπ) β (((π β§ π β (0...π)) β§ ((β β π»)βπ) β (π»βπ)) β ((β β π»)βπ) β π)) |
355 | 354 | anabsi7 670 |
. . . . . . . . . 10
β’ (((π β§ π β (0...π)) β§ ((β β π»)βπ) β (π»βπ)) β ((β β π»)βπ) β π) |
356 | 316, 317,
340, 355 | syl21anc 837 |
. . . . . . . . 9
β’ (((π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) β§ π β (0...π)) β ((β β π»)βπ) β π) |
357 | 1 | eleq2i 2830 |
. . . . . . . . . 10
β’ (((β β π»)βπ) β π β ((β β π»)βπ) β {π¦ β π΄ β£ βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1)}) |
358 | | nfcv 2906 |
. . . . . . . . . . 11
β’
β²π¦π΄ |
359 | | nfcv 2906 |
. . . . . . . . . . . 12
β’
β²π¦π |
360 | | nfcv 2906 |
. . . . . . . . . . . . . 14
β’
β²π¦0 |
361 | | nfcv 2906 |
. . . . . . . . . . . . . 14
β’
β²π¦
β€ |
362 | | nfcv 2906 |
. . . . . . . . . . . . . . 15
β’
β²π¦π‘ |
363 | 343, 362 | nffv 6848 |
. . . . . . . . . . . . . 14
β’
β²π¦(((β β π»)βπ)βπ‘) |
364 | 360, 361,
363 | nfbr 5151 |
. . . . . . . . . . . . 13
β’
β²π¦0 β€
(((β β π»)βπ)βπ‘) |
365 | | nfcv 2906 |
. . . . . . . . . . . . . 14
β’
β²π¦1 |
366 | 363, 361,
365 | nfbr 5151 |
. . . . . . . . . . . . 13
β’
β²π¦(((β β π»)βπ)βπ‘) β€ 1 |
367 | 364, 366 | nfan 1903 |
. . . . . . . . . . . 12
β’
β²π¦(0 β€
(((β β π»)βπ)βπ‘) β§ (((β β π»)βπ)βπ‘) β€ 1) |
368 | 359, 367 | nfralw 3293 |
. . . . . . . . . . 11
β’
β²π¦βπ‘ β π (0 β€ (((β β π»)βπ)βπ‘) β§ (((β β π»)βπ)βπ‘) β€ 1) |
369 | | nfcv 2906 |
. . . . . . . . . . . . 13
β’
β²π‘π¦ |
370 | | nfcv 2906 |
. . . . . . . . . . . . . . 15
β’
β²π‘β |
371 | | nfra1 3266 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π‘βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π) |
372 | | nfra1 3266 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π‘βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘) |
373 | 371, 372 | nfan 1903 |
. . . . . . . . . . . . . . . . . 18
β’
β²π‘(βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘)) |
374 | | nfra1 3266 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π‘βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1) |
375 | | nfcv 2906 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π‘π΄ |
376 | 374, 375 | nfrabw 3439 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π‘{π¦ β π΄ β£ βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1)} |
377 | 1, 376 | nfcxfr 2904 |
. . . . . . . . . . . . . . . . . 18
β’
β²π‘π |
378 | 373, 377 | nfrabw 3439 |
. . . . . . . . . . . . . . . . 17
β’
β²π‘{π¦ β π β£ (βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘))} |
379 | 70, 378 | nfmpt 5211 |
. . . . . . . . . . . . . . . 16
β’
β²π‘(π β (0...π) β¦ {π¦ β π β£ (βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘))}) |
380 | 22, 379 | nfcxfr 2904 |
. . . . . . . . . . . . . . 15
β’
β²π‘π» |
381 | 370, 380 | nfco 5818 |
. . . . . . . . . . . . . 14
β’
β²π‘(β β π») |
382 | 381, 74 | nffv 6848 |
. . . . . . . . . . . . 13
β’
β²π‘((β β π»)βπ) |
383 | 369, 382 | nfeq 2919 |
. . . . . . . . . . . 12
β’
β²π‘ π¦ = ((β β π»)βπ) |
384 | | fveq1 6837 |
. . . . . . . . . . . . . 14
β’ (π¦ = ((β β π»)βπ) β (π¦βπ‘) = (((β β π»)βπ)βπ‘)) |
385 | 384 | breq2d 5116 |
. . . . . . . . . . . . 13
β’ (π¦ = ((β β π»)βπ) β (0 β€ (π¦βπ‘) β 0 β€ (((β β π»)βπ)βπ‘))) |
386 | 384 | breq1d 5114 |
. . . . . . . . . . . . 13
β’ (π¦ = ((β β π»)βπ) β ((π¦βπ‘) β€ 1 β (((β β π»)βπ)βπ‘) β€ 1)) |
387 | 385, 386 | anbi12d 632 |
. . . . . . . . . . . 12
β’ (π¦ = ((β β π»)βπ) β ((0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1) β (0 β€ (((β β π»)βπ)βπ‘) β§ (((β β π»)βπ)βπ‘) β€ 1))) |
388 | 383, 387 | ralbid 3255 |
. . . . . . . . . . 11
β’ (π¦ = ((β β π»)βπ) β (βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1) β βπ‘ β π (0 β€ (((β β π»)βπ)βπ‘) β§ (((β β π»)βπ)βπ‘) β€ 1))) |
389 | 343, 358,
368, 388 | elrabf 3640 |
. . . . . . . . . 10
β’ (((β β π»)βπ) β {π¦ β π΄ β£ βπ‘ β π (0 β€ (π¦βπ‘) β§ (π¦βπ‘) β€ 1)} β (((β β π»)βπ) β π΄ β§ βπ‘ β π (0 β€ (((β β π»)βπ)βπ‘) β§ (((β β π»)βπ)βπ‘) β€ 1))) |
390 | 357, 389 | bitri 275 |
. . . . . . . . 9
β’ (((β β π»)βπ) β π β (((β β π»)βπ) β π΄ β§ βπ‘ β π (0 β€ (((β β π»)βπ)βπ‘) β§ (((β β π»)βπ)βπ‘) β€ 1))) |
391 | 356, 390 | sylib 217 |
. . . . . . . 8
β’ (((π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) β§ π β (0...π)) β (((β β π»)βπ) β π΄ β§ βπ‘ β π (0 β€ (((β β π»)βπ)βπ‘) β§ (((β β π»)βπ)βπ‘) β€ 1))) |
392 | 391 | simprd 497 |
. . . . . . 7
β’ (((π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) β§ π β (0...π)) β βπ‘ β π (0 β€ (((β β π»)βπ)βπ‘) β§ (((β β π»)βπ)βπ‘) β€ 1)) |
393 | | nfcv 2906 |
. . . . . . . . . . . 12
β’
β²π¦(π·βπ) |
394 | | nfcv 2906 |
. . . . . . . . . . . . 13
β’
β²π¦
< |
395 | | nfcv 2906 |
. . . . . . . . . . . . 13
β’
β²π¦(πΈ / π) |
396 | 363, 394,
395 | nfbr 5151 |
. . . . . . . . . . . 12
β’
β²π¦(((β β π»)βπ)βπ‘) < (πΈ / π) |
397 | 393, 396 | nfralw 3293 |
. . . . . . . . . . 11
β’
β²π¦βπ‘ β (π·βπ)(((β β π»)βπ)βπ‘) < (πΈ / π) |
398 | 347, 397 | nfim 1900 |
. . . . . . . . . 10
β’
β²π¦(((π β§ π β (0...π)) β§ ((β β π»)βπ) β (π»βπ)) β βπ‘ β (π·βπ)(((β β π»)βπ)βπ‘) < (πΈ / π)) |
399 | 384 | breq1d 5114 |
. . . . . . . . . . . 12
β’ (π¦ = ((β β π»)βπ) β ((π¦βπ‘) < (πΈ / π) β (((β β π»)βπ)βπ‘) < (πΈ / π))) |
400 | 383, 399 | ralbid 3255 |
. . . . . . . . . . 11
β’ (π¦ = ((β β π»)βπ) β (βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π) β βπ‘ β (π·βπ)(((β β π»)βπ)βπ‘) < (πΈ / π))) |
401 | 351, 400 | imbi12d 345 |
. . . . . . . . . 10
β’ (π¦ = ((β β π»)βπ) β ((((π β§ π β (0...π)) β§ π¦ β (π»βπ)) β βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π)) β (((π β§ π β (0...π)) β§ ((β β π»)βπ) β (π»βπ)) β βπ‘ β (π·βπ)(((β β π»)βπ)βπ‘) < (πΈ / π)))) |
402 | 291 | simprd 497 |
. . . . . . . . . . 11
β’ (((π β§ π β (0...π)) β§ π¦ β (π»βπ)) β (βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘))) |
403 | 402 | simpld 496 |
. . . . . . . . . 10
β’ (((π β§ π β (0...π)) β§ π¦ β (π»βπ)) β βπ‘ β (π·βπ)(π¦βπ‘) < (πΈ / π)) |
404 | 343, 398,
401, 403 | vtoclgf 3522 |
. . . . . . . . 9
β’ (((β β π»)βπ) β (π»βπ) β (((π β§ π β (0...π)) β§ ((β β π»)βπ) β (π»βπ)) β βπ‘ β (π·βπ)(((β β π»)βπ)βπ‘) < (πΈ / π))) |
405 | 404 | anabsi7 670 |
. . . . . . . 8
β’ (((π β§ π β (0...π)) β§ ((β β π»)βπ) β (π»βπ)) β βπ‘ β (π·βπ)(((β β π»)βπ)βπ‘) < (πΈ / π)) |
406 | 316, 317,
340, 405 | syl21anc 837 |
. . . . . . 7
β’ (((π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) β§ π β (0...π)) β βπ‘ β (π·βπ)(((β β π»)βπ)βπ‘) < (πΈ / π)) |
407 | | nfcv 2906 |
. . . . . . . . . . . 12
β’
β²π¦(π΅βπ) |
408 | | nfcv 2906 |
. . . . . . . . . . . . 13
β’
β²π¦(1
β (πΈ / π)) |
409 | 408, 394,
363 | nfbr 5151 |
. . . . . . . . . . . 12
β’
β²π¦(1 β
(πΈ / π)) < (((β β π»)βπ)βπ‘) |
410 | 407, 409 | nfralw 3293 |
. . . . . . . . . . 11
β’
β²π¦βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (((β β π»)βπ)βπ‘) |
411 | 347, 410 | nfim 1900 |
. . . . . . . . . 10
β’
β²π¦(((π β§ π β (0...π)) β§ ((β β π»)βπ) β (π»βπ)) β βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (((β β π»)βπ)βπ‘)) |
412 | 384 | breq2d 5116 |
. . . . . . . . . . . 12
β’ (π¦ = ((β β π»)βπ) β ((1 β (πΈ / π)) < (π¦βπ‘) β (1 β (πΈ / π)) < (((β β π»)βπ)βπ‘))) |
413 | 383, 412 | ralbid 3255 |
. . . . . . . . . . 11
β’ (π¦ = ((β β π»)βπ) β (βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘) β βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (((β β π»)βπ)βπ‘))) |
414 | 351, 413 | imbi12d 345 |
. . . . . . . . . 10
β’ (π¦ = ((β β π»)βπ) β ((((π β§ π β (0...π)) β§ π¦ β (π»βπ)) β βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘)) β (((π β§ π β (0...π)) β§ ((β β π»)βπ) β (π»βπ)) β βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (((β β π»)βπ)βπ‘)))) |
415 | 402 | simprd 497 |
. . . . . . . . . 10
β’ (((π β§ π β (0...π)) β§ π¦ β (π»βπ)) β βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (π¦βπ‘)) |
416 | 343, 411,
414, 415 | vtoclgf 3522 |
. . . . . . . . 9
β’ (((β β π»)βπ) β (π»βπ) β (((π β§ π β (0...π)) β§ ((β β π»)βπ) β (π»βπ)) β βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (((β β π»)βπ)βπ‘))) |
417 | 416 | anabsi7 670 |
. . . . . . . 8
β’ (((π β§ π β (0...π)) β§ ((β β π»)βπ) β (π»βπ)) β βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (((β β π»)βπ)βπ‘)) |
418 | 316, 317,
340, 417 | syl21anc 837 |
. . . . . . 7
β’ (((π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) β§ π β (0...π)) β βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (((β β π»)βπ)βπ‘)) |
419 | 392, 406,
418 | 3jca 1129 |
. . . . . 6
β’ (((π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) β§ π β (0...π)) β (βπ‘ β π (0 β€ (((β β π»)βπ)βπ‘) β§ (((β β π»)βπ)βπ‘) β€ 1) β§ βπ‘ β (π·βπ)(((β β π»)βπ)βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (((β β π»)βπ)βπ‘))) |
420 | 419 | ex 414 |
. . . . 5
β’ ((π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) β (π β (0...π) β (βπ‘ β π (0 β€ (((β β π»)βπ)βπ‘) β§ (((β β π»)βπ)βπ‘) β€ 1) β§ βπ‘ β (π·βπ)(((β β π»)βπ)βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (((β β π»)βπ)βπ‘)))) |
421 | 315, 420 | ralrimi 3239 |
. . . 4
β’ ((π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) β βπ β (0...π)(βπ‘ β π (0 β€ (((β β π»)βπ)βπ‘) β§ (((β β π»)βπ)βπ‘) β€ 1) β§ βπ‘ β (π·βπ)(((β β π»)βπ)βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (((β β π»)βπ)βπ‘))) |
422 | 309, 421 | jca 513 |
. . 3
β’ ((π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) β ((β β π»):(0...π)βΆπ΄ β§ βπ β (0...π)(βπ‘ β π (0 β€ (((β β π»)βπ)βπ‘) β§ (((β β π»)βπ)βπ‘) β€ 1) β§ βπ‘ β (π·βπ)(((β β π»)βπ)βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (((β β π»)βπ)βπ‘)))) |
423 | | feq1 6645 |
. . . . 5
β’ (π₯ = (β β π») β (π₯:(0...π)βΆπ΄ β (β β π»):(0...π)βΆπ΄)) |
424 | | nfcv 2906 |
. . . . . . 7
β’
β²ππ₯ |
425 | 310, 53 | nfco 5818 |
. . . . . . 7
β’
β²π(β β π») |
426 | 424, 425 | nfeq 2919 |
. . . . . 6
β’
β²π π₯ = (β β π») |
427 | | nfcv 2906 |
. . . . . . . . 9
β’
β²π‘π₯ |
428 | 427, 381 | nfeq 2919 |
. . . . . . . 8
β’
β²π‘ π₯ = (β β π») |
429 | | fveq1 6837 |
. . . . . . . . . . 11
β’ (π₯ = (β β π») β (π₯βπ) = ((β β π»)βπ)) |
430 | 429 | fveq1d 6840 |
. . . . . . . . . 10
β’ (π₯ = (β β π») β ((π₯βπ)βπ‘) = (((β β π»)βπ)βπ‘)) |
431 | 430 | breq2d 5116 |
. . . . . . . . 9
β’ (π₯ = (β β π») β (0 β€ ((π₯βπ)βπ‘) β 0 β€ (((β β π»)βπ)βπ‘))) |
432 | 430 | breq1d 5114 |
. . . . . . . . 9
β’ (π₯ = (β β π») β (((π₯βπ)βπ‘) β€ 1 β (((β β π»)βπ)βπ‘) β€ 1)) |
433 | 431, 432 | anbi12d 632 |
. . . . . . . 8
β’ (π₯ = (β β π») β ((0 β€ ((π₯βπ)βπ‘) β§ ((π₯βπ)βπ‘) β€ 1) β (0 β€ (((β β π»)βπ)βπ‘) β§ (((β β π»)βπ)βπ‘) β€ 1))) |
434 | 428, 433 | ralbid 3255 |
. . . . . . 7
β’ (π₯ = (β β π») β (βπ‘ β π (0 β€ ((π₯βπ)βπ‘) β§ ((π₯βπ)βπ‘) β€ 1) β βπ‘ β π (0 β€ (((β β π»)βπ)βπ‘) β§ (((β β π»)βπ)βπ‘) β€ 1))) |
435 | 430 | breq1d 5114 |
. . . . . . . 8
β’ (π₯ = (β β π») β (((π₯βπ)βπ‘) < (πΈ / π) β (((β β π»)βπ)βπ‘) < (πΈ / π))) |
436 | 428, 435 | ralbid 3255 |
. . . . . . 7
β’ (π₯ = (β β π») β (βπ‘ β (π·βπ)((π₯βπ)βπ‘) < (πΈ / π) β βπ‘ β (π·βπ)(((β β π»)βπ)βπ‘) < (πΈ / π))) |
437 | 430 | breq2d 5116 |
. . . . . . . 8
β’ (π₯ = (β β π») β ((1 β (πΈ / π)) < ((π₯βπ)βπ‘) β (1 β (πΈ / π)) < (((β β π»)βπ)βπ‘))) |
438 | 428, 437 | ralbid 3255 |
. . . . . . 7
β’ (π₯ = (β β π») β (βπ‘ β (π΅βπ)(1 β (πΈ / π)) < ((π₯βπ)βπ‘) β βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (((β β π»)βπ)βπ‘))) |
439 | 434, 436,
438 | 3anbi123d 1437 |
. . . . . 6
β’ (π₯ = (β β π») β ((βπ‘ β π (0 β€ ((π₯βπ)βπ‘) β§ ((π₯βπ)βπ‘) β€ 1) β§ βπ‘ β (π·βπ)((π₯βπ)βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < ((π₯βπ)βπ‘)) β (βπ‘ β π (0 β€ (((β β π»)βπ)βπ‘) β§ (((β β π»)βπ)βπ‘) β€ 1) β§ βπ‘ β (π·βπ)(((β β π»)βπ)βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (((β β π»)βπ)βπ‘)))) |
440 | 426, 439 | ralbid 3255 |
. . . . 5
β’ (π₯ = (β β π») β (βπ β (0...π)(βπ‘ β π (0 β€ ((π₯βπ)βπ‘) β§ ((π₯βπ)βπ‘) β€ 1) β§ βπ‘ β (π·βπ)((π₯βπ)βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < ((π₯βπ)βπ‘)) β βπ β (0...π)(βπ‘ β π (0 β€ (((β β π»)βπ)βπ‘) β§ (((β β π»)βπ)βπ‘) β€ 1) β§ βπ‘ β (π·βπ)(((β β π»)βπ)βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (((β β π»)βπ)βπ‘)))) |
441 | 423, 440 | anbi12d 632 |
. . . 4
β’ (π₯ = (β β π») β ((π₯:(0...π)βΆπ΄ β§ βπ β (0...π)(βπ‘ β π (0 β€ ((π₯βπ)βπ‘) β§ ((π₯βπ)βπ‘) β€ 1) β§ βπ‘ β (π·βπ)((π₯βπ)βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < ((π₯βπ)βπ‘))) β ((β β π»):(0...π)βΆπ΄ β§ βπ β (0...π)(βπ‘ β π (0 β€ (((β β π»)βπ)βπ‘) β§ (((β β π»)βπ)βπ‘) β€ 1) β§ βπ‘ β (π·βπ)(((β β π»)βπ)βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (((β β π»)βπ)βπ‘))))) |
442 | 441 | spcegv 3555 |
. . 3
β’ ((β β π») β V β (((β β π»):(0...π)βΆπ΄ β§ βπ β (0...π)(βπ‘ β π (0 β€ (((β β π»)βπ)βπ‘) β§ (((β β π»)βπ)βπ‘) β€ 1) β§ βπ‘ β (π·βπ)(((β β π»)βπ)βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < (((β β π»)βπ)βπ‘))) β βπ₯(π₯:(0...π)βΆπ΄ β§ βπ β (0...π)(βπ‘ β π (0 β€ ((π₯βπ)βπ‘) β§ ((π₯βπ)βπ‘) β€ 1) β§ βπ‘ β (π·βπ)((π₯βπ)βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < ((π₯βπ)βπ‘))))) |
443 | 40, 422, 442 | sylc 65 |
. 2
β’ ((π β§ (β Fn ran π» β§ βπ€ β ran π»(π€ β β
β (ββπ€) β π€))) β βπ₯(π₯:(0...π)βΆπ΄ β§ βπ β (0...π)(βπ‘ β π (0 β€ ((π₯βπ)βπ‘) β§ ((π₯βπ)βπ‘) β€ 1) β§ βπ‘ β (π·βπ)((π₯βπ)βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < ((π₯βπ)βπ‘)))) |
444 | 31, 443 | exlimddv 1939 |
1
β’ (π β βπ₯(π₯:(0...π)βΆπ΄ β§ βπ β (0...π)(βπ‘ β π (0 β€ ((π₯βπ)βπ‘) β§ ((π₯βπ)βπ‘) β€ 1) β§ βπ‘ β (π·βπ)((π₯βπ)βπ‘) < (πΈ / π) β§ βπ‘ β (π΅βπ)(1 β (πΈ / π)) < ((π₯βπ)βπ‘)))) |