Theorem bndext ≪ | index | src | ≫ 

theorem bndext (a b n: nat) {x: nat}:
  $ A. x (x < n -> (x e. a <-> x e. b)) -> mod(2 ^ n): a = b $;
StepHypRefExpression
1 bndextle 
A. x (x < n -> x e. a -> x e. b) -> a % 2 ^ n <= b % 2 ^ n
2 bi1 
(x e. a <-> x e. b) -> x e. a -> x e. b
3 2 imim2i 
(x < n -> (x e. a <-> x e. b)) -> x < n -> x e. a -> x e. b
4 3 alimi 
A. x (x < n -> (x e. a <-> x e. b)) -> A. x (x < n -> x e. a -> x e. b)
5 1, 4 syl 
A. x (x < n -> (x e. a <-> x e. b)) -> a % 2 ^ n <= b % 2 ^ n
6 bndextle 
A. x (x < n -> x e. b -> x e. a) -> b % 2 ^ n <= a % 2 ^ n
7 bi2 
(x e. a <-> x e. b) -> x e. b -> x e. a
8 7 imim2i 
(x < n -> (x e. a <-> x e. b)) -> x < n -> x e. b -> x e. a
9 8 alimi 
A. x (x < n -> (x e. a <-> x e. b)) -> A. x (x < n -> x e. b -> x e. a)
10 6, 9 syl 
A. x (x < n -> (x e. a <-> x e. b)) -> b % 2 ^ n <= a % 2 ^ n
11 5, 10 leasymd 
A. x (x < n -> (x e. a <-> x e. b)) -> a % 2 ^ n = b % 2 ^ n
12 11 conv eqm 
A. x (x < n -> (x e. a <-> x e. b)) -> mod(2 ^ n): a = b

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)