Metamath Proof Explorer

Theorem fzen2

Description: The cardinality of a finite set of sequential integers with arbitrary endpoints. (Contributed by Mario Carneiro, 13-Feb-2014)

Ref Expression
Hypothesis fzennn.1 ⊢ 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω )
Assertion fzen2 ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 ... 𝑁 ) ≈ ( ◡ 𝐺 ‘ ( ( 𝑁 + 1 ) − 𝑀 ) ) )

Proof

Step Hyp Ref Expression
1 fzennn.1 ⊢ 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω )
2 eluzel2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
3 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
4 1z ⊢ 1 ∈ ℤ
5 zsubcl ⊢ ( ( 1 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 1 − 𝑀 ) ∈ ℤ )
6 4 2 5 sylancr ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 1 − 𝑀 ) ∈ ℤ )
7 fzen ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 1 − 𝑀 ) ∈ ℤ ) → ( 𝑀 ... 𝑁 ) ≈ ( ( 𝑀 + ( 1 − 𝑀 ) ) ... ( 𝑁 + ( 1 − 𝑀 ) ) ) )
8 2 3 6 7 syl3anc ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 ... 𝑁 ) ≈ ( ( 𝑀 + ( 1 − 𝑀 ) ) ... ( 𝑁 + ( 1 − 𝑀 ) ) ) )
9 2 zcnd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℂ )
10 ax-1cn ⊢ 1 ∈ ℂ
11 pncan3 ⊢ ( ( 𝑀 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑀 + ( 1 − 𝑀 ) ) = 1 )
12 9 10 11 sylancl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 + ( 1 − 𝑀 ) ) = 1 )
13 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
14 zcn ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
15 addsubass ⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( ( 𝑁 + 1 ) − 𝑀 ) = ( 𝑁 + ( 1 − 𝑀 ) ) )
16 10 15 mp3an2 ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( ( 𝑁 + 1 ) − 𝑀 ) = ( 𝑁 + ( 1 − 𝑀 ) ) )
17 13 14 16 syl2an ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( 𝑁 + 1 ) − 𝑀 ) = ( 𝑁 + ( 1 − 𝑀 ) ) )
18 3 2 17 syl2anc ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑁 + 1 ) − 𝑀 ) = ( 𝑁 + ( 1 − 𝑀 ) ) )
19 18 eqcomd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + ( 1 − 𝑀 ) ) = ( ( 𝑁 + 1 ) − 𝑀 ) )
20 12 19 oveq12d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑀 + ( 1 − 𝑀 ) ) ... ( 𝑁 + ( 1 − 𝑀 ) ) ) = ( 1 ... ( ( 𝑁 + 1 ) − 𝑀 ) ) )
21 8 20 breqtrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 ... 𝑁 ) ≈ ( 1 ... ( ( 𝑁 + 1 ) − 𝑀 ) ) )
22 peano2uz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
23 uznn0sub ⊢ ( ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑁 + 1 ) − 𝑀 ) ∈ ℕ0 )
24 1 fzennn ⊢ ( ( ( 𝑁 + 1 ) − 𝑀 ) ∈ ℕ0 → ( 1 ... ( ( 𝑁 + 1 ) − 𝑀 ) ) ≈ ( ◡ 𝐺 ‘ ( ( 𝑁 + 1 ) − 𝑀 ) ) )
25 22 23 24 3syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 1 ... ( ( 𝑁 + 1 ) − 𝑀 ) ) ≈ ( ◡ 𝐺 ‘ ( ( 𝑁 + 1 ) − 𝑀 ) ) )
26 entr ⊢ ( ( ( 𝑀 ... 𝑁 ) ≈ ( 1 ... ( ( 𝑁 + 1 ) − 𝑀 ) ) ∧ ( 1 ... ( ( 𝑁 + 1 ) − 𝑀 ) ) ≈ ( ◡ 𝐺 ‘ ( ( 𝑁 + 1 ) − 𝑀 ) ) ) → ( 𝑀 ... 𝑁 ) ≈ ( ◡ 𝐺 ‘ ( ( 𝑁 + 1 ) − 𝑀 ) ) )
27 21 25 26 syl2anc ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 ... 𝑁 ) ≈ ( ◡ 𝐺 ‘ ( ( 𝑁 + 1 ) − 𝑀 ) ) )