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	$$⊢A\in {\mathbb{N}}_0$$
Assertion	sqn5i	Could not format assertion : No typesetting found for |- ( ; A 5 x. ; A 5 ) = ; ; ( A x. ( A + 1 ) ) 2 5 with typecode |-

Proof

Step	Hyp	Ref	Expression
1		sqn5i.1	$$⊢A\in {\mathbb{N}}_0$$
2		0nn0	$$⊢0\in {\mathbb{N}}_0$$
3	1 2	deccl	Could not format ; A 0 e. NN0 : No typesetting found for |- ; A 0 e. NN0 with typecode |-
4	3	nn0cni	Could not format ; A 0 e. CC : No typesetting found for |- ; A 0 e. CC with typecode |-
5		5cn	$$⊢5\in ℂ$$
6		5nn0	$$⊢5\in {\mathbb{N}}_0$$
7		eqid	Could not format ; A 0 = ; A 0 : No typesetting found for |- ; A 0 = ; A 0 with typecode |-
8	5	addid2i	$$⊢0+5=5$$
9	1 2 6 7 8	decaddi	Could not format ( ; A 0 + 5 ) = ; A 5 : No typesetting found for |- ( ; A 0 + 5 ) = ; A 5 with typecode |-
10		eqid	Could not format ; A 5 = ; A 5 : No typesetting found for |- ; A 5 = ; A 5 with typecode |-
11		eqid	$$⊢A+1=A+1$$
12		5p5e10	$$⊢5+5=10$$
13	1 6 6 10 11 12	decaddci2	Could not format ( ; A 5 + 5 ) = ; ( A + 1 ) 0 : No typesetting found for |- ( ; A 5 + 5 ) = ; ( A + 1 ) 0 with typecode |-
14	4 5 9 13	sqmid3api	Could not format ( ; A 5 x. ; A 5 ) = ( ( ; A 0 x. ; ( A + 1 ) 0 ) + ( 5 x. 5 ) ) : No typesetting found for |- ( ; A 5 x. ; A 5 ) = ( ( ; A 0 x. ; ( A + 1 ) 0 ) + ( 5 x. 5 ) ) with typecode |-
15		2nn0	$$⊢2\in {\mathbb{N}}_0$$
16		5t5e25	$$⊢5\cdot 5=25$$
17		peano2nn0	$$⊢A\in {\mathbb{N}}_0\to A+1\in {\mathbb{N}}_0$$
18	1 17	ax-mp	$$⊢A+1\in {\mathbb{N}}_0$$
19	18 2	deccl	Could not format ; ( A + 1 ) 0 e. NN0 : No typesetting found for |- ; ( A + 1 ) 0 e. NN0 with typecode |-
20	1 18	nn0mulcli	$$⊢A\left(A+1\right)\in {\mathbb{N}}_0$$
21	1 18 2	decmulnc	Could not format ( A x. ; ( A + 1 ) 0 ) = ; ( A x. ( A + 1 ) ) ( A x. 0 ) : No typesetting found for |- ( A x. ; ( A + 1 ) 0 ) = ; ( A x. ( A + 1 ) ) ( A x. 0 ) with typecode |-
22	1	nn0cni	$$⊢A\in ℂ$$
23	22	mul01i	$$⊢A\cdot 0=0$$
24	23	deceq2i	Could not format ; ( A x. ( A + 1 ) ) ( A x. 0 ) = ; ( A x. ( A + 1 ) ) 0 : No typesetting found for |- ; ( A x. ( A + 1 ) ) ( A x. 0 ) = ; ( A x. ( A + 1 ) ) 0 with typecode |-
25	21 24	eqtri	Could not format ( A x. ; ( A + 1 ) 0 ) = ; ( A x. ( A + 1 ) ) 0 : No typesetting found for |- ( A x. ; ( A + 1 ) 0 ) = ; ( A x. ( A + 1 ) ) 0 with typecode |-
26		2cn	$$⊢2\in ℂ$$
27	26	addid2i	$$⊢0+2=2$$
28	20 2 15 25 27	decaddi	Could not format ( ( A x. ; ( A + 1 ) 0 ) + 2 ) = ; ( A x. ( A + 1 ) ) 2 : No typesetting found for |- ( ( A x. ; ( A + 1 ) 0 ) + 2 ) = ; ( A x. ( A + 1 ) ) 2 with typecode |-
29	19	nn0cni	Could not format ; ( A + 1 ) 0 e. CC : No typesetting found for |- ; ( A + 1 ) 0 e. CC with typecode |-
30	29	mul02i	Could not format ( 0 x. ; ( A + 1 ) 0 ) = 0 : No typesetting found for |- ( 0 x. ; ( A + 1 ) 0 ) = 0 with typecode |-
31	30	oveq1i	Could not format ( ( 0 x. ; ( A + 1 ) 0 ) + 5 ) = ( 0 + 5 ) : No typesetting found for |- ( ( 0 x. ; ( A + 1 ) 0 ) + 5 ) = ( 0 + 5 ) with typecode |-
32	31 8	eqtri	Could not format ( ( 0 x. ; ( A + 1 ) 0 ) + 5 ) = 5 : No typesetting found for |- ( ( 0 x. ; ( A + 1 ) 0 ) + 5 ) = 5 with typecode |-
33	1 2 15 6 7 16 19 28 32	decma	Could not format ( ( ; A 0 x. ; ( A + 1 ) 0 ) + ( 5 x. 5 ) ) = ; ; ( A x. ( A + 1 ) ) 2 5 : No typesetting found for |- ( ( ; A 0 x. ; ( A + 1 ) 0 ) + ( 5 x. 5 ) ) = ; ; ( A x. ( A + 1 ) ) 2 5 with typecode |-
34	14 33	eqtri	Could not format ( ; A 5 x. ; A 5 ) = ; ; ( A x. ( A + 1 ) ) 2 5 : No typesetting found for |- ( ; A 5 x. ; A 5 ) = ; ; ( A x. ( A + 1 ) ) 2 5 with typecode |-