Metamath Proof Explorer

Theorem decmul1

Description: The product of a numeral with a number (no carry). (Contributed by AV, 22-Jul-2021) (Revised by AV, 6-Sep-2021) Remove hypothesis D e. NN0 . (Revised by Steven Nguyen, 7-Dec-2022)

Ref Expression
Hypotheses decmul1.p โŠข ๐‘ƒ โˆˆ โ„•0
decmul1.a โŠข ๐ด โˆˆ โ„•0
decmul1.b โŠข ๐ต โˆˆ โ„•0
decmul1.n โŠข ๐‘ = ๐ด ๐ต
decmul1.c โŠข ( ๐ด ยท ๐‘ƒ ) = ๐ถ
decmul1.d โŠข ( ๐ต ยท ๐‘ƒ ) = ๐ท
Assertion decmul1 ( ๐‘ ยท ๐‘ƒ ) = ๐ถ ๐ท

Proof

Step Hyp Ref Expression
1 decmul1.p โŠข ๐‘ƒ โˆˆ โ„•0
2 decmul1.a โŠข ๐ด โˆˆ โ„•0
3 decmul1.b โŠข ๐ต โˆˆ โ„•0
4 decmul1.n โŠข ๐‘ = ๐ด ๐ต
5 decmul1.c โŠข ( ๐ด ยท ๐‘ƒ ) = ๐ถ
6 decmul1.d โŠข ( ๐ต ยท ๐‘ƒ ) = ๐ท
7 2 3 deccl โŠข ๐ด ๐ต โˆˆ โ„•0
8 4 7 eqeltri โŠข ๐‘ โˆˆ โ„•0
9 8 1 num0u โŠข ( ๐‘ ยท ๐‘ƒ ) = ( ( ๐‘ ยท ๐‘ƒ ) + 0 )
10 0nn0 โŠข 0 โˆˆ โ„•0
11 3 1 nn0mulcli โŠข ( ๐ต ยท ๐‘ƒ ) โˆˆ โ„•0
12 11 nn0cni โŠข ( ๐ต ยท ๐‘ƒ ) โˆˆ โ„‚
13 12 addid1i โŠข ( ( ๐ต ยท ๐‘ƒ ) + 0 ) = ( ๐ต ยท ๐‘ƒ )
14 13 6 eqtri โŠข ( ( ๐ต ยท ๐‘ƒ ) + 0 ) = ๐ท
15 2 3 10 4 1 5 14 decrmanc โŠข ( ( ๐‘ ยท ๐‘ƒ ) + 0 ) = ๐ถ ๐ท
16 9 15 eqtri โŠข ( ๐‘ ยท ๐‘ƒ ) = ๐ถ ๐ท