Theorem eluzaddOLD

Description: Obsolete version of eluzadd as of 7-Feb-2025. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof modification is discouraged.) (New usage is discouraged.)

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

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	13	eluzaddi	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) → ( 𝑁 + if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) ) ∈ ( ℤ≥ ‘ ( if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) + if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) ) ) )
15	6 11 14	dedth2h	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + 𝐾 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) ) )
16	15	com12	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑁 + 𝐾 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) ) )
17	1 16	mpand	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝐾 ∈ ℤ → ( 𝑁 + 𝐾 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) ) )
18	17	imp	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐾 ∈ ℤ ) → ( 𝑁 + 𝐾 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) )