Metamath Proof Explorer

Theorem reorelicc

Description: Membership in and outside of a closed real interval. (Contributed by AV, 15-Feb-2023)

Ref Expression
Assertion reorelicc ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 < 𝐴 ∨ 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ∨ 𝐵 < 𝐶 ) )

Proof

Step Hyp Ref Expression
1 orc ⊢ ( 𝐶 < 𝐴 → ( 𝐶 < 𝐴 ∨ 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ) )
2 1 a1d ⊢ ( 𝐶 < 𝐴 → ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐶 ≤ 𝐵 ) → ( 𝐶 < 𝐴 ∨ 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ) ) )
3 simp3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℝ )
4 3 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐶 ≤ 𝐵 ) ∧ ¬ 𝐶 < 𝐴 ) → 𝐶 ∈ ℝ )
5 lenlt ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ≤ 𝐶 ↔ ¬ 𝐶 < 𝐴 ) )
6 5 biimprd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ¬ 𝐶 < 𝐴 → 𝐴 ≤ 𝐶 ) )
7 6 3adant2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ¬ 𝐶 < 𝐴 → 𝐴 ≤ 𝐶 ) )
8 7 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐶 ≤ 𝐵 ) → ( ¬ 𝐶 < 𝐴 → 𝐴 ≤ 𝐶 ) )
9 8 imp ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐶 ≤ 𝐵 ) ∧ ¬ 𝐶 < 𝐴 ) → 𝐴 ≤ 𝐶 )
10 simplr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐶 ≤ 𝐵 ) ∧ ¬ 𝐶 < 𝐴 ) → 𝐶 ≤ 𝐵 )
11 3simpa ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
12 11 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐶 ≤ 𝐵 ) ∧ ¬ 𝐶 < 𝐴 ) → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
13 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵 ) ) )
14 12 13 syl ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐶 ≤ 𝐵 ) ∧ ¬ 𝐶 < 𝐴 ) → ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵 ) ) )
15 4 9 10 14 mpbir3and ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐶 ≤ 𝐵 ) ∧ ¬ 𝐶 < 𝐴 ) → 𝐶 ∈ ( 𝐴 [,] 𝐵 ) )
16 15 olcd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐶 ≤ 𝐵 ) ∧ ¬ 𝐶 < 𝐴 ) → ( 𝐶 < 𝐴 ∨ 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ) )
17 16 expcom ⊢ ( ¬ 𝐶 < 𝐴 → ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐶 ≤ 𝐵 ) → ( 𝐶 < 𝐴 ∨ 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ) ) )
18 2 17 pm2.61i ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐶 ≤ 𝐵 ) → ( 𝐶 < 𝐴 ∨ 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ) )
19 18 orcd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝐶 ≤ 𝐵 ) → ( ( 𝐶 < 𝐴 ∨ 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ) ∨ 𝐵 < 𝐶 ) )
20 19 ex ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 ≤ 𝐵 → ( ( 𝐶 < 𝐴 ∨ 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ) ∨ 𝐵 < 𝐶 ) ) )
21 olc ⊢ ( 𝐵 < 𝐶 → ( ( 𝐶 < 𝐴 ∨ 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ) ∨ 𝐵 < 𝐶 ) )
22 21 a1i ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 < 𝐶 → ( ( 𝐶 < 𝐴 ∨ 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ) ∨ 𝐵 < 𝐶 ) ) )
23 simp2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℝ )
24 lelttric ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐶 ≤ 𝐵 ∨ 𝐵 < 𝐶 ) )
25 3 23 24 syl2anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 ≤ 𝐵 ∨ 𝐵 < 𝐶 ) )
26 20 22 25 mpjaod ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐶 < 𝐴 ∨ 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ) ∨ 𝐵 < 𝐶 ) )
27 df-3or ⊢ ( ( 𝐶 < 𝐴 ∨ 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ∨ 𝐵 < 𝐶 ) ↔ ( ( 𝐶 < 𝐴 ∨ 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ) ∨ 𝐵 < 𝐶 ) )
28 26 27 sylibr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 < 𝐴 ∨ 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ∨ 𝐵 < 𝐶 ) )