q implies p.i=i-1) proof let n,q be Nat; defpred R[Nat,set] means ($1q implies $2=$1-1); assume A1: q in Seg(n+1); A2: for i being Nat st i in Seg(n+1) ex p being Element of NAT st R[i,p] proof let i be Nat; assume i in Seg(n+1); per cases by XXREAL_0:1; suppose A3: iq; 1 <= q by A1,FINSEQ_1:1; then reconsider p=i-1 as Element of NAT by A5,INT_1:5,XXREAL_0:2; take p; thus thesis by A5; end; end; consider p being FinSequence of NAT such that A6: dom p = Seg(n+1) and A7: for i being Nat st i in Seg(n+1) holds R[i,p/.i] from RECDEF_1:sch 17(A2); A8: for i being Element of NAT st i in Seg(n+1) holds i=q iff p/.i=n+1 proof let i be Element of NAT; assume A9: i in Seg(n+1); hence i=q implies p/.i=n+1 by A7; thus p/.i=n+1 implies i=q proof assume A10: p/.i=n+1; per cases by XXREAL_0:1; suppose i=q; hence thesis; end; suppose iq; then i-1 = n+1 by A7,A9,A10; then i >= n+1+1; then i > n+1 by NAT_1:13; hence thesis by A9,FINSEQ_1:1; end; end; end; A11: for i being Element of NAT st i in Seg(n+1) holds (iq implies p.i=i-1) proof let i be Element of NAT; assume A12: i in Seg(n+1); then p/.i = p.i by A6,PARTFUN1:def 6; hence thesis by A7,A12; end; for i being object holds i in rng p iff i in Seg(n+1) proof let i being object; thus i in rng p implies i in Seg(n+1) proof assume i in rng p; then consider j being object such that A13: j in Seg(n+1) and A14: p.j = i by A6,FUNCT_1:def 3; reconsider j as Element of NAT by A13; per cases by XXREAL_0:1; suppose jq; then A16: i = j-1 by A11,A13,A14; A17: 1 <= q by A1,FINSEQ_1:1; then reconsider i as Element of NAT by A15,A16,INT_1:5,XXREAL_0:2; j <= n+1 by A13,FINSEQ_1:1; then i <= n by A16,XREAL_1:20; then A18: i <= n+1 by NAT_1:12; 1 < i+1 by A15,A16,A17,XXREAL_0:2; then 1 <= i by NAT_1:13; hence thesis by A18,FINSEQ_1:1; end; end; thus i in Seg(n+1) implies i in rng p proof assume A19: i in Seg(n+1); then reconsider i as Element of NAT; i <= n+1 by A19,FINSEQ_1:1; then A20: i = n+1 or i < n+1 by XXREAL_0:1; per cases by A20,NAT_1:13; suppose i < q; then p.i = i by A11,A19; hence thesis by A6,A19,FUNCT_1:3; end; suppose A21: q <= i & i <= n; A22: 1 <= i+1 by NAT_1:12; i+1 <= n+1 by A21,XREAL_1:6; then A23: i+1 in Seg(n+1) by A22,FINSEQ_1:1; q < i+1 by A21,NAT_1:13; then p.(i+1) = i+1-1 by A11,A23 .= i; hence thesis by A6,A23,FUNCT_1:3; end; suppose i=n+1; then p.q = i by A1,A11; hence thesis by A1,A6,FUNCT_1:3; end; end; end; then A24: rng p = Seg(n+1) by TARSKI:2; then A25: p is Function of Seg(n+1), Seg(n+1) by A6,FUNCT_2:1; A26: for i being Element of NAT st i in Seg(n+1) & p/.i<>n+1 holds in+1; thus iq; then p/.i = i-1 by A7,A27; then i-1+1 < q+1 by A29,XREAL_1:8; hence thesis by A30,NAT_1:13; end; end; end; for i1,i2 being object st i1 in Seg(n+1) & i2 in Seg(n+1) & p.i1 = p.i2 holds i1 = i2 proof let i1,i2 be object; assume that A31: i1 in Seg(n+1) and A32: i2 in Seg(n+1) and A33: p.i1 = p.i2; reconsider i1 as Element of NAT by A31; A34: p/.i1 = p.i1 by A6,A31,PARTFUN1:def 6; reconsider i2 as Element of NAT by A32; A35: p/.i2 = p.i2 by A6,A32,PARTFUN1:def 6; per cases; suppose A36: p/.i1 = n+1; then i1 = q by A8,A31; hence thesis by A8,A32,A33,A34,A35,A36; end; suppose A37: p/.i1 <> n+1 & p/.i1 < q; then i1n+1 & p/.i1 >= q; then A40: i1 <> q by A8,A31; i1 >= q by A26,A31,A39; then i1 > q by A40,XXREAL_0:1; then A41: p/.i1=i1-1 by A7,A31; A42: i2 <> q by A8,A32,A33,A34,A35,A39; i2 >= q by A26,A32,A33,A34,A35,A39; then i2 > q by A42,XXREAL_0:1; then p/.i2=i2-1 by A7,A32; hence thesis by A6,A32,A33,A34,A41,PARTFUN1:def 6,XCMPLX_1:19; end; end; then p is one-to-one by A6,FUNCT_1:def 4; then reconsider p as Permutation of Seg(n+1) by A24,A25,FUNCT_2:57; take p; thus thesis by A11; end; Lm4: for n,q being Nat, s,p being Permutation of Seg(n+1), s9 being FinSequence of Seg(n+1) st s9=s & q=s.(n+1) & for i being Element of NAT st i in Seg(n+1) holds (iq implies p. i=i-1) holds p*s9|n is Permutation of Seg n proof let n,q be Nat, s,p be Permutation of Seg(n+1), s9 be FinSequence of Seg(n+1 ); assume that A1: s9=s and A2: q=s.(n+1) and A3: for i being Element of NAT st i in Seg(n+1) holds (iq implies p.i=i-1); A4: dom p = Seg(n+1) by FUNCT_2:def 1; reconsider r=p*s9|n as FinSequence of Seg(n+1) by FINSEQ_2:32; A5: 0+n <= 1+n by XREAL_1:6; then A6: Seg n c= Seg(n+1) by FINSEQ_1:5; s9|n = s9 | Seg n by FINSEQ_1:def 15; then A7: s9|n is one-to-one by A1,FUNCT_1:52; A8: rng p = Seg(n+1) by FUNCT_2:def 3; A9: dom s = Seg(n+1) by FUNCT_2:def 1; then len s9 = n+1 by A1,FINSEQ_1:def 3; then len(s9|n) = n by A5,FINSEQ_1:59; then len r = n by FINSEQ_2:33; then A10: dom r = Seg n by FINSEQ_1:def 3; A11: rng s = Seg(n+1) by FUNCT_2:def 3; then q in Seg(n+1) by A2,A9,FINSEQ_1:4,FUNCT_1:3; then A12: q <= n+1 by FINSEQ_1:1; for i being object holds i in rng r iff i in Seg n proof let i being object; thus i in rng r implies i in Seg n proof assume i in rng r; then consider j being object such that A13: j in Seg n and A14: r.j = i by A10,FUNCT_1:def 3; reconsider j as Element of NAT by A13; A15: j <= n by A13,FINSEQ_1:1; then A16: (s9|n).j = s.j by A1,FINSEQ_3:112; then A17: i = p.(s.j) by A10,A13,A14,FUNCT_1:12; s.j in dom p by A9,A11,A4,A6,A13,FUNCT_1:3; then A18: p.(s.j) in rng p by FUNCT_1:3; then reconsider i as Element of NAT by A8,A10,A13,A14,A16,FUNCT_1:12; A19: n+1 in dom s by A9,FINSEQ_1:4; A20: s.j in Seg(n+1) by A9,A11,A6,A13,FUNCT_1:3; then reconsider q1 = s.j as Element of NAT; j < n+1 by A15,NAT_1:13; then A21: q1 <> q by A2,A9,A6,A13,A19,FUNCT_1:def 4; per cases by A21,XXREAL_0:1; suppose q1 < q; then i < q by A3,A17,A20; then i < n+1 by A12,XXREAL_0:2; then A22: i <= n by NAT_1:13; 1 <= i by A17,A18,FINSEQ_1:1; hence thesis by A22,FINSEQ_1:1; end; suppose A23: q1 > q; A24: q1 <= n+1 by A20,FINSEQ_1:1; i = q1-1 by A3,A17,A20,A23; then A25: i <= n by A24,XREAL_1:20; 1 <= i by A17,A18,FINSEQ_1:1; hence thesis by A25,FINSEQ_1:1; end; end; assume A26: i in Seg n; then reconsider i as Element of NAT; per cases; suppose A27: i < q; then A28: p.i = i by A3,A6,A26; consider j being object such that A29: j in dom s and A30: i = s.j by A11,A6,A26,FUNCT_1:def 3; j in Seg(n+1) by A29; then reconsider j as Element of NAT; j <= n+1 by A29,FINSEQ_1:1; then j < n+1 by A2,A27,A30,XXREAL_0:1; then A31: j <= n by NAT_1:13; 1 <= j by A29,FINSEQ_1:1; then A32: j in dom r by A10,A31,FINSEQ_1:1; (s9|n).j = s.j by A1,A31,FINSEQ_3:112; then r.j = i by A28,A30,A32,FUNCT_1:12; hence thesis by A32,FUNCT_1:3; end; suppose A33: i >= q; i <= n by A26,FINSEQ_1:1; then A34: i+1 <= n+1 by XREAL_1:6; 1 <= i+1 by NAT_1:12; then A35: i+1 in Seg(n+1) by A34,FINSEQ_1:1; then consider j being object such that A36: j in dom s and A37: i+1 = s.j by A11,FUNCT_1:def 3; j in Seg(n+1) by A36; then reconsider j as Element of NAT; A38: j <= n+1 by A36,FINSEQ_1:1; j <> n+1 by A2,A33,A37,NAT_1:13; then j < n+1 by A38,XXREAL_0:1; then A39: j <= n by NAT_1:13; 1 <= j by A36,FINSEQ_1:1; then A40: j in Seg n by A39,FINSEQ_1:1; i+1 > q by A33,NAT_1:13; then A41: p.(i+1) = i+1-1 by A3,A35 .= i; (s9|n).j = s.j by A1,A39,FINSEQ_3:112; then r.j = p.(s.j) by A10,A40,FUNCT_1:12; hence thesis by A10,A37,A41,A40,FUNCT_1:3; end; end; then A42: rng r = Seg n by TARSKI:2; then p*s9|n is Function of Seg n, Seg n by A10,FUNCT_2:1; hence thesis by A42,A7,FUNCT_2:57; end; Lm5: for n,q being Nat, p being Permutation of Seg(n+1), F,H being FinSequence of ExtREAL st F=H*p & q in Seg(n+1) & len H = n+1 & not -infty in rng H & for i being Element of NAT st i in Seg(n+1) holds (iq implies p.i=i-1) holds Sum F = Sum H proof let n,q be Nat, p be Permutation of Seg(n+1), F,H be FinSequence of ExtREAL; assume that A1: F=H*p and A2: q in Seg(n+1) and A3: len H = n+1 and A4: not -infty in rng H and A5: for i being Element of NAT st i in Seg(n+1) holds (iq implies p.i=i-1); A6: 1 <= q by A2,FINSEQ_1:1; then q-1 >= 1-1 by XREAL_1:9; then A7: q-'1 = q-1 by XREAL_0:def 2; set H1 = H|n; A8: H1 = (H1|(q-'1))^(H1/^(q-'1)) by RFINSEQ:8; reconsider p9 = p as FinSequence of Seg(n+1) by FINSEQ_2:25; dom p = Seg(n+1) by FUNCT_2:def 1; then A9: len p9 = n+1 by FINSEQ_1:def 3; A10: q <= n+1 by A2,FINSEQ_1:1; then A11: q-'1 <= n+1-1 by A7,XREAL_1:9; A12: dom H = Seg(n+1) by A3,FINSEQ_1:def 3; then H is Function of Seg(n+1), ExtREAL by FINSEQ_2:26; then A13: len F = n+1 by A1,A9,FINSEQ_2:33; then A14: len(F/^q) = n+1-q by A10,RFINSEQ:def 1; A15: n <= n+1 by NAT_1:11; then A16: len(F|(q-'1)) = q-'1 by A11,A13,FINSEQ_1:59,XXREAL_0:2; A17: dom F = Seg(n+1) by A13,FINSEQ_1:def 3; A18: for i being Nat st 1 <= i & i <= q-'1 holds (F|(q-'1)).i=(H1|(q-'1)).i proof let i be Nat; assume that A19: 1 <= i and A20: i <= q-'1; A21: (F|(q-'1)).i = F.i by A20,FINSEQ_3:112; A22: H1.i = H.i by A11,A20,FINSEQ_3:112,XXREAL_0:2; A23: (H1|(q-'1)).i = H1.i by A20,FINSEQ_3:112; A24: i < q-'1+1 by A20,NAT_1:13; i <= n by A11,A20,XXREAL_0:2; then i <= n+1 by A15,XXREAL_0:2; then A25: i in Seg(n+1) by A19,FINSEQ_1:1; then F.i = H.(p.i) by A1,A17,FUNCT_1:12; hence thesis by A5,A7,A21,A23,A22,A25,A24; end; 0+n <= 1+n by XREAL_1:6; then A26: len H1 = n by A3,FINSEQ_1:59; then A27: len(H1|(q-'1)) = q-'1 by A11,FINSEQ_1:59; A28: len(H1/^(q-'1)) = n-(q-1) by A7,A11,A26,RFINSEQ:def 1; for i being Nat st 1 <= i & i <= n+1-q holds (F/^q).i=(H1/^(q-'1)).i proof reconsider n1 = n+1-q as Element of NAT by A10,INT_1:5; let i be Nat; assume that A29: 1 <= i and A30: i <= n+1-q; A31: i+q <= n+1 by A30,XREAL_1:19; A32: i in Seg n1 by A29,A30,FINSEQ_1:1; then i in dom(H1/^(q-'1)) by A28,FINSEQ_1:def 3; then A33: (H1/^(q-'1)).i = H1.(i+(q-'1)) by A11,A26,RFINSEQ:def 1; i+(q-'1) = i+q-1 by A7; then i+(q-'1) <= n by A31,XREAL_1:20; then A34: (H1/^(q-'1)).i = H.(i+q-1) by A7,A33,FINSEQ_3:112; A35: 1 <= i+q by A29,NAT_1:12; then i+q in dom F by A17,A31,FINSEQ_1:1; then A36: F.(i+q) = H.(p.(i+q)) by A1,FUNCT_1:12; dom(F/^q) = Seg n1 by A14,FINSEQ_1:def 3; then A37: (F/^q).i = F.(i+q) by A10,A13,A32,RFINSEQ:def 1; i+q >= 1+q by A29,XREAL_1:6; then A38: i+q>q by NAT_1:13; i+q in Seg(n+1) by A31,A35,FINSEQ_1:1; hence thesis by A5,A37,A34,A36,A38; end; then A39: F/^q = H1/^(q-'1) by A14,A28,FINSEQ_1:14; A40: F = (F|(q-'1))^<*F.q*>^(F/^q) by A6,A10,A13,FINSEQ_5:84; then A41: rng F = rng((F|(q-'1))^<*F.q*>) \/ rng(F/^q) by FINSEQ_1:31; p.q = n+1 by A2,A5; then A42: F.q = H.(n+1) by A1,A2,A17,FUNCT_1:12; A43: H1 = H | Seg n by FINSEQ_1:def 15; then rng H1 c= rng H by RELAT_1:70; then not -infty in rng H1 by A4; then A44: not -infty in rng(H1|(q-'1)) \/ rng(H1/^(q-'1)) by A8,FINSEQ_1:31; then A45: not -infty in rng(H1|(q-'1)) by XBOOLE_0:def 3; A46: not -infty in rng F by A1,A4,FUNCT_1:14; then A47: not -infty in rng((F|(q-'1))^<*F.q*>) by A41,XBOOLE_0:def 3; then A48: not -infty in rng(F|(q-'1)) \/ rng<*F.q*> by FINSEQ_1:31; then not -infty in rng(F|(q-'1)) by XBOOLE_0:def 3; then A49: Sum(F|(q-'1)) <> -infty by Lm2; not -infty in rng<*F.q*> by A48,XBOOLE_0:def 3; then not -infty in {F.q} by FINSEQ_1:39; then A50: -infty <> F.q by TARSKI:def 1; A51: not -infty in rng(F/^q) by A46,A41,XBOOLE_0:def 3; then A52: Sum(F/^q) <> -infty by Lm2; A53: H|(n+1) = H | Seg(n+1) by FINSEQ_1:def 15; H|(n+1) = H by A3,FINSEQ_1:58; then A54: H = H1^<*H.(n+1)*> by A12,A43,A53,FINSEQ_1:4,FINSEQ_5:10; A55: not -infty in rng(H1/^(q-'1)) by A44,XBOOLE_0:def 3; thus Sum F = Sum((F|(q-'1))^<*F.q*>) + Sum(F/^q) by A40,A47,A51,Th8 .= Sum(F|(q-'1)) + F.q + Sum(F/^q) by Lm1 .= Sum(F|(q-'1)) + Sum(F/^q) + F.q by A50,A49,A52,XXREAL_3:29 .= Sum(H1|(q-'1)) + Sum(H1/^(q-'1)) + H.(n+1) by A16,A27,A18,A42,A39, FINSEQ_1:14 .= Sum H1 + H.(n+1) by A8,A45,A55,Th8 .= Sum H by A54,Lm1; end; theorem for F,G being FinSequence of ExtREAL, s being Permutation of dom F st G = F*s & not -infty in rng F holds Sum(F) = Sum(G) proof let F,G be FinSequence of ExtREAL, s be Permutation of dom F; defpred P[Nat] means for F,G being FinSequence of ExtREAL, s being Permutation of Seg $1 st len F = $1 & G = F*s & not -infty in rng F holds Sum F = Sum G; A1: P[0] proof let F,G be FinSequence of ExtREAL, s be Permutation of Seg 0; assume that A2: len F = 0 and A3: G = F*s; F = <*> ExtREAL by A2; hence thesis by A3; end; A4: for n being non zero Nat st P[n] holds P[n+1] proof let n be non zero Nat; assume A5: P[n]; thus P[n+1] proof let F,G be FinSequence of ExtREAL, s be Permutation of Seg(n+1); assume that A6: len F = n+1 and A7: G = F*s and A8: not -infty in rng F; reconsider s9=s as FinSequence of Seg(n+1) by FINSEQ_2:25; A9: rng s = Seg(n+1) by FUNCT_2:def 3; A10: dom s = Seg(n+1) by FUNCT_2:def 1; then n+1 in dom s by FINSEQ_1:4; then A11: s.(n+1) in Seg(n+1) by A9,FUNCT_1:def 3; then reconsider q=s.(n+1) as Element of NAT; consider p being Permutation of Seg(n+1) such that A12: for i being Element of NAT st i in Seg(n+1) holds (iq implies p.i=i-1) by A11,Lm3; reconsider p2 = p" as FinSequence of Seg(n+1) by FINSEQ_2:25; A13: dom p = Seg(n+1) by FUNCT_2:def 1; p.q = n+1 by A11,A12; then A14: F.(s.(n+1)) = F.(p2.(n+1)) by A11,A13,FUNCT_1:34; A15: 0+n <= 1+n by XREAL_1:6; then A16: Seg n c= Seg(n+1) by FINSEQ_1:5; A17: dom F = Seg(n+1) by A6,FINSEQ_1:def 3; then A18: F is Function of Seg(n+1), ExtREAL by FINSEQ_2:26; then reconsider H = F*p2 as FinSequence of ExtREAL by FINSEQ_2:32; A19: H*p = F*(p2*p) by RELAT_1:36 .= F*(id Seg(n+1)) by A13,FUNCT_1:39 .= F by A17,RELAT_1:52; len s9 = n+1 by A10,FINSEQ_1:def 3; then A20: len G = n+1 by A7,A18,FINSEQ_2:33; then A21: dom G = Seg(n+1) by FINSEQ_1:def 3; then A22: G.(n+1) = F.(s.(n+1)) by A7,FINSEQ_1:4,FUNCT_1:12; reconsider p1 = p*s9|n as Permutation of Seg n by A12,Lm4; A23: dom p1 = Seg n by FUNCT_2:def 1; reconsider p19 = p1 as FinSequence of Seg n by FINSEQ_2:25; A24: not -infty in rng H by A8,FUNCT_1:14; dom p2 = rng p by FUNCT_1:33; then dom p2 = Seg(n+1) by FUNCT_2:def 3; then len p2 = n+1 by FINSEQ_1:def 3; then A25: len H = n+1 by A18,FINSEQ_2:33; then A26: dom H = Seg(n+1) by FINSEQ_1:def 3; A27: len(H|n) = n by A25,A15,FINSEQ_1:59; A28: G|n = (H|n)*p1 proof dom(H|n) = Seg n by A27,FINSEQ_1:def 3; then A29: H|n is Function of Seg n, ExtREAL by FINSEQ_2:26; then reconsider H1 = (H|n)*p19 as FinSequence of ExtREAL by FINSEQ_2:32 ; n in NAT by ORDINAL1:def 12; then len p19 = n by A23,FINSEQ_1:def 3; then A30: len H1 = n by A29,FINSEQ_2:33; A31: for i being Nat st 1 <= i & i <= n holds (G|n).i=((H|n)*p1).i proof let i be Nat; assume that A32: 1 <= i and A33: i <= n; A34: i in Seg n by A32,A33,FINSEQ_1:1; then A35: s.i in rng s by A10,A16,FUNCT_1:3; i in dom H1 by A30,A34,FINSEQ_1:def 3; then A36: ((H|n)*p1).i = (H|n).(p1.i) by FUNCT_1:12; rng p1 = Seg n by FUNCT_2:def 3; then A37: p1.i in Seg n by A23,A34,FUNCT_1:3; then reconsider a = p1.i as Element of NAT; a <= n by A37,FINSEQ_1:1; then A38: ((H|n)*p1).i = H.(p1.i) by A36,FINSEQ_3:112; (s9|n).i = s.i by A33,FINSEQ_3:112; then A39: p1.i = p.(s.i) by A23,A34,FUNCT_1:12; A40: (G|n).i = G.i by A33,FINSEQ_3:112; H.(p1.i) = F.(p2.(p1.i)) by A26,A16,A37,FUNCT_1:12; then ((H|n)*p1).i = F.(s.i) by A13,A39,A38,A35,FUNCT_1:34; hence thesis by A7,A21,A16,A40,A34,FUNCT_1:12; end; len(G|n) = n by A20,A15,FINSEQ_1:59; hence thesis by A30,A31,FINSEQ_1:14; end; G|n = G | Seg n by FINSEQ_1:def 15; then G = (G|n)^<*G.(n+1)*> by A20,FINSEQ_3:55; then A41: Sum G = Sum(G|n)+G.(n+1) by Lm1; A42: H|n = H | Seg n by FINSEQ_1:def 15; then H = (H|n)^<*H.(n+1)*> by A25,FINSEQ_3:55; then A43: Sum H = Sum(H|n)+H.(n+1) by Lm1; rng(H|n) c= rng H by A42,RELAT_1:70; then not -infty in rng (H|n) by A8,FUNCT_1:14; then A44: Sum(G|n) = Sum(H|n) by A5,A27,A28; H.(n+1) = F.(p2.(n+1)) by A26,FINSEQ_1:4,FUNCT_1:12; hence thesis by A11,A12,A25,A44,A14,A22,A41,A43,A24,A19,Lm5; end; end; A45: P[1] proof let F,G be FinSequence of ExtREAL, s be Permutation of Seg 1; assume that A46: len F = 1 and A47: G = F*s; reconsider s1 = s as FinSequence of Seg 1 by FINSEQ_2:25; dom s = Seg 1 by FUNCT_2:def 1; then A48: len s1 = 1 by FINSEQ_1:def 3; dom F = Seg 1 by A46,FINSEQ_1:def 3; then F is Function of Seg 1, ExtREAL by FINSEQ_2:26; then len G = 1 by A47,A48,FINSEQ_2:33; then A49: G = <*G.1*> by FINSEQ_1:40; then rng G = {G.1} by FINSEQ_1:39; then G.1 in rng G by TARSKI:def 1; then A50: G.1 in rng F by A47,FUNCT_1:14; A51: F = <*F.1*> by A46,FINSEQ_1:40; then rng F = {F.1} by FINSEQ_1:39; hence thesis by A51,A49,A50,TARSKI:def 1; end; A52: for n being non zero Nat holds P[n] from NAT_1:sch 10(A45,A4); len F = 0 or len F <> 0; then A53: P[len F] by A1,A52; assume that A54: G = F*s and A55: not -infty in rng F; dom F = Seg(len F) by FINSEQ_1:def 3; hence thesis by A53,A54,A55; end; reserve x,y,w,z for ExtReal, a for Real; begin :: Basic properties of absolute value for extended real numbers theorem Th1: x = a implies |.x.| = |.a qua Complex.| proof assume A1: x = a; reconsider x as R_eal by XXREAL_0:def 1; per cases; suppose 0 <= x; then |.x.| = a by A1,Def1; hence thesis by ABSVALUE:def 1; end; suppose A2: not 0 <= x; then |.x.| = -x by Def1 .= -a by A1,SUPINF_2:2; hence thesis by A1,A2,ABSVALUE:def 1; end; end; theorem |.x.| = x or |.x.| = -x by Def1; theorem 0 <= |.x.| proof reconsider x as R_eal by XXREAL_0:def 1; 0 <= |.x.|; hence thesis; end; theorem Th4: x <> 0 implies 0 < |.x.| proof assume A1: x <> 0; per cases; suppose 0 <= x; hence thesis by A1,Def1; end; suppose A2: not 0 <= x; then 0 < -x; hence thesis by A2,Def1; end; end; theorem x = 0 iff |.x.| = 0 by Th4,Def1; theorem |.x.| = -x & x <> 0 implies x < 0 proof reconsider x as R_eal by XXREAL_0:def 1; 0 <= |.x.|; hence thesis; end; theorem Th7: x <= 0 implies |.x.| = -x proof assume A1: x <= 0; per cases by A1; suppose x < 0; hence thesis by Def1; end; suppose A2: x = 0; then -0 = -x; hence thesis by A2,Def1; end; end; theorem |.x * y.| = |.x.| * |.y.| proof reconsider x,y as R_eal by XXREAL_0:def 1; per cases; suppose x = 0; then |.x.| = 0 & |.x * y.| = 0 by Def1; hence thesis; end; suppose A1: 0 < x; per cases; suppose y = 0; then |.y.| = 0 & |.x * y.| = 0 by Def1; hence thesis; end; suppose 0 < y; then A2: |.y.| = y by Def1; |.x.| = x by A1,Def1; hence thesis by A2,Def1; end; suppose A3: y < 0; then A4: |.y.| = -y by Def1; |.x.| = x by A1,Def1; then |.x.| * |.y.| = -(x * y) by A4,XXREAL_3:92; hence thesis by A1,A3,Def1; end; end; suppose A5: x < 0; per cases; suppose y = 0; then |.y.| = 0 & |.x * y.| = 0 by Def1; hence thesis; end; suppose A6: 0 < y; then |.y.| = y by Def1; then A7: |.x.| * |.y.| = (-x) * y by A5,Def1; |.x * y.| = -(x * y) by A5,A6,Def1; hence thesis by A7,XXREAL_3:92; end; suppose y < 0; then |.y.| = -y by Def1; then |.x.| * |.y.| = (-x) * (-y) by A5,Def1; then |.x.| * |.y.| = -(x * (-y)) by XXREAL_3:92 .= -(-(x * y)) by XXREAL_3:92; hence thesis by Def1; end; end; end; theorem Th9: -|.x.| <= x & x <= |.x.| proof reconsider x as R_eal by XXREAL_0:def 1; per cases; suppose A1: 0 <= x; thus thesis by A1,Def1; end; suppose not 0 <= x; then |.x.|=-x by Def1; hence thesis; end; end; theorem Th10: |.x.| < y implies -y < x & x < y proof assume A1: |.x.| < y; reconsider x,y as R_eal by XXREAL_0:def 1; A2: |.x.| < y by A1; per cases; suppose 0 <= x; hence thesis by A2,Def1; end; suppose A3: not 0 <= x; then |.x.|=-x by Def1; hence thesis by A1,A3,XXREAL_3:60; end; end; theorem Th11: -y < x & x < y implies 0 < y & |.x.| < y proof assume that A1: -y < x and A2: x < y; per cases; suppose 0 <= x; hence thesis by A2,Def1; end; suppose A3: not 0 <= x; -x < y by A1,XXREAL_3:60; hence thesis by A3,Def1; end; end; theorem Th12: -y <= x & x <= y iff |.x.| <= y proof A1: -y <= x & x <= y implies |.x.| <= y proof assume that A2: -y <= x and A3: x <= y; per cases; suppose 0 <= x; hence thesis by A3,Def1; end; suppose A4: not 0 <= x; -x <= y by A2,XXREAL_3:60; hence thesis by A4,Def1; end; end; |.x.| <= y implies -y <= x & x <= y proof assume A5: |.x.| <= y; per cases by A5,XXREAL_0:1; suppose |.x.| = y; hence thesis by Th9; end; suppose |.x.| < y; hence thesis by Th10; end; end; hence thesis by A1; end; theorem Th13: |.x + y.| <= |.x.| + |.y.| proof A1: -|.x.| <= x & -|.y.| <= y by Th9; A2: x <= |.x.| & y <= |.y.| by Th9; A3: -|.x.|-|.y.| = -(|.x.|+|.y.|) by XXREAL_3:25; x + y <= |.x.| + |.y.| & -|.x.|+(-|.y.|) <= x + y by A1,A2,XXREAL_3:36; hence thesis by A3,Th12; end; theorem Th14: -infty < x & x < +infty & x <> 0 implies |.x.|*|. 1. / x .| = 1. proof assume that A1: -infty < x & x < +infty and A2: x <> 0; reconsider a = x as Element of REAL by A1,XXREAL_0:14; A3: 1./x = 1/a; per cases; suppose 0 <= x; then |.x.| = a & |. 1./x .| = 1/a by Def1; then |.x.|*|. 1./x .| = a * (1/a) by XXREAL_3:def 5; hence thesis by A2,XCMPLX_1:106; end; suppose A4: not 0 <= x; then A5: |.x.| = -x by Def1 .= -a by SUPINF_2:2; |. 1./x .| = -(1./x) by A3,A4,Def1 .= -(1/a); then |.x.|*|. 1./x .| = (-a) * (-(1/a)) by A5,XXREAL_3:def 5 .= a * (1/a); hence thesis by A4,XCMPLX_1:106; end; end; theorem x = +infty or x = -infty implies |.x.|*|. 1./x .| = 0 proof assume x = +infty or x = -infty; then |. 1./x .| = 0 by Def1; hence thesis; end; theorem x <> 0 implies |. 1./x .| = 1./|.x.| proof assume A1: x <> 0; per cases; suppose A2: x = +infty; then |. 1./x .| = 0 by Def1; hence thesis by A2,Def1; end; suppose x = -infty; then |. 1./x .| = 0 & |.x.| = +infty by Def1,XXREAL_3:5; hence thesis; end; suppose A3: x <> +infty & x <> -infty; A4: 0 < |.x.| by A1,Th4; A5: x < +infty by A3,XXREAL_0:4; -infty <= x by XXREAL_0:5; then A6: -infty < x by A3,XXREAL_0:1; then -(+infty) < x by XXREAL_3:def 3; then A7: |.x.| < +infty by A5,Th11; |. 1./x .|*|.x.| = 1. by A1,A6,A5,Th14; hence thesis by A4,A7,XXREAL_3:88; end; end; theorem not((x=-infty or x=+infty) & (y=-infty or y=+infty)) & y<>0 implies |. x/y.| = |.x.|/|.y.| proof assume that A1: not((x=-infty or x=+infty) & (y=-infty or y=+infty)) and A2: y<>0; reconsider y as R_eal by XXREAL_0:def 1; per cases; suppose A3: x = +infty; A4: -infty < y by A1,A3,XXREAL_0:12,14; per cases by A2; suppose A5: 0 < y; then x / y = +infty by A3,A1,XXREAL_3:83; then A6: |.x/y.| = +infty by Def1; |.y.| = y by A5,Def1; hence thesis by A3,A1,A5,A6,XXREAL_3:83; end; suppose A7: y < 0; then |.y.| = -y by Def1; then A8: |.y.| < +infty by A4,XXREAL_3:5,38; x / y = -infty by A3,A1,A7,XXREAL_3:85; then |.x/y.| = +infty by Def1,XXREAL_3:5; hence thesis by A8,A2,A3,Th4,XXREAL_3:83; end; end; suppose A9: x = -infty; A10: -infty < y by A1,A9,XXREAL_0:12,14; per cases by A2; suppose A11: 0 < y; then A12: x / y = -infty by A9,A1,XXREAL_3:86; A13: |.x.| = +infty by A9,Def1,XXREAL_3:5; |.y.| = y by A11,Def1; hence thesis by A9,A1,A11,A12,A13,XXREAL_3:83; end; suppose A14: y < 0; then |.y.| = -y by Def1; then A15: |.y.| < +infty by A10,XXREAL_3:5,38; A16: x / y = +infty by A9,A1,A14,XXREAL_3:84; 0 < |.y.| & |.x.| = +infty by A2,A9,Th4,Def1,XXREAL_3:5; hence thesis by A15,A16,XXREAL_3:83; end; end; suppose x <> +infty & x <> -infty; then reconsider a = x as Element of REAL by XXREAL_0:14; per cases; suppose y = +infty; then |.x/y.| = 0 & |.y.| = +infty by Def1; hence thesis; end; suppose y = -infty; then |.x/y.| = 0 & |.y.| = +infty by Def1,XXREAL_3:5; hence thesis; end; suppose y <> +infty & y <> -infty; then reconsider b = y as Element of REAL by XXREAL_0:14; |.x.| = |.a qua Complex.| & |.y.| = |.b qua Complex.| by Th1; then A17: |.x.|/|.y.| = |.a qua Complex.|/|.b qua Complex.|; |.x/y.| = |.a/b qua Complex.| by Th1; hence thesis by A17,COMPLEX1:67; end; end; end; theorem Th18: |.x.| = |.-x.| proof reconsider x as R_eal by XXREAL_0:def 1; per cases; suppose 0 < x; then |.-x.| = -(-x) by Def1 .= x; hence thesis; end; suppose x < 0; then |.x.| = -x by Def1; hence thesis; end; suppose x = 0; hence thesis; end; end; theorem Th19: |.+infty.| = +infty & |.-infty.| = +infty proof thus |.+infty.| = +infty by Def1; --infty = +infty by XXREAL_3:23; hence thesis by Def1; end; theorem Th20: x is Real or y is Real implies |.x.|-|.y.| <= |.x-y.| proof assume A1: x is Real or y is Real; reconsider x,y as R_eal by XXREAL_0:def 1; per cases by A1; suppose y is Real; then (x - y) + y = x by XXREAL_3:22; then |.x.| <= |.x-y.| + |.y.| by Th13; hence thesis by XXREAL_3:42; end; suppose x is Real; then reconsider a = x as Real; A2: |.x.| = |.a.|; per cases; suppose A3: y = +infty or y = -infty; |.y.| = +infty by Th19,A3; then |.x.| - |.y.| = -infty by A2,XXREAL_3:13; then |.x.|-|.y.| <= |.x-y.|; hence thesis; end; suppose y <> +infty & y <> -infty; then reconsider b = y as Element of REAL by XXREAL_0:14; x - y = a - b by SUPINF_2:3; then A4: |.x-y.| = |.a-b qua Complex.| by Th1; |.y.| = |.b qua Complex.| by Th1; then |.x.|-|.y.| = |.a qua Complex.|-|.b qua Complex.| by A2,SUPINF_2:3; hence thesis by A4,COMPLEX1:59; end; end; end; theorem |.x-y.| <= |.x.| + |.y.| proof reconsider x,y as R_eal by XXREAL_0:def 1; per cases; suppose x = +infty or x = -infty; then |.x.| + |.y.| = +infty by Th19,XXREAL_3:def 2; hence thesis by XXREAL_0:3; end; suppose A1: x <> +infty & x <> -infty; then reconsider a = x as Element of REAL by XXREAL_0:14; per cases; suppose A2: y = +infty; x - y = -infty by A1,A2,XXREAL_3:13; hence thesis by A2,Th19,XXREAL_3:def 2; end; suppose A3: y = -infty; x - y = +infty by A1,A3,XXREAL_3:14; hence thesis by A3,Th19,XXREAL_3:def 2; end; suppose y <> +infty & y <> -infty; then reconsider b = y as Element of REAL by XXREAL_0:14; |.x.|=|.a qua Complex.| & |.y.|=|.b qua Complex.| by Th1; then A4: |.x.|+|.y.|=|.a qua Complex.|+|.b qua Complex.| by SUPINF_2:1; x - y = a - b by SUPINF_2:3; then |.x-y.| = |.a-b qua Complex.| by Th1; hence thesis by A4,COMPLEX1:57; end; end; end; ::$CT theorem |.x.| <= z & |.y.| <= w implies |.x+y.| <= z + w proof assume A1: |.x.| <= z & |.y.| <= w; then -z <= x & -w <= y by Th12; then A2: -z + -w <= x + y by XXREAL_3:36; x <= z & y <= w by A1,Th12; then A3: x + y <= z + w by XXREAL_3:36; -z -w = -(z + w) by XXREAL_3:25; hence thesis by A3,A2,Th12; end; theorem x is Real or y is Real implies |.|.x.|-|.y.|.| <= |.x-y.| proof A1: |.y.|-|.x.| = -(|.x.|-|.y.|) by XXREAL_3:26; assume A2: x is Real or y is Real; then A3: |.x.|-|.y.| <= |.x-y.| by Th20; y - x = -(x - y) by XXREAL_3:26; then A4: |.y-x.| = |.x-y.| by Th18; |.y.|-|.x.| <= |.y-x.| by A2,Th20; then -|.x-y.| <= -(-(|.x.|-|.y.|)) by A4,A1,XXREAL_3:38; hence thesis by A3,Th12; end; theorem 0 <= x * y implies |.x+y.| = |.x.|+|.y.| proof assume A1: 0 <= x * y; per cases by A1; suppose (0 <= x or 0 < x) & (0 <= y or 0 < y); then |.x.| = x & |.y.| = y by Def1; hence thesis by Def1; end; suppose A2: (x <= 0 or x < 0) & (y <= 0 or y < 0); then A3: |.x+y.| = -(x + y) by Th7 .= -x -y by XXREAL_3:25; |.x.| = -x by A2,Th7; hence thesis by A2,A3,Th7; end; end; begin theorem x <> +infty & y <> +infty & not ( x = +infty & y = +infty or x = -infty & y = -infty ) implies min(x,y) = (x + y - |.x - y.|) / 2 proof assume that A1: x <> +infty and A2: y <> +infty and A3: not ( x = +infty & y = +infty or x = -infty & y = -infty ); per cases; suppose A4: x = -infty; then x + y = -infty & x - y = -infty by A2,A3,XXREAL_3:14,def 2; then A5: x + y - |.x - y.| = -infty by XXREAL_3:14; A6: min(x,y) = -infty by A4,XXREAL_0:44; thus thesis by A6,A5,XXREAL_3:86; end; suppose x <> -infty; then reconsider a = x as Element of REAL by A1,XXREAL_0:14; per cases; suppose A7: y = -infty; then x + y = -infty & x - y = +infty by A1,A3,XXREAL_3:14,def 2; then A8: x + y - |.x - y.| = -infty by XXREAL_3:14; A9: min(x,y) = -infty by A7,XXREAL_0:44; thus thesis by A9,A8,XXREAL_3:86; end; suppose y <> -infty; then reconsider b = y as Element of REAL by A2,XXREAL_0:14; x - y = a - b by SUPINF_2:3; then x + y = a + b & |.x - y.| = |.a-b.| by SUPINF_2:1; then A10: x + y - |.x - y.| = a + b - |.a-b qua Complex.| by SUPINF_2:3; (x + y - |.x - y.|) / 2 = (a+b-|.a-b qua Complex.|)/2 by A10; hence thesis by COMPLEX1:73; end; end; end; theorem x <> -infty & y <> -infty & not ( x = +infty & y = +infty or x = -infty & y = -infty ) implies max(x,y) = (x + y + |.x - y.|) / 2 proof assume that A1: x <> -infty and A2: y <> -infty and A3: not ( x = +infty & y = +infty or x = -infty & y = -infty ); per cases; suppose A4: x = +infty; then x + y = +infty & x - y = +infty by A2,A3,XXREAL_3:13,def 2; then A5: x + y + |.x - y.| = +infty by XXREAL_3:def 2; A6: max(x,y) = +infty by A4,XXREAL_0:41; thus thesis by A6,A5,XXREAL_3:83; end; suppose x <> +infty; then reconsider a = x as Element of REAL by A1,XXREAL_0:14; per cases; suppose A7: y = +infty; then x + y = +infty & x - y = -infty by A1,A3,XXREAL_3:13,def 2; then A8: x + y + |.x - y.| = +infty by XXREAL_3:def 2; A9: max(x,y) = +infty by A7,XXREAL_0:41; thus thesis by A9,A8,XXREAL_3:83; end; suppose y <> +infty; then reconsider b = y as Element of REAL by A2,XXREAL_0:14; x - y = a - b by SUPINF_2:3; then x + y = a + b & |.x - y.| = |.a-b.| by SUPINF_2:1; then A10: x + y + |.x - y.| = a + b + |.a-b qua Complex.| by SUPINF_2:1; (x + y + |.x - y.|) / 2 = (a+b+|.a-b qua Complex.|)/2 by A10; hence thesis by COMPLEX1:74; end; end; end; definition let x,y be R_eal; redefine func max(x,y) -> R_eal; coherence by XXREAL_0:def 1; redefine func min(x,y) -> R_eal; coherence by XXREAL_0:def 1; end; theorem min(x,y) + max(x,y)= x + y proof per cases; suppose A1: x <= y; then min(x,y) = x by XXREAL_0:def 9; hence thesis by A1,XXREAL_0:def 10; end; suppose A2: not x <= y; then min(x,y) = y by XXREAL_0:def 9; hence thesis by A2,XXREAL_0:def 10; end; end; begin ::Addenda :: missing, 2007.07.20, A.T. theorem Th28: |.x.| = +infty implies x = +infty or x = -infty proof A1: |.x.| = x or -|.x.| = --x by Def1; assume |.x.| = +infty; hence thesis by A1,XXREAL_3:5; end; theorem |.x.| < +infty iff x in REAL by Th19,Th28,XXREAL_0:4,14;