Metamath Proof Explorer


Theorem metnrmlem1a

Description: Lemma for metnrm . (Contributed by Mario Carneiro, 14-Jan-2014) (Revised by Mario Carneiro, 4-Sep-2015)

Ref Expression
Hypotheses metdscn.f F=xXsupranySxDy*<
metdscn.j J=MetOpenD
metnrmlem.1 φD∞MetX
metnrmlem.2 φSClsdJ
metnrmlem.3 φTClsdJ
metnrmlem.4 φST=
Assertion metnrmlem1a φAT0<FAif1FA1FA+

Proof

Step Hyp Ref Expression
1 metdscn.f F=xXsupranySxDy*<
2 metdscn.j J=MetOpenD
3 metnrmlem.1 φD∞MetX
4 metnrmlem.2 φSClsdJ
5 metnrmlem.3 φTClsdJ
6 metnrmlem.4 φST=
7 6 adantr φATST=
8 inelcm ASATST
9 8 expcom ATASST
10 9 adantl φATASST
11 10 necon2bd φATST=¬AS
12 7 11 mpd φAT¬AS
13 eqcom 0=FAFA=0
14 3 adantr φATD∞MetX
15 4 adantr φATSClsdJ
16 eqid J=J
17 16 cldss SClsdJSJ
18 15 17 syl φATSJ
19 2 mopnuni D∞MetXX=J
20 14 19 syl φATX=J
21 18 20 sseqtrrd φATSX
22 5 adantr φATTClsdJ
23 16 cldss TClsdJTJ
24 22 23 syl φATTJ
25 24 20 sseqtrrd φATTX
26 simpr φATAT
27 25 26 sseldd φATAX
28 1 2 metdseq0 D∞MetXSXAXFA=0AclsJS
29 14 21 27 28 syl3anc φATFA=0AclsJS
30 13 29 syl5bb φAT0=FAAclsJS
31 cldcls SClsdJclsJS=S
32 15 31 syl φATclsJS=S
33 32 eleq2d φATAclsJSAS
34 30 33 bitrd φAT0=FAAS
35 12 34 mtbird φAT¬0=FA
36 1 metdsf D∞MetXSXF:X0+∞
37 14 21 36 syl2anc φATF:X0+∞
38 37 27 ffvelrnd φATFA0+∞
39 elxrge0 FA0+∞FA*0FA
40 39 simprbi FA0+∞0FA
41 38 40 syl φAT0FA
42 0xr 0*
43 eliccxr FA0+∞FA*
44 38 43 syl φATFA*
45 xrleloe 0*FA*0FA0<FA0=FA
46 42 44 45 sylancr φAT0FA0<FA0=FA
47 41 46 mpbid φAT0<FA0=FA
48 47 ord φAT¬0<FA0=FA
49 35 48 mt3d φAT0<FA
50 1xr 1*
51 ifcl 1*FA*if1FA1FA*
52 50 44 51 sylancr φATif1FA1FA*
53 1red φAT1
54 0lt1 0<1
55 breq2 1=if1FA1FA0<10<if1FA1FA
56 breq2 FA=if1FA1FA0<FA0<if1FA1FA
57 55 56 ifboth 0<10<FA0<if1FA1FA
58 54 49 57 sylancr φAT0<if1FA1FA
59 xrltle 0*if1FA1FA*0<if1FA1FA0if1FA1FA
60 42 52 59 sylancr φAT0<if1FA1FA0if1FA1FA
61 58 60 mpd φAT0if1FA1FA
62 xrmin1 1*FA*if1FA1FA1
63 50 44 62 sylancr φATif1FA1FA1
64 xrrege0 if1FA1FA*10if1FA1FAif1FA1FA1if1FA1FA
65 52 53 61 63 64 syl22anc φATif1FA1FA
66 65 58 elrpd φATif1FA1FA+
67 49 66 jca φAT0<FAif1FA1FA+