Step | Hyp | Ref
| Expression |
1 | | stoweidlem21.5 |
. . . 4
β’ πΊ = (π‘ β π β¦ ((π»βπ‘) + π)) |
2 | | stoweidlem21.4 |
. . . . 5
β’
β²π‘π |
3 | | stoweidlem21.7 |
. . . . . . . 8
β’ (π β π β β) |
4 | | fvconst2g 7155 |
. . . . . . . 8
β’ ((π β β β§ π‘ β π) β ((π Γ {π})βπ‘) = π) |
5 | 3, 4 | sylan 581 |
. . . . . . 7
β’ ((π β§ π‘ β π) β ((π Γ {π})βπ‘) = π) |
6 | 5 | eqcomd 2739 |
. . . . . 6
β’ ((π β§ π‘ β π) β π = ((π Γ {π})βπ‘)) |
7 | 6 | oveq2d 7377 |
. . . . 5
β’ ((π β§ π‘ β π) β ((π»βπ‘) + π) = ((π»βπ‘) + ((π Γ {π})βπ‘))) |
8 | 2, 7 | mpteq2da 5207 |
. . . 4
β’ (π β (π‘ β π β¦ ((π»βπ‘) + π)) = (π‘ β π β¦ ((π»βπ‘) + ((π Γ {π})βπ‘)))) |
9 | 1, 8 | eqtrid 2785 |
. . 3
β’ (π β πΊ = (π‘ β π β¦ ((π»βπ‘) + ((π Γ {π})βπ‘)))) |
10 | | stoweidlem21.11 |
. . . 4
β’ (π β π» β π΄) |
11 | | fconstmpt 5698 |
. . . . . 6
β’ (π Γ {π}) = (π β π β¦ π) |
12 | | stoweidlem21.3 |
. . . . . . 7
β’
β²π‘π |
13 | | nfcv 2904 |
. . . . . . 7
β’
β²π π |
14 | | eqidd 2734 |
. . . . . . 7
β’ (π = π‘ β π = π) |
15 | 12, 13, 14 | cbvmpt 5220 |
. . . . . 6
β’ (π β π β¦ π) = (π‘ β π β¦ π) |
16 | 11, 15 | eqtri 2761 |
. . . . 5
β’ (π Γ {π}) = (π‘ β π β¦ π) |
17 | 12 | nfeq2 2921 |
. . . . . . . . . 10
β’
β²π‘ π₯ = π |
18 | | simpl 484 |
. . . . . . . . . 10
β’ ((π₯ = π β§ π‘ β π) β π₯ = π) |
19 | 17, 18 | mpteq2da 5207 |
. . . . . . . . 9
β’ (π₯ = π β (π‘ β π β¦ π₯) = (π‘ β π β¦ π)) |
20 | 19 | eleq1d 2819 |
. . . . . . . 8
β’ (π₯ = π β ((π‘ β π β¦ π₯) β π΄ β (π‘ β π β¦ π) β π΄)) |
21 | 20 | imbi2d 341 |
. . . . . . 7
β’ (π₯ = π β ((π β (π‘ β π β¦ π₯) β π΄) β (π β (π‘ β π β¦ π) β π΄))) |
22 | | stoweidlem21.9 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β (π‘ β π β¦ π₯) β π΄) |
23 | 22 | expcom 415 |
. . . . . . 7
β’ (π₯ β β β (π β (π‘ β π β¦ π₯) β π΄)) |
24 | 21, 23 | vtoclga 3536 |
. . . . . 6
β’ (π β β β (π β (π‘ β π β¦ π) β π΄)) |
25 | 3, 24 | mpcom 38 |
. . . . 5
β’ (π β (π‘ β π β¦ π) β π΄) |
26 | 16, 25 | eqeltrid 2838 |
. . . 4
β’ (π β (π Γ {π}) β π΄) |
27 | | stoweidlem21.8 |
. . . . 5
β’ ((π β§ π β π΄ β§ π β π΄) β (π‘ β π β¦ ((πβπ‘) + (πβπ‘))) β π΄) |
28 | | stoweidlem21.2 |
. . . . 5
β’
β²π‘π» |
29 | | nfcv 2904 |
. . . . . 6
β’
β²π‘π |
30 | 12 | nfsn 4672 |
. . . . . 6
β’
β²π‘{π} |
31 | 29, 30 | nfxp 5670 |
. . . . 5
β’
β²π‘(π Γ {π}) |
32 | 27, 28, 31 | stoweidlem8 44339 |
. . . 4
β’ ((π β§ π» β π΄ β§ (π Γ {π}) β π΄) β (π‘ β π β¦ ((π»βπ‘) + ((π Γ {π})βπ‘))) β π΄) |
33 | 10, 26, 32 | mpd3an23 1464 |
. . 3
β’ (π β (π‘ β π β¦ ((π»βπ‘) + ((π Γ {π})βπ‘))) β π΄) |
34 | 9, 33 | eqeltrd 2834 |
. 2
β’ (π β πΊ β π΄) |
35 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π‘ β π) β π‘ β π) |
36 | | stoweidlem21.10 |
. . . . . . . . . . . 12
β’ (π β βπ β π΄ π:πβΆβ) |
37 | | feq1 6653 |
. . . . . . . . . . . . 13
β’ (π = π» β (π:πβΆβ β π»:πβΆβ)) |
38 | 37 | rspccva 3582 |
. . . . . . . . . . . 12
β’
((βπ β
π΄ π:πβΆβ β§ π» β π΄) β π»:πβΆβ) |
39 | 36, 10, 38 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β π»:πβΆβ) |
40 | 39 | ffvelcdmda 7039 |
. . . . . . . . . 10
β’ ((π β§ π‘ β π) β (π»βπ‘) β β) |
41 | 3 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π‘ β π) β π β β) |
42 | 40, 41 | readdcld 11192 |
. . . . . . . . 9
β’ ((π β§ π‘ β π) β ((π»βπ‘) + π) β β) |
43 | 1 | fvmpt2 6963 |
. . . . . . . . 9
β’ ((π‘ β π β§ ((π»βπ‘) + π) β β) β (πΊβπ‘) = ((π»βπ‘) + π)) |
44 | 35, 42, 43 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β (πΊβπ‘) = ((π»βπ‘) + π)) |
45 | 44 | oveq1d 7376 |
. . . . . . 7
β’ ((π β§ π‘ β π) β ((πΊβπ‘) β (πΉβπ‘)) = (((π»βπ‘) + π) β (πΉβπ‘))) |
46 | 40 | recnd 11191 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β (π»βπ‘) β β) |
47 | | stoweidlem21.6 |
. . . . . . . . . 10
β’ (π β πΉ:πβΆβ) |
48 | 47 | ffvelcdmda 7039 |
. . . . . . . . 9
β’ ((π β§ π‘ β π) β (πΉβπ‘) β β) |
49 | 48 | recnd 11191 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β (πΉβπ‘) β β) |
50 | 3 | recnd 11191 |
. . . . . . . . 9
β’ (π β π β β) |
51 | 50 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π‘ β π) β π β β) |
52 | 46, 49, 51 | subsub3d 11550 |
. . . . . . 7
β’ ((π β§ π‘ β π) β ((π»βπ‘) β ((πΉβπ‘) β π)) = (((π»βπ‘) + π) β (πΉβπ‘))) |
53 | 45, 52 | eqtr4d 2776 |
. . . . . 6
β’ ((π β§ π‘ β π) β ((πΊβπ‘) β (πΉβπ‘)) = ((π»βπ‘) β ((πΉβπ‘) β π))) |
54 | 53 | fveq2d 6850 |
. . . . 5
β’ ((π β§ π‘ β π) β (absβ((πΊβπ‘) β (πΉβπ‘))) = (absβ((π»βπ‘) β ((πΉβπ‘) β π)))) |
55 | | stoweidlem21.12 |
. . . . . 6
β’ (π β βπ‘ β π (absβ((π»βπ‘) β ((πΉβπ‘) β π))) < πΈ) |
56 | 55 | r19.21bi 3233 |
. . . . 5
β’ ((π β§ π‘ β π) β (absβ((π»βπ‘) β ((πΉβπ‘) β π))) < πΈ) |
57 | 54, 56 | eqbrtrd 5131 |
. . . 4
β’ ((π β§ π‘ β π) β (absβ((πΊβπ‘) β (πΉβπ‘))) < πΈ) |
58 | 57 | ex 414 |
. . 3
β’ (π β (π‘ β π β (absβ((πΊβπ‘) β (πΉβπ‘))) < πΈ)) |
59 | 2, 58 | ralrimi 3239 |
. 2
β’ (π β βπ‘ β π (absβ((πΊβπ‘) β (πΉβπ‘))) < πΈ) |
60 | | stoweidlem21.1 |
. . . . 5
β’
β²π‘πΊ |
61 | 60 | nfeq2 2921 |
. . . 4
β’
β²π‘ π = πΊ |
62 | | fveq1 6845 |
. . . . . . 7
β’ (π = πΊ β (πβπ‘) = (πΊβπ‘)) |
63 | 62 | oveq1d 7376 |
. . . . . 6
β’ (π = πΊ β ((πβπ‘) β (πΉβπ‘)) = ((πΊβπ‘) β (πΉβπ‘))) |
64 | 63 | fveq2d 6850 |
. . . . 5
β’ (π = πΊ β (absβ((πβπ‘) β (πΉβπ‘))) = (absβ((πΊβπ‘) β (πΉβπ‘)))) |
65 | 64 | breq1d 5119 |
. . . 4
β’ (π = πΊ β ((absβ((πβπ‘) β (πΉβπ‘))) < πΈ β (absβ((πΊβπ‘) β (πΉβπ‘))) < πΈ)) |
66 | 61, 65 | ralbid 3255 |
. . 3
β’ (π = πΊ β (βπ‘ β π (absβ((πβπ‘) β (πΉβπ‘))) < πΈ β βπ‘ β π (absβ((πΊβπ‘) β (πΉβπ‘))) < πΈ)) |
67 | 66 | rspcev 3583 |
. 2
β’ ((πΊ β π΄ β§ βπ‘ β π (absβ((πΊβπ‘) β (πΉβπ‘))) < πΈ) β βπ β π΄ βπ‘ β π (absβ((πβπ‘) β (πΉβπ‘))) < πΈ) |
68 | 34, 59, 67 | syl2anc 585 |
1
β’ (π β βπ β π΄ βπ‘ β π (absβ((πβπ‘) β (πΉβπ‘))) < πΈ) |