:: An ordered pair for natural numbers
::   by Robert M. Solovay
environ
vocabulary PAIR, ARYTM_1, RELAT_1, NEWTON, ORDINAL2, ARYTM, ARYTM_3,
 QC_LANG1;
notation ARYTM_0, ARYTM, REAL_1, NAT_1, NEWTON, ORDINAL2;
constructors REAL_1, POLYNOM1, BINOM;
clusters ARYTM, ARYTM_3, NAT_1;
requirements NUMERALS, ARYTM, SUBSET, REAL;
theorems NAT_1, AXIOMS, ORDINAL2, REAL_1, NEWTON;
schemes NAT_1;
begin
  reserve i,k,n,m,k1, m1, n1,l,p,r for natural number;

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::  
::                      Preliminary lemmas                                 ::
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

  PLm1: for m, n st m < n holds ex k being Nat st n = (m + k) + 1
  proof
     let m,n;
     assume 1_1: m < n; then
     consider r being Nat such that 1_2: n = m + r by NAT_1:28;
     per cases by NAT_1:22;
     suppose  r = 0;
     hence thesis by 1_2, 1_1;
     suppose  ex s being Nat st  r = s + 1; then
     consider s being Nat such that 2_1: r = s + 1;
     n  = (m + s) + 1 by 2_1, 1_2, AXIOMS:13;
     hence thesis;
        end;

definition
  let m,n;
   redefine func n choose m -> Nat;
   coherence by NEWTON:35;
  end;

definition
  let k,n be natural number;
  func J(k,n) -> Nat equals :Def1: ((k + n + 1) choose 2) + n;
coherence by ORDINAL2:def 21;
  end;

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
::     Properties of (n + 1) choose 2                                      ::
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

  deffunc f(natural number) = ($1 + 1) choose 2;

  Lm1: f(0) = 0 by NEWTON:def 3;

  theorem
   for n being natural number holds f(n) = ((n + 1) * n)/2
:: This theorem plays no role in any of our proofs. It's just provided to
:: connect up with the definition of the ordered pair that Raph uses.
  proof
    let n;
    per cases by NAT_1:22;
    suppose n = 0;
    hence thesis by NEWTON:def 3;
    suppose 1'1: ex k being Nat st n = k + 1;
    consider k being Nat such that 2_1: n = k+1 by 1'1;
    2_2:k + 2 = k + (1+1)
       .= (k+1) + 1 by AXIOMS:13;
    2_3: (k + 2) - 2 = k + (2 - 2) by REAL_1:17
    .= k;
    2_4: (k+2)! * (k!)" = (n+1) * n
       proof
          3_1: (k+2)!
          = (n+1) * ((k+1)!) by 2_1, 2_2, NEWTON:21
          .= (n+1) * (n * (k!)) by 2_1, NEWTON:21
          .= ((n+1) * n) * (k!) by AXIOMS:16;
          3_2: (k!) * (k!)" = 1
          proof
            set x = k!;
            4_1: x * x" = x * (1/x) by REAL_1:33;
            x <> 0 by NEWTON:23;
            hence thesis by 4_1, REAL_1:34;
          end;
          (k+2)! * (k!)" = ((n+1) * n) * 1 by AXIOMS:16, 3_1, 3_2
          .= (n+1) * n;
         hence thesis;
       end;
    (k + 2) >= 2 by NAT_1:29;
    then (k + 2) choose 2
    = (k+2)!/ ( 2 * (k!)) by NEWTON:def 3, 2_3, NEWTON:20
    .= (k+2)! * ((k!) * 2)" by REAL_1:def 4
    .= (k+2)! * ((k!)" * 2") by REAL_1:24
    .= ((n+1) * n) * 2" by AXIOMS:16, 2_4
    .= ((n+1) * n)/2 by REAL_1:def 4;
    hence  thesis by 2_1,2_2;
    end;


Lm2: for n holds f(n+1) = f(n) + (n+1)
proof
let n;
per cases by NAT_1:22;
suppose 1'1: n = 0; then
    f(n) + (n + 1) = 1 by NEWTON:def 3;
hence thesis by 1'1, NEWTON:31;

suppose 1'2: ex k being Nat st n = k + 1;
    consider k being Nat such that 2'1: n = k+1 by 1'2;
    0 <> (k + 1) by NAT_1:21;
    then 2_1: 0 < n by 2'1, NAT_1:19;
    2_2:(0 + 1 ) < (n + 1) by 2_1, REAL_1:67; then
   ((n+1) + 1) choose (1 + 1) = ((n + 1) choose (1 + 1)) + ((n + 1) choose 1)
   by NEWTON:32;
   hence thesis by NEWTON:33, 2_2;
end;

Lm3: for n  holds f(n) >= n
proof
  let n;
  per cases by NAT_1:22;
  suppose n = 0;
  hence thesis by NEWTON:def 3;

  suppose 1'1: ex k being Nat st n = k + 1;
  consider k being Nat such that 2_1:n = k + 1 by 1'1;
  0 <= f(k) by NAT_1:18; then
  0 + (k+1) <= f(k) + (k+1) by AXIOMS:24;
  hence thesis by Lm2, 2_1;
  end;

Lm4: for n holds ex m st f(m) <= n & n < f(m+1)
proof
let n;
1_1:f(n+1) >= n+1 by Lm3;
1_2:0 + n < 1 + n by REAL_1:53;
set m = 1 + n;
reconsider m as Nat by ORDINAL2: def 21;
defpred P[Nat] means n < f($1);
1_3: ex r being Nat st P[r]
  proof
    take m;
    thus thesis by 1_2, 1_1, AXIOMS:22;
    end;
consider r being Nat such that
1_4:P[r] & for w being Nat st P[w] holds r <= w from Min(1_3);
1_5: r <> 0 by Lm1, 1_4, NAT_1:18;
consider k being Nat such that 1_6: r = k + 1 by 1_5, NAT_1:22;
 1_7: not r <= k by 1_6, NAT_1:38;
take k;
thus thesis by 1_4, 1_7, 1_6;
end;

Lm5: for k,m holds f(m) <= f(m + k)
proof
  defpred P[natural number] means for m holds f(m) <= f(m+$1);
  1_1: P[0];
  1_2: for k holds (P[k] implies P[k+1])
  proof
    let k;
    assume 2_1:P[k];
    let m;
    2_2: f(m) <= f(m+k) by 2_1;
    f(m+k) <= f(m + (k+1))
    proof
      f(m + (k+1)) = f((m+k) + 1) by AXIOMS:13
      .= f(m+k) + ((m+k) + 1) by Lm2;
      hence thesis by NAT_1:29;
    end;
    hence thesis by 2_2, AXIOMS:22;
  end;
  for k holds P[k] from Nat_Ind(1_1,1_2);
  hence thesis;
  end;

  Lm6: for m, n st m <= n holds f(m) <= f(n)
  proof
    let m, n;
    assume m <= n; then
    consider k being Nat such that 1_1: n = m + k by NAT_1:28;
    thus thesis by 1_1, Lm5;
  end;

  Lm7: for m holds f(m) < f(m+1)
  proof
    let m;
    1_1:f(m+1) = f(m) + (m + 1) by Lm2
    .= (f(m) + m) + 1 by AXIOMS:13;
    f(m) <= f(m) + m by NAT_1:29;
    hence thesis by 1_1, NAT_1:38;
    end;

  Lm8: for m, n st m < n holds f(m) < f(n)
  proof
    let m, n;
    assume m < n; then
    consider k being Nat such that 1_1:n = (m + k) + 1 by PLm1;
    1_2: f(m) <= f(m+k) by  Lm5;
    f(m+k) < f(n) by 1_1, Lm7;
    hence thesis by 1_2, AXIOMS:22;
  end;

  Lm9: for m, n holds m < n iff f(m) < f(n)
  proof
     let m,n;
     per cases;
     suppose m < n;
     hence thesis by Lm8;
     suppose n <= m;
     hence thesis by Lm6;
     end;
     
  
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
::    The principal results                                                  ::
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

theorem
  Th1: for m ex n, k st J(n,k) = m
  proof
    let m;
    consider l such that 1_1: f(l) <= m & m < f(l+1) by Lm4;
    consider r being Nat such that 1_2: m = f(l) + r by 1_1, NAT_1:28;
    1_3: r <= l
       proof
         f(l) + r < f(l) + (l + 1) by 1_1, 1_2, Lm2; then
         r < (l + 1) by AXIOMS:24;
         hence thesis by NAT_1:38;
       end;
    consider k being Nat  such that 1_4: l = r + k
    by 1_3, NAT_1:28;
    m = J(k,r) by Def1, 1_4, 1_2;
    hence thesis;
    end;

    Lm10: for m, n holds f(m+n) <= J(m,n) & J(m,n) < f(m+n+1)
    proof
      let m,n;
      1_1: J(m,n) = f(m+n) + n by Def1;
      hence f(m+n) <= J(m,n) by NAT_1:29;
      1_2:f(m + n) + (m + n) + 0 < f(m+n) + (m+n) + 1 by REAL_1:53; 
      1_3:f(m+n+1) = f(m+n) + (m+n+1) by Lm2
      .= f(m+n) + (m+n) + 1 by AXIOMS:13; then
      n <= m+n by  NAT_1:29; then
      J(m,n) <= f(m+n) + (m+n) by AXIOMS:24, 1_1;
      hence thesis by 1_2, 1_3, AXIOMS:22;
      end;

    theorem
    Th2: for m,n,m1,n1 st J(m,n) = J(m1,n1) holds m = m1 & n = n1
    proof
      let m,n,m1,n1;
      assume 1_1: J(m,n) = J(m1,n1);
      set p = m+n;
      set p1 = m1 + n1;
      1_2:f(p) <= J(m,n) by Lm10;
      J(m,n) < f(p1 + 1) by Lm10, 1_1; then
      f(p) < f(p1 + 1) by 1_2, AXIOMS:22;
      then p < p1 + 1 by Lm9; then
      1_3:p <= p1 by NAT_1:38;
      1_4:f(p1) <= J(m1,n1) by Lm10;
      J(m1,n1) < f(p + 1) by Lm10, 1_1; then
      f(p1) < f(p + 1) by 1_4, AXIOMS:22;
      then p1 < p + 1 by Lm9; then
      1_5:p1 <= p by NAT_1:38; then
      1_6:f(p) + n = J(m1,n1) by Def1, 1_1
      .= f(p1) + n1 by Def1
      .= f(p) + n1 by 1_3, 1_5, AXIOMS:21;
      1_7:n = (n1 + f(p)) -f(p ) by REAL_1:30, 1_6
      .= n1 by REAL_1:30;
       m = p - n by REAL_1:30
      .= p1 -n1 by 1_3, 1_5, AXIOMS:21, 1_7
      .= m1 by REAL_1:30;
      hence m = m1;
      thus thesis by 1_7;
    end;      

definition
   let p be natural number;
   func K(p) -> Nat means
   :Def2: ex n  st J(it,n) = p;
   existence
      proof
        
      for p ex k being Nat st ex n st J(k,n) = p
      proof
        let p;
        consider k such that 1_1: ex n st J(k,n) = p by Th1;
        reconsider k as Nat by ORDINAL2:def 21;
        take k;
        thus thesis by 1_1;
      end;
        hence thesis;
        end;
   
   uniqueness by Th2;
   end;

   definition
   let p be natural number;
   func L(p) -> Nat means
   :Def3: ex n  st J(n,it) = p;
   existence
      proof
        
      for p ex k being Nat st ex n st J(n,k) = p
      proof
        let p;
        ex n, k st J(n,k) = p by Th1; then
        consider k such that 1_1: ex n st J(n,k) = p;
        reconsider k as Nat by ORDINAL2:def 21;
        take k;
        thus thesis by 1_1;
      end;
        hence thesis;
        end;
   
   uniqueness by Th2;
   end;

theorem
  for p holds p = J(K(p), L(p))
  proof
    let p;
    consider n such that 1_1: p = J(K(p),n) by Def2;
    consider m such that 1_2: p = J(m, L(p)) by Def3;
    thus thesis by 1_2, 1_1 , Th2;
  end;

  theorem
    for m, n holds K(J(m,n)) = m
    proof
      let m, n;
      set r = J(m,n);
      consider k such that 1_1:J(K(r),k) = r by Def2; 
      thus thesis by 1_1, Th2;
    end;

    theorem
      for m, n holds L(J(m,n)) = n
      proof
        let m,n;
        set r = J(m,n);
        consider k such that 1_1: J(k, L(r)) = r by Def3;
        thus thesis by 1_1, Th2;
        end;