Metamath Proof Explorer


Theorem dvferm2lem

Description: Lemma for dvferm . (Contributed by Mario Carneiro, 24-Feb-2015)

Ref Expression
Hypotheses dvferm.a φF:X
dvferm.b φX
dvferm.u φUAB
dvferm.s φABX
dvferm.d φUdomF
dvferm2.r φyAUFyFU
dvferm2.z φFU<0
dvferm2.t φT+
dvferm2.l φzXUzUzU<TFzFUzUFU<FU
dvferm2.x S=ifAUTUTA+U2
Assertion dvferm2lem ¬φ

Proof

Step Hyp Ref Expression
1 dvferm.a φF:X
2 dvferm.b φX
3 dvferm.u φUAB
4 dvferm.s φABX
5 dvferm.d φUdomF
6 dvferm2.r φyAUFyFU
7 dvferm2.z φFU<0
8 dvferm2.t φT+
9 dvferm2.l φzXUzUzU<TFzFUzUFU<FU
10 dvferm2.x S=ifAUTUTA+U2
11 mnfxr −∞*
12 11 a1i φ−∞*
13 ioossre AB
14 13 3 sselid φU
15 8 rpred φT
16 14 15 resubcld φUT
17 16 rexrd φUT*
18 ne0i UABAB
19 ndmioo ¬A*B*AB=
20 19 necon1ai ABA*B*
21 3 18 20 3syl φA*B*
22 21 simpld φA*
23 17 22 ifcld φifAUTUTA*
24 14 rexrd φU*
25 16 mnfltd φ−∞<UT
26 xrmax2 A*UT*UTifAUTUTA
27 22 17 26 syl2anc φUTifAUTUTA
28 12 17 23 25 27 xrltletrd φ−∞<ifAUTUTA
29 14 8 ltsubrpd φUT<U
30 eliooord UABA<UU<B
31 3 30 syl φA<UU<B
32 31 simpld φA<U
33 breq1 UT=ifAUTUTAUT<UifAUTUTA<U
34 breq1 A=ifAUTUTAA<UifAUTUTA<U
35 33 34 ifboth UT<UA<UifAUTUTA<U
36 29 32 35 syl2anc φifAUTUTA<U
37 xrre2 −∞*ifAUTUTA*U*−∞<ifAUTUTAifAUTUTA<UifAUTUTA
38 12 23 24 28 36 37 syl32anc φifAUTUTA
39 38 14 readdcld φifAUTUTA+U
40 39 rehalfcld φifAUTUTA+U2
41 10 40 eqeltrid φS
42 avglt2 ifAUTUTAUifAUTUTA<UifAUTUTA+U2<U
43 38 14 42 syl2anc φifAUTUTA<UifAUTUTA+U2<U
44 36 43 mpbid φifAUTUTA+U2<U
45 10 44 eqbrtrid φS<U
46 41 45 ltned φSU
47 41 14 45 ltled φSU
48 41 14 47 abssuble0d φSU=US
49 avglt1 ifAUTUTAUifAUTUTA<UifAUTUTA<ifAUTUTA+U2
50 38 14 49 syl2anc φifAUTUTA<UifAUTUTA<ifAUTUTA+U2
51 36 50 mpbid φifAUTUTA<ifAUTUTA+U2
52 51 10 breqtrrdi φifAUTUTA<S
53 16 38 41 27 52 lelttrd φUT<S
54 14 15 41 53 ltsub23d φUS<T
55 48 54 eqbrtrd φSU<T
56 neeq1 z=SzUSU
57 fvoveq1 z=SzU=SU
58 57 breq1d z=SzU<TSU<T
59 56 58 anbi12d z=SzUzU<TSUSU<T
60 fveq2 z=SFz=FS
61 60 oveq1d z=SFzFU=FSFU
62 oveq1 z=SzU=SU
63 61 62 oveq12d z=SFzFUzU=FSFUSU
64 63 fvoveq1d z=SFzFUzUFU=FSFUSUFU
65 64 breq1d z=SFzFUzUFU<FUFSFUSUFU<FU
66 59 65 imbi12d z=SzUzU<TFzFUzUFU<FUSUSU<TFSFUSUFU<FU
67 21 simprd φB*
68 31 simprd φU<B
69 24 67 68 xrltled φUB
70 iooss2 B*UBAUAB
71 67 69 70 syl2anc φAUAB
72 71 4 sstrd φAUX
73 41 rexrd φS*
74 xrmax1 A*UT*AifAUTUTA
75 22 17 74 syl2anc φAifAUTUTA
76 22 23 73 75 52 xrlelttrd φA<S
77 elioo2 A*U*SAUSA<SS<U
78 22 24 77 syl2anc φSAUSA<SS<U
79 41 76 45 78 mpbir3and φSAU
80 72 79 sseldd φSX
81 eldifsn SXUSXSU
82 80 46 81 sylanbrc φSXU
83 66 9 82 rspcdva φSUSU<TFSFUSUFU<FU
84 46 55 83 mp2and φFSFUSUFU<FU
85 1 80 ffvelrnd φFS
86 4 3 sseldd φUX
87 1 86 ffvelrnd φFU
88 85 87 resubcld φFSFU
89 41 14 resubcld φSU
90 41 recnd φS
91 14 recnd φU
92 90 91 46 subne0d φSU0
93 88 89 92 redivcld φFSFUSU
94 dvfre F:XXF:domF
95 1 2 94 syl2anc φF:domF
96 95 5 ffvelrnd φFU
97 96 renegcld φFU
98 93 96 97 absdifltd φFSFUSUFU<FUFUFU<FSFUSUFSFUSU<FU+FU
99 84 98 mpbid φFUFU<FSFUSUFSFUSU<FU+FU
100 99 simprd φFSFUSU<FU+FU
101 96 recnd φFU
102 101 negidd φFU+FU=0
103 100 102 breqtrd φFSFUSU<0
104 93 lt0neg1d φFSFUSU<00<FSFUSU
105 103 104 mpbid φ0<FSFUSU
106 88 recnd φFSFU
107 89 recnd φSU
108 106 107 92 divneg2d φFSFUSU=FSFUSU
109 105 108 breqtrd φ0<FSFUSU
110 89 renegcld φSU
111 41 14 posdifd φS<U0<US
112 45 111 mpbid φ0<US
113 90 91 negsubdi2d φSU=US
114 112 113 breqtrrd φ0<SU
115 gt0div FSFUSU0<SU0<FSFU0<FSFUSU
116 88 110 114 115 syl3anc φ0<FSFU0<FSFUSU
117 109 116 mpbird φ0<FSFU
118 87 85 posdifd φFU<FS0<FSFU
119 117 118 mpbird φFU<FS
120 fveq2 y=SFy=FS
121 120 breq1d y=SFyFUFSFU
122 121 6 79 rspcdva φFSFU
123 85 87 122 lensymd φ¬FU<FS
124 119 123 pm2.65i ¬φ