Metamath Proof Explorer

Theorem fzospliti

Description: One direction of splitting a half-open integer range in half. (Contributed by Stefan O'Rear, 14-Aug-2015)

Ref Expression
Assertion fzospliti ⊢ A ∈ B ..^ C ∧ D ∈ ℤ → A ∈ B ..^ D ∨ A ∈ D ..^ C

Proof

Step Hyp Ref Expression
1 zre ⊢ D ∈ ℤ → D ∈ ℝ
2 elfzoelz ⊢ A ∈ B ..^ C → A ∈ ℤ
3 2 adantr ⊢ A ∈ B ..^ C ∧ D ∈ ℤ → A ∈ ℤ
4 3 zred ⊢ A ∈ B ..^ C ∧ D ∈ ℤ → A ∈ ℝ
5 lelttric ⊢ D ∈ ℝ ∧ A ∈ ℝ → D ≤ A ∨ A < D
6 1 4 5 syl2an2 ⊢ A ∈ B ..^ C ∧ D ∈ ℤ → D ≤ A ∨ A < D
7 6 orcomd ⊢ A ∈ B ..^ C ∧ D ∈ ℤ → A < D ∨ D ≤ A
8 elfzole1 ⊢ A ∈ B ..^ C → B ≤ A
9 8 adantr ⊢ A ∈ B ..^ C ∧ D ∈ ℤ → B ≤ A
10 9 a1d ⊢ A ∈ B ..^ C ∧ D ∈ ℤ → A < D → B ≤ A
11 10 ancrd ⊢ A ∈ B ..^ C ∧ D ∈ ℤ → A < D → B ≤ A ∧ A < D
12 elfzolt2 ⊢ A ∈ B ..^ C → A < C
13 12 adantr ⊢ A ∈ B ..^ C ∧ D ∈ ℤ → A < C
14 13 a1d ⊢ A ∈ B ..^ C ∧ D ∈ ℤ → D ≤ A → A < C
15 14 ancld ⊢ A ∈ B ..^ C ∧ D ∈ ℤ → D ≤ A → D ≤ A ∧ A < C
16 11 15 orim12d ⊢ A ∈ B ..^ C ∧ D ∈ ℤ → A < D ∨ D ≤ A → B ≤ A ∧ A < D ∨ D ≤ A ∧ A < C
17 7 16 mpd ⊢ A ∈ B ..^ C ∧ D ∈ ℤ → B ≤ A ∧ A < D ∨ D ≤ A ∧ A < C
18 elfzoel1 ⊢ A ∈ B ..^ C → B ∈ ℤ
19 18 adantr ⊢ A ∈ B ..^ C ∧ D ∈ ℤ → B ∈ ℤ
20 simpr ⊢ A ∈ B ..^ C ∧ D ∈ ℤ → D ∈ ℤ
21 elfzo ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ D ∈ ℤ → A ∈ B ..^ D ↔ B ≤ A ∧ A < D
22 3 19 20 21 syl3anc ⊢ A ∈ B ..^ C ∧ D ∈ ℤ → A ∈ B ..^ D ↔ B ≤ A ∧ A < D
23 elfzoel2 ⊢ A ∈ B ..^ C → C ∈ ℤ
24 23 adantr ⊢ A ∈ B ..^ C ∧ D ∈ ℤ → C ∈ ℤ
25 elfzo ⊢ A ∈ ℤ ∧ D ∈ ℤ ∧ C ∈ ℤ → A ∈ D ..^ C ↔ D ≤ A ∧ A < C
26 3 20 24 25 syl3anc ⊢ A ∈ B ..^ C ∧ D ∈ ℤ → A ∈ D ..^ C ↔ D ≤ A ∧ A < C
27 22 26 orbi12d ⊢ A ∈ B ..^ C ∧ D ∈ ℤ → A ∈ B ..^ D ∨ A ∈ D ..^ C ↔ B ≤ A ∧ A < D ∨ D ≤ A ∧ A < C
28 17 27 mpbird ⊢ A ∈ B ..^ C ∧ D ∈ ℤ → A ∈ B ..^ D ∨ A ∈ D ..^ C