:: XCMPLX_1 semantic presentation begin theorem :: XCMPLX_1:1 for a, b, c being complex number holds a + (b + c) = (a + b) + c ; theorem :: XCMPLX_1:2 for a, c, b being complex number st a + c = b + c holds a = b ; theorem :: XCMPLX_1:3 for a, b being complex number st a = a + b holds b = 0 ; theorem Th4: :: XCMPLX_1:4 for a, b, c being complex number holds a * (b * c) = (a * b) * c ; theorem :: XCMPLX_1:5 for c, a, b being complex number st c <> 0 & a * c = b * c holds a = b proof let c, a, b be complex number ; ::_thesis: ( c <> 0 & a * c = b * c implies a = b ) assume A1: c <> 0 ; ::_thesis: ( not a * c = b * c or a = b ) assume a * c = b * c ; ::_thesis: a = b then a * (c * (c ")) = (b * c) * (c ") by Th4; then a * 1 = (b * c) * (c ") by A1, XCMPLX_0:def_7; then a = b * (c * (c ")) ; then a = b * 1 by A1, XCMPLX_0:def_7; hence a = b ; ::_thesis: verum end; theorem :: XCMPLX_1:6 for a, b being complex number holds ( not a * b = 0 or a = 0 or b = 0 ) ; theorem Th7: :: XCMPLX_1:7 for b, a being complex number st b <> 0 & a * b = b holds a = 1 proof let b, a be complex number ; ::_thesis: ( b <> 0 & a * b = b implies a = 1 ) assume that A1: b <> 0 and A2: a * b = b ; ::_thesis: a = 1 (a * b) * (b ") = 1 by A1, A2, XCMPLX_0:def_7; then a * 1 = 1 by A2, Th4; hence a = 1 ; ::_thesis: verum end; theorem :: XCMPLX_1:8 for a, b, c being complex number holds a * (b + c) = (a * b) + (a * c) ; theorem :: XCMPLX_1:9 for a, b, c, d being complex number holds ((a + b) + c) * d = ((a * d) + (b * d)) + (c * d) ; theorem :: XCMPLX_1:10 for a, b, c, d being complex number holds (a + b) * (c + d) = (((a * c) + (a * d)) + (b * c)) + (b * d) ; theorem :: XCMPLX_1:11 for a being complex number holds 2 * a = a + a ; theorem :: XCMPLX_1:12 for a being complex number holds 3 * a = (a + a) + a ; theorem :: XCMPLX_1:13 for a being complex number holds 4 * a = ((a + a) + a) + a ; theorem :: XCMPLX_1:14 for a being complex number holds a - a = 0 ; theorem :: XCMPLX_1:15 for a, b being complex number st a - b = 0 holds a = b ; theorem :: XCMPLX_1:16 for b, a being complex number st b - a = b holds a = 0 ; theorem :: XCMPLX_1:17 for a, b being complex number holds a = a - (b - b) ; theorem :: XCMPLX_1:18 for a, b being complex number holds a - (a - b) = b ; theorem :: XCMPLX_1:19 for a, c, b being complex number st a - c = b - c holds a = b ; theorem :: XCMPLX_1:20 for c, a, b being complex number st c - a = c - b holds a = b ; theorem :: XCMPLX_1:21 for a, b, c being complex number holds (a - b) - c = (a - c) - b ; theorem :: XCMPLX_1:22 for a, c, b being complex number holds a - c = (a - b) - (c - b) ; theorem :: XCMPLX_1:23 for c, a, b being complex number holds (c - a) - (c - b) = b - a ; theorem :: XCMPLX_1:24 for a, b, c, d being complex number st a - b = c - d holds a - c = b - d ; Lm1: for a, b being complex number holds (a ") * (b ") = (a * b) " proof let a, b be complex number ; ::_thesis: (a ") * (b ") = (a * b) " percases ( a = 0 or b = 0 or ( a <> 0 & b <> 0 ) ) ; supposeA1: ( a = 0 or b = 0 ) ; ::_thesis: (a ") * (b ") = (a * b) " then ( a " = 0 or b " = 0 ) ; hence (a ") * (b ") = (a * b) " by A1; ::_thesis: verum end; supposethat A2: a <> 0 and A3: b <> 0 ; ::_thesis: (a ") * (b ") = (a * b) " thus (a ") * (b ") = ((a ") * (b ")) * 1 .= ((a ") * (b ")) * ((a * b) * ((a * b) ")) by A2, A3, XCMPLX_0:def_7 .= (((a ") * a) * ((b ") * b)) * ((a * b) ") .= (1 * ((b ") * b)) * ((a * b) ") by A2, XCMPLX_0:def_7 .= 1 * ((a * b) ") by A3, XCMPLX_0:def_7 .= (a * b) " ; ::_thesis: verum end; end; end; Lm2: for a, b, c being complex number holds a / (b / c) = (a * c) / b proof let a, b, c be complex number ; ::_thesis: a / (b / c) = (a * c) / b thus a / (b / c) = a / (b * (c ")) by XCMPLX_0:def_9 .= a * ((b * (c ")) ") by XCMPLX_0:def_9 .= a * ((b ") * ((c ") ")) by Lm1 .= (a * c) * (b ") .= (a * c) / b by XCMPLX_0:def_9 ; ::_thesis: verum end; Lm3: for b, a being complex number st b <> 0 holds (a / b) * b = a proof let b, a be complex number ; ::_thesis: ( b <> 0 implies (a / b) * b = a ) assume A1: b <> 0 ; ::_thesis: (a / b) * b = a thus (a / b) * b = (a * (b ")) * b by XCMPLX_0:def_9 .= a * ((b ") * b) .= a * 1 by A1, XCMPLX_0:def_7 .= a ; ::_thesis: verum end; Lm4: for a being complex number holds 1 / a = a " proof let a be complex number ; ::_thesis: 1 / a = a " thus 1 / a = 1 * (a ") by XCMPLX_0:def_9 .= a " ; ::_thesis: verum end; Lm5: for a being complex number st a <> 0 holds a / a = 1 proof let a be complex number ; ::_thesis: ( a <> 0 implies a / a = 1 ) assume A1: a <> 0 ; ::_thesis: a / a = 1 thus a / a = a * (a ") by XCMPLX_0:def_9 .= 1 by A1, XCMPLX_0:def_7 ; ::_thesis: verum end; theorem :: XCMPLX_1:25 for a, b being complex number holds a = a + (b - b) ; theorem :: XCMPLX_1:26 for a, b being complex number holds a = (a + b) - b ; theorem :: XCMPLX_1:27 for a, b being complex number holds a = (a - b) + b ; theorem :: XCMPLX_1:28 for a, c, b being complex number holds a + c = (a + b) + (c - b) ; theorem :: XCMPLX_1:29 for a, b, c being complex number holds (a + b) - c = (a - c) + b ; theorem :: XCMPLX_1:30 for a, b, c being complex number holds (a - b) + c = (c - b) + a ; theorem :: XCMPLX_1:31 for a, c, b being complex number holds a + c = (a + b) - (b - c) ; theorem :: XCMPLX_1:32 for a, c, b being complex number holds a - c = (a + b) - (c + b) ; theorem :: XCMPLX_1:33 for a, b, c, d being complex number st a + b = c + d holds a - c = d - b ; theorem :: XCMPLX_1:34 for a, c, d, b being complex number st a - c = d - b holds a + b = c + d ; theorem :: XCMPLX_1:35 for a, b, c, d being complex number st a + b = c - d holds a + d = c - b ; theorem :: XCMPLX_1:36 for a, b, c being complex number holds a - (b + c) = (a - b) - c ; theorem :: XCMPLX_1:37 for a, b, c being complex number holds a - (b - c) = (a - b) + c ; theorem :: XCMPLX_1:38 for a, b, c being complex number holds a - (b - c) = a + (c - b) ; theorem :: XCMPLX_1:39 for a, c, b being complex number holds a - c = (a - b) + (b - c) ; theorem :: XCMPLX_1:40 for a, b, c being complex number holds a * (b - c) = (a * b) - (a * c) ; theorem :: XCMPLX_1:41 for a, b, c, d being complex number holds (a - b) * (c - d) = (b - a) * (d - c) ; theorem :: XCMPLX_1:42 for a, b, c, d being complex number holds ((a - b) - c) * d = ((a * d) - (b * d)) - (c * d) ; theorem :: XCMPLX_1:43 for a, b, c, d being complex number holds ((a + b) - c) * d = ((a * d) + (b * d)) - (c * d) ; theorem :: XCMPLX_1:44 for a, b, c, d being complex number holds ((a - b) + c) * d = ((a * d) - (b * d)) + (c * d) ; theorem :: XCMPLX_1:45 for a, b, c, d being complex number holds (a + b) * (c - d) = (((a * c) - (a * d)) + (b * c)) - (b * d) ; theorem :: XCMPLX_1:46 for a, b, c, d being complex number holds (a - b) * (c + d) = (((a * c) + (a * d)) - (b * c)) - (b * d) ; theorem :: XCMPLX_1:47 for a, b, e, d being complex number holds (a - b) * (e - d) = (((a * e) - (a * d)) - (b * e)) + (b * d) ; theorem :: XCMPLX_1:48 for a, b, c being complex number holds (a / b) / c = (a / c) / b proof let a, b, c be complex number ; ::_thesis: (a / b) / c = (a / c) / b thus (a / b) / c = (a * (b ")) / c by XCMPLX_0:def_9 .= (a * (b ")) * (c ") by XCMPLX_0:def_9 .= (a * (c ")) * (b ") .= (a / c) * (b ") by XCMPLX_0:def_9 .= (a / c) / b by XCMPLX_0:def_9 ; ::_thesis: verum end; theorem Th49: :: XCMPLX_1:49 for a being complex number holds a / 0 = 0 proof let a be complex number ; ::_thesis: a / 0 = 0 thus a / 0 = a * (0 ") by XCMPLX_0:def_9 .= 0 ; ::_thesis: verum end; theorem :: XCMPLX_1:50 for a, b being complex number st a <> 0 & b <> 0 holds a / b <> 0 ; theorem :: XCMPLX_1:51 for b, a being complex number st b <> 0 holds a = a / (b / b) proof let b, a be complex number ; ::_thesis: ( b <> 0 implies a = a / (b / b) ) A1: a = a / 1 ; assume b <> 0 ; ::_thesis: a = a / (b / b) hence a = a / (b / b) by A1, Lm5; ::_thesis: verum end; Lm6: for a, b, c, d being complex number holds (a / b) * (c / d) = (a * c) / (b * d) proof let a, b, c, d be complex number ; ::_thesis: (a / b) * (c / d) = (a * c) / (b * d) thus (a / b) * (c / d) = (a * (b ")) * (c / d) by XCMPLX_0:def_9 .= (a * (b ")) * (c * (d ")) by XCMPLX_0:def_9 .= (a * c) * ((b ") * (d ")) .= (a * c) * ((b * d) ") by Lm1 .= (a * c) / (b * d) by XCMPLX_0:def_9 ; ::_thesis: verum end; Lm7: for a, b being complex number holds (a / b) " = b / a proof let a, b be complex number ; ::_thesis: (a / b) " = b / a percases ( a = 0 or b = 0 or ( a <> 0 & b <> 0 ) ) ; supposeA1: a = 0 ; ::_thesis: (a / b) " = b / a hence (a / b) " = b * (0 ") .= b / a by A1, XCMPLX_0:def_9 ; ::_thesis: verum end; supposeA2: b = 0 ; ::_thesis: (a / b) " = b / a hence (a / b) " = (a * (0 ")) " by XCMPLX_0:def_9 .= b / a by A2 ; ::_thesis: verum end; supposeA3: ( a <> 0 & b <> 0 ) ; ::_thesis: (a / b) " = b / a (a / b) * (b / a) = (a * b) / (a * b) by Lm6; then (a / b) * (b / a) = 1 by A3, Lm5; hence (a / b) " = b / a by A3, XCMPLX_0:def_7; ::_thesis: verum end; end; end; Lm8: for a, b, c being complex number holds a * (b / c) = (a * b) / c proof let a, b, c be complex number ; ::_thesis: a * (b / c) = (a * b) / c thus a * (b / c) = (a / 1) * (b / c) .= (a * b) / (1 * c) by Lm6 .= (a * b) / c ; ::_thesis: verum end; theorem :: XCMPLX_1:52 for a, b being complex number st a <> 0 holds a / (a / b) = b proof let a, b be complex number ; ::_thesis: ( a <> 0 implies a / (a / b) = b ) assume A1: a <> 0 ; ::_thesis: a / (a / b) = b thus a / (a / b) = a * ((a / b) ") by XCMPLX_0:def_9 .= a * (b / a) by Lm7 .= (a * b) / a by Lm8 .= (a / a) * b by Lm8 .= 1 * b by A1, Lm5 .= b ; ::_thesis: verum end; theorem :: XCMPLX_1:53 for c, a, b being complex number st c <> 0 & a / c = b / c holds a = b proof let c, a, b be complex number ; ::_thesis: ( c <> 0 & a / c = b / c implies a = b ) assume that A1: c <> 0 and A2: a / c = b / c ; ::_thesis: a = b a = (b / c) * c by A1, A2, Lm3; hence a = b by A1, Lm3; ::_thesis: verum end; Lm9: for b, a being complex number st b <> 0 holds a = (a * b) / b proof let b, a be complex number ; ::_thesis: ( b <> 0 implies a = (a * b) / b ) A1: a = a * 1 ; assume b <> 0 ; ::_thesis: a = (a * b) / b then a = a * (b / b) by A1, Lm5; then a = a * (b * (b ")) by XCMPLX_0:def_9; then a = (a * b) * (b ") ; hence a = (a * b) / b by XCMPLX_0:def_9; ::_thesis: verum end; theorem :: XCMPLX_1:54 for a, b being complex number st a / b <> 0 holds b = a / (a / b) proof let a, b be complex number ; ::_thesis: ( a / b <> 0 implies b = a / (a / b) ) assume A1: a / b <> 0 ; ::_thesis: b = a / (a / b) then b <> 0 by Th49; then (a / b) * b = a by Lm3; hence b = a / (a / b) by A1, Lm9; ::_thesis: verum end; Lm10: for c, a, b being complex number st c <> 0 holds a / b = (a * c) / (b * c) proof let c, a, b be complex number ; ::_thesis: ( c <> 0 implies a / b = (a * c) / (b * c) ) assume A1: c <> 0 ; ::_thesis: a / b = (a * c) / (b * c) thus a / b = (a * (b ")) * 1 by XCMPLX_0:def_9 .= (a * (b ")) * (c * (c ")) by A1, XCMPLX_0:def_7 .= (a * c) * ((b ") * (c ")) .= (a * c) * ((b * c) ") by Lm1 .= (a * c) / (b * c) by XCMPLX_0:def_9 ; ::_thesis: verum end; theorem :: XCMPLX_1:55 for c, a, b being complex number st c <> 0 holds a / b = (a / c) / (b / c) proof let c, a, b be complex number ; ::_thesis: ( c <> 0 implies a / b = (a / c) / (b / c) ) assume c <> 0 ; ::_thesis: a / b = (a / c) / (b / c) hence a / b = (a * (c ")) / (b * (c ")) by Lm10 .= (a / c) / (b * (c ")) by XCMPLX_0:def_9 .= (a / c) / (b / c) by XCMPLX_0:def_9 ; ::_thesis: verum end; theorem :: XCMPLX_1:56 for a being complex number holds 1 / (1 / a) = a proof let a be complex number ; ::_thesis: 1 / (1 / a) = a thus 1 / (1 / a) = (1 * a) / 1 by Lm2 .= a ; ::_thesis: verum end; Lm11: for a, b being complex number holds (a * (b ")) " = (a ") * b proof let a, b be complex number ; ::_thesis: (a * (b ")) " = (a ") * b thus (a * (b ")) " = (a ") * ((b ") ") by Lm1 .= (a ") * b ; ::_thesis: verum end; theorem :: XCMPLX_1:57 for a, b being complex number holds 1 / (a / b) = b / a proof let a, b be complex number ; ::_thesis: 1 / (a / b) = b / a thus 1 / (a / b) = 1 / (a * (b ")) by XCMPLX_0:def_9 .= (a * (b ")) " by Lm4 .= b * (a ") by Lm11 .= b / a by XCMPLX_0:def_9 ; ::_thesis: verum end; theorem Th58: :: XCMPLX_1:58 for a, b being complex number st a / b = 1 holds a = b proof let a, b be complex number ; ::_thesis: ( a / b = 1 implies a = b ) assume A1: a / b = 1 ; ::_thesis: a = b then b <> 0 by Th49; then a = 1 * b by A1, Lm3; hence a = b ; ::_thesis: verum end; Lm12: for a, b being complex number st a " = b " holds a = b proof let a, b be complex number ; ::_thesis: ( a " = b " implies a = b ) assume a " = b " ; ::_thesis: a = b then a = (b ") " ; hence a = b ; ::_thesis: verum end; theorem Th59: :: XCMPLX_1:59 for a, b being complex number st 1 / a = 1 / b holds a = b proof let a, b be complex number ; ::_thesis: ( 1 / a = 1 / b implies a = b ) assume 1 / a = 1 / b ; ::_thesis: a = b then a " = 1 / b by Lm4; then a " = b " by Lm4; hence a = b by Lm12; ::_thesis: verum end; theorem :: XCMPLX_1:60 for a being complex number st a <> 0 holds a / a = 1 by Lm5; theorem :: XCMPLX_1:61 for b, a being complex number st b <> 0 & b / a = b holds a = 1 proof let b, a be complex number ; ::_thesis: ( b <> 0 & b / a = b implies a = 1 ) assume that A1: b <> 0 and A2: b / a = b ; ::_thesis: a = 1 a <> 0 by A1, A2, Th49; then b = b * a by A2, Lm3; hence a = 1 by A1, Th7; ::_thesis: verum end; theorem Th62: :: XCMPLX_1:62 for a, c, b being complex number holds (a / c) + (b / c) = (a + b) / c proof let a, c, b be complex number ; ::_thesis: (a / c) + (b / c) = (a + b) / c thus (a / c) + (b / c) = (a * (c ")) + (b / c) by XCMPLX_0:def_9 .= (a * (c ")) + (b * (c ")) by XCMPLX_0:def_9 .= (a + b) * (c ") .= (a + b) / c by XCMPLX_0:def_9 ; ::_thesis: verum end; theorem :: XCMPLX_1:63 for a, b, e, d being complex number holds ((a + b) + e) / d = ((a / d) + (b / d)) + (e / d) proof let a, b, e, d be complex number ; ::_thesis: ((a + b) + e) / d = ((a / d) + (b / d)) + (e / d) thus ((a + b) + e) / d = ((a + b) / d) + (e / d) by Th62 .= ((a / d) + (b / d)) + (e / d) by Th62 ; ::_thesis: verum end; theorem :: XCMPLX_1:64 for a being complex number holds (a + a) / 2 = a ; theorem :: XCMPLX_1:65 for a being complex number holds (a / 2) + (a / 2) = a ; theorem :: XCMPLX_1:66 for a, b being complex number st a = (a + b) / 2 holds a = b ; theorem :: XCMPLX_1:67 for a being complex number holds ((a + a) + a) / 3 = a ; theorem :: XCMPLX_1:68 for a being complex number holds ((a / 3) + (a / 3)) + (a / 3) = a ; theorem :: XCMPLX_1:69 for a being complex number holds (((a + a) + a) + a) / 4 = a ; theorem :: XCMPLX_1:70 for a being complex number holds (((a / 4) + (a / 4)) + (a / 4)) + (a / 4) = a ; theorem :: XCMPLX_1:71 for a being complex number holds (a / 4) + (a / 4) = a / 2 ; theorem :: XCMPLX_1:72 for a being complex number holds (a + a) / 4 = a / 2 ; theorem :: XCMPLX_1:73 for a, b being complex number st a * b = 1 holds a = 1 / b proof let a, b be complex number ; ::_thesis: ( a * b = 1 implies a = 1 / b ) assume A1: a * b = 1 ; ::_thesis: a = 1 / b then b <> 0 ; then a * 1 = 1 * (b ") by A1, XCMPLX_0:def_7; hence a = 1 / b by Lm4; ::_thesis: verum end; theorem :: XCMPLX_1:74 for a, b, c being complex number holds a * (b / c) = (a * b) / c by Lm8; theorem :: XCMPLX_1:75 for a, b, e being complex number holds (a / b) * e = (e / b) * a proof let a, b, e be complex number ; ::_thesis: (a / b) * e = (e / b) * a thus (a / b) * e = (a * e) / b by Lm8 .= (e / b) * a by Lm8 ; ::_thesis: verum end; theorem :: XCMPLX_1:76 for a, b, c, d being complex number holds (a / b) * (c / d) = (a * c) / (b * d) by Lm6; theorem :: XCMPLX_1:77 for a, b, c being complex number holds a / (b / c) = (a * c) / b by Lm2; Lm13: for a, b, c, d being complex number holds (a / b) / (c / d) = (a * d) / (b * c) proof let a, b, c, d be complex number ; ::_thesis: (a / b) / (c / d) = (a * d) / (b * c) thus (a / b) / (c / d) = (a / b) * ((c / d) ") by XCMPLX_0:def_9 .= (a / b) * (d / c) by Lm7 .= (a * d) / (b * c) by Lm6 ; ::_thesis: verum end; theorem Th78: :: XCMPLX_1:78 for a, b, c being complex number holds a / (b * c) = (a / b) / c proof let a, b, c be complex number ; ::_thesis: a / (b * c) = (a / b) / c thus a / (b * c) = (a * 1) / (b * c) .= (a / b) / (c / 1) by Lm13 .= (a / b) / c ; ::_thesis: verum end; theorem :: XCMPLX_1:79 for a, b, c being complex number holds a / (b / c) = a * (c / b) proof let a, b, c be complex number ; ::_thesis: a / (b / c) = a * (c / b) thus a / (b / c) = (a * c) / b by Lm2 .= (a * c) * (b ") by XCMPLX_0:def_9 .= a * (c * (b ")) .= a * (c / b) by XCMPLX_0:def_9 ; ::_thesis: verum end; theorem :: XCMPLX_1:80 for a, b, c being complex number holds a / (b / c) = (c / b) * a proof let a, b, c be complex number ; ::_thesis: a / (b / c) = (c / b) * a a / (b / c) = (a * c) / b by Lm2 .= (a * c) * (b ") by XCMPLX_0:def_9 .= a * (c * (b ")) .= a * (c / b) by XCMPLX_0:def_9 ; hence a / (b / c) = (c / b) * a ; ::_thesis: verum end; theorem Th81: :: XCMPLX_1:81 for a, b, e being complex number holds a / (b / e) = e * (a / b) proof let a, b, e be complex number ; ::_thesis: a / (b / e) = e * (a / b) thus a / (b / e) = (a * e) / b by Lm2 .= (e * a) * (b ") by XCMPLX_0:def_9 .= e * (a * (b ")) .= e * (a / b) by XCMPLX_0:def_9 ; ::_thesis: verum end; theorem :: XCMPLX_1:82 for a, b, c being complex number holds a / (b / c) = (a / b) * c proof let a, b, c be complex number ; ::_thesis: a / (b / c) = (a / b) * c a / (b / c) = (a * c) / b by Lm2 .= (c * a) * (b ") by XCMPLX_0:def_9 .= c * (a * (b ")) .= c * (a / b) by XCMPLX_0:def_9 ; hence a / (b / c) = (a / b) * c ; ::_thesis: verum end; Lm14: for a, b being complex number holds a * (1 / b) = a / b proof let a, b be complex number ; ::_thesis: a * (1 / b) = a / b thus a / b = a * (b ") by XCMPLX_0:def_9 .= a * (1 / b) by Lm4 ; ::_thesis: verum end; Lm15: for c, a, b being complex number holds (1 / c) * (a / b) = a / (b * c) proof let c, a, b be complex number ; ::_thesis: (1 / c) * (a / b) = a / (b * c) (a / b) / c = (c ") * (a / b) by XCMPLX_0:def_9 .= (1 / c) * (a / b) by Lm4 ; hence (1 / c) * (a / b) = a / (b * c) by Th78; ::_thesis: verum end; theorem :: XCMPLX_1:83 for a, b, c, d being complex number holds (a * b) / (c * d) = ((a / c) * b) / d proof let a, b, c, d be complex number ; ::_thesis: (a * b) / (c * d) = ((a / c) * b) / d thus (a * b) / (c * d) = (1 / c) * ((a * b) / d) by Lm15 .= ((1 / c) * (a * b)) / d by Lm8 .= (((1 / c) * a) * b) / d .= ((a / c) * b) / d by Lm14 ; ::_thesis: verum end; theorem :: XCMPLX_1:84 for a, b, c, d being complex number holds (a / b) / (c / d) = (a * d) / (b * c) by Lm13; theorem :: XCMPLX_1:85 for a, c, b, d being complex number holds (a / c) * (b / d) = (a / d) * (b / c) proof let a, c, b, d be complex number ; ::_thesis: (a / c) * (b / d) = (a / d) * (b / c) thus (a / c) * (b / d) = (a * b) / (d * c) by Lm6 .= (a / d) * (b / c) by Lm6 ; ::_thesis: verum end; theorem :: XCMPLX_1:86 for a, b, c, d, e being complex number holds a / ((b * c) * (d / e)) = (e / c) * (a / (b * d)) proof let a, b, c, d, e be complex number ; ::_thesis: a / ((b * c) * (d / e)) = (e / c) * (a / (b * d)) thus a / ((b * c) * (d / e)) = a / ((b * c) * (d * (e "))) by XCMPLX_0:def_9 .= a / (c * ((b * d) * (e "))) .= a / (c * ((b * d) / e)) by XCMPLX_0:def_9 .= a / ((b * d) / (e / c)) by Th81 .= (e / c) * (a / (b * d)) by Th81 ; ::_thesis: verum end; theorem :: XCMPLX_1:87 for b, a being complex number st b <> 0 holds (a / b) * b = a by Lm3; theorem :: XCMPLX_1:88 for b, a being complex number st b <> 0 holds a = a * (b / b) proof let b, a be complex number ; ::_thesis: ( b <> 0 implies a = a * (b / b) ) A1: a = a * 1 ; assume b <> 0 ; ::_thesis: a = a * (b / b) hence a = a * (b / b) by A1, Lm5; ::_thesis: verum end; theorem :: XCMPLX_1:89 for b, a being complex number st b <> 0 holds a = (a * b) / b by Lm9; theorem :: XCMPLX_1:90 for b, a, c being complex number st b <> 0 holds a * c = (a * b) * (c / b) proof let b, a, c be complex number ; ::_thesis: ( b <> 0 implies a * c = (a * b) * (c / b) ) assume A1: b <> 0 ; ::_thesis: a * c = (a * b) * (c / b) thus a * c = (a * 1) * c .= (a * (b * (b "))) * c by A1, XCMPLX_0:def_7 .= (a * b) * ((b ") * c) .= (a * b) * (c / b) by XCMPLX_0:def_9 ; ::_thesis: verum end; theorem :: XCMPLX_1:91 for c, a, b being complex number st c <> 0 holds a / b = (a * c) / (b * c) by Lm10; theorem :: XCMPLX_1:92 for c, a, b being complex number st c <> 0 holds a / b = (a / (b * c)) * c proof let c, a, b be complex number ; ::_thesis: ( c <> 0 implies a / b = (a / (b * c)) * c ) assume A1: c <> 0 ; ::_thesis: a / b = (a / (b * c)) * c c * (a / (b * c)) = c * ((a * 1) / (b * c)) .= c * ((1 / c) * (a / b)) by Lm6 .= ((1 / c) * c) * (a / b) .= 1 * (a / b) by A1, Lm3 .= a / b ; hence a / b = (a / (b * c)) * c ; ::_thesis: verum end; theorem :: XCMPLX_1:93 for b, a, c being complex number st b <> 0 holds a * c = (a * b) / (b / c) proof let b, a, c be complex number ; ::_thesis: ( b <> 0 implies a * c = (a * b) / (b / c) ) assume A1: b <> 0 ; ::_thesis: a * c = (a * b) / (b / c) thus a * c = (a * 1) * c .= (a * (b * (b "))) * c by A1, XCMPLX_0:def_7 .= (a * b) * ((b ") * c) .= (a * b) * ((b * (c ")) ") by Lm11 .= (a * b) / (b * (c ")) by XCMPLX_0:def_9 .= (a * b) / (b / c) by XCMPLX_0:def_9 ; ::_thesis: verum end; theorem Th94: :: XCMPLX_1:94 for c, d, a, b being complex number st c <> 0 & d <> 0 & a * c = b * d holds a / d = b / c proof let c, d, a, b be complex number ; ::_thesis: ( c <> 0 & d <> 0 & a * c = b * d implies a / d = b / c ) assume that A1: c <> 0 and A2: d <> 0 ; ::_thesis: ( not a * c = b * d or a / d = b / c ) assume a * c = b * d ; ::_thesis: a / d = b / c then a = (b * d) / c by A1, Lm9; then a = d * (b / c) by Lm8; hence a / d = b / c by A2, Lm9; ::_thesis: verum end; theorem Th95: :: XCMPLX_1:95 for c, d, a, b being complex number st c <> 0 & d <> 0 & a / d = b / c holds a * c = b * d proof let c, d, a, b be complex number ; ::_thesis: ( c <> 0 & d <> 0 & a / d = b / c implies a * c = b * d ) assume that A1: c <> 0 and A2: d <> 0 and A3: a / d = b / c ; ::_thesis: a * c = b * d c * (a / d) = b by A1, A3, Lm3; then (a * c) / d = b by Lm8; hence a * c = b * d by A2, Lm3; ::_thesis: verum end; theorem :: XCMPLX_1:96 for c, d, a, b being complex number st c <> 0 & d <> 0 & a * c = b / d holds a * d = b / c proof let c, d, a, b be complex number ; ::_thesis: ( c <> 0 & d <> 0 & a * c = b / d implies a * d = b / c ) assume that A1: c <> 0 and A2: d <> 0 ; ::_thesis: ( not a * c = b / d or a * d = b / c ) assume a * c = b / d ; ::_thesis: a * d = b / c then (a * c) * d = b by A2, Lm3; then (a * d) * c = b ; hence a * d = b / c by A1, Lm9; ::_thesis: verum end; theorem :: XCMPLX_1:97 for c, a, b being complex number st c <> 0 holds a / b = c * ((a / c) / b) proof let c, a, b be complex number ; ::_thesis: ( c <> 0 implies a / b = c * ((a / c) / b) ) assume A1: c <> 0 ; ::_thesis: a / b = c * ((a / c) / b) thus a / b = a * (b ") by XCMPLX_0:def_9 .= (c * (a / c)) * (b ") by A1, Lm3 .= c * ((a / c) * (b ")) .= c * ((a / c) / b) by XCMPLX_0:def_9 ; ::_thesis: verum end; theorem :: XCMPLX_1:98 for c, a, b being complex number st c <> 0 holds a / b = (a / c) * (c / b) proof let c, a, b be complex number ; ::_thesis: ( c <> 0 implies a / b = (a / c) * (c / b) ) assume A1: c <> 0 ; ::_thesis: a / b = (a / c) * (c / b) thus a / b = a * (b ") by XCMPLX_0:def_9 .= ((a / c) * c) * (b ") by A1, Lm3 .= (a / c) * (c * (b ")) .= (a / c) * (c / b) by XCMPLX_0:def_9 ; ::_thesis: verum end; theorem :: XCMPLX_1:99 for a, b being complex number holds a * (1 / b) = a / b by Lm14; Lm16: for a being complex number holds 1 / (a ") = a proof let a be complex number ; ::_thesis: 1 / (a ") = a 1 / (a ") = (a ") " by Lm4 .= a ; hence 1 / (a ") = a ; ::_thesis: verum end; theorem :: XCMPLX_1:100 for a, b being complex number holds a / (1 / b) = a * b proof let a, b be complex number ; ::_thesis: a / (1 / b) = a * b thus a / (1 / b) = a / (b ") by Lm4 .= a * (1 / (b ")) by Lm14 .= a * b by Lm16 ; ::_thesis: verum end; theorem :: XCMPLX_1:101 for a, b, c being complex number holds (a / b) * c = ((1 / b) * c) * a proof let a, b, c be complex number ; ::_thesis: (a / b) * c = ((1 / b) * c) * a (a / b) * c = ((1 / b) * a) * c by Lm14; hence (a / b) * c = ((1 / b) * c) * a ; ::_thesis: verum end; theorem :: XCMPLX_1:102 for a, b being complex number holds (1 / a) * (1 / b) = 1 / (a * b) proof let a, b be complex number ; ::_thesis: (1 / a) * (1 / b) = 1 / (a * b) thus (1 / a) * (1 / b) = (a ") * (1 / b) by Lm4 .= (a ") * (b ") by Lm4 .= (a * b) " by Lm1 .= 1 / (a * b) by Lm4 ; ::_thesis: verum end; theorem :: XCMPLX_1:103 for c, a, b being complex number holds (1 / c) * (a / b) = a / (b * c) by Lm15; theorem :: XCMPLX_1:104 for a, b, c being complex number holds (a / b) / c = (1 / b) * (a / c) proof let a, b, c be complex number ; ::_thesis: (a / b) / c = (1 / b) * (a / c) (a / b) / c = (a * (b ")) / c by XCMPLX_0:def_9 .= (a * (b ")) * (c ") by XCMPLX_0:def_9 .= (a * (c ")) * (b ") .= (a / c) * (b ") by XCMPLX_0:def_9 .= (a / c) / b by XCMPLX_0:def_9 ; hence (a / b) / c = (b ") * (a / c) by XCMPLX_0:def_9 .= (1 / b) * (a / c) by Lm4 ; ::_thesis: verum end; theorem :: XCMPLX_1:105 for a, b, c being complex number holds (a / b) / c = (1 / c) * (a / b) proof let a, b, c be complex number ; ::_thesis: (a / b) / c = (1 / c) * (a / b) thus (a / b) / c = (c ") * (a / b) by XCMPLX_0:def_9 .= (1 / c) * (a / b) by Lm4 ; ::_thesis: verum end; theorem Th106: :: XCMPLX_1:106 for a being complex number st a <> 0 holds a * (1 / a) = 1 proof let a be complex number ; ::_thesis: ( a <> 0 implies a * (1 / a) = 1 ) assume A1: a <> 0 ; ::_thesis: a * (1 / a) = 1 thus a * (1 / a) = a * (a ") by Lm4 .= 1 by A1, XCMPLX_0:def_7 ; ::_thesis: verum end; theorem :: XCMPLX_1:107 for b, a being complex number st b <> 0 holds a = (a * b) * (1 / b) proof let b, a be complex number ; ::_thesis: ( b <> 0 implies a = (a * b) * (1 / b) ) A1: a = a * 1 ; assume b <> 0 ; ::_thesis: a = (a * b) * (1 / b) then a = a * (b / b) by A1, Lm5; then a = a * (b * (b ")) by XCMPLX_0:def_9 .= a * (b * (1 / b)) by Lm4 ; hence a = (a * b) * (1 / b) ; ::_thesis: verum end; theorem :: XCMPLX_1:108 for b, a being complex number st b <> 0 holds a = a * ((1 / b) * b) proof let b, a be complex number ; ::_thesis: ( b <> 0 implies a = a * ((1 / b) * b) ) assume A1: b <> 0 ; ::_thesis: a = a * ((1 / b) * b) thus a = a * 1 .= a * ((1 / b) * b) by A1, Lm3 ; ::_thesis: verum end; theorem :: XCMPLX_1:109 for b, a being complex number st b <> 0 holds a = (a * (1 / b)) * b proof let b, a be complex number ; ::_thesis: ( b <> 0 implies a = (a * (1 / b)) * b ) assume A1: b <> 0 ; ::_thesis: a = (a * (1 / b)) * b a = a * 1 .= a * ((1 / b) * b) by A1, Lm3 ; hence a = (a * (1 / b)) * b ; ::_thesis: verum end; theorem :: XCMPLX_1:110 for b, a being complex number st b <> 0 holds a = a / (b * (1 / b)) proof let b, a be complex number ; ::_thesis: ( b <> 0 implies a = a / (b * (1 / b)) ) assume A1: b <> 0 ; ::_thesis: a = a / (b * (1 / b)) thus a = a / 1 .= a / (b * (1 / b)) by A1, Th106 ; ::_thesis: verum end; theorem :: XCMPLX_1:111 for a, b being complex number st a <> 0 & b <> 0 holds 1 / (a * b) <> 0 ; theorem :: XCMPLX_1:112 for a, b being complex number st a <> 0 & b <> 0 holds (a / b) * (b / a) = 1 proof let a, b be complex number ; ::_thesis: ( a <> 0 & b <> 0 implies (a / b) * (b / a) = 1 ) assume A1: ( a <> 0 & b <> 0 ) ; ::_thesis: (a / b) * (b / a) = 1 b / a = (a / b) " by Lm7; hence (a / b) * (b / a) = 1 by A1, XCMPLX_0:def_7; ::_thesis: verum end; theorem Th113: :: XCMPLX_1:113 for b, a, c being complex number st b <> 0 holds (a / b) + c = (a + (b * c)) / b proof let b, a, c be complex number ; ::_thesis: ( b <> 0 implies (a / b) + c = (a + (b * c)) / b ) assume A1: b <> 0 ; ::_thesis: (a / b) + c = (a + (b * c)) / b (a / b) + c = (a / b) + (1 * c) .= (a / b) + ((b * (b ")) * c) by A1, XCMPLX_0:def_7 .= (a / b) + ((b * c) * (b ")) .= (a / b) + ((c * b) / b) by XCMPLX_0:def_9 .= (a + (c * b)) / b by Th62 ; hence (a / b) + c = (a + (b * c)) / b ; ::_thesis: verum end; theorem Th114: :: XCMPLX_1:114 for c, a, b being complex number st c <> 0 holds a + b = c * ((a / c) + (b / c)) proof let c, a, b be complex number ; ::_thesis: ( c <> 0 implies a + b = c * ((a / c) + (b / c)) ) assume A1: c <> 0 ; ::_thesis: a + b = c * ((a / c) + (b / c)) hence a + b = (c * (a / c)) + b by Lm3 .= (c * (a / c)) + (c * (b / c)) by A1, Lm3 .= c * ((a / c) + (b / c)) ; ::_thesis: verum end; theorem Th115: :: XCMPLX_1:115 for c, a, b being complex number st c <> 0 holds a + b = ((a * c) + (b * c)) / c proof let c, a, b be complex number ; ::_thesis: ( c <> 0 implies a + b = ((a * c) + (b * c)) / c ) assume A1: c <> 0 ; ::_thesis: a + b = ((a * c) + (b * c)) / c hence a + b = ((a * c) / c) + b by Lm9 .= ((a * c) / c) + ((b * c) / c) by A1, Lm9 .= ((a * c) + (b * c)) / c by Th62 ; ::_thesis: verum end; theorem Th116: :: XCMPLX_1:116 for b, d, a, c being complex number st b <> 0 & d <> 0 holds (a / b) + (c / d) = ((a * d) + (c * b)) / (b * d) proof let b, d, a, c be complex number ; ::_thesis: ( b <> 0 & d <> 0 implies (a / b) + (c / d) = ((a * d) + (c * b)) / (b * d) ) assume A1: b <> 0 ; ::_thesis: ( not d <> 0 or (a / b) + (c / d) = ((a * d) + (c * b)) / (b * d) ) assume d <> 0 ; ::_thesis: (a / b) + (c / d) = ((a * d) + (c * b)) / (b * d) hence (a / b) + (c / d) = ((a * d) / (b * d)) + (c / d) by Lm10 .= ((a * d) / (b * d)) + ((c * b) / (b * d)) by A1, Lm10 .= ((a * d) + (c * b)) / (b * d) by Th62 ; ::_thesis: verum end; theorem Th117: :: XCMPLX_1:117 for a, b being complex number st a <> 0 holds a + b = a * (1 + (b / a)) proof let a, b be complex number ; ::_thesis: ( a <> 0 implies a + b = a * (1 + (b / a)) ) assume A1: a <> 0 ; ::_thesis: a + b = a * (1 + (b / a)) hence a + b = a * ((a / a) + (b / a)) by Th114 .= a * (1 + (b / a)) by A1, Lm5 ; ::_thesis: verum end; theorem :: XCMPLX_1:118 for a, b being complex number holds (a / (2 * b)) + (a / (2 * b)) = a / b proof let a, b be complex number ; ::_thesis: (a / (2 * b)) + (a / (2 * b)) = a / b thus (a / (2 * b)) + (a / (2 * b)) = (a + a) / (2 * b) by Th62 .= (2 * a) / (2 * b) .= a / b by Lm10 ; ::_thesis: verum end; theorem :: XCMPLX_1:119 for a, b being complex number holds ((a / (3 * b)) + (a / (3 * b))) + (a / (3 * b)) = a / b proof let a, b be complex number ; ::_thesis: ((a / (3 * b)) + (a / (3 * b))) + (a / (3 * b)) = a / b thus ((a / (3 * b)) + (a / (3 * b))) + (a / (3 * b)) = ((a + a) / (3 * b)) + (a / (3 * b)) by Th62 .= ((a + a) + a) / (3 * b) by Th62 .= (3 * a) / (3 * b) .= a / b by Lm10 ; ::_thesis: verum end; Lm17: for a, b being complex number holds - (a / b) = (- a) / b proof let a, b be complex number ; ::_thesis: - (a / b) = (- a) / b thus - (a / b) = - (a * (b ")) by XCMPLX_0:def_9 .= (- a) * (b ") .= (- a) / b by XCMPLX_0:def_9 ; ::_thesis: verum end; theorem Th120: :: XCMPLX_1:120 for a, c, b being complex number holds (a / c) - (b / c) = (a - b) / c proof let a, c, b be complex number ; ::_thesis: (a / c) - (b / c) = (a - b) / c thus (a / c) - (b / c) = (a / c) + (- (b / c)) .= (a / c) + ((- b) / c) by Lm17 .= (a + (- b)) / c by Th62 .= (a - b) / c ; ::_thesis: verum end; theorem :: XCMPLX_1:121 for a being complex number holds a - (a / 2) = a / 2 ; theorem :: XCMPLX_1:122 for a, b, c, d being complex number holds ((a - b) - c) / d = ((a / d) - (b / d)) - (c / d) proof let a, b, c, d be complex number ; ::_thesis: ((a - b) - c) / d = ((a / d) - (b / d)) - (c / d) thus ((a - b) - c) / d = ((a - b) / d) - (c / d) by Th120 .= ((a / d) - (b / d)) - (c / d) by Th120 ; ::_thesis: verum end; theorem :: XCMPLX_1:123 for b, d, a, e being complex number st b <> 0 & d <> 0 & b <> d & a / b = e / d holds a / b = (a - e) / (b - d) proof let b, d, a, e be complex number ; ::_thesis: ( b <> 0 & d <> 0 & b <> d & a / b = e / d implies a / b = (a - e) / (b - d) ) assume that A1: b <> 0 and A2: d <> 0 and A3: b <> d and A4: a / b = e / d ; ::_thesis: a / b = (a - e) / (b - d) a * d = e * b by A1, A2, A4, Th95; then A5: a * (b - d) = (a - e) * b ; b - d <> 0 by A3; hence a / b = (a - e) / (b - d) by A1, A5, Th94; ::_thesis: verum end; theorem :: XCMPLX_1:124 for a, b, e, d being complex number holds ((a + b) - e) / d = ((a / d) + (b / d)) - (e / d) proof let a, b, e, d be complex number ; ::_thesis: ((a + b) - e) / d = ((a / d) + (b / d)) - (e / d) thus ((a + b) - e) / d = ((a + b) / d) - (e / d) by Th120 .= ((a / d) + (b / d)) - (e / d) by Th62 ; ::_thesis: verum end; theorem :: XCMPLX_1:125 for a, b, e, d being complex number holds ((a - b) + e) / d = ((a / d) - (b / d)) + (e / d) proof let a, b, e, d be complex number ; ::_thesis: ((a - b) + e) / d = ((a / d) - (b / d)) + (e / d) thus ((a - b) + e) / d = ((a - b) / d) + (e / d) by Th62 .= ((a / d) - (b / d)) + (e / d) by Th120 ; ::_thesis: verum end; theorem Th126: :: XCMPLX_1:126 for b, a, e being complex number st b <> 0 holds (a / b) - e = (a - (e * b)) / b proof let b, a, e be complex number ; ::_thesis: ( b <> 0 implies (a / b) - e = (a - (e * b)) / b ) assume A1: b <> 0 ; ::_thesis: (a / b) - e = (a - (e * b)) / b thus (a / b) - e = (a / b) + (- e) .= (a + ((- e) * b)) / b by A1, Th113 .= (a - (e * b)) / b ; ::_thesis: verum end; theorem :: XCMPLX_1:127 for b, c, a being complex number st b <> 0 holds c - (a / b) = ((c * b) - a) / b proof let b, c, a be complex number ; ::_thesis: ( b <> 0 implies c - (a / b) = ((c * b) - a) / b ) assume A1: b <> 0 ; ::_thesis: c - (a / b) = ((c * b) - a) / b thus c - (a / b) = - ((a / b) - c) .= - ((a - (c * b)) / b) by A1, Th126 .= (- (a - (c * b))) / b by Lm17 .= ((c * b) - a) / b ; ::_thesis: verum end; theorem :: XCMPLX_1:128 for c, a, b being complex number st c <> 0 holds a - b = c * ((a / c) - (b / c)) proof let c, a, b be complex number ; ::_thesis: ( c <> 0 implies a - b = c * ((a / c) - (b / c)) ) assume A1: c <> 0 ; ::_thesis: a - b = c * ((a / c) - (b / c)) hence a - b = (c * (a / c)) - b by Lm3 .= (c * (a / c)) - (c * (b / c)) by A1, Lm3 .= c * ((a / c) - (b / c)) ; ::_thesis: verum end; theorem :: XCMPLX_1:129 for c, a, b being complex number st c <> 0 holds a - b = ((a * c) - (b * c)) / c proof let c, a, b be complex number ; ::_thesis: ( c <> 0 implies a - b = ((a * c) - (b * c)) / c ) assume A1: c <> 0 ; ::_thesis: a - b = ((a * c) - (b * c)) / c thus a - b = a + (- b) .= ((a * c) + ((- b) * c)) / c by A1, Th115 .= ((a * c) - (b * c)) / c ; ::_thesis: verum end; theorem :: XCMPLX_1:130 for b, d, a, c being complex number st b <> 0 & d <> 0 holds (a / b) - (c / d) = ((a * d) - (c * b)) / (b * d) proof let b, d, a, c be complex number ; ::_thesis: ( b <> 0 & d <> 0 implies (a / b) - (c / d) = ((a * d) - (c * b)) / (b * d) ) assume A1: b <> 0 ; ::_thesis: ( not d <> 0 or (a / b) - (c / d) = ((a * d) - (c * b)) / (b * d) ) assume A2: d <> 0 ; ::_thesis: (a / b) - (c / d) = ((a * d) - (c * b)) / (b * d) thus (a / b) - (c / d) = (a / b) + (- (c / d)) .= (a / b) + ((- c) / d) by Lm17 .= ((a * d) + ((- c) * b)) / (b * d) by A1, A2, Th116 .= ((a * d) - (c * b)) / (b * d) ; ::_thesis: verum end; theorem :: XCMPLX_1:131 for a, b being complex number st a <> 0 holds a - b = a * (1 - (b / a)) proof let a, b be complex number ; ::_thesis: ( a <> 0 implies a - b = a * (1 - (b / a)) ) assume A1: a <> 0 ; ::_thesis: a - b = a * (1 - (b / a)) thus a - b = a + (- b) .= a * (1 + ((- b) / a)) by A1, Th117 .= a * (1 + (- (b / a))) by Lm17 .= a * (1 - (b / a)) ; ::_thesis: verum end; theorem :: XCMPLX_1:132 for a, c, b being complex number st a <> 0 holds c = (((a * c) + b) - b) / a by Lm9; theorem :: XCMPLX_1:133 for a, b being complex number st - a = - b holds a = b ; theorem :: XCMPLX_1:134 for a being complex number st - a = 0 holds a = 0 ; theorem :: XCMPLX_1:135 for a, b being complex number st a + (- b) = 0 holds a = b ; theorem :: XCMPLX_1:136 for a, b being complex number holds a = (a + b) + (- b) ; theorem :: XCMPLX_1:137 for a, b being complex number holds a = a + (b + (- b)) ; theorem :: XCMPLX_1:138 for a, b being complex number holds a = ((- b) + a) + b ; theorem :: XCMPLX_1:139 for a, b being complex number holds - (a + b) = (- a) + (- b) ; theorem :: XCMPLX_1:140 for a, b being complex number holds - ((- a) + b) = a + (- b) ; theorem :: XCMPLX_1:141 for a, b being complex number holds a + b = - ((- a) + (- b)) ; theorem :: XCMPLX_1:142 for a, b being complex number holds - (a - b) = b - a ; theorem :: XCMPLX_1:143 for a, b being complex number holds (- a) - b = (- b) - a ; theorem :: XCMPLX_1:144 for a, b being complex number holds a = (- b) - ((- a) - b) ; theorem :: XCMPLX_1:145 for a, b, c being complex number holds ((- a) - b) - c = ((- a) - c) - b ; theorem :: XCMPLX_1:146 for a, b, c being complex number holds ((- a) - b) - c = ((- b) - c) - a ; theorem :: XCMPLX_1:147 for a, b, c being complex number holds ((- a) - b) - c = ((- c) - b) - a ; theorem :: XCMPLX_1:148 for c, a, b being complex number holds (c - a) - (c - b) = - (a - b) ; theorem :: XCMPLX_1:149 for a being complex number holds 0 - a = - a ; theorem :: XCMPLX_1:150 for a, b being complex number holds a + b = a - (- b) ; theorem :: XCMPLX_1:151 for a, b being complex number holds a = a - (b + (- b)) ; theorem :: XCMPLX_1:152 for a, c, b being complex number st a - c = b + (- c) holds a = b ; theorem :: XCMPLX_1:153 for c, a, b being complex number st c - a = c + (- b) holds a = b ; theorem :: XCMPLX_1:154 for a, b, c being complex number holds (a + b) - c = ((- c) + a) + b ; theorem :: XCMPLX_1:155 for a, b, c being complex number holds (a - b) + c = ((- b) + c) + a ; theorem :: XCMPLX_1:156 for a, b, c being complex number holds a - ((- b) - c) = (a + b) + c ; theorem :: XCMPLX_1:157 for a, b, c being complex number holds (a - b) - c = ((- b) - c) + a ; theorem :: XCMPLX_1:158 for a, b, c being complex number holds (a - b) - c = ((- c) + a) - b ; theorem :: XCMPLX_1:159 for a, b, c being complex number holds (a - b) - c = ((- c) - b) + a ; theorem :: XCMPLX_1:160 for a, b being complex number holds - (a + b) = (- b) - a ; theorem :: XCMPLX_1:161 for a, b being complex number holds - (a - b) = (- a) + b ; theorem :: XCMPLX_1:162 for a, b being complex number holds - ((- a) + b) = a - b ; theorem :: XCMPLX_1:163 for a, b being complex number holds a + b = - ((- a) - b) ; theorem :: XCMPLX_1:164 for a, b, c being complex number holds ((- a) + b) - c = ((- c) + b) - a ; theorem :: XCMPLX_1:165 for a, b, c being complex number holds ((- a) + b) - c = ((- c) - a) + b ; theorem :: XCMPLX_1:166 for a, b, c being complex number holds - ((a + b) + c) = ((- a) - b) - c ; theorem :: XCMPLX_1:167 for a, b, c being complex number holds - ((a + b) - c) = ((- a) - b) + c ; theorem :: XCMPLX_1:168 for a, b, c being complex number holds - ((a - b) + c) = ((- a) + b) - c ; theorem :: XCMPLX_1:169 for a, b, c being complex number holds - ((a - b) - c) = ((- a) + b) + c ; theorem :: XCMPLX_1:170 for a, b, c being complex number holds - (((- a) + b) + c) = (a - b) - c ; theorem :: XCMPLX_1:171 for a, b, c being complex number holds - (((- a) + b) - c) = (a - b) + c ; theorem :: XCMPLX_1:172 for a, b, c being complex number holds - (((- a) - b) + c) = (a + b) - c ; theorem :: XCMPLX_1:173 for a, b, c being complex number holds - (((- a) - b) - c) = (a + b) + c ; theorem :: XCMPLX_1:174 for a, b being complex number holds (- a) * b = - (a * b) ; theorem :: XCMPLX_1:175 for a, b being complex number holds (- a) * b = a * (- b) ; theorem :: XCMPLX_1:176 for a, b being complex number holds (- a) * (- b) = a * b ; theorem :: XCMPLX_1:177 for a, b being complex number holds - (a * (- b)) = a * b ; theorem :: XCMPLX_1:178 for a, b being complex number holds - ((- a) * b) = a * b ; theorem :: XCMPLX_1:179 for a being complex number holds (- 1) * a = - a ; theorem :: XCMPLX_1:180 for a being complex number holds (- a) * (- 1) = a ; theorem Th181: :: XCMPLX_1:181 for b, a being complex number st b <> 0 & a * b = - b holds a = - 1 proof let b, a be complex number ; ::_thesis: ( b <> 0 & a * b = - b implies a = - 1 ) assume that A1: b <> 0 and A2: a * b = - b ; ::_thesis: a = - 1 a * (b * (b ")) = (- b) * (b ") by A2, Th4; then a * 1 = (- b) * (b ") by A1, XCMPLX_0:def_7; hence a = - (b * (b ")) .= - 1 by A1, XCMPLX_0:def_7 ; ::_thesis: verum end; theorem Th182: :: XCMPLX_1:182 for a being complex number holds ( not a * a = 1 or a = 1 or a = - 1 ) proof let a be complex number ; ::_thesis: ( not a * a = 1 or a = 1 or a = - 1 ) assume a * a = 1 ; ::_thesis: ( a = 1 or a = - 1 ) then (a - 1) * (a + 1) = 0 ; then ( a - 1 = 0 or a + 1 = 0 ) ; hence ( a = 1 or a = - 1 ) ; ::_thesis: verum end; theorem :: XCMPLX_1:183 for a being complex number holds (- a) + (2 * a) = a ; theorem :: XCMPLX_1:184 for a, b, c being complex number holds (a - b) * c = (b - a) * (- c) ; theorem :: XCMPLX_1:185 for a, b, c being complex number holds (a - b) * c = - ((b - a) * c) ; theorem :: XCMPLX_1:186 for a being complex number holds a - (2 * a) = - a ; theorem :: XCMPLX_1:187 for a, b being complex number holds - (a / b) = (- a) / b by Lm17; theorem Th188: :: XCMPLX_1:188 for a, b being complex number holds a / (- b) = - (a / b) proof let a, b be complex number ; ::_thesis: a / (- b) = - (a / b) a / (- b) = (a * (- 1)) / ((- b) * (- 1)) by Lm10; then a / (- b) = (- a) / ((- (- b)) * 1) .= - (a / b) by Lm17 ; hence a / (- b) = - (a / b) ; ::_thesis: verum end; theorem :: XCMPLX_1:189 for a, b being complex number holds - (a / (- b)) = a / b proof let a, b be complex number ; ::_thesis: - (a / (- b)) = a / b thus - (a / (- b)) = - (- (a / b)) by Th188 .= a / b ; ::_thesis: verum end; theorem Th190: :: XCMPLX_1:190 for a, b being complex number holds - ((- a) / b) = a / b proof let a, b be complex number ; ::_thesis: - ((- a) / b) = a / b thus - ((- a) / b) = - (- (a / b)) by Lm17 .= a / b ; ::_thesis: verum end; theorem :: XCMPLX_1:191 for a, b being complex number holds (- a) / (- b) = a / b proof let a, b be complex number ; ::_thesis: (- a) / (- b) = a / b - ((- a) / b) = a / b by Th190; hence (- a) / (- b) = a / b by Th188; ::_thesis: verum end; theorem :: XCMPLX_1:192 for a, b being complex number holds (- a) / b = a / (- b) proof let a, b be complex number ; ::_thesis: (- a) / b = a / (- b) thus (- a) / b = - (a / b) by Lm17 .= a / (- b) by Th188 ; ::_thesis: verum end; theorem :: XCMPLX_1:193 for a being complex number holds - a = a / (- 1) ; theorem :: XCMPLX_1:194 for a being complex number holds a = (- a) / (- 1) ; theorem :: XCMPLX_1:195 for a, b being complex number st a / b = - 1 holds ( a = - b & b = - a ) proof let a, b be complex number ; ::_thesis: ( a / b = - 1 implies ( a = - b & b = - a ) ) assume A1: a / b = - 1 ; ::_thesis: ( a = - b & b = - a ) then b <> 0 by Th49; then a = (- 1) * b by A1, Lm3; hence ( a = - b & b = - a ) ; ::_thesis: verum end; theorem :: XCMPLX_1:196 for b, a being complex number st b <> 0 & b / a = - b holds a = - 1 proof let b, a be complex number ; ::_thesis: ( b <> 0 & b / a = - b implies a = - 1 ) assume that A1: b <> 0 and A2: b / a = - b ; ::_thesis: a = - 1 a <> 0 by A1, A2, Th49; then b = (- b) * a by A2, Lm3; then b = - (b * a) ; hence a = - 1 by A1, A2, Th181; ::_thesis: verum end; theorem :: XCMPLX_1:197 for a being complex number st a <> 0 holds (- a) / a = - 1 proof let a be complex number ; ::_thesis: ( a <> 0 implies (- a) / a = - 1 ) assume A1: a <> 0 ; ::_thesis: (- a) / a = - 1 thus (- a) / a = - (a / a) by Lm17 .= - 1 by A1, Lm5 ; ::_thesis: verum end; theorem :: XCMPLX_1:198 for a being complex number st a <> 0 holds a / (- a) = - 1 proof let a be complex number ; ::_thesis: ( a <> 0 implies a / (- a) = - 1 ) assume A1: a <> 0 ; ::_thesis: a / (- a) = - 1 thus a / (- a) = - (a / a) by Th188 .= - 1 by A1, Lm5 ; ::_thesis: verum end; Lm18: for a being complex number st a <> 0 & a = a " & not a = 1 holds a = - 1 proof let a be complex number ; ::_thesis: ( a <> 0 & a = a " & not a = 1 implies a = - 1 ) assume A1: a <> 0 ; ::_thesis: ( not a = a " or a = 1 or a = - 1 ) assume a = a " ; ::_thesis: ( a = 1 or a = - 1 ) then a * a = 1 by A1, XCMPLX_0:def_7; hence ( a = 1 or a = - 1 ) by Th182; ::_thesis: verum end; theorem :: XCMPLX_1:199 for a being complex number st a <> 0 & a = 1 / a & not a = 1 holds a = - 1 proof let a be complex number ; ::_thesis: ( a <> 0 & a = 1 / a & not a = 1 implies a = - 1 ) assume a <> 0 ; ::_thesis: ( not a = 1 / a or a = 1 or a = - 1 ) then ( not a = a " or a = 1 or a = - 1 ) by Lm18; hence ( not a = 1 / a or a = 1 or a = - 1 ) by Lm4; ::_thesis: verum end; theorem :: XCMPLX_1:200 for b, d, a, e being complex number st b <> 0 & d <> 0 & b <> - d & a / b = e / d holds a / b = (a + e) / (b + d) proof let b, d, a, e be complex number ; ::_thesis: ( b <> 0 & d <> 0 & b <> - d & a / b = e / d implies a / b = (a + e) / (b + d) ) assume that A1: b <> 0 and A2: d <> 0 and A3: b <> - d and A4: a / b = e / d ; ::_thesis: a / b = (a + e) / (b + d) a * d = e * b by A1, A2, A4, Th95; then A5: a * (b + d) = (a + e) * b ; b + d <> 0 by A3; hence a / b = (a + e) / (b + d) by A1, A5, Th94; ::_thesis: verum end; theorem :: XCMPLX_1:201 for a, b being complex number st a " = b " holds a = b by Lm12; theorem :: XCMPLX_1:202 0 " = 0 ; theorem :: XCMPLX_1:203 for b, a being complex number st b <> 0 holds a = (a * b) * (b ") proof let b, a be complex number ; ::_thesis: ( b <> 0 implies a = (a * b) * (b ") ) A1: a * (b * (b ")) = (a * b) * (b ") ; assume b <> 0 ; ::_thesis: a = (a * b) * (b ") then a * 1 = (a * b) * (b ") by A1, XCMPLX_0:def_7; hence a = (a * b) * (b ") ; ::_thesis: verum end; theorem :: XCMPLX_1:204 for a, b being complex number holds (a ") * (b ") = (a * b) " by Lm1; theorem :: XCMPLX_1:205 for a, b being complex number holds (a * (b ")) " = (a ") * b by Lm11; theorem :: XCMPLX_1:206 for a, b being complex number holds ((a ") * (b ")) " = a * b proof let a, b be complex number ; ::_thesis: ((a ") * (b ")) " = a * b thus ((a ") * (b ")) " = ((a ") ") * ((b ") ") by Lm1 .= a * b ; ::_thesis: verum end; theorem :: XCMPLX_1:207 for a, b being complex number st a <> 0 & b <> 0 holds a * (b ") <> 0 ; theorem :: XCMPLX_1:208 for a, b being complex number st a <> 0 & b <> 0 holds (a ") * (b ") <> 0 ; theorem :: XCMPLX_1:209 for a, b being complex number st a * (b ") = 1 holds a = b proof let a, b be complex number ; ::_thesis: ( a * (b ") = 1 implies a = b ) assume a * (b ") = 1 ; ::_thesis: a = b then a / b = 1 by XCMPLX_0:def_9; hence a = b by Th58; ::_thesis: verum end; theorem :: XCMPLX_1:210 for a, b being complex number st a * b = 1 holds a = b " proof let a, b be complex number ; ::_thesis: ( a * b = 1 implies a = b " ) assume A1: a * b = 1 ; ::_thesis: a = b " then b <> 0 ; hence a = b " by A1, XCMPLX_0:def_7; ::_thesis: verum end; theorem Th211: :: XCMPLX_1:211 for a, b being complex number st a <> 0 & b <> 0 holds (a ") + (b ") = (a + b) * ((a * b) ") proof let a, b be complex number ; ::_thesis: ( a <> 0 & b <> 0 implies (a ") + (b ") = (a + b) * ((a * b) ") ) assume that A1: a <> 0 and A2: b <> 0 ; ::_thesis: (a ") + (b ") = (a + b) * ((a * b) ") b " = (b ") * 1 ; then b " = (b ") * ((a ") * a) by A1, XCMPLX_0:def_7; then b " = ((a ") * (b ")) * a ; then A3: b " = ((a * b) ") * a by Lm1; a " = (a ") * 1 ; then a " = (a ") * ((b ") * b) by A2, XCMPLX_0:def_7; then a " = ((a ") * (b ")) * b ; then a " = ((a * b) ") * b by Lm1; hence (a ") + (b ") = (a + b) * ((a * b) ") by A3; ::_thesis: verum end; Lm19: for a being complex number holds (- a) " = - (a ") proof let a be complex number ; ::_thesis: (- a) " = - (a ") thus (- a) " = 1 / (- a) by Lm4 .= - (1 / a) by Th188 .= - (a ") by Lm4 ; ::_thesis: verum end; theorem :: XCMPLX_1:212 for a, b being complex number st a <> 0 & b <> 0 holds (a ") - (b ") = (b - a) * ((a * b) ") proof let a, b be complex number ; ::_thesis: ( a <> 0 & b <> 0 implies (a ") - (b ") = (b - a) * ((a * b) ") ) assume A1: ( a <> 0 & b <> 0 ) ; ::_thesis: (a ") - (b ") = (b - a) * ((a * b) ") thus (a ") - (b ") = (a ") + (- (b ")) .= (a ") + ((- b) ") by Lm19 .= (a + (- b)) * ((a * (- b)) ") by A1, Th211 .= (a + (- b)) * ((- (a * b)) ") .= (a + (- b)) * (- ((a * b) ")) by Lm19 .= (b - a) * ((a * b) ") ; ::_thesis: verum end; theorem :: XCMPLX_1:213 for a, b being complex number holds (a / b) " = b / a by Lm7; theorem :: XCMPLX_1:214 for a, b being complex number holds (a ") / (b ") = b / a proof let a, b be complex number ; ::_thesis: (a ") / (b ") = b / a thus (a ") / (b ") = (a ") * ((b ") ") by XCMPLX_0:def_9 .= b / a by XCMPLX_0:def_9 ; ::_thesis: verum end; theorem :: XCMPLX_1:215 for a being complex number holds 1 / a = a " by Lm4; theorem :: XCMPLX_1:216 for a being complex number holds 1 / (a ") = a by Lm16; theorem :: XCMPLX_1:217 for a being complex number holds (1 / a) " = a proof let a be complex number ; ::_thesis: (1 / a) " = a ( 1 / a = a " implies (1 / a) " = a ) ; hence (1 / a) " = a by Lm4; ::_thesis: verum end; theorem :: XCMPLX_1:218 for a, b being complex number st 1 / a = b " holds a = b proof let a, b be complex number ; ::_thesis: ( 1 / a = b " implies a = b ) ( 1 / a = 1 / b implies a = b ) by Th59; hence ( 1 / a = b " implies a = b ) by Lm4; ::_thesis: verum end; theorem :: XCMPLX_1:219 for a, b being complex number holds a / (b ") = a * b proof let a, b be complex number ; ::_thesis: a / (b ") = a * b thus a / (b ") = a * ((b ") ") by XCMPLX_0:def_9 .= a * b ; ::_thesis: verum end; theorem :: XCMPLX_1:220 for a, c, b being complex number holds (a ") * (c / b) = c / (a * b) proof let a, c, b be complex number ; ::_thesis: (a ") * (c / b) = c / (a * b) thus (a ") * (c / b) = (a ") * (c * (b ")) by XCMPLX_0:def_9 .= c * ((a ") * (b ")) .= c * ((a * b) ") by Lm1 .= c / (a * b) by XCMPLX_0:def_9 ; ::_thesis: verum end; theorem :: XCMPLX_1:221 for a, b being complex number holds (a ") / b = (a * b) " proof let a, b be complex number ; ::_thesis: (a ") / b = (a * b) " thus (a ") / b = (a ") * (b ") by XCMPLX_0:def_9 .= (a * b) " by Lm1 ; ::_thesis: verum end; theorem :: XCMPLX_1:222 for a being complex number holds (- a) " = - (a ") by Lm19; theorem :: XCMPLX_1:223 for a being complex number st a <> 0 & a = a " & not a = 1 holds a = - 1 by Lm18; begin theorem :: XCMPLX_1:224 for a, b, c being complex number holds ((a + b) + c) - b = a + c ; theorem :: XCMPLX_1:225 for a, b, c being complex number holds ((a - b) + c) + b = a + c ; theorem :: XCMPLX_1:226 for a, b, c being complex number holds ((a + b) - c) - b = a - c ; theorem :: XCMPLX_1:227 for a, b, c being complex number holds ((a - b) - c) + b = a - c ; theorem :: XCMPLX_1:228 for a, b being complex number holds (a - a) - b = - b ; theorem :: XCMPLX_1:229 for a, b being complex number holds ((- a) + a) - b = - b ; theorem :: XCMPLX_1:230 for a, b being complex number holds (a - b) - a = - b ; theorem :: XCMPLX_1:231 for a, b being complex number holds ((- a) - b) + a = - b ; begin theorem :: XCMPLX_1:232 for a, b being complex number st b <> 0 holds ex e being complex number st a = b / e proof let a, b be complex number ; ::_thesis: ( b <> 0 implies ex e being complex number st a = b / e ) assume A1: b <> 0 ; ::_thesis: ex e being complex number st a = b / e percases ( a = 0 or a <> 0 ) ; supposeA2: a = 0 ; ::_thesis: ex e being complex number st a = b / e take 0 ; ::_thesis: a = b / 0 b / 0 = b * (0 ") by XCMPLX_0:def_9; hence a = b / 0 by A2; ::_thesis: verum end; supposeA3: a <> 0 ; ::_thesis: ex e being complex number st a = b / e take e = b / a; ::_thesis: a = b / e thus a = a * 1 .= a * (e * (e ")) by A1, A3, XCMPLX_0:def_7 .= (a * e) * (e ") .= (a * ((a ") * b)) * (e ") by XCMPLX_0:def_9 .= ((a * (a ")) * b) * (e ") .= (1 * b) * (e ") by A3, XCMPLX_0:def_7 .= b / e by XCMPLX_0:def_9 ; ::_thesis: verum end; end; end; theorem :: XCMPLX_1:233 for a, b, c, d, e being complex number holds a / ((b * c) * (d / e)) = (e / c) * (a / (b * d)) proof let a, b, c, d, e be complex number ; ::_thesis: a / ((b * c) * (d / e)) = (e / c) * (a / (b * d)) thus a / ((b * c) * (d / e)) = a / ((b * c) * (d * (e "))) by XCMPLX_0:def_9 .= a / (c * ((b * d) * (e "))) .= a / (c * ((b * d) / e)) by XCMPLX_0:def_9 .= a / ((b * d) / (e / c)) by Th81 .= (e / c) * (a / (b * d)) by Th81 ; ::_thesis: verum end; theorem :: XCMPLX_1:234 for d, c, b, a being complex number holds (((d - c) / b) * a) + c = ((1 - (a / b)) * c) + ((a / b) * d) proof let d, c, b, a be complex number ; ::_thesis: (((d - c) / b) * a) + c = ((1 - (a / b)) * c) + ((a / b) * d) percases ( b = 0 or b <> 0 ) ; supposeA1: b = 0 ; ::_thesis: (((d - c) / b) * a) + c = ((1 - (a / b)) * c) + ((a / b) * d) A2: a / b = a * (b ") by XCMPLX_0:def_9 .= a * 0 by A1 ; thus (((d - c) / b) * a) + c = (((d - c) * (b ")) * a) + c by XCMPLX_0:def_9 .= (((d - c) * 0) * a) + c by A1 .= ((1 - (a / b)) * c) + ((a / b) * d) by A2 ; ::_thesis: verum end; supposeA3: b <> 0 ; ::_thesis: (((d - c) / b) * a) + c = ((1 - (a / b)) * c) + ((a / b) * d) (((d - c) / b) * a) + c = (((d - c) / b) * a) + (c * 1) .= (((d - c) / b) * a) + (c * (b / b)) by A3, Lm5 .= (((d - c) / b) * a) + ((c * b) / b) by Lm8 .= (((d - c) * a) / b) + ((c * b) / b) by Lm8 .= (((d - c) * a) + (c * b)) / b by Th62 .= (((b - a) * c) + (a * d)) / b .= (((b - a) * c) / b) + ((a * d) / b) by Th62 .= (((b - a) * c) / b) + ((a / b) * d) by Lm8 .= (((b - a) / b) * c) + ((a / b) * d) by Lm8 .= (((b / b) - (a / b)) * c) + ((a / b) * d) by Th120 .= ((1 - (a / b)) * c) + ((a / b) * d) by A3, Lm5 ; hence (((d - c) / b) * a) + c = ((1 - (a / b)) * c) + ((a / b) * d) ; ::_thesis: verum end; end; end; theorem :: XCMPLX_1:235 for a, b, c being complex number st a <> 0 holds (a * b) + c = a * (b + (c / a)) proof let a, b, c be complex number ; ::_thesis: ( a <> 0 implies (a * b) + c = a * (b + (c / a)) ) assume a <> 0 ; ::_thesis: (a * b) + c = a * (b + (c / a)) hence (a * b) + c = (a * b) + (a * (c / a)) by Lm3 .= a * (b + (c / a)) ; ::_thesis: verum end;