Very cool page! The only interesting step is step 32, which is just an application of http://us.metamath.org/mpeuni/geoisum1c.html http://us.metamath.org/mpeun

Very cool page! The only interesting step is step 32, which is just an application of http://us.metamath.org/mpeuni/geoisum1c.html http://us.metamath.org/mpeuni/geoisum1c.html, whose only interesting step is step 21 which is just an application of http://us.metamath.org/mpeuni/geoisum1.html http://us.metamath.org/mpeuni/geoisum1.html. They key steps for that are http://us.metamath.org/mpeuni/geolim2.html http://us.metamath.org/mpeuni/geolim2.html and http://us.metamath.org/mpeuni/isumclim.html http://us.metamath.org/mpeuni/isumclim.html , which is indeed the crux of the issue