`∀p:ℕ+. ∀a:p-adics(p). ∀n:ℕ+.  ((0 ≤ ((a (n + 1)) - a n)) ∧ (((a (n + 1)) - a n) ≤ (p^(n + 1) - p^n)))`

Proof

Definitions occuring in Statement :  p-adics: `p-adics(p)` exp: `i^n` nat_plus: `ℕ+` le: `A ≤ B` all: `∀x:A. B[x]` and: `P ∧ Q` apply: `f a` subtract: `n - m` add: `n + m` natural_number: `\$n`
Definitions unfolded in proof :  all: `∀x:A. B[x]` and: `P ∧ Q` cand: `A c∧ B` p-adics: `p-adics(p)` uall: `∀[x:A]. B[x]` member: `t ∈ T` nat_plus: `ℕ+` decidable: `Dec(P)` or: `P ∨ Q` iff: `P `⇐⇒` Q` not: `¬A` rev_implies: `P `` Q` implies: `P `` Q` false: `False` prop: `ℙ` uiff: `uiff(P;Q)` uimplies: `b supposing a` subtract: `n - m` subtype_rel: `A ⊆r B` le: `A ≤ B` less_than': `less_than'(a;b)` true: `True` int_seg: `{i..j-}` sq_stable: `SqStable(P)` eqmod: `a ≡ b mod m` divides: `b | a` exists: `∃x:A. B[x]` sq_type: `SQType(T)` guard: `{T}` squash: `↓T` nat: `ℕ` satisfiable_int_formula: `satisfiable_int_formula(fmla)` top: `Top` lelt: `i ≤ j < k`
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut sqequalHypSubstitution setElimination thin rename introduction extract_by_obid isectElimination natural_numberEquality applyEquality functionExtensionality hypothesisEquality hypothesis dependent_set_memberEquality addEquality dependent_functionElimination unionElimination independent_pairFormation voidElimination productElimination independent_functionElimination independent_isectElimination sqequalRule because_Cache minusEquality lambdaEquality instantiate cumulativity intEquality equalityTransitivity equalitySymmetry imageMemberEquality baseClosed imageElimination approximateComputation dependent_pairFormation int_eqEquality isect_memberEquality voidEquality baseApply closedConclusion applyLambdaEquality universeEquality multiplyEquality

Latex: