Step | Hyp | Ref
| Expression |
1 | | breq1 5109 |
. . . . . 6
β’ (π₯ = π¦ β (π₯ β€ (πΉβπ) β π¦ β€ (πΉβπ))) |
2 | 1 | rexralbidv 3211 |
. . . . 5
β’ (π₯ = π¦ β (βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ) β βπ β π βπ β (β€β₯βπ)π¦ β€ (πΉβπ))) |
3 | | fveq2 6843 |
. . . . . . . 8
β’ (π = π β (β€β₯βπ) =
(β€β₯βπ)) |
4 | 3 | raleqdv 3312 |
. . . . . . 7
β’ (π = π β (βπ β (β€β₯βπ)π¦ β€ (πΉβπ) β βπ β (β€β₯βπ)π¦ β€ (πΉβπ))) |
5 | | nfv 1918 |
. . . . . . . 8
β’
β²π π¦ β€ (πΉβπ) |
6 | | nfcv 2904 |
. . . . . . . . 9
β’
β²ππ¦ |
7 | | nfcv 2904 |
. . . . . . . . 9
β’
β²π
β€ |
8 | | xlimpnfxnegmnf.1 |
. . . . . . . . . 10
β’
β²ππΉ |
9 | | nfcv 2904 |
. . . . . . . . . 10
β’
β²ππ |
10 | 8, 9 | nffv 6853 |
. . . . . . . . 9
β’
β²π(πΉβπ) |
11 | 6, 7, 10 | nfbr 5153 |
. . . . . . . 8
β’
β²π π¦ β€ (πΉβπ) |
12 | | fveq2 6843 |
. . . . . . . . 9
β’ (π = π β (πΉβπ) = (πΉβπ)) |
13 | 12 | breq2d 5118 |
. . . . . . . 8
β’ (π = π β (π¦ β€ (πΉβπ) β π¦ β€ (πΉβπ))) |
14 | 5, 11, 13 | cbvralw 3288 |
. . . . . . 7
β’
(βπ β
(β€β₯βπ)π¦ β€ (πΉβπ) β βπ β (β€β₯βπ)π¦ β€ (πΉβπ)) |
15 | 4, 14 | bitrdi 287 |
. . . . . 6
β’ (π = π β (βπ β (β€β₯βπ)π¦ β€ (πΉβπ) β βπ β (β€β₯βπ)π¦ β€ (πΉβπ))) |
16 | 15 | cbvrexvw 3225 |
. . . . 5
β’
(βπ β
π βπ β
(β€β₯βπ)π¦ β€ (πΉβπ) β βπ β π βπ β (β€β₯βπ)π¦ β€ (πΉβπ)) |
17 | 2, 16 | bitrdi 287 |
. . . 4
β’ (π₯ = π¦ β (βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ) β βπ β π βπ β (β€β₯βπ)π¦ β€ (πΉβπ))) |
18 | 17 | cbvralvw 3224 |
. . 3
β’
(βπ₯ β
β βπ β
π βπ β
(β€β₯βπ)π₯ β€ (πΉβπ) β βπ¦ β β βπ β π βπ β (β€β₯βπ)π¦ β€ (πΉβπ)) |
19 | 18 | a1i 11 |
. 2
β’ (π β (βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ) β βπ¦ β β βπ β π βπ β (β€β₯βπ)π¦ β€ (πΉβπ))) |
20 | | simpll 766 |
. . . . 5
β’ (((π β§ βπ¦ β β βπ β π βπ β (β€β₯βπ)π¦ β€ (πΉβπ)) β§ π€ β β) β π) |
21 | | simpr 486 |
. . . . 5
β’ (((π β§ βπ¦ β β βπ β π βπ β (β€β₯βπ)π¦ β€ (πΉβπ)) β§ π€ β β) β π€ β β) |
22 | | xnegrecl 43759 |
. . . . . . 7
β’ (π€ β β β
-ππ€
β β) |
23 | | simpl 484 |
. . . . . . 7
β’
((βπ¦ β
β βπ β
π βπ β
(β€β₯βπ)π¦ β€ (πΉβπ) β§ π€ β β) β βπ¦ β β βπ β π βπ β (β€β₯βπ)π¦ β€ (πΉβπ)) |
24 | | breq1 5109 |
. . . . . . . . 9
β’ (π¦ = -ππ€ β (π¦ β€ (πΉβπ) β -ππ€ β€ (πΉβπ))) |
25 | 24 | rexralbidv 3211 |
. . . . . . . 8
β’ (π¦ = -ππ€ β (βπ β π βπ β (β€β₯βπ)π¦ β€ (πΉβπ) β βπ β π βπ β (β€β₯βπ)-ππ€ β€ (πΉβπ))) |
26 | 25 | rspcva 3578 |
. . . . . . 7
β’
((-ππ€ β β β§ βπ¦ β β βπ β π βπ β (β€β₯βπ)π¦ β€ (πΉβπ)) β βπ β π βπ β (β€β₯βπ)-ππ€ β€ (πΉβπ)) |
27 | 22, 23, 26 | syl2an2 685 |
. . . . . 6
β’
((βπ¦ β
β βπ β
π βπ β
(β€β₯βπ)π¦ β€ (πΉβπ) β§ π€ β β) β βπ β π βπ β (β€β₯βπ)-ππ€ β€ (πΉβπ)) |
28 | 27 | adantll 713 |
. . . . 5
β’ (((π β§ βπ¦ β β βπ β π βπ β (β€β₯βπ)π¦ β€ (πΉβπ)) β§ π€ β β) β βπ β π βπ β (β€β₯βπ)-ππ€ β€ (πΉβπ)) |
29 | | simpll 766 |
. . . . . . . . 9
β’ ((((π β§ π€ β β) β§ π β π) β§ π β (β€β₯βπ)) β (π β§ π€ β β)) |
30 | | xlimpnfxnegmnf.2 |
. . . . . . . . . . 11
β’ π =
(β€β₯βπ) |
31 | 30 | uztrn2 12787 |
. . . . . . . . . 10
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
32 | 31 | adantll 713 |
. . . . . . . . 9
β’ ((((π β§ π€ β β) β§ π β π) β§ π β (β€β₯βπ)) β π β π) |
33 | | rexr 11206 |
. . . . . . . . . . . 12
β’ (π€ β β β π€ β
β*) |
34 | 33 | ad2antlr 726 |
. . . . . . . . . . 11
β’ (((π β§ π€ β β) β§ π β π) β π€ β β*) |
35 | | xlimpnfxnegmnf.3 |
. . . . . . . . . . . . 13
β’ (π β πΉ:πβΆβ*) |
36 | 35 | ffvelcdmda 7036 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β (πΉβπ) β
β*) |
37 | 36 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ π€ β β) β§ π β π) β (πΉβπ) β
β*) |
38 | | xlenegcon1 43808 |
. . . . . . . . . . 11
β’ ((π€ β β*
β§ (πΉβπ) β β*)
β (-ππ€ β€ (πΉβπ) β -π(πΉβπ) β€ π€)) |
39 | 34, 37, 38 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β§ π€ β β) β§ π β π) β (-ππ€ β€ (πΉβπ) β -π(πΉβπ) β€ π€)) |
40 | 39 | biimpd 228 |
. . . . . . . . 9
β’ (((π β§ π€ β β) β§ π β π) β (-ππ€ β€ (πΉβπ) β -π(πΉβπ) β€ π€)) |
41 | 29, 32, 40 | syl2anc 585 |
. . . . . . . 8
β’ ((((π β§ π€ β β) β§ π β π) β§ π β (β€β₯βπ)) β
(-ππ€
β€ (πΉβπ) β
-π(πΉβπ) β€ π€)) |
42 | 41 | ralimdva 3161 |
. . . . . . 7
β’ (((π β§ π€ β β) β§ π β π) β (βπ β (β€β₯βπ)-ππ€ β€ (πΉβπ) β βπ β (β€β₯βπ)-π(πΉβπ) β€ π€)) |
43 | 42 | reximdva 3162 |
. . . . . 6
β’ ((π β§ π€ β β) β (βπ β π βπ β (β€β₯βπ)-ππ€ β€ (πΉβπ) β βπ β π βπ β (β€β₯βπ)-π(πΉβπ) β€ π€)) |
44 | 43 | imp 408 |
. . . . 5
β’ (((π β§ π€ β β) β§ βπ β π βπ β (β€β₯βπ)-ππ€ β€ (πΉβπ)) β βπ β π βπ β (β€β₯βπ)-π(πΉβπ) β€ π€) |
45 | 20, 21, 28, 44 | syl21anc 837 |
. . . 4
β’ (((π β§ βπ¦ β β βπ β π βπ β (β€β₯βπ)π¦ β€ (πΉβπ)) β§ π€ β β) β βπ β π βπ β (β€β₯βπ)-π(πΉβπ) β€ π€) |
46 | 45 | ralrimiva 3140 |
. . 3
β’ ((π β§ βπ¦ β β βπ β π βπ β (β€β₯βπ)π¦ β€ (πΉβπ)) β βπ€ β β βπ β π βπ β (β€β₯βπ)-π(πΉβπ) β€ π€) |
47 | | simpll 766 |
. . . . 5
β’ (((π β§ βπ€ β β βπ β π βπ β (β€β₯βπ)-π(πΉβπ) β€ π€) β§ π¦ β β) β π) |
48 | | simpr 486 |
. . . . 5
β’ (((π β§ βπ€ β β βπ β π βπ β (β€β₯βπ)-π(πΉβπ) β€ π€) β§ π¦ β β) β π¦ β β) |
49 | | xnegrecl 43759 |
. . . . . . 7
β’ (π¦ β β β
-ππ¦
β β) |
50 | | simpl 484 |
. . . . . . 7
β’
((βπ€ β
β βπ β
π βπ β
(β€β₯βπ)-π(πΉβπ) β€ π€ β§ π¦ β β) β βπ€ β β βπ β π βπ β (β€β₯βπ)-π(πΉβπ) β€ π€) |
51 | | breq2 5110 |
. . . . . . . . 9
β’ (π€ = -ππ¦ β
(-π(πΉβπ) β€ π€ β -π(πΉβπ) β€ -ππ¦)) |
52 | 51 | rexralbidv 3211 |
. . . . . . . 8
β’ (π€ = -ππ¦ β (βπ β π βπ β (β€β₯βπ)-π(πΉβπ) β€ π€ β βπ β π βπ β (β€β₯βπ)-π(πΉβπ) β€ -ππ¦)) |
53 | 52 | rspcva 3578 |
. . . . . . 7
β’
((-ππ¦ β β β§ βπ€ β β βπ β π βπ β (β€β₯βπ)-π(πΉβπ) β€ π€) β βπ β π βπ β (β€β₯βπ)-π(πΉβπ) β€ -ππ¦) |
54 | 49, 50, 53 | syl2an2 685 |
. . . . . 6
β’
((βπ€ β
β βπ β
π βπ β
(β€β₯βπ)-π(πΉβπ) β€ π€ β§ π¦ β β) β βπ β π βπ β (β€β₯βπ)-π(πΉβπ) β€ -ππ¦) |
55 | 54 | adantll 713 |
. . . . 5
β’ (((π β§ βπ€ β β βπ β π βπ β (β€β₯βπ)-π(πΉβπ) β€ π€) β§ π¦ β β) β βπ β π βπ β (β€β₯βπ)-π(πΉβπ) β€ -ππ¦) |
56 | | simpll 766 |
. . . . . . . . 9
β’ ((((π β§ π¦ β β) β§ π β π) β§ π β (β€β₯βπ)) β (π β§ π¦ β β)) |
57 | 31 | adantll 713 |
. . . . . . . . 9
β’ ((((π β§ π¦ β β) β§ π β π) β§ π β (β€β₯βπ)) β π β π) |
58 | | rexr 11206 |
. . . . . . . . . . . 12
β’ (π¦ β β β π¦ β
β*) |
59 | 58 | ad2antlr 726 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β) β§ π β π) β π¦ β β*) |
60 | 36 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β) β§ π β π) β (πΉβπ) β
β*) |
61 | | xleneg 13143 |
. . . . . . . . . . 11
β’ ((π¦ β β*
β§ (πΉβπ) β β*)
β (π¦ β€ (πΉβπ) β -π(πΉβπ) β€ -ππ¦)) |
62 | 59, 60, 61 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β) β§ π β π) β (π¦ β€ (πΉβπ) β -π(πΉβπ) β€ -ππ¦)) |
63 | 62 | biimprd 248 |
. . . . . . . . 9
β’ (((π β§ π¦ β β) β§ π β π) β (-π(πΉβπ) β€ -ππ¦ β π¦ β€ (πΉβπ))) |
64 | 56, 57, 63 | syl2anc 585 |
. . . . . . . 8
β’ ((((π β§ π¦ β β) β§ π β π) β§ π β (β€β₯βπ)) β
(-π(πΉβπ) β€ -ππ¦ β π¦ β€ (πΉβπ))) |
65 | 64 | ralimdva 3161 |
. . . . . . 7
β’ (((π β§ π¦ β β) β§ π β π) β (βπ β (β€β₯βπ)-π(πΉβπ) β€ -ππ¦ β βπ β
(β€β₯βπ)π¦ β€ (πΉβπ))) |
66 | 65 | reximdva 3162 |
. . . . . 6
β’ ((π β§ π¦ β β) β (βπ β π βπ β (β€β₯βπ)-π(πΉβπ) β€ -ππ¦ β βπ β π βπ β (β€β₯βπ)π¦ β€ (πΉβπ))) |
67 | 66 | imp 408 |
. . . . 5
β’ (((π β§ π¦ β β) β§ βπ β π βπ β (β€β₯βπ)-π(πΉβπ) β€ -ππ¦) β βπ β π βπ β (β€β₯βπ)π¦ β€ (πΉβπ)) |
68 | 47, 48, 55, 67 | syl21anc 837 |
. . . 4
β’ (((π β§ βπ€ β β βπ β π βπ β (β€β₯βπ)-π(πΉβπ) β€ π€) β§ π¦ β β) β βπ β π βπ β (β€β₯βπ)π¦ β€ (πΉβπ)) |
69 | 68 | ralrimiva 3140 |
. . 3
β’ ((π β§ βπ€ β β βπ β π βπ β (β€β₯βπ)-π(πΉβπ) β€ π€) β βπ¦ β β βπ β π βπ β (β€β₯βπ)π¦ β€ (πΉβπ)) |
70 | 46, 69 | impbida 800 |
. 2
β’ (π β (βπ¦ β β βπ β π βπ β (β€β₯βπ)π¦ β€ (πΉβπ) β βπ€ β β βπ β π βπ β (β€β₯βπ)-π(πΉβπ) β€ π€)) |
71 | | breq2 5110 |
. . . . . 6
β’ (π€ = π₯ β (-π(πΉβπ) β€ π€ β -π(πΉβπ) β€ π₯)) |
72 | 71 | rexralbidv 3211 |
. . . . 5
β’ (π€ = π₯ β (βπ β π βπ β (β€β₯βπ)-π(πΉβπ) β€ π€ β βπ β π βπ β (β€β₯βπ)-π(πΉβπ) β€ π₯)) |
73 | | fveq2 6843 |
. . . . . . . 8
β’ (π = π β (β€β₯βπ) =
(β€β₯βπ)) |
74 | 73 | raleqdv 3312 |
. . . . . . 7
β’ (π = π β (βπ β (β€β₯βπ)-π(πΉβπ) β€ π₯ β βπ β (β€β₯βπ)-π(πΉβπ) β€ π₯)) |
75 | 10 | nfxneg 43782 |
. . . . . . . . 9
β’
β²π-π(πΉβπ) |
76 | | nfcv 2904 |
. . . . . . . . 9
β’
β²ππ₯ |
77 | 75, 7, 76 | nfbr 5153 |
. . . . . . . 8
β’
β²π-π(πΉβπ) β€ π₯ |
78 | | nfv 1918 |
. . . . . . . 8
β’
β²π-π(πΉβπ) β€ π₯ |
79 | | fveq2 6843 |
. . . . . . . . . 10
β’ (π = π β (πΉβπ) = (πΉβπ)) |
80 | 79 | xnegeqd 43758 |
. . . . . . . . 9
β’ (π = π β -π(πΉβπ) = -π(πΉβπ)) |
81 | 80 | breq1d 5116 |
. . . . . . . 8
β’ (π = π β (-π(πΉβπ) β€ π₯ β -π(πΉβπ) β€ π₯)) |
82 | 77, 78, 81 | cbvralw 3288 |
. . . . . . 7
β’
(βπ β
(β€β₯βπ)-π(πΉβπ) β€ π₯ β βπ β (β€β₯βπ)-π(πΉβπ) β€ π₯) |
83 | 74, 82 | bitrdi 287 |
. . . . . 6
β’ (π = π β (βπ β (β€β₯βπ)-π(πΉβπ) β€ π₯ β βπ β (β€β₯βπ)-π(πΉβπ) β€ π₯)) |
84 | 83 | cbvrexvw 3225 |
. . . . 5
β’
(βπ β
π βπ β
(β€β₯βπ)-π(πΉβπ) β€ π₯ β βπ β π βπ β (β€β₯βπ)-π(πΉβπ) β€ π₯) |
85 | 72, 84 | bitrdi 287 |
. . . 4
β’ (π€ = π₯ β (βπ β π βπ β (β€β₯βπ)-π(πΉβπ) β€ π€ β βπ β π βπ β (β€β₯βπ)-π(πΉβπ) β€ π₯)) |
86 | 85 | cbvralvw 3224 |
. . 3
β’
(βπ€ β
β βπ β
π βπ β
(β€β₯βπ)-π(πΉβπ) β€ π€ β βπ₯ β β βπ β π βπ β (β€β₯βπ)-π(πΉβπ) β€ π₯) |
87 | 86 | a1i 11 |
. 2
β’ (π β (βπ€ β β βπ β π βπ β (β€β₯βπ)-π(πΉβπ) β€ π€ β βπ₯ β β βπ β π βπ β (β€β₯βπ)-π(πΉβπ) β€ π₯)) |
88 | 19, 70, 87 | 3bitrd 305 |
1
β’ (π β (βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ) β βπ₯ β β βπ β π βπ β (β€β₯βπ)-π(πΉβπ) β€ π₯)) |