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 ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ♯ ‘ ( 𝐴 ..^ 𝐵 ) ) = ( 𝐵 − 𝐴 ) )

Proof

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