This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem decrmanc

Description: Perform a multiply-add of two numerals M and N against a fixed multiplicand P (no carry). (Contributed by AV, 16-Sep-2021)

Ref Expression
Hypotheses decrmanc.a ⊢ A ∈ ℕ 0
decrmanc.b ⊢ B ∈ ℕ 0
decrmanc.n ⊢ N ∈ ℕ 0
decrmanc.m No typesetting found for |- M = ; A B with typecode |-
decrmanc.p ⊢ P ∈ ℕ 0
decrmanc.e ⊢ A ⁢ P = E
decrmanc.f ⊢ B ⁢ P + N = F
Assertion decrmanc Could not format assertion : No typesetting found for |- ( ( M x. P ) + N ) = ; E F with typecode |-

Proof

Step Hyp Ref Expression
1 decrmanc.a ⊢ A ∈ ℕ 0
2 decrmanc.b ⊢ B ∈ ℕ 0
3 decrmanc.n ⊢ N ∈ ℕ 0
4 decrmanc.m Could not format M = ; A B : No typesetting found for |- M = ; A B with typecode |-
5 decrmanc.p ⊢ P ∈ ℕ 0
6 decrmanc.e ⊢ A ⁢ P = E
7 decrmanc.f ⊢ B ⁢ P + N = F
8 0nn0 ⊢ 0 ∈ ℕ 0
9 3 dec0h ⊢ N = 0N
10 1 5 nn0mulcli ⊢ A ⁢ P ∈ ℕ 0
11 10 nn0cni ⊢ A ⁢ P ∈ ℂ
12 11 addridi ⊢ A ⁢ P + 0 = A ⁢ P
13 12 6 eqtri ⊢ A ⁢ P + 0 = E
14 1 2 8 3 4 9 5 13 7 decma Could not format ( ( M x. P ) + N ) = ; E F : No typesetting found for |- ( ( M x. P ) + N ) = ; E F with typecode |-