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 deceq1i ⊢ ( 𝐴 · ( 𝐴 + 1 ) ) 2 = ( 𝐴 · 𝐵 ) 2
7 6 deceq1i ⊢ ( 𝐴 · ( 𝐴 + 1 ) ) 2 5 = ( 𝐴 · 𝐵 ) 2 5
8 3 deceq1i ⊢ ( 𝐴 · 𝐵 ) 2 = 𝐶 2
9 8 deceq1i ⊢ ( 𝐴 · 𝐵 ) 2 5 = 𝐶 2 5
10 4 7 9 3eqtri ⊢ ( 𝐴 5 · 𝐴 5 ) = 𝐶 2 5