bdtrilem - Intuitionistic Logic Explorer

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

Theorem bdtrilem 11202

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

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

**Proof of Theorem bdtrilem**
Step	Hyp	Ref	Expression
1		simp1l 1016	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
2		simp3 994	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
3	2	rpred 9653	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
4	1, 3	resubcld 8300	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
5	4	resqcld 10635	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
6		2re 8948	. . . . . . . . . . . 12
7	6	a1i 9	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
8	1	recnd 7948	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
9	2	rpcnd 9655	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
10	8, 9	subcld 8230	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
11	10	abscld 11145	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
12		simp2l 1018	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
13	12	recnd 7948	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
14	13, 9	subcld 8230	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
15	14	abscld 11145	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
16	11, 15	remulcld 7950	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
17	7, 16	remulcld 7950	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
18	5, 17	readdcld 7949	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
19	1, 12	remulcld 7950	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
20	7, 19	remulcld 7950	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
21	8, 13	addcld 7939	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
22	21, 9	subcld 8230	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
23	22	abscld 11145	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
24	3, 23	remulcld 7950	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
25	7, 24	remulcld 7950	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
26	20, 25	readdcld 7949	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
27	5, 26	readdcld 7949	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
28	12, 3	resubcld 8300	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
29	28	resqcld 10635	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
30	19, 24	readdcld 7949	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
31		0le2 8968	. . . . . . . . . . . . 13
32	31	a1i 9	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
33	8, 9, 13, 9	mulsubd 8336	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
34	19	recnd 7948	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
35	9, 9	mulcld 7940	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
36	8, 9	mulcld 7940	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
37	13, 9	mulcld 7940	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
38	36, 37	addcld 7939	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
39	34, 35, 38	addsubassd 8250	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
40	33, 39	eqtrd 2203	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
41	40	fveq2d 5500	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
42	35, 38	subcld 8230	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
43	34, 42	abstrid 11160	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
44	41, 43	eqbrtrd 4011	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
45		simp1r 1017	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
46		simp2r 1019	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
47	1, 12, 45, 46	mulge0d 8540	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
48	19, 47	absidd 11131	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
49	9, 21	subcld 8230	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
50	49, 9	absmuld 11158	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
51	9, 21, 9	subdird 8334	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
52	8, 13, 9	adddird 7945	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
53	52	oveq2d 5869	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
54	51, 53	eqtrd 2203	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
55	54	fveq2d 5500	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
56	9, 21	abssubd 11157	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
57	2	rpge0d 9657	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
58	3, 57	absidd 11131	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
59	56, 58	oveq12d 5871	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
60	50, 55, 59	3eqtr3d 2211	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
61	48, 60	oveq12d 5871	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
62	44, 61	breqtrd 4015	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
63	10, 14	absmuld 11158	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
64	23	recnd 7948	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
65	64, 9	mulcomd 7941	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
66	65	oveq2d 5869	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
67	62, 63, 66	3brtr3d 4020	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
68	16, 30, 7, 32, 67	lemul2ad 8856	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
69	7	recnd 7948	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
70	9, 64	mulcld 7940	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
71	69, 34, 70	adddid 7944	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
72	68, 71	breqtrd 4015	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
73	17, 26, 5, 72	leadd2dd 8479	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
74	18, 27, 29, 73	leadd1dd 8478	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
75	5	recnd 7948	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
76	26	recnd 7948	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
77	29	recnd 7948	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
78	75, 76, 77	add32d 8087	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
79	74, 78	breqtrd 4015	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
80	75, 77	addcld 7939	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
81	69, 34	mulcld 7940	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
82	69, 70	mulcld 7940	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
83	80, 81, 82	addassd 7942	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
84	79, 83	breqtrrd 4017	. . . . . 6 $/\$ $/\$ $/\$ $/\$
85	8	sqcld 10607	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
86	69, 36	mulcld 7940	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
87	85, 86	subcld 8230	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
88	9	sqcld 10607	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
89	87, 88	addcld 7939	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
90	89, 81	addcld 7939	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
91	13	sqcld 10607	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
92	69, 37	mulcld 7940	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
93	91, 92	subcld 8230	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
94	90, 93	addcld 7939	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
95	93, 88	addcld 7939	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
96	89, 95, 81	add32d 8087	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
97	90, 93, 88	addassd 7942	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
98	96, 97	eqtr4d 2206	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
99	94, 88, 98	comraddd 8076	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
100	81, 93	addcld 7939	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
101	87, 100	addcld 7939	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
102	89, 81, 93	addassd 7942	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
103	87, 88	addcomd 8070	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
104	103	oveq1d 5868	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
105	102, 104	eqtrd 2203	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
106	88, 87, 100	addassd 7942	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
107	105, 106	eqtrd 2203	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
108	88, 101, 107	comraddd 8076	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
109	85, 86, 93	subadd23d 8252	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
110	91, 92, 86	subsub4d 8261	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
111	92, 86	addcomd 8070	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
112	111	oveq2d 5869	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
113	110, 112	eqtrd 2203	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
114	113	oveq2d 5869	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
115	109, 114	eqtrd 2203	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
116	115	oveq2d 5869	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
117	87, 81, 93	add12d 8086	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
118	86, 92	addcld 7939	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
119	91, 118	subcld 8230	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
120	85, 119	addcld 7939	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
121	85, 81	addcld 7939	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
122	121, 91, 118	addsubassd 8250	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
123	85, 81, 119	add32d 8087	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
124	122, 123	eqtrd 2203	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
125	120, 81, 124	comraddd 8076	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
126	116, 117, 125	3eqtr4d 2213	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
127	126	oveq1d 5868	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
128	108, 127	eqtrd 2203	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
129	128	oveq2d 5869	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
130	99, 129	eqtrd 2203	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
131		binom2sub 10589	. . . . . . . . . . 11 $/\$
132	8, 9, 131	syl2anc 409	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
133		binom2sub 10589	. . . . . . . . . . 11 $/\$
134	13, 9, 133	syl2anc 409	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
135	132, 134	oveq12d 5871	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
136	135	oveq1d 5868	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
137		binom2sub 10589	. . . . . . . . . . 11 $/\$
138	21, 9, 137	syl2anc 409	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
139		binom2 10587	. . . . . . . . . . . . 13 $/\$
140	8, 13, 139	syl2anc 409	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
141	52	oveq2d 5869	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
142	69, 36, 37	adddid 7944	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
143	141, 142	eqtrd 2203	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
144	140, 143	oveq12d 5871	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
145	144	oveq1d 5868	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
146	138, 145	eqtrd 2203	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
147	146	oveq2d 5869	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
148	130, 136, 147	3eqtr4d 2213	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
149	148	oveq1d 5868	. . . . . 6 $/\$ $/\$ $/\$ $/\$
150	84, 149	breqtrd 4015	. . . . 5 $/\$ $/\$ $/\$ $/\$
151	22	sqcld 10607	. . . . . 6 $/\$ $/\$ $/\$ $/\$
152	88, 151, 82	add32d 8087	. . . . 5 $/\$ $/\$ $/\$ $/\$
153	150, 152	breqtrd 4015	. . . 4 $/\$ $/\$ $/\$ $/\$
154		absresq 11042	. . . . . . 7
155	4, 154	syl 14	. . . . . 6 $/\$ $/\$ $/\$ $/\$
156	155	oveq1d 5868	. . . . 5 $/\$ $/\$ $/\$ $/\$
157		absresq 11042	. . . . . 6
158	28, 157	syl 14	. . . . 5 $/\$ $/\$ $/\$ $/\$
159	156, 158	oveq12d 5871	. . . 4 $/\$ $/\$ $/\$ $/\$
160	1, 12	readdcld 7949	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
161	160, 3	resubcld 8300	. . . . . 6 $/\$ $/\$ $/\$ $/\$
162		absresq 11042	. . . . . 6
163	161, 162	syl 14	. . . . 5 $/\$ $/\$ $/\$ $/\$
164	163	oveq2d 5869	. . . 4 $/\$ $/\$ $/\$ $/\$
165	153, 159, 164	3brtr4d 4021	. . 3 $/\$ $/\$ $/\$ $/\$
166	11	recnd 7948	. . . 4 $/\$ $/\$ $/\$ $/\$
167	15	recnd 7948	. . . 4 $/\$ $/\$ $/\$ $/\$
168		binom2 10587	. . . 4 $/\$
169	166, 167, 168	syl2anc 409	. . 3 $/\$ $/\$ $/\$ $/\$
170		binom2 10587	. . . 4 $/\$
171	9, 64, 170	syl2anc 409	. . 3 $/\$ $/\$ $/\$ $/\$
172	165, 169, 171	3brtr4d 4021	. 2 $/\$ $/\$ $/\$ $/\$
173	11, 15	readdcld 7949	. . 3 $/\$ $/\$ $/\$ $/\$
174	3, 23	readdcld 7949	. . 3 $/\$ $/\$ $/\$ $/\$
175	10	absge0d 11148	. . . 4 $/\$ $/\$ $/\$ $/\$
176	14	absge0d 11148	. . . 4 $/\$ $/\$ $/\$ $/\$
177	11, 15, 175, 176	addge0d 8441	. . 3 $/\$ $/\$ $/\$ $/\$
178	22	absge0d 11148	. . . 4 $/\$ $/\$ $/\$ $/\$
179	3, 23, 57, 178	addge0d 8441	. . 3 $/\$ $/\$ $/\$ $/\$
180	173, 174, 177, 179	le2sqd 10641	. 2 $/\$ $/\$ $/\$ $/\$
181	172, 180	mpbird 166	1 $/\$ $/\$ $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

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

wceq 1348

wcel 2141 class class class wbr 3989

cfv 5198 (class class class)co 5853

cc 7772

cr 7773

cc0 7774

caddc 7777

cmul 7779

cle 7955

cmin 8090

c2 8929

crp 9610

cexp 10475

cabs 10961

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 609 ax-in2 610 ax-io 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-13 2143 ax-14 2144 ax-ext 2152 ax-coll 4104 ax-sep 4107 ax-nul 4115 ax-pow 4160 ax-pr 4194 ax-un 4418 ax-setind 4521 ax-iinf 4572 ax-cnex 7865 ax-resscn 7866 ax-1cn 7867 ax-1re 7868 ax-icn 7869 ax-addcl 7870 ax-addrcl 7871 ax-mulcl 7872 ax-mulrcl 7873 ax-addcom 7874 ax-mulcom 7875 ax-addass 7876 ax-mulass 7877 ax-distr 7878 ax-i2m1 7879 ax-0lt1 7880 ax-1rid 7881 ax-0id 7882 ax-rnegex 7883 ax-precex 7884 ax-cnre 7885 ax-pre-ltirr 7886 ax-pre-ltwlin 7887 ax-pre-lttrn 7888 ax-pre-apti 7889 ax-pre-ltadd 7890 ax-pre-mulgt0 7891 ax-pre-mulext 7892 ax-arch 7893 ax-caucvg 7894

This theorem depends on definitions: df-bi 116 df-dc 830 df-3or 974 df-3an 975 df-tru 1351 df-fal 1354 df-nf 1454 df-sb 1756 df-eu 2022 df-mo 2023 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-ne 2341 df-nel 2436 df-ral 2453 df-rex 2454 df-reu 2455 df-rmo 2456 df-rab 2457 df-v 2732 df-sbc 2956 df-csb 3050 df-dif 3123 df-un 3125 df-in 3127 df-ss 3134 df-nul 3415 df-if 3527 df-pw 3568 df-sn 3589 df-pr 3590 df-op 3592 df-uni 3797 df-int 3832 df-iun 3875 df-br 3990 df-opab 4051 df-mpt 4052 df-tr 4088 df-id 4278 df-po 4281 df-iso 4282 df-iord 4351 df-on 4353 df-ilim 4354 df-suc 4356 df-iom 4575 df-xp 4617 df-rel 4618 df-cnv 4619 df-co 4620 df-dm 4621 df-rn 4622 df-res 4623 df-ima 4624 df-iota 5160 df-fun 5200 df-fn 5201 df-f 5202 df-f1 5203 df-fo 5204 df-f1o 5205 df-fv 5206 df-riota 5809 df-ov 5856 df-oprab 5857 df-mpo 5858 df-1st 6119 df-2nd 6120 df-recs 6284 df-frec 6370 df-pnf 7956 df-mnf 7957 df-xr 7958 df-ltxr 7959 df-le 7960 df-sub 8092 df-neg 8093 df-reap 8494 df-ap 8501 df-div 8590 df-inn 8879 df-2 8937 df-3 8938 df-4 8939 df-n0 9136 df-z 9213 df-uz 9488 df-rp 9611 df-seqfrec 10402 df-exp 10476 df-cj 10806 df-re 10807 df-im 10808 df-rsqrt 10962 df-abs 10963

This theorem is referenced by: bdtri 11203

W3C validator