Metamath Proof Explorer


Theorem efif1olem3

Description: Lemma for efif1o . (Contributed by Mario Carneiro, 8-May-2015)

Ref Expression
Hypotheses efif1o.1 F = w D e i w
efif1o.2 C = abs -1 1
Assertion efif1olem3 φ x C x 1 1

Proof

Step Hyp Ref Expression
1 efif1o.1 F = w D e i w
2 efif1o.2 C = abs -1 1
3 simpr φ x C x C
4 3 2 eleqtrdi φ x C x abs -1 1
5 absf abs :
6 ffn abs : abs Fn
7 fniniseg abs Fn x abs -1 1 x x = 1
8 5 6 7 mp2b x abs -1 1 x x = 1
9 4 8 sylib φ x C x x = 1
10 9 simpld φ x C x
11 10 sqrtcld φ x C x
12 11 imcld φ x C x
13 absimle x x x
14 11 13 syl φ x C x x
15 10 sqsqrtd φ x C x 2 = x
16 15 fveq2d φ x C x 2 = x
17 2nn0 2 0
18 absexp x 2 0 x 2 = x 2
19 11 17 18 sylancl φ x C x 2 = x 2
20 9 simprd φ x C x = 1
21 16 19 20 3eqtr3d φ x C x 2 = 1
22 sq1 1 2 = 1
23 21 22 eqtr4di φ x C x 2 = 1 2
24 11 abscld φ x C x
25 11 absge0d φ x C 0 x
26 1re 1
27 0le1 0 1
28 sq11 x 0 x 1 0 1 x 2 = 1 2 x = 1
29 26 27 28 mpanr12 x 0 x x 2 = 1 2 x = 1
30 24 25 29 syl2anc φ x C x 2 = 1 2 x = 1
31 23 30 mpbid φ x C x = 1
32 14 31 breqtrd φ x C x 1
33 absle x 1 x 1 1 x x 1
34 12 26 33 sylancl φ x C x 1 1 x x 1
35 32 34 mpbid φ x C 1 x x 1
36 35 simpld φ x C 1 x
37 35 simprd φ x C x 1
38 neg1rr 1
39 38 26 elicc2i x 1 1 x 1 x x 1
40 12 36 37 39 syl3anbrc φ x C x 1 1