Step | Hyp | Ref
| Expression |
1 | | cncfshift.f |
. . . . . 6
β’ (π β πΉ β (π΄βcnββ)) |
2 | | cncff 24279 |
. . . . . 6
β’ (πΉ β (π΄βcnββ) β πΉ:π΄βΆβ) |
3 | 1, 2 | syl 17 |
. . . . 5
β’ (π β πΉ:π΄βΆβ) |
4 | 3 | adantr 482 |
. . . 4
β’ ((π β§ π₯ β π΅) β πΉ:π΄βΆβ) |
5 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π₯ β π΅) β π₯ β π΅) |
6 | | cncfshift.b |
. . . . . . . 8
β’ π΅ = {π₯ β β β£ βπ¦ β π΄ π₯ = (π¦ + π)} |
7 | 5, 6 | eleqtrdi 2844 |
. . . . . . 7
β’ ((π β§ π₯ β π΅) β π₯ β {π₯ β β β£ βπ¦ β π΄ π₯ = (π¦ + π)}) |
8 | | rabid 3426 |
. . . . . . 7
β’ (π₯ β {π₯ β β β£ βπ¦ β π΄ π₯ = (π¦ + π)} β (π₯ β β β§ βπ¦ β π΄ π₯ = (π¦ + π))) |
9 | 7, 8 | sylib 217 |
. . . . . 6
β’ ((π β§ π₯ β π΅) β (π₯ β β β§ βπ¦ β π΄ π₯ = (π¦ + π))) |
10 | 9 | simprd 497 |
. . . . 5
β’ ((π β§ π₯ β π΅) β βπ¦ β π΄ π₯ = (π¦ + π)) |
11 | | oveq1 7368 |
. . . . . . . . 9
β’ (π₯ = (π¦ + π) β (π₯ β π) = ((π¦ + π) β π)) |
12 | 11 | 3ad2ant3 1136 |
. . . . . . . 8
β’ (((π β§ π₯ β π΅) β§ π¦ β π΄ β§ π₯ = (π¦ + π)) β (π₯ β π) = ((π¦ + π) β π)) |
13 | | cncfshift.a |
. . . . . . . . . . . 12
β’ (π β π΄ β β) |
14 | 13 | sselda 3948 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β π΄) β π¦ β β) |
15 | | cncfshift.t |
. . . . . . . . . . . 12
β’ (π β π β β) |
16 | 15 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β π΄) β π β β) |
17 | 14, 16 | pncand 11521 |
. . . . . . . . . 10
β’ ((π β§ π¦ β π΄) β ((π¦ + π) β π) = π¦) |
18 | 17 | adantlr 714 |
. . . . . . . . 9
β’ (((π β§ π₯ β π΅) β§ π¦ β π΄) β ((π¦ + π) β π) = π¦) |
19 | 18 | 3adant3 1133 |
. . . . . . . 8
β’ (((π β§ π₯ β π΅) β§ π¦ β π΄ β§ π₯ = (π¦ + π)) β ((π¦ + π) β π) = π¦) |
20 | 12, 19 | eqtrd 2773 |
. . . . . . 7
β’ (((π β§ π₯ β π΅) β§ π¦ β π΄ β§ π₯ = (π¦ + π)) β (π₯ β π) = π¦) |
21 | | simp2 1138 |
. . . . . . 7
β’ (((π β§ π₯ β π΅) β§ π¦ β π΄ β§ π₯ = (π¦ + π)) β π¦ β π΄) |
22 | 20, 21 | eqeltrd 2834 |
. . . . . 6
β’ (((π β§ π₯ β π΅) β§ π¦ β π΄ β§ π₯ = (π¦ + π)) β (π₯ β π) β π΄) |
23 | 22 | rexlimdv3a 3153 |
. . . . 5
β’ ((π β§ π₯ β π΅) β (βπ¦ β π΄ π₯ = (π¦ + π) β (π₯ β π) β π΄)) |
24 | 10, 23 | mpd 15 |
. . . 4
β’ ((π β§ π₯ β π΅) β (π₯ β π) β π΄) |
25 | 4, 24 | ffvelcdmd 7040 |
. . 3
β’ ((π β§ π₯ β π΅) β (πΉβ(π₯ β π)) β β) |
26 | | cncfshift.g |
. . 3
β’ πΊ = (π₯ β π΅ β¦ (πΉβ(π₯ β π))) |
27 | 25, 26 | fmptd 7066 |
. 2
β’ (π β πΊ:π΅βΆβ) |
28 | | fvoveq1 7384 |
. . . . . . . . . . 11
β’ (π = (π₯ β π) β (absβ(π β π)) = (absβ((π₯ β π) β π))) |
29 | 28 | breq1d 5119 |
. . . . . . . . . 10
β’ (π = (π₯ β π) β ((absβ(π β π)) < π§ β (absβ((π₯ β π) β π)) < π§)) |
30 | 29 | imbrov2fvoveq 7386 |
. . . . . . . . 9
β’ (π = (π₯ β π) β (((absβ(π β π)) < π§ β (absβ((πΉβπ) β (πΉβπ))) < π€) β ((absβ((π₯ β π) β π)) < π§ β (absβ((πΉβ(π₯ β π)) β (πΉβπ))) < π€))) |
31 | 30 | rexralbidv 3211 |
. . . . . . . 8
β’ (π = (π₯ β π) β (βπ§ β β+ βπ β π΄ ((absβ(π β π)) < π§ β (absβ((πΉβπ) β (πΉβπ))) < π€) β βπ§ β β+ βπ β π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ((πΉβ(π₯ β π)) β (πΉβπ))) < π€))) |
32 | 31 | ralbidv 3171 |
. . . . . . 7
β’ (π = (π₯ β π) β (βπ€ β β+ βπ§ β β+
βπ β π΄ ((absβ(π β π)) < π§ β (absβ((πΉβπ) β (πΉβπ))) < π€) β βπ€ β β+ βπ§ β β+
βπ β π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ((πΉβ(π₯ β π)) β (πΉβπ))) < π€))) |
33 | 1 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΅) β πΉ β (π΄βcnββ)) |
34 | 13 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΅) β π΄ β β) |
35 | | ssid 3970 |
. . . . . . . . . 10
β’ β
β β |
36 | | elcncf 24275 |
. . . . . . . . . 10
β’ ((π΄ β β β§ β
β β) β (πΉ
β (π΄βcnββ) β (πΉ:π΄βΆβ β§ βπ β π΄ βπ€ β β+ βπ§ β β+
βπ β π΄ ((absβ(π β π)) < π§ β (absβ((πΉβπ) β (πΉβπ))) < π€)))) |
37 | 34, 35, 36 | sylancl 587 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΅) β (πΉ β (π΄βcnββ) β (πΉ:π΄βΆβ β§ βπ β π΄ βπ€ β β+ βπ§ β β+
βπ β π΄ ((absβ(π β π)) < π§ β (absβ((πΉβπ) β (πΉβπ))) < π€)))) |
38 | 33, 37 | mpbid 231 |
. . . . . . . 8
β’ ((π β§ π₯ β π΅) β (πΉ:π΄βΆβ β§ βπ β π΄ βπ€ β β+ βπ§ β β+
βπ β π΄ ((absβ(π β π)) < π§ β (absβ((πΉβπ) β (πΉβπ))) < π€))) |
39 | 38 | simprd 497 |
. . . . . . 7
β’ ((π β§ π₯ β π΅) β βπ β π΄ βπ€ β β+ βπ§ β β+
βπ β π΄ ((absβ(π β π)) < π§ β (absβ((πΉβπ) β (πΉβπ))) < π€)) |
40 | 32, 39, 24 | rspcdva 3584 |
. . . . . 6
β’ ((π β§ π₯ β π΅) β βπ€ β β+ βπ§ β β+
βπ β π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ((πΉβ(π₯ β π)) β (πΉβπ))) < π€)) |
41 | 40 | adantrr 716 |
. . . . 5
β’ ((π β§ (π₯ β π΅ β§ π€ β β+)) β
βπ€ β
β+ βπ§ β β+ βπ β π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ((πΉβ(π₯ β π)) β (πΉβπ))) < π€)) |
42 | | simprr 772 |
. . . . 5
β’ ((π β§ (π₯ β π΅ β§ π€ β β+)) β π€ β
β+) |
43 | | rspa 3230 |
. . . . 5
β’
((βπ€ β
β+ βπ§ β β+ βπ β π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ((πΉβ(π₯ β π)) β (πΉβπ))) < π€) β§ π€ β β+) β
βπ§ β
β+ βπ β π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ((πΉβ(π₯ β π)) β (πΉβπ))) < π€)) |
44 | 41, 42, 43 | syl2anc 585 |
. . . 4
β’ ((π β§ (π₯ β π΅ β§ π€ β β+)) β
βπ§ β
β+ βπ β π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ((πΉβ(π₯ β π)) β (πΉβπ))) < π€)) |
45 | | simpl1l 1225 |
. . . . . . . . . . 11
β’ ((((π β§ (π₯ β π΅ β§ π€ β β+)) β§ π§ β β+
β§ βπ β
π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ((πΉβ(π₯ β π)) β (πΉβπ))) < π€)) β§ π£ β π΅) β π) |
46 | 45 | adantr 482 |
. . . . . . . . . 10
β’
(((((π β§ (π₯ β π΅ β§ π€ β β+)) β§ π§ β β+
β§ βπ β
π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ((πΉβ(π₯ β π)) β (πΉβπ))) < π€)) β§ π£ β π΅) β§ (absβ(π₯ β π£)) < π§) β π) |
47 | | simp1rl 1239 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β π΅ β§ π€ β β+)) β§ π§ β β+
β§ βπ β
π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ((πΉβ(π₯ β π)) β (πΉβπ))) < π€)) β π₯ β π΅) |
48 | 47 | ad2antrr 725 |
. . . . . . . . . 10
β’
(((((π β§ (π₯ β π΅ β§ π€ β β+)) β§ π§ β β+
β§ βπ β
π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ((πΉβ(π₯ β π)) β (πΉβπ))) < π€)) β§ π£ β π΅) β§ (absβ(π₯ β π£)) < π§) β π₯ β π΅) |
49 | | simplr 768 |
. . . . . . . . . 10
β’
(((((π β§ (π₯ β π΅ β§ π€ β β+)) β§ π§ β β+
β§ βπ β
π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ((πΉβ(π₯ β π)) β (πΉβπ))) < π€)) β§ π£ β π΅) β§ (absβ(π₯ β π£)) < π§) β π£ β π΅) |
50 | 26 | fvmpt2 6963 |
. . . . . . . . . . . . . 14
β’ ((π₯ β π΅ β§ (πΉβ(π₯ β π)) β β) β (πΊβπ₯) = (πΉβ(π₯ β π))) |
51 | 5, 25, 50 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β π΅) β (πΊβπ₯) = (πΉβ(π₯ β π))) |
52 | 51 | 3adant3 1133 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΅ β§ π£ β π΅) β (πΊβπ₯) = (πΉβ(π₯ β π))) |
53 | | fvoveq1 7384 |
. . . . . . . . . . . . . 14
β’ (π₯ = π£ β (πΉβ(π₯ β π)) = (πΉβ(π£ β π))) |
54 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π β§ π£ β π΅) β π£ β π΅) |
55 | 3 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π£ β π΅) β πΉ:π΄βΆβ) |
56 | | eleq1w 2817 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π£ β (π₯ β π΅ β π£ β π΅)) |
57 | 56 | anbi2d 630 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π£ β ((π β§ π₯ β π΅) β (π β§ π£ β π΅))) |
58 | | oveq1 7368 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π£ β (π₯ β π) = (π£ β π)) |
59 | 58 | eleq1d 2819 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π£ β ((π₯ β π) β π΄ β (π£ β π) β π΄)) |
60 | 57, 59 | imbi12d 345 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π£ β (((π β§ π₯ β π΅) β (π₯ β π) β π΄) β ((π β§ π£ β π΅) β (π£ β π) β π΄))) |
61 | 60, 24 | chvarvv 2003 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π£ β π΅) β (π£ β π) β π΄) |
62 | 55, 61 | ffvelcdmd 7040 |
. . . . . . . . . . . . . 14
β’ ((π β§ π£ β π΅) β (πΉβ(π£ β π)) β β) |
63 | 26, 53, 54, 62 | fvmptd3 6975 |
. . . . . . . . . . . . 13
β’ ((π β§ π£ β π΅) β (πΊβπ£) = (πΉβ(π£ β π))) |
64 | 63 | 3adant2 1132 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΅ β§ π£ β π΅) β (πΊβπ£) = (πΉβ(π£ β π))) |
65 | 52, 64 | oveq12d 7379 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΅ β§ π£ β π΅) β ((πΊβπ₯) β (πΊβπ£)) = ((πΉβ(π₯ β π)) β (πΉβ(π£ β π)))) |
66 | 65 | fveq2d 6850 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΅ β§ π£ β π΅) β (absβ((πΊβπ₯) β (πΊβπ£))) = (absβ((πΉβ(π₯ β π)) β (πΉβ(π£ β π))))) |
67 | 46, 48, 49, 66 | syl3anc 1372 |
. . . . . . . . 9
β’
(((((π β§ (π₯ β π΅ β§ π€ β β+)) β§ π§ β β+
β§ βπ β
π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ((πΉβ(π₯ β π)) β (πΉβπ))) < π€)) β§ π£ β π΅) β§ (absβ(π₯ β π£)) < π§) β (absβ((πΊβπ₯) β (πΊβπ£))) = (absβ((πΉβ(π₯ β π)) β (πΉβ(π£ β π))))) |
68 | | simpr 486 |
. . . . . . . . . . 11
β’
(((((π β§ (π₯ β π΅ β§ π€ β β+)) β§ π§ β β+
β§ βπ β
π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ((πΉβ(π₯ β π)) β (πΉβπ))) < π€)) β§ π£ β π΅) β§ (absβ(π₯ β π£)) < π§) β (absβ(π₯ β π£)) < π§) |
69 | 9 | simpld 496 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β π΅) β π₯ β β) |
70 | 69 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β π΅) β§ π£ β π΅) β π₯ β β) |
71 | 6 | ssrab3 4044 |
. . . . . . . . . . . . . . . . 17
β’ π΅ β
β |
72 | 71 | sseli 3944 |
. . . . . . . . . . . . . . . 16
β’ (π£ β π΅ β π£ β β) |
73 | 72 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β π΅) β§ π£ β π΅) β π£ β β) |
74 | 15 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β π΅) β§ π£ β π΅) β π β β) |
75 | 70, 73, 74 | nnncan2d 11555 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β π΅) β§ π£ β π΅) β ((π₯ β π) β (π£ β π)) = (π₯ β π£)) |
76 | 75 | fveq2d 6850 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β π΅) β§ π£ β π΅) β (absβ((π₯ β π) β (π£ β π))) = (absβ(π₯ β π£))) |
77 | 76 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β π΅) β§ π£ β π΅) β§ (absβ(π₯ β π£)) < π§) β (absβ((π₯ β π) β (π£ β π))) = (absβ(π₯ β π£))) |
78 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β π΅) β§ π£ β π΅) β§ (absβ(π₯ β π£)) < π§) β (absβ(π₯ β π£)) < π§) |
79 | 77, 78 | eqbrtrd 5131 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β π΅) β§ π£ β π΅) β§ (absβ(π₯ β π£)) < π§) β (absβ((π₯ β π) β (π£ β π))) < π§) |
80 | 46, 48, 49, 68, 79 | syl1111anc 839 |
. . . . . . . . . 10
β’
(((((π β§ (π₯ β π΅ β§ π€ β β+)) β§ π§ β β+
β§ βπ β
π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ((πΉβ(π₯ β π)) β (πΉβπ))) < π€)) β§ π£ β π΅) β§ (absβ(π₯ β π£)) < π§) β (absβ((π₯ β π) β (π£ β π))) < π§) |
81 | | oveq2 7369 |
. . . . . . . . . . . . . 14
β’ (π = (π£ β π) β ((π₯ β π) β π) = ((π₯ β π) β (π£ β π))) |
82 | 81 | fveq2d 6850 |
. . . . . . . . . . . . 13
β’ (π = (π£ β π) β (absβ((π₯ β π) β π)) = (absβ((π₯ β π) β (π£ β π)))) |
83 | 82 | breq1d 5119 |
. . . . . . . . . . . 12
β’ (π = (π£ β π) β ((absβ((π₯ β π) β π)) < π§ β (absβ((π₯ β π) β (π£ β π))) < π§)) |
84 | | fveq2 6846 |
. . . . . . . . . . . . . . 15
β’ (π = (π£ β π) β (πΉβπ) = (πΉβ(π£ β π))) |
85 | 84 | oveq2d 7377 |
. . . . . . . . . . . . . 14
β’ (π = (π£ β π) β ((πΉβ(π₯ β π)) β (πΉβπ)) = ((πΉβ(π₯ β π)) β (πΉβ(π£ β π)))) |
86 | 85 | fveq2d 6850 |
. . . . . . . . . . . . 13
β’ (π = (π£ β π) β (absβ((πΉβ(π₯ β π)) β (πΉβπ))) = (absβ((πΉβ(π₯ β π)) β (πΉβ(π£ β π))))) |
87 | 86 | breq1d 5119 |
. . . . . . . . . . . 12
β’ (π = (π£ β π) β ((absβ((πΉβ(π₯ β π)) β (πΉβπ))) < π€ β (absβ((πΉβ(π₯ β π)) β (πΉβ(π£ β π)))) < π€)) |
88 | 83, 87 | imbi12d 345 |
. . . . . . . . . . 11
β’ (π = (π£ β π) β (((absβ((π₯ β π) β π)) < π§ β (absβ((πΉβ(π₯ β π)) β (πΉβπ))) < π€) β ((absβ((π₯ β π) β (π£ β π))) < π§ β (absβ((πΉβ(π₯ β π)) β (πΉβ(π£ β π)))) < π€))) |
89 | | simpll3 1215 |
. . . . . . . . . . 11
β’
(((((π β§ (π₯ β π΅ β§ π€ β β+)) β§ π§ β β+
β§ βπ β
π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ((πΉβ(π₯ β π)) β (πΉβπ))) < π€)) β§ π£ β π΅) β§ (absβ(π₯ β π£)) < π§) β βπ β π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ((πΉβ(π₯ β π)) β (πΉβπ))) < π€)) |
90 | 46, 49, 61 | syl2anc 585 |
. . . . . . . . . . 11
β’
(((((π β§ (π₯ β π΅ β§ π€ β β+)) β§ π§ β β+
β§ βπ β
π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ((πΉβ(π₯ β π)) β (πΉβπ))) < π€)) β§ π£ β π΅) β§ (absβ(π₯ β π£)) < π§) β (π£ β π) β π΄) |
91 | 88, 89, 90 | rspcdva 3584 |
. . . . . . . . . 10
β’
(((((π β§ (π₯ β π΅ β§ π€ β β+)) β§ π§ β β+
β§ βπ β
π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ((πΉβ(π₯ β π)) β (πΉβπ))) < π€)) β§ π£ β π΅) β§ (absβ(π₯ β π£)) < π§) β ((absβ((π₯ β π) β (π£ β π))) < π§ β (absβ((πΉβ(π₯ β π)) β (πΉβ(π£ β π)))) < π€)) |
92 | 80, 91 | mpd 15 |
. . . . . . . . 9
β’
(((((π β§ (π₯ β π΅ β§ π€ β β+)) β§ π§ β β+
β§ βπ β
π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ((πΉβ(π₯ β π)) β (πΉβπ))) < π€)) β§ π£ β π΅) β§ (absβ(π₯ β π£)) < π§) β (absβ((πΉβ(π₯ β π)) β (πΉβ(π£ β π)))) < π€) |
93 | 67, 92 | eqbrtrd 5131 |
. . . . . . . 8
β’
(((((π β§ (π₯ β π΅ β§ π€ β β+)) β§ π§ β β+
β§ βπ β
π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ((πΉβ(π₯ β π)) β (πΉβπ))) < π€)) β§ π£ β π΅) β§ (absβ(π₯ β π£)) < π§) β (absβ((πΊβπ₯) β (πΊβπ£))) < π€) |
94 | 93 | ex 414 |
. . . . . . 7
β’ ((((π β§ (π₯ β π΅ β§ π€ β β+)) β§ π§ β β+
β§ βπ β
π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ((πΉβ(π₯ β π)) β (πΉβπ))) < π€)) β§ π£ β π΅) β ((absβ(π₯ β π£)) < π§ β (absβ((πΊβπ₯) β (πΊβπ£))) < π€)) |
95 | 94 | ralrimiva 3140 |
. . . . . 6
β’ (((π β§ (π₯ β π΅ β§ π€ β β+)) β§ π§ β β+
β§ βπ β
π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ((πΉβ(π₯ β π)) β (πΉβπ))) < π€)) β βπ£ β π΅ ((absβ(π₯ β π£)) < π§ β (absβ((πΊβπ₯) β (πΊβπ£))) < π€)) |
96 | 95 | 3exp 1120 |
. . . . 5
β’ ((π β§ (π₯ β π΅ β§ π€ β β+)) β (π§ β β+
β (βπ β
π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ((πΉβ(π₯ β π)) β (πΉβπ))) < π€) β βπ£ β π΅ ((absβ(π₯ β π£)) < π§ β (absβ((πΊβπ₯) β (πΊβπ£))) < π€)))) |
97 | 96 | reximdvai 3159 |
. . . 4
β’ ((π β§ (π₯ β π΅ β§ π€ β β+)) β
(βπ§ β
β+ βπ β π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ((πΉβ(π₯ β π)) β (πΉβπ))) < π€) β βπ§ β β+ βπ£ β π΅ ((absβ(π₯ β π£)) < π§ β (absβ((πΊβπ₯) β (πΊβπ£))) < π€))) |
98 | 44, 97 | mpd 15 |
. . 3
β’ ((π β§ (π₯ β π΅ β§ π€ β β+)) β
βπ§ β
β+ βπ£ β π΅ ((absβ(π₯ β π£)) < π§ β (absβ((πΊβπ₯) β (πΊβπ£))) < π€)) |
99 | 98 | ralrimivva 3194 |
. 2
β’ (π β βπ₯ β π΅ βπ€ β β+ βπ§ β β+
βπ£ β π΅ ((absβ(π₯ β π£)) < π§ β (absβ((πΊβπ₯) β (πΊβπ£))) < π€)) |
100 | 71 | a1i 11 |
. . . 4
β’ (π β π΅ β β) |
101 | | elcncf 24275 |
. . . 4
β’ ((π΅ β β β§ β
β β) β (πΊ
β (π΅βcnββ) β (πΊ:π΅βΆβ β§ βπ β π΅ βπ€ β β+ βπ§ β β+
βπ£ β π΅ ((absβ(π β π£)) < π§ β (absβ((πΊβπ) β (πΊβπ£))) < π€)))) |
102 | 100, 35, 101 | sylancl 587 |
. . 3
β’ (π β (πΊ β (π΅βcnββ) β (πΊ:π΅βΆβ β§ βπ β π΅ βπ€ β β+ βπ§ β β+
βπ£ β π΅ ((absβ(π β π£)) < π§ β (absβ((πΊβπ) β (πΊβπ£))) < π€)))) |
103 | | nfcv 2904 |
. . . . . . 7
β’
β²π₯β+ |
104 | | nfcv 2904 |
. . . . . . . . 9
β’
β²π₯π΅ |
105 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π₯(absβ(π β π£)) < π§ |
106 | | nfcv 2904 |
. . . . . . . . . . . 12
β’
β²π₯abs |
107 | | nfmpt1 5217 |
. . . . . . . . . . . . . . 15
β’
β²π₯(π₯ β π΅ β¦ (πΉβ(π₯ β π))) |
108 | 26, 107 | nfcxfr 2902 |
. . . . . . . . . . . . . 14
β’
β²π₯πΊ |
109 | | nfcv 2904 |
. . . . . . . . . . . . . 14
β’
β²π₯π |
110 | 108, 109 | nffv 6856 |
. . . . . . . . . . . . 13
β’
β²π₯(πΊβπ) |
111 | | nfcv 2904 |
. . . . . . . . . . . . 13
β’
β²π₯
β |
112 | | nfcv 2904 |
. . . . . . . . . . . . . 14
β’
β²π₯π£ |
113 | 108, 112 | nffv 6856 |
. . . . . . . . . . . . 13
β’
β²π₯(πΊβπ£) |
114 | 110, 111,
113 | nfov 7391 |
. . . . . . . . . . . 12
β’
β²π₯((πΊβπ) β (πΊβπ£)) |
115 | 106, 114 | nffv 6856 |
. . . . . . . . . . 11
β’
β²π₯(absβ((πΊβπ) β (πΊβπ£))) |
116 | | nfcv 2904 |
. . . . . . . . . . 11
β’
β²π₯
< |
117 | | nfcv 2904 |
. . . . . . . . . . 11
β’
β²π₯π€ |
118 | 115, 116,
117 | nfbr 5156 |
. . . . . . . . . 10
β’
β²π₯(absβ((πΊβπ) β (πΊβπ£))) < π€ |
119 | 105, 118 | nfim 1900 |
. . . . . . . . 9
β’
β²π₯((absβ(π β π£)) < π§ β (absβ((πΊβπ) β (πΊβπ£))) < π€) |
120 | 104, 119 | nfralw 3293 |
. . . . . . . 8
β’
β²π₯βπ£ β π΅ ((absβ(π β π£)) < π§ β (absβ((πΊβπ) β (πΊβπ£))) < π€) |
121 | 103, 120 | nfrexw 3295 |
. . . . . . 7
β’
β²π₯βπ§ β β+
βπ£ β π΅ ((absβ(π β π£)) < π§ β (absβ((πΊβπ) β (πΊβπ£))) < π€) |
122 | 103, 121 | nfralw 3293 |
. . . . . 6
β’
β²π₯βπ€ β β+ βπ§ β β+
βπ£ β π΅ ((absβ(π β π£)) < π§ β (absβ((πΊβπ) β (πΊβπ£))) < π€) |
123 | | nfv 1918 |
. . . . . 6
β’
β²πβπ€ β β+ βπ§ β β+
βπ£ β π΅ ((absβ(π₯ β π£)) < π§ β (absβ((πΊβπ₯) β (πΊβπ£))) < π€) |
124 | | fvoveq1 7384 |
. . . . . . . . . 10
β’ (π = π₯ β (absβ(π β π£)) = (absβ(π₯ β π£))) |
125 | 124 | breq1d 5119 |
. . . . . . . . 9
β’ (π = π₯ β ((absβ(π β π£)) < π§ β (absβ(π₯ β π£)) < π§)) |
126 | 125 | imbrov2fvoveq 7386 |
. . . . . . . 8
β’ (π = π₯ β (((absβ(π β π£)) < π§ β (absβ((πΊβπ) β (πΊβπ£))) < π€) β ((absβ(π₯ β π£)) < π§ β (absβ((πΊβπ₯) β (πΊβπ£))) < π€))) |
127 | 126 | rexralbidv 3211 |
. . . . . . 7
β’ (π = π₯ β (βπ§ β β+ βπ£ β π΅ ((absβ(π β π£)) < π§ β (absβ((πΊβπ) β (πΊβπ£))) < π€) β βπ§ β β+ βπ£ β π΅ ((absβ(π₯ β π£)) < π§ β (absβ((πΊβπ₯) β (πΊβπ£))) < π€))) |
128 | 127 | ralbidv 3171 |
. . . . . 6
β’ (π = π₯ β (βπ€ β β+ βπ§ β β+
βπ£ β π΅ ((absβ(π β π£)) < π§ β (absβ((πΊβπ) β (πΊβπ£))) < π€) β βπ€ β β+ βπ§ β β+
βπ£ β π΅ ((absβ(π₯ β π£)) < π§ β (absβ((πΊβπ₯) β (πΊβπ£))) < π€))) |
129 | 122, 123,
128 | cbvralw 3288 |
. . . . 5
β’
(βπ β
π΅ βπ€ β β+
βπ§ β
β+ βπ£ β π΅ ((absβ(π β π£)) < π§ β (absβ((πΊβπ) β (πΊβπ£))) < π€) β βπ₯ β π΅ βπ€ β β+ βπ§ β β+
βπ£ β π΅ ((absβ(π₯ β π£)) < π§ β (absβ((πΊβπ₯) β (πΊβπ£))) < π€)) |
130 | 129 | bicomi 223 |
. . . 4
β’
(βπ₯ β
π΅ βπ€ β β+
βπ§ β
β+ βπ£ β π΅ ((absβ(π₯ β π£)) < π§ β (absβ((πΊβπ₯) β (πΊβπ£))) < π€) β βπ β π΅ βπ€ β β+ βπ§ β β+
βπ£ β π΅ ((absβ(π β π£)) < π§ β (absβ((πΊβπ) β (πΊβπ£))) < π€)) |
131 | 130 | anbi2i 624 |
. . 3
β’ ((πΊ:π΅βΆβ β§ βπ₯ β π΅ βπ€ β β+ βπ§ β β+
βπ£ β π΅ ((absβ(π₯ β π£)) < π§ β (absβ((πΊβπ₯) β (πΊβπ£))) < π€)) β (πΊ:π΅βΆβ β§ βπ β π΅ βπ€ β β+ βπ§ β β+
βπ£ β π΅ ((absβ(π β π£)) < π§ β (absβ((πΊβπ) β (πΊβπ£))) < π€))) |
132 | 102, 131 | bitr4di 289 |
. 2
β’ (π β (πΊ β (π΅βcnββ) β (πΊ:π΅βΆβ β§ βπ₯ β π΅ βπ€ β β+ βπ§ β β+
βπ£ β π΅ ((absβ(π₯ β π£)) < π§ β (absβ((πΊβπ₯) β (πΊβπ£))) < π€)))) |
133 | 27, 99, 132 | mpbir2and 712 |
1
β’ (π β πΊ β (π΅βcnββ)) |