bdtrilem - Intuitionistic Logic Explorer

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

Theorem bdtrilem 11042

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

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

**Proof of Theorem bdtrilem**
Step	Hyp	Ref	Expression
1		simp1l 1006	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
2		simp3 984	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
3	2	rpred 9513	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
4	1, 3	resubcld 8167	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
5	4	resqcld 10481	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
6		2re 8814	. . . . . . . . . . . 12
7	6	a1i 9	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
8	1	recnd 7818	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
9	2	rpcnd 9515	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
10	8, 9	subcld 8097	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
11	10	abscld 10985	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
12		simp2l 1008	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
13	12	recnd 7818	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
14	13, 9	subcld 8097	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
15	14	abscld 10985	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
16	11, 15	remulcld 7820	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
17	7, 16	remulcld 7820	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
18	5, 17	readdcld 7819	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
19	1, 12	remulcld 7820	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
20	7, 19	remulcld 7820	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
21	8, 13	addcld 7809	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
22	21, 9	subcld 8097	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
23	22	abscld 10985	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
24	3, 23	remulcld 7820	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
25	7, 24	remulcld 7820	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
26	20, 25	readdcld 7819	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
27	5, 26	readdcld 7819	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
28	12, 3	resubcld 8167	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
29	28	resqcld 10481	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
30	19, 24	readdcld 7819	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
31		0le2 8834	. . . . . . . . . . . . 13
32	31	a1i 9	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
33	8, 9, 13, 9	mulsubd 8203	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
34	19	recnd 7818	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
35	9, 9	mulcld 7810	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
36	8, 9	mulcld 7810	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
37	13, 9	mulcld 7810	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
38	36, 37	addcld 7809	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
39	34, 35, 38	addsubassd 8117	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
40	33, 39	eqtrd 2173	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
41	40	fveq2d 5433	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
42	35, 38	subcld 8097	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
43	34, 42	abstrid 11000	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
44	41, 43	eqbrtrd 3958	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
45		simp1r 1007	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
46		simp2r 1009	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
47	1, 12, 45, 46	mulge0d 8407	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
48	19, 47	absidd 10971	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
49	9, 21	subcld 8097	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
50	49, 9	absmuld 10998	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
51	9, 21, 9	subdird 8201	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
52	8, 13, 9	adddird 7815	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
53	52	oveq2d 5798	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
54	51, 53	eqtrd 2173	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
55	54	fveq2d 5433	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
56	9, 21	abssubd 10997	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
57	2	rpge0d 9517	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
58	3, 57	absidd 10971	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
59	56, 58	oveq12d 5800	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
60	50, 55, 59	3eqtr3d 2181	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
61	48, 60	oveq12d 5800	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
62	44, 61	breqtrd 3962	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
63	10, 14	absmuld 10998	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
64	23	recnd 7818	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
65	64, 9	mulcomd 7811	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
66	65	oveq2d 5798	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
67	62, 63, 66	3brtr3d 3967	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
68	16, 30, 7, 32, 67	lemul2ad 8722	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
69	7	recnd 7818	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
70	9, 64	mulcld 7810	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
71	69, 34, 70	adddid 7814	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
72	68, 71	breqtrd 3962	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
73	17, 26, 5, 72	leadd2dd 8346	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
74	18, 27, 29, 73	leadd1dd 8345	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
75	5	recnd 7818	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
76	26	recnd 7818	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
77	29	recnd 7818	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
78	75, 76, 77	add32d 7954	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
79	74, 78	breqtrd 3962	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
80	75, 77	addcld 7809	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
81	69, 34	mulcld 7810	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
82	69, 70	mulcld 7810	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
83	80, 81, 82	addassd 7812	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
84	79, 83	breqtrrd 3964	. . . . . 6 $/\$ $/\$ $/\$ $/\$
85	8	sqcld 10453	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
86	69, 36	mulcld 7810	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
87	85, 86	subcld 8097	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
88	9	sqcld 10453	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
89	87, 88	addcld 7809	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
90	89, 81	addcld 7809	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
91	13	sqcld 10453	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
92	69, 37	mulcld 7810	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
93	91, 92	subcld 8097	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
94	90, 93	addcld 7809	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
95	93, 88	addcld 7809	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
96	89, 95, 81	add32d 7954	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
97	90, 93, 88	addassd 7812	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
98	96, 97	eqtr4d 2176	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
99	94, 88, 98	comraddd 7943	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
100	81, 93	addcld 7809	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
101	87, 100	addcld 7809	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
102	89, 81, 93	addassd 7812	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
103	87, 88	addcomd 7937	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
104	103	oveq1d 5797	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
105	102, 104	eqtrd 2173	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
106	88, 87, 100	addassd 7812	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
107	105, 106	eqtrd 2173	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
108	88, 101, 107	comraddd 7943	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
109	85, 86, 93	subadd23d 8119	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
110	91, 92, 86	subsub4d 8128	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
111	92, 86	addcomd 7937	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
112	111	oveq2d 5798	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
113	110, 112	eqtrd 2173	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
114	113	oveq2d 5798	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
115	109, 114	eqtrd 2173	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
116	115	oveq2d 5798	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
117	87, 81, 93	add12d 7953	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
118	86, 92	addcld 7809	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
119	91, 118	subcld 8097	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
120	85, 119	addcld 7809	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
121	85, 81	addcld 7809	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
122	121, 91, 118	addsubassd 8117	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
123	85, 81, 119	add32d 7954	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
124	122, 123	eqtrd 2173	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
125	120, 81, 124	comraddd 7943	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
126	116, 117, 125	3eqtr4d 2183	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
127	126	oveq1d 5797	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
128	108, 127	eqtrd 2173	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
129	128	oveq2d 5798	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
130	99, 129	eqtrd 2173	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
131		binom2sub 10436	. . . . . . . . . . 11 $/\$
132	8, 9, 131	syl2anc 409	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
133		binom2sub 10436	. . . . . . . . . . 11 $/\$
134	13, 9, 133	syl2anc 409	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
135	132, 134	oveq12d 5800	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
136	135	oveq1d 5797	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
137		binom2sub 10436	. . . . . . . . . . 11 $/\$
138	21, 9, 137	syl2anc 409	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
139		binom2 10434	. . . . . . . . . . . . 13 $/\$
140	8, 13, 139	syl2anc 409	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
141	52	oveq2d 5798	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
142	69, 36, 37	adddid 7814	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
143	141, 142	eqtrd 2173	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
144	140, 143	oveq12d 5800	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
145	144	oveq1d 5797	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
146	138, 145	eqtrd 2173	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
147	146	oveq2d 5798	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
148	130, 136, 147	3eqtr4d 2183	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
149	148	oveq1d 5797	. . . . . 6 $/\$ $/\$ $/\$ $/\$
150	84, 149	breqtrd 3962	. . . . 5 $/\$ $/\$ $/\$ $/\$
151	22	sqcld 10453	. . . . . 6 $/\$ $/\$ $/\$ $/\$
152	88, 151, 82	add32d 7954	. . . . 5 $/\$ $/\$ $/\$ $/\$
153	150, 152	breqtrd 3962	. . . 4 $/\$ $/\$ $/\$ $/\$
154		absresq 10882	. . . . . . 7
155	4, 154	syl 14	. . . . . 6 $/\$ $/\$ $/\$ $/\$
156	155	oveq1d 5797	. . . . 5 $/\$ $/\$ $/\$ $/\$
157		absresq 10882	. . . . . 6
158	28, 157	syl 14	. . . . 5 $/\$ $/\$ $/\$ $/\$
159	156, 158	oveq12d 5800	. . . 4 $/\$ $/\$ $/\$ $/\$
160	1, 12	readdcld 7819	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
161	160, 3	resubcld 8167	. . . . . 6 $/\$ $/\$ $/\$ $/\$
162		absresq 10882	. . . . . 6
163	161, 162	syl 14	. . . . 5 $/\$ $/\$ $/\$ $/\$
164	163	oveq2d 5798	. . . 4 $/\$ $/\$ $/\$ $/\$
165	153, 159, 164	3brtr4d 3968	. . 3 $/\$ $/\$ $/\$ $/\$
166	11	recnd 7818	. . . 4 $/\$ $/\$ $/\$ $/\$
167	15	recnd 7818	. . . 4 $/\$ $/\$ $/\$ $/\$
168		binom2 10434	. . . 4 $/\$
169	166, 167, 168	syl2anc 409	. . 3 $/\$ $/\$ $/\$ $/\$
170		binom2 10434	. . . 4 $/\$
171	9, 64, 170	syl2anc 409	. . 3 $/\$ $/\$ $/\$ $/\$
172	165, 169, 171	3brtr4d 3968	. 2 $/\$ $/\$ $/\$ $/\$
173	11, 15	readdcld 7819	. . 3 $/\$ $/\$ $/\$ $/\$
174	3, 23	readdcld 7819	. . 3 $/\$ $/\$ $/\$ $/\$
175	10	absge0d 10988	. . . 4 $/\$ $/\$ $/\$ $/\$
176	14	absge0d 10988	. . . 4 $/\$ $/\$ $/\$ $/\$
177	11, 15, 175, 176	addge0d 8308	. . 3 $/\$ $/\$ $/\$ $/\$
178	22	absge0d 10988	. . . 4 $/\$ $/\$ $/\$ $/\$
179	3, 23, 57, 178	addge0d 8308	. . 3 $/\$ $/\$ $/\$ $/\$
180	173, 174, 177, 179	le2sqd 10487	. 2 $/\$ $/\$ $/\$ $/\$
181	172, 180	mpbird 166	1 $/\$ $/\$ $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

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

wceq 1332

wcel 1481 class class class wbr 3937

cfv 5131 (class class class)co 5782

cc 7642

cr 7643

cc0 7644

caddc 7647

cmul 7649

cle 7825

cmin 7957

c2 8795

crp 9470

cexp 10323

cabs 10801

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 604 ax-in2 605 ax-io 699 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-10 1484 ax-11 1485 ax-i12 1486 ax-bndl 1487 ax-4 1488 ax-13 1492 ax-14 1493 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 ax-coll 4051 ax-sep 4054 ax-nul 4062 ax-pow 4106 ax-pr 4139 ax-un 4363 ax-setind 4460 ax-iinf 4510 ax-cnex 7735 ax-resscn 7736 ax-1cn 7737 ax-1re 7738 ax-icn 7739 ax-addcl 7740 ax-addrcl 7741 ax-mulcl 7742 ax-mulrcl 7743 ax-addcom 7744 ax-mulcom 7745 ax-addass 7746 ax-mulass 7747 ax-distr 7748 ax-i2m1 7749 ax-0lt1 7750 ax-1rid 7751 ax-0id 7752 ax-rnegex 7753 ax-precex 7754 ax-cnre 7755 ax-pre-ltirr 7756 ax-pre-ltwlin 7757 ax-pre-lttrn 7758 ax-pre-apti 7759 ax-pre-ltadd 7760 ax-pre-mulgt0 7761 ax-pre-mulext 7762 ax-arch 7763 ax-caucvg 7764

This theorem depends on definitions: df-bi 116 df-dc 821 df-3or 964 df-3an 965 df-tru 1335 df-fal 1338 df-nf 1438 df-sb 1737 df-eu 2003 df-mo 2004 df-clab 2127 df-cleq 2133 df-clel 2136 df-nfc 2271 df-ne 2310 df-nel 2405 df-ral 2422 df-rex 2423 df-reu 2424 df-rmo 2425 df-rab 2426 df-v 2691 df-sbc 2914 df-csb 3008 df-dif 3078 df-un 3080 df-in 3082 df-ss 3089 df-nul 3369 df-if 3480 df-pw 3517 df-sn 3538 df-pr 3539 df-op 3541 df-uni 3745 df-int 3780 df-iun 3823 df-br 3938 df-opab 3998 df-mpt 3999 df-tr 4035 df-id 4223 df-po 4226 df-iso 4227 df-iord 4296 df-on 4298 df-ilim 4299 df-suc 4301 df-iom 4513 df-xp 4553 df-rel 4554 df-cnv 4555 df-co 4556 df-dm 4557 df-rn 4558 df-res 4559 df-ima 4560 df-iota 5096 df-fun 5133 df-fn 5134 df-f 5135 df-f1 5136 df-fo 5137 df-f1o 5138 df-fv 5139 df-riota 5738 df-ov 5785 df-oprab 5786 df-mpo 5787 df-1st 6046 df-2nd 6047 df-recs 6210 df-frec 6296 df-pnf 7826 df-mnf 7827 df-xr 7828 df-ltxr 7829 df-le 7830 df-sub 7959 df-neg 7960 df-reap 8361 df-ap 8368 df-div 8457 df-inn 8745 df-2 8803 df-3 8804 df-4 8805 df-n0 9002 df-z 9079 df-uz 9351 df-rp 9471 df-seqfrec 10250 df-exp 10324 df-cj 10646 df-re 10647 df-im 10648 df-rsqrt 10802 df-abs 10803

This theorem is referenced by: bdtri 11043

W3C validator