Step | Hyp | Ref
| Expression |
1 | | climcl 15390 |
. . . 4
β’ (πΉ β π΄ β π΄ β β) |
2 | 1 | adantl 483 |
. . 3
β’ ((π β§ πΉ β π΄) β π΄ β β) |
3 | | id 22 |
. . . . . . 7
β’ (πΉ β π΄ β πΉ β π΄) |
4 | | climrel 15383 |
. . . . . . . . 9
β’ Rel
β |
5 | 4 | brrelex1i 5692 |
. . . . . . . 8
β’ (πΉ β π΄ β πΉ β V) |
6 | | eqidd 2734 |
. . . . . . . 8
β’ ((πΉ β π΄ β§ π β β€) β (πΉβπ) = (πΉβπ)) |
7 | 5, 6 | clim 15385 |
. . . . . . 7
β’ (πΉ β π΄ β (πΉ β π΄ β (π΄ β β β§ βπ₯ β β+
βπ β β€
βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯)))) |
8 | 3, 7 | mpbid 231 |
. . . . . 6
β’ (πΉ β π΄ β (π΄ β β β§ βπ₯ β β+
βπ β β€
βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯))) |
9 | 8 | simprd 497 |
. . . . 5
β’ (πΉ β π΄ β βπ₯ β β+ βπ β β€ βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯)) |
10 | 9 | adantl 483 |
. . . 4
β’ ((π β§ πΉ β π΄) β βπ₯ β β+ βπ β β€ βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯)) |
11 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ βπ β β€ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯)) β βπ β β€ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯)) |
12 | | climuzlem.1 |
. . . . . . . . . . . 12
β’ (π β π β β€) |
13 | | climuzlem.2 |
. . . . . . . . . . . . 13
β’ π =
(β€β₯βπ) |
14 | 13 | rexuz3 15242 |
. . . . . . . . . . . 12
β’ (π β β€ β
(βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯) β βπ β β€ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯))) |
15 | 12, 14 | syl 17 |
. . . . . . . . . . 11
β’ (π β (βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯) β βπ β β€ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯))) |
16 | 15 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ βπ β β€ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯)) β (βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯) β βπ β β€ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯))) |
17 | 11, 16 | mpbird 257 |
. . . . . . . . 9
β’ ((π β§ βπ β β€ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯)) β βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯)) |
18 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯) β (absβ((πΉβπ) β π΄)) < π₯) |
19 | 18 | ralimi 3083 |
. . . . . . . . . . 11
β’
(βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯) β βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯) |
20 | 19 | reximi 3084 |
. . . . . . . . . 10
β’
(βπ β
π βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯) β βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯) |
21 | 20 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ βπ β β€ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯)) β (βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯) β βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯)) |
22 | 17, 21 | mpd 15 |
. . . . . . . 8
β’ ((π β§ βπ β β€ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯)) β βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯) |
23 | 22 | ex 414 |
. . . . . . 7
β’ (π β (βπ β β€ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯) β βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯)) |
24 | 23 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β β+) β
(βπ β β€
βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯) β βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯)) |
25 | 24 | ralimdva 3161 |
. . . . 5
β’ (π β (βπ₯ β β+
βπ β β€
βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯) β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯)) |
26 | 25 | adantr 482 |
. . . 4
β’ ((π β§ πΉ β π΄) β (βπ₯ β β+ βπ β β€ βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯) β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯)) |
27 | 10, 26 | mpd 15 |
. . 3
β’ ((π β§ πΉ β π΄) β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯) |
28 | 2, 27 | jca 513 |
. 2
β’ ((π β§ πΉ β π΄) β (π΄ β β β§ βπ₯ β β+
βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯)) |
29 | | simprl 770 |
. . . 4
β’ ((π β§ (π΄ β β β§ βπ₯ β β+
βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯)) β π΄ β β) |
30 | | nfv 1918 |
. . . . . . . 8
β’
β²ππ |
31 | | nfre1 3267 |
. . . . . . . 8
β’
β²πβπ β β€ βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯) |
32 | 13 | uzssz2 43781 |
. . . . . . . . . . . 12
β’ π β
β€ |
33 | 32 | sseli 3944 |
. . . . . . . . . . 11
β’ (π β π β π β β€) |
34 | 33 | 3ad2ant2 1135 |
. . . . . . . . . 10
β’ ((π β§ π β π β§ βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯) β π β β€) |
35 | | simpll 766 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β π) |
36 | 13 | uztrn2 12790 |
. . . . . . . . . . . . . . . . 17
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
37 | 36 | adantll 713 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β π β π) |
38 | | climuzlem.3 |
. . . . . . . . . . . . . . . . 17
β’ (π β πΉ:πβΆβ) |
39 | 38 | ffvelcdmda 7039 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π) β (πΉβπ) β β) |
40 | 35, 37, 39 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β (πΉβπ) β β) |
41 | 40 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β π) β§ π β (β€β₯βπ)) β§ (absβ((πΉβπ) β π΄)) < π₯) β (πΉβπ) β β) |
42 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β π) β§ π β (β€β₯βπ)) β§ (absβ((πΉβπ) β π΄)) < π₯) β (absβ((πΉβπ) β π΄)) < π₯) |
43 | 41, 42 | jca 513 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π) β§ π β (β€β₯βπ)) β§ (absβ((πΉβπ) β π΄)) < π₯) β ((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯)) |
44 | 43 | ex 414 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β ((absβ((πΉβπ) β π΄)) < π₯ β ((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯))) |
45 | 44 | ralimdva 3161 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯ β βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯))) |
46 | 45 | 3impia 1118 |
. . . . . . . . . 10
β’ ((π β§ π β π β§ βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯) β βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯)) |
47 | | rspe 3231 |
. . . . . . . . . 10
β’ ((π β β€ β§
βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯)) β βπ β β€ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯)) |
48 | 34, 46, 47 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ π β π β§ βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯) β βπ β β€ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯)) |
49 | 48 | 3exp 1120 |
. . . . . . . 8
β’ (π β (π β π β (βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯ β βπ β β€ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯)))) |
50 | 30, 31, 49 | rexlimd 3248 |
. . . . . . 7
β’ (π β (βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯ β βπ β β€ βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯))) |
51 | 50 | ralimdv 3163 |
. . . . . 6
β’ (π β (βπ₯ β β+
βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯ β βπ₯ β β+ βπ β β€ βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯))) |
52 | 51 | imp 408 |
. . . . 5
β’ ((π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯) β βπ₯ β β+ βπ β β€ βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯)) |
53 | 52 | adantrl 715 |
. . . 4
β’ ((π β§ (π΄ β β β§ βπ₯ β β+
βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯)) β βπ₯ β β+ βπ β β€ βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯)) |
54 | 29, 53 | jca 513 |
. . 3
β’ ((π β§ (π΄ β β β§ βπ₯ β β+
βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯)) β (π΄ β β β§ βπ₯ β β+
βπ β β€
βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯))) |
55 | 13 | fvexi 6860 |
. . . . . . 7
β’ π β V |
56 | 55 | a1i 11 |
. . . . . 6
β’ (π β π β V) |
57 | 38, 56 | fexd 7181 |
. . . . 5
β’ (π β πΉ β V) |
58 | | eqidd 2734 |
. . . . 5
β’ ((π β§ π β β€) β (πΉβπ) = (πΉβπ)) |
59 | 57, 58 | clim 15385 |
. . . 4
β’ (π β (πΉ β π΄ β (π΄ β β β§ βπ₯ β β+
βπ β β€
βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯)))) |
60 | 59 | adantr 482 |
. . 3
β’ ((π β§ (π΄ β β β§ βπ₯ β β+
βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯)) β (πΉ β π΄ β (π΄ β β β§ βπ₯ β β+
βπ β β€
βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β π΄)) < π₯)))) |
61 | 54, 60 | mpbird 257 |
. 2
β’ ((π β§ (π΄ β β β§ βπ₯ β β+
βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯)) β πΉ β π΄) |
62 | 28, 61 | impbida 800 |
1
β’ (π β (πΉ β π΄ β (π΄ β β β§ βπ₯ β β+
βπ β π βπ β (β€β₯βπ)(absβ((πΉβπ) β π΄)) < π₯))) |