Copyright (c) 2000 Association of Mizar Users
environ vocabulary RLVECT_1, VECTSP_1, COMPLEX1, ARYTM_1, SQUARE_1, ABSVALUE, COMPLFLD, HAHNBAN1, GROUP_1, FUNCT_1, BINOP_1, POWER, RAT_1, PREPOWER, RCOMP_1, SIN_COS, ARYTM_3, RFUNCT_2, FDIFF_1, PRE_TOPC, BOOLE, RELAT_1, FCONT_1, PARTFUN1, COMPTRIG, ARYTM; notation TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, ORDINAL1, NUMBERS, ARYTM_0, XREAL_0, REAL_1, SQUARE_1, NAT_1, RAT_1, ABSVALUE, PREPOWER, POWER, RLVECT_1, VECTSP_1, BINOP_1, RELAT_1, FUNCT_1, RFUNCT_2, FCONT_1, FDIFF_1, SEQ_1, PARTFUN1, PARTFUN2, COMPLEX1, BINARITH, RCOMP_1, GROUP_1, SIN_COS, COMPLFLD, HAHNBAN1; constructors REAL_1, BINOP_1, TRIANG_1, SQUARE_1, PREPOWER, POWER, SEQ_1, RFUNCT_1, RFUNCT_2, FCONT_1, BINARITH, COMSEQ_3, GROUP_1, ALGSTR_2, RCOMP_1, VECTSP_2, FDIFF_1, PARTFUN2, COMPLSP1, SIN_COS, HAHNBAN1, COMPLEX1, MEMBERED, ARYTM_0, ARYTM_3, FUNCT_4; clusters XREAL_0, STRUCT_0, RELSET_1, PARTFUN2, BINARITH, GROUP_1, GCD_1, COMPLFLD, POLYNOM2, MONOID_0, NAT_1, MEMBERED, NUMBERS, ORDINAL2; requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM; definitions RFUNCT_2; theorems AXIOMS, XREAL_0, REAL_1, REAL_2, NAT_1, SQUARE_1, PREPOWER, POWER, BINARITH, ABSVALUE, RELAT_1, FUNCT_1, RFUNCT_2, PARTFUN1, FCONT_1, FCONT_2, CARD_1, TOPREAL3, RLVECT_1, VECTSP_1, GROUP_1, RCOMP_1, FDIFF_1, ROLLE, COMPLEX1, SIN_COS, SIN_COS2, COMPLFLD, HAHNBAN1, POLYNOM2, TOPREAL5, JORDAN6, XBOOLE_0, XCMPLX_0, XCMPLX_1, ARYTM_0; schemes NAT_1; begin scheme Regr_without_0 { P[Nat] } : P[1] provided A1: ex k be non empty Nat st P[k] and A2: for k be non empty Nat st k <> 1 & P[k] ex n be non empty Nat st n < k & P[n] proof defpred R[Nat] means P[$1+1]; consider t be non empty Nat such that A3: P[t] by A1; consider s be Nat such that A4: t = s+1 by NAT_1:22; A5: ex k be Nat st R[k] by A3,A4; A6: now let k be Nat; assume that A7: k <> 0 and A8: R[k]; reconsider k1=k+1 as non empty Nat; k > 0 by A7,NAT_1:19; then k+1 > 0+1 by REAL_1:53; then consider n be non empty Nat such that A9: n < k1 and A10: P[n] by A2,A8; consider l be Nat such that A11: n = l+1 by NAT_1:22; take l; thus l < k by A9,A11,AXIOMS:24; thus R[l] by A10,A11; end; R[0] from Regr(A5,A6); hence thesis; end; canceled 2; theorem Th3: for z be Element of COMPLEX holds Re z >= -|.z.| proof let z be Element of COMPLEX; 0 <= (Im z)^2 by SQUARE_1:72; then (Re z)^2+0 <= (Re z)^2 + (Im z)^2 by REAL_1:55; then 0 <= (Re z)^2 & (Re z)^2 <= (Re z)^2 + (Im z)^2 by SQUARE_1:72; then sqrt(Re z)^2 <= sqrt((Re z)^2 + (Im z)^2) by SQUARE_1:94; then sqrt(Re z)^2 <= |.z.| by COMPLEX1:def 16; then -sqrt(Re z)^2 >= -|.z.| by REAL_1:50; then Re z >= -abs(Re z) & -abs(Re z) >= -|.z.| by ABSVALUE:11,SQUARE_1:91; hence thesis by AXIOMS:22; end; theorem Th4: for z be Element of COMPLEX holds Im z >= -|.z.| proof let z be Element of COMPLEX; 0 <= (Re z)^2 by SQUARE_1:72; then (Im z)^2+0 <= (Re z)^2 + (Im z)^2 by REAL_1:55; then 0 <= (Im z)^2 & (Im z)^2 <= (Re z)^2 + (Im z)^2 by SQUARE_1:72; then sqrt(Im z)^2 <= sqrt((Re z)^2 + (Im z)^2) by SQUARE_1:94; then sqrt(Im z)^2 <= |.z.| by COMPLEX1:def 16; then -sqrt(Im z)^2 >= -|.z.| by REAL_1:50; then Im z >= -abs(Im z) & -abs(Im z) >= -|.z.| by ABSVALUE:11,SQUARE_1:91; hence thesis by AXIOMS:22; end; theorem Th5: for z be Element of F_Complex holds Re z >= -|.z.| proof let z be Element of F_Complex; consider z1 be Element of COMPLEX such that A1: z = z1 and A2: Re z = Re z1 by HAHNBAN1:def 3; consider z2 be Element of COMPLEX such that A3: z = z2 and A4: |.z.| = |.z2.| by COMPLFLD:def 3; thus thesis by A1,A2,A3,A4,Th3; end; theorem for z be Element of F_Complex holds Im z >= -|.z.| proof let z be Element of F_Complex; consider z1 be Element of COMPLEX such that A1: z = z1 and A2: Im z = Im z1 by HAHNBAN1:def 4; consider z2 be Element of COMPLEX such that A3: z = z2 and A4: |.z.| = |.z2.| by COMPLFLD:def 3; thus thesis by A1,A2,A3,A4,Th4; end; theorem Th7: for z be Element of F_Complex holds |.z.|^2 = (Re z)^2 + (Im z)^2 proof let z be Element of F_Complex; consider z1 be Element of COMPLEX such that A1: z = z1 and A2: Re z = Re z1 by HAHNBAN1:def 3; consider z2 be Element of COMPLEX such that A3: z = z2 and A4: Im z = Im z2 by HAHNBAN1:def 4; consider z3 be Element of COMPLEX such that A5: z = z3 and A6: |.z.| = |.z3.| by COMPLFLD:def 3; thus |.z.|^2 = |.z.|*|.z.| by SQUARE_1:def 3 .= |.z3*z3.| by A6,COMPLEX1:151 .= (Re z)^2 + (Im z)^2 by A1,A2,A3,A4,A5,COMPLEX1:154; end; theorem Th8: for x1,x2,y1,y2 be Real holds [**x1,x2**] = [**y1,y2**] implies x1 = y1 & x2 = y2 proof let x1,x2,y1,y2 be Real; assume [**x1,x2**] = [**y1,y2**]; then [*x1,x2*] = [**y1,y2**] by HAHNBAN1:def 1 .= [*y1,y2*] by HAHNBAN1:def 1; hence thesis by ARYTM_0:12; end; theorem Th9: for z be Element of F_Complex holds z = [**Re z,Im z**] proof let z be Element of F_Complex; reconsider z1=z as Element of COMPLEX by COMPLFLD:def 1; thus z = [*Re z1,Im z1*] by COMPLEX1:8 .= [**Re z1,Im z1**] by HAHNBAN1:def 1 .= [**Re z,Im z1**] by HAHNBAN1:def 3 .= [**Re z,Im z**] by HAHNBAN1:def 4; end; L0: 0c = [*0,0*] by ARYTM_0:def 7,COMPLEX1:def 6; L1: 1r = [*1,0*] by ARYTM_0:def 7,COMPLEX1:def 7; theorem Th10: 0.F_Complex = [**0,0**] by L0,COMPLFLD:9,HAHNBAN1:def 1; Lm1: 0.F_Complex = the Zero of F_Complex by RLVECT_1:def 2; canceled; theorem Th12: for L be unital (non empty HGrStr) for x be Element of L holds (power L).(x,1) = x proof let L be unital (non empty HGrStr); let x be Element of L; 0+1 = 1; hence (power L).(x,1) = (power L).(x,0) * x by GROUP_1:def 7 .= 1.L * x by GROUP_1:def 7 .= x by GROUP_1:def 4; end; theorem for L be unital (non empty HGrStr) for x be Element of L holds (power L).(x,2) = x*x proof let L be unital (non empty HGrStr); let x be Element of L; 1+1 = 2; hence (power L).(x,2) = (power L).(x,1) * x by GROUP_1:def 7 .= x * x by Th12; end; theorem Th14: for L be add-associative right_zeroed right_complementable right-distributive unital (non empty doubleLoopStr) for n be Nat st n > 0 holds (power L).(0.L,n) = 0.L proof let L be add-associative right_zeroed right_complementable right-distributive unital (non empty doubleLoopStr); let n be Nat; assume n > 0; then n >= 0+1 by NAT_1:38; then A1: n-1 >= 0 by REAL_1:84; n = n+-1+1 by XCMPLX_1:139 .= n-1+1 by XCMPLX_0:def 8 .= n-'1+1 by A1,BINARITH:def 3; hence (power L).(0.L,n) = (power L).(0.L,n-'1)*0.L by GROUP_1:def 7 .= 0.L by VECTSP_1:36; end; theorem Th15: for L be associative commutative unital (non empty HGrStr) for x,y be Element of L for n be Nat holds (power L).(x*y,n) = (power L).(x,n) * (power L).(y,n) proof let L be associative commutative unital (non empty HGrStr); let x,y be Element of L; defpred P[Nat] means (power L).(x*y,$1) = (power L).(x,$1) * (power L).(y,$1); (power L).(x*y,0) = 1.L by GROUP_1:def 7 .= 1.L * 1.L by GROUP_1:def 4 .= (power L).(x,0) * 1.L by GROUP_1:def 7 .= (power L).(x,0) * (power L).(y,0) by GROUP_1:def 7; then A1: P[0]; A2: now let n be Nat; assume P[n]; then (power L).(x*y,n+1) = (power L).(x,n) * (power L).(y,n) * (x*y) by GROUP_1:def 7 .= (power L).(x,n) * ((power L).(y,n) * (x*y)) by VECTSP_1:def 16 .= (power L).(x,n) * (x*((power L).(y,n)*y)) by VECTSP_1:def 16 .= (power L).(x,n) * (x*(power L).(y,n+1)) by GROUP_1:def 7 .= (power L).(x,n)*x * (power L).(y,n+1) by VECTSP_1:def 16 .= (power L).(x,n+1) * (power L).(y,n+1) by GROUP_1:def 7; hence P[n+1]; end; thus for n be Nat holds P[n] from Ind(A1,A2); end; theorem Th16: for x be Real st x > 0 for n be Nat holds (power F_Complex).([**x,0**],n) = [**x to_power n,0**] proof let x be Real; assume A1: x > 0; defpred P[Nat] means (power F_Complex).([**x,0**],$1) = [**x to_power $1,0**]; (power F_Complex).([**x,0**],0) = 1.F_Complex by GROUP_1:def 7 .= [*1,0*] by COMPLFLD:10,POLYNOM2:3,L1 .= [**1,0**] by HAHNBAN1:def 1 .= [**x to_power 0,0**] by POWER:29; then A2: P[0]; A3: now let n be Nat; assume P[n]; then (power F_Complex).([**x,0**],n+1) = [**x to_power n,0**]*[**x,0**] by GROUP_1:def 7 .= [**(x to_power n)*x-0*0,(x to_power n)*0+0*x**] by HAHNBAN1:11 .= [**(x to_power n)*(x to_power 1),0**] by POWER:30 .= [**x to_power (n+1),0**] by A1,POWER:32; hence P[n+1]; end; thus for n be Nat holds P[n] from Ind(A2,A3); end; theorem Th17: for x be real number for n be Nat st x >= 0 & n <> 0 holds (n-root x) to_power n = x proof let x be real number; let n be Nat; assume that A1: x >= 0 and A2: n <> 0; A3: n > 0 by A2,NAT_1:19; then A4: n >= 0+1 by NAT_1:38; reconsider n1=n as Rational; per cases by A1; suppose A5: x > 0; n-root x = n -Root x by A1,A4,POWER:def 1; then A6: n-root x > 0 by A4,A5,PREPOWER:def 3; hence (n-root x) to_power n = (n-root x) #R n by POWER:def 2 .= (n-root x) #Q n1 by A6,PREPOWER:88 .= (n-root x) |^ n by A6,PREPOWER:60 .= x by A1,A4,POWER:5; suppose A7: x = 0; hence (n-root x) to_power n = 0 to_power n by A4,POWER:6 .= x by A3,A7,POWER:def 2; end; begin canceled 2; theorem Th20: PI+PI/2 = 3/2*PI & 3/2*PI+PI/2 = 2*PI & 3/2*PI - PI = PI/2 proof thus PI+PI/2 = (2/2)*PI + 1*(PI/2) .= (2*PI)/2 + 1*(PI/2) by XCMPLX_1:75 .= 2*(PI/2) + 1*(PI/2) by XCMPLX_1:75 .= (2 + 1)*(PI/2) by XCMPLX_1:8 .= (3*PI)/2 by XCMPLX_1:75 .= 3/2*PI by XCMPLX_1:75; thus 3/2*PI + PI/2 = 3*PI/2 + 1*PI/2 by XCMPLX_1:75 .= (3*PI+1*PI)/2 by XCMPLX_1:63 .= ((3+1)*PI)/2 by XCMPLX_1:8 .= 4/2*PI by XCMPLX_1:75 .= 2*PI; thus 3/2*PI - PI = 3/2*PI - 2/2*PI .= (3/2 - 2/2)*PI by XCMPLX_1:40 .= (3-2)/2*PI .= 1*PI/2 by XCMPLX_1:75 .= PI/2; end; theorem Th21: 0 < PI/2 & PI/2 < PI & 0 < PI & -PI/2 < PI/2 & PI < 2*PI & PI/2 < 3/2*PI & -PI/2 < 0 & 0 < 2*PI & PI < 3/2*PI & 3/2*PI < 2*PI & 0 < 3/2*PI proof thus A1: 0 < PI/2 proof PI in ].0, 4.[ by SIN_COS:def 30; then 0 < PI & PI < 4 by JORDAN6:45; then 0/2 < PI/2 by REAL_1:73; hence 0 < PI/2; end; thus A2: PI/2 < PI proof 0 + PI/2 < PI/2 + PI/2 by A1,REAL_1:53; hence PI/2 < PI by XCMPLX_1:66; end; hence A3: 0 < PI by A1,AXIOMS:22; then A4: 0-PI/2 < PI-PI/2 by REAL_1:54; PI/2 + PI/2 = PI by XCMPLX_1:66; then PI - PI/2 = PI/2 by XCMPLX_1:26; hence -PI/2 < PI/2 by A4,XCMPLX_1:150; 0 + PI < PI + PI by A3,REAL_1:53; hence A5: PI < 2*PI by XCMPLX_1:11; 0+PI/2 < PI+PI/2 by A3,REAL_1:53; hence PI/2 < 3/2*PI by Th20; 0 = -0; hence -PI/2 < 0 by A1,REAL_1:50; thus 0 < 2*PI by A1,A2,A5,AXIOMS:22; PI/2+PI/2 < PI+PI/2 by A2,REAL_1:53; hence A6: PI < 3/2*PI by Th20,XCMPLX_1:66; hence 3/2*PI < 2*PI by Th20,REAL_1:53; thus 0 < 3/2*PI by A1,A2,A6,AXIOMS:22; end; theorem Th22: for a,b,c,x be real number st x in ].a,c.[ holds x in ].a,b.[ or x = b or x in ].b,c.[ proof let a,b,c,x be real number; assume that A1: x in ].a,c.[ and A2: not x in ].a,b.[ and A3: not x = b; A4: a < x & x < c by A1,JORDAN6:45; x <= a or x >= b by A2,JORDAN6:45; then x > b by A1,A3,JORDAN6:45,REAL_1:def 5; hence x in ].b,c.[ by A4,JORDAN6:45; end; theorem Th23: for x be Real st x in ].0,PI.[ holds sin.x > 0 proof let x be Real; assume A1: x in ].0,PI.[; PI/2 + PI/2 = PI by XCMPLX_1:66; then A2: PI - PI/2 = PI/2 by XCMPLX_1:26; per cases by A1,Th22; suppose x in ].0,PI/2.[; then 0 < x & x < PI/2 by JORDAN6:45; then 0-x < 0 & -x > -PI/2 by REAL_1:50,REAL_2:105; then -x < 0 & -x > -PI/2 by XCMPLX_1:150; then -x+PI/2 < 0+PI/2 & -x+PI/2 > -PI/2+PI/2 by REAL_1:53; then PI/2-x < PI/2 & PI/2+ -x > PI/2-PI/2 by XCMPLX_0:def 8; then PI/2-x < PI/2 & PI/2-x > PI/2-PI/2 by XCMPLX_0:def 8; then 0 < PI/2-x & PI/2-x < PI/2 by XCMPLX_1:14; then PI/2-x in ].0,PI/2.[ by JORDAN6:45; then cos.(PI/2-x) > 0 by SIN_COS:85; hence sin.x > 0 by SIN_COS:83; suppose x=PI/2; hence sin.x > 0 by SIN_COS:81; suppose x in ].PI/2,PI.[; then PI/2 < x & x < PI by JORDAN6:45; then PI/2-PI/2 < x-PI/2 & x-PI/2 < PI-PI/2 by REAL_1:54; then 0 < x-PI/2 & x-PI/2 < PI-PI/2 by XCMPLX_1:14; then x-PI/2 in ].0,PI/2.[ by A2,JORDAN6:45; then cos.(x-PI/2) > 0 by SIN_COS:85; then cos.(-(PI/2-x)) > 0 by XCMPLX_1:143; then cos.(PI/2-x) > 0 by SIN_COS:33; hence sin.x > 0 by SIN_COS:83; end; theorem Th24: for x be real number st x in [.0,PI.] holds sin.x >= 0 proof let x be real number; assume x in [.0,PI.]; then 0 <= x & x <= PI by TOPREAL5:1; then x = 0 or x = PI or (0 < x & x < PI) by REAL_1:def 5; then x = 0 or x = PI or x in ].0,PI.[ by JORDAN6:45; hence sin.x >= 0 by Th23,SIN_COS:33,81; end; theorem Th25: for x be Real st x in ].PI,2*PI.[ holds sin.x < 0 proof let x be Real; assume x in ].PI,2*PI.[; then PI < x & x < 2*PI by JORDAN6:45; then PI-PI < x-PI & x-PI < 2*PI-PI by REAL_1:54; then 0 < x-PI & x-PI < 2*PI+-PI by XCMPLX_0:def 8,XCMPLX_1:14; then 0 < x-PI & x-PI < PI by XCMPLX_1:184; then A1: x-PI in ].0,PI.[ by JORDAN6:45; sin.(x-PI) = sin.(-(PI-x)) by XCMPLX_1:143 .= -sin.(PI-x) by SIN_COS:33 .= -sin.(PI+-x) by XCMPLX_0:def 8 .= --sin.(-x) by SIN_COS:83 .= -sin.x by SIN_COS:33; then -sin.x > 0 by A1,Th23; hence sin.x < 0 by REAL_1:66; end; theorem Th26: for x be real number st x in [.PI,2*PI.] holds sin.x <= 0 proof let x be real number; assume x in [.PI,2*PI.]; then PI <= x & x <= 2*PI by TOPREAL5:1; then x = PI or x = 2*PI or (PI < x & x < 2*PI) by REAL_1:def 5; then x = PI or x = 2*PI or x in ].PI,2*PI.[ by JORDAN6:45; hence sin.x <= 0 by Th25,SIN_COS:81; end; reserve x for Real; theorem Th27: x in ].-PI/2,PI/2.[ implies cos.x > 0 proof assume x in ].-PI/2,PI/2.[; then -PI/2 < x & x < PI/2 by JORDAN6:45; then -PI/2+PI/2 < x+PI/2 & x+PI/2 < PI/2+PI/2 by REAL_1:53; then 0 < x+PI/2 & x+PI/2 < PI by XCMPLX_0:def 6,XCMPLX_1:66; then A1: x+PI/2 in ].0,PI.[ by JORDAN6:45; sin.(x+PI/2) = cos.x by SIN_COS:83; hence cos.x > 0 by A1,Th23; end; theorem Th28: for x be real number st x in [.-PI/2,PI/2.] holds cos.x >= 0 proof let x be real number; assume x in [.-PI/2,PI/2.]; then -PI/2 <= x & x <= PI/2 by TOPREAL5:1; then x = -PI/2 or x = PI/2 or (-PI/2 < x & x < PI/2) by REAL_1:def 5; then x = -PI/2 or x = PI/2 or x in ].-PI/2,PI/2.[ by JORDAN6:45; hence cos.x >= 0 by Th27,SIN_COS:33,81; end; theorem Th29: x in ].PI/2,3/2*PI.[ implies cos.x < 0 proof assume x in ].PI/2,3/2*PI.[; then PI/2 < x & x < 3/2*PI by JORDAN6:45; then PI/2+PI/2 < x+PI/2 & x+PI/2 < 3/2*PI+PI/2 by REAL_1:53; then PI < x+PI/2 & x+PI/2 < 3/2*PI+PI/2 by XCMPLX_1:66; then A1: x+PI/2 in ].PI,2*PI.[ by Th20,JORDAN6:45; sin.(x+PI/2) = cos.x by SIN_COS:83; hence cos.x < 0 by A1,Th25; end; theorem Th30: for x be real number st x in [.PI/2,3/2*PI.] holds cos.x <= 0 proof let x be real number; assume x in [.PI/2,3/2*PI.]; then PI/2 <= x & x <= 3/2*PI by TOPREAL5:1; then x = PI/2 or x = 3/2*PI or (PI/2 < x & x < 3/2*PI) by REAL_1:def 5; then x = PI/2 or x = 3/2*PI or x in ].PI/2,3/2*PI.[ by JORDAN6:45; hence cos.x <= 0 by Th20,Th29,SIN_COS:81; end; theorem Th31: x in ].3/2*PI,2*PI.[ implies cos.x > 0 proof assume x in ].3/2*PI,2*PI.[; then 3/2*PI < x & x < 2*PI by JORDAN6:45; then 3/2*PI-PI < x-PI & x-PI < 2*PI-PI by REAL_1:54; then PI/2 < x-PI & x-PI < 2*PI+-PI by Th20,XCMPLX_0:def 8; then PI/2 < x-PI & x-PI < PI by XCMPLX_1:184; then PI/2 < x-PI & x-PI < 3/2*PI by Th21,AXIOMS:22; then A1: x-PI in ].PI/2,3/2*PI.[ by JORDAN6:45; cos.(x-PI) = cos.(-(PI-x)) by XCMPLX_1:143 .= cos.(PI-x) by SIN_COS:33 .= cos.(PI+-x) by XCMPLX_0:def 8 .= -cos.(-x) by SIN_COS:83 .= -cos.x by SIN_COS:33; then -cos.x < -0 by A1,Th29; hence cos.x > 0 by REAL_1:50; end; theorem Th32: for x be real number st x in [.3/2*PI,2*PI.] holds cos.x >= 0 proof let x be real number; assume x in [.3/2*PI,2*PI.]; then 3/2*PI <= x & x <= 2*PI by TOPREAL5:1; then x = 3/2*PI or x = 2*PI or (3/2*PI < x & x < 2*PI) by REAL_1:def 5; then x = 3/2*PI or x = 2*PI or x in ].3/2*PI,2*PI.[ by JORDAN6:45; hence cos.x >= 0 by Th20,Th31,SIN_COS:81; end; theorem Th33: for x be real number st 0 <= x & x < 2*PI & sin x = 0 holds x = 0 or x = PI proof let x be real number; assume that A1: 0 <= x and A2: x < 2*PI and A3: sin x = 0; sin.x = 0 by A3,SIN_COS:def 21; then not x in ].0,PI.[ & not x in ].PI,2*PI.[ by Th23,Th25; then x = 0 or x >= PI & PI >= x by A1,A2,JORDAN6:45; hence x = 0 or x = PI by AXIOMS:21; end; theorem Th34: for x be real number st 0 <= x & x < 2*PI & cos x = 0 holds x = PI/2 or x = 3/2*PI proof let x be real number; assume that A1: 0 <= x and A2: x < 2*PI and A3: cos x = 0; A4: cos.x = 0 by A3,SIN_COS:def 23; then not x in ].-PI/2,PI/2.[ & not x in ].PI/2,3/2*PI.[ by Th27,Th29; then (-PI/2 >= x or x >= PI/2) & (PI/2 >= x or x >= 3/2*PI) by JORDAN6:45; then x = PI/2 or x = 3/2*PI or x > 3/2* PI by A1,Th21,REAL_1:def 5; then x = PI/2 or x = 3/2*PI or x in ].3/2* PI,2*PI.[ by A2,JORDAN6:45; hence x = PI/2 or x = 3/2*PI by A4,Th31; end; theorem Th35: sin is_increasing_on ].-PI/2,PI/2.[ proof A1: sin is_differentiable_on ].-PI/2,PI/2.[ proof ].-PI/2,PI/2.[ is open by RCOMP_1:25; hence sin is_differentiable_on ].-PI/2,PI/2.[ by FDIFF_1:34,SIN_COS:73; end; for x be Real st x in ].-PI/2,PI/2.[ holds diff(sin,x) > 0 proof let x be Real; assume x in ].-PI/2,PI/2.[; then 0 < cos.x by Th27; hence diff(sin,x) > 0 by SIN_COS:73; end; hence thesis by A1,Th21,ROLLE:9; end; theorem Th36: sin is_decreasing_on ].PI/2,3/2*PI.[ proof A1: sin is_differentiable_on ].PI/2,3/2*PI.[ proof ].PI/2,3/2*PI.[ is open by RCOMP_1:25; hence sin is_differentiable_on ].PI/2,3/2*PI.[ by FDIFF_1:34,SIN_COS:73; end; for x be Real st x in ].PI/2,3/2*PI.[ holds diff(sin,x) < 0 proof let x be Real; assume x in ].PI/2,3/2*PI.[; then 0 > cos.x by Th29; hence diff(sin,x) < 0 by SIN_COS:73; end; hence thesis by A1,Th21,ROLLE:10; end; theorem Th37: cos is_decreasing_on ].0,PI.[ proof A1: cos is_differentiable_on ].0,PI.[ proof ].0,PI.[ is open by RCOMP_1:25; hence cos is_differentiable_on ].0,PI.[ by FDIFF_1:34,SIN_COS:72; end; for x be Real st x in ].0,PI.[ holds diff(cos,x) < 0 proof let x be Real; assume A2: x in ].0,PI.[; A3: diff(cos,x) = -sin.x by SIN_COS:72; 0 < sin.x by A2,Th23; then 0-sin.x < 0 by REAL_2:105; hence diff(cos,x) < 0 by A3,XCMPLX_1:150; end; hence thesis by A1,Th21,ROLLE:10; end; theorem Th38: cos is_increasing_on ].PI,2*PI.[ proof A1: cos is_differentiable_on ].PI,2*PI.[ proof ].PI,2*PI.[ is open by RCOMP_1:25; hence cos is_differentiable_on ].PI,2*PI.[ by FDIFF_1:34,SIN_COS:72; end; for x be Real st x in ].PI,2*PI.[ holds diff(cos,x) > 0 proof let x be Real; assume A2: x in ].PI,2*PI.[; A3: diff(cos,x) = -sin.x by SIN_COS:72; 0 > sin.x by A2,Th25; then 0-sin.x > 0 by SQUARE_1:11; hence diff(cos,x) > 0 by A3,XCMPLX_1:150; end; hence thesis by A1,Th21,ROLLE:9; end; theorem sin is_increasing_on [.-PI/2,PI/2.] proof let r1,r2 be Real; assume that A1: r1 in [.-PI/2,PI/2.] /\ dom sin and A2: r2 in [.-PI/2,PI/2.] /\ dom sin and A3: r1 < r2; A4: r1 in [.-PI/2,PI/2.] & r1 in dom sin & r2 in [.-PI/2,PI/2.] & r2 in dom sin by A1,A2,XBOOLE_0:def 3; then A5: -PI/2 <= r1 & r1 <= PI/2 & -PI/2 <= r2 & r2 <= PI/2 by TOPREAL5:1; set r3 = (r1+r2)/2; abs(sin r3 ) <= 1 by SIN_COS:30; then abs(sin.r3 ) <= 1 by SIN_COS:def 21; then A6: sin.r3 >= -1 & sin.r3 <= 1 by ABSVALUE:12; abs(sin r2 ) <= 1 by SIN_COS:30; then abs(sin.r2 ) <= 1 by SIN_COS:def 21; then A7: sin.r2 >= -1 by ABSVALUE:12; A8: r1 < r3 & r3 < r2 by A3,TOPREAL3:3; then -PI/2 < r3 & r3 < PI/2 by A5,AXIOMS:22; then r3 in ].-PI/2,PI/2.[ & r3 in dom sin by JORDAN6:45,SIN_COS:27; then A9: r3 in ].-PI/2,PI/2.[ /\ dom sin by XBOOLE_0:def 3; now per cases by A5,REAL_1:def 5; suppose A10: -PI/2 < r1; then A11: -PI/2 < r2 by A3,AXIOMS:22; now per cases by A5,REAL_1:def 5; suppose A12: r2 < PI/2; then r1 < PI/2 by A3,AXIOMS:22; then r1 in ].-PI/2,PI/2.[ & r2 in ].-PI/2,PI/2.[ by A10,A11,A12,JORDAN6:45; then r1 in ].-PI/2,PI/2.[ /\ dom sin & r2 in ].-PI/2,PI/2.[ /\ dom sin by A4,XBOOLE_0:def 3; hence sin.r2 > sin.r1 by A3,Th35,RFUNCT_2:def 2; suppose A13: r2 = PI/2; then r1 in ].-PI/2,PI/2.[ by A3,A10,JORDAN6:45; then r1 in ].-PI/2,PI/2.[ /\ dom sin by A4,XBOOLE_0:def 3; then A14: sin.r3 > sin.r1 by A8,A9,Th35,RFUNCT_2:def 2; assume sin.r2 <= sin.r1; hence contradiction by A6,A13,A14,AXIOMS:22,SIN_COS:81; end; hence sin.r2 > sin.r1; suppose A15: -PI/2 = r1; now per cases by A5,REAL_1:def 5; suppose r2 < PI/2; then r2 in ].-PI/2,PI/2.[ by A3,A15,JORDAN6:45; then r2 in ].-PI/2,PI/2.[ /\ dom sin by A4,XBOOLE_0:def 3; then A16: sin.r2 > sin.r3 by A8,A9,Th35,RFUNCT_2:def 2; assume sin.r2 <= sin.r1; then sin.r2 <= -1 by A15,SIN_COS:33,81; hence contradiction by A6,A7,A16,AXIOMS:21; suppose r2 = PI/2; then sin.r2 = 1 & sin.r1 = -1 by A15,SIN_COS:33,81; hence sin.r2 > sin.r1; end; hence sin.r2 > sin.r1; end; hence sin.r2 > sin.r1; end; theorem sin is_decreasing_on [.PI/2,3/2*PI.] proof let r1,r2 be Real; assume that A1: r1 in [.PI/2,3/2*PI.] /\ dom sin and A2: r2 in [.PI/2,3/2*PI.] /\ dom sin and A3: r1 < r2; A4: r1 in [.PI/2,3/2*PI.] & r1 in dom sin & r2 in [.PI/2,3/2*PI.] & r2 in dom sin by A1,A2,XBOOLE_0:def 3; then A5: PI/2 <= r1 & r1 <= 3/2*PI & PI/2 <= r2 & r2 <= 3/2*PI by TOPREAL5: 1; abs(sin r1 ) <= 1 by SIN_COS:30; then abs(sin.r1 ) <= 1 by SIN_COS:def 21; then A6: sin.r1 >= -1 by ABSVALUE:12; set r3 = (r1+r2)/2; abs(sin r3 ) <= 1 by SIN_COS:30; then abs(sin.r3 ) <= 1 by SIN_COS:def 21; then A7: sin.r3 >= -1 & sin.r3 <= 1 by ABSVALUE:12; abs(sin r2 ) <= 1 by SIN_COS:30; then abs(sin.r2 ) <= 1 by SIN_COS:def 21; then A8: sin.r2 <= 1 by ABSVALUE:12; A9: r1 < r3 & r3 < r2 by A3,TOPREAL3:3; then PI/2 < r3 & r3 < 3/2*PI by A5,AXIOMS:22; then r3 in ].PI/2,3/2*PI.[ & r3 in dom sin by JORDAN6:45,SIN_COS:27; then A10: r3 in ].PI/2,3/2*PI.[ /\ dom sin by XBOOLE_0:def 3; now per cases by A5,REAL_1:def 5; suppose A11: PI/2 < r1; then A12: PI/2 < r2 by A3,AXIOMS:22; now per cases by A5,REAL_1:def 5; suppose A13: r2 < 3/2*PI; then r1 < 3/2*PI by A3,AXIOMS:22; then r1 in ].PI/2,3/2*PI.[ & r2 in ].PI/2,3/2*PI.[ by A11,A12,A13,JORDAN6:45; then r1 in ].PI/2,3/2*PI.[ /\ dom sin & r2 in ].PI/2,3/2*PI.[ /\ dom sin by A4,XBOOLE_0:def 3; hence sin.r2 < sin.r1 by A3,Th36,RFUNCT_2:def 3; suppose A14: r2 = 3/2*PI; then r1 in ].PI/2,3/2*PI.[ by A3,A11,JORDAN6:45; then r1 in ].PI/2,3/2*PI.[ /\ dom sin by A4,XBOOLE_0:def 3; then A15: sin.r3 < sin.r1 by A9,A10,Th36,RFUNCT_2:def 3; assume sin.r2 >= sin.r1; hence contradiction by A6,A7,A14,A15,Th20,AXIOMS:21,SIN_COS:81; end; hence sin.r2 < sin.r1; suppose A16: PI/2 = r1; now per cases by A5,REAL_1:def 5; suppose r2 < 3/2*PI; then r2 in ].PI/2,3/2*PI.[ by A3,A16,JORDAN6:45; then r2 in ].PI/2,3/2*PI.[ /\ dom sin by A4,XBOOLE_0:def 3; then A17: sin.r2 < sin.r3 by A9,A10,Th36,RFUNCT_2:def 3; assume sin.r2 >= sin.r1; hence contradiction by A7,A8,A16,A17,AXIOMS:21,SIN_COS:81; suppose r2 = 3/2*PI; hence sin.r2 < sin.r1 by A16,Th20,SIN_COS:81; end; hence sin.r2 < sin.r1; end; hence sin.r2 < sin.r1; end; theorem Th41: cos is_decreasing_on [.0,PI.] proof let r1,r2 be Real; assume that A1: r1 in [.0,PI.] /\ dom cos and A2: r2 in [.0,PI.] /\ dom cos and A3: r1 < r2; A4: r1 in [.0,PI.] & r1 in dom cos & r2 in [.0,PI.] & r2 in dom cos by A1,A2,XBOOLE_0:def 3; then A5: 0 <= r1 & r1 <= PI & 0 <= r2 & r2 <= PI by TOPREAL5:1; abs(cos r1) <= 1 by SIN_COS:30; then abs(cos.r1) <= 1 by SIN_COS:def 23; then A6: cos.r1 >= -1 by ABSVALUE:12; set r3 = (r1+r2)/2; abs(cos r3) <= 1 by SIN_COS:30; then abs(cos.r3) <= 1 by SIN_COS:def 23; then A7: cos.r3 >= -1 & cos.r3 <= 1 by ABSVALUE:12; abs(cos r2) <= 1 by SIN_COS:30; then abs(cos.r2) <= 1 by SIN_COS:def 23; then A8: cos.r2 <= 1 by ABSVALUE:12; A9: r1 < r3 & r3 < r2 by A3,TOPREAL3:3; then 0 < r3 & r3 < PI by A5,AXIOMS:22; then r3 in ].0,PI.[ & r3 in dom cos by JORDAN6:45,SIN_COS:27; then A10: r3 in ].0,PI.[ /\ dom cos by XBOOLE_0:def 3; now per cases by A4,TOPREAL5:1; suppose A11: 0 < r1; then A12: 0 < r2 by A3,AXIOMS:22; now per cases by A5,REAL_1:def 5; suppose A13: r2 < PI; then r1 < PI by A3,AXIOMS:22; then r1 in ].0,PI.[ & r2 in ].0,PI.[ by A11,A12,A13,JORDAN6:45; then r1 in ].0,PI.[ /\ dom cos & r2 in ].0,PI.[ /\ dom cos by A4,XBOOLE_0:def 3; hence cos.r2 < cos.r1 by A3,Th37,RFUNCT_2:def 3; suppose A14: r2 = PI; then r1 in ].0,PI.[ by A3,A11,JORDAN6:45; then r1 in ].0,PI.[ /\ dom cos by A4,XBOOLE_0:def 3; then A15: cos.r3 < cos.r1 by A9,A10,Th37,RFUNCT_2:def 3; assume cos.r2 >= cos.r1; hence contradiction by A6,A7,A14,A15,AXIOMS:21,SIN_COS:81; end; hence cos.r2 < cos.r1; suppose A16: 0 = r1; now per cases by A5,REAL_1:def 5; suppose r2 < PI; then r2 in ].0,PI.[ by A3,A16,JORDAN6:45; then r2 in ].0,PI.[ /\ dom cos by A4,XBOOLE_0:def 3; then A17: cos.r2 < cos.r3 by A9,A10,Th37,RFUNCT_2:def 3; assume cos.r2 >= cos.r1; hence contradiction by A7,A8,A16,A17,AXIOMS:21,SIN_COS:33; suppose r2 = PI; hence cos.r2 < cos.r1 by A16,SIN_COS:33,81; end; hence cos.r2 < cos.r1; end; hence cos.r2 < cos.r1; end; theorem Th42: cos is_increasing_on [.PI,2*PI.] proof let r1,r2 be Real; assume that A1: r1 in [.PI,2*PI.] /\ dom cos and A2: r2 in [.PI,2*PI.] /\ dom cos and A3: r1 < r2; A4: r1 in [.PI,2*PI.] & r1 in dom cos & r2 in [.PI,2*PI.] & r2 in dom cos by A1,A2,XBOOLE_0:def 3; then A5: PI <= r1 & r1 <= 2*PI & PI <= r2 & r2 <= 2*PI by TOPREAL5:1; set r3 = (r1+r2)/2; abs(cos r3 ) <= 1 by SIN_COS:30; then abs(cos.r3 ) <= 1 by SIN_COS:def 23; then A6: cos.r3 >= -1 & cos.r3 <= 1 by ABSVALUE:12; abs(cos r2 ) <= 1 by SIN_COS:30; then abs(cos.r2 ) <= 1 by SIN_COS:def 23; then A7: cos.r2 >= -1 by ABSVALUE:12; A8: r1 < r3 & r3 < r2 by A3,TOPREAL3:3; then PI < r3 & r3 < 2*PI by A5,AXIOMS:22; then r3 in ].PI,2*PI.[ & r3 in dom cos by JORDAN6:45,SIN_COS:27; then A9: r3 in ].PI,2*PI.[ /\ dom cos by XBOOLE_0:def 3; now per cases by A5,REAL_1:def 5; suppose A10: PI < r1; then A11: PI < r2 by A3,AXIOMS:22; now per cases by A5,REAL_1:def 5; suppose A12: r2 < 2*PI; then r1 < 2*PI by A3,AXIOMS:22; then r1 in ].PI,2*PI.[ & r2 in ].PI,2*PI.[ by A10,A11,A12,JORDAN6:45; then r1 in ].PI,2*PI.[ /\ dom cos & r2 in ].PI,2*PI.[ /\ dom cos by A4,XBOOLE_0:def 3; hence cos.r2 > cos.r1 by A3,Th38,RFUNCT_2:def 2; suppose A13: r2 = 2*PI; then r1 in ].PI,2*PI.[ by A3,A10,JORDAN6:45; then r1 in ].PI,2*PI.[ /\ dom cos by A4,XBOOLE_0:def 3; then A14: cos.r3 > cos.r1 by A8,A9,Th38,RFUNCT_2:def 2; assume cos.r2 <= cos.r1; hence contradiction by A6,A13,A14,AXIOMS:22,SIN_COS:81; end; hence cos.r2 > cos.r1; suppose A15: PI = r1; now per cases by A5,REAL_1:def 5; suppose r2 < 2*PI; then r2 in ].PI,2*PI.[ by A3,A15,JORDAN6:45; then r2 in ].PI,2*PI.[ /\ dom cos by A4,XBOOLE_0:def 3; then A16: cos.r2 > cos.r3 by A8,A9,Th38,RFUNCT_2:def 2; assume cos.r2 <= cos.r1; hence contradiction by A6,A7,A15,A16,AXIOMS:21,SIN_COS:81; suppose r2 = 2*PI; hence cos.r2 > cos.r1 by A15,SIN_COS:81; end; hence cos.r2 > cos.r1; end; hence cos.r2 > cos.r1; end; theorem Th43: sin is_continuous_on REAL & for x,y be real number holds sin is_continuous_on [.x,y.] & sin is_continuous_on ].x,y.[ proof thus A1: sin is_continuous_on REAL by FDIFF_1:33,SIN_COS:73; let x,y be real number; thus thesis by A1,FCONT_1:17; end; theorem Th44: cos is_continuous_on REAL & for x,y be real number holds cos is_continuous_on [.x,y.] & cos is_continuous_on ].x,y.[ proof thus A1: cos is_continuous_on REAL by FDIFF_1:33,SIN_COS:72; let x,y be real number; thus thesis by A1,FCONT_1:17; end; theorem Th45: sin.x in [.-1,1 .] & cos.x in [.-1,1 .] proof abs(sin x) <= 1 & abs(cos x) <= 1 by SIN_COS:30; then abs(sin.x) <= 1 & abs(cos.x) <= 1 by SIN_COS:def 21,def 23; then -1 <= sin.x & sin.x <= 1 & -1 <= cos.x & cos.x <= 1 by ABSVALUE:12; hence thesis by TOPREAL5:1; end; theorem rng sin = [.-1,1 .] proof now let y be set; thus y in [.-1,1 .] implies ex x be set st x in dom sin & y = sin.x proof assume A1: y in [.-1,1 .]; then reconsider y1=y as Real; A2: sin is_continuous_on [.-PI/2,PI/2 .] by Th43; y1 in [.-1,1 .] \/ [.1,sin.(-PI/2).] by A1,XBOOLE_0:def 2; then y1 in [.sin.(-PI/2),sin.(PI/2).] \/ [.sin.(PI/2),sin.(-PI/2).] by SIN_COS:33,81; then consider x be Real such that x in [.-PI/2,PI/2 .] and A3: y1 = sin.x by A2,Th21,FCONT_2:16; take x; x in REAL; hence x in dom sin & y = sin.x by A3,SIN_COS:def 20; end; thus (ex x be set st x in dom sin & y = sin.x) implies y in [.-1,1 .] proof given x be set such that A4: x in dom sin and A5: y = sin.x; reconsider x1=x as Real by A4,SIN_COS:def 20; y = sin.x1 by A5; hence y in [.-1,1 .] by Th45; end; end; hence thesis by FUNCT_1:def 5; end; theorem rng cos = [.-1,1 .] proof now let y be set; thus y in [.-1,1 .] implies ex x be set st x in dom cos & y = cos.x proof assume A1: y in [.-1,1 .]; then reconsider y1=y as Real; A2: cos is_continuous_on [.0,PI.] by Th44; y1 in [.cos.0,cos.PI.] \/ [.cos.PI,cos.0 .] by A1,SIN_COS:33,81,XBOOLE_0:def 2; then consider x be Real such that x in [.0,PI.] and A3: y1 = cos.x by A2,Th21,FCONT_2:16; take x; x in REAL; hence x in dom cos & y = cos.x by A3,SIN_COS:def 22; end; thus (ex x be set st x in dom cos & y = cos.x) implies y in [.-1,1 .] proof given x be set such that A4: x in dom cos and A5: y = cos.x; reconsider x1=x as Real by A4,SIN_COS:def 22; y = cos.x1 by A5; hence y in [.-1,1 .] by Th45; end; end; hence thesis by FUNCT_1:def 5; end; theorem rng (sin|[.-PI/2,PI/2.]) = [.-1,1 .] proof set sin1 = sin|[.-PI/2,PI/2.]; now let y be set; thus y in [.-1,1 .] implies ex x be set st x in dom sin1 & y = sin1.x proof assume A1: y in [.-1,1 .]; then reconsider y1=y as Real; sin is_continuous_on [.-PI/2,PI/2 .] by Th43; then A2: sin1 is_continuous_on [.-PI/2,PI/2 .] by FCONT_1:16; -PI/2 in [.-PI/2,PI/2.] & PI/2 in [.-PI/2,PI/2.] by Th21,TOPREAL5:1; then sin1.(PI/2) = sin.(PI/2) & sin1.(-PI/2) = sin.(-PI/2) by FUNCT_1:72; then y1 in [.sin1.(-PI/2),sin1.(PI/2).] by A1,SIN_COS:33,81; then y1 in [.sin1.(-PI/2),sin1.(PI/2).]\/[.sin1.(PI/2),sin1.(-PI/2).] by XBOOLE_0:def 2; then consider x be Real such that A3: x in [.-PI/2,PI/2 .] and A4: y1 = sin1.x by A2,Th21,FCONT_2:16; take x; x in REAL /\ [.-PI/2,PI/2 .] by A3,XBOOLE_0:def 3; then x in dom sin /\ [.-PI/2,PI/2 .] by SIN_COS:def 20; hence x in dom sin1 & y = sin1.x by A4,FUNCT_1:68; end; thus (ex x be set st x in dom sin1 & y = sin1.x) implies y in [.-1,1 .] proof given x be set such that A5: x in dom sin1 and A6: y = sin1.x; dom sin1 c= dom sin by FUNCT_1:76; then reconsider x1=x as Real by A5,SIN_COS:def 20; y = sin.x1 by A5,A6,FUNCT_1:70; hence y in [.-1,1 .] by Th45; end; end; hence thesis by FUNCT_1:def 5; end; theorem rng (sin|[.PI/2,3/2*PI.]) = [.-1,1 .] proof set sin1 = sin|[.PI/2,3/2*PI.]; now let y be set; thus y in [.-1,1 .] implies ex x be set st x in dom sin1 & y = sin1.x proof assume A1: y in [.-1,1 .]; then reconsider y1=y as Real; sin is_continuous_on [.PI/2,3/2*PI.] by Th43; then A2: sin1 is_continuous_on [.PI/2,3/2*PI.] by FCONT_1:16; PI/2 in [.PI/2,3/2*PI.] & 3/2*PI in [.PI/2,3/2*PI.] by Th21,TOPREAL5:1; then sin1.(PI/2) = sin.(PI/2) & sin1.(3/2*PI) = sin.(3/2*PI) by FUNCT_1:72; then y1 in [.sin1.(PI/2),sin1.(3/2*PI).] \/ [.sin1.(3/2*PI),sin1.(PI/2).] by A1,Th20,SIN_COS:81,XBOOLE_0:def 2; then consider x be Real such that A3: x in [.PI/2,3/2*PI.] and A4: y1 = sin1.x by A2,Th21,FCONT_2:16; take x; x in REAL /\ [.PI/2,3/2*PI.] by A3,XBOOLE_0:def 3; then x in dom sin /\ [.PI/2,3/2*PI.] by SIN_COS:def 20; hence x in dom sin1 & y = sin1.x by A4,FUNCT_1:68; end; thus (ex x be set st x in dom sin1 & y = sin1.x) implies y in [.-1,1 .] proof given x be set such that A5: x in dom sin1 and A6: y = sin1.x; dom sin1 c= dom sin by FUNCT_1:76; then reconsider x1=x as Real by A5,SIN_COS:def 20; y = sin.x1 by A5,A6,FUNCT_1:70; hence y in [.-1,1 .] by Th45; end; end; hence thesis by FUNCT_1:def 5; end; theorem Th50: rng (cos|[.0,PI.]) = [.-1,1 .] proof set cos1 = cos|[.0,PI.]; now let y be set; thus y in [.-1,1 .] implies ex x be set st x in dom cos1 & y = cos1.x proof assume A1: y in [.-1,1 .]; then reconsider y1=y as Real; cos is_continuous_on [.0,PI.] by Th44; then A2: cos1 is_continuous_on [.0,PI.] by FCONT_1:16; 0 in [.0,PI.] & PI in [.0,PI.] by Th21,TOPREAL5:1; then cos1.0 = cos.0 & cos1.PI = cos.PI by FUNCT_1:72; then y1 in [.cos1.0,cos1.PI.] \/ [.cos1.PI,cos1.0 .] by A1,SIN_COS:33,81,XBOOLE_0:def 2; then consider x be Real such that A3: x in [.0,PI.] and A4: y1 = cos1.x by A2,Th21,FCONT_2:16; take x; x in REAL /\ [.0,PI.] by A3,XBOOLE_0:def 3; then x in dom cos /\ [.0,PI.] by SIN_COS:def 22; hence x in dom cos1 & y = cos1.x by A4,FUNCT_1:68; end; thus (ex x be set st x in dom cos1 & y = cos1.x) implies y in [.-1,1 .] proof given x be set such that A5: x in dom cos1 and A6: y = cos1.x; dom cos1 c= dom cos by FUNCT_1:76; then reconsider x1=x as Real by A5,SIN_COS:def 22; y = cos.x1 by A5,A6,FUNCT_1:70; hence y in [.-1,1 .] by Th45; end; end; hence thesis by FUNCT_1:def 5; end; theorem Th51: rng (cos|[.PI,2*PI.]) = [.-1,1 .] proof set cos1 = cos|[.PI,2*PI.]; now let y be set; thus y in [.-1,1 .] implies ex x be set st x in dom cos1 & y = cos1.x proof assume A1: y in [.-1,1 .]; then reconsider y1=y as Real; cos is_continuous_on [.PI,2*PI.] by Th44; then A2: cos1 is_continuous_on [.PI,2*PI.] by FCONT_1:16; PI in [.PI,2*PI.] & 2*PI in [.PI,2*PI.] by Th21,TOPREAL5:1; then cos1.PI = cos.PI & cos1.(2*PI) = cos.(2*PI) by FUNCT_1:72; then y1 in [.cos1.PI,cos1.(2*PI).] \/ [.cos1.(2*PI),cos1.PI.] by A1,SIN_COS:81,XBOOLE_0:def 2; then consider x be Real such that A3: x in [.PI,2*PI.] and A4: y1 = cos1.x by A2,Th21,FCONT_2:16; take x; x in REAL /\ [.PI,2*PI.] by A3,XBOOLE_0:def 3; then x in dom cos /\ [.PI,2*PI.] by SIN_COS:def 22; hence x in dom cos1 & y = cos1.x by A4,FUNCT_1:68; end; thus (ex x be set st x in dom cos1 & y = cos1.x) implies y in [.-1,1 .] proof given x be set such that A5: x in dom cos1 and A6: y = cos1.x; dom cos1 c= dom cos by FUNCT_1:76; then reconsider x1=x as Real by A5,SIN_COS:def 22; y = cos.x1 by A5,A6,FUNCT_1:70; hence y in [.-1,1 .] by Th45; end; end; hence thesis by FUNCT_1:def 5; end; begin :: Argument of Complex Number definition let z be Element of F_Complex; func Arg z -> Real means :Def1: z = [**|.z.|*cos it,|.z.|*sin it**] & 0 <= it & it < 2*PI if z <> 0.F_Complex otherwise it = 0; existence proof thus z <> 0.F_Complex implies ex r be Real st z = [**|.z.|*cos r,|.z.|*sin r**] & 0 <= r & r < 2*PI proof assume z <> 0.F_Complex; then A1: |.z.| <> 0 by COMPLFLD:94; A2: |.z.| >= 0 by COMPLFLD:95; Re z <= |.z.| by HAHNBAN1:18; then A3: Re z/|.z.| <= 1 by A1,A2,REAL_2:117; reconsider z1=z as Element of COMPLEX by COMPLFLD:def 1; now per cases; suppose A4: Im z >= 0; set 0PI = [.0,PI.]; reconsider cos1 = cos|0PI as PartFunc of 0PI,REAL by PARTFUN1:43; reconsider cos1 as one-to-one PartFunc of 0PI,REAL by Th41,RFUNCT_2:82; now per cases; suppose Re z/|.z.| in dom (cos1"); then cos1".(Re z/|.z.|) in 0PI by PARTFUN1:27; hence cos1".(Re z/|.z.|) is real number by XREAL_0:def 1; suppose not Re z/|.z.| in dom (cos1"); hence cos1".(Re z/|.z.|) is real number by FUNCT_1:def 4; end; then reconsider r = cos1".(Re z/|.z.|) as Real by XREAL_0:def 1; take r; Re z >= -|.z.| by Th5; then -1 <= Re z/|.z.| by A1,A2,REAL_2:117; then A5: Re z/|.z.| in rng cos1 by A3,Th50,TOPREAL5:1; then Re z/|.z.| in dom (cos1") by FUNCT_1:55; then r in rng (cos1") by FUNCT_1:def 5; then r in dom cos1 by FUNCT_1:55; then A6: r in [.0,PI.] by RELAT_1:86; A7: cos r = cos.r by SIN_COS:def 23 .= cos1.r by A6,FUNCT_1:72 .= Re z/|.z.| by A5,FUNCT_1:57; then A8: Re z = |.z.|*cos r by A1,XCMPLX_1:88; A9: |.z.|^2 = (Re z)^2 + (Im z)^2 by Th7; A10: |.z.|^2 <> 0 by A1,SQUARE_1:73; 0 <= r & r <= PI by A6,TOPREAL5:1; then (0 = r or 0 < r) & (r = PI or r < PI) by REAL_1:def 5; then r = 0 or r = PI or r in ].0,PI.[ by JORDAN6:45; then A11: sin.r >= 0 by Th23,SIN_COS:33,81; (cos.r)^2 + (sin.r)^2 = 1 by SIN_COS:31; then (sin.r)^2 = 1 - (cos.r)^2 by XCMPLX_1:26 .= 1 - (Re z/|.z.|)^2 by A7,SIN_COS:def 23 .= 1 - (Re z)^2/|.z.|^2 by SQUARE_1:69 .= |.z.|^2/|.z.|^2 - (Re z)^2/|.z.|^2 by A10,XCMPLX_1:60 .= (|.z.|^2 - (Re z)^2)/|.z.|^2 by XCMPLX_1:121 .= (Im z)^2/|.z.|^2 by A9,XCMPLX_1:26 .= ((Im z)/|.z.|)^2 by SQUARE_1:69; then sin.r = sqrt((Im z)/|.z.|)^2 by A11,SQUARE_1:89 .= abs((Im z)/|.z.|) by SQUARE_1:91 .= abs(Im z)/abs |.z.| by ABSVALUE:16 .= abs(Im z)/|.z.| by HAHNBAN1:12; then abs(Im z) = |.z.|*sin.r by A1,XCMPLX_1:88; then A12: Im z = |.z.|*sin.r by A4,ABSVALUE:def 1 .= |.z.|*sin r by SIN_COS:def 21; z1 = [*Re z1,Im z1*] by COMPLEX1:8 .= [*Re z,Im z1*] by HAHNBAN1:def 3 .= [*Re z,Im z*] by HAHNBAN1:def 4; hence z = [**|.z.|*cos r,|.z.|*sin r**] by A8,A12,HAHNBAN1:def 1; thus 0 <= r by A6,TOPREAL5:1; r <= PI by A6,TOPREAL5:1; hence r < 2*PI by Th21,AXIOMS:22; suppose A13: Im z < 0; now per cases; suppose Re z <> |.z.|; then A14: Re z/|.z.| <> 1 by XCMPLX_1:58; set 0PI = [.PI,2*PI.]; reconsider cos1 = cos|0PI as PartFunc of 0PI,REAL by PARTFUN1:43; reconsider cos1 as one-to-one PartFunc of 0PI,REAL by Th42,RFUNCT_2:82; now per cases; suppose Re z/|.z.| in dom (cos1"); then cos1".(Re z/|.z.|) in 0PI by PARTFUN1:27; hence cos1".(Re z/|.z.|) is real number by XREAL_0:def 1; suppose not Re z/|.z.| in dom (cos1"); hence cos1".(Re z/|.z.|) is real number by CARD_1:51,FUNCT_1:def 4; end; then reconsider r = cos1".(Re z/|.z.|) as Real by XREAL_0:def 1; take r; Re z >= -|.z.| by Th5; then -1 <= Re z/|.z.| by A1,A2,REAL_2:117; then A15: Re z/|.z.| in rng cos1 by A3,Th51,TOPREAL5:1; then A16: Re z/|.z.| in dom (cos1") by FUNCT_1:55; then r in rng (cos1") by FUNCT_1:def 5; then r in dom cos1 by FUNCT_1:55; then A17: r in [.PI,2*PI.] by RELAT_1:86; A18: cos r = cos.r by SIN_COS:def 23 .= cos1.r by A17,FUNCT_1:72 .= Re z/|.z.| by A15,FUNCT_1:57; then A19: Re z = |.z.|*cos r by A1,XCMPLX_1:88; A20: |.z.|^2 = (Re z)^2 + (Im z)^2 by Th7; A21: |.z.|^2 <> 0 by A1,SQUARE_1:73; PI <= r & r <= 2*PI by A17,TOPREAL5:1; then (PI = r or PI < r) & (r = 2*PI or r < 2*PI) by REAL_1:def 5; then r = PI or r = 2*PI or r in ].PI,2*PI.[ by JORDAN6:45; then A22: sin.r <= 0 by Th25,SIN_COS:81; (cos.r)^2 + (sin.r)^2 = 1 by SIN_COS:31; then (sin.r)^2 = 1 - (cos.r)^2 by XCMPLX_1:26 .= 1 - (Re z/|.z.|)^2 by A18,SIN_COS:def 23 .= 1 - (Re z)^2/|.z.|^2 by SQUARE_1:69 .= |.z.|^2/|.z.|^2 - (Re z)^2/|.z.|^2 by A21,XCMPLX_1:60 .= (|.z.|^2 - (Re z)^2)/|.z.|^2 by XCMPLX_1:121 .= (Im z)^2/|.z.|^2 by A20,XCMPLX_1:26 .= ((Im z)/|.z.|)^2 by SQUARE_1:69; then -sin.r = sqrt((Im z)/|.z.|)^2 by A22,SQUARE_1:90 .= abs((Im z)/|.z.|) by SQUARE_1:91 .= abs(Im z)/abs |.z.| by ABSVALUE:16 .= abs(Im z)/|.z.| by HAHNBAN1:12; then sin.r = -(abs(Im z)/|.z.|); then sin.r = (-abs(Im z))/|.z.| by XCMPLX_1:188; then -abs(Im z) = |.z.|*sin.r by A1,XCMPLX_1:88; then A23: --Im z = |.z.|*sin.r by A13,ABSVALUE:def 1 .= |.z.|*sin r by SIN_COS:def 21; z1 = [*Re z1,Im z1*] by COMPLEX1:8 .= [*Re z,Im z1*] by HAHNBAN1:def 3 .= [*Re z,Im z*] by HAHNBAN1:def 4; hence z = [**|.z.|*cos r,|.z.|*sin r**] by A19,A23,HAHNBAN1:def 1; PI <= r by A17,TOPREAL5:1; hence 0 <= r by Th21,AXIOMS:22; A24: r <> 2*PI proof A25: dom cos = REAL by SIN_COS:def 22; A26: cos1" is one-to-one by FUNCT_1:62; 1 in rng cos1 by Th51,TOPREAL5:1; then A27: 1 in dom (cos1") by FUNCT_1:55; assume A28: r = 2*PI; A29: 2*PI in [.PI,2*PI.] by Th21,TOPREAL5:1; then A30: 2*PI in dom cos1 by A25,RELAT_1:86; cos1.(2*PI) = 1 by A29,FUNCT_1:72,SIN_COS:81; then cos1".1 = 2*PI by A30,FUNCT_1:54; hence contradiction by A14,A16,A26,A27,A28,FUNCT_1:def 8; end; r <= 2*PI by A17,TOPREAL5:1; hence r < 2*PI by A24,REAL_1:def 5; suppose A31: Re z = |.z.|; then (Re z)^2 = (Re z)^2 + (Im z)^2 by Th7; then (Re z)^2 - (Re z)^2 = (Im z)^2 by XCMPLX_1:26; then (Im z)^2 = 0 by XCMPLX_1:14; then A32: Im z = 0 by SQUARE_1:73; consider z2 be Element of COMPLEX such that A33: z = z2 and A34: Re z = Re z2 by HAHNBAN1:def 3; consider z3 be Element of COMPLEX such that A35: z = z3 and A36: Im z = Im z3 by HAHNBAN1:def 4; A37: z = [*Re z2,Im z3*] by A33,A35,COMPLEX1:8; reconsider r=0 as Real; take r; thus z = [**|.z.|*cos r,|.z.|*sin r**] by A31,A32,A34,A36,A37,HAHNBAN1:def 1,SIN_COS:34; thus 0 <= r; thus r < 2*PI by Th21; end; hence thesis; end; hence thesis; end; thus thesis; end; uniqueness proof z <> 0.F_Complex implies for x,y be Real st z = [**|.z.|*cos x,|.z.|*sin x**] & 0 <= x & x < 2*PI & z = [**|.z.|*cos y,|.z.|*sin y**] & 0 <= y & y < 2*PI holds x = y proof assume z <> 0.F_Complex; then A38: |.z.| <> 0 by COMPLFLD:94; let x,y be Real; assume that A39: z = [**|.z.|*cos x,|.z.|*sin x**] and A40: 0 <= x and A41: x < 2*PI and A42: z = [**|.z.|*cos y,|.z.|*sin y**] and A43: 0 <= y and A44: y < 2*PI; [*|.z.|*cos x,|.z.|*sin x*] = [**|.z.|*cos y,|.z.|*sin y**] by A39,A42,HAHNBAN1:def 1 .= [*|.z.|*cos y,|.z.|*sin y*] by HAHNBAN1:def 1; then |.z.|*cos x = |.z.|*cos y & |.z.|*sin x = |.z.|*sin y by ARYTM_0:12 ; then cos x = cos y & sin x = sin y by A38,XCMPLX_1:5; then A45: cos x = cos y & sin x = sin.y by SIN_COS:def 21; then cos x = cos.y & sin.x = sin.y by SIN_COS:def 21,def 23; then A46: cos.x = cos.y & sin.x = sin.y by SIN_COS:def 23; A47: dom cos = REAL by SIN_COS:def 22; now per cases; suppose x <= PI & y <= PI; then x in [.0,PI.] & y in [.0,PI.] by A40,A43,TOPREAL5:1; then A48: x in [.0,PI.] /\ dom cos & y in [.0,PI.] /\ dom cos by A47,XBOOLE_0:def 3; assume x <> y; then x < y or y < x by AXIOMS:21; hence contradiction by A46,A48,Th41,RFUNCT_2:def 3; suppose x > PI & y > PI; then x in [.PI,2*PI.] & y in [.PI,2*PI.] by A41,A44,TOPREAL5:1; then A49: x in [.PI,2*PI.] /\ dom cos & y in [.PI,2*PI.] /\ dom cos by A47,XBOOLE_0:def 3 ; assume x <> y; then x < y or y < x by AXIOMS:21; hence contradiction by A46,A49,Th42,RFUNCT_2:def 2; suppose x <= PI & y > PI; then x in [.0,PI.] & y in ].PI,2*PI.[ by A40,A44,JORDAN6:45,TOPREAL5:1; then sin.x >= 0 & sin.y < 0 by Th24,Th25; hence x = y by A45,SIN_COS:def 21; suppose y <= PI & x > PI; then y in [.0,PI.] & x in ].PI,2*PI.[ by A41,A43,JORDAN6:45,TOPREAL5:1; then sin.y >= 0 & sin.x < 0 by Th24,Th25; hence x = y by A45,SIN_COS:def 21; end; hence x = y; end; hence thesis; end; consistency; end; theorem Th52: for z be Element of F_Complex holds 0 <= Arg z & Arg z < 2*PI proof let z be Element of F_Complex; 0 <= Arg z & Arg z < 2*PI or z = 0.F_Complex by Def1; hence thesis by Def1,Th21; end; theorem Th53: for x be Real st x >= 0 holds Arg [**x,0**] = 0 proof let x be Real; assume A1: x >= 0; A2: 0 <= Arg [**x,0**] & Arg [**x,0**] < 2*PI by Th52; per cases by A1; suppose A3: x > -0; then [*x,0*] <> 0.F_Complex by ARYTM_0:12,L0,COMPLFLD:9; then A4: [**x,0**] <> 0.F_Complex by HAHNBAN1:def 1; then A5: |. [**x,0**] .| <> 0 by COMPLFLD:94; [**x,0**] = [**|. [**x,0**] .|*cos Arg [**x,0**], |. [**x,0**] .|*sin Arg [**x,0**]**] by A4,Def1; then A6: |. [**x,0**] .|*cos Arg [**x,0**] = x & |. [**x,0**] .|*sin Arg [**x,0**] = 0 by Th8; then sin Arg [**x,0**] = 0 by A5,XCMPLX_1:6; then Arg [**x,0**] = 0 or |. [**x,0**] .|*-1 = x by A2,A6,Th33,SIN_COS:82; then Arg [**x,0**] = 0 or -|. [**x,0**] .| = x by XCMPLX_1:180; then Arg [**x,0**] = 0 or |. [**x,0**] .| < 0 by A3,REAL_1:50; hence Arg [**x,0**] = 0 by COMPLFLD:95; suppose x = 0; then [**x,0**] = 0.F_Complex by L0,COMPLFLD:9,HAHNBAN1:def 1 ; hence thesis by Def1; end; theorem Th54: for x be Real st x < 0 holds Arg [**x,0**] = PI proof let x be Real; assume A1: x < 0; A2: 0 <= Arg [**x,0**] & Arg [**x,0**] < 2*PI by Th52; [*x,0*] <> 0.F_Complex by A1,ARYTM_0:12,L0,COMPLFLD:9; then A3: [**x,0**] <> 0.F_Complex by HAHNBAN1:def 1; then A4: |. [**x,0**] .| <> 0 by COMPLFLD:94; [**x,0**] = [**|. [**x,0**] .|*cos Arg [**x,0**], |. [**x,0**] .|*sin Arg [**x,0**]**] by A3,Def1; then A5: |. [**x,0**] .|*cos Arg [**x,0**] = x & |. [**x,0**] .|*sin Arg [**x,0**] = 0 by Th8; then sin Arg [**x,0**] = 0 by A4,XCMPLX_1:6; then Arg [**x,0**] = PI or |. [**x,0**] .|*1 = x by A2,A5,Th33,SIN_COS:34; hence thesis by A1,COMPLFLD:95; end; theorem Th55: for x be Real st x > 0 holds Arg [**0,x**] = PI/2 proof let x be Real; assume A1: x > 0; then A2: x > -0; A3: 0 <= Arg [**0,x**] & Arg [**0,x**] < 2*PI by Th52; [*0,x*] <> 0.F_Complex by A1,ARYTM_0:12,L0,COMPLFLD:9; then A4: [**0,x**] <> 0.F_Complex by HAHNBAN1:def 1; then A5: |. [**0,x**] .| <> 0 by COMPLFLD:94; [**0,x**] = [**|. [**0,x**] .|*cos Arg [**0,x**], |. [**0,x**] .|*sin Arg [**0,x**]**] by A4,Def1; then A6: |. [**0,x**] .|*cos Arg [**0,x**] = 0 & |. [**0,x**] .|*sin Arg [**0,x**] = x by Th8; then cos Arg [**0,x**] = 0 by A5,XCMPLX_1:6; then Arg [**0,x**] = PI/2 or |. [**0,x**] .|*-1 = x by A3,A6,Th20,Th34,SIN_COS:82; then Arg [**0,x**] = PI/2 or -|. [**0,x**] .| = x by XCMPLX_1:180; then Arg [**0,x**] = PI/2 or |. [**0,x**] .| < 0 by A2,REAL_1:50; hence thesis by COMPLFLD:95; end; theorem Th56: for x be Real st x < 0 holds Arg [**0,x**] = 3/2*PI proof let x be Real; assume A1: x < 0; A2: 0 <= Arg [**0,x**] & Arg [**0,x**] < 2*PI by Th52; [*0,x*] <> 0.F_Complex by A1,ARYTM_0:12,L0,COMPLFLD:9; then A3: [**0,x**] <> 0.F_Complex by HAHNBAN1:def 1; then A4: |. [**0,x**] .| <> 0 by COMPLFLD:94; [**0,x**] = [**|. [**0,x**] .|*cos Arg [**0,x**], |. [**0,x**] .|*sin Arg [**0,x**]**] by A3,Def1; then A5: |. [**0,x**] .|*cos Arg [**0,x**] = 0 & |. [**0,x**] .|*sin Arg [**0,x**] = x by Th8; then cos Arg [**0,x**] = 0 by A4,XCMPLX_1:6; then Arg [**0,x**] = 3/2*PI or |. [**0,x**] .|*1 = x by A2,A5,Th34,SIN_COS:82; hence thesis by A1,COMPLFLD:95; end; theorem Arg 1_(F_Complex) = 0 proof 1_(F_Complex) = [**1,0**] by L1,COMPLFLD:10,HAHNBAN1:def 1; hence thesis by Th53; end; theorem Arg i_FC = PI/2 by Th55,HAHNBAN1:6; theorem Th59: for z be Element of F_Complex holds Arg z in ].0,PI/2.[ iff Re z > 0 & Im z > 0 proof let z be Element of F_Complex; thus Arg z in ].0,PI/2.[ implies Re z > 0 & Im z > 0 proof assume A1: Arg z in ].0,PI/2.[; then A2: Arg z > 0 & Arg z < PI/2 by JORDAN6:45; then A3: z <> 0.F_Complex by Def1; then z = [**|.z.|*cos Arg z,|.z.|*sin Arg z**] by Def1; then A4: Re z = |.z.|*cos Arg z & Im z = |.z.|*sin Arg z by HAHNBAN1:15; A5: |.z.| > 0 by A3,COMPLFLD:96; cos Arg z > 0 by A1,SIN_COS:86; hence Re z > 0 by A4,A5,SQUARE_1:21; Arg z < PI by A2,Th21,AXIOMS:22; then Arg z in ].0,PI.[ by A2,JORDAN6:45; then sin.Arg z > 0 by Th23; then sin Arg z > 0 by SIN_COS:def 21; hence Im z > 0 by A4,A5,SQUARE_1:21; end; assume that A6: Re z > 0 and A7: Im z > 0; z = [**Re z,Im z**] by Th9; then A8: z <> 0.F_Complex by A6,Th8,Th10; then A9: |.z.| > 0 by COMPLFLD:96; A10: 0 <= Arg z & Arg z < 2*PI by Th52; z = [**|.z.|*cos Arg z,|.z.|*sin Arg z**] by A8,Def1; then |.z.|*cos Arg z > 0 & |.z.|*sin Arg z > 0 by A6,A7,HAHNBAN1:15; then cos Arg z > 0 & sin Arg z > 0 by A9,SQUARE_1:23; then A11: cos.Arg z > 0 & sin.Arg z > 0 by SIN_COS:def 21,def 23; then not Arg z in [.PI,2*PI.] & not Arg z in [.PI/2,3/2*PI.] by Th26,Th30; then A12: PI/2 > Arg z or PI > Arg z & 3/2*PI < Arg z by A10,TOPREAL5:1; Arg z > 0 by A10,A11,REAL_1:def 5,SIN_COS:33; hence thesis by A12,Th21,AXIOMS:22,JORDAN6:45; end; theorem Th60: for z be Element of F_Complex holds Arg z in ].PI/2,PI.[ iff Re z < 0 & Im z > 0 proof let z be Element of F_Complex; thus Arg z in ].PI/2,PI.[ implies Re z < 0 & Im z > 0 proof assume A1: Arg z in ].PI/2,PI.[; then A2: Arg z > PI/2 & Arg z < PI by JORDAN6:45; then A3: z <> 0.F_Complex by Def1,Th21; then z = [**|.z.|*cos Arg z,|.z.|*sin Arg z**] by Def1; then A4: Re z = |.z.|*cos Arg z & Im z = |.z.|*sin Arg z by HAHNBAN1:15; A5: |.z.| > 0 by A3,COMPLFLD:96; PI/2 < Arg z & Arg z < PI by A1,JORDAN6:45; then PI/2 < Arg z & Arg z < 3/2*PI by Th21,AXIOMS:22; then Arg z in ].PI/2,3/2*PI.[ by JORDAN6:45; then cos.Arg z < 0 by Th29; then cos Arg z < 0 by SIN_COS:def 23; hence Re z < 0 by A4,A5,SQUARE_1:24; Arg z > 0 by A2,Th21,AXIOMS:22; then Arg z in ].0,PI.[ by A2,JORDAN6:45; then sin.Arg z > 0 by Th23; then sin Arg z > 0 by SIN_COS:def 21; hence Im z > 0 by A4,A5,SQUARE_1:21; end; assume that A6: Re z < 0 and A7: Im z > 0; z = [**Re z,Im z**] by Th9; then A8: z <> 0.F_Complex by A6,Th8,Th10; then A9: |.z.| > 0 by COMPLFLD:96; A10: 0 <= Arg z & Arg z < 2*PI by Th52; z = [**|.z.|*cos Arg z,|.z.|*sin Arg z**] by A8,Def1; then |.z.|*cos Arg z < 0 & |.z.|*sin Arg z > 0 by A6,A7,HAHNBAN1:15; then cos Arg z < 0 & sin Arg z > 0 by A9,SQUARE_1:19,23; then cos.Arg z < 0 & sin.Arg z > 0 by SIN_COS:def 21,def 23; then not Arg z in [.PI,2*PI.] & not Arg z in [.-PI/2,PI/2.] by Th26,Th28; then Arg z < PI & (Arg z < -PI/2 or Arg z > PI/2) by A10,TOPREAL5:1; hence thesis by A10,Th21,AXIOMS:22,JORDAN6:45; end; theorem Th61: for z be Element of F_Complex holds Arg z in ].PI,3/2*PI.[ iff Re z < 0 & Im z < 0 proof let z be Element of F_Complex; thus Arg z in ].PI,3/2*PI.[ implies Re z < 0 & Im z < 0 proof assume A1: Arg z in ].PI,3/2*PI.[; then A2: Arg z > PI & Arg z < 3/2*PI by JORDAN6:45; then A3: z <> 0.F_Complex by Def1,Th21; then z = [**|.z.|*cos Arg z,|.z.|*sin Arg z**] by Def1; then A4: Re z = |.z.|*cos Arg z & Im z = |.z.|*sin Arg z by HAHNBAN1:15; A5: |.z.| > 0 by A3,COMPLFLD:96; PI < Arg z & Arg z < 3/2*PI by A1,JORDAN6:45; then PI/2 < Arg z & Arg z < 3/2*PI by Th21,AXIOMS:22; then Arg z in ].PI/2,3/2*PI.[ by JORDAN6:45; then cos.Arg z < 0 by Th29; then cos Arg z < 0 by SIN_COS:def 23; hence Re z < 0 by A4,A5,SQUARE_1:24; Arg z < 2*PI by A2,Th21,AXIOMS:22; then Arg z in ].PI,2*PI.[ by A2,JORDAN6:45; then sin.Arg z < 0 by Th25; then sin Arg z < 0 by SIN_COS:def 21; hence Im z < 0 by A4,A5,SQUARE_1:24; end; assume that A6: Re z < 0 and A7: Im z < 0; z = [**Re z,Im z**] by Th9; then A8: z <> 0.F_Complex by A6,Th8,Th10; then A9: |.z.| > 0 by COMPLFLD:96; A10: 0 <= Arg z & Arg z < 2*PI by Th52; z = [**|.z.|*cos Arg z,|.z.|*sin Arg z**] by A8,Def1; then |.z.|*cos Arg z < 0 & |.z.|*sin Arg z < 0 by A6,A7,HAHNBAN1:15; then cos Arg z < 0 & sin Arg z < 0 by A9,SQUARE_1:19; then cos.Arg z < 0 & sin.Arg z < 0 by SIN_COS:def 21,def 23; then not Arg z in [.0,PI.] & not Arg z in [.-PI/2,PI/2.] & not Arg z in [.3/2*PI,2*PI.] by Th24,Th28,Th32; then Arg z > PI & (Arg z < -PI/2 or Arg z > PI/2) & Arg z < 3/2*PI by A10, TOPREAL5:1; hence thesis by JORDAN6:45; end; theorem Th62: for z be Element of F_Complex holds Arg z in ].3/2*PI,2*PI.[ iff Re z > 0 & Im z < 0 proof let z be Element of F_Complex; thus Arg z in ].3/2*PI,2*PI.[ implies Re z > 0 & Im z < 0 proof assume A1: Arg z in ].3/2*PI,2*PI.[; then A2: Arg z > 3/2*PI & Arg z < 2*PI by JORDAN6:45; then A3: z <> 0.F_Complex by Def1,Th21; then z = [**|.z.|*cos Arg z,|.z.|*sin Arg z**] by Def1; then A4: Re z = |.z.|*cos Arg z & Im z = |.z.|*sin Arg z by HAHNBAN1:15; A5: |.z.| > 0 by A3,COMPLFLD:96; cos.Arg z > 0 by A1,Th31; then cos Arg z > 0 by SIN_COS:def 23; hence Re z > 0 by A4,A5,SQUARE_1:21; Arg z > PI by A2,Th21,AXIOMS:22; then Arg z in ].PI,2*PI.[ by A2,JORDAN6:45; then sin.Arg z < 0 by Th25; then sin Arg z < 0 by SIN_COS:def 21; hence Im z < 0 by A4,A5,SQUARE_1:24; end; assume that A6: Re z > 0 and A7: Im z < 0; z = [**Re z,Im z**] by Th9; then A8: z <> 0.F_Complex by A6,Th8,Th10; then A9: |.z.| > 0 by COMPLFLD:96; A10: 0 <= Arg z & Arg z < 2*PI by Th52; z = [**|.z.|*cos Arg z,|.z.|*sin Arg z**] by A8,Def1; then |.z.|*cos Arg z > 0 & |.z.|*sin Arg z < 0 by A6,A7,HAHNBAN1:15; then cos Arg z > 0 & sin Arg z < 0 by A9,SQUARE_1:19,23; then cos.Arg z > 0 & sin.Arg z < 0 by SIN_COS:def 21,def 23; then not Arg z in [.0,PI.] & not Arg z in [.PI/2,3/2*PI.] by Th24,Th30; then Arg z > PI & (Arg z < PI/2 or Arg z > 3/2*PI) by A10,TOPREAL5:1; hence thesis by A10,Th21,AXIOMS:22,JORDAN6:45; end; theorem Th63: for z be Element of F_Complex st Im z > 0 holds sin Arg z > 0 proof let z be Element of F_Complex; assume A1: Im z > 0; Re z < 0 or Re z = 0 or Re z > 0; then Re z < 0 or Re z > 0 or z = [**0,Im z**] by Th9; then Arg z in ].PI/2,PI.[ or Arg z in ].0,PI/2.[ or Arg z = PI/2 by A1,Th55,Th59,Th60; then PI/2 < Arg z & Arg z < PI or 0 < Arg z & Arg z < PI/2 or Arg z = PI/2 by JORDAN6:45; then 0 < Arg z & Arg z < PI by Th21,AXIOMS:22; then Arg z in ].0,PI.[ by JORDAN6:45; then sin.Arg z > 0 by Th23; hence thesis by SIN_COS:def 21; end; theorem Th64: for z be Element of F_Complex st Im z < 0 holds sin Arg z < 0 proof let z be Element of F_Complex; assume A1: Im z < 0; Re z < 0 or Re z = 0 or Re z > 0; then Re z < 0 or Re z > 0 or z = [**0,Im z**] by Th9; then Arg z in ].PI,3/2*PI.[ or Arg z in ].3/2*PI,2*PI.[ or Arg z = 3/2*PI by A1,Th56,Th61,Th62; then PI < Arg z & Arg z < 3/2*PI or 3/2*PI < Arg z & Arg z < 2*PI or Arg z = 3/2*PI by JORDAN6:45; then PI < Arg z & Arg z < 2*PI by Th21,AXIOMS:22; then Arg z in ].PI,2*PI.[ by JORDAN6:45; then sin.Arg z < 0 by Th25; hence thesis by SIN_COS:def 21; end; theorem for z be Element of F_Complex st Im z >= 0 holds sin Arg z >= 0 proof let z be Element of F_Complex; assume Im z >= 0; then Im z > 0 or Im z = 0; then sin Arg z > 0 or z = [**Re z,0**] & (Re z >= 0 or Re z < 0) by Th9,Th63; hence thesis by Th53,Th54,SIN_COS:34,82; end; theorem for z be Element of F_Complex st Im z <= 0 holds sin Arg z <= 0 proof let z be Element of F_Complex; assume Im z <= 0; then Im z < 0 or Im z = 0; then sin Arg z < 0 or z = [**Re z,0**] & (Re z >= 0 or Re z < 0) by Th9,Th64; hence thesis by Th53,Th54,SIN_COS:34,82; end; theorem Th67: for z be Element of F_Complex st Re z > 0 holds cos Arg z > 0 proof let z be Element of F_Complex; assume A1: Re z > 0; Im z < 0 or Im z = 0 or Im z > 0; then Im z < 0 or Im z > 0 or z = [**Re z,0**] by Th9; then Arg z in ].0,PI/2.[ or Arg z in ].3/2*PI,2*PI.[ or Arg z = 0 by A1,Th53,Th59,Th62; then cos.Arg z > 0 by Th31,SIN_COS:33,85; hence thesis by SIN_COS:def 23; end; theorem Th68: for z be Element of F_Complex st Re z < 0 holds cos Arg z < 0 proof let z be Element of F_Complex; assume A1: Re z < 0; Im z < 0 or Im z = 0 or Im z > 0; then Im z < 0 or Im z > 0 or z = [**Re z,0**] by Th9; then Arg z in ].PI/2,PI.[ or Arg z in ].PI,3/2*PI.[ or Arg z = PI by A1,Th54,Th60,Th61; then PI/2 < Arg z & Arg z < PI or PI < Arg z & Arg z < 3/2*PI or Arg z = PI by JORDAN6:45; then PI/2 < Arg z & Arg z < 3/2*PI by Th21,AXIOMS:22; then Arg z in ].PI/2,3/2*PI.[ by JORDAN6:45; then cos.Arg z < 0 by Th29; hence thesis by SIN_COS:def 23; end; theorem for z be Element of F_Complex st Re z >= 0 holds cos Arg z >= 0 proof let z be Element of F_Complex; assume Re z >= 0; then Re z > 0 or Re z = 0; then cos Arg z > 0 or z = [**0,Im z**] & (Im z > 0 or Im z < 0 or Im z = 0 ) by Th9,Th67; then cos Arg z > 0 or Arg z = PI/2 or Arg z = 3/2*PI or Arg z = 0 by Def1,Th10,Th55,Th56; hence thesis by Th20,SIN_COS:34,82; end; theorem for z be Element of F_Complex st Re z <= 0 & z <> 0.F_Complex holds cos Arg z <= 0 proof let z be Element of F_Complex; assume that A1: Re z <= 0 and A2: z <> 0.F_Complex; Re z < 0 or Re z = 0 by A1; then cos Arg z < 0 or z = [**0,Im z**] & (Im z >= 0 or Im z < 0) by Th9,Th68; then cos Arg z < 0 or z = [**0,Im z**] & (Im z > 0 or Im z < 0) by A2,Th10,REAL_1:def 5; hence thesis by Th20,Th55,Th56,SIN_COS:82; end; theorem Th71: for n be Nat holds (power F_Complex).([**cos x,sin x**],n) = [**cos (n*x),sin (n*x)**] proof defpred P[Nat] means (power F_Complex).([**cos x,sin x**],$1) = [**cos ($1*x),sin ($1*x)**]; (power F_Complex).([**cos x,sin x**],0) = 1.F_Complex by GROUP_1:def 7 .= [*1,0*] by L1,COMPLFLD:10,POLYNOM2:3 .= [**cos (0*x),sin (0*x)**] by HAHNBAN1:def 1,SIN_COS:34; then A1: P[0]; A2: now let n be Nat; assume P[n]; then (power F_Complex).([**cos x,sin x**],n+1) = [**cos(n*x),sin(n*x)**]*[**cos x,sin x**] by GROUP_1:def 7 .= [**cos(n*x)*cos x - sin(n*x)*sin x,cos(n*x)*sin x+cos x*sin(n*x)**] by HAHNBAN1:11 .= [**cos(n*x+x),cos(n*x)*sin x+cos x*sin(n*x)**] by SIN_COS:80 .= [**cos(n*x+1*x),sin(n*x+1*x)**] by SIN_COS:80 .= [**cos((n+1)*x),sin(n*x+1*x)**] by XCMPLX_1:8 .= [**cos((n+1)*x),sin((n+1)*x)**] by XCMPLX_1:8; hence P[n+1]; end; thus for n be Nat holds P[n] from Ind(A1,A2); end; theorem for z be Element of F_Complex for n be Nat st z <> 0.F_Complex or n <> 0 holds (power F_Complex).(z,n) = [**(|.z.| to_power n)*cos (n*Arg z),(|.z.| to_power n)*sin (n*Arg z)**] proof let z be Element of F_Complex; let n be Nat; assume A1: z <> 0.F_Complex or n <> 0; per cases by A1,NAT_1:18; suppose A2: z <> 0.F_Complex; then A3: |.z.| > 0 by COMPLFLD:96; thus (power F_Complex).(z,n) = (power F_Complex).([**|.z.|*cos Arg z-0*sin Arg z, |.z.|*sin Arg z+cos Arg z*0**],n) by A2,Def1 .= (power F_Complex).([**|.z.|,0**]*[**cos Arg z,sin Arg z**],n) by HAHNBAN1:11 .= (power F_Complex).([**|.z.|,0**],n)* (power F_Complex).([**cos Arg z,sin Arg z**],n) by Th15 .= (power F_Complex).([**|.z.|,0**],n)* [**cos (n*Arg z),sin (n*Arg z)**] by Th71 .= [**|.z.| to_power n,0**]*[**cos (n*Arg z),sin (n*Arg z)**] by A3,Th16 .= [**(|.z.| to_power n)*cos(n*Arg z)-0*sin (n*Arg z), (|.z.| to_power n)*sin(n*Arg z)+0*cos(n*Arg z)**] by HAHNBAN1:11 .= [**(|.z.| to_power n)*cos(n*Arg z), (|.z.| to_power n)*sin(n*Arg z)**]; suppose A4: z = 0.F_Complex & n > 0; hence (power F_Complex).(z,n) = [**0*cos(n*Arg z),0*sin(n*Arg z)**] by Th10,Th14 .= [**0*cos(n*Arg z),(|.z.| to_power n)*sin(n*Arg z)**] by A4,Lm1,COMPLFLD:93,POWER:def 2 .= [**(|.z.| to_power n)*cos(n*Arg z),(|.z.| to_power n)*sin(n*Arg z)**] by A4,Lm1,COMPLFLD:93,POWER:def 2; end; theorem Th73: for n,k be Nat st n <> 0 holds (power F_Complex).([**cos((x+2*PI*k)/n),sin((x+2*PI*k)/n)**],n) = [**cos x,sin x**] proof let n,k be Nat; assume A1: n <> 0; thus (power F_Complex).([**cos((x+2*PI*k)/n),sin((x+2*PI*k)/n)**],n) = [**cos(n*((x+2*PI*k)/n)),sin(n*((x+2*PI*k)/n))**] by Th71 .= [**cos(x+2*PI*k),sin(n*((x+2*PI*k)/n))**] by A1,XCMPLX_1:88 .= [**cos(x+2*PI*k),sin(x+2*PI*k)**] by A1,XCMPLX_1:88 .= [**cos.(x+2*PI*k),sin(x+2*PI*k)**] by SIN_COS:def 23 .= [**cos.(x+2*PI*k),sin.(x+2*PI*k)**] by SIN_COS:def 21 .= [**cos.(x+2*PI*k),sin.x**] by SIN_COS2:10 .= [**cos.x,sin.x**] by SIN_COS2:11 .= [**cos.x,sin x**] by SIN_COS:def 21 .= [**cos x,sin x**] by SIN_COS:def 23; end; theorem Th74: for z be Element of F_Complex for n,k be Nat st n <> 0 holds z = (power F_Complex).([**(n-root |.z.|)*cos((Arg z+2*PI*k)/n), (n-root |.z.|)*sin((Arg z+2*PI*k)/n)**],n) proof let z be Element of F_Complex; let n,k be Nat; assume A1: n <> 0; then A2: n > 0 by NAT_1:19; then A3: n >= 0+1 by NAT_1:38; per cases; suppose A4: z <> 0.F_Complex; then A5: |.z.| > 0 by COMPLFLD:96; then n-root |.z.| = n -Root |.z.| by A3,POWER:def 1; then A6: n-root |.z.| > 0 by A3,A5,PREPOWER:def 3; thus (power F_Complex).([**(n-root |.z.|)*cos((Arg z+2*PI*k)/n), (n-root |.z.|)*sin((Arg z+2*PI*k)/n)**],n) = (power F_Complex).([**(n-root |.z.|)*cos((Arg z+2*PI*k)/n)- 0*sin((Arg z+2*PI*k)/n),(n-root |.z.|)*sin((Arg z+2*PI*k)/n)+ 0*cos((Arg z+2*PI*k)/n)**],n) .= (power F_Complex).([**n-root |.z.|,0**]* [**cos((Arg z+2*PI*k)/n),sin((Arg z+2*PI*k)/n)**],n) by HAHNBAN1:11 .= (power F_Complex).([**n-root |.z.|,0**],n)*(power F_Complex). ([**cos((Arg z+2*PI*k)/n),sin((Arg z+2*PI*k)/n)**],n) by Th15 .= (power F_Complex).([**n-root |.z.|,0**],n)*[**cos Arg z,sin Arg z**] by A1,Th73 .= [**(n-root |.z.|) to_power n,0**]*[**cos Arg z,sin Arg z**] by A6,Th16 .= [**|.z.|,0**]*[**cos Arg z,sin Arg z**] by A1,A5,Th17 .= [**|.z.|*cos Arg z-0*sin Arg z,|.z.|*sin Arg z+0*cos Arg z**] by HAHNBAN1:11 .= z by A4,Def1; suppose A7: z = 0.F_Complex; then |.z.| = 0 by COMPLFLD:9,93,def 1; hence (power F_Complex).([**(n-root |.z.|)*cos((Arg z+2*PI*k)/n), (n-root |.z.|)*sin((Arg z+2*PI*k)/n)**],n) = (power F_Complex).([**0*cos((Arg z+2*PI*k)/n), (n-root 0)*sin((Arg z+2*PI*k)/n)**],n) by A3,POWER:6 .= (power F_Complex).([**0,0*sin((Arg z+2*PI*k)/n)**],n) by A3,POWER:6 .= z by A2,A7,Th10,Th14; end; definition let x be Element of F_Complex; let n be non empty Nat; mode CRoot of n,x -> Element of F_Complex means :Def2: (power F_Complex).(it,n) = x; existence proof take [**(n-root |.x.|)*cos((Arg x+2*PI*0)/n), (n-root |.x.|)*sin((Arg x+2*PI*0)/n)**]; thus thesis by Th74; end; end; theorem for x be Element of F_Complex for n be non empty Nat for k be Nat holds [**(n-root |.x.|)*cos((Arg x+2*PI*k)/n), (n-root |.x.|)*sin((Arg x+2*PI*k)/n)**] is CRoot of n,x proof let x be Element of F_Complex; let n be non empty Nat; let k be Nat; (power F_Complex).([**(n-root |.x.|)*cos((Arg x+2*PI*k)/n), (n-root |.x.|)*sin((Arg x+2*PI*k)/n)**],n) = x by Th74; hence thesis by Def2; end; theorem for x be Element of F_Complex for v be CRoot of 1,x holds v = x proof let x be Element of F_Complex; let v be CRoot of 1,x; (power F_Complex).(v,1) = x by Def2; hence v = x by Th12; end; theorem for n be non empty Nat for v be CRoot of n,0.F_Complex holds v = 0.F_Complex proof let n be non empty Nat; let v be CRoot of n,0.F_Complex; defpred P[Nat] means (power F_Complex).(v,$1) = 0.F_Complex; A1: ex n be non empty Nat st P[n] proof take n; thus thesis by Def2; end; A2: now let k be non empty Nat; assume that A3: k <> 1 and A4: P[k]; consider t be Nat such that A5: k = t+1 by NAT_1:22; k >= 1 by RLVECT_1:99; then t+1 > 0+1 by A3,A5,REAL_1:def 5; then A6: t > 0 by AXIOMS:24; reconsider t as non empty Nat by A3,A5,CARD_1:51; take t; thus t < k by A5,NAT_1:38; (power F_Complex).(v,k) = (power F_Complex).(v,t)*v by A5,GROUP_1:def 7; then (power F_Complex).(v,t) = 0.F_Complex or v = 0.F_Complex by A4,VECTSP_1:44; hence P[t] by A6,Th14; end; P[1] from Regr_without_0(A1,A2); hence thesis by Th12; end; theorem for n be non empty Nat for x be Element of F_Complex for v be CRoot of n,x st v = 0.F_Complex holds x = 0.F_Complex proof let n be non empty Nat; let x be Element of F_Complex; let v be CRoot of n,x; A1: n >= 0 & n <> 0 by NAT_1:18; assume v = 0.F_Complex; then (power F_Complex).(0.F_Complex,n) = x by Def2; hence thesis by A1,Th14; end;