Step | Hyp | Ref
| Expression |
1 | | fvexd 6203 |
. 2
EEG |
2 | | simpl 473 |
. . . . . . 7
EEG EEG
|
3 | 2 | adantr 481 |
. . . . . 6
EEG EEG EEG
EEG
EEG |
4 | | simprl 794 |
. . . . . . . 8
EEG EEG
EEG |
5 | | eengbas 25861 |
. . . . . . . . 9
EEG |
6 | 5 | adantr 481 |
. . . . . . . 8
EEG EEG
EEG |
7 | 4, 6 | eleqtrrd 2704 |
. . . . . . 7
EEG EEG
|
8 | 7 | adantr 481 |
. . . . . 6
EEG EEG EEG
EEG
EEG |
9 | | simprr 796 |
. . . . . . . 8
EEG EEG
EEG |
10 | 9, 6 | eleqtrrd 2704 |
. . . . . . 7
EEG EEG
|
11 | 10 | adantr 481 |
. . . . . 6
EEG EEG EEG
EEG
EEG |
12 | 4 | adantr 481 |
. . . . . . 7
EEG EEG EEG
EEG
EEG EEG |
13 | 9 | adantr 481 |
. . . . . . 7
EEG EEG EEG
EEG
EEG EEG |
14 | | simpr1 1067 |
. . . . . . 7
EEG EEG EEG
EEG
EEG EEG |
15 | | simpr3 1069 |
. . . . . . . 8
EEG EEG
EEG EEG |
16 | 5 | adantr 481 |
. . . . . . . 8
EEG EEG
EEG EEG |
17 | 15, 16 | eleqtrrd 2704 |
. . . . . . 7
EEG EEG
EEG |
18 | 3, 12, 13, 14, 17 | syl13anc 1328 |
. . . . . 6
EEG EEG EEG
EEG
EEG |
19 | | simpr2 1068 |
. . . . . . 7
EEG EEG EEG
EEG
EEG EEG |
20 | 5 | ad2antrr 762 |
. . . . . . 7
EEG EEG EEG
EEG
EEG EEG |
21 | 19, 20 | eleqtrrd 2704 |
. . . . . 6
EEG EEG EEG
EEG
EEG |
22 | | simpr3 1069 |
. . . . . . 7
EEG EEG EEG
EEG
EEG EEG |
23 | 22, 20 | eleqtrrd 2704 |
. . . . . 6
EEG EEG EEG
EEG
EEG |
24 | | axeuclid 25843 |
. . . . . 6
|
25 | 3, 8, 11, 18, 21, 23, 24 | syl132anc 1344 |
. . . . 5
EEG EEG EEG
EEG
EEG
|
26 | | eqid 2622 |
. . . . . . 7
EEG EEG |
27 | | eqid 2622 |
. . . . . . 7
ItvEEG ItvEEG |
28 | 3, 26, 27, 12, 22, 19 | ebtwntg 25862 |
. . . . . 6
EEG EEG EEG
EEG
EEG ItvEEG |
29 | 3, 26, 27, 13, 14, 19 | ebtwntg 25862 |
. . . . . 6
EEG EEG EEG
EEG
EEG ItvEEG |
30 | 28, 29 | 3anbi12d 1400 |
. . . . 5
EEG EEG EEG
EEG
EEG
ItvEEG ItvEEG |
31 | 20 | adantr 481 |
. . . . . . 7
EEG
EEG EEG EEG
EEG
EEG |
32 | 3 | ad2antrr 762 |
. . . . . . . . 9
EEG
EEG EEG
EEG
EEG |
33 | 12 | ad2antrr 762 |
. . . . . . . . 9
EEG
EEG EEG
EEG
EEG EEG |
34 | | simpr 477 |
. . . . . . . . . . 11
EEG
EEG EEG EEG
EEG
|
35 | 34, 31 | eleqtrd 2703 |
. . . . . . . . . 10
EEG
EEG EEG EEG
EEG
EEG |
36 | 35 | adantr 481 |
. . . . . . . . 9
EEG
EEG EEG
EEG
EEG EEG |
37 | 13 | ad2antrr 762 |
. . . . . . . . 9
EEG
EEG EEG
EEG
EEG EEG |
38 | 32, 26, 27, 33, 36, 37 | ebtwntg 25862 |
. . . . . . . 8
EEG
EEG EEG
EEG
EEG
ItvEEG |
39 | | simpr 477 |
. . . . . . . . . 10
EEG
EEG EEG
EEG
EEG |
40 | 20 | ad2antrr 762 |
. . . . . . . . . 10
EEG
EEG EEG
EEG
EEG EEG |
41 | 39, 40 | eleqtrd 2703 |
. . . . . . . . 9
EEG
EEG EEG
EEG
EEG EEG |
42 | 14 | ad2antrr 762 |
. . . . . . . . 9
EEG
EEG EEG
EEG
EEG EEG |
43 | 32, 26, 27, 33, 41, 42 | ebtwntg 25862 |
. . . . . . . 8
EEG
EEG EEG
EEG
EEG
ItvEEG |
44 | 22 | ad2antrr 762 |
. . . . . . . . 9
EEG
EEG EEG
EEG
EEG EEG |
45 | 32, 26, 27, 36, 41, 44 | ebtwntg 25862 |
. . . . . . . 8
EEG
EEG EEG
EEG
EEG
ItvEEG |
46 | 38, 43, 45 | 3anbi123d 1399 |
. . . . . . 7
EEG
EEG EEG
EEG
EEG ItvEEG ItvEEG ItvEEG |
47 | 31, 46 | rexeqbidva 3155 |
. . . . . 6
EEG
EEG EEG EEG
EEG
EEG ItvEEG ItvEEG ItvEEG |
48 | 20, 47 | rexeqbidva 3155 |
. . . . 5
EEG EEG EEG
EEG
EEG
EEG EEG ItvEEG ItvEEG ItvEEG |
49 | 25, 30, 48 | 3imtr3d 282 |
. . . 4
EEG EEG EEG
EEG
EEG ItvEEG ItvEEG EEG EEG ItvEEG ItvEEG ItvEEG |
50 | 49 | ralrimivvva 2972 |
. . 3
EEG EEG
EEG
EEG EEG ItvEEG ItvEEG EEG EEG ItvEEG ItvEEG ItvEEG |
51 | 50 | ralrimivva 2971 |
. 2
EEG
EEG EEG
EEG EEG ItvEEG ItvEEG EEG EEG ItvEEG ItvEEG ItvEEG |
52 | | eqid 2622 |
. . 3
EEG EEG |
53 | 26, 52, 27 | istrkge 25356 |
. 2
EEG TarskiGE
EEG EEG EEG
EEG EEG
EEG ItvEEG ItvEEG EEG EEG ItvEEG ItvEEG ItvEEG |
54 | 1, 51, 53 | sylanbrc 698 |
1
EEG TarskiGE |