Theorem eluzsub

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

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

Proof

Step	Hyp	Ref	Expression
1		fvoveq1	⊢ ( 𝑀 = if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) → ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) = ( ℤ≥ ‘ ( if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) + 𝐾 ) ) )
2	1	eleq2d	⊢ ( 𝑀 = if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) → ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) ↔ 𝑁 ∈ ( ℤ≥ ‘ ( if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) + 𝐾 ) ) ) )
3		fveq2	⊢ ( 𝑀 = if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) → ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) )
4	3	eleq2d	⊢ ( 𝑀 = if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) → ( ( 𝑁 − 𝐾 ) ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑁 − 𝐾 ) ∈ ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ) )
5	2 4	imbi12d	⊢ ( 𝑀 = if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) → ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) → ( 𝑁 − 𝐾 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ↔ ( 𝑁 ∈ ( ℤ≥ ‘ ( if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) + 𝐾 ) ) → ( 𝑁 − 𝐾 ) ∈ ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ) ) )
6		oveq2	⊢ ( 𝐾 = if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) → ( if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) + 𝐾 ) = ( if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) + if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) ) )
7	6	fveq2d	⊢ ( 𝐾 = if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) → ( ℤ≥ ‘ ( if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) + 𝐾 ) ) = ( ℤ≥ ‘ ( if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) + if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) ) ) )
8	7	eleq2d	⊢ ( 𝐾 = if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) → ( 𝑁 ∈ ( ℤ≥ ‘ ( if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) + 𝐾 ) ) ↔ 𝑁 ∈ ( ℤ≥ ‘ ( if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) + if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) ) ) ) )
9		oveq2	⊢ ( 𝐾 = if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) → ( 𝑁 − 𝐾 ) = ( 𝑁 − if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) ) )
10	9	eleq1d	⊢ ( 𝐾 = if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) → ( ( 𝑁 − 𝐾 ) ∈ ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ↔ ( 𝑁 − if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) ) ∈ ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ) )
11	8 10	imbi12d	⊢ ( 𝐾 = 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	eluzsubi	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) + if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) ) ) → ( 𝑁 − if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) ) ∈ ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) )
16	5 11 15	dedth2h	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) → ( 𝑁 − 𝐾 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) )
17	16	3impia	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) ) → ( 𝑁 − 𝐾 ) ∈ ( ℤ≥ ‘ 𝑀 ) )