Theorem iintlem1 10632

Description: Lemma for iint 10634.

Assertion

Ref	Expression
iintlem1	|- ((A e. RR /\ y e. |^|_x e. RR+ ((A - x)(,)(A + x))) -> (y e. RR -> y = A))

Distinct variable groups:   x,A   x,y

Proof of Theorem iintlem1

Step	Hyp	Ref	Expression
1		eliin 2571	. . . . . . 7 |- (y e. |^|_x e. RR+ ((A - x)(,)(A + x)) -> (y e. |^|_x e. RR+ ((A - x)(,)(A + x)) <-> A.x e. RR+ y e. ((A - x)(,)(A + x))))
2		absrpclt 6855	. . . . . . . . . . . . . . . 16 |- (((y - A) e. CC /\ (y - A) =/= 0) -> (abs` (y - A)) e. RR+)
3		resubclt 5438	. . . . . . . . . . . . . . . . . . 19 |- ((y e. RR /\ A e. RR) -> (y - A) e. RR)
4	3	ancoms 436	. . . . . . . . . . . . . . . . . 18 |- ((A e. RR /\ y e. RR) -> (y - A) e. RR)
5	4	recnd 5315	. . . . . . . . . . . . . . . . 17 |- ((A e. RR /\ y e. RR) -> (y - A) e. CC)
6	5	adantr 389	. . . . . . . . . . . . . . . 16 |- (((A e. RR /\ y e. RR) /\ -. y = A) -> (y - A) e. CC)
7		recnt 5313	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y e. RR -> y e. CC)
8		recnt 5313	. . . . . . . . . . . . . . . . . . . . . . 23 |- (A e. RR -> A e. CC)
9	7, 8	anim12i 333	. . . . . . . . . . . . . . . . . . . . . 22 |- ((y e. RR /\ A e. RR) -> (y e. CC /\ A e. CC))
10	9	ancoms 436	. . . . . . . . . . . . . . . . . . . . 21 |- ((A e. RR /\ y e. RR) -> (y e. CC /\ A e. CC))
11		subeq0t 5403	. . . . . . . . . . . . . . . . . . . . 21 |- ((y e. CC /\ A e. CC) -> ((y - A) = 0 <-> y = A))
12	10, 11	syl 10	. . . . . . . . . . . . . . . . . . . 20 |- ((A e. RR /\ y e. RR) -> ((y - A) = 0 <-> y = A))
13	12	biimpd 153	. . . . . . . . . . . . . . . . . . 19 |- ((A e. RR /\ y e. RR) -> ((y - A) = 0 -> y = A))
14	13	con3d 95	. . . . . . . . . . . . . . . . . 18 |- ((A e. RR /\ y e. RR) -> (-. y = A -> -. (y - A) = 0))
15	14	imp 350	. . . . . . . . . . . . . . . . 17 |- (((A e. RR /\ y e. RR) /\ -. y = A) -> -. (y - A) = 0)
16		df-ne 1587	. . . . . . . . . . . . . . . . 17 |- ((y - A) =/= 0 <-> -. (y - A) = 0)
17	15, 16	sylibr 200	. . . . . . . . . . . . . . . 16 |- (((A e. RR /\ y e. RR) /\ -. y = A) -> (y - A) =/= 0)
18	2, 6, 17	sylanc 471	. . . . . . . . . . . . . . 15 |- (((A e. RR /\ y e. RR) /\ -. y = A) -> (abs` (y - A)) e. RR+)
19		elrp 6282	. . . . . . . . . . . . . . . 16 |- (2 e. RR+ <-> (2 e. RR /\ 0 < 2))
20		2re 5979	. . . . . . . . . . . . . . . 16 |- 2 e. RR
21		2pos 5989	. . . . . . . . . . . . . . . 16 |- 0 < 2
22	19, 20, 21	mpbir2an 730	. . . . . . . . . . . . . . 15 |- 2 e. RR+
23	18, 22	jctir 293	. . . . . . . . . . . . . 14 |- (((A e. RR /\ y e. RR) /\ -. y = A) -> ((abs` (y - A)) e. RR+ /\ 2 e. RR+))
24		rpdivclt 6292	. . . . . . . . . . . . . 14 |- (((abs` (y - A)) e. RR+ /\ 2 e. RR+) -> ((abs` (y - A)) / 2) e. RR+)
25	23, 24	syl 10	. . . . . . . . . . . . 13 |- (((A e. RR /\ y e. RR) /\ -. y = A) -> ((abs` (y - A)) / 2) e. RR+)
26		simplr 413	. . . . . . . . . . . . . . . . . . . . . 22 |- (((A e. RR /\ y e. RR) /\ -. y = A) -> y e. RR)
27	26	ad2antrl 406	. . . . . . . . . . . . . . . . . . . . 21 |- (((y - A) < 0 /\ (((A e. RR /\ y e. RR) /\ -. y = A) /\ ((abs` (y - A)) / 2) e. RR+)) -> y e. RR)
28		simpll 412	. . . . . . . . . . . . . . . . . . . . . 22 |- (((A e. RR /\ y e. RR) /\ -. y = A) -> A e. RR)
29	28	ad2antrl 406	. . . . . . . . . . . . . . . . . . . . 21 |- (((y - A) < 0 /\ (((A e. RR /\ y e. RR) /\ -. y = A) /\ ((abs` (y - A)) / 2) e. RR+)) -> A e. RR)
30		0re 5440	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- 0 e. RR
31		ltsubadd2t 5628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((y e. RR /\ A e. RR /\ 0 e. RR) -> ((y - A) < 0 <-> y < (A + 0)))
32		3simp2 789	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((y e. RR /\ A e. RR /\ 0 e. RR) -> A e. RR)
33		ax0id 5281	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (A e. CC -> (A + 0) = A)
34	32, 8, 33	3syl 20	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((y e. RR /\ A e. RR /\ 0 e. RR) -> (A + 0) = A)
35	34	breq2d 2630	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((y e. RR /\ A e. RR /\ 0 e. RR) -> (y < (A + 0) <-> y < A))
36	31, 35	bitrd 528	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((y e. RR /\ A e. RR /\ 0 e. RR) -> ((y - A) < 0 <-> y < A))
37	36	biimpd 153	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((y e. RR /\ A e. RR /\ 0 e. RR) -> ((y - A) < 0 -> y < A))
38	37	3exp 832	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (y e. RR -> (A e. RR -> (0 e. RR -> ((y - A) < 0 -> y < A))))
39	38	com13 33	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (0 e. RR -> (A e. RR -> (y e. RR -> ((y - A) < 0 -> y < A))))
40	30, 39	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (A e. RR -> (y e. RR -> ((y - A) < 0 -> y < A)))
41	40	imp 350	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((A e. RR /\ y e. RR) -> ((y - A) < 0 -> y < A))
42	41	ad2antrr 404	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((A e. RR /\ y e. RR) /\ -. y = A) /\ ((abs` (y - A)) / 2) e. RR+) -> ((y - A) < 0 -> y < A))
43	42	impcom 351	. . . . . . . . . . . . . . . . . . . . 21 |- (((y - A) < 0 /\ (((A e. RR /\ y e. RR) /\ -. y = A) /\ ((abs` (y - A)) / 2) e. RR+)) -> y < A)
44	27, 29, 43	3jca 819	. . . . . . . . . . . . . . . . . . . 20 |- (((y - A) < 0 /\ (((A e. RR /\ y e. RR) /\ -. y = A) /\ ((abs` (y - A)) / 2) e. RR+)) -> (y e. RR /\ A e. RR /\ y < A))
45		msra3 10631	. . . . . . . . . . . . . . . . . . . 20 |- ((y e. RR /\ A e. RR /\ y < A) -> y < (A - ((abs` (y - A)) / 2)))
46		orc 269	. . . . . . . . . . . . . . . . . . . 20 |- (y < (A - ((abs` (y - A)) / 2)) -> (y < (A - ((abs` (y - A)) / 2)) \/ y = (A - ((abs` (y - A)) / 2))))
47	44, 45, 46	3syl 20	. . . . . . . . . . . . . . . . . . 19 |- (((y - A) < 0 /\ (((A e. RR /\ y e. RR) /\ -. y = A) /\ ((abs` (y - A)) / 2) e. RR+)) -> (y < (A - ((abs` (y - A)) / 2)) \/ y = (A - ((abs` (y - A)) / 2))))
48		leloet 5518	. . . . . . . . . . . . . . . . . . . 20 |- ((y e. RR /\ (A - ((abs` (y - A)) / 2)) e. RR) -> (y <_ (A - ((abs` (y - A)) / 2)) <-> (y < (A - ((abs` (y - A)) / 2)) \/ y = (A - ((abs` (y - A)) / 2)))))
49		pm3.22 438	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((A e. RR /\ y e. RR) -> (y e. RR /\ A e. RR))
50	49	ad2antrr 404	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((A e. RR /\ y e. RR) /\ -. y = A) /\ ((abs` (y - A)) / 2) e. RR+) -> (y e. RR /\ A e. RR))
51	50	adantl 388	. . . . . . . . . . . . . . . . . . . . 21 |- (((y - A) < 0 /\ (((A e. RR /\ y e. RR) /\ -. y = A) /\ ((abs` (y - A)) / 2) e. RR+)) -> (y e. RR /\ A e. RR))
52		msr3 10625	. . . . . . . . . . . . . . . . . . . . 21 |- ((y e. RR /\ A e. RR) -> (A - ((abs` (y - A)) / 2)) e. RR)
53	51, 52	syl 10	. . . . . . . . . . . . . . . . . . . 20 |- (((y - A) < 0 /\ (((A e. RR /\ y e. RR) /\ -. y = A) /\ ((abs` (y - A)) / 2) e. RR+)) -> (A - ((abs` (y - A)) / 2)) e. RR)
54	48, 27, 53	sylanc 471	. . . . . . . . . . . . . . . . . . 19 |- (((y - A) < 0 /\ (((A e. RR /\ y e. RR) /\ -. y = A) /\ ((abs` (y - A)) / 2) e. RR+)) -> (y <_ (A - ((abs` (y - A)) / 2)) <-> (y < (A - ((abs` (y - A)) / 2)) \/ y = (A - ((abs` (y - A)) / 2)))))
55	47, 54	mpbird 196	. . . . . . . . . . . . . . . . . 18 |- (((y - A) < 0 /\ (((A e. RR /\ y e. RR) /\ -. y = A) /\ ((abs` (y - A)) / 2) e. RR+)) -> y <_ (A - ((abs` (y - A)) / 2)))
56		xrlenltt 5501	. . . . . . . . . . . . . . . . . . 19 |- ((y e. RR* /\ (A - ((abs` (y - A)) / 2)) e. RR*) -> (y <_ (A - ((abs` (y - A)) / 2)) <-> -. (A - ((abs` (y - A)) / 2)) < y))