Metamath Proof Explorer

Theorem eluzsubOLD

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

Ref Expression
Assertion eluzsubOLD ⊢M∈ℤ∧K∈ℤ∧N∈ℤ≥M+K→N−K∈ℤ≥M

Proof

Step Hyp Ref Expression
1 fvoveq1 ⊢M=ifM∈ℤM0→ℤ≥M+K=ℤ≥ifM∈ℤM0+K
2 1 eleq2d ⊢M=ifM∈ℤM0→N∈ℤ≥M+K↔N∈ℤ≥ifM∈ℤM0+K
3 fveq2 ⊢M=ifM∈ℤM0→ℤ≥M=ℤ≥ifM∈ℤM0
4 3 eleq2d ⊢M=ifM∈ℤM0→N−K∈ℤ≥M↔N−K∈ℤ≥ifM∈ℤM0
5 2 4 imbi12d ⊢M=ifM∈ℤM0→N∈ℤ≥M+K→N−K∈ℤ≥M↔N∈ℤ≥ifM∈ℤM0+K→N−K∈ℤ≥ifM∈ℤM0
6 oveq2 ⊢K=ifK∈ℤK0→ifM∈ℤM0+K=ifM∈ℤM0+ifK∈ℤK0
7 6 fveq2d ⊢K=ifK∈ℤK0→ℤ≥ifM∈ℤM0+K=ℤ≥ifM∈ℤM0+ifK∈ℤK0
8 7 eleq2d ⊢K=ifK∈ℤK0→N∈ℤ≥ifM∈ℤM0+K↔N∈ℤ≥ifM∈ℤM0+ifK∈ℤK0
9 oveq2 ⊢K=ifK∈ℤK0→N−K=N−ifK∈ℤK0
10 9 eleq1d ⊢K=ifK∈ℤK0→N−K∈ℤ≥ifM∈ℤM0↔N−ifK∈ℤK0∈ℤ≥ifM∈ℤM0
11 8 10 imbi12d ⊢K=ifK∈ℤK0→N∈ℤ≥ifM∈ℤM0+K→N−K∈ℤ≥ifM∈ℤM0↔N∈ℤ≥ifM∈ℤM0+ifK∈ℤK0→N−ifK∈ℤK0∈ℤ≥ifM∈ℤM0
12 0z ⊢0∈ℤ
13 12 elimel ⊢ifM∈ℤM0∈ℤ
14 12 elimel ⊢ifK∈ℤK0∈ℤ
15 13 14 eluzsubi ⊢N∈ℤ≥ifM∈ℤM0+ifK∈ℤK0→N−ifK∈ℤK0∈ℤ≥ifM∈ℤM0
16 5 11 15 dedth2h ⊢M∈ℤ∧K∈ℤ→N∈ℤ≥M+K→N−K∈ℤ≥M
17 16 3impia ⊢M∈ℤ∧K∈ℤ∧N∈ℤ≥M+K→N−K∈ℤ≥M