Theorem projlem7 9147

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

Hypotheses

Ref	Expression
projlem5.1	⊢ A ∈ ℋ
projlem5.2	⊢ B ∈ ℋ
projlem5.3	⊢ C ∈ ℋ
projlem5.4	⊢ R ∈ ℝ
projlem5.5	⊢ 0 ≤ R
projlem5.6	⊢ (4 · (R↑2)) ≤ ((normh ‘((B +h C) −h (2 ·h A)))↑2)
projlem5.7	⊢ D ∈ ℕ
projlem5.8	⊢ G ∈ ℕ
projlem5.9	⊢ N ∈ ℕ

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)) < (√ ‘((4 · ((2 · R) + 1)) / N))))

Proof of Theorem projlem7

Step	Hyp	Ref	Expression
1		opreq1 3963	. . . . 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))
2	1	fveq2d 3723	. . . 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)))
3	2	breq1d 2625	. . 3 ⊢ (B = if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), B, A) → ((normh ‘(B −h C)) < (√ ‘((4 · ((2 · R) + 1)) / N)) ↔ (normh ‘( if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), B, A) −h C)) < (√ ‘((4 · ((2 · R) + 1)) / N))))
4	3	imbi2d 611	. 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)) < (√ ‘((4 · ((2 · 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)) < (√ ‘((4 · ((2 · R) + 1)) / N)))))
5		opreq2 3964	. . . . 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)))
6	5	fveq2d 3723	. . . 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))))
7	6	breq1d 2625	. . 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)) < (√ ‘((4 · ((2 · 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))) < (√ ‘((4 · ((2 · R) + 1)) / N))))
8	7	imbi2d 611	. 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)) < (√ ‘((4 · ((2 · 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))) < (√ ‘((4 · ((2 · R) + 1)) / N)))))
9		opreq2 3964	. . . . . . . 8 ⊢ (R = if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), R, 0) → (2 · R) = (2 · if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), R, 0)))
10	9	opreq1d 3970	. . . . . . 7 ⊢ (R = if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), R, 0) → ((2 · R) + 1) = ((2 · if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), R, 0)) + 1))
11	10	opreq2d 3971	. . . . . 6 ⊢ (R = if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), R, 0) → (4 · ((2 · R) + 1)) = (4 · ((2 · if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), R, 0)) + 1)))
12	11	opreq1d 3970	. . . . 5 ⊢ (R = if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), R, 0) → ((4 · ((2 · R) + 1)) / N) = ((4 · ((2 · if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), R, 0)) + 1)) / N))
13	12	fveq2d 3723	. . . 4 ⊢ (R = if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), R, 0) → (√ ‘((4 · ((2 · R) + 1)) / N)) = (√ ‘((4 · ((2 · if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), R, 0)) + 1)) / N)))
14	13	breq2d 2626	. . 3 ⊢ (R = if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), R, 0) → ((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))) < (√ ‘((4 · ((2 · 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))) < (√ ‘((4 · ((2 · if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), R, 0)) + 1)) / N))))
15	14	imbi2d 611	. 2 ⊢ (R = if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), R, 0) → (((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))) < (√ ‘((4 · ((2 · 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))) < (√ ‘((4 · ((2 · if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), R, 0)) + 1)) / N)))))
16		projlem5.1	. . 3 ⊢ A ∈ ℋ
17		projlem5.2	. . . 4 ⊢ B ∈ ℋ
18	17, 16	keepel 2396	. . 3 ⊢ if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), B, A) ∈ ℋ
19		projlem5.3	. . . 4 ⊢ C ∈ ℋ
20	19, 16	keepel 2396	. . 3 ⊢ if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), C, A) ∈ ℋ
21		projlem5.4	. . . 4 ⊢ R ∈ ℝ
22		0re 5423	. . . 4 ⊢ 0 ∈ ℝ
23	21, 22	keepel 2396	. . 3 ⊢ if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), R, 0) ∈ ℝ
24		breq2 2619	. . . 4 ⊢ (R = if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), R, 0) → (0 ≤ R ↔ 0 ≤ if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), R, 0)))
25		breq2 2619	. . . 4 ⊢ (0 = if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), R, 0) → (0 ≤ 0 ↔ 0 ≤ if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), R, 0)))
26		projlem5.5	. . . 4 ⊢ 0 ≤ R
27	22	leid 5594	. . . 4 ⊢ 0 ≤ 0
28	24, 25, 26, 27	keephyp 2393	. . 3 ⊢ 0 ≤ if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), R, 0)
29		opreq1 3963	. . . . . . . 8 ⊢ (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))
30	29	opreq1d 3970	. . . . . . 7 ⊢ (B = if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), B, A) → ((B +h C) −h (2 ·h A)) = (( if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), B, A) +h C) −h (2 ·h A)))
31	30	fveq2d 3723	. . . . . 6 ⊢ (B = if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), B, A) → (normh ‘((B +h C) −h (2 ·h A))) = (normh ‘(( if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), B, A) +h C) −h (2 ·h A))))
32	31	opreq1d 3970	. . . . 5 ⊢ (B = if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), B, A) → ((normh ‘((B +h C) −h (2 ·h A)))↑2) = ((normh ‘(( if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), B, A) +h C) −h (2 ·h A)))↑2))
33	32	breq2d 2626	. . . 4 ⊢ (B = if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), B, A) → ((4 · (R↑2)) ≤ ((normh ‘((B +h C) −h (2 ·h A)))↑2) ↔ (4 · (R↑2)) ≤ ((normh ‘(( if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), B, A) +h C) −h (2 ·h A)))↑2)))
34		opreq2 3964	. . . . . . . 8 ⊢ (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)))
35	34	opreq1d 3970	. . . . . . 7 ⊢ (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) −h (2 ·h A)) = (( 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)) −h (2 ·h A)))
36	35	fveq2d 3723	. . . . . 6 ⊢ (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) −h (2 ·h A))) = (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)) −h (2 ·h A))))
37	36	opreq1d 3970	. . . . 5 ⊢ (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) −h (2 ·h A)))↑2) = ((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)) −h (2 ·h A)))↑2))
38	37	breq2d 2626	. . . 4 ⊢ (C = if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), C, A) → ((4 · (R↑2)) ≤ ((normh ‘(( if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), B, A) +h C) −h (2 ·h A)))↑2) ↔ (4 · (R↑2)) ≤ ((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)) −h (2 ·h A)))↑2)))
39		opreq1 3963	. . . . . 6 ⊢ (R = if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), R, 0) → (R↑2) = ( if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), R, 0)↑2))
40	39	opreq2d 3971	. . . . 5 ⊢ (R = if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), R, 0) → (4 · (R↑2)) = (4 · ( if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), R, 0)↑2)))
41	40	breq1d 2625	. . . 4 ⊢ (R = if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), R, 0) → ((4 · (R↑2)) ≤ ((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)) −h (2 ·h A)))↑2) ↔ (4 · ( if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), R, 0)↑2)) ≤ ((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)) −h (2 ·h A)))↑2)))
42		opreq1 3963	. . . . . . . 8 ⊢ (A = if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), B, A) → (A +h A) = ( if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), B, A) +h A))
43	42	opreq1d 3970	. . . . . . 7 ⊢ (A = if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), B, A) → ((A +h A) −h (2 ·h A)) = (( if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), B, A) +h A) −h (2 ·h A)))
44	43	fveq2d 3723	. . . . . 6 ⊢ (A = if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), B, A) → (normh ‘((A +h A) −h (2 ·h A))) = (normh ‘(( if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), B, A) +h A) −h (2 ·h A))))
45	44	opreq1d 3970	. . . . 5 ⊢ (A = if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), B, A) → ((normh ‘((A +h A) −h (2 ·h A)))↑2) = ((normh ‘(( if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), B, A) +h A) −h (2 ·h A)))↑2))
46	45	breq2d 2626	. . . 4 ⊢ (A = if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), B, A) → ((4 · (0↑2)) ≤ ((normh ‘((A +h A) −h (2 ·h A)))↑2) ↔ (4 · (0↑2)) ≤ ((normh ‘(( if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), B, A) +h A) −h (2 ·h A)))↑2)))
47		opreq2 3964	. . . . . . . 8 ⊢ (A = 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 A) = ( 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)))
48	47	opreq1d 3970	. . . . . . 7 ⊢ (A = 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 A) −h (2 ·h A)) = (( 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)) −h (2 ·h A)))
49	48	fveq2d 3723	. . . . . 6 ⊢ (A = 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 A) −h (2 ·h A))) = (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)) −h (2 ·h A))))
50	49	opreq1d 3970	. . . . 5 ⊢ (A = 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 A) −h (2 ·h A)))↑2) = ((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)) −h (2 ·h A)))↑2))
51	50	breq2d 2626	. . . 4 ⊢ (A = if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), C, A) → ((4 · (0↑2)) ≤ ((normh ‘(( if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), B, A) +h A) −h (2 ·h A)))↑2) ↔ (4 · (0↑2)) ≤ ((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)) −h (2 ·h A)))↑2)))
52		opreq1 3963	. . . . . 6 ⊢ (0 = if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), R, 0) → (0↑2) = ( if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), R, 0)↑2))
53	52	opreq2d 3971	. . . . 5 ⊢ (0 = if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), R, 0) → (4 · (0↑2)) = (4 · ( if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), R, 0)↑2)))
54	53	breq1d 2625	. . . 4 ⊢ (0 = if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), R, 0) → ((4 · (0↑2)) ≤ ((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)) −h (2 ·h A)))↑2) ↔ (4 · ( if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), R, 0)↑2)) ≤ ((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)) −h (2 ·h A)))↑2)))
55		projlem5.6	. . . 4 ⊢ (4 · (R↑2)) ≤ ((normh ‘((B +h C) −h (2 ·h A)))↑2)
56		sq0 6580	. . . . . . 7 ⊢ (0↑2) = 0
57	56	opreq2i 3967	. . . . . 6 ⊢ (4 · (0↑2)) = (4 · 0)
58		4re 5939	. . . . . . . 8 ⊢ 4 ∈ ℝ
59	58	recn 5297	. . . . . . 7 ⊢ 4 ∈ ℂ
60	59	mul01 5414	. . . . . 6 ⊢ (4 · 0) = 0
61	57, 60	eqtr 1493	. . . . 5 ⊢ (4 · (0↑2)) = 0
62	16, 16	hvaddcl 8843	. . . . . . . 8 ⊢ (A +h A) ∈ ℋ
63		2cn 5937	. . . . . . . . 9 ⊢ 2 ∈ ℂ
64	63, 16	hvmulcl 8839	. . . . . . . 8 ⊢ (2 ·h A) ∈ ℋ
65	62, 64	hvsubcl 8846	. . . . . . 7 ⊢ ((A +h A) −h (2 ·h A)) ∈ ℋ
66	65	normcl 8953	. . . . . 6 ⊢ (normh ‘((A +h A) −h (2 ·h A))) ∈ ℝ
67	66	sqge0 6573	. . . . 5 ⊢ 0 ≤ ((normh ‘((A +h A) −h (2 ·h A)))↑2)
68	61, 67	eqbrtr 2630	. . . 4 ⊢ (4 · (0↑2)) ≤ ((normh ‘((A +h A) −h (2 ·h A)))↑2)
69	33, 38, 41, 46, 51, 54, 55, 68	keephyp3v 2395	. . 3 ⊢ (4 · ( if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), R, 0)↑2)) ≤ ((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)) −h (2 ·h A)))↑2)
70		projlem5.7	. . 3 ⊢ D ∈ ℕ
71		projlem5.8	. . 3 ⊢ G ∈ ℕ
72		projlem5.9	. . 3 ⊢ N ∈ ℕ
73		opreq1 3963	. . . . . . . 8 ⊢ (B = if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), B, A) → (B −h A) = ( if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), B, A) −h A))
74	73	fveq2d 3723	. . . . . . 7 ⊢ (B = if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), B, A) → (normh ‘(B −h A)) = (normh ‘( if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), B, A) −h A)))
75	74	breq1d 2625	. . . . . 6 ⊢ (B = if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), B, A) → ((normh ‘(B −h A)) < (R + (1 / D)) ↔ (normh ‘( if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), B, A) −h A)) < (R + (1 / D))))
76	75	anbi1d 616	. . . . 5 ⊢ (B = if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), B, A) → (((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))) ↔ ((normh ‘( if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), B, A) −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G)))))
77		opreq1 3963	. . . . . . . 8 ⊢ (C = if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), C, A) → (C −h A) = ( if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), C, A) −h A))
78	77	fveq2d 3723	. . . . . . 7 ⊢ (C = if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), C, A) → (normh ‘(C −h A)) = (normh ‘( if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), C, A) −h A)))
79	78	breq1d 2625	. . . . . 6 ⊢ (C = if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), C, A) → ((normh ‘(C −h A)) < (R + (1 / G)) ↔ (normh ‘( if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), C, A) −h A)) < (R + (1 / G))))
80	79	anbi2d 615	. . . . 5 ⊢ (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 A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))) ↔ ((normh ‘( if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))), B, A) −h A)) < (R + (1 / D)) ⋀ (normh ‘( if(((normh ‘(B −h A)) < (R + (1 / D)) ⋀ (normh ‘(C −h A)) < (R + (1 / G))),