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 ⊢ 𝐴 ∈ ℕ0
4t3lem.2 ⊢ 𝐵 ∈ ℕ0
4t3lem.3 ⊢ 𝐶 = ( 𝐵 + 1 )
4t3lem.4 ⊢ ( 𝐴 · 𝐵 ) = 𝐷
4t3lem.5 ⊢ ( 𝐷 + 𝐴 ) = 𝐸
Assertion 4t3lem ( 𝐴 · 𝐶 ) = 𝐸

Proof

Step Hyp Ref Expression
1 4t3lem.1 ⊢ 𝐴 ∈ ℕ0
2 4t3lem.2 ⊢ 𝐵 ∈ ℕ0
3 4t3lem.3 ⊢ 𝐶 = ( 𝐵 + 1 )
4 4t3lem.4 ⊢ ( 𝐴 · 𝐵 ) = 𝐷
5 4t3lem.5 ⊢ ( 𝐷 + 𝐴 ) = 𝐸
6 3 oveq2i ⊢ ( 𝐴 · 𝐶 ) = ( 𝐴 · ( 𝐵 + 1 ) )
7 1 nn0cni ⊢ 𝐴 ∈ ℂ
8 2 nn0cni ⊢ 𝐵 ∈ ℂ
9 ax-1cn ⊢ 1 ∈ ℂ
10 7 8 9 adddii ⊢ ( 𝐴 · ( 𝐵 + 1 ) ) = ( ( 𝐴 · 𝐵 ) + ( 𝐴 · 1 ) )
11 7 mulridi ⊢ ( 𝐴 · 1 ) = 𝐴
12 4 11 oveq12i ⊢ ( ( 𝐴 · 𝐵 ) + ( 𝐴 · 1 ) ) = ( 𝐷 + 𝐴 )
13 10 12 eqtri ⊢ ( 𝐴 · ( 𝐵 + 1 ) ) = ( 𝐷 + 𝐴 )
14 13 5 eqtri ⊢ ( 𝐴 · ( 𝐵 + 1 ) ) = 𝐸
15 6 14 eqtri ⊢ ( 𝐴 · 𝐶 ) = 𝐸