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 30390

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 11214	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
2		ax-1cn 11168	. . . . . . . . . . . 12 ⊢ 1 ∈ ℂ
3	2	cjrebi 15121	. . . . . . . . . . 11 ⊢ (1 ∈ ℝ ↔ (∗‘1) = 1)
4	1, 3	mpbi 229	. . . . . . . . . 10 ⊢ (∗‘1) = 1
5	4	oveq1i 7419	. . . . . . . . 9 ⊢ ((∗‘1) · (𝐵 ·_ih 𝐴)) = (1 · (𝐵 ·_ih 𝐴))
6		norm-ii.2	. . . . . . . . . . 11 ⊢ 𝐵 ∈ ℋ
7		norm-ii.1	. . . . . . . . . . 11 ⊢ 𝐴 ∈ ℋ
8	6, 7	hicli 30334	. . . . . . . . . 10 ⊢ (𝐵 ·_ih 𝐴) ∈ ℂ
9	8	mullidi 11219	. . . . . . . . 9 ⊢ (1 · (𝐵 ·_ih 𝐴)) = (𝐵 ·_ih 𝐴)
10	5, 9	eqtri 2761	. . . . . . . 8 ⊢ ((∗‘1) · (𝐵 ·_ih 𝐴)) = (𝐵 ·_ih 𝐴)
11	7, 6	hicli 30334	. . . . . . . . 9 ⊢ (𝐴 ·_ih 𝐵) ∈ ℂ
12	11	mullidi 11219	. . . . . . . 8 ⊢ (1 · (𝐴 ·_ih 𝐵)) = (𝐴 ·_ih 𝐵)
13	10, 12	oveq12i 7421	. . . . . . 7 ⊢ (((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵))) = ((𝐵 ·_ih 𝐴) + (𝐴 ·_ih 𝐵))
14		abs1 15244	. . . . . . . 8 ⊢ (abs‘1) = 1
15	2, 6, 7, 14	normlem7 30369	. . . . . . 7 ⊢ (((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵))) ≤ (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵))))
16	13, 15	eqbrtrri 5172	. . . . . 6 ⊢ ((𝐵 ·_ih 𝐴) + (𝐴 ·_ih 𝐵)) ≤ (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵))))
17		eqid 2733	. . . . . . . . . 10 ⊢ -(((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵))) = -(((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵)))
18	2, 6, 7, 17	normlem2 30364	. . . . . . . . 9 ⊢ -(((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵))) ∈ ℝ
19	2	cjcli 15116	. . . . . . . . . . . 12 ⊢ (∗‘1) ∈ ℂ
20	19, 8	mulcli 11221	. . . . . . . . . . 11 ⊢ ((∗‘1) · (𝐵 ·_ih 𝐴)) ∈ ℂ
21	2, 11	mulcli 11221	. . . . . . . . . . 11 ⊢ (1 · (𝐴 ·_ih 𝐵)) ∈ ℂ
22	20, 21	addcli 11220	. . . . . . . . . 10 ⊢ (((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵))) ∈ ℂ
23	22	negrebi 11534	. . . . . . . . 9 ⊢ (-(((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵))) ∈ ℝ ↔ (((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵))) ∈ ℝ)
24	18, 23	mpbi 229	. . . . . . . 8 ⊢ (((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵))) ∈ ℝ
25	13, 24	eqeltrri 2831	. . . . . . 7 ⊢ ((𝐵 ·_ih 𝐴) + (𝐴 ·_ih 𝐵)) ∈ ℝ
26		2re 12286	. . . . . . . 8 ⊢ 2 ∈ ℝ
27		hiidge0 30351	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℋ → 0 ≤ (𝐴 ·_ih 𝐴))
28	7, 27	ax-mp 5	. . . . . . . . . 10 ⊢ 0 ≤ (𝐴 ·_ih 𝐴)
29		hiidrcl 30348	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℋ → (𝐴 ·_ih 𝐴) ∈ ℝ)
30	7, 29	ax-mp 5	. . . . . . . . . . 11 ⊢ (𝐴 ·_ih 𝐴) ∈ ℝ
31	30	sqrtcli 15318	. . . . . . . . . 10 ⊢ (0 ≤ (𝐴 ·_ih 𝐴) → (√‘(𝐴 ·_ih 𝐴)) ∈ ℝ)
32	28, 31	ax-mp 5	. . . . . . . . 9 ⊢ (√‘(𝐴 ·_ih 𝐴)) ∈ ℝ
33		hiidge0 30351	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ℋ → 0 ≤ (𝐵 ·_ih 𝐵))
34	6, 33	ax-mp 5	. . . . . . . . . 10 ⊢ 0 ≤ (𝐵 ·_ih 𝐵)
35		hiidrcl 30348	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ℋ → (𝐵 ·_ih 𝐵) ∈ ℝ)
36	6, 35	ax-mp 5	. . . . . . . . . . 11 ⊢ (𝐵 ·_ih 𝐵) ∈ ℝ
37	36	sqrtcli 15318	. . . . . . . . . 10 ⊢ (0 ≤ (𝐵 ·_ih 𝐵) → (√‘(𝐵 ·_ih 𝐵)) ∈ ℝ)
38	34, 37	ax-mp 5	. . . . . . . . 9 ⊢ (√‘(𝐵 ·_ih 𝐵)) ∈ ℝ
39	32, 38	remulcli 11230	. . . . . . . 8 ⊢ ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵))) ∈ ℝ
40	26, 39	remulcli 11230	. . . . . . 7 ⊢ (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵)))) ∈ ℝ
41	30, 36	readdcli 11229	. . . . . . 7 ⊢ ((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) ∈ ℝ
42	25, 40, 41	leadd2i 11770	. . . . . 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 30370	. . . . . 6 ⊢ ((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)) = (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + ((𝐴 ·_ih 𝐵) + (𝐵 ·_ih 𝐴)))
45	11, 8	addcomi 11405	. . . . . . 7 ⊢ ((𝐴 ·_ih 𝐵) + (𝐵 ·_ih 𝐴)) = ((𝐵 ·_ih 𝐴) + (𝐴 ·_ih 𝐵))
46	45	oveq2i 7420	. . . . . 6 ⊢ (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + ((𝐴 ·_ih 𝐵) + (𝐵 ·_ih 𝐴))) = (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + ((𝐵 ·_ih 𝐴) + (𝐴 ·_ih 𝐵)))
47	44, 46	eqtri 2761	. . . . 5 ⊢ ((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)) = (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + ((𝐵 ·_ih 𝐴) + (𝐴 ·_ih 𝐵)))
48	32	recni 11228	. . . . . . 7 ⊢ (√‘(𝐴 ·_ih 𝐴)) ∈ ℂ
49	38	recni 11228	. . . . . . 7 ⊢ (√‘(𝐵 ·_ih 𝐵)) ∈ ℂ
50	48, 49	binom2i 14176	. . . . . 6 ⊢ (((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2) = ((((√‘(𝐴 ·_ih 𝐴))↑2) + (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵))))) + ((√‘(𝐵 ·_ih 𝐵))↑2))
51	48	sqcli 14145	. . . . . . 7 ⊢ ((√‘(𝐴 ·_ih 𝐴))↑2) ∈ ℂ
52		2cn 12287	. . . . . . . 8 ⊢ 2 ∈ ℂ
53	48, 49	mulcli 11221	. . . . . . . 8 ⊢ ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵))) ∈ ℂ
54	52, 53	mulcli 11221	. . . . . . 7 ⊢ (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵)))) ∈ ℂ
55	49	sqcli 14145	. . . . . . 7 ⊢ ((√‘(𝐵 ·_ih 𝐵))↑2) ∈ ℂ
56	51, 54, 55	add32i 11437	. . . . . 6 ⊢ ((((√‘(𝐴 ·_ih 𝐴))↑2) + (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵))))) + ((√‘(𝐵 ·_ih 𝐵))↑2)) = ((((√‘(𝐴 ·_ih 𝐴))↑2) + ((√‘(𝐵 ·_ih 𝐵))↑2)) + (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵)))))
57	30	sqsqrti 15322	. . . . . . . . 9 ⊢ (0 ≤ (𝐴 ·_ih 𝐴) → ((√‘(𝐴 ·_ih 𝐴))↑2) = (𝐴 ·_ih 𝐴))
58	28, 57	ax-mp 5	. . . . . . . 8 ⊢ ((√‘(𝐴 ·_ih 𝐴))↑2) = (𝐴 ·_ih 𝐴)
59	36	sqsqrti 15322	. . . . . . . . 9 ⊢ (0 ≤ (𝐵 ·_ih 𝐵) → ((√‘(𝐵 ·_ih 𝐵))↑2) = (𝐵 ·_ih 𝐵))
60	34, 59	ax-mp 5	. . . . . . . 8 ⊢ ((√‘(𝐵 ·_ih 𝐵))↑2) = (𝐵 ·_ih 𝐵)
61	58, 60	oveq12i 7421	. . . . . . 7 ⊢ (((√‘(𝐴 ·_ih 𝐴))↑2) + ((√‘(𝐵 ·_ih 𝐵))↑2)) = ((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵))
62	61	oveq1i 7419	. . . . . 6 ⊢ ((((√‘(𝐴 ·_ih 𝐴))↑2) + ((√‘(𝐵 ·_ih 𝐵))↑2)) + (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵))))) = (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵)))))
63	50, 56, 62	3eqtri 2765	. . . . 5 ⊢ (((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2) = (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵)))))
64	43, 47, 63	3brtr4i 5179	. . . 4 ⊢ ((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)) ≤ (((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2)
65	7, 6	hvaddcli 30271	. . . . . 6 ⊢ (𝐴 +_ℎ 𝐵) ∈ ℋ
66		hiidge0 30351	. . . . . 6 ⊢ ((𝐴 +_ℎ 𝐵) ∈ ℋ → 0 ≤ ((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)))
67	65, 66	ax-mp 5	. . . . 5 ⊢ 0 ≤ ((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵))
68	32, 38	readdcli 11229	. . . . . 6 ⊢ ((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵))) ∈ ℝ
69	68	sqge0i 14152	. . . . 5 ⊢ 0 ≤ (((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2)
70		hiidrcl 30348	. . . . . . 7 ⊢ ((𝐴 +_ℎ 𝐵) ∈ ℋ → ((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)) ∈ ℝ)
71	65, 70	ax-mp 5	. . . . . 6 ⊢ ((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)) ∈ ℝ
72	68	resqcli 14150	. . . . . 6 ⊢ (((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2) ∈ ℝ
73	71, 72	sqrtlei 15335	. . . . 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 229	. . 3 ⊢ (√‘((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵))) ≤ (√‘(((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2))
76	30	sqrtge0i 15323	. . . . . 6 ⊢ (0 ≤ (𝐴 ·_ih 𝐴) → 0 ≤ (√‘(𝐴 ·_ih 𝐴)))
77	28, 76	ax-mp 5	. . . . 5 ⊢ 0 ≤ (√‘(𝐴 ·_ih 𝐴))
78	36	sqrtge0i 15323	. . . . . 6 ⊢ (0 ≤ (𝐵 ·_ih 𝐵) → 0 ≤ (√‘(𝐵 ·_ih 𝐵)))
79	34, 78	ax-mp 5	. . . . 5 ⊢ 0 ≤ (√‘(𝐵 ·_ih 𝐵))
80	32, 38	addge0i 11754	. . . . 5 ⊢ ((0 ≤ (√‘(𝐴 ·_ih 𝐴)) ∧ 0 ≤ (√‘(𝐵 ·_ih 𝐵))) → 0 ≤ ((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵))))
81	77, 79, 80	mp2an 691	. . . 4 ⊢ 0 ≤ ((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))
82	68	sqrtsqi 15321	. . . 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 5174	. 2 ⊢ (√‘((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵))) ≤ ((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))
85		normval 30377	. . 3 ⊢ ((𝐴 +_ℎ 𝐵) ∈ ℋ → (norm_ℎ‘(𝐴 +_ℎ 𝐵)) = (√‘((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵))))
86	65, 85	ax-mp 5	. 2 ⊢ (norm_ℎ‘(𝐴 +_ℎ 𝐵)) = (√‘((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)))
87		normval 30377	. . . 4 ⊢ (𝐴 ∈ ℋ → (norm_ℎ‘𝐴) = (√‘(𝐴 ·_ih 𝐴)))
88	7, 87	ax-mp 5	. . 3 ⊢ (norm_ℎ‘𝐴) = (√‘(𝐴 ·_ih 𝐴))
89		normval 30377	. . . 4 ⊢ (𝐵 ∈ ℋ → (norm_ℎ‘𝐵) = (√‘(𝐵 ·_ih 𝐵)))
90	6, 89	ax-mp 5	. . 3 ⊢ (norm_ℎ‘𝐵) = (√‘(𝐵 ·_ih 𝐵))
91	88, 90	oveq12i 7421	. 2 ⊢ ((norm_ℎ‘𝐴) + (norm_ℎ‘𝐵)) = ((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))
92	84, 86, 91	3brtr4i 5179	1 ⊢ (norm_ℎ‘(𝐴 +_ℎ 𝐵)) ≤ ((norm_ℎ‘𝐴) + (norm_ℎ‘𝐵))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 205 = wceq 1542 ∈ wcel 2107 class class class wbr 5149 ‘cfv 6544 (class class class)co 7409 ℝcr 11109 0cc0 11110 1c1 11111 + caddc 11113 · cmul 11115 ≤ cle 11249 -cneg 11445 2c2 12267 ↑cexp 14027 ∗ccj 15043 √csqrt 15180 ℋchba 30172 +_ℎ cva 30173 ·_ih csp 30175 norm_ℎcno 30176

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725 ax-cnex 11166 ax-resscn 11167 ax-1cn 11168 ax-icn 11169 ax-addcl 11170 ax-addrcl 11171 ax-mulcl 11172 ax-mulrcl 11173 ax-mulcom 11174 ax-addass 11175 ax-mulass 11176 ax-distr 11177 ax-i2m1 11178 ax-1ne0 11179 ax-1rid 11180 ax-rnegex 11181 ax-rrecex 11182 ax-cnre 11183 ax-pre-lttri 11184 ax-pre-lttrn 11185 ax-pre-ltadd 11186 ax-pre-mulgt0 11187 ax-pre-sup 11188 ax-hfvadd 30253 ax-hv0cl 30256 ax-hfvmul 30258 ax-hvmulass 30260 ax-hvmul0 30263 ax-hfi 30332 ax-his1 30335 ax-his2 30336 ax-his3 30337 ax-his4 30338

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-pss 3968 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-iun 5000 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5575 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-we 5634 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-pred 6301 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-riota 7365 df-ov 7412 df-oprab 7413 df-mpo 7414 df-om 7856 df-2nd 7976 df-frecs 8266 df-wrecs 8297 df-recs 8371 df-rdg 8410 df-er 8703 df-en 8940 df-dom 8941 df-sdom 8942 df-sup 9437 df-pnf 11250 df-mnf 11251 df-xr 11252 df-ltxr 11253 df-le 11254 df-sub 11446 df-neg 11447 df-div 11872 df-nn 12213 df-2 12275 df-3 12276 df-4 12277 df-n0 12473 df-z 12559 df-uz 12823 df-rp 12975 df-seq 13967 df-exp 14028 df-cj 15046 df-re 15047 df-im 15048 df-sqrt 15182 df-abs 15183 df-hnorm 30221 df-hvsub 30224

This theorem is referenced by: norm-ii 30391 norm3difi 30400

W3C validator