HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem ivthlem6OLD 7230
Description: Lemma for ivthOLD 7233: modus tollens case 1.
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))
Assertion
Ref Expression
ivthlem6OLD |- -. (ph /\ ps)
Distinct variable groups:   w,c,A   B,c,w   w,C   w,D   F,c,w   w,S   U,c,w
Proof of Theorem ivthlem6OLD
StepHypRef Expression
1 fveq2 3709 . . . . . . . . . . . . . 14 |- (c = x -> (F` c) = (F` x))
21breq1d 2619 . . . . . . . . . . . . 13 |- (c = x -> ((F` c) <_ U <-> (F` x) <_ U))
3 ivthlem4OLD.7 . . . . . . . . . . . . 13 |- S = {c e. (A[,]B) | (F` c) <_ U}
42, 3elrab2 1898 . . . . . . . . . . . 12 |- (x e. S <-> (x e. (A[,]B) /\ (F` x) <_ U))
54pm3.27bi 326 . . . . . . . . . . 11 |- (x e. S -> (F` x) <_ U)
64pm3.26bi 322 . . . . . . . . . . . . 13 |- (x e. S -> x e. (A[,]B))
7 ivthlem4OLD.8 . . . . . . . . . . . . . 14 |- F:(A[,]B)-->RR
87ffvelrni 3800 . . . . . . . . . . . . 13 |- (x e. (A[,]B) -> (F` x) e. RR)
96, 8syl 10 . . . . . . . . . . . 12 |- (x e. S -> (F` x) e. RR)
10 ivthOLD.3 . . . . . . . . . . . . 13 |- U e. RR
11 lenltt 5482 . . . . . . . . . . . . 13 |- (((F` x) e. RR /\ U e. RR) -> ((F` x) <_ U <-> -. U < (F` x)))
1210, 11mpan2 694 . . . . . . . . . . . 12 |- ((F` x) e. RR -> ((F` x) <_ U <-> -. U < (F` x)))
139, 12syl 10 . . . . . . . . . . 11 |- (x e. S -> ((F` x) <_ U <-> -. U < (F` x)))
145, 13mpbid 195 . . . . . . . . . 10 |- (x e. S -> -. U < (F` x))
15143ad2ant1 798 . . . . . . . . 9 |- ((x e. S /\ ph /\ ps) -> -. U < (F` x))
16 ivthOLD.1 . . . . . . . . . . . . . . . . 17 |- A e. RR
17 ivthOLD.2 . . . . . . . . . . . . . . . . 17 |- B e. RR
18 ivthOLD.4 . . . . . . . . . . . . . . . . 17 |- A < B
19 ivthOLD.5 . . . . . . . . . . . . . . . . 17 |- ((F` A) < U /\ U < (F` B))
20 ivthlem4OLD.6 . . . . . . . . . . . . . . . . 17 |- C = sup(S, RR, < )
2116, 17, 10, 18, 19, 20, 3, 7ivthlem4OLD 7228 . . . . . . . . . . . . . . . 16 |- ((S (_ RR /\ S =/= (/) /\ E.v e. RR A.y e. S y <_ v) /\ A e. S)
2221pm3.26i 320 . . . . . . . . . . . . . . 15 |- (S (_ RR /\ S =/= (/) /\ E.v e. RR A.y e. S y <_ v)
2322suprubi 6009 . . . . . . . . . . . . . 14 |- (x e. S -> x <_ sup(S, RR, < ))
2423, 20syl6breqr 2645 . . . . . . . . . . . . 13 |- (x e. S -> x <_ C)
2524adantr 389 . . . . . . . . . . . 12 |- ((x e. S /\ ph) -> x <_ C)
26 elrp 6220 . . . . . . . . . . . . . . . . 17 |- (D e. RR+ <-> (D e. RR /\ 0 < D))
2726pm3.27bi 326 . . . . . . . . . . . . . . . 16 |- (D e. RR+ -> 0 < D)
28 ivthlem6OLD.9 . . . . . . . . . . . . . . . 16 |- (ph <-> D e. RR+)
2916, 17, 10, 18, 19, 20, 3, 7ivthlem5OLD 7229 . . . . . . . . . . . . . . . . . . . . . . 23 |- C e. (A[,]B)
30 elicc2t 6324 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ((A e. RR /\ B e. RR) -> (C e. (A[,]B) <-> (C e. RR /\ A <_ C /\ C <_ B)))
3116, 17, 30mp2an 695 . . . . . . . . . . . . . . . . . . . . . . 23 |- (C e. (A[,]B) <-> (C e. RR /\ A <_ C /\ C <_ B))
3229, 31mpbi 189 . . . . . . . . . . . . . . . . . . . . . 22 |- (C e. RR /\ A <_ C /\ C <_ B)
33323simp1i 789 . . . . . . . . . . . . . . . . . . . . 21 |- C e. RR
3433recn 5286 . . . . . . . . . . . . . . . . . . . 20 |- C e. CC
3534subid 5363 . . . . . . . . . . . . . . . . . . 19 |- (C - C) = 0
3635fveq2i 3712 . . . . . . . . . . . . . . . . . 18 |- (abs` (C - C)) = (abs` 0)
37 abs0 6814 . . . . . . . . . . . . . . . . . 18 |- (abs` 0) = 0
3836, 37eqtr 1487 . . . . . . . . . . . . . . . . 17 |- (abs` (C - C)) = 0
3938breq1i 2616 . . . . . . . . . . . . . . . 16 |- ((abs` (C - C)) < D <-> 0 < D)
4027, 28, 393imtr4 219 . . . . . . . . . . . . . . 15 |- (ph -> (abs` (C - C)) < D)
41 absdifltt 6821 . . . . . . . . . . . . . . . 16 |- ((C e. RR /\ C e. RR /\ D e. RR) -> ((abs` (C - C)) < D <-> ((C - D) < C /\ C < (C + D))))
4233a1i 8 . . . . . . . . . . . . . . . 16 |- (ph -> C e. RR)
43 rpret 6222 . . . . . . . . . . . . . . . . 17 |- (D e. RR+ -> D e. RR)
4428, 43sylbi 199 . . . . . . . . . . . . . . . 16 |- (ph -> D e. RR)
4541, 42, 42, 44syl3anc 856 . . . . . . . . . . . . . . 15 |- (ph -> ((abs` (C - C)) < D <-> ((C - D) < C /\ C < (C + D))))
4640, 45mpbid 195 . . . . . . . . . . . . . 14 |- (ph -> ((C - D) < C /\ C < (C + D)))
4746pm3.27d 325 . . . . . . . . . . . . 13 |- (ph -> C < (C + D))
4847adantl 388 . . . . . . . . . . . 12 |- ((x e. S /\ ph) -> C < (C + D))
49 lelttrt 5496 . . . . . . . . . . . . . 14 |- ((x e. RR /\ C e. RR /\ (C + D) e. RR) -> ((x <_ C /\ C < (C + D)) -> x < (C + D)))
5033, 49mp3an2 901 . . . . . . . . . . . . 13 |- ((x e. RR /\ (C + D) e. RR) -> ((x <_ C /\ C < (C + D)) -> x < (C + D)))
51 elicc2t 6324 . . . . . . . . . . . . . . . 16 |- ((A e. RR /\ B e. RR) -> (x e. (A[,]B) <-> (x e. RR /\ A <_ x /\ x <_ B)))
5216, 17, 51mp2an 695 . . . . . . . . . . . . . . 15 |- (x e. (A[,]B) <-> (x e. RR /\ A <_ x /\ x <_ B))
536, 52sylib 198 . . . . . . . . . . . . . 14 |- (x e. S -> (x e. RR /\ A <_ x /\ x <_ B))
54533simp1d 792 . . . . . . . . . . . . 13 |- (x e. S -> x e. RR)
55 axaddrcl 5244 . . . . . . . . . . . . . 14 |- ((C e. RR /\ D e. RR) -> (C + D) e. RR)
5655, 42, 44sylanc 471 . . . . . . . . . . . . 13 |- (ph -> (C + D) e. RR)
5750, 54, 56syl2an 454 . . . . . . . . . . . 12 |- ((x e. S /\ ph) -> ((x <_ C /\ C < (C + D)) -> x < (C + D)))
5825, 48, 57mp2and 701 . . . . . . . . . . 11 |- ((x e. S /\ ph) -> x < (C + D))
59583adant3 797 . . . . . . . . . 10 |- ((x e. S /\ ph /\ ps) -> x < (C + D))
60 opreq2 3954 . . . . . . . . . . . . . . . . . . 19 |- (w = x -> (C - w) = (C - x))
6160fveq2d 3713 . . . . . . . . . . . . . . . . . 18 |- (w = x -> (abs` (C - w)) = (abs` (C - x)))
6261breq1d 2619 . . . . . . . . . . . . . . . . 17 |- (w = x -> ((abs` (C - w)) < D <-> (abs` (C - x)) < D))
63 fveq2 3709 . . . . . . . . . . . . . . . . . 18 |- (w = x -> (F` w) = (F` x))
6463breq2d 2620 . . . . . . . . . . . . . . . . 17 |- (w = x -> (U < (F` w) <-> U < (F` x)))
6562, 64imbi12d 624 . . . . . . . . . . . . . . . 16 |- (w = x -> (((abs` (C - w)) < D -> U < (F` w)) <-> ((abs` (C - x)) < D -> U < (F` x))))
6665rcla4v 1864 . . . . . . . . . . . . . . 15 |- (x e. (A[,]B) -> (A.w e. (A[,]B)((abs` (C - w)) < D -> U < (F` w)) -> ((abs` (C - x)) < D -> U < (F` x))))
67 ivthlem6OLD.10 . . . . . . . . . . . . . . 15 |- (ps <-> A.w e. (A[,]B)((abs` (C - w)) < D -> U < (F` w)))
6866, 67syl5ib 206 . . . . . . . . . . . . . 14 |- (x e. (A[,]B) -> (ps -> ((abs` (C - x)) < D -> U < (F` x))))
6968adantr 389 . . . . . . . . . . . . 13 |- ((x e. (A[,]B) /\ ph) -> (ps -> ((abs` (C - x)) < D -> U < (F` x))))
70693impia 828 . . . . . . . . . . . 12 |- ((x e. (A[,]B) /\ ph /\ ps) -> ((abs` (C - x)) < D -> U < (F` x)))
7152biimp 151 . . . . . . . . . . . . . . . . . . . . 21 |- (x e. (A[,]B) -> (x e. RR /\ A <_ x /\ x <_ B))
72713simp1d 792 . . . . . . . . . . . . . . . . . . . 20 |- (x e. (A[,]B) -> x e. RR)
7372recnd 5287 . . . . . . . . . . . . . . . . . . 19 |- (x e. (A[,]B) -> x e. CC)
74 abssubt 6832 . . . . . . . . . . . . . . . . . . . 20 |- ((x e. CC /\ C e. CC) -> (abs` (x - C)) = (abs` (C - x)))
7534, 74mpan2 694 . . . . . . . . . . . . . . . . . . 19 |- (x e. CC -> (abs` (x - C)) = (abs` (C - x)))
7673, 75syl 10 . . . . . . . . . . . . . . . . . 18 |- (x e. (A[,]B) -> (abs` (x - C)) = (abs` (C - x)))
7776adantr 389 . . . . . . . . . . . . . . . . 17 |- ((x e. (A[,]B) /\ ph) -> (abs` (x - C)) = (abs` (C - x)))
7877breq1d 2619 . . . . . . . . . . . . . . . 16 |- ((x e. (A[,]B) /\ ph) -> ((abs` (x - C)) < D <-> (abs` (C - x)) < D))
79 absdifltt 6821 . . . . . . . . . . . . . . . . . 18 |- ((x e. RR /\ C e. RR /\ D e. RR) -> ((abs` (x - C)) < D <-> ((C - D) < x /\ x < (C + D))))
8033, 79mp3an2 901 . . . . . . . . . . . . . . . . 17 |- ((x e. RR /\ D e. RR) -> ((abs` (x - C)) < D <-> ((C - D) < x /\ x < (C + D))