Metamath Proof Explorer

Theorem hashfzp1

Description: Value of the numeric cardinality of a (possibly empty) integer range. (Contributed by AV, 19-Jun-2021)

Ref Expression
Assertion hashfzp1 ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ♯ ‘ ( ( 𝐴 + 1 ) ... 𝐵 ) ) = ( 𝐵 − 𝐴 ) )

Proof

Step Hyp Ref Expression
1 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
2 eluzelre ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝐵 ∈ ℝ )
3 2 ltp1d ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝐵 < ( 𝐵 + 1 ) )
4 eluzelz ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝐵 ∈ ℤ )
5 peano2z ⊢ ( 𝐵 ∈ ℤ → ( 𝐵 + 1 ) ∈ ℤ )
6 5 ancri ⊢ ( 𝐵 ∈ ℤ → ( ( 𝐵 + 1 ) ∈ ℤ ∧ 𝐵 ∈ ℤ ) )
7 fzn ⊢ ( ( ( 𝐵 + 1 ) ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐵 < ( 𝐵 + 1 ) ↔ ( ( 𝐵 + 1 ) ... 𝐵 ) = ∅ ) )
8 4 6 7 3syl ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐵 < ( 𝐵 + 1 ) ↔ ( ( 𝐵 + 1 ) ... 𝐵 ) = ∅ ) )
9 3 8 mpbid ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ( 𝐵 + 1 ) ... 𝐵 ) = ∅ )
10 9 fveq2d ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ♯ ‘ ( ( 𝐵 + 1 ) ... 𝐵 ) ) = ( ♯ ‘ ∅ ) )
11 4 zcnd ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝐵 ∈ ℂ )
12 11 subidd ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐵 − 𝐵 ) = 0 )
13 1 10 12 3eqtr4a ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ♯ ‘ ( ( 𝐵 + 1 ) ... 𝐵 ) ) = ( 𝐵 − 𝐵 ) )
14 oveq1 ⊢ ( 𝐴 = 𝐵 → ( 𝐴 + 1 ) = ( 𝐵 + 1 ) )
15 14 fvoveq1d ⊢ ( 𝐴 = 𝐵 → ( ♯ ‘ ( ( 𝐴 + 1 ) ... 𝐵 ) ) = ( ♯ ‘ ( ( 𝐵 + 1 ) ... 𝐵 ) ) )
16 oveq2 ⊢ ( 𝐴 = 𝐵 → ( 𝐵 − 𝐴 ) = ( 𝐵 − 𝐵 ) )
17 15 16 eqeq12d ⊢ ( 𝐴 = 𝐵 → ( ( ♯ ‘ ( ( 𝐴 + 1 ) ... 𝐵 ) ) = ( 𝐵 − 𝐴 ) ↔ ( ♯ ‘ ( ( 𝐵 + 1 ) ... 𝐵 ) ) = ( 𝐵 − 𝐵 ) ) )
18 13 17 syl5ibr ⊢ ( 𝐴 = 𝐵 → ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ♯ ‘ ( ( 𝐴 + 1 ) ... 𝐵 ) ) = ( 𝐵 − 𝐴 ) ) )
19 uzp1 ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐵 = 𝐴 ∨ 𝐵 ∈ ( ℤ≥ ‘ ( 𝐴 + 1 ) ) ) )
20 pm2.24 ⊢ ( 𝐴 = 𝐵 → ( ¬ 𝐴 = 𝐵 → 𝐵 ∈ ( ℤ≥ ‘ ( 𝐴 + 1 ) ) ) )
21 20 eqcoms ⊢ ( 𝐵 = 𝐴 → ( ¬ 𝐴 = 𝐵 → 𝐵 ∈ ( ℤ≥ ‘ ( 𝐴 + 1 ) ) ) )
22 ax-1 ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ ( 𝐴 + 1 ) ) → ( ¬ 𝐴 = 𝐵 → 𝐵 ∈ ( ℤ≥ ‘ ( 𝐴 + 1 ) ) ) )
23 21 22 jaoi ⊢ ( ( 𝐵 = 𝐴 ∨ 𝐵 ∈ ( ℤ≥ ‘ ( 𝐴 + 1 ) ) ) → ( ¬ 𝐴 = 𝐵 → 𝐵 ∈ ( ℤ≥ ‘ ( 𝐴 + 1 ) ) ) )
24 19 23 syl ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ¬ 𝐴 = 𝐵 → 𝐵 ∈ ( ℤ≥ ‘ ( 𝐴 + 1 ) ) ) )
25 24 impcom ⊢ ( ( ¬ 𝐴 = 𝐵 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) → 𝐵 ∈ ( ℤ≥ ‘ ( 𝐴 + 1 ) ) )
26 hashfz ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ ( 𝐴 + 1 ) ) → ( ♯ ‘ ( ( 𝐴 + 1 ) ... 𝐵 ) ) = ( ( 𝐵 − ( 𝐴 + 1 ) ) + 1 ) )
27 25 26 syl ⊢ ( ( ¬ 𝐴 = 𝐵 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ♯ ‘ ( ( 𝐴 + 1 ) ... 𝐵 ) ) = ( ( 𝐵 − ( 𝐴 + 1 ) ) + 1 ) )
28 eluzel2 ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝐴 ∈ ℤ )
29 28 zcnd ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝐴 ∈ ℂ )
30 1cnd ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → 1 ∈ ℂ )
31 11 29 30 nppcan2d ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ( 𝐵 − ( 𝐴 + 1 ) ) + 1 ) = ( 𝐵 − 𝐴 ) )
32 31 adantl ⊢ ( ( ¬ 𝐴 = 𝐵 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ( 𝐵 − ( 𝐴 + 1 ) ) + 1 ) = ( 𝐵 − 𝐴 ) )
33 27 32 eqtrd ⊢ ( ( ¬ 𝐴 = 𝐵 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ♯ ‘ ( ( 𝐴 + 1 ) ... 𝐵 ) ) = ( 𝐵 − 𝐴 ) )
34 33 ex ⊢ ( ¬ 𝐴 = 𝐵 → ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ♯ ‘ ( ( 𝐴 + 1 ) ... 𝐵 ) ) = ( 𝐵 − 𝐴 ) ) )
35 18 34 pm2.61i ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ♯ ‘ ( ( 𝐴 + 1 ) ... 𝐵 ) ) = ( 𝐵 − 𝐴 ) )