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∈ℕ01R≤x+k
Assertion lgamgulmlem1 ⊢φ→U⊆ℂ∖ℤ∖ℕ

Proof

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