let n be Element of NAT ; :: thesis: for x being Element of REAL n st n >= 2 & x <> 0* n holds
ex y being Element of REAL n st
for r being Real holds
( not y = r * x & not x = r * y )
let x be Element of REAL n; :: thesis: ( n >= 2 & x <> 0* n implies ex y being Element of REAL n st
for r being Real holds
( not y = r * x & not x = r * y ) )
assume A1:
( n >= 2 & x <> 0* n )
; :: thesis: ex y being Element of REAL n st
for r being Real holds
( not y = r * x & not x = r * y )
reconsider f = x as FinSequence of REAL ;
consider i2 being Element of NAT such that
A2:
( 1 <= i2 & i2 <= n & f . i2 <> 0 )
by A1, Th54;
A3:
len f = n
by FINSEQ_1:def 18;
then A4:
1 <= len f
by A1, XXREAL_0:2;
per cases
( i2 > 1 or i2 <= 1 )
;
suppose A5:
i2 > 1
;
:: thesis: ex y being Element of REAL n st
for r being Real holds
( not y = r * x & not x = r * y )reconsider g =
<*((f /. 1) + 1)*> ^ (mid f,2,(len f)) as
FinSequence of
REAL ;
A6:
len g = (len <*((f /. 1) + 1)*>) + (len (mid f,2,(len f)))
by FINSEQ_1:35;
A7:
len <*((f /. 1) + 1)*> = 1
by FINSEQ_1:56;
A8:
len (mid f,2,(len f)) =
((len f) -' 2) + 1
by A1, A3, A4, JORDAN3:27
.=
((len f) - 2) + 1
by A1, A3, XREAL_1:235
;
then A9:
len g =
1
+ (((len f) - 2) + 1)
by A6, FINSEQ_1:56
.=
len f
;
then reconsider y2 =
g as
Element of
REAL n by A3, Th52;
now given r being
Real such that A10:
(
y2 = r * x or
x = r * y2 )
;
:: thesis: contradictionper cases
( y2 = r * x or x = r * y2 )
by A10;
suppose A11:
y2 = r * x
;
:: thesis: contradictionA12:
g /. i2 = g . i2
by A2, A3, A9, FINSEQ_4:24;
A13:
f /. i2 = f . i2
by A2, A3, FINSEQ_4:24;
A14:
1
<= len f
by A1, A3, XXREAL_0:2;
A15:
i2 -' 1
= i2 - 1
by A2, XREAL_1:235;
A16:
1
<= i2 -' 1
by A5, NAT_D:49;
i2 <= ((len f) - (1 + 1)) + (1 + 1)
by A2, FINSEQ_1:def 18;
then A17:
i2 - 1
<= ((((len f) - (1 + 1)) + 1) + 1) - 1
by XREAL_1:11;
A18:
((i2 -' 1) + 2) -' 1 =
(((i2 -' 1) + 1) + 1) -' 1
.=
(i2 -' 1) + 1
by NAT_D:34
.=
(i2 - 1) + 1
by A2, XREAL_1:235
.=
i2
;
( 1
+ 1
<= i2 &
i2 <= 1
+ (len (mid f,2,(len f))) )
by A2, A5, A8, FINSEQ_1:def 18, NAT_1:13;
then g . i2 =
(mid f,2,(len f)) . (i2 - 1)
by A7, FINSEQ_1:36
.=
f . i2
by A1, A3, A8, A14, A15, A16, A17, A18, JORDAN3:27
;
then
1
* (f /. i2) = r * (f /. i2)
by A2, A3, A11, A12, A13, Th53;
then A19:
1
= r
by A2, A13, XCMPLX_1:5;
A20:
g /. 1
= r * (f /. 1)
by A11, A14, Th53;
g /. 1
= g . 1
by A9, A14, FINSEQ_4:24;
then
(f /. 1) + 1
= 1
* (f /. 1)
by A19, A20, FINSEQ_1:58;
hence
contradiction
;
:: thesis: verum end; suppose A21:
x = r * y2
;
:: thesis: contradictionA22:
g /. i2 = g . i2
by A2, A3, A9, FINSEQ_4:24;
A23:
f /. i2 = f . i2
by A2, A3, FINSEQ_4:24;
A24:
1
<= len f
by A1, A3, XXREAL_0:2;
A25:
i2 -' 1
= i2 - 1
by A2, XREAL_1:235;
A26:
1
<= i2 -' 1
by A5, NAT_D:49;
i2 <= ((len f) - (1 + 1)) + (1 + 1)
by A2, FINSEQ_1:def 18;
then A27:
i2 - 1
<= ((((len f) - (1 + 1)) + 1) + 1) - 1
by XREAL_1:11;
A28:
((i2 -' 1) + 2) -' 1 =
(((i2 -' 1) + 1) + 1) -' 1
.=
(i2 -' 1) + 1
by NAT_D:34
.=
(i2 - 1) + 1
by A2, XREAL_1:235
.=
i2
;
( 1
+ 1
<= i2 &
i2 <= 1
+ (len (mid f,2,(len f))) )
by A2, A5, A8, FINSEQ_1:def 18, NAT_1:13;
then g . i2 =
(mid f,2,(len f)) . (i2 - 1)
by A7, FINSEQ_1:36
.=
f . i2
by A1, A3, A8, A24, A25, A26, A27, A28, JORDAN3:27
;
then
1
* (f /. i2) = r * (f /. i2)
by A2, A3, A9, A21, A22, A23, Th53;
then A29:
1
= r
by A2, A23, XCMPLX_1:5;
A30:
f /. 1
= r * (g /. 1)
by A9, A21, A24, Th53;
g /. 1
= g . 1
by A9, A24, FINSEQ_4:24;
then
(f /. 1) + 1
= 1
* (f /. 1)
by A29, A30, FINSEQ_1:58;
hence
contradiction
;
:: thesis: verum end; end; hence
ex
y being
Element of
REAL n st
for
r being
Real holds
( not
y = r * x & not
x = r * y )
;
:: thesis: verum end; suppose
i2 <= 1
;
:: thesis: ex y being Element of REAL n st
for r being Real holds
( not y = r * x & not x = r * y )then A31:
i2 = 1
by A2, XXREAL_0:1;
reconsider g =
(mid f,1,((len f) -' 1)) ^ <*((f /. (len f)) + 1)*> as
FinSequence of
REAL ;
A32:
len <*((f /. (len f)) + 1)*> = 1
by FINSEQ_1:56;
A33:
(len f) -' 1
= (len f) - 1
by A1, A3, XREAL_1:235, XXREAL_0:2;
A34:
(len f) -' 1
<= len f
by NAT_D:44;
A35:
(1 + 1) - 1
<= (len f) - 1
by A1, A3, XREAL_1:11;
then A36:
(((len f) -' 1) -' 1) + 1 =
(((len f) - 1) - 1) + 1
by A33, XREAL_1:235
.=
((len f) - (1 + 1)) + 1
;
then A37:
len (mid f,1,((len f) -' 1)) = ((len f) - 2) + 1
by A4, A33, A34, A35, JORDAN3:27;
A38:
len (mid f,1,((len f) -' 1)) = (len f) - 1
by A4, A33, A34, A35, A36, JORDAN3:27;
A39:
len g =
(((len f) - 2) + 1) + 1
by A32, A37, FINSEQ_1:35
.=
len f
;
then reconsider y2 =
g as
Element of
REAL n by A3, Th52;
now given r being
Real such that A40:
(
y2 = r * x or
x = r * y2 )
;
:: thesis: contradictionper cases
( y2 = r * x or x = r * y2 )
by A40;
suppose A41:
y2 = r * x
;
:: thesis: contradictionA42:
g /. i2 = g . i2
by A2, A3, A39, FINSEQ_4:24;
A43:
f /. i2 = f . i2
by A2, A3, FINSEQ_4:24;
A44:
1
<= len f
by A1, A3, XXREAL_0:2;
g . i2 =
(mid f,1,((len f) -' 1)) . i2
by A31, A35, A38, JORDAN3:17
.=
f . i2
by A31, A33, A34, A35, JORDAN3:32
;
then
1
* (f /. i2) = r * (f /. i2)
by A2, A3, A41, A42, A43, Th53;
then A45:
1
= r
by A2, A43, XCMPLX_1:5;
A46:
g /. (len f) = r * (f /. (len f))
by A41, A44, Th53;
A47:
g /. (len f) = g . (len f)
by A39, A44, FINSEQ_4:24;
g . (len f) =
g . (((len f) - 1) + 1)
.=
(f /. (len f)) + 1
by A38, FINSEQ_1:59
;
hence
contradiction
by A45, A46, A47;
:: thesis: verum end; suppose A48:
x = r * y2
;
:: thesis: contradictionA49:
g /. i2 = g . i2
by A2, A3, A39, FINSEQ_4:24;
A50:
f /. i2 = f . i2
by A2, A3, FINSEQ_4:24;
A51:
1
<= len f
by A1, A3, XXREAL_0:2;
g . i2 =
(mid f,1,((len f) -' 1)) . i2
by A31, A35, A38, JORDAN3:17
.=
f . i2
by A31, A33, A34, A35, JORDAN3:32
;
then
1
* (f /. i2) = r * (f /. i2)
by A2, A3, A39, A48, A49, A50, Th53;
then A52:
1
= r
by A2, A50, XCMPLX_1:5;
A53:
f /. (len f) = r * (g /. (len f))
by A39, A48, A51, Th53;
A54:
g /. (len f) = g . (len f)
by A39, A51, FINSEQ_4:24;
g . (len f) =
g . (((len f) - 1) + 1)
.=
(f /. (len f)) + 1
by A38, FINSEQ_1:59
;
hence
contradiction
by A52, A53, A54;
:: thesis: verum end; end; hence
ex
y being
Element of
REAL n st
for
r being
Real holds
( not
y = r * x & not
x = r * y )
;
:: thesis: verum end;