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 = 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 K ∈ ℤ K 0 ∈ ℤ
14 13 eluzaddi ⊢ N ∈ ℤ ≥ if M ∈ ℤ M 0 → N + if K ∈ ℤ K 0 ∈ ℤ ≥ if M ∈ ℤ M 0 + if K ∈ ℤ K 0
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