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∈AB∨B<C

Proof

Step Hyp Ref Expression
1 orc ⊢C<A→C<A∨C∈AB
2 1 a1d ⊢C<A→A∈ℝ∧B∈ℝ∧C∈ℝ∧C≤B→C<A∨C∈AB
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∈AB↔C∈ℝ∧A≤C∧C≤B
14 12 13 syl ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧C≤B∧¬C<A→C∈AB↔C∈ℝ∧A≤C∧C≤B
15 4 9 10 14 mpbir3and ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧C≤B∧¬C<A→C∈AB
16 15 olcd ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧C≤B∧¬C<A→C<A∨C∈AB
17 16 expcom ⊢¬C<A→A∈ℝ∧B∈ℝ∧C∈ℝ∧C≤B→C<A∨C∈AB
18 2 17 pm2.61i ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧C≤B→C<A∨C∈AB
19 18 orcd ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧C≤B→C<A∨C∈AB∨B<C
20 19 ex ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→C≤B→C<A∨C∈AB∨B<C
21 olc ⊢B<C→C<A∨C∈AB∨B<C
22 21 a1i ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→B<C→C<A∨C∈AB∨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∈AB∨B<C
27 df-3or ⊢C<A∨C∈AB∨B<C↔C<A∨C∈AB∨B<C
28 26 27 sylibr ⊢A∈ℝ∧B∈ℝ∧C∈ℝ→C<A∨C∈AB∨B<C