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

Metamath Proof Explorer

Theorem sqn5i

Description: The square of a number ending in 5. This shortcut only works because 5 is half of 10. (Contributed by Steven Nguyen, 16-Sep-2022)

Ref Expression
Hypothesis sqn5i.1 
|- A e. NN0
Assertion sqn5i 
|- ( ; A 5 x. ; A 5 ) = ; ; ( A x. ( A + 1 ) ) 2 5

Proof

Step Hyp Ref Expression
1 sqn5i.1 
 |-  A e. NN0
2 0nn0 
 |-  0 e. NN0
3 1 2 deccl 
 |-  ; A 0 e. NN0
4 3 nn0cni 
 |-  ; A 0 e. CC
5 5cn 
 |-  5 e. CC
6 5nn0 
 |-  5 e. NN0
7 eqid 
 |-  ; A 0 = ; A 0
8 5 addlidi 
 |-  ( 0 + 5 ) = 5
9 1 2 6 7 8 decaddi 
 |-  ( ; A 0 + 5 ) = ; A 5
10 eqid 
 |-  ; A 5 = ; A 5
11 eqid 
 |-  ( A + 1 ) = ( A + 1 )
12 5p5e10 
 |-  ( 5 + 5 ) = ; 1 0
13 1 6 6 10 11 12 decaddci2 
 |-  ( ; A 5 + 5 ) = ; ( A + 1 ) 0
14 4 5 9 13 sqmid3api 
 |-  ( ; A 5 x. ; A 5 ) = ( ( ; A 0 x. ; ( A + 1 ) 0 ) + ( 5 x. 5 ) )
15 2nn0 
 |-  2 e. NN0
16 5t5e25 
 |-  ( 5 x. 5 ) = ; 2 5
17 peano2nn0 
 |-  ( A e. NN0 -> ( A + 1 ) e. NN0 )
18 1 17 ax-mp 
 |-  ( A + 1 ) e. NN0
19 18 2 deccl 
 |-  ; ( A + 1 ) 0 e. NN0
20 1 18 nn0mulcli 
 |-  ( A x. ( A + 1 ) ) e. NN0
21 1 18 2 decmulnc 
 |-  ( A x. ; ( A + 1 ) 0 ) = ; ( A x. ( A + 1 ) ) ( A x. 0 )
22 1 nn0cni 
 |-  A e. CC
23 22 mul01i 
 |-  ( A x. 0 ) = 0
24 23 deceq2i 
 |-  ; ( A x. ( A + 1 ) ) ( A x. 0 ) = ; ( A x. ( A + 1 ) ) 0
25 21 24 eqtri 
 |-  ( A x. ; ( A + 1 ) 0 ) = ; ( A x. ( A + 1 ) ) 0
26 2cn 
 |-  2 e. CC
27 26 addlidi 
 |-  ( 0 + 2 ) = 2
28 20 2 15 25 27 decaddi 
 |-  ( ( A x. ; ( A + 1 ) 0 ) + 2 ) = ; ( A x. ( A + 1 ) ) 2
29 19 nn0cni 
 |-  ; ( A + 1 ) 0 e. CC
30 29 mul02i 
 |-  ( 0 x. ; ( A + 1 ) 0 ) = 0
31 30 oveq1i 
 |-  ( ( 0 x. ; ( A + 1 ) 0 ) + 5 ) = ( 0 + 5 )
32 31 8 eqtri 
 |-  ( ( 0 x. ; ( A + 1 ) 0 ) + 5 ) = 5
33 1 2 15 6 7 16 19 28 32 decma 
 |-  ( ( ; A 0 x. ; ( A + 1 ) 0 ) + ( 5 x. 5 ) ) = ; ; ( A x. ( A + 1 ) ) 2 5
34 14 33 eqtri 
 |-  ( ; A 5 x. ; A 5 ) = ; ; ( A x. ( A + 1 ) ) 2 5