Metamath Proof Explorer


Theorem lgamgulmlem1

Description: Lemma for lgamgulm . (Contributed by Mario Carneiro, 3-Jul-2017)

Ref Expression
Hypotheses lgamgulm.r φ R
lgamgulm.u U = x | x R k 0 1 R x + k
Assertion lgamgulmlem1 φ U

Proof

Step Hyp Ref Expression
1 lgamgulm.r φ R
2 lgamgulm.u U = x | x R k 0 1 R x + k
3 simp2 φ x x R k 0 1 R x + k x
4 1 3ad2ant1 φ x x R k 0 1 R x + k R
5 4 nnred φ x x R k 0 1 R x + k R
6 4 nngt0d φ x x R k 0 1 R x + k 0 < R
7 5 6 recgt0d φ x x R k 0 1 R x + k 0 < 1 R
8 0red φ x x R k 0 1 R x + k 0
9 4 nnrecred φ x x R k 0 1 R x + k 1 R
10 8 9 ltnled φ x x R k 0 1 R x + k 0 < 1 R ¬ 1 R 0
11 7 10 mpbid φ x x R k 0 1 R x + k ¬ 1 R 0
12 oveq2 k = x x + k = x + x
13 12 fveq2d k = x x + k = x + x
14 13 breq2d k = x 1 R x + k 1 R x + x
15 14 rspccv k 0 1 R x + k x 0 1 R x + x
16 15 adantl x R k 0 1 R x + k x 0 1 R x + x
17 16 3ad2ant3 φ x x R k 0 1 R x + k x 0 1 R x + x
18 3 negidd φ x x R k 0 1 R x + k x + x = 0
19 18 fveq2d φ x x R k 0 1 R x + k x + x = 0
20 abs0 0 = 0
21 19 20 eqtrdi φ x x R k 0 1 R x + k x + x = 0
22 21 breq2d φ x x R k 0 1 R x + k 1 R x + x 1 R 0
23 17 22 sylibd φ x x R k 0 1 R x + k x 0 1 R 0
24 11 23 mtod φ x x R k 0 1 R x + k ¬ x 0
25 eldmgm x x ¬ x 0
26 3 24 25 sylanbrc φ x x R k 0 1 R x + k x
27 26 rabssdv φ x | x R k 0 1 R x + k
28 2 27 eqsstrid φ U