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 ⊢ A ∈ ℕ 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 ∈ ℕ 0
2 0nn0 ⊢ 0 ∈ ℕ 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 ∈ ℂ
6 5nn0 ⊢ 5 ∈ ℕ 0
7 eqid Could not format ; A 0 = ; A 0 : No typesetting found for |- ; A 0 = ; A 0 with typecode |-
8 5 addlidi ⊢ 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 ∈ ℕ 0
16 5t5e25 ⊢ 5 ⋅ 5 = 25
17 peano2nn0 ⊢ A ∈ ℕ 0 → A + 1 ∈ ℕ 0
18 1 17 ax-mp ⊢ A + 1 ∈ ℕ 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 ⁢ A + 1 ∈ ℕ 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 ∈ ℂ
23 22 mul01i ⊢ A ⋅ 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 ∈ ℂ
27 26 addlidi ⊢ 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 |-