Metamath Proof Explorer


Theorem 4t4e16

Description: 4 times 4 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015)

Ref Expression
Assertion 4t4e16 44=16

Proof

Step Hyp Ref Expression
1 4nn0 40
2 3nn0 30
3 df-4 4=3+1
4 4t3e12 43=12
5 1nn0 10
6 2nn0 20
7 eqid 12=12
8 4cn 4
9 2cn 2
10 4p2e6 4+2=6
11 8 9 10 addcomli 2+4=6
12 5 6 1 7 11 decaddi 12+4=16
13 1 2 3 4 12 4t3lem 44=16