Theorem eluzadd

Description: Membership in a later upper set of integers. (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Assertion	eluzadd	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐾 ∈ ℤ ) → ( 𝑁 + 𝐾 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eluzel2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
2		fveq2	⊢ ( 𝑀 = if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) → ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) )
3	2	eleq2d	⊢ ( 𝑀 = if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ 𝑁 ∈ ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ) )
4		fvoveq1	⊢ ( 𝑀 = if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) → ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) = ( ℤ≥ ‘ ( if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) + 𝐾 ) ) )
5	4	eleq2d	⊢ ( 𝑀 = if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) → ( ( 𝑁 + 𝐾 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) ↔ ( 𝑁 + 𝐾 ) ∈ ( ℤ≥ ‘ ( if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) + 𝐾 ) ) ) )
6	3 5	imbi12d	⊢ ( 𝑀 = if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) → ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + 𝐾 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) ) ↔ ( 𝑁 ∈ ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) → ( 𝑁 + 𝐾 ) ∈ ( ℤ≥ ‘ ( if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) + 𝐾 ) ) ) ) )
7		oveq2	⊢ ( 𝐾 = if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) → ( 𝑁 + 𝐾 ) = ( 𝑁 + if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) ) )
8		oveq2	⊢ ( 𝐾 = if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) → ( if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) + 𝐾 ) = ( if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) + if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) ) )
9	8	fveq2d	⊢ ( 𝐾 = if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) → ( ℤ≥ ‘ ( if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) + 𝐾 ) ) = ( ℤ≥ ‘ ( if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) + if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) ) ) )
10	7 9	eleq12d	⊢ ( 𝐾 = if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) → ( ( 𝑁 + 𝐾 ) ∈ ( ℤ≥ ‘ ( if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) + 𝐾 ) ) ↔ ( 𝑁 + if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) ) ∈ ( ℤ≥ ‘ ( if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) + if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) ) ) ) )
11	10	imbi2d	⊢ ( 𝐾 = if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) → ( ( 𝑁 ∈ ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) → ( 𝑁 + 𝐾 ) ∈ ( ℤ≥ ‘ ( if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) + 𝐾 ) ) ) ↔ ( 𝑁 ∈ ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) → ( 𝑁 + if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) ) ∈ ( ℤ≥ ‘ ( if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) + if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) ) ) ) ) )
12		0z	⊢ 0 ∈ ℤ
13	12	elimel	⊢ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ∈ ℤ
14	12	elimel	⊢ if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) ∈ ℤ
15	13 14	eluzaddi	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) → ( 𝑁 + if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) ) ∈ ( ℤ≥ ‘ ( if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) + if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) ) ) )
16	6 11 15	dedth2h	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + 𝐾 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) ) )
17	16	com12	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑁 + 𝐾 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) ) )
18	1 17	mpand	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝐾 ∈ ℤ → ( 𝑁 + 𝐾 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) ) )
19	18	imp	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐾 ∈ ℤ ) → ( 𝑁 + 𝐾 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) )