let i be Nat; :: thesis: ( 3 <= i implies i mod (i -' 1) = 1 )
assume A1: 3 <= i ; :: thesis: i mod (i -' 1) = 1
then A2: i -' 1 = i - 1 by XREAL_1:233, XXREAL_0:2;
3 -' 1 = (2 + 1) -' 1
.= 2 by NAT_D:34 ;
then 2 <= i -' 1 by A1, NAT_D:42;
then 1 < i - 1 by A2, XXREAL_0:2;
then 1 + i < (i - 1) + i by XREAL_1:8;
then (1 + i) - 1 < ((i - 1) + i) - 1 by XREAL_1:14;
then A3: i < (i - 1) + (i - 1) ;
i -' 1 <= i by NAT_D:35;
hence i mod (i -' 1) = i - (i - 1) by A2, A3, JORDAN4:2
.= 1 ;
:: thesis: verum