fperdvper - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > fperdvper		Structured version Unicode version

Theorem fperdvper 31571

Description: The derivative of a periodic function is periodic (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypotheses**
Ref	Expression
fperdvper.f
fperdvper.t
fperdvper.fper	$/\$
fperdvper.g

**Assertion**
Ref	Expression
fperdvper	$/\$ $/\$

Distinct variable groups:

Allowed substitution hint:

(

)

Proof of Theorem fperdvper Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dvf 22179	. . . . . . . . 9
2	1	a1i 11	. . . . . . . 8
3		fperdvper.g	. . . . . . . . . 10
4	3	a1i 11	. . . . . . . . 9
5	4	feq1d 5723	. . . . . . . 8
6	2, 5	mpbird 232	. . . . . . 7
7	6	adantr 465	. . . . . 6 $/\$
8		id 22	. . . . . . . 8
9	3	dmeqi 5210	. . . . . . . . 9
10	9	a1i 11	. . . . . . . 8
11	8, 10	eleqtrd 2557	. . . . . . 7
12	11	adantl 466	. . . . . 6 $/\$
13	7, 12	ffvelrnd 6033	. . . . 5 $/\$
14		dvbsss 22174	. . . . . . . . . . . . 13
15	14	sseli 3505	. . . . . . . . . . . 12
16	11, 15	syl 16	. . . . . . . . . . 11
17	16	adantl 466	. . . . . . . . . 10 $/\$
18		fperdvper.t	. . . . . . . . . . 11
19	18	adantr 465	. . . . . . . . . 10 $/\$
20	17, 19	readdcld 9635	. . . . . . . . 9 $/\$
21		reopn 31376	. . . . . . . . . . . 12
22	21	a1i 11	. . . . . . . . . . 11 $/\$
23		retop 21136	. . . . . . . . . . . . 13
24	23	a1i 11	. . . . . . . . . . . 12 $/\$
25		ssid 3528	. . . . . . . . . . . . 13
26	25	a1i 11	. . . . . . . . . . . 12 $/\$
27		uniretop 21137	. . . . . . . . . . . . 13
28	27	isopn3 19435	. . . . . . . . . . . 12 $/\$
29	24, 26, 28	syl2anc 661	. . . . . . . . . . 11 $/\$
30	22, 29	mpbid 210	. . . . . . . . . 10 $/\$
31	30	eqcomd 2475	. . . . . . . . 9 $/\$
32	20, 31	eleqtrd 2557	. . . . . . . 8 $/\$
33	3	fveq1i 5873	. . . . . . . . . . . . . . 15
34	33	eqcomi 2480	. . . . . . . . . . . . . 14
35	34	a1i 11	. . . . . . . . . . . . 13 $/\$
36	12, 35	jca 532	. . . . . . . . . . . 12 $/\$ $/\$
37		ffun 5739	. . . . . . . . . . . . . . . 16
38	1, 37	ax-mp 5	. . . . . . . . . . . . . . 15
39	38	a1i 11	. . . . . . . . . . . . . 14
40		funbrfv2b 5918	. . . . . . . . . . . . . 14 $/\$
41	39, 40	syl 16	. . . . . . . . . . . . 13 $/\$
42	41	adantr 465	. . . . . . . . . . . 12 $/\$ $/\$
43	36, 42	mpbird 232	. . . . . . . . . . 11 $/\$
44		eqid 2467	. . . . . . . . . . . . 13 ℂ_fld ℂ_fld
45	44	tgioo2 21176	. . . . . . . . . . . 12 ℂ_fld ↾_t
46		eqid 2467	. . . . . . . . . . . 12 $\$ $\$
47		ax-resscn 9561	. . . . . . . . . . . . 13
48	47	a1i 11	. . . . . . . . . . . 12 $/\$
49		fperdvper.f	. . . . . . . . . . . . 13
50	49	adantr 465	. . . . . . . . . . . 12 $/\$
51	45, 44, 46, 48, 50, 26	eldv 22170	. . . . . . . . . . 11 $/\$ $/\$ $\$ lim
52	43, 51	mpbid 210	. . . . . . . . . 10 $/\$ $/\$ $\$ lim
53	52	simprd 463	. . . . . . . . 9 $/\$ $\$ lim
54		nfv 1683	. . . . . . . . . . . 12 $/\$
55	50, 48, 17	dvlem 22168	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
56	55, 46	fmptd 6056	. . . . . . . . . . . . . 14 $/\$ $\$ $\$
57	48	ssdifssd 3647	. . . . . . . . . . . . . 14 $/\$ $\$
58	47, 17	sseldi 3507	. . . . . . . . . . . . . 14 $/\$
59	56, 57, 58	ellimc3 22151	. . . . . . . . . . . . 13 $/\$ $\$ lim $/\$ $\$ $/\$ $\$
60		eqidd 2468	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$ $\$ $\$
61		fveq2 5872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
62	61	oveq1d 6310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
63		oveq1 6302	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
64	62, 63	oveq12d 6313	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
65	64	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\$ $/\$
66		eldifi 3631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $\$
67	47, 66	sseldi 3507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $\$
68	67	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $\$
69	47, 18	sseldi 3507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
70	69	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $\$
71	68, 70	npcand 9946	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $\$
72	71	eqcomd 2475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $\$
73	72	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $\$
74		ovex 6320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
75	74	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $\$
76	66	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $\$
77	18	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $\$
78	76, 77	resubcld 9999	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $\$
79	78	ex 434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $\$
80	79	imdistani 690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $\$ $/\$
81		eleq1 2539	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
82	81	anbi2d 703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
83		oveq1 6302	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
84	83	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
85		fveq2 5872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
86	84, 85	eqeq12d 2489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
87	82, 86	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
88		fperdvper.fper	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
89	88	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
90	87, 89	vtoclga 3182	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
91	75, 80, 90	sylc 60	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $\$
92	73, 91	eqtrd 2508	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $\$
93	92	adantlr 714	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $\$
94		simpll 753	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $\$
95	17	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $\$
96	94, 95, 88	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $\$
97	93, 96	oveq12d 6313	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $\$
98	67	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $\$
99	94, 69	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $\$
100	58	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $\$
101	98, 99, 100	subsub4d 9973	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $\$
102	99, 100	addcomd 9793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $\$
103	102	oveq2d 6311	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $\$
104	101, 103	eqtr2d 2509	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $\$
105	97, 104	oveq12d 6313	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\$
106	105	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\$ $/\$
107	65, 106	eqtrd 2508	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$ $/\$
108		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$ $\$
109	49	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $\$
110	109, 78	ffvelrnd 6033	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $\$
111	110	adantlr 714	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\$
112	50, 17	ffvelrnd 6033	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
113	112	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\$
114	111, 113	subcld 9942	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\$
115	98, 99	subcld 9942	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\$
116	115, 100	subcld 9942	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\$
117		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $\$ $/\$
118	98	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $\$ $/\$
119	99	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $\$ $/\$
120	100	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $\$ $/\$
121	118, 119, 120	subadd2d 9961	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $\$ $/\$
122	117, 121	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $\$ $/\$
123	122	eqcomd 2475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $\$ $/\$
124		eldifsni 4159	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $\$
125	124	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $\$ $/\$
126	125	neneqd 2669	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $\$ $/\$
127	123, 126	pm2.65da 576	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $\$
128	127	neqned 2670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\$
129	115, 100, 128	subne0d 9951	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\$
130	114, 116, 129	divcld 10332	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$
131	60, 107, 108, 130	fvmptd 5962	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$ $\$
132	131	oveq1d 6310	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $\$ $\$
133	132	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $\$ $\$
134	133	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$ $/\$ $/\$ $\$
135	134	adantllr 718	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $\$
136		simpllr 758	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
137	66	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$
138	19	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$
139	137, 138	resubcld 9999	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$
140		elsni 4058	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
141	140	necon3ai 2695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
142	128, 141	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\$
143	142	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$ $/\$
144	143	adantllr 718	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$
145	139, 144	eldifd 3492	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
146		neeq1 2748	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
147		oveq1 6302	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
148	147	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
149	148	breq1d 4463	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
150	146, 149	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
151		fveq2 5872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $\$
152	151	oveq1d 6310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $\$
153	152	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $\$
154	153	breq1d 4463	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $\$
155	150, 154	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $\$ $/\$ $\$
156	155	rspccva 3218	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
157	136, 145, 156	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $\$
158		eqidd 2468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $\$ $\$ $\$
159		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $\$ $/\$
160	159	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $\$ $/\$
161	160	oveq1d 6310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $\$ $/\$
162	159	oveq1d 6310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $\$ $/\$
163	161, 162	oveq12d 6313	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $\$ $/\$
164	66	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $\$
165	94, 18	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $\$
166	164, 165	resubcld 9999	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $\$
167	166, 142	eldifd 3492	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $\$ $\$
168	158, 163, 167, 130	fvmptd 5962	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $\$ $\$
169	168	eqcomd 2475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $\$ $\$
170	169	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $\$
171	170	oveq1d 6310	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $\$
172	171	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $\$
173	128	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $\$ $/\$
174	104	eqcomd 2475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $\$
175	174	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $\$ $/\$
176	175	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $\$ $/\$
177		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $\$ $/\$
178	176, 177	eqbrtrd 4473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $\$ $/\$
179	173, 178	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\$ $/\$ $/\$
180	179	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $/\$
181		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
182	180, 181	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $\$
183	172, 182	eqbrtrd 4473	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
184	183	ex 434	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $\$ $/\$ $/\$ $\$
185	184	adantllr 718	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $\$
186	157, 185	mpd 15	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$
187	186	adantrl 715	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$
188	135, 187	eqbrtrd 4473	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $\$
189	188	ex 434	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
190	189	ralrimiva 2881	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $\$ $/\$ $\$ $\$ $/\$ $\$
191	190	ex 434	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $/\$ $\$ $\$ $/\$ $\$
192		eqidd 2468	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $\$ $\$
193		fveq2 5872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
194	193	oveq1d 6310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
195		oveq1 6302	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
196	194, 195	oveq12d 6313	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
197	196	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $/\$
198		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $\$
199		ovex 6320	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
200	199	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$
201	192, 197, 198, 200	fvmptd 5962	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $\$
202	201	oveq1d 6310	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$
203	202	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$
204	203	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$ $/\$ $/\$ $\$
205	204	adantllr 718	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $\$
206		simpll 753	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $\$
207	198	eldifad 3493	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$
208	207	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $\$
209		eleq1 2539	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
210	209	anbi2d 703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
211		oveq1 6302	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
212	211	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
213		fveq2 5872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
214	212, 213	eqeq12d 2489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
215	210, 214	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
216	215, 88	chvarv 1983	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
217	216	eqcomd 2475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
218	206, 208, 217	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $\$
219	17	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $\$
220	206, 219, 88	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $\$
221	220	eqcomd 2475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $\$
222	218, 221	oveq12d 6313	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\$
223	47, 208	sseldi 3507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $\$
224	58	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $\$
225	206, 69	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $\$
226	223, 224, 225	pnpcan2d 9980	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $\$
227	226	eqcomd 2475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\$
228	222, 227	oveq12d 6313	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\$
229	228	oveq1d 6310	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$
230	229	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$
231	230	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $\$ $/\$
232	231	adantllr 718	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$
233		simpllr 758	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
234	207	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$
235	19	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$
236	234, 235	readdcld 9635	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$
237		eldifsni 4159	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$
238	237	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $\$
239	223, 224, 225, 238	addneintr2d 9799	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $\$
240	239	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\$ $/\$
241	240	adantllr 718	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$
242		elsni 4058	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
243	242	necon3ai 2695	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
244	241, 243	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$
245	236, 244	eldifd 3492	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
246		neeq1 2748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
247		oveq1 6302	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
248	247	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
249	248	breq1d 4463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
250	246, 249	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
251		fveq2 5872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$
252	251	oveq1d 6310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $\$
253	252	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $\$
254	253	breq1d 4463	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $\$
255	250, 254	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $/\$ $\$
256	255	rspccva 3218	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
257	233, 245, 256	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $\$
258		eqidd 2468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $\$ $\$ $\$
259		fveq2 5872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
260	259	oveq1d 6310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35