Step | Hyp | Ref
| Expression |
1 | | 0re 11162 |
. . . . 5
β’ 0 β
β |
2 | | stoweidlem55.10 |
. . . . . 6
β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) |
3 | 2 | stoweidlem4 44331 |
. . . . 5
β’ ((π β§ 0 β β) β
(π‘ β π β¦ 0) β π΄) |
4 | 1, 3 | mpan2 690 |
. . . 4
β’ (π β (π‘ β π β¦ 0) β π΄) |
5 | 4 | adantr 482 |
. . 3
β’ ((π β§ (π β π) = β
) β (π‘ β π β¦ 0) β π΄) |
6 | | stoweidlem55.2 |
. . . . 5
β’
β²π‘π |
7 | | nfcv 2904 |
. . . . . . 7
β’
β²π‘π |
8 | | stoweidlem55.1 |
. . . . . . 7
β’
β²π‘π |
9 | 7, 8 | nfdif 4086 |
. . . . . 6
β’
β²π‘(π β π) |
10 | | nfcv 2904 |
. . . . . 6
β’
β²π‘β
|
11 | 9, 10 | nfeq 2917 |
. . . . 5
β’
β²π‘(π β π) = β
|
12 | 6, 11 | nfan 1903 |
. . . 4
β’
β²π‘(π β§ (π β π) = β
) |
13 | | 0le0 12259 |
. . . . . . . 8
β’ 0 β€
0 |
14 | | 0cn 11152 |
. . . . . . . . 9
β’ 0 β
β |
15 | | eqid 2733 |
. . . . . . . . . 10
β’ (π‘ β π β¦ 0) = (π‘ β π β¦ 0) |
16 | 15 | fvmpt2 6960 |
. . . . . . . . 9
β’ ((π‘ β π β§ 0 β β) β ((π‘ β π β¦ 0)βπ‘) = 0) |
17 | 14, 16 | mpan2 690 |
. . . . . . . 8
β’ (π‘ β π β ((π‘ β π β¦ 0)βπ‘) = 0) |
18 | 13, 17 | breqtrrid 5144 |
. . . . . . 7
β’ (π‘ β π β 0 β€ ((π‘ β π β¦ 0)βπ‘)) |
19 | 18 | adantl 483 |
. . . . . 6
β’ (((π β§ (π β π) = β
) β§ π‘ β π) β 0 β€ ((π‘ β π β¦ 0)βπ‘)) |
20 | | 0le1 11683 |
. . . . . . . 8
β’ 0 β€
1 |
21 | 17, 20 | eqbrtrdi 5145 |
. . . . . . 7
β’ (π‘ β π β ((π‘ β π β¦ 0)βπ‘) β€ 1) |
22 | 21 | adantl 483 |
. . . . . 6
β’ (((π β§ (π β π) = β
) β§ π‘ β π) β ((π‘ β π β¦ 0)βπ‘) β€ 1) |
23 | 19, 22 | jca 513 |
. . . . 5
β’ (((π β§ (π β π) = β
) β§ π‘ β π) β (0 β€ ((π‘ β π β¦ 0)βπ‘) β§ ((π‘ β π β¦ 0)βπ‘) β€ 1)) |
24 | 23 | ex 414 |
. . . 4
β’ ((π β§ (π β π) = β
) β (π‘ β π β (0 β€ ((π‘ β π β¦ 0)βπ‘) β§ ((π‘ β π β¦ 0)βπ‘) β€ 1))) |
25 | 12, 24 | ralrimi 3239 |
. . 3
β’ ((π β§ (π β π) = β
) β βπ‘ β π (0 β€ ((π‘ β π β¦ 0)βπ‘) β§ ((π‘ β π β¦ 0)βπ‘) β€ 1)) |
26 | | stoweidlem55.13 |
. . . . . 6
β’ (π β π β π) |
27 | | stoweidlem55.12 |
. . . . . 6
β’ (π β π β π½) |
28 | 26, 27 | jca 513 |
. . . . 5
β’ (π β (π β π β§ π β π½)) |
29 | | elunii 4871 |
. . . . . 6
β’ ((π β π β§ π β π½) β π β βͺ π½) |
30 | | stoweidlem55.5 |
. . . . . 6
β’ π = βͺ
π½ |
31 | 29, 30 | eleqtrrdi 2845 |
. . . . 5
β’ ((π β π β§ π β π½) β π β π) |
32 | | eqidd 2734 |
. . . . . 6
β’ (π‘ = π β 0 = 0) |
33 | | c0ex 11154 |
. . . . . 6
β’ 0 β
V |
34 | 32, 15, 33 | fvmpt 6949 |
. . . . 5
β’ (π β π β ((π‘ β π β¦ 0)βπ) = 0) |
35 | 28, 31, 34 | 3syl 18 |
. . . 4
β’ (π β ((π‘ β π β¦ 0)βπ) = 0) |
36 | 35 | adantr 482 |
. . 3
β’ ((π β§ (π β π) = β
) β ((π‘ β π β¦ 0)βπ) = 0) |
37 | 11 | rzalf 43310 |
. . . 4
β’ ((π β π) = β
β βπ‘ β (π β π)0 < ((π‘ β π β¦ 0)βπ‘)) |
38 | 37 | adantl 483 |
. . 3
β’ ((π β§ (π β π) = β
) β βπ‘ β (π β π)0 < ((π‘ β π β¦ 0)βπ‘)) |
39 | | nfcv 2904 |
. . . . . . 7
β’
β²π‘π |
40 | | nfmpt1 5214 |
. . . . . . 7
β’
β²π‘(π‘ β π β¦ 0) |
41 | 39, 40 | nfeq 2917 |
. . . . . 6
β’
β²π‘ π = (π‘ β π β¦ 0) |
42 | | fveq1 6842 |
. . . . . . . 8
β’ (π = (π‘ β π β¦ 0) β (πβπ‘) = ((π‘ β π β¦ 0)βπ‘)) |
43 | 42 | breq2d 5118 |
. . . . . . 7
β’ (π = (π‘ β π β¦ 0) β (0 β€ (πβπ‘) β 0 β€ ((π‘ β π β¦ 0)βπ‘))) |
44 | 42 | breq1d 5116 |
. . . . . . 7
β’ (π = (π‘ β π β¦ 0) β ((πβπ‘) β€ 1 β ((π‘ β π β¦ 0)βπ‘) β€ 1)) |
45 | 43, 44 | anbi12d 632 |
. . . . . 6
β’ (π = (π‘ β π β¦ 0) β ((0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β (0 β€ ((π‘ β π β¦ 0)βπ‘) β§ ((π‘ β π β¦ 0)βπ‘) β€ 1))) |
46 | 41, 45 | ralbid 3255 |
. . . . 5
β’ (π = (π‘ β π β¦ 0) β (βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β βπ‘ β π (0 β€ ((π‘ β π β¦ 0)βπ‘) β§ ((π‘ β π β¦ 0)βπ‘) β€ 1))) |
47 | | fveq1 6842 |
. . . . . 6
β’ (π = (π‘ β π β¦ 0) β (πβπ) = ((π‘ β π β¦ 0)βπ)) |
48 | 47 | eqeq1d 2735 |
. . . . 5
β’ (π = (π‘ β π β¦ 0) β ((πβπ) = 0 β ((π‘ β π β¦ 0)βπ) = 0)) |
49 | 42 | breq2d 5118 |
. . . . . 6
β’ (π = (π‘ β π β¦ 0) β (0 < (πβπ‘) β 0 < ((π‘ β π β¦ 0)βπ‘))) |
50 | 41, 49 | ralbid 3255 |
. . . . 5
β’ (π = (π‘ β π β¦ 0) β (βπ‘ β (π β π)0 < (πβπ‘) β βπ‘ β (π β π)0 < ((π‘ β π β¦ 0)βπ‘))) |
51 | 46, 48, 50 | 3anbi123d 1437 |
. . . 4
β’ (π = (π‘ β π β¦ 0) β ((βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β§ (πβπ) = 0 β§ βπ‘ β (π β π)0 < (πβπ‘)) β (βπ‘ β π (0 β€ ((π‘ β π β¦ 0)βπ‘) β§ ((π‘ β π β¦ 0)βπ‘) β€ 1) β§ ((π‘ β π β¦ 0)βπ) = 0 β§ βπ‘ β (π β π)0 < ((π‘ β π β¦ 0)βπ‘)))) |
52 | 51 | rspcev 3580 |
. . 3
β’ (((π‘ β π β¦ 0) β π΄ β§ (βπ‘ β π (0 β€ ((π‘ β π β¦ 0)βπ‘) β§ ((π‘ β π β¦ 0)βπ‘) β€ 1) β§ ((π‘ β π β¦ 0)βπ) = 0 β§ βπ‘ β (π β π)0 < ((π‘ β π β¦ 0)βπ‘))) β βπ β π΄ (βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β§ (πβπ) = 0 β§ βπ‘ β (π β π)0 < (πβπ‘))) |
53 | 5, 25, 36, 38, 52 | syl13anc 1373 |
. 2
β’ ((π β§ (π β π) = β
) β βπ β π΄ (βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β§ (πβπ) = 0 β§ βπ‘ β (π β π)0 < (πβπ‘))) |
54 | 11 | nfn 1861 |
. . . 4
β’
β²π‘ Β¬
(π β π) = β
|
55 | 6, 54 | nfan 1903 |
. . 3
β’
β²π‘(π β§ Β¬ (π β π) = β
) |
56 | | stoweidlem55.3 |
. . 3
β’ πΎ = (topGenβran
(,)) |
57 | | stoweidlem55.14 |
. . 3
β’ π = {β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))} |
58 | | stoweidlem55.15 |
. . 3
β’ π = {π€ β π½ β£ ββ β π π€ = {π‘ β π β£ 0 < (ββπ‘)}} |
59 | | stoweidlem55.6 |
. . 3
β’ πΆ = (π½ Cn πΎ) |
60 | | stoweidlem55.4 |
. . . 4
β’ (π β π½ β Comp) |
61 | 60 | adantr 482 |
. . 3
β’ ((π β§ Β¬ (π β π) = β
) β π½ β Comp) |
62 | | stoweidlem55.7 |
. . . 4
β’ (π β π΄ β πΆ) |
63 | 62 | adantr 482 |
. . 3
β’ ((π β§ Β¬ (π β π) = β
) β π΄ β πΆ) |
64 | | stoweidlem55.8 |
. . . 4
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) |
65 | 64 | 3adant1r 1178 |
. . 3
β’ (((π β§ Β¬ (π β π) = β
) β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) |
66 | | stoweidlem55.9 |
. . . 4
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) |
67 | 66 | 3adant1r 1178 |
. . 3
β’ (((π β§ Β¬ (π β π) = β
) β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π΄) |
68 | 2 | adantlr 714 |
. . 3
β’ (((π β§ Β¬ (π β π) = β
) β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) |
69 | | stoweidlem55.11 |
. . . 4
β’ ((π β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘)) |
70 | 69 | adantlr 714 |
. . 3
β’ (((π β§ Β¬ (π β π) = β
) β§ (π β π β§ π‘ β π β§ π β π‘)) β βπ β π΄ (πβπ) β (πβπ‘)) |
71 | 27 | adantr 482 |
. . 3
β’ ((π β§ Β¬ (π β π) = β
) β π β π½) |
72 | | neqne 2948 |
. . . 4
β’ (Β¬
(π β π) = β
β (π β π) β β
) |
73 | 72 | adantl 483 |
. . 3
β’ ((π β§ Β¬ (π β π) = β
) β (π β π) β β
) |
74 | 26 | adantr 482 |
. . 3
β’ ((π β§ Β¬ (π β π) = β
) β π β π) |
75 | 8, 55, 56, 57, 58, 30, 59, 61, 63, 65, 67, 68, 70, 71, 73, 74 | stoweidlem53 44380 |
. 2
β’ ((π β§ Β¬ (π β π) = β
) β βπ β π΄ (βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β§ (πβπ) = 0 β§ βπ‘ β (π β π)0 < (πβπ‘))) |
76 | 53, 75 | pm2.61dan 812 |
1
β’ (π β βπ β π΄ (βπ‘ β π (0 β€ (πβπ‘) β§ (πβπ‘) β€ 1) β§ (πβπ) = 0 β§ βπ‘ β (π β π)0 < (πβπ‘))) |