bdtrilem - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > bdtrilem		Unicode version

Theorem bdtrilem 11238

Description: Lemma for bdtri 11239. (Contributed by Steven Nguyen and Jim Kingdon, 17-May-2023.)

**Assertion**
Ref	Expression
bdtrilem	$/\$ $/\$ $/\$ $/\$

**Proof of Theorem bdtrilem**
Step	Hyp	Ref	Expression
1		simp1l 1021	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
2		simp3 999	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
3	2	rpred 9690	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
4	1, 3	resubcld 8332	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
5	4	resqcld 10672	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
6		2re 8983	. . . . . . . . . . . 12
7	6	a1i 9	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
8	1	recnd 7980	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
9	2	rpcnd 9692	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
10	8, 9	subcld 8262	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
11	10	abscld 11181	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
12		simp2l 1023	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
13	12	recnd 7980	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
14	13, 9	subcld 8262	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
15	14	abscld 11181	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
16	11, 15	remulcld 7982	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
17	7, 16	remulcld 7982	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
18	5, 17	readdcld 7981	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
19	1, 12	remulcld 7982	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
20	7, 19	remulcld 7982	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
21	8, 13	addcld 7971	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
22	21, 9	subcld 8262	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
23	22	abscld 11181	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
24	3, 23	remulcld 7982	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
25	7, 24	remulcld 7982	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
26	20, 25	readdcld 7981	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
27	5, 26	readdcld 7981	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
28	12, 3	resubcld 8332	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
29	28	resqcld 10672	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
30	19, 24	readdcld 7981	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
31		0le2 9003	. . . . . . . . . . . . 13
32	31	a1i 9	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
33	8, 9, 13, 9	mulsubd 8368	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
34	19	recnd 7980	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
35	9, 9	mulcld 7972	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
36	8, 9	mulcld 7972	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
37	13, 9	mulcld 7972	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
38	36, 37	addcld 7971	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
39	34, 35, 38	addsubassd 8282	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
40	33, 39	eqtrd 2210	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
41	40	fveq2d 5516	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
42	35, 38	subcld 8262	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
43	34, 42	abstrid 11196	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
44	41, 43	eqbrtrd 4023	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
45		simp1r 1022	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
46		simp2r 1024	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
47	1, 12, 45, 46	mulge0d 8572	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
48	19, 47	absidd 11167	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
49	9, 21	subcld 8262	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
50	49, 9	absmuld 11194	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
51	9, 21, 9	subdird 8366	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
52	8, 13, 9	adddird 7977	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
53	52	oveq2d 5886	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
54	51, 53	eqtrd 2210	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
55	54	fveq2d 5516	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
56	9, 21	abssubd 11193	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
57	2	rpge0d 9694	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
58	3, 57	absidd 11167	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
59	56, 58	oveq12d 5888	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
60	50, 55, 59	3eqtr3d 2218	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
61	48, 60	oveq12d 5888	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
62	44, 61	breqtrd 4027	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
63	10, 14	absmuld 11194	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
64	23	recnd 7980	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
65	64, 9	mulcomd 7973	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
66	65	oveq2d 5886	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
67	62, 63, 66	3brtr3d 4032	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
68	16, 30, 7, 32, 67	lemul2ad 8891	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
69	7	recnd 7980	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
70	9, 64	mulcld 7972	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
71	69, 34, 70	adddid 7976	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
72	68, 71	breqtrd 4027	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
73	17, 26, 5, 72	leadd2dd 8511	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
74	18, 27, 29, 73	leadd1dd 8510	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
75	5	recnd 7980	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
76	26	recnd 7980	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
77	29	recnd 7980	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
78	75, 76, 77	add32d 8119	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
79	74, 78	breqtrd 4027	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
80	75, 77	addcld 7971	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
81	69, 34	mulcld 7972	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
82	69, 70	mulcld 7972	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
83	80, 81, 82	addassd 7974	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
84	79, 83	breqtrrd 4029	. . . . . 6 $/\$ $/\$ $/\$ $/\$
85	8	sqcld 10644	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
86	69, 36	mulcld 7972	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
87	85, 86	subcld 8262	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
88	9	sqcld 10644	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
89	87, 88	addcld 7971	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
90	89, 81	addcld 7971	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
91	13	sqcld 10644	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
92	69, 37	mulcld 7972	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
93	91, 92	subcld 8262	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
94	90, 93	addcld 7971	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
95	93, 88	addcld 7971	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
96	89, 95, 81	add32d 8119	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
97	90, 93, 88	addassd 7974	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
98	96, 97	eqtr4d 2213	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
99	94, 88, 98	comraddd 8108	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
100	81, 93	addcld 7971	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
101	87, 100	addcld 7971	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
102	89, 81, 93	addassd 7974	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
103	87, 88	addcomd 8102	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
104	103	oveq1d 5885	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
105	102, 104	eqtrd 2210	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
106	88, 87, 100	addassd 7974	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
107	105, 106	eqtrd 2210	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
108	88, 101, 107	comraddd 8108	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
109	85, 86, 93	subadd23d 8284	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
110	91, 92, 86	subsub4d 8293	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
111	92, 86	addcomd 8102	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
112	111	oveq2d 5886	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
113	110, 112	eqtrd 2210	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
114	113	oveq2d 5886	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
115	109, 114	eqtrd 2210	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
116	115	oveq2d 5886	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
117	87, 81, 93	add12d 8118	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
118	86, 92	addcld 7971	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
119	91, 118	subcld 8262	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
120	85, 119	addcld 7971	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
121	85, 81	addcld 7971	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
122	121, 91, 118	addsubassd 8282	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
123	85, 81, 119	add32d 8119	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
124	122, 123	eqtrd 2210	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
125	120, 81, 124	comraddd 8108	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
126	116, 117, 125	3eqtr4d 2220	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
127	126	oveq1d 5885	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
128	108, 127	eqtrd 2210	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
129	128	oveq2d 5886	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
130	99, 129	eqtrd 2210	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
131		binom2sub 10626	. . . . . . . . . . 11 $/\$
132	8, 9, 131	syl2anc 411	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
133		binom2sub 10626	. . . . . . . . . . 11 $/\$
134	13, 9, 133	syl2anc 411	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
135	132, 134	oveq12d 5888	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
136	135	oveq1d 5885	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
137		binom2sub 10626	. . . . . . . . . . 11 $/\$
138	21, 9, 137	syl2anc 411	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
139		binom2 10624	. . . . . . . . . . . . 13 $/\$
140	8, 13, 139	syl2anc 411	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
141	52	oveq2d 5886	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
142	69, 36, 37	adddid 7976	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
143	141, 142	eqtrd 2210	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
144	140, 143	oveq12d 5888	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
145	144	oveq1d 5885	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
146	138, 145	eqtrd 2210	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
147	146	oveq2d 5886	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
148	130, 136, 147	3eqtr4d 2220	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
149	148	oveq1d 5885	. . . . . 6 $/\$ $/\$ $/\$ $/\$
150	84, 149	breqtrd 4027	. . . . 5 $/\$ $/\$ $/\$ $/\$
151	22	sqcld 10644	. . . . . 6 $/\$ $/\$ $/\$ $/\$
152	88, 151, 82	add32d 8119	. . . . 5 $/\$ $/\$ $/\$ $/\$
153	150, 152	breqtrd 4027	. . . 4 $/\$ $/\$ $/\$ $/\$
154		absresq 11078	. . . . . . 7
155	4, 154	syl 14	. . . . . 6 $/\$ $/\$ $/\$ $/\$
156	155	oveq1d 5885	. . . . 5 $/\$ $/\$ $/\$ $/\$
157		absresq 11078	. . . . . 6
158	28, 157	syl 14	. . . . 5 $/\$ $/\$ $/\$ $/\$
159	156, 158	oveq12d 5888	. . . 4 $/\$ $/\$ $/\$ $/\$
160	1, 12	readdcld 7981	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
161	160, 3	resubcld 8332	. . . . . 6 $/\$ $/\$ $/\$ $/\$
162		absresq 11078	. . . . . 6
163	161, 162	syl 14	. . . . 5 $/\$ $/\$ $/\$ $/\$
164	163	oveq2d 5886	. . . 4 $/\$ $/\$ $/\$ $/\$
165	153, 159, 164	3brtr4d 4033	. . 3 $/\$ $/\$ $/\$ $/\$
166	11	recnd 7980	. . . 4 $/\$ $/\$ $/\$ $/\$
167	15	recnd 7980	. . . 4 $/\$ $/\$ $/\$ $/\$
168		binom2 10624	. . . 4 $/\$
169	166, 167, 168	syl2anc 411	. . 3 $/\$ $/\$ $/\$ $/\$
170		binom2 10624	. . . 4 $/\$
171	9, 64, 170	syl2anc 411	. . 3 $/\$ $/\$ $/\$ $/\$
172	165, 169, 171	3brtr4d 4033	. 2 $/\$ $/\$ $/\$ $/\$
173	11, 15	readdcld 7981	. . 3 $/\$ $/\$ $/\$ $/\$
174	3, 23	readdcld 7981	. . 3 $/\$ $/\$ $/\$ $/\$
175	10	absge0d 11184	. . . 4 $/\$ $/\$ $/\$ $/\$
176	14	absge0d 11184	. . . 4 $/\$ $/\$ $/\$ $/\$
177	11, 15, 175, 176	addge0d 8473	. . 3 $/\$ $/\$ $/\$ $/\$
178	22	absge0d 11184	. . . 4 $/\$ $/\$ $/\$ $/\$
179	3, 23, 57, 178	addge0d 8473	. . 3 $/\$ $/\$ $/\$ $/\$
180	173, 174, 177, 179	le2sqd 10678	. 2 $/\$ $/\$ $/\$ $/\$
181	172, 180	mpbird 167	1 $/\$ $/\$ $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104 $/\$ w3a 978

wceq 1353

wcel 2148 class class class wbr 4001

cfv 5213 (class class class)co 5870

cc 7804

cr 7805

cc0 7806

caddc 7809

cmul 7811

cle 7987

cmin 8122

c2 8964

crp 9647

cexp 10512

cabs 10997

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 614 ax-in2 615 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-13 2150 ax-14 2151 ax-ext 2159 ax-coll 4116 ax-sep 4119 ax-nul 4127 ax-pow 4172 ax-pr 4207 ax-un 4431 ax-setind 4534 ax-iinf 4585 ax-cnex 7897 ax-resscn 7898 ax-1cn 7899 ax-1re 7900 ax-icn 7901 ax-addcl 7902 ax-addrcl 7903 ax-mulcl 7904 ax-mulrcl 7905 ax-addcom 7906 ax-mulcom 7907 ax-addass 7908 ax-mulass 7909 ax-distr 7910 ax-i2m1 7911 ax-0lt1 7912 ax-1rid 7913 ax-0id 7914 ax-rnegex 7915 ax-precex 7916 ax-cnre 7917 ax-pre-ltirr 7918 ax-pre-ltwlin 7919 ax-pre-lttrn 7920 ax-pre-apti 7921 ax-pre-ltadd 7922 ax-pre-mulgt0 7923 ax-pre-mulext 7924 ax-arch 7925 ax-caucvg 7926

This theorem depends on definitions: df-bi 117 df-dc 835 df-3or 979 df-3an 980 df-tru 1356 df-fal 1359 df-nf 1461 df-sb 1763 df-eu 2029 df-mo 2030 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ne 2348 df-nel 2443 df-ral 2460 df-rex 2461 df-reu 2462 df-rmo 2463 df-rab 2464 df-v 2739 df-sbc 2963 df-csb 3058 df-dif 3131 df-un 3133 df-in 3135 df-ss 3142 df-nul 3423 df-if 3535 df-pw 3577 df-sn 3598 df-pr 3599 df-op 3601 df-uni 3809 df-int 3844 df-iun 3887 df-br 4002 df-opab 4063 df-mpt 4064 df-tr 4100 df-id 4291 df-po 4294 df-iso 4295 df-iord 4364 df-on 4366 df-ilim 4367 df-suc 4369 df-iom 4588 df-xp 4630 df-rel 4631 df-cnv 4632 df-co 4633 df-dm 4634 df-rn 4635 df-res 4636 df-ima 4637 df-iota 5175 df-fun 5215 df-fn 5216 df-f 5217 df-f1 5218 df-fo 5219 df-f1o 5220 df-fv 5221 df-riota 5826 df-ov 5873 df-oprab 5874 df-mpo 5875 df-1st 6136 df-2nd 6137 df-recs 6301 df-frec 6387 df-pnf 7988 df-mnf 7989 df-xr 7990 df-ltxr 7991 df-le 7992 df-sub 8124 df-neg 8125 df-reap 8526 df-ap 8533 df-div 8624 df-inn 8914 df-2 8972 df-3 8973 df-4 8974 df-n0 9171 df-z 9248 df-uz 9523 df-rp 9648 df-seqfrec 10439 df-exp 10513 df-cj 10842 df-re 10843 df-im 10844 df-rsqrt 10998 df-abs 10999

This theorem is referenced by: bdtri 11239

W3C validator