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 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C < A ∨ C ∈ A B ∨ B < C

Proof

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