Metamath Proof Explorer


Theorem eliccelico

Description: Relate elementhood to a closed interval with elementhood to the same closed-below, open-above interval or to its upper bound. (Contributed by Thierry Arnoux, 3-Jul-2017)

Ref Expression
Assertion eliccelico A * B * A B C A B C A B C = B

Proof

Step Hyp Ref Expression
1 simpl1 A * B * A B C A B ¬ C A B A *
2 simpl2 A * B * A B C A B ¬ C A B B *
3 simprl A * B * A B C A B ¬ C A B C A B
4 elicc1 A * B * C A B C * A C C B
5 4 biimpa A * B * C A B C * A C C B
6 5 simp1d A * B * C A B C *
7 1 2 3 6 syl21anc A * B * A B C A B ¬ C A B C *
8 5 simp3d A * B * C A B C B
9 1 2 3 8 syl21anc A * B * A B C A B ¬ C A B C B
10 1 2 jca A * B * A B C A B ¬ C A B A * B *
11 simprr A * B * A B C A B ¬ C A B ¬ C A B
12 5 simp2d A * B * C A B A C
13 10 3 12 syl2anc A * B * A B C A B ¬ C A B A C
14 elico1 A * B * C A B C * A C C < B
15 14 notbid A * B * ¬ C A B ¬ C * A C C < B
16 15 biimpa A * B * ¬ C A B ¬ C * A C C < B
17 df-3an C * A C C < B C * A C C < B
18 17 notbii ¬ C * A C C < B ¬ C * A C C < B
19 imnan C * A C ¬ C < B ¬ C * A C C < B
20 18 19 bitr4i ¬ C * A C C < B C * A C ¬ C < B
21 16 20 sylib A * B * ¬ C A B C * A C ¬ C < B
22 21 imp A * B * ¬ C A B C * A C ¬ C < B
23 10 11 7 13 22 syl22anc A * B * A B C A B ¬ C A B ¬ C < B
24 xeqlelt C * B * C = B C B ¬ C < B
25 24 biimpar C * B * C B ¬ C < B C = B
26 7 2 9 23 25 syl22anc A * B * A B C A B ¬ C A B C = B
27 26 ex A * B * A B C A B ¬ C A B C = B
28 pm5.6 C A B ¬ C A B C = B C A B C A B C = B
29 27 28 sylib A * B * A B C A B C A B C = B
30 icossicc A B A B
31 simpr A * B * A B C A B C A B
32 30 31 sselid A * B * A B C A B C A B
33 simpr A * B * A B C = B C = B
34 simpl2 A * B * A B C = B B *
35 33 34 eqeltrd A * B * A B C = B C *
36 simpl3 A * B * A B C = B A B
37 36 33 breqtrrd A * B * A B C = B A C
38 34 xrleidd A * B * A B C = B B B
39 33 38 eqbrtrd A * B * A B C = B C B
40 simpl1 A * B * A B C = B A *
41 40 34 4 syl2anc A * B * A B C = B C A B C * A C C B
42 35 37 39 41 mpbir3and A * B * A B C = B C A B
43 32 42 jaodan A * B * A B C A B C = B C A B
44 43 ex A * B * A B C A B C = B C A B
45 29 44 impbid A * B * A B C A B C A B C = B