Theorem projlem7 5199

Description: Part of Lemma 3.6 of [Beran] p. 101. Applies weak deduction theorem to projlem6 5198. Used by projlem19 5211.

Hypotheses

Ref	Expression
projlem5.1	|- A e. H~
projlem5.2	|- B e. H~
projlem5.3	|- C e. H~
projlem5.4	|- R e. RR
projlem5.5	|- 0 <_ R
projlem5.6	|- (4 x. (R^2)) <_ ((norm` ((B +v C) -v (2 .s A)))^2)
projlem5.7	|- D e. NN
projlem5.8	|- G e. NN
projlem5.9	|- N e. NN

Assertion

Ref	Expression
projlem7	|- (((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))))

Proof of Theorem projlem7

Step	Hyp	Ref	Expression
1		opreq1 3006	. . . . 5 |- (B = if(((norm` (B -v A)) < (R + (1 / D)) /\ (norm` (C -v A)) < (R + (1 / G))), B, A) -> (B -v C) = (if(((norm` (B -v A)) < (R + (1 / D)) /\ (norm` (C -v A)) < (R + (1 / G))), B, A) -v C))
2	1	fveq2d 2836	. . . 4 |- (B = if(((norm` (B -v A)) < (R + (1 / D)) /\ (norm` (C -v A)) < (R + (1 / G))), B, A) -> (norm` (B -v C)) = (norm` (if(((norm` (B -v A)) < (R + (1 / D)) /\ (norm` (C -v A)) < (R + (1 / G))), B, A) -v C)))
3	2	breq1d 2071	. . 3 |- (B = if(((norm` (B -v A)) < (R + (1 / D)) /\ (norm` (C -v A)) < (R + (1 / G))), B, A) -> ((norm` (B -v C)) < (sqr` ((4 x. ((2 x. R) + 1)) / N)) <-> (norm` (if(((norm` (B -v A)) < (R + (1 / D)) /\ (norm` (C -v A)) < (R + (1 / G))), B, A) -v C)) < (sqr` ((4 x. ((2 x. R) + 1)) / N))))
4	3	imbi2d 464	. 2 |- (B = if(((norm` (B -v A)) < (R + (1 / D)) /\ (norm` (C -v A)) < (R + (1 / G))), B, A) -> (((N <_ D /\ N <_ G) -> (norm` (B -v C)) < (sqr` ((4 x. ((2 x. R) + 1)) / N))) <-> ((N <_ D /\ N <_ G) -> (norm` (if(((norm` (B -v A)) < (R + (1 / D)) /\ (norm` (C -v A)) < (R + (1 / G))), B, A) -v C)) < (sqr` ((4 x. ((2 x. R) + 1)) / N)))))
5		opreq2 3007	. . . . 5 |- (C = if(((norm` (B -v A)) < (R + (1 / D)) /\ (norm` (C -v A)) < (R + (1 / G))), C, A) -> (if(((norm` (B -v A)) < (R + (1 / D)) /\ (norm` (C -v A)) < (R + (1 / G))), B, A) -v C) = (if(((norm` (B -v A)) < (R + (1 / D)) /\ (norm` (C -v A)) < (R + (1 / G))), B, A) -v if(((norm` (B -v A)) < (R + (1 / D)) /\ (norm` (C -v A)) < (R + (1 / G))), C, A)))
6	5	fveq2d 2836	. . . 4 |- (C = if(((norm` (B -v A)) < (R + (1 / D)) /\ (norm` (C -v A)) < (R + (1 / G))), C, A) -> (norm` (if(((norm` (B -v A)) < (R + (1 / D)) /\ (norm` (C -v A)) < (R + (1 / G))), B, A) -v C)) = (norm` (if(((norm` (B -v A)) < (R + (1 / D)) /\ (norm` (C -v A)) < (R + (1 / G))), B, A) -v if(((norm` (B -v A)) < (R + (1 / D)) /\ (norm` (C -v A)) < (R + (1 / G))), C, A))))
7	6	breq1d 2071	. . 3 |- (C = if(((norm` (B -v A)) < (R + (1 / D)) /\ (norm` (C -v A)) < (R + (1 / G))), C, A) -> ((norm` (if(((norm` (B -v A)) < (R + (1 / D)) /\ (norm` (C -v A)) < (R + (1 / G))), B, A) -v C)) < (sqr` ((4 x. ((2 x. R) + 1)) / N)) <-> (norm` (if(((norm` (B -v A)) < (R + (1 / D)) /\ (norm` (C -v A)) < (R + (1 / G))), B, A) -v if(((norm` (B -v A)) < (R + (1 / D)) /\ (norm` (C -v A)) < (R + (1 / G))), C, A))) < (sqr` ((4 x. ((2 x. R) + 1)) / N))))
8	7	imbi2d 464	. 2 |- (C = if(((norm` (B -v A)) < (R + (1 / D)) /\ (norm` (C -v A)) < (R + (1 / G))), C, A) -> (((N <_ D /\ N <_ G) -> (norm` (if(((norm` (B -v A)) < (R + (1 / D)) /\ (norm` (C -v A)) < (R + (1 / G))), B, A) -v C)) < (sqr` ((4 x. ((2 x. R) + 1)) / N))) <-> ((N <_ D /\ N <_ G) -> (norm` (if(((norm` (B -v A)) < (R + (1 / D)) /\ (norm` (C -v A)) < (R + (1 / G))), B, A) -v if(((norm` (B -v A)) < (R + (1 / D)) /\ (norm` (C -v A)) < (R + (1 / G))), C, A))) < (sqr` ((4 x. ((2 x. R) + 1)) / N)))))
9		opreq2 3007	. . . . . . . 8 |- (R = if(((norm` (B -v A)) < (R + (1 / D)) /\ (norm` (C -v A)) < (R + (1 / G))), R, 0) -> (2 x. R) = (2 x. if(((norm` (B -v A)) < (R + (1 / D)) /\ (norm` (C -v A)) < (R + (1 / G))), R, 0)))
10	9	opreq1d 3012	. . . . . . 7 |- (R = if(((norm` (B -v A)) < (R + (1 / D)) /\ (norm` (C -v A)) < (R + (1 / G))), R, 0) -> ((2 x. R) + 1) = ((2 x. if(((norm` (B -v A)) < (R + (1 / D)) /\ (norm` (C -v A)) < (R + (1 / G))), R, 0)) + 1))
11	10	opreq2d 3013	. . . . . 6 |- (R = if(((norm` (B -v A)) < (R + (1 / D)) /\ (norm` (C -v A)) < (R + (1 / G))), R, 0) -> (4 x. ((2 x. R) + 1)) = (4 x. ((2 x. if(((norm` (B -v A)) < (R + (1 / D)) /\ (norm` (C -v A)) < (R + (1 / G))), R, 0)) + 1)))
12	11	opreq1d 3012	. . . . 5 |- (R = if(((norm` (B -v A)) < (R + (1 / D)) /\ (norm` (C -v A)) < (R + (1 / G))), R, 0) -> ((4 x. ((2 x. R) + 1)) / N) = ((4 x. ((2 x. if(((norm` (B -v A)) < (R + (1 / D)) /\ (norm` (C -v A)) < (R + (1 / G))), R, 0)) + 1)) / N))
13	12	fveq2d 2836	. . . 4 |- (R = if(((norm` (B -v A)) < (R + (1 / D)) /\ (norm