let i be Element of NAT ; :: thesis: ( 3 <= i implies i mod (i -' 1) = 1 )
A1: 3 -' 1 = (2 + 1) -' 1
.= 2 by NAT_D:34 ;
assume A2: 3 <= i ; :: thesis: i mod (i -' 1) = 1
then A3: i -' 1 = i - 1 by XREAL_1:235, XXREAL_0:2;
A4: 2 <= i -' 1 by A1, A2, NAT_D:42;
A5: i -' 1 <= i by NAT_D:35;
1 < i - 1 by A3, A4, XXREAL_0:2;
then 1 + i < (i - 1) + i by XREAL_1:10;
then (1 + i) - 1 < ((i - 1) + i) - 1 by XREAL_1:16;
then i < (i - 1) + (i - 1) ;
hence i mod (i -' 1) = i - (i - 1) by A3, A4, A5, JORDAN4:7
.= 1 ;
:: thesis: verum