Metamath Proof Explorer


Theorem dec5nprm

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

Ref Expression
Hypothesis dec5nprm.1 A
Assertion dec5nprm Could not format assertion : No typesetting found for |- -. ; A 5 e. Prime with typecode |-

Proof

Step Hyp Ref Expression
1 dec5nprm.1 A
2 2nn 2
3 2 1 nnmulcli 2A
4 peano2nn 2A2A+1
5 3 4 ax-mp 2A+1
6 5nn 5
7 1nn0 10
8 1lt2 1<2
9 2 1 7 7 8 numlti 1<2A+1
10 1lt5 1<5
11 2 nncni 2
12 1 nncni A
13 5cn 5
14 11 12 13 mul32i 2A5=25A
15 5t2e10 52=10
16 13 11 15 mulcomli 25=10
17 16 oveq1i 25A=10A
18 14 17 eqtri 2A5=10A
19 13 mulid2i 15=5
20 18 19 oveq12i 2A5+15=10A+5
21 3 nncni 2A
22 ax-1cn 1
23 21 22 13 adddiri 2A+15=2A5+15
24 dfdec10 Could not format ; A 5 = ( ( ; 1 0 x. A ) + 5 ) : No typesetting found for |- ; A 5 = ( ( ; 1 0 x. A ) + 5 ) with typecode |-
25 20 23 24 3eqtr4i Could not format ( ( ( 2 x. A ) + 1 ) x. 5 ) = ; A 5 : No typesetting found for |- ( ( ( 2 x. A ) + 1 ) x. 5 ) = ; A 5 with typecode |-
26 5 6 9 10 25 nprmi Could not format -. ; A 5 e. Prime : No typesetting found for |- -. ; A 5 e. Prime with typecode |-