deffunc H1( non zero Nat) -> Element of NAT = (Product (SqFactors $1)) |^ 2;
deffunc H2( non zero Nat) -> Element of NAT = Product (SqFactors $1);
deffunc H3( non zero Nat) -> set = SqFactors $1;
deffunc H4( non zero Nat) -> Element of NAT = Product (TSqFactors $1);
defpred S1[ Nat] means for n being non zero Nat st support H3(n) c= Seg $1 holds
H1(n) = H4(n);
let n be non zero Nat; (SqF n) |^ 2 = TSqF n
A1:
ex mS being Element of NAT st support (ppf n) c= Seg mS
by MOEBIUS1:14;
A2: support (ppf n) =
support (pfexp n)
by NAT_3:def 9
.=
support H3(n)
by MOEBIUS2:def 3
;
A3:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A4:
S1[
k]
;
S1[k + 1]
let n be non
zero Nat;
( support H3(n) c= Seg (k + 1) implies H1(n) = H4(n) )
assume A5:
support H3(
n)
c= Seg (k + 1)
;
H1(n) = H4(n)
A6:
support (pfexp n) = support H3(
n)
by MOEBIUS2:def 3;
per cases
( not support H3(n) c= Seg k or support H3(n) c= Seg k )
;
suppose A7:
not
support H3(
n)
c= Seg k
;
H1(n) = H4(n)set p =
k + 1;
set e =
(k + 1) |-count n;
set s =
(k + 1) |^ ((k + 1) |-count n);
then A12:
k + 1 is
Prime
by A6, NAT_3:34;
then A13:
k + 1
> 1
by INT_2:def 4;
then
(k + 1) |^ ((k + 1) |-count n) divides n
by NAT_3:def 7;
then consider t being
Nat such that A14:
n = ((k + 1) |^ ((k + 1) |-count n)) * t
;
reconsider s =
(k + 1) |^ ((k + 1) |-count n),
t =
t as non
zero Nat by A14;
consider f being
FinSequence of
COMPLEX such that A15:
Product H3(
s)
= Product f
and A16:
f = H3(
s)
* (canFS (support H3(s)))
by NAT_3:def 5;
A17:
dom H3(
s)
= SetPrimes
by PARTFUN1:def 2;
A18:
support (ppf s) = support (pfexp s)
by NAT_3:def 9;
then A19:
support (ppf s) = support H3(
s)
by MOEBIUS2:def 3;
(pfexp n) . (k + 1) = (k + 1) |-count n
by A12, NAT_3:def 8;
then
(k + 1) |-count n <> 0
by A6, A8, PRE_POLY:def 7;
then A21:
support (ppf s) = {(k + 1)}
by A12, A18, NAT_3:42;
then A22:
k + 1
in support (pfexp s)
by A18, TARSKI:def 1;
A23:
support H3(
t)
c= Seg k
then A31:
H1(
t)
= H4(
t)
by A4;
a21:
support H3(
s)
= {(k + 1)}
by A18, A21, MOEBIUS2:def 3;
Aa1:
support (TSqFactors s) = {(k + 1)}
by A18, A21, MOEBIUS2:def 8;
f =
H3(
s)
* <*(k + 1)*>
by A16, FINSEQ_1:94, a21
.=
<*(H3(s) . (k + 1))*>
by FINSEQ_2:34, A17, A8
;
then Product H3(
s) =
H3(
s)
. (k + 1)
by A15, RVSUM_1:95
.=
(k + 1) |^ (((k + 1) |-count s) div 2)
by A22, MOEBIUS2:def 3
;
then aa1:
(Product H3(s)) |^ 2 =
(k + 1) |^ (2 * (((k + 1) |-count s) div 2))
by NEWTON:9
.=
(TSqFactors s) . (k + 1)
by A22, MOEBIUS2:def 8
.=
Product (TSqFactors s)
by A12, KeyValue, Aa1
;
set j =
(k + 1) |-count s;
reconsider s1 =
s,
t1 =
t as non
zero Element of
NAT by ORDINAL1:def 12;
support (ppf t) = support (pfexp t)
by NAT_3:def 9;
then A33:
support (ppf t) = support H3(
t)
by MOEBIUS2:def 3;
ZZ:
s1,
t1 are_coprime
proof
set u =
s1 gcd t1;
A38:
s1 gcd t1 divides t1
by NAT_D:def 5;
A39:
0 + 1
<= s1 gcd t1
by NAT_1:13;
assume
not
s1,
t1 are_coprime
;
contradiction
then
s1 gcd t1 > 1
by A39, XXREAL_0:1;
then
s1 gcd t1 >= 1
+ 1
by NAT_1:13;
then consider r being
Element of
NAT such that A40:
r is
prime
and A41:
r divides s1 gcd t1
by INT_2:31;
s1 gcd t1 divides s1
by NAT_D:def 5;
then
r divides s1
by A41, NAT_D:4;
then
(
r = 1 or
r = k + 1 )
by A12, INT_2:def 4, A40, NAT_3:5;
then
k + 1
in support (pfexp t)
by NAT_3:37, A40, A41, A38, NAT_D:4;
then
k + 1
in support H3(
t)
by MOEBIUS2:def 3;
then
k + 1
<= k
by A23, FINSEQ_1:1;
hence
contradiction
by NAT_1:13;
verum
end;
(
support (TSqFactors s) = support (pfexp s) &
support (TSqFactors t) = support (pfexp t) )
by MOEBIUS2:def 8;
then za:
(
support (TSqFactors s) = support (ppf s) &
support (TSqFactors t) = support (ppf t) )
by NAT_3:def 9;
H1(
n) =
(Product (H3(s) + H3(t))) |^ 2
by A14, MOEBIUS2:44, ZZ
.=
(H2(s) * H2(t)) |^ 2
by A34, A19, A33, NAT_3:19
.=
(H2(s) |^ 2) * (H2(t) |^ 2)
by NEWTON:7
.=
Product ((TSqFactors s) + (TSqFactors t))
by za, NAT_3:19, aa1, A31, A34
.=
H4(
n)
by A14, ZZ, MOEBIUS2:52
;
hence
H1(
n)
= H4(
n)
;
verum end; end;
end;
A42:
S1[ 0 ]
for k being Nat holds S1[k]
from NAT_1:sch 2(A42, A3);
hence
(SqF n) |^ 2 = TSqF n
by A1, A2; verum