let a, b be Nat; :: thesis: for t being Integer st b |^ 2 = ((2 * a) + t) * t holds
ex c being Nat st (a |^ 2) + (b |^ 2) = c |^ 2

let t be Integer; :: thesis: ( b |^ 2 = ((2 * a) + t) * t implies ex c being Nat st (a |^ 2) + (b |^ 2) = c |^ 2 )
assume b |^ 2 = ((2 * a) + t) * t ; :: thesis: ex c being Nat st (a |^ 2) + (b |^ 2) = c |^ 2
then A1: b |^ 2 = ((a + t) + a) * ((a + t) - a)
.= ((a + t) |^ 2) - (a |^ 2) by NEWTON01:1 ;
|.(a + t).| in NAT by INT_1:3;
then consider c being Nat such that
A2: c = |.(a + t).| ;
( c |^ 2 = (a + t) |^ 2 or c |^ 2 = (- (a + t)) |^ 2 ) by ;
then c |^ 2 = (a + t) |^ 2 by WSIERP_1:1;
hence ex c being Nat st (a |^ 2) + (b |^ 2) = c |^ 2 by A1; :: thesis: verum
{"found_math": false, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 0, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0, "url": "http://mizar.uwb.edu.pl/version/current/html/proofs/newton02/91", "fetch_time": 1571773063000000000, "content_mime_type": "text/plain", "warc_filename": "crawl-data/CC-MAIN-2019-43/segments/1570987823061.83/warc/CC-MAIN-20191022182744-20191022210244-00156.warc.gz", "warc_record_offset": 128042167, "warc_record_length": 1709, "token_count": 350, "char_count": 701, "score": 3.609375, "int_score": 4, "crawl": "CC-MAIN-2019-43", "snapshot_type": "latest", "language": "en", "language_score": 0.7466076612472534, "file_path": "/sailhome/yjruan/project/latent-lm/data/processed/finemath-4plus/finemath-4plus/train-00008-of-00064.parquet"}