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

Metamath Proof Explorer

Theorem dec5dvds

Description: Divisibility by five is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015)

Ref Expression
Hypotheses dec5dvds.1 
|- A e. NN0
dec5dvds.2 
|- B e. NN
dec5dvds.3 
|- B < 5
Assertion dec5dvds 
|- -. 5 || ; A B

Proof

Step Hyp Ref Expression
1 dec5dvds.1 
 |-  A e. NN0
2 dec5dvds.2 
 |-  B e. NN
3 dec5dvds.3 
 |-  B < 5
4 5nn 
 |-  5 e. NN
5 2nn0 
 |-  2 e. NN0
6 5 1 nn0mulcli 
 |-  ( 2 x. A ) e. NN0
7 5cn 
 |-  5 e. CC
8 2cn 
 |-  2 e. CC
9 1 nn0cni 
 |-  A e. CC
10 7 8 9 mulassi 
 |-  ( ( 5 x. 2 ) x. A ) = ( 5 x. ( 2 x. A ) )
11 5t2e10 
 |-  ( 5 x. 2 ) = ; 1 0
12 11 oveq1i 
 |-  ( ( 5 x. 2 ) x. A ) = ( ; 1 0 x. A )
13 10 12 eqtr3i 
 |-  ( 5 x. ( 2 x. A ) ) = ( ; 1 0 x. A )
14 13 oveq1i 
 |-  ( ( 5 x. ( 2 x. A ) ) + B ) = ( ( ; 1 0 x. A ) + B )
15 dfdec10 
 |-  ; A B = ( ( ; 1 0 x. A ) + B )
16 14 15 eqtr4i 
 |-  ( ( 5 x. ( 2 x. A ) ) + B ) = ; A B
17 4 6 2 16 3 ndvdsi 
 |-  -. 5 || ; A B