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	addid1d	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + 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 ) → ( 𝑁 + 𝐾 ) ∈ ( ℤ≥ ‘ 𝑀 ) )