Theorem ivthlem7OLD 7231

Description: Lemma for ivthOLD 7233: modus tollens case 2.

Hypotheses

Ref	Expression
ivthOLD.1	|- A e. RR
ivthOLD.2	|- B e. RR
ivthOLD.3	|- U e. RR
ivthOLD.4	|- A < B
ivthOLD.5	|- ((F` A) < U /\ U < (F` B))
ivthlem4OLD.6	|- C = sup(S, RR, < )
ivthlem4OLD.7	|- S = {c e. (A[,]B) | (F` c) <_ U}
ivthlem4OLD.8	|- F:(A[,]B)-->RR
ivthlem6OLD.9	|- (ph <-> D e. RR+)
ivthlem6OLD.10	|- (ps <-> A.w e. (A[,]B)((abs` (C - w)) < D -> U < (F` w)))
ivthlem6OLD.11	|- (ch <-> A.w e. (A[,]B)((abs` (C - w)) < D -> (F` w) < U))
ivthlem7OLD.12	|- P = if(B <_ (C + D), B, (C + D))

Assertion

Ref	Expression
ivthlem7OLD	|- -. (ph /\ ch)

Distinct variable groups:   w,c,A   B,c,w   w,C   w,D   F,c,w   w,S   U,c,w

Proof of Theorem ivthlem7OLD

Step	Hyp	Ref	Expression
1		pm3.26 319	. . . . . . . . 9 |- ((C < x /\ x < P) -> C < x)
2	1	a1i 8	. . . . . . . 8 |- ((x e. (A[,]B) /\ ph /\ ch) -> ((C < x /\ x < P) -> C < x))
3		opreq2 3954	. . . . . . . . . . . . . . . . . . . 20 |- (w = x -> (C - w) = (C - x))
4	3	fveq2d 3713	. . . . . . . . . . . . . . . . . . 19 |- (w = x -> (abs` (C - w)) = (abs` (C - x)))
5	4	breq1d 2619	. . . . . . . . . . . . . . . . . 18 |- (w = x -> ((abs` (C - w)) < D <-> (abs` (C - x)) < D))
6		fveq2 3709	. . . . . . . . . . . . . . . . . . 19 |- (w = x -> (F` w) = (F` x))
7	6	breq1d 2619	. . . . . . . . . . . . . . . . . 18 |- (w = x -> ((F` w) < U <-> (F` x) < U))
8	5, 7	imbi12d 624	. . . . . . . . . . . . . . . . 17 |- (w = x -> (((abs` (C - w)) < D -> (F` w) < U) <-> ((abs` (C - x)) < D -> (F` x) < U)))
9	8	rcla4v 1864	. . . . . . . . . . . . . . . 16 |- (x e. (A[,]B) -> (A.w e. (A[,]B)((abs` (C - w)) < D -> (F` w) < U) -> ((abs` (C - x)) < D -> (F` x) < U)))
10		ivthlem6OLD.11	. . . . . . . . . . . . . . . 16 |- (ch <-> A.w e. (A[,]B)((abs` (C - w)) < D -> (F` w) < U))
11	9, 10	syl5ib 206	. . . . . . . . . . . . . . 15 |- (x e. (A[,]B) -> (ch -> ((abs` (C - x)) < D -> (F` x) < U)))
12	11	adantr 389	. . . . . . . . . . . . . 14 |- ((x e. (A[,]B) /\ ph) -> (ch -> ((abs` (C - x)) < D -> (F` x) < U)))
13	12	3impia 828	. . . . . . . . . . . . 13 |- ((x e. (A[,]B) /\ ph /\ ch) -> ((abs` (C - x)) < D -> (F` x) < U))
14		ivthOLD.1	. . . . . . . . . . . . . . . . . . . . . . . 24 |- A e. RR
15		ivthOLD.2	. . . . . . . . . . . . . . . . . . . . . . . 24 |- B e. RR
16		elicc2t 6324	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((A e. RR /\ B e. RR) -> (x e. (A[,]B) <-> (x e. RR /\ A <_ x /\ x <_ B)))
17	14, 15, 16	mp2an 695	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x e. (A[,]B) <-> (x e. RR /\ A <_ x /\ x <_ B))
18	17	biimp 151	. . . . . . . . . . . . . . . . . . . . . 22 |- (x e. (A[,]B) -> (x e. RR /\ A <_ x /\ x <_ B))
19	18	3simp1d 792	. . . . . . . . . . . . . . . . . . . . 21 |- (x e. (A[,]B) -> x e. RR)
20	19	recnd 5287	. . . . . . . . . . . . . . . . . . . 20 |- (x e. (A[,]B) -> x e. CC)
21		ivthOLD.3	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- U e. RR
22		ivthOLD.4	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- A < B
23		ivthOLD.5	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((F` A) < U /\ U < (F` B))
24		ivthlem4OLD.6	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- C = sup(S, RR, < )
25		ivthlem4OLD.7	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- S = {c e. (A[,]B) | (F` c) <_ U}
26		ivthlem4OLD.8	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- F:(A[,]B)-->RR
27	14, 15, 21, 22, 23, 24, 25, 26	ivthlem5OLD 7229	. . . . . . . . . . . . . . . . . . . . . . . 24 |- C e. (A[,]B)
28		elicc2t 6324	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((A e. RR /\ B e. RR) -> (C e. (A[,]B) <-> (C e. RR /\ A <_ C /\ C <_ B)))
29	14, 15, 28	mp2an 695	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (C e. (A[,]B) <-> (C e. RR /\ A <_ C /\ C <_ B))
30	27, 29	mpbi 189	. . . . . . . . . . . . . . . . . . . . . . 23 |- (C e. RR /\ A <_ C /\ C <_ B)
31	30	3simp1i 789	. . . . . . . . . . . . . . . . . . . . . 22 |- C e. RR
32	31	recn 5286	. . . . . . . . . . . . . . . . . . . . 21 |- C e. CC
33		abssubt 6832	. . . . . . . . . . . . . . . . . . . . 21 |- ((x e. CC /\ C e. CC) -> (abs` (x - C)) = (abs` (C - x)))
34	32, 33	mpan2 694	. . . . . . . . . . . . . . . . . . . 20 |- (x e. CC -> (abs` (x - C)) = (abs` (C - x)))
35	20, 34	syl 10	. . . . . . . . . . . . . . . . . . 19 |- (x e. (A[,]B) -> (abs` (x - C)) = (abs` (C - x)))
36	35	adantr 389	. . . . . . . . . . . . . . . . . 18 |- ((x e. (A[,]B) /\ ph) -> (abs` (x - C)) = (abs` (C - x)))
37	36	breq1d 2619	. . . . . . . . . . . . . . . . 17 |- ((x e. (A[,]B) /\ ph) -> ((abs` (x - C)) < D <-> (abs` (C - x)) < D))
38		absdifltt 6821	. . . . . . . . . . . . . . . . . . 19 |- ((x e. RR /\ C e. RR /\ D e. RR) -> ((abs` (x - C)) < D <-> ((C - D) < x /\ x < (C + D))))
39	31, 38	mp3an2 901	. . . . . . . . . . . . . . . . . 18 |- ((x e. RR /\ D e. RR) -> ((abs` (x - C)) < D <-> ((C - D) < x /\ x < (C + D))))
40		ivthlem6OLD.9	. . . . . . . . . . . . . . . . . . 19 |- (ph <-> D e. RR+)
41		rpret 6222	. . . . . . . . . . . . . . . . . . 19 |- (D e. RR+ -> D e. RR)
42	40, 41	sylbi 199	. . . . . . . . . . . . . . . . . 18 |- (ph -> D e. RR)
43	39, 19, 42	syl2an 454	. . . . . . . . . . . . . . . . 17 |- ((x e. (A[,]B) /\ ph) -> ((abs` (x - C)) < D <-> ((C - D) < x /\ x < (C + D))))
44	37, 43	bitr3d 528	. . . . . . . . . . . . . . . 16 |- ((x e. (A[,]B) /\ ph) -> ((abs` (C - x)) < D <-> ((C - D) < x /\ x < (C + D))))
45	44	imbi1d 611	. . . . . . . . . . . . . . 15 |- ((x e. (A[,]B) /\ ph) -> (((abs` (C - x)) < D -> (F` x) < U) <-> (((C - D) < x /\ x < (C + D)) -> (F` x) < U)))
46	45	biimpd 153	. . . . . . . . . . . . . 14 |- ((x e. (A[,]B) /\ ph) -> (((abs` (C - x)) < D -> (F` x) < U) -> (((C - D) < x /\ x < (C + D)) -> (F` x) < U)))
47	46	3adant3 797	. . . . . . . . . . . . 13 |- ((x e. (A[,]B) /\ ph /\ ch) -> (((abs` (C - x)) < D -> (F` x) < U) -> (((C - D) < x /\ x < (C + D)) -> (F` x) < U)))
48	13, 47	mpd 26	. . . . . . . . . . . 12 |- ((x e. (A[,]B) /\ ph /\ ch) -> (((C - D) < x /\ x < (C + D)) -> (F` x) < U))
49		elrp 6220	. . . . . . . . . . . . . . . . . . 19 |- (D e. RR+ <-> (D e. RR /\ 0 < D))
50	49	pm3.27bi 326	. . . . . . . . . . . . . . . . . 18 |- (D e. RR+ -> 0 < D)
51	32	subid 5363	. . . . . . . . . . . . . . . . . . . . 21 |- (C - C) = 0
52	51	fveq2i 3712	. . . . . . . . . . . . . . . . . . . 20 |- (abs` (C - C)) = (abs` 0)
53		abs0 6814	. . . . . . . . . . . . . . . . . . . 20 |- (abs` 0) = 0
54	52, 53	eqtr 1487	. . . . . . . . . . . . . . . . . . 19 |- (abs` (C - C)) = 0
55	54	breq1i 2616	. . . . . . . . . . . . . . . . . 18 |- ((abs` (C - C)) < D <-> 0 < D)
56	50, 40, 55	3imtr4 219	. . . . . . . . . . . . . . . . 17 |- (ph -> (abs` (C - C)) < D)
57		absdifltt 6821	. . . . . . . . . . . . . . . . . 18 |- ((C e. RR /\ C e. RR /\ D e. RR) -> ((abs` (C - C)) < D <-> ((C - D) < C /\ C < (C + D))))
58	31	a1i 8	. . . . . . . . . . . . . . . . . 18 |- (ph -> C e. RR)
59	57, 58, 58, 42	syl3anc 856	. . . . . . . . . . . . . . . . 17 |- (ph -> ((abs` (C - C)) < D <-> ((C - D) < C /\ C < (C + D))))
60	56, 59	mpbid 195	. . . . . . . . . . . . . . . 16 |- (ph -> ((C - D) < C /\ C < (C + D)))
61	60	pm3.26d 321	. . . . . . . . . . . . . . 15 |- (ph -> (C - D) < C)
62	61	adantl 388	. . . . . . . . . . . . . 14 |- ((x e. (A[,]B) /\ ph) -> (C - D) < C)
63		axlttrn 5476	. . . . . . . . . . . . . . . . 17 |- (((C - D) e. RR /\ C e. RR /\ x e. RR) -> (((C - D) < C /\ C < x) -> (C - D) < x))
64	31, 63	mp3an2 901	. . . . . . . . . . . . . . . 16 |- (((C - D) e. RR /\ x e. RR) -> (((C - D) < C /\ C < x) -> (C - D) < x))
65		resubclt 5410	. . . . . . . . . . . . . . . . 17 |- ((C e. RR /\ D e. RR) -> (C - D) e. RR)
66	65, 58, 42	sylanc 471	. . . . . . . . . . . . . . . 16 |- (ph -> (C - D) e. RR)
67	64, 66, 19	syl2an 454	. . . . . . . . . . . . . . 15 |- ((ph /\ x e. (A[,]B)) -> (((C - D) < C /\ C < x) -> (C - D) < x))
68	67	ancoms 436	. . . . . . . . . . . . . 14 |- ((x e. (A[,]B) /\ ph) -> (((C - D) < C /\ C < x) -> (C - D) < x))
69	62, 68	mpand 699	. . . . . . . . . . . . 13 |- ((x e. (A[,]B) /\