Theorem projlem20 5212

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

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(norm` (v -v 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)) -> (((norm` (B -v A)) < (R + (1 / D)) /\ (norm` (C -v A)) < (R + (1 / G))) -> ((N <_ D /\ N <_ G) -> (norm` (B -v C)) < (sqr` ((4 x. ((2 x. R) + 1)) / N)))))

Distinct variable group(s):   v,u,A   u,H,v

Proof of Theorem projlem20

Step	Hyp	Ref	Expression
1		opreq1 3006	. . . . . 6 |- (B = if(B e. H, B, 0v) -> (B -v A) = (if(B e. H, B, 0v) -v A))
2	1	fveq2d 2836	. . . . 5 |- (B = if(B e. H, B, 0v) -> (norm` (B -v A)) = (norm` (if(B e. H, B, 0v) -v A)))
3	2	breq1d 2071	. . . 4 |- (B = if(B e. H, B, 0v) -> ((norm` (B -v A)) < (R + (1 / D)) <-> (norm` (if(B e. H, B, 0v) -v A)) < (R + (1 / D))))
4	3	anbi1d 469	. . 3 |- (B = if(B e. H, B, 0v) -> (((norm` (B -v A)) < (R + (1 / D)) /\ (norm` (C -v A)) < (R + (1 / G))) <-> ((norm` (if(B e. H, B, 0v) -v A)) < (R + (1 / D)) /\ (norm` (C -v A)) < (R + (1 / G)))))
5		opreq1 3006	. . . . . 6 |- (B = if(B e. H, B, 0v) -> (B -v C) = (if(B e. H, B, 0v) -v C))
6	5	fveq2d 2836	. . . . 5 |- (B = if(B e. H, B, 0v) -> (norm` (B -v C)) = (norm` (if(B e. H, B, 0v) -v C)))
7	6	breq1d 2071	. . . 4 |- (B = if(B e. H, B, 0v) -> ((norm` (B -v C)) < (sqr` ((4 x. ((2 x. R) + 1)) / N)) <-> (norm` (if(B e. H, B, 0v) -v C)) < (sqr` ((4 x. ((2 x. R) + 1)) / N))))
8	7	imbi2d 464	. . 3 |- (B = if(B e. H, B, 0v) -> (((N <_ D /\ N <_ G) -> (norm` (B -v C)) < (sqr` ((4 x. ((2 x. R) + 1)) / N))) <-> ((N <_ D /\ N <_ G) -> (norm` (if(B e. H, B, 0v) -v C)) < (sqr` ((4 x. ((2 x. R) + 1)) / N)))))
9	4, 8	imbi12d 474	. 2 |- (B = if(B e. H, B, 0v) -> ((((norm` (B -v A)) < (R + (1 / D)) /\ (norm` (C -v A)) < (R + (1 / G))) -> ((N <_ D /\ N <_ G) -> (norm` (B -v C)) < (sqr` ((4 x. ((2 x. R) + 1)) / N)))) <-> (((norm` (if(B e. H, B, 0v) -v A)) < (R + (1 / D)) /\ (norm` (C -v A)) < (R + (1 / G))) -> ((N <_ D /\ N <_ G) -> (norm` (if(B e. H, B, 0v) -v C)) < (sqr` ((4 x. ((2 x. R) + 1)) / N))))))
10		opreq1 3006	. . . . . 6 |- (C = if(C e. H, C, 0v) -> (C -v A) = (if(C e. H, C, 0v) -v A))
11	10	fveq2d 2836	. . . . 5 |- (C = if(C e. H, C, 0v) -> (norm` (C -v A)) = (norm` (if(C e. H, C, 0v) -v A)))
12	11	breq1d 2071	. . . 4 |- (C = if(C e. H, C, 0v) -> ((norm` (C -v A)) < (R + (1 / G)) <-> (norm` (if(C e. H, C, 0v) -v A)) < (R + (1 / G))))
13	12	anbi2d 468	. . 3 |- (C = if(C e. H, C, 0v) -> (((norm` (if(B e. H, B, 0v) -v A)) < (R + (1 / D)) /\ (norm` (C -v A)) < (R + (1 / G))) <-> ((norm` (if(B e. H, B, 0v) -v A)) < (R + (1 / D)) /\ (norm` (if(C e. H, C, 0v) -v A)) < (R + (1 / G)))))
14		opreq2 3007	. . . . . 6 |- (C = if(C e. H, C, 0v) -> (if(B e. H, B, 0v) -v C) = (if(B e. H, B, 0v) -v if(C e. H, C, 0v)))
15	14	fveq2d 2836	. . . . 5 |- (C = if(C e. H, C, 0v) -> (norm` (if(B e. H, B, 0v) -v C)) = (norm` (if(B e. H, B, 0v) -v if(C e. H, C, 0v))))
16	15	breq1d 2071	. . . 4 |- (C = if(C e. H, C, 0v) -> ((norm` (if(B e. H, B, 0v) -v C)) < (sqr` ((4 x. ((2 x. R) + 1)) / N)) <-> (norm` (if(B e. H, B, 0v) -v if(C e. H, C, 0v))) < (sqr` ((4 x. ((2 x. R) + 1)) / N))))
17	16	imbi2d 464	. . 3 |- (C = if(C e. H, C, 0v) -> (((N <_ D /\ N <_ G) -> (norm` (if(B e. H, B, 0v) -v C)) < (sqr` ((4 x. ((2 x. R) + 1)) / N))) <-> ((N <_ D /\ N <_ G) -> (norm` (if(B e. H, B, 0v) -v if(C e. H, C, 0v))) < (sqr` ((4 x. ((2 x. R) + 1)) / N)))))
18	13, 17	imbi12d 474	. 2 |- (C = if(C e. H, C, 0v) -> ((((norm` (if(B e. H, B, 0v) -v A)) < (R + (1 / D)) /\ (norm` (C -v A)) < (R + (1 / G))) -> ((N <_ D /\ N <_ G) -> (norm` (if(B e. H, B, 0v) -v C)) < (sqr` ((4 x. ((2 x. R) + 1)) / N)))) <-> (((norm` (if(B e. H, B, 0v) -v A)) < (R + (1 / D)) /\ (norm` (if(C e. H, C, 0v) -v A)) < (R + (1 / G))) -> ((N <_ D /\ N <_ G) -> (norm` (if(B e. H, B, 0v) -v if(C e. H, C, 0v))) < (sqr` ((4 x. ((2 x. R) + 1)) / N))))))
19		opreq2 3007	. . . . . 6 |- (D = if(D e. NN, D, 1) -> (1 / D) = (1 / if(D e. NN, D, 1)))
20	19	opreq2d 3013	. . . . 5 |- (D = if(D e. NN, D, 1) -> (R + (1 / D)) = (R + (1 / if(D e. NN, D, 1))))
21	20	breq2d 2072	. . . 4 |- (D = if(D e. NN, D, 1) -> ((norm` (if(B e. H, B, 0v) -v A)) < (R + (1 / D)) <-> (norm` (if(B e. H, B, 0v) -v A)) < (R + (1 / if(D e. NN, D, 1)))))
22	21	anbi1d 469	. . 3 |- (D = if(D e. NN, D, 1) -> (((norm` (if(B e. H, B, 0v) -v A)) < (R + (1 / D)) /\ (norm` (if(C e. H, C, 0v) -v A)) < (R + (1 / G))) <-> ((norm` (if(B e. H, B, 0v) -v A)) < (R + (1 / if(D e. NN, D, 1))) /\ (norm` (if(C e. H, C, 0v) -v A)) < (R + (1 / G)))))
23		breq2 2066	. . . . 5 |- (D = if(D e. NN, D, 1) -> (N <_ D <-> N <_ if(D e. NN, D, 1)))
24	23	anbi1d 469	. . . 4 |- (D = if(D e. NN, D, 1) -> ((N <_ D /\ N <_ G) <-> (N <_ if(D e. NN, D, 1) /\ N <_ G)))
25	24	imbi1d 465	. . 3 |- (D