Theorem 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	$$⊢S\in ℂ$$
	normlem1.2	$$⊢F\in \mathscr{H}$$
	normlem1.3	$$⊢G\in \mathscr{H}$$
	normlem2.4	$$⊢B=-\left(\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)\right)$$
	normlem3.5	$$⊢A=G{\cdot }_{\mathrm{ih}}G$$
	normlem3.6	$$⊢C=F{\cdot }_{\mathrm{ih}}F$$
	normlem6.7	$$⊢\left|S\right|=1$$
Assertion	normlem6	$$⊢\left|B\right|\le 2\sqrt{A}\sqrt{C}$$

Proof

Step	Hyp	Ref	Expression
1		normlem1.1	$$⊢S\in ℂ$$
2		normlem1.2	$$⊢F\in \mathscr{H}$$
3		normlem1.3	$$⊢G\in \mathscr{H}$$
4		normlem2.4	$$⊢B=-\left(\bar{S}\left(F{\cdot }_{\mathrm{ih}}G\right)+S\left(G{\cdot }_{\mathrm{ih}}F\right)\right)$$
5		normlem3.5	$$⊢A=G{\cdot }_{\mathrm{ih}}G$$
6		normlem3.6	$$⊢C=F{\cdot }_{\mathrm{ih}}F$$
7		normlem6.7	$$⊢\left|S\right|=1$$
8		hiidrcl	$$⊢G\in \mathscr{H}\to G{\cdot }_{\mathrm{ih}}G\in ℝ$$
9	3 8	ax-mp	$$⊢G{\cdot }_{\mathrm{ih}}G\in ℝ$$
10	5 9	eqeltri	$$⊢A\in ℝ$$
11	10	a1i	$$⊢\top \to A\in ℝ$$
12	1 2 3 4	normlem2	$$⊢B\in ℝ$$
13	12	a1i	$$⊢\top \to B\in ℝ$$
14		hiidrcl	$$⊢F\in \mathscr{H}\to F{\cdot }_{\mathrm{ih}}F\in ℝ$$
15	2 14	ax-mp	$$⊢F{\cdot }_{\mathrm{ih}}F\in ℝ$$
16	6 15	eqeltri	$$⊢C\in ℝ$$
17	16	a1i	$$⊢\top \to C\in ℝ$$
18		oveq1	$$⊢x=if\left(x\in ℝ,x,0\right)\to x^2={if\left(x\in ℝ,x,0\right)}^2$$
19	18	oveq2d	$$⊢x=if\left(x\in ℝ,x,0\right)\to A{x}^2=A{if\left(x\in ℝ,x,0\right)}^2$$
20		oveq2	$$⊢x=if\left(x\in ℝ,x,0\right)\to Bx=Bif\left(x\in ℝ,x,0\right)$$
21	19 20	oveq12d	$$⊢x=if\left(x\in ℝ,x,0\right)\to A{x}^2+Bx=A{if\left(x\in ℝ,x,0\right)}^2+Bif\left(x\in ℝ,x,0\right)$$
22	21	oveq1d	$$⊢x=if\left(x\in ℝ,x,0\right)\to A{x}^2+Bx+C=A{if\left(x\in ℝ,x,0\right)}^2+Bif\left(x\in ℝ,x,0\right)+C$$
23	22	breq2d	$$⊢x=if\left(x\in ℝ,x,0\right)\to \left(0\le A{x}^2+Bx+C\leftrightarrow 0\le A{if\left(x\in ℝ,x,0\right)}^2+Bif\left(x\in ℝ,x,0\right)+C\right)$$
24		0re	$$⊢0\in ℝ$$
25	24	elimel	$$⊢if\left(x\in ℝ,x,0\right)\in ℝ$$
26	1 2 3 4 5 6 25 7	normlem5	$$⊢0\le A{if\left(x\in ℝ,x,0\right)}^2+Bif\left(x\in ℝ,x,0\right)+C$$
27	23 26	dedth	$$⊢x\in ℝ\to 0\le A{x}^2+Bx+C$$
28	27	adantl	$$⊢\left(\top \wedge x\in ℝ\right)\to 0\le A{x}^2+Bx+C$$
29	11 13 17 28	discr	$$⊢\top \to B^2-4AC\le 0$$
30	29	mptru	$$⊢B^2-4AC\le 0$$
31	12	resqcli	$$⊢B^2\in ℝ$$
32		4re	$$⊢4\in ℝ$$
33	10 16	remulcli	$$⊢AC\in ℝ$$
34	32 33	remulcli	$$⊢4AC\in ℝ$$
35	31 34 24	lesubadd2i	$$⊢B^2-4AC\le 0\leftrightarrow B^2\le 4AC+0$$
36	30 35	mpbi	$$⊢B^2\le 4AC+0$$
37	34	recni	$$⊢4AC\in ℂ$$
38	37	addridi	$$⊢4AC+0=4AC$$
39	36 38	breqtri	$$⊢B^2\le 4AC$$
40	12	sqge0i	$$⊢0\le B^2$$
41		4pos	$$⊢0<4$$
42	24 32 41	ltleii	$$⊢0\le 4$$
43		hiidge0	$$⊢G\in \mathscr{H}\to 0\le G{\cdot }_{\mathrm{ih}}G$$
44	3 43	ax-mp	$$⊢0\le G{\cdot }_{\mathrm{ih}}G$$
45	44 5	breqtrri	$$⊢0\le A$$
46		hiidge0	$$⊢F\in \mathscr{H}\to 0\le F{\cdot }_{\mathrm{ih}}F$$
47	2 46	ax-mp	$$⊢0\le F{\cdot }_{\mathrm{ih}}F$$
48	47 6	breqtrri	$$⊢0\le C$$
49	10 16	mulge0i	$$⊢\left(0\le A\wedge 0\le C\right)\to 0\le AC$$
50	45 48 49	mp2an	$$⊢0\le AC$$
51	32 33	mulge0i	$$⊢\left(0\le 4\wedge 0\le AC\right)\to 0\le 4AC$$
52	42 50 51	mp2an	$$⊢0\le 4AC$$
53	31 34	sqrtlei	$$⊢\left(0\le B^2\wedge 0\le 4AC\right)\to \left(B^2\le 4AC\leftrightarrow \sqrt{B^2}\le \sqrt{4AC}\right)$$
54	40 52 53	mp2an	$$⊢B^2\le 4AC\leftrightarrow \sqrt{B^2}\le \sqrt{4AC}$$
55	39 54	mpbi	$$⊢\sqrt{B^2}\le \sqrt{4AC}$$
56	12	absrei	$$⊢\left|B\right|=\sqrt{B^2}$$
57	32 33 42 50	sqrtmulii	$$⊢\sqrt{4AC}=\sqrt{4}\sqrt{AC}$$
58		sqrt4	$$⊢\sqrt{4}=2$$
59	10 16 45 48	sqrtmulii	$$⊢\sqrt{AC}=\sqrt{A}\sqrt{C}$$
60	58 59	oveq12i	$$⊢\sqrt{4}\sqrt{AC}=2\sqrt{A}\sqrt{C}$$
61	57 60	eqtr2i	$$⊢2\sqrt{A}\sqrt{C}=\sqrt{4AC}$$
62	55 56 61	3brtr4i	$$⊢\left|B\right|\le 2\sqrt{A}\sqrt{C}$$