Theorem pilem1 8938

Description: Lemma for pire 8944, pigt2lt4 8942 and sinpi 8943.

Hypotheses

Ref	Expression
pilem1.1	|- S = {x e. (-u4[,)0) | (sin` x) = 0}
pilem1.2	|- C = sup(S, RR, < )
pilem1.3	|- T = {x e. (-u4[,]-u2) | (sin` x) = 0}

Assertion

Ref	Expression
pilem1	|- (C e. (-u4(,)-u2) /\ (sin` C) = 0)

Distinct variable group:   x,C

Proof of Theorem pilem1

Step	Hyp	Ref	Expression
1		4re 6128	. . 3 |- 4 e. RR
2	1	renegcli 5570	. 2 |- -u4 e. RR
3		2re 6125	. . 3 |- 2 e. RR
4	3	renegcli 5570	. 2 |- -u2 e. RR
5		0re 5594	. 2 |- 0 e. RR
6		2pos 6135	. . . . 5 |- 0 < 2
7	5, 3, 3	ltadd1i 5745	. . . . 5 |- (0 < 2 <-> (0 + 2) < (2 + 2))
8	6, 7	mpbi 187	. . . 4 |- (0 + 2) < (2 + 2)
9		2cn 6126	. . . . 5 |- 2 e. CC
10	9	addid2i 5485	. . . 4 |- (0 + 2) = 2
11		2p2e4 6147	. . . 4 |- (2 + 2) = 4
12	8, 10, 11	3brtr3i 2715	. . 3 |- 2 < 4
13	3, 1	ltnegi 5757	. . 3 |- (2 < 4 <-> -u4 < -u2)
14	12, 13	mpbi 187	. 2 |- -u4 < -u2
15		iccssre 6523	. . . 4 |- ((-u4 e. RR /\ -u2 e. RR) -> (-u4[,]-u2) (_ RR)
16	2, 4, 15	mp2an 701	. . 3 |- (-u4[,]-u2) (_ RR
17		axresscn 5422	. . 3 |- RR (_ CC
18	16, 17	sstri 2125	. 2 |- (-u4[,]-u2) (_ CC
19		ssid 2132	. 2 |- CC (_ CC
20		sincn 8936	. 2 |- sin e. (CC-cn->CC)
21	16	sseli 2117	. . 3 |- (x e. (-u4[,]-u2) -> x e. RR)
22		resincl 7646	. . 3 |- (x e. RR -> (sin` x) e. RR)
23	21, 22	syl 10	. 2 |- (x e. (-u4[,]-u2) -> (sin` x) e. RR)
24		letric 5774	. . . . . . . . . . . . . 14 |- ((y e. RR /\ -u2 e. RR) -> (y <_ -u2 \/ -u2 <_ y))
25	4, 24	mpan2 700	. . . . . . . . . . . . 13 |- (y e. RR -> (y <_ -u2 \/ -u2 <_ y))
26	25	biantrurd 732	. . . . . . . . . . . 12 |- (y e. RR -> (y < 0 <-> ((y <_ -u2 \/ -u2 <_ y) /\ y < 0)))
27		andir 608	. . . . . . . . . . . 12 |- (((y <_ -u2 \/ -u2 <_ y) /\ y < 0) <-> ((y <_ -u2 /\ y < 0) \/ (-u2 <_ y /\ y < 0)))
28	26, 27	syl6bb 539	. . . . . . . . . . 11 |- (y e. RR -> (y < 0 <-> ((y <_ -u2 /\ y < 0) \/ (-u2 <_ y /\ y < 0))))
29		lt0neg2 5823	. . . . . . . . . . . . . . . 16 |- (2 e. RR -> (0 < 2 <-> -u2 < 0))
30	3, 29	ax-mp 7	. . . . . . . . . . . . . . 15 |- (0 < 2 <-> -u2 < 0)
31	6, 30	mpbi 187	. . . . . . . . . . . . . 14 |- -u2 < 0
32		lelttr 5677	. . . . . . . . . . . . . . 15 |- ((y e. RR /\ -u2 e. RR /\ 0 e. RR) -> ((y <_ -u2 /\ -u2 < 0) -> y < 0))
33	4, 5, 32	mp3an23 914	. . . . . . . . . . . . . 14 |- (y e. RR -> ((y <_ -u2 /\ -u2 < 0) -> y < 0))
34	31, 33	mpan2i 703	. . . . . . . . . . . . 13 |- (y e. RR -> (y <_ -u2 -> y < 0))
35		pm4.71 638	. . . . . . . . . . . . 13 |- ((y <_ -u2 -> y < 0) <-> (y <_ -u2 <-> (y <_ -u2 /\ y < 0)))
36	34, 35	sylib 196	. . . . . . . . . . . 12 |- (y e. RR -> (y <_ -u2 <-> (y <_ -u2 /\ y < 0)))
37	36	orbi1d 618	. . . . . . . . . . 11 |- (y e. RR -> ((y <_ -u2 \/ (-u2 <_ y /\ y < 0)) <-> ((y <_ -u2 /\ y < 0) \/ (-u2 <_ y /\ y < 0))))
38	28, 37	bitr4d 534	. . . . . . . . . 10 |- (y e. RR -> (y < 0 <-> (y <_ -u2 \/ (-u2 <_ y /\ y < 0))))
39	38	anbi1d 620	. . . . . . . . 9 |- (y e. RR -> ((y < 0 /\ (sin` y) = 0) <-> ((y <_ -u2 \/ (-u2 <_ y /\ y < 0)) /\ (sin` y) = 0)))
40		andir 608	. . . . . . . . 9 |- (((y <_ -u2 \/ (-u2 <_ y /\ y < 0)) /\ (sin` y) = 0) <-> ((y <_ -u2 /\ (sin` y) = 0) \/ ((-u2 <_ y /\ y < 0) /\ (sin` y) = 0)))
41	39, 40	syl6bb 539	. . . . . . . 8 |- (y e. RR -> ((y < 0 /\ (sin` y) = 0) <-> ((y <_ -u2 /\ (sin` y) = 0) \/ ((-u2 <_ y /\ y < 0) /\ (sin` y) = 0))))
42		renegcl 5591	. . . . . . . . . . . . . . 15 |- (y e. RR -> -uy e. RR)
43	42	3ad2ant1 806	. . . . . . . . . . . . . 14 |- ((y e. RR /\ -u2 <_ y /\ y < 0) -> -uy e. RR)
44		lt0neg1 5822	. . . . . . . . . . . . . . . 16 |- (y e. RR -> (y < 0 <-> 0 < -uy))
45	44	adantr 389	. . . . . . . . . . . . . . 15 |- ((y e. RR /\ -u2 <_ y) -> (y < 0 <-> 0 < -uy))
46	45	biimp3a 925	. . . . . . . . . . . . . 14 |- ((y e. RR /\ -u2 <_ y /\ y < 0) -> 0 < -uy)
47		lenegcon1 5812	. . . . . . . . . . . . . . . . 17 |- ((2 e. RR /\ y e. RR) -> (-u2 <_ y <-> -uy <_ 2))
48	3, 47	mpan 699	. . . . . . . . . . . . . . . 16 |- (y e. RR -> (-u2 <_ y <-> -uy <_ 2))
49	48	biimpa 416	. . . . . . . . . . . . . . 15 |- ((y e. RR /\ -u2 <_ y) -> -uy <_ 2)
50	49	3adant3 805	. . . . . . . . . . . . . 14 |- ((y e. RR /\ -u2 <_ y /\ y < 0) -> -uy <_ 2)
51	43, 46, 50	3jca 825	. . . . . . . . . . . . 13 |- ((y e. RR /\ -u2 <_ y /\ y < 0) -> (-uy e. RR /\ 0 < -uy /\ -uy <_ 2))
52		elioc2 6516	. . . . . . . . . . . . . . 15 |- ((0 e. RR /\ 2 e. RR) -> (-uy e. (0(,]2) <-> (-uy e. RR /\ 0 < -uy /\ -uy <_ 2)))
53	5, 3, 52	mp2an 701	. . . . . . . . . . . . . 14 |- (-uy e. (0(,]2) <-> (-uy e. RR /\ 0 < -uy /\ -uy <_ 2))
54	53	biimpri 150	. . . . . . . . . . . . 13 |- ((-uy e. RR /\ 0 < -uy /\ -uy <_ 2) -> -uy e. (0(,]2))
55		sin02gt0 7687	. . . . . . . . . . . . 13 |- (-uy e. (0(,]2) -> 0 < (sin` -uy))
56	51, 54, 55	3syl 20	. . . . . . . . . . . 12 |- ((y e. RR /\ -u2 <_ y /\ y < 0) -> 0 < (sin` -uy))
57		recn 5467	. . . . . . . . . . . . . . . . . 18 |- (y e. RR -> y e. CC)
58		sinneg 7650	. . . . . . . . . . . . . . . . . 18 |- (y e. CC -> (sin` -uy) = -u(sin` y))
59	57, 58	syl 10	. . . . . . . . . . . . . . . . 17 |- (y e. RR -> (sin` -uy) = -u(sin` y))
60	59	breq2d 2703	. . . . . . . . . . . . . . . 16 |- (y e. RR -> (0 < (sin` -uy) <-> 0 < -u(sin` y)))
61		resincl 7646	. . . . . . . . . . . . . . . . 17 |- (y e. RR -> (sin` y) e. RR)
62		lt0neg1 5822	. . . . . . . . . . . . . . . . 17 |- ((sin` y) e. RR -> ((sin` y) < 0 <-> 0 < -u(sin` y)))
63	61, 62	syl 10	. . . . . . . . . . . . . . . 16 |- (y e. RR -> ((sin` y) < 0 <-> 0 < -u(sin` y)))
64	60, 63	bitr4d 534	. . . . . . . . . . . . . . 15 |- (y e. RR -> (0 < (sin` -uy) <-> (sin` y) < 0))
65		ltne 5670	. . . . . . . . . . . . . . . . . 18 |- (((sin` y) e. RR /\ 0 e. RR /\ (sin` y) < 0) -> 0 =/= (sin` y))
66	5, 65	mp3an2 910	. . . . . . . . . . . . . . . . 17 |- (((sin` y) e. RR /\ (sin` y) < 0) -> 0 =/= (sin` y))
67	66	ex 371	. . . . . . . . . . . . . . . 16 |- ((sin` y) e. RR -> ((sin` y) < 0 -> 0 =/= (sin` y)))
68	61, 67	syl 10	. . . . . . . . . . . . . . 15 |- (y e. RR -> ((sin` y) < 0 -> 0 =/= (sin` y)))
69	64, 68	sylbid 201	. . . . . . . . . . . . . 14 |- (y e. RR -> (0 < (sin` -uy) -> 0 =/= (sin` y)))
70		necom 1682	. . . . . . . . . . . . . . 15 |- (0 =/= (sin` y) <-> (sin` y) =/= 0)
71		df-ne 1630	. . . . . . . . . . . . . . 15 |- ((sin` y) =/= 0 <-> -. (sin` y) = 0)
72	70, 71	bitri 171	. . . . . . . . . . . . . 14 |- (0 =/= (sin` y) <-> -. (sin` y) = 0)
73	69, 72	syl6ib 210	. . . . . . . . . . . . 13 |- (y e. RR -> (0 < (sin` -uy) -> -. (sin` y) = 0))
74	73	3ad2ant1 806	. . . . . . . . . . . 12 |- ((y e. RR /\ -u2 <_ y /\ y < 0) -> (0 < (sin` -uy) -> -. (sin` y) = 0))
75	56, 74	mpd 26	. . . . . . . . . . 11 |- ((y e. RR /\ -u2 <_ y /\ y < 0) -> -. (sin` y) = 0)
76	75	3expib 842	. . . . . . . . . 10 |- (y e. RR -> ((-u2 <_ y /\ y < 0) -> -. (sin` y) = 0))
77		imnan 240	. . . . . . . . . 10 |- (((-u2 <_ y /\ y < 0) -> -. (sin` y) = 0) <-> -. ((-u2 <_ y /\ y < 0) /\ (sin` y) = 0))
78	76, 77	sylib 196	. . . . . . . . 9 |- (y e. RR -> -. ((-u2 <_ y /\ y < 0) /\ (sin` y) = 0))
79		biorf 740	. . . . . . . . . 10 |- (-. ((-u2 <_ y /\ y < 0) /\ (sin` y) = 0) -> ((y <_ -u2 /\ (sin` y) = 0) <-> (((-u2 <_ y /\ y < 0) /\ (sin` y) = 0) \/ (y <_ -u2 /\ (sin` y) = 0))))
80		orcom 244	. . . . . . . . . 10 |- ((((-u2 <_ y /\ y < 0) /\ (sin` y) = 0) \/ (y <_ -u2 /\ (sin` y) = 0)) <-> ((y <_ -u2 /\ (sin` y) = 0) \/ ((-u2 <_ y /\ y < 0) /\ (sin` y) = 0)))
81	79, 80	syl6bb 539	. . . . . . . . 9 |- (-. ((-u2 <_ y /\ y < 0) /\ (sin` y) = 0) -> ((y <_ -u2 /\ (sin` y) = 0) <-> ((y <_ -u2 /\ (sin` y) = 0) \/ ((-u2 <_ y /\ y < 0) /\ (sin` y) = 0))))
82	78, 81	syl 10	. . . . . . . 8 |- (y e. RR -> ((y <_ -u2 /\ (sin` y) = 0) <-> ((y <_ -u2 /\ (sin` y) = 0) \/ ((-u2 <_ y /\ y < 0) /\ (sin` y) = 0))))
83	41, 82	bitr4d 534	. . . . . . 7 |- (y e. RR -> ((y < 0 /\ (sin` y) = 0) <-> (y <_ -u2 /\ (sin` y) = 0)))
84	83	pm5.32i 648	. . . . . 6 |- ((y e. RR /\ (y < 0 /\ (sin` y) = 0)) <-> (y e. RR /\ (y <_ -u2 /\ (sin` y) = 0)))
85	84	anbi2i 483	. . . . 5 |- ((-u4 <_ y /\ (y e. RR /\ (y < 0 /\ (sin` y) = 0))) <-> (-u4 <_ y /\ (y e. RR /\ (y <_ -u2 /\ (sin` y) = 0))))
86		fveq2 3835	. . . . . . . 8 |- (x = y -> (sin` x) = (sin` y))
87	86	eqeq1d 1526	. . . . . . 7 |- (x = y -> ((sin` x) = 0 <-> (sin` y) = 0))
88		pilem1.1	. . . . . . 7 |- S = {x e. (-u4[,)0) | (sin` x) = 0}
89	87, 88	elrab2 1953	. . . . . 6 |- (y e. S <-> (y e. (-u4[,)0) /\ (sin` y) = 0))
90		elico2 6517	. . . . . . . . . 10 |- ((-u4 e. RR /\ 0 e. RR) -> (y e. (-u4[,)0) <-> (y e. RR /\ -u4 <_ y /\ y < 0)))
91	2, 5, 90	mp2an 701	. . . . . . . . 9 |- (y e. (-u4[,)0) <-> (y e. RR /\ -u4 <_ y /\ y < 0))
92		3ancoma 788	. . . . . . . . 9 |- ((y e. RR /\ -u4 <_ y /\ y < 0) <-> (-u4 <_ y /\ y e. RR /\ y < 0))
93		3anass 785	. . . . . . . . 9 |- ((-u4 <_ y /\ y e. RR /\ y < 0) <-> (-u4 <_ y /\ (y e. RR /\ y < 0)))
94	91, 92, 93	3bitri 175	. . . . . . . 8 |- (y e. (-u4[,)0) <-> (-u4 <_ y /\ (y e. RR /\ y < 0)))
95	94	anbi1i 484	. . . . . . 7 |- ((y e. (-u4[,)0) /\ (sin` y) = 0) <-> ((-u4 <_ y /\ (y e. RR /\ y < 0)) /\ (sin` y) = 0))
96		anass 441	. . . . . . 7 |- (((-u4 <_ y /\ (y e. RR /\ y < 0)) /\ (sin` y) = 0) <-> (-u4 <_ y /\ ((y e. RR /\ y < 0) /\ (sin` y) = 0)))
97		anass 441	. . . . . . . 8 |- (((y e. RR /\ y < 0) /\ (sin` y) = 0) <-> (y e. RR /\ (y < 0 /\ (sin` y) = 0)))
98	97	anbi2i 483	. . . . . . 7 |- ((-u4 <_ y /\ ((y e. RR /\ y < 0) /\ (sin` y) = 0)) <-> (-u4 <_ y /\ (y e. RR /\ (y < 0 /\ (sin` y) = 0))))
99	95, 96, 98	3bitri 175	. . . . . 6 |- ((y e. (-u4[,)0) /\ (sin` y) = 0) <-> (-u4 <_ y /\ (y e. RR /\ (y < 0 /\ (sin` y) = 0))))
100	89, 99	bitri 171	. . . . 5 |- (y e. S <-> (-u4 <_ y /\ (y e. RR /\ (y < 0 /\ (sin` y) = 0))))
101		pilem1.3	. . . . . . 7 |- T = {x e. (-u4[,]-u2) | (sin` x) = 0}
102	87, 101	elrab2 1953	. . . . . 6 |- (y e. T <-> (y e. (-u4[,]-u2) /\ (sin` y) = 0))
103		elicc2 6518	. . . . . . . . . 10 |- ((-u4 e. RR /\ -u2 e. RR) -> (y e. (-u4[,]-u2) <-> (y e. RR /\ -u4 <_ y /\ y <_ -u2)))
104	2, 4, 103	mp2an 701	. . . . . . . . 9 |- (y e. (-u4[,]-u2) <-> (y e. RR /\ -u4 <_ y /\ y <_ -u2))
105		3ancoma 788	. . . . . . . . 9 |- ((y e. RR /\ -u4 <_ y /\ y <_ -u2) <-> (-u4 <_ y /\ y e. RR /\ y <_ -u2))
106		3anass 785	. . . . . . . . 9 |- ((-u4 <_ y /\ y e. RR /\ y <_ -u2) <-> (-u4 <_ y /\ (y e. RR /\ y <_ -u2)))
107	104, 105, 106	3bitri 175	. . . . . . . 8 |- (y e. (-u4[,]-u2) <-> (-u4 <_ y /\ (y e. RR /\ y <_ -u2)))
108	107	anbi1i 484	. . . . . . 7 |- ((y e. (-u4[,]-u2) /\ (sin` y) = 0) <-> ((-u4 <_ y /\ (y e. RR /\ y <_ -u2)) /\ (sin` y) = 0))
109		anass 441	. . . . . . 7 |- (((-u4 <_ y /\ (y e. RR /\ y <_ -u2)) /\ (sin` y) = 0) <-> (-u4 <_ y /\ ((y e. RR /\ y <_ -u2) /\ (sin` y) = 0)))
110		anass 441	. . . . . . . 8 |- (((y e. RR /\ y <_ -u2) /\ (sin` y) = 0) <-> (y e. RR /\ (y <_ -u2 /\ (sin` y) = 0)))
111	110	anbi2i 483	. . . . . . 7 |- ((-u4 <_ y /\ ((y e. RR /\ y <_ -u2) /\ (sin` y) = 0)) <-> (-u4 <_ y /\ (y e. RR /\ (y <_ -u2 /\ (sin` y) = 0))))
112	108, 109, 111	3bitri 175	. . . . . 6 |- ((y e. (-u4[,]-u2) /\ (sin` y) = 0) <-> (-u4 <_ y /\ (y e. RR /\ (y <_ -u2 /\ (sin` y) = 0))))
113	102, 112	bitri 171	. . . . 5 |- (y e. T <-> (-u4 <_ y /\ (y e. RR /\ (y <_ -u2 /\ (sin` y) = 0))))
114	85, 100, 113	3bitr4i 181	. . . 4 |- (y e. S <-> y e. T)
115	114	eqriv 1515	. . 3 |- S = T
116	115, 101	eqtri 1538	. 2 |- S = {x e. (-u4[,]-u2) | (sin` x) = 0}
117		sinneg 7650	. . . . 5 |- (2 e. CC -> (sin` -u2) = -u(sin` 2))
118	9, 117	ax-mp 7	. . . 4 |- (sin` -u2) = -u(sin` 2)
119		sincos2sgn 7689	. . . . . 6 |- (0 < (sin` 2) /\ (cos` 2) < 0)
120	119	pm3.26i 318	. . . . 5 |- 0 < (sin` 2)
121		resincl 7646	. . . . . . 7 |- (2 e. RR -> (sin` 2) e. RR)
122	3, 121	ax-mp 7	. . . . . 6 |- (sin` 2) e. RR
123		lt0neg2 5823	. . . . . 6 |- ((sin` 2) e. RR -> (0 < (sin` 2) <-> -u(sin` 2) < 0))
124	122, 123	ax-mp 7	. . . . 5 |- (0 < (sin` 2) <-> -u(sin` 2) < 0)
125	120, 124	mpbi 187	. . . 4 |- -u(sin` 2) < 0
126	118, 125	eqbrtri 2707	. . 3 |- (sin` -u2) < 0
127		sin4lt0 7690	. . . . 5 |- (sin` 4) < 0
128		resincl 7646	. . . . . . 7 |- (4 e. RR -> (sin` 4) e. RR)
129	1, 128	ax-mp 7	. . . . . 6 |- (sin` 4) e. RR
130		lt0neg1 5822	. . . . . 6 |- ((sin` 4) e. RR -> ((sin` 4) < 0 <-> 0 < -u(sin` 4)))
131	129, 130	ax-mp 7	. . . . 5 |- ((sin` 4) < 0 <-> 0 < -u(sin` 4))
132	127, 131	mpbi 187	. . . 4 |- 0 < -u(sin` 4)
133	1	recni 5468	. . . . 5 |- 4 e. CC
134		sinneg 7650	. . . . 5 |- (4 e. CC -> (sin` -u4) = -u(sin` 4))
135	133, 134	ax-mp 7	. . . 4 |- (sin` -u4) = -u(sin` 4)
136	132, 135	breqtrri 2713	. . 3 |- 0 < (sin` -u4)
137	126, 136	pm3.2i 283	. 2 |- ((sin` -u2) < 0 /\ 0 < (sin` -u4))
138		pilem1.2	. 2 |- C = sup(S, RR, < )
139	2, 4, 5, 14, 18, 19, 20, 23, 116, 137, 138	dsupivthi 7497	1 |- (C e. (-u4(,)-u2) /\ (sin` C) = 0)

Syntax hints:  -. wn 2   -> wi 3   <-> wb 144   \/ wo 220   /\ wa 221   /\ w3a 781   = wceq 992   e. wcel 994   =/= wne 1628  {crab 1694   (_ wss 2099   class class class wbr 2692  ` cfv 3263  (class class class)co 4021  supcsup 4716  CCcc 5386  RRcr 5387  0cc0 5388   + caddc 5391  -ucneg 5447   <_ cle 5449   < clt 5640  2c2 6107  4c4 6109  (,)cioo 6483  (,]cioc 6484  [,)cico 6485  [,]cicc 6486  sincsin 7500  cosccos 7501

This theorem is referenced by:  pilem2 8939  pilem3 8940

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-9 1001  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-rep 2767  ax-sep 2777  ax-nul 2784  ax-pow 2818  ax-pr 2855  ax-un 3089  ax-reg 4736  ax-inf2 4770  ax-ac 4890

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-3or 782  df-3an 783  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-nel 1631  df-ral 1695  df-rex 1696  df-reu 1697  df-rab 1698  df-v 1858  df-sbc 1987  df-csb 2052  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-pss 2107  df-nul 2333  df-if 2416  df-pw 2459  df-sn 2470  df-pr 2471  df-tp 2473  df-op 2474  df-uni 2570  df-int 2601  df-iun 2635  df-iin 2636  df-br 2693  df-opab 2741  df-tr 2755  df-eprel 2910  df-id 2913  df-po 2918  df-so 2929  df-fr 2947  df-we 2962  df-ord 2978  df-on 2979  df-lim 2980  df-suc 2981  df-om 3219  df-xp 3265  df-rel 3266  df-cnv 3267  df-co 3268  df-dm 3269  df-rn 3270  df-res 3271  df-ima 3272  df-fun 3273  df-fn 3274  df-f 3275  df-f1 3276  df-fo 3277  df-f1o 3278  df-fv 3279  df-opr 4023  df-oprab 4024  df-1st 4140  df-2nd 4141  df-rdg 4233  df-1o 4269  df-oadd 4271  df-omul 4272  df-er 4401  df-ec 4403  df-qs 4406  df-map 4465  df-en 4509  df-dom 4510  df-sdom 4511  df-sup 4717  df-r1 4789  df-rank 4790  df-ni 5154  df-pli 5155  df-mi 5156  df-lti 5157  df-plpq 5189  df-mpq 5190  df-enq 5191  df-nq 5192  df-plq 5193  df-mq 5194  df-rq 5195  df-ltq 5196  df-1q 5197  df-np 5240  df-1p 5241  df-plp 5242  df-mp 5243  df-ltp 5244  df-plpr 5318  df-mpr 5319  df-enr 5320  df-nr 5321  df-plr 5322  df-mr 5323  df-ltr 5324  df-0r 5325  df-1r 5326  df-m1r 5327  df-c 5394  df-0 5395  df-1 5396  df-i 5397  df-r 5398  df-plus 5399  df-mul 5400  df-lt 5401  df-sub 5510  df-neg 5512  df-pnf 5641  df-mnf 5642  df-xr 5643  df-ltxr 5644  df-le 5645  df-div 5855  df-n 6070  df-2 6116  df-3 6117  df-4 6118  df-5 6119  df-6 6120  df-7 6121  df-8 6122  df-9 6123  df-rp 6191  df-n0 6268  df-z 6304  df-q 6395  df-fl 6422  df-ioo 6487  df-ioc 6488  df-ico 6489  df-icc 6490  df-uz 6545  df-fz 6596  df-seq1 6673  df-shft 6706  df-seqz 6728  df-seq0 6729  df-exp 6764  df-sqr 6871  df-re 6952  df-im 6953  df-cj 6954  df-abs 6955  df-fac 7135  df-bc 7160  df-clim 7178  df-sum 7183  df-cncf 7468  df-ef 7503  df-sin 7505  df-cos 7506  df-top 7804  df-cn 7964  df-cnp 7965  df-met 8003  df-bl 8005  df-opn 8006  df-lm 8133

Copyright terms: Public domain