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

Metamath Proof Explorer

Theorem decsubi

Description: Difference between a numeral M and a nonnegative integer N (no underflow). (Contributed by AV, 22-Jul-2021) (Revised by AV, 6-Sep-2021)

Ref Expression
Hypotheses decaddi.1 ⊢ 𝐴 ∈ ℕ0
decaddi.2 ⊢ 𝐵 ∈ ℕ0
decaddi.3 ⊢ 𝑁 ∈ ℕ0
decaddi.4 ⊢ 𝑀 = 𝐴 𝐵
decaddci.5 ⊢ ( 𝐴 + 1 ) = 𝐷
decsubi.5 ⊢ ( 𝐵 − 𝑁 ) = 𝐶
Assertion decsubi ( 𝑀 − 𝑁 ) = 𝐴 𝐶

Proof

Step Hyp Ref Expression
1 decaddi.1 ⊢ 𝐴 ∈ ℕ0
2 decaddi.2 ⊢ 𝐵 ∈ ℕ0
3 decaddi.3 ⊢ 𝑁 ∈ ℕ0
4 decaddi.4 ⊢ 𝑀 = 𝐴 𝐵
5 decaddci.5 ⊢ ( 𝐴 + 1 ) = 𝐷
6 decsubi.5 ⊢ ( 𝐵 − 𝑁 ) = 𝐶
7 10nn0 ⊢ 1 0 ∈ ℕ0
8 7 1 nn0mulcli ⊢ ( 1 0 · 𝐴 ) ∈ ℕ0
9 8 nn0cni ⊢ ( 1 0 · 𝐴 ) ∈ ℂ
10 2 nn0cni ⊢ 𝐵 ∈ ℂ
11 3 nn0cni ⊢ 𝑁 ∈ ℂ
12 9 10 11 addsubassi ⊢ ( ( ( 1 0 · 𝐴 ) + 𝐵 ) − 𝑁 ) = ( ( 1 0 · 𝐴 ) + ( 𝐵 − 𝑁 ) )
13 dfdec10 ⊢ 𝐴 𝐵 = ( ( 1 0 · 𝐴 ) + 𝐵 )
14 4 13 eqtri ⊢ 𝑀 = ( ( 1 0 · 𝐴 ) + 𝐵 )
15 14 oveq1i ⊢ ( 𝑀 − 𝑁 ) = ( ( ( 1 0 · 𝐴 ) + 𝐵 ) − 𝑁 )
16 dfdec10 ⊢ 𝐴 𝐶 = ( ( 1 0 · 𝐴 ) + 𝐶 )
17 6 eqcomi ⊢ 𝐶 = ( 𝐵 − 𝑁 )
18 17 oveq2i ⊢ ( ( 1 0 · 𝐴 ) + 𝐶 ) = ( ( 1 0 · 𝐴 ) + ( 𝐵 − 𝑁 ) )
19 16 18 eqtri ⊢ 𝐴 𝐶 = ( ( 1 0 · 𝐴 ) + ( 𝐵 − 𝑁 ) )
20 12 15 19 3eqtr4i ⊢ ( 𝑀 − 𝑁 ) = 𝐴 𝐶