This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem uzaddcl

Description: Addition closure law for an upper set of integers. (Contributed by NM, 4-Jun-2006)

Ref Expression
Assertion uzaddcl ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝑁 + 𝐾 ) ∈ ( ℤ≥ ‘ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 eluzelcn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℂ )
2 nn0cn ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℂ )
3 ax-1cn ⊢ 1 ∈ ℂ
4 addass ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑘 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 + 𝑘 ) + 1 ) = ( 𝑁 + ( 𝑘 + 1 ) ) )
5 3 4 mp3an3 ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( ( 𝑁 + 𝑘 ) + 1 ) = ( 𝑁 + ( 𝑘 + 1 ) ) )
6 1 2 5 syl2anr ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑁 + 𝑘 ) + 1 ) = ( 𝑁 + ( 𝑘 + 1 ) ) )
7 6 adantr ⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ ( 𝑁 + 𝑘 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑁 + 𝑘 ) + 1 ) = ( 𝑁 + ( 𝑘 + 1 ) ) )
8 peano2uz ⊢ ( ( 𝑁 + 𝑘 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑁 + 𝑘 ) + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
9 8 adantl ⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ ( 𝑁 + 𝑘 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑁 + 𝑘 ) + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
10 7 9 eqeltrrd ⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ ( 𝑁 + 𝑘 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑁 + ( 𝑘 + 1 ) ) ∈ ( ℤ≥ ‘ 𝑀 ) )
11 10 exp31 ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑁 + 𝑘 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + ( 𝑘 + 1 ) ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ) )
12 11 a2d ⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + 𝑘 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + ( 𝑘 + 1 ) ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ) )
13 1 addridd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + 0 ) = 𝑁 )
14 13 eleq1d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑁 + 0 ) ∈ ( ℤ≥ ‘ 𝑀 ) ↔ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) )
15 14 ibir ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + 0 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
16 oveq2 ⊢ ( 𝑗 = 0 → ( 𝑁 + 𝑗 ) = ( 𝑁 + 0 ) )
17 16 eleq1d ⊢ ( 𝑗 = 0 → ( ( 𝑁 + 𝑗 ) ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑁 + 0 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) )
18 17 imbi2d ⊢ ( 𝑗 = 0 → ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + 𝑗 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ↔ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + 0 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ) )
19 oveq2 ⊢ ( 𝑗 = 𝑘 → ( 𝑁 + 𝑗 ) = ( 𝑁 + 𝑘 ) )
20 19 eleq1d ⊢ ( 𝑗 = 𝑘 → ( ( 𝑁 + 𝑗 ) ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑁 + 𝑘 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) )
21 20 imbi2d ⊢ ( 𝑗 = 𝑘 → ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + 𝑗 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ↔ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + 𝑘 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ) )
22 oveq2 ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝑁 + 𝑗 ) = ( 𝑁 + ( 𝑘 + 1 ) ) )
23 22 eleq1d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝑁 + 𝑗 ) ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑁 + ( 𝑘 + 1 ) ) ∈ ( ℤ≥ ‘ 𝑀 ) ) )
24 23 imbi2d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + 𝑗 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ↔ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + ( 𝑘 + 1 ) ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ) )
25 oveq2 ⊢ ( 𝑗 = 𝐾 → ( 𝑁 + 𝑗 ) = ( 𝑁 + 𝐾 ) )
26 25 eleq1d ⊢ ( 𝑗 = 𝐾 → ( ( 𝑁 + 𝑗 ) ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑁 + 𝐾 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) )
27 26 imbi2d ⊢ ( 𝑗 = 𝐾 → ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + 𝑗 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ↔ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + 𝐾 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ) )
28 12 15 18 21 24 27 nn0indALT ⊢ ( 𝐾 ∈ ℕ0 → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + 𝐾 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) )
29 28 impcom ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝑁 + 𝐾 ) ∈ ( ℤ≥ ‘ 𝑀 ) )