This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fzosplit

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

Ref Expression
Assertion fzosplit ( 𝐷 ∈ ( 𝐵 ... 𝐶 ) → ( 𝐵 ..^ 𝐶 ) = ( ( 𝐵 ..^ 𝐷 ) ∪ ( 𝐷 ..^ 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( 𝐷 ∈ ( 𝐵 ... 𝐶 ) ∧ 𝑥 ∈ ( 𝐵 ..^ 𝐶 ) ) → 𝑥 ∈ ( 𝐵 ..^ 𝐶 ) )
2 elfzelz ⊢ ( 𝐷 ∈ ( 𝐵 ... 𝐶 ) → 𝐷 ∈ ℤ )
3 2 adantr ⊢ ( ( 𝐷 ∈ ( 𝐵 ... 𝐶 ) ∧ 𝑥 ∈ ( 𝐵 ..^ 𝐶 ) ) → 𝐷 ∈ ℤ )
4 fzospliti ⊢ ( ( 𝑥 ∈ ( 𝐵 ..^ 𝐶 ) ∧ 𝐷 ∈ ℤ ) → ( 𝑥 ∈ ( 𝐵 ..^ 𝐷 ) ∨ 𝑥 ∈ ( 𝐷 ..^ 𝐶 ) ) )
5 1 3 4 syl2anc ⊢ ( ( 𝐷 ∈ ( 𝐵 ... 𝐶 ) ∧ 𝑥 ∈ ( 𝐵 ..^ 𝐶 ) ) → ( 𝑥 ∈ ( 𝐵 ..^ 𝐷 ) ∨ 𝑥 ∈ ( 𝐷 ..^ 𝐶 ) ) )
6 elun ⊢ ( 𝑥 ∈ ( ( 𝐵 ..^ 𝐷 ) ∪ ( 𝐷 ..^ 𝐶 ) ) ↔ ( 𝑥 ∈ ( 𝐵 ..^ 𝐷 ) ∨ 𝑥 ∈ ( 𝐷 ..^ 𝐶 ) ) )
7 5 6 sylibr ⊢ ( ( 𝐷 ∈ ( 𝐵 ... 𝐶 ) ∧ 𝑥 ∈ ( 𝐵 ..^ 𝐶 ) ) → 𝑥 ∈ ( ( 𝐵 ..^ 𝐷 ) ∪ ( 𝐷 ..^ 𝐶 ) ) )
8 7 ex ⊢ ( 𝐷 ∈ ( 𝐵 ... 𝐶 ) → ( 𝑥 ∈ ( 𝐵 ..^ 𝐶 ) → 𝑥 ∈ ( ( 𝐵 ..^ 𝐷 ) ∪ ( 𝐷 ..^ 𝐶 ) ) ) )
9 8 ssrdv ⊢ ( 𝐷 ∈ ( 𝐵 ... 𝐶 ) → ( 𝐵 ..^ 𝐶 ) ⊆ ( ( 𝐵 ..^ 𝐷 ) ∪ ( 𝐷 ..^ 𝐶 ) ) )
10 elfzuz3 ⊢ ( 𝐷 ∈ ( 𝐵 ... 𝐶 ) → 𝐶 ∈ ( ℤ≥ ‘ 𝐷 ) )
11 fzoss2 ⊢ ( 𝐶 ∈ ( ℤ≥ ‘ 𝐷 ) → ( 𝐵 ..^ 𝐷 ) ⊆ ( 𝐵 ..^ 𝐶 ) )
12 10 11 syl ⊢ ( 𝐷 ∈ ( 𝐵 ... 𝐶 ) → ( 𝐵 ..^ 𝐷 ) ⊆ ( 𝐵 ..^ 𝐶 ) )
13 elfzuz ⊢ ( 𝐷 ∈ ( 𝐵 ... 𝐶 ) → 𝐷 ∈ ( ℤ≥ ‘ 𝐵 ) )
14 fzoss1 ⊢ ( 𝐷 ∈ ( ℤ≥ ‘ 𝐵 ) → ( 𝐷 ..^ 𝐶 ) ⊆ ( 𝐵 ..^ 𝐶 ) )
15 13 14 syl ⊢ ( 𝐷 ∈ ( 𝐵 ... 𝐶 ) → ( 𝐷 ..^ 𝐶 ) ⊆ ( 𝐵 ..^ 𝐶 ) )
16 12 15 unssd ⊢ ( 𝐷 ∈ ( 𝐵 ... 𝐶 ) → ( ( 𝐵 ..^ 𝐷 ) ∪ ( 𝐷 ..^ 𝐶 ) ) ⊆ ( 𝐵 ..^ 𝐶 ) )
17 9 16 eqssd ⊢ ( 𝐷 ∈ ( 𝐵 ... 𝐶 ) → ( 𝐵 ..^ 𝐶 ) = ( ( 𝐵 ..^ 𝐷 ) ∪ ( 𝐷 ..^ 𝐶 ) ) )