Step |
Hyp |
Ref |
Expression |
1 |
|
sqn5i.1 |
|
2 |
|
sqn5ii.2 |
|
3 |
|
sqn5ii.3 |
|
4 |
1
|
sqn5i |
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 |- |
5 |
2
|
oveq2i |
|
6 |
5 3
|
eqtri |
|
7 |
6
|
deceq1i |
Could not format ; ( A x. ( A + 1 ) ) 2 = ; C 2 : No typesetting found for |- ; ( A x. ( A + 1 ) ) 2 = ; C 2 with typecode |- |
8 |
7
|
deceq1i |
Could not format ; ; ( A x. ( A + 1 ) ) 2 5 = ; ; C 2 5 : No typesetting found for |- ; ; ( A x. ( A + 1 ) ) 2 5 = ; ; C 2 5 with typecode |- |
9 |
4 8
|
eqtri |
Could not format ( ; A 5 x. ; A 5 ) = ; ; C 2 5 : No typesetting found for |- ( ; A 5 x. ; A 5 ) = ; ; C 2 5 with typecode |- |