ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  4t3lem GIF version

Theorem 4t3lem 9466
Description: Lemma for 4t3e12 9467 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
StepHypRef Expression
1 4t3lem.3 . . 3 𝐶 = (𝐵 + 1)
21oveq2i 5880 . 2 (𝐴 · 𝐶) = (𝐴 · (𝐵 + 1))
3 4t3lem.1 . . . . . 6 𝐴 ∈ ℕ0
43nn0cni 9174 . . . . 5 𝐴 ∈ ℂ
5 4t3lem.2 . . . . . 6 𝐵 ∈ ℕ0
65nn0cni 9174 . . . . 5 𝐵 ∈ ℂ
7 ax-1cn 7892 . . . . 5 1 ∈ ℂ
84, 6, 7adddii 7955 . . . 4 (𝐴 · (𝐵 + 1)) = ((𝐴 · 𝐵) + (𝐴 · 1))
9 4t3lem.4 . . . . 5 (𝐴 · 𝐵) = 𝐷
104mulid1i 7947 . . . . 5 (𝐴 · 1) = 𝐴
119, 10oveq12i 5881 . . . 4 ((𝐴 · 𝐵) + (𝐴 · 1)) = (𝐷 + 𝐴)
128, 11eqtri 2198 . . 3 (𝐴 · (𝐵 + 1)) = (𝐷 + 𝐴)
13 4t3lem.5 . . 3 (𝐷 + 𝐴) = 𝐸
1412, 13eqtri 2198 . 2 (𝐴 · (𝐵 + 1)) = 𝐸
152, 14eqtri 2198 1 (𝐴 · 𝐶) = 𝐸
Colors of variables: wff set class
Syntax hints:   = wceq 1353  wcel 2148  (class class class)co 5869  1c1 7800   + caddc 7802   · cmul 7804  0cn0 9162
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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-sep 4118  ax-cnex 7890  ax-resscn 7891  ax-1cn 7892  ax-1re 7893  ax-icn 7894  ax-addcl 7895  ax-addrcl 7896  ax-mulcl 7897  ax-mulcom 7900  ax-mulass 7902  ax-distr 7903  ax-1rid 7906  ax-rnegex 7908  ax-cnre 7910
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2739  df-un 3133  df-in 3135  df-ss 3142  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-int 3843  df-br 4001  df-iota 5174  df-fv 5220  df-ov 5872  df-inn 8906  df-n0 9163
This theorem is referenced by:  4t3e12  9467  4t4e16  9468  5t2e10  9469  5t3e15  9470  5t4e20  9471  5t5e25  9472  6t3e18  9474  6t4e24  9475  6t5e30  9476  6t6e36  9477  7t3e21  9479  7t4e28  9480  7t5e35  9481  7t6e42  9482  7t7e49  9483  8t3e24  9485  8t4e32  9486  8t5e40  9487  8t6e48  9488  8t7e56  9489  8t8e64  9490  9t3e27  9492  9t4e36  9493  9t5e45  9494  9t6e54  9495  9t7e63  9496  9t8e72  9497  9t9e81  9498
  Copyright terms: Public domain W3C validator