Step | Hyp | Ref
| Expression |
1 | | fdvposlt.d |
. . . 4
β’ πΈ = (πΆ(,)π·) |
2 | | fdvposlt.a |
. . . 4
β’ (π β π΄ β πΈ) |
3 | | fdvposlt.b |
. . . 4
β’ (π β π΅ β πΈ) |
4 | | fdvposlt.f |
. . . . . . 7
β’ (π β πΉ:πΈβΆβ) |
5 | 4 | ffvelcdmda 7083 |
. . . . . 6
β’ ((π β§ π¦ β πΈ) β (πΉβπ¦) β β) |
6 | 5 | renegcld 11637 |
. . . . 5
β’ ((π β§ π¦ β πΈ) β -(πΉβπ¦) β β) |
7 | 6 | fmpttd 7111 |
. . . 4
β’ (π β (π¦ β πΈ β¦ -(πΉβπ¦)):πΈβΆβ) |
8 | | reelprrecn 11198 |
. . . . . . 7
β’ β
β {β, β} |
9 | 8 | a1i 11 |
. . . . . 6
β’ (π β β β {β,
β}) |
10 | | ax-resscn 11163 |
. . . . . . 7
β’ β
β β |
11 | 10, 5 | sselid 3979 |
. . . . . 6
β’ ((π β§ π¦ β πΈ) β (πΉβπ¦) β β) |
12 | | fvexd 6903 |
. . . . . 6
β’ ((π β§ π¦ β πΈ) β ((β D πΉ)βπ¦) β V) |
13 | 4 | feqmptd 6957 |
. . . . . . . 8
β’ (π β πΉ = (π¦ β πΈ β¦ (πΉβπ¦))) |
14 | 13 | oveq2d 7421 |
. . . . . . 7
β’ (π β (β D πΉ) = (β D (π¦ β πΈ β¦ (πΉβπ¦)))) |
15 | | fdvposlt.c |
. . . . . . . . 9
β’ (π β (β D πΉ) β (πΈβcnββ)) |
16 | | cncff 24400 |
. . . . . . . . 9
β’ ((β
D πΉ) β (πΈβcnββ) β (β D πΉ):πΈβΆβ) |
17 | 15, 16 | syl 17 |
. . . . . . . 8
β’ (π β (β D πΉ):πΈβΆβ) |
18 | 17 | feqmptd 6957 |
. . . . . . 7
β’ (π β (β D πΉ) = (π¦ β πΈ β¦ ((β D πΉ)βπ¦))) |
19 | 14, 18 | eqtr3d 2774 |
. . . . . 6
β’ (π β (β D (π¦ β πΈ β¦ (πΉβπ¦))) = (π¦ β πΈ β¦ ((β D πΉ)βπ¦))) |
20 | 9, 11, 12, 19 | dvmptneg 25474 |
. . . . 5
β’ (π β (β D (π¦ β πΈ β¦ -(πΉβπ¦))) = (π¦ β πΈ β¦ -((β D πΉ)βπ¦))) |
21 | 17 | ffvelcdmda 7083 |
. . . . . . . 8
β’ ((π β§ π¦ β πΈ) β ((β D πΉ)βπ¦) β β) |
22 | 21 | renegcld 11637 |
. . . . . . 7
β’ ((π β§ π¦ β πΈ) β -((β D πΉ)βπ¦) β β) |
23 | 22 | fmpttd 7111 |
. . . . . 6
β’ (π β (π¦ β πΈ β¦ -((β D πΉ)βπ¦)):πΈβΆβ) |
24 | | ssid 4003 |
. . . . . . . . . 10
β’ β
β β |
25 | | cncfss 24406 |
. . . . . . . . . 10
β’ ((β
β β β§ β β β) β (πΈβcnββ) β (πΈβcnββ)) |
26 | 10, 24, 25 | mp2an 690 |
. . . . . . . . 9
β’ (πΈβcnββ) β (πΈβcnββ) |
27 | 26, 15 | sselid 3979 |
. . . . . . . 8
β’ (π β (β D πΉ) β (πΈβcnββ)) |
28 | | eqid 2732 |
. . . . . . . . 9
β’ (π¦ β πΈ β¦ -((β D πΉ)βπ¦)) = (π¦ β πΈ β¦ -((β D πΉ)βπ¦)) |
29 | 28 | negfcncf 24430 |
. . . . . . . 8
β’ ((β
D πΉ) β (πΈβcnββ) β (π¦ β πΈ β¦ -((β D πΉ)βπ¦)) β (πΈβcnββ)) |
30 | 27, 29 | syl 17 |
. . . . . . 7
β’ (π β (π¦ β πΈ β¦ -((β D πΉ)βπ¦)) β (πΈβcnββ)) |
31 | | cncfcdm 24405 |
. . . . . . 7
β’ ((β
β β β§ (π¦
β πΈ β¦ -((β
D πΉ)βπ¦)) β (πΈβcnββ)) β ((π¦ β πΈ β¦ -((β D πΉ)βπ¦)) β (πΈβcnββ) β (π¦ β πΈ β¦ -((β D πΉ)βπ¦)):πΈβΆβ)) |
32 | 10, 30, 31 | sylancr 587 |
. . . . . 6
β’ (π β ((π¦ β πΈ β¦ -((β D πΉ)βπ¦)) β (πΈβcnββ) β (π¦ β πΈ β¦ -((β D πΉ)βπ¦)):πΈβΆβ)) |
33 | 23, 32 | mpbird 256 |
. . . . 5
β’ (π β (π¦ β πΈ β¦ -((β D πΉ)βπ¦)) β (πΈβcnββ)) |
34 | 20, 33 | eqeltrd 2833 |
. . . 4
β’ (π β (β D (π¦ β πΈ β¦ -(πΉβπ¦))) β (πΈβcnββ)) |
35 | | fdvnegge.le |
. . . 4
β’ (π β π΄ β€ π΅) |
36 | | fdvnegge.1 |
. . . . . 6
β’ ((π β§ π₯ β (π΄(,)π΅)) β ((β D πΉ)βπ₯) β€ 0) |
37 | 17 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π₯ β (π΄(,)π΅)) β (β D πΉ):πΈβΆβ) |
38 | | ioossicc 13406 |
. . . . . . . . . . 11
β’ (π΄(,)π΅) β (π΄[,]π΅) |
39 | 38 | a1i 11 |
. . . . . . . . . 10
β’ (π β (π΄(,)π΅) β (π΄[,]π΅)) |
40 | 1, 2, 3 | fct2relem 33597 |
. . . . . . . . . 10
β’ (π β (π΄[,]π΅) β πΈ) |
41 | 39, 40 | sstrd 3991 |
. . . . . . . . 9
β’ (π β (π΄(,)π΅) β πΈ) |
42 | 41 | sselda 3981 |
. . . . . . . 8
β’ ((π β§ π₯ β (π΄(,)π΅)) β π₯ β πΈ) |
43 | 37, 42 | ffvelcdmd 7084 |
. . . . . . 7
β’ ((π β§ π₯ β (π΄(,)π΅)) β ((β D πΉ)βπ₯) β β) |
44 | 43 | le0neg1d 11781 |
. . . . . 6
β’ ((π β§ π₯ β (π΄(,)π΅)) β (((β D πΉ)βπ₯) β€ 0 β 0 β€ -((β D πΉ)βπ₯))) |
45 | 36, 44 | mpbid 231 |
. . . . 5
β’ ((π β§ π₯ β (π΄(,)π΅)) β 0 β€ -((β D πΉ)βπ₯)) |
46 | 20 | adantr 481 |
. . . . . . 7
β’ ((π β§ π₯ β (π΄(,)π΅)) β (β D (π¦ β πΈ β¦ -(πΉβπ¦))) = (π¦ β πΈ β¦ -((β D πΉ)βπ¦))) |
47 | 46 | fveq1d 6890 |
. . . . . 6
β’ ((π β§ π₯ β (π΄(,)π΅)) β ((β D (π¦ β πΈ β¦ -(πΉβπ¦)))βπ₯) = ((π¦ β πΈ β¦ -((β D πΉ)βπ¦))βπ₯)) |
48 | 28 | a1i 11 |
. . . . . . 7
β’ ((π β§ π₯ β (π΄(,)π΅)) β (π¦ β πΈ β¦ -((β D πΉ)βπ¦)) = (π¦ β πΈ β¦ -((β D πΉ)βπ¦))) |
49 | | simpr 485 |
. . . . . . . . 9
β’ (((π β§ π₯ β (π΄(,)π΅)) β§ π¦ = π₯) β π¦ = π₯) |
50 | 49 | fveq2d 6892 |
. . . . . . . 8
β’ (((π β§ π₯ β (π΄(,)π΅)) β§ π¦ = π₯) β ((β D πΉ)βπ¦) = ((β D πΉ)βπ₯)) |
51 | 50 | negeqd 11450 |
. . . . . . 7
β’ (((π β§ π₯ β (π΄(,)π΅)) β§ π¦ = π₯) β -((β D πΉ)βπ¦) = -((β D πΉ)βπ₯)) |
52 | 43 | renegcld 11637 |
. . . . . . 7
β’ ((π β§ π₯ β (π΄(,)π΅)) β -((β D πΉ)βπ₯) β β) |
53 | 48, 51, 42, 52 | fvmptd 7002 |
. . . . . 6
β’ ((π β§ π₯ β (π΄(,)π΅)) β ((π¦ β πΈ β¦ -((β D πΉ)βπ¦))βπ₯) = -((β D πΉ)βπ₯)) |
54 | 47, 53 | eqtrd 2772 |
. . . . 5
β’ ((π β§ π₯ β (π΄(,)π΅)) β ((β D (π¦ β πΈ β¦ -(πΉβπ¦)))βπ₯) = -((β D πΉ)βπ₯)) |
55 | 45, 54 | breqtrrd 5175 |
. . . 4
β’ ((π β§ π₯ β (π΄(,)π΅)) β 0 β€ ((β D (π¦ β πΈ β¦ -(πΉβπ¦)))βπ₯)) |
56 | 1, 2, 3, 7, 34, 35, 55 | fdvposle 33601 |
. . 3
β’ (π β ((π¦ β πΈ β¦ -(πΉβπ¦))βπ΄) β€ ((π¦ β πΈ β¦ -(πΉβπ¦))βπ΅)) |
57 | | eqidd 2733 |
. . . 4
β’ (π β (π¦ β πΈ β¦ -(πΉβπ¦)) = (π¦ β πΈ β¦ -(πΉβπ¦))) |
58 | | simpr 485 |
. . . . . 6
β’ ((π β§ π¦ = π΄) β π¦ = π΄) |
59 | 58 | fveq2d 6892 |
. . . . 5
β’ ((π β§ π¦ = π΄) β (πΉβπ¦) = (πΉβπ΄)) |
60 | 59 | negeqd 11450 |
. . . 4
β’ ((π β§ π¦ = π΄) β -(πΉβπ¦) = -(πΉβπ΄)) |
61 | 4, 2 | ffvelcdmd 7084 |
. . . . 5
β’ (π β (πΉβπ΄) β β) |
62 | 61 | renegcld 11637 |
. . . 4
β’ (π β -(πΉβπ΄) β β) |
63 | 57, 60, 2, 62 | fvmptd 7002 |
. . 3
β’ (π β ((π¦ β πΈ β¦ -(πΉβπ¦))βπ΄) = -(πΉβπ΄)) |
64 | | simpr 485 |
. . . . . 6
β’ ((π β§ π¦ = π΅) β π¦ = π΅) |
65 | 64 | fveq2d 6892 |
. . . . 5
β’ ((π β§ π¦ = π΅) β (πΉβπ¦) = (πΉβπ΅)) |
66 | 65 | negeqd 11450 |
. . . 4
β’ ((π β§ π¦ = π΅) β -(πΉβπ¦) = -(πΉβπ΅)) |
67 | 4, 3 | ffvelcdmd 7084 |
. . . . 5
β’ (π β (πΉβπ΅) β β) |
68 | 67 | renegcld 11637 |
. . . 4
β’ (π β -(πΉβπ΅) β β) |
69 | 57, 66, 3, 68 | fvmptd 7002 |
. . 3
β’ (π β ((π¦ β πΈ β¦ -(πΉβπ¦))βπ΅) = -(πΉβπ΅)) |
70 | 56, 63, 69 | 3brtr3d 5178 |
. 2
β’ (π β -(πΉβπ΄) β€ -(πΉβπ΅)) |
71 | 67, 61 | lenegd 11789 |
. 2
β’ (π β ((πΉβπ΅) β€ (πΉβπ΄) β -(πΉβπ΄) β€ -(πΉβπ΅))) |
72 | 70, 71 | mpbird 256 |
1
β’ (π β (πΉβπ΅) β€ (πΉβπ΄)) |