Quantum Logic Explorer		< Previous   Next > Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  vneulemexp		Unicode version

---

Theorem vneulemexp 1146

Description: Expanded version of vneulem 1145.

Hypothesis

Ref	Expression
vneulemexp.1

Assertion

Ref	Expression
vneulemexp

---

Proof of Theorem vneulemexp

Step	Hyp	Ref	Expression
1		ax-a2 31	. . . . . . 7
2	1	ax-r5 38	. . . . . 6
3		or32 82	. . . . . 6
4	2, 3	2an 79	. . . . 5
5		orcom 73	. . . . . . . . . . . 12
6	5	ror 71	. . . . . . . . . . 11
7		or32 82	. . . . . . . . . . 11
8	6, 7	tr 62	. . . . . . . . . 10
9		or32 82	. . . . . . . . . 10
10	8, 9	2an 79	. . . . . . . . 9
11		ancom 74	. . . . . . . . . 10
12		ml 1121	. . . . . . . . . . 11
13	12	cm 61	. . . . . . . . . 10
14		ancom 74	. . . . . . . . . . 11
15	14	lor 70	. . . . . . . . . 10
16	11, 13, 15	3tr 65	. . . . . . . . 9
17	10, 16	ax-r2 36	. . . . . . . 8
18		leor 159	. . . . . . . . 9
19		or32 82	. . . . . . . . . . . 12
20	19	ran 78	. . . . . . . . . . 11
21		leor 159	. . . . . . . . . . . . . . 15
22		leid 148	. . . . . . . . . . . . . . 15
23	21, 22	ler2an 173	. . . . . . . . . . . . . 14
24		lear 161	. . . . . . . . . . . . . 14
25	23, 24	lebi 145	. . . . . . . . . . . . 13
26	25	lan 77	. . . . . . . . . . . 12
27		anass 76	. . . . . . . . . . . . . 14
28	27	cm 61	. . . . . . . . . . . . 13
29		ax-a2 31	. . . . . . . . . . . . . . . 16
30	29	ran 78	. . . . . . . . . . . . . . 15
31		ml 1121	. . . . . . . . . . . . . . . 16
32	31	cm 61	. . . . . . . . . . . . . . 15
33		orcom 73	. . . . . . . . . . . . . . 15
34	30, 32, 33	3tr 65	. . . . . . . . . . . . . 14
35	34	ran 78	. . . . . . . . . . . . 13
36	28, 35	tr 62	. . . . . . . . . . . 12
37		vneulemexp.1	. . . . . . . . . . . . . . 15
38	37	ror 71	. . . . . . . . . . . . . 14
39		or0r 103	. . . . . . . . . . . . . 14
40	38, 39	tr 62	. . . . . . . . . . . . 13
41	40	ran 78	. . . . . . . . . . . 12
42	26, 36, 41	3tr 65	. . . . . . . . . . 11
43	20, 42	tr 62	. . . . . . . . . 10
44		leao3 164	. . . . . . . . . . 11
45	44	lerr 150	. . . . . . . . . 10
46	43, 45	bltr 138	. . . . . . . . 9
47	18, 46	lel2or 170	. . . . . . . 8
48	17, 47	bltr 138	. . . . . . 7
49		leao2 163	. . . . . . . . . 10
50	49	ler 149	. . . . . . . . 9
51		leor 159	. . . . . . . . . 10
52	51	leror 152	. . . . . . . . 9
53	50, 52	lel2or 170	. . . . . . . 8
54		leao3 164	. . . . . . . . . 10
55	54	ler 149	. . . . . . . . 9
56		leo 158	. . . . . . . . . 10
57	56	leror 152	. . . . . . . . 9
58	55, 57	lel2or 170	. . . . . . . 8
59	53, 58	ler2an 173	. . . . . . 7
60	48, 59	lebi 145	. . . . . 6
61		leao1 162	. . . . . . . . . . 11
62	49, 61	ler2an 173	. . . . . . . . . 10
63		orcom 73	. . . . . . . . . . . 12
64	5, 63	2an 79	. . . . . . . . . . 11
65	64, 37	tr 62	. . . . . . . . . 10
66	62, 65	lbtr 139	. . . . . . . . 9
67		le0 147	. . . . . . . . 9
68	66, 67	lebi 145	. . . . . . . 8
69	68	ror 71	. . . . . . 7
70		or0r 103	. . . . . . 7
71	69, 70	tr 62	. . . . . 6
72	60, 71	tr 62	. . . . 5
73	4, 72	tr 62	. . . 4
74		orcom 73	. . . . . . . . . . 11
75	74	ror 71	. . . . . . . . . 10
76		or32 82	. . . . . . . . . 10
77	75, 76	tr 62	. . . . . . . . 9
78		or32 82	. . . . . . . . 9
79	77, 78	2an 79	. . . . . . . 8
80		ancom 74	. . . . . . . . 9
81		ml 1121	. . . . . . . . . 10
82	81	cm 61	. . . . . . . . 9
83		ancom 74	. . . . . . . . . 10
84	83	lor 70	. . . . . . . . 9
85	80, 82, 84	3tr 65	. . . . . . . 8
86	79, 85	ax-r2 36	. . . . . . 7
87		leor 159	. . . . . . . 8
88		or32 82	. . . . . . . . . . 11
89	88	ran 78	. . . . . . . . . 10
90		leor 159	. . . . . . . . . . . . . 14
91		leid 148	. . . . . . . . . . . . . 14
92	90, 91	ler2an 173	. . . . . . . . . . . . 13
93		lear 161	. . . . . . . . . . . . 13
94	92, 93	lebi 145	. . . . . . . . . . . 12
95	94	lan 77	. . . . . . . . . . 11
96		anass 76	. . . . . . . . . . . . 13
97	96	cm 61	. . . . . . . . . . . 12
98		ax-a2 31	. . . . . . . . . . . . . . 15
99	98	ran 78	. . . . . . . . . . . . . 14
100		ml 1121	. . . . . . . . . . . . . . 15
101	100	cm 61	. . . . . . . . . . . . . 14
102		orcom 73	. . . . . . . . . . . . . 14
103	99, 101, 102	3tr 65	. . . . . . . . . . . . 13
104	103	ran 78	. . . . . . . . . . . 12
105	97, 104	tr 62	. . . . . . . . . . 11
106	65	ror 71	. . . . . . . . . . . . 13
107		or0r 103	. . . . . . . . . . . . 13
108	106, 107	tr 62	. . . . . . . . . . . 12
109	108	ran 78	. . . . . . . . . . 11
110	95, 105, 109	3tr 65	. . . . . . . . . 10
111	89, 110	tr 62	. . . . . . . . 9
112		leao3 164	. . . . . . . . . 10
113	112	lerr 150	. . . . . . . . 9
114	111, 113	bltr 138	. . . . . . . 8
115	87, 114	lel2or 170	. . . . . . 7
116	86, 115	bltr 138	. . . . . 6
117		leao2 163	. . . . . . . . 9
118	117	ler 149	. . . . . . . 8
119		leor 159	. . . . . . . . 9
120	119	leror 152	. . . . . . . 8
121	118, 120	lel2or 170	. . . . . . 7
122		leao3 164	. . . . . . . . 9
123	122	ler 149	. . . . . . . 8
124		leo 158	. . . . . . . . 9
125	124	leror 152	. . . . . . . 8
126	123, 125	lel2or 170	. . . . . . 7
127	121, 126	ler2an 173	. . . . . 6
128	116, 127	lebi 145	. . . . 5
129		leao1 162	. . . . . . . . . 10
130	117, 129	ler2an 173	. . . . . . . . 9
131	130, 37	lbtr 139	. . . . . . . 8
132		le0 147	. . . . . . . 8
133	131, 132	lebi 145	. . . . . . 7
134	133	ror 71	. . . . . 6
135		or0r 103	. . . . . 6
136	134, 135	tr 62	. . . . 5
137	128, 136	tr 62	. . . 4
138	73, 137	2an 79	. . 3
139	138	cm 61	. 2
140		ancom 74	. . 3
141		an4 86	. . . 4
142		ancom 74	. . . . . . 7
143		ancom 74	. . . . . . . 8
144		ml 1121	. . . . . . . . 9
145	144	cm 61	. . . . . . . 8
146		ancom 74	. . . . . . . . 9
147	146	lor 70	. . . . . . . 8
148	143, 145, 147	3tr 65	. . . . . . 7
149	142, 148	ax-r2 36	. . . . . 6
150		orcom 73	. . . . . 6
151	42	ror 71	. . . . . 6
152	149, 150, 151	3tr 65	. . . . 5
153		ax-a3 32	. . . . . . . 8
154		orcom 73	. . . . . . . 8
155	153, 154	tr 62	. . . . . . 7
156		ax-a2 31	. . . . . . . . 9
157	156	ror 71	. . . . . . . 8
158		or32 82	. . . . . . . 8
159	157, 158	tr 62	. . . . . . 7
160	155, 159	2an 79	. . . . . 6
161		ancom 74	. . . . . . . 8
162		ancom 74	. . . . . . . . 9
163		ml 1121	. . . . . . . . . 10
164	163	cm 61	. . . . . . . . 9
165		ancom 74	. . . . . . . . . 10
166	165	lor 70	. . . . . . . . 9
167	162, 164, 166	3tr 65	. . . . . . . 8
168	161, 167	ax-r2 36	. . . . . . 7
169		orcom 73	. . . . . . 7
170		leid 148	. . . . . . . . . . . 12
171	119, 170	ler2an 173	. . . . . . . . . . 11
172		lear 161	. . . . . . . . . . 11
173	171, 172	lebi 145	. . . . . . . . . 10
174	173	lan 77	. . . . . . . . 9
175		anass 76	. . . . . . . . . . 11
176	175	cm 61	. . . . . . . . . 10
177		ax-a2 31	. . . . . . . . . . . . 13
178	177	ran 78	. . . . . . . . . . . 12
179		ml 1121	. . . . . . . . . . . . 13
180	179	cm 61	. . . . . . . . . . . 12
181		orcom 73	. . . . . . . . . . . 12
182	178, 180, 181	3tr 65	. . . . . . . . . . 11
183	182	ran 78	. . . . . . . . . 10
184	176, 183	tr 62	. . . . . . . . 9
185		ancom 74	. . . . . . . . . . . . 13
186	185, 37	tr 62	. . . . . . . . . . . 12
187	186	ror 71	. . . . . . . . . . 11
188		or0r 103	. . . . . . . . . . 11
189	187, 188	tr 62	. . . . . . . . . 10
190	189	ran 78	. . . . . . . . 9
191	174, 184, 190	3tr 65	. . . . . . . 8
192	191	ror 71	. . . . . . 7
193	168, 169, 192	3tr 65	. . . . . 6
194		orcom 73	. . . . . 6
195	160, 193, 194	3tr 65	. . . . 5
196	152, 195	2an 79	. . . 4
197	141, 196	tr 62	. . 3
198		ml 1121	. . . . . . 7
199	198	cm 61	. . . . . 6
200		orass 75	. . . . . . . . 9
201	200	cm 61	. . . . . . . 8
202		leao1 162	. . . . . . . . . 10
203	202	df-le2 131	. . . . . . . . 9
204	203	ror 71	. . . . . . . 8
205	201, 204	tr 62	. . . . . . 7
206	205	lan 77	. . . . . 6
207	205	lan 77	. . . . . . 7
208	207	lor 70	. . . . . 6
209	199, 206, 208	3tr2 64	. . . . 5
210		leao1 162	. . . . . . . . . . 11
211		leid 148	. . . . . . . . . . 11
212	210, 211	ler2an 173	. . . . . . . . . 10
213		lear 161	. . . . . . . . . 10
214	212, 213	lebi 145	. . . . . . . . 9
215	214	lor 70	. . . . . . . 8
216	215	lan 77	. . . . . . 7
217		mldual 1122	. . . . . . 7
218	213, 212	lebi 145	. . . . . . . . 9
219	37, 218	2or 72	. . . . . . . 8
220		or0r 103	. . . . . . . 8
221	219, 220	tr 62	. . . . . . 7
222	216, 217, 221	3tr 65	. . . . . 6
223	222	lor 70	. . . . 5
224	209, 223	tr 62	. . . 4
225		orcom 73	. . . 4
226	224, 225	tr 62	. . 3
227	140, 197, 226	3tr 65	. 2
228	139, 227	tr 62	1

Colors of variables: term

Syntax hints:   wb 1   wo 6   wa 7  wf 9

This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-ml 1120

This theorem depends on definitions:  df-a 40  df-t 41  df-f 42  df-le1 130  df-le2 131

This theorem is referenced by: (None)

Copyright terms: Public domain

W3C validator