Step | Hyp | Ref
| Expression |
1 | | ivth.1 |
. . 3
β’ (π β π΄ β β) |
2 | | ivth.2 |
. . 3
β’ (π β π΅ β β) |
3 | | ivth.3 |
. . . 4
β’ (π β π β β) |
4 | 3 | renegcld 8336 |
. . 3
β’ (π β -π β β) |
5 | | ivth.4 |
. . 3
β’ (π β π΄ < π΅) |
6 | | ivth.5 |
. . 3
β’ (π β (π΄[,]π΅) β π·) |
7 | | ivth.7 |
. . . 4
β’ (π β πΉ β (π·βcnββ)) |
8 | | eqid 2177 |
. . . . 5
β’ (π€ β π· β¦ -(πΉβπ€)) = (π€ β π· β¦ -(πΉβπ€)) |
9 | 8 | negfcncf 14059 |
. . . 4
β’ (πΉ β (π·βcnββ) β (π€ β π· β¦ -(πΉβπ€)) β (π·βcnββ)) |
10 | 7, 9 | syl 14 |
. . 3
β’ (π β (π€ β π· β¦ -(πΉβπ€)) β (π·βcnββ)) |
11 | | fveq2 5515 |
. . . . . 6
β’ (π€ = π₯ β (πΉβπ€) = (πΉβπ₯)) |
12 | 11 | negeqd 8151 |
. . . . 5
β’ (π€ = π₯ β -(πΉβπ€) = -(πΉβπ₯)) |
13 | 6 | sselda 3155 |
. . . . 5
β’ ((π β§ π₯ β (π΄[,]π΅)) β π₯ β π·) |
14 | | ivth.8 |
. . . . . 6
β’ ((π β§ π₯ β (π΄[,]π΅)) β (πΉβπ₯) β β) |
15 | 14 | renegcld 8336 |
. . . . 5
β’ ((π β§ π₯ β (π΄[,]π΅)) β -(πΉβπ₯) β β) |
16 | 8, 12, 13, 15 | fvmptd3 5609 |
. . . 4
β’ ((π β§ π₯ β (π΄[,]π΅)) β ((π€ β π· β¦ -(πΉβπ€))βπ₯) = -(πΉβπ₯)) |
17 | 16, 15 | eqeltrd 2254 |
. . 3
β’ ((π β§ π₯ β (π΄[,]π΅)) β ((π€ β π· β¦ -(πΉβπ€))βπ₯) β β) |
18 | | fveq2 5515 |
. . . . . . 7
β’ (π€ = π΄ β (πΉβπ€) = (πΉβπ΄)) |
19 | 18 | negeqd 8151 |
. . . . . 6
β’ (π€ = π΄ β -(πΉβπ€) = -(πΉβπ΄)) |
20 | 1 | rexrd 8006 |
. . . . . . . 8
β’ (π β π΄ β
β*) |
21 | 2 | rexrd 8006 |
. . . . . . . 8
β’ (π β π΅ β
β*) |
22 | 1, 2, 5 | ltled 8075 |
. . . . . . . 8
β’ (π β π΄ β€ π΅) |
23 | | lbicc2 9983 |
. . . . . . . 8
β’ ((π΄ β β*
β§ π΅ β
β* β§ π΄
β€ π΅) β π΄ β (π΄[,]π΅)) |
24 | 20, 21, 22, 23 | syl3anc 1238 |
. . . . . . 7
β’ (π β π΄ β (π΄[,]π΅)) |
25 | 6, 24 | sseldd 3156 |
. . . . . 6
β’ (π β π΄ β π·) |
26 | | fveq2 5515 |
. . . . . . . . 9
β’ (π₯ = π΄ β (πΉβπ₯) = (πΉβπ΄)) |
27 | 26 | eleq1d 2246 |
. . . . . . . 8
β’ (π₯ = π΄ β ((πΉβπ₯) β β β (πΉβπ΄) β β)) |
28 | 14 | ralrimiva 2550 |
. . . . . . . 8
β’ (π β βπ₯ β (π΄[,]π΅)(πΉβπ₯) β β) |
29 | 27, 28, 24 | rspcdva 2846 |
. . . . . . 7
β’ (π β (πΉβπ΄) β β) |
30 | 29 | renegcld 8336 |
. . . . . 6
β’ (π β -(πΉβπ΄) β β) |
31 | 8, 19, 25, 30 | fvmptd3 5609 |
. . . . 5
β’ (π β ((π€ β π· β¦ -(πΉβπ€))βπ΄) = -(πΉβπ΄)) |
32 | | ivthdec.9 |
. . . . . . 7
β’ (π β ((πΉβπ΅) < π β§ π < (πΉβπ΄))) |
33 | 32 | simprd 114 |
. . . . . 6
β’ (π β π < (πΉβπ΄)) |
34 | 3, 29 | ltnegd 8479 |
. . . . . 6
β’ (π β (π < (πΉβπ΄) β -(πΉβπ΄) < -π)) |
35 | 33, 34 | mpbid 147 |
. . . . 5
β’ (π β -(πΉβπ΄) < -π) |
36 | 31, 35 | eqbrtrd 4025 |
. . . 4
β’ (π β ((π€ β π· β¦ -(πΉβπ€))βπ΄) < -π) |
37 | 32 | simpld 112 |
. . . . . 6
β’ (π β (πΉβπ΅) < π) |
38 | | fveq2 5515 |
. . . . . . . . 9
β’ (π₯ = π΅ β (πΉβπ₯) = (πΉβπ΅)) |
39 | 38 | eleq1d 2246 |
. . . . . . . 8
β’ (π₯ = π΅ β ((πΉβπ₯) β β β (πΉβπ΅) β β)) |
40 | | ubicc2 9984 |
. . . . . . . . 9
β’ ((π΄ β β*
β§ π΅ β
β* β§ π΄
β€ π΅) β π΅ β (π΄[,]π΅)) |
41 | 20, 21, 22, 40 | syl3anc 1238 |
. . . . . . . 8
β’ (π β π΅ β (π΄[,]π΅)) |
42 | 39, 28, 41 | rspcdva 2846 |
. . . . . . 7
β’ (π β (πΉβπ΅) β β) |
43 | 42, 3 | ltnegd 8479 |
. . . . . 6
β’ (π β ((πΉβπ΅) < π β -π < -(πΉβπ΅))) |
44 | 37, 43 | mpbid 147 |
. . . . 5
β’ (π β -π < -(πΉβπ΅)) |
45 | | fveq2 5515 |
. . . . . . 7
β’ (π€ = π΅ β (πΉβπ€) = (πΉβπ΅)) |
46 | 45 | negeqd 8151 |
. . . . . 6
β’ (π€ = π΅ β -(πΉβπ€) = -(πΉβπ΅)) |
47 | 6, 41 | sseldd 3156 |
. . . . . 6
β’ (π β π΅ β π·) |
48 | 42 | renegcld 8336 |
. . . . . 6
β’ (π β -(πΉβπ΅) β β) |
49 | 8, 46, 47, 48 | fvmptd3 5609 |
. . . . 5
β’ (π β ((π€ β π· β¦ -(πΉβπ€))βπ΅) = -(πΉβπ΅)) |
50 | 44, 49 | breqtrrd 4031 |
. . . 4
β’ (π β -π < ((π€ β π· β¦ -(πΉβπ€))βπ΅)) |
51 | 36, 50 | jca 306 |
. . 3
β’ (π β (((π€ β π· β¦ -(πΉβπ€))βπ΄) < -π β§ -π < ((π€ β π· β¦ -(πΉβπ€))βπ΅))) |
52 | | ivthdec.i |
. . . . 5
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ (π¦ β (π΄[,]π΅) β§ π₯ < π¦)) β (πΉβπ¦) < (πΉβπ₯)) |
53 | | fveq2 5515 |
. . . . . . . 8
β’ (π₯ = π¦ β (πΉβπ₯) = (πΉβπ¦)) |
54 | 53 | eleq1d 2246 |
. . . . . . 7
β’ (π₯ = π¦ β ((πΉβπ₯) β β β (πΉβπ¦) β β)) |
55 | | simpll 527 |
. . . . . . . 8
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ (π¦ β (π΄[,]π΅) β§ π₯ < π¦)) β π) |
56 | 55, 28 | syl 14 |
. . . . . . 7
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ (π¦ β (π΄[,]π΅) β§ π₯ < π¦)) β βπ₯ β (π΄[,]π΅)(πΉβπ₯) β β) |
57 | | simprl 529 |
. . . . . . 7
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ (π¦ β (π΄[,]π΅) β§ π₯ < π¦)) β π¦ β (π΄[,]π΅)) |
58 | 54, 56, 57 | rspcdva 2846 |
. . . . . 6
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ (π¦ β (π΄[,]π΅) β§ π₯ < π¦)) β (πΉβπ¦) β β) |
59 | 14 | adantr 276 |
. . . . . 6
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ (π¦ β (π΄[,]π΅) β§ π₯ < π¦)) β (πΉβπ₯) β β) |
60 | 58, 59 | ltnegd 8479 |
. . . . 5
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ (π¦ β (π΄[,]π΅) β§ π₯ < π¦)) β ((πΉβπ¦) < (πΉβπ₯) β -(πΉβπ₯) < -(πΉβπ¦))) |
61 | 52, 60 | mpbid 147 |
. . . 4
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ (π¦ β (π΄[,]π΅) β§ π₯ < π¦)) β -(πΉβπ₯) < -(πΉβπ¦)) |
62 | 13 | adantr 276 |
. . . . 5
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ (π¦ β (π΄[,]π΅) β§ π₯ < π¦)) β π₯ β π·) |
63 | 15 | adantr 276 |
. . . . 5
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ (π¦ β (π΄[,]π΅) β§ π₯ < π¦)) β -(πΉβπ₯) β β) |
64 | 8, 12, 62, 63 | fvmptd3 5609 |
. . . 4
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ (π¦ β (π΄[,]π΅) β§ π₯ < π¦)) β ((π€ β π· β¦ -(πΉβπ€))βπ₯) = -(πΉβπ₯)) |
65 | | fveq2 5515 |
. . . . . 6
β’ (π€ = π¦ β (πΉβπ€) = (πΉβπ¦)) |
66 | 65 | negeqd 8151 |
. . . . 5
β’ (π€ = π¦ β -(πΉβπ€) = -(πΉβπ¦)) |
67 | 6 | sseld 3154 |
. . . . . 6
β’ (π β (π¦ β (π΄[,]π΅) β π¦ β π·)) |
68 | 55, 57, 67 | sylc 62 |
. . . . 5
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ (π¦ β (π΄[,]π΅) β§ π₯ < π¦)) β π¦ β π·) |
69 | 58 | renegcld 8336 |
. . . . 5
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ (π¦ β (π΄[,]π΅) β§ π₯ < π¦)) β -(πΉβπ¦) β β) |
70 | 8, 66, 68, 69 | fvmptd3 5609 |
. . . 4
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ (π¦ β (π΄[,]π΅) β§ π₯ < π¦)) β ((π€ β π· β¦ -(πΉβπ€))βπ¦) = -(πΉβπ¦)) |
71 | 61, 64, 70 | 3brtr4d 4035 |
. . 3
β’ (((π β§ π₯ β (π΄[,]π΅)) β§ (π¦ β (π΄[,]π΅) β§ π₯ < π¦)) β ((π€ β π· β¦ -(πΉβπ€))βπ₯) < ((π€ β π· β¦ -(πΉβπ€))βπ¦)) |
72 | 1, 2, 4, 5, 6, 10,
17, 51, 71 | ivthinc 14091 |
. 2
β’ (π β βπ β (π΄(,)π΅)((π€ β π· β¦ -(πΉβπ€))βπ) = -π) |
73 | | fveq2 5515 |
. . . . . . 7
β’ (π€ = π β (πΉβπ€) = (πΉβπ)) |
74 | 73 | negeqd 8151 |
. . . . . 6
β’ (π€ = π β -(πΉβπ€) = -(πΉβπ)) |
75 | | ioossicc 9958 |
. . . . . . . 8
β’ (π΄(,)π΅) β (π΄[,]π΅) |
76 | 75, 6 | sstrid 3166 |
. . . . . . 7
β’ (π β (π΄(,)π΅) β π·) |
77 | 76 | sselda 3155 |
. . . . . 6
β’ ((π β§ π β (π΄(,)π΅)) β π β π·) |
78 | | fveq2 5515 |
. . . . . . . . 9
β’ (π₯ = π β (πΉβπ₯) = (πΉβπ)) |
79 | 78 | eleq1d 2246 |
. . . . . . . 8
β’ (π₯ = π β ((πΉβπ₯) β β β (πΉβπ) β β)) |
80 | 28 | adantr 276 |
. . . . . . . 8
β’ ((π β§ π β (π΄(,)π΅)) β βπ₯ β (π΄[,]π΅)(πΉβπ₯) β β) |
81 | 75 | sseli 3151 |
. . . . . . . . 9
β’ (π β (π΄(,)π΅) β π β (π΄[,]π΅)) |
82 | 81 | adantl 277 |
. . . . . . . 8
β’ ((π β§ π β (π΄(,)π΅)) β π β (π΄[,]π΅)) |
83 | 79, 80, 82 | rspcdva 2846 |
. . . . . . 7
β’ ((π β§ π β (π΄(,)π΅)) β (πΉβπ) β β) |
84 | 83 | renegcld 8336 |
. . . . . 6
β’ ((π β§ π β (π΄(,)π΅)) β -(πΉβπ) β β) |
85 | 8, 74, 77, 84 | fvmptd3 5609 |
. . . . 5
β’ ((π β§ π β (π΄(,)π΅)) β ((π€ β π· β¦ -(πΉβπ€))βπ) = -(πΉβπ)) |
86 | 85 | eqeq1d 2186 |
. . . 4
β’ ((π β§ π β (π΄(,)π΅)) β (((π€ β π· β¦ -(πΉβπ€))βπ) = -π β -(πΉβπ) = -π)) |
87 | | cncff 14034 |
. . . . . . . 8
β’ (πΉ β (π·βcnββ) β πΉ:π·βΆβ) |
88 | 7, 87 | syl 14 |
. . . . . . 7
β’ (π β πΉ:π·βΆβ) |
89 | 88 | ffvelcdmda 5651 |
. . . . . 6
β’ ((π β§ π β π·) β (πΉβπ) β β) |
90 | 77, 89 | syldan 282 |
. . . . 5
β’ ((π β§ π β (π΄(,)π΅)) β (πΉβπ) β β) |
91 | 3 | recnd 7985 |
. . . . . 6
β’ (π β π β β) |
92 | 91 | adantr 276 |
. . . . 5
β’ ((π β§ π β (π΄(,)π΅)) β π β β) |
93 | 90, 92 | neg11ad 8263 |
. . . 4
β’ ((π β§ π β (π΄(,)π΅)) β (-(πΉβπ) = -π β (πΉβπ) = π)) |
94 | 86, 93 | bitrd 188 |
. . 3
β’ ((π β§ π β (π΄(,)π΅)) β (((π€ β π· β¦ -(πΉβπ€))βπ) = -π β (πΉβπ) = π)) |
95 | 94 | rexbidva 2474 |
. 2
β’ (π β (βπ β (π΄(,)π΅)((π€ β π· β¦ -(πΉβπ€))βπ) = -π β βπ β (π΄(,)π΅)(πΉβπ) = π)) |
96 | 72, 95 | mpbid 147 |
1
β’ (π β βπ β (π΄(,)π΅)(πΉβπ) = π) |