Metamath Proof Explorer

Theorem 5ndvds3

Description: 5 does not divide 3. (Contributed by AV, 8-Sep-2025)

Ref Expression
Assertion 5ndvds3 
|- -. 5 || 3

Proof

Step Hyp Ref Expression
1 5nn 
 |-  5 e. NN
2 0nn0 
 |-  0 e. NN0
3 3nn 
 |-  3 e. NN
4 5cn 
 |-  5 e. CC
5 4 mul01i 
 |-  ( 5 x. 0 ) = 0
6 5 oveq1i 
 |-  ( ( 5 x. 0 ) + 3 ) = ( 0 + 3 )
7 3cn 
 |-  3 e. CC
8 7 addlidi 
 |-  ( 0 + 3 ) = 3
9 6 8 eqtri 
 |-  ( ( 5 x. 0 ) + 3 ) = 3
10 3lt5 
 |-  3 < 5
11 1 2 3 9 10 ndvdsi 
 |-  -. 5 || 3