Metamath Proof Explorer


Theorem icoiccdif

Description: Left-closed right-open interval gotten by a closed iterval taking away the upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion icoiccdif A * B * A B = A B B

Proof

Step Hyp Ref Expression
1 icossicc A B A B
2 1 a1i A * B * A B A B
3 2 sselda A * B * x A B x A B
4 elico1 A * B * x A B x * A x x < B
5 4 biimpa A * B * x A B x * A x x < B
6 5 simp1d A * B * x A B x *
7 simplr A * B * x A B B *
8 5 simp3d A * B * x A B x < B
9 xrltne x * B * x < B B x
10 6 7 8 9 syl3anc A * B * x A B B x
11 10 necomd A * B * x A B x B
12 11 neneqd A * B * x A B ¬ x = B
13 velsn x B x = B
14 12 13 sylnibr A * B * x A B ¬ x B
15 3 14 eldifd A * B * x A B x A B B
16 15 ex A * B * x A B x A B B
17 16 ssrdv A * B * A B A B B
18 simpll A * B * x A B B A *
19 simplr A * B * x A B B B *
20 eldifi x A B B x A B
21 eliccxr x A B x *
22 20 21 syl x A B B x *
23 22 adantl A * B * x A B B x *
24 20 adantl A * B * x A B B x A B
25 elicc1 A * B * x A B x * A x x B
26 25 adantr A * B * x A B B x A B x * A x x B
27 24 26 mpbid A * B * x A B B x * A x x B
28 27 simp2d A * B * x A B B A x
29 eldifsni x A B B x B
30 29 necomd x A B B B x
31 30 adantl A * B * x A B B B x
32 27 simp3d A * B * x A B B x B
33 xrleltne x * B * x B x < B B x
34 23 19 32 33 syl3anc A * B * x A B B x < B B x
35 31 34 mpbird A * B * x A B B x < B
36 18 19 23 28 35 elicod A * B * x A B B x A B
37 17 36 eqelssd A * B * A B = A B B