Metamath Proof Explorer

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