Step | Hyp | Ref
| Expression |
1 | | tgbtwncgr.p |
. . 3
|
2 | | tgbtwncgr.m |
. . 3
|
3 | | tgbtwncgr.i |
. . 3
Itv |
4 | | tgbtwncgr.g |
. . . 4
TarskiG |
5 | 4 | adantr 481 |
. . 3
TarskiG |
6 | | tgbtwncgr.b |
. . . 4
|
7 | 6 | adantr 481 |
. . 3
|
8 | | tgbtwncgr.d |
. . . 4
|
9 | 8 | adantr 481 |
. . 3
|
10 | | tgifscgr.f |
. . . 4
|
11 | 10 | adantr 481 |
. . 3
|
12 | | simpr 477 |
. . 3
|
13 | | tgifscgr.h |
. . . 4
|
14 | 13 | adantr 481 |
. . 3
|
15 | 1, 2, 3, 5, 7, 9, 11, 12, 14 | tgldim0cgr 25400 |
. 2
|
16 | | tgifscgr.6 |
. . . . 5
|
17 | 16 | ad2antrr 762 |
. . . 4
|
18 | 4 | ad2antrr 762 |
. . . . . 6
TarskiG |
19 | | tgbtwncgr.c |
. . . . . . 7
|
20 | 19 | ad2antrr 762 |
. . . . . 6
|
21 | 6 | ad2antrr 762 |
. . . . . 6
|
22 | | tgifscgr.1 |
. . . . . . . 8
|
23 | 22 | ad2antrr 762 |
. . . . . . 7
|
24 | | simpr 477 |
. . . . . . . 8
|
25 | 24 | oveq1d 6665 |
. . . . . . 7
|
26 | 23, 25 | eleqtrd 2703 |
. . . . . 6
|
27 | 1, 2, 3, 18, 20, 21, 26 | axtgbtwnid 25365 |
. . . . 5
|
28 | 27 | oveq1d 6665 |
. . . 4
|
29 | | tgifscgr.g |
. . . . . . 7
|
30 | 29 | ad2antrr 762 |
. . . . . 6
|
31 | 10 | ad2antrr 762 |
. . . . . 6
|
32 | | tgifscgr.2 |
. . . . . . . 8
|
33 | 32 | ad2antrr 762 |
. . . . . . 7
|
34 | | tgifscgr.e |
. . . . . . . . . 10
|
35 | 34 | ad2antrr 762 |
. . . . . . . . 9
|
36 | | tgbtwncgr.a |
. . . . . . . . . 10
|
37 | 36 | ad2antrr 762 |
. . . . . . . . 9
|
38 | 24 | oveq2d 6666 |
. . . . . . . . . 10
|
39 | | tgifscgr.3 |
. . . . . . . . . . 11
|
40 | 39 | ad2antrr 762 |
. . . . . . . . . 10
|
41 | 38, 40 | eqtr2d 2657 |
. . . . . . . . 9
|
42 | 1, 2, 3, 18, 35, 30, 37, 41 | axtgcgrid 25362 |
. . . . . . . 8
|
43 | 42 | oveq1d 6665 |
. . . . . . 7
|
44 | 33, 43 | eleqtrd 2703 |
. . . . . 6
|
45 | 1, 2, 3, 18, 30, 31, 44 | axtgbtwnid 25365 |
. . . . 5
|
46 | 45 | oveq1d 6665 |
. . . 4
|
47 | 17, 28, 46 | 3eqtr3d 2664 |
. . 3
|
48 | 4 | ad2antrr 762 |
. . . . . . . 8
TarskiG |
49 | 48 | ad2antrr 762 |
. . . . . . 7
TarskiG |
50 | 49 | ad2antrr 762 |
. . . . . 6
TarskiG |
51 | | simp-4r 807 |
. . . . . 6
|
52 | 19 | ad2antrr 762 |
. . . . . . . 8
|
53 | 52 | ad2antrr 762 |
. . . . . . 7
|
54 | 53 | ad2antrr 762 |
. . . . . 6
|
55 | 6 | ad6antr 772 |
. . . . . 6
|
56 | | simplr 792 |
. . . . . 6
|
57 | 29 | ad4antr 768 |
. . . . . . 7
|
58 | 57 | ad2antrr 762 |
. . . . . 6
|
59 | 10 | ad6antr 772 |
. . . . . 6
|
60 | 8 | ad6antr 772 |
. . . . . 6
|
61 | 13 | ad6antr 772 |
. . . . . 6
|
62 | | simpllr 799 |
. . . . . . . 8
|
63 | 62 | simprd 479 |
. . . . . . 7
|
64 | 63 | necomd 2849 |
. . . . . 6
|
65 | 36 | ad2antrr 762 |
. . . . . . . . 9
|
66 | 65 | ad4antr 768 |
. . . . . . . 8
|
67 | 22 | ad6antr 772 |
. . . . . . . 8
|
68 | 62 | simpld 475 |
. . . . . . . 8
|
69 | 1, 2, 3, 50, 66, 55, 54, 51, 67, 68 | tgbtwnexch3 25389 |
. . . . . . 7
|
70 | 1, 2, 3, 50, 55, 54, 51, 69 | tgbtwncom 25383 |
. . . . . 6
|
71 | 34 | ad6antr 772 |
. . . . . . . 8
|
72 | 32 | ad6antr 772 |
. . . . . . . 8
|
73 | | simprl 794 |
. . . . . . . 8
|
74 | 1, 2, 3, 50, 71, 59, 58, 56, 72, 73 | tgbtwnexch3 25389 |
. . . . . . 7
|
75 | 1, 2, 3, 50, 59, 58, 56, 74 | tgbtwncom 25383 |
. . . . . 6
|
76 | | simprr 796 |
. . . . . . . 8
|
77 | 76 | eqcomd 2628 |
. . . . . . 7
|
78 | 1, 2, 3, 50, 54, 51, 58, 56, 77 | tgcgrcomlr 25375 |
. . . . . 6
|
79 | | tgifscgr.4 |
. . . . . . . 8
|
80 | 79 | ad6antr 772 |
. . . . . . 7
|
81 | 1, 2, 3, 50, 55, 54, 59, 58, 80 | tgcgrcomlr 25375 |
. . . . . 6
|
82 | | simp-5r 809 |
. . . . . . 7
|
83 | 39 | ad6antr 772 |
. . . . . . 7
|
84 | | tgifscgr.5 |
. . . . . . . 8
|
85 | 84 | ad6antr 772 |
. . . . . . 7
|
86 | 16 | ad6antr 772 |
. . . . . . 7
|
87 | 1, 2, 3, 50, 66, 54, 51, 71, 58, 56, 60, 61, 82, 68, 73, 83, 77, 85, 86 | axtg5seg 25364 |
. . . . . 6
|
88 | 1, 2, 3, 50, 51, 54, 55, 56, 58, 59, 60, 61, 64, 70, 75, 78, 81, 87, 86 | axtg5seg 25364 |
. . . . 5
|
89 | 34 | ad4antr 768 |
. . . . . 6
|
90 | | simplr 792 |
. . . . . 6
|
91 | 1, 2, 3, 49, 89, 57, 53, 90 | axtgsegcon 25363 |
. . . . 5
|
92 | 88, 91 | r19.29a 3078 |
. . . 4
|
93 | | simplr 792 |
. . . . 5
|
94 | 1, 2, 3, 48, 65, 52, 93 | tgbtwndiff 25401 |
. . . 4
|
95 | 92, 94 | r19.29a 3078 |
. . 3
|
96 | 47, 95 | pm2.61dane 2881 |
. 2
|
97 | 1, 36 | tgldimor 25397 |
. 2
|
98 | 15, 96, 97 | mpjaodan 827 |
1
|