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

Step	Hyp	Ref	Expression
1		sqn5i.1	$⊢ A \in ℕ_{0}$
2		sqn5ii.2	$⊢ A + 1 = B$
3		sqn5ii.3	$⊢ A B = 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 (A + 1) = A B$
6	5 3	eqtri	$⊢ A (A + 1) = 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 \|-

Metamath Proof Explorer