Metamath Proof Explorer

Theorem 6p5lem

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

Ref Expression
Hypotheses 6p5lem.1 ⊢ 𝐴 ∈ ℕ0
6p5lem.2 ⊢ 𝐷 ∈ ℕ0
6p5lem.3 ⊢ 𝐸 ∈ ℕ0
6p5lem.4 ⊢ 𝐵 = ( 𝐷 + 1 )
6p5lem.5 ⊢ 𝐶 = ( 𝐸 + 1 )
6p5lem.6 ⊢ ( 𝐴 + 𝐷 ) = 1 𝐸
Assertion 6p5lem ( 𝐴 + 𝐵 ) = 1 𝐶

Proof

Step Hyp Ref Expression
1 6p5lem.1 ⊢ 𝐴 ∈ ℕ0
2 6p5lem.2 ⊢ 𝐷 ∈ ℕ0
3 6p5lem.3 ⊢ 𝐸 ∈ ℕ0
4 6p5lem.4 ⊢ 𝐵 = ( 𝐷 + 1 )
5 6p5lem.5 ⊢ 𝐶 = ( 𝐸 + 1 )
6 6p5lem.6 ⊢ ( 𝐴 + 𝐷 ) = 1 𝐸
7 4 oveq2i ⊢ ( 𝐴 + 𝐵 ) = ( 𝐴 + ( 𝐷 + 1 ) )
8 1 nn0cni ⊢ 𝐴 ∈ ℂ
9 2 nn0cni ⊢ 𝐷 ∈ ℂ
10 ax-1cn ⊢ 1 ∈ ℂ
11 8 9 10 addassi ⊢ ( ( 𝐴 + 𝐷 ) + 1 ) = ( 𝐴 + ( 𝐷 + 1 ) )
12 1nn0 ⊢ 1 ∈ ℕ0
13 5 eqcomi ⊢ ( 𝐸 + 1 ) = 𝐶
14 12 3 13 6 decsuc ⊢ ( ( 𝐴 + 𝐷 ) + 1 ) = 1 𝐶
15 7 11 14 3eqtr2i ⊢ ( 𝐴 + 𝐵 ) = 1 𝐶