Step | Hyp | Ref
| Expression |
1 | | climuz.m |
. . 3
β’ (π β π β β€) |
2 | | climuz.z |
. . 3
β’ π =
(β€β₯βπ) |
3 | | climuz.f |
. . 3
β’ (π β πΉ:πβΆβ) |
4 | 1, 2, 3 | climuzlem 43332 |
. 2
β’ (π β (πΉ β π΄ β (π΄ β β β§ βπ¦ β β+
βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π¦))) |
5 | | breq2 5085 |
. . . . . . . 8
β’ (π¦ = π₯ β ((absβ((πΉβπ) β π΄)) < π¦ β (absβ((πΉβπ) β π΄)) < π₯)) |
6 | 5 | ralbidv 3171 |
. . . . . . 7
β’ (π¦ = π₯ β (βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π¦ β βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯)) |
7 | 6 | rexbidv 3172 |
. . . . . 6
β’ (π¦ = π₯ β (βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π¦ β βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯)) |
8 | | fveq2 6800 |
. . . . . . . . . 10
β’ (π = π β (β€β₯βπ) =
(β€β₯βπ)) |
9 | 8 | raleqdv 3360 |
. . . . . . . . 9
β’ (π = π β (βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯ β βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯)) |
10 | | nfcv 2905 |
. . . . . . . . . . . . 13
β’
β²πabs |
11 | | climuz.k |
. . . . . . . . . . . . . . 15
β’
β²ππΉ |
12 | | nfcv 2905 |
. . . . . . . . . . . . . . 15
β’
β²ππ |
13 | 11, 12 | nffv 6810 |
. . . . . . . . . . . . . 14
β’
β²π(πΉβπ) |
14 | | nfcv 2905 |
. . . . . . . . . . . . . 14
β’
β²π
β |
15 | | nfcv 2905 |
. . . . . . . . . . . . . 14
β’
β²ππ΄ |
16 | 13, 14, 15 | nfov 7333 |
. . . . . . . . . . . . 13
β’
β²π((πΉβπ) β π΄) |
17 | 10, 16 | nffv 6810 |
. . . . . . . . . . . 12
β’
β²π(absβ((πΉβπ) β π΄)) |
18 | | nfcv 2905 |
. . . . . . . . . . . 12
β’
β²π
< |
19 | | nfcv 2905 |
. . . . . . . . . . . 12
β’
β²ππ₯ |
20 | 17, 18, 19 | nfbr 5128 |
. . . . . . . . . . 11
β’
β²π(absβ((πΉβπ) β π΄)) < π₯ |
21 | | nfv 1915 |
. . . . . . . . . . 11
β’
β²π(absβ((πΉβπ) β π΄)) < π₯ |
22 | | fveq2 6800 |
. . . . . . . . . . . . 13
β’ (π = π β (πΉβπ) = (πΉβπ)) |
23 | 22 | fvoveq1d 7325 |
. . . . . . . . . . . 12
β’ (π = π β (absβ((πΉβπ) β π΄)) = (absβ((πΉβπ) β π΄))) |
24 | 23 | breq1d 5091 |
. . . . . . . . . . 11
β’ (π = π β ((absβ((πΉβπ) β π΄)) < π₯ β (absβ((πΉβπ) β π΄)) < π₯)) |
25 | 20, 21, 24 | cbvralw 3385 |
. . . . . . . . . 10
β’
(βπ β
(β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯ β βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯) |
26 | 25 | a1i 11 |
. . . . . . . . 9
β’ (π = π β (βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯ β βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯)) |
27 | 9, 26 | bitrd 280 |
. . . . . . . 8
β’ (π = π β (βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯ β βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯)) |
28 | 27 | cbvrexvw 3223 |
. . . . . . 7
β’
(βπ β
π βπ β
(β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯ β βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯) |
29 | 28 | a1i 11 |
. . . . . 6
β’ (π¦ = π₯ β (βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯ β βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯)) |
30 | 7, 29 | bitrd 280 |
. . . . 5
β’ (π¦ = π₯ β (βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π¦ β βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯)) |
31 | 30 | cbvralvw 3222 |
. . . 4
β’
(βπ¦ β
β+ βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π¦ β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯) |
32 | 31 | anbi2i 624 |
. . 3
β’ ((π΄ β β β§
βπ¦ β
β+ βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π¦) β (π΄ β β β§ βπ₯ β β+
βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯)) |
33 | 32 | a1i 11 |
. 2
β’ (π β ((π΄ β β β§ βπ¦ β β+
βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π¦) β (π΄ β β β§ βπ₯ β β+
βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯))) |
34 | 4, 33 | bitrd 280 |
1
β’ (π β (πΉ β π΄ β (π΄ β β β§ βπ₯ β β+
βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯))) |