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 imbitrrid ⊢ 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