HomeHome Hilbert Space Explorer < Previous   Next >
Related theorems
Unicode version
Theorem projlem7 9322
Description: Part of Lemma 3.6 of [Beran] p. 101. Applies weak deduction theorem to projlem6 9321. Used by projlem19 9334.
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)) <_ ((normh` ((B +h C) -h (2 .h A)))^2)
projlem5.7 |- D e. NN
projlem5.8 |- G e. NN
projlem5.9 |- N e. NN
Assertion
Ref Expression
projlem7 |- (((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))))
Proof of Theorem projlem7
StepHypRef Expression
1 opreq1 3907 . . . . 5 |- (B = if(((normh` (B -h A)) < (R + (1 / D)) /\ (normh` (C -h A)) < (R + (1 / G))), B, A) -> (B -h C) = (if(((normh` (B -h A)) < (R + (1 / D)) /\ (normh` (C -h A)) < (R + (1 / G))), B, A) -h C))
21fveq2d 3667 . . . 4 |- (B = if(((normh` (B -h A)) < (R + (1 / D)) /\ (normh` (C -h A)) < (R + (1 / G))), B, A) -> (normh` (B -h C)) = (normh` (if(((normh` (B -h A)) < (R + (1 / D)) /\ (normh` (C -h A)) < (R + (1 / G))), B, A) -h C)))
32breq1d 2597 . . 3 |- (B = if(((normh` (B -h A)) < (R + (1 / D)) /\ (normh` (C -h A)) < (R + (1 / G))), B, A) -> ((normh` (B -h C)) < (sqr` ((4 x. ((2 x. R) + 1)) / N)) <-> (normh` (if(((normh` (B -h A)) < (R + (1 / D)) /\ (normh` (C -h A)) < (R + (1 / G))), B, A) -h C)) < (sqr` ((4 x. ((2 x. R) + 1)) / N))))
43imbi2d 610 . 2 |- (B = if(((normh` (B -h A)) < (R + (1 / D)) /\ (normh` (C -h A)) < (R + (1 / G))), B, A) -> (((N <_ D /\ N <_ G) -> (normh` (B -h C)) < (sqr` ((4 x. ((2 x. R) + 1)) / N))) <-> ((N <_ D /\ N <_ G) -> (normh` (if(((normh` (B -h A)) < (R + (1 / D)) /\ (normh` (C -h A)) < (R + (1 / G))), B, A) -h C)) < (sqr` ((4 x. ((2 x. R) + 1)) / N)))))
5 opreq2 3908 . . . . 5 |- (C = if(((normh` (B -h A)) < (R + (1 / D)) /\ (normh` (C -h A)) < (R + (1 / G))), C, A) -> (if(((normh` (B -h A)) < (R + (1 / D)) /\ (normh` (C -h A)) < (R + (1 / G))), B, A) -h C) = (if(((normh` (B -h A)) < (R + (1 / D)) /\ (normh` (C -h A)) < (R + (1 / G))), B, A) -h if(((normh` (B -h A)) < (R + (1 / D)) /\ (normh` (C -h A)) < (R + (1 / G))), C, A)))
65fveq2d 3667 . . . 4 |- (C = if(((normh` (B -h A)) < (R + (1 / D)) /\ (normh` (C -h A)) < (R + (1 / G))), C, A) -> (normh` (if(((normh` (B -h A)) < (R + (1 / D)) /\ (normh` (C -h A)) < (R + (1 / G))), B, A) -h C)) = (normh` (if(((normh` (B -h A)) < (R + (1 / D)) /\ (normh` (C -h A)) < (R + (1 / G))), B, A) -h if(((normh` (B -h A)) < (R + (1 / D)) /\ (normh` (C -h A)) < (R + (1 / G))), C, A))))
76breq1d 2597 . . 3 |- (C = if(((normh` (B -h A)) < (R + (1 / D)) /\ (normh` (C -h A)) < (R + (1 / G))), C, A) -> ((normh` (if(((normh` (B -h A)) < (R + (1 / D)) /\ (normh` (C -h A)) < (R + (1 / G))), B, A) -h C)) < (sqr` ((4 x. ((2 x. R) + 1)) / N)) <-> (normh` (if(((normh` (B -h A)) < (R + (1 / D)) /\ (normh` (C -h A)) < (R + (1 / G))), B, A) -h if(((normh` (B -h A)) < (R + (1 / D)) /\ (normh` (C -h A)) < (R + (1 / G))), C, A))) < (sqr` ((4 x. ((2 x. R) + 1)) / N))))
87imbi2d 610 . 2 |- (C = if(((normh` (B -h A)) < (R + (1 / D)) /\ (normh` (C -h A)) < (R + (1 / G))), C, A) -> (((N <_ D /\ N <_ G) -> (normh` (if(((normh` (B -h A)) < (R + (1 / D)) /\ (normh` (C -h A)) < (R + (1 / G))), B, A) -h C)) < (sqr` ((4 x. ((2 x. R) + 1)) / N))) <-> ((N <_ D /\ N <_ G) -> (normh` (if(((normh` (B -h A)) < (R + (1 / D)) /\ (normh` (C -h A)) < (R + (1 / G))), B, A) -h if(((normh` (B -h A)) < (R + (1 / D)) /\ (normh` (C -h A)) < (R + (1 / G))), C, A))) < (sqr` ((4 x. ((2 x. R) + 1)) / N)))))
9 opreq2 3908 . . . . . . . 8 |- (R = if(((normh` (B -h A)) < (R + (1 / D)) /\ (normh` (C -h A)) < (R + (1 / G))), R, 0) -> (2 x. R) = (2 x. if(((normh` (B -h A)) < (R + (1 / D)) /\ (normh` (C -h A)) < (R + (1 / G))), R, 0)))
109opreq1d 3914 . . . . . . 7 |- (R = if(((normh` (B -h A)) < (R + (1 / D)) /\ (normh` (C -h A)) < (R + (1 / G))), R, 0) -> ((2 x. R) + 1) = ((2 x. if(((normh` (B -h A)) < (R + (1 / D)) /\ (normh` (C -h A)) < (R + (1 / G))), R, 0)) + 1))
1110opreq2d 3915 . . . . . 6 |- (R = if(((normh` (B -h A)) < (R + (1 / D)) /\ (normh` (C -h A)) < (R + (1 / G))), R, 0) -> (4 x. ((2 x. R) + 1)) = (4 x. ((2 x. if(((normh` (B -h A)) < (R + (1 / D)) /\ (normh` (C -h A)) < (R + (1 / G))), R, 0)) + 1)))
1211opreq1d 3914 . . . . 5 |- (R = if(((normh` (B -h A)) < (R + (1 / D)) /\ (normh` (C -h A)) < (R + (1 / G))), R, 0) -> ((4 x. ((2 x. R) + 1)) / N) = ((4 x. ((2 x. if(((normh` (B -h A)) < (R + (1 / D)) /\ (normh` (C -h A)) < (R + (1 / G))), R, 0)) + 1)) / N))
1312fveq2d 3667 . . . 4 |- (R = if(((normh` (B -h