Metamath Proof Explorer

Theorem fzouzsplit

Description: Split an upper integer set into a half-open integer range and another upper integer set. (Contributed by Mario Carneiro, 21-Sep-2016)

Ref Expression
Assertion fzouzsplit ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ℤ≥ ‘ 𝐴 ) = ( ( 𝐴 ..^ 𝐵 ) ∪ ( ℤ≥ ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 eluzelre ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝐵 ∈ ℝ )
2 eluzelre ⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝑥 ∈ ℝ )
3 lelttric ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝐵 ≤ 𝑥 ∨ 𝑥 < 𝐵 ) )
4 1 2 3 syl2an ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝐵 ≤ 𝑥 ∨ 𝑥 < 𝐵 ) )
5 4 orcomd ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝑥 < 𝐵 ∨ 𝐵 ≤ 𝑥 ) )
6 id ⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝑥 ∈ ( ℤ≥ ‘ 𝐴 ) )
7 eluzelz ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝐵 ∈ ℤ )
8 elfzo2 ⊢ ( 𝑥 ∈ ( 𝐴 ..^ 𝐵 ) ↔ ( 𝑥 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 ∈ ℤ ∧ 𝑥 < 𝐵 ) )
9 df-3an ⊢ ( ( 𝑥 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 ∈ ℤ ∧ 𝑥 < 𝐵 ) ↔ ( ( 𝑥 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 ∈ ℤ ) ∧ 𝑥 < 𝐵 ) )
10 8 9 bitri ⊢ ( 𝑥 ∈ ( 𝐴 ..^ 𝐵 ) ↔ ( ( 𝑥 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 ∈ ℤ ) ∧ 𝑥 < 𝐵 ) )
11 10 baib ⊢ ( ( 𝑥 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 ∈ ℤ ) → ( 𝑥 ∈ ( 𝐴 ..^ 𝐵 ) ↔ 𝑥 < 𝐵 ) )
12 6 7 11 syl2anr ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝑥 ∈ ( 𝐴 ..^ 𝐵 ) ↔ 𝑥 < 𝐵 ) )
13 eluzelz ⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝑥 ∈ ℤ )
14 eluz ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( 𝑥 ∈ ( ℤ≥ ‘ 𝐵 ) ↔ 𝐵 ≤ 𝑥 ) )
15 7 13 14 syl2an ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝑥 ∈ ( ℤ≥ ‘ 𝐵 ) ↔ 𝐵 ≤ 𝑥 ) )
16 12 15 orbi12d ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ( 𝑥 ∈ ( 𝐴 ..^ 𝐵 ) ∨ 𝑥 ∈ ( ℤ≥ ‘ 𝐵 ) ) ↔ ( 𝑥 < 𝐵 ∨ 𝐵 ≤ 𝑥 ) ) )
17 5 16 mpbird ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝑥 ∈ ( 𝐴 ..^ 𝐵 ) ∨ 𝑥 ∈ ( ℤ≥ ‘ 𝐵 ) ) )
18 17 ex ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝑥 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝑥 ∈ ( 𝐴 ..^ 𝐵 ) ∨ 𝑥 ∈ ( ℤ≥ ‘ 𝐵 ) ) ) )
19 elun ⊢ ( 𝑥 ∈ ( ( 𝐴 ..^ 𝐵 ) ∪ ( ℤ≥ ‘ 𝐵 ) ) ↔ ( 𝑥 ∈ ( 𝐴 ..^ 𝐵 ) ∨ 𝑥 ∈ ( ℤ≥ ‘ 𝐵 ) ) )
20 18 19 imbitrrdi ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝑥 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝑥 ∈ ( ( 𝐴 ..^ 𝐵 ) ∪ ( ℤ≥ ‘ 𝐵 ) ) ) )
21 20 ssrdv ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ℤ≥ ‘ 𝐴 ) ⊆ ( ( 𝐴 ..^ 𝐵 ) ∪ ( ℤ≥ ‘ 𝐵 ) ) )
22 elfzouz ⊢ ( 𝑥 ∈ ( 𝐴 ..^ 𝐵 ) → 𝑥 ∈ ( ℤ≥ ‘ 𝐴 ) )
23 22 ssriv ⊢ ( 𝐴 ..^ 𝐵 ) ⊆ ( ℤ≥ ‘ 𝐴 )
24 23 a1i ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐴 ..^ 𝐵 ) ⊆ ( ℤ≥ ‘ 𝐴 ) )
25 uzss ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ℤ≥ ‘ 𝐵 ) ⊆ ( ℤ≥ ‘ 𝐴 ) )
26 24 25 unssd ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ( 𝐴 ..^ 𝐵 ) ∪ ( ℤ≥ ‘ 𝐵 ) ) ⊆ ( ℤ≥ ‘ 𝐴 ) )
27 21 26 eqssd ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ℤ≥ ‘ 𝐴 ) = ( ( 𝐴 ..^ 𝐵 ) ∪ ( ℤ≥ ‘ 𝐵 ) ) )