Step | Hyp | Ref
| Expression |
1 | | cncfperiod.f |
. . 3
β’ (π β πΉ:dom πΉβΆβ) |
2 | | cncfperiod.cssdmf |
. . 3
β’ (π β π΅ β dom πΉ) |
3 | 1, 2 | fssresd 6713 |
. 2
β’ (π β (πΉ βΎ π΅):π΅βΆβ) |
4 | | fvoveq1 7384 |
. . . . . . . . . . 11
β’ (π = (π₯ β π) β (absβ(π β π)) = (absβ((π₯ β π) β π))) |
5 | 4 | breq1d 5119 |
. . . . . . . . . 10
β’ (π = (π₯ β π) β ((absβ(π β π)) < π§ β (absβ((π₯ β π) β π)) < π§)) |
6 | 5 | imbrov2fvoveq 7386 |
. . . . . . . . 9
β’ (π = (π₯ β π) β (((absβ(π β π)) < π§ β (absβ(((πΉ βΎ π΄)βπ) β ((πΉ βΎ π΄)βπ))) < π€) β ((absβ((π₯ β π) β π)) < π§ β (absβ(((πΉ βΎ π΄)β(π₯ β π)) β ((πΉ βΎ π΄)βπ))) < π€))) |
7 | 6 | rexralbidv 3211 |
. . . . . . . 8
β’ (π = (π₯ β π) β (βπ§ β β+ βπ β π΄ ((absβ(π β π)) < π§ β (absβ(((πΉ βΎ π΄)βπ) β ((πΉ βΎ π΄)βπ))) < π€) β βπ§ β β+ βπ β π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ(((πΉ βΎ π΄)β(π₯ β π)) β ((πΉ βΎ π΄)βπ))) < π€))) |
8 | 7 | ralbidv 3171 |
. . . . . . 7
β’ (π = (π₯ β π) β (βπ€ β β+ βπ§ β β+
βπ β π΄ ((absβ(π β π)) < π§ β (absβ(((πΉ βΎ π΄)βπ) β ((πΉ βΎ π΄)βπ))) < π€) β βπ€ β β+ βπ§ β β+
βπ β π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ(((πΉ βΎ π΄)β(π₯ β π)) β ((πΉ βΎ π΄)βπ))) < π€))) |
9 | | cncfperiod.fcn |
. . . . . . . . . 10
β’ (π β (πΉ βΎ π΄) β (π΄βcnββ)) |
10 | 9 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΅) β (πΉ βΎ π΄) β (π΄βcnββ)) |
11 | | cncfperiod.a |
. . . . . . . . . . 11
β’ (π β π΄ β β) |
12 | 11 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΅) β π΄ β β) |
13 | | ssidd 3971 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΅) β β β
β) |
14 | | elcncf 24275 |
. . . . . . . . . 10
β’ ((π΄ β β β§ β
β β) β ((πΉ
βΎ π΄) β (π΄βcnββ) β ((πΉ βΎ π΄):π΄βΆβ β§ βπ β π΄ βπ€ β β+ βπ§ β β+
βπ β π΄ ((absβ(π β π)) < π§ β (absβ(((πΉ βΎ π΄)βπ) β ((πΉ βΎ π΄)βπ))) < π€)))) |
15 | 12, 13, 14 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΅) β ((πΉ βΎ π΄) β (π΄βcnββ) β ((πΉ βΎ π΄):π΄βΆβ β§ βπ β π΄ βπ€ β β+ βπ§ β β+
βπ β π΄ ((absβ(π β π)) < π§ β (absβ(((πΉ βΎ π΄)βπ) β ((πΉ βΎ π΄)βπ))) < π€)))) |
16 | 10, 15 | mpbid 231 |
. . . . . . . 8
β’ ((π β§ π₯ β π΅) β ((πΉ βΎ π΄):π΄βΆβ β§ βπ β π΄ βπ€ β β+ βπ§ β β+
βπ β π΄ ((absβ(π β π)) < π§ β (absβ(((πΉ βΎ π΄)βπ) β ((πΉ βΎ π΄)βπ))) < π€))) |
17 | 16 | simprd 497 |
. . . . . . 7
β’ ((π β§ π₯ β π΅) β βπ β π΄ βπ€ β β+ βπ§ β β+
βπ β π΄ ((absβ(π β π)) < π§ β (absβ(((πΉ βΎ π΄)βπ) β ((πΉ βΎ π΄)βπ))) < π€)) |
18 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΅) β π₯ β π΅) |
19 | | cncfperiod.b |
. . . . . . . . . . 11
β’ π΅ = {π₯ β β β£ βπ¦ β π΄ π₯ = (π¦ + π)} |
20 | 18, 19 | eleqtrdi 2844 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΅) β π₯ β {π₯ β β β£ βπ¦ β π΄ π₯ = (π¦ + π)}) |
21 | | rabid 3426 |
. . . . . . . . . 10
β’ (π₯ β {π₯ β β β£ βπ¦ β π΄ π₯ = (π¦ + π)} β (π₯ β β β§ βπ¦ β π΄ π₯ = (π¦ + π))) |
22 | 20, 21 | sylib 217 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΅) β (π₯ β β β§ βπ¦ β π΄ π₯ = (π¦ + π))) |
23 | 22 | simprd 497 |
. . . . . . . 8
β’ ((π β§ π₯ β π΅) β βπ¦ β π΄ π₯ = (π¦ + π)) |
24 | | oveq1 7368 |
. . . . . . . . . . . 12
β’ (π₯ = (π¦ + π) β (π₯ β π) = ((π¦ + π) β π)) |
25 | 24 | 3ad2ant3 1136 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β π΅) β§ π¦ β π΄ β§ π₯ = (π¦ + π)) β (π₯ β π) = ((π¦ + π) β π)) |
26 | 11 | sselda 3948 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β π΄) β π¦ β β) |
27 | | cncfperiod.t |
. . . . . . . . . . . . . . . 16
β’ (π β π β β) |
28 | 27 | recnd 11191 |
. . . . . . . . . . . . . . 15
β’ (π β π β β) |
29 | 28 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β π΄) β π β β) |
30 | 26, 29 | pncand 11521 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β π΄) β ((π¦ + π) β π) = π¦) |
31 | 30 | adantlr 714 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β π΅) β§ π¦ β π΄) β ((π¦ + π) β π) = π¦) |
32 | 31 | 3adant3 1133 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β π΅) β§ π¦ β π΄ β§ π₯ = (π¦ + π)) β ((π¦ + π) β π) = π¦) |
33 | 25, 32 | eqtrd 2773 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π΅) β§ π¦ β π΄ β§ π₯ = (π¦ + π)) β (π₯ β π) = π¦) |
34 | | simp2 1138 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π΅) β§ π¦ β π΄ β§ π₯ = (π¦ + π)) β π¦ β π΄) |
35 | 33, 34 | eqeltrd 2834 |
. . . . . . . . 9
β’ (((π β§ π₯ β π΅) β§ π¦ β π΄ β§ π₯ = (π¦ + π)) β (π₯ β π) β π΄) |
36 | 35 | rexlimdv3a 3153 |
. . . . . . . 8
β’ ((π β§ π₯ β π΅) β (βπ¦ β π΄ π₯ = (π¦ + π) β (π₯ β π) β π΄)) |
37 | 23, 36 | mpd 15 |
. . . . . . 7
β’ ((π β§ π₯ β π΅) β (π₯ β π) β π΄) |
38 | 8, 17, 37 | rspcdva 3584 |
. . . . . 6
β’ ((π β§ π₯ β π΅) β βπ€ β β+ βπ§ β β+
βπ β π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ(((πΉ βΎ π΄)β(π₯ β π)) β ((πΉ βΎ π΄)βπ))) < π€)) |
39 | 38 | adantrr 716 |
. . . . 5
β’ ((π β§ (π₯ β π΅ β§ π€ β β+)) β
βπ€ β
β+ βπ§ β β+ βπ β π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ(((πΉ βΎ π΄)β(π₯ β π)) β ((πΉ βΎ π΄)βπ))) < π€)) |
40 | | simprr 772 |
. . . . 5
β’ ((π β§ (π₯ β π΅ β§ π€ β β+)) β π€ β
β+) |
41 | | rspa 3230 |
. . . . 5
β’
((βπ€ β
β+ βπ§ β β+ βπ β π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ(((πΉ βΎ π΄)β(π₯ β π)) β ((πΉ βΎ π΄)βπ))) < π€) β§ π€ β β+) β
βπ§ β
β+ βπ β π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ(((πΉ βΎ π΄)β(π₯ β π)) β ((πΉ βΎ π΄)βπ))) < π€)) |
42 | 39, 40, 41 | syl2anc 585 |
. . . 4
β’ ((π β§ (π₯ β π΅ β§ π€ β β+)) β
βπ§ β
β+ βπ β π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ(((πΉ βΎ π΄)β(π₯ β π)) β ((πΉ βΎ π΄)βπ))) < π€)) |
43 | | simpl1l 1225 |
. . . . . . . . . . 11
β’ ((((π β§ (π₯ β π΅ β§ π€ β β+)) β§ π§ β β+
β§ βπ β
π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ(((πΉ βΎ π΄)β(π₯ β π)) β ((πΉ βΎ π΄)βπ))) < π€)) β§ π£ β π΅) β π) |
44 | 43 | adantr 482 |
. . . . . . . . . 10
β’
(((((π β§ (π₯ β π΅ β§ π€ β β+)) β§ π§ β β+
β§ βπ β
π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ(((πΉ βΎ π΄)β(π₯ β π)) β ((πΉ βΎ π΄)βπ))) < π€)) β§ π£ β π΅) β§ (absβ(π₯ β π£)) < π§) β π) |
45 | | simp1rl 1239 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β π΅ β§ π€ β β+)) β§ π§ β β+
β§ βπ β
π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ(((πΉ βΎ π΄)β(π₯ β π)) β ((πΉ βΎ π΄)βπ))) < π€)) β π₯ β π΅) |
46 | 45 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π β§ (π₯ β π΅ β§ π€ β β+)) β§ π§ β β+
β§ βπ β
π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ(((πΉ βΎ π΄)β(π₯ β π)) β ((πΉ βΎ π΄)βπ))) < π€)) β§ π£ β π΅) β π₯ β π΅) |
47 | 46 | adantr 482 |
. . . . . . . . . 10
β’
(((((π β§ (π₯ β π΅ β§ π€ β β+)) β§ π§ β β+
β§ βπ β
π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ(((πΉ βΎ π΄)β(π₯ β π)) β ((πΉ βΎ π΄)βπ))) < π€)) β§ π£ β π΅) β§ (absβ(π₯ β π£)) < π§) β π₯ β π΅) |
48 | | simplr 768 |
. . . . . . . . . 10
β’
(((((π β§ (π₯ β π΅ β§ π€ β β+)) β§ π§ β β+
β§ βπ β
π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ(((πΉ βΎ π΄)β(π₯ β π)) β ((πΉ βΎ π΄)βπ))) < π€)) β§ π£ β π΅) β§ (absβ(π₯ β π£)) < π§) β π£ β π΅) |
49 | | fvres 6865 |
. . . . . . . . . . . . . . 15
β’ (π₯ β π΅ β ((πΉ βΎ π΅)βπ₯) = (πΉβπ₯)) |
50 | 49 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β π΅) β ((πΉ βΎ π΅)βπ₯) = (πΉβπ₯)) |
51 | 19 | ssrab3 4044 |
. . . . . . . . . . . . . . . . . . 19
β’ π΅ β
β |
52 | 51 | sseli 3944 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β π΅ β π₯ β β) |
53 | 52 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β π΅) β π₯ β β) |
54 | 28 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β π΅) β π β β) |
55 | 53, 54 | npcand 11524 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β π΅) β ((π₯ β π) + π) = π₯) |
56 | 55 | eqcomd 2739 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β π΅) β π₯ = ((π₯ β π) + π)) |
57 | 56 | fveq2d 6850 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β π΅) β (πΉβπ₯) = (πΉβ((π₯ β π) + π))) |
58 | | simpl 484 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β π΅) β π) |
59 | 58, 37 | jca 513 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β π΅) β (π β§ (π₯ β π) β π΄)) |
60 | | eleq1 2822 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ = (π₯ β π) β (π¦ β π΄ β (π₯ β π) β π΄)) |
61 | 60 | anbi2d 630 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ = (π₯ β π) β ((π β§ π¦ β π΄) β (π β§ (π₯ β π) β π΄))) |
62 | | fvoveq1 7384 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ = (π₯ β π) β (πΉβ(π¦ + π)) = (πΉβ((π₯ β π) + π))) |
63 | | fveq2 6846 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ = (π₯ β π) β (πΉβπ¦) = (πΉβ(π₯ β π))) |
64 | 62, 63 | eqeq12d 2749 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ = (π₯ β π) β ((πΉβ(π¦ + π)) = (πΉβπ¦) β (πΉβ((π₯ β π) + π)) = (πΉβ(π₯ β π)))) |
65 | 61, 64 | imbi12d 345 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ = (π₯ β π) β (((π β§ π¦ β π΄) β (πΉβ(π¦ + π)) = (πΉβπ¦)) β ((π β§ (π₯ β π) β π΄) β (πΉβ((π₯ β π) + π)) = (πΉβ(π₯ β π))))) |
66 | | eleq1 2822 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ = π¦ β (π₯ β π΄ β π¦ β π΄)) |
67 | 66 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ = π¦ β ((π β§ π₯ β π΄) β (π β§ π¦ β π΄))) |
68 | | fvoveq1 7384 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ = π¦ β (πΉβ(π₯ + π)) = (πΉβ(π¦ + π))) |
69 | | fveq2 6846 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ = π¦ β (πΉβπ₯) = (πΉβπ¦)) |
70 | 68, 69 | eqeq12d 2749 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ = π¦ β ((πΉβ(π₯ + π)) = (πΉβπ₯) β (πΉβ(π¦ + π)) = (πΉβπ¦))) |
71 | 67, 70 | imbi12d 345 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π¦ β (((π β§ π₯ β π΄) β (πΉβ(π₯ + π)) = (πΉβπ₯)) β ((π β§ π¦ β π΄) β (πΉβ(π¦ + π)) = (πΉβπ¦)))) |
72 | | cncfperiod.fper |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β π΄) β (πΉβ(π₯ + π)) = (πΉβπ₯)) |
73 | 71, 72 | chvarvv 2003 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π¦ β π΄) β (πΉβ(π¦ + π)) = (πΉβπ¦)) |
74 | 65, 73 | vtoclg 3527 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β π) β π΄ β ((π β§ (π₯ β π) β π΄) β (πΉβ((π₯ β π) + π)) = (πΉβ(π₯ β π)))) |
75 | 37, 59, 74 | sylc 65 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β π΅) β (πΉβ((π₯ β π) + π)) = (πΉβ(π₯ β π))) |
76 | 37 | fvresd 6866 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β π΅) β ((πΉ βΎ π΄)β(π₯ β π)) = (πΉβ(π₯ β π))) |
77 | 75, 76 | eqtr4d 2776 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β π΅) β (πΉβ((π₯ β π) + π)) = ((πΉ βΎ π΄)β(π₯ β π))) |
78 | 50, 57, 77 | 3eqtrd 2777 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β π΅) β ((πΉ βΎ π΅)βπ₯) = ((πΉ βΎ π΄)β(π₯ β π))) |
79 | 78 | 3adant3 1133 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΅ β§ π£ β π΅) β ((πΉ βΎ π΅)βπ₯) = ((πΉ βΎ π΄)β(π₯ β π))) |
80 | | eleq1 2822 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π£ β (π₯ β π΅ β π£ β π΅)) |
81 | 80 | anbi2d 630 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π£ β ((π β§ π₯ β π΅) β (π β§ π£ β π΅))) |
82 | | fveq2 6846 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π£ β ((πΉ βΎ π΅)βπ₯) = ((πΉ βΎ π΅)βπ£)) |
83 | | fvoveq1 7384 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π£ β ((πΉ βΎ π΄)β(π₯ β π)) = ((πΉ βΎ π΄)β(π£ β π))) |
84 | 82, 83 | eqeq12d 2749 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π£ β (((πΉ βΎ π΅)βπ₯) = ((πΉ βΎ π΄)β(π₯ β π)) β ((πΉ βΎ π΅)βπ£) = ((πΉ βΎ π΄)β(π£ β π)))) |
85 | 81, 84 | imbi12d 345 |
. . . . . . . . . . . . . 14
β’ (π₯ = π£ β (((π β§ π₯ β π΅) β ((πΉ βΎ π΅)βπ₯) = ((πΉ βΎ π΄)β(π₯ β π))) β ((π β§ π£ β π΅) β ((πΉ βΎ π΅)βπ£) = ((πΉ βΎ π΄)β(π£ β π))))) |
86 | 85, 78 | chvarvv 2003 |
. . . . . . . . . . . . 13
β’ ((π β§ π£ β π΅) β ((πΉ βΎ π΅)βπ£) = ((πΉ βΎ π΄)β(π£ β π))) |
87 | 86 | 3adant2 1132 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΅ β§ π£ β π΅) β ((πΉ βΎ π΅)βπ£) = ((πΉ βΎ π΄)β(π£ β π))) |
88 | 79, 87 | oveq12d 7379 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΅ β§ π£ β π΅) β (((πΉ βΎ π΅)βπ₯) β ((πΉ βΎ π΅)βπ£)) = (((πΉ βΎ π΄)β(π₯ β π)) β ((πΉ βΎ π΄)β(π£ β π)))) |
89 | 88 | fveq2d 6850 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΅ β§ π£ β π΅) β (absβ(((πΉ βΎ π΅)βπ₯) β ((πΉ βΎ π΅)βπ£))) = (absβ(((πΉ βΎ π΄)β(π₯ β π)) β ((πΉ βΎ π΄)β(π£ β π))))) |
90 | 44, 47, 48, 89 | syl3anc 1372 |
. . . . . . . . 9
β’
(((((π β§ (π₯ β π΅ β§ π€ β β+)) β§ π§ β β+
β§ βπ β
π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ(((πΉ βΎ π΄)β(π₯ β π)) β ((πΉ βΎ π΄)βπ))) < π€)) β§ π£ β π΅) β§ (absβ(π₯ β π£)) < π§) β (absβ(((πΉ βΎ π΅)βπ₯) β ((πΉ βΎ π΅)βπ£))) = (absβ(((πΉ βΎ π΄)β(π₯ β π)) β ((πΉ βΎ π΄)β(π£ β π))))) |
91 | | simpr 486 |
. . . . . . . . . . 11
β’
(((((π β§ (π₯ β π΅ β§ π€ β β+)) β§ π§ β β+
β§ βπ β
π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ(((πΉ βΎ π΄)β(π₯ β π)) β ((πΉ βΎ π΄)βπ))) < π€)) β§ π£ β π΅) β§ (absβ(π₯ β π£)) < π§) β (absβ(π₯ β π£)) < π§) |
92 | 22 | simpld 496 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β π΅) β π₯ β β) |
93 | 92 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β π΅) β§ π£ β π΅) β π₯ β β) |
94 | 51 | sseli 3944 |
. . . . . . . . . . . . . . . 16
β’ (π£ β π΅ β π£ β β) |
95 | 94 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β π΅) β§ π£ β π΅) β π£ β β) |
96 | 54 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β π΅) β§ π£ β π΅) β π β β) |
97 | 93, 95, 96 | nnncan2d 11555 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β π΅) β§ π£ β π΅) β ((π₯ β π) β (π£ β π)) = (π₯ β π£)) |
98 | 97 | fveq2d 6850 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β π΅) β§ π£ β π΅) β (absβ((π₯ β π) β (π£ β π))) = (absβ(π₯ β π£))) |
99 | 98 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β π΅) β§ π£ β π΅) β§ (absβ(π₯ β π£)) < π§) β (absβ((π₯ β π) β (π£ β π))) = (absβ(π₯ β π£))) |
100 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β π΅) β§ π£ β π΅) β§ (absβ(π₯ β π£)) < π§) β (absβ(π₯ β π£)) < π§) |
101 | 99, 100 | eqbrtrd 5131 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β π΅) β§ π£ β π΅) β§ (absβ(π₯ β π£)) < π§) β (absβ((π₯ β π) β (π£ β π))) < π§) |
102 | 44, 47, 48, 91, 101 | syl1111anc 839 |
. . . . . . . . . 10
β’
(((((π β§ (π₯ β π΅ β§ π€ β β+)) β§ π§ β β+
β§ βπ β
π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ(((πΉ βΎ π΄)β(π₯ β π)) β ((πΉ βΎ π΄)βπ))) < π€)) β§ π£ β π΅) β§ (absβ(π₯ β π£)) < π§) β (absβ((π₯ β π) β (π£ β π))) < π§) |
103 | | oveq2 7369 |
. . . . . . . . . . . . . 14
β’ (π = (π£ β π) β ((π₯ β π) β π) = ((π₯ β π) β (π£ β π))) |
104 | 103 | fveq2d 6850 |
. . . . . . . . . . . . 13
β’ (π = (π£ β π) β (absβ((π₯ β π) β π)) = (absβ((π₯ β π) β (π£ β π)))) |
105 | 104 | breq1d 5119 |
. . . . . . . . . . . 12
β’ (π = (π£ β π) β ((absβ((π₯ β π) β π)) < π§ β (absβ((π₯ β π) β (π£ β π))) < π§)) |
106 | | fveq2 6846 |
. . . . . . . . . . . . . . 15
β’ (π = (π£ β π) β ((πΉ βΎ π΄)βπ) = ((πΉ βΎ π΄)β(π£ β π))) |
107 | 106 | oveq2d 7377 |
. . . . . . . . . . . . . 14
β’ (π = (π£ β π) β (((πΉ βΎ π΄)β(π₯ β π)) β ((πΉ βΎ π΄)βπ)) = (((πΉ βΎ π΄)β(π₯ β π)) β ((πΉ βΎ π΄)β(π£ β π)))) |
108 | 107 | fveq2d 6850 |
. . . . . . . . . . . . 13
β’ (π = (π£ β π) β (absβ(((πΉ βΎ π΄)β(π₯ β π)) β ((πΉ βΎ π΄)βπ))) = (absβ(((πΉ βΎ π΄)β(π₯ β π)) β ((πΉ βΎ π΄)β(π£ β π))))) |
109 | 108 | breq1d 5119 |
. . . . . . . . . . . 12
β’ (π = (π£ β π) β ((absβ(((πΉ βΎ π΄)β(π₯ β π)) β ((πΉ βΎ π΄)βπ))) < π€ β (absβ(((πΉ βΎ π΄)β(π₯ β π)) β ((πΉ βΎ π΄)β(π£ β π)))) < π€)) |
110 | 105, 109 | imbi12d 345 |
. . . . . . . . . . 11
β’ (π = (π£ β π) β (((absβ((π₯ β π) β π)) < π§ β (absβ(((πΉ βΎ π΄)β(π₯ β π)) β ((πΉ βΎ π΄)βπ))) < π€) β ((absβ((π₯ β π) β (π£ β π))) < π§ β (absβ(((πΉ βΎ π΄)β(π₯ β π)) β ((πΉ βΎ π΄)β(π£ β π)))) < π€))) |
111 | | simpll3 1215 |
. . . . . . . . . . 11
β’
(((((π β§ (π₯ β π΅ β§ π€ β β+)) β§ π§ β β+
β§ βπ β
π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ(((πΉ βΎ π΄)β(π₯ β π)) β ((πΉ βΎ π΄)βπ))) < π€)) β§ π£ β π΅) β§ (absβ(π₯ β π£)) < π§) β βπ β π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ(((πΉ βΎ π΄)β(π₯ β π)) β ((πΉ βΎ π΄)βπ))) < π€)) |
112 | | oveq1 7368 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π£ β (π₯ β π) = (π£ β π)) |
113 | 112 | eleq1d 2819 |
. . . . . . . . . . . . . 14
β’ (π₯ = π£ β ((π₯ β π) β π΄ β (π£ β π) β π΄)) |
114 | 81, 113 | imbi12d 345 |
. . . . . . . . . . . . 13
β’ (π₯ = π£ β (((π β§ π₯ β π΅) β (π₯ β π) β π΄) β ((π β§ π£ β π΅) β (π£ β π) β π΄))) |
115 | 114, 37 | chvarvv 2003 |
. . . . . . . . . . . 12
β’ ((π β§ π£ β π΅) β (π£ β π) β π΄) |
116 | 44, 48, 115 | syl2anc 585 |
. . . . . . . . . . 11
β’
(((((π β§ (π₯ β π΅ β§ π€ β β+)) β§ π§ β β+
β§ βπ β
π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ(((πΉ βΎ π΄)β(π₯ β π)) β ((πΉ βΎ π΄)βπ))) < π€)) β§ π£ β π΅) β§ (absβ(π₯ β π£)) < π§) β (π£ β π) β π΄) |
117 | 110, 111,
116 | rspcdva 3584 |
. . . . . . . . . 10
β’
(((((π β§ (π₯ β π΅ β§ π€ β β+)) β§ π§ β β+
β§ βπ β
π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ(((πΉ βΎ π΄)β(π₯ β π)) β ((πΉ βΎ π΄)βπ))) < π€)) β§ π£ β π΅) β§ (absβ(π₯ β π£)) < π§) β ((absβ((π₯ β π) β (π£ β π))) < π§ β (absβ(((πΉ βΎ π΄)β(π₯ β π)) β ((πΉ βΎ π΄)β(π£ β π)))) < π€)) |
118 | 102, 117 | mpd 15 |
. . . . . . . . 9
β’
(((((π β§ (π₯ β π΅ β§ π€ β β+)) β§ π§ β β+
β§ βπ β
π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ(((πΉ βΎ π΄)β(π₯ β π)) β ((πΉ βΎ π΄)βπ))) < π€)) β§ π£ β π΅) β§ (absβ(π₯ β π£)) < π§) β (absβ(((πΉ βΎ π΄)β(π₯ β π)) β ((πΉ βΎ π΄)β(π£ β π)))) < π€) |
119 | 90, 118 | eqbrtrd 5131 |
. . . . . . . 8
β’
(((((π β§ (π₯ β π΅ β§ π€ β β+)) β§ π§ β β+
β§ βπ β
π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ(((πΉ βΎ π΄)β(π₯ β π)) β ((πΉ βΎ π΄)βπ))) < π€)) β§ π£ β π΅) β§ (absβ(π₯ β π£)) < π§) β (absβ(((πΉ βΎ π΅)βπ₯) β ((πΉ βΎ π΅)βπ£))) < π€) |
120 | 119 | ex 414 |
. . . . . . 7
β’ ((((π β§ (π₯ β π΅ β§ π€ β β+)) β§ π§ β β+
β§ βπ β
π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ(((πΉ βΎ π΄)β(π₯ β π)) β ((πΉ βΎ π΄)βπ))) < π€)) β§ π£ β π΅) β ((absβ(π₯ β π£)) < π§ β (absβ(((πΉ βΎ π΅)βπ₯) β ((πΉ βΎ π΅)βπ£))) < π€)) |
121 | 120 | ralrimiva 3140 |
. . . . . 6
β’ (((π β§ (π₯ β π΅ β§ π€ β β+)) β§ π§ β β+
β§ βπ β
π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ(((πΉ βΎ π΄)β(π₯ β π)) β ((πΉ βΎ π΄)βπ))) < π€)) β βπ£ β π΅ ((absβ(π₯ β π£)) < π§ β (absβ(((πΉ βΎ π΅)βπ₯) β ((πΉ βΎ π΅)βπ£))) < π€)) |
122 | 121 | 3exp 1120 |
. . . . 5
β’ ((π β§ (π₯ β π΅ β§ π€ β β+)) β (π§ β β+
β (βπ β
π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ(((πΉ βΎ π΄)β(π₯ β π)) β ((πΉ βΎ π΄)βπ))) < π€) β βπ£ β π΅ ((absβ(π₯ β π£)) < π§ β (absβ(((πΉ βΎ π΅)βπ₯) β ((πΉ βΎ π΅)βπ£))) < π€)))) |
123 | 122 | reximdvai 3159 |
. . . 4
β’ ((π β§ (π₯ β π΅ β§ π€ β β+)) β
(βπ§ β
β+ βπ β π΄ ((absβ((π₯ β π) β π)) < π§ β (absβ(((πΉ βΎ π΄)β(π₯ β π)) β ((πΉ βΎ π΄)βπ))) < π€) β βπ§ β β+ βπ£ β π΅ ((absβ(π₯ β π£)) < π§ β (absβ(((πΉ βΎ π΅)βπ₯) β ((πΉ βΎ π΅)βπ£))) < π€))) |
124 | 42, 123 | mpd 15 |
. . 3
β’ ((π β§ (π₯ β π΅ β§ π€ β β+)) β
βπ§ β
β+ βπ£ β π΅ ((absβ(π₯ β π£)) < π§ β (absβ(((πΉ βΎ π΅)βπ₯) β ((πΉ βΎ π΅)βπ£))) < π€)) |
125 | 124 | ralrimivva 3194 |
. 2
β’ (π β βπ₯ β π΅ βπ€ β β+ βπ§ β β+
βπ£ β π΅ ((absβ(π₯ β π£)) < π§ β (absβ(((πΉ βΎ π΅)βπ₯) β ((πΉ βΎ π΅)βπ£))) < π€)) |
126 | 51 | a1i 11 |
. . 3
β’ (π β π΅ β β) |
127 | | ssidd 3971 |
. . 3
β’ (π β β β
β) |
128 | | elcncf 24275 |
. . 3
β’ ((π΅ β β β§ β
β β) β ((πΉ
βΎ π΅) β (π΅βcnββ) β ((πΉ βΎ π΅):π΅βΆβ β§ βπ₯ β π΅ βπ€ β β+ βπ§ β β+
βπ£ β π΅ ((absβ(π₯ β π£)) < π§ β (absβ(((πΉ βΎ π΅)βπ₯) β ((πΉ βΎ π΅)βπ£))) < π€)))) |
129 | 126, 127,
128 | syl2anc 585 |
. 2
β’ (π β ((πΉ βΎ π΅) β (π΅βcnββ) β ((πΉ βΎ π΅):π΅βΆβ β§ βπ₯ β π΅ βπ€ β β+ βπ§ β β+
βπ£ β π΅ ((absβ(π₯ β π£)) < π§ β (absβ(((πΉ βΎ π΅)βπ₯) β ((πΉ βΎ π΅)βπ£))) < π€)))) |
130 | 3, 125, 129 | mpbir2and 712 |
1
β’ (π β (πΉ βΎ π΅) β (π΅βcnββ)) |