Metamath Proof Explorer

Theorem hashfzo

Description: Cardinality of a half-open set of integers. (Contributed by Stefan O'Rear, 15-Aug-2015)

Ref Expression
Assertion hashfzo ⊢ B ∈ ℤ ≥ A → A ..^ B = B − A

Proof

Step Hyp Ref Expression
1 fzo0 ⊢ A ..^ A = ∅
2 1 fveq2i ⊢ A ..^ A = ∅
3 hash0 ⊢ ∅ = 0
4 2 3 eqtri ⊢ A ..^ A = 0
5 eluzel2 ⊢ B ∈ ℤ ≥ A → A ∈ ℤ
6 5 zcnd ⊢ B ∈ ℤ ≥ A → A ∈ ℂ
7 6 subidd ⊢ B ∈ ℤ ≥ A → A − A = 0
8 4 7 eqtr4id ⊢ B ∈ ℤ ≥ A → A ..^ A = A − A
9 oveq2 ⊢ B = A → A ..^ B = A ..^ A
10 9 fveq2d ⊢ B = A → A ..^ B = A ..^ A
11 oveq1 ⊢ B = A → B − A = A − A
12 10 11 eqeq12d ⊢ B = A → A ..^ B = B − A ↔ A ..^ A = A − A
13 8 12 syl5ibrcom ⊢ B ∈ ℤ ≥ A → B = A → A ..^ B = B − A
14 eluzelz ⊢ B ∈ ℤ ≥ A → B ∈ ℤ
15 fzoval ⊢ B ∈ ℤ → A ..^ B = A … B − 1
16 14 15 syl ⊢ B ∈ ℤ ≥ A → A ..^ B = A … B − 1
17 16 fveq2d ⊢ B ∈ ℤ ≥ A → A ..^ B = A … B − 1
18 17 adantr ⊢ B ∈ ℤ ≥ A ∧ B − 1 ∈ ℤ ≥ A → A ..^ B = A … B − 1
19 hashfz ⊢ B − 1 ∈ ℤ ≥ A → A … B − 1 = B − 1 - A + 1
20 14 zcnd ⊢ B ∈ ℤ ≥ A → B ∈ ℂ
21 1cnd ⊢ B ∈ ℤ ≥ A → 1 ∈ ℂ
22 20 21 6 sub32d ⊢ B ∈ ℤ ≥ A → B - 1 - A = B - A - 1
23 22 oveq1d ⊢ B ∈ ℤ ≥ A → B − 1 - A + 1 = B − A - 1 + 1
24 20 6 subcld ⊢ B ∈ ℤ ≥ A → B − A ∈ ℂ
25 ax-1cn ⊢ 1 ∈ ℂ
26 npcan ⊢ B − A ∈ ℂ ∧ 1 ∈ ℂ → B − A - 1 + 1 = B − A
27 24 25 26 sylancl ⊢ B ∈ ℤ ≥ A → B − A - 1 + 1 = B − A
28 23 27 eqtrd ⊢ B ∈ ℤ ≥ A → B − 1 - A + 1 = B − A
29 19 28 sylan9eqr ⊢ B ∈ ℤ ≥ A ∧ B − 1 ∈ ℤ ≥ A → A … B − 1 = B − A
30 18 29 eqtrd ⊢ B ∈ ℤ ≥ A ∧ B − 1 ∈ ℤ ≥ A → A ..^ B = B − A
31 30 ex ⊢ B ∈ ℤ ≥ A → B − 1 ∈ ℤ ≥ A → A ..^ B = B − A
32 uzm1 ⊢ B ∈ ℤ ≥ A → B = A ∨ B − 1 ∈ ℤ ≥ A
33 13 31 32 mpjaod ⊢ B ∈ ℤ ≥ A → A ..^ B = B − A