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	⊢ 𝐴 ∈ ℕ0
	sqn5ii.2	⊢ ( 𝐴 + 1 ) = 𝐵
	sqn5ii.3	⊢ ( 𝐴 · 𝐵 ) = 𝐶
Assertion	sqn5ii	⊢ ( ; 𝐴 5 · ; 𝐴 5 ) = ; ; 𝐶 2 5

Proof

Step	Hyp	Ref	Expression
1		sqn5i.1	⊢ 𝐴 ∈ ℕ0
2		sqn5ii.2	⊢ ( 𝐴 + 1 ) = 𝐵
3		sqn5ii.3	⊢ ( 𝐴 · 𝐵 ) = 𝐶
4	1	sqn5i	⊢ ( ; 𝐴 5 · ; 𝐴 5 ) = ; ; ( 𝐴 · ( 𝐴 + 1 ) ) 2 5
5	2	oveq2i	⊢ ( 𝐴 · ( 𝐴 + 1 ) ) = ( 𝐴 · 𝐵 )
6	5 3	eqtri	⊢ ( 𝐴 · ( 𝐴 + 1 ) ) = 𝐶
7	6	deceq1i	⊢ ; ( 𝐴 · ( 𝐴 + 1 ) ) 2 = ; 𝐶 2
8	7	deceq1i	⊢ ; ; ( 𝐴 · ( 𝐴 + 1 ) ) 2 5 = ; ; 𝐶 2 5
9	4 8	eqtri	⊢ ( ; 𝐴 5 · ; 𝐴 5 ) = ; ; 𝐶 2 5