Hilbert Space Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HSE Home  >  Th. List  >  normlem3 Unicode version

Theorem normlem3 21691
 Description: Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 21-Aug-1999.) (New usage is discouraged.)
Hypotheses
Ref Expression
normlem1.1
normlem1.2
normlem1.3
normlem2.4
normlem3.5
normlem3.6
normlem3.7
Assertion
Ref Expression
normlem3

Proof of Theorem normlem3
StepHypRef Expression
1 normlem3.6 . . 3
2 normlem3.5 . . . . . . 7
3 normlem1.3 . . . . . . . 8
43, 3hicli 21660 . . . . . . 7
52, 4eqeltri 2353 . . . . . 6
6 normlem3.7 . . . . . . . 8
76recni 8849 . . . . . . 7
87sqcli 11184 . . . . . 6
95, 8mulcli 8842 . . . . 5
10 normlem1.1 . . . . . . . 8
11 normlem1.2 . . . . . . . 8
12 normlem2.4 . . . . . . . 8
1310, 11, 3, 12normlem2 21690 . . . . . . 7
1413recni 8849 . . . . . 6
1514, 7mulcli 8842 . . . . 5
169, 15addcomi 9003 . . . 4
1710cjcli 11654 . . . . . . . . . 10
1811, 3hicli 21660 . . . . . . . . . 10
1917, 18mulcli 8842 . . . . . . . . 9
203, 11hicli 21660 . . . . . . . . . 10
2110, 20mulcli 8842 . . . . . . . . 9
2219, 21addcli 8841 . . . . . . . 8
2322, 7mulneg1i 9225 . . . . . . 7
2412oveq1i 5868 . . . . . . 7
2522, 7mulneg2i 9226 . . . . . . 7
2623, 24, 253eqtr4i 2313 . . . . . 6
277negcli 9114 . . . . . . 7
2819, 21, 27adddiri 8848 . . . . . 6
2917, 18, 27mul32i 9008 . . . . . . 7
3010, 20, 27mul32i 9008 . . . . . . 7
3129, 30oveq12i 5870 . . . . . 6
3226, 28, 313eqtri 2307 . . . . 5
332oveq2i 5869 . . . . . 6
348, 5, 33mulcomli 8844 . . . . 5
3532, 34oveq12i 5870 . . . 4
3617, 27mulcli 8842 . . . . . 6
3736, 18mulcli 8842 . . . . 5
3810, 27mulcli 8842 . . . . . 6
3938, 20mulcli 8842 . . . . 5
408, 4mulcli 8842 . . . . 5
4137, 39, 40addassi 8845 . . . 4
4216, 35, 413eqtri 2307 . . 3
431, 42oveq12i 5870 . 2
449, 15addcli 8841 . . 3
4511, 11hicli 21660 . . . 4
461, 45eqeltri 2353 . . 3