Theorem ivthlem6 7286

Description: Lemma for isupivth 7290: modus tollens case 1.

Hypotheses

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

Assertion

Ref	Expression
ivthlem6	|- -. (ph /\ ps)

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

Proof of Theorem ivthlem6

Step	Hyp	Ref	Expression
1		fveq2 3724	. . . . . . . . . . . . . 14 |- (c = x -> (F` c) = (F` x))
2	1	breq1d 2629	. . . . . . . . . . . . 13 |- (c = x -> ((F` c) <_ U <-> (F` x) <_ U))
3		ivthlem4.7	. . . . . . . . . . . . 13 |- S = {c e. (A[,]B) | (F` c) <_ U}
4	2, 3	elrab2 1907	. . . . . . . . . . . 12 |- (x e. S <-> (x e. (A[,]B) /\ (F` x) <_ U))
5	4	pm3.27bi 326	. . . . . . . . . . 11 |- (x e. S -> (F` x) <_ U)
6	4	pm3.26bi 322	. . . . . . . . . . . . 13 |- (x e. S -> x e. (A[,]B))
7		ivthlem4.1	. . . . . . . . . . . . . . . 16 |- A e. RR
8		ivthlem4.2	. . . . . . . . . . . . . . . 16 |- B e. RR
9		iccssret 6396	. . . . . . . . . . . . . . . 16 |- ((A e. RR /\ B e. RR) -> (A[,]B) (_ RR)
10	7, 8, 9	mp2an 697	. . . . . . . . . . . . . . 15 |- (A[,]B) (_ RR
11		axresscn 5268	. . . . . . . . . . . . . . 15 |- RR (_ CC
12	10, 11	sstri 2073	. . . . . . . . . . . . . 14 |- (A[,]B) (_ CC
13		ivthlem4.8	. . . . . . . . . . . . . 14 |- F e. ((A[,]B)-cn->RR)
14		cncffvelrn 7268	. . . . . . . . . . . . . 14 |- (((A[,]B) (_ CC /\ RR (_ CC /\ F e. ((A[,]B)-cn->RR)) -> (x e. (A[,]B) -> (F` x) e. RR))
15	12, 11, 13, 14	mp3an 916	. . . . . . . . . . . . 13 |- (x e. (A[,]B) -> (F` x) e. RR)
16	6, 15	syl 10	. . . . . . . . . . . 12 |- (x e. S -> (F` x) e. RR)
17		ivthlem4.3	. . . . . . . . . . . . 13 |- U e. RR
18		lenltt 5510	. . . . . . . . . . . . 13 |- (((F` x) e. RR /\ U e. RR) -> ((F` x) <_ U <-> -. U < (F` x)))
19	17, 18	mpan2 696	. . . . . . . . . . . 12 |- ((F` x) e. RR -> ((F` x) <_ U <-> -. U < (F` x)))
20	16, 19	syl 10	. . . . . . . . . . 11 |- (x e. S -> ((F` x) <_ U <-> -. U < (F` x)))
21	5, 20	mpbid 195	. . . . . . . . . 10 |- (x e. S -> -. U < (F` x))
22	21	3ad2ant1 800	. . . . . . . . 9 |- ((x e. S /\ ph /\ ps) -> -. U < (F` x))
23		ivthlem4.4	. . . . . . . . . . . . . . . . 17 |- A < B
24		ivthlem4.5	. . . . . . . . . . . . . . . . 17 |- ((F` A) < U /\ U < (F` B))
25		ivthlem4.6	. . . . . . . . . . . . . . . . 17 |- C = sup(S, RR, < )
26	7, 8, 17, 23, 24, 25, 3, 13	ivthlem4 7284	. . . . . . . . . . . . . . . 16 |- ((S (_ RR /\ S =/= (/) /\ E.v e. RR A.y e. S y <_ v) /\ A e. S)
27	26	pm3.26i 320	. . . . . . . . . . . . . . 15 |- (S (_ RR /\ S =/= (/) /\ E.v e. RR A.y e. S y <_ v)
28	27	suprubi 6062	. . . . . . . . . . . . . 14 |- (x e. S -> x <_ sup(S, RR, < ))
29	28, 25	syl6breqr 2655	. . . . . . . . . . . . 13 |- (x e. S -> x <_ C)
30	29	adantr 389	. . . . . . . . . . . 12 |- ((x e. S /\ ph) -> x <_ C)
31		ivthlem6.9	. . . . . . . . . . . . . . . . 17 |- (ph <-> D e. RR+)
32		rpgt0t 6286	. . . . . . . . . . . . . . . . 17 |- (D e. RR+ -> 0 < D)
33	31, 32	sylbi 199	. . . . . . . . . . . . . . . 16 |- (ph -> 0 < D)
34	7, 8, 17, 23, 24, 25, 3, 13	ivthlem5 7285	. . . . . . . . . . . . . . . . . . . . . 22 |- C e. (A[,]B)
35		elicc2t 6392	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((A e. RR /\ B e. RR) -> (C e. (A[,]B) <-> (C e. RR /\ A <_ C /\ C <_ B)))
36	7, 8, 35	mp2an 697	. . . . . . . . . . . . . . . . . . . . . 22 |- (C e. (A[,]B) <-> (C e. RR /\ A <_ C /\ C <_ B))
37	34, 36	mpbi 189	. . . . . . . . . . . . . . . . . . . . 21 |- (C e. RR /\ A <_ C /\ C <_ B)
38	37	3simp1i 791	. . . . . . . . . . . . . . . . . . . 20 |- C e. RR
39	38	recn 5314	. . . . . . . . . . . . . . . . . . 19 |- C e. CC
40	39	subid 5391	. . . . . . . . . . . . . . . . . 18 |- (C - C) = 0
41	40	fveq2i 3727	. . . . . . . . . . . . . . . . 17 |- (abs` (C - C)) = (abs` 0)
42		abs0 6877	. . . . . . . . . . . . . . . . 17 |- (abs` 0) = 0
43	41, 42	eqtr 1495	. . . . . . . . . . . . . . . 16 |- (abs` (C - C)) = 0
44	33, 43	syl5eqbr 2648	. . . . . . . . . . . . . . 15 |- (ph -> (abs` (C - C)) < D)
45		absdifltt 6883	. . . . . . . . . . . . . . . 16 |- ((C e. RR /\ C e. RR /\ D e. RR) -> ((abs` (C - C)) < D <-> ((C - D) < C /\ C < (C + D))))
46	38	a1i 8	. . . . . . . . . . . . . . . 16 |- (ph -> C e. RR)
47		rpret 6284	. . . . . . . . . . . . . . . . 17 |- (D e. RR+ -> D e. RR)
48	31, 47	sylbi 199	. . . . . . . . . . . . . . . 16 |- (ph -> D e. RR)
49	45, 46, 46, 48	syl3anc 858	. . . . . . . . . . . . . . 15 |- (ph -> ((abs` (C - C)) < D <-> ((C - D) < C /\ C < (C + D))))
50	44, 49	mpbid 195	. . . . . . . . . . . . . 14 |- (ph -> ((C - D) < C /\ C < (C + D)))
51	50	pm3.27d 325	. . . . . . . . . . . . 13 |- (ph -> C < (C + D))
52	51	adantl 388	. . . . . . . . . . . 12 |- ((x e. S /\ ph) -> C < (C + D))
53		lelttrt 5523	. . . . . . . . . . . . . 14 |- ((x e. RR /\ C e. RR /\ (C + D) e. RR) -> ((x <_ C /\ C < (C + D)) -> x < (C + D)))
54	38, 53	mp3an2 904	. . . . . . . . . . . . 13 |- ((x e. RR /\ (C + D) e. RR) -> ((x <_ C /\ C < (C + D)) -> x < (C + D)))
55		elicc2t 6392	. . . . . . . . . . . . . . . 16 |- ((A e. RR /\ B e. RR) -> (x e. (A[,]B) <-> (x e. RR /\ A <_ x /\ x <_ B)))
56	7, 8, 55	mp2an 697	. . . . . . . . . . . . . . 15 |- (x e. (A[,]B) <-> (x e. RR /\ A <_ x /\ x <_ B))
57	6, 56	sylib 198	. . . . . . . . . . . . . 14 |- (x e. S -> (x e. RR /\ A <_ x /\ x <_ B))
58	57	3simp1d 794	. . . . . . . . . . . . 13 |- (x e. S -> x e. RR)
59		axaddrcl 5272	. . . . . . . . . . . . . 14 |- ((C e. RR /\ D e. RR) -> (C + D) e. RR)
60	59, 46, 48	sylanc 471	. . . . . . . . . . . . 13 |- (ph -> (C + D) e. RR)
61	54, 58, 60	syl2an 454	. . . . . . . . . . . 12 |- ((x e. S /\ ph) -> ((x <_ C /\ C < (C + D)) -> x < (C + D)))
62	30, 52, 61	mp2and 703	. . . . . . . . . . 11 |- ((x e. S /\ ph) -> x < (C + D))
63	62	3adant3 799	. . . . . . . . . 10 |- ((x e. S /\ ph /\ ps) -> x < (C + D))
64		opreq2 3969	. . . . . . . . . . . . . . . . . . 19 |- (w = x -> (C - w) = (C - x))
65	64	fveq2d 3728	. . . . . . . . . . . . . . . . . 18 |- (w = x -> (abs` (C - w)) = (abs` (C - x)))
66	65	breq1d 2629	. . . . . . . . . . . . . . . . 17 |- (w = x -> ((abs` (C - w)) < D <-> (abs` (C - x)) < D))
67		fveq2 3724	. . . . . . . . . . . . . . . . . 18 |- (w = x -> (F` w) = (F` x))
68	67	breq2d 2630	. . . . . . . . . . . . . . . . 17 |- (w = x -> (U < (F` w) <-> U < (F` x)))
69	66, 68	imbi12d 626	. . . . . . . . . . . . . . . 16 |- (w = x -> (((abs` (C - w)) < D -> U < (F` w)) <-> ((abs` (C - x)) < D -> U < (F` x))))
70	69	rcla4v 1873	. . . . . . . . . . . . . . 15 |- (x e. (A[,]B) -> (A.w e. (A[,]B)((abs` (C - w)) < D -> U < (F` w)) -> ((abs` (C - x)) < D -> U < (F` x))))
71		ivthlem6.10	. . . . . . . . . . . . . . 15 |- (ps <-> A.w e. (A[,]B)((abs` (C - w)) < D -> U < (F` w)))
72	70, 71	syl5ib 206	. . . . . . . . . . . . . 14 |- (x e. (A[,]B) -> (ps -> ((abs` (C - x)) < D -> U < (F` x))))
73	72	adantr 389	. . . . . . . . . . . . 13 |- ((x e. (A[,]B) /\ ph) -> (ps -> ((abs` (C - x)) < D -> U < (F` x))))
74	73	3impia 830	. . . . . . . . . . . 12 |- ((x e. (A[,]B) /\ ph /\ ps) -> ((abs` (C - x)) < D -> U < (F` x)))
75	56	biimp 151	. . . . . . . . . . . . . . . . . . . . 21 |- (x e. (A[,]B) -> (x e. RR /\ A <_ x /\ x <_ B))
76	75	3simp1d 794	. . . . . . . . . . . . . . . . . . . 20 |- (x e. (A[,]B) -> x e. RR)
77	76	recnd 5315	. . . . . . . . . . . . . . . . . . 19 |- (x e. (A[,]B) -> x e. CC)
78		abssubt 6894	. . . . . . . . . . . . . . . . . . . 20 |- ((x e. CC /\ C e. CC) -> (abs` (x - C)) = (abs` (C - x)))
79	39, 78	mpan2 696	. . . . . . . . . . . . . . . . . . 19 |- (x e. CC -> (abs` (x - C)) = (abs` (C - x)))
80	77, 79	syl 10	. . . . . . . . . . . . . . . . . 18 |- (x e. (A[,]B) -> (abs` (x - C)) = (abs` (C - x)))
81	80	adantr 389	. . . . . . . . . . . . . . . . 17 |- ((x e. (A[,]B) /\ ph) -> (abs` (x - C)) = (abs` (C - x)))
82	81	breq1d 2629	. . . . . . . . . . . . . . . 16 |- ((x e. (A[,]B) /\ ph) -> ((abs` (x - C)) < D <-> (abs` (C - x)) < D))
83