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 28914

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 10641	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ
2		ax-1cn 10595	. . . . . . . . . . . 12 ⊢ 1 ∈ ℂ
3	2	cjrebi 14533	. . . . . . . . . . 11 ⊢ (1 ∈ ℝ ↔ (∗‘1) = 1)
4	1, 3	mpbi 232	. . . . . . . . . 10 ⊢ (∗‘1) = 1
5	4	oveq1i 7166	. . . . . . . . 9 ⊢ ((∗‘1) · (𝐵 ·_ih 𝐴)) = (1 · (𝐵 ·_ih 𝐴))
6		norm-ii.2	. . . . . . . . . . 11 ⊢ 𝐵 ∈ ℋ
7		norm-ii.1	. . . . . . . . . . 11 ⊢ 𝐴 ∈ ℋ
8	6, 7	hicli 28858	. . . . . . . . . 10 ⊢ (𝐵 ·_ih 𝐴) ∈ ℂ
9	8	mulid2i 10646	. . . . . . . . 9 ⊢ (1 · (𝐵 ·_ih 𝐴)) = (𝐵 ·_ih 𝐴)
10	5, 9	eqtri 2844	. . . . . . . 8 ⊢ ((∗‘1) · (𝐵 ·_ih 𝐴)) = (𝐵 ·_ih 𝐴)
11	7, 6	hicli 28858	. . . . . . . . 9 ⊢ (𝐴 ·_ih 𝐵) ∈ ℂ
12	11	mulid2i 10646	. . . . . . . 8 ⊢ (1 · (𝐴 ·_ih 𝐵)) = (𝐴 ·_ih 𝐵)
13	10, 12	oveq12i 7168	. . . . . . 7 ⊢ (((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵))) = ((𝐵 ·_ih 𝐴) + (𝐴 ·_ih 𝐵))
14		abs1 14657	. . . . . . . 8 ⊢ (abs‘1) = 1
15	2, 6, 7, 14	normlem7 28893	. . . . . . 7 ⊢ (((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵))) ≤ (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵))))
16	13, 15	eqbrtrri 5089	. . . . . 6 ⊢ ((𝐵 ·_ih 𝐴) + (𝐴 ·_ih 𝐵)) ≤ (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵))))
17		eqid 2821	. . . . . . . . . 10 ⊢ -(((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵))) = -(((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵)))
18	2, 6, 7, 17	normlem2 28888	. . . . . . . . 9 ⊢ -(((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵))) ∈ ℝ
19	2	cjcli 14528	. . . . . . . . . . . 12 ⊢ (∗‘1) ∈ ℂ
20	19, 8	mulcli 10648	. . . . . . . . . . 11 ⊢ ((∗‘1) · (𝐵 ·_ih 𝐴)) ∈ ℂ
21	2, 11	mulcli 10648	. . . . . . . . . . 11 ⊢ (1 · (𝐴 ·_ih 𝐵)) ∈ ℂ
22	20, 21	addcli 10647	. . . . . . . . . 10 ⊢ (((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵))) ∈ ℂ
23	22	negrebi 10960	. . . . . . . . 9 ⊢ (-(((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵))) ∈ ℝ ↔ (((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵))) ∈ ℝ)
24	18, 23	mpbi 232	. . . . . . . 8 ⊢ (((∗‘1) · (𝐵 ·_ih 𝐴)) + (1 · (𝐴 ·_ih 𝐵))) ∈ ℝ
25	13, 24	eqeltrri 2910	. . . . . . 7 ⊢ ((𝐵 ·_ih 𝐴) + (𝐴 ·_ih 𝐵)) ∈ ℝ
26		2re 11712	. . . . . . . 8 ⊢ 2 ∈ ℝ
27		hiidge0 28875	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℋ → 0 ≤ (𝐴 ·_ih 𝐴))
28	7, 27	ax-mp 5	. . . . . . . . . 10 ⊢ 0 ≤ (𝐴 ·_ih 𝐴)
29		hiidrcl 28872	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℋ → (𝐴 ·_ih 𝐴) ∈ ℝ)
30	7, 29	ax-mp 5	. . . . . . . . . . 11 ⊢ (𝐴 ·_ih 𝐴) ∈ ℝ
31	30	sqrtcli 14731	. . . . . . . . . 10 ⊢ (0 ≤ (𝐴 ·_ih 𝐴) → (√‘(𝐴 ·_ih 𝐴)) ∈ ℝ)
32	28, 31	ax-mp 5	. . . . . . . . 9 ⊢ (√‘(𝐴 ·_ih 𝐴)) ∈ ℝ
33		hiidge0 28875	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ℋ → 0 ≤ (𝐵 ·_ih 𝐵))
34	6, 33	ax-mp 5	. . . . . . . . . 10 ⊢ 0 ≤ (𝐵 ·_ih 𝐵)
35		hiidrcl 28872	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ℋ → (𝐵 ·_ih 𝐵) ∈ ℝ)
36	6, 35	ax-mp 5	. . . . . . . . . . 11 ⊢ (𝐵 ·_ih 𝐵) ∈ ℝ
37	36	sqrtcli 14731	. . . . . . . . . 10 ⊢ (0 ≤ (𝐵 ·_ih 𝐵) → (√‘(𝐵 ·_ih 𝐵)) ∈ ℝ)
38	34, 37	ax-mp 5	. . . . . . . . 9 ⊢ (√‘(𝐵 ·_ih 𝐵)) ∈ ℝ
39	32, 38	remulcli 10657	. . . . . . . 8 ⊢ ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵))) ∈ ℝ
40	26, 39	remulcli 10657	. . . . . . 7 ⊢ (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵)))) ∈ ℝ
41	30, 36	readdcli 10656	. . . . . . 7 ⊢ ((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) ∈ ℝ
42	25, 40, 41	leadd2i 11196	. . . . . 6 ⊢ (((𝐵 ·_ih 𝐴) + (𝐴 ·_ih 𝐵)) ≤ (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵)))) ↔ (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + ((𝐵 ·_ih 𝐴) + (𝐴 ·_ih 𝐵))) ≤ (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵))))))
43	16, 42	mpbi 232	. . . . 5 ⊢ (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + ((𝐵 ·_ih 𝐴) + (𝐴 ·_ih 𝐵))) ≤ (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵)))))
44	7, 6, 7, 6	normlem8 28894	. . . . . 6 ⊢ ((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)) = (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + ((𝐴 ·_ih 𝐵) + (𝐵 ·_ih 𝐴)))
45	11, 8	addcomi 10831	. . . . . . 7 ⊢ ((𝐴 ·_ih 𝐵) + (𝐵 ·_ih 𝐴)) = ((𝐵 ·_ih 𝐴) + (𝐴 ·_ih 𝐵))
46	45	oveq2i 7167	. . . . . 6 ⊢ (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + ((𝐴 ·_ih 𝐵) + (𝐵 ·_ih 𝐴))) = (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + ((𝐵 ·_ih 𝐴) + (𝐴 ·_ih 𝐵)))
47	44, 46	eqtri 2844	. . . . 5 ⊢ ((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)) = (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + ((𝐵 ·_ih 𝐴) + (𝐴 ·_ih 𝐵)))
48	32	recni 10655	. . . . . . 7 ⊢ (√‘(𝐴 ·_ih 𝐴)) ∈ ℂ
49	38	recni 10655	. . . . . . 7 ⊢ (√‘(𝐵 ·_ih 𝐵)) ∈ ℂ
50	48, 49	binom2i 13575	. . . . . 6 ⊢ (((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2) = ((((√‘(𝐴 ·_ih 𝐴))↑2) + (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵))))) + ((√‘(𝐵 ·_ih 𝐵))↑2))
51	48	sqcli 13545	. . . . . . 7 ⊢ ((√‘(𝐴 ·_ih 𝐴))↑2) ∈ ℂ
52		2cn 11713	. . . . . . . 8 ⊢ 2 ∈ ℂ
53	48, 49	mulcli 10648	. . . . . . . 8 ⊢ ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵))) ∈ ℂ
54	52, 53	mulcli 10648	. . . . . . 7 ⊢ (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵)))) ∈ ℂ
55	49	sqcli 13545	. . . . . . 7 ⊢ ((√‘(𝐵 ·_ih 𝐵))↑2) ∈ ℂ
56	51, 54, 55	add32i 10863	. . . . . 6 ⊢ ((((√‘(𝐴 ·_ih 𝐴))↑2) + (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵))))) + ((√‘(𝐵 ·_ih 𝐵))↑2)) = ((((√‘(𝐴 ·_ih 𝐴))↑2) + ((√‘(𝐵 ·_ih 𝐵))↑2)) + (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵)))))
57	30	sqsqrti 14735	. . . . . . . . 9 ⊢ (0 ≤ (𝐴 ·_ih 𝐴) → ((√‘(𝐴 ·_ih 𝐴))↑2) = (𝐴 ·_ih 𝐴))
58	28, 57	ax-mp 5	. . . . . . . 8 ⊢ ((√‘(𝐴 ·_ih 𝐴))↑2) = (𝐴 ·_ih 𝐴)
59	36	sqsqrti 14735	. . . . . . . . 9 ⊢ (0 ≤ (𝐵 ·_ih 𝐵) → ((√‘(𝐵 ·_ih 𝐵))↑2) = (𝐵 ·_ih 𝐵))
60	34, 59	ax-mp 5	. . . . . . . 8 ⊢ ((√‘(𝐵 ·_ih 𝐵))↑2) = (𝐵 ·_ih 𝐵)
61	58, 60	oveq12i 7168	. . . . . . 7 ⊢ (((√‘(𝐴 ·_ih 𝐴))↑2) + ((√‘(𝐵 ·_ih 𝐵))↑2)) = ((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵))
62	61	oveq1i 7166	. . . . . 6 ⊢ ((((√‘(𝐴 ·_ih 𝐴))↑2) + ((√‘(𝐵 ·_ih 𝐵))↑2)) + (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵))))) = (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵)))))
63	50, 56, 62	3eqtri 2848	. . . . 5 ⊢ (((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2) = (((𝐴 ·_ih 𝐴) + (𝐵 ·_ih 𝐵)) + (2 · ((√‘(𝐴 ·_ih 𝐴)) · (√‘(𝐵 ·_ih 𝐵)))))
64	43, 47, 63	3brtr4i 5096	. . . 4 ⊢ ((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)) ≤ (((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2)
65	7, 6	hvaddcli 28795	. . . . . 6 ⊢ (𝐴 +_ℎ 𝐵) ∈ ℋ
66		hiidge0 28875	. . . . . 6 ⊢ ((𝐴 +_ℎ 𝐵) ∈ ℋ → 0 ≤ ((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)))
67	65, 66	ax-mp 5	. . . . 5 ⊢ 0 ≤ ((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵))
68	32, 38	readdcli 10656	. . . . . 6 ⊢ ((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵))) ∈ ℝ
69	68	sqge0i 13552	. . . . 5 ⊢ 0 ≤ (((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2)
70		hiidrcl 28872	. . . . . . 7 ⊢ ((𝐴 +_ℎ 𝐵) ∈ ℋ → ((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)) ∈ ℝ)
71	65, 70	ax-mp 5	. . . . . 6 ⊢ ((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)) ∈ ℝ
72	68	resqcli 13550	. . . . . 6 ⊢ (((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2) ∈ ℝ
73	71, 72	sqrtlei 14748	. . . . 5 ⊢ ((0 ≤ ((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)) ∧ 0 ≤ (((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2)) → (((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)) ≤ (((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2) ↔ (√‘((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵))) ≤ (√‘(((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2))))
74	67, 69, 73	mp2an 690	. . . 4 ⊢ (((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)) ≤ (((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2) ↔ (√‘((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵))) ≤ (√‘(((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2)))
75	64, 74	mpbi 232	. . 3 ⊢ (√‘((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵))) ≤ (√‘(((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))↑2))
76	30	sqrtge0i 14736	. . . . . 6 ⊢ (0 ≤ (𝐴 ·_ih 𝐴) → 0 ≤ (√‘(𝐴 ·_ih 𝐴)))
77	28, 76	ax-mp 5	. . . . 5 ⊢ 0 ≤ (√‘(𝐴 ·_ih 𝐴))
78	36	sqrtge0i 14736	. . . . . 6 ⊢ (0 ≤ (𝐵 ·_ih 𝐵) → 0 ≤ (√‘(𝐵 ·_ih 𝐵)))
79	34, 78	ax-mp 5	. . . . 5 ⊢ 0 ≤ (√‘(𝐵 ·_ih 𝐵))
80	32, 38	addge0i 11180	. . . . 5 ⊢ ((0 ≤ (√‘(𝐴 ·_ih 𝐴)) ∧ 0 ≤ (√‘(𝐵 ·_ih 𝐵))) → 0 ≤ ((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵))))
81	77, 79, 80	mp2an 690	. . . 4 ⊢ 0 ≤ ((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))
82	68	sqrtsqi 14734	. . . 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 5091	. 2 ⊢ (√‘((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵))) ≤ ((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))
85		normval 28901	. . 3 ⊢ ((𝐴 +_ℎ 𝐵) ∈ ℋ → (norm_ℎ‘(𝐴 +_ℎ 𝐵)) = (√‘((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵))))
86	65, 85	ax-mp 5	. 2 ⊢ (norm_ℎ‘(𝐴 +_ℎ 𝐵)) = (√‘((𝐴 +_ℎ 𝐵) ·_ih (𝐴 +_ℎ 𝐵)))
87		normval 28901	. . . 4 ⊢ (𝐴 ∈ ℋ → (norm_ℎ‘𝐴) = (√‘(𝐴 ·_ih 𝐴)))
88	7, 87	ax-mp 5	. . 3 ⊢ (norm_ℎ‘𝐴) = (√‘(𝐴 ·_ih 𝐴))
89		normval 28901	. . . 4 ⊢ (𝐵 ∈ ℋ → (norm_ℎ‘𝐵) = (√‘(𝐵 ·_ih 𝐵)))
90	6, 89	ax-mp 5	. . 3 ⊢ (norm_ℎ‘𝐵) = (√‘(𝐵 ·_ih 𝐵))
91	88, 90	oveq12i 7168	. 2 ⊢ ((norm_ℎ‘𝐴) + (norm_ℎ‘𝐵)) = ((√‘(𝐴 ·_ih 𝐴)) + (√‘(𝐵 ·_ih 𝐵)))
92	84, 86, 91	3brtr4i 5096	1 ⊢ (norm_ℎ‘(𝐴 +_ℎ 𝐵)) ≤ ((norm_ℎ‘𝐴) + (norm_ℎ‘𝐵))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 208 = wceq 1537 ∈ wcel 2114 class class class wbr 5066 ‘cfv 6355 (class class class)co 7156 ℝcr 10536 0cc0 10537 1c1 10538 + caddc 10540 · cmul 10542 ≤ cle 10676 -cneg 10871 2c2 11693 ↑cexp 13430 ∗ccj 14455 √csqrt 14592 ℋchba 28696 +_ℎ cva 28697 ·_ih csp 28699 norm_ℎcno 28700

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-sep 5203 ax-nul 5210 ax-pow 5266 ax-pr 5330 ax-un 7461 ax-cnex 10593 ax-resscn 10594 ax-1cn 10595 ax-icn 10596 ax-addcl 10597 ax-addrcl 10598 ax-mulcl 10599 ax-mulrcl 10600 ax-mulcom 10601 ax-addass 10602 ax-mulass 10603 ax-distr 10604 ax-i2m1 10605 ax-1ne0 10606 ax-1rid 10607 ax-rnegex 10608 ax-rrecex 10609 ax-cnre 10610 ax-pre-lttri 10611 ax-pre-lttrn 10612 ax-pre-ltadd 10613 ax-pre-mulgt0 10614 ax-pre-sup 10615 ax-hfvadd 28777 ax-hv0cl 28780 ax-hfvmul 28782 ax-hvmulass 28784 ax-hvmul0 28787 ax-hfi 28856 ax-his1 28859 ax-his2 28860 ax-his3 28861 ax-his4 28862

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3496 df-sbc 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-pss 3954 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4839 df-iun 4921 df-br 5067 df-opab 5129 df-mpt 5147 df-tr 5173 df-id 5460 df-eprel 5465 df-po 5474 df-so 5475 df-fr 5514 df-we 5516 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-rn 5566 df-res 5567 df-ima 5568 df-pred 6148 df-ord 6194 df-on 6195 df-lim 6196 df-suc 6197 df-iota 6314 df-fun 6357 df-fn 6358 df-f 6359 df-f1 6360 df-fo 6361 df-f1o 6362 df-fv 6363 df-riota 7114 df-ov 7159 df-oprab 7160 df-mpo 7161 df-om 7581 df-2nd 7690 df-wrecs 7947 df-recs 8008 df-rdg 8046 df-er 8289 df-en 8510 df-dom 8511 df-sdom 8512 df-sup 8906 df-pnf 10677 df-mnf 10678 df-xr 10679 df-ltxr 10680 df-le 10681 df-sub 10872 df-neg 10873 df-div 11298 df-nn 11639 df-2 11701 df-3 11702 df-4 11703 df-n0 11899 df-z 11983 df-uz 12245 df-rp 12391 df-seq 13371 df-exp 13431 df-cj 14458 df-re 14459 df-im 14460 df-sqrt 14594 df-abs 14595 df-hnorm 28745 df-hvsub 28748

This theorem is referenced by: norm-ii 28915 norm3difi 28924

W3C validator