bdtrilem - Intuitionistic Logic Explorer

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

Theorem bdtrilem 11180

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

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

**Proof of Theorem bdtrilem**
Step	Hyp	Ref	Expression
1		simp1l 1011	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
2		simp3 989	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
3	2	rpred 9632	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
4	1, 3	resubcld 8279	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
5	4	resqcld 10614	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
6		2re 8927	. . . . . . . . . . . 12
7	6	a1i 9	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
8	1	recnd 7927	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
9	2	rpcnd 9634	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
10	8, 9	subcld 8209	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
11	10	abscld 11123	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
12		simp2l 1013	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
13	12	recnd 7927	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
14	13, 9	subcld 8209	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
15	14	abscld 11123	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
16	11, 15	remulcld 7929	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
17	7, 16	remulcld 7929	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
18	5, 17	readdcld 7928	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
19	1, 12	remulcld 7929	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
20	7, 19	remulcld 7929	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
21	8, 13	addcld 7918	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
22	21, 9	subcld 8209	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
23	22	abscld 11123	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
24	3, 23	remulcld 7929	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
25	7, 24	remulcld 7929	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
26	20, 25	readdcld 7928	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
27	5, 26	readdcld 7928	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
28	12, 3	resubcld 8279	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
29	28	resqcld 10614	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
30	19, 24	readdcld 7928	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
31		0le2 8947	. . . . . . . . . . . . 13
32	31	a1i 9	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
33	8, 9, 13, 9	mulsubd 8315	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
34	19	recnd 7927	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
35	9, 9	mulcld 7919	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
36	8, 9	mulcld 7919	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
37	13, 9	mulcld 7919	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
38	36, 37	addcld 7918	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
39	34, 35, 38	addsubassd 8229	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
40	33, 39	eqtrd 2198	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
41	40	fveq2d 5490	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
42	35, 38	subcld 8209	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
43	34, 42	abstrid 11138	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
44	41, 43	eqbrtrd 4004	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
45		simp1r 1012	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
46		simp2r 1014	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
47	1, 12, 45, 46	mulge0d 8519	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
48	19, 47	absidd 11109	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
49	9, 21	subcld 8209	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
50	49, 9	absmuld 11136	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
51	9, 21, 9	subdird 8313	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
52	8, 13, 9	adddird 7924	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
53	52	oveq2d 5858	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
54	51, 53	eqtrd 2198	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
55	54	fveq2d 5490	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
56	9, 21	abssubd 11135	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
57	2	rpge0d 9636	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
58	3, 57	absidd 11109	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
59	56, 58	oveq12d 5860	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
60	50, 55, 59	3eqtr3d 2206	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
61	48, 60	oveq12d 5860	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
62	44, 61	breqtrd 4008	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
63	10, 14	absmuld 11136	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
64	23	recnd 7927	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
65	64, 9	mulcomd 7920	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
66	65	oveq2d 5858	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
67	62, 63, 66	3brtr3d 4013	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
68	16, 30, 7, 32, 67	lemul2ad 8835	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
69	7	recnd 7927	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
70	9, 64	mulcld 7919	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
71	69, 34, 70	adddid 7923	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
72	68, 71	breqtrd 4008	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
73	17, 26, 5, 72	leadd2dd 8458	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
74	18, 27, 29, 73	leadd1dd 8457	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
75	5	recnd 7927	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
76	26	recnd 7927	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
77	29	recnd 7927	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
78	75, 76, 77	add32d 8066	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
79	74, 78	breqtrd 4008	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
80	75, 77	addcld 7918	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
81	69, 34	mulcld 7919	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
82	69, 70	mulcld 7919	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
83	80, 81, 82	addassd 7921	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
84	79, 83	breqtrrd 4010	. . . . . 6 $/\$ $/\$ $/\$ $/\$
85	8	sqcld 10586	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
86	69, 36	mulcld 7919	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
87	85, 86	subcld 8209	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
88	9	sqcld 10586	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
89	87, 88	addcld 7918	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
90	89, 81	addcld 7918	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
91	13	sqcld 10586	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
92	69, 37	mulcld 7919	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
93	91, 92	subcld 8209	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
94	90, 93	addcld 7918	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
95	93, 88	addcld 7918	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
96	89, 95, 81	add32d 8066	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
97	90, 93, 88	addassd 7921	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
98	96, 97	eqtr4d 2201	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
99	94, 88, 98	comraddd 8055	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
100	81, 93	addcld 7918	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
101	87, 100	addcld 7918	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
102	89, 81, 93	addassd 7921	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
103	87, 88	addcomd 8049	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
104	103	oveq1d 5857	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
105	102, 104	eqtrd 2198	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
106	88, 87, 100	addassd 7921	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
107	105, 106	eqtrd 2198	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
108	88, 101, 107	comraddd 8055	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
109	85, 86, 93	subadd23d 8231	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
110	91, 92, 86	subsub4d 8240	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
111	92, 86	addcomd 8049	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
112	111	oveq2d 5858	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
113	110, 112	eqtrd 2198	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
114	113	oveq2d 5858	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
115	109, 114	eqtrd 2198	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
116	115	oveq2d 5858	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
117	87, 81, 93	add12d 8065	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
118	86, 92	addcld 7918	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
119	91, 118	subcld 8209	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
120	85, 119	addcld 7918	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
121	85, 81	addcld 7918	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
122	121, 91, 118	addsubassd 8229	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
123	85, 81, 119	add32d 8066	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
124	122, 123	eqtrd 2198	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
125	120, 81, 124	comraddd 8055	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
126	116, 117, 125	3eqtr4d 2208	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
127	126	oveq1d 5857	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
128	108, 127	eqtrd 2198	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
129	128	oveq2d 5858	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
130	99, 129	eqtrd 2198	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
131		binom2sub 10568	. . . . . . . . . . 11 $/\$
132	8, 9, 131	syl2anc 409	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
133		binom2sub 10568	. . . . . . . . . . 11 $/\$
134	13, 9, 133	syl2anc 409	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
135	132, 134	oveq12d 5860	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
136	135	oveq1d 5857	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
137		binom2sub 10568	. . . . . . . . . . 11 $/\$
138	21, 9, 137	syl2anc 409	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
139		binom2 10566	. . . . . . . . . . . . 13 $/\$
140	8, 13, 139	syl2anc 409	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
141	52	oveq2d 5858	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
142	69, 36, 37	adddid 7923	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
143	141, 142	eqtrd 2198	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
144	140, 143	oveq12d 5860	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
145	144	oveq1d 5857	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
146	138, 145	eqtrd 2198	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
147	146	oveq2d 5858	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
148	130, 136, 147	3eqtr4d 2208	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
149	148	oveq1d 5857	. . . . . 6 $/\$ $/\$ $/\$ $/\$
150	84, 149	breqtrd 4008	. . . . 5 $/\$ $/\$ $/\$ $/\$
151	22	sqcld 10586	. . . . . 6 $/\$ $/\$ $/\$ $/\$
152	88, 151, 82	add32d 8066	. . . . 5 $/\$ $/\$ $/\$ $/\$
153	150, 152	breqtrd 4008	. . . 4 $/\$ $/\$ $/\$ $/\$
154		absresq 11020	. . . . . . 7
155	4, 154	syl 14	. . . . . 6 $/\$ $/\$ $/\$ $/\$
156	155	oveq1d 5857	. . . . 5 $/\$ $/\$ $/\$ $/\$
157		absresq 11020	. . . . . 6
158	28, 157	syl 14	. . . . 5 $/\$ $/\$ $/\$ $/\$
159	156, 158	oveq12d 5860	. . . 4 $/\$ $/\$ $/\$ $/\$
160	1, 12	readdcld 7928	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
161	160, 3	resubcld 8279	. . . . . 6 $/\$ $/\$ $/\$ $/\$
162		absresq 11020	. . . . . 6
163	161, 162	syl 14	. . . . 5 $/\$ $/\$ $/\$ $/\$
164	163	oveq2d 5858	. . . 4 $/\$ $/\$ $/\$ $/\$
165	153, 159, 164	3brtr4d 4014	. . 3 $/\$ $/\$ $/\$ $/\$
166	11	recnd 7927	. . . 4 $/\$ $/\$ $/\$ $/\$
167	15	recnd 7927	. . . 4 $/\$ $/\$ $/\$ $/\$
168		binom2 10566	. . . 4 $/\$
169	166, 167, 168	syl2anc 409	. . 3 $/\$ $/\$ $/\$ $/\$
170		binom2 10566	. . . 4 $/\$
171	9, 64, 170	syl2anc 409	. . 3 $/\$ $/\$ $/\$ $/\$
172	165, 169, 171	3brtr4d 4014	. 2 $/\$ $/\$ $/\$ $/\$
173	11, 15	readdcld 7928	. . 3 $/\$ $/\$ $/\$ $/\$
174	3, 23	readdcld 7928	. . 3 $/\$ $/\$ $/\$ $/\$
175	10	absge0d 11126	. . . 4 $/\$ $/\$ $/\$ $/\$
176	14	absge0d 11126	. . . 4 $/\$ $/\$ $/\$ $/\$
177	11, 15, 175, 176	addge0d 8420	. . 3 $/\$ $/\$ $/\$ $/\$
178	22	absge0d 11126	. . . 4 $/\$ $/\$ $/\$ $/\$
179	3, 23, 57, 178	addge0d 8420	. . 3 $/\$ $/\$ $/\$ $/\$
180	173, 174, 177, 179	le2sqd 10620	. 2 $/\$ $/\$ $/\$ $/\$
181	172, 180	mpbird 166	1 $/\$ $/\$ $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

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

wceq 1343

wcel 2136 class class class wbr 3982

cfv 5188 (class class class)co 5842

cc 7751

cr 7752

cc0 7753

caddc 7756

cmul 7758

cle 7934

cmin 8069

c2 8908

crp 9589

cexp 10454

cabs 10939

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 1435 ax-7 1436 ax-gen 1437 ax-ie1 1481 ax-ie2 1482 ax-8 1492 ax-10 1493 ax-11 1494 ax-i12 1495 ax-bndl 1497 ax-4 1498 ax-17 1514 ax-i9 1518 ax-ial 1522 ax-i5r 1523 ax-13 2138 ax-14 2139 ax-ext 2147 ax-coll 4097 ax-sep 4100 ax-nul 4108 ax-pow 4153 ax-pr 4187 ax-un 4411 ax-setind 4514 ax-iinf 4565 ax-cnex 7844 ax-resscn 7845 ax-1cn 7846 ax-1re 7847 ax-icn 7848 ax-addcl 7849 ax-addrcl 7850 ax-mulcl 7851 ax-mulrcl 7852 ax-addcom 7853 ax-mulcom 7854 ax-addass 7855 ax-mulass 7856 ax-distr 7857 ax-i2m1 7858 ax-0lt1 7859 ax-1rid 7860 ax-0id 7861 ax-rnegex 7862 ax-precex 7863 ax-cnre 7864 ax-pre-ltirr 7865 ax-pre-ltwlin 7866 ax-pre-lttrn 7867 ax-pre-apti 7868 ax-pre-ltadd 7869 ax-pre-mulgt0 7870 ax-pre-mulext 7871 ax-arch 7872 ax-caucvg 7873

This theorem depends on definitions: df-bi 116 df-dc 825 df-3or 969 df-3an 970 df-tru 1346 df-fal 1349 df-nf 1449 df-sb 1751 df-eu 2017 df-mo 2018 df-clab 2152 df-cleq 2158 df-clel 2161 df-nfc 2297 df-ne 2337 df-nel 2432 df-ral 2449 df-rex 2450 df-reu 2451 df-rmo 2452 df-rab 2453 df-v 2728 df-sbc 2952 df-csb 3046 df-dif 3118 df-un 3120 df-in 3122 df-ss 3129 df-nul 3410 df-if 3521 df-pw 3561 df-sn 3582 df-pr 3583 df-op 3585 df-uni 3790 df-int 3825 df-iun 3868 df-br 3983 df-opab 4044 df-mpt 4045 df-tr 4081 df-id 4271 df-po 4274 df-iso 4275 df-iord 4344 df-on 4346 df-ilim 4347 df-suc 4349 df-iom 4568 df-xp 4610 df-rel 4611 df-cnv 4612 df-co 4613 df-dm 4614 df-rn 4615 df-res 4616 df-ima 4617 df-iota 5153 df-fun 5190 df-fn 5191 df-f 5192 df-f1 5193 df-fo 5194 df-f1o 5195 df-fv 5196 df-riota 5798 df-ov 5845 df-oprab 5846 df-mpo 5847 df-1st 6108 df-2nd 6109 df-recs 6273 df-frec 6359 df-pnf 7935 df-mnf 7936 df-xr 7937 df-ltxr 7938 df-le 7939 df-sub 8071 df-neg 8072 df-reap 8473 df-ap 8480 df-div 8569 df-inn 8858 df-2 8916 df-3 8917 df-4 8918 df-n0 9115 df-z 9192 df-uz 9467 df-rp 9590 df-seqfrec 10381 df-exp 10455 df-cj 10784 df-re 10785 df-im 10786 df-rsqrt 10940 df-abs 10941

This theorem is referenced by: bdtri 11181

W3C validator