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