Description: The converse to 2sq . (Contributed by Mario Carneiro, 20-Jun-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | 2sqb | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ne | |
|
2 | prmz | |
|
3 | 2 | ad3antrrr | |
4 | simplrr | |
|
5 | bezout | |
|
6 | 3 4 5 | syl2anc | |
7 | simplll | |
|
8 | simpllr | |
|
9 | simplr | |
|
10 | simprll | |
|
11 | simprlr | |
|
12 | simprr | |
|
13 | 7 8 9 10 11 12 | 2sqblem | |
14 | 13 | expr | |
15 | 14 | rexlimdvva | |
16 | 6 15 | mpd | |
17 | 16 | ex | |
18 | 17 | rexlimdvva | |
19 | 18 | impancom | |
20 | 1 19 | biimtrrid | |
21 | 20 | orrd | |
22 | 1z | |
|
23 | oveq1 | |
|
24 | sq1 | |
|
25 | 23 24 | eqtrdi | |
26 | 25 | oveq1d | |
27 | 26 | eqeq2d | |
28 | oveq1 | |
|
29 | 28 24 | eqtrdi | |
30 | 29 | oveq2d | |
31 | 1p1e2 | |
|
32 | 30 31 | eqtrdi | |
33 | 32 | eqeq2d | |
34 | 27 33 | rspc2ev | |
35 | 22 22 34 | mp3an12 | |
36 | 35 | adantl | |
37 | 2sq | |
|
38 | 36 37 | jaodan | |
39 | 21 38 | impbida | |