let n be Nat; :: thesis: for a being non trivial Nat holds Px (a,n), Py (a,n) are_coprime
let a be non trivial Nat; :: thesis: Px (a,n), Py (a,n) are_coprime
defpred S1[ Nat] means (Px (a,$1)) gcd (Py (a,$1)) = 1;
( Px (a,0) = 1 & Py (a,0) = 0 ) by Th6;
then A1: S1[ 0 ] ;
A2: for n being Nat st S1[n] holds
S1[n + 1]
proof
set A = (a ^2) -' 1;
A3: (a ^2) -' 1 = (a ^2) - 1 by NAT_1:14, XREAL_1:233;
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A4: S1[n] ; :: thesis: S1[n + 1]
A5: ( Px (a,(n + 1)) = ((Px (a,n)) * a) + ((Py (a,n)) * ((a ^2) -' 1)) & Py (a,(n + 1)) = (Px (a,n)) + ((Py (a,n)) * a) ) by Th9;
thus 1 = ((Px (a,n)) + ((Py (a,n)) * a)) gcd (Py (a,n)) by A4, EULER_1:8
.= (Py (a,(n + 1))) gcd (- (Py (a,n))) by A5, NEWTON02:1
.= ((- (Py (a,n))) + (a * (Py (a,(n + 1))))) gcd (Py (a,(n + 1))) by NEWTON02:5
.= (Px (a,(n + 1))) gcd (Py (a,(n + 1))) by A3, A5 ; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(A1, A2);
 then (Px (a,n)) gcd (Py (a,n)) = 1 ;
hence Px (a,n), Py (a,n) are_coprime by INT_2:def 3; :: thesis: verum