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 ⊆ ℂ ∖ ℤ ∖ ℕ