bdtrilem - Intuitionistic Logic Explorer

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

Theorem bdtrilem 11003

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

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

**Proof of Theorem bdtrilem**
Step	Hyp	Ref	Expression
1		simp1l 1005	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
2		simp3 983	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
3	2	rpred 9476	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
4	1, 3	resubcld 8136	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
5	4	resqcld 10443	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
6		2re 8783	. . . . . . . . . . . 12
7	6	a1i 9	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
8	1	recnd 7787	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
9	2	rpcnd 9478	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
10	8, 9	subcld 8066	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
11	10	abscld 10946	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
12		simp2l 1007	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
13	12	recnd 7787	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
14	13, 9	subcld 8066	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
15	14	abscld 10946	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
16	11, 15	remulcld 7789	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
17	7, 16	remulcld 7789	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
18	5, 17	readdcld 7788	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
19	1, 12	remulcld 7789	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
20	7, 19	remulcld 7789	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
21	8, 13	addcld 7778	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
22	21, 9	subcld 8066	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
23	22	abscld 10946	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
24	3, 23	remulcld 7789	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
25	7, 24	remulcld 7789	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
26	20, 25	readdcld 7788	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
27	5, 26	readdcld 7788	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
28	12, 3	resubcld 8136	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
29	28	resqcld 10443	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
30	19, 24	readdcld 7788	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
31		0le2 8803	. . . . . . . . . . . . 13
32	31	a1i 9	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
33	8, 9, 13, 9	mulsubd 8172	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
34	19	recnd 7787	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
35	9, 9	mulcld 7779	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
36	8, 9	mulcld 7779	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
37	13, 9	mulcld 7779	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
38	36, 37	addcld 7778	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
39	34, 35, 38	addsubassd 8086	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
40	33, 39	eqtrd 2170	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
41	40	fveq2d 5418	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
42	35, 38	subcld 8066	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
43	34, 42	abstrid 10961	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
44	41, 43	eqbrtrd 3945	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
45		simp1r 1006	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
46		simp2r 1008	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
47	1, 12, 45, 46	mulge0d 8376	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
48	19, 47	absidd 10932	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
49	9, 21	subcld 8066	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
50	49, 9	absmuld 10959	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
51	9, 21, 9	subdird 8170	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
52	8, 13, 9	adddird 7784	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
53	52	oveq2d 5783	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
54	51, 53	eqtrd 2170	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
55	54	fveq2d 5418	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
56	9, 21	abssubd 10958	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
57	2	rpge0d 9480	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
58	3, 57	absidd 10932	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
59	56, 58	oveq12d 5785	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
60	50, 55, 59	3eqtr3d 2178	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
61	48, 60	oveq12d 5785	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
62	44, 61	breqtrd 3949	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
63	10, 14	absmuld 10959	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
64	23	recnd 7787	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
65	64, 9	mulcomd 7780	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
66	65	oveq2d 5783	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
67	62, 63, 66	3brtr3d 3954	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
68	16, 30, 7, 32, 67	lemul2ad 8691	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
69	7	recnd 7787	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
70	9, 64	mulcld 7779	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
71	69, 34, 70	adddid 7783	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
72	68, 71	breqtrd 3949	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
73	17, 26, 5, 72	leadd2dd 8315	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
74	18, 27, 29, 73	leadd1dd 8314	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
75	5	recnd 7787	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
76	26	recnd 7787	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
77	29	recnd 7787	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
78	75, 76, 77	add32d 7923	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
79	74, 78	breqtrd 3949	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
80	75, 77	addcld 7778	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
81	69, 34	mulcld 7779	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
82	69, 70	mulcld 7779	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
83	80, 81, 82	addassd 7781	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
84	79, 83	breqtrrd 3951	. . . . . 6 $/\$ $/\$ $/\$ $/\$
85	8	sqcld 10415	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
86	69, 36	mulcld 7779	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
87	85, 86	subcld 8066	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
88	9	sqcld 10415	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
89	87, 88	addcld 7778	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
90	89, 81	addcld 7778	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
91	13	sqcld 10415	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
92	69, 37	mulcld 7779	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
93	91, 92	subcld 8066	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
94	90, 93	addcld 7778	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
95	93, 88	addcld 7778	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
96	89, 95, 81	add32d 7923	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
97	90, 93, 88	addassd 7781	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
98	96, 97	eqtr4d 2173	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
99	94, 88, 98	comraddd 7912	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
100	81, 93	addcld 7778	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
101	87, 100	addcld 7778	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
102	89, 81, 93	addassd 7781	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
103	87, 88	addcomd 7906	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
104	103	oveq1d 5782	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
105	102, 104	eqtrd 2170	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
106	88, 87, 100	addassd 7781	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
107	105, 106	eqtrd 2170	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
108	88, 101, 107	comraddd 7912	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
109	85, 86, 93	subadd23d 8088	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
110	91, 92, 86	subsub4d 8097	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
111	92, 86	addcomd 7906	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
112	111	oveq2d 5783	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
113	110, 112	eqtrd 2170	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
114	113	oveq2d 5783	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
115	109, 114	eqtrd 2170	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
116	115	oveq2d 5783	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
117	87, 81, 93	add12d 7922	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
118	86, 92	addcld 7778	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
119	91, 118	subcld 8066	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
120	85, 119	addcld 7778	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
121	85, 81	addcld 7778	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
122	121, 91, 118	addsubassd 8086	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
123	85, 81, 119	add32d 7923	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
124	122, 123	eqtrd 2170	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
125	120, 81, 124	comraddd 7912	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
126	116, 117, 125	3eqtr4d 2180	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
127	126	oveq1d 5782	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
128	108, 127	eqtrd 2170	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
129	128	oveq2d 5783	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
130	99, 129	eqtrd 2170	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
131		binom2sub 10398	. . . . . . . . . . 11 $/\$
132	8, 9, 131	syl2anc 408	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
133		binom2sub 10398	. . . . . . . . . . 11 $/\$
134	13, 9, 133	syl2anc 408	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
135	132, 134	oveq12d 5785	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
136	135	oveq1d 5782	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
137		binom2sub 10398	. . . . . . . . . . 11 $/\$
138	21, 9, 137	syl2anc 408	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
139		binom2 10396	. . . . . . . . . . . . 13 $/\$
140	8, 13, 139	syl2anc 408	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
141	52	oveq2d 5783	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
142	69, 36, 37	adddid 7783	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
143	141, 142	eqtrd 2170	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
144	140, 143	oveq12d 5785	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
145	144	oveq1d 5782	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
146	138, 145	eqtrd 2170	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
147	146	oveq2d 5783	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
148	130, 136, 147	3eqtr4d 2180	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
149	148	oveq1d 5782	. . . . . 6 $/\$ $/\$ $/\$ $/\$
150	84, 149	breqtrd 3949	. . . . 5 $/\$ $/\$ $/\$ $/\$
151	22	sqcld 10415	. . . . . 6 $/\$ $/\$ $/\$ $/\$
152	88, 151, 82	add32d 7923	. . . . 5 $/\$ $/\$ $/\$ $/\$
153	150, 152	breqtrd 3949	. . . 4 $/\$ $/\$ $/\$ $/\$
154		absresq 10843	. . . . . . 7
155	4, 154	syl 14	. . . . . 6 $/\$ $/\$ $/\$ $/\$
156	155	oveq1d 5782	. . . . 5 $/\$ $/\$ $/\$ $/\$
157		absresq 10843	. . . . . 6
158	28, 157	syl 14	. . . . 5 $/\$ $/\$ $/\$ $/\$
159	156, 158	oveq12d 5785	. . . 4 $/\$ $/\$ $/\$ $/\$
160	1, 12	readdcld 7788	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
161	160, 3	resubcld 8136	. . . . . 6 $/\$ $/\$ $/\$ $/\$
162		absresq 10843	. . . . . 6
163	161, 162	syl 14	. . . . 5 $/\$ $/\$ $/\$ $/\$
164	163	oveq2d 5783	. . . 4 $/\$ $/\$ $/\$ $/\$
165	153, 159, 164	3brtr4d 3955	. . 3 $/\$ $/\$ $/\$ $/\$
166	11	recnd 7787	. . . 4 $/\$ $/\$ $/\$ $/\$
167	15	recnd 7787	. . . 4 $/\$ $/\$ $/\$ $/\$
168		binom2 10396	. . . 4 $/\$
169	166, 167, 168	syl2anc 408	. . 3 $/\$ $/\$ $/\$ $/\$
170		binom2 10396	. . . 4 $/\$
171	9, 64, 170	syl2anc 408	. . 3 $/\$ $/\$ $/\$ $/\$
172	165, 169, 171	3brtr4d 3955	. 2 $/\$ $/\$ $/\$ $/\$
173	11, 15	readdcld 7788	. . 3 $/\$ $/\$ $/\$ $/\$
174	3, 23	readdcld 7788	. . 3 $/\$ $/\$ $/\$ $/\$
175	10	absge0d 10949	. . . 4 $/\$ $/\$ $/\$ $/\$
176	14	absge0d 10949	. . . 4 $/\$ $/\$ $/\$ $/\$
177	11, 15, 175, 176	addge0d 8277	. . 3 $/\$ $/\$ $/\$ $/\$
178	22	absge0d 10949	. . . 4 $/\$ $/\$ $/\$ $/\$
179	3, 23, 57, 178	addge0d 8277	. . 3 $/\$ $/\$ $/\$ $/\$
180	173, 174, 177, 179	le2sqd 10449	. 2 $/\$ $/\$ $/\$ $/\$
181	172, 180	mpbird 166	1 $/\$ $/\$ $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 103 $/\$ w3a 962

wceq 1331

wcel 1480 class class class wbr 3924

cfv 5118 (class class class)co 5767

cc 7611

cr 7612

cc0 7613

caddc 7616

cmul 7618

cle 7794

cmin 7926

c2 8764

crp 9434

cexp 10285

cabs 10762

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 603 ax-in2 604 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-13 1491 ax-14 1492 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2119 ax-coll 4038 ax-sep 4041 ax-nul 4049 ax-pow 4093 ax-pr 4126 ax-un 4350 ax-setind 4447 ax-iinf 4497 ax-cnex 7704 ax-resscn 7705 ax-1cn 7706 ax-1re 7707 ax-icn 7708 ax-addcl 7709 ax-addrcl 7710 ax-mulcl 7711 ax-mulrcl 7712 ax-addcom 7713 ax-mulcom 7714 ax-addass 7715 ax-mulass 7716 ax-distr 7717 ax-i2m1 7718 ax-0lt1 7719 ax-1rid 7720 ax-0id 7721 ax-rnegex 7722 ax-precex 7723 ax-cnre 7724 ax-pre-ltirr 7725 ax-pre-ltwlin 7726 ax-pre-lttrn 7727 ax-pre-apti 7728 ax-pre-ltadd 7729 ax-pre-mulgt0 7730 ax-pre-mulext 7731 ax-arch 7732 ax-caucvg 7733

This theorem depends on definitions: df-bi 116 df-dc 820 df-3or 963 df-3an 964 df-tru 1334 df-fal 1337 df-nf 1437 df-sb 1736 df-eu 2000 df-mo 2001 df-clab 2124 df-cleq 2130 df-clel 2133 df-nfc 2268 df-ne 2307 df-nel 2402 df-ral 2419 df-rex 2420 df-reu 2421 df-rmo 2422 df-rab 2423 df-v 2683 df-sbc 2905 df-csb 2999 df-dif 3068 df-un 3070 df-in 3072 df-ss 3079 df-nul 3359 df-if 3470 df-pw 3507 df-sn 3528 df-pr 3529 df-op 3531 df-uni 3732 df-int 3767 df-iun 3810 df-br 3925 df-opab 3985 df-mpt 3986 df-tr 4022 df-id 4210 df-po 4213 df-iso 4214 df-iord 4283 df-on 4285 df-ilim 4286 df-suc 4288 df-iom 4500 df-xp 4540 df-rel 4541 df-cnv 4542 df-co 4543 df-dm 4544 df-rn 4545 df-res 4546 df-ima 4547 df-iota 5083 df-fun 5120 df-fn 5121 df-f 5122 df-f1 5123 df-fo 5124 df-f1o 5125 df-fv 5126 df-riota 5723 df-ov 5770 df-oprab 5771 df-mpo 5772 df-1st 6031 df-2nd 6032 df-recs 6195 df-frec 6281 df-pnf 7795 df-mnf 7796 df-xr 7797 df-ltxr 7798 df-le 7799 df-sub 7928 df-neg 7929 df-reap 8330 df-ap 8337 df-div 8426 df-inn 8714 df-2 8772 df-3 8773 df-4 8774 df-n0 8971 df-z 9048 df-uz 9320 df-rp 9435 df-seqfrec 10212 df-exp 10286 df-cj 10607 df-re 10608 df-im 10609 df-rsqrt 10763 df-abs 10764

This theorem is referenced by: bdtri 11004

W3C validator