Theorem bndextle ≪ | index | src | ≫ 

theorem bndextle (a b n: nat) {x: nat}:
  $ A. x (x < n -> x e. a -> x e. b) -> a % 2 ^ n <= b % 2 ^ n $;
StepHypRefExpression
1 id 
_1 = n -> _1 = n
2 1 lteq2d 
_1 = n -> (x < _1 <-> x < n)
3 2 imeq1d 
_1 = n -> (x < _1 -> x e. a -> x e. b <-> x < n -> x e. a -> x e. b)
4 3 aleqd 
_1 = n -> (A. x (x < _1 -> x e. a -> x e. b) <-> A. x (x < n -> x e. a -> x e. b))
5 1 poweq2d 
_1 = n -> 2 ^ _1 = 2 ^ n
6 5 modeq2d 
_1 = n -> a % 2 ^ _1 = a % 2 ^ n
7 5 modeq2d 
_1 = n -> b % 2 ^ _1 = b % 2 ^ n
8 6, 7 leeqd 
_1 = n -> (a % 2 ^ _1 <= b % 2 ^ _1 <-> a % 2 ^ n <= b % 2 ^ n)
9 4, 8 imeqd 
_1 = n -> (A. x (x < _1 -> x e. a -> x e. b) -> a % 2 ^ _1 <= b % 2 ^ _1 <-> A. x (x < n -> x e. a -> x e. b) -> a % 2 ^ n <= b % 2 ^ n)
10 id 
_1 = 0 -> _1 = 0
11 10 lteq2d 
_1 = 0 -> (x < _1 <-> x < 0)
12 11 imeq1d 
_1 = 0 -> (x < _1 -> x e. a -> x e. b <-> x < 0 -> x e. a -> x e. b)
13 12 aleqd 
_1 = 0 -> (A. x (x < _1 -> x e. a -> x e. b) <-> A. x (x < 0 -> x e. a -> x e. b))
14 10 poweq2d 
_1 = 0 -> 2 ^ _1 = 2 ^ 0
15 14 modeq2d 
_1 = 0 -> a % 2 ^ _1 = a % 2 ^ 0
16 14 modeq2d 
_1 = 0 -> b % 2 ^ _1 = b % 2 ^ 0
17 15, 16 leeqd 
_1 = 0 -> (a % 2 ^ _1 <= b % 2 ^ _1 <-> a % 2 ^ 0 <= b % 2 ^ 0)
18 13, 17 imeqd 
_1 = 0 -> (A. x (x < _1 -> x e. a -> x e. b) -> a % 2 ^ _1 <= b % 2 ^ _1 <-> A. x (x < 0 -> x e. a -> x e. b) -> a % 2 ^ 0 <= b % 2 ^ 0)
19 id 
_1 = a1 -> _1 = a1
20 19 lteq2d 
_1 = a1 -> (x < _1 <-> x < a1)
21 20 imeq1d 
_1 = a1 -> (x < _1 -> x e. a -> x e. b <-> x < a1 -> x e. a -> x e. b)
22 21 aleqd 
_1 = a1 -> (A. x (x < _1 -> x e. a -> x e. b) <-> A. x (x < a1 -> x e. a -> x e. b))
23 19 poweq2d 
_1 = a1 -> 2 ^ _1 = 2 ^ a1
24 23 modeq2d 
_1 = a1 -> a % 2 ^ _1 = a % 2 ^ a1
25 23 modeq2d 
_1 = a1 -> b % 2 ^ _1 = b % 2 ^ a1
26 24, 25 leeqd 
_1 = a1 -> (a % 2 ^ _1 <= b % 2 ^ _1 <-> a % 2 ^ a1 <= b % 2 ^ a1)
27 22, 26 imeqd 
_1 = a1 -> (A. x (x < _1 -> x e. a -> x e. b) -> a % 2 ^ _1 <= b % 2 ^ _1 <-> A. x (x < a1 -> x e. a -> x e. b) -> a % 2 ^ a1 <= b % 2 ^ a1)
28 id 
_1 = suc a1 -> _1 = suc a1
29 28 lteq2d 
_1 = suc a1 -> (x < _1 <-> x < suc a1)
30 29 imeq1d 
_1 = suc a1 -> (x < _1 -> x e. a -> x e. b <-> x < suc a1 -> x e. a -> x e. b)
31 30 aleqd 
_1 = suc a1 -> (A. x (x < _1 -> x e. a -> x e. b) <-> A. x (x < suc a1 -> x e. a -> x e. b))
32 28 poweq2d 
_1 = suc a1 -> 2 ^ _1 = 2 ^ suc a1
33 32 modeq2d 
_1 = suc a1 -> a % 2 ^ _1 = a % 2 ^ suc a1
34 32 modeq2d 
_1 = suc a1 -> b % 2 ^ _1 = b % 2 ^ suc a1
35 33, 34 leeqd 
_1 = suc a1 -> (a % 2 ^ _1 <= b % 2 ^ _1 <-> a % 2 ^ suc a1 <= b % 2 ^ suc a1)
36 31, 35 imeqd 
_1 = suc a1 -> (A. x (x < _1 -> x e. a -> x e. b) -> a % 2 ^ _1 <= b % 2 ^ _1 <-> A. x (x < suc a1 -> x e. a -> x e. b) -> a % 2 ^ suc a1 <= b % 2 ^ suc a1)
37 leeq1 
a % 2 ^ 0 = 0 -> (a % 2 ^ 0 <= b % 2 ^ 0 <-> 0 <= b % 2 ^ 0)
38 eqtr 
a % 2 ^ 0 = a % 1 -> a % 1 = 0 -> a % 2 ^ 0 = 0
39 modeq2 
2 ^ 0 = 1 -> a % 2 ^ 0 = a % 1
40 pow0 
2 ^ 0 = 1
41 39, 40 ax_mp 
a % 2 ^ 0 = a % 1
42 38, 41 ax_mp 
a % 1 = 0 -> a % 2 ^ 0 = 0
43 mod12 
a % 1 = 0
44 42, 43 ax_mp 
a % 2 ^ 0 = 0
45 37, 44 ax_mp 
a % 2 ^ 0 <= b % 2 ^ 0 <-> 0 <= b % 2 ^ 0
46 le01 
0 <= b % 2 ^ 0
47 45, 46 mpbir 
a % 2 ^ 0 <= b % 2 ^ 0
48 47 a1i 
A. x (x < 0 -> x e. a -> x e. b) -> a % 2 ^ 0 <= b % 2 ^ 0
49 ltsucid 
a1 < suc a1
50 lttr 
x < a1 -> a1 < suc a1 -> x < suc a1
51 49, 50 mpi 
x < a1 -> x < suc a1
52 51 imim1i 
(x < suc a1 -> x e. a -> x e. b) -> x < a1 -> x e. a -> x e. b
53 52 alimi 
A. x (x < suc a1 -> x e. a -> x e. b) -> A. x (x < a1 -> x e. a -> x e. b)
54 53 imim1i 
(A. x (x < a1 -> x e. a -> x e. b) -> a % 2 ^ a1 <= b % 2 ^ a1) -> A. x (x < suc a1 -> x e. a -> x e. b) -> a % 2 ^ a1 <= b % 2 ^ a1
55 lteq1 
x = a1 -> (x < suc a1 <-> a1 < suc a1)
56 eleq1 
x = a1 -> (x e. a <-> a1 e. a)
57 eleq1 
x = a1 -> (x e. b <-> a1 e. b)
58 56, 57 imeqd 
x = a1 -> (x e. a -> x e. b <-> a1 e. a -> a1 e. b)
59 55, 58 imeqd 
x = a1 -> (x < suc a1 -> x e. a -> x e. b <-> a1 < suc a1 -> a1 e. a -> a1 e. b)
60 59 eale 
A. x (x < suc a1 -> x e. a -> x e. b) -> a1 < suc a1 -> a1 e. a -> a1 e. b
61 49, 60 mpi 
A. x (x < suc a1 -> x e. a -> x e. b) -> a1 e. a -> a1 e. b
62 leeq 
2 ^ a1 * (a % 2 ^ suc a1 // 2 ^ a1) + a % 2 ^ suc a1 % 2 ^ a1 = a % 2 ^ suc a1 ->
  2 ^ a1 * (b % 2 ^ suc a1 // 2 ^ a1) + b % 2 ^ suc a1 % 2 ^ a1 = b % 2 ^ suc a1 ->
  (2 ^ a1 * (a % 2 ^ suc a1 // 2 ^ a1) + a % 2 ^ suc a1 % 2 ^ a1 <= 2 ^ a1 * (b % 2 ^ suc a1 // 2 ^ a1) + b % 2 ^ suc a1 % 2 ^ a1 <->
    a % 2 ^ suc a1 <= b % 2 ^ suc a1)
63 divmod 
2 ^ a1 * (a % 2 ^ suc a1 // 2 ^ a1) + a % 2 ^ suc a1 % 2 ^ a1 = a % 2 ^ suc a1
64 62, 63 ax_mp 
2 ^ a1 * (b % 2 ^ suc a1 // 2 ^ a1) + b % 2 ^ suc a1 % 2 ^ a1 = b % 2 ^ suc a1 ->
  (2 ^ a1 * (a % 2 ^ suc a1 // 2 ^ a1) + a % 2 ^ suc a1 % 2 ^ a1 <= 2 ^ a1 * (b % 2 ^ suc a1 // 2 ^ a1) + b % 2 ^ suc a1 % 2 ^ a1 <->
    a % 2 ^ suc a1 <= b % 2 ^ suc a1)
65 divmod 
2 ^ a1 * (b % 2 ^ suc a1 // 2 ^ a1) + b % 2 ^ suc a1 % 2 ^ a1 = b % 2 ^ suc a1
66 64, 65 ax_mp 
2 ^ a1 * (a % 2 ^ suc a1 // 2 ^ a1) + a % 2 ^ suc a1 % 2 ^ a1 <= 2 ^ a1 * (b % 2 ^ suc a1 // 2 ^ a1) + b % 2 ^ suc a1 % 2 ^ a1 <->
  a % 2 ^ suc a1 <= b % 2 ^ suc a1
67 leeq 
2 ^ a1 * (a % 2 ^ suc a1 // 2 ^ a1) + a % 2 ^ suc a1 % 2 ^ a1 = 2 ^ a1 * (a // 2 ^ a1 % 2) + a % 2 ^ a1 ->
  2 ^ a1 * (b % 2 ^ suc a1 // 2 ^ a1) + b % 2 ^ suc a1 % 2 ^ a1 = 2 ^ a1 * (b // 2 ^ a1 % 2) + b % 2 ^ a1 ->
  (2 ^ a1 * (a % 2 ^ suc a1 // 2 ^ a1) + a % 2 ^ suc a1 % 2 ^ a1 <= 2 ^ a1 * (b % 2 ^ suc a1 // 2 ^ a1) + b % 2 ^ suc a1 % 2 ^ a1 <->
    2 ^ a1 * (a // 2 ^ a1 % 2) + a % 2 ^ a1 <= 2 ^ a1 * (b // 2 ^ a1 % 2) + b % 2 ^ a1)
68 addeq 
2 ^ a1 * (a % 2 ^ suc a1 // 2 ^ a1) = 2 ^ a1 * (a // 2 ^ a1 % 2) ->
  a % 2 ^ suc a1 % 2 ^ a1 = a % 2 ^ a1 ->
  2 ^ a1 * (a % 2 ^ suc a1 // 2 ^ a1) + a % 2 ^ suc a1 % 2 ^ a1 = 2 ^ a1 * (a // 2 ^ a1 % 2) + a % 2 ^ a1
69 muleq2 
a % 2 ^ suc a1 // 2 ^ a1 = a // 2 ^ a1 % 2 -> 2 ^ a1 * (a % 2 ^ suc a1 // 2 ^ a1) = 2 ^ a1 * (a // 2 ^ a1 % 2)
70 eqtr4 
a % 2 ^ suc a1 // 2 ^ a1 = a % (2 ^ a1 * 2) // 2 ^ a1 -> a // 2 ^ a1 % 2 = a % (2 ^ a1 * 2) // 2 ^ a1 -> a % 2 ^ suc a1 // 2 ^ a1 = a // 2 ^ a1 % 2
71 diveq1 
a % 2 ^ suc a1 = a % (2 ^ a1 * 2) -> a % 2 ^ suc a1 // 2 ^ a1 = a % (2 ^ a1 * 2) // 2 ^ a1
72 modeq2 
2 ^ suc a1 = 2 ^ a1 * 2 -> a % 2 ^ suc a1 = a % (2 ^ a1 * 2)
73 powS2 
2 ^ suc a1 = 2 ^ a1 * 2
74 72, 73 ax_mp 
a % 2 ^ suc a1 = a % (2 ^ a1 * 2)
75 71, 74 ax_mp 
a % 2 ^ suc a1 // 2 ^ a1 = a % (2 ^ a1 * 2) // 2 ^ a1
76 70, 75 ax_mp 
a // 2 ^ a1 % 2 = a % (2 ^ a1 * 2) // 2 ^ a1 -> a % 2 ^ suc a1 // 2 ^ a1 = a // 2 ^ a1 % 2
77 divmod1 
a // 2 ^ a1 % 2 = a % (2 ^ a1 * 2) // 2 ^ a1
78 76, 77 ax_mp 
a % 2 ^ suc a1 // 2 ^ a1 = a // 2 ^ a1 % 2
79 69, 78 ax_mp 
2 ^ a1 * (a % 2 ^ suc a1 // 2 ^ a1) = 2 ^ a1 * (a // 2 ^ a1 % 2)
80 68, 79 ax_mp 
a % 2 ^ suc a1 % 2 ^ a1 = a % 2 ^ a1 -> 2 ^ a1 * (a % 2 ^ suc a1 // 2 ^ a1) + a % 2 ^ suc a1 % 2 ^ a1 = 2 ^ a1 * (a // 2 ^ a1 % 2) + a % 2 ^ a1
81 modmod 
2 ^ a1 || 2 ^ suc a1 -> a % 2 ^ suc a1 % 2 ^ a1 = a % 2 ^ a1
82 powdvd 
a1 <= suc a1 -> 2 ^ a1 || 2 ^ suc a1
83 lesucid 
a1 <= suc a1
84 82, 83 ax_mp 
2 ^ a1 || 2 ^ suc a1
85 81, 84 ax_mp 
a % 2 ^ suc a1 % 2 ^ a1 = a % 2 ^ a1
86 80, 85 ax_mp 
2 ^ a1 * (a % 2 ^ suc a1 // 2 ^ a1) + a % 2 ^ suc a1 % 2 ^ a1 = 2 ^ a1 * (a // 2 ^ a1 % 2) + a % 2 ^ a1
87 67, 86 ax_mp 
2 ^ a1 * (b % 2 ^ suc a1 // 2 ^ a1) + b % 2 ^ suc a1 % 2 ^ a1 = 2 ^ a1 * (b // 2 ^ a1 % 2) + b % 2 ^ a1 ->
  (2 ^ a1 * (a % 2 ^ suc a1 // 2 ^ a1) + a % 2 ^ suc a1 % 2 ^ a1 <= 2 ^ a1 * (b % 2 ^ suc a1 // 2 ^ a1) + b % 2 ^ suc a1 % 2 ^ a1 <->
    2 ^ a1 * (a // 2 ^ a1 % 2) + a % 2 ^ a1 <= 2 ^ a1 * (b // 2 ^ a1 % 2) + b % 2 ^ a1)
88 addeq 
2 ^ a1 * (b % 2 ^ suc a1 // 2 ^ a1) = 2 ^ a1 * (b // 2 ^ a1 % 2) ->
  b % 2 ^ suc a1 % 2 ^ a1 = b % 2 ^ a1 ->
  2 ^ a1 * (b % 2 ^ suc a1 // 2 ^ a1) + b % 2 ^ suc a1 % 2 ^ a1 = 2 ^ a1 * (b // 2 ^ a1 % 2) + b % 2 ^ a1
89 muleq2 
b % 2 ^ suc a1 // 2 ^ a1 = b // 2 ^ a1 % 2 -> 2 ^ a1 * (b % 2 ^ suc a1 // 2 ^ a1) = 2 ^ a1 * (b // 2 ^ a1 % 2)
90 eqtr4 
b % 2 ^ suc a1 // 2 ^ a1 = b % (2 ^ a1 * 2) // 2 ^ a1 -> b // 2 ^ a1 % 2 = b % (2 ^ a1 * 2) // 2 ^ a1 -> b % 2 ^ suc a1 // 2 ^ a1 = b // 2 ^ a1 % 2
91 diveq1 
b % 2 ^ suc a1 = b % (2 ^ a1 * 2) -> b % 2 ^ suc a1 // 2 ^ a1 = b % (2 ^ a1 * 2) // 2 ^ a1
92 modeq2 
2 ^ suc a1 = 2 ^ a1 * 2 -> b % 2 ^ suc a1 = b % (2 ^ a1 * 2)
93 92, 73 ax_mp 
b % 2 ^ suc a1 = b % (2 ^ a1 * 2)
94 91, 93 ax_mp 
b % 2 ^ suc a1 // 2 ^ a1 = b % (2 ^ a1 * 2) // 2 ^ a1
95 90, 94 ax_mp 
b // 2 ^ a1 % 2 = b % (2 ^ a1 * 2) // 2 ^ a1 -> b % 2 ^ suc a1 // 2 ^ a1 = b // 2 ^ a1 % 2
96 divmod1 
b // 2 ^ a1 % 2 = b % (2 ^ a1 * 2) // 2 ^ a1
97 95, 96 ax_mp 
b % 2 ^ suc a1 // 2 ^ a1 = b // 2 ^ a1 % 2
98 89, 97 ax_mp 
2 ^ a1 * (b % 2 ^ suc a1 // 2 ^ a1) = 2 ^ a1 * (b // 2 ^ a1 % 2)
99 88, 98 ax_mp 
b % 2 ^ suc a1 % 2 ^ a1 = b % 2 ^ a1 -> 2 ^ a1 * (b % 2 ^ suc a1 // 2 ^ a1) + b % 2 ^ suc a1 % 2 ^ a1 = 2 ^ a1 * (b // 2 ^ a1 % 2) + b % 2 ^ a1
100 modmod 
2 ^ a1 || 2 ^ suc a1 -> b % 2 ^ suc a1 % 2 ^ a1 = b % 2 ^ a1
101 100, 84 ax_mp 
b % 2 ^ suc a1 % 2 ^ a1 = b % 2 ^ a1
102 99, 101 ax_mp 
2 ^ a1 * (b % 2 ^ suc a1 // 2 ^ a1) + b % 2 ^ suc a1 % 2 ^ a1 = 2 ^ a1 * (b // 2 ^ a1 % 2) + b % 2 ^ a1
103 87, 102 ax_mp 
2 ^ a1 * (a % 2 ^ suc a1 // 2 ^ a1) + a % 2 ^ suc a1 % 2 ^ a1 <= 2 ^ a1 * (b % 2 ^ suc a1 // 2 ^ a1) + b % 2 ^ suc a1 % 2 ^ a1 <->
  2 ^ a1 * (a // 2 ^ a1 % 2) + a % 2 ^ a1 <= 2 ^ a1 * (b // 2 ^ a1 % 2) + b % 2 ^ a1
104 lemul2a 
a // 2 ^ a1 % 2 <= b // 2 ^ a1 % 2 -> 2 ^ a1 * (a // 2 ^ a1 % 2) <= 2 ^ a1 * (b // 2 ^ a1 % 2)
105 letrueb 
bool (a // 2 ^ a1 % 2) -> (a // 2 ^ a1 % 2 <= b // 2 ^ a1 % 2 <-> true (a // 2 ^ a1 % 2) -> true (b // 2 ^ a1 % 2))
106 boolmod2 
bool (a // 2 ^ a1 % 2)
107 105, 106 ax_mp 
a // 2 ^ a1 % 2 <= b // 2 ^ a1 % 2 <-> true (a // 2 ^ a1 % 2) -> true (b // 2 ^ a1 % 2)
108 dfodd2 
odd (a // 2 ^ a1) <-> true (a // 2 ^ a1 % 2)
109 dfodd2 
odd (b // 2 ^ a1) <-> true (b // 2 ^ a1 % 2)
110 elnel 
a1 e. a <-> odd (shr a a1)
111 110 conv shr 
a1 e. a <-> odd (a // 2 ^ a1)
112 elnel 
a1 e. b <-> odd (shr b a1)
113 112 conv shr 
a1 e. b <-> odd (b // 2 ^ a1)
114 anl 
(a1 e. a -> a1 e. b) /\ a % 2 ^ a1 <= b % 2 ^ a1 -> a1 e. a -> a1 e. b
115 113, 114 syl6ib 
(a1 e. a -> a1 e. b) /\ a % 2 ^ a1 <= b % 2 ^ a1 -> a1 e. a -> odd (b // 2 ^ a1)
116 111, 115 syl5bir 
(a1 e. a -> a1 e. b) /\ a % 2 ^ a1 <= b % 2 ^ a1 -> odd (a // 2 ^ a1) -> odd (b // 2 ^ a1)
117 109, 116 syl6ib 
(a1 e. a -> a1 e. b) /\ a % 2 ^ a1 <= b % 2 ^ a1 -> odd (a // 2 ^ a1) -> true (b // 2 ^ a1 % 2)
118 108, 117 syl5bir 
(a1 e. a -> a1 e. b) /\ a % 2 ^ a1 <= b % 2 ^ a1 -> true (a // 2 ^ a1 % 2) -> true (b // 2 ^ a1 % 2)
119 107, 118 sylibr 
(a1 e. a -> a1 e. b) /\ a % 2 ^ a1 <= b % 2 ^ a1 -> a // 2 ^ a1 % 2 <= b // 2 ^ a1 % 2
120 104, 119 syl 
(a1 e. a -> a1 e. b) /\ a % 2 ^ a1 <= b % 2 ^ a1 -> 2 ^ a1 * (a // 2 ^ a1 % 2) <= 2 ^ a1 * (b // 2 ^ a1 % 2)
121 anr 
(a1 e. a -> a1 e. b) /\ a % 2 ^ a1 <= b % 2 ^ a1 -> a % 2 ^ a1 <= b % 2 ^ a1
122 120, 121 leaddd 
(a1 e. a -> a1 e. b) /\ a % 2 ^ a1 <= b % 2 ^ a1 -> 2 ^ a1 * (a // 2 ^ a1 % 2) + a % 2 ^ a1 <= 2 ^ a1 * (b // 2 ^ a1 % 2) + b % 2 ^ a1
123 103, 122 sylibr 
(a1 e. a -> a1 e. b) /\ a % 2 ^ a1 <= b % 2 ^ a1 ->
  2 ^ a1 * (a % 2 ^ suc a1 // 2 ^ a1) + a % 2 ^ suc a1 % 2 ^ a1 <= 2 ^ a1 * (b % 2 ^ suc a1 // 2 ^ a1) + b % 2 ^ suc a1 % 2 ^ a1
124 66, 123 sylib 
(a1 e. a -> a1 e. b) /\ a % 2 ^ a1 <= b % 2 ^ a1 -> a % 2 ^ suc a1 <= b % 2 ^ suc a1
125 124 exp 
(a1 e. a -> a1 e. b) -> a % 2 ^ a1 <= b % 2 ^ a1 -> a % 2 ^ suc a1 <= b % 2 ^ suc a1
126 61, 125 rsyl 
A. x (x < suc a1 -> x e. a -> x e. b) -> a % 2 ^ a1 <= b % 2 ^ a1 -> a % 2 ^ suc a1 <= b % 2 ^ suc a1
127 126 a2i 
(A. x (x < suc a1 -> x e. a -> x e. b) -> a % 2 ^ a1 <= b % 2 ^ a1) -> A. x (x < suc a1 -> x e. a -> x e. b) -> a % 2 ^ suc a1 <= b % 2 ^ suc a1
128 54, 127 rsyl 
(A. x (x < a1 -> x e. a -> x e. b) -> a % 2 ^ a1 <= b % 2 ^ a1) -> A. x (x < suc a1 -> x e. a -> x e. b) -> a % 2 ^ suc a1 <= b % 2 ^ suc a1
129 9, 18, 27, 36, 48, 128 ind 
A. x (x < n -> x e. a -> x e. b) -> a % 2 ^ n <= b % 2 ^ n

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)