defpred S₁[ Nat] means ex f being non-empty increasing FinSequence of NAT st
( dom f = Seg ($1 + 1) & ( for i being Nat st i in dom f holds
f . i is triangular ) & f is with_all_coprime_terms );
A1: S₁[ 0 ]

proof

set f = (Seg 1) --> 1;
reconsider f = (Seg 1) --> 1 as increasing FinSequence of NAT by IncFinNAT;
G1: dom f = Seg (0 + 1) by FUNCOP_1:13;
g1: dom f = {1} by FINSEQ_1:2, FUNCOP_1:13;
GG: for i being Nat st i in dom f holds
f . i is triangular by NUMPOLY1:def 2, NUMPOLY1:11, FUNCOP_1:7, G1;
for n being object st n in dom f holds
not f . n is empty by FUNCOP_1:7, G1;
then JH: f is non-empty by FUNCT_1:def 9;
for i, j being Nat st i in dom f & j in dom f & i <> j holds
f . i,f . j are_coprime

proof

let i, j be Nat; :: thesis: ( i in dom f & j in dom f & i <> j implies f . i,f . j are_coprime )
assume H1: ( i in dom f & j in dom f & i <> j ) ; :: thesis: f . i,f . j are_coprime
then ( i = 1 & j = 1 ) by g1, TARSKI:def 1;
hence f . i,f . j are_coprime by H1; :: thesis: verum

end;

then f is with_all_coprime_terms by INT_6:def 2;
hence S₁[ 0 ] by FUNCOP_1:13, GG, JH; :: thesis: verum

end;

A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
then consider f being non-empty increasing FinSequence of NAT such that
B1: ( dom f = Seg (k + 1) & ( for i being Nat st i in dom f holds
f . i is triangular ) & f is with_all_coprime_terms ) ;
reconsider ff = f as FinSequence of NAT ;
J1: len ff = k + 1 by B1, FINSEQ_1:def 3;
set a = Product ff;
reconsider a = Product ff as Nat ;
G1: a,a + 1 are_coprime ;
G2: a,(2 * a) + 1 are_coprime by Coprime21;
reconsider T = (((2 * a) + 1) * (((2 * a) + 1) + 1)) / 2 as Element of NAT by ORDINAL1:def 12;
we: ex k being Nat st T = Triangle k

proof

take k = (2 * a) + 1; :: thesis: T = Triangle k
thus T = Triangle k by NUMPOLY1:19; :: thesis: verum

end;

J2: ((2 * a) + 1) * (a + 1) = T ;
for i being Nat holds
( not i in dom ff or not ff . i = 0 ) by FUNCT_1:def 9;
then WC: Product ff <> 0 by RVSUM_1:103;
k + 1 >= 1 by NAT_1:12;
then f . (k + 1) divides a by B1, INT_4:32, FINSEQ_1:1;
then WV: f . (k + 1) <= a by WC, NAT_D:7;
1 * (a + 1) < T by J2, WC, NAT_1:16, XREAL_1:68;
then a < T by NAT_1:16, XXREAL_0:2;
then ZO: T > f . (k + 1) by WV, XXREAL_0:2;
cd: ((2 * a) + 1) * (a + 1),a are_coprime by WC, G1, G2, EULER_1:14;
set fg = ff ^ <*T*>;
C1: dom (ff ^ <*T*>) = Seg ((len ff) + (len <*T*>)) by FINSEQ_1:def 7
.= Seg ((k + 1) + 1) by J1, FINSEQ_1:39 ;
for i being Nat st i in dom ff holds
ff . i < T

proof

let i be Nat; :: thesis: ( i in dom ff implies ff . i < T )
assume ZP: i in dom ff ; :: thesis: ff . i < T
1 <= k + 1 by NAT_1:12;
then ZR: k + 1 in dom ff by B1;
i <= k + 1 by ZP, B1, FINSEQ_1:1;
then ff . i <= f . (k + 1) by ZP, ZR, SEQM_3:def 3;
hence ff . i < T by ZO, XXREAL_0:2; :: thesis: verum

end;

then reconsider fg = ff ^ <*T*> as increasing FinSequence of NAT by ConcatIsIncreasing;
v1: Seg ((k + 1) + 1) = (Seg (k + 1)) \/ {((k + 1) + 1)} by FINSEQ_1:9;
GD: fg . 1 <> 0

proof

assume F1: fg . 1 = 0 ; :: thesis: contradiction
f2: 1 <= k + 1 by NAT_1:12;
then 1 in dom ff by B1;
then fg . 1 = ff . 1 by FINSEQ_1:def 7;
hence contradiction by F1, f2, FUNCT_1:def 9, B1, FINSEQ_1:1; :: thesis: verum

end;

T1: for i being Nat st i in dom fg holds
( fg . i is triangular & not fg . i is empty )

proof

let i be Nat; :: thesis: ( i in dom fg implies ( fg . i is triangular & not fg . i is empty ) )
assume WR: i in dom fg ; :: thesis: ( fg . i is triangular & not fg . i is empty )
then i in (Seg (k + 1)) \/ {((k + 1) + 1)} by C1, FINSEQ_1:9;

per cases then ( i in Seg (k + 1) or i in {((k + 1) + 1)} ) by XBOOLE_0:def 3;

suppose U1: i in Seg (k + 1) ; :: thesis: ( fg . i is triangular & not fg . i is empty )

then KK: fg . i = ff . i by B1, FINSEQ_1:def 7;
1 <= (k + 1) + 1 by NAT_1:12;
then SE: 1 in dom fg by C1;
1 <= i by U1, FINSEQ_1:1;
hence ( fg . i is triangular & not fg . i is empty ) by U1, B1, KK, GD, WR, SE, SEQM_3:def 3; :: thesis: verum

end;

suppose i in {((k + 1) + 1)} ; :: thesis: ( fg . i is triangular & not fg . i is empty )

then i = (k + 1) + 1 by TARSKI:def 1;
hence ( fg . i is triangular & not fg . i is empty ) by we, J1, NUMPOLY1:def 2; :: thesis: verum

end;

end;

end;

for i being object st i in dom fg holds
not fg . i is empty by T1;
then reconsider fg = fg as non-empty increasing FinSequence of NAT by FUNCT_1:def 9;
for i, j being Nat st i in dom fg & j in dom fg & i <> j holds
fg . i,fg . j are_coprime

proof

let i, j be Nat; :: thesis: ( i in dom fg & j in dom fg & i <> j implies fg . i,fg . j are_coprime )
assume Z1: ( i in dom fg & j in dom fg & i <> j ) ; :: thesis: fg . i,fg . j are_coprime

per cases ( ( i in dom ff & j in dom ff ) or ( i in dom ff & not j in dom ff ) or ( not i in dom ff & j in dom ff ) or ( not i in dom ff & not j in dom ff ) ) ;

suppose Z2: ( i in dom ff & j in dom ff ) ; :: thesis: fg . i,fg . j are_coprime

then ( ff . i = fg . i & ff . j = fg . j ) by FINSEQ_1:def 7;
hence fg . i,fg . j are_coprime by B1, Z1, Z2, INT_6:def 2; :: thesis: verum

end;

suppose Z2: ( i in dom ff & not j in dom ff ) ; :: thesis: fg . i,fg . j are_coprime

then ( i in Seg (k + 1) & j in {((k + 1) + 1)} ) by B1, v1, Z1, C1, XBOOLE_0:def 3;
then Y9: j = (len ff) + 1 by J1, TARSKI:def 1;
ff . i,T are_coprime by cd, CoprimeDivides, Z2, INT_4:32;
hence fg . i,fg . j are_coprime by Y9, Z2, FINSEQ_1:def 7; :: thesis: verum

end;

suppose Z2: ( not i in dom ff & j in dom ff ) ; :: thesis: fg . i,fg . j are_coprime

then ( j in Seg (k + 1) & i in {((k + 1) + 1)} ) by B1, v1, Z1, C1, XBOOLE_0:def 3;
then Y1: i = (len ff) + 1 by J1, TARSKI:def 1;
ff . j,T are_coprime by cd, CoprimeDivides, Z2, INT_4:32;
hence fg . i,fg . j are_coprime by Y1, Z2, FINSEQ_1:def 7; :: thesis: verum

end;

suppose ( not i in dom ff & not j in dom ff ) ; :: thesis: fg . i,fg . j are_coprime

then ( i in {((k + 1) + 1)} & j in {((k + 1) + 1)} ) by v1, Z1, B1, C1, XBOOLE_0:def 3;
then ( i = (k + 1) + 1 & j = (k + 1) + 1 ) by TARSKI:def 1;
hence fg . i,fg . j are_coprime by Z1; :: thesis: verum

end;

end;

end;

then ( dom fg = Seg ((k + 1) + 1) & ( for i being Nat st i in dom fg holds
fg . i is triangular ) & fg is with_all_coprime_terms ) by C1, T1, INT_6:def 2;
hence S₁[k + 1] ; :: thesis: verum

end;

A3: for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
let n be Nat; :: thesis: ex f being non-empty increasing FinSequence of NAT st
( dom f = Seg (n + 1) & ( for i being Nat st i in dom f holds
f . i is triangular ) & f is with_all_coprime_terms )
consider f being non-empty increasing FinSequence of NAT such that
JJ: ( dom f = Seg (n + 1) & ( for i being Nat st i in dom f holds
f . i is triangular ) & f is with_all_coprime_terms ) by A3;
take f ; :: thesis: ( dom f = Seg (n + 1) & ( for i being Nat st i in dom f holds
f . i is triangular ) & f is with_all_coprime_terms )
thus ( dom f = Seg (n + 1) & ( for i being Nat st i in dom f holds
f . i is triangular ) & f is with_all_coprime_terms ) by JJ; :: thesis: verum