Step |
Hyp |
Ref |
Expression |
1 |
|
simplll |
|
2 |
|
nnre |
|
3 |
2
|
ad3antlr |
|
4 |
|
prmz |
|
5 |
4
|
zred |
|
6 |
5
|
ad2antlr |
|
7 |
|
simprl |
|
8 |
|
simprr |
|
9 |
1 3 6 7 8
|
lttrd |
|
10 |
|
arch |
|
11 |
|
prmunb |
|
12 |
11
|
rgen |
|
13 |
|
r19.29r |
|
14 |
10 12 13
|
sylancl |
|
15 |
|
r19.42v |
|
16 |
15
|
rexbii |
|
17 |
14 16
|
sylibr |
|
18 |
9 17
|
reximddv2 |
|
19 |
|
1nn |
|
20 |
|
ne0i |
|
21 |
|
r19.9rzv |
|
22 |
19 20 21
|
mp2b |
|
23 |
18 22
|
sylibr |
|