Theorem sineq0OLD 10066

Description: A real number whose sine is zero is an integer multiple of pi.

Assertion

Ref	Expression
sineq0OLD	|- ((A e. RR /\ (sin` A) = 0) -> A = ((|_` (A / pi)) x. pi))

Proof of Theorem sineq0OLD

Step	Hyp	Ref	Expression
1		recn 6466	. . . . . 6 |- (A e. RR -> A e. CC)
2		pire 10026	. . . . . . . 8 |- pi e. RR
3	2	recni 6467	. . . . . . 7 |- pi e. CC
4		pipos 10027	. . . . . . . 8 |- 0 < pi
5	2, 4	gt0ne0ii 6799	. . . . . . 7 |- pi =/= 0
6		divcan1 6909	. . . . . . 7 |- ((A e. CC /\ pi e. CC /\ pi =/= 0) -> ((A / pi) x. pi) = A)
7	3, 5, 6	mp3an23 1183	. . . . . 6 |- (A e. CC -> ((A / pi) x. pi) = A)
8	1, 7	syl 12	. . . . 5 |- (A e. RR -> ((A / pi) x. pi) = A)
9		redivcl 6978	. . . . . . . . 9 |- ((A e. RR /\ pi e. RR /\ pi =/= 0) -> (A / pi) e. RR)
10	2, 5, 9	mp3an23 1183	. . . . . . . 8 |- (A e. RR -> (A / pi) e. RR)
11		eqid 1884	. . . . . . . . . 10 |- (|_` (A / pi)) = (|_` (A / pi))
12		eqid 1884	. . . . . . . . . 10 |- ((A / pi) - (|_` (A / pi))) = ((A / pi) - (|_` (A / pi)))
13	11, 12	intfrac2 7495	. . . . . . . . 9 |- ((A / pi) e. RR -> (0 <_ ((A / pi) - (|_` (A / pi))) /\ ((A / pi) - (|_` (A / pi))) < 1 /\ (A / pi) = ((|_` (A / pi)) + ((A / pi) - (|_` (A / pi))))))
14	13	simp3d 890	. . . . . . . 8 |- ((A / pi) e. RR -> (A / pi) = ((|_` (A / pi)) + ((A / pi) - (|_` (A / pi)))))
15	10, 14	syl 12	. . . . . . 7 |- (A e. RR -> (A / pi) = ((|_` (A / pi)) + ((A / pi) - (|_` (A / pi)))))
16	15	opreq1d 4897	. . . . . 6 |- (A e. RR -> ((A / pi) x. pi) = (((|_` (A / pi)) + ((A / pi) - (|_` (A / pi)))) x. pi))
17		reflcl 7466	. . . . . . . . 9 |- ((A / pi) e. RR -> (|_` (A / pi)) e. RR)
18	10, 17	syl 12	. . . . . . . 8 |- (A e. RR -> (|_` (A / pi)) e. RR)
19	18	recnd 6468	. . . . . . 7 |- (A e. RR -> (|_` (A / pi)) e. CC)
20		resubcl 6601	. . . . . . . . 9 |- (((A / pi) e. RR /\ (|_` (A / pi)) e. RR) -> ((A / pi) - (|_` (A / pi))) e. RR)
21	10, 18, 20	syl11anc 524	. . . . . . . 8 |- (A e. RR -> ((A / pi) - (|_` (A / pi))) e. RR)
22	21	recnd 6468	. . . . . . 7 |- (A e. RR -> ((A / pi) - (|_` (A / pi))) e. CC)
23		adddir 6472	. . . . . . . 8 |- (((|_` (A / pi)) e. CC /\ ((A / pi) - (|_` (A / pi))) e. CC /\ pi e. CC) -> (((|_` (A / pi)) + ((A / pi) - (|_` (A / pi)))) x. pi) = (((|_` (A / pi)) x. pi) + (((A / pi) - (|_` (A / pi))) x. pi)))
24	3, 23	mp3an3 1180	. . . . . . 7 |- (((|_` (A / pi)) e. CC /\ ((A / pi) - (|_` (A / pi))) e. CC) -> (((|_` (A / pi)) + ((A / pi) - (|_` (A / pi)))) x. pi) = (((|_` (A / pi)) x. pi) + (((A / pi) - (|_` (A / pi))) x. pi)))
25	19, 22, 24	syl11anc 524	. . . . . 6 |- (A e. RR -> (((|_` (A / pi)) + ((A / pi) - (|_` (A / pi)))) x. pi) = (((|_` (A / pi)) x. pi) + (((A / pi) - (|_` (A / pi))) x. pi)))
26	16, 25	eqtrd 1925	. . . . 5 |- (A e. RR -> ((A / pi) x. pi) = (((|_` (A / pi)) x. pi) + (((A / pi) - (|_` (A / pi))) x. pi)))
27	8, 26	eqtr3d 1927	. . . 4 |- (A e. RR -> A = (((|_` (A / pi)) x. pi) + (((A / pi) - (|_` (A / pi))) x. pi)))
28	27	adantr 425	. . 3 |- ((A e. RR /\ (sin` A) = 0) -> A = (((|_` (A / pi)) x. pi) + (((A / pi) - (|_` (A / pi))) x. pi)))
29		remulcl 6457	. . . . . . . . . . . . . . . 16 |- (((|_` (A / pi)) e. RR /\ pi e. RR) -> ((|_` (A / pi)) x. pi) e. RR)
30	2, 29	mpan2 760	. . . . . . . . . . . . . . 15 |- ((|_` (A / pi)) e. RR -> ((|_` (A / pi)) x. pi) e. RR)
31	18, 30	syl 12	. . . . . . . . . . . . . 14 |- (A e. RR -> ((|_` (A / pi)) x. pi) e. RR)
32	31	recnd 6468	. . . . . . . . . . . . 13 |- (A e. RR -> ((|_` (A / pi)) x. pi) e. CC)
33		remulcl 6457	. . . . . . . . . . . . . . . 16 |- ((((A / pi) - (|_` (A / pi))) e. RR /\ pi e. RR) -> (((A / pi) - (|_` (A / pi))) x. pi) e. RR)
34	2, 33	mpan2 760	. . . . . . . . . . . . . . 15 |- (((A / pi) - (|_` (A / pi))) e. RR -> (((A / pi) - (|_` (A / pi))) x. pi) e. RR)
35	21, 34	syl 12	. . . . . . . . . . . . . 14 |- (A e. RR -> (((A / pi) - (|_` (A / pi))) x. pi) e. RR)
36	35	recnd 6468	. . . . . . . . . . . . 13 |- (A e. RR -> (((A / pi) - (|_` (A / pi))) x. pi) e. CC)
37		addcom 6458	. . . . . . . . . . . . 13 |- ((((|_` (A / pi)) x. pi) e. CC /\ (((A / pi) - (|_` (A / pi))) x. pi) e. CC) -> (((|_` (A / pi)) x. pi) + (((A / pi) - (|_` (A / pi))) x. pi)) = ((((A / pi) - (|_` (A / pi))) x. pi) + ((|_` (A / pi)) x. pi)))
38	32, 36, 37	syl11anc 524	. . . . . . . . . . . 12 |- (A e. RR -> (((|_` (A / pi)) x. pi) + (((A / pi) - (|_` (A / pi))) x. pi)) = ((((A / pi) - (|_` (A / pi))) x. pi) + ((|_` (A / pi)) x. pi)))
39	27, 38	eqtrd 1925	. . . . . . . . . . 11 |- (A e. RR -> A = ((((A / pi) - (|_` (A / pi))) x. pi) + ((|_` (A / pi)) x. pi)))
40	39	fveq2d 4685	. . . . . . . . . 10 |- (A e. RR -> (sin` A) = (sin` ((((A / pi) - (|_` (A / pi))) x. pi) + ((|_` (A / pi)) x. pi))))
41	40	fveq2d 4685	. . . . . . . . 9 |- (A e. RR -> (abs` (sin` A)) = (abs` (sin` ((((A / pi) - (|_` (A / pi))) x. pi) + ((|_` (A / pi)) x. pi)))))
42		flcl 7465	. . . . . . . . . . 11 |- ((A / pi) e. RR -> (|_` (A / pi)) e. ZZ)
43	10, 42	syl 12	. . . . . . . . . 10 |- (A e. RR -> (|_` (A / pi)) e. ZZ)
44		abssinper 10062	. . . . . . . . . 10 |- (((((A / pi) - (|_` (A / pi))) x. pi) e. CC /\ (|_` (A / pi)) e. ZZ) -> (abs` (sin` ((((A / pi) - (|_` (A / pi))) x. pi) + ((|_` (A / pi)) x. pi)))) = (abs` (sin` (((A / pi) - (|_` (A / pi))) x. pi))))
45	36, 43, 44	syl11anc 524	. . . . . . . . 9 |- (A e. RR -> (abs` (sin` ((((A / pi) - (|_` (A / pi))) x. pi) + ((|_` (A / pi)) x. pi)))) = (abs` (sin` (((A / pi) - (|_` (A / pi))) x. pi))))
46	41, 45	eqtr2d 1926	. . . . . . . 8 |- (A e. RR -> (abs` (sin` (((A / pi) - (|_` (A / pi))) x. pi))) = (abs` (sin` A)))
47	46	adantr 425	. . . . . . 7 |- ((A e. RR /\ (sin` A) = 0) -> (abs` (sin` (((A / pi) - (|_` (A / pi))) x. pi))) = (abs` (sin` A)))
48		resincl 8703	. . . . . . . . . 10 |- (A e. RR -> (sin` A) e. RR)
49	48	recnd 6468	. . . . . . . . 9 |- (A e. RR -> (sin` A) e. CC)
50		abs00 8104	. . . . . . . . 9 |- ((sin` A) e. CC -> ((abs` (sin` A)) = 0 <-> (sin` A) = 0))
51	49, 50	syl 12	. . . . . . . 8 |- (A e. RR -> ((abs` (sin` A)) = 0 <-> (sin` A) = 0))
52	51	biimpar 461	. . . . . . 7 |- ((A e. RR /\ (sin` A) = 0) -> (abs` (sin` A)) = 0)
53	47, 52	eqtrd 1925	. . . . . 6 |- ((A e. RR /\ (sin` A) = 0) -> (abs` (sin` (((A / pi) - (|_` (A / pi))) x. pi))) = 0)
54		resincl 8703	. . . . . . . . . 10 |- ((((A / pi) - (|_` (A / pi))) x. pi) e. RR -> (sin` (((A / pi) - (|_` (A / pi))) x. pi)) e. RR)
55	35, 54	syl 12	. . . . . . . . 9 |- (A e. RR -> (sin` (((A / pi) - (|_` (A / pi))) x. pi)) e. RR)
56	55	recnd 6468	. . . . . . . 8 |- (A e. RR -> (sin` (((A / pi) - (|_` (A / pi))) x. pi)) e. CC)
57		abs00 8104	. . . . . . . 8 |- ((sin` (((A / pi) - (|_` (A / pi))) x. pi)) e. CC -> ((abs` (sin` (((A / pi) - (|_` (A / pi))) x. pi))) = 0 <-> (sin` (((A / pi) - (|_` (A / pi))) x. pi)) = 0))
58	56, 57	syl 12	. . . . . . 7 |- (A e. RR -> ((abs` (sin` (((A / pi) - (|_` (A / pi))) x. pi))) = 0 <-> (sin` (((A / pi) - (|_` (A / pi))) x. pi)) = 0))
59	58	adantr 425	. . . . . 6 |- ((A e. RR /\ (sin` A) = 0) -> ((abs` (sin` (((A / pi) - (|_` (A / pi))) x. pi))) = 0 <-> (sin` (((A / pi) - (|_` (A / pi))) x. pi)) = 0))
60	53, 59	mpbid 212	. . . . 5 |- ((A e. RR /\ (sin` A) = 0) -> (sin` (((A / pi) - (|_` (A / pi))) x. pi)) = 0)
61	55	adantr 425	. . . . . . . . 9 |- ((A e. RR /\ (((A / pi) - (|_` (A / pi))) x. pi) =/= 0) -> (sin` (((A / pi) - (|_` (A / pi))) x. pi)) e. RR)
62		rexr 6668	. . . . . . . . . . . . . 14 |- ((((A / pi) - (|_` (A / pi))) x. pi) e. RR -> (((A / pi) - (|_` (A / pi))) x. pi) e. RR*)
63	35, 62	syl 12	. . . . . . . . . . . . 13 |- (A e. RR -> (((A / pi) - (|_` (A / pi))) x. pi) e. RR*)
64		0re 6603	. . . . . . . . . . . . . . 15 |- 0 e. RR
65		rexr 6668	. . . . . . . . . . . . . . 15 |- (0 e. RR -> 0 e. RR*)
66	64, 65	ax-mp 7	. . . . . . . . . . . . . 14 |- 0 e. RR*
67		rexr 6668	. . . . . . . . . . . . . . 15 |- (pi e. RR -> pi e. RR*)
68	2, 67	ax-mp 7	. . . . . . . . . . . . . 14 |- pi e. RR*
69		elioo5 7552	. . . . . . . . . . . . . 14 |- ((0 e. RR* /\ pi e. RR* /\ (((A / pi) - (|_` (A / pi))) x. pi) e. RR*) -> ((((A / pi) - (|_` (A / pi))) x. pi) e. (0(,)pi) <-> (0 < (((A / pi) - (|_` (A / pi))) x. pi) /\ (((A / pi) - (|_` (A / pi))) x. pi) < pi)))
70	66, 68, 69	mp3an12 1181	. . . . . . . . . . . . 13 |- ((((A / pi) - (|_` (A / pi))) x. pi) e. RR* -> ((((A / pi) - (|_` (A / pi))) x. pi) e. (0(,)pi) <-> (0 < (((A / pi) - (|_` (A / pi))) x. pi) /\ (((A / pi) - (|_` (A / pi))) x. pi) < pi)))
71	63, 70	syl 12	. . . . . . . . . . . 12 |- (A e. RR -> ((((A / pi) - (|_` (A / pi))) x. pi) e. (0(,)pi) <-> (0 < (((A / pi) - (|_` (A / pi))) x. pi) /\ (((A / pi) - (|_` (A / pi))) x. pi) < pi)))
72	71	adantr 425	. . . . . . . . . . 11 |- ((A e. RR /\ (((A / pi) - (|_` (A / pi))) x. pi) =/= 0) -> ((((A / pi) - (|_` (A / pi))) x. pi) e. (0(,)pi) <-> (0 < (((A / pi) - (|_` (A / pi))) x. pi) /\ (((A / pi) - (|_` (A / pi))) x. pi) < pi)))
73		fracge0 7471	. . . . . . . . . . . . . . 15 |- ((A / pi) e. RR -> 0 <_ ((A / pi) - (|_` (A / pi))))
74	10, 73	syl 12	. . . . . . . . . . . . . 14 |- (A e. RR -> 0 <_ ((A / pi) - (|_` (A / pi))))
75	64, 2, 4	ltleii 6756	. . . . . . . . . . . . . . . 16 |- 0 <_ pi
76		mulge0OLD 6869	. . . . . . . . . . . . . . . 16 |- (((((A / pi) - (|_` (A / pi))) e. RR /\ pi e. RR) /\ (0 <_ ((A / pi) - (|_` (A / pi))) /\ 0 <_ pi)) -> 0 <_ (((A / pi) - (|_` (A / pi))) x. pi))
77	75, 76	mpanr2 776	. . . . . . . . . . . . . . 15 |- (((((A / pi) - (|_` (A / pi))) e. RR /\ pi e. RR) /\ 0 <_ ((A / pi) - (|_` (A / pi)))) -> 0 <_ (((A / pi) - (|_` (A / pi))) x. pi))
78	2, 77	mpanl2 771	. . . . . . . . . . . . . 14 |- ((((A / pi) - (|_` (A / pi))) e. RR /\ 0 <_ ((A / pi) - (|_` (A / pi)))) -> 0 <_ (((A / pi) - (|_` (A / pi))) x. pi))
79	21, 74, 78	syl11anc 524	. . . . . . . . . . . . 13 |- (A e. RR -> 0 <_ (((A / pi) - (|_` (A / pi))) x. pi))
80		ne0gt0 6801	. . . . . . . . . . . . 13 |- (((((A / pi) - (|_` (A / pi))) x. pi) e. RR /\ 0 <_ (((A / pi) - (|_` (A / pi))) x. pi)) -> ((((A / pi) - (|_` (A / pi))) x. pi) =/= 0 <-> 0 < (((A / pi) - (|_` (A / pi))) x. pi)))
81	35, 79, 80	syl11anc 524	. . . . . . . . . . . 12 |- (A e. RR -> ((((A / pi) - (|_` (A / pi))) x. pi) =/= 0 <-> 0 < (((A / pi) - (|_` (A / pi))) x. pi)))
82	81	biimpa 460	. . . . . . . . . . 11 |- ((A e. RR /\ (((A / pi) - (|_` (A / pi))) x. pi) =/= 0) -> 0 < (((A / pi) - (|_` (A / pi))) x. pi))
83		fraclt1 7470	. . . . . . . . . . . . . . 15 |- ((A / pi) e. RR -> ((A / pi) - (|_` (A / pi))) < 1)
84	10, 83	syl 12	. . . . . . . . . . . . . 14 |- (A e. RR -> ((A / pi) - (|_` (A / pi))) < 1)
85		1re 6598	. . . . . . . . . . . . . . . 16 |- 1 e. RR
86	2, 4	pm3.2i 307	. . . . . . . . . . . . . . . 16 |- (pi e. RR /\ 0 < pi)
87		ltmul1 7008	. . . . . . . . . . . . . . . 16 |- ((((A / pi) - (|_` (A / pi))) e. RR /\ 1 e. RR /\ (pi e. RR /\ 0 < pi)) -> (((A / pi) - (|_` (A / pi))) < 1 <-> (((A / pi) - (|_` (A / pi))) x. pi) < (1 x. pi)))
88	85, 86, 87	mp3an23 1183	. . . . . . . . . . . . . . 15 |- (((A / pi) - (|_` (A / pi))) e. RR -> (((A / pi) - (|_` (A / pi))) < 1 <-> (((A / pi) - (|_` (A / pi))) x. pi) < (1 x. pi)))
89	21, 88	syl 12	. . . . . . . . . . . . . 14 |- (A e. RR -> (((A / pi) - (|_` (A / pi))) < 1 <-> (((A / pi) - (|_` (A / pi))) x. pi) < (1 x. pi)))
90	84, 89	mpbid 212	. . . . . . . . . . . . 13 |- (A e. RR -> (((A / pi) - (|_` (A / pi))) x. pi) < (1 x. pi))
91	3	mulid2i 6486	. . . . . . . . . . . . 13 |- (1 x. pi) = pi
92	90, 91	syl6breq 3376	. . . . . . . . . . . 12 |- (A e. RR -> (((A / pi) - (|_` (A / pi))) x. pi) < pi)
93	92	adantr 425	. . . . . . . . . . 11 |- ((A e. RR /\ (((A / pi) - (|_` (A / pi))) x. pi) =/= 0) -> (((A / pi) - (|_` (A / pi))) x. pi) < pi)
94	72, 82, 93	mpbir2and 802	. . . . . . . . . 10 |- ((A e. RR /\ (((A / pi) - (|_` (A / pi))) x. pi) =/= 0) -> (((A / pi) - (|_` (A / pi))) x. pi) e. (0(,)pi))
95		sinq12gt0t 10057	. . . . . . . . . 10 |- ((((A / pi) - (|_` (A / pi))) x. pi) e. (0(,)pi) -> 0 < (sin` (((A / pi) - (|_` (A / pi))) x. pi)))
96	94, 95	syl 12	. . . . . . . . 9 |- ((A e. RR /\ (((A / pi) - (|_` (A / pi))) x. pi) =/= 0) -> 0 < (sin` (((A / pi) - (|_` (A / pi))) x. pi)))
97		gt0ne0 6800	. . . . . . . . 9 |- (((sin` (((A / pi) - (|_` (A / pi))) x. pi)) e. RR /\ 0 < (sin` (((A / pi) - (|_` (A / pi))) x. pi))) -> (sin` (((A / pi) - (|_` (A / pi))) x. pi)) =/= 0)
98	61, 96, 97	syl11anc 524	. . . . . . . 8 |- ((A e. RR /\ (((A / pi) - (|_` (A / pi))) x. pi) =/= 0) -> (sin` (((A / pi) - (|_` (A / pi))) x. pi)) =/= 0)
99	98	ex 402	. . . . . . 7 |- (A e. RR -> ((((A / pi) - (|_` (A / pi))) x. pi) =/= 0 -> (sin` (((A / pi) - (|_` (A / pi))) x. pi)) =/= 0))
100	99	necon4d 2075	. . . . . 6 |- (A e. RR -> ((sin` (((A / pi) - (|_` (A / pi))) x. pi)) = 0 -> (((A / pi) - (|_` (A / pi))) x. pi) = 0))
101	100	adantr 425	. . . . 5 |- ((A e. RR /\ (sin` A) = 0) -> ((sin` (((A / pi) - (|_` (A / pi))) x. pi)) = 0 -> (((A / pi) - (|_` (A / pi))) x. pi) = 0))
102	60, 101	mpd 29	. . . 4 |- ((A e. RR /\ (sin` A) = 0) -> (((A / pi) - (|_` (A / pi))) x. pi) = 0)
103	102	opreq2d 4898	. . 3 |- ((A e. RR /\ (sin` A) = 0) -> (((|_` (A / pi)) x. pi) + (((A / pi) - (|_` (A / pi))) x. pi)) = (((|_` (A / pi)) x. pi) + 0))
104	28, 103	eqtrd 1925	. 2 |- ((A e. RR /\ (sin` A) = 0) -> A = (((|_` (A / pi)) x. pi) + 0))
105		addid1 6463	. . . 4 |- (((|_` (A / pi)) x. pi) e. CC -> (((|_` (A / pi)) x. pi) + 0) = ((|_` (A / pi)) x. pi))
106	32, 105	syl 12	. . 3 |- (A e. RR -> (((|_` (A / pi)) x. pi) + 0) = ((|_` (A / pi)) x. pi))
107	106	adantr 425	. 2 |- ((A e. RR /\ (sin` A) = 0) -> (((|_` (A / pi)) x. pi) + 0) = ((|_` (A / pi)) x. pi))
108	104, 107	eqtrd 1925	1 |- ((A e. RR /\ (sin` A) = 0) -> A = ((|_` (A / pi)) x. pi))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   = wceq 1298   e. wcel 1300   =/= wne 2017   class class class wbr 3338  ` cfv 3998  (class class class)co 4884  CCcc 6384  RRcr 6385  0cc0 6386  1c1 6387   + caddc 6389   x. cmul 6391   - cmin 6445   / cdiv 6447   <_ cle 6448  ZZcz 6451  RR*cxr 6652   < clt 6653  |_cfl 7462  (,)cioo 7524  abscabs 8000  sincsin 8557  picpi 8559

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1302  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-reg 5695  ax-inf2 5731  ax-ac 5906

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-nel 2020  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-iin 3258  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-mpt 5006  df-1st 5020  df-2nd 5021  df-iota 5089  df-rdg 5140  df-1o 5177  df-oadd 5179  df-omul 5180  df-er 5318  df-ec 5320  df-qs 5323  df-map 5383  df-en 5427  df-dom 5428  df-sdom 5429  df-undef 5556  df-riota 5560  df-sup 5664  df-r1 5750  df-rank 5751  df-ni 6152  df-pli 6153  df-mi 6154  df-lti 6155  df-plpq 6187  df-mpq 6188  df-enq 6189  df-nq 6190  df-plq 6191  df-mq 6192  df-rq 6193  df-ltq 6194  df-1q 6195  df-np 6238  df-1p 6239  df-plp 6240  df-mp 6241  df-ltp 6242  df-plpr 6316  df-mpr 6317  df-enr 6318  df-nr 6319  df-plr 6320  df-mr 6321  df-ltr 6322  df-0r 6323  df-1r 6324  df-m1r 6325  df-c 6392  df-0 6393  df-1 6394  df-i 6395  df-r 6396  df-plus 6397  df-mul 6398  df-lt 6399  df-sub 6511  df-neg 6513  df-pnf 6654  df-mnf 6655  df-xr 6656  df-ltxr 6657  df-le 6658  df-div 6892  df-n 7108  df-2 7154  df-3 7155  df-4 7156  df-5 7157  df-6 7158  df-7 7159  df-8 7160  df-9 7161  df-rp 7232  df-n0 7309  df-z 7345  df-q 7436  df-fl 7463  df-ioo 7528  df-ioc 7529  df-ico 7530  df-icc 7531  df-uz 7587  df-fz 7638  df-seq1 7721  df-shft 7754  df-seqz 7776  df-seq0 7777  df-exp 7812  df-sqr 7920  df-re 8001  df-im 8002  df-cj 8003  df-abs 8004  df-fac 8184  df-bc 8209  df-clim 8235  df-sum 8240  df-cncf 8525  df-ef 8560  df-sin 8562  df-cos 8563  df-pi 8564  df-top 8861  df-cn 9030  df-cnp 9031  df-met 9070  df-bl 9072  df-opn 9073  df-lm 9200

Copyright terms: Public domain