Theorem projlem20 9205

Description: Part of Lemma 3.6 of [Beran] p. 101. Used by projlem27 9212.

Hypotheses

Ref	Expression
projlem11.1	|- A e. H~
projlem11.2	|- H e. CH
projlem11.3	|- S = {u e. RR | E.v e. H u = -u(normh` (v -h A))}
projlem11.4	|- R = -usup(S, RR, < )
projlem20.5	|- N e. NN

Assertion

Ref	Expression
projlem20	|- (((B e. H /\ C e. H) /\ (D e. NN /\ G e. NN)) -> (((normh` (B -h A)) < (R + (1 / D)) /\ (normh` (C -h A)) < (R + (1 / G))) -> ((N <_ D /\ N <_ G) -> (normh` (B -h C)) < (sqr` ((4 x. ((2 x. R) + 1)) / N)))))

Distinct variable groups:   v,u,A   u,H,v

Proof of Theorem projlem20

Step	Hyp	Ref	Expression
1		opreq1 3968	. . . . . 6 |- (B = if(B e. H, B, 0h) -> (B -h A) = (if(B e. H, B, 0h) -h A))
2	1	fveq2d 3728	. . . . 5 |- (B = if(B e. H, B, 0h) -> (normh` (B -h A)) = (normh` (if(B e. H, B, 0h) -h A)))
3	2	breq1d 2629	. . . 4 |- (B = if(B e. H, B, 0h) -> ((normh` (B -h A)) < (R + (1 / D)) <-> (normh` (if(B e. H, B, 0h) -h A)) < (R + (1 / D))))
4	3	anbi1d 617	. . 3 |- (B = if(B e. H, B, 0h) -> (((normh` (B -h A)) < (R + (1 / D)) /\ (normh` (C -h A)) < (R + (1 / G))) <-> ((normh` (if(B e. H, B, 0h) -h A)) < (R + (1 / D)) /\ (normh` (C -h A)) < (R + (1 / G)))))
5		opreq1 3968	. . . . . 6 |- (B = if(B e. H, B, 0h) -> (B -h C) = (if(B e. H, B, 0h) -h C))
6	5	fveq2d 3728	. . . . 5 |- (B = if(B e. H, B, 0h) -> (normh` (B -h C)) = (normh` (if(B e. H, B, 0h) -h C)))
7	6	breq1d 2629	. . . 4 |- (B = if(B e. H, B, 0h) -> ((normh` (B -h C)) < (sqr` ((4 x. ((2 x. R) + 1)) / N)) <-> (normh` (if(B e. H, B, 0h) -h C)) < (sqr` ((4 x. ((2 x. R) + 1)) / N))))
8	7	imbi2d 612	. . 3 |- (B = if(B e. H, B, 0h) -> (((N <_ D /\ N <_ G) -> (normh` (B -h C)) < (sqr` ((4 x. ((2 x. R) + 1)) / N))) <-> ((N <_ D /\ N <_ G) -> (normh` (if(B e. H, B, 0h) -h C)) < (sqr` ((4 x. ((2 x. R) + 1)) / N)))))
9	4, 8	imbi12d 626	. 2 |- (B = if(B e. H, B, 0h) -> ((((normh` (B -h A)) < (R + (1 / D)) /\ (normh` (C -h A)) < (R + (1 / G))) -> ((N <_ D /\ N <_ G) -> (normh` (B -h C)) < (sqr` ((4 x. ((2 x. R) + 1)) / N)))) <-> (((normh` (if(B e. H, B, 0h) -h A)) < (R + (1 / D)) /\ (normh` (C -h A)) < (R + (1 / G))) -> ((N <_ D /\ N <_ G) -> (normh` (if(B e. H, B, 0h) -h C)) < (sqr` ((4 x. ((2 x. R) + 1)) / N))))))
10		opreq1 3968	. . . . . 6 |- (C = if(C e. H, C, 0h) -> (C -h A) = (if(C e. H, C, 0h) -h A))
11	10	fveq2d 3728	. . . . 5 |- (C = if(C e. H, C, 0h) -> (normh` (C -h A)) = (normh` (if(C e. H, C, 0h) -h A)))
12	11	breq1d 2629	. . . 4 |- (C = if(C e. H, C, 0h) -> ((normh` (C -h A)) < (R + (1 / G)) <-> (normh` (if(C e. H, C, 0h) -h A)) < (R + (1 / G))))
13	12	anbi2d 616	. . 3 |- (C = if(C e. H, C, 0h) -> (((normh` (if(B e. H, B, 0h) -h A)) < (R + (1 / D)) /\ (normh` (C -h A)) < (R + (1 / G))) <-> ((normh` (if(B e. H, B, 0h) -h A)) < (R + (1 / D)) /\ (normh` (if(C e. H, C, 0h) -h A)) < (R + (1 / G)))))
14		opreq2 3969	. . . . . 6 |- (C = if(C e. H, C, 0h) -> (if(B e. H, B, 0h) -h C) = (if(B e. H, B, 0h) -h if(C e. H, C, 0h)))
15	14	fveq2d 3728	. . . . 5 |- (C = if(C e. H, C, 0h) -> (normh` (if(B e. H, B, 0h) -h C)) = (normh` (if(B e. H, B, 0h) -h if(C e. H, C, 0h))))
16	15	breq1d 2629	. . . 4 |- (C = if(C e. H, C, 0h) -> ((normh` (if(B e. H, B, 0h) -h C)) < (sqr` ((4 x. ((2 x. R) + 1)) / N)) <-> (normh` (if(B e. H, B, 0h) -h if(C e. H, C, 0h))) < (sqr` ((4 x. ((2 x. R) + 1)) / N))))
17	16	imbi2d 612	. . 3 |- (C = if(C e. H, C, 0h) -> (((N <_ D /\ N <_ G) -> (normh` (if(B e. H, B, 0h) -h C)) < (sqr` ((4 x. ((2 x. R) + 1)) / N))) <-> ((N <_ D /\ N <_ G) -> (normh` (if(B e. H, B, 0h) -h if(C e. H, C, 0h))) < (sqr` ((4 x. ((2 x. R) + 1)) / N)))))
18	13, 17	imbi12d 626	. 2 |- (C = if(C e. H, C, 0h) -> ((((normh` (if(B e. H, B, 0h) -h A)) < (R + (1 / D)) /\ (normh` (C -h A)) < (R + (1 / G))) -> ((N <_ D /\ N <_ G) -> (normh` (if(B e. H, B, 0h) -h C)) < (sqr` ((4 x. ((2 x. R) + 1)) / N)))) <-> (((normh` (if(B e. H, B, 0h) -h A)) < (R + (1 / D)) /\ (normh` (if(C e. H, C, 0h) -h A)) < (R + (1 / G))) -> ((N <_ D /\ N <_ G) -> (normh` (if(B e. H, B, 0h) -h if(C e. H, C, 0h))) < (sqr` ((4 x. ((2 x. R) + 1)) / N))))))
19		opreq2 3969	. . . . . 6 |- (D = if(D e. NN, D, 1) -> (1 / D) = (1 / if(D e. NN, D, 1)))
20	19	opreq2d 3976	. . . . 5 |- (D = if(D e. NN, D, 1) -> (R + (1 / D)) = (R + (1 / if(D e. NN, D, 1))))
21	20	breq2d 2630	. . . 4 |- (D = if(D e. NN, D, 1) -> ((normh` (if(B e. H, B, 0h) -h A)) < (R + (1 / D)) <-> (normh` (if(B e. H, B, 0h) -h A)) < (R + (1 / if(D e. NN, D, 1)))))
22	21	anbi1d 617	. . 3 |- (D = if(D e. NN, D, 1) -> (((normh` (if(B e. H, B, 0h) -h A)) < (R + (1 / D)) /\ (normh` (if(C e. H, C, 0h) -h A)) < (R + (1 / G))) <-> ((normh` (if(B e. H, B, 0h) -h A)) < (R + (1 / if(D e. NN, D, 1))) /\ (normh` (if(C e. H, C, 0h) -h A)) < (R + (1 / G)))))
23		breq2 2623	. . . . 5 |- (D = if(D e. NN, D, 1) -> (N <_ D <-> N <_ if(D e. NN, D, 1)))
24	23	anbi1d 617	. . . 4 |- (D = if(D e. NN, D, 1) -> ((N <_ D /\ N