# Metamath Proof Explorer

## Theorem 6p5lem

Description: Lemma for 6p5e11 and related theorems. (Contributed by Mario Carneiro, 19-Apr-2015)

Ref Expression
Hypotheses 6p5lem.1 $⊢ A ∈ ℕ 0$
6p5lem.2 $⊢ D ∈ ℕ 0$
6p5lem.3 $⊢ E ∈ ℕ 0$
6p5lem.4 $⊢ B = D + 1$
6p5lem.5 $⊢ C = E + 1$
6p5lem.6 No typesetting found for |- ( A + D ) = ; 1 E with typecode |-
Assertion 6p5lem Could not format assertion : No typesetting found for |- ( A + B ) = ; 1 C with typecode |-

### Proof

Step Hyp Ref Expression
1 6p5lem.1 $⊢ A ∈ ℕ 0$
2 6p5lem.2 $⊢ D ∈ ℕ 0$
3 6p5lem.3 $⊢ E ∈ ℕ 0$
4 6p5lem.4 $⊢ B = D + 1$
5 6p5lem.5 $⊢ C = E + 1$
6 6p5lem.6 Could not format ( A + D ) = ; 1 E : No typesetting found for |- ( A + D ) = ; 1 E with typecode |-
7 4 oveq2i $⊢ A + B = A + D + 1$
8 1 nn0cni $⊢ A ∈ ℂ$
9 2 nn0cni $⊢ D ∈ ℂ$
10 ax-1cn $⊢ 1 ∈ ℂ$
11 8 9 10 addassi $⊢ A + D + 1 = A + D + 1$
12 1nn0 $⊢ 1 ∈ ℕ 0$
13 5 eqcomi $⊢ E + 1 = C$
14 12 3 13 6 decsuc Could not format ( ( A + D ) + 1 ) = ; 1 C : No typesetting found for |- ( ( A + D ) + 1 ) = ; 1 C with typecode |-
15 7 11 14 3eqtr2i Could not format ( A + B ) = ; 1 C : No typesetting found for |- ( A + B ) = ; 1 C with typecode |-