Home

Hilbert Space Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem iintlem1 10476

Description: Lemma for iint 10478.

Assertion

Ref	Expression
iintlem1	(,)

Distinct variable groups:   ,   ,

---

Proof of Theorem iintlem1

Step	Hyp	Ref	Expression
1		eliin 2561	. . . . . . 7 (,) (,) (,)
2		absrpclt 6790	. . . . . . . . . . . . . . . 16
3		resubclt 5410	. . . . . . . . . . . . . . . . . . 19
4	3	ancoms 436	. . . . . . . . . . . . . . . . . 18
5	4	recnd 5287	. . . . . . . . . . . . . . . . 17
6	5	adantr 389	. . . . . . . . . . . . . . . 16
7		recnt 5285	. . . . . . . . . . . . . . . . . . . . . . 23
8		recnt 5285	. . . . . . . . . . . . . . . . . . . . . . 23
9	7, 8	anim12i 333	. . . . . . . . . . . . . . . . . . . . . 22
10	9	ancoms 436	. . . . . . . . . . . . . . . . . . . . 21
11		subeq0t 5375	. . . . . . . . . . . . . . . . . . . . 21
12	10, 11	syl 10	. . . . . . . . . . . . . . . . . . . 20
13	12	biimpd 153	. . . . . . . . . . . . . . . . . . 19
14	13	con3d 95	. . . . . . . . . . . . . . . . . 18
15	14	imp 350	. . . . . . . . . . . . . . . . 17
16		df-ne 1579	. . . . . . . . . . . . . . . . 17
17	15, 16	sylibr 200	. . . . . . . . . . . . . . . 16
18	2, 6, 17	sylanc 471	. . . . . . . . . . . . . . 15
19		elrp 6220	. . . . . . . . . . . . . . . 16
20		2re 5926	. . . . . . . . . . . . . . . 16
21		2pos 5936	. . . . . . . . . . . . . . . 16
22	19, 20, 21	mpbir2an 728	. . . . . . . . . . . . . . 15
23	18, 22	jctir 293	. . . . . . . . . . . . . 14
24		rpdivclt 6229	. . . . . . . . . . . . . 14
25	23, 24	syl 10	. . . . . . . . . . . . 13
26		simplr 413	. . . . . . . . . . . . . . . . . . . . . 22
27	26	ad2antrl 406	. . . . . . . . . . . . . . . . . . . . 21
28		simpll 412	. . . . . . . . . . . . . . . . . . . . . 22
29	28	ad2antrl 406	. . . . . . . . . . . . . . . . . . . . 21
30		0re 5412	. . . . . . . . . . . . . . . . . . . . . . . . 25
31		ltsubadd2t 5602	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
32		3simp2 787	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
33		ax0id 5253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
34	32, 8, 33	3syl 20	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
35	34	breq2d 2620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
36	31, 35	bitrd 526	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
37	36	biimpd 153	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
38	37	3exp 830	. . . . . . . . . . . . . . . . . . . . . . . . . 26
39	38	com13 33	. . . . . . . . . . . . . . . . . . . . . . . . 25
40	30, 39	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . 24
41	40	imp 350	. . . . . . . . . . . . . . . . . . . . . . 23
42	41	ad2antrr 404	. . . . . . . . . . . . . . . . . . . . . 22
43	42	impcom 351	. . . . . . . . . . . . . . . . . . . . 21
44	27, 29, 43	3jca 817	. . . . . . . . . . . . . . . . . . . 20
45		msra3 10475	. . . . . . . . . . . . . . . . . . . 20
46		orc 269	. . . . . . . . . . . . . . . . . . . 20
47	44, 45, 46	3syl 20	. . . . . . . . . . . . . . . . . . 19
48		leloet 5491	. . . . . . . . . . . . . . . . . . . 20
49		pm3.22 438	. . . . . . . . . . . . . . . . . . . . . . 23
50	49	ad2antrr 404	. . . . . . . . . . . . . . . . . . . . . 22
51	50	adantl 388	. . . . . . . . . . . . . . . . . . . . 21
52		msr3 10469	. . . . . . . . . . . . . . . . . . . . 21
53	51, 52	syl 10	. . . . . . . . . . . . . . . . . . . 20
54	48, 27, 53	sylanc 471	. . . . . . . . . . . . . . . . . . 19
55	47, 54	mpbird 196	. . . . . . . . . . . . . . . . . 18
56		xrlenltt 5473	. . . . . . . . . . . . . . . . . . 19
57