Metamath Proof Explorer

Theorem eluzsub

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

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

Proof

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