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