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 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴𝐵 ) → ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ∨ 𝐶 = 𝐵 ) ) )

Proof

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