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\in {\mathbb{N}}_0$$
	sqn5ii.2	$$⊢A+1=B$$
	sqn5ii.3	$$⊢AB=C$$
Assertion	sqn5ii	Could not format assertion : No typesetting found for |- ( ; A 5 x. ; A 5 ) = ; ; C 2 5 with typecode |-

Proof

Step	Hyp	Ref	Expression
1		sqn5i.1	$$⊢A\in {\mathbb{N}}_0$$
2		sqn5ii.2	$$⊢A+1=B$$
3		sqn5ii.3	$$⊢AB=C$$
4	1	sqn5i	Could not format ( ; A 5 x. ; A 5 ) = ; ; ( A x. ( A + 1 ) ) 2 5 : No typesetting found for |- ( ; A 5 x. ; A 5 ) = ; ; ( A x. ( A + 1 ) ) 2 5 with typecode |-
5	2	oveq2i	$$⊢A\left(A+1\right)=AB$$
6	5 3	eqtri	$$⊢A\left(A+1\right)=C$$
7	6	deceq1i	Could not format ; ( A x. ( A + 1 ) ) 2 = ; C 2 : No typesetting found for |- ; ( A x. ( A + 1 ) ) 2 = ; C 2 with typecode |-
8	7	deceq1i	Could not format ; ; ( A x. ( A + 1 ) ) 2 5 = ; ; C 2 5 : No typesetting found for |- ; ; ( A x. ( A + 1 ) ) 2 5 = ; ; C 2 5 with typecode |-
9	4 8	eqtri	Could not format ( ; A 5 x. ; A 5 ) = ; ; C 2 5 : No typesetting found for |- ( ; A 5 x. ; A 5 ) = ; ; C 2 5 with typecode |-