bdtrilem - Intuitionistic Logic Explorer

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

Theorem bdtrilem 11246

Description: Lemma for bdtri 11247. (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 9695	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
4	1, 3	resubcld 8337	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
5	4	resqcld 10679	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
6		2re 8988	. . . . . . . . . . . 12
7	6	a1i 9	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
8	1	recnd 7985	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
9	2	rpcnd 9697	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
10	8, 9	subcld 8267	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
11	10	abscld 11189	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
12		simp2l 1023	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
13	12	recnd 7985	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
14	13, 9	subcld 8267	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
15	14	abscld 11189	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
16	11, 15	remulcld 7987	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
17	7, 16	remulcld 7987	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
18	5, 17	readdcld 7986	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
19	1, 12	remulcld 7987	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
20	7, 19	remulcld 7987	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
21	8, 13	addcld 7976	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
22	21, 9	subcld 8267	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
23	22	abscld 11189	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
24	3, 23	remulcld 7987	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
25	7, 24	remulcld 7987	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
26	20, 25	readdcld 7986	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
27	5, 26	readdcld 7986	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
28	12, 3	resubcld 8337	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
29	28	resqcld 10679	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
30	19, 24	readdcld 7986	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
31		0le2 9008	. . . . . . . . . . . . 13
32	31	a1i 9	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
33	8, 9, 13, 9	mulsubd 8373	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
34	19	recnd 7985	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
35	9, 9	mulcld 7977	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
36	8, 9	mulcld 7977	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
37	13, 9	mulcld 7977	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
38	36, 37	addcld 7976	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
39	34, 35, 38	addsubassd 8287	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
40	33, 39	eqtrd 2210	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
41	40	fveq2d 5519	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
42	35, 38	subcld 8267	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
43	34, 42	abstrid 11204	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
44	41, 43	eqbrtrd 4025	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
45		simp1r 1022	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
46		simp2r 1024	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
47	1, 12, 45, 46	mulge0d 8577	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
48	19, 47	absidd 11175	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
49	9, 21	subcld 8267	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
50	49, 9	absmuld 11202	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
51	9, 21, 9	subdird 8371	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
52	8, 13, 9	adddird 7982	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
53	52	oveq2d 5890	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
54	51, 53	eqtrd 2210	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
55	54	fveq2d 5519	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
56	9, 21	abssubd 11201	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
57	2	rpge0d 9699	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
58	3, 57	absidd 11175	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
59	56, 58	oveq12d 5892	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
60	50, 55, 59	3eqtr3d 2218	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
61	48, 60	oveq12d 5892	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
62	44, 61	breqtrd 4029	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
63	10, 14	absmuld 11202	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
64	23	recnd 7985	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
65	64, 9	mulcomd 7978	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
66	65	oveq2d 5890	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
67	62, 63, 66	3brtr3d 4034	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
68	16, 30, 7, 32, 67	lemul2ad 8896	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
69	7	recnd 7985	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
70	9, 64	mulcld 7977	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
71	69, 34, 70	adddid 7981	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
72	68, 71	breqtrd 4029	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
73	17, 26, 5, 72	leadd2dd 8516	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
74	18, 27, 29, 73	leadd1dd 8515	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
75	5	recnd 7985	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
76	26	recnd 7985	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
77	29	recnd 7985	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
78	75, 76, 77	add32d 8124	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
79	74, 78	breqtrd 4029	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
80	75, 77	addcld 7976	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
81	69, 34	mulcld 7977	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
82	69, 70	mulcld 7977	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
83	80, 81, 82	addassd 7979	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
84	79, 83	breqtrrd 4031	. . . . . 6 $/\$ $/\$ $/\$ $/\$
85	8	sqcld 10651	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
86	69, 36	mulcld 7977	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
87	85, 86	subcld 8267	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
88	9	sqcld 10651	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
89	87, 88	addcld 7976	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
90	89, 81	addcld 7976	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
91	13	sqcld 10651	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
92	69, 37	mulcld 7977	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
93	91, 92	subcld 8267	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
94	90, 93	addcld 7976	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
95	93, 88	addcld 7976	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
96	89, 95, 81	add32d 8124	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
97	90, 93, 88	addassd 7979	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
98	96, 97	eqtr4d 2213	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
99	94, 88, 98	comraddd 8113	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
100	81, 93	addcld 7976	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
101	87, 100	addcld 7976	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
102	89, 81, 93	addassd 7979	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
103	87, 88	addcomd 8107	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
104	103	oveq1d 5889	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
105	102, 104	eqtrd 2210	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
106	88, 87, 100	addassd 7979	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
107	105, 106	eqtrd 2210	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
108	88, 101, 107	comraddd 8113	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
109	85, 86, 93	subadd23d 8289	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
110	91, 92, 86	subsub4d 8298	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
111	92, 86	addcomd 8107	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
112	111	oveq2d 5890	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
113	110, 112	eqtrd 2210	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
114	113	oveq2d 5890	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
115	109, 114	eqtrd 2210	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
116	115	oveq2d 5890	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
117	87, 81, 93	add12d 8123	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
118	86, 92	addcld 7976	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
119	91, 118	subcld 8267	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
120	85, 119	addcld 7976	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
121	85, 81	addcld 7976	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
122	121, 91, 118	addsubassd 8287	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
123	85, 81, 119	add32d 8124	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
124	122, 123	eqtrd 2210	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
125	120, 81, 124	comraddd 8113	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
126	116, 117, 125	3eqtr4d 2220	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
127	126	oveq1d 5889	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
128	108, 127	eqtrd 2210	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
129	128	oveq2d 5890	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
130	99, 129	eqtrd 2210	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
131		binom2sub 10633	. . . . . . . . . . 11 $/\$
132	8, 9, 131	syl2anc 411	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
133		binom2sub 10633	. . . . . . . . . . 11 $/\$
134	13, 9, 133	syl2anc 411	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
135	132, 134	oveq12d 5892	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
136	135	oveq1d 5889	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
137		binom2sub 10633	. . . . . . . . . . 11 $/\$
138	21, 9, 137	syl2anc 411	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
139		binom2 10631	. . . . . . . . . . . . 13 $/\$
140	8, 13, 139	syl2anc 411	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
141	52	oveq2d 5890	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
142	69, 36, 37	adddid 7981	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
143	141, 142	eqtrd 2210	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
144	140, 143	oveq12d 5892	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
145	144	oveq1d 5889	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
146	138, 145	eqtrd 2210	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
147	146	oveq2d 5890	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
148	130, 136, 147	3eqtr4d 2220	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
149	148	oveq1d 5889	. . . . . 6 $/\$ $/\$ $/\$ $/\$
150	84, 149	breqtrd 4029	. . . . 5 $/\$ $/\$ $/\$ $/\$
151	22	sqcld 10651	. . . . . 6 $/\$ $/\$ $/\$ $/\$
152	88, 151, 82	add32d 8124	. . . . 5 $/\$ $/\$ $/\$ $/\$
153	150, 152	breqtrd 4029	. . . 4 $/\$ $/\$ $/\$ $/\$
154		absresq 11086	. . . . . . 7
155	4, 154	syl 14	. . . . . 6 $/\$ $/\$ $/\$ $/\$
156	155	oveq1d 5889	. . . . 5 $/\$ $/\$ $/\$ $/\$
157		absresq 11086	. . . . . 6
158	28, 157	syl 14	. . . . 5 $/\$ $/\$ $/\$ $/\$
159	156, 158	oveq12d 5892	. . . 4 $/\$ $/\$ $/\$ $/\$
160	1, 12	readdcld 7986	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
161	160, 3	resubcld 8337	. . . . . 6 $/\$ $/\$ $/\$ $/\$
162		absresq 11086	. . . . . 6
163	161, 162	syl 14	. . . . 5 $/\$ $/\$ $/\$ $/\$
164	163	oveq2d 5890	. . . 4 $/\$ $/\$ $/\$ $/\$
165	153, 159, 164	3brtr4d 4035	. . 3 $/\$ $/\$ $/\$ $/\$
166	11	recnd 7985	. . . 4 $/\$ $/\$ $/\$ $/\$
167	15	recnd 7985	. . . 4 $/\$ $/\$ $/\$ $/\$
168		binom2 10631	. . . 4 $/\$
169	166, 167, 168	syl2anc 411	. . 3 $/\$ $/\$ $/\$ $/\$
170		binom2 10631	. . . 4 $/\$
171	9, 64, 170	syl2anc 411	. . 3 $/\$ $/\$ $/\$ $/\$
172	165, 169, 171	3brtr4d 4035	. 2 $/\$ $/\$ $/\$ $/\$
173	11, 15	readdcld 7986	. . 3 $/\$ $/\$ $/\$ $/\$
174	3, 23	readdcld 7986	. . 3 $/\$ $/\$ $/\$ $/\$
175	10	absge0d 11192	. . . 4 $/\$ $/\$ $/\$ $/\$
176	14	absge0d 11192	. . . 4 $/\$ $/\$ $/\$ $/\$
177	11, 15, 175, 176	addge0d 8478	. . 3 $/\$ $/\$ $/\$ $/\$
178	22	absge0d 11192	. . . 4 $/\$ $/\$ $/\$ $/\$
179	3, 23, 57, 178	addge0d 8478	. . 3 $/\$ $/\$ $/\$ $/\$
180	173, 174, 177, 179	le2sqd 10685	. 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 4003

cfv 5216 (class class class)co 5874

cc 7808

cr 7809

cc0 7810

caddc 7813

cmul 7815

cle 7992

cmin 8127

c2 8969

crp 9652

cexp 10518

cabs 11005

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 4118 ax-sep 4121 ax-nul 4129 ax-pow 4174 ax-pr 4209 ax-un 4433 ax-setind 4536 ax-iinf 4587 ax-cnex 7901 ax-resscn 7902 ax-1cn 7903 ax-1re 7904 ax-icn 7905 ax-addcl 7906 ax-addrcl 7907 ax-mulcl 7908 ax-mulrcl 7909 ax-addcom 7910 ax-mulcom 7911 ax-addass 7912 ax-mulass 7913 ax-distr 7914 ax-i2m1 7915 ax-0lt1 7916 ax-1rid 7917 ax-0id 7918 ax-rnegex 7919 ax-precex 7920 ax-cnre 7921 ax-pre-ltirr 7922 ax-pre-ltwlin 7923 ax-pre-lttrn 7924 ax-pre-apti 7925 ax-pre-ltadd 7926 ax-pre-mulgt0 7927 ax-pre-mulext 7928 ax-arch 7929 ax-caucvg 7930

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 3810 df-int 3845 df-iun 3888 df-br 4004 df-opab 4065 df-mpt 4066 df-tr 4102 df-id 4293 df-po 4296 df-iso 4297 df-iord 4366 df-on 4368 df-ilim 4369 df-suc 4371 df-iom 4590 df-xp 4632 df-rel 4633 df-cnv 4634 df-co 4635 df-dm 4636 df-rn 4637 df-res 4638 df-ima 4639 df-iota 5178 df-fun 5218 df-fn 5219 df-f 5220 df-f1 5221 df-fo 5222 df-f1o 5223 df-fv 5224 df-riota 5830 df-ov 5877 df-oprab 5878 df-mpo 5879 df-1st 6140 df-2nd 6141 df-recs 6305 df-frec 6391 df-pnf 7993 df-mnf 7994 df-xr 7995 df-ltxr 7996 df-le 7997 df-sub 8129 df-neg 8130 df-reap 8531 df-ap 8538 df-div 8629 df-inn 8919 df-2 8977 df-3 8978 df-4 8979 df-n0 9176 df-z 9253 df-uz 9528 df-rp 9653 df-seqfrec 10445 df-exp 10519 df-cj 10850 df-re 10851 df-im 10852 df-rsqrt 11006 df-abs 11007

This theorem is referenced by: bdtri 11247

W3C validator