norm-ii-i - Hilbert Space Explorer

	Hilbert Space Explorer		< Previous Next > Nearby theorems
Mirrors > Home > HSE Home > Th. List > norm-ii-i		Structured version Visualization version GIF version

Theorem norm-ii-i 29400

Description: Triangle inequality for norms. Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 11-Aug-1999.) (New usage is discouraged.)

**Hypotheses**
Ref	Expression
norm-ii.1	⊢ 𝐴 ∈ ℋ
norm-ii.2	⊢ 𝐵 ∈ ℋ

**Assertion**
Ref	Expression
norm-ii-i	⊢ (norm_ℎ‘(𝐴 +_ℎ 𝐵)) ≤ ((norm_ℎ‘𝐴) + (norm_ℎ‘𝐵))

**Proof of Theorem norm-ii-i**
Step	Hyp	Ref	Expression
1		1re 10906	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
2		ax-1cn 10860	. . . . . . . . . . . 12 ⊢ 1 ∈ ℂ
3	2	cjrebi 14813	. . . . . . . . . . 11 ⊢ (1 ∈ ℝ ↔ (∗‘1) = 1)
4	1, 3	mpbi 229	. . . . . . . . . 10 ⊢ (∗‘1) = 1
5	4	oveq1i 7265	. . . . . . . . 9 ⊢ ((∗‘1) · (𝐵 ·_ih 𝐴)) = (1 · (𝐵 ·_ih 𝐴))
6		norm-ii.2	. . . . . . . . . . 11 ⊢ 𝐵 ∈ ℋ
7		norm-ii.1	. . . . . . . . . . 11 ⊢ 𝐴 ∈ ℋ
8	6, 7	hicli 29344	. . . . . . . . . 10 ⊢ (𝐵 ·_ih 𝐴) ∈ ℂ
9	8	mulid2i 10911	. . . . . . . . 9 ⊢ (1 · (𝐵 ·_ih 𝐴)) = (𝐵 ·_ih 𝐴)
10	5, 9	eqtri 2766	. . . . . . . 8 ⊢ ((∗‘1) · (𝐵 ·_ih 𝐴)) = (𝐵 ·_ih 𝐴)
11	7, 6	hicli 29344	. . . . . . . . 9 ⊢ (𝐴 ·_ih 𝐵) ∈ ℂ
12	11	mulid2i 10911	. . . . . . . 8 ⊢ (1 · (𝐴 ·_ih 𝐵)) = (𝐴 ·_ih 𝐵)
13	10, 12	oveq12i 7267	. . . . . . 7 ⊢ (((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵))) = ((𝐵 ·_ih 𝐴) + (𝐴 ·_ih 𝐵))
14		abs1 14937	. . . . . . . 8 ⊢ (abs‘1) = 1
15	2, 6, 7, 14	normlem7 29379	. . . . . . 7 ⊢ (((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵))) ≤ (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵))))
16	13, 15	eqbrtrri 5093	. . . . . 6 ⊢ ((𝐵 ·_ih 𝐴) + (𝐴 ·_ih 𝐵)) ≤ (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵))))
17		eqid 2738	. . . . . . . . . 10 ⊢ -(((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵))) = -(((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵)))
18	2, 6, 7, 17	normlem2 29374	. . . . . . . . 9 ⊢ -(((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵))) ∈ ℝ
19	2	cjcli 14808	. . . . . . . . . . . 12 ⊢ (∗‘1) ∈ ℂ
20	19, 8	mulcli 10913	. . . . . . . . . . 11 ⊢ ((∗‘1) · (𝐵 ·_ih 𝐴)) ∈ ℂ
21	2, 11	mulcli 10913	. . . . . . . . . . 11 ⊢ (1 · (𝐴 ·_ih 𝐵)) ∈ ℂ
22	20, 21	addcli 10912	. . . . . . . . . 10 ⊢ (((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵))) ∈ ℂ
23	22	negrebi 11225	. . . . . . . . 9 ⊢ (-(((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵))) ∈ ℝ ↔ (((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵))) ∈ ℝ)
24	18, 23	mpbi 229	. . . . . . . 8 ⊢ (((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵))) ∈ ℝ
25	13, 24	eqeltrri 2836	. . . . . . 7 ⊢ ((𝐵 ·_ih 𝐴) + (𝐴 ·_ih 𝐵)) ∈ ℝ
26		2re 11977	. . . . . . . 8 ⊢ 2 ∈ ℝ
27		hiidge0 29361	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℋ → 0 ≤ (𝐴 ·_ih 𝐴))
28	7, 27	ax-mp 5	. . . . . . . . . 10 ⊢ 0 ≤ (𝐴 ·_ih 𝐴)
29		hiidrcl 29358	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℋ → (𝐴 ·_ih 𝐴) ∈ ℝ)
30	7, 29	ax-mp 5	. . . . . . . . . . 11 ⊢ (𝐴 ·_ih 𝐴) ∈ ℝ
31	30	sqrtcli 15011	. . . . . . . . . 10 ⊢ (0 ≤ (𝐴 ·_ih 𝐴) → (√‘(𝐴 ·_ih 𝐴)) ∈ ℝ)
32	28, 31	ax-mp 5	. . . . . . . . 9 ⊢ (√‘(𝐴 ·_ih 𝐴)) ∈ ℝ
33		hiidge0 29361	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ℋ → 0 ≤ (𝐵 ·_ih 𝐵))
34	6, 33	ax-mp 5	. . . . . . . . . 10 ⊢ 0 ≤ (𝐵 ·_ih 𝐵)
35		hiidrcl 29358	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ℋ → (𝐵 ·_ih 𝐵) ∈ ℝ)
36	6, 35	ax-mp 5	. . . . . . . . . . 11 ⊢ (𝐵 ·_ih 𝐵) ∈ ℝ
37	36	sqrtcli 15011	. . . . . . . . . 10 ⊢ (0 ≤ (𝐵 ·_ih 𝐵) → (√‘(𝐵 ·_ih 𝐵)) ∈ ℝ)
38	34, 37	ax-mp 5	. . . . . . . . 9 ⊢ (√‘(𝐵 ·_ih 𝐵)) ∈ ℝ
39	32, 38	remulcli 10922	. . . . . . . 8 ⊢ ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵))) ∈ ℝ
40	26, 39	remulcli 10922	. . . . . . 7 ⊢ (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵)))) ∈ ℝ
41	30, 36	readdcli 10921	. . . . . . 7 ⊢ ((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) ∈ ℝ
42	25, 40, 41	leadd2i 11461	. . . . . 6 ⊢ (((𝐵 ·_ih 𝐴) + (𝐴 ·_ih 𝐵)) ≤ (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵)))) ↔ (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + ((𝐵 ·_ih 𝐴) + (𝐴 ·_ih 𝐵))) ≤ (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵))))))
43	16, 42	mpbi 229	. . . . 5 ⊢ (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + ((𝐵 ·_ih 𝐴) + (𝐴 ·_ih 𝐵))) ≤ (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵)))))
44	7, 6, 7, 6	normlem8 29380	. . . . . 6 ⊢ ((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)) = (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + ((𝐴 ·_ih 𝐵) + (𝐵 ·_ih 𝐴)))
45	11, 8	addcomi 11096	. . . . . . 7 ⊢ ((𝐴 ·_ih 𝐵) + (𝐵 ·_ih 𝐴)) = ((𝐵 ·_ih 𝐴) + (𝐴 ·_ih 𝐵))
46	45	oveq2i 7266	. . . . . 6 ⊢ (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + ((𝐴 ·_ih 𝐵) + (𝐵 ·_ih 𝐴))) = (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + ((𝐵 ·_ih 𝐴) + (𝐴 ·_ih 𝐵)))
47	44, 46	eqtri 2766	. . . . 5 ⊢ ((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)) = (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + ((𝐵 ·_ih 𝐴) + (𝐴 ·_ih 𝐵)))
48	32	recni 10920	. . . . . . 7 ⊢ (√‘(𝐴 ·_ih 𝐴)) ∈ ℂ
49	38	recni 10920	. . . . . . 7 ⊢ (√‘(𝐵 ·_ih 𝐵)) ∈ ℂ
50	48, 49	binom2i 13856	. . . . . 6 ⊢ (((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2) = ((((√‘(𝐴 ·_ih 𝐴))↑2) + (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵))))) + ((√‘(𝐵 ·_ih 𝐵))↑2))
51	48	sqcli 13826	. . . . . . 7 ⊢ ((√‘(𝐴 ·_ih 𝐴))↑2) ∈ ℂ
52		2cn 11978	. . . . . . . 8 ⊢ 2 ∈ ℂ
53	48, 49	mulcli 10913	. . . . . . . 8 ⊢ ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵))) ∈ ℂ
54	52, 53	mulcli 10913	. . . . . . 7 ⊢ (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵)))) ∈ ℂ
55	49	sqcli 13826	. . . . . . 7 ⊢ ((√‘(𝐵 ·_ih 𝐵))↑2) ∈ ℂ
56	51, 54, 55	add32i 11128	. . . . . 6 ⊢ ((((√‘(𝐴 ·_ih 𝐴))↑2) + (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵))))) + ((√‘(𝐵 ·_ih 𝐵))↑2)) = ((((√‘(𝐴 ·_ih 𝐴))↑2) + ((√‘(𝐵 ·_ih 𝐵))↑2)) + (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵)))))
57	30	sqsqrti 15015	. . . . . . . . 9 ⊢ (0 ≤ (𝐴 ·_ih 𝐴) → ((√‘(𝐴 ·_ih 𝐴))↑2) = (𝐴 ·_ih 𝐴))
58	28, 57	ax-mp 5	. . . . . . . 8 ⊢ ((√‘(𝐴 ·_ih 𝐴))↑2) = (𝐴 ·_ih 𝐴)
59	36	sqsqrti 15015	. . . . . . . . 9 ⊢ (0 ≤ (𝐵 ·_ih 𝐵) → ((√‘(𝐵 ·_ih 𝐵))↑2) = (𝐵 ·_ih 𝐵))
60	34, 59	ax-mp 5	. . . . . . . 8 ⊢ ((√‘(𝐵 ·_ih 𝐵))↑2) = (𝐵 ·_ih 𝐵)
61	58, 60	oveq12i 7267	. . . . . . 7 ⊢ (((√‘(𝐴 ·_ih 𝐴))↑2) + ((√‘(𝐵 ·_ih 𝐵))↑2)) = ((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵))
62	61	oveq1i 7265	. . . . . 6 ⊢ ((((√‘(𝐴 ·_ih 𝐴))↑2) + ((√‘(𝐵 ·_ih 𝐵))↑2)) + (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵))))) = (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵)))))
63	50, 56, 62	3eqtri 2770	. . . . 5 ⊢ (((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2) = (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵)))))
64	43, 47, 63	3brtr4i 5100	. . . 4 ⊢ ((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)) ≤ (((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2)
65	7, 6	hvaddcli 29281	. . . . . 6 ⊢ (𝐴 +_ℎ 𝐵) ∈ ℋ
66		hiidge0 29361	. . . . . 6 ⊢ ((𝐴 +_ℎ 𝐵) ∈ ℋ → 0 ≤ ((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)))
67	65, 66	ax-mp 5	. . . . 5 ⊢ 0 ≤ ((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵))
68	32, 38	readdcli 10921	. . . . . 6 ⊢ ((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵))) ∈ ℝ
69	68	sqge0i 13833	. . . . 5 ⊢ 0 ≤ (((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2)
70		hiidrcl 29358	. . . . . . 7 ⊢ ((𝐴 +_ℎ 𝐵) ∈ ℋ → ((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)) ∈ ℝ)
71	65, 70	ax-mp 5	. . . . . 6 ⊢ ((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)) ∈ ℝ
72	68	resqcli 13831	. . . . . 6 ⊢ (((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2) ∈ ℝ
73	71, 72	sqrtlei 15028	. . . . 5 ⊢ ((0 ≤ ((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)) ∧ 0 ≤ (((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2)) → (((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)) ≤ (((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2) ↔ (√‘((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵))) ≤ (√‘(((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2))))
74	67, 69, 73	mp2an 688	. . . 4 ⊢ (((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)) ≤ (((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2) ↔ (√‘((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵))) ≤ (√‘(((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2)))
75	64, 74	mpbi 229	. . 3 ⊢ (√‘((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵))) ≤ (√‘(((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2))
76	30	sqrtge0i 15016	. . . . . 6 ⊢ (0 ≤ (𝐴 ·_ih 𝐴) → 0 ≤ (√‘(𝐴 ·_ih 𝐴)))
77	28, 76	ax-mp 5	. . . . 5 ⊢ 0 ≤ (√‘(𝐴 ·_ih 𝐴))
78	36	sqrtge0i 15016	. . . . . 6 ⊢ (0 ≤ (𝐵 ·_ih 𝐵) → 0 ≤ (√‘(𝐵 ·_ih 𝐵)))
79	34, 78	ax-mp 5	. . . . 5 ⊢ 0 ≤ (√‘(𝐵 ·_ih 𝐵))
80	32, 38	addge0i 11445	. . . . 5 ⊢ ((0 ≤ (√‘(𝐴 ·_ih 𝐴)) ∧ 0 ≤ (√‘(𝐵 ·_ih 𝐵))) → 0 ≤ ((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵))))
81	77, 79, 80	mp2an 688	. . . 4 ⊢ 0 ≤ ((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))
82	68	sqrtsqi 15014	. . . 4 ⊢ (0 ≤ ((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵))) → (√‘(((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2)) = ((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵))))
83	81, 82	ax-mp 5	. . 3 ⊢ (√‘(((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2)) = ((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))
84	75, 83	breqtri 5095	. 2 ⊢ (√‘((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵))) ≤ ((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))
85		normval 29387	. . 3 ⊢ ((𝐴 +_ℎ 𝐵) ∈ ℋ → (norm_ℎ‘(𝐴 +_ℎ 𝐵)) = (√‘((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵))))
86	65, 85	ax-mp 5	. 2 ⊢ (norm_ℎ‘(𝐴 +_ℎ 𝐵)) = (√‘((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)))
87		normval 29387	. . . 4 ⊢ (𝐴 ∈ ℋ → (norm_ℎ‘𝐴) = (√‘(𝐴 ·_ih 𝐴)))
88	7, 87	ax-mp 5	. . 3 ⊢ (norm_ℎ‘𝐴) = (√‘(𝐴 ·_ih 𝐴))
89		normval 29387	. . . 4 ⊢ (𝐵 ∈ ℋ → (norm_ℎ‘𝐵) = (√‘(𝐵 ·_ih 𝐵)))
90	6, 89	ax-mp 5	. . 3 ⊢ (norm_ℎ‘𝐵) = (√‘(𝐵 ·_ih 𝐵))
91	88, 90	oveq12i 7267	. 2 ⊢ ((norm_ℎ‘𝐴) + (norm_ℎ‘𝐵)) = ((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))
92	84, 86, 91	3brtr4i 5100	1 ⊢ (norm_ℎ‘(𝐴 +_ℎ 𝐵)) ≤ ((norm_ℎ‘𝐴) + (norm_ℎ‘𝐵))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 205 = wceq 1539 ∈ wcel 2108 class class class wbr 5070 ‘cfv 6418 (class class class)co 7255 ℝcr 10801 0cc0 10802 1c1 10803 + caddc 10805 · cmul 10807 ≤ cle 10941 -cneg 11136 2c2 11958 ↑cexp 13710 ∗ccj 14735 √csqrt 14872 ℋchba 29182 +_ℎ cva 29183 ·_ih csp 29185 norm_ℎcno 29186

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879 ax-pre-sup 10880 ax-hfvadd 29263 ax-hv0cl 29266 ax-hfvmul 29268 ax-hvmulass 29270 ax-hvmul0 29273 ax-hfi 29342 ax-his1 29345 ax-his2 29346 ax-his3 29347 ax-his4 29348

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-om 7688 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-er 8456 df-en 8692 df-dom 8693 df-sdom 8694 df-sup 9131 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-div 11563 df-nn 11904 df-2 11966 df-3 11967 df-4 11968 df-n0 12164 df-z 12250 df-uz 12512 df-rp 12660 df-seq 13650 df-exp 13711 df-cj 14738 df-re 14739 df-im 14740 df-sqrt 14874 df-abs 14875 df-hnorm 29231 df-hvsub 29234

This theorem is referenced by: norm-ii 29401 norm3difi 29410

W3C validator