![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > decmac | Structured version Visualization version GIF version |
Description: Perform a multiply-add of two numerals 𝑀 and 𝑁 against a fixed multiplicand 𝑃 (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
Ref | Expression |
---|---|
decma.a | ⊢ 𝐴 ∈ ℕ0 |
decma.b | ⊢ 𝐵 ∈ ℕ0 |
decma.c | ⊢ 𝐶 ∈ ℕ0 |
decma.d | ⊢ 𝐷 ∈ ℕ0 |
decma.m | ⊢ 𝑀 = ;𝐴𝐵 |
decma.n | ⊢ 𝑁 = ;𝐶𝐷 |
decmac.p | ⊢ 𝑃 ∈ ℕ0 |
decmac.f | ⊢ 𝐹 ∈ ℕ0 |
decmac.g | ⊢ 𝐺 ∈ ℕ0 |
decmac.e | ⊢ ((𝐴 · 𝑃) + (𝐶 + 𝐺)) = 𝐸 |
decmac.2 | ⊢ ((𝐵 · 𝑃) + 𝐷) = ;𝐺𝐹 |
Ref | Expression |
---|---|
decmac | ⊢ ((𝑀 · 𝑃) + 𝑁) = ;𝐸𝐹 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 10nn0 11970 | . . 3 ⊢ ;10 ∈ ℕ0 | |
2 | decma.a | . . 3 ⊢ 𝐴 ∈ ℕ0 | |
3 | decma.b | . . 3 ⊢ 𝐵 ∈ ℕ0 | |
4 | decma.c | . . 3 ⊢ 𝐶 ∈ ℕ0 | |
5 | decma.d | . . 3 ⊢ 𝐷 ∈ ℕ0 | |
6 | decma.m | . . . 4 ⊢ 𝑀 = ;𝐴𝐵 | |
7 | dfdec10 11955 | . . . 4 ⊢ ;𝐴𝐵 = ((;10 · 𝐴) + 𝐵) | |
8 | 6, 7 | eqtri 2819 | . . 3 ⊢ 𝑀 = ((;10 · 𝐴) + 𝐵) |
9 | decma.n | . . . 4 ⊢ 𝑁 = ;𝐶𝐷 | |
10 | dfdec10 11955 | . . . 4 ⊢ ;𝐶𝐷 = ((;10 · 𝐶) + 𝐷) | |
11 | 9, 10 | eqtri 2819 | . . 3 ⊢ 𝑁 = ((;10 · 𝐶) + 𝐷) |
12 | decmac.p | . . 3 ⊢ 𝑃 ∈ ℕ0 | |
13 | decmac.f | . . 3 ⊢ 𝐹 ∈ ℕ0 | |
14 | decmac.g | . . 3 ⊢ 𝐺 ∈ ℕ0 | |
15 | decmac.e | . . 3 ⊢ ((𝐴 · 𝑃) + (𝐶 + 𝐺)) = 𝐸 | |
16 | decmac.2 | . . . 4 ⊢ ((𝐵 · 𝑃) + 𝐷) = ;𝐺𝐹 | |
17 | dfdec10 11955 | . . . 4 ⊢ ;𝐺𝐹 = ((;10 · 𝐺) + 𝐹) | |
18 | 16, 17 | eqtri 2819 | . . 3 ⊢ ((𝐵 · 𝑃) + 𝐷) = ((;10 · 𝐺) + 𝐹) |
19 | 1, 2, 3, 4, 5, 8, 11, 12, 13, 14, 15, 18 | nummac 11997 | . 2 ⊢ ((𝑀 · 𝑃) + 𝑁) = ((;10 · 𝐸) + 𝐹) |
20 | dfdec10 11955 | . 2 ⊢ ;𝐸𝐹 = ((;10 · 𝐸) + 𝐹) | |
21 | 19, 20 | eqtr4i 2822 | 1 ⊢ ((𝑀 · 𝑃) + 𝑁) = ;𝐸𝐹 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1522 ∈ wcel 2081 (class class class)co 7021 0cc0 10388 1c1 10389 + caddc 10391 · cmul 10393 ℕ0cn0 11750 ;cdc 11952 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-sep 5099 ax-nul 5106 ax-pow 5162 ax-pr 5226 ax-un 7324 ax-resscn 10445 ax-1cn 10446 ax-icn 10447 ax-addcl 10448 ax-addrcl 10449 ax-mulcl 10450 ax-mulrcl 10451 ax-mulcom 10452 ax-addass 10453 ax-mulass 10454 ax-distr 10455 ax-i2m1 10456 ax-1ne0 10457 ax-1rid 10458 ax-rnegex 10459 ax-rrecex 10460 ax-cnre 10461 ax-pre-lttri 10462 ax-pre-lttrn 10463 ax-pre-ltadd 10464 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ne 2985 df-nel 3091 df-ral 3110 df-rex 3111 df-reu 3112 df-rab 3114 df-v 3439 df-sbc 3710 df-csb 3816 df-dif 3866 df-un 3868 df-in 3870 df-ss 3878 df-pss 3880 df-nul 4216 df-if 4386 df-pw 4459 df-sn 4477 df-pr 4479 df-tp 4481 df-op 4483 df-uni 4750 df-iun 4831 df-br 4967 df-opab 5029 df-mpt 5046 df-tr 5069 df-id 5353 df-eprel 5358 df-po 5367 df-so 5368 df-fr 5407 df-we 5409 df-xp 5454 df-rel 5455 df-cnv 5456 df-co 5457 df-dm 5458 df-rn 5459 df-res 5460 df-ima 5461 df-pred 6028 df-ord 6074 df-on 6075 df-lim 6076 df-suc 6077 df-iota 6194 df-fun 6232 df-fn 6233 df-f 6234 df-f1 6235 df-fo 6236 df-f1o 6237 df-fv 6238 df-riota 6982 df-ov 7024 df-oprab 7025 df-mpo 7026 df-om 7442 df-wrecs 7803 df-recs 7865 df-rdg 7903 df-er 8144 df-en 8363 df-dom 8364 df-sdom 8365 df-pnf 10528 df-mnf 10529 df-ltxr 10531 df-sub 10724 df-nn 11492 df-2 11553 df-3 11554 df-4 11555 df-5 11556 df-6 11557 df-7 11558 df-8 11559 df-9 11560 df-n0 11751 df-dec 11953 |
This theorem is referenced by: decrmac 12010 2exp16 16258 37prm 16288 43prm 16289 83prm 16290 139prm 16291 163prm 16292 317prm 16293 631prm 16294 1259lem1 16298 1259lem2 16299 1259lem3 16300 1259lem4 16301 1259lem5 16302 1259prm 16303 2503lem1 16304 2503lem2 16305 2503lem3 16306 2503prm 16307 4001lem1 16308 4001lem2 16309 4001lem3 16310 log2ublem3 25213 log2ub 25214 235t711 38724 257prm 43231 139prmALT 43267 127prm 43271 |
Copyright terms: Public domain | W3C validator |