This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 4t3lem

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

Ref Expression
Hypotheses 4t3lem.1 ⊢ A ∈ ℕ 0
4t3lem.2 ⊢ B ∈ ℕ 0
4t3lem.3 ⊢ C = B + 1
4t3lem.4 ⊢ A ⁢ B = D
4t3lem.5 ⊢ D + A = E
Assertion 4t3lem ⊢ A ⁢ C = E

Proof

Step Hyp Ref Expression
1 4t3lem.1 ⊢ A ∈ ℕ 0
2 4t3lem.2 ⊢ B ∈ ℕ 0
3 4t3lem.3 ⊢ C = B + 1
4 4t3lem.4 ⊢ A ⁢ B = D
5 4t3lem.5 ⊢ D + A = E
6 3 oveq2i ⊢ A ⁢ C = A ⁢ B + 1
7 1 nn0cni ⊢ A ∈ ℂ
8 2 nn0cni ⊢ B ∈ ℂ
9 ax-1cn ⊢ 1 ∈ ℂ
10 7 8 9 adddii ⊢ A ⁢ B + 1 = A ⁢ B + A ⋅ 1
11 7 mulridi ⊢ A ⋅ 1 = A
12 4 11 oveq12i ⊢ A ⁢ B + A ⋅ 1 = D + A
13 10 12 eqtri ⊢ A ⁢ B + 1 = D + A
14 13 5 eqtri ⊢ A ⁢ B + 1 = E
15 6 14 eqtri ⊢ A ⁢ C = E