Metamath Proof Explorer

Theorem nn0diffz0

Description: Upper set of the nonnegative integers. (Contributed by Thierry Arnoux, 25-Jan-2026)

Ref Expression
Assertion nn0diffz0 ( 𝑁 ∈ ℕ0 → ( ℕ0 ∖ ( 0 ... 𝑁 ) ) = ( ℤ≥ ‘ ( 𝑁 + 1 ) ) )

Proof

Step Hyp Ref Expression
1 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
2 peano2nn0 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
3 2 1 eleqtrdi ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 0 ) )
4 fzouzsplit ⊢ ( ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 0 ) → ( ℤ≥ ‘ 0 ) = ( ( 0 ..^ ( 𝑁 + 1 ) ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) )
5 3 4 syl ⊢ ( 𝑁 ∈ ℕ0 → ( ℤ≥ ‘ 0 ) = ( ( 0 ..^ ( 𝑁 + 1 ) ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) )
6 1 5 eqtrid ⊢ ( 𝑁 ∈ ℕ0 → ℕ0 = ( ( 0 ..^ ( 𝑁 + 1 ) ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) )
7 6 difeq1d ⊢ ( 𝑁 ∈ ℕ0 → ( ℕ0 ∖ ( 0 ... 𝑁 ) ) = ( ( ( 0 ..^ ( 𝑁 + 1 ) ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∖ ( 0 ... 𝑁 ) ) )
8 uncom ⊢ ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ∪ ( 0 ... 𝑁 ) ) = ( ( 0 ... 𝑁 ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) )
9 nn0z ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
10 fzval3 ⊢ ( 𝑁 ∈ ℤ → ( 0 ... 𝑁 ) = ( 0 ..^ ( 𝑁 + 1 ) ) )
11 9 10 syl ⊢ ( 𝑁 ∈ ℕ0 → ( 0 ... 𝑁 ) = ( 0 ..^ ( 𝑁 + 1 ) ) )
12 11 uneq1d ⊢ ( 𝑁 ∈ ℕ0 → ( ( 0 ... 𝑁 ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = ( ( 0 ..^ ( 𝑁 + 1 ) ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) )
13 8 12 eqtrid ⊢ ( 𝑁 ∈ ℕ0 → ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ∪ ( 0 ... 𝑁 ) ) = ( ( 0 ..^ ( 𝑁 + 1 ) ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) )
14 13 difeq1d ⊢ ( 𝑁 ∈ ℕ0 → ( ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ∪ ( 0 ... 𝑁 ) ) ∖ ( 0 ... 𝑁 ) ) = ( ( ( 0 ..^ ( 𝑁 + 1 ) ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∖ ( 0 ... 𝑁 ) ) )
15 11 ineq2d ⊢ ( 𝑁 ∈ ℕ0 → ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ∩ ( 0 ... 𝑁 ) ) = ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
16 fzouzdisj ⊢ ( ( 0 ..^ ( 𝑁 + 1 ) ) ∩ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = ∅
17 16 ineqcomi ⊢ ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) = ∅
18 15 17 eqtrdi ⊢ ( 𝑁 ∈ ℕ0 → ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ∩ ( 0 ... 𝑁 ) ) = ∅ )
19 undif5 ⊢ ( ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ∩ ( 0 ... 𝑁 ) ) = ∅ → ( ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ∪ ( 0 ... 𝑁 ) ) ∖ ( 0 ... 𝑁 ) ) = ( ℤ≥ ‘ ( 𝑁 + 1 ) ) )
20 18 19 syl ⊢ ( 𝑁 ∈ ℕ0 → ( ( ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ∪ ( 0 ... 𝑁 ) ) ∖ ( 0 ... 𝑁 ) ) = ( ℤ≥ ‘ ( 𝑁 + 1 ) ) )
21 7 14 20 3eqtr2d ⊢ ( 𝑁 ∈ ℕ0 → ( ℕ0 ∖ ( 0 ... 𝑁 ) ) = ( ℤ≥ ‘ ( 𝑁 + 1 ) ) )