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 31169

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 11290	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
2		ax-1cn 11242	. . . . . . . . . . . 12 ⊢ 1 ∈ ℂ
3	2	cjrebi 15223	. . . . . . . . . . 11 ⊢ (1 ∈ ℝ ↔ (∗‘1) = 1)
4	1, 3	mpbi 230	. . . . . . . . . 10 ⊢ (∗‘1) = 1
5	4	oveq1i 7458	. . . . . . . . 9 ⊢ ((∗‘1) · (𝐵 ·_ih 𝐴)) = (1 · (𝐵 ·_ih 𝐴))
6		norm-ii.2	. . . . . . . . . . 11 ⊢ 𝐵 ∈ ℋ
7		norm-ii.1	. . . . . . . . . . 11 ⊢ 𝐴 ∈ ℋ
8	6, 7	hicli 31113	. . . . . . . . . 10 ⊢ (𝐵 ·_ih 𝐴) ∈ ℂ
9	8	mullidi 11295	. . . . . . . . 9 ⊢ (1 · (𝐵 ·_ih 𝐴)) = (𝐵 ·_ih 𝐴)
10	5, 9	eqtri 2768	. . . . . . . 8 ⊢ ((∗‘1) · (𝐵 ·_ih 𝐴)) = (𝐵 ·_ih 𝐴)
11	7, 6	hicli 31113	. . . . . . . . 9 ⊢ (𝐴 ·_ih 𝐵) ∈ ℂ
12	11	mullidi 11295	. . . . . . . 8 ⊢ (1 · (𝐴 ·_ih 𝐵)) = (𝐴 ·_ih 𝐵)
13	10, 12	oveq12i 7460	. . . . . . 7 ⊢ (((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵))) = ((𝐵 ·_ih 𝐴) + (𝐴 ·_ih 𝐵))
14		abs1 15346	. . . . . . . 8 ⊢ (abs‘1) = 1
15	2, 6, 7, 14	normlem7 31148	. . . . . . 7 ⊢ (((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵))) ≤ (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵))))
16	13, 15	eqbrtrri 5189	. . . . . 6 ⊢ ((𝐵 ·_ih 𝐴) + (𝐴 ·_ih 𝐵)) ≤ (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵))))
17		eqid 2740	. . . . . . . . . 10 ⊢ -(((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵))) = -(((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵)))
18	2, 6, 7, 17	normlem2 31143	. . . . . . . . 9 ⊢ -(((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵))) ∈ ℝ
19	2	cjcli 15218	. . . . . . . . . . . 12 ⊢ (∗‘1) ∈ ℂ
20	19, 8	mulcli 11297	. . . . . . . . . . 11 ⊢ ((∗‘1) · (𝐵 ·_ih 𝐴)) ∈ ℂ
21	2, 11	mulcli 11297	. . . . . . . . . . 11 ⊢ (1 · (𝐴 ·_ih 𝐵)) ∈ ℂ
22	20, 21	addcli 11296	. . . . . . . . . 10 ⊢ (((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵))) ∈ ℂ
23	22	negrebi 11610	. . . . . . . . 9 ⊢ (-(((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵))) ∈ ℝ ↔ (((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵))) ∈ ℝ)
24	18, 23	mpbi 230	. . . . . . . 8 ⊢ (((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵))) ∈ ℝ
25	13, 24	eqeltrri 2841	. . . . . . 7 ⊢ ((𝐵 ·_ih 𝐴) + (𝐴 ·_ih 𝐵)) ∈ ℝ
26		2re 12367	. . . . . . . 8 ⊢ 2 ∈ ℝ
27		hiidge0 31130	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℋ → 0 ≤ (𝐴 ·_ih 𝐴))
28	7, 27	ax-mp 5	. . . . . . . . . 10 ⊢ 0 ≤ (𝐴 ·_ih 𝐴)
29		hiidrcl 31127	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℋ → (𝐴 ·_ih 𝐴) ∈ ℝ)
30	7, 29	ax-mp 5	. . . . . . . . . . 11 ⊢ (𝐴 ·_ih 𝐴) ∈ ℝ
31	30	sqrtcli 15420	. . . . . . . . . 10 ⊢ (0 ≤ (𝐴 ·_ih 𝐴) → (√‘(𝐴 ·_ih 𝐴)) ∈ ℝ)
32	28, 31	ax-mp 5	. . . . . . . . 9 ⊢ (√‘(𝐴 ·_ih 𝐴)) ∈ ℝ
33		hiidge0 31130	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ℋ → 0 ≤ (𝐵 ·_ih 𝐵))
34	6, 33	ax-mp 5	. . . . . . . . . 10 ⊢ 0 ≤ (𝐵 ·_ih 𝐵)
35		hiidrcl 31127	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ℋ → (𝐵 ·_ih 𝐵) ∈ ℝ)
36	6, 35	ax-mp 5	. . . . . . . . . . 11 ⊢ (𝐵 ·_ih 𝐵) ∈ ℝ
37	36	sqrtcli 15420	. . . . . . . . . 10 ⊢ (0 ≤ (𝐵 ·_ih 𝐵) → (√‘(𝐵 ·_ih 𝐵)) ∈ ℝ)
38	34, 37	ax-mp 5	. . . . . . . . 9 ⊢ (√‘(𝐵 ·_ih 𝐵)) ∈ ℝ
39	32, 38	remulcli 11306	. . . . . . . 8 ⊢ ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵))) ∈ ℝ
40	26, 39	remulcli 11306	. . . . . . 7 ⊢ (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵)))) ∈ ℝ
41	30, 36	readdcli 11305	. . . . . . 7 ⊢ ((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) ∈ ℝ
42	25, 40, 41	leadd2i 11846	. . . . . 6 ⊢ (((𝐵 ·_ih 𝐴) + (𝐴 ·_ih 𝐵)) ≤ (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵)))) ↔ (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + ((𝐵 ·_ih 𝐴) + (𝐴 ·_ih 𝐵))) ≤ (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵))))))
43	16, 42	mpbi 230	. . . . 5 ⊢ (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + ((𝐵 ·_ih 𝐴) + (𝐴 ·_ih 𝐵))) ≤ (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵)))))
44	7, 6, 7, 6	normlem8 31149	. . . . . 6 ⊢ ((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)) = (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + ((𝐴 ·_ih 𝐵) + (𝐵 ·_ih 𝐴)))
45	11, 8	addcomi 11481	. . . . . . 7 ⊢ ((𝐴 ·_ih 𝐵) + (𝐵 ·_ih 𝐴)) = ((𝐵 ·_ih 𝐴) + (𝐴 ·_ih 𝐵))
46	45	oveq2i 7459	. . . . . 6 ⊢ (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + ((𝐴 ·_ih 𝐵) + (𝐵 ·_ih 𝐴))) = (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + ((𝐵 ·_ih 𝐴) + (𝐴 ·_ih 𝐵)))
47	44, 46	eqtri 2768	. . . . 5 ⊢ ((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)) = (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + ((𝐵 ·_ih 𝐴) + (𝐴 ·_ih 𝐵)))
48	32	recni 11304	. . . . . . 7 ⊢ (√‘(𝐴 ·_ih 𝐴)) ∈ ℂ
49	38	recni 11304	. . . . . . 7 ⊢ (√‘(𝐵 ·_ih 𝐵)) ∈ ℂ
50	48, 49	binom2i 14261	. . . . . 6 ⊢ (((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2) = ((((√‘(𝐴 ·_ih 𝐴))↑2) + (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵))))) + ((√‘(𝐵 ·_ih 𝐵))↑2))
51	48	sqcli 14230	. . . . . . 7 ⊢ ((√‘(𝐴 ·_ih 𝐴))↑2) ∈ ℂ
52		2cn 12368	. . . . . . . 8 ⊢ 2 ∈ ℂ
53	48, 49	mulcli 11297	. . . . . . . 8 ⊢ ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵))) ∈ ℂ
54	52, 53	mulcli 11297	. . . . . . 7 ⊢ (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵)))) ∈ ℂ
55	49	sqcli 14230	. . . . . . 7 ⊢ ((√‘(𝐵 ·_ih 𝐵))↑2) ∈ ℂ
56	51, 54, 55	add32i 11513	. . . . . 6 ⊢ ((((√‘(𝐴 ·_ih 𝐴))↑2) + (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵))))) + ((√‘(𝐵 ·_ih 𝐵))↑2)) = ((((√‘(𝐴 ·_ih 𝐴))↑2) + ((√‘(𝐵 ·_ih 𝐵))↑2)) + (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵)))))
57	30	sqsqrti 15424	. . . . . . . . 9 ⊢ (0 ≤ (𝐴 ·_ih 𝐴) → ((√‘(𝐴 ·_ih 𝐴))↑2) = (𝐴 ·_ih 𝐴))
58	28, 57	ax-mp 5	. . . . . . . 8 ⊢ ((√‘(𝐴 ·_ih 𝐴))↑2) = (𝐴 ·_ih 𝐴)
59	36	sqsqrti 15424	. . . . . . . . 9 ⊢ (0 ≤ (𝐵 ·_ih 𝐵) → ((√‘(𝐵 ·_ih 𝐵))↑2) = (𝐵 ·_ih 𝐵))
60	34, 59	ax-mp 5	. . . . . . . 8 ⊢ ((√‘(𝐵 ·_ih 𝐵))↑2) = (𝐵 ·_ih 𝐵)
61	58, 60	oveq12i 7460	. . . . . . 7 ⊢ (((√‘(𝐴 ·_ih 𝐴))↑2) + ((√‘(𝐵 ·_ih 𝐵))↑2)) = ((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵))
62	61	oveq1i 7458	. . . . . 6 ⊢ ((((√‘(𝐴 ·_ih 𝐴))↑2) + ((√‘(𝐵 ·_ih 𝐵))↑2)) + (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵))))) = (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵)))))
63	50, 56, 62	3eqtri 2772	. . . . 5 ⊢ (((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2) = (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵)))))
64	43, 47, 63	3brtr4i 5196	. . . 4 ⊢ ((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)) ≤ (((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2)
65	7, 6	hvaddcli 31050	. . . . . 6 ⊢ (𝐴 +_ℎ 𝐵) ∈ ℋ
66		hiidge0 31130	. . . . . 6 ⊢ ((𝐴 +_ℎ 𝐵) ∈ ℋ → 0 ≤ ((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)))
67	65, 66	ax-mp 5	. . . . 5 ⊢ 0 ≤ ((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵))
68	32, 38	readdcli 11305	. . . . . 6 ⊢ ((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵))) ∈ ℝ
69	68	sqge0i 14237	. . . . 5 ⊢ 0 ≤ (((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2)
70		hiidrcl 31127	. . . . . . 7 ⊢ ((𝐴 +_ℎ 𝐵) ∈ ℋ → ((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)) ∈ ℝ)
71	65, 70	ax-mp 5	. . . . . 6 ⊢ ((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)) ∈ ℝ
72	68	resqcli 14235	. . . . . 6 ⊢ (((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2) ∈ ℝ
73	71, 72	sqrtlei 15437	. . . . 5 ⊢ ((0 ≤ ((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)) ∧ 0 ≤ (((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2)) → (((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)) ≤ (((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2) ↔ (√‘((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵))) ≤ (√‘(((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2))))
74	67, 69, 73	mp2an 691	. . . 4 ⊢ (((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)) ≤ (((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2) ↔ (√‘((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵))) ≤ (√‘(((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2)))
75	64, 74	mpbi 230	. . 3 ⊢ (√‘((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵))) ≤ (√‘(((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2))
76	30	sqrtge0i 15425	. . . . . 6 ⊢ (0 ≤ (𝐴 ·_ih 𝐴) → 0 ≤ (√‘(𝐴 ·_ih 𝐴)))
77	28, 76	ax-mp 5	. . . . 5 ⊢ 0 ≤ (√‘(𝐴 ·_ih 𝐴))
78	36	sqrtge0i 15425	. . . . . 6 ⊢ (0 ≤ (𝐵 ·_ih 𝐵) → 0 ≤ (√‘(𝐵 ·_ih 𝐵)))
79	34, 78	ax-mp 5	. . . . 5 ⊢ 0 ≤ (√‘(𝐵 ·_ih 𝐵))
80	32, 38	addge0i 11830	. . . . 5 ⊢ ((0 ≤ (√‘(𝐴 ·_ih 𝐴)) ∧ 0 ≤ (√‘(𝐵 ·_ih 𝐵))) → 0 ≤ ((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵))))
81	77, 79, 80	mp2an 691	. . . 4 ⊢ 0 ≤ ((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))
82	68	sqrtsqi 15423	. . . 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 5191	. 2 ⊢ (√‘((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵))) ≤ ((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))
85		normval 31156	. . 3 ⊢ ((𝐴 +_ℎ 𝐵) ∈ ℋ → (norm_ℎ‘(𝐴 +_ℎ 𝐵)) = (√‘((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵))))
86	65, 85	ax-mp 5	. 2 ⊢ (norm_ℎ‘(𝐴 +_ℎ 𝐵)) = (√‘((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)))
87		normval 31156	. . . 4 ⊢ (𝐴 ∈ ℋ → (norm_ℎ‘𝐴) = (√‘(𝐴 ·_ih 𝐴)))
88	7, 87	ax-mp 5	. . 3 ⊢ (norm_ℎ‘𝐴) = (√‘(𝐴 ·_ih 𝐴))
89		normval 31156	. . . 4 ⊢ (𝐵 ∈ ℋ → (norm_ℎ‘𝐵) = (√‘(𝐵 ·_ih 𝐵)))
90	6, 89	ax-mp 5	. . 3 ⊢ (norm_ℎ‘𝐵) = (√‘(𝐵 ·_ih 𝐵))
91	88, 90	oveq12i 7460	. 2 ⊢ ((norm_ℎ‘𝐴) + (norm_ℎ‘𝐵)) = ((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))
92	84, 86, 91	3brtr4i 5196	1 ⊢ (norm_ℎ‘(𝐴 +_ℎ 𝐵)) ≤ ((norm_ℎ‘𝐴) + (norm_ℎ‘𝐵))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 206 = wceq 1537 ∈ wcel 2108 class class class wbr 5166 ‘cfv 6573 (class class class)co 7448 ℝcr 11183 0cc0 11184 1c1 11185 + caddc 11187 · cmul 11189 ≤ cle 11325 -cneg 11521 2c2 12348 ↑cexp 14112 ∗ccj 15145 √csqrt 15282 ℋchba 30951 +_ℎ cva 30952 ·_ih csp 30954 norm_ℎcno 30955

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770 ax-cnex 11240 ax-resscn 11241 ax-1cn 11242 ax-icn 11243 ax-addcl 11244 ax-addrcl 11245 ax-mulcl 11246 ax-mulrcl 11247 ax-mulcom 11248 ax-addass 11249 ax-mulass 11250 ax-distr 11251 ax-i2m1 11252 ax-1ne0 11253 ax-1rid 11254 ax-rnegex 11255 ax-rrecex 11256 ax-cnre 11257 ax-pre-lttri 11258 ax-pre-lttrn 11259 ax-pre-ltadd 11260 ax-pre-mulgt0 11261 ax-pre-sup 11262 ax-hfvadd 31032 ax-hv0cl 31035 ax-hfvmul 31037 ax-hvmulass 31039 ax-hvmul0 31042 ax-hfi 31111 ax-his1 31114 ax-his2 31115 ax-his3 31116 ax-his4 31117

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-nel 3053 df-ral 3068 df-rex 3077 df-rmo 3388 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-pss 3996 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-iun 5017 df-br 5167 df-opab 5229 df-mpt 5250 df-tr 5284 df-id 5593 df-eprel 5599 df-po 5607 df-so 5608 df-fr 5652 df-we 5654 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-pred 6332 df-ord 6398 df-on 6399 df-lim 6400 df-suc 6401 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-riota 7404 df-ov 7451 df-oprab 7452 df-mpo 7453 df-om 7904 df-2nd 8031 df-frecs 8322 df-wrecs 8353 df-recs 8427 df-rdg 8466 df-er 8763 df-en 9004 df-dom 9005 df-sdom 9006 df-sup 9511 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11522 df-neg 11523 df-div 11948 df-nn 12294 df-2 12356 df-3 12357 df-4 12358 df-n0 12554 df-z 12640 df-uz 12904 df-rp 13058 df-seq 14053 df-exp 14113 df-cj 15148 df-re 15149 df-im 15150 df-sqrt 15284 df-abs 15285 df-hnorm 31000 df-hvsub 31003

This theorem is referenced by: norm-ii 31170 norm3difi 31179

W3C validator