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 eqidd 
_1 = n -> x = x
2 id 
_1 = n -> _1 = n
3 1, 2 lteqd 
_1 = n -> (x < _1 <-> x < n)
4 biidd 
_1 = n -> (x e. a -> x e. b <-> x e. a -> x e. b)
5 3, 4 imeqd 
_1 = n -> (x < _1 -> x e. a -> x e. b <-> x < n -> x e. a -> x e. b)
6 5 aleqd 
_1 = n -> (A. x (x < _1 -> x e. a -> x e. b) <-> A. x (x < n -> x e. a -> x e. b))
7 eqidd 
_1 = n -> a = a
8 eqidd 
_1 = n -> 2 = 2
9 8, 2 poweqd 
_1 = n -> 2 ^ _1 = 2 ^ n
10 7, 9 modeqd 
_1 = n -> a % 2 ^ _1 = a % 2 ^ n
11 eqidd 
_1 = n -> b = b
12 11, 9 modeqd 
_1 = n -> b % 2 ^ _1 = b % 2 ^ n
13 10, 12 leeqd 
_1 = n -> (a % 2 ^ _1 <= b % 2 ^ _1 <-> a % 2 ^ n <= b % 2 ^ n)
14 6, 13 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)
15 eqidd 
_1 = 0 -> x = x
16 id 
_1 = 0 -> _1 = 0
17 15, 16 lteqd 
_1 = 0 -> (x < _1 <-> x < 0)
18 biidd 
_1 = 0 -> (x e. a -> x e. b <-> x e. a -> x e. b)
19 17, 18 imeqd 
_1 = 0 -> (x < _1 -> x e. a -> x e. b <-> x < 0 -> x e. a -> x e. b)
20 19 aleqd 
_1 = 0 -> (A. x (x < _1 -> x e. a -> x e. b) <-> A. x (x < 0 -> x e. a -> x e. b))
21 eqidd 
_1 = 0 -> a = a
22 eqidd 
_1 = 0 -> 2 = 2
23 22, 16 poweqd 
_1 = 0 -> 2 ^ _1 = 2 ^ 0
24 21, 23 modeqd 
_1 = 0 -> a % 2 ^ _1 = a % 2 ^ 0
25 eqidd 
_1 = 0 -> b = b
26 25, 23 modeqd 
_1 = 0 -> b % 2 ^ _1 = b % 2 ^ 0
27 24, 26 leeqd 
_1 = 0 -> (a % 2 ^ _1 <= b % 2 ^ _1 <-> a % 2 ^ 0 <= b % 2 ^ 0)
28 20, 27 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)
29 eqidd 
_1 = a1 -> x = x
30 id 
_1 = a1 -> _1 = a1
31 29, 30 lteqd 
_1 = a1 -> (x < _1 <-> x < a1)
32 biidd 
_1 = a1 -> (x e. a -> x e. b <-> x e. a -> x e. b)
33 31, 32 imeqd 
_1 = a1 -> (x < _1 -> x e. a -> x e. b <-> x < a1 -> x e. a -> x e. b)
34 33 aleqd 
_1 = a1 -> (A. x (x < _1 -> x e. a -> x e. b) <-> A. x (x < a1 -> x e. a -> x e. b))
35 eqidd 
_1 = a1 -> a = a
36 eqidd 
_1 = a1 -> 2 = 2
37 36, 30 poweqd 
_1 = a1 -> 2 ^ _1 = 2 ^ a1
38 35, 37 modeqd 
_1 = a1 -> a % 2 ^ _1 = a % 2 ^ a1
39 eqidd 
_1 = a1 -> b = b
40 39, 37 modeqd 
_1 = a1 -> b % 2 ^ _1 = b % 2 ^ a1
41 38, 40 leeqd 
_1 = a1 -> (a % 2 ^ _1 <= b % 2 ^ _1 <-> a % 2 ^ a1 <= b % 2 ^ a1)
42 34, 41 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)
43 eqidd 
_1 = suc a1 -> x = x
44 id 
_1 = suc a1 -> _1 = suc a1
45 43, 44 lteqd 
_1 = suc a1 -> (x < _1 <-> x < suc a1)
46 biidd 
_1 = suc a1 -> (x e. a -> x e. b <-> x e. a -> x e. b)
47 45, 46 imeqd 
_1 = suc a1 -> (x < _1 -> x e. a -> x e. b <-> x < suc a1 -> x e. a -> x e. b)
48 47 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))
49 eqidd 
_1 = suc a1 -> a = a
50 eqidd 
_1 = suc a1 -> 2 = 2
51 50, 44 poweqd 
_1 = suc a1 -> 2 ^ _1 = 2 ^ suc a1
52 49, 51 modeqd 
_1 = suc a1 -> a % 2 ^ _1 = a % 2 ^ suc a1
53 eqidd 
_1 = suc a1 -> b = b
54 53, 51 modeqd 
_1 = suc a1 -> b % 2 ^ _1 = b % 2 ^ suc a1
55 52, 54 leeqd 
_1 = suc a1 -> (a % 2 ^ _1 <= b % 2 ^ _1 <-> a % 2 ^ suc a1 <= b % 2 ^ suc a1)
56 48, 55 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)
57 leeq1 
a % 2 ^ 0 = 0 -> (a % 2 ^ 0 <= b % 2 ^ 0 <-> 0 <= b % 2 ^ 0)
58 eqtr 
a % 2 ^ 0 = a % 1 -> a % 1 = 0 -> a % 2 ^ 0 = 0
59 modeq2 
2 ^ 0 = 1 -> a % 2 ^ 0 = a % 1
60 pow0 
2 ^ 0 = 1
61 59, 60 ax_mp 
a % 2 ^ 0 = a % 1
62 58, 61 ax_mp 
a % 1 = 0 -> a % 2 ^ 0 = 0
63 mod12 
a % 1 = 0
64 62, 63 ax_mp 
a % 2 ^ 0 = 0
65 57, 64 ax_mp 
a % 2 ^ 0 <= b % 2 ^ 0 <-> 0 <= b % 2 ^ 0
66 le01 
0 <= b % 2 ^ 0
67 65, 66 mpbir 
a % 2 ^ 0 <= b % 2 ^ 0
68 67 a1i 
A. x (x < 0 -> x e. a -> x e. b) -> a % 2 ^ 0 <= b % 2 ^ 0
69 ltsucid 
a1 < suc a1
70 lttr 
x < a1 -> a1 < suc a1 -> x < suc a1
71 69, 70 mpi 
x < a1 -> x < suc a1
72 71 imim1i 
(x < suc a1 -> x e. a -> x e. b) -> x < a1 -> x e. a -> x e. b
73 72 alimi 
A. x (x < suc a1 -> x e. a -> x e. b) -> A. x (x < a1 -> x e. a -> x e. b)
74 73 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
75 lteq1 
x = a1 -> (x < suc a1 <-> a1 < suc a1)
76 eleq1 
x = a1 -> (x e. a <-> a1 e. a)
77 eleq1 
x = a1 -> (x e. b <-> a1 e. b)
78 76, 77 imeqd 
x = a1 -> (x e. a -> x e. b <-> a1 e. a -> a1 e. b)
79 75, 78 imeqd 
x = a1 -> (x < suc a1 -> x e. a -> x e. b <-> a1 < suc a1 -> a1 e. a -> a1 e. b)
80 79 eale 
A. x (x < suc a1 -> x e. a -> x e. b) -> a1 < suc a1 -> a1 e. a -> a1 e. b
81 69, 80 mpi 
A. x (x < suc a1 -> x e. a -> x e. b) -> a1 e. a -> a1 e. b
82 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)
83 divmod 
2 ^ a1 * (a % 2 ^ suc a1 // 2 ^ a1) + a % 2 ^ suc a1 % 2 ^ a1 = a % 2 ^ suc a1
84 82, 83 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)
85 divmod 
2 ^ a1 * (b % 2 ^ suc a1 // 2 ^ a1) + b % 2 ^ suc a1 % 2 ^ a1 = b % 2 ^ suc a1
86 84, 85 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
87 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)
88 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
89 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)
90 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
91 diveq1 
a % 2 ^ suc a1 = a % (2 ^ a1 * 2) -> a % 2 ^ suc a1 // 2 ^ a1 = a % (2 ^ a1 * 2) // 2 ^ a1
92 modeq2 
2 ^ suc a1 = 2 ^ a1 * 2 -> a % 2 ^ suc a1 = a % (2 ^ a1 * 2)
93 powS2 
2 ^ suc a1 = 2 ^ a1 * 2
94 92, 93 ax_mp 
a % 2 ^ suc a1 = a % (2 ^ a1 * 2)
95 91, 94 ax_mp 
a % 2 ^ suc a1 // 2 ^ a1 = a % (2 ^ a1 * 2) // 2 ^ a1
96 90, 95 ax_mp 
a // 2 ^ a1 % 2 = a % (2 ^ a1 * 2) // 2 ^ a1 -> a % 2 ^ suc a1 // 2 ^ a1 = a // 2 ^ a1 % 2
97 divmod1 
a // 2 ^ a1 % 2 = a % (2 ^ a1 * 2) // 2 ^ a1
98 96, 97 ax_mp 
a % 2 ^ suc a1 // 2 ^ a1 = a // 2 ^ a1 % 2
99 89, 98 ax_mp 
2 ^ a1 * (a % 2 ^ suc a1 // 2 ^ a1) = 2 ^ a1 * (a // 2 ^ a1 % 2)
100 88, 99 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
101 modmod 
2 ^ a1 || 2 ^ suc a1 -> a % 2 ^ suc a1 % 2 ^ a1 = a % 2 ^ a1
102 powdvd 
a1 <= suc a1 -> 2 ^ a1 || 2 ^ suc a1
103 lesucid 
a1 <= suc a1
104 102, 103 ax_mp 
2 ^ a1 || 2 ^ suc a1
105 101, 104 ax_mp 
a % 2 ^ suc a1 % 2 ^ a1 = a % 2 ^ a1
106 100, 105 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
107 87, 106 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)
108 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
109 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)
110 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
111 diveq1 
b % 2 ^ suc a1 = b % (2 ^ a1 * 2) -> b % 2 ^ suc a1 // 2 ^ a1 = b % (2 ^ a1 * 2) // 2 ^ a1
112 modeq2 
2 ^ suc a1 = 2 ^ a1 * 2 -> b % 2 ^ suc a1 = b % (2 ^ a1 * 2)
113 112, 93 ax_mp 
b % 2 ^ suc a1 = b % (2 ^ a1 * 2)
114 111, 113 ax_mp 
b % 2 ^ suc a1 // 2 ^ a1 = b % (2 ^ a1 * 2) // 2 ^ a1
115 110, 114 ax_mp 
b // 2 ^ a1 % 2 = b % (2 ^ a1 * 2) // 2 ^ a1 -> b % 2 ^ suc a1 // 2 ^ a1 = b // 2 ^ a1 % 2
116 divmod1 
b // 2 ^ a1 % 2 = b % (2 ^ a1 * 2) // 2 ^ a1
117 115, 116 ax_mp 
b % 2 ^ suc a1 // 2 ^ a1 = b // 2 ^ a1 % 2
118 109, 117 ax_mp 
2 ^ a1 * (b % 2 ^ suc a1 // 2 ^ a1) = 2 ^ a1 * (b // 2 ^ a1 % 2)
119 108, 118 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
120 modmod 
2 ^ a1 || 2 ^ suc a1 -> b % 2 ^ suc a1 % 2 ^ a1 = b % 2 ^ a1
121 120, 104 ax_mp 
b % 2 ^ suc a1 % 2 ^ a1 = b % 2 ^ a1
122 119, 121 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
123 107, 122 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
124 lemul2a 
a // 2 ^ a1 % 2 <= b // 2 ^ a1 % 2 -> 2 ^ a1 * (a // 2 ^ a1 % 2) <= 2 ^ a1 * (b // 2 ^ a1 % 2)
125 letrueb 
bool (a // 2 ^ a1 % 2) -> (a // 2 ^ a1 % 2 <= b // 2 ^ a1 % 2 <-> true (a // 2 ^ a1 % 2) -> true (b // 2 ^ a1 % 2))
126 boolmod2 
bool (a // 2 ^ a1 % 2)
127 125, 126 ax_mp 
a // 2 ^ a1 % 2 <= b // 2 ^ a1 % 2 <-> true (a // 2 ^ a1 % 2) -> true (b // 2 ^ a1 % 2)
128 dfodd2 
odd (a // 2 ^ a1) <-> true (a // 2 ^ a1 % 2)
129 dfodd2 
odd (b // 2 ^ a1) <-> true (b // 2 ^ a1 % 2)
130 elnel 
a1 e. a <-> odd (shr a a1)
131 130 conv shr 
a1 e. a <-> odd (a // 2 ^ a1)
132 elnel 
a1 e. b <-> odd (shr b a1)
133 132 conv shr 
a1 e. b <-> odd (b // 2 ^ a1)
134 anl 
(a1 e. a -> a1 e. b) /\ a % 2 ^ a1 <= b % 2 ^ a1 -> a1 e. a -> a1 e. b
135 133, 134 syl6ib 
(a1 e. a -> a1 e. b) /\ a % 2 ^ a1 <= b % 2 ^ a1 -> a1 e. a -> odd (b // 2 ^ a1)
136 131, 135 syl5bir 
(a1 e. a -> a1 e. b) /\ a % 2 ^ a1 <= b % 2 ^ a1 -> odd (a // 2 ^ a1) -> odd (b // 2 ^ a1)
137 129, 136 syl6ib 
(a1 e. a -> a1 e. b) /\ a % 2 ^ a1 <= b % 2 ^ a1 -> odd (a // 2 ^ a1) -> true (b // 2 ^ a1 % 2)
138 128, 137 syl5bir 
(a1 e. a -> a1 e. b) /\ a % 2 ^ a1 <= b % 2 ^ a1 -> true (a // 2 ^ a1 % 2) -> true (b // 2 ^ a1 % 2)
139 127, 138 sylibr 
(a1 e. a -> a1 e. b) /\ a % 2 ^ a1 <= b % 2 ^ a1 -> a // 2 ^ a1 % 2 <= b // 2 ^ a1 % 2
140 124, 139 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)
141 anr 
(a1 e. a -> a1 e. b) /\ a % 2 ^ a1 <= b % 2 ^ a1 -> a % 2 ^ a1 <= b % 2 ^ a1
142 140, 141 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
143 123, 142 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
144 86, 143 sylib 
(a1 e. a -> a1 e. b) /\ a % 2 ^ a1 <= b % 2 ^ a1 -> a % 2 ^ suc a1 <= b % 2 ^ suc a1
145 144 exp 
(a1 e. a -> a1 e. b) -> a % 2 ^ a1 <= b % 2 ^ a1 -> a % 2 ^ suc a1 <= b % 2 ^ suc a1
146 81, 145 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
147 146 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
148 74, 147 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
149 14, 28, 42, 56, 68, 148 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)