Theorem normpar2 5100

Description: Corollary of parallelogram law for norms. Part of Lemma 3.6 of [Beran] p. 100.

Hypotheses

Ref	Expression
normpar2.1	⊢ A ∈ ℋ
normpar2.2	⊢ B ∈ ℋ
normpar2.3	⊢ C ∈ ℋ

Assertion

Ref	Expression
normpar2	⊢ ((norm ‘(A −v B))↑2) = (((2 · ((norm ‘(A −v C))↑2)) + (2 · ((norm ‘(B −v C))↑2))) − ((norm ‘((A +v B) −v (2 ·s C)))↑2))

Proof of Theorem normpar2

Step	Hyp	Ref	Expression
1		4re 4473	. . . . . . 7 ⊢ 4 ∈ ℝ
2	1	recn 4098	. . . . . 6 ⊢ 4 ∈ ℂ
3		normpar2.1	. . . . . . . . . 10 ⊢ A ∈ ℋ
4		normpar2.3	. . . . . . . . . 10 ⊢ C ∈ ℋ
5	3, 4	hvsubcl 5002	. . . . . . . . 9 ⊢ (A −v C) ∈ ℋ
6	5	normcl 5081	. . . . . . . 8 ⊢ (norm ‘(A −v C)) ∈ ℝ
7	6	sqrecl 4699	. . . . . . 7 ⊢ ((norm ‘(A −v C))↑2) ∈ ℝ
8	7	recn 4098	. . . . . 6 ⊢ ((norm ‘(A −v C))↑2) ∈ ℂ
9	2, 8	mulcl 4105	. . . . 5 ⊢ (4 · ((norm ‘(A −v C))↑2)) ∈ ℂ
10		normpar2.2	. . . . . . . . . 10 ⊢ B ∈ ℋ
11	10, 4	hvsubcl 5002	. . . . . . . . 9 ⊢ (B −v C) ∈ ℋ
12	11	normcl 5081	. . . . . . . 8 ⊢ (norm ‘(B −v C)) ∈ ℝ
13	12	sqrecl 4699	. . . . . . 7 ⊢ ((norm ‘(B −v C))↑2) ∈ ℝ
14	13	recn 4098	. . . . . 6 ⊢ ((norm ‘(B −v C))↑2) ∈ ℂ
15	2, 14	mulcl 4105	. . . . 5 ⊢ (4 · ((norm ‘(B −v C))↑2)) ∈ ℂ
16		2cn 4471	. . . . 5 ⊢ 2 ∈ ℂ
17		2re 4470	. . . . . 6 ⊢ 2 ∈ ℝ
18		2pos 4479	. . . . . 6 ⊢ 0 < 2
19	17, 18	gt0ne0i 4345	. . . . 5 ⊢ 2 ≠ 0
20	9, 15, 16, 19	divdistr 4243	. . . 4 ⊢ (((4 · ((norm ‘(A −v C))↑2)) + (4 · ((norm ‘(B −v C))↑2))) / 2) = (((4 · ((norm ‘(A −v C))↑2)) / 2) + ((4 · ((norm ‘(B −v C))↑2)) / 2))
21	9, 15	addcom 4106	. . . . . . . 8 ⊢ ((4 · ((norm ‘(A −v C))↑2)) + (4 · ((norm ‘(B −v C))↑2))) = ((4 · ((norm ‘(B −v C))↑2)) + (4 · ((norm ‘(A −v C))↑2)))
22	3, 10	hvaddcl 4999	. . . . . . . . . . . . . . . . 17 ⊢ (A +v B) ∈ ℋ
23	16, 4	hvmulcl 4990	. . . . . . . . . . . . . . . . 17 ⊢ (2 ·s C) ∈ ℋ
24	22, 23	hvsubcl 5002	. . . . . . . . . . . . . . . 16 ⊢ ((A +v B) −v (2 ·s C)) ∈ ℋ
25	3, 10	hvsubcl 5002	. . . . . . . . . . . . . . . 16 ⊢ (A −v B) ∈ ℋ
26	24, 25	hvsubval 5001	. . . . . . . . . . . . . . 15 ⊢ (((A +v B) −v (2 ·s C)) −v (A −v B)) = (((A +v B) −v (2 ·s C)) +v (-1 ·s (A −v B)))
27	22, 23	hvsubval 5001	. . . . . . . . . . . . . . . 16 ⊢ ((A +v B) −v (2 ·s C)) = ((A +v B) +v (-1 ·s (2 ·s C)))
28	27	opreq1i 3009	. . . . . . . . . . . . . . 15 ⊢ (((A +v B) −v (2 ·s C)) +v (-1 ·s (A −v B))) = (((A +v B) +v (-1 ·s (2 ·s C))) +v (-1 ·s (A −v B)))
29	3, 10	hvcom 5000	. . . . . . . . . . . . . . . . . . 19 ⊢ (A +v B) = (B +v A)
30	3, 10	hvnegdi 5034	. . . . . . . . . . . . . . . . . . 19 ⊢ (-1 ·s (A −v B)) = (B −v A)
31	29, 30	opreq12i 3011	. . . . . . . . . . . . . . . . . 18 ⊢ ((A +v B) +v (-1 ·s (A −v B))) = ((B +v A) +v (B −v A))
32	10, 3	hvsubcan2 5036	. . . . . . . . . . . . . . . . . 18 ⊢ ((B +v A) +v (B −v A)) = (2 ·s B)
33	31, 32	eqtr 1119	. . . . . . . . . . . . . . . . 17 ⊢ ((A +v B) +v (-1 ·s (A −v B))) = (2 ·s B)
34	33	opreq1i 3009	. . . . . . . . . . . . . . . 16 ⊢ (((A +v B) +v (-1 ·s (A −v B))) +v (-1 ·s (2 ·s C))) = ((2 ·s B) +v (-1 ·s (2 ·s C)))
35		1cn 4101	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℂ
36	35	negcl 4142	. . . . . . . . . . . . . . . . . 18 ⊢ -1 ∈ ℂ
37	36, 23	hvmulcl 4990	. . . . . . . . . . . . . . . . 17 ⊢ (-1 ·s (2 ·s C)) ∈ ℋ
38	36, 25	hvmulcl 4990	. . . . . . . . . . . . . . . . 17 ⊢ (-1 ·s (A −v B)) ∈ ℋ
39	22, 37, 38	hvadd23 5026	. . . . . . . . . . . . . . . 16 ⊢ (((A +v B) +v (-1 ·s (2 ·s C))) +v (-1 ·s (A −v B))) = (((A +v B) +v (-1 ·s (A −v B))) +v (-1 ·s (2 ·s C)))
40	16, 10	hvmulcl 4990	. . . . . . . . . . . . . . . . 17 ⊢ (2 ·s B) ∈ ℋ
41	40, 23	hvsubval 5001	. . . . . . . . . . . . . . . 16 ⊢ ((2 ·s B) −v (2 ·s C)) = ((2 ·s B) +v (-1 ·s (2 ·s C)))
42	34, 39, 41	3eqtr4 1126	. . . . . . . . . . . . . . 15 ⊢ (((A +v B) +v (-1 ·s (2 ·s C))) +v (-1 ·s (A −v B))) = ((2 ·s B) −v (2 ·s C))
43	26, 28, 42	3eqtr 1123	. . . . . . . . . . . . . 14 ⊢ (((A +v B) −v (2 ·s C)) −v (A −v B)) = ((2 ·s B) −v (2 ·s C))
44	16, 10, 4	hvsubdistr1 5024	. . . . . . . . . . . . . 14 ⊢ (2 ·s (B −v C)) = ((2 ·s B) −v (2 ·s C))
45	43, 44	eqtr4 1122	. . . . . . . . . . . . 13 ⊢ (((A +v B) −v (2 ·s C)) −v (A −v B)) = (2 ·s (B −v C))
46	45	fveq2i 2835	. . . . . . . . . . . 12 ⊢ (norm ‘(((A +v B) −v (2 ·s C)) −v (A −v B))) = (norm ‘(2 ·s (B −v C)))
47	16, 11	norm-iii 5087	. . . . . . . . . . . 12 ⊢ (norm ‘(2 ·s (B −v C))) = ((abs ‘2) · (norm ‘(B −v C)))
48		ax0re 4063	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ ℝ
49	48, 17, 18	ltlei 4303	. . . . . . . . . . . . . 14 ⊢ 0 ≤ 2
50	17	absid 4850	. . . . . . . . . . . . . 14 ⊢ (0 ≤ 2 → (abs ‘2) = 2)
51	49, 50	ax-mp 6	. . . . . . . . . . . . 13 ⊢ (abs ‘2) = 2
52	51	opreq1i 3009	. . . . . . . . . . . 12 ⊢ ((abs ‘2) · (norm ‘(B −v C))) = (2 · (norm ‘(B −v C)))
53	46, 47, 52	3eqtr 1123	. . . . . . . . . . 11 ⊢ (norm ‘(((A +v B) −v (2 ·s C)) −v (A −v B))) = (2 · (norm ‘(B −v C)))
54	53	opreq1i 3009	. . . . . . . . . 10 ⊢ ((norm ‘(((A +v B) −v (2 ·s C)) −v (A −v B)))↑2) = ((2 · (norm ‘(B −v C)))↑2)
55	12	recn 4098	. . . . . . . . . . 11 ⊢ (norm ‘(B −v C)) ∈ ℂ
56	16, 55	sqmul 4688	. . . . . . . . . 10 ⊢ ((2 · (norm ‘(B −v C)))↑2) = ((2↑2) · ((norm ‘(B −v C))↑2))
57		sq2 4710	. . . . . . . . . . 11 ⊢ (2↑2) = 4
58	57	opreq1i 3009	. . . . . . . . . 10 ⊢ ((2↑2) · ((norm ‘(B −v C))↑2)) = (4 · ((norm ‘(B −v C))↑2))
59	54, 56, 58	3eqtr 1123	. . . . . . . . 9 ⊢ ((norm ‘(((A +v B) −v (2 ·s C)) −v (A −v B)))↑2) = (4 · ((norm ‘(B −v C))↑2))
60	27	opreq1i 3009	. . . . . . . . . . . . . . 15 ⊢ (((A +v B) −v (2 ·s C)) +v (A −v B)) = (((A +v B) +v (-1 ·s (2 ·s C))) +v (A −v B))
61	22, 37, 25	hvadd23 5026	. . . . . . . . . . . . . . 15 ⊢ (((A +v B) +v (-1 ·s (2 ·s C))) +v (A −v B)) = (((A +v B) +v (A −v B)) +v (-1 ·s (2 ·s C)))
62	3, 10	hvsubcan2 5036	. . . . . . . . . . . . . . . . 17 ⊢ ((A +v B) +v (A −v B)) = (2 ·s A)
63	62	opreq1i 3009	. . . . . . . . . . . . . . . 16 ⊢ (((A +v B) +v (A −v B)) +v (-1 ·s (2 ·s C))) = ((2 ·s A) +v (-1 ·s (2 ·s C)))
64	16, 3	hvmulcl 4990	. . . . . . . . . . . . . . . . 17 ⊢ (2 ·s A) ∈ ℋ
65	64, 23	hvsubval 5001	. . . . . . . . . . . . . . . 16 ⊢ ((2 ·s A) −v (2 ·s C)) = ((2 ·s A) +v (-1 ·s (2 ·s C)))
66	63, 65	eqtr4 1122	. . . . . . . . . . . . . . 15 ⊢ (((A +v B) +v (A −v B)) +v (-1 ·s (2 ·s C))) = ((2 ·s A) −v (2 ·s C))
67	60, 61, 66	3eqtr 1123	. . . . . . . . . . . . . 14 ⊢ (((A +v B) −v (2 ·s C)) +v (A −v B)) = ((2 ·s A) −v (2 ·s C))
68	16, 3, 4	hvsubdistr1 5024	. . . . . . . . . . . . . 14 ⊢ (2 ·s (A −v C)) = ((2 ·s A) −v (2 ·s C))
69	67, 68	eqtr4 1122	. . . . . . . . . . . . 13 ⊢ (((A +v B) −v (2 ·s C)) +v (A −v B)) = (2 ·s (A −v C))
70	69	fveq2i 2835	. . . . . . . . . . . 12 ⊢ (norm ‘(((A +v B) −v (2 ·s C)) +v (A −v B))) = (norm ‘(2 ·s (A −v C)))
71	16, 5	norm-iii 5087	. . . . . . . . . . . 12 ⊢ (norm ‘(2 ·s (A −v C))) = ((abs ‘2) · (norm ‘(A −v C)))
72	51	opreq1i 3009	. . . . . . . . . . . 12 ⊢ ((abs ‘2) · (norm ‘(A −v C))) = (2 · (norm ‘(A −v C)))
73	70, 71, 72	3eqtr 1123	. . . . . . . . . . 11 ⊢ (norm ‘(((A +v B) −v (2 ·s C)) +v (A −v B))) = (2 · (norm ‘(A −v C)))
74	73	opreq1i 3009	. . . . . . . . . 10 ⊢ ((norm ‘(((A +v B) −v (2 ·s C)) +v (A −v B)))↑2) = ((2 · (norm ‘(A −v C)))↑2)
75	6	recn 4098	. . . . . . . . . . 11 ⊢ (norm ‘(A −v C)) ∈ ℂ
76	16, 75	sqmul 4688	. . . . . . . . . 10 ⊢ ((2 · (norm ‘(A −v C)))↑2) = ((2↑2) · ((norm ‘(A −v C))↑2))
77	57	opreq1i 3009	. . . . . . . . . 10 ⊢ ((2↑2) · ((norm ‘(A −v C))↑2)) = (4 · ((norm ‘(A −v C))↑2))
78	74, 76, 77	3eqtr 1123	. . . . . . . . 9 ⊢ ((norm ‘(((A +v B) −v (2 ·s C)) +v (A −v B)))↑2) = (4 · ((norm ‘(A −v C))↑2))
79	59, 78	opreq12i 3011	. . . . . . . 8 ⊢ (((norm ‘(((A +v B) −v (2 ·s C)) −v (A −v B)))↑2) + ((norm ‘(((A +v B) −v (2 ·s C)) +v (A −v B)))↑2)) = ((4 · ((norm ‘(B −v C))↑2)) + (4 · ((norm ‘(A −v C))↑2)))
80	21, 79	eqtr4 1122	. . . . . . 7 ⊢ ((4 · ((norm ‘(A −v C))↑2)) + (4 · ((norm ‘(B −v C))↑2))) = (((norm ‘(((A +v B) −v (2 ·s C)) −v (A −v B)))↑2) + ((norm ‘(((A +v B) −v (2 ·s C)) +v (A −v B)))↑2))
81	24, 25	normpar 5099	. . . . . . 7 ⊢ (((norm ‘(((A +v B) −v (2 ·s C)) −v (A −v B)))↑2) + ((norm ‘(((A +v B) −v (2 ·s C)) +v (A −v B)))↑2)) = ((2 · ((norm ‘((A +v B) −v (2 ·s C)))↑2)) + (2 · ((norm ‘(A −v B))↑2)))
82	80, 81	eqtr 1119	. . . . . 6 ⊢ ((4 · ((norm ‘(A −v C))↑2)) + (4 · ((norm ‘(B −v C))↑2))) = ((2 · ((norm ‘((A +v B) −v (2 ·s C)))↑2)) + (2 · ((norm ‘(A −v B))↑2)))
83	82	opreq1i 3009	. . . . 5 ⊢ (((4 · ((norm ‘(A −v C))↑2)) + (4 · ((norm ‘(B −v C))↑2))) / 2) = (((2 · ((norm ‘((A +v B) −v (2 ·s C)))↑2)) + (2 · ((norm ‘(A −v B))↑2))) / 2)
84	24	normcl 5081	. . . . . . . . 9 ⊢ (norm ‘((A +v B) −v (2 ·s C))) ∈ ℝ
85	84	sqrecl 4699	. . . . . . . 8 ⊢ ((norm ‘((A +v B) −v (2 ·s C)))↑2) ∈ ℝ
86	85	recn 4098	. . . . . . 7 ⊢ ((norm ‘((A +v B) −v (2 ·s C)))↑2) ∈ ℂ
87	16, 86	mulcl 4105	. . . . . 6 ⊢ (2 · ((norm ‘((A +v B) −v (2 ·s C)))↑2)) ∈ ℂ
88	25	normcl 5081	. . . . . . . . 9 ⊢ (norm ‘(A −v B)) ∈ ℝ
89	88	sqrecl 4699	. . . . . . . 8 ⊢ ((norm ‘(A −v B))↑2) ∈ ℝ
90	89	recn 4098	. . . . . . 7 ⊢ ((norm ‘(A −v B))↑2) ∈ ℂ
91	16, 90	mulcl 4105	. . . . . 6 ⊢ (2 · ((norm ‘(A −v B))↑2)) ∈ ℂ
92	87, 91, 16, 19	divdistr 4243	. . . . 5 ⊢ (((2 · ((norm ‘((A +v B) −v (2 ·s C)))↑2)) + (2 · ((norm ‘(A −v B))↑2))) / 2) = (((2 · ((norm ‘((A +v B) −v (2 ·s C)))↑2)) / 2) + ((2 · ((norm ‘(A −v B))↑2)) / 2))
93	16, 86, 19	divcan3 4247	. . . . . 6 ⊢ ((2 · ((norm ‘((A +v B) −v (2 ·s C)))↑2)) / 2) = ((norm ‘((A +v B) −v (2 ·s C)))↑2)
94	16, 90, 19	divcan3 4247	. . . . . 6 ⊢ ((2 · ((norm ‘(A −v B))↑2)) / 2) = ((norm ‘(A −v B))↑2)
95	93, 94	opreq12i 3011	. . . . 5 ⊢ (((2 · ((norm ‘((A +v B) −v (2 ·s C)))↑2)) / 2) + ((2 · ((norm ‘(A −v B))↑2)) / 2)) = (((norm ‘((A +v B) −v (2 ·s C)))↑2) + ((norm ‘(A −v B))↑2))
96	83, 92, 95	3eqtr 1123	. . . 4 ⊢ (((4 · ((norm ‘(A −v C))↑2)) + (4 · ((norm ‘(B −v C))↑2))) / 2) = (((norm ‘((A +v B) −v (2 ·s C)))↑2) + ((norm ‘(A −v B))↑2))
97	2, 8, 16, 19	div23 4244	. . . . . 6 ⊢ ((4 · ((norm ‘(A −v C))↑2)) / 2) = ((4 / 2) · ((norm ‘(A −v C))↑2))
98		4d2e2 4507	. . . . . . 7 ⊢ (4 / 2) = 2
99	98	opreq1i 3009	. . . . . 6 ⊢ ((4 / 2) · ((norm ‘(A −v C))↑2)) = (2 · ((norm ‘(A −v C))↑2))
100	97, 99	eqtr 1119	. . . . 5 ⊢ ((4 · ((norm ‘(A −v C))↑2)) / 2) = (2 · ((norm ‘(A −v C))↑2))
101	2, 14, 16, 19	div23 4244	. . . . . 6 ⊢ ((4 · ((norm ‘(B −v C))↑2)) / 2) = ((4 / 2) · ((norm ‘(B −v C))↑2))
102	98	opreq1i 3009	. . . . . 6 ⊢ ((4 / 2) · ((norm ‘(B −v C))↑2)) = (2 · ((norm ‘(B −v C))↑2))
103	101, 102	eqtr 1119	. . . . 5 ⊢ ((4 · ((norm ‘(B −v C))↑2)) / 2) = (2 · ((norm ‘(B −v C))↑2))
104	100, 103	opreq12i 3011	. . . 4 ⊢ (((4 · ((norm ‘(A −v C))↑2)) / 2) + ((4 · ((norm ‘(B −v C))↑2)) / 2)) = ((2 · ((norm ‘(A −v C))↑2)) + (2 · ((norm ‘(B −v C))↑2)))
105	20, 96, 104	3eqtr3 1124	. . 3 ⊢ (((norm ‘((A +v B) −v (2 ·s C)))↑2) + ((norm ‘(A −v B))↑2)) = ((2 · ((norm ‘(A −v C))↑2)) + (2 · ((norm ‘(B −v C))↑2)))
106	17, 7	remulcl 4119	. . . . . 6 ⊢ (2 · ((norm ‘(A −v C))↑2)) ∈ ℝ
107	17, 13	remulcl 4119	. . . . . 6 ⊢ (2 · ((norm ‘(B −v C))↑2)) ∈ ℝ
108	106, 107	readdcl 4118	. . . . 5 ⊢ ((2 · ((norm ‘(A −v C))↑2)) + (2 · ((norm ‘(B −v C))↑2))) ∈ ℝ
109	108	recn 4098	. . . 4 ⊢ ((2 · ((norm ‘(A −v C))↑2)) + (2 · ((norm ‘(B −v C))↑2))) ∈ ℂ
110	109, 86, 90	subadd 4143	. . 3 ⊢ ((((2 · ((norm ‘(A −v C))↑2)) + (2 · ((norm ‘(B −v C))↑2))) − ((norm ‘((A +v B) −v (2 ·s C)))↑2)) = ((norm ‘(A −v B))↑2) ↔ (((norm ‘((A +v B) −v (2 ·s C)))↑2) + ((norm ‘(A −v B))↑2)) = ((2 · ((norm ‘(A −v C))↑2)) + (2 · ((norm ‘(B −v C))↑2))))
111	105, 110	mpbir 165	. 2 ⊢ (((2 · ((norm ‘(A −v C))↑2)) + (2 · ((norm ‘(B −v C))↑2))) − ((norm ‘((A +v B) −v (2 ·s C)))↑2)) = ((norm ‘(A −v B))↑2)
112	111	cleqcomi 1105	1 ⊢ ((norm ‘(A −v B))↑2) = (((2 · ((norm ‘(A −v C))↑2)) + (2 · ((norm ‘(B −v C))↑2))) − ((norm ‘((A +v B) −v (2 ·s C)))↑2))

Syntax hints:   = wceq 1091   ∈ wcel 1092   class class class wbr 2054   ‘cfv 2422  (class class class)co 3001  0cc0 4028  1c1 4029   + caddc 4031   · cmulc 4032   − cmin 4089  -cneg 4090   / cdiv 4091   ≤ cle 4092  2c2 4454  4c4 4456  ↑cexp 4675  abscabs 4789   ℋ chil 4958   +_v cva 4959   ·_s csm 4960   −_v cmv 4962  normcno 4964

This theorem is referenced by:  projlem5 5197

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077  ax-reg 1078  ax-inf 1079  ax-hvaddcl 4984  ax-hvcom 4985  ax-hvass 4986  ax-hvzercl 4987  ax-hvaddid 4988  ax-hvmulcl 4989  ax-hvmulid 4991  ax-hvmulass 4992  ax-hvdistr1 4993  ax-hvdistr2 4994  ax-hvmulzer 4995  ax-hicl 5043  ax-his1 5045  ax-his2 5046  ax-his3 5047  ax-his4 5048

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3or 582  df-3an 583  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ne 1192  df-ral 1205  df-rex 1206  df-reu 1207  df-rab 1208  df-v 1349  df-sbc 1441  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-pss 1494  df-nul 1708  df-if 1777  df-pw 1799  df-sn 1811  df-pr 1812  df-tp 1814  df-op 1815  df-uni 1920  df-int 1966  df-iun 1996  df-tr 2042  df-br 2063  df-opab 2098  df-eprel 2122  df-id 2125  df-po 2128  df-so 2138  df-sup 2154  df-fr 2169  df-we 2186  df-ord 2202  df-on 2203  df-lim 2204  df-suc 2205  df-om 2373  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-f 2434  df-f1 2435  df-fo 2436  df-f1o 2437  df-fv 2438  df-rdg 2970  df-opr 3003  df-oprab 3004  df-1st 3087  df-2nd 3088  df-1o 3104  df-oadd 3106  df-omul 3107  df-er 3200  df-ec 3202  df-qs 3205  df-ni 3794  df-pli 3795  df-mi 3796  df-lti 3797  df-plpq 3829  df-mpq 3830  df-enq 3831  df-nq 3832  df-plq 3833  df-mq 3834  df-rq 3835  df-ltq 3836  df-1q 3837  df-np 3880  df-1p 3881  df-plp 3882  df-mp 3883  df-ltp 3884  df-plpr 3958  df-mpr 3959  df-enr 3960  df-nr 3961  df-plr 3962  df-mr 3963  df-ltr 3964  df-0r 3965  df-1r 3966  df-m1r 3967  df-c 4034  df-0 4035  df-1 4036  df-i 4037  df-r 4038  df-plus 4039  df-mul 4040  df-lt 4041  df-sub 4133  df-neg 4135  df-div 4216  df-le 4277  df-n 4423  df-2 4462  df-3 4463  df-4 4464  df-n0 4535  df-z 4564  df-seq 4661  df-exp 4676  df-sqr 4728  df-re 4790  df-im 4791  df-cj 4792  df-abs 4793  df-hvsub 4996  df-hnorm 5074

metamath.org