bdtrilem - Intuitionistic Logic Explorer

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

Theorem bdtrilem 11665

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

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

**Proof of Theorem bdtrilem**
Step	Hyp	Ref	Expression
1		simp1l 1024	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
2		simp3 1002	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
3	2	rpred 9853	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
4	1, 3	resubcld 8488	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
5	4	resqcld 10881	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
6		2re 9141	. . . . . . . . . . . 12
7	6	a1i 9	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
8	1	recnd 8136	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
9	2	rpcnd 9855	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
10	8, 9	subcld 8418	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
11	10	abscld 11607	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
12		simp2l 1026	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
13	12	recnd 8136	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
14	13, 9	subcld 8418	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
15	14	abscld 11607	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
16	11, 15	remulcld 8138	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
17	7, 16	remulcld 8138	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
18	5, 17	readdcld 8137	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
19	1, 12	remulcld 8138	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
20	7, 19	remulcld 8138	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
21	8, 13	addcld 8127	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
22	21, 9	subcld 8418	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
23	22	abscld 11607	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
24	3, 23	remulcld 8138	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
25	7, 24	remulcld 8138	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
26	20, 25	readdcld 8137	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
27	5, 26	readdcld 8137	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
28	12, 3	resubcld 8488	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
29	28	resqcld 10881	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
30	19, 24	readdcld 8137	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
31		0le2 9161	. . . . . . . . . . . . 13
32	31	a1i 9	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
33	8, 9, 13, 9	mulsubd 8524	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
34	19	recnd 8136	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
35	9, 9	mulcld 8128	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
36	8, 9	mulcld 8128	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
37	13, 9	mulcld 8128	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
38	36, 37	addcld 8127	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
39	34, 35, 38	addsubassd 8438	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
40	33, 39	eqtrd 2240	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
41	40	fveq2d 5603	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
42	35, 38	subcld 8418	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
43	34, 42	abstrid 11622	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
44	41, 43	eqbrtrd 4081	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
45		simp1r 1025	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
46		simp2r 1027	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
47	1, 12, 45, 46	mulge0d 8729	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
48	19, 47	absidd 11593	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
49	9, 21	subcld 8418	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
50	49, 9	absmuld 11620	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
51	9, 21, 9	subdird 8522	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
52	8, 13, 9	adddird 8133	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
53	52	oveq2d 5983	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
54	51, 53	eqtrd 2240	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
55	54	fveq2d 5603	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
56	9, 21	abssubd 11619	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
57	2	rpge0d 9857	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
58	3, 57	absidd 11593	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
59	56, 58	oveq12d 5985	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
60	50, 55, 59	3eqtr3d 2248	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
61	48, 60	oveq12d 5985	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
62	44, 61	breqtrd 4085	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
63	10, 14	absmuld 11620	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
64	23	recnd 8136	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
65	64, 9	mulcomd 8129	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
66	65	oveq2d 5983	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
67	62, 63, 66	3brtr3d 4090	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
68	16, 30, 7, 32, 67	lemul2ad 9048	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
69	7	recnd 8136	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
70	9, 64	mulcld 8128	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
71	69, 34, 70	adddid 8132	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
72	68, 71	breqtrd 4085	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
73	17, 26, 5, 72	leadd2dd 8668	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
74	18, 27, 29, 73	leadd1dd 8667	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
75	5	recnd 8136	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
76	26	recnd 8136	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
77	29	recnd 8136	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
78	75, 76, 77	add32d 8275	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
79	74, 78	breqtrd 4085	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
80	75, 77	addcld 8127	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
81	69, 34	mulcld 8128	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
82	69, 70	mulcld 8128	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
83	80, 81, 82	addassd 8130	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
84	79, 83	breqtrrd 4087	. . . . . 6 $/\$ $/\$ $/\$ $/\$
85	8	sqcld 10853	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
86	69, 36	mulcld 8128	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
87	85, 86	subcld 8418	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
88	9	sqcld 10853	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
89	87, 88	addcld 8127	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
90	89, 81	addcld 8127	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
91	13	sqcld 10853	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
92	69, 37	mulcld 8128	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
93	91, 92	subcld 8418	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
94	90, 93	addcld 8127	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
95	93, 88	addcld 8127	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
96	89, 95, 81	add32d 8275	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
97	90, 93, 88	addassd 8130	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
98	96, 97	eqtr4d 2243	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
99	94, 88, 98	comraddd 8264	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
100	81, 93	addcld 8127	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
101	87, 100	addcld 8127	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
102	89, 81, 93	addassd 8130	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
103	87, 88	addcomd 8258	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
104	103	oveq1d 5982	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
105	102, 104	eqtrd 2240	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
106	88, 87, 100	addassd 8130	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
107	105, 106	eqtrd 2240	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
108	88, 101, 107	comraddd 8264	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
109	85, 86, 93	subadd23d 8440	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
110	91, 92, 86	subsub4d 8449	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
111	92, 86	addcomd 8258	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
112	111	oveq2d 5983	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
113	110, 112	eqtrd 2240	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
114	113	oveq2d 5983	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
115	109, 114	eqtrd 2240	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
116	115	oveq2d 5983	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
117	87, 81, 93	add12d 8274	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
118	86, 92	addcld 8127	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
119	91, 118	subcld 8418	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
120	85, 119	addcld 8127	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
121	85, 81	addcld 8127	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
122	121, 91, 118	addsubassd 8438	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
123	85, 81, 119	add32d 8275	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
124	122, 123	eqtrd 2240	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
125	120, 81, 124	comraddd 8264	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
126	116, 117, 125	3eqtr4d 2250	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
127	126	oveq1d 5982	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
128	108, 127	eqtrd 2240	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
129	128	oveq2d 5983	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
130	99, 129	eqtrd 2240	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
131		binom2sub 10835	. . . . . . . . . . 11 $/\$
132	8, 9, 131	syl2anc 411	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
133		binom2sub 10835	. . . . . . . . . . 11 $/\$
134	13, 9, 133	syl2anc 411	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
135	132, 134	oveq12d 5985	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
136	135	oveq1d 5982	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
137		binom2sub 10835	. . . . . . . . . . 11 $/\$
138	21, 9, 137	syl2anc 411	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
139		binom2 10833	. . . . . . . . . . . . 13 $/\$
140	8, 13, 139	syl2anc 411	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
141	52	oveq2d 5983	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
142	69, 36, 37	adddid 8132	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
143	141, 142	eqtrd 2240	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
144	140, 143	oveq12d 5985	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
145	144	oveq1d 5982	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
146	138, 145	eqtrd 2240	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
147	146	oveq2d 5983	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
148	130, 136, 147	3eqtr4d 2250	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
149	148	oveq1d 5982	. . . . . 6 $/\$ $/\$ $/\$ $/\$
150	84, 149	breqtrd 4085	. . . . 5 $/\$ $/\$ $/\$ $/\$
151	22	sqcld 10853	. . . . . 6 $/\$ $/\$ $/\$ $/\$
152	88, 151, 82	add32d 8275	. . . . 5 $/\$ $/\$ $/\$ $/\$
153	150, 152	breqtrd 4085	. . . 4 $/\$ $/\$ $/\$ $/\$
154		absresq 11504	. . . . . . 7
155	4, 154	syl 14	. . . . . 6 $/\$ $/\$ $/\$ $/\$
156	155	oveq1d 5982	. . . . 5 $/\$ $/\$ $/\$ $/\$
157		absresq 11504	. . . . . 6
158	28, 157	syl 14	. . . . 5 $/\$ $/\$ $/\$ $/\$
159	156, 158	oveq12d 5985	. . . 4 $/\$ $/\$ $/\$ $/\$
160	1, 12	readdcld 8137	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
161	160, 3	resubcld 8488	. . . . . 6 $/\$ $/\$ $/\$ $/\$
162		absresq 11504	. . . . . 6
163	161, 162	syl 14	. . . . 5 $/\$ $/\$ $/\$ $/\$
164	163	oveq2d 5983	. . . 4 $/\$ $/\$ $/\$ $/\$
165	153, 159, 164	3brtr4d 4091	. . 3 $/\$ $/\$ $/\$ $/\$
166	11	recnd 8136	. . . 4 $/\$ $/\$ $/\$ $/\$
167	15	recnd 8136	. . . 4 $/\$ $/\$ $/\$ $/\$
168		binom2 10833	. . . 4 $/\$
169	166, 167, 168	syl2anc 411	. . 3 $/\$ $/\$ $/\$ $/\$
170		binom2 10833	. . . 4 $/\$
171	9, 64, 170	syl2anc 411	. . 3 $/\$ $/\$ $/\$ $/\$
172	165, 169, 171	3brtr4d 4091	. 2 $/\$ $/\$ $/\$ $/\$
173	11, 15	readdcld 8137	. . 3 $/\$ $/\$ $/\$ $/\$
174	3, 23	readdcld 8137	. . 3 $/\$ $/\$ $/\$ $/\$
175	10	absge0d 11610	. . . 4 $/\$ $/\$ $/\$ $/\$
176	14	absge0d 11610	. . . 4 $/\$ $/\$ $/\$ $/\$
177	11, 15, 175, 176	addge0d 8630	. . 3 $/\$ $/\$ $/\$ $/\$
178	22	absge0d 11610	. . . 4 $/\$ $/\$ $/\$ $/\$
179	3, 23, 57, 178	addge0d 8630	. . 3 $/\$ $/\$ $/\$ $/\$
180	173, 174, 177, 179	le2sqd 10887	. 2 $/\$ $/\$ $/\$ $/\$
181	172, 180	mpbird 167	1 $/\$ $/\$ $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

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

wceq 1373

wcel 2178 class class class wbr 4059

cfv 5290 (class class class)co 5967

cc 7958

cr 7959

cc0 7960

caddc 7963

cmul 7965

cle 8143

cmin 8278

c2 9122

crp 9810

cexp 10720

cabs 11423

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 615 ax-in2 616 ax-io 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2180 ax-14 2181 ax-ext 2189 ax-coll 4175 ax-sep 4178 ax-nul 4186 ax-pow 4234 ax-pr 4269 ax-un 4498 ax-setind 4603 ax-iinf 4654 ax-cnex 8051 ax-resscn 8052 ax-1cn 8053 ax-1re 8054 ax-icn 8055 ax-addcl 8056 ax-addrcl 8057 ax-mulcl 8058 ax-mulrcl 8059 ax-addcom 8060 ax-mulcom 8061 ax-addass 8062 ax-mulass 8063 ax-distr 8064 ax-i2m1 8065 ax-0lt1 8066 ax-1rid 8067 ax-0id 8068 ax-rnegex 8069 ax-precex 8070 ax-cnre 8071 ax-pre-ltirr 8072 ax-pre-ltwlin 8073 ax-pre-lttrn 8074 ax-pre-apti 8075 ax-pre-ltadd 8076 ax-pre-mulgt0 8077 ax-pre-mulext 8078 ax-arch 8079 ax-caucvg 8080

This theorem depends on definitions: df-bi 117 df-dc 837 df-3or 982 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2194 df-cleq 2200 df-clel 2203 df-nfc 2339 df-ne 2379 df-nel 2474 df-ral 2491 df-rex 2492 df-reu 2493 df-rmo 2494 df-rab 2495 df-v 2778 df-sbc 3006 df-csb 3102 df-dif 3176 df-un 3178 df-in 3180 df-ss 3187 df-nul 3469 df-if 3580 df-pw 3628 df-sn 3649 df-pr 3650 df-op 3652 df-uni 3865 df-int 3900 df-iun 3943 df-br 4060 df-opab 4122 df-mpt 4123 df-tr 4159 df-id 4358 df-po 4361 df-iso 4362 df-iord 4431 df-on 4433 df-ilim 4434 df-suc 4436 df-iom 4657 df-xp 4699 df-rel 4700 df-cnv 4701 df-co 4702 df-dm 4703 df-rn 4704 df-res 4705 df-ima 4706 df-iota 5251 df-fun 5292 df-fn 5293 df-f 5294 df-f1 5295 df-fo 5296 df-f1o 5297 df-fv 5298 df-riota 5922 df-ov 5970 df-oprab 5971 df-mpo 5972 df-1st 6249 df-2nd 6250 df-recs 6414 df-frec 6500 df-pnf 8144 df-mnf 8145 df-xr 8146 df-ltxr 8147 df-le 8148 df-sub 8280 df-neg 8281 df-reap 8683 df-ap 8690 df-div 8781 df-inn 9072 df-2 9130 df-3 9131 df-4 9132 df-n0 9331 df-z 9408 df-uz 9684 df-rp 9811 df-seqfrec 10630 df-exp 10721 df-cj 11268 df-re 11269 df-im 11270 df-rsqrt 11424 df-abs 11425

This theorem is referenced by: bdtri 11666

W3C validator