normlem6

Description: Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of Beran p. 97. (Contributed by NM, 2-Aug-1999) (Revised by Mario Carneiro, 4-Jun-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	normlem1.1	⊢ 𝑆 ∈ ℂ
	normlem1.2	⊢ 𝐹 ∈ ℋ
	normlem1.3	⊢ 𝐺 ∈ ℋ
	normlem2.4	⊢ 𝐵 = - ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·_ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·_ih 𝐹 ) ) )
	normlem3.5	⊢ 𝐴 = ( 𝐺 ·_ih 𝐺 )
	normlem3.6	⊢ 𝐶 = ( 𝐹 ·_ih 𝐹 )
	normlem6.7	⊢ ( abs ‘ 𝑆 ) = 1
Assertion	normlem6	⊢ ( abs ‘ 𝐵 ) ≤ ( 2 · ( ( √ ‘ 𝐴 ) · ( √ ‘ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		normlem1.1	⊢ 𝑆 ∈ ℂ
2		normlem1.2	⊢ 𝐹 ∈ ℋ
3		normlem1.3	⊢ 𝐺 ∈ ℋ
4		normlem2.4	⊢ 𝐵 = - ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·_ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·_ih 𝐹 ) ) )
5		normlem3.5	⊢ 𝐴 = ( 𝐺 ·_ih 𝐺 )
6		normlem3.6	⊢ 𝐶 = ( 𝐹 ·_ih 𝐹 )
7		normlem6.7	⊢ ( abs ‘ 𝑆 ) = 1
8		hiidrcl	⊢ ( 𝐺 ∈ ℋ → ( 𝐺 ·_ih 𝐺 ) ∈ ℝ )
9	3 8	ax-mp	⊢ ( 𝐺 ·_ih 𝐺 ) ∈ ℝ
10	5 9	eqeltri	⊢ 𝐴 ∈ ℝ
11	10	a1i	⊢ ( ⊤ → 𝐴 ∈ ℝ )
12	1 2 3 4	normlem2	⊢ 𝐵 ∈ ℝ
13	12	a1i	⊢ ( ⊤ → 𝐵 ∈ ℝ )
14		hiidrcl	⊢ ( 𝐹 ∈ ℋ → ( 𝐹 ·_ih 𝐹 ) ∈ ℝ )
15	2 14	ax-mp	⊢ ( 𝐹 ·_ih 𝐹 ) ∈ ℝ
16	6 15	eqeltri	⊢ 𝐶 ∈ ℝ
17	16	a1i	⊢ ( ⊤ → 𝐶 ∈ ℝ )
18		oveq1	⊢ ( 𝑥 = if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) → ( 𝑥 ↑ 2 ) = ( if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) ↑ 2 ) )
19	18	oveq2d	⊢ ( 𝑥 = if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) → ( 𝐴 · ( 𝑥 ↑ 2 ) ) = ( 𝐴 · ( if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) ↑ 2 ) ) )
20		oveq2	⊢ ( 𝑥 = if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) → ( 𝐵 · 𝑥 ) = ( 𝐵 · if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) ) )
21	19 20	oveq12d	⊢ ( 𝑥 = if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) → ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( 𝐵 · 𝑥 ) ) = ( ( 𝐴 · ( if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) ↑ 2 ) ) + ( 𝐵 · if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) ) ) )
22	21	oveq1d	⊢ ( 𝑥 = if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) → ( ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( 𝐵 · 𝑥 ) ) + 𝐶 ) = ( ( ( 𝐴 · ( if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) ↑ 2 ) ) + ( 𝐵 · if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) ) ) + 𝐶 ) )
23	22	breq2d	⊢ ( 𝑥 = if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) → ( 0 ≤ ( ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( 𝐵 · 𝑥 ) ) + 𝐶 ) ↔ 0 ≤ ( ( ( 𝐴 · ( if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) ↑ 2 ) ) + ( 𝐵 · if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) ) ) + 𝐶 ) ) )
24		0re	⊢ 0 ∈ ℝ
25	24	elimel	⊢ if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) ∈ ℝ
26	1 2 3 4 5 6 25 7	normlem5	⊢ 0 ≤ ( ( ( 𝐴 · ( if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) ↑ 2 ) ) + ( 𝐵 · if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) ) ) + 𝐶 )
27	23 26	dedth	⊢ ( 𝑥 ∈ ℝ → 0 ≤ ( ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( 𝐵 · 𝑥 ) ) + 𝐶 ) )
28	27	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ ) → 0 ≤ ( ( ( 𝐴 · ( 𝑥 ↑ 2 ) ) + ( 𝐵 · 𝑥 ) ) + 𝐶 ) )
29	11 13 17 28	discr	⊢ ( ⊤ → ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ≤ 0 )
30	29	mptru	⊢ ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ≤ 0
31	12	resqcli	⊢ ( 𝐵 ↑ 2 ) ∈ ℝ
32		4re	⊢ 4 ∈ ℝ
33	10 16	remulcli	⊢ ( 𝐴 · 𝐶 ) ∈ ℝ
34	32 33	remulcli	⊢ ( 4 · ( 𝐴 · 𝐶 ) ) ∈ ℝ
35	31 34 24	lesubadd2i	⊢ ( ( ( 𝐵 ↑ 2 ) − ( 4 · ( 𝐴 · 𝐶 ) ) ) ≤ 0 ↔ ( 𝐵 ↑ 2 ) ≤ ( ( 4 · ( 𝐴 · 𝐶 ) ) + 0 ) )
36	30 35	mpbi	⊢ ( 𝐵 ↑ 2 ) ≤ ( ( 4 · ( 𝐴 · 𝐶 ) ) + 0 )
37	34	recni	⊢ ( 4 · ( 𝐴 · 𝐶 ) ) ∈ ℂ
38	37	addridi	⊢ ( ( 4 · ( 𝐴 · 𝐶 ) ) + 0 ) = ( 4 · ( 𝐴 · 𝐶 ) )
39	36 38	breqtri	⊢ ( 𝐵 ↑ 2 ) ≤ ( 4 · ( 𝐴 · 𝐶 ) )
40	12	sqge0i	⊢ 0 ≤ ( 𝐵 ↑ 2 )
41		4pos	⊢ 0 < 4
42	24 32 41	ltleii	⊢ 0 ≤ 4
43		hiidge0	⊢ ( 𝐺 ∈ ℋ → 0 ≤ ( 𝐺 ·_ih 𝐺 ) )
44	3 43	ax-mp	⊢ 0 ≤ ( 𝐺 ·_ih 𝐺 )
45	44 5	breqtrri	⊢ 0 ≤ 𝐴
46		hiidge0	⊢ ( 𝐹 ∈ ℋ → 0 ≤ ( 𝐹 ·_ih 𝐹 ) )
47	2 46	ax-mp	⊢ 0 ≤ ( 𝐹 ·_ih 𝐹 )
48	47 6	breqtrri	⊢ 0 ≤ 𝐶
49	10 16	mulge0i	⊢ ( ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐶 ) → 0 ≤ ( 𝐴 · 𝐶 ) )
50	45 48 49	mp2an	⊢ 0 ≤ ( 𝐴 · 𝐶 )
51	32 33	mulge0i	⊢ ( ( 0 ≤ 4 ∧ 0 ≤ ( 𝐴 · 𝐶 ) ) → 0 ≤ ( 4 · ( 𝐴 · 𝐶 ) ) )
52	42 50 51	mp2an	⊢ 0 ≤ ( 4 · ( 𝐴 · 𝐶 ) )
53	31 34	sqrtlei	⊢ ( ( 0 ≤ ( 𝐵 ↑ 2 ) ∧ 0 ≤ ( 4 · ( 𝐴 · 𝐶 ) ) ) → ( ( 𝐵 ↑ 2 ) ≤ ( 4 · ( 𝐴 · 𝐶 ) ) ↔ ( √ ‘ ( 𝐵 ↑ 2 ) ) ≤ ( √ ‘ ( 4 · ( 𝐴 · 𝐶 ) ) ) ) )
54	40 52 53	mp2an	⊢ ( ( 𝐵 ↑ 2 ) ≤ ( 4 · ( 𝐴 · 𝐶 ) ) ↔ ( √ ‘ ( 𝐵 ↑ 2 ) ) ≤ ( √ ‘ ( 4 · ( 𝐴 · 𝐶 ) ) ) )
55	39 54	mpbi	⊢ ( √ ‘ ( 𝐵 ↑ 2 ) ) ≤ ( √ ‘ ( 4 · ( 𝐴 · 𝐶 ) ) )
56	12	absrei	⊢ ( abs ‘ 𝐵 ) = ( √ ‘ ( 𝐵 ↑ 2 ) )
57	32 33 42 50	sqrtmulii	⊢ ( √ ‘ ( 4 · ( 𝐴 · 𝐶 ) ) ) = ( ( √ ‘ 4 ) · ( √ ‘ ( 𝐴 · 𝐶 ) ) )
58		sqrt4	⊢ ( √ ‘ 4 ) = 2
59	10 16 45 48	sqrtmulii	⊢ ( √ ‘ ( 𝐴 · 𝐶 ) ) = ( ( √ ‘ 𝐴 ) · ( √ ‘ 𝐶 ) )
60	58 59	oveq12i	⊢ ( ( √ ‘ 4 ) · ( √ ‘ ( 𝐴 · 𝐶 ) ) ) = ( 2 · ( ( √ ‘ 𝐴 ) · ( √ ‘ 𝐶 ) ) )
61	57 60	eqtr2i	⊢ ( 2 · ( ( √ ‘ 𝐴 ) · ( √ ‘ 𝐶 ) ) ) = ( √ ‘ ( 4 · ( 𝐴 · 𝐶 ) ) )
62	55 56 61	3brtr4i	⊢ ( abs ‘ 𝐵 ) ≤ ( 2 · ( ( √ ‘ 𝐴 ) · ( √ ‘ 𝐶 ) ) )

Metamath Proof Explorer

Theorem normlem6

Proof