Metamath Proof Explorer

Theorem lgamgulmlem1

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

Ref Expression
Hypotheses lgamgulm.r ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
lgamgulm.u ⊢ 𝑈 = { 𝑥 ∈ ℂ ∣ ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) }
Assertion lgamgulmlem1 ( 𝜑 → 𝑈 ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )

Proof

Step Hyp Ref Expression
1 lgamgulm.r ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
2 lgamgulm.u ⊢ 𝑈 = { 𝑥 ∈ ℂ ∣ ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) }
3 simp2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) ) → 𝑥 ∈ ℂ )
4 1 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) ) → 𝑅 ∈ ℕ )
5 4 nnred ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) ) → 𝑅 ∈ ℝ )
6 4 nngt0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) ) → 0 < 𝑅 )
7 5 6 recgt0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) ) → 0 < ( 1 / 𝑅 ) )
8 0red ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) ) → 0 ∈ ℝ )
9 4 nnrecred ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) ) → ( 1 / 𝑅 ) ∈ ℝ )
10 8 9 ltnled ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) ) → ( 0 < ( 1 / 𝑅 ) ↔ ¬ ( 1 / 𝑅 ) ≤ 0 ) )
11 7 10 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) ) → ¬ ( 1 / 𝑅 ) ≤ 0 )
12 oveq2 ⊢ ( 𝑘 = - 𝑥 → ( 𝑥 + 𝑘 ) = ( 𝑥 + - 𝑥 ) )
13 12 fveq2d ⊢ ( 𝑘 = - 𝑥 → ( abs ‘ ( 𝑥 + 𝑘 ) ) = ( abs ‘ ( 𝑥 + - 𝑥 ) ) )
14 13 breq2d ⊢ ( 𝑘 = - 𝑥 → ( ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ↔ ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + - 𝑥 ) ) ) )
15 14 rspccv ⊢ ( ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) → ( - 𝑥 ∈ ℕ0 → ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + - 𝑥 ) ) ) )
16 15 adantl ⊢ ( ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) → ( - 𝑥 ∈ ℕ0 → ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + - 𝑥 ) ) ) )
17 16 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) ) → ( - 𝑥 ∈ ℕ0 → ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + - 𝑥 ) ) ) )
18 3 negidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) ) → ( 𝑥 + - 𝑥 ) = 0 )
19 18 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) ) → ( abs ‘ ( 𝑥 + - 𝑥 ) ) = ( abs ‘ 0 ) )
20 abs0 ⊢ ( abs ‘ 0 ) = 0
21 19 20 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) ) → ( abs ‘ ( 𝑥 + - 𝑥 ) ) = 0 )
22 21 breq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) ) → ( ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + - 𝑥 ) ) ↔ ( 1 / 𝑅 ) ≤ 0 ) )
23 17 22 sylibd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) ) → ( - 𝑥 ∈ ℕ0 → ( 1 / 𝑅 ) ≤ 0 ) )
24 11 23 mtod ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) ) → ¬ - 𝑥 ∈ ℕ0 )
25 eldmgm ⊢ ( 𝑥 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ↔ ( 𝑥 ∈ ℂ ∧ ¬ - 𝑥 ∈ ℕ0 ) )
26 3 24 25 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ∧ ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) ) → 𝑥 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
27 26 rabssdv ⊢ ( 𝜑 → { 𝑥 ∈ ℂ ∣ ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) } ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
28 2 27 eqsstrid ⊢ ( 𝜑 → 𝑈 ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )