This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sqn5i

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
Hypothesis sqn5i.1 ⊢ 𝐴 ∈ ℕ0
Assertion sqn5i ( 𝐴 5 · 𝐴 5 ) = ( 𝐴 · ( 𝐴 + 1 ) ) 2 5

Proof

Step Hyp Ref Expression
1 sqn5i.1 ⊢ 𝐴 ∈ ℕ0
2 0nn0 ⊢ 0 ∈ ℕ0
3 1 2 deccl ⊢ 𝐴 0 ∈ ℕ0
4 3 nn0cni ⊢ 𝐴 0 ∈ ℂ
5 5cn ⊢ 5 ∈ ℂ
6 5nn0 ⊢ 5 ∈ ℕ0
7 eqid ⊢ 𝐴 0 = 𝐴 0
8 5 addlidi ⊢ ( 0 + 5 ) = 5
9 1 2 6 7 8 decaddi ⊢ ( 𝐴 0 + 5 ) = 𝐴 5
10 eqid ⊢ 𝐴 5 = 𝐴 5
11 eqid ⊢ ( 𝐴 + 1 ) = ( 𝐴 + 1 )
12 5p5e10 ⊢ ( 5 + 5 ) = 1 0
13 1 6 6 10 11 12 decaddci2 ⊢ ( 𝐴 5 + 5 ) = ( 𝐴 + 1 ) 0
14 4 5 9 13 sqmid3api ⊢ ( 𝐴 5 · 𝐴 5 ) = ( ( 𝐴 0 · ( 𝐴 + 1 ) 0 ) + ( 5 · 5 ) )
15 2nn0 ⊢ 2 ∈ ℕ0
16 5t5e25 ⊢ ( 5 · 5 ) = 2 5
17 peano2nn0 ⊢ ( 𝐴 ∈ ℕ0 → ( 𝐴 + 1 ) ∈ ℕ0 )
18 1 17 ax-mp ⊢ ( 𝐴 + 1 ) ∈ ℕ0
19 18 2 deccl ⊢ ( 𝐴 + 1 ) 0 ∈ ℕ0
20 1 18 nn0mulcli ⊢ ( 𝐴 · ( 𝐴 + 1 ) ) ∈ ℕ0
21 1 18 2 decmulnc ⊢ ( 𝐴 · ( 𝐴 + 1 ) 0 ) = ( 𝐴 · ( 𝐴 + 1 ) ) ( 𝐴 · 0 )
22 1 nn0cni ⊢ 𝐴 ∈ ℂ
23 22 mul01i ⊢ ( 𝐴 · 0 ) = 0
24 23 deceq2i ⊢ ( 𝐴 · ( 𝐴 + 1 ) ) ( 𝐴 · 0 ) = ( 𝐴 · ( 𝐴 + 1 ) ) 0
25 21 24 eqtri ⊢ ( 𝐴 · ( 𝐴 + 1 ) 0 ) = ( 𝐴 · ( 𝐴 + 1 ) ) 0
26 2cn ⊢ 2 ∈ ℂ
27 26 addlidi ⊢ ( 0 + 2 ) = 2
28 20 2 15 25 27 decaddi ⊢ ( ( 𝐴 · ( 𝐴 + 1 ) 0 ) + 2 ) = ( 𝐴 · ( 𝐴 + 1 ) ) 2
29 19 nn0cni ⊢ ( 𝐴 + 1 ) 0 ∈ ℂ
30 29 mul02i ⊢ ( 0 · ( 𝐴 + 1 ) 0 ) = 0
31 30 oveq1i ⊢ ( ( 0 · ( 𝐴 + 1 ) 0 ) + 5 ) = ( 0 + 5 )
32 31 8 eqtri ⊢ ( ( 0 · ( 𝐴 + 1 ) 0 ) + 5 ) = 5
33 1 2 15 6 7 16 19 28 32 decma ⊢ ( ( 𝐴 0 · ( 𝐴 + 1 ) 0 ) + ( 5 · 5 ) ) = ( 𝐴 · ( 𝐴 + 1 ) ) 2 5
34 14 33 eqtri ⊢ ( 𝐴 5 · 𝐴 5 ) = ( 𝐴 · ( 𝐴 + 1 ) ) 2 5