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