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 
|- A e. NN0
decaddi.2 
|- B e. NN0
decaddi.3 
|- N e. NN0
decaddi.4 
|- M = ; A B
decaddci.5 
|- ( A + 1 ) = D
decsubi.5 
|- ( B - N ) = C
Assertion decsubi 
|- ( M - N ) = ; A C

Proof

Step Hyp Ref Expression
1 decaddi.1 
 |-  A e. NN0
2 decaddi.2 
 |-  B e. NN0
3 decaddi.3 
 |-  N e. NN0
4 decaddi.4 
 |-  M = ; A B
5 decaddci.5 
 |-  ( A + 1 ) = D
6 decsubi.5 
 |-  ( B - N ) = C
7 10nn0 
 |-  ; 1 0 e. NN0
8 7 1 nn0mulcli 
 |-  ( ; 1 0 x. A ) e. NN0
9 8 nn0cni 
 |-  ( ; 1 0 x. A ) e. CC
10 2 nn0cni 
 |-  B e. CC
11 3 nn0cni 
 |-  N e. CC
12 9 10 11 addsubassi 
 |-  ( ( ( ; 1 0 x. A ) + B ) - N ) = ( ( ; 1 0 x. A ) + ( B - N ) )
13 dfdec10 
 |-  ; A B = ( ( ; 1 0 x. A ) + B )
14 4 13 eqtri 
 |-  M = ( ( ; 1 0 x. A ) + B )
15 14 oveq1i 
 |-  ( M - N ) = ( ( ( ; 1 0 x. A ) + B ) - N )
16 dfdec10 
 |-  ; A C = ( ( ; 1 0 x. A ) + C )
17 6 eqcomi 
 |-  C = ( B - N )
18 17 oveq2i 
 |-  ( ( ; 1 0 x. A ) + C ) = ( ( ; 1 0 x. A ) + ( B - N ) )
19 16 18 eqtri 
 |-  ; A C = ( ( ; 1 0 x. A ) + ( B - N ) )
20 12 15 19 3eqtr4i 
 |-  ( M - N ) = ; A C