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 ⊢B∈ℤ≥A→A+1…B=B−A

Proof

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