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	addid2i	⊢ ( 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	addid2i	⊢ ( 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