Metamath Proof Explorer

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 ⊢N∈ℤ≥M∧K∈ℤ→N+K∈ℤ≥M+K

Proof

Step Hyp Ref Expression
1 eluzel2 ⊢N∈ℤ≥M→M∈ℤ
2 fveq2 ⊢M=ifM∈ℤM0→ℤ≥M=ℤ≥ifM∈ℤM0
3 2 eleq2d ⊢M=ifM∈ℤM0→N∈ℤ≥M↔N∈ℤ≥ifM∈ℤM0
4 fvoveq1 ⊢M=ifM∈ℤM0→ℤ≥M+K=ℤ≥ifM∈ℤM0+K
5 4 eleq2d ⊢M=ifM∈ℤM0→N+K∈ℤ≥M+K↔N+K∈ℤ≥ifM∈ℤM0+K
6 3 5 imbi12d ⊢M=ifM∈ℤM0→N∈ℤ≥M→N+K∈ℤ≥M+K↔N∈ℤ≥ifM∈ℤM0→N+K∈ℤ≥ifM∈ℤM0+K
7 oveq2 ⊢K=ifK∈ℤK0→N+K=N+ifK∈ℤK0
8 oveq2 ⊢K=ifK∈ℤK0→ifM∈ℤM0+K=ifM∈ℤM0+ifK∈ℤK0
9 8 fveq2d ⊢K=ifK∈ℤK0→ℤ≥ifM∈ℤM0+K=ℤ≥ifM∈ℤM0+ifK∈ℤK0
10 7 9 eleq12d ⊢K=ifK∈ℤK0→N+K∈ℤ≥ifM∈ℤM0+K↔N+ifK∈ℤK0∈ℤ≥ifM∈ℤM0+ifK∈ℤK0
11 10 imbi2d ⊢K=ifK∈ℤK0→N∈ℤ≥ifM∈ℤM0→N+K∈ℤ≥ifM∈ℤM0+K↔N∈ℤ≥ifM∈ℤM0→N+ifK∈ℤK0∈ℤ≥ifM∈ℤM0+ifK∈ℤK0
12 0z ⊢0∈ℤ
13 12 elimel ⊢ifK∈ℤK0∈ℤ
14 13 eluzaddi ⊢N∈ℤ≥ifM∈ℤM0→N+ifK∈ℤK0∈ℤ≥ifM∈ℤM0+ifK∈ℤK0
15 6 11 14 dedth2h ⊢M∈ℤ∧K∈ℤ→N∈ℤ≥M→N+K∈ℤ≥M+K
16 15 com12 ⊢N∈ℤ≥M→M∈ℤ∧K∈ℤ→N+K∈ℤ≥M+K
17 1 16 mpand ⊢N∈ℤ≥M→K∈ℤ→N+K∈ℤ≥M+K
18 17 imp ⊢N∈ℤ≥M∧K∈ℤ→N+K∈ℤ≥M+K