Theorem ruclem4 7513

Description: Lemma for ruc 7549. 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 3724	. . . . . 6 |- (A = C -> (1st` A) = (1st` C))
2	1	breq1d 2629	. . . . 5 |- (A = C -> ((1st` A) < B <-> (1st` C) < B))
3		fveq2 3724	. . . . . 6 |- (A = C -> (2nd` A) = (2nd` C))
4	3	breq2d 2630	. . . . 5 |- (A = C -> (B < (2nd` A) <-> B < (2nd` C)))
5	2, 4	anbi12d 628	. . . 4 |- (A = C -> (((1st` A) < B /\ B < (2nd` A)) <-> ((1st` C) < B /\ B < (2nd` C))))
6	5	ifbid 2372	. . 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)>.))
7		ifeq12 2368	. . . 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 x. (1st` C)) + (2nd` C)) / 3), (((1st` C) + (2 x. (2nd` C))) / 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)>.) = if(((1st` C) < B /\ B < (2nd` C)), <.(((2 x. B) + (2nd` C)) / 3), ((B + (2 x. (2nd` C))) / 3)>., <.(((2 x. (1st` C)) + (2nd` C)) / 3), (((1st` C) + (2 x. (2nd` C))) / 3)>.))
8	3	opreq2d 3976	. . . . . 6 |- (A = C -> ((2 x. B) + (2nd` A)) = ((2 x. B) + (2nd` C)))
9	8	opreq1d 3975	. . . . 5 |- (A = C -> (((2 x. B) + (2nd` A)) / 3) = (((2 x. B) + (2nd` C)) / 3))
10	3	opreq2d 3976	. . . . . . 7 |- (A = C -> (2 x. (2nd` A)) = (2 x. (2nd` C)))
11	10	opreq2d 3976	. . . . . 6 |- (A = C -> (B + (2 x. (2nd` A))) = (B + (2 x. (2nd` C))))
12	11	opreq1d 3975	. . . . 5 |- (A = C -> ((B + (2 x. (2nd` A))) / 3) = ((B + (2 x. (2nd` C))) / 3))
13	9, 12	opeq12d 2495	. . . 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)>.)
14	1	opreq2d 3976	. . . . . . 7 |- (A = C -> (2 x. (1st` A)) = (2 x. (1st` C)))
15	14, 3	opreq12d 3978	. . . . . 6 |- (A = C -> ((2 x. (1st` A)) + (2nd` A)) = ((2 x. (1st` C)) + (2nd` C)))
16	15	opreq1d 3975	. . . . 5 |- (A = C -> (((2 x. (1st` A)) + (2nd` A)) / 3) = (((2 x. (1st` C)) + (2nd` C)) / 3))
17	1, 10	opreq12d 3978	. . . . . 6 |- (A = C -> ((1st` A) + (2 x. (2nd` A))) = ((1st` C) + (2 x. (2nd` C))))
18	17	opreq1d 3975	. . . . 5 |- (A = C -> (((1st` A) + (2 x. (2nd` A))) / 3) = (((1st` C) + (2 x. (2nd` C))) / 3))
19	16, 18	opeq12d 2495	. . . 4 |- (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)>.)
20	7, 13, 19	sylanc 471	. . 3 |- (A = C -> 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)>.) = if(((1st` C) < B /\ B < (2nd` C)), <.(((2 x. B) + (2nd` C)) / 3), ((B + (2 x. (2nd` C))) / 3)>., <.(((2 x. (1st` C)) + (2nd` C)) / 3), (((1st` C) + (2 x. (2nd` C))) / 3)>.))
21	6, 20	eqtrd 1507	. 2 |- (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` C)) / 3), ((B + (2 x. (2nd` C))) / 3)>., <.(((2 x. (1st` C)) + (2nd` C)) / 3), (((1st` C) + (2 x. (2nd` C))) / 3)>.))
22		breq2 2623	. . . . 5 |- (B = D -> ((1st` C) < B <-> (1st` C) < D))
23		breq1 2622	. . . . 5 |- (B = D -> (B < (2nd` C) <-> D < (2nd` C)))
24	22, 23	anbi12d 628	. . . 4 |- (B = D -> (((1st` C) < B /\ B < (2nd` C)) <-> ((1st` C) < D /\ D < (2nd` C))))
25	24	ifbid 2372	. . 3 |- (B = D -> if(((1st` C) < B /\ B < (2nd` C)), <.(((2 x. B) + (2nd` C)) / 3), ((B + (2 x. (2nd` C))) / 3)>., <.(((2 x. (1st` C)) + (2nd` C)) / 3), (((1st` C) + (2 x. (2nd` C))) / 3)>.) = if(((1st` C) < D /\ D < (2nd` C)), <.((