Metamath Proof Explorer


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
normlem1.2 F
normlem1.3 G
normlem2.4 B = S F ih G + S G ih F
normlem3.5 A = G ih G
normlem3.6 C = F ih F
normlem6.7 S = 1
Assertion normlem6 B 2 A C

Proof

Step Hyp Ref Expression
1 normlem1.1 S
2 normlem1.2 F
3 normlem1.3 G
4 normlem2.4 B = S F ih G + S G ih F
5 normlem3.5 A = G ih G
6 normlem3.6 C = F ih F
7 normlem6.7 S = 1
8 hiidrcl G G ih G
9 3 8 ax-mp G ih G
10 5 9 eqeltri A
11 10 a1i A
12 1 2 3 4 normlem2 B
13 12 a1i B
14 hiidrcl F F ih F
15 2 14 ax-mp F ih F
16 6 15 eqeltri C
17 16 a1i C
18 oveq1 x = if x x 0 x 2 = if x x 0 2
19 18 oveq2d x = if x x 0 A x 2 = A if x x 0 2
20 oveq2 x = if x x 0 B x = B if x x 0
21 19 20 oveq12d x = if x x 0 A x 2 + B x = A if x x 0 2 + B if x x 0
22 21 oveq1d x = if x x 0 A x 2 + B x + C = A if x x 0 2 + B if x x 0 + C
23 22 breq2d x = if x x 0 0 A x 2 + B x + C 0 A if x x 0 2 + B if x x 0 + C
24 0re 0
25 24 elimel if x x 0
26 1 2 3 4 5 6 25 7 normlem5 0 A if x x 0 2 + B if x x 0 + C
27 23 26 dedth x 0 A x 2 + B x + C
28 27 adantl x 0 A x 2 + B x + C
29 11 13 17 28 discr B 2 4 A C 0
30 29 mptru B 2 4 A C 0
31 12 resqcli B 2
32 4re 4
33 10 16 remulcli A C
34 32 33 remulcli 4 A C
35 31 34 24 lesubadd2i B 2 4 A C 0 B 2 4 A C + 0
36 30 35 mpbi B 2 4 A C + 0
37 34 recni 4 A C
38 37 addid1i 4 A C + 0 = 4 A C
39 36 38 breqtri B 2 4 A C
40 12 sqge0i 0 B 2
41 4pos 0 < 4
42 24 32 41 ltleii 0 4
43 hiidge0 G 0 G ih G
44 3 43 ax-mp 0 G ih G
45 44 5 breqtrri 0 A
46 hiidge0 F 0 F ih F
47 2 46 ax-mp 0 F ih F
48 47 6 breqtrri 0 C
49 10 16 mulge0i 0 A 0 C 0 A C
50 45 48 49 mp2an 0 A C
51 32 33 mulge0i 0 4 0 A C 0 4 A C
52 42 50 51 mp2an 0 4 A C
53 31 34 sqrtlei 0 B 2 0 4 A C B 2 4 A C B 2 4 A C
54 40 52 53 mp2an B 2 4 A C B 2 4 A C
55 39 54 mpbi B 2 4 A C
56 12 absrei B = B 2
57 32 33 42 50 sqrtmulii 4 A C = 4 A C
58 sqrt4 4 = 2
59 10 16 45 48 sqrtmulii A C = A C
60 58 59 oveq12i 4 A C = 2 A C
61 57 60 eqtr2i 2 A C = 4 A C
62 55 56 61 3brtr4i B 2 A C