Metamath Proof Explorer


Theorem expdiophlem1

Description: Lemma for expdioph . Fully expanded expression for exponential. (Contributed by Stefan O'Rear, 17-Oct-2014)

Ref Expression
Assertion expdiophlem1 C 0 A 2 B C = A B d 0 e 0 f 0 A 2 B A 2 d = A Y rm B + 1 d 2 e = d Y rm B d 2 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C

Proof

Step Hyp Ref Expression
1 2re 2
2 1 a1i A 2 B 2
3 nnre B B
4 peano2re B B + 1
5 3 4 syl B B + 1
6 5 adantl A 2 B B + 1
7 nnz B B
8 7 peano2zd B B + 1
9 frmy Y rm : 2 ×
10 9 fovcl A 2 B + 1 A Y rm B + 1
11 8 10 sylan2 A 2 B A Y rm B + 1
12 11 zred A 2 B A Y rm B + 1
13 elnnuz B B 1
14 eluzp1p1 B 1 B + 1 1 + 1
15 df-2 2 = 1 + 1
16 15 fveq2i 2 = 1 + 1
17 14 16 eleqtrrdi B 1 B + 1 2
18 13 17 sylbi B B + 1 2
19 eluzle B + 1 2 2 B + 1
20 18 19 syl B 2 B + 1
21 20 adantl A 2 B 2 B + 1
22 nnnn0 B B 0
23 peano2nn0 B 0 B + 1 0
24 22 23 syl B B + 1 0
25 rmygeid A 2 B + 1 0 B + 1 A Y rm B + 1
26 24 25 sylan2 A 2 B B + 1 A Y rm B + 1
27 2 6 12 21 26 letrd A 2 B 2 A Y rm B + 1
28 2z 2
29 eluz 2 A Y rm B + 1 A Y rm B + 1 2 2 A Y rm B + 1
30 28 11 29 sylancr A 2 B A Y rm B + 1 2 2 A Y rm B + 1
31 27 30 mpbird A 2 B A Y rm B + 1 2
32 31 adantl C 0 A 2 B A Y rm B + 1 2
33 simprl C 0 A 2 B A 2
34 simprr C 0 A 2 B B
35 12 leidd A 2 B A Y rm B + 1 A Y rm B + 1
36 35 adantl C 0 A 2 B A Y rm B + 1 A Y rm B + 1
37 jm3.1 A Y rm B + 1 2 A 2 B A Y rm B + 1 A Y rm B + 1 A B = A Y rm B + 1 X rm B A Y rm B + 1 A A Y rm B + 1 Y rm B mod 2 A Y rm B + 1 A - A 2 - 1
38 32 33 34 36 37 syl31anc C 0 A 2 B A B = A Y rm B + 1 X rm B A Y rm B + 1 A A Y rm B + 1 Y rm B mod 2 A Y rm B + 1 A - A 2 - 1
39 38 eqeq2d C 0 A 2 B C = A B C = A Y rm B + 1 X rm B A Y rm B + 1 A A Y rm B + 1 Y rm B mod 2 A Y rm B + 1 A - A 2 - 1
40 7 adantl A 2 B B
41 frmx X rm : 2 × 0
42 41 fovcl A Y rm B + 1 2 B A Y rm B + 1 X rm B 0
43 31 40 42 syl2anc A 2 B A Y rm B + 1 X rm B 0
44 43 nn0zd A 2 B A Y rm B + 1 X rm B
45 eluzelz A 2 A
46 45 adantr A 2 B A
47 11 46 zsubcld A 2 B A Y rm B + 1 A
48 9 fovcl A Y rm B + 1 2 B A Y rm B + 1 Y rm B
49 31 40 48 syl2anc A 2 B A Y rm B + 1 Y rm B
50 47 49 zmulcld A 2 B A Y rm B + 1 A A Y rm B + 1 Y rm B
51 44 50 zsubcld A 2 B A Y rm B + 1 X rm B A Y rm B + 1 A A Y rm B + 1 Y rm B
52 51 adantl C 0 A 2 B A Y rm B + 1 X rm B A Y rm B + 1 A A Y rm B + 1 Y rm B
53 32 33 34 36 jm3.1lem3 C 0 A 2 B 2 A Y rm B + 1 A - A 2 - 1
54 simpl C 0 A 2 B C 0
55 divalgmodcl A Y rm B + 1 X rm B A Y rm B + 1 A A Y rm B + 1 Y rm B 2 A Y rm B + 1 A - A 2 - 1 C 0 C = A Y rm B + 1 X rm B A Y rm B + 1 A A Y rm B + 1 Y rm B mod 2 A Y rm B + 1 A - A 2 - 1 C < 2 A Y rm B + 1 A - A 2 - 1 2 A Y rm B + 1 A - A 2 - 1 A Y rm B + 1 X rm B - A Y rm B + 1 A A Y rm B + 1 Y rm B - C
56 52 53 54 55 syl3anc C 0 A 2 B C = A Y rm B + 1 X rm B A Y rm B + 1 A A Y rm B + 1 Y rm B mod 2 A Y rm B + 1 A - A 2 - 1 C < 2 A Y rm B + 1 A - A 2 - 1 2 A Y rm B + 1 A - A 2 - 1 A Y rm B + 1 X rm B - A Y rm B + 1 A A Y rm B + 1 Y rm B - C
57 39 56 bitrd C 0 A 2 B C = A B C < 2 A Y rm B + 1 A - A 2 - 1 2 A Y rm B + 1 A - A 2 - 1 A Y rm B + 1 X rm B - A Y rm B + 1 A A Y rm B + 1 Y rm B - C
58 rmynn0 A 2 B + 1 0 A Y rm B + 1 0
59 24 58 sylan2 A 2 B A Y rm B + 1 0
60 59 adantl C 0 A 2 B A Y rm B + 1 0
61 oveq1 d = A Y rm B + 1 d Y rm B = A Y rm B + 1 Y rm B
62 61 eqeq2d d = A Y rm B + 1 e = d Y rm B e = A Y rm B + 1 Y rm B
63 oveq1 d = A Y rm B + 1 d X rm B = A Y rm B + 1 X rm B
64 63 eqeq2d d = A Y rm B + 1 f = d X rm B f = A Y rm B + 1 X rm B
65 oveq2 d = A Y rm B + 1 2 d = 2 A Y rm B + 1
66 65 oveq1d d = A Y rm B + 1 2 d A = 2 A Y rm B + 1 A
67 66 oveq1d d = A Y rm B + 1 2 d A A 2 = 2 A Y rm B + 1 A A 2
68 67 oveq1d d = A Y rm B + 1 2 d A - A 2 - 1 = 2 A Y rm B + 1 A - A 2 - 1
69 68 breq2d d = A Y rm B + 1 C < 2 d A - A 2 - 1 C < 2 A Y rm B + 1 A - A 2 - 1
70 oveq1 d = A Y rm B + 1 d A = A Y rm B + 1 A
71 70 oveq1d d = A Y rm B + 1 d A e = A Y rm B + 1 A e
72 71 oveq2d d = A Y rm B + 1 f d A e = f A Y rm B + 1 A e
73 72 oveq1d d = A Y rm B + 1 f - d A e - C = f - A Y rm B + 1 A e - C
74 68 73 breq12d d = A Y rm B + 1 2 d A - A 2 - 1 f - d A e - C 2 A Y rm B + 1 A - A 2 - 1 f - A Y rm B + 1 A e - C
75 69 74 anbi12d d = A Y rm B + 1 C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C C < 2 A Y rm B + 1 A - A 2 - 1 2 A Y rm B + 1 A - A 2 - 1 f - A Y rm B + 1 A e - C
76 64 75 anbi12d d = A Y rm B + 1 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C f = A Y rm B + 1 X rm B C < 2 A Y rm B + 1 A - A 2 - 1 2 A Y rm B + 1 A - A 2 - 1 f - A Y rm B + 1 A e - C
77 76 rexbidv d = A Y rm B + 1 f 0 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C f 0 f = A Y rm B + 1 X rm B C < 2 A Y rm B + 1 A - A 2 - 1 2 A Y rm B + 1 A - A 2 - 1 f - A Y rm B + 1 A e - C
78 62 77 anbi12d d = A Y rm B + 1 e = d Y rm B f 0 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C e = A Y rm B + 1 Y rm B f 0 f = A Y rm B + 1 X rm B C < 2 A Y rm B + 1 A - A 2 - 1 2 A Y rm B + 1 A - A 2 - 1 f - A Y rm B + 1 A e - C
79 78 rexbidv d = A Y rm B + 1 e 0 e = d Y rm B f 0 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C e 0 e = A Y rm B + 1 Y rm B f 0 f = A Y rm B + 1 X rm B C < 2 A Y rm B + 1 A - A 2 - 1 2 A Y rm B + 1 A - A 2 - 1 f - A Y rm B + 1 A e - C
80 79 ceqsrexv A Y rm B + 1 0 d 0 d = A Y rm B + 1 e 0 e = d Y rm B f 0 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C e 0 e = A Y rm B + 1 Y rm B f 0 f = A Y rm B + 1 X rm B C < 2 A Y rm B + 1 A - A 2 - 1 2 A Y rm B + 1 A - A 2 - 1 f - A Y rm B + 1 A e - C
81 60 80 syl C 0 A 2 B d 0 d = A Y rm B + 1 e 0 e = d Y rm B f 0 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C e 0 e = A Y rm B + 1 Y rm B f 0 f = A Y rm B + 1 X rm B C < 2 A Y rm B + 1 A - A 2 - 1 2 A Y rm B + 1 A - A 2 - 1 f - A Y rm B + 1 A e - C
82 22 ad2antll C 0 A 2 B B 0
83 rmynn0 A Y rm B + 1 2 B 0 A Y rm B + 1 Y rm B 0
84 32 82 83 syl2anc C 0 A 2 B A Y rm B + 1 Y rm B 0
85 oveq2 e = A Y rm B + 1 Y rm B A Y rm B + 1 A e = A Y rm B + 1 A A Y rm B + 1 Y rm B
86 85 oveq2d e = A Y rm B + 1 Y rm B f A Y rm B + 1 A e = f A Y rm B + 1 A A Y rm B + 1 Y rm B
87 86 oveq1d e = A Y rm B + 1 Y rm B f - A Y rm B + 1 A e - C = f - A Y rm B + 1 A A Y rm B + 1 Y rm B - C
88 87 breq2d e = A Y rm B + 1 Y rm B 2 A Y rm B + 1 A - A 2 - 1 f - A Y rm B + 1 A e - C 2 A Y rm B + 1 A - A 2 - 1 f - A Y rm B + 1 A A Y rm B + 1 Y rm B - C
89 88 anbi2d e = A Y rm B + 1 Y rm B C < 2 A Y rm B + 1 A - A 2 - 1 2 A Y rm B + 1 A - A 2 - 1 f - A Y rm B + 1 A e - C C < 2 A Y rm B + 1 A - A 2 - 1 2 A Y rm B + 1 A - A 2 - 1 f - A Y rm B + 1 A A Y rm B + 1 Y rm B - C
90 89 anbi2d e = A Y rm B + 1 Y rm B f = A Y rm B + 1 X rm B C < 2 A Y rm B + 1 A - A 2 - 1 2 A Y rm B + 1 A - A 2 - 1 f - A Y rm B + 1 A e - C f = A Y rm B + 1 X rm B C < 2 A Y rm B + 1 A - A 2 - 1 2 A Y rm B + 1 A - A 2 - 1 f - A Y rm B + 1 A A Y rm B + 1 Y rm B - C
91 90 rexbidv e = A Y rm B + 1 Y rm B f 0 f = A Y rm B + 1 X rm B C < 2 A Y rm B + 1 A - A 2 - 1 2 A Y rm B + 1 A - A 2 - 1 f - A Y rm B + 1 A e - C f 0 f = A Y rm B + 1 X rm B C < 2 A Y rm B + 1 A - A 2 - 1 2 A Y rm B + 1 A - A 2 - 1 f - A Y rm B + 1 A A Y rm B + 1 Y rm B - C
92 91 ceqsrexv A Y rm B + 1 Y rm B 0 e 0 e = A Y rm B + 1 Y rm B f 0 f = A Y rm B + 1 X rm B C < 2 A Y rm B + 1 A - A 2 - 1 2 A Y rm B + 1 A - A 2 - 1 f - A Y rm B + 1 A e - C f 0 f = A Y rm B + 1 X rm B C < 2 A Y rm B + 1 A - A 2 - 1 2 A Y rm B + 1 A - A 2 - 1 f - A Y rm B + 1 A A Y rm B + 1 Y rm B - C
93 84 92 syl C 0 A 2 B e 0 e = A Y rm B + 1 Y rm B f 0 f = A Y rm B + 1 X rm B C < 2 A Y rm B + 1 A - A 2 - 1 2 A Y rm B + 1 A - A 2 - 1 f - A Y rm B + 1 A e - C f 0 f = A Y rm B + 1 X rm B C < 2 A Y rm B + 1 A - A 2 - 1 2 A Y rm B + 1 A - A 2 - 1 f - A Y rm B + 1 A A Y rm B + 1 Y rm B - C
94 7 ad2antll C 0 A 2 B B
95 32 94 42 syl2anc C 0 A 2 B A Y rm B + 1 X rm B 0
96 oveq1 f = A Y rm B + 1 X rm B f A Y rm B + 1 A A Y rm B + 1 Y rm B = A Y rm B + 1 X rm B A Y rm B + 1 A A Y rm B + 1 Y rm B
97 96 oveq1d f = A Y rm B + 1 X rm B f - A Y rm B + 1 A A Y rm B + 1 Y rm B - C = A Y rm B + 1 X rm B - A Y rm B + 1 A A Y rm B + 1 Y rm B - C
98 97 breq2d f = A Y rm B + 1 X rm B 2 A Y rm B + 1 A - A 2 - 1 f - A Y rm B + 1 A A Y rm B + 1 Y rm B - C 2 A Y rm B + 1 A - A 2 - 1 A Y rm B + 1 X rm B - A Y rm B + 1 A A Y rm B + 1 Y rm B - C
99 98 anbi2d f = A Y rm B + 1 X rm B C < 2 A Y rm B + 1 A - A 2 - 1 2 A Y rm B + 1 A - A 2 - 1 f - A Y rm B + 1 A A Y rm B + 1 Y rm B - C C < 2 A Y rm B + 1 A - A 2 - 1 2 A Y rm B + 1 A - A 2 - 1 A Y rm B + 1 X rm B - A Y rm B + 1 A A Y rm B + 1 Y rm B - C
100 99 ceqsrexv A Y rm B + 1 X rm B 0 f 0 f = A Y rm B + 1 X rm B C < 2 A Y rm B + 1 A - A 2 - 1 2 A Y rm B + 1 A - A 2 - 1 f - A Y rm B + 1 A A Y rm B + 1 Y rm B - C C < 2 A Y rm B + 1 A - A 2 - 1 2 A Y rm B + 1 A - A 2 - 1 A Y rm B + 1 X rm B - A Y rm B + 1 A A Y rm B + 1 Y rm B - C
101 95 100 syl C 0 A 2 B f 0 f = A Y rm B + 1 X rm B C < 2 A Y rm B + 1 A - A 2 - 1 2 A Y rm B + 1 A - A 2 - 1 f - A Y rm B + 1 A A Y rm B + 1 Y rm B - C C < 2 A Y rm B + 1 A - A 2 - 1 2 A Y rm B + 1 A - A 2 - 1 A Y rm B + 1 X rm B - A Y rm B + 1 A A Y rm B + 1 Y rm B - C
102 81 93 101 3bitrrd C 0 A 2 B C < 2 A Y rm B + 1 A - A 2 - 1 2 A Y rm B + 1 A - A 2 - 1 A Y rm B + 1 X rm B - A Y rm B + 1 A A Y rm B + 1 Y rm B - C d 0 d = A Y rm B + 1 e 0 e = d Y rm B f 0 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C
103 r19.42v f 0 d = A Y rm B + 1 e = d Y rm B f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C d = A Y rm B + 1 f 0 e = d Y rm B f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C
104 r19.42v f 0 e = d Y rm B f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C e = d Y rm B f 0 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C
105 104 anbi2i d = A Y rm B + 1 f 0 e = d Y rm B f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C d = A Y rm B + 1 e = d Y rm B f 0 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C
106 103 105 bitri f 0 d = A Y rm B + 1 e = d Y rm B f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C d = A Y rm B + 1 e = d Y rm B f 0 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C
107 106 rexbii e 0 f 0 d = A Y rm B + 1 e = d Y rm B f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C e 0 d = A Y rm B + 1 e = d Y rm B f 0 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C
108 r19.42v e 0 d = A Y rm B + 1 e = d Y rm B f 0 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C d = A Y rm B + 1 e 0 e = d Y rm B f 0 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C
109 107 108 bitri e 0 f 0 d = A Y rm B + 1 e = d Y rm B f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C d = A Y rm B + 1 e 0 e = d Y rm B f 0 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C
110 109 rexbii d 0 e 0 f 0 d = A Y rm B + 1 e = d Y rm B f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C d 0 d = A Y rm B + 1 e 0 e = d Y rm B f 0 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C
111 102 110 bitr4di C 0 A 2 B C < 2 A Y rm B + 1 A - A 2 - 1 2 A Y rm B + 1 A - A 2 - 1 A Y rm B + 1 X rm B - A Y rm B + 1 A A Y rm B + 1 Y rm B - C d 0 e 0 f 0 d = A Y rm B + 1 e = d Y rm B f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C
112 eleq1 d = A Y rm B + 1 d 2 A Y rm B + 1 2
113 32 112 syl5ibrcom C 0 A 2 B d = A Y rm B + 1 d 2
114 113 imp C 0 A 2 B d = A Y rm B + 1 d 2
115 ibar d 2 e = d Y rm B d 2 e = d Y rm B
116 ibar d 2 f = d X rm B d 2 f = d X rm B
117 116 anbi1d d 2 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C d 2 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C
118 115 117 anbi12d d 2 e = d Y rm B f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C d 2 e = d Y rm B d 2 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C
119 114 118 syl C 0 A 2 B d = A Y rm B + 1 e = d Y rm B f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C d 2 e = d Y rm B d 2 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C
120 119 pm5.32da C 0 A 2 B d = A Y rm B + 1 e = d Y rm B f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C d = A Y rm B + 1 d 2 e = d Y rm B d 2 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C
121 ibar A 2 d = A Y rm B + 1 A 2 d = A Y rm B + 1
122 121 ad2antrl C 0 A 2 B d = A Y rm B + 1 A 2 d = A Y rm B + 1
123 122 anbi1d C 0 A 2 B d = A Y rm B + 1 d 2 e = d Y rm B d 2 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C A 2 d = A Y rm B + 1 d 2 e = d Y rm B d 2 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C
124 120 123 bitrd C 0 A 2 B d = A Y rm B + 1 e = d Y rm B f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C A 2 d = A Y rm B + 1 d 2 e = d Y rm B d 2 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C
125 124 rexbidv C 0 A 2 B f 0 d = A Y rm B + 1 e = d Y rm B f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C f 0 A 2 d = A Y rm B + 1 d 2 e = d Y rm B d 2 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C
126 125 2rexbidv C 0 A 2 B d 0 e 0 f 0 d = A Y rm B + 1 e = d Y rm B f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C d 0 e 0 f 0 A 2 d = A Y rm B + 1 d 2 e = d Y rm B d 2 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C
127 111 126 bitrd C 0 A 2 B C < 2 A Y rm B + 1 A - A 2 - 1 2 A Y rm B + 1 A - A 2 - 1 A Y rm B + 1 X rm B - A Y rm B + 1 A A Y rm B + 1 Y rm B - C d 0 e 0 f 0 A 2 d = A Y rm B + 1 d 2 e = d Y rm B d 2 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C
128 57 127 bitrd C 0 A 2 B C = A B d 0 e 0 f 0 A 2 d = A Y rm B + 1 d 2 e = d Y rm B d 2 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C
129 128 pm5.32da C 0 A 2 B C = A B A 2 B d 0 e 0 f 0 A 2 d = A Y rm B + 1 d 2 e = d Y rm B d 2 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C
130 r19.42v f 0 A 2 B A 2 d = A Y rm B + 1 d 2 e = d Y rm B d 2 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C A 2 B f 0 A 2 d = A Y rm B + 1 d 2 e = d Y rm B d 2 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C
131 130 2rexbii d 0 e 0 f 0 A 2 B A 2 d = A Y rm B + 1 d 2 e = d Y rm B d 2 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C d 0 e 0 A 2 B f 0 A 2 d = A Y rm B + 1 d 2 e = d Y rm B d 2 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C
132 r19.42v e 0 A 2 B f 0 A 2 d = A Y rm B + 1 d 2 e = d Y rm B d 2 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C A 2 B e 0 f 0 A 2 d = A Y rm B + 1 d 2 e = d Y rm B d 2 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C
133 132 rexbii d 0 e 0 A 2 B f 0 A 2 d = A Y rm B + 1 d 2 e = d Y rm B d 2 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C d 0 A 2 B e 0 f 0 A 2 d = A Y rm B + 1 d 2 e = d Y rm B d 2 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C
134 r19.42v d 0 A 2 B e 0 f 0 A 2 d = A Y rm B + 1 d 2 e = d Y rm B d 2 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C A 2 B d 0 e 0 f 0 A 2 d = A Y rm B + 1 d 2 e = d Y rm B d 2 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C
135 133 134 bitri d 0 e 0 A 2 B f 0 A 2 d = A Y rm B + 1 d 2 e = d Y rm B d 2 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C A 2 B d 0 e 0 f 0 A 2 d = A Y rm B + 1 d 2 e = d Y rm B d 2 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C
136 131 135 bitri d 0 e 0 f 0 A 2 B A 2 d = A Y rm B + 1 d 2 e = d Y rm B d 2 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C A 2 B d 0 e 0 f 0 A 2 d = A Y rm B + 1 d 2 e = d Y rm B d 2 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C
137 129 136 bitr4di C 0 A 2 B C = A B d 0 e 0 f 0 A 2 B A 2 d = A Y rm B + 1 d 2 e = d Y rm B d 2 f = d X rm B C < 2 d A - A 2 - 1 2 d A - A 2 - 1 f - d A e - C