metamath/valid/mathd-algebra-247.mm

${
  mathd-algebra-247.0 $e |- ( ph -> T e. RR ) $.
  mathd-algebra-247.1 $e |- ( ph -> S e. RR ) $.
  mathd-algebra-247.2 $e |- ( ph -> N e. ZZ ) $.
  mathd-algebra-247.3 $e |- ( ph -> T = ( ( 2 x. S ) - ( S ^ 2 ) ) ) $.
  mathd-algebra-247.4 $e |- ( ph -> S = ( ( ( N ^ 2 ) - ( 2 ^ N ) ) + 1 ) ) $.
  mathd-algebra-247.5 $e |- ( ph -> N = 3 ) $.
  $( (Contributed by Kunhao Zheng, 1-Jun-2021.) $)
  mathd-algebra-247 $p |- ( ph -> T = 0 ) $=
( c2 wceq cc0 cexp co cmin c1 caddc c9 c4 c8 c3 oveq1d sq3 syl6eq oveq2d wa cu2 
wi oveq12 9cn 8cn ax-1cn 8p1e9 subaddrii oveq1i 1p1e2 eqtri mp2and cmul a1i 
eqtrd adantr simpr 2t2e4 sq2 cc wcel 4cn subidd eqeq1d syl5ibrcom mpdan ) 
ABKLZCMLABDKNOZKDNOZPOZQROZKIAVOSLZVPUALZVRKLZAVOUBKNOSADUBKNJUCUDUEAVPKU 
BNOUAADUBKNJUFUHUEVSVTUGZWAUIAWBVRSUAPOZQROZKWBVQWCQRVOSVPUAPUJUCWDQQROKWCQ 
QRSUAQUKULUMUNUOUPUQURUEVAUSVBAVNUGZCKBUTOZBKNOZPOZMACWHLVNHVCWEWFTLZWGTLZW 
HMLZWEWFKKUTOTWEBKKUTAVNVDZUFVEUEWEWGKKNOTWEBKKNWLUCVFUEAWIWJUGZWKUIVNAWKWM 
TTPOZMLATTVGVHAVIVAVJWMWHWNMWFTWGTPUJVKVLVCUSVBVM $.
$}