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 ∈ ℋ
projlem5.2	⊢ B ∈ ℋ
projlem5.3	⊢ C ∈ ℋ
projlem5.4	⊢ R ∈ ℝ
projlem5.5	⊢ 0 ≤ R
projlem5.6	⊢ (4 · (R↑2)) ≤ ((norm ‘((B +v C) −v (2 ·s A)))↑2)
projlem5.7	⊢ D ∈ ℕ
projlem5.8	⊢ G ∈ ℕ
projlem5.9	⊢ N ∈ ℕ

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)) < (√ ‘((4 · ((2 · 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)) < (√ ‘((4 · ((2 · R) + 1)) / N)) ↔ (norm ‘(if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), B, A) −v C)) < (√ ‘((4 · ((2 · 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)) < (√ ‘((4 · ((2 · 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)) < (√ ‘((4 · ((2 · 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)) < (√ ‘((4 · ((2 · 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))) < (√ ‘((4 · ((2 · 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)) < (√ ‘((4 · ((2 · 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))) < (√ ‘((4 · ((2 · 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 · R) = (2 · 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 · R) + 1) = ((2 · 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 · ((2 · R) + 1)) = (4 · ((2 · 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 · ((2 · R) + 1)) / N) = ((4 · ((2 · 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 ‘(C −v A)) < (R + (1 / G))), R, 0) → (√ ‘((4 · ((2 · R) + 1)) / N)) = (√ ‘((4 · ((2 · if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), R, 0)) + 1)) / N)))
14	13	breq2d 2072	. . 3 ⊢ (R = if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), R, 0) → ((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))) < (√ ‘((4 · ((2 · 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))) < (√ ‘((4 · ((2 · if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), R, 0)) + 1)) / N))))
15	14	imbi2d 464	. 2 ⊢ (R = if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), R, 0) → (((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))) < (√ ‘((4 · ((2 · 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))) < (√ ‘((4 · ((2 · if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), R, 0)) + 1)) / N)))))
16		projlem5.1	. . 3 ⊢ A ∈ ℋ
17		projlem5.2	. . . 4 ⊢ B ∈ ℋ
18	17, 16	keepel 1796	. . 3 ⊢ if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), B, A) ∈ ℋ
19		projlem5.3	. . . 4 ⊢ C ∈ ℋ
20	19, 16	keepel 1796	. . 3 ⊢ if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), C, A) ∈ ℋ
21		projlem5.4	. . . 4 ⊢ R ∈ ℝ
22		ax0re 4063	. . . 4 ⊢ 0 ∈ ℝ
23	21, 22	keepel 1796	. . 3 ⊢ if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), R, 0) ∈ ℝ
24		breq2 2066	. . . 4 ⊢ (R = if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), R, 0) → (0 ≤ R ↔ 0 ≤ if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), R, 0)))
25		breq2 2066	. . . 4 ⊢ (0 = if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), R, 0) → (0 ≤ 0 ↔ 0 ≤ if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), R, 0)))
26		projlem5.5	. . . 4 ⊢ 0 ≤ R
27	22	leid 4339	. . . 4 ⊢ 0 ≤ 0
28	24, 25, 26, 27	keephyp 1794	. . 3 ⊢ 0 ≤ if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), R, 0)
29		opreq1 3006	. . . . . . . 8 ⊢ (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))
30	29	opreq1d 3012	. . . . . . 7 ⊢ (B = if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), B, A) → ((B +v C) −v (2 ·s A)) = ((if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), B, A) +v C) −v (2 ·s A)))
31	30	fveq2d 2836	. . . . . 6 ⊢ (B = if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), B, A) → (norm ‘((B +v C) −v (2 ·s A))) = (norm ‘((if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), B, A) +v C) −v (2 ·s A))))
32	31	opreq1d 3012	. . . . 5 ⊢ (B = if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), B, A) → ((norm ‘((B +v C) −v (2 ·s A)))↑2) = ((norm ‘((if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), B, A) +v C) −v (2 ·s A)))↑2))
33	32	breq2d 2072	. . . 4 ⊢ (B = if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), B, A) → ((4 · (R↑2)) ≤ ((norm ‘((B +v C) −v (2 ·s A)))↑2) ↔ (4 · (R↑2)) ≤ ((norm ‘((if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), B, A) +v C) −v (2 ·s A)))↑2)))
34		opreq2 3007	. . . . . . . 8 ⊢ (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)))
35	34	opreq1d 3012	. . . . . . 7 ⊢ (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) −v (2 ·s A)) = ((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)) −v (2 ·s A)))
36	35	fveq2d 2836	. . . . . 6 ⊢ (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) −v (2 ·s A))) = (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)) −v (2 ·s A))))
37	36	opreq1d 3012	. . . . 5 ⊢ (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) −v (2 ·s A)))↑2) = ((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)) −v (2 ·s A)))↑2))
38	37	breq2d 2072	. . . 4 ⊢ (C = if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), C, A) → ((4 · (R↑2)) ≤ ((norm ‘((if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), B, A) +v C) −v (2 ·s A)))↑2) ↔ (4 · (R↑2)) ≤ ((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)) −v (2 ·s A)))↑2)))
39		opreq1 3006	. . . . . 6 ⊢ (R = if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), R, 0) → (R↑2) = (if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), R, 0)↑2))
40	39	opreq2d 3013	. . . . 5 ⊢ (R = if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), R, 0) → (4 · (R↑2)) = (4 · (if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), R, 0)↑2)))
41	40	breq1d 2071	. . . 4 ⊢ (R = if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), R, 0) → ((4 · (R↑2)) ≤ ((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)) −v (2 ·s A)))↑2) ↔ (4 · (if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), R, 0)↑2)) ≤ ((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)) −v (2 ·s A)))↑2)))
42		opreq1 3006	. . . . . . . 8 ⊢ (A = if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), B, A) → (A +v A) = (if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), B, A) +v A))
43	42	opreq1d 3012	. . . . . . 7 ⊢ (A = if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), B, A) → ((A +v A) −v (2 ·s A)) = ((if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), B, A) +v A) −v (2 ·s A)))
44	43	fveq2d 2836	. . . . . 6 ⊢ (A = if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), B, A) → (norm ‘((A +v A) −v (2 ·s A))) = (norm ‘((if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), B, A) +v A) −v (2 ·s A))))
45	44	opreq1d 3012	. . . . 5 ⊢ (A = if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), B, A) → ((norm ‘((A +v A) −v (2 ·s A)))↑2) = ((norm ‘((if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), B, A) +v A) −v (2 ·s A)))↑2))
46	45	breq2d 2072	. . . 4 ⊢ (A = if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), B, A) → ((4 · (0↑2)) ≤ ((norm ‘((A +v A) −v (2 ·s A)))↑2) ↔ (4 · (0↑2)) ≤ ((norm ‘((if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), B, A) +v A) −v (2 ·s A)))↑2)))
47		opreq2 3007	. . . . . . . 8 ⊢ (A = 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 A) = (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)))
48	47	opreq1d 3012	. . . . . . 7 ⊢ (A = 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 A) −v (2 ·s A)) = ((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)) −v (2 ·s A)))
49	48	fveq2d 2836	. . . . . 6 ⊢ (A = 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 A) −v (2 ·s A))) = (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)) −v (2 ·s A))))
50	49	opreq1d 3012	. . . . 5 ⊢ (A = 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 A) −v (2 ·s A)))↑2) = ((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)) −v (2 ·s A)))↑2))
51	50	breq2d 2072	. . . 4 ⊢ (A = if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), C, A) → ((4 · (0↑2)) ≤ ((norm ‘((if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), B, A) +v A) −v (2 ·s A)))↑2) ↔ (4 · (0↑2)) ≤ ((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)) −v (2 ·s A)))↑2)))
52		opreq1 3006	. . . . . 6 ⊢ (0 = if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), R, 0) → (0↑2) = (if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), R, 0)↑2))
53	52	opreq2d 3013	. . . . 5 ⊢ (0 = if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), R, 0) → (4 · (0↑2)) = (4 · (if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), R, 0)↑2)))
54	53	breq1d 2071	. . . 4 ⊢ (0 = if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), R, 0) → ((4 · (0↑2)) ≤ ((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)) −v (2 ·s A)))↑2) ↔ (4 · (if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), R, 0)↑2)) ≤ ((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)) −v (2 ·s A)))↑2)))
55		projlem5.6	. . . 4 ⊢ (4 · (R↑2)) ≤ ((norm ‘((B +v C) −v (2 ·s A)))↑2)
56		0cn 4100	. . . . . . . . 9 ⊢ 0 ∈ ℂ
57	56	sqval 4685	. . . . . . . 8 ⊢ (0↑2) = (0 · 0)
58	56	mulzer1 4185	. . . . . . . 8 ⊢ (0 · 0) = 0
59	57, 58	eqtr 1119	. . . . . . 7 ⊢ (0↑2) = 0
60	59	opreq2i 3010	. . . . . 6 ⊢ (4 · (0↑2)) = (4 · 0)
61		4re 4473	. . . . . . . 8 ⊢ 4 ∈ ℝ
62	61	recn 4098	. . . . . . 7 ⊢ 4 ∈ ℂ
63	62	mulzer1 4185	. . . . . 6 ⊢ (4 · 0) = 0
64	60, 63	eqtr 1119	. . . . 5 ⊢ (4 · (0↑2)) = 0
65	16, 16	hvaddcl 4999	. . . . . . . 8 ⊢ (A +v A) ∈ ℋ
66		2cn 4471	. . . . . . . . 9 ⊢ 2 ∈ ℂ
67	66, 16	hvmulcl 4990	. . . . . . . 8 ⊢ (2 ·s A) ∈ ℋ
68	65, 67	hvsubcl 5002	. . . . . . 7 ⊢ ((A +v A) −v (2 ·s A)) ∈ ℋ
69	68	normcl 5081	. . . . . 6 ⊢ (norm ‘((A +v A) −v (2 ·s A))) ∈ ℝ
70	69	sqege0 4704	. . . . 5 ⊢ 0 ≤ ((norm ‘((A +v A) −v (2 ·s A)))↑2)
71	64, 70	eqbrtr 2076	. . . 4 ⊢ (4 · (0↑2)) ≤ ((norm ‘((A +v A) −v (2 ·s A)))↑2)
72	33, 38, 41, 46, 51, 54, 55, 71	keephyp3v 1795	. . 3 ⊢ (4 · (if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), R, 0)↑2)) ≤ ((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)) −v (2 ·s A)))↑2)
73		projlem5.7	. . 3 ⊢ D ∈ ℕ
74		projlem5.8	. . 3 ⊢ G ∈ ℕ
75		projlem5.9	. . 3 ⊢ N ∈ ℕ
76		opreq1 3006	. . . . . . . 8 ⊢ (B = if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), B, A) → (B −v A) = (if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), B, A) −v A))
77	76	fveq2d 2836	. . . . . . 7 ⊢ (B = if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), B, A) → (norm ‘(B −v A)) = (norm ‘(if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), B, A) −v A)))
78	77	breq1d 2071	. . . . . 6 ⊢ (B = if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), B, A) → ((norm ‘(B −v A)) < (R + (1 / D)) ↔ (norm ‘(if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), B, A) −v A)) < (R + (1 / D))))
79	78	anbi1d 469	. . . . 5 ⊢ (B = if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), B, A) → (((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))) ↔ ((norm ‘(if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), B, A) −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G)))))
80		opreq1 3006	. . . . . . . 8 ⊢ (C = if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), C, A) → (C −v A) = (if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), C, A) −v A))
81	80	fveq2d 2836	. . . . . . 7 ⊢ (C = if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), C, A) → (norm ‘(C −v A)) = (norm ‘(if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), C, A) −v A)))
82	81	breq1d 2071	. . . . . 6 ⊢ (C = if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), C, A) → ((norm ‘(C −v A)) < (R + (1 / G)) ↔ (norm ‘(if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), C, A) −v A)) < (R + (1 / G))))
83	82	anbi2d 468	. . . . 5 ⊢ (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 A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))) ↔ ((norm ‘(if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), B, A) −v A)) < (R + (1 / D)) ∧ (norm ‘(if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), C, A) −v A)) < (R + (1 / G)))))
84		opreq1 3006	. . . . . . 7 ⊢ (R = if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), R, 0) → (R + (1 / D)) = (if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), R, 0) + (1 / D)))
85	84	breq2d 2072	. . . . . 6 ⊢ (R = if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), R, 0) → ((norm ‘(if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), B, A) −v A)) < (R + (1 / D)) ↔ (norm ‘(if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), B, A) −v A)) < (if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), R, 0) + (1 / D))))
86		opreq1 3006	. . . . . . 7 ⊢ (R = if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), R, 0) → (R + (1 / G)) = (if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), R, 0) + (1 / G)))
87	86	breq2d 2072	. . . . . 6 ⊢ (R = if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), R, 0) → ((norm ‘(if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), C, A) −v A)) < (R + (1 / G)) ↔ (norm ‘(if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), C, A) −v A)) < (if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), R, 0) + (1 / G))))
88	85, 87	anbi12d 476	. . . . 5 ⊢ (R = if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), R, 0) → (((norm ‘(if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), B, A) −v A)) < (R + (1 / D)) ∧ (norm ‘(if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), C, A) −v A)) < (R + (1 / G))) ↔ ((norm ‘(if(((norm ‘(B −v A)) < (R + (1 / D)) ∧ (norm ‘(C −v A)) < (R + (1 / G))), B<