![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 4t3lem | GIF version |
Description: Lemma for 4t3e12 8725 and related theorems. (Contributed by Mario Carneiro, 19-Apr-2015.) |
Ref | Expression |
---|---|
4t3lem.1 | ⊢ 𝐴 ∈ ℕ0 |
4t3lem.2 | ⊢ 𝐵 ∈ ℕ0 |
4t3lem.3 | ⊢ 𝐶 = (𝐵 + 1) |
4t3lem.4 | ⊢ (𝐴 · 𝐵) = 𝐷 |
4t3lem.5 | ⊢ (𝐷 + 𝐴) = 𝐸 |
Ref | Expression |
---|---|
4t3lem | ⊢ (𝐴 · 𝐶) = 𝐸 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 4t3lem.3 | . . 3 ⊢ 𝐶 = (𝐵 + 1) | |
2 | 1 | oveq2i 5575 | . 2 ⊢ (𝐴 · 𝐶) = (𝐴 · (𝐵 + 1)) |
3 | 4t3lem.1 | . . . . . 6 ⊢ 𝐴 ∈ ℕ0 | |
4 | 3 | nn0cni 8437 | . . . . 5 ⊢ 𝐴 ∈ ℂ |
5 | 4t3lem.2 | . . . . . 6 ⊢ 𝐵 ∈ ℕ0 | |
6 | 5 | nn0cni 8437 | . . . . 5 ⊢ 𝐵 ∈ ℂ |
7 | ax-1cn 7201 | . . . . 5 ⊢ 1 ∈ ℂ | |
8 | 4, 6, 7 | adddii 7261 | . . . 4 ⊢ (𝐴 · (𝐵 + 1)) = ((𝐴 · 𝐵) + (𝐴 · 1)) |
9 | 4t3lem.4 | . . . . 5 ⊢ (𝐴 · 𝐵) = 𝐷 | |
10 | 4 | mulid1i 7253 | . . . . 5 ⊢ (𝐴 · 1) = 𝐴 |
11 | 9, 10 | oveq12i 5576 | . . . 4 ⊢ ((𝐴 · 𝐵) + (𝐴 · 1)) = (𝐷 + 𝐴) |
12 | 8, 11 | eqtri 2103 | . . 3 ⊢ (𝐴 · (𝐵 + 1)) = (𝐷 + 𝐴) |
13 | 4t3lem.5 | . . 3 ⊢ (𝐷 + 𝐴) = 𝐸 | |
14 | 12, 13 | eqtri 2103 | . 2 ⊢ (𝐴 · (𝐵 + 1)) = 𝐸 |
15 | 2, 14 | eqtri 2103 | 1 ⊢ (𝐴 · 𝐶) = 𝐸 |
Colors of variables: wff set class |
Syntax hints: = wceq 1285 ∈ wcel 1434 (class class class)co 5564 1c1 7114 + caddc 7116 · cmul 7118 ℕ0cn0 8425 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2065 ax-sep 3916 ax-cnex 7199 ax-resscn 7200 ax-1cn 7201 ax-1re 7202 ax-icn 7203 ax-addcl 7204 ax-addrcl 7205 ax-mulcl 7206 ax-mulcom 7209 ax-mulass 7211 ax-distr 7212 ax-1rid 7215 ax-rnegex 7217 ax-cnre 7219 |
This theorem depends on definitions: df-bi 115 df-3an 922 df-tru 1288 df-nf 1391 df-sb 1688 df-clab 2070 df-cleq 2076 df-clel 2079 df-nfc 2212 df-ral 2358 df-rex 2359 df-v 2612 df-un 2986 df-in 2988 df-ss 2995 df-sn 3422 df-pr 3423 df-op 3425 df-uni 3622 df-int 3657 df-br 3806 df-iota 4917 df-fv 4960 df-ov 5567 df-inn 8177 df-n0 8426 |
This theorem is referenced by: 4t3e12 8725 4t4e16 8726 5t2e10 8727 5t3e15 8728 5t4e20 8729 5t5e25 8730 6t3e18 8732 6t4e24 8733 6t5e30 8734 6t6e36 8735 7t3e21 8737 7t4e28 8738 7t5e35 8739 7t6e42 8740 7t7e49 8741 8t3e24 8743 8t4e32 8744 8t5e40 8745 8t6e48 8746 8t7e56 8747 8t8e64 8748 9t3e27 8750 9t4e36 8751 9t5e45 8752 9t6e54 8753 9t7e63 8754 9t8e72 8755 9t9e81 8756 |
Copyright terms: Public domain | W3C validator |