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 ( ( 𝐴 ∈ ( 𝐵 ..^ 𝐶 ) ∧ 𝐷 ∈ ℤ ) → ( 𝐴 ∈ ( 𝐵 ..^ 𝐷 ) ∨ 𝐴 ∈ ( 𝐷 ..^ 𝐶 ) ) )

Proof

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