Metamath Proof Explorer


Theorem efopnlem1

Description: Lemma for efopn . (Contributed by Mario Carneiro, 23-Apr-2015) (Revised by Mario Carneiro, 8-Sep-2015)

Ref Expression
Assertion efopnlem1 R + R < π A 0 ball abs R A < π

Proof

Step Hyp Ref Expression
1 simpr R + R < π A 0 ball abs R A 0 ball abs R
2 rpxr R + R *
3 2 ad2antrr R + R < π A 0 ball abs R R *
4 eqid abs = abs
5 4 cnbl0 R * abs -1 0 R = 0 ball abs R
6 3 5 syl R + R < π A 0 ball abs R abs -1 0 R = 0 ball abs R
7 1 6 eleqtrrd R + R < π A 0 ball abs R A abs -1 0 R
8 absf abs :
9 ffn abs : abs Fn
10 elpreima abs Fn A abs -1 0 R A A 0 R
11 8 9 10 mp2b A abs -1 0 R A A 0 R
12 11 simplbi A abs -1 0 R A
13 7 12 syl R + R < π A 0 ball abs R A
14 13 imcld R + R < π A 0 ball abs R A
15 14 recnd R + R < π A 0 ball abs R A
16 15 abscld R + R < π A 0 ball abs R A
17 rpre R + R
18 17 ad2antrr R + R < π A 0 ball abs R R
19 pire π
20 19 a1i R + R < π A 0 ball abs R π
21 13 abscld R + R < π A 0 ball abs R A
22 absimle A A A
23 13 22 syl R + R < π A 0 ball abs R A A
24 11 simprbi A abs -1 0 R A 0 R
25 7 24 syl R + R < π A 0 ball abs R A 0 R
26 0re 0
27 elico2 0 R * A 0 R A 0 A A < R
28 26 3 27 sylancr R + R < π A 0 ball abs R A 0 R A 0 A A < R
29 25 28 mpbid R + R < π A 0 ball abs R A 0 A A < R
30 29 simp3d R + R < π A 0 ball abs R A < R
31 16 21 18 23 30 lelttrd R + R < π A 0 ball abs R A < R
32 simplr R + R < π A 0 ball abs R R < π
33 16 18 20 31 32 lttrd R + R < π A 0 ball abs R A < π