Theorem 4t3lem 8522

Description: Lemma for 4t3e12 8523 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 5550	. 2 ⊢ (𝐴 · 𝐶) = (𝐴 · (𝐵 + 1))
3		4t3lem.1	. . . . . 6 ⊢ 𝐴 ∈ ℕ0
4	3	nn0cni 8250	. . . . 5 ⊢ 𝐴 ∈ ℂ
5		4t3lem.2	. . . . . 6 ⊢ 𝐵 ∈ ℕ0
6	5	nn0cni 8250	. . . . 5 ⊢ 𝐵 ∈ ℂ
7		ax-1cn 7034	. . . . 5 ⊢ 1 ∈ ℂ
8	4, 6, 7	adddii 7094	. . . 4 ⊢ (𝐴 · (𝐵 + 1)) = ((𝐴 · 𝐵) + (𝐴 · 1))
9		4t3lem.4	. . . . 5 ⊢ (𝐴 · 𝐵) = 𝐷
10	4	mulid1i 7086	. . . . 5 ⊢ (𝐴 · 1) = 𝐴
11	9, 10	oveq12i 5551	. . . 4 ⊢ ((𝐴 · 𝐵) + (𝐴 · 1)) = (𝐷 + 𝐴)
12	8, 11	eqtri 2076	. . 3 ⊢ (𝐴 · (𝐵 + 1)) = (𝐷 + 𝐴)
13		4t3lem.5	. . 3 ⊢ (𝐷 + 𝐴) = 𝐸
14	12, 13	eqtri 2076	. 2 ⊢ (𝐴 · (𝐵 + 1)) = 𝐸
15	2, 14	eqtri 2076	1 ⊢ (𝐴 · 𝐶) = 𝐸

Syntax hints:   = wceq 1259   ∈ wcel 1409  (class class class)co 5539  1c1 6947   + caddc 6949   · cmul 6951  ℕ₀cn0 8238

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-sep 3902  ax-cnex 7032  ax-resscn 7033  ax-1cn 7034  ax-1re 7035  ax-icn 7036  ax-addcl 7037  ax-addrcl 7038  ax-mulcl 7039  ax-mulcom 7042  ax-mulass 7044  ax-distr 7045  ax-1rid 7048  ax-rnegex 7050  ax-cnre 7052

This theorem depends on definitions:  df-bi 114  df-3an 898  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-ral 2328  df-rex 2329  df-v 2576  df-un 2949  df-in 2951  df-ss 2958  df-sn 3408  df-pr 3409  df-op 3411  df-uni 3608  df-int 3643  df-br 3792  df-iota 4894  df-fv 4937  df-ov 5542  df-inn 7990  df-n0 8239

This theorem is referenced by:  4t3e12  8523  4t4e16  8524  5t2e10  8525  5t3e15  8526  5t4e20  8527  5t5e25  8528  6t3e18  8530  6t4e24  8531  6t5e30  8532  6t6e36  8533  7t3e21  8535  7t4e28  8536  7t5e35  8537  7t6e42  8538  7t7e49  8539  8t3e24  8541  8t4e32  8542  8t5e40  8543  8t6e48  8544  8t7e56  8545  8t8e64  8546  9t3e27  8548  9t4e36  8549  9t5e45  8550  9t6e54  8551  9t7e63  8552  9t8e72  8553  9t9e81  8554