Step | Hyp | Ref
| Expression |
1 | | limccl 25383 |
. . 3
β’ ((πΉ βΎ π΄) limβ π·) β β |
2 | | limcperiod.clim |
. . 3
β’ (π β πΆ β ((πΉ βΎ π΄) limβ π·)) |
3 | 1, 2 | sselid 3979 |
. 2
β’ (π β πΆ β β) |
4 | | limcperiod.f |
. . . . . . . . 9
β’ (π β πΉ:dom πΉβΆβ) |
5 | | limcperiod.3 |
. . . . . . . . 9
β’ (π β π΄ β dom πΉ) |
6 | 4, 5 | fssresd 6755 |
. . . . . . . 8
β’ (π β (πΉ βΎ π΄):π΄βΆβ) |
7 | | limcperiod.assc |
. . . . . . . 8
β’ (π β π΄ β β) |
8 | | limcrcl 25382 |
. . . . . . . . . 10
β’ (πΆ β ((πΉ βΎ π΄) limβ π·) β ((πΉ βΎ π΄):dom (πΉ βΎ π΄)βΆβ β§ dom (πΉ βΎ π΄) β β β§ π· β β)) |
9 | 2, 8 | syl 17 |
. . . . . . . . 9
β’ (π β ((πΉ βΎ π΄):dom (πΉ βΎ π΄)βΆβ β§ dom (πΉ βΎ π΄) β β β§ π· β β)) |
10 | 9 | simp3d 1144 |
. . . . . . . 8
β’ (π β π· β β) |
11 | 6, 7, 10 | ellimc3 25387 |
. . . . . . 7
β’ (π β (πΆ β ((πΉ βΎ π΄) limβ π·) β (πΆ β β β§ βπ€ β β+
βπ§ β
β+ βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)))) |
12 | 2, 11 | mpbid 231 |
. . . . . 6
β’ (π β (πΆ β β β§ βπ€ β β+
βπ§ β
β+ βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€))) |
13 | 12 | simprd 496 |
. . . . 5
β’ (π β βπ€ β β+ βπ§ β β+
βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) |
14 | 13 | r19.21bi 3248 |
. . . 4
β’ ((π β§ π€ β β+) β
βπ§ β
β+ βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) |
15 | | simpl1l 1224 |
. . . . . . . . . . 11
β’ ((((π β§ π€ β β+) β§ π§ β β+
β§ βπ¦ β
π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β§ π β π΅) β π) |
16 | 15 | adantr 481 |
. . . . . . . . . 10
β’
(((((π β§ π€ β β+)
β§ π§ β
β+ β§ βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β§ π β π΅) β§ (π β (π· + π) β§ (absβ(π β (π· + π))) < π§)) β π) |
17 | | simplr 767 |
. . . . . . . . . 10
β’
(((((π β§ π€ β β+)
β§ π§ β
β+ β§ βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β§ π β π΅) β§ (π β (π· + π) β§ (absβ(π β (π· + π))) < π§)) β π β π΅) |
18 | | id 22 |
. . . . . . . . . . . . . . . 16
β’ (π β π΅ β π β π΅) |
19 | | limcperiod.b |
. . . . . . . . . . . . . . . . 17
β’ π΅ = {π₯ β β β£ βπ¦ β π΄ π₯ = (π¦ + π)} |
20 | | oveq1 7412 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π¦ = π§ β (π¦ + π) = (π§ + π)) |
21 | 20 | eqeq2d 2743 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ = π§ β (π₯ = (π¦ + π) β π₯ = (π§ + π))) |
22 | 21 | cbvrexvw 3235 |
. . . . . . . . . . . . . . . . . . 19
β’
(βπ¦ β
π΄ π₯ = (π¦ + π) β βπ§ β π΄ π₯ = (π§ + π)) |
23 | | eqeq1 2736 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ = π€ β (π₯ = (π§ + π) β π€ = (π§ + π))) |
24 | 23 | rexbidv 3178 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ = π€ β (βπ§ β π΄ π₯ = (π§ + π) β βπ§ β π΄ π€ = (π§ + π))) |
25 | 22, 24 | bitrid 282 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π€ β (βπ¦ β π΄ π₯ = (π¦ + π) β βπ§ β π΄ π€ = (π§ + π))) |
26 | 25 | cbvrabv 3442 |
. . . . . . . . . . . . . . . . 17
β’ {π₯ β β β£
βπ¦ β π΄ π₯ = (π¦ + π)} = {π€ β β β£ βπ§ β π΄ π€ = (π§ + π)} |
27 | 19, 26 | eqtri 2760 |
. . . . . . . . . . . . . . . 16
β’ π΅ = {π€ β β β£ βπ§ β π΄ π€ = (π§ + π)} |
28 | 18, 27 | eleqtrdi 2843 |
. . . . . . . . . . . . . . 15
β’ (π β π΅ β π β {π€ β β β£ βπ§ β π΄ π€ = (π§ + π)}) |
29 | | eqeq1 2736 |
. . . . . . . . . . . . . . . . 17
β’ (π€ = π β (π€ = (π§ + π) β π = (π§ + π))) |
30 | 29 | rexbidv 3178 |
. . . . . . . . . . . . . . . 16
β’ (π€ = π β (βπ§ β π΄ π€ = (π§ + π) β βπ§ β π΄ π = (π§ + π))) |
31 | 30 | elrab 3682 |
. . . . . . . . . . . . . . 15
β’ (π β {π€ β β β£ βπ§ β π΄ π€ = (π§ + π)} β (π β β β§ βπ§ β π΄ π = (π§ + π))) |
32 | 28, 31 | sylib 217 |
. . . . . . . . . . . . . 14
β’ (π β π΅ β (π β β β§ βπ§ β π΄ π = (π§ + π))) |
33 | 32 | simprd 496 |
. . . . . . . . . . . . 13
β’ (π β π΅ β βπ§ β π΄ π = (π§ + π)) |
34 | 33 | adantl 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΅) β βπ§ β π΄ π = (π§ + π)) |
35 | | oveq1 7412 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (π§ + π) β (π β π) = ((π§ + π) β π)) |
36 | 35 | 3ad2ant3 1135 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π§ β π΄ β§ π = (π§ + π)) β (π β π) = ((π§ + π) β π)) |
37 | 7 | sselda 3981 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π§ β π΄) β π§ β β) |
38 | | limcperiod.t |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π β β) |
39 | 38 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π§ β π΄) β π β β) |
40 | 37, 39 | pncand 11568 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π§ β π΄) β ((π§ + π) β π) = π§) |
41 | 40 | 3adant3 1132 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π§ β π΄ β§ π = (π§ + π)) β ((π§ + π) β π) = π§) |
42 | 36, 41 | eqtrd 2772 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π§ β π΄ β§ π = (π§ + π)) β (π β π) = π§) |
43 | | simp2 1137 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π§ β π΄ β§ π = (π§ + π)) β π§ β π΄) |
44 | 42, 43 | eqeltrd 2833 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π§ β π΄ β§ π = (π§ + π)) β (π β π) β π΄) |
45 | 44 | 3exp 1119 |
. . . . . . . . . . . . . 14
β’ (π β (π§ β π΄ β (π = (π§ + π) β (π β π) β π΄))) |
46 | 45 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΅) β (π§ β π΄ β (π = (π§ + π) β (π β π) β π΄))) |
47 | 46 | rexlimdv 3153 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΅) β (βπ§ β π΄ π = (π§ + π) β (π β π) β π΄)) |
48 | 34, 47 | mpd 15 |
. . . . . . . . . . 11
β’ ((π β§ π β π΅) β (π β π) β π΄) |
49 | 19 | ssrab3 4079 |
. . . . . . . . . . . . . . 15
β’ π΅ β
β |
50 | 49 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β π΅ β β) |
51 | 50 | sselda 3981 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΅) β π β β) |
52 | 38 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΅) β π β β) |
53 | 51, 52 | npcand 11571 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΅) β ((π β π) + π) = π) |
54 | 53 | eqcomd 2738 |
. . . . . . . . . . 11
β’ ((π β§ π β π΅) β π = ((π β π) + π)) |
55 | | oveq1 7412 |
. . . . . . . . . . . 12
β’ (π₯ = (π β π) β (π₯ + π) = ((π β π) + π)) |
56 | 55 | rspceeqv 3632 |
. . . . . . . . . . 11
β’ (((π β π) β π΄ β§ π = ((π β π) + π)) β βπ₯ β π΄ π = (π₯ + π)) |
57 | 48, 54, 56 | syl2anc 584 |
. . . . . . . . . 10
β’ ((π β§ π β π΅) β βπ₯ β π΄ π = (π₯ + π)) |
58 | 16, 17, 57 | syl2anc 584 |
. . . . . . . . 9
β’
(((((π β§ π€ β β+)
β§ π§ β
β+ β§ βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β§ π β π΅) β§ (π β (π· + π) β§ (absβ(π β (π· + π))) < π§)) β βπ₯ β π΄ π = (π₯ + π)) |
59 | | nfv 1917 |
. . . . . . . . . . . 12
β’
β²π₯((π β§ π€ β β+) β§ π§ β β+
β§ βπ¦ β
π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) |
60 | | nfrab1 3451 |
. . . . . . . . . . . . . 14
β’
β²π₯{π₯ β β β£ βπ¦ β π΄ π₯ = (π¦ + π)} |
61 | 19, 60 | nfcxfr 2901 |
. . . . . . . . . . . . 13
β’
β²π₯π΅ |
62 | 61 | nfcri 2890 |
. . . . . . . . . . . 12
β’
β²π₯ π β π΅ |
63 | 59, 62 | nfan 1902 |
. . . . . . . . . . 11
β’
β²π₯(((π β§ π€ β β+) β§ π§ β β+
β§ βπ¦ β
π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β§ π β π΅) |
64 | | nfv 1917 |
. . . . . . . . . . 11
β’
β²π₯(π β (π· + π) β§ (absβ(π β (π· + π))) < π§) |
65 | 63, 64 | nfan 1902 |
. . . . . . . . . 10
β’
β²π₯((((π β§ π€ β β+) β§ π§ β β+
β§ βπ¦ β
π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β§ π β π΅) β§ (π β (π· + π) β§ (absβ(π β (π· + π))) < π§)) |
66 | | nfcv 2903 |
. . . . . . . . . . . 12
β’
β²π₯abs |
67 | | nfcv 2903 |
. . . . . . . . . . . . . . 15
β’
β²π₯πΉ |
68 | 67, 61 | nfres 5981 |
. . . . . . . . . . . . . 14
β’
β²π₯(πΉ βΎ π΅) |
69 | | nfcv 2903 |
. . . . . . . . . . . . . 14
β’
β²π₯π |
70 | 68, 69 | nffv 6898 |
. . . . . . . . . . . . 13
β’
β²π₯((πΉ βΎ π΅)βπ) |
71 | | nfcv 2903 |
. . . . . . . . . . . . 13
β’
β²π₯
β |
72 | | nfcv 2903 |
. . . . . . . . . . . . 13
β’
β²π₯πΆ |
73 | 70, 71, 72 | nfov 7435 |
. . . . . . . . . . . 12
β’
β²π₯(((πΉ βΎ π΅)βπ) β πΆ) |
74 | 66, 73 | nffv 6898 |
. . . . . . . . . . 11
β’
β²π₯(absβ(((πΉ βΎ π΅)βπ) β πΆ)) |
75 | | nfcv 2903 |
. . . . . . . . . . 11
β’
β²π₯
< |
76 | | nfcv 2903 |
. . . . . . . . . . 11
β’
β²π₯π€ |
77 | 74, 75, 76 | nfbr 5194 |
. . . . . . . . . 10
β’
β²π₯(absβ(((πΉ βΎ π΅)βπ) β πΆ)) < π€ |
78 | | simp3 1138 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ π€ β β+)
β§ π§ β
β+ β§ βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β§ π β π΅) β§ (π β (π· + π) β§ (absβ(π β (π· + π))) < π§)) β§ π₯ β π΄ β§ π = (π₯ + π)) β π = (π₯ + π)) |
79 | 78 | fveq2d 6892 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π€ β β+)
β§ π§ β
β+ β§ βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β§ π β π΅) β§ (π β (π· + π) β§ (absβ(π β (π· + π))) < π§)) β§ π₯ β π΄ β§ π = (π₯ + π)) β ((πΉ βΎ π΅)βπ) = ((πΉ βΎ π΅)β(π₯ + π))) |
80 | 17 | 3ad2ant1 1133 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ π€ β β+)
β§ π§ β
β+ β§ βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β§ π β π΅) β§ (π β (π· + π) β§ (absβ(π β (π· + π))) < π§)) β§ π₯ β π΄ β§ π = (π₯ + π)) β π β π΅) |
81 | 78, 80 | eqeltrrd 2834 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ π€ β β+)
β§ π§ β
β+ β§ βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β§ π β π΅) β§ (π β (π· + π) β§ (absβ(π β (π· + π))) < π§)) β§ π₯ β π΄ β§ π = (π₯ + π)) β (π₯ + π) β π΅) |
82 | 81 | fvresd 6908 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π€ β β+)
β§ π§ β
β+ β§ βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β§ π β π΅) β§ (π β (π· + π) β§ (absβ(π β (π· + π))) < π§)) β§ π₯ β π΄ β§ π = (π₯ + π)) β ((πΉ βΎ π΅)β(π₯ + π)) = (πΉβ(π₯ + π))) |
83 | 16 | 3ad2ant1 1133 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ π€ β β+)
β§ π§ β
β+ β§ βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β§ π β π΅) β§ (π β (π· + π) β§ (absβ(π β (π· + π))) < π§)) β§ π₯ β π΄ β§ π = (π₯ + π)) β π) |
84 | | simp2 1137 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ π€ β β+)
β§ π§ β
β+ β§ βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β§ π β π΅) β§ (π β (π· + π) β§ (absβ(π β (π· + π))) < π§)) β§ π₯ β π΄ β§ π = (π₯ + π)) β π₯ β π΄) |
85 | | eleq1w 2816 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ = π₯ β (π¦ β π΄ β π₯ β π΄)) |
86 | 85 | anbi2d 629 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ = π₯ β ((π β§ π¦ β π΄) β (π β§ π₯ β π΄))) |
87 | | fvoveq1 7428 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ = π₯ β (πΉβ(π¦ + π)) = (πΉβ(π₯ + π))) |
88 | | fveq2 6888 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ = π₯ β (πΉβπ¦) = (πΉβπ₯)) |
89 | 87, 88 | eqeq12d 2748 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ = π₯ β ((πΉβ(π¦ + π)) = (πΉβπ¦) β (πΉβ(π₯ + π)) = (πΉβπ₯))) |
90 | 86, 89 | imbi12d 344 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ = π₯ β (((π β§ π¦ β π΄) β (πΉβ(π¦ + π)) = (πΉβπ¦)) β ((π β§ π₯ β π΄) β (πΉβ(π₯ + π)) = (πΉβπ₯)))) |
91 | | limcperiod.fper |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π¦ β π΄) β (πΉβ(π¦ + π)) = (πΉβπ¦)) |
92 | 90, 91 | chvarvv 2002 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β π΄) β (πΉβ(π₯ + π)) = (πΉβπ₯)) |
93 | 83, 84, 92 | syl2anc 584 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ π€ β β+)
β§ π§ β
β+ β§ βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β§ π β π΅) β§ (π β (π· + π) β§ (absβ(π β (π· + π))) < π§)) β§ π₯ β π΄ β§ π = (π₯ + π)) β (πΉβ(π₯ + π)) = (πΉβπ₯)) |
94 | 84 | fvresd 6908 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ π€ β β+)
β§ π§ β
β+ β§ βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β§ π β π΅) β§ (π β (π· + π) β§ (absβ(π β (π· + π))) < π§)) β§ π₯ β π΄ β§ π = (π₯ + π)) β ((πΉ βΎ π΄)βπ₯) = (πΉβπ₯)) |
95 | 93, 94 | eqtr4d 2775 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π€ β β+)
β§ π§ β
β+ β§ βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β§ π β π΅) β§ (π β (π· + π) β§ (absβ(π β (π· + π))) < π§)) β§ π₯ β π΄ β§ π = (π₯ + π)) β (πΉβ(π₯ + π)) = ((πΉ βΎ π΄)βπ₯)) |
96 | 79, 82, 95 | 3eqtrd 2776 |
. . . . . . . . . . . . 13
β’
((((((π β§ π€ β β+)
β§ π§ β
β+ β§ βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β§ π β π΅) β§ (π β (π· + π) β§ (absβ(π β (π· + π))) < π§)) β§ π₯ β π΄ β§ π = (π₯ + π)) β ((πΉ βΎ π΅)βπ) = ((πΉ βΎ π΄)βπ₯)) |
97 | 96 | fvoveq1d 7427 |
. . . . . . . . . . . 12
β’
((((((π β§ π€ β β+)
β§ π§ β
β+ β§ βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β§ π β π΅) β§ (π β (π· + π) β§ (absβ(π β (π· + π))) < π§)) β§ π₯ β π΄ β§ π = (π₯ + π)) β (absβ(((πΉ βΎ π΅)βπ) β πΆ)) = (absβ(((πΉ βΎ π΄)βπ₯) β πΆ))) |
98 | | simpll3 1214 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π€ β β+)
β§ π§ β
β+ β§ βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β§ π β π΅) β§ (π β (π· + π) β§ (absβ(π β (π· + π))) < π§)) β βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) |
99 | 98 | 3ad2ant1 1133 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π€ β β+)
β§ π§ β
β+ β§ βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β§ π β π΅) β§ (π β (π· + π) β§ (absβ(π β (π· + π))) < π§)) β§ π₯ β π΄ β§ π = (π₯ + π)) β βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) |
100 | 99, 84 | jca 512 |
. . . . . . . . . . . . 13
β’
((((((π β§ π€ β β+)
β§ π§ β
β+ β§ βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β§ π β π΅) β§ (π β (π· + π) β§ (absβ(π β (π· + π))) < π§)) β§ π₯ β π΄ β§ π = (π₯ + π)) β (βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€) β§ π₯ β π΄)) |
101 | | simp1rl 1238 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§ π€ β β+)
β§ π§ β
β+ β§ βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β§ π β π΅) β§ (π β (π· + π) β§ (absβ(π β (π· + π))) < π§)) β§ π₯ β π΄ β§ π = (π₯ + π)) β π β (π· + π)) |
102 | 101 | neneqd 2945 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ π€ β β+)
β§ π§ β
β+ β§ βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β§ π β π΅) β§ (π β (π· + π) β§ (absβ(π β (π· + π))) < π§)) β§ π₯ β π΄ β§ π = (π₯ + π)) β Β¬ π = (π· + π)) |
103 | | oveq1 7412 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π· β (π₯ + π) = (π· + π)) |
104 | 78, 103 | sylan9eq 2792 |
. . . . . . . . . . . . . . . 16
β’
(((((((π β§ π€ β β+)
β§ π§ β
β+ β§ βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β§ π β π΅) β§ (π β (π· + π) β§ (absβ(π β (π· + π))) < π§)) β§ π₯ β π΄ β§ π = (π₯ + π)) β§ π₯ = π·) β π = (π· + π)) |
105 | 102, 104 | mtand 814 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ π€ β β+)
β§ π§ β
β+ β§ βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β§ π β π΅) β§ (π β (π· + π) β§ (absβ(π β (π· + π))) < π§)) β§ π₯ β π΄ β§ π = (π₯ + π)) β Β¬ π₯ = π·) |
106 | 105 | neqned 2947 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π€ β β+)
β§ π§ β
β+ β§ βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β§ π β π΅) β§ (π β (π· + π) β§ (absβ(π β (π· + π))) < π§)) β§ π₯ β π΄ β§ π = (π₯ + π)) β π₯ β π·) |
107 | 78 | oveq1d 7420 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§ π€ β β+)
β§ π§ β
β+ β§ βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β§ π β π΅) β§ (π β (π· + π) β§ (absβ(π β (π· + π))) < π§)) β§ π₯ β π΄ β§ π = (π₯ + π)) β (π β (π· + π)) = ((π₯ + π) β (π· + π))) |
108 | 7 | sselda 3981 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β π΄) β π₯ β β) |
109 | 83, 84, 108 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π β§ π€ β β+)
β§ π§ β
β+ β§ βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β§ π β π΅) β§ (π β (π· + π) β§ (absβ(π β (π· + π))) < π§)) β§ π₯ β π΄ β§ π = (π₯ + π)) β π₯ β β) |
110 | 83, 10 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π β§ π€ β β+)
β§ π§ β
β+ β§ βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β§ π β π΅) β§ (π β (π· + π) β§ (absβ(π β (π· + π))) < π§)) β§ π₯ β π΄ β§ π = (π₯ + π)) β π· β β) |
111 | 83, 38 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π β§ π€ β β+)
β§ π§ β
β+ β§ βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β§ π β π΅) β§ (π β (π· + π) β§ (absβ(π β (π· + π))) < π§)) β§ π₯ β π΄ β§ π = (π₯ + π)) β π β β) |
112 | 109, 110,
111 | pnpcan2d 11605 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§ π€ β β+)
β§ π§ β
β+ β§ βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β§ π β π΅) β§ (π β (π· + π) β§ (absβ(π β (π· + π))) < π§)) β§ π₯ β π΄ β§ π = (π₯ + π)) β ((π₯ + π) β (π· + π)) = (π₯ β π·)) |
113 | 107, 112 | eqtr2d 2773 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ π€ β β+)
β§ π§ β
β+ β§ βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β§ π β π΅) β§ (π β (π· + π) β§ (absβ(π β (π· + π))) < π§)) β§ π₯ β π΄ β§ π = (π₯ + π)) β (π₯ β π·) = (π β (π· + π))) |
114 | 113 | fveq2d 6892 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ π€ β β+)
β§ π§ β
β+ β§ βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β§ π β π΅) β§ (π β (π· + π) β§ (absβ(π β (π· + π))) < π§)) β§ π₯ β π΄ β§ π = (π₯ + π)) β (absβ(π₯ β π·)) = (absβ(π β (π· + π)))) |
115 | | simp1rr 1239 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ π€ β β+)
β§ π§ β
β+ β§ βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β§ π β π΅) β§ (π β (π· + π) β§ (absβ(π β (π· + π))) < π§)) β§ π₯ β π΄ β§ π = (π₯ + π)) β (absβ(π β (π· + π))) < π§) |
116 | 114, 115 | eqbrtrd 5169 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π€ β β+)
β§ π§ β
β+ β§ βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β§ π β π΅) β§ (π β (π· + π) β§ (absβ(π β (π· + π))) < π§)) β§ π₯ β π΄ β§ π = (π₯ + π)) β (absβ(π₯ β π·)) < π§) |
117 | 106, 116 | jca 512 |
. . . . . . . . . . . . 13
β’
((((((π β§ π€ β β+)
β§ π§ β
β+ β§ βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β§ π β π΅) β§ (π β (π· + π) β§ (absβ(π β (π· + π))) < π§)) β§ π₯ β π΄ β§ π = (π₯ + π)) β (π₯ β π· β§ (absβ(π₯ β π·)) < π§)) |
118 | | neeq1 3003 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = π₯ β (π¦ β π· β π₯ β π·)) |
119 | | fvoveq1 7428 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ = π₯ β (absβ(π¦ β π·)) = (absβ(π₯ β π·))) |
120 | 119 | breq1d 5157 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = π₯ β ((absβ(π¦ β π·)) < π§ β (absβ(π₯ β π·)) < π§)) |
121 | 118, 120 | anbi12d 631 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π₯ β ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (π₯ β π· β§ (absβ(π₯ β π·)) < π§))) |
122 | 121 | imbrov2fvoveq 7430 |
. . . . . . . . . . . . . 14
β’ (π¦ = π₯ β (((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€) β ((π₯ β π· β§ (absβ(π₯ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ₯) β πΆ)) < π€))) |
123 | 122 | rspccva 3611 |
. . . . . . . . . . . . 13
β’
((βπ¦ β
π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€) β§ π₯ β π΄) β ((π₯ β π· β§ (absβ(π₯ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ₯) β πΆ)) < π€)) |
124 | 100, 117,
123 | sylc 65 |
. . . . . . . . . . . 12
β’
((((((π β§ π€ β β+)
β§ π§ β
β+ β§ βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β§ π β π΅) β§ (π β (π· + π) β§ (absβ(π β (π· + π))) < π§)) β§ π₯ β π΄ β§ π = (π₯ + π)) β (absβ(((πΉ βΎ π΄)βπ₯) β πΆ)) < π€) |
125 | 97, 124 | eqbrtrd 5169 |
. . . . . . . . . . 11
β’
((((((π β§ π€ β β+)
β§ π§ β
β+ β§ βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β§ π β π΅) β§ (π β (π· + π) β§ (absβ(π β (π· + π))) < π§)) β§ π₯ β π΄ β§ π = (π₯ + π)) β (absβ(((πΉ βΎ π΅)βπ) β πΆ)) < π€) |
126 | 125 | 3exp 1119 |
. . . . . . . . . 10
β’
(((((π β§ π€ β β+)
β§ π§ β
β+ β§ βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β§ π β π΅) β§ (π β (π· + π) β§ (absβ(π β (π· + π))) < π§)) β (π₯ β π΄ β (π = (π₯ + π) β (absβ(((πΉ βΎ π΅)βπ) β πΆ)) < π€))) |
127 | 65, 77, 126 | rexlimd 3263 |
. . . . . . . . 9
β’
(((((π β§ π€ β β+)
β§ π§ β
β+ β§ βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β§ π β π΅) β§ (π β (π· + π) β§ (absβ(π β (π· + π))) < π§)) β (βπ₯ β π΄ π = (π₯ + π) β (absβ(((πΉ βΎ π΅)βπ) β πΆ)) < π€)) |
128 | 58, 127 | mpd 15 |
. . . . . . . 8
β’
(((((π β§ π€ β β+)
β§ π§ β
β+ β§ βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β§ π β π΅) β§ (π β (π· + π) β§ (absβ(π β (π· + π))) < π§)) β (absβ(((πΉ βΎ π΅)βπ) β πΆ)) < π€) |
129 | 128 | ex 413 |
. . . . . . 7
β’ ((((π β§ π€ β β+) β§ π§ β β+
β§ βπ¦ β
π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β§ π β π΅) β ((π β (π· + π) β§ (absβ(π β (π· + π))) < π§) β (absβ(((πΉ βΎ π΅)βπ) β πΆ)) < π€)) |
130 | 129 | ralrimiva 3146 |
. . . . . 6
β’ (((π β§ π€ β β+) β§ π§ β β+
β§ βπ¦ β
π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€)) β βπ β π΅ ((π β (π· + π) β§ (absβ(π β (π· + π))) < π§) β (absβ(((πΉ βΎ π΅)βπ) β πΆ)) < π€)) |
131 | 130 | 3exp 1119 |
. . . . 5
β’ ((π β§ π€ β β+) β (π§ β β+
β (βπ¦ β
π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€) β βπ β π΅ ((π β (π· + π) β§ (absβ(π β (π· + π))) < π§) β (absβ(((πΉ βΎ π΅)βπ) β πΆ)) < π€)))) |
132 | 131 | reximdvai 3165 |
. . . 4
β’ ((π β§ π€ β β+) β
(βπ§ β
β+ βπ¦ β π΄ ((π¦ β π· β§ (absβ(π¦ β π·)) < π§) β (absβ(((πΉ βΎ π΄)βπ¦) β πΆ)) < π€) β βπ§ β β+ βπ β π΅ ((π β (π· + π) β§ (absβ(π β (π· + π))) < π§) β (absβ(((πΉ βΎ π΅)βπ) β πΆ)) < π€))) |
133 | 14, 132 | mpd 15 |
. . 3
β’ ((π β§ π€ β β+) β
βπ§ β
β+ βπ β π΅ ((π β (π· + π) β§ (absβ(π β (π· + π))) < π§) β (absβ(((πΉ βΎ π΅)βπ) β πΆ)) < π€)) |
134 | 133 | ralrimiva 3146 |
. 2
β’ (π β βπ€ β β+ βπ§ β β+
βπ β π΅ ((π β (π· + π) β§ (absβ(π β (π· + π))) < π§) β (absβ(((πΉ βΎ π΅)βπ) β πΆ)) < π€)) |
135 | | limcperiod.bss |
. . . 4
β’ (π β π΅ β dom πΉ) |
136 | 4, 135 | fssresd 6755 |
. . 3
β’ (π β (πΉ βΎ π΅):π΅βΆβ) |
137 | 10, 38 | addcld 11229 |
. . 3
β’ (π β (π· + π) β β) |
138 | 136, 50, 137 | ellimc3 25387 |
. 2
β’ (π β (πΆ β ((πΉ βΎ π΅) limβ (π· + π)) β (πΆ β β β§ βπ€ β β+
βπ§ β
β+ βπ β π΅ ((π β (π· + π) β§ (absβ(π β (π· + π))) < π§) β (absβ(((πΉ βΎ π΅)βπ) β πΆ)) < π€)))) |
139 | 3, 134, 138 | mpbir2and 711 |
1
β’ (π β πΆ β ((πΉ βΎ π΅) limβ (π· + π))) |