Proof of Theorem dalawlem3
Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. 2
|
2 | | dalawlem.l |
. 2
|
3 | | simp11 1091 |
. . 3
|
4 | | hllat 34650 |
. . 3
|
5 | 3, 4 | syl 17 |
. 2
|
6 | | simp22 1095 |
. . . . 5
|
7 | | simp32 1098 |
. . . . 5
|
8 | | dalawlem.j |
. . . . . 6
|
9 | | dalawlem.a |
. . . . . 6
|
10 | 1, 8, 9 | hlatjcl 34653 |
. . . . 5
|
11 | 3, 6, 7, 10 | syl3anc 1326 |
. . . 4
|
12 | | simp21 1094 |
. . . . 5
|
13 | 1, 9 | atbase 34576 |
. . . . 5
|
14 | 12, 13 | syl 17 |
. . . 4
|
15 | 1, 8 | latjcl 17051 |
. . . 4
|
16 | 5, 11, 14, 15 | syl3anc 1326 |
. . 3
|
17 | | simp31 1097 |
. . . 4
|
18 | 1, 9 | atbase 34576 |
. . . 4
|
19 | 17, 18 | syl 17 |
. . 3
|
20 | | dalawlem.m |
. . . 4
|
21 | 1, 20 | latmcl 17052 |
. . 3
|
22 | 5, 16, 19, 21 | syl3anc 1326 |
. 2
|
23 | | simp23 1096 |
. . . . 5
|
24 | 1, 8, 9 | hlatjcl 34653 |
. . . . 5
|
25 | 3, 6, 23, 24 | syl3anc 1326 |
. . . 4
|
26 | | simp33 1099 |
. . . . 5
|
27 | 1, 9 | atbase 34576 |
. . . . 5
|
28 | 26, 27 | syl 17 |
. . . 4
|
29 | 1, 20 | latmcl 17052 |
. . . 4
|
30 | 5, 25, 28, 29 | syl3anc 1326 |
. . 3
|
31 | 1, 8, 9 | hlatjcl 34653 |
. . . . 5
|
32 | 3, 23, 12, 31 | syl3anc 1326 |
. . . 4
|
33 | 1, 8, 9 | hlatjcl 34653 |
. . . . 5
|
34 | 3, 26, 17, 33 | syl3anc 1326 |
. . . 4
|
35 | 1, 20 | latmcl 17052 |
. . . 4
|
36 | 5, 32, 34, 35 | syl3anc 1326 |
. . 3
|
37 | 1, 8 | latjcl 17051 |
. . 3
|
38 | 5, 30, 36, 37 | syl3anc 1326 |
. 2
|
39 | 1, 8, 9 | hlatjcl 34653 |
. . . . 5
|
40 | 3, 7, 26, 39 | syl3anc 1326 |
. . . 4
|
41 | 1, 20 | latmcl 17052 |
. . . 4
|
42 | 5, 25, 40, 41 | syl3anc 1326 |
. . 3
|
43 | 1, 8 | latjcl 17051 |
. . 3
|
44 | 5, 42, 36, 43 | syl3anc 1326 |
. 2
|
45 | 1, 9 | atbase 34576 |
. . . . . . . . . 10
|
46 | 6, 45 | syl 17 |
. . . . . . . . 9
|
47 | 1, 20 | latmcl 17052 |
. . . . . . . . 9
|
48 | 5, 46, 28, 47 | syl3anc 1326 |
. . . . . . . 8
|
49 | 1, 8, 9 | hlatjcl 34653 |
. . . . . . . . . 10
|
50 | 3, 12, 17, 49 | syl3anc 1326 |
. . . . . . . . 9
|
51 | 1, 20 | latmcl 17052 |
. . . . . . . . 9
|
52 | 5, 50, 46, 51 | syl3anc 1326 |
. . . . . . . 8
|
53 | 1, 8 | latjcl 17051 |
. . . . . . . 8
|
54 | 5, 48, 52, 53 | syl3anc 1326 |
. . . . . . 7
|
55 | 1, 8 | latjcl 17051 |
. . . . . . 7
|
56 | 5, 14, 54, 55 | syl3anc 1326 |
. . . . . 6
|
57 | 1, 9 | atbase 34576 |
. . . . . . . . 9
|
58 | 23, 57 | syl 17 |
. . . . . . . 8
|
59 | 1, 8 | latjcl 17051 |
. . . . . . . 8
|
60 | 5, 58, 30, 59 | syl3anc 1326 |
. . . . . . 7
|
61 | 1, 8 | latjcl 17051 |
. . . . . . 7
|
62 | 5, 14, 60, 61 | syl3anc 1326 |
. . . . . 6
|
63 | 1, 8 | latjcl 17051 |
. . . . . . . . . . 11
|
64 | 5, 48, 14, 63 | syl3anc 1326 |
. . . . . . . . . 10
|
65 | 1, 2, 8, 20 | latmlej22 17093 |
. . . . . . . . . 10
|
66 | 5, 19, 16, 64, 65 | syl13anc 1328 |
. . . . . . . . 9
|
67 | 1, 8 | latjass 17095 |
. . . . . . . . . 10
|
68 | 5, 48, 14, 19, 67 | syl13anc 1328 |
. . . . . . . . 9
|
69 | 66, 68 | breqtrd 4679 |
. . . . . . . 8
|
70 | 1, 20 | latmcl 17052 |
. . . . . . . . . . 11
|
71 | 5, 11, 50, 70 | syl3anc 1326 |
. . . . . . . . . 10
|
72 | 1, 8 | latjcl 17051 |
. . . . . . . . . 10
|
73 | 5, 71, 14, 72 | syl3anc 1326 |
. . . . . . . . 9
|
74 | 1, 8, 9 | hlatjcl 34653 |
. . . . . . . . . 10
|
75 | 3, 12, 6, 74 | syl3anc 1326 |
. . . . . . . . 9
|
76 | 2, 8, 9 | hlatlej2 34662 |
. . . . . . . . . . . 12
|
77 | 3, 12, 17, 76 | syl3anc 1326 |
. . . . . . . . . . 11
|
78 | 1, 2, 20 | latmlem2 17082 |
. . . . . . . . . . . 12
|
79 | 5, 19, 50, 16, 78 | syl13anc 1328 |
. . . . . . . . . . 11
|
80 | 77, 79 | mpd 15 |
. . . . . . . . . 10
|
81 | 2, 8, 9 | hlatlej1 34661 |
. . . . . . . . . . . 12
|
82 | 3, 12, 17, 81 | syl3anc 1326 |
. . . . . . . . . . 11
|
83 | 1, 2, 8, 20, 9 | atmod4i1 35152 |
. . . . . . . . . . 11
|
84 | 3, 12, 11, 50, 82, 83 | syl131anc 1339 |
. . . . . . . . . 10
|
85 | 80, 84 | breqtrrd 4681 |
. . . . . . . . 9
|
86 | 1, 20 | latmcom 17075 |
. . . . . . . . . . . 12
|
87 | 5, 11, 50, 86 | syl3anc 1326 |
. . . . . . . . . . 11
|
88 | | simp12 1092 |
. . . . . . . . . . 11
|
89 | 87, 88 | eqbrtrd 4675 |
. . . . . . . . . 10
|
90 | 2, 8, 9 | hlatlej1 34661 |
. . . . . . . . . . 11
|
91 | 3, 12, 6, 90 | syl3anc 1326 |
. . . . . . . . . 10
|
92 | 1, 2, 8 | latjle12 17062 |
. . . . . . . . . . 11
|
93 | 5, 71, 14, 75, 92 | syl13anc 1328 |
. . . . . . . . . 10
|
94 | 89, 91, 93 | mpbi2and 956 |
. . . . . . . . 9
|
95 | 1, 2, 5, 22, 73, 75, 85, 94 | lattrd 17058 |
. . . . . . . 8
|
96 | 1, 8 | latjcl 17051 |
. . . . . . . . . 10
|
97 | 5, 48, 50, 96 | syl3anc 1326 |
. . . . . . . . 9
|
98 | 1, 2, 20 | latlem12 17078 |
. . . . . . . . 9
|
99 | 5, 22, 97, 75, 98 | syl13anc 1328 |
. . . . . . . 8
|
100 | 69, 95, 99 | mpbi2and 956 |
. . . . . . 7
|
101 | 1, 2, 8, 20, 9 | atmod3i1 35150 |
. . . . . . . . . 10
|
102 | 3, 12, 50, 46, 82, 101 | syl131anc 1339 |
. . . . . . . . 9
|
103 | 102 | oveq2d 6666 |
. . . . . . . 8
|
104 | 1, 8 | latj12 17096 |
. . . . . . . . 9
|
105 | 5, 48, 14, 52, 104 | syl13anc 1328 |
. . . . . . . 8
|
106 | 1, 2, 8, 20 | latmlej12 17091 |
. . . . . . . . . 10
|
107 | 5, 46, 28, 14, 106 | syl13anc 1328 |
. . . . . . . . 9
|
108 | 1, 2, 8, 20, 9 | atmod1i1m 35144 |
. . . . . . . . 9
|
109 | 3, 26, 46, 50, 75, 107, 108 | syl231anc 1346 |
. . . . . . . 8
|
110 | 103, 105,
109 | 3eqtr3rd 2665 |
. . . . . . 7
|
111 | 100, 110 | breqtrd 4679 |
. . . . . 6
|
112 | 2, 8, 9 | hlatlej1 34661 |
. . . . . . . . . 10
|
113 | 3, 6, 23, 112 | syl3anc 1326 |
. . . . . . . . 9
|
114 | 2, 8, 9 | hlatlej2 34662 |
. . . . . . . . . . 11
|
115 | 3, 23, 26, 114 | syl3anc 1326 |
. . . . . . . . . 10
|
116 | 1, 20 | latmcl 17052 |
. . . . . . . . . . . 12
|
117 | 5, 50, 11, 116 | syl3anc 1326 |
. . . . . . . . . . 11
|
118 | 1, 8, 9 | hlatjcl 34653 |
. . . . . . . . . . . 12
|
119 | 3, 23, 26, 118 | syl3anc 1326 |
. . . . . . . . . . 11
|
120 | 2, 8, 9 | hlatlej1 34661 |
. . . . . . . . . . . . 13
|
121 | 3, 6, 7, 120 | syl3anc 1326 |
. . . . . . . . . . . 12
|
122 | 1, 2, 20 | latmlem2 17082 |
. . . . . . . . . . . . 13
|
123 | 5, 46, 11, 50, 122 | syl13anc 1328 |
. . . . . . . . . . . 12
|
124 | 121, 123 | mpd 15 |
. . . . . . . . . . 11
|
125 | | simp13 1093 |
. . . . . . . . . . 11
|
126 | 1, 2, 5, 52, 117, 119, 124, 125 | lattrd 17058 |
. . . . . . . . . 10
|
127 | 1, 2, 8 | latjle12 17062 |
. . . . . . . . . . 11
|
128 | 5, 28, 52, 119, 127 | syl13anc 1328 |
. . . . . . . . . 10
|
129 | 115, 126,
128 | mpbi2and 956 |
. . . . . . . . 9
|
130 | 1, 8 | latjcl 17051 |
. . . . . . . . . . 11
|
131 | 5, 28, 52, 130 | syl3anc 1326 |
. . . . . . . . . 10
|
132 | 1, 2, 20 | latmlem12 17083 |
. . . . . . . . . 10
|
133 | 5, 46, 25, 131, 119, 132 | syl122anc 1335 |
. . . . . . . . 9
|
134 | 113, 129,
133 | mp2and 715 |
. . . . . . . 8
|
135 | 1, 2, 20 | latmle2 17077 |
. . . . . . . . . 10
|
136 | 5, 50, 46, 135 | syl3anc 1326 |
. . . . . . . . 9
|
137 | 1, 2, 8, 20, 9 | atmod2i2 35148 |
. . . . . . . . 9
|
138 | 3, 26, 46, 52, 136, 137 | syl131anc 1339 |
. . . . . . . 8
|
139 | 2, 8, 9 | hlatlej2 34662 |
. . . . . . . . . 10
|
140 | 3, 6, 23, 139 | syl3anc 1326 |
. . . . . . . . 9
|
141 | 1, 2, 8, 20, 9 | atmod3i2 35151 |
. . . . . . . . 9
|
142 | 3, 26, 58, 25, 140, 141 | syl131anc 1339 |
. . . . . . . 8
|
143 | 134, 138,
142 | 3brtr4d 4685 |
. . . . . . 7
|
144 | 1, 2, 8 | latjlej2 17066 |
. . . . . . . 8
|
145 | 5, 54, 60, 14, 144 | syl13anc 1328 |
. . . . . . 7
|
146 | 143, 145 | mpd 15 |
. . . . . 6
|
147 | 1, 2, 5, 22, 56, 62, 111, 146 | lattrd 17058 |
. . . . 5
|
148 | 1, 8 | latj13 17098 |
. . . . . 6
|
149 | 5, 14, 58, 30, 148 | syl13anc 1328 |
. . . . 5
|
150 | 147, 149 | breqtrd 4679 |
. . . 4
|
151 | 1, 2, 8, 20 | latmlej22 17093 |
. . . . 5
|
152 | 5, 19, 16, 28, 151 | syl13anc 1328 |
. . . 4
|
153 | 1, 8 | latjcl 17051 |
. . . . . 6
|
154 | 5, 30, 32, 153 | syl3anc 1326 |
. . . . 5
|
155 | 1, 2, 20 | latlem12 17078 |
. . . . 5
|
156 | 5, 22, 154, 34, 155 | syl13anc 1328 |
. . . 4
|
157 | 150, 152,
156 | mpbi2and 956 |
. . 3
|
158 | 1, 2, 8, 20 | latmlej21 17092 |
. . . . 5
|
159 | 5, 28, 25, 19, 158 | syl13anc 1328 |
. . . 4
|
160 | 1, 2, 8, 20, 9 | atmod1i1m 35144 |
. . . 4
|
161 | 3, 26, 25, 32, 34, 159, 160 | syl231anc 1346 |
. . 3
|
162 | 157, 161 | breqtrrd 4681 |
. 2
|
163 | 2, 8, 9 | hlatlej2 34662 |
. . . . 5
|
164 | 3, 7, 26, 163 | syl3anc 1326 |
. . . 4
|
165 | 1, 2, 20 | latmlem2 17082 |
. . . . 5
|
166 | 5, 28, 40, 25, 165 | syl13anc 1328 |
. . . 4
|
167 | 164, 166 | mpd 15 |
. . 3
|
168 | 1, 2, 8 | latjlej1 17065 |
. . . 4
|
169 | 5, 30, 42, 36, 168 | syl13anc 1328 |
. . 3
|
170 | 167, 169 | mpd 15 |
. 2
|
171 | 1, 2, 5, 22, 38, 44, 162, 170 | lattrd 17058 |
1
|