Step | Hyp | Ref
| Expression |
1 | | stoweidlem54.3 |
. . 3
β’
β²π¦π |
2 | | nfv 1918 |
. . 3
β’
β²π¦βπ₯(π₯ β π΄ β§ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π· (π₯βπ‘) < πΈ β§ βπ‘ β π΅ (1 β πΈ) < (π₯βπ‘))) |
3 | | stoweidlem54.18 |
. . 3
β’ (π β βπ¦(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (πβπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) |
4 | | stoweidlem54.1 |
. . . . 5
β’
β²ππ |
5 | | nfv 1918 |
. . . . . 6
β’
β²π π¦:(1...π)βΆπ |
6 | | nfra1 3270 |
. . . . . 6
β’
β²πβπ β (1...π)(βπ‘ β (πβπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)) |
7 | 5, 6 | nfan 1903 |
. . . . 5
β’
β²π(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (πβπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))) |
8 | 4, 7 | nfan 1903 |
. . . 4
β’
β²π(π β§ (π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (πβπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) |
9 | | stoweidlem54.2 |
. . . . 5
β’
β²π‘π |
10 | | nfcv 2908 |
. . . . . . 7
β’
β²π‘π¦ |
11 | | nfcv 2908 |
. . . . . . 7
β’
β²π‘(1...π) |
12 | | stoweidlem54.6 |
. . . . . . . 8
β’ π = {β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} |
13 | | nfra1 3270 |
. . . . . . . . 9
β’
β²π‘βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) |
14 | | nfcv 2908 |
. . . . . . . . 9
β’
β²π‘π΄ |
15 | 13, 14 | nfrabw 3443 |
. . . . . . . 8
β’
β²π‘{β β π΄ β£ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1)} |
16 | 12, 15 | nfcxfr 2906 |
. . . . . . 7
β’
β²π‘π |
17 | 10, 11, 16 | nff 6669 |
. . . . . 6
β’
β²π‘ π¦:(1...π)βΆπ |
18 | | nfra1 3270 |
. . . . . . . 8
β’
β²π‘βπ‘ β (πβπ)((π¦βπ)βπ‘) < (πΈ / π) |
19 | | nfra1 3270 |
. . . . . . . 8
β’
β²π‘βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘) |
20 | 18, 19 | nfan 1903 |
. . . . . . 7
β’
β²π‘(βπ‘ β (πβπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)) |
21 | 11, 20 | nfralw 3297 |
. . . . . 6
β’
β²π‘βπ β (1...π)(βπ‘ β (πβπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)) |
22 | 17, 21 | nfan 1903 |
. . . . 5
β’
β²π‘(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (πβπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))) |
23 | 9, 22 | nfan 1903 |
. . . 4
β’
β²π‘(π β§ (π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (πβπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) |
24 | | stoweidlem54.4 |
. . . . 5
β’
β²π€π |
25 | | nfv 1918 |
. . . . 5
β’
β²π€(π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (πβπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))) |
26 | 24, 25 | nfan 1903 |
. . . 4
β’
β²π€(π β§ (π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (πβπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) |
27 | | stoweidlem54.10 |
. . . . 5
β’ π = {π€ β π½ β£ βπ β β+ ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘))} |
28 | | nfrab1 3429 |
. . . . 5
β’
β²π€{π€ β π½ β£ βπ β β+ ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘))} |
29 | 27, 28 | nfcxfr 2906 |
. . . 4
β’
β²π€π |
30 | | stoweidlem54.7 |
. . . 4
β’ π = (π β π, π β π β¦ (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘)))) |
31 | | eqid 2737 |
. . . 4
β’
(seq1(π, π¦)βπ) = (seq1(π, π¦)βπ) |
32 | | stoweidlem54.8 |
. . . 4
β’ πΉ = (π‘ β π β¦ (π β (1...π) β¦ ((π¦βπ)βπ‘))) |
33 | | stoweidlem54.9 |
. . . 4
β’ π = (π‘ β π β¦ (seq1( Β· , (πΉβπ‘))βπ)) |
34 | | stoweidlem54.13 |
. . . . 5
β’ (π β π β β) |
35 | 34 | adantr 482 |
. . . 4
β’ ((π β§ (π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (πβπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) β π β β) |
36 | | stoweidlem54.14 |
. . . . 5
β’ (π β π:(1...π)βΆπ) |
37 | 36 | adantr 482 |
. . . 4
β’ ((π β§ (π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (πβπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) β π:(1...π)βΆπ) |
38 | | simprl 770 |
. . . 4
β’ ((π β§ (π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (πβπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) β π¦:(1...π)βΆπ) |
39 | | simpr 486 |
. . . . 5
β’ (((π β§ (π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (πβπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) β§ π€ β π) β π€ β π) |
40 | 27 | reqabi 3432 |
. . . . . 6
β’ (π€ β π β (π€ β π½ β§ βπ β β+ ββ β π΄ (βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1) β§ βπ‘ β π€ (ββπ‘) < π β§ βπ‘ β (π β π)(1 β π) < (ββπ‘)))) |
41 | 40 | simplbi 499 |
. . . . 5
β’ (π€ β π β π€ β π½) |
42 | | elssuni 4903 |
. . . . . 6
β’ (π€ β π½ β π€ β βͺ π½) |
43 | | stoweidlem54.5 |
. . . . . 6
β’ π = βͺ
π½ |
44 | 42, 43 | sseqtrrdi 4000 |
. . . . 5
β’ (π€ β π½ β π€ β π) |
45 | 39, 41, 44 | 3syl 18 |
. . . 4
β’ (((π β§ (π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (πβπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) β§ π€ β π) β π€ β π) |
46 | | stoweidlem54.16 |
. . . . 5
β’ (π β π· β βͺ ran
π) |
47 | 46 | adantr 482 |
. . . 4
β’ ((π β§ (π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (πβπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) β π· β βͺ ran
π) |
48 | | stoweidlem54.17 |
. . . . 5
β’ (π β π· β π) |
49 | 48 | adantr 482 |
. . . 4
β’ ((π β§ (π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (πβπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) β π· β π) |
50 | | stoweidlem54.15 |
. . . . 5
β’ (π β π΅ β π) |
51 | 50 | adantr 482 |
. . . 4
β’ ((π β§ (π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (πβπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) β π΅ β π) |
52 | | r19.26 3115 |
. . . . . . 7
β’
(βπ β
(1...π)(βπ‘ β (πβπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)) β (βπ β (1...π)βπ‘ β (πβπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ β (1...π)βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘))) |
53 | 52 | simplbi 499 |
. . . . . 6
β’
(βπ β
(1...π)(βπ‘ β (πβπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)) β βπ β (1...π)βπ‘ β (πβπ)((π¦βπ)βπ‘) < (πΈ / π)) |
54 | 53 | ad2antll 728 |
. . . . 5
β’ ((π β§ (π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (πβπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) β βπ β (1...π)βπ‘ β (πβπ)((π¦βπ)βπ‘) < (πΈ / π)) |
55 | 54 | r19.21bi 3237 |
. . . 4
β’ (((π β§ (π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (πβπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) β§ π β (1...π)) β βπ‘ β (πβπ)((π¦βπ)βπ‘) < (πΈ / π)) |
56 | 52 | simprbi 498 |
. . . . . 6
β’
(βπ β
(1...π)(βπ‘ β (πβπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)) β βπ β (1...π)βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)) |
57 | 56 | ad2antll 728 |
. . . . 5
β’ ((π β§ (π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (πβπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) β βπ β (1...π)βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)) |
58 | 57 | r19.21bi 3237 |
. . . 4
β’ (((π β§ (π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (πβπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) β§ π β (1...π)) β βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)) |
59 | | stoweidlem54.11 |
. . . . 5
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) |
60 | 59 | 3adant1r 1178 |
. . . 4
β’ (((π β§ (π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (πβπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) |
61 | | stoweidlem54.12 |
. . . . 5
β’ ((π β§ π β π΄) β π:πβΆβ) |
62 | 61 | adantlr 714 |
. . . 4
β’ (((π β§ (π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (πβπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) β§ π β π΄) β π:πβΆβ) |
63 | | stoweidlem54.19 |
. . . . 5
β’ (π β π β V) |
64 | 63 | adantr 482 |
. . . 4
β’ ((π β§ (π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (πβπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) β π β V) |
65 | | stoweidlem54.20 |
. . . . 5
β’ (π β πΈ β
β+) |
66 | 65 | adantr 482 |
. . . 4
β’ ((π β§ (π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (πβπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) β πΈ β
β+) |
67 | | stoweidlem54.21 |
. . . . 5
β’ (π β πΈ < (1 / 3)) |
68 | 67 | adantr 482 |
. . . 4
β’ ((π β§ (π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (πβπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) β πΈ < (1 / 3)) |
69 | 8, 23, 26, 29, 12, 30, 31, 32, 33, 35, 37, 38, 45, 47, 49, 51, 55, 58, 60, 62, 64, 66, 68 | stoweidlem51 44366 |
. . 3
β’ ((π β§ (π¦:(1...π)βΆπ β§ βπ β (1...π)(βπ‘ β (πβπ)((π¦βπ)βπ‘) < (πΈ / π) β§ βπ‘ β π΅ (1 β (πΈ / π)) < ((π¦βπ)βπ‘)))) β βπ₯(π₯ β π΄ β§ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π· (π₯βπ‘) < πΈ β§ βπ‘ β π΅ (1 β πΈ) < (π₯βπ‘)))) |
70 | 1, 2, 3, 69 | exlimdd 2214 |
. 2
β’ (π β βπ₯(π₯ β π΄ β§ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π· (π₯βπ‘) < πΈ β§ βπ‘ β π΅ (1 β πΈ) < (π₯βπ‘)))) |
71 | | df-rex 3075 |
. 2
β’
(βπ₯ β
π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π· (π₯βπ‘) < πΈ β§ βπ‘ β π΅ (1 β πΈ) < (π₯βπ‘)) β βπ₯(π₯ β π΄ β§ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π· (π₯βπ‘) < πΈ β§ βπ‘ β π΅ (1 β πΈ) < (π₯βπ‘)))) |
72 | 70, 71 | sylibr 233 |
1
β’ (π β βπ₯ β π΄ (βπ‘ β π (0 β€ (π₯βπ‘) β§ (π₯βπ‘) β€ 1) β§ βπ‘ β π· (π₯βπ‘) < πΈ β§ βπ‘ β π΅ (1 β πΈ) < (π₯βπ‘))) |