Metamath Proof Explorer

Theorem eluzadd

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

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

Proof

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