Theorem sqn5ii

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
Hypotheses	sqn5i.1	|- A e. NN0
	sqn5ii.2	|- ( A + 1 ) = B
	sqn5ii.3	|- ( A x. B ) = C
Assertion	sqn5ii	|- ( ; A 5 x. ; A 5 ) = ; ; C 2 5

Proof

Step	Hyp	Ref	Expression
1		sqn5i.1	|- A e. NN0
2		sqn5ii.2	|- ( A + 1 ) = B
3		sqn5ii.3	|- ( A x. B ) = C
4	1	sqn5i	|- ( ; A 5 x. ; A 5 ) = ; ; ( A x. ( A + 1 ) ) 2 5
5	2	oveq2i	|- ( A x. ( A + 1 ) ) = ( A x. B )
6	5	deceq1i	|- ; ( A x. ( A + 1 ) ) 2 = ; ( A x. B ) 2
7	6	deceq1i	|- ; ; ( A x. ( A + 1 ) ) 2 5 = ; ; ( A x. B ) 2 5
8	3	deceq1i	|- ; ( A x. B ) 2 = ; C 2
9	8	deceq1i	|- ; ; ( A x. B ) 2 5 = ; ; C 2 5
10	4 7 9	3eqtri	|- ( ; A 5 x. ; A 5 ) = ; ; C 2 5