Description: The geometry structure for EE ^ N is a Euclidean geometry. (Contributed by Thierry Arnoux, 15-Mar-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | eengtrkge | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fvexd | |
|
2 | simpll | |
|
3 | simprl | |
|
4 | eengbas | |
|
5 | 4 | adantr | |
6 | 3 5 | eleqtrrd | |
7 | 6 | adantr | |
8 | simprr | |
|
9 | 8 5 | eleqtrrd | |
10 | 9 | adantr | |
11 | 3 | adantr | |
12 | 8 | adantr | |
13 | simpr1 | |
|
14 | simpr3 | |
|
15 | 4 | adantr | |
16 | 14 15 | eleqtrrd | |
17 | 2 11 12 13 16 | syl13anc | |
18 | simpr2 | |
|
19 | 4 | ad2antrr | |
20 | 18 19 | eleqtrrd | |
21 | simpr3 | |
|
22 | 21 19 | eleqtrrd | |
23 | axeuclid | |
|
24 | 2 7 10 17 20 22 23 | syl132anc | |
25 | eqid | |
|
26 | eqid | |
|
27 | 2 25 26 11 21 18 | ebtwntg | |
28 | 2 25 26 12 13 18 | ebtwntg | |
29 | 27 28 | 3anbi12d | |
30 | 19 | adantr | |
31 | 2 | ad2antrr | |
32 | 11 | ad2antrr | |
33 | simpr | |
|
34 | 33 30 | eleqtrd | |
35 | 34 | adantr | |
36 | 12 | ad2antrr | |
37 | 31 25 26 32 35 36 | ebtwntg | |
38 | simpr | |
|
39 | 19 | ad2antrr | |
40 | 38 39 | eleqtrd | |
41 | 13 | ad2antrr | |
42 | 31 25 26 32 40 41 | ebtwntg | |
43 | 21 | ad2antrr | |
44 | 31 25 26 35 40 43 | ebtwntg | |
45 | 37 42 44 | 3anbi123d | |
46 | 30 45 | rexeqbidva | |
47 | 19 46 | rexeqbidva | |
48 | 24 29 47 | 3imtr3d | |
49 | 48 | ralrimivvva | |
50 | 49 | ralrimivva | |
51 | eqid | |
|
52 | 25 51 26 | istrkge | |
53 | 1 50 52 | sylanbrc | |