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 31954

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		dvbsss 22472	. . . . . . . 8
2		id 22	. . . . . . . . 9
3		fperdvper.g	. . . . . . . . . 10
4	3	dmeqi 5193	. . . . . . . . 9
5	2, 4	syl6eleq 2552	. . . . . . . 8
6	1, 5	sseldi 3487	. . . . . . 7
7	6	adantl 464	. . . . . 6 $/\$
8		fperdvper.t	. . . . . . 7
9	8	adantr 463	. . . . . 6 $/\$
10	7, 9	readdcld 9612	. . . . 5 $/\$
11		reopn 31716	. . . . . . 7
12		retop 21434	. . . . . . . 8
13		ssid 3508	. . . . . . . . 9
14	13	a1i 11	. . . . . . . 8 $/\$
15		uniretop 21435	. . . . . . . . 9
16	15	isopn3 19734	. . . . . . . 8 $/\$
17	12, 14, 16	sylancr 661	. . . . . . 7 $/\$
18	11, 17	mpbii 211	. . . . . 6 $/\$
19	18	eqcomd 2462	. . . . 5 $/\$
20	10, 19	eleqtrd 2544	. . . 4 $/\$
21	5	adantl 464	. . . . . . . 8 $/\$
22	3	fveq1i 5849	. . . . . . . . . 10
23	22	eqcomi 2467	. . . . . . . . 9
24	23	a1i 11	. . . . . . . 8 $/\$
25		dvf 22477	. . . . . . . . . . . 12
26		ffun 5715	. . . . . . . . . . . 12
27	25, 26	ax-mp 5	. . . . . . . . . . 11
28	27	a1i 11	. . . . . . . . . 10
29		funbrfv2b 5892	. . . . . . . . . 10 $/\$
30	28, 29	syl 16	. . . . . . . . 9 $/\$
31	30	adantr 463	. . . . . . . 8 $/\$ $/\$
32	21, 24, 31	mpbir2and 920	. . . . . . 7 $/\$
33		eqid 2454	. . . . . . . . 9 ℂ_fld ℂ_fld
34	33	tgioo2 21474	. . . . . . . 8 ℂ_fld ↾_t
35		eqid 2454	. . . . . . . 8 $\$ $\$
36		ax-resscn 9538	. . . . . . . . 9
37	36	a1i 11	. . . . . . . 8 $/\$
38		fperdvper.f	. . . . . . . . 9
39	38	adantr 463	. . . . . . . 8 $/\$
40	34, 33, 35, 37, 39, 14	eldv 22468	. . . . . . 7 $/\$ $/\$ $\$ lim
41	32, 40	mpbid 210	. . . . . 6 $/\$ $/\$ $\$ lim
42	41	simprd 461	. . . . 5 $/\$ $\$ lim
43		eqidd 2455	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$ $\$ $\$
44		fveq2 5848	. . . . . . . . . . . . . . . . . . . . . . 23
45	44	oveq1d 6285	. . . . . . . . . . . . . . . . . . . . . 22
46		oveq1 6277	. . . . . . . . . . . . . . . . . . . . . 22
47	45, 46	oveq12d 6288	. . . . . . . . . . . . . . . . . . . . 21
48		eldifi 3612	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$
49	48	recnd 9611	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$
50	49	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\$
51	8	recnd 9611	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
52	51	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\$
53	50, 52	npcand 9926	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$
54	53	eqcomd 2462	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $\$
55	54	fveq2d 5852	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $\$
56		ovex 6298	. . . . . . . . . . . . . . . . . . . . . . . . . 26
57	48	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $\$
58	8	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $\$
59	57, 58	resubcld 9983	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\$
60	59	ex 432	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$
61	60	imdistani 688	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $\$ $/\$
62		eleq1 2526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
63	62	anbi2d 701	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
64		oveq1 6277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
65	64	fveq2d 5852	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
66		fveq2 5848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
67	65, 66	eqeq12d 2476	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
68	63, 67	imbi12d 318	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
69		fperdvper.fper	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
70	68, 69	vtoclg 3164	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
71	56, 61, 70	mpsyl 63	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $\$
72	55, 71	eqtrd 2495	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\$
73	72	adantlr 712	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$
74		simpll 751	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $\$
75	6	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $\$
76	74, 75, 69	syl2anc 659	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$
77	73, 76	oveq12d 6288	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$
78	49	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $\$
79	74, 51	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $\$
80	7	recnd 9611	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
81	80	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $\$
82	78, 79, 81	subsub4d 9953	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$
83	79, 81	addcomd 9771	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $\$
84	83	oveq2d 6286	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$
85	82, 84	eqtr2d 2496	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$
86	77, 85	oveq12d 6288	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$
87	47, 86	sylan9eqr 2517	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$ $/\$
88		simpr 459	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$ $\$
89	38	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\$
90	89, 59	ffvelrnd 6008	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\$
91	90	adantlr 712	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$
92	39, 7	ffvelrnd 6008	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
93	92	adantr 463	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$
94	91, 93	subcld 9922	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$
95	78, 79	subcld 9922	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$
96	95, 81	subcld 9922	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$
97		simpr 459	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$ $/\$
98	49	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$ $/\$
99	79	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$ $/\$
100	81	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$ $/\$
101	98, 99, 100	subadd2d 9941	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$ $/\$
102	97, 101	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $\$ $/\$
103	102	eqcomd 2462	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $\$ $/\$
104		eldifsni 4142	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$
105	104	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $\$ $/\$
106	105	neneqd 2656	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $\$ $/\$
107	103, 106	pm2.65da 574	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$
108	107	neqned 2657	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$
109	95, 81, 108	subne0d 9931	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$
110	94, 96, 109	divcld 10316	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$
111	43, 87, 88, 110	fvmptd 5936	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $\$ $\$
112	111	oveq1d 6285	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$ $\$
113	112	fveq2d 5852	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $\$
114	113	adantr 463	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $/\$ $/\$ $\$
115	114	adantllr 716	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $\$
116		simpllr 758	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
117	48	ad2antlr 724	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$
118	8	ad4antr 729	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$
119	117, 118	resubcld 9983	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$
120		elsni 4041	. . . . . . . . . . . . . . . . . . . . . 22
121	107, 120	nsyl 121	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$
122	121	adantr 463	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$ $/\$
123	122	adantllr 716	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$
124	119, 123	eldifd 3472	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
125		neeq1 2735	. . . . . . . . . . . . . . . . . . . . 21
126		oveq1 6277	. . . . . . . . . . . . . . . . . . . . . . 23
127	126	fveq2d 5852	. . . . . . . . . . . . . . . . . . . . . 22
128	127	breq1d 4449	. . . . . . . . . . . . . . . . . . . . 21
129	125, 128	anbi12d 708	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
130		fveq2 5848	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$
131	130	oveq1d 6285	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$
132	131	fveq2d 5852	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
133	132	breq1d 4449	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
134	129, 133	imbi12d 318	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$ $/\$ $\$
135	134	rspccva 3206	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
136	116, 124, 135	syl2anc 659	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $\$
137		eqidd 2455	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $\$ $\$ $\$
138		simpr 459	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\$ $/\$
139	138	fveq2d 5852	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$ $/\$
140	139	oveq1d 6285	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$ $/\$
141	138	oveq1d 6285	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$ $/\$
142	140, 141	oveq12d 6288	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $\$ $/\$
143	48	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$
144	74, 8	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$
145	143, 144	resubcld 9983	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$
146	145, 121	eldifd 3472	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $\$ $\$
147	137, 142, 146, 110	fvmptd 5936	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $\$ $\$
148	147	eqcomd 2462	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$ $\$
149	148	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $\$
150	149	oveq1d 6285	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $\$
151	150	fveq2d 5852	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $\$
152	108	adantr 463	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$ $/\$
153	85	eqcomd 2462	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$
154	153	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $\$ $/\$
155	154	fveq2d 5852	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $\$ $/\$
156		simpr 459	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $\$ $/\$
157	155, 156	eqbrtrd 4459	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$ $/\$
158	152, 157	jca 530	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$ $/\$ $/\$
159	158	adantr 463	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $/\$
160		simpr 459	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
161	159, 160	mpd 15	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $\$
162	151, 161	eqbrtrd 4459	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
163	162	ex 432	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$ $/\$ $/\$ $\$
164	163	adantllr 716	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $\$
165	136, 164	mpd 15	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$
166	165	adantrl 713	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$
167	115, 166	eqbrtrd 4459	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $\$
168	167	ex 432	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
169	168	ralrimiva 2868	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $/\$ $\$ $\$ $/\$ $\$
170		eqidd 2455	. . . . . . . . . . . . . . . . . . 19 $\$ $\$ $\$
171		fveq2 5848	. . . . . . . . . . . . . . . . . . . . . 22
172	171	oveq1d 6285	. . . . . . . . . . . . . . . . . . . . 21
173		oveq1 6277	. . . . . . . . . . . . . . . . . . . . 21
174	172, 173	oveq12d 6288	. . . . . . . . . . . . . . . . . . . 20
175	174	adantl 464	. . . . . . . . . . . . . . . . . . 19 $\$ $/\$
176		id 22	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
177		ovex 6298	. . . . . . . . . . . . . . . . . . . 20
178	177	a1i 11	. . . . . . . . . . . . . . . . . . 19 $\$
179	170, 175, 176, 178	fvmptd 5936	. . . . . . . . . . . . . . . . . 18 $\$ $\$
180	179	oveq1d 6285	. . . . . . . . . . . . . . . . 17 $\$ $\$
181	180	fveq2d 5852	. . . . . . . . . . . . . . . 16 $\$ $\$
182	181	ad2antlr 724	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $\$
183		simpll 751	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $\$
184		eldifi 3612	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
185	184	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $\$
186		eleq1 2526	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
187	186	anbi2d 701	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
188		oveq1 6277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
189	188	fveq2d 5852	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
190		fveq2 5848	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
191	189, 190	eqeq12d 2476	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
192	187, 191	imbi12d 318	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
193	192, 69	chvarv 2019	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
194	193	eqcomd 2462	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
195	183, 185, 194	syl2anc 659	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$
196	6	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $\$
197	183, 196, 69	syl2anc 659	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $\$
198	197	eqcomd 2462	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$
199	195, 198	oveq12d 6288	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$
200	185	recnd 9611	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $\$
201	80	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $\$
202	183, 51	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $\$
203	200, 201, 202	pnpcan2d 9960	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$
204	203	eqcomd 2462	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$
205	199, 204	oveq12d 6288	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$
206	205	oveq1d 6285	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$
207	206	fveq2d 5852	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $\$
208	207	adantr 463	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$ $/\$
209	208	adantllr 716	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$
210		simpllr 758	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
211	184	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$
212	8	ad4antr 729	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$
213	211, 212	readdcld 9612	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$
214		eldifsni 4142	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
215	214	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $\$
216	200, 201, 202, 215	addneintr2d 9777	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$
217	216	adantr 463	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$ $/\$
218	217	adantllr 716	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$
219		elsni 4041	. . . . . . . . . . . . . . . . . . . . . 22
220	219	necon3ai 2682	. . . . . . . . . . . . . . . . . . . . 21
221	218, 220	syl 16	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$
222	213, 221	eldifd 3472	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
223		neeq1 2735	. . . . . . . . . . . . . . . . . . . . . 22
224		oveq1 6277	. . . . . . . . . . . . . . . . . . . . . . . 24
225	224	fveq2d 5852	. . . . . . . . . . . . . . . . . . . . . . 23
226	225	breq1d 4449	. . . . . . . . . . . . . . . . . . . . . 22
227	223, 226	anbi12d 708	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
228		fveq2 5848	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$
229	228	oveq1d 6285	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$
230	229	fveq2d 5852	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$
231	230	breq1d 4449	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
232	227, 231	imbi12d 318	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$ $/\$ $\$
233	232	rspccva 3206	. . . . . . . . . . . . . . . . . . 19 $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
234	210, 222, 233	syl2anc 659	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $\$
235		eqidd 2455	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$ $\$ $\$
236		fveq2 5848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
237	236	oveq1d 6285	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
238		oveq1 6277	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
239	237, 238	oveq12d 6288	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
240	239	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$ $/\$
241	183, 8	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\$
242	185, 241	readdcld 9612	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$
243	216, 220	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$
244	242, 243	eldifd 3472	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$ $\$
245	205, 177	syl6eqelr 2551	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$
246	235, 240, 244, 245	fvmptd 5936	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $\$ $\$
247	246	eqcomd 2462	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $\$ $\$
248	247	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $\$
249	248	oveq1d 6285	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $\$
250	249	fveq2d 5852	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$ $/\$ $/\$ $/\$