Theorem 4t3lem 9511

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

Hypotheses

Ref	Expression
4t3lem.1	⊢ 𝐴 ∈ ℕ0
4t3lem.2	⊢ 𝐵 ∈ ℕ0
4t3lem.3	⊢ 𝐶 = (𝐵 + 1)
4t3lem.4	⊢ (𝐴 · 𝐵) = 𝐷
4t3lem.5	⊢ (𝐷 + 𝐴) = 𝐸

Assertion

Ref	Expression
4t3lem	⊢ (𝐴 · 𝐶) = 𝐸

Proof of Theorem 4t3lem

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

Syntax hints:   = wceq 1364   ∈ wcel 2160  (class class class)co 5897  1c1 7843   + caddc 7845   · cmul 7847  ℕ₀cn0 9207

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171  ax-sep 4136  ax-cnex 7933  ax-resscn 7934  ax-1cn 7935  ax-1re 7936  ax-icn 7937  ax-addcl 7938  ax-addrcl 7939  ax-mulcl 7940  ax-mulcom 7943  ax-mulass 7945  ax-distr 7946  ax-1rid 7949  ax-rnegex 7951  ax-cnre 7953

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ral 2473  df-rex 2474  df-v 2754  df-un 3148  df-in 3150  df-ss 3157  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-int 3860  df-br 4019  df-iota 5196  df-fv 5243  df-ov 5900  df-inn 8951  df-n0 9208

This theorem is referenced by:  4t3e12  9512  4t4e16  9513  5t2e10  9514  5t3e15  9515  5t4e20  9516  5t5e25  9517  6t3e18  9519  6t4e24  9520  6t5e30  9521  6t6e36  9522  7t3e21  9524  7t4e28  9525  7t5e35  9526  7t6e42  9527  7t7e49  9528  8t3e24  9530  8t4e32  9531  8t5e40  9532  8t6e48  9533  8t7e56  9534  8t8e64  9535  9t3e27  9537  9t4e36  9538  9t5e45  9539  9t6e54  9540  9t7e63  9541  9t8e72  9542  9t9e81  9543