itg2addnclem3 - Mathbox for Brendan Leahy

	Mathbox for Brendan Leahy		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > itg2addnclem3		Structured version Visualization version Unicode version

Theorem itg2addnclem3 33463

Description: Lemma incomprehensible in isolation split off to shorten proof of itg2addnc 33464. (Contributed by Brendan Leahy, 11-Mar-2018.)

**Hypotheses**
Ref	Expression
itg2addnc.f1	MblFn
itg2addnc.f2
itg2addnc.f3
itg2addnc.g2
itg2addnc.g3

**Assertion**
Ref	Expression
itg2addnclem3	$/\$ $/\$ $/\$ $/\$ $/\$

Distinct variable groups:

Proof of Theorem itg2addnclem3 Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		itg2addnc.f1	. . . . . . . . 9 MblFn
2		itg2addnc.f2	. . . . . . . . 9
3	1, 2	itg2addnclem2 33462	. . . . . . . 8 $/\$ $/\$ $/\$
4	3	adantrr 753	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
5		simplr 792	. . . . . . . . 9 $/\$ $/\$
6		i1fsub 23475	. . . . . . . . 9 $/\$ $/\$ $/\$
7	5, 3, 6	syl2anc 693	. . . . . . . 8 $/\$ $/\$ $/\$
8	7	adantrr 753	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
9		3nn 11186	. . . . . . . . . . . . 13
10		nnrp 11842	. . . . . . . . . . . . 13
11	9, 10	ax-mp 5	. . . . . . . . . . . 12
12		rpdivcl 11856	. . . . . . . . . . . 12 $/\$
13	11, 12	mpan2 707	. . . . . . . . . . 11
14	13	adantl 482	. . . . . . . . . 10 $/\$ $/\$
15		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . 24
16	15	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . 23
17	16	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . 22
18	17	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . 21
19	18	oveq1d 6665	. . . . . . . . . . . . . . . . . . . 20
20		fveq2 6191	. . . . . . . . . . . . . . . . . . . 20
21	19, 20	breq12d 4666	. . . . . . . . . . . . . . . . . . 19
22	20	neeq1d 2853	. . . . . . . . . . . . . . . . . . 19
23	21, 22	anbi12d 747	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
24	23, 19, 20	ifbieq12d 4113	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
25		eqid 2622	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
26		ovex 6678	. . . . . . . . . . . . . . . . . 18
27		fvex 6201	. . . . . . . . . . . . . . . . . 18
28	26, 27	ifex 4156	. . . . . . . . . . . . . . . . 17 $/\$
29	24, 25, 28	fvmpt 6282	. . . . . . . . . . . . . . . 16 $/\$ $/\$
30	29	eqeq1d 2624	. . . . . . . . . . . . . . 15 $/\$ $/\$
31	29	oveq1d 6665	. . . . . . . . . . . . . . 15 $/\$ $/\$
32	30, 31	ifbieq2d 4111	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
33	32	adantl 482	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
34		breq1 4656	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
35		breq1 4656	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
36	2	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
37	36	ffvelrnda 6359	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
38		elrege0 12278	. . . . . . . . . . . . . . . . 17 $/\$
39	37, 38	sylib 208	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
40	39	simprd 479	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
41	40	adantr 481	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
42		df-ne 2795	. . . . . . . . . . . . . . . 16 $/\$ $/\$
43		neeq1 2856	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
44		oveq1 6657	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
45	44	breq1d 4663	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
46	43, 45	imbi12d 334	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
47		neeq1 2856	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
48		oveq1 6657	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
49	48	breq1d 4663	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
50	47, 49	imbi12d 334	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
51		rge0ssre 12280	. . . . . . . . . . . . . . . . . . . . . . . . 25
52	51, 37	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
53	13	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
54	52, 53	rerpdivcld 11903	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
55		reflcl 12597	. . . . . . . . . . . . . . . . . . . . . . 23
56		peano2rem 10348	. . . . . . . . . . . . . . . . . . . . . . 23
57	54, 55, 56	3syl 18	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
58	13	rpred 11872	. . . . . . . . . . . . . . . . . . . . . . 23
59	58	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
60	57, 59	remulcld 10070	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
61		peano2rem 10348	. . . . . . . . . . . . . . . . . . . . . . 23
62	54, 61	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
63	62, 59	remulcld 10070	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
64	54, 55	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
65		1red 10055	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
66		flle 12600	. . . . . . . . . . . . . . . . . . . . . . . 24
67	54, 66	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
68	64, 54, 65, 67	lesub1dd 10643	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
69	57, 62, 53	lemul1d 11915	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
70	68, 69	mpbid 222	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
71	60, 63, 59, 70	leadd1dd 10641	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
72	54	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
73		ax-1cn 9994	. . . . . . . . . . . . . . . . . . . . . . . 24
74		subcl 10280	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
75	72, 73, 74	sylancl 694	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
76	73	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
77	53	rpcnd 11874	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
78	75, 76, 77	adddird 10065	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
79		npcan 10290	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
80	72, 73, 79	sylancl 694	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
81	80	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
82	77	mulid2d 10058	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
83	82	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
84	78, 81, 83	3eqtr3rd 2665	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
85	52	recnd 10068	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
86	53	rpne0d 11877	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
87	85, 77, 86	divcan1d 10802	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
88	84, 87	eqtrd 2656	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
89	71, 88	breqtrd 4679	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
90	89	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
91	90	a1d 25	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
92		ianor 509	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\/$
93	92	anbi1i 731	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\/$ $/\$
94		oranabs 901	. . . . . . . . . . . . . . . . . . . 20 $\/$ $/\$ $/\$
95	93, 94	bitri 264	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
96		i1ff 23443	. . . . . . . . . . . . . . . . . . . . . . . . 25
97	96	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
98	97	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
99	98, 59	readdcld 10069	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
100	99	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
101	52	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
102	60, 59	readdcld 10069	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
103	102	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
104	98	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
105	60	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
106	58	ad3antlr 767	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
107	98, 60	ltnled 10184	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
108	107	biimpar 502	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
109	104, 105, 106, 108	ltadd1dd 10638	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
110	89	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
111	100, 103, 101, 109, 110	ltletrd 10197	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
112	100, 101, 111	ltled 10185	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
113	112	adantrr 753	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
114	95, 113	sylan2b 492	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
115	114	expr 643	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
116	46, 50, 91, 115	ifbothda 4123	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
117	42, 116	syl5bir 233	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
118	117	imp 445	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
119	34, 35, 41, 118	ifbothda 4123	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
120	33, 119	eqbrtrd 4675	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
121	120	ralrimiva 2966	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
122		reex 10027	. . . . . . . . . . . . 13
123	122	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$
124		c0ex 10034	. . . . . . . . . . . . . 14
125		ovex 6678	. . . . . . . . . . . . . 14 $/\$
126	124, 125	ifex 4156	. . . . . . . . . . . . 13 $/\$ $/\$
127	126	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
128		eqidd 2623	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
129	2	feqmptd 6249	. . . . . . . . . . . . 13
130	129	ad2antrr 762	. . . . . . . . . . . 12 $/\$ $/\$
131	123, 127, 37, 128, 130	ofrfval2 6915	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
132	121, 131	mpbird 247	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
133		oveq2 6658	. . . . . . . . . . . . . 14 $/\$ $/\$
134	133	ifeq2d 4105	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
135	134	mpteq2dv 4745	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
136	135	breq1d 4663	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
137	136	rspcev 3309	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
138	14, 132, 137	syl2anc 693	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
139	138	adantrr 753	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
140	13	ad2antrl 764	. . . . . . . . 9 $/\$ $/\$ $/\$
141		ffn 6045	. . . . . . . . . . . . . . . . . . . 20
142	96, 141	syl 17	. . . . . . . . . . . . . . . . . . 19
143	142	ad2antlr 763	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
144		ovex 6678	. . . . . . . . . . . . . . . . . . . . 21
145		fvex 6201	. . . . . . . . . . . . . . . . . . . . 21
146	144, 145	ifex 4156	. . . . . . . . . . . . . . . . . . . 20 $/\$
147	146, 25	fnmpti 6022	. . . . . . . . . . . . . . . . . . 19 $/\$
148	147	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
149		inidm 3822	. . . . . . . . . . . . . . . . . 18
150		eqidd 2623	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
151	29	adantl 482	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
152	143, 148, 123, 123, 149, 150, 151	ofval 6906	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
153	152	eqeq1d 2624	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
154	152	oveq1d 6665	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
155	153, 154	ifbieq2d 4111	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
156	155	adantr 481	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
157		breq1 4656	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
158		breq1 4656	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
159		itg2addnc.g2	. . . . . . . . . . . . . . . . . . . 20
160	159	ad2antrr 762	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
161	160	ffvelrnda 6359	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
162		elrege0 12278	. . . . . . . . . . . . . . . . . 18 $/\$
163	161, 162	sylib 208	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
164	163	simprd 479	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
165	164	ad2antrr 762	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
166		oveq2 6658	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
167	166	oveq1d 6665	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
168	167	breq1d 4663	. . . . . . . . . . . . . . . 16 $/\$ $/\$
169		oveq2 6658	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
170	169	oveq1d 6665	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
171	170	breq1d 4663	. . . . . . . . . . . . . . . 16 $/\$ $/\$
172		id 22	. . . . . . . . . . . . . . . . . . . . . . . . 25
173		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
174	173	necon2bi 2824	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
175		iffalse 4095	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
176	174, 175	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
177	176, 172	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
178	172, 177	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
179		0m0e0 11130	. . . . . . . . . . . . . . . . . . . . . . . 24
180	178, 179	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
181	180	con3i 150	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
182		iffalse 4095	. . . . . . . . . . . . . . . . . . . . . . 23
183	182	breq1d 4663	. . . . . . . . . . . . . . . . . . . . . 22
184	181, 183	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$
185	184	adantl 482	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
186	98	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
187	60	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
188	186, 187, 77	subsubd 10420	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
189	188	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
190	60, 59	resubcld 10458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
191		rpre 11839	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
192	191	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
193	190, 192	readdcld 10069	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
194	51, 161	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
195		1re 10039	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
196	195, 195	readdcli 10053	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
197		resubcl 10345	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
198	54, 196, 197	sylancl 694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
199	198, 59	remulcld 10070	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
200		peano2re 10209	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
201	64, 200	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
202		resubcl 10345	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
203	201, 196, 202	sylancl 694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
204	203, 59	remulcld 10070	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
205	58, 191	resubcld 10458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
206	205	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
207	196	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
208		fllep1 12602	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
209	54, 208	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
210	54, 201, 207, 209	lesub1dd 10643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
211	198, 203, 53	lemul1d 11915	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
212	210, 211	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
213	199, 204, 206, 212	lesub1dd 10643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
214	73, 73	addcli 10044	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
215	214	negcli 10349	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
216	215	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
217	72, 216, 77	adddird 10065	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
218		negsub 10329	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
219	72, 214, 218	sylancl 694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
220	219	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
221		df-2 11079	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
222	221	negeqi 10274	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
223	222	oveq1i 6660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
224		2cn 11091	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
225	13	rpcnd 11874	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
226		mulneg1 10466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
227	224, 225, 226	sylancr 695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
228	223, 227	syl5eqr 2670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
229	228	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
230	87, 229	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
231	217, 220, 230	3eqtr3d 2664	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
232		rpcn 11841	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
233	232, 225	negsubdi2d 10408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
234		3cn 11095	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
235		3ne0 11115	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
236		divcan2 10693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$
237	234, 235, 236	mp3an23 1416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
238	232, 237	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
239	225	mulid2d 10058	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
240	238, 239	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
241		3m1e2 11137	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
242	241	oveq1i 6660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
243		subdir 10464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$
244	234, 73, 243	mp3an12 1414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
245	225, 244	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
246	242, 245	syl5reqr 2671	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
247	240, 246	eqtr3d 2658	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
248	247	negeqd 10275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
249	233, 248	eqtr3d 2658	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
250	249	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
251	231, 250	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
252		rpcn 11841	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
253		mulcl 10020	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
254	224, 252, 253	sylancr 695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
255	13, 254	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
256	255	negcld 10379	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
257	256	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
258	85, 257	pncand 10393	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
259	251, 258	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
260	64	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
261		peano2cn 10208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
262		subsub4 10314	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
263	73, 73, 262	mp3an23 1416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
264	260, 261, 263	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
265		pncan 10287	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
266	260, 73, 265	sylancl 694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
267	266	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
268	264, 267	eqtr3d 2658	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
269	268	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
270	269	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
271	192	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
272	187, 77, 271	subsubd 10420	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
273	270, 272	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
274	213, 259, 273	3brtr3d 4684	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
275	52, 193, 194, 274	leadd1dd 10641	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
276	194	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
277	190	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
278	232	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
279	276, 277, 278	addassd 10062	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
280	277, 278	addcld 10059	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
281	276, 280	addcomd 10238	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
282	279, 281	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
283	275, 282	breqtrrd 4681	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
284	98, 192	readdcld 10069	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
285	52, 194	readdcld 10069	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
286	194, 190	readdcld 10069	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
287	286, 192	readdcld 10069	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
288		letr 10131	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
289	284, 285, 287, 288	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$
290	283, 289	mpan2d 710	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
291	290	imp 445	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
292	98, 190, 194	lesubaddd 10624	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
293	98, 286, 192	leadd1d 10621	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
294	292, 293	bitrd 268	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
295	294	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
296	291, 295	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
297	189, 296	eqbrtrrd 4677	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
298	297	ex 450	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
299	298	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
300	185, 299	sylbid 230	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
301	300	imp 445	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
302	301	an32s 846	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
303	302	adantr 481	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
304	175	oveq2d 6666	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
305	186	subidd 10380	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
306	305	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
307	304, 306	sylan9eqr 2678	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
308	307	pm2.24d 147	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
309	308	imp 445	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
310	309	an32s 846	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
311	168, 171, 303, 310	ifbothda 4123	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
312	157, 158, 165, 311	ifbothda 4123	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
313	156, 312	eqbrtrd 4675	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
314	313	ex 450	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
315	314	ralimdva 2962	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
316	122	a1i 11	. . . . . . . . . . . . 13
317		ovex 6678	. . . . . . . . . . . . . . 15
318	124, 317	ifex 4156	. . . . . . . . . . . . . 14
319	318	a1i 11	. . . . . . . . . . . . 13 $/\$
320	2	ffvelrnda 6359	. . . . . . . . . . . . . . 15 $/\$
321	51, 320	sseldi 3601	. . . . . . . . . . . . . 14 $/\$
322	159	ffvelrnda 6359	. . . . . . . . . . . . . . 15 $/\$
323	51, 322	sseldi 3601	. . . . . . . . . . . . . 14 $/\$
324	321, 323	readdcld 10069	. . . . . . . . . . . . 13 $/\$
325		eqidd 2623	. . . . . . . . . . . . 13
326	159	feqmptd 6249	. . . . . . . . . . . . . 14
327	316, 320, 322, 129, 326	offval2 6914	. . . . . . . . . . . . 13
328	316, 319, 324, 325, 327	ofrfval2 6915	. . . . . . . . . . . 12
329	328	ad2antrr 762	. . . . . . . . . . 11 $/\$ $/\$
330		ovex 6678	. . . . . . . . . . . . . . 15 $/\$
331	124, 330	ifex 4156	. . . . . . . . . . . . . 14 $/\$ $/\$
332	331	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
333		eqidd 2623	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
334	316, 332, 322, 333, 326	ofrfval2 6915	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
335	334	ad2antrr 762	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
336	315, 329, 335	3imtr4d 283	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
337	336	impr 649	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
338		oveq2 6658	. . . . . . . . . . . . 13 $/\$ $/\$
339	338	ifeq2d 4105	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
340	339	mpteq2dv 4745	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
341	340	breq1d 4663	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
342	341	rspcev 3309	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
343	140, 337, 342	syl2anc 693	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
344	36	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
345	51, 344	sseldi 3601	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
346	13	ad2antlr 763	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
347	345, 346	rerpdivcld 11903	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
348		reflcl 12597	. . . . . . . . . . . . . . . . . 18
349		peano2rem 10348	. . . . . . . . . . . . . . . . . 18
350	347, 348, 349	3syl 18	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
351	58	ad2antlr 763	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
352	350, 351	remulcld 10070	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
353	97	ffvelrnda 6359	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
354	352, 353	ifcld 4131	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
355	354	recnd 10068	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
356	353	recnd 10068	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
357	355, 356	pncan3d 10395	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
358	357	mpteq2dva 4744	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
359	353, 354	resubcld 10458	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
360		eqidd 2623	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
361	96	feqmptd 6249	. . . . . . . . . . . . . . 15
362	361	ad2antlr 763	. . . . . . . . . . . . . 14 $/\$ $/\$
363	123, 353, 354, 362, 360	offval2 6914	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
364	123, 354, 359, 360, 363	offval2 6914	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
365	358, 364, 362	3eqtr4d 2666	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
366	365	fveq2d 6195	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
367	3, 7	itg1add 23468	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
368	366, 367	eqtr3d 2658	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
369	368	adantrr 753	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
370		fvex 6201	. . . . . . . . 9 $/\$
371		fvex 6201	. . . . . . . . 9 $/\$
372		iba 524	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
373		iba 524	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
374	372, 373	bi2anan9 917	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
375	374	bicomd 213	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
376		oveq12 6659	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
377	376	eqeq2d 2632	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
378	375, 377	anbi12d 747	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
379	370, 371, 378	spc2ev 3301	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
380	139, 343, 369, 379	syl21anc 1325	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
381		fveq1 6190	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
382	381	eqeq1d 2624	. . . . . . . . . . . . . . . 16 $/\$ $/\$
383	381	oveq1d 6665	. . . . . . . . . . . . . . . 16 $/\$ $/\$
384	382, 383	ifbieq2d 4111	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
385	384	mpteq2dv 4745	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
386	385	breq1d 4663	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
387	386	rexbidv 3052	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
388		fveq2 6191	. . . . . . . . . . . . 13 $/\$ $/\$
389	388	eqeq2d 2632	. . . . . . . . . . . 12 $/\$ $/\$
390	387, 389	anbi12d 747	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
391	390	anbi1d 741	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
392	391	anbi1d 741	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
393	392	2exbidv 1852	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
394		fveq1 6190	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
395	394	eqeq1d 2624	. . . . . . . . . . . . . . . 16 $/\$ $/\$
396	394	oveq1d 6665	. . . . . . . . . . . . . . . 16 $/\$ $/\$
397	395, 396	ifbieq2d 4111	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
398	397	mpteq2dv 4745	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
399	398	breq1d 4663	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
400	399	rexbidv 3052	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
401		fveq2 6191	. . . . . . . . . . . . 13 $/\$ $/\$
402	401	eqeq2d 2632	. . . . . . . . . . . 12 $/\$ $/\$
403	400, 402	anbi12d 747	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
404	403	anbi2d 740	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
405	404	anbi1d 741	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
406	405	2exbidv 1852	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
407	393, 406	rspc2ev 3324	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
408	4, 8, 380, 407	syl3anc 1326	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
409		eqeq1 2626	. . . . . . . . 9
410	409	anbi2d 740	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
411	410	2exbidv 1852	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
412	411	2rexbidv 3057	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
413	408, 412	syl5ibrcom 237	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
414	413	rexlimdvaa 3032	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
415	414	impd 447	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
416	415	rexlimdva 3031	. 2 $/\$ $/\$ $/\$ $/\$ $/\$
417		rexcom4 3225	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
418	417	rexbii 3041	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
419		rexcom4 3225	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
420	418, 419	bitri 264	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
421		rexcom4 3225	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
422	421	rexbii 3041	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
423		rexcom4 3225	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
424	422, 423	bitri 264	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
425	424	exbii 1774	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
426		r19.41vv 3091	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
427	426	2exbii 1775	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
428	420, 425, 427	3bitrri 287	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
429	416, 428	syl6ibr 242	1 $/\$ $/\$ $/\$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $\/$ wo 383 $/\$ wa 384

wceq 1483

wex 1704

wcel 1990

wne 2794

wral 2912

wrex 2913

cvv 3200

cif 4086 class class class wbr 4653

cmpt 4729

cdm 5114

wfn 5883

wf 5884

cfv 5888 (class class class)co 6650

cof 6895

cofr 6896

cc 9934

cr 9935

cc0 9936

c1 9937

caddc 9939

cmul 9941

cpnf 10071

clt 10074

cle 10075

cmin 10266

cneg 10267

cdiv 10684

cn 11020

c2 11070

c3 11071

crp 11832

cico 12177

cfl 12591 MblFncmbf 23383

citg1 23384

citg2 23385

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014 ax-addf 10015

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-disj 4621 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-of 6897 df-ofr 6898 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-map 7859 df-pm 7860 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fi 8317 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-n0 11293 df-z 11378 df-uz 11688 df-q 11789 df-rp 11833 df-xneg 11946 df-xadd 11947 df-xmul 11948 df-ioo 12179 df-ico 12181 df-icc 12182 df-fz 12327 df-fzo 12466 df-fl 12593 df-seq 12802 df-exp 12861 df-hash 13118 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-clim 14219 df-sum 14417 df-rest 16083 df-topgen 16104 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-top 20699 df-topon 20716 df-bases 20750 df-cmp 21190 df-ovol 23233 df-vol 23234 df-mbf 23388 df-itg1 23389

This theorem is referenced by: itg2addnc 33464

W3C validator