Metamath Proof Explorer

Theorem nndiffz1

Description: Upper set of the positive integers. (Contributed by Thierry Arnoux, 22-Aug-2017)

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

Proof

Step Hyp Ref Expression
1 1z ⊢ 1 ∈ ℤ
2 nn0z ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
3 elfz1 ⊢ ( ( 1 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑗 ∈ ( 1 ... 𝑁 ) ↔ ( 𝑗 ∈ ℤ ∧ 1 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) )
4 1 2 3 sylancr ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑗 ∈ ( 1 ... 𝑁 ) ↔ ( 𝑗 ∈ ℤ ∧ 1 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) )
5 3anass ⊢ ( ( 𝑗 ∈ ℤ ∧ 1 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ↔ ( 𝑗 ∈ ℤ ∧ ( 1 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) )
6 4 5 bitrdi ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑗 ∈ ( 1 ... 𝑁 ) ↔ ( 𝑗 ∈ ℤ ∧ ( 1 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) ) )
7 6 baibd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑗 ∈ ℤ ) → ( 𝑗 ∈ ( 1 ... 𝑁 ) ↔ ( 1 ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) )
8 7 baibd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑗 ∈ ℤ ) ∧ 1 ≤ 𝑗 ) → ( 𝑗 ∈ ( 1 ... 𝑁 ) ↔ 𝑗 ≤ 𝑁 ) )
9 8 notbid ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑗 ∈ ℤ ) ∧ 1 ≤ 𝑗 ) → ( ¬ 𝑗 ∈ ( 1 ... 𝑁 ) ↔ ¬ 𝑗 ≤ 𝑁 ) )
10 simpl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑗 ∈ ℤ ) → 𝑁 ∈ ℤ )
11 10 zred ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑗 ∈ ℤ ) → 𝑁 ∈ ℝ )
12 simpr ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑗 ∈ ℤ ) → 𝑗 ∈ ℤ )
13 12 zred ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑗 ∈ ℤ ) → 𝑗 ∈ ℝ )
14 11 13 ltnled ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑗 ∈ ℤ ) → ( 𝑁 < 𝑗 ↔ ¬ 𝑗 ≤ 𝑁 ) )
15 zltp1le ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑗 ∈ ℤ ) → ( 𝑁 < 𝑗 ↔ ( 𝑁 + 1 ) ≤ 𝑗 ) )
16 14 15 bitr3d ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑗 ∈ ℤ ) → ( ¬ 𝑗 ≤ 𝑁 ↔ ( 𝑁 + 1 ) ≤ 𝑗 ) )
17 2 16 sylan ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑗 ∈ ℤ ) → ( ¬ 𝑗 ≤ 𝑁 ↔ ( 𝑁 + 1 ) ≤ 𝑗 ) )
18 17 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑗 ∈ ℤ ) ∧ 1 ≤ 𝑗 ) → ( ¬ 𝑗 ≤ 𝑁 ↔ ( 𝑁 + 1 ) ≤ 𝑗 ) )
19 9 18 bitrd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑗 ∈ ℤ ) ∧ 1 ≤ 𝑗 ) → ( ¬ 𝑗 ∈ ( 1 ... 𝑁 ) ↔ ( 𝑁 + 1 ) ≤ 𝑗 ) )
20 19 pm5.32da ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑗 ∈ ℤ ) → ( ( 1 ≤ 𝑗 ∧ ¬ 𝑗 ∈ ( 1 ... 𝑁 ) ) ↔ ( 1 ≤ 𝑗 ∧ ( 𝑁 + 1 ) ≤ 𝑗 ) ) )
21 1red ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑁 + 1 ) ≤ 𝑗 ) → 1 ∈ ℝ )
22 simpll ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑁 + 1 ) ≤ 𝑗 ) → 𝑁 ∈ ℕ0 )
23 22 nn0red ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑁 + 1 ) ≤ 𝑗 ) → 𝑁 ∈ ℝ )
24 23 21 readdcld ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑁 + 1 ) ≤ 𝑗 ) → ( 𝑁 + 1 ) ∈ ℝ )
25 simplr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑁 + 1 ) ≤ 𝑗 ) → 𝑗 ∈ ℤ )
26 25 zred ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑁 + 1 ) ≤ 𝑗 ) → 𝑗 ∈ ℝ )
27 0p1e1 ⊢ ( 0 + 1 ) = 1
28 0red ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑁 + 1 ) ≤ 𝑗 ) → 0 ∈ ℝ )
29 22 nn0ge0d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑁 + 1 ) ≤ 𝑗 ) → 0 ≤ 𝑁 )
30 28 23 21 29 leadd1dd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑁 + 1 ) ≤ 𝑗 ) → ( 0 + 1 ) ≤ ( 𝑁 + 1 ) )
31 27 30 eqbrtrrid ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑁 + 1 ) ≤ 𝑗 ) → 1 ≤ ( 𝑁 + 1 ) )
32 simpr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑁 + 1 ) ≤ 𝑗 ) → ( 𝑁 + 1 ) ≤ 𝑗 )
33 21 24 26 31 32 letrd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑗 ∈ ℤ ) ∧ ( 𝑁 + 1 ) ≤ 𝑗 ) → 1 ≤ 𝑗 )
34 33 ex ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑗 ∈ ℤ ) → ( ( 𝑁 + 1 ) ≤ 𝑗 → 1 ≤ 𝑗 ) )
35 34 pm4.71rd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑗 ∈ ℤ ) → ( ( 𝑁 + 1 ) ≤ 𝑗 ↔ ( 1 ≤ 𝑗 ∧ ( 𝑁 + 1 ) ≤ 𝑗 ) ) )
36 20 35 bitr4d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑗 ∈ ℤ ) → ( ( 1 ≤ 𝑗 ∧ ¬ 𝑗 ∈ ( 1 ... 𝑁 ) ) ↔ ( 𝑁 + 1 ) ≤ 𝑗 ) )
37 36 pm5.32da ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑗 ∈ ℤ ∧ ( 1 ≤ 𝑗 ∧ ¬ 𝑗 ∈ ( 1 ... 𝑁 ) ) ) ↔ ( 𝑗 ∈ ℤ ∧ ( 𝑁 + 1 ) ≤ 𝑗 ) ) )
38 eldif ⊢ ( 𝑗 ∈ ( ℕ ∖ ( 1 ... 𝑁 ) ) ↔ ( 𝑗 ∈ ℕ ∧ ¬ 𝑗 ∈ ( 1 ... 𝑁 ) ) )
39 elnnz1 ⊢ ( 𝑗 ∈ ℕ ↔ ( 𝑗 ∈ ℤ ∧ 1 ≤ 𝑗 ) )
40 39 anbi1i ⊢ ( ( 𝑗 ∈ ℕ ∧ ¬ 𝑗 ∈ ( 1 ... 𝑁 ) ) ↔ ( ( 𝑗 ∈ ℤ ∧ 1 ≤ 𝑗 ) ∧ ¬ 𝑗 ∈ ( 1 ... 𝑁 ) ) )
41 anass ⊢ ( ( ( 𝑗 ∈ ℤ ∧ 1 ≤ 𝑗 ) ∧ ¬ 𝑗 ∈ ( 1 ... 𝑁 ) ) ↔ ( 𝑗 ∈ ℤ ∧ ( 1 ≤ 𝑗 ∧ ¬ 𝑗 ∈ ( 1 ... 𝑁 ) ) ) )
42 38 40 41 3bitri ⊢ ( 𝑗 ∈ ( ℕ ∖ ( 1 ... 𝑁 ) ) ↔ ( 𝑗 ∈ ℤ ∧ ( 1 ≤ 𝑗 ∧ ¬ 𝑗 ∈ ( 1 ... 𝑁 ) ) ) )
43 42 a1i ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑗 ∈ ( ℕ ∖ ( 1 ... 𝑁 ) ) ↔ ( 𝑗 ∈ ℤ ∧ ( 1 ≤ 𝑗 ∧ ¬ 𝑗 ∈ ( 1 ... 𝑁 ) ) ) ) )
44 peano2nn0 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
45 44 nn0zd ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℤ )
46 eluz1 ⊢ ( ( 𝑁 + 1 ) ∈ ℤ → ( 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ↔ ( 𝑗 ∈ ℤ ∧ ( 𝑁 + 1 ) ≤ 𝑗 ) ) )
47 45 46 syl ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ↔ ( 𝑗 ∈ ℤ ∧ ( 𝑁 + 1 ) ≤ 𝑗 ) ) )
48 37 43 47 3bitr4d ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑗 ∈ ( ℕ ∖ ( 1 ... 𝑁 ) ) ↔ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) )
49 48 eqrdv ⊢ ( 𝑁 ∈ ℕ0 → ( ℕ ∖ ( 1 ... 𝑁 ) ) = ( ℤ≥ ‘ ( 𝑁 + 1 ) ) )