HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem ivthlem7 7222
Description: Lemma for isupivth 7225: modus tollens case 2.
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
ivthlem7 |- -. (ph /\ ch)
Distinct variable groups:   A,c,w   B,c,w   w,C   F,c,w   w,S   U,c,w   w,D
Proof of Theorem ivthlem7
StepHypRef Expression
1 pm3.26 319 . . . . . . . . 9 |- ((C < x /\ x < P) -> C < x)
21a1i 8 . . . . . . . 8 |- ((x e. (A[,]B) /\ ph /\ ch) -> ((C < x /\ x < P) -> C < x))
3 opreq2 3954 . . . . . . . . . . . . . . . . . . . 20 |- (w = x -> (C - w) = (C - x))
43fveq2d 3713 . . . . . . . . . . . . . . . . . . 19 |- (w = x -> (abs` (C - w)) = (abs` (C - x)))
54breq1d 2619 . . . . . . . . . . . . . . . . . 18 |- (w = x -> ((abs` (C - w)) < D <-> (abs` (C - x)) < D))
6 fveq2 3709 . . . . . . . . . . . . . . . . . . 19 |- (w = x -> (F` w) = (F` x))
76breq1d 2619 . . . . . . . . . . . . . . . . . 18 |- (w = x -> ((F` w) < U <-> (F` x) < U))
85, 7imbi12d 624 . . . . . . . . . . . . . . . . 17 |- (w = x -> (((abs` (C - w)) < D -> (F` w) < U) <-> ((abs` (C - x)) < D -> (F` x) < U)))
98rcla4v 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 ivthlem6.11 . . . . . . . . . . . . . . . 16 |- (ch <-> A.w e. (A[,]B)((abs` (C - w)) < D -> (F` w) < U))
119, 10syl5ib 206 . . . . . . . . . . . . . . 15 |- (x e. (A[,]B) -> (ch -> ((abs` (C - x)) < D -> (F` x) < U)))
1211adantr 389 . . . . . . . . . . . . . 14 |- ((x e. (A[,]B) /\ ph) -> (ch -> ((abs` (C - x)) < D -> (F` x) < U)))
13123impia 828 . . . . . . . . . . . . 13 |- ((x e. (A[,]B) /\ ph /\ ch) -> ((abs` (C - x)) < D -> (F` x) < U))
14 ivthlem4.1 . . . . . . . . . . . . . . . . . . . . . . . 24 |- A e. RR
15 ivthlem4.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)))
1714, 15, 16mp2an 695 . . . . . . . . . . . . . . . . . . . . . . 23 |- (x e. (A[,]B) <-> (x e. RR /\ A <_ x /\ x <_ B))
1817biimp 151 . . . . . . . . . . . . . . . . . . . . . 22 |- (x e. (A[,]B) -> (x e. RR /\ A <_ x /\ x <_ B))
19183simp1d 792 . . . . . . . . . . . . . . . . . . . . 21 |- (x e. (A[,]B) -> x e. RR)
2019recnd 5287 . . . . . . . . . . . . . . . . . . . 20 |- (x e. (A[,]B) -> x e. CC)
21 ivthlem4.3 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- U e. RR
22 ivthlem4.4 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- A < B
23 ivthlem4.5 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((F` A) < U /\ U < (F` B))
24 ivthlem4.6 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- C = sup(S, RR, < )
25 ivthlem4.7 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- S = {c e. (A[,]B) | (F` c) <_ U}
26 ivthlem4.8 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- F e. ((A[,]B)-cn->RR)
2714, 15, 21, 22, 23, 24, 25, 26ivthlem5 7220 . . . . . . . . . . . . . . . . . . . . . . . 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)))
2914, 15, 28mp2an 695 . . . . . . . . . . . . . . . . . . . . . . . 24 |- (C e. (A[,]B) <-> (C e. RR /\ A <_ C /\ C <_ B))
3027, 29mpbi 189 . . . . . . . . . . . . . . . . . . . . . . 23 |- (C e. RR /\ A <_ C /\ C <_ B)
31303simp1i 789 . . . . . . . . . . . . . . . . . . . . . 22 |- C e. RR
3231recn 5286 . . . . . . . . . . . . . . . . . . . . 21 |- C e. CC
33 abssubt 6832 . . . . . . . . . . . . . . . . . . . . 21 |- ((x e. CC /\ C e. CC) -> (abs` (x - C)) = (abs` (C - x)))
3432, 33mpan2 694 . . . . . . . . . . . . . . . . . . . 20 |- (x e. CC -> (abs` (x - C)) = (abs` (C - x)))
3520, 34syl 10 . . . . . . . . . . . . . . . . . . 19 |- (x e. (A[,]B) -> (abs` (x - C)) = (abs` (C - x)))
3635adantr 389 . . . . . . . . . . . . . . . . . 18 |- ((x e. (A[,]B) /\ ph) -> (abs` (x - C)) = (abs` (C - x)))
3736breq1d 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))))
3931, 38mp3an2 901 . . . . . . . . . . . . . . . . . 18 |- ((x e. RR /\ D e. RR) -> ((abs` (x - C)) < D <-> ((C - D) < x /\ x < (C + D))))
40 ivthlem6.9 . . . . . . . . . . . . . . . . . . 19 |- (ph <-> D e. RR+)
41 rpret 6222 . . . . . . . . . . . . . . . . . . 19 |- (D e. RR+ -> D e. RR)
4240, 41sylbi 199 . . . . . . . . . . . . . . . . . 18 |- (ph -> D e. RR)
4339, 19, 42syl2an 454 . . . . . . . . . . . . . . . . 17 |- ((x e. (A[,]B) /\ ph) -> ((abs` (x - C)) < D <-> ((C - D) < x /\ x < (C + D))))
4437, 43bitr3d 528 . . . . . . . . . . . . . . . 16 |- ((x e. (A[,]B) /\ ph) -> ((abs` (C - x)) < D <-> ((C - D) < x /\ x < (C + D))))
4544imbi1d 611 . . . . . . . . . . . . . . 15 |- ((x e. (A[,]B) /\ ph) -> (((abs` (C - x)) < D -> (F` x) < U) <-> (((C - D) < x /\ x < (C + D)) -> (F` x) < U)))
4645biimpd 153 . . . . . . . . . . . . . 14 |- ((x e. (A[,]B) /\ ph) -> (((abs` (C - x)) < D -> (F` x) < U) -> (((C - D) < x /\ x < (C + D)) -> (F` x) < U)))
47463adant3 797 . . . . . . . . . . . . 13 |- ((x e. (A[,]B) /\ ph /\ ch) -> (((abs` (C - x)) < D -> (F` x) < U) -> (((C - D) < x /\ x < (C + D)) -> (F` x) < U)))
4813, 47mpd 26 . . . . . . . . . . . 12 |- ((x e. (A[,]B) /\ ph /\ ch) -> (((C - D) < x /\ x < (C + D)) -> (F` x) < U))
49 rpgt0t 6224 . . . . . . . . . . . . . . . . . . 19 |- (D e. RR+ -> 0 < D)
5040, 49sylbi 199 . . . . . . . . . . . . . . . . . 18 |- (ph -> 0 < D)
5132subid 5363 . . . . . . . . . . . . . . . . . . . 20 |- (C - C) = 0
5251fveq2i 3712 . . . . . . . . . . . . . . . . . . 19 |- (abs` (C - C)) = (abs` 0)
53 abs0 6814 . . . . . . . . . . . . . . . . . . 19 |- (abs` 0) = 0
5452, 53eqtr 1487 . . . . . . . . . . . . . . . . . 18 |- (abs` (C - C)) = 0
5550, 54syl5eqbr 2638 . . . . . . . . . . . . . . . . 17 |- (ph -> (abs` (C - C)) < D)
56 absdifltt 6821 . . . . . . . . . . . . . . . . . 18 |- ((C e. RR /\ C e. RR /\ D e. RR) -> ((abs` (C - C)) < D <-> ((C - D) < C /\ C < (C + D))))
5731a1i 8 . . . . . . . . . . . . . . . . . 18 |- (ph -> C e. RR)
5856, 57, 57, 42syl3anc 856 . . . . . . . . . . . . . . . . 17 |- (ph -> ((abs` (C - C)) < D <-> ((C - D) < C /\ C < (C + D))))
5955, 58mpbid 195 . . . . . . . . . . . . . . . 16 |- (ph -> ((C - D) < C /\ C < (C + D)))
6059pm3.26d 321 . . . . . . . . . . . . . . 15 |- (ph -> (C - D) < C)
6160adantl 388 . . . . . . . . . . . . . 14 |- ((x e. (A[,]B) /\ ph) -> (C - D) < C)
62 axlttrn 5476 . . . . . . . . . . . . . . . . 17 |- (((C - D) e. RR /\ C e. RR /\ x e. RR) -> (((C - D) < C /\ C < x) -> (C - D) < x))
6331, 62mp3an2 901 . . . . . . . . . . . . . . . 16 |- (((C - D) e. RR /\ x e. RR) -> (((C - D) < C /\ C < x) -> (C - D) < x))
64 resubclt 5410 . . . . . . . . . . . . . . . . 17 |- ((C e. RR /\ D e. RR) -> (C - D) e. RR)
6564, 57, 42sylanc 471 . . . . . . . . . . . . . . . 16 |- (ph -> (C - D) e. RR)
6663, 65, 19syl2an 454 . . . . . . . . . . . . . . 15 |- ((ph /\ x e. (A[,]B)) -> (((C - D) < C /\ C < x) -> (C - D) < x))
6766ancoms 436 . . . . . . . . . . . . . 14 |- ((x e. (A[,]B) /\ ph) -> (((C - D) < C /\ C < x) -> (C - D) < x))
6861, 67mpand 699 . . . . . . . . . . . . 13 |- ((x e. (A[,]B) /\ ph) -> (C < x -> (C - D) < x))
69683adant3 797 . . . . . . . . . . . 12 |- ((x e. (