Theorem ruclem4 4888

Description: Lemma for ruc 4924. Helper lemma showing a tedious equality used several times.

Assertion

Ref	Expression
ruclem4	|- ((A = C /\ B = D) -> if(((1st` A) < B /\ B < (2nd` A)), <.(((2 x. B) + (2nd` A)) / 3), ((B + (2 x. (2nd` A))) / 3)>., <.(((2 x. (1st` A)) + (2nd` A)) / 3), (((1st` A) + (2 x. (2nd` A))) / 3)>.) = if(((1st` C) < D /\ D < (2nd` C)), <.(((2 x. D) + (2nd` C)) / 3), ((D + (2 x. (2nd` C))) / 3)>., <.(((2 x. (1st` C)) + (2nd` C)) / 3), (((1st` C) + (2 x. (2nd` C))) / 3)>.))

Proof of Theorem ruclem4

Step	Hyp	Ref	Expression
1		fveq2 2832	. . . . . 6 |- (A = C -> (1st` A) = (1st` C))
2	1	breq1d 2071	. . . . 5 |- (A = C -> ((1st` A) < B <-> (1st` C) < B))
3		fveq2 2832	. . . . . 6 |- (A = C -> (2nd` A) = (2nd` C))
4	3	breq2d 2072	. . . . 5 |- (A = C -> (B < (2nd` A) <-> B < (2nd` C)))
5	2, 4	anbi12d 476	. . . 4 |- (A = C -> (((1st` A) < B /\ B < (2nd` A)) <-> ((1st` C) < B /\ B < (2nd` C))))
6		ifbi 1783	. . . 4 |- ((((1st` A) < B /\ B < (2nd` A)) <-> ((1st` C) < B /\ B < (2nd` C))) -> if(((1st` A) < B /\ B < (2nd` A)), <.(((2 x. B) + (2nd` A)) / 3), ((B + (2 x. (2nd` A))) / 3)>., <.(((2 x. (1st` A)) + (2nd` A)) / 3), (((1st` A) + (2 x. (2nd` A))) / 3)>.) = if(((1st` C) < B /\ B < (2nd` C)), <.(((2 x. B) + (2nd` A)) / 3), ((B + (2 x. (2nd` A))) / 3)>., <.(((2 x. (1st` A)) + (2nd` A)) / 3), (((1st` A) + (2 x. (2nd` A))) / 3)>.))
7	5, 6	syl 12	. . 3 |- (A = C -> if(((1st` A) < B /\ B < (2nd` A)), <.(((2 x. B) + (2nd` A)) / 3), ((B + (2 x. (2nd` A))) / 3)>., <.(((2 x. (1st` A)) + (2nd` A)) / 3), (((1st` A) + (2 x. (2nd` A))) / 3)>.) = if(((1st` C) < B /\ B < (2nd` C)), <.(((2 x. B) + (2nd` A)) / 3), ((B + (2 x. (2nd` A))) / 3)>., <.(((2 x. (1st` A)) + (2nd` A)) / 3), (((1st` A) + (2 x. (2nd` A))) / 3)>.))
8	3	opreq2d 3013	. . . . . . . 8 |- (A = C -> ((2 x. B) + (2nd` A)) = ((2 x. B) + (2nd` C)))
9	8	opreq1d 3012	. . . . . . 7 |- (A = C -> (((2 x. B) + (2nd` A)) / 3) = (((2 x. B) + (2nd` C)) / 3))
10	3	opreq2d 3013	. . . . . . . . 9 |- (A = C -> (2 x. (2nd` A)) = (2 x. (2nd` C)))
11	10	opreq2d 3013	. . . . . . . 8 |- (A = C -> (B + (2 x. (2nd` A))) = (B + (2 x. (2nd` C))))
12	11	opreq1d 3012	. . . . . . 7 |- (A = C -> ((B + (2 x. (2nd` A))) / 3) = ((B + (2 x. (2nd` C))) / 3))
13	9, 12	jca 236	. . . . . 6 |- (A = C -> ((((2 x. B) + (2nd` A)) / 3) = (((2 x. B) + (2nd` C)) / 3) /\ ((B + (2 x. (2nd` A))) / 3) = ((B + (2 x. (2nd` C))) / 3)))
14		opeq12 1878	. . . . . 6 |- (((((2 x. B) + (2nd` A)) / 3) = (((2 x. B) + (2nd` C)) / 3) /\ ((B + (2 x. (2nd` A))) / 3) = ((B + (2 x. (2nd` C))) / 3)) -> <.(((2 x. B) + (2nd` A)) / 3), ((B + (2 x. (2nd` A))) / 3)>. = <.(((2 x. B) + (2nd` C)) / 3), ((B + (2 x. (2nd` C))) / 3)>.)
15	13, 14	syl 12	. . . . 5 |- (A = C -> <.(((2 x. B) + (2nd` A)) / 3), ((B + (2 x. (2nd` A))) / 3)>. = <.(((2 x. B) + (2nd` C)) / 3), ((B + (2 x. (2nd` C))) / 3)>.)
16	1	opreq2d 3013	. . . . . . . . 9 |- (A = C -> (2 x. (1st` A)) = (2 x. (1st` C)))
17	16, 3	opreq12d 3014	. . . . . . . 8 |- (A = C -> ((2 x. (1st` A)) + (2nd` A)) = ((2 x. (1st` C)) + (2nd` C)))
18	17	opreq1d 3012	. . . . . . 7 |- (A = C -> (((2 x. (1st` A)) + (2nd` A)) / 3) = (((2 x. (1st` C)) + (2nd` C)) / 3))
19	1, 10	opreq12d 3014	. . . . . . . 8 |- (A = C -> ((1st` A) + (2 x. (2nd` A))) = ((1st` C) + (2 x. (2nd` C))))
20	19	opreq1d 3012	. . . . . . 7 |- (A = C -> (((1st` A) + (2 x. (2nd` A))) / 3) = (((1st` C) + (2 x. (2nd` C))) / 3))
21	18, 20	jca 236	. . . . . 6 |- (A = C -> ((((2 x. (1st` A)) + (2nd` A)) / 3) = (((2 x. (1st` C)) + (2nd` C)) / 3) /\ (((1st` A) + (2 x. (2nd` A))) / 3) = (((1st` C) + (2 x. (2nd` C))) / 3)))
22		opeq12 1878	. . . . . 6 |- (((((2 x. (1st` A)) + (2nd` A)) / 3) = (((2 x. (1st` C)) + (2nd` C)) / 3) /\ (((1st` A) + (2 x. (2nd` A))) / 3) = (((1st` C) + (2 x. (2nd` C))) / 3)) -> <.(((2 x. (1st` A)) + (2nd` A)) / 3), (((1st` A) + (2 x. (2nd` A))) / 3)>. = <.(((2 x. (1st` C)) + (2nd` C)) / 3), (((1st` C) + (2 x. (2nd` C))) / 3)>.)
23	21, 22	syl 12	. . . . 5 |- (A = C -> <.(((2 x. (1st` A)) + (2nd` A)) / 3), (((1st` A) + (2 x. (2nd` A))) / 3)>. = <.(((2 x. (1st` C)) + (2nd` C)) / 3), (((1st` C) + (2 x. (2nd` C))) / 3)>.)
24	15, 23	jca 236	. . . 4 |- (A = C -> (<.(((2 x. B) + (2nd` A)) / 3), ((B + (2 x. (2nd` A))) / 3)>. = <.(((2 x. B) + (2nd` C)) / 3), ((B + (2 x. (2nd` C))) / 3)>. /\ <.(((2 x. (1st` A)) + (2nd` A)) / 3), (((1st` A) + (2 x. (2nd` A))) / 3)>. = <.(((2 x. (1st` C)) + (2nd` C)) / 3), (((1st` C) + (2 x. (2nd` C))) / 3)>.))
25		ifeq12 1782	. . . 4 |- ((<.(((2 x. B) + (2nd` A)) / 3), ((B + (2 x. (2nd` A))) / 3)>. = <.(((2 x. B) + (2nd` C)) / 3), ((B + (2 x. (2nd` C))) / 3)>. /\ <.(((2 x. (1st` A)) + (2nd` A)) / 3), (((1st` A) + (2 x. (2nd` A))) / 3)>. = <.(((2