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 31394

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 11196	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
2		ax-1cn 11146	. . . . . . . . . . . 12 ⊢ 1 ∈ ℂ
3	2	cjrebi 15213	. . . . . . . . . . 11 ⊢ (1 ∈ ℝ ↔ (∗‘1) = 1)
4	1, 3	mpbi 233	. . . . . . . . . 10 ⊢ (∗‘1) = 1
5	4	oveq1i 7410	. . . . . . . . 9 ⊢ ((∗‘1) · (𝐵 ·_ih 𝐴)) = (1 · (𝐵 ·_ih 𝐴))
6		norm-ii.2	. . . . . . . . . . 11 ⊢ 𝐵 ∈ ℋ
7		norm-ii.1	. . . . . . . . . . 11 ⊢ 𝐴 ∈ ℋ
8	6, 7	hicli 31338	. . . . . . . . . 10 ⊢ (𝐵 ·_ih 𝐴) ∈ ℂ
9	8	mullidi 11202	. . . . . . . . 9 ⊢ (1 · (𝐵 ·_ih 𝐴)) = (𝐵 ·_ih 𝐴)
10	5, 9	eqtri 2788	. . . . . . . 8 ⊢ ((∗‘1) · (𝐵 ·_ih 𝐴)) = (𝐵 ·_ih 𝐴)
11	7, 6	hicli 31338	. . . . . . . . 9 ⊢ (𝐴 ·_ih 𝐵) ∈ ℂ
12	11	mullidi 11202	. . . . . . . 8 ⊢ (1 · (𝐴 ·_ih 𝐵)) = (𝐴 ·_ih 𝐵)
13	10, 12	oveq12i 7412	. . . . . . 7 ⊢ (((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵))) = ((𝐵 ·_ih 𝐴) + (𝐴 ·_ih 𝐵))
14		abs1 15336	. . . . . . . 8 ⊢ (abs‘1) = 1
15	2, 6, 7, 14	normlem7 31373	. . . . . . 7 ⊢ (((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵))) ≤ (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵))))
16	13, 15	eqbrtrri 5127	. . . . . 6 ⊢ ((𝐵 ·_ih 𝐴) + (𝐴 ·_ih 𝐵)) ≤ (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵))))
17		eqid 2765	. . . . . . . . . 10 ⊢ -(((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵))) = -(((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵)))
18	2, 6, 7, 17	normlem2 31368	. . . . . . . . 9 ⊢ -(((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵))) ∈ ℝ
19	2	cjcli 15208	. . . . . . . . . . . 12 ⊢ (∗‘1) ∈ ℂ
20	19, 8	mulcli 11204	. . . . . . . . . . 11 ⊢ ((∗‘1) · (𝐵 ·_ih 𝐴)) ∈ ℂ
21	2, 11	mulcli 11204	. . . . . . . . . . 11 ⊢ (1 · (𝐴 ·_ih 𝐵)) ∈ ℂ
22	20, 21	addcli 11203	. . . . . . . . . 10 ⊢ (((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵))) ∈ ℂ
23	22	negrebi 11520	. . . . . . . . 9 ⊢ (-(((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵))) ∈ ℝ ↔ (((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵))) ∈ ℝ)
24	18, 23	mpbi 233	. . . . . . . 8 ⊢ (((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵))) ∈ ℝ
25	13, 24	eqeltrri 2862	. . . . . . 7 ⊢ ((𝐵 ·_ih 𝐴) + (𝐴 ·_ih 𝐵)) ∈ ℝ
26		2re 12303	. . . . . . . 8 ⊢ 2 ∈ ℝ
27		hiidge0 31355	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℋ → 0 ≤ (𝐴 ·_ih 𝐴))
28	7, 27	ax-mp 5	. . . . . . . . . 10 ⊢ 0 ≤ (𝐴 ·_ih 𝐴)
29		hiidrcl 31352	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℋ → (𝐴 ·_ih 𝐴) ∈ ℝ)
30	7, 29	ax-mp 5	. . . . . . . . . . 11 ⊢ (𝐴 ·_ih 𝐴) ∈ ℝ
31	30	sqrtcli 15411	. . . . . . . . . 10 ⊢ (0 ≤ (𝐴 ·_ih 𝐴) → (√‘(𝐴 ·_ih 𝐴)) ∈ ℝ)
32	28, 31	ax-mp 5	. . . . . . . . 9 ⊢ (√‘(𝐴 ·_ih 𝐴)) ∈ ℝ
33		hiidge0 31355	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ℋ → 0 ≤ (𝐵 ·_ih 𝐵))
34	6, 33	ax-mp 5	. . . . . . . . . 10 ⊢ 0 ≤ (𝐵 ·_ih 𝐵)
35		hiidrcl 31352	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ℋ → (𝐵 ·_ih 𝐵) ∈ ℝ)
36	6, 35	ax-mp 5	. . . . . . . . . . 11 ⊢ (𝐵 ·_ih 𝐵) ∈ ℝ
37	36	sqrtcli 15411	. . . . . . . . . 10 ⊢ (0 ≤ (𝐵 ·_ih 𝐵) → (√‘(𝐵 ·_ih 𝐵)) ∈ ℝ)
38	34, 37	ax-mp 5	. . . . . . . . 9 ⊢ (√‘(𝐵 ·_ih 𝐵)) ∈ ℝ
39	32, 38	remulcli 11213	. . . . . . . 8 ⊢ ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵))) ∈ ℝ
40	26, 39	remulcli 11213	. . . . . . 7 ⊢ (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵)))) ∈ ℝ
41	30, 36	readdcli 11212	. . . . . . 7 ⊢ ((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) ∈ ℝ
42	25, 40, 41	leadd2i 11758	. . . . . 6 ⊢ (((𝐵 ·_ih 𝐴) + (𝐴 ·_ih 𝐵)) ≤ (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵)))) ↔ (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + ((𝐵 ·_ih 𝐴) + (𝐴 ·_ih 𝐵))) ≤ (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵))))))
43	16, 42	mpbi 233	. . . . 5 ⊢ (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + ((𝐵 ·_ih 𝐴) + (𝐴 ·_ih 𝐵))) ≤ (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵)))))
44	7, 6, 7, 6	normlem8 31374	. . . . . 6 ⊢ ((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)) = (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + ((𝐴 ·_ih 𝐵) + (𝐵 ·_ih 𝐴)))
45	11, 8	addcomi 11389	. . . . . . 7 ⊢ ((𝐴 ·_ih 𝐵) + (𝐵 ·_ih 𝐴)) = ((𝐵 ·_ih 𝐴) + (𝐴 ·_ih 𝐵))
46	45	oveq2i 7411	. . . . . 6 ⊢ (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + ((𝐴 ·_ih 𝐵) + (𝐵 ·_ih 𝐴))) = (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + ((𝐵 ·_ih 𝐴) + (𝐴 ·_ih 𝐵)))
47	44, 46	eqtri 2788	. . . . 5 ⊢ ((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)) = (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + ((𝐵 ·_ih 𝐴) + (𝐴 ·_ih 𝐵)))
48	32	recni 11211	. . . . . . 7 ⊢ (√‘(𝐴 ·_ih 𝐴)) ∈ ℂ
49	38	recni 11211	. . . . . . 7 ⊢ (√‘(𝐵 ·_ih 𝐵)) ∈ ℂ
50	48, 49	binom2i 14236	. . . . . 6 ⊢ (((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2) = ((((√‘(𝐴 ·_ih 𝐴))↑2) + (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵))))) + ((√‘(𝐵 ·_ih 𝐵))↑2))
51	48	sqcli 14205	. . . . . . 7 ⊢ ((√‘(𝐴 ·_ih 𝐴))↑2) ∈ ℂ
52		2cn 12304	. . . . . . . 8 ⊢ 2 ∈ ℂ
53	48, 49	mulcli 11204	. . . . . . . 8 ⊢ ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵))) ∈ ℂ
54	52, 53	mulcli 11204	. . . . . . 7 ⊢ (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵)))) ∈ ℂ
55	49	sqcli 14205	. . . . . . 7 ⊢ ((√‘(𝐵 ·_ih 𝐵))↑2) ∈ ℂ
56	51, 54, 55	add32i 11422	. . . . . 6 ⊢ ((((√‘(𝐴 ·_ih 𝐴))↑2) + (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵))))) + ((√‘(𝐵 ·_ih 𝐵))↑2)) = ((((√‘(𝐴 ·_ih 𝐴))↑2) + ((√‘(𝐵 ·_ih 𝐵))↑2)) + (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵)))))
57	30	sqsqrti 15415	. . . . . . . . 9 ⊢ (0 ≤ (𝐴 ·_ih 𝐴) → ((√‘(𝐴 ·_ih 𝐴))↑2) = (𝐴 ·_ih 𝐴))
58	28, 57	ax-mp 5	. . . . . . . 8 ⊢ ((√‘(𝐴 ·_ih 𝐴))↑2) = (𝐴 ·_ih 𝐴)
59	36	sqsqrti 15415	. . . . . . . . 9 ⊢ (0 ≤ (𝐵 ·_ih 𝐵) → ((√‘(𝐵 ·_ih 𝐵))↑2) = (𝐵 ·_ih 𝐵))
60	34, 59	ax-mp 5	. . . . . . . 8 ⊢ ((√‘(𝐵 ·_ih 𝐵))↑2) = (𝐵 ·_ih 𝐵)
61	58, 60	oveq12i 7412	. . . . . . 7 ⊢ (((√‘(𝐴 ·_ih 𝐴))↑2) + ((√‘(𝐵 ·_ih 𝐵))↑2)) = ((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵))
62	61	oveq1i 7410	. . . . . 6 ⊢ ((((√‘(𝐴 ·_ih 𝐴))↑2) + ((√‘(𝐵 ·_ih 𝐵))↑2)) + (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵))))) = (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵)))))
63	50, 56, 62	3eqtri 2792	. . . . 5 ⊢ (((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2) = (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵)))))
64	43, 47, 63	3brtr4i 5134	. . . 4 ⊢ ((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)) ≤ (((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2)
65	7, 6	hvaddcli 31275	. . . . . 6 ⊢ (𝐴 +_ℎ 𝐵) ∈ ℋ
66		hiidge0 31355	. . . . . 6 ⊢ ((𝐴 +_ℎ 𝐵) ∈ ℋ → 0 ≤ ((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)))
67	65, 66	ax-mp 5	. . . . 5 ⊢ 0 ≤ ((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵))
68	32, 38	readdcli 11212	. . . . . 6 ⊢ ((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵))) ∈ ℝ
69	68	sqge0i 14212	. . . . 5 ⊢ 0 ≤ (((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2)
70		hiidrcl 31352	. . . . . . 7 ⊢ ((𝐴 +_ℎ 𝐵) ∈ ℋ → ((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)) ∈ ℝ)
71	65, 70	ax-mp 5	. . . . . 6 ⊢ ((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)) ∈ ℝ
72	68	resqcli 14210	. . . . . 6 ⊢ (((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2) ∈ ℝ
73	71, 72	sqrtlei 15428	. . . . 5 ⊢ ((0 ≤ ((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)) ∧ 0 ≤ (((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2)) → (((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)) ≤ (((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2) ↔ (√‘((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵))) ≤ (√‘(((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2))))
74	67, 69, 73	mp2an 704	. . . 4 ⊢ (((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)) ≤ (((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2) ↔ (√‘((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵))) ≤ (√‘(((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2)))
75	64, 74	mpbi 233	. . 3 ⊢ (√‘((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵))) ≤ (√‘(((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2))
76	30	sqrtge0i 15416	. . . . . 6 ⊢ (0 ≤ (𝐴 ·_ih 𝐴) → 0 ≤ (√‘(𝐴 ·_ih 𝐴)))
77	28, 76	ax-mp 5	. . . . 5 ⊢ 0 ≤ (√‘(𝐴 ·_ih 𝐴))
78	36	sqrtge0i 15416	. . . . . 6 ⊢ (0 ≤ (𝐵 ·_ih 𝐵) → 0 ≤ (√‘(𝐵 ·_ih 𝐵)))
79	34, 78	ax-mp 5	. . . . 5 ⊢ 0 ≤ (√‘(𝐵 ·_ih 𝐵))
80	32, 38	addge0i 11742	. . . . 5 ⊢ ((0 ≤ (√‘(𝐴 ·_ih 𝐴)) ∧ 0 ≤ (√‘(𝐵 ·_ih 𝐵))) → 0 ≤ ((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵))))
81	77, 79, 80	mp2an 704	. . . 4 ⊢ 0 ≤ ((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))
82	68	sqrtsqi 15414	. . . 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 5129	. 2 ⊢ (√‘((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵))) ≤ ((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))
85		normval 31381	. . 3 ⊢ ((𝐴 +_ℎ 𝐵) ∈ ℋ → (norm_ℎ‘(𝐴 +_ℎ 𝐵)) = (√‘((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵))))
86	65, 85	ax-mp 5	. 2 ⊢ (norm_ℎ‘(𝐴 +_ℎ 𝐵)) = (√‘((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)))
87		normval 31381	. . . 4 ⊢ (𝐴 ∈ ℋ → (norm_ℎ‘𝐴) = (√‘(𝐴 ·_ih 𝐴)))
88	7, 87	ax-mp 5	. . 3 ⊢ (norm_ℎ‘𝐴) = (√‘(𝐴 ·_ih 𝐴))
89		normval 31381	. . . 4 ⊢ (𝐵 ∈ ℋ → (norm_ℎ‘𝐵) = (√‘(𝐵 ·_ih 𝐵)))
90	6, 89	ax-mp 5	. . 3 ⊢ (norm_ℎ‘𝐵) = (√‘(𝐵 ·_ih 𝐵))
91	88, 90	oveq12i 7412	. 2 ⊢ ((norm_ℎ‘𝐴) + (norm_ℎ‘𝐵)) = ((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))
92	84, 86, 91	3brtr4i 5134	1 ⊢ (norm_ℎ‘(𝐴 +_ℎ 𝐵)) ≤ ((norm_ℎ‘𝐴) + (norm_ℎ‘𝐵))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 209 = wceq 1563 ∈ wcel 2145 class class class wbr 5104 ‘cfv 6525 (class class class)co 7400 ℝcr 11087 0cc0 11088 1c1 11089 + caddc 11091 · cmul 11093 ≤ cle 11232 -cneg 11430 2c2 12283 ↑cexp 14085 ∗ccj 15135 √csqrt 15272 ℋchba 31176 +_ℎ cva 31177 ·_ih csp 31179 norm_ℎcno 31180

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-sep 5250 ax-nul 5260 ax-pow 5326 ax-pr 5394 ax-un 7722 ax-cnex 11144 ax-resscn 11145 ax-1cn 11146 ax-icn 11147 ax-addcl 11148 ax-addrcl 11149 ax-mulcl 11150 ax-mulrcl 11151 ax-mulcom 11152 ax-addass 11153 ax-mulass 11154 ax-distr 11155 ax-i2m1 11156 ax-1ne0 11157 ax-1rid 11158 ax-rnegex 11159 ax-rrecex 11160 ax-cnre 11161 ax-pre-lttri 11162 ax-pre-lttrn 11163 ax-pre-ltadd 11164 ax-pre-mulgt0 11165 ax-pre-sup 11166 ax-hfvadd 31257 ax-hv0cl 31260 ax-hfvmul 31262 ax-hvmulass 31264 ax-hvmul0 31267 ax-hfi 31336 ax-his1 31339 ax-his2 31340 ax-his3 31341 ax-his4 31342

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3370 df-reu 3371 df-rab 3418 df-v 3459 df-sbc 3748 df-csb 3856 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-pss 3927 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-iun 4953 df-br 5105 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6291 df-ord 6352 df-on 6353 df-lim 6354 df-suc 6355 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-f1 6530 df-fo 6531 df-f1o 6532 df-fv 6533 df-riota 7357 df-ov 7403 df-oprab 7404 df-mpo 7405 df-om 7851 df-2nd 7975 df-frecs 8266 df-wrecs 8297 df-recs 8346 df-rdg 8385 df-er 8682 df-en 8932 df-dom 8933 df-sdom 8934 df-sup 9390 df-pnf 11233 df-mnf 11234 df-xr 11235 df-ltxr 11236 df-le 11237 df-sub 11431 df-neg 11432 df-div 11860 df-nn 12222 df-2 12291 df-3 12292 df-4 12293 df-n0 12493 df-z 12580 df-uz 12851 df-rp 13005 df-seq 14026 df-exp 14086 df-cj 15138 df-re 15139 df-im 15140 df-sqrt 15274 df-abs 15275 df-hnorm 31225 df-hvsub 31228

This theorem is referenced by: norm-ii 31395 norm3difi 31404

W3C validator