Step | Hyp | Ref
| Expression |
1 | | nfv 1918 |
. . . . . . . 8
β’
β²ππ |
2 | | nfcv 2904 |
. . . . . . . . 9
β’
β²ππ |
3 | | nfixp1 8862 |
. . . . . . . . 9
β’
β²πXπ β
π ((π΄βπ)[,)(π΅βπ)) |
4 | 2, 3 | nfel 2918 |
. . . . . . . 8
β’
β²π π β Xπ β
π ((π΄βπ)[,)(π΅βπ)) |
5 | 1, 4 | nfan 1903 |
. . . . . . 7
β’
β²π(π β§ π β Xπ β π ((π΄βπ)[,)(π΅βπ))) |
6 | | ixpfn 8847 |
. . . . . . . . . . . . 13
β’ (π β Xπ β
π ((π΄βπ)[,)(π΅βπ)) β π Fn π) |
7 | 6 | ad2antlr 726 |
. . . . . . . . . . . 12
β’ (((π β§ π β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β π) β π Fn π) |
8 | | fveq2 6846 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (π΅βπ) = (π΅βπ)) |
9 | 8 | oveq2d 7377 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (-β(,)(π΅βπ)) = (-β(,)(π΅βπ))) |
10 | | iftrue 4496 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β if(π = π, (-β(,)(π΅βπ)), β) = (-β(,)(π΅βπ))) |
11 | 9, 10 | eqtr4d 2776 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (-β(,)(π΅βπ)) = if(π = π, (-β(,)(π΅βπ)), β)) |
12 | | eqimss 4004 |
. . . . . . . . . . . . . . . . 17
β’
((-β(,)(π΅βπ)) = if(π = π, (-β(,)(π΅βπ)), β) β (-β(,)(π΅βπ)) β if(π = π, (-β(,)(π΅βπ)), β)) |
13 | 11, 12 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (-β(,)(π΅βπ)) β if(π = π, (-β(,)(π΅βπ)), β)) |
14 | | ioossre 13334 |
. . . . . . . . . . . . . . . . 17
β’
(-β(,)(π΅βπ)) β β |
15 | | iffalse 4499 |
. . . . . . . . . . . . . . . . 17
β’ (Β¬
π = π β if(π = π, (-β(,)(π΅βπ)), β) = β) |
16 | 14, 15 | sseqtrrid 4001 |
. . . . . . . . . . . . . . . 16
β’ (Β¬
π = π β (-β(,)(π΅βπ)) β if(π = π, (-β(,)(π΅βπ)), β)) |
17 | 13, 16 | pm2.61i 182 |
. . . . . . . . . . . . . . 15
β’
(-β(,)(π΅βπ)) β if(π = π, (-β(,)(π΅βπ)), β) |
18 | | mnfxr 11220 |
. . . . . . . . . . . . . . . . 17
β’ -β
β β* |
19 | 18 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β π) β -β β
β*) |
20 | | hspdifhsp.b |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π΅:πβΆβ) |
21 | 20 | ffvelcdmda 7039 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β π) β (π΅βπ) β β) |
22 | 21 | rexrd 11213 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β π) β (π΅βπ) β
β*) |
23 | 22 | adantlr 714 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β π) β (π΅βπ) β
β*) |
24 | | hspdifhsp.a |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π΄:πβΆβ) |
25 | 24 | ffvelcdmda 7039 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β π) β (π΄βπ) β β) |
26 | | icossre 13354 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π΄βπ) β β β§ (π΅βπ) β β*) β ((π΄βπ)[,)(π΅βπ)) β β) |
27 | 25, 22, 26 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β π) β ((π΄βπ)[,)(π΅βπ)) β β) |
28 | 27 | adantlr 714 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β π) β ((π΄βπ)[,)(π΅βπ)) β β) |
29 | | simpl 484 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β Xπ β
π ((π΄βπ)[,)(π΅βπ)) β§ π β π) β π β Xπ β π ((π΄βπ)[,)(π΅βπ))) |
30 | | simpr 486 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β Xπ β
π ((π΄βπ)[,)(π΅βπ)) β§ π β π) β π β π) |
31 | | fveq2 6846 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β (π΄βπ) = (π΄βπ)) |
32 | | fveq2 6846 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β (π΅βπ) = (π΅βπ)) |
33 | 31, 32 | oveq12d 7379 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β ((π΄βπ)[,)(π΅βπ)) = ((π΄βπ)[,)(π΅βπ))) |
34 | 33 | fvixp 8846 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β Xπ β
π ((π΄βπ)[,)(π΅βπ)) β§ π β π) β (πβπ) β ((π΄βπ)[,)(π΅βπ))) |
35 | 29, 30, 34 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β Xπ β
π ((π΄βπ)[,)(π΅βπ)) β§ π β π) β (πβπ) β ((π΄βπ)[,)(π΅βπ))) |
36 | 35 | adantll 713 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β π) β (πβπ) β ((π΄βπ)[,)(π΅βπ))) |
37 | 28, 36 | sseldd 3949 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β π) β (πβπ) β β) |
38 | 37 | mnfltd 13053 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β π) β -β < (πβπ)) |
39 | 25 | rexrd 11213 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β π) β (π΄βπ) β
β*) |
40 | 39 | adantlr 714 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β π) β (π΄βπ) β
β*) |
41 | | icoltub 43836 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄βπ) β β* β§ (π΅βπ) β β* β§ (πβπ) β ((π΄βπ)[,)(π΅βπ))) β (πβπ) < (π΅βπ)) |
42 | 40, 23, 36, 41 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β π) β (πβπ) < (π΅βπ)) |
43 | 19, 23, 37, 38, 42 | eliood 43826 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β π) β (πβπ) β (-β(,)(π΅βπ))) |
44 | 17, 43 | sselid 3946 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β π) β (πβπ) β if(π = π, (-β(,)(π΅βπ)), β)) |
45 | 44 | adantlr 714 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β π) β§ π β π) β (πβπ) β if(π = π, (-β(,)(π΅βπ)), β)) |
46 | 45 | ralrimiva 3140 |
. . . . . . . . . . . 12
β’ (((π β§ π β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β π) β βπ β π (πβπ) β if(π = π, (-β(,)(π΅βπ)), β)) |
47 | 7, 46 | jca 513 |
. . . . . . . . . . 11
β’ (((π β§ π β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β π) β (π Fn π β§ βπ β π (πβπ) β if(π = π, (-β(,)(π΅βπ)), β))) |
48 | | vex 3451 |
. . . . . . . . . . . 12
β’ π β V |
49 | 48 | elixp 8848 |
. . . . . . . . . . 11
β’ (π β Xπ β
π if(π = π, (-β(,)(π΅βπ)), β) β (π Fn π β§ βπ β π (πβπ) β if(π = π, (-β(,)(π΅βπ)), β))) |
50 | 47, 49 | sylibr 233 |
. . . . . . . . . 10
β’ (((π β§ π β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β π) β π β Xπ β π if(π = π, (-β(,)(π΅βπ)), β)) |
51 | | hspdifhsp.h |
. . . . . . . . . . . . 13
β’ π» = (π₯ β Fin β¦ (π β π₯, π¦ β β β¦ Xπ β
π₯ if(π = π, (-β(,)π¦), β))) |
52 | | equequ1 2029 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (π = π β π = π)) |
53 | 52 | ifbid 4513 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β if(π = π, (-β(,)π¦), β) = if(π = π, (-β(,)π¦), β)) |
54 | 53 | cbvixpv 8859 |
. . . . . . . . . . . . . . . 16
β’ Xπ β
π₯ if(π = π, (-β(,)π¦), β) = Xπ β π₯ if(π = π, (-β(,)π¦), β) |
55 | 54 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π β π₯ β§ π¦ β β) β Xπ β
π₯ if(π = π, (-β(,)π¦), β) = Xπ β π₯ if(π = π, (-β(,)π¦), β)) |
56 | 55 | mpoeq3ia 7439 |
. . . . . . . . . . . . . 14
β’ (π β π₯, π¦ β β β¦ Xπ β
π₯ if(π = π, (-β(,)π¦), β)) = (π β π₯, π¦ β β β¦ Xπ β
π₯ if(π = π, (-β(,)π¦), β)) |
57 | 56 | mpteq2i 5214 |
. . . . . . . . . . . . 13
β’ (π₯ β Fin β¦ (π β π₯, π¦ β β β¦ Xπ β
π₯ if(π = π, (-β(,)π¦), β))) = (π₯ β Fin β¦ (π β π₯, π¦ β β β¦ Xπ β
π₯ if(π = π, (-β(,)π¦), β))) |
58 | 51, 57 | eqtri 2761 |
. . . . . . . . . . . 12
β’ π» = (π₯ β Fin β¦ (π β π₯, π¦ β β β¦ Xπ β
π₯ if(π = π, (-β(,)π¦), β))) |
59 | | hspdifhsp.x |
. . . . . . . . . . . . 13
β’ (π β π β Fin) |
60 | 59 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β π β Fin) |
61 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β π β π) |
62 | 20 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β π΅:πβΆβ) |
63 | 62, 61 | ffvelcdmd 7040 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β (π΅βπ) β β) |
64 | 58, 60, 61, 63 | hspval 44940 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (π(π»βπ)(π΅βπ)) = Xπ β π if(π = π, (-β(,)(π΅βπ)), β)) |
65 | 64 | adantlr 714 |
. . . . . . . . . 10
β’ (((π β§ π β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β π) β (π(π»βπ)(π΅βπ)) = Xπ β π if(π = π, (-β(,)(π΅βπ)), β)) |
66 | 50, 65 | eleqtrrd 2837 |
. . . . . . . . 9
β’ (((π β§ π β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β π) β π β (π(π»βπ)(π΅βπ))) |
67 | 18 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ π β (π(π»βπ)(π΄βπ))) β -β β
β*) |
68 | 24 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π) β π΄:πβΆβ) |
69 | 68, 61 | ffvelcdmd 7040 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π) β (π΄βπ) β β) |
70 | 69 | rexrd 11213 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β (π΄βπ) β
β*) |
71 | 70 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ π β (π(π»βπ)(π΄βπ))) β (π΄βπ) β
β*) |
72 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π) β§ π β (π(π»βπ)(π΄βπ))) β π β (π(π»βπ)(π΄βπ))) |
73 | 58, 60, 61, 69 | hspval 44940 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π) β (π(π»βπ)(π΄βπ)) = Xπ β π if(π = π, (-β(,)(π΄βπ)), β)) |
74 | 73 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π) β§ π β (π(π»βπ)(π΄βπ))) β (π(π»βπ)(π΄βπ)) = Xπ β π if(π = π, (-β(,)(π΄βπ)), β)) |
75 | 72, 74 | eleqtrd 2836 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π) β§ π β (π(π»βπ)(π΄βπ))) β π β Xπ β π if(π = π, (-β(,)(π΄βπ)), β)) |
76 | 61 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π) β§ π β (π(π»βπ)(π΄βπ))) β π β π) |
77 | | iftrue 4496 |
. . . . . . . . . . . . . 14
β’ (π = π β if(π = π, (-β(,)(π΄βπ)), β) = (-β(,)(π΄βπ))) |
78 | 77 | fvixp 8846 |
. . . . . . . . . . . . 13
β’ ((π β Xπ β
π if(π = π, (-β(,)(π΄βπ)), β) β§ π β π) β (πβπ) β (-β(,)(π΄βπ))) |
79 | 75, 76, 78 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ π β (π(π»βπ)(π΄βπ))) β (πβπ) β (-β(,)(π΄βπ))) |
80 | | iooltub 43838 |
. . . . . . . . . . . 12
β’
((-β β β* β§ (π΄βπ) β β* β§ (πβπ) β (-β(,)(π΄βπ))) β (πβπ) < (π΄βπ)) |
81 | 67, 71, 79, 80 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ π β (π(π»βπ)(π΄βπ))) β (πβπ) < (π΄βπ)) |
82 | 81 | adantllr 718 |
. . . . . . . . . 10
β’ ((((π β§ π β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β π) β§ π β (π(π»βπ)(π΄βπ))) β (πβπ) < (π΄βπ)) |
83 | 70 | adantlr 714 |
. . . . . . . . . . . . 13
β’ (((π β§ π β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β π) β (π΄βπ) β
β*) |
84 | 63 | rexrd 11213 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π) β (π΅βπ) β
β*) |
85 | 84 | adantlr 714 |
. . . . . . . . . . . . 13
β’ (((π β§ π β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β π) β (π΅βπ) β
β*) |
86 | 48 | elixp 8848 |
. . . . . . . . . . . . . . . . 17
β’ (π β Xπ β
π ((π΄βπ)[,)(π΅βπ)) β (π Fn π β§ βπ β π (πβπ) β ((π΄βπ)[,)(π΅βπ)))) |
87 | 86 | biimpi 215 |
. . . . . . . . . . . . . . . 16
β’ (π β Xπ β
π ((π΄βπ)[,)(π΅βπ)) β (π Fn π β§ βπ β π (πβπ) β ((π΄βπ)[,)(π΅βπ)))) |
88 | 87 | simprd 497 |
. . . . . . . . . . . . . . 15
β’ (π β Xπ β
π ((π΄βπ)[,)(π΅βπ)) β βπ β π (πβπ) β ((π΄βπ)[,)(π΅βπ))) |
89 | | rspa 3230 |
. . . . . . . . . . . . . . 15
β’
((βπ β
π (πβπ) β ((π΄βπ)[,)(π΅βπ)) β§ π β π) β (πβπ) β ((π΄βπ)[,)(π΅βπ))) |
90 | 88, 89 | sylan 581 |
. . . . . . . . . . . . . 14
β’ ((π β Xπ β
π ((π΄βπ)[,)(π΅βπ)) β§ π β π) β (πβπ) β ((π΄βπ)[,)(π΅βπ))) |
91 | 90 | adantll 713 |
. . . . . . . . . . . . 13
β’ (((π β§ π β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β π) β (πβπ) β ((π΄βπ)[,)(π΅βπ))) |
92 | | icogelb 13324 |
. . . . . . . . . . . . 13
β’ (((π΄βπ) β β* β§ (π΅βπ) β β* β§ (πβπ) β ((π΄βπ)[,)(π΅βπ))) β (π΄βπ) β€ (πβπ)) |
93 | 83, 85, 91, 92 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (((π β§ π β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β π) β (π΄βπ) β€ (πβπ)) |
94 | 69 | adantlr 714 |
. . . . . . . . . . . . 13
β’ (((π β§ π β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β π) β (π΄βπ) β β) |
95 | | icossre 13354 |
. . . . . . . . . . . . . . . 16
β’ (((π΄βπ) β β β§ (π΅βπ) β β*) β ((π΄βπ)[,)(π΅βπ)) β β) |
96 | 69, 84, 95 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π) β ((π΄βπ)[,)(π΅βπ)) β β) |
97 | 96 | adantlr 714 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β π) β ((π΄βπ)[,)(π΅βπ)) β β) |
98 | 97, 91 | sseldd 3949 |
. . . . . . . . . . . . 13
β’ (((π β§ π β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β π) β (πβπ) β β) |
99 | 94, 98 | lenltd 11309 |
. . . . . . . . . . . 12
β’ (((π β§ π β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β π) β ((π΄βπ) β€ (πβπ) β Β¬ (πβπ) < (π΄βπ))) |
100 | 93, 99 | mpbid 231 |
. . . . . . . . . . 11
β’ (((π β§ π β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β π) β Β¬ (πβπ) < (π΄βπ)) |
101 | 100 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β§ π β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β π) β§ π β (π(π»βπ)(π΄βπ))) β Β¬ (πβπ) < (π΄βπ)) |
102 | 82, 101 | pm2.65da 816 |
. . . . . . . . 9
β’ (((π β§ π β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β π) β Β¬ π β (π(π»βπ)(π΄βπ))) |
103 | 66, 102 | eldifd 3925 |
. . . . . . . 8
β’ (((π β§ π β Xπ β π ((π΄βπ)[,)(π΅βπ))) β§ π β π) β π β ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) |
104 | 103 | ex 414 |
. . . . . . 7
β’ ((π β§ π β Xπ β π ((π΄βπ)[,)(π΅βπ))) β (π β π β π β ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ))))) |
105 | 5, 104 | ralrimi 3239 |
. . . . . 6
β’ ((π β§ π β Xπ β π ((π΄βπ)[,)(π΅βπ))) β βπ β π π β ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) |
106 | | eliin 4963 |
. . . . . . 7
β’ (π β V β (π β β© π β π ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ))) β βπ β π π β ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ))))) |
107 | 48, 106 | ax-mp 5 |
. . . . . 6
β’ (π β β© π β π ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ))) β βπ β π π β ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) |
108 | 105, 107 | sylibr 233 |
. . . . 5
β’ ((π β§ π β Xπ β π ((π΄βπ)[,)(π΅βπ))) β π β β©
π β π ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) |
109 | 108 | ex 414 |
. . . 4
β’ (π β (π β Xπ β π ((π΄βπ)[,)(π΅βπ)) β π β β©
π β π ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ))))) |
110 | | hspdifhsp.n |
. . . . . . . . . 10
β’ (π β π β β
) |
111 | | n0 4310 |
. . . . . . . . . . 11
β’ (π β β
β
βπ π β π) |
112 | 111 | biimpi 215 |
. . . . . . . . . 10
β’ (π β β
β
βπ π β π) |
113 | 110, 112 | syl 17 |
. . . . . . . . 9
β’ (π β βπ π β π) |
114 | 113 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β β©
π β π ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) β βπ π β π) |
115 | | simpl 484 |
. . . . . . . . . . . . . . 15
β’ ((π β β© π β π ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ))) β§ π β π) β π β β©
π β π ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) |
116 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ ((π β β© π β π ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ))) β§ π β π) β π β π) |
117 | | id 22 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β π = π) |
118 | 117, 32 | oveq12d 7379 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (π(π»βπ)(π΅βπ)) = (π(π»βπ)(π΅βπ))) |
119 | 117, 31 | oveq12d 7379 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (π(π»βπ)(π΄βπ)) = (π(π»βπ)(π΄βπ))) |
120 | 118, 119 | difeq12d 4087 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ))) = ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) |
121 | 120 | eleq2d 2820 |
. . . . . . . . . . . . . . 15
β’ (π = π β (π β ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ))) β π β ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ))))) |
122 | 115, 116,
121 | eliind 43371 |
. . . . . . . . . . . . . 14
β’ ((π β β© π β π ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ))) β§ π β π) β π β ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) |
123 | 122 | eldifad 3926 |
. . . . . . . . . . . . 13
β’ ((π β β© π β π ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ))) β§ π β π) β π β (π(π»βπ)(π΅βπ))) |
124 | 123 | adantll 713 |
. . . . . . . . . . . 12
β’ (((π β§ π β β©
π β π ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) β§ π β π) β π β (π(π»βπ)(π΅βπ))) |
125 | | equequ1 2029 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = β β (π = π β β = π)) |
126 | 125 | ifbid 4513 |
. . . . . . . . . . . . . . . . . 18
β’ (π = β β if(π = π, (-β(,)π¦), β) = if(β = π, (-β(,)π¦), β)) |
127 | 126 | cbvixpv 8859 |
. . . . . . . . . . . . . . . . 17
β’ Xπ β
π₯ if(π = π, (-β(,)π¦), β) = Xβ β π₯ if(β = π, (-β(,)π¦), β) |
128 | 127 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((π β π₯ β§ π¦ β β) β Xπ β
π₯ if(π = π, (-β(,)π¦), β) = Xβ β π₯ if(β = π, (-β(,)π¦), β)) |
129 | 128 | mpoeq3ia 7439 |
. . . . . . . . . . . . . . 15
β’ (π β π₯, π¦ β β β¦ Xπ β
π₯ if(π = π, (-β(,)π¦), β)) = (π β π₯, π¦ β β β¦ Xβ β
π₯ if(β = π, (-β(,)π¦), β)) |
130 | 129 | mpteq2i 5214 |
. . . . . . . . . . . . . 14
β’ (π₯ β Fin β¦ (π β π₯, π¦ β β β¦ Xπ β
π₯ if(π = π, (-β(,)π¦), β))) = (π₯ β Fin β¦ (π β π₯, π¦ β β β¦ Xβ β
π₯ if(β = π, (-β(,)π¦), β))) |
131 | 51, 130 | eqtri 2761 |
. . . . . . . . . . . . 13
β’ π» = (π₯ β Fin β¦ (π β π₯, π¦ β β β¦ Xβ β
π₯ if(β = π, (-β(,)π¦), β))) |
132 | 59 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β©
π β π ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) β§ π β π) β π β Fin) |
133 | | simpr 486 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β©
π β π ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) β§ π β π) β π β π) |
134 | 21 | adantlr 714 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β©
π β π ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) β§ π β π) β (π΅βπ) β β) |
135 | 131, 132,
133, 134 | hspval 44940 |
. . . . . . . . . . . 12
β’ (((π β§ π β β©
π β π ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) β§ π β π) β (π(π»βπ)(π΅βπ)) = Xβ β π if(β = π, (-β(,)(π΅βπ)), β)) |
136 | 124, 135 | eleqtrd 2836 |
. . . . . . . . . . 11
β’ (((π β§ π β β©
π β π ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) β§ π β π) β π β Xβ β π if(β = π, (-β(,)(π΅βπ)), β)) |
137 | | ixpfn 8847 |
. . . . . . . . . . 11
β’ (π β Xβ β
π if(β = π, (-β(,)(π΅βπ)), β) β π Fn π) |
138 | 136, 137 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π β β©
π β π ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) β§ π β π) β π Fn π) |
139 | 138 | ex 414 |
. . . . . . . . 9
β’ ((π β§ π β β©
π β π ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) β (π β π β π Fn π)) |
140 | 139 | exlimdv 1937 |
. . . . . . . 8
β’ ((π β§ π β β©
π β π ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) β (βπ π β π β π Fn π)) |
141 | 114, 140 | mpd 15 |
. . . . . . 7
β’ ((π β§ π β β©
π β π ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) β π Fn π) |
142 | | nfii1 4993 |
. . . . . . . . . 10
β’
β²πβ© π β π ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ))) |
143 | 2, 142 | nfel 2918 |
. . . . . . . . 9
β’
β²π π β β© π β π ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ))) |
144 | 1, 143 | nfan 1903 |
. . . . . . . 8
β’
β²π(π β§ π β β©
π β π ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) |
145 | | simpll 766 |
. . . . . . . . . 10
β’ (((π β§ π β β©
π β π ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) β§ π β π) β π) |
146 | 107 | biimpi 215 |
. . . . . . . . . . . . 13
β’ (π β β© π β π ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ))) β βπ β π π β ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) |
147 | 146 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β β© π β π ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ))) β§ π β π) β βπ β π π β ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) |
148 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π β β© π β π ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ))) β§ π β π) β π β π) |
149 | | rspa 3230 |
. . . . . . . . . . . 12
β’
((βπ β
π π β ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ))) β§ π β π) β π β ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) |
150 | 147, 148,
149 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π β β© π β π ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ))) β§ π β π) β π β ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) |
151 | 150 | adantll 713 |
. . . . . . . . . 10
β’ (((π β§ π β β©
π β π ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) β§ π β π) β π β ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) |
152 | | simpr 486 |
. . . . . . . . . 10
β’ (((π β§ π β β©
π β π ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) β§ π β π) β π β π) |
153 | 70 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ π β ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) β§ π β π) β (π΄βπ) β
β*) |
154 | 84 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ π β ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) β§ π β π) β (π΅βπ) β
β*) |
155 | | simpll 766 |
. . . . . . . . . . . . 13
β’ (((π β§ π β ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) β§ π β π) β π) |
156 | | eldifi 4090 |
. . . . . . . . . . . . . 14
β’ (π β ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ))) β π β (π(π»βπ)(π΅βπ))) |
157 | 156 | ad2antlr 726 |
. . . . . . . . . . . . 13
β’ (((π β§ π β ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) β§ π β π) β π β (π(π»βπ)(π΅βπ))) |
158 | | simpr 486 |
. . . . . . . . . . . . 13
β’ (((π β§ π β ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) β§ π β π) β π β π) |
159 | | ioossre 13334 |
. . . . . . . . . . . . . 14
β’
(-β(,)(π΅βπ)) β β |
160 | | simplr 768 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (π(π»βπ)(π΅βπ))) β§ π β π) β π β (π(π»βπ)(π΅βπ))) |
161 | 64 | adantlr 714 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (π(π»βπ)(π΅βπ))) β§ π β π) β (π(π»βπ)(π΅βπ)) = Xπ β π if(π = π, (-β(,)(π΅βπ)), β)) |
162 | 160, 161 | eleqtrd 2836 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (π(π»βπ)(π΅βπ))) β§ π β π) β π β Xπ β π if(π = π, (-β(,)(π΅βπ)), β)) |
163 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (π(π»βπ)(π΅βπ))) β§ π β π) β π β π) |
164 | 10 | fvixp 8846 |
. . . . . . . . . . . . . . 15
β’ ((π β Xπ β
π if(π = π, (-β(,)(π΅βπ)), β) β§ π β π) β (πβπ) β (-β(,)(π΅βπ))) |
165 | 162, 163,
164 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (π(π»βπ)(π΅βπ))) β§ π β π) β (πβπ) β (-β(,)(π΅βπ))) |
166 | 159, 165 | sselid 3946 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (π(π»βπ)(π΅βπ))) β§ π β π) β (πβπ) β β) |
167 | 155, 157,
158, 166 | syl21anc 837 |
. . . . . . . . . . . 12
β’ (((π β§ π β ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) β§ π β π) β (πβπ) β β) |
168 | 167 | rexrd 11213 |
. . . . . . . . . . 11
β’ (((π β§ π β ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) β§ π β π) β (πβπ) β
β*) |
169 | | simpl 484 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) β π) |
170 | 156 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) β π β (π(π»βπ)(π΅βπ))) |
171 | 169, 170 | jca 513 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) β (π β§ π β (π(π»βπ)(π΅βπ)))) |
172 | 171 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) β§ π β π) β§ (πβπ) < (π΄βπ)) β (π β§ π β (π(π»βπ)(π΅βπ)))) |
173 | | simplr 768 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) β§ π β π) β§ (πβπ) < (π΄βπ)) β π β π) |
174 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) β§ π β π) β§ (πβπ) < (π΄βπ)) β (πβπ) < (π΄βπ)) |
175 | | ixpfn 8847 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β Xπ β
π if(π = π, (-β(,)(π΅βπ)), β) β π Fn π) |
176 | 162, 175 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (π(π»βπ)(π΅βπ))) β§ π β π) β π Fn π) |
177 | 176 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β (π(π»βπ)(π΅βπ))) β§ π β π) β§ (πβπ) < (π΄βπ)) β π Fn π) |
178 | | fveq2 6846 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π β (πβπ) = (πβπ)) |
179 | 178 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ π β (π(π»βπ)(π΅βπ))) β§ π β π) β§ (πβπ) < (π΄βπ)) β§ π = π) β (πβπ) = (πβπ)) |
180 | 18 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π β (π(π»βπ)(π΅βπ))) β§ π β π) β§ (πβπ) < (π΄βπ)) β -β β
β*) |
181 | 70 | ad4ant13 750 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π β (π(π»βπ)(π΅βπ))) β§ π β π) β§ (πβπ) < (π΄βπ)) β (π΄βπ) β
β*) |
182 | 166 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π β (π(π»βπ)(π΅βπ))) β§ π β π) β§ (πβπ) < (π΄βπ)) β (πβπ) β β) |
183 | 182 | mnfltd 13053 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π β (π(π»βπ)(π΅βπ))) β§ π β π) β§ (πβπ) < (π΄βπ)) β -β < (πβπ)) |
184 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π β (π(π»βπ)(π΅βπ))) β§ π β π) β§ (πβπ) < (π΄βπ)) β (πβπ) < (π΄βπ)) |
185 | 180, 181,
182, 183, 184 | eliood 43826 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π β (π(π»βπ)(π΅βπ))) β§ π β π) β§ (πβπ) < (π΄βπ)) β (πβπ) β (-β(,)(π΄βπ))) |
186 | 185 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ π β (π(π»βπ)(π΅βπ))) β§ π β π) β§ (πβπ) < (π΄βπ)) β§ π = π) β (πβπ) β (-β(,)(π΄βπ))) |
187 | 179, 186 | eqeltrd 2834 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ π β (π(π»βπ)(π΅βπ))) β§ π β π) β§ (πβπ) < (π΄βπ)) β§ π = π) β (πβπ) β (-β(,)(π΄βπ))) |
188 | 187 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π β§ π β (π(π»βπ)(π΅βπ))) β§ π β π) β§ (πβπ) < (π΄βπ)) β§ π β π) β§ π = π) β (πβπ) β (-β(,)(π΄βπ))) |
189 | 77 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β (-β(,)(π΄βπ)) = if(π = π, (-β(,)(π΄βπ)), β)) |
190 | 189 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π β§ π β (π(π»βπ)(π΅βπ))) β§ π β π) β§ (πβπ) < (π΄βπ)) β§ π β π) β§ π = π) β (-β(,)(π΄βπ)) = if(π = π, (-β(,)(π΄βπ)), β)) |
191 | 188, 190 | eleqtrd 2836 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π β§ π β (π(π»βπ)(π΅βπ))) β§ π β π) β§ (πβπ) < (π΄βπ)) β§ π β π) β§ π = π) β (πβπ) β if(π = π, (-β(,)(π΄βπ)), β)) |
192 | 10, 159 | eqsstrdi 4002 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = π β if(π = π, (-β(,)(π΅βπ)), β) β
β) |
193 | | ssid 3970 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ β
β β |
194 | 15, 193 | eqsstrdi 4002 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (Β¬
π = π β if(π = π, (-β(,)(π΅βπ)), β) β
β) |
195 | 192, 194 | pm2.61i 182 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ if(π = π, (-β(,)(π΅βπ)), β) β β |
196 | 162 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π β (π(π»βπ)(π΅βπ))) β§ π β π) β§ π β π) β π β Xπ β π if(π = π, (-β(,)(π΅βπ)), β)) |
197 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π β (π(π»βπ)(π΅βπ))) β§ π β π) β§ π β π) β π β π) |
198 | | fvixp2 43511 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β Xπ β
π if(π = π, (-β(,)(π΅βπ)), β) β§ π β π) β (πβπ) β if(π = π, (-β(,)(π΅βπ)), β)) |
199 | 196, 197,
198 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π β (π(π»βπ)(π΅βπ))) β§ π β π) β§ π β π) β (πβπ) β if(π = π, (-β(,)(π΅βπ)), β)) |
200 | 195, 199 | sselid 3946 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π β (π(π»βπ)(π΅βπ))) β§ π β π) β§ π β π) β (πβπ) β β) |
201 | 200 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ π β (π(π»βπ)(π΅βπ))) β§ π β π) β§ π β π) β§ Β¬ π = π) β (πβπ) β β) |
202 | | iffalse 4499 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (Β¬
π = π β if(π = π, (-β(,)(π΄βπ)), β) = β) |
203 | 202 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (Β¬
π = π β β = if(π = π, (-β(,)(π΄βπ)), β)) |
204 | 203 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ π β (π(π»βπ)(π΅βπ))) β§ π β π) β§ π β π) β§ Β¬ π = π) β β = if(π = π, (-β(,)(π΄βπ)), β)) |
205 | 201, 204 | eleqtrd 2836 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ π β (π(π»βπ)(π΅βπ))) β§ π β π) β§ π β π) β§ Β¬ π = π) β (πβπ) β if(π = π, (-β(,)(π΄βπ)), β)) |
206 | 205 | adantllr 718 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π β§ π β (π(π»βπ)(π΅βπ))) β§ π β π) β§ (πβπ) < (π΄βπ)) β§ π β π) β§ Β¬ π = π) β (πβπ) β if(π = π, (-β(,)(π΄βπ)), β)) |
207 | 191, 206 | pm2.61dan 812 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π β (π(π»βπ)(π΅βπ))) β§ π β π) β§ (πβπ) < (π΄βπ)) β§ π β π) β (πβπ) β if(π = π, (-β(,)(π΄βπ)), β)) |
208 | 207 | ralrimiva 3140 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β (π(π»βπ)(π΅βπ))) β§ π β π) β§ (πβπ) < (π΄βπ)) β βπ β π (πβπ) β if(π = π, (-β(,)(π΄βπ)), β)) |
209 | 177, 208 | jca 513 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β (π(π»βπ)(π΅βπ))) β§ π β π) β§ (πβπ) < (π΄βπ)) β (π Fn π β§ βπ β π (πβπ) β if(π = π, (-β(,)(π΄βπ)), β))) |
210 | 48 | elixp 8848 |
. . . . . . . . . . . . . . . 16
β’ (π β Xπ β
π if(π = π, (-β(,)(π΄βπ)), β) β (π Fn π β§ βπ β π (πβπ) β if(π = π, (-β(,)(π΄βπ)), β))) |
211 | 209, 210 | sylibr 233 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β (π(π»βπ)(π΅βπ))) β§ π β π) β§ (πβπ) < (π΄βπ)) β π β Xπ β π if(π = π, (-β(,)(π΄βπ)), β)) |
212 | 73 | eqcomd 2739 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π) β Xπ β π if(π = π, (-β(,)(π΄βπ)), β) = (π(π»βπ)(π΄βπ))) |
213 | 212 | ad4ant13 750 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β (π(π»βπ)(π΅βπ))) β§ π β π) β§ (πβπ) < (π΄βπ)) β Xπ β π if(π = π, (-β(,)(π΄βπ)), β) = (π(π»βπ)(π΄βπ))) |
214 | 211, 213 | eleqtrd 2836 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β (π(π»βπ)(π΅βπ))) β§ π β π) β§ (πβπ) < (π΄βπ)) β π β (π(π»βπ)(π΄βπ))) |
215 | 172, 173,
174, 214 | syl21anc 837 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) β§ π β π) β§ (πβπ) < (π΄βπ)) β π β (π(π»βπ)(π΄βπ))) |
216 | | eldifn 4091 |
. . . . . . . . . . . . . 14
β’ (π β ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ))) β Β¬ π β (π(π»βπ)(π΄βπ))) |
217 | 216 | ad3antlr 730 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) β§ π β π) β§ (πβπ) < (π΄βπ)) β Β¬ π β (π(π»βπ)(π΄βπ))) |
218 | 215, 217 | pm2.65da 816 |
. . . . . . . . . . . 12
β’ (((π β§ π β ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) β§ π β π) β Β¬ (πβπ) < (π΄βπ)) |
219 | 155, 158,
69 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π β§ π β ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) β§ π β π) β (π΄βπ) β β) |
220 | 219, 167 | lenltd 11309 |
. . . . . . . . . . . 12
β’ (((π β§ π β ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) β§ π β π) β ((π΄βπ) β€ (πβπ) β Β¬ (πβπ) < (π΄βπ))) |
221 | 218, 220 | mpbird 257 |
. . . . . . . . . . 11
β’ (((π β§ π β ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) β§ π β π) β (π΄βπ) β€ (πβπ)) |
222 | 18 | a1i 11 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (π(π»βπ)(π΅βπ))) β§ π β π) β -β β
β*) |
223 | 84 | adantlr 714 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (π(π»βπ)(π΅βπ))) β§ π β π) β (π΅βπ) β
β*) |
224 | | iooltub 43838 |
. . . . . . . . . . . . 13
β’
((-β β β* β§ (π΅βπ) β β* β§ (πβπ) β (-β(,)(π΅βπ))) β (πβπ) < (π΅βπ)) |
225 | 222, 223,
165, 224 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (((π β§ π β (π(π»βπ)(π΅βπ))) β§ π β π) β (πβπ) < (π΅βπ)) |
226 | 155, 157,
158, 225 | syl21anc 837 |
. . . . . . . . . . 11
β’ (((π β§ π β ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) β§ π β π) β (πβπ) < (π΅βπ)) |
227 | 153, 154,
168, 221, 226 | elicod 13323 |
. . . . . . . . . 10
β’ (((π β§ π β ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) β§ π β π) β (πβπ) β ((π΄βπ)[,)(π΅βπ))) |
228 | 145, 151,
152, 227 | syl21anc 837 |
. . . . . . . . 9
β’ (((π β§ π β β©
π β π ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) β§ π β π) β (πβπ) β ((π΄βπ)[,)(π΅βπ))) |
229 | 228 | ex 414 |
. . . . . . . 8
β’ ((π β§ π β β©
π β π ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) β (π β π β (πβπ) β ((π΄βπ)[,)(π΅βπ)))) |
230 | 144, 229 | ralrimi 3239 |
. . . . . . 7
β’ ((π β§ π β β©
π β π ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) β βπ β π (πβπ) β ((π΄βπ)[,)(π΅βπ))) |
231 | 141, 230 | jca 513 |
. . . . . 6
β’ ((π β§ π β β©
π β π ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) β (π Fn π β§ βπ β π (πβπ) β ((π΄βπ)[,)(π΅βπ)))) |
232 | 231, 86 | sylibr 233 |
. . . . 5
β’ ((π β§ π β β©
π β π ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) β π β Xπ β π ((π΄βπ)[,)(π΅βπ))) |
233 | 232 | ex 414 |
. . . 4
β’ (π β (π β β©
π β π ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ))) β π β Xπ β π ((π΄βπ)[,)(π΅βπ)))) |
234 | 109, 233 | impbid 211 |
. . 3
β’ (π β (π β Xπ β π ((π΄βπ)[,)(π΅βπ)) β π β β©
π β π ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ))))) |
235 | 234 | alrimiv 1931 |
. 2
β’ (π β βπ(π β Xπ β π ((π΄βπ)[,)(π΅βπ)) β π β β©
π β π ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ))))) |
236 | | dfcleq 2726 |
. 2
β’ (Xπ β
π ((π΄βπ)[,)(π΅βπ)) = β©
π β π ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ))) β βπ(π β Xπ β π ((π΄βπ)[,)(π΅βπ)) β π β β©
π β π ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ))))) |
237 | 235, 236 | sylibr 233 |
1
β’ (π β Xπ β
π ((π΄βπ)[,)(π΅βπ)) = β©
π β π ((π(π»βπ)(π΅βπ)) β (π(π»βπ)(π΄βπ)))) |