Theorem negantlem10 843

Description: Lemma for negated antecedent identity.

Hypothesis

Ref	Expression
negant.1	(a ->1 c) = (b ->1 c)

Assertion

Ref	Expression
negantlem10	(a ->4 c) =< (b ->4 c)

Proof of Theorem negantlem10

Step	Hyp	Ref	Expression
1		leao4 157	. . . . 5 (a ^ c) =< (b_|_ v c)
2		leor 151	. . . . . . . 8 (a ^ c) =< (a_|_ v (a ^ c))
3		df-i1 43	. . . . . . . . 9 (a ->1 c) = (a_|_ v (a ^ c))
4	3	ax-r1 34	. . . . . . . 8 (a_|_ v (a ^ c)) = (a ->1 c)
5	2, 4	lbtr 131	. . . . . . 7 (a ^ c) =< (a ->1 c)
6		lear 153	. . . . . . 7 (a ^ c) =< c
7	5, 6	ler2an 165	. . . . . 6 (a ^ c) =< ((a ->1 c) ^ c)
8		negant.1	. . . . . . . 8 (a ->1 c) = (b ->1 c)
9	8	ran 71	. . . . . . 7 ((a ->1 c) ^ c) = ((b ->1 c) ^ c)
10		u1lemab 592	. . . . . . . 8 ((b ->1 c) ^ c) = ((b ^ c) v (b_|_ ^ c))
11		leor 151	. . . . . . . . 9 ((b ^ c) v (b_|_ ^ c)) =< (c_|_ v ((b ^ c) v (b_|_ ^ c)))
12		ancom 68	. . . . . . . . . . . . 13 (b ^ c) = (c ^ b)
13		ancom 68	. . . . . . . . . . . . 13 (b_|_ ^ c) = (c ^ b_|_)
14	12, 13	2or 67	. . . . . . . . . . . 12 ((b ^ c) v (b_|_ ^ c)) = ((c ^ b) v (c ^ b_|_))
15		ax-a2 30	. . . . . . . . . . . 12 ((c ^ b) v (c ^ b_|_)) = ((c ^ b_|_) v (c ^ b))
16	14, 15	ax-r2 35	. . . . . . . . . . 11 ((b ^ c) v (b_|_ ^ c)) = ((c ^ b_|_) v (c ^ b))
17	16	lor 66	. . . . . . . . . 10 (c_|_ v ((b ^ c) v (b_|_ ^ c))) = (c_|_ v ((c ^ b_|_) v (c ^ b)))
18		ax-a3 31	. . . . . . . . . . 11 ((c_|_ v (c ^ b_|_)) v (c ^ b)) = (c_|_ v ((c ^ b_|_) v (c ^ b)))
19	18	ax-r1 34	. . . . . . . . . 10 (c_|_ v ((c ^ b_|_) v (c ^ b))) = ((c_|_ v (c ^ b_|_)) v (c ^ b))
20	17, 19	ax-r2 35	. . . . . . . . 9 (c_|_ v ((b ^ c) v (b_|_ ^ c))) = ((c_|_ v (c ^ b_|_)) v (c ^ b))
21	11, 20	lbtr 131	. . . . . . . 8 ((b ^ c) v (b_|_ ^ c)) =< ((c_|_ v (c ^ b_|_)) v (c ^ b))
22	10, 21	bltr 130	. . . . . . 7 ((b ->1 c) ^ c) =< ((c_|_ v (c ^ b_|_)) v (c ^ b))
23	9, 22	bltr 130	. . . . . 6 ((a ->1 c) ^ c) =< ((c_|_ v (c ^ b_|_)) v (c ^ b))
24	7, 23	letr 129	. . . . 5 (a ^ c) =< ((c_|_ v (c ^ b_|_)) v (c ^ b))
25	1, 24	ler2an 165	. . . 4 (a ^ c) =< ((b_|_ v c) ^ ((c_|_ v (c ^ b_|_)) v (c ^ b)))
26		leao4 157	. . . . 5 (a_|_ ^ c) =< (b_|_ v c)
27		leor 151	. . . . . . . 8 (a_|_ ^ c) =< (a_|__|_ v (a_|_ ^ c))
28		df-i1 43	. . . . . . . . 9 (a_|_ ->1 c) = (a_|__|_ v (a_|_ ^ c))
29	28	ax-r1 34	. . . . . . . 8 (a_|__|_ v (a_|_ ^ c)) = (a_|_ ->1 c)
30	27, 29	lbtr 131	. . . . . . 7 (a_|_ ^ c) =< (a_|_ ->1 c)
31		lear 153	. . . . . . 7 (a_|_ ^ c) =< c
32	30, 31	ler2an 165	. . . . . 6 (a_|_ ^ c) =< ((a_|_ ->1 c) ^ c)
33	8	negant 834	. . . . . . . 8 (a_|_ ->1 c) = (b_|_ ->1 c)
34	33	ran 71	. . . . . . 7 ((a_|_ ->1 c) ^ c) = ((b_|_ ->1 c) ^ c)
35		u1lemab 592	. . . . . . . 8 ((b_|_ ->1 c) ^ c) = ((b_|_ ^ c) v (b_|__|_ ^ c))
36		leor 151	. . . . . . . . 9 ((b_|_ ^ c) v (b_|__|_ ^ c)) =< (c_|_ v ((b_|_ ^ c) v (b_|__|_ ^ c)))
37		ancom 68	. . . . . . . . . . . . 13 (c ^ b_|_) = (b_|_ ^ c)
38		ancom 68	. . . . . . . . . . . . . 14 (c ^ b) = (b ^ c)
39		ax-a1 29	. . . . . . . . . . . . . . 15 b = b_|__|_
40	39	ran 71	. . . . . . . . . . . . . 14 (b ^ c) = (b_|__|_ ^ c)
41	38, 40	ax-r2 35	. . . . . . . . . . . . 13 (c ^ b) = (b_|__|_ ^ c)
42	37, 41	2or 67	. . . . . . . . . . . 12 ((c ^ b_|_) v (c ^ b)) = ((b_|_ ^ c) v (b_|__|_ ^ c))
43	42	lor 66	. . . . . . . . . . 11 (c_|_ v ((c ^ b_|_) v (c ^ b))) = (c_|_ v ((b_|_ ^ c) v (b_|__|_ ^ c)))
44	43	ax-r1 34	. . . . . . . . . 10 (c_|_ v ((b_|_ ^ c) v (b_|__|_ ^ c))) = (c_|_ v ((c ^ b_|_) v (c ^ b)))
45	44, 19	ax-r2 35	. . . . . . . . 9 (c_|_ v ((b_|_ ^ c) v (b_|__|_ ^ c))) = ((c_|_ v (c ^ b_|_)) v (c ^ b))
46	36, 45	lbtr 131	. . . . . . . 8 ((b_|_ ^ c) v (b_|__|_ ^ c)) =< ((c_|_ v (c ^ b_|_)) v (c ^ b))
47	35, 46	bltr 130	. . . . . . 7 ((b_|_ ->1 c) ^ c) =< ((c_|_ v (c ^ b_|_)) v (c ^ b))
48	34, 47	bltr 130	. . . . . 6 ((a_|_ ->1 c) ^ c) =< ((c_|_ v (c ^ b_|_)) v (c ^ b))
49	32, 48	letr 129	. . . . 5 (a_|_ ^ c) =< ((c_|_ v (c ^ b_|_)) v (c ^ b))
50	26, 49	ler2an 165	. . . 4 (a_|_ ^ c) =< ((b_|_ v c) ^ ((c_|_ v (c ^ b_|_)) v (c ^ b)))
51	25, 50	lel2or 162	. . 3 ((a ^ c) v (a_|_ ^ c)) =< ((b_|_ v c) ^ ((c_|_ v (c ^ b_|_)) v (c ^ b)))
52		lea 152	. . . . 5 ((a_|_ v c) ^ c_|_) =< (a_|_ v c)
53	8	negantlem8 838	. . . . 5 (a_|_ v c) = (b_|_ v c)
54	52, 53	lbtr 131	. . . 4 ((a_|_ v c) ^ c_|_) =< (b_|_ v c)
55		leao2 155	. . . . 5 ((a_|_ v c) ^ c_|_) =< (c_|_ v (c ^ b_|_))
56	55	ler 141	. . . 4 ((a_|_ v c) ^ c_|_) =< ((c_|_ v (c ^ b_|_)) v (c ^ b))
57	54, 56	ler2an 165	. . 3 ((a_|_ v c) ^ c_|_) =< ((b_|_ v c) ^ ((c_|_ v (c ^ b_|_)) v (c ^ b)))
58	51, 57	lel2or 162	. 2 (((a ^ c) v (a_|_ ^ c)) v ((a_|_ v c) ^ c_|_)) =< ((b_|_ v c) ^ ((c_|_ v (c ^ b_|_)) v (c ^ b)))
59		df-i4 46	. 2 (a ->4 c) = (((a ^ c) v (a_|_ ^ c)) v ((a_|_ v c) ^ c_|_))
60		dfi4b 482	. 2 (b ->4 c) = ((b_|_ v c) ^ ((c_|_ v (c ^ b_|_)) v (c ^ b)))
61	58, 59, 60	le3tr1 132	1 (a ->4 c) =< (b ->4 c)

Syntax hints:   = wb 1   =< wle 2  _|_wn 4   v wo 6   ^ wa 7   ->1 wi1 13   ->4 wi4 16

This theorem is referenced by:  negant4 844

This theorem was proved from axioms:  ax-a1 29  ax-a2 30  ax-a3 31  ax-a4 32  ax-a5 33  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37  ax-r3 421

This theorem depends on definitions:  df-b 38  df-a 39  df-t 40  df-f 41  df-i1 43  df-i3 45  df-i4 46  df-le1 122  df-le2 123  df-c1 124  df-c2 125

metamath.org