:: PYTHTRIP semantic presentation begin definition let m, n be Nat; redefine pred m,n are_relative_prime means :Def1: :: PYTHTRIP:def 1 for k being Nat st k divides m & k divides n holds k = 1; compatibility ( m,n are_relative_prime iff for k being Nat st k divides m & k divides n holds k = 1 ) proof hereby ::_thesis: ( ( for k being Nat st k divides m & k divides n holds k = 1 ) implies m,n are_relative_prime ) assume m,n are_relative_prime ; ::_thesis: for k being Nat st k divides m & k divides n holds k = 1 then A1: m gcd n = 1 by INT_2:def_3; let k be Nat; ::_thesis: ( k divides m & k divides n implies k = 1 ) assume ( k divides m & k divides n ) ; ::_thesis: k = 1 then k divides 1 by A1, NAT_D:def_5; hence k = 1 by WSIERP_1:15; ::_thesis: verum end; assume for k being Nat st k divides m & k divides n holds k = 1 ; ::_thesis: m,n are_relative_prime then A2: for k being Nat st k divides m & k divides n holds k divides 1 ; ( 1 divides m & 1 divides n ) by NAT_D:6; hence m gcd n = 1 by A2, NAT_D:def_5; :: according to INT_2:def_3 ::_thesis: verum end; end; :: deftheorem Def1 defines are_relative_prime PYTHTRIP:def_1_:_ for m, n being Nat holds ( m,n are_relative_prime iff for k being Nat st k divides m & k divides n holds k = 1 ); definition let m, n be Nat; redefine pred m,n are_relative_prime means :Def2: :: PYTHTRIP:def 2 for p being prime Nat holds ( not p divides m or not p divides n ); compatibility ( m,n are_relative_prime iff for p being prime Nat holds ( not p divides m or not p divides n ) ) proof hereby ::_thesis: ( ( for p being prime Nat holds ( not p divides m or not p divides n ) ) implies m,n are_relative_prime ) assume A1: m,n are_relative_prime ; ::_thesis: for p being prime Nat st p divides m holds not p divides n let p be prime Nat; ::_thesis: ( p divides m implies not p divides n ) assume ( p divides m & p divides n ) ; ::_thesis: contradiction then p = 1 by A1, Def1; hence contradiction by INT_2:def_4; ::_thesis: verum end; assume A2: for p being prime Nat holds ( not p divides m or not p divides n ) ; ::_thesis: m,n are_relative_prime let k be Nat; :: according to PYTHTRIP:def_1 ::_thesis: ( k divides m & k divides n implies k = 1 ) assume A3: ( k divides m & k divides n ) ; ::_thesis: k = 1 percases ( k = 0 or k = 1 or k > 1 ) by NAT_1:25; suppose k = 0 ; ::_thesis: k = 1 then ( m = 0 & n = 0 ) by A3, INT_2:3; hence k = 1 by A2, INT_2:28, NAT_D:6; ::_thesis: verum end; suppose k = 1 ; ::_thesis: k = 1 hence k = 1 ; ::_thesis: verum end; suppose k > 1 ; ::_thesis: k = 1 then k >= 1 + 1 by NAT_1:13; then consider p being Element of NAT such that A4: p is prime and A5: p divides k by INT_2:31; reconsider p9 = p as prime Element of NAT by A4; ( p9 divides m & p9 divides n ) by A3, A5, NAT_D:4; hence k = 1 by A2; ::_thesis: verum end; end; end; end; :: deftheorem Def2 defines are_relative_prime PYTHTRIP:def_2_:_ for m, n being Nat holds ( m,n are_relative_prime iff for p being prime Nat holds ( not p divides m or not p divides n ) ); begin definition let n be number ; attrn is square means :Def3: :: PYTHTRIP:def 3 ex m being Nat st n = m ^2 ; end; :: deftheorem Def3 defines square PYTHTRIP:def_3_:_ for n being number holds ( n is square iff ex m being Nat st n = m ^2 ); registration cluster square -> natural for set ; coherence for b1 being number st b1 is square holds b1 is natural proof let n be number ; ::_thesis: ( n is square implies n is natural ) assume n is square ; ::_thesis: n is natural then ex m being Nat st n = m ^2 by Def3; hence n is natural ; ::_thesis: verum end; end; registration let n be Nat; clustern ^2 -> square ; coherence n ^2 is square by Def3; end; registration cluster epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even square for Element of NAT ; existence ex b1 being Element of NAT st ( b1 is even & b1 is square ) proof take 0 ; ::_thesis: ( 0 is even & 0 is square ) 0 = 2 * (0 ^2) ; hence ( 0 is even & 0 is square ) ; ::_thesis: verum end; end; registration cluster epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer odd square for Element of NAT ; existence ex b1 being Element of NAT st ( b1 is odd & b1 is square ) proof take 1 ; ::_thesis: ( 1 is odd & 1 is square ) 1 ^2 = (2 * 0) + 1 ; hence ( 1 is odd & 1 is square ) ; ::_thesis: verum end; end; registration clusterV24() V25() ext-real integer even square for set ; existence ex b1 being Integer st ( b1 is even & b1 is square ) proof set n = the even square Element of NAT ; take the even square Element of NAT ; ::_thesis: ( the even square Element of NAT is even & the even square Element of NAT is square ) thus ( the even square Element of NAT is even & the even square Element of NAT is square ) ; ::_thesis: verum end; end; registration clusterV24() V25() ext-real integer odd square for set ; existence ex b1 being Integer st ( b1 is odd & b1 is square ) proof set n = the odd square Element of NAT ; take the odd square Element of NAT ; ::_thesis: ( the odd square Element of NAT is odd & the odd square Element of NAT is square ) thus ( the odd square Element of NAT is odd & the odd square Element of NAT is square ) ; ::_thesis: verum end; end; registration let m, n be square number ; clusterm * n -> square ; coherence m * n is square proof consider n9 being Nat such that A1: n = n9 ^2 by Def3; consider m9 being Nat such that A2: m = m9 ^2 by Def3; m * n = (m9 * n9) ^2 by A2, A1; hence m * n is square ; ::_thesis: verum end; end; theorem Th1: :: PYTHTRIP:1 for m, n being Element of NAT st m * n is square & m,n are_relative_prime holds ( m is square & n is square ) proof let m, n be Element of NAT ; ::_thesis: ( m * n is square & m,n are_relative_prime implies ( m is square & n is square ) ) defpred S1[ Nat] means for m, n being Element of NAT st m * n = \$1 & m * n is square & m,n are_relative_prime holds ( m is square & n is square ); A1: for mn being Nat st ( for k being Nat st k < mn holds S1[k] ) holds S1[mn] proof let mn be Nat; ::_thesis: ( ( for k being Nat st k < mn holds S1[k] ) implies S1[mn] ) assume A2: for k being Nat st k < mn holds for m, n being Element of NAT st m * n = k & m * n is square & m,n are_relative_prime holds ( m is square & n is square ) ; ::_thesis: S1[mn] let m, n be Element of NAT ; ::_thesis: ( m * n = mn & m * n is square & m,n are_relative_prime implies ( m is square & n is square ) ) assume A3: m * n = mn ; ::_thesis: ( not m * n is square or not m,n are_relative_prime or ( m is square & n is square ) ) assume m * n is square ; ::_thesis: ( not m,n are_relative_prime or ( m is square & n is square ) ) then consider mn9 being Nat such that A4: mn = mn9 ^2 by A3, Def3; assume A5: m,n are_relative_prime ; ::_thesis: ( m is square & n is square ) then A6: m gcd n = 1 ^2 by INT_2:def_3; percases ( m * n = 0 or m * n = 1 ^2 or mn > 1 ) by A3, NAT_1:25; supposeA7: m * n = 0 ; ::_thesis: ( m is square & n is square ) hereby ::_thesis: verum percases ( m = 0 ^2 or n = 0 ^2 ) by A7, XCMPLX_1:6; suppose m = 0 ^2 ; ::_thesis: ( m is square & n is square ) hence ( m is square & n is square ) by A6, NEWTON:52; ::_thesis: verum end; suppose n = 0 ^2 ; ::_thesis: ( m is square & n is square ) hence ( m is square & n is square ) by A6, NEWTON:52; ::_thesis: verum end; end; end; end; suppose m * n = 1 ^2 ; ::_thesis: ( m is square & n is square ) hence ( m is square & n is square ) by NAT_1:15; ::_thesis: verum end; supposeA8: mn > 1 ; ::_thesis: ( m is square & n is square ) then mn >= 1 + 1 by NAT_1:13; then consider p9 being Element of NAT such that A9: p9 is prime and A10: p9 divides mn by INT_2:31; reconsider p = p9 as prime Element of NAT by A9; p divides mn9 by A4, A10, NEWTON:80; then consider mn99 being Nat such that A11: mn9 = p * mn99 by NAT_D:def_3; A12: p > 1 by INT_2:def_4; then p * p > p by XREAL_1:155; then A13: p * p > 1 by A12, XXREAL_0:2; A14: n > 0 by A3, A8; A15: p <> 0 by INT_2:def_4; A16: m > 0 by A3, A8; hereby ::_thesis: verum percases ( p divides m or p divides n ) by A3, A10, NEWTON:80; supposeA17: p divides m ; ::_thesis: ( m is square & n is square ) then A18: not p divides n by A5, Def2; consider m9 being Nat such that A19: m = p * m9 by A17, NAT_D:def_3; p * (m9 * n) = p * (p * (mn99 * mn99)) by A3, A4, A11, A19; then m9 * n = p * (mn99 * mn99) by A15, XCMPLX_1:5; then p divides m9 * n by NAT_D:def_3; then p divides m9 by A18, NEWTON:80; then consider m99 being Nat such that A20: m9 = p * m99 by NAT_D:def_3; reconsider m99 = m99 as Element of NAT by ORDINAL1:def_12; A21: m99 <> 0 by A3, A8, A19, A20; p * (p * (m99 * n)) = p * (p * (mn99 * mn99)) by A3, A4, A11, A19, A20; then p * (m99 * n) = p * (mn99 * mn99) by A15, XCMPLX_1:5; then A22: m99 * n = mn99 ^2 by A15, XCMPLX_1:5; m = (p * p) * m99 by A19, A20; then m99 divides m by NAT_D:def_3; then m99 gcd n = 1 by A6, WSIERP_1:16; then A23: m99,n are_relative_prime by INT_2:def_3; m = (p * p) * m99 by A19, A20; then 1 * m99 < m by A13, A21, XREAL_1:98; then A24: m99 * n < mn by A3, A14, A21, XREAL_1:98; then m99 is square by A2, A22, A23; then consider m999 being Nat such that A25: m99 = m999 ^2 by Def3; m = (p * m999) ^2 by A19, A20, A25; hence ( m is square & n is square ) by A2, A24, A22, A23; ::_thesis: verum end; supposeA26: p divides n ; ::_thesis: ( m is square & n is square ) then A27: not p divides m by A5, Def2; consider n9 being Nat such that A28: n = p * n9 by A26, NAT_D:def_3; p * (m * n9) = p * (p * (mn99 * mn99)) by A3, A4, A11, A28; then m * n9 = p * (mn99 * mn99) by A15, XCMPLX_1:5; then p divides m * n9 by NAT_D:def_3; then p divides n9 by A27, NEWTON:80; then consider n99 being Nat such that A29: n9 = p * n99 by NAT_D:def_3; reconsider n99 = n99 as Element of NAT by ORDINAL1:def_12; A30: n99 <> 0 by A3, A8, A28, A29; p * (p * (m * n99)) = p * (p * (mn99 * mn99)) by A3, A4, A11, A28, A29; then p * (m * n99) = p * (mn99 * mn99) by A15, XCMPLX_1:5; then A31: m * n99 = mn99 ^2 by A15, XCMPLX_1:5; n = (p * p) * n99 by A28, A29; then n99 divides n by NAT_D:def_3; then m gcd n99 = 1 by A6, WSIERP_1:16; then A32: m,n99 are_relative_prime by INT_2:def_3; n = (p * p) * n99 by A28, A29; then 1 * n99 < n by A13, A30, XREAL_1:98; then A33: m * n99 < mn by A3, A16, A30, XREAL_1:98; then n99 is square by A2, A31, A32; then consider n999 being Nat such that A34: n99 = n999 ^2 by Def3; n = (p * n999) ^2 by A28, A29, A34; hence ( m is square & n is square ) by A2, A33, A31, A32; ::_thesis: verum end; end; end; end; end; end; for mn being Nat holds S1[mn] from NAT_1:sch_4(A1); hence ( m * n is square & m,n are_relative_prime implies ( m is square & n is square ) ) ; ::_thesis: verum end; registration let i be Integer; clusteri ^2 -> integer ; coherence i ^2 is integer ; end; registration let i be even Integer; clusteri ^2 -> even ; coherence i ^2 is even ; end; registration let i be odd Integer; clusteri ^2 -> odd ; coherence not i ^2 is even ; end; theorem :: PYTHTRIP:2 for i being Integer holds ( i is even iff i ^2 is even ) ; theorem Th3: :: PYTHTRIP:3 for i being Integer st i is even holds (i ^2) mod 4 = 0 proof let i be Integer; ::_thesis: ( i is even implies (i ^2) mod 4 = 0 ) given i9 being Integer such that A1: i = 2 * i9 ; :: according to INT_1:def_3,ABIAN:def_1 ::_thesis: (i ^2) mod 4 = 0 i ^2 = (4 * (i9 ^2)) + 0 by A1; hence (i ^2) mod 4 = 0 mod 4 by EULER_1:12 .= 0 by NAT_D:24 ; ::_thesis: verum end; theorem Th4: :: PYTHTRIP:4 for i being Integer st i is odd holds (i ^2) mod 4 = 1 proof let i be Integer; ::_thesis: ( i is odd implies (i ^2) mod 4 = 1 ) assume i is odd ; ::_thesis: (i ^2) mod 4 = 1 then consider i9 being Integer such that A1: i = (2 * i9) + 1 by ABIAN:1; i ^2 = (4 * ((i9 ^2) + i9)) + 1 by A1; hence (i ^2) mod 4 = 1 mod 4 by EULER_1:12 .= 1 by NAT_D:24 ; ::_thesis: verum end; registration let m, n be odd square Integer; clusterm + n -> non square ; coherence not m + n is square proof reconsider n99 = n as Element of NAT by ORDINAL1:def_12; reconsider m99 = m as Element of NAT by ORDINAL1:def_12; consider m9 being Nat such that A1: m = m9 ^2 by Def3; A2: m9 is odd by A1; consider n9 being Nat such that A3: n = n9 ^2 by Def3; A4: n9 is odd by A3; A5: (m99 + n99) mod 4 = ((m99 mod 4) + (n99 mod 4)) mod 4 by EULER_2:6 .= (1 + (n99 mod 4)) mod 4 by A1, A2, Th4 .= (1 + 1) mod 4 by A3, A4, Th4 .= 2 by NAT_D:24 ; hereby ::_thesis: verum assume m + n is square ; ::_thesis: contradiction then consider mn9 being Nat such that A6: m + n = mn9 ^2 by Def3; mn9 is even by A6; hence contradiction by A5, A6, Th3; ::_thesis: verum end; end; end; theorem Th5: :: PYTHTRIP:5 for m, n being Element of NAT st m ^2 = n ^2 holds m = n proof let m, n be Element of NAT ; ::_thesis: ( m ^2 = n ^2 implies m = n ) assume A1: m ^2 = n ^2 ; ::_thesis: m = n percases ( m = n or m = - n ) by A1, SQUARE_1:40; suppose m = n ; ::_thesis: m = n hence m = n ; ::_thesis: verum end; supposeA2: m = - n ; ::_thesis: m = n then m = - 0 ; hence m = n by A2; ::_thesis: verum end; end; end; theorem Th6: :: PYTHTRIP:6 for m, n being Element of NAT holds ( m divides n iff m ^2 divides n ^2 ) proof let m, n be Element of NAT ; ::_thesis: ( m divides n iff m ^2 divides n ^2 ) defpred S1[ Nat] means for n being Element of NAT holds ( \$1 divides n iff \$1 ^2 divides n ^2 ); A1: for m being Nat st ( for k being Nat st k < m holds S1[k] ) holds S1[m] proof let m be Nat; ::_thesis: ( ( for k being Nat st k < m holds S1[k] ) implies S1[m] ) assume A2: for k being Nat st k < m holds for n being Element of NAT holds ( k divides n iff k ^2 divides n ^2 ) ; ::_thesis: S1[m] let n be Element of NAT ; ::_thesis: ( m divides n iff m ^2 divides n ^2 ) hereby ::_thesis: ( m ^2 divides n ^2 implies m divides n ) assume m divides n ; ::_thesis: m ^2 divides n ^2 then consider k9 being Nat such that A3: n = m * k9 by NAT_D:def_3; n ^2 = (m ^2) * (k9 ^2) by A3; hence m ^2 divides n ^2 by NAT_D:def_3; ::_thesis: verum end; assume A4: m ^2 divides n ^2 ; ::_thesis: m divides n percases ( m = 0 or m = 1 or m > 1 ) by NAT_1:25; suppose m = 0 ; ::_thesis: m divides n then n ^2 = 0 by A4, INT_2:3; then n = 0 by XCMPLX_1:6; hence m divides n by NAT_D:6; ::_thesis: verum end; suppose m = 1 ; ::_thesis: m divides n hence m divides n by NAT_D:6; ::_thesis: verum end; supposeA5: m > 1 ; ::_thesis: m divides n consider k9 being Nat such that A6: n ^2 = (m ^2) * k9 by A4, NAT_D:def_3; m >= 1 + 1 by A5, NAT_1:13; then consider p9 being Element of NAT such that A7: p9 is prime and A8: p9 divides m by INT_2:31; reconsider p = p9 as prime Element of NAT by A7; consider m9 being Nat such that A9: m = p * m9 by A8, NAT_D:def_3; reconsider m9 = m9 as Element of NAT by ORDINAL1:def_12; m ^2 = (m * m9) * p by A9; then p divides m ^2 by NAT_D:def_3; then p divides n ^2 by A4, NAT_D:4; then p divides n by NEWTON:80; then consider n9 being Nat such that A10: n = p * n9 by NAT_D:def_3; A11: p > 1 by INT_2:def_4; then A12: p ^2 > 0 by SQUARE_1:12; reconsider n9 = n9 as Element of NAT by ORDINAL1:def_12; (p ^2) * (n9 ^2) = (p ^2) * ((m9 ^2) * k9) by A9, A10, A6; then n9 ^2 = (m9 ^2) * k9 by A12, XCMPLX_1:5; then A13: m9 ^2 divides n9 ^2 by NAT_D:def_3; p * m9 > 1 * m9 by A5, A9, A11, XREAL_1:98; then m9 divides n9 by A2, A9, A13; then consider k being Nat such that A14: n9 = m9 * k by NAT_D:def_3; n = m * k by A9, A10, A14; hence m divides n by NAT_D:def_3; ::_thesis: verum end; end; end; for m being Nat holds S1[m] from NAT_1:sch_4(A1); hence ( m divides n iff m ^2 divides n ^2 ) ; ::_thesis: verum end; begin theorem Th7: :: PYTHTRIP:7 for m, n, k being Element of NAT holds ( ( m divides n or k = 0 ) iff k * m divides k * n ) proof let m, n, k be Element of NAT ; ::_thesis: ( ( m divides n or k = 0 ) iff k * m divides k * n ) hereby ::_thesis: ( not k * m divides k * n or m divides n or k = 0 ) assume A1: ( m divides n or k = 0 ) ; ::_thesis: k * m divides k * n percases ( m divides n or k = 0 ) by A1; suppose m divides n ; ::_thesis: k * m divides k * n then consider k9 being Nat such that A2: n = m * k9 by NAT_D:def_3; k * n = (k * m) * k9 by A2; hence k * m divides k * n by NAT_D:def_3; ::_thesis: verum end; suppose k = 0 ; ::_thesis: k * m divides k * n hence k * m divides k * n ; ::_thesis: verum end; end; end; assume A3: k * m divides k * n ; ::_thesis: ( m divides n or k = 0 ) now__::_thesis:_(_k_<>_0_implies_m_divides_n_) consider k9 being Nat such that A4: k * n = (k * m) * k9 by A3, NAT_D:def_3; assume A5: k <> 0 ; ::_thesis: m divides n k * n = k * (m * k9) by A4; then n = m * k9 by A5, XCMPLX_1:5; hence m divides n by NAT_D:def_3; ::_thesis: verum end; hence ( m divides n or k = 0 ) ; ::_thesis: verum end; theorem Th8: :: PYTHTRIP:8 for k, m, n being Element of NAT holds (k * m) gcd (k * n) = k * (m gcd n) proof let k, m, n be Element of NAT ; ::_thesis: (k * m) gcd (k * n) = k * (m gcd n) percases ( k <> 0 or k = 0 ) ; supposeA1: k <> 0 ; ::_thesis: (k * m) gcd (k * n) = k * (m gcd n) ( k divides k * m & k divides k * n ) by NAT_D:9; then k divides (k * m) gcd (k * n) by NAT_D:def_5; then consider k9 being Nat such that A2: (k * m) gcd (k * n) = k * k9 by NAT_D:def_3; reconsider k9 = k9 as Element of NAT by ORDINAL1:def_12; now__::_thesis:_(_k9_divides_m_&_k9_divides_n_&_(_for_p_being_Nat_st_p_divides_m_&_p_divides_n_holds_ p_divides_k9_)_) k * k9 divides k * m by A2, NAT_D:def_5; hence k9 divides m by A1, Th7; ::_thesis: ( k9 divides n & ( for p being Nat st p divides m & p divides n holds p divides k9 ) ) k * k9 divides k * n by A2, NAT_D:def_5; hence k9 divides n by A1, Th7; ::_thesis: for p being Nat st p divides m & p divides n holds p divides k9 let p be Nat; ::_thesis: ( p divides m & p divides n implies p divides k9 ) reconsider p9 = p as Element of NAT by ORDINAL1:def_12; assume ( p divides m & p divides n ) ; ::_thesis: p divides k9 then ( k * p9 divides k * m & k * p9 divides k * n ) by Th7; then k * p divides k * k9 by A2, NAT_D:def_5; then p9 divides k9 by A1, Th7; hence p divides k9 ; ::_thesis: verum end; hence (k * m) gcd (k * n) = k * (m gcd n) by A2, NAT_D:def_5; ::_thesis: verum end; suppose k = 0 ; ::_thesis: (k * m) gcd (k * n) = k * (m gcd n) hence (k * m) gcd (k * n) = k * (m gcd n) by NEWTON:52; ::_thesis: verum end; end; end; begin theorem Th9: :: PYTHTRIP:9 for X being set st ( for m being Element of NAT ex n being Element of NAT st ( n >= m & n in X ) ) holds X is infinite proof let X be set ; ::_thesis: ( ( for m being Element of NAT ex n being Element of NAT st ( n >= m & n in X ) ) implies X is infinite ) A1: now__::_thesis:_for_f_being_Function for_k_being_Element_of_NAT_holds_S1[k] let f be Function; ::_thesis: for k being Element of NAT holds S1[k] defpred S1[ Element of NAT ] means ex m being Element of NAT st for n being Element of NAT st n >= m holds not n in f .: \$1; A2: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume ex m being Element of NAT st for n being Element of NAT st n >= m holds not n in f .: k ; ::_thesis: S1[k + 1] then consider m being Element of NAT such that A3: for n being Element of NAT st n >= m holds not n in f .: k ; k + 1 = succ k by NAT_1:38 .= k \/ {k} by ORDINAL1:def_1 ; then A4: f .: (k + 1) = (f .: k) \/ (Im (f,k)) by RELAT_1:120; percases ( ( k in dom f & f . k in NAT ) or ( k in dom f & not f . k in NAT ) or not k in dom f ) ; supposeA5: ( k in dom f & f . k in NAT ) ; ::_thesis: S1[k + 1] then reconsider m9 = f . k as Element of NAT ; take max (m,(m9 + 1)) ; ::_thesis: for n being Element of NAT st n >= max (m,(m9 + 1)) holds not n in f .: (k + 1) let n be Element of NAT ; ::_thesis: ( n >= max (m,(m9 + 1)) implies not n in f .: (k + 1) ) assume A6: n >= max (m,(m9 + 1)) ; ::_thesis: not n in f .: (k + 1) then A7: not n in f .: k by A3, XXREAL_0:30; n >= m9 + 1 by A6, XXREAL_0:30; then n <> m9 by NAT_1:13; then A8: not n in {m9} by TARSKI:def_1; f .: (k + 1) = (f .: k) \/ {m9} by A4, A5, FUNCT_1:59; hence not n in f .: (k + 1) by A7, A8, XBOOLE_0:def_3; ::_thesis: verum end; supposeA9: ( k in dom f & not f . k in NAT ) ; ::_thesis: S1[k + 1] take m ; ::_thesis: for n being Element of NAT st n >= m holds not n in f .: (k + 1) set m9 = f . k; let n be Element of NAT ; ::_thesis: ( n >= m implies not n in f .: (k + 1) ) n <> f . k by A9; then A10: not n in {(f . k)} by TARSKI:def_1; assume n >= m ; ::_thesis: not n in f .: (k + 1) then A11: not n in f .: k by A3; f .: (k + 1) = (f .: k) \/ {(f . k)} by A4, A9, FUNCT_1:59; hence not n in f .: (k + 1) by A11, A10, XBOOLE_0:def_3; ::_thesis: verum end; suppose not k in dom f ; ::_thesis: S1[k + 1] then A12: dom f misses {k} by ZFMISC_1:50; take m ; ::_thesis: for n being Element of NAT st n >= m holds not n in f .: (k + 1) let n be Element of NAT ; ::_thesis: ( n >= m implies not n in f .: (k + 1) ) assume A13: n >= m ; ::_thesis: not n in f .: (k + 1) Im (f,k) = f .: ((dom f) /\ {k}) by RELAT_1:112 .= f .: {} by A12, XBOOLE_0:def_7 .= {} ; hence not n in f .: (k + 1) by A3, A4, A13; ::_thesis: verum end; end; end; A14: S1[ 0 ] proof take 0 ; ::_thesis: for n being Element of NAT st n >= 0 holds not n in f .: 0 let n be Element of NAT ; ::_thesis: ( n >= 0 implies not n in f .: 0 ) assume n >= 0 ; ::_thesis: not n in f .: 0 thus not n in f .: 0 ; ::_thesis: verum end; thus for k being Element of NAT holds S1[k] from NAT_1:sch_1(A14, A2); ::_thesis: verum end; now__::_thesis:_(_X_is_finite_implies_ex_m_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_n_>=_m_holds_ not_n_in_X_) assume X is finite ; ::_thesis: ex m being Element of NAT st for n being Element of NAT st n >= m holds not n in X then consider f being Function such that A15: rng f = X and A16: dom f in omega by FINSET_1:def_1; reconsider k = dom f as Element of NAT by A16; f .: k = X by A15, RELAT_1:113; hence ex m being Element of NAT st for n being Element of NAT st n >= m holds not n in X by A1; ::_thesis: verum end; hence ( ( for m being Element of NAT ex n being Element of NAT st ( n >= m & n in X ) ) implies X is infinite ) ; ::_thesis: verum end; begin theorem Th10: :: PYTHTRIP:10 for a, b being Element of NAT holds ( not a,b are_relative_prime or a is odd or b is odd ) proof let a, b be Element of NAT ; ::_thesis: ( not a,b are_relative_prime or a is odd or b is odd ) assume A1: a,b are_relative_prime ; ::_thesis: ( a is odd or b is odd ) assume a is even ; ::_thesis: b is odd then A2: 2 divides a by PEPIN:22; assume b is even ; ::_thesis: contradiction then 2 divides b by PEPIN:22; hence contradiction by A1, A2, Def1; ::_thesis: verum end; theorem Th11: :: PYTHTRIP:11 for a, b, c being Element of NAT st (a ^2) + (b ^2) = c ^2 & a,b are_relative_prime & a is odd holds ex m, n being Element of NAT st ( m <= n & a = (n ^2) - (m ^2) & b = (2 * m) * n & c = (n ^2) + (m ^2) ) proof let a, b, c be Element of NAT ; ::_thesis: ( (a ^2) + (b ^2) = c ^2 & a,b are_relative_prime & a is odd implies ex m, n being Element of NAT st ( m <= n & a = (n ^2) - (m ^2) & b = (2 * m) * n & c = (n ^2) + (m ^2) ) ) assume A1: (a ^2) + (b ^2) = c ^2 ; ::_thesis: ( not a,b are_relative_prime or not a is odd or ex m, n being Element of NAT st ( m <= n & a = (n ^2) - (m ^2) & b = (2 * m) * n & c = (n ^2) + (m ^2) ) ) assume A2: a,b are_relative_prime ; ::_thesis: ( not a is odd or ex m, n being Element of NAT st ( m <= n & a = (n ^2) - (m ^2) & b = (2 * m) * n & c = (n ^2) + (m ^2) ) ) assume a is odd ; ::_thesis: ex m, n being Element of NAT st ( m <= n & a = (n ^2) - (m ^2) & b = (2 * m) * n & c = (n ^2) + (m ^2) ) then reconsider a9 = a as odd Element of NAT ; b is even proof assume b is odd ; ::_thesis: contradiction then reconsider b9 = b as odd Element of NAT ; (a9 ^2) + (b9 ^2) = c ^2 by A1; hence contradiction ; ::_thesis: verum end; then reconsider b9 = b as even Element of NAT ; (a9 ^2) + (b9 ^2) = c ^2 by A1; then reconsider c9 = c as odd Element of NAT ; 2 divides c9 - a9 by ABIAN:def_1; then consider i being Integer such that A3: c9 - a9 = 2 * i by INT_1:def_3; c ^2 >= (a ^2) + 0 by A1, XREAL_1:6; then c >= a by SQUARE_1:16; then 2 * i >= 2 * 0 by A3, XREAL_1:48; then i >= 0 by XREAL_1:68; then reconsider m9 = i as Element of NAT by INT_1:3; consider n9 being Element of NAT such that A4: c9 + a9 = 2 * n9 by ABIAN:def_2; consider k9 being Element of NAT such that A5: b9 = 2 * k9 by ABIAN:def_2; A6: n9 * m9 = ((c + a) / 2) * ((c - a) / 2) by A4, A3 .= (b / 2) ^2 by A1 .= k9 ^2 by A5 ; A7: n9 + m9 = c by A4, A3; A8: n9,m9 are_relative_prime proof let p be prime Nat; :: according to PYTHTRIP:def_2 ::_thesis: ( not p divides n9 or not p divides m9 ) assume that A9: p divides n9 and A10: p divides m9 ; ::_thesis: contradiction reconsider p = p as prime Element of NAT by ORDINAL1:def_12; p divides c by A7, A9, A10, NAT_D:8; then A11: p divides c * c by NAT_D:9; p divides - m9 by A10, INT_2:10; then A12: p divides n9 + (- m9) by A9, WSIERP_1:4; then p divides a * a by A4, A3, NAT_D:9; then A13: p divides - (a * a) by INT_2:10; b * b = (c * c) + (- (a * a)) by A1; then p divides b * b by A13, A11, WSIERP_1:4; then p divides b by NEWTON:80; hence contradiction by A2, A4, A3, A12, Def2; ::_thesis: verum end; then n9 is square by A6, Th1; then consider n being Nat such that A14: n9 = n ^2 by Def3; m9 is square by A8, A6, Th1; then consider m being Nat such that A15: m9 = m ^2 by Def3; reconsider m = m, n = n as Element of NAT by ORDINAL1:def_12; take m ; ::_thesis: ex n being Element of NAT st ( m <= n & a = (n ^2) - (m ^2) & b = (2 * m) * n & c = (n ^2) + (m ^2) ) take n ; ::_thesis: ( m <= n & a = (n ^2) - (m ^2) & b = (2 * m) * n & c = (n ^2) + (m ^2) ) n9 - m9 = a by A4, A3; then m ^2 <= n ^2 by A14, A15, XREAL_1:49; hence m <= n by SQUARE_1:16; ::_thesis: ( a = (n ^2) - (m ^2) & b = (2 * m) * n & c = (n ^2) + (m ^2) ) thus a = (n ^2) - (m ^2) by A4, A3, A14, A15; ::_thesis: ( b = (2 * m) * n & c = (n ^2) + (m ^2) ) b ^2 = (2 ^2) * ((n * m) ^2) by A5, A6, A14, A15, SQUARE_1:9 .= ((2 * m) * n) ^2 ; hence b = (2 * m) * n by Th5; ::_thesis: c = (n ^2) + (m ^2) thus c = (n ^2) + (m ^2) by A4, A3, A14, A15; ::_thesis: verum end; theorem :: PYTHTRIP:12 for a, n, m, b, c being Element of NAT st a = (n ^2) - (m ^2) & b = (2 * m) * n & c = (n ^2) + (m ^2) holds (a ^2) + (b ^2) = c ^2 ; definition mode Pythagorean_triple -> Subset of NAT means :Def4: :: PYTHTRIP:def 4 ex a, b, c being Element of NAT st ( (a ^2) + (b ^2) = c ^2 & it = {a,b,c} ); existence ex b1 being Subset of NAT ex a, b, c being Element of NAT st ( (a ^2) + (b ^2) = c ^2 & b1 = {a,b,c} ) proof take {0,0,0} ; ::_thesis: ex a, b, c being Element of NAT st ( (a ^2) + (b ^2) = c ^2 & {0,0,0} = {a,b,c} ) take 0 ; ::_thesis: ex b, c being Element of NAT st ( (0 ^2) + (b ^2) = c ^2 & {0,0,0} = {0,b,c} ) take 0 ; ::_thesis: ex c being Element of NAT st ( (0 ^2) + (0 ^2) = c ^2 & {0,0,0} = {0,0,c} ) take 0 ; ::_thesis: ( (0 ^2) + (0 ^2) = 0 ^2 & {0,0,0} = {0,0,0} ) thus (0 ^2) + (0 ^2) = 0 ^2 ; ::_thesis: {0,0,0} = {0,0,0} thus {0,0,0} = {0,0,0} ; ::_thesis: verum end; end; :: deftheorem Def4 defines Pythagorean_triple PYTHTRIP:def_4_:_ for b1 being Subset of NAT holds ( b1 is Pythagorean_triple iff ex a, b, c being Element of NAT st ( (a ^2) + (b ^2) = c ^2 & b1 = {a,b,c} ) ); registration cluster -> finite for Pythagorean_triple ; coherence for b1 being Pythagorean_triple holds b1 is finite proof let X be Pythagorean_triple ; ::_thesis: X is finite ex a, b, c being Element of NAT st ( (a ^2) + (b ^2) = c ^2 & X = {a,b,c} ) by Def4; hence X is finite ; ::_thesis: verum end; end; definition redefine mode Pythagorean_triple means :Def5: :: PYTHTRIP:def 5 ex k, m, n being Element of NAT st ( m <= n & it = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} ); compatibility for b1 being Subset of NAT holds ( b1 is Pythagorean_triple iff ex k, m, n being Element of NAT st ( m <= n & b1 = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} ) ) proof let X be Subset of NAT; ::_thesis: ( X is Pythagorean_triple iff ex k, m, n being Element of NAT st ( m <= n & X = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} ) ) hereby ::_thesis: ( ex k, m, n being Element of NAT st ( m <= n & X = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} ) implies X is Pythagorean_triple ) assume X is Pythagorean_triple ; ::_thesis: ex k, m, n being Element of NAT st ( m <= n & X = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} ) then consider a, b, c being Element of NAT such that A1: (a ^2) + (b ^2) = c ^2 and A2: X = {a,b,c} by Def4; set k = a gcd b; A3: a gcd b divides a by NAT_D:def_5; A4: a gcd b divides b by NAT_D:def_5; percases ( a gcd b = 0 or a gcd b <> 0 ) ; suppose a gcd b = 0 ; ::_thesis: ex k, m, n being Element of NAT st ( m <= n & X = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} ) then A5: ( a = 0 & b = 0 ) by A3, A4, INT_2:3; thus ex k, m, n being Element of NAT st ( m <= n & X = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} ) ::_thesis: verum proof take 0 ; ::_thesis: ex m, n being Element of NAT st ( m <= n & X = {(0 * ((n ^2) - (m ^2))),(0 * ((2 * m) * n)),(0 * ((n ^2) + (m ^2)))} ) take 0 ; ::_thesis: ex n being Element of NAT st ( 0 <= n & X = {(0 * ((n ^2) - (0 ^2))),(0 * ((2 * 0) * n)),(0 * ((n ^2) + (0 ^2)))} ) take 0 ; ::_thesis: ( 0 <= 0 & X = {(0 * ((0 ^2) - (0 ^2))),(0 * ((2 * 0) * 0)),(0 * ((0 ^2) + (0 ^2)))} ) thus ( 0 <= 0 & X = {(0 * ((0 ^2) - (0 ^2))),(0 * ((2 * 0) * 0)),(0 * ((0 ^2) + (0 ^2)))} ) by A1, A2, A5, XCMPLX_1:6; ::_thesis: verum end; end; supposeA6: a gcd b <> 0 ; ::_thesis: ex k, m, n being Element of NAT st ( m <= n & X = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} ) then A7: (a gcd b) * (a gcd b) <> 0 by XCMPLX_1:6; consider a9 being Nat such that A8: a = (a gcd b) * a9 by A3, NAT_D:def_3; consider b9 being Nat such that A9: b = (a gcd b) * b9 by A4, NAT_D:def_3; reconsider a9 = a9, b9 = b9 as Element of NAT by ORDINAL1:def_12; (a gcd b) * (a9 gcd b9) = (a gcd b) * 1 by A8, A9, Th8; then a9 gcd b9 = 1 by A6, XCMPLX_1:5; then A10: a9,b9 are_relative_prime by INT_2:def_3; c ^2 = ((a gcd b) ^2) * ((a9 ^2) + (b9 ^2)) by A1, A8, A9; then (a gcd b) ^2 divides c ^2 by NAT_D:def_3; then a gcd b divides c by Th6; then consider c9 being Nat such that A11: c = (a gcd b) * c9 by NAT_D:def_3; reconsider c9 = c9 as Element of NAT by ORDINAL1:def_12; ((a gcd b) ^2) * ((a9 ^2) + (b9 ^2)) = ((a gcd b) ^2) * (c9 ^2) by A1, A8, A9, A11; then A12: (a9 ^2) + (b9 ^2) = c9 ^2 by A7, XCMPLX_1:5; thus ex k, m, n being Element of NAT st ( m <= n & X = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} ) ::_thesis: verum proof percases ( a9 is odd or b9 is odd ) by A10, Th10; suppose a9 is odd ; ::_thesis: ex k, m, n being Element of NAT st ( m <= n & X = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} ) then consider m, n being Element of NAT such that A13: ( m <= n & a9 = (n ^2) - (m ^2) & b9 = (2 * m) * n & c9 = (n ^2) + (m ^2) ) by A12, A10, Th11; take a gcd b ; ::_thesis: ex m, n being Element of NAT st ( m <= n & X = {((a gcd b) * ((n ^2) - (m ^2))),((a gcd b) * ((2 * m) * n)),((a gcd b) * ((n ^2) + (m ^2)))} ) take m ; ::_thesis: ex n being Element of NAT st ( m <= n & X = {((a gcd b) * ((n ^2) - (m ^2))),((a gcd b) * ((2 * m) * n)),((a gcd b) * ((n ^2) + (m ^2)))} ) take n ; ::_thesis: ( m <= n & X = {((a gcd b) * ((n ^2) - (m ^2))),((a gcd b) * ((2 * m) * n)),((a gcd b) * ((n ^2) + (m ^2)))} ) thus ( m <= n & X = {((a gcd b) * ((n ^2) - (m ^2))),((a gcd b) * ((2 * m) * n)),((a gcd b) * ((n ^2) + (m ^2)))} ) by A2, A8, A9, A11, A13; ::_thesis: verum end; suppose b9 is odd ; ::_thesis: ex k, m, n being Element of NAT st ( m <= n & X = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} ) then consider m, n being Element of NAT such that A14: ( m <= n & b9 = (n ^2) - (m ^2) & a9 = (2 * m) * n & c9 = (n ^2) + (m ^2) ) by A12, A10, Th11; take a gcd b ; ::_thesis: ex m, n being Element of NAT st ( m <= n & X = {((a gcd b) * ((n ^2) - (m ^2))),((a gcd b) * ((2 * m) * n)),((a gcd b) * ((n ^2) + (m ^2)))} ) take m ; ::_thesis: ex n being Element of NAT st ( m <= n & X = {((a gcd b) * ((n ^2) - (m ^2))),((a gcd b) * ((2 * m) * n)),((a gcd b) * ((n ^2) + (m ^2)))} ) take n ; ::_thesis: ( m <= n & X = {((a gcd b) * ((n ^2) - (m ^2))),((a gcd b) * ((2 * m) * n)),((a gcd b) * ((n ^2) + (m ^2)))} ) thus ( m <= n & X = {((a gcd b) * ((n ^2) - (m ^2))),((a gcd b) * ((2 * m) * n)),((a gcd b) * ((n ^2) + (m ^2)))} ) by A2, A8, A9, A11, A14, ENUMSET1:58; ::_thesis: verum end; end; end; end; end; end; assume ex k, m, n being Element of NAT st ( m <= n & X = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} ) ; ::_thesis: X is Pythagorean_triple then consider k, m, n being Element of NAT such that A15: m <= n and A16: X = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} ; m ^2 <= n ^2 by A15, SQUARE_1:15; then reconsider a9 = (n ^2) - (m ^2) as Element of NAT by INT_1:3, XREAL_1:48; set a = k * a9; set c9 = (n ^2) + (m ^2); set b9 = (2 * m) * n; set b = k * ((2 * m) * n); set c = k * ((n ^2) + (m ^2)); ((k * a9) ^2) + ((k * ((2 * m) * n)) ^2) = (k * ((n ^2) + (m ^2))) ^2 ; hence X is Pythagorean_triple by A16, Def4; ::_thesis: verum end; end; :: deftheorem Def5 defines Pythagorean_triple PYTHTRIP:def_5_:_ for b1 being Subset of NAT holds ( b1 is Pythagorean_triple iff ex k, m, n being Element of NAT st ( m <= n & b1 = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} ) ); definition let X be Pythagorean_triple ; attrX is degenerate means :Def6: :: PYTHTRIP:def 6 0 in X; end; :: deftheorem Def6 defines degenerate PYTHTRIP:def_6_:_ for X being Pythagorean_triple holds ( X is degenerate iff 0 in X ); theorem :: PYTHTRIP:13 for n being Element of NAT st n > 2 holds ex X being Pythagorean_triple st ( not X is degenerate & n in X ) proof let n be Element of NAT ; ::_thesis: ( n > 2 implies ex X being Pythagorean_triple st ( not X is degenerate & n in X ) ) assume A1: n > 2 ; ::_thesis: ex X being Pythagorean_triple st ( not X is degenerate & n in X ) percases ( n is even or n is odd ) ; suppose n is even ; ::_thesis: ex X being Pythagorean_triple st ( not X is degenerate & n in X ) then consider m being Element of NAT such that A2: n = 2 * m by ABIAN:def_2; set c = 1 * ((m ^2) + (1 ^2)); set b = 1 * ((2 * 1) * m); 2 * m > 2 * 1 by A1, A2; then A3: m > 1 by XREAL_1:64; then m ^2 > 1 ^2 by SQUARE_1:16; then (m ^2) - (1 ^2) > 0 by XREAL_1:50; then reconsider a = 1 * ((m ^2) - (1 ^2)) as Element of NAT by INT_1:3; reconsider X = {a,(1 * ((2 * 1) * m)),(1 * ((m ^2) + (1 ^2)))} as Pythagorean_triple by A3, Def5; take X ; ::_thesis: ( not X is degenerate & n in X ) a <> 0 by A3, SQUARE_1:16; hence not 0 in X by A1, A2, ENUMSET1:def_1; :: according to PYTHTRIP:def_6 ::_thesis: n in X thus n in X by A2, ENUMSET1:def_1; ::_thesis: verum end; suppose n is odd ; ::_thesis: ex X being Pythagorean_triple st ( not X is degenerate & n in X ) then consider i being Integer such that A4: n = (2 * i) + 1 by ABIAN:1; A5: 2 * i >= 2 * 1 by A1, A4, INT_1:7; then i >= 1 by XREAL_1:68; then reconsider m = i as Element of NAT by INT_1:3; reconsider a = 1 * (((m + 1) ^2) - (m ^2)) as Element of NAT by A4; set b = 1 * ((2 * m) * (m + 1)); set c = 1 * (((m + 1) ^2) + (m ^2)); m <= m + 1 by NAT_1:11; then reconsider X = {a,(1 * ((2 * m) * (m + 1))),(1 * (((m + 1) ^2) + (m ^2)))} as Pythagorean_triple by Def5; take X ; ::_thesis: ( not X is degenerate & n in X ) ( a = (2 * m) + 1 & 1 * (((m + 1) ^2) + (m ^2)) = (((m ^2) + (2 * m)) + (m ^2)) + 1 ) ; hence not 0 in X by A5, ENUMSET1:def_1; :: according to PYTHTRIP:def_6 ::_thesis: n in X thus n in X by A4, ENUMSET1:def_1; ::_thesis: verum end; end; end; definition let X be Pythagorean_triple ; attrX is simplified means :Def7: :: PYTHTRIP:def 7 for k being Element of NAT st ( for n being Element of NAT st n in X holds k divides n ) holds k = 1; end; :: deftheorem Def7 defines simplified PYTHTRIP:def_7_:_ for X being Pythagorean_triple holds ( X is simplified iff for k being Element of NAT st ( for n being Element of NAT st n in X holds k divides n ) holds k = 1 ); definition let X be Pythagorean_triple ; redefine attr X is simplified means :Def8: :: PYTHTRIP:def 8 ex m, n being Element of NAT st ( m in X & n in X & m,n are_relative_prime ); compatibility ( X is simplified iff ex m, n being Element of NAT st ( m in X & n in X & m,n are_relative_prime ) ) proof hereby ::_thesis: ( ex m, n being Element of NAT st ( m in X & n in X & m,n are_relative_prime ) implies X is simplified ) assume A1: X is simplified ; ::_thesis: ex a, b being Element of NAT st ( a in X & b in X & a,b are_relative_prime ) consider a, b, c being Element of NAT such that A2: (a ^2) + (b ^2) = c ^2 and A3: X = {a,b,c} by Def4; take a = a; ::_thesis: ex b being Element of NAT st ( a in X & b in X & a,b are_relative_prime ) take b = b; ::_thesis: ( a in X & b in X & a,b are_relative_prime ) thus a in X by A3, ENUMSET1:def_1; ::_thesis: ( b in X & a,b are_relative_prime ) thus b in X by A3, ENUMSET1:def_1; ::_thesis: a,b are_relative_prime now__::_thesis:_for_k_being_Nat_st_k_divides_a_&_k_divides_b_holds_ k_=_1 let k be Nat; ::_thesis: ( k divides a & k divides b implies k = 1 ) reconsider k1 = k as Element of NAT by ORDINAL1:def_12; assume A4: ( k divides a & k divides b ) ; ::_thesis: k = 1 then ( k1 ^2 divides a ^2 & k1 ^2 divides b ^2 ) by Th6; then k ^2 divides c ^2 by A2, NAT_D:8; then k1 divides c by Th6; then for n being Element of NAT st n in X holds k1 divides n by A3, A4, ENUMSET1:def_1; hence k = 1 by A1, Def7; ::_thesis: verum end; hence a,b are_relative_prime by Def1; ::_thesis: verum end; assume ex m, n being Element of NAT st ( m in X & n in X & m,n are_relative_prime ) ; ::_thesis: X is simplified then consider m, n being Element of NAT such that A5: ( m in X & n in X ) and A6: m,n are_relative_prime ; let k be Element of NAT ; :: according to PYTHTRIP:def_7 ::_thesis: ( ( for n being Element of NAT st n in X holds k divides n ) implies k = 1 ) assume for n being Element of NAT st n in X holds k divides n ; ::_thesis: k = 1 then A7: ( k divides m & k divides n ) by A5; m gcd n = 1 by A6, INT_2:def_3; then k divides 1 by A7, NAT_D:def_5; hence k = 1 by WSIERP_1:15; ::_thesis: verum end; end; :: deftheorem Def8 defines simplified PYTHTRIP:def_8_:_ for X being Pythagorean_triple holds ( X is simplified iff ex m, n being Element of NAT st ( m in X & n in X & m,n are_relative_prime ) ); theorem Th14: :: PYTHTRIP:14 for n being Element of NAT st n > 0 holds ex X being Pythagorean_triple st ( not X is degenerate & X is simplified & 4 * n in X ) proof let n be Element of NAT ; ::_thesis: ( n > 0 implies ex X being Pythagorean_triple st ( not X is degenerate & X is simplified & 4 * n in X ) ) set b = 1 * ((2 * 1) * (2 * n)); set c = 1 * (((2 * n) ^2) + (1 ^2)); assume A1: n > 0 ; ::_thesis: ex X being Pythagorean_triple st ( not X is degenerate & X is simplified & 4 * n in X ) then n >= 0 + 1 by NAT_1:13; then A2: n + n > 0 + 1 by XREAL_1:8; then (2 * n) ^2 > 1 ^2 by SQUARE_1:16; then ((2 * n) ^2) - (1 ^2) > 0 by XREAL_1:50; then reconsider a = 1 * (((2 * n) ^2) - (1 ^2)) as Element of NAT by INT_1:3; reconsider X = {a,(1 * ((2 * 1) * (2 * n))),(1 * (((2 * n) ^2) + (1 ^2)))} as Pythagorean_triple by A2, Def5; take X ; ::_thesis: ( not X is degenerate & X is simplified & 4 * n in X ) ( a <> 0 & 1 * ((2 * 1) * (2 * n)) <> 0 ) by A1; hence not 0 in X by ENUMSET1:def_1; :: according to PYTHTRIP:def_6 ::_thesis: ( X is simplified & 4 * n in X ) a - (1 * (((2 * n) ^2) + (1 ^2))) = - 2 ; then a gcd (1 * (((2 * n) ^2) + (1 ^2))) = (1 * (((2 * n) ^2) + (1 ^2))) gcd (- 2) by PREPOWER:97 .= (abs (1 * (((2 * n) ^2) + (1 ^2)))) gcd (abs (- 2)) by INT_2:34 .= (abs (1 * (((2 * n) ^2) + (1 ^2)))) gcd (abs 2) by COMPLEX1:52 .= ((2 * (2 * (n ^2))) + 1) gcd 2 by INT_2:34 .= 1 gcd 2 by EULER_1:16 .= 1 by WSIERP_1:8 ; then A3: a,1 * (((2 * n) ^2) + (1 ^2)) are_relative_prime by INT_2:def_3; ( a in X & 1 * (((2 * n) ^2) + (1 ^2)) in X ) by ENUMSET1:def_1; hence X is simplified by A3, Def8; ::_thesis: 4 * n in X thus 4 * n in X by ENUMSET1:def_1; ::_thesis: verum end; registration cluster finite non degenerate simplified for Pythagorean_triple ; existence ex b1 being Pythagorean_triple st ( not b1 is degenerate & b1 is simplified ) proof consider X being Pythagorean_triple such that A1: ( not X is degenerate & X is simplified ) and 4 * 1 in X by Th14; take X ; ::_thesis: ( not X is degenerate & X is simplified ) thus ( not X is degenerate & X is simplified ) by A1; ::_thesis: verum end; end; theorem :: PYTHTRIP:15 {3,4,5} is non degenerate simplified Pythagorean_triple proof (3 ^2) + (4 ^2) = 5 ^2 ; then reconsider X = {3,4,5} as Pythagorean_triple by Def4; 3 gcd 4 = 3 gcd (4 - 3) by PREPOWER:97 .= 1 by WSIERP_1:8 ; then A1: ( 4 in X & 3,4 are_relative_prime ) by ENUMSET1:def_1, INT_2:def_3; ( not 0 in X & 3 in X ) by ENUMSET1:def_1; hence {3,4,5} is non degenerate simplified Pythagorean_triple by A1, Def6, Def8; ::_thesis: verum end; theorem :: PYTHTRIP:16 { X where X is Pythagorean_triple : ( not X is degenerate & X is simplified ) } is infinite proof set T = { X where X is Pythagorean_triple : ( not X is degenerate & X is simplified ) } ; for m being Element of NAT ex n being Element of NAT st ( n >= m & n in union { X where X is Pythagorean_triple : ( not X is degenerate & X is simplified ) } ) proof let m be Element of NAT ; ::_thesis: ex n being Element of NAT st ( n >= m & n in union { X where X is Pythagorean_triple : ( not X is degenerate & X is simplified ) } ) set m9 = m + 1; set n = 4 * (m + 1); take 4 * (m + 1) ; ::_thesis: ( 4 * (m + 1) >= m & 4 * (m + 1) in union { X where X is Pythagorean_triple : ( not X is degenerate & X is simplified ) } ) consider X being Pythagorean_triple such that A1: ( not X is degenerate & X is simplified ) and A2: 4 * (m + 1) in X by Th14; (4 * (m + 1)) + 0 = (1 * (m + 1)) + (3 * (m + 1)) ; then A3: 4 * (m + 1) >= (m + 1) + 0 by XREAL_1:6; m + 1 >= m by NAT_1:11; hence 4 * (m + 1) >= m by A3, XXREAL_0:2; ::_thesis: 4 * (m + 1) in union { X where X is Pythagorean_triple : ( not X is degenerate & X is simplified ) } X in { X where X is Pythagorean_triple : ( not X is degenerate & X is simplified ) } by A1; hence 4 * (m + 1) in union { X where X is Pythagorean_triple : ( not X is degenerate & X is simplified ) } by A2, TARSKI:def_4; ::_thesis: verum end; then A4: union { X where X is Pythagorean_triple : ( not X is degenerate & X is simplified ) } is infinite by Th9; now__::_thesis:_for_X_being_set_st_X_in__{__X_where_X_is_Pythagorean_triple_:_(_not_X_is_degenerate_&_X_is_simplified_)__}__holds_ X_is_finite let X be set ; ::_thesis: ( X in { X where X is Pythagorean_triple : ( not X is degenerate & X is simplified ) } implies X is finite ) assume X in { X where X is Pythagorean_triple : ( not X is degenerate & X is simplified ) } ; ::_thesis: X is finite then ex X9 being Pythagorean_triple st ( X = X9 & not X9 is degenerate & X9 is simplified ) ; hence X is finite ; ::_thesis: verum end; hence { X where X is Pythagorean_triple : ( not X is degenerate & X is simplified ) } is infinite by A4, FINSET_1:7; ::_thesis: verum end;