let n, m be non zero Nat; :: thesis: for p being Prime st p |^ n divides m holds
Euler (p |^ n) <= Euler m
let p be Prime; :: thesis: ( p |^ n divides m implies Euler (p |^ n) <= Euler m )
assume A1: p |^ n divides m ; :: thesis: Euler (p |^ n) <= Euler m
p |^ 1 divides p |^ n by NAT_1:14, NEWTON:89;
then consider k, w being positive Nat such that
A2: ( 0 < k & m = w * (p |^ k) & w,p are_coprime ) by A1, INT_2:9, NUMBER15:21;
Euler m = (Euler w) * (Euler (p |^ k)) by A2, WSIERP_1:10, EULER_1:21;
then A3: Euler m >= (Euler (p |^ k)) * 1 by NAT_1:14, XREAL_1:64;
w,p |^ n are_coprime by A2, WSIERP_1:10;
then ( p |-count (p |^ n) <= p |-count (p |^ k) & p |-count (p |^ k) = k ) by A2, A1, EULER_1:13, NAT_3:25, NAT_3:30, INT_2:def 4;
then A4: n <= k by NAT_3:25, INT_2:def 4;
A5: ( (k -' 1) + 1 = (k - 1) + 1 & (n -' 1) + 1 = (n - 1) + 1 ) ;
then ( p |^ k = p * (p |^ (k -' 1)) & p |^ n = p * (p |^ (n -' 1)) ) by NEWTON:6;
then A6: ( Euler (p |^ k) = (p * (p |^ (k -' 1))) - (p |^ (k -' 1)) & (p * (p |^ (k -' 1))) - (p |^ (k -' 1)) = (p |^ (k -' 1)) * (p - 1) & Euler (p |^ n) = (p * (p |^ (n -' 1))) - (p |^ (n -' 1)) & (p * (p |^ (n -' 1))) - (p |^ (n -' 1)) = (p |^ (n -' 1)) * (p - 1) ) by NAT_1:14, INT_8:8;
n -' 1 <= k -' 1 by A5, A4, XREAL_1:9;
then p |^ (n -' 1) <= p |^ (k -' 1) by NAT_6:1;
then (p |^ (n -' 1)) * (p - 1) <= (p |^ (k -' 1)) * (p - 1) by XREAL_1:64;
hence Euler (p |^ n) <= Euler m by A3, A6, XXREAL_0:2; :: thesis: verum