Metamath Proof Explorer

Theorem dchrmusumlema

Description: Lemma for dchrmusum and dchrisumn0 . Apply dchrisum for the function 1 / y . (Contributed by Mario Carneiro, 4-May-2016)

Ref Expression
Hypotheses rpvmasum.z ⊢ Z = ℤ/Nℤ
rpvmasum.l ⊢ L = ℤRHom ⁡ Z
rpvmasum.a ⊢ φ → N ∈ ℕ
rpvmasum.g ⊢ G = DChr ⁡ N
rpvmasum.d ⊢ D = Base G
rpvmasum.1 ⊢ 1 ˙ = 0 G
dchrisum.b ⊢ φ → X ∈ D
dchrisum.n1 ⊢ φ → X ≠ 1 ˙
dchrisumn0.f ⊢ F = a ∈ ℕ ⟼ X ⁡ L ⁡ a a
Assertion dchrmusumlema ⊢ φ → ∃ t ∃ c ∈ 0 +∞ seq 1 + F ⇝ t ∧ ∀ y ∈ 1 +∞ seq 1 + F ⁡ y − t ≤ c y

Proof

Step Hyp Ref Expression
1 rpvmasum.z ⊢ Z = ℤ/Nℤ
2 rpvmasum.l ⊢ L = ℤRHom ⁡ Z
3 rpvmasum.a ⊢ φ → N ∈ ℕ
4 rpvmasum.g ⊢ G = DChr ⁡ N
5 rpvmasum.d ⊢ D = Base G
6 rpvmasum.1 ⊢ 1 ˙ = 0 G
7 dchrisum.b ⊢ φ → X ∈ D
8 dchrisum.n1 ⊢ φ → X ≠ 1 ˙
9 dchrisumn0.f ⊢ F = a ∈ ℕ ⟼ X ⁡ L ⁡ a a
10 oveq2 ⊢ n = x → 1 n = 1 x
11 1nn ⊢ 1 ∈ ℕ
12 11 a1i ⊢ φ → 1 ∈ ℕ
13 rpreccl ⊢ n ∈ ℝ + → 1 n ∈ ℝ +
14 13 adantl ⊢ φ ∧ n ∈ ℝ + → 1 n ∈ ℝ +
15 14 rpred ⊢ φ ∧ n ∈ ℝ + → 1 n ∈ ℝ
16 simp3r ⊢ φ ∧ n ∈ ℝ + ∧ x ∈ ℝ + ∧ 1 ≤ n ∧ n ≤ x → n ≤ x
17 rpregt0 ⊢ n ∈ ℝ + → n ∈ ℝ ∧ 0 < n
18 rpregt0 ⊢ x ∈ ℝ + → x ∈ ℝ ∧ 0 < x
19 lerec ⊢ n ∈ ℝ ∧ 0 < n ∧ x ∈ ℝ ∧ 0 < x → n ≤ x ↔ 1 x ≤ 1 n
20 17 18 19 syl2an ⊢ n ∈ ℝ + ∧ x ∈ ℝ + → n ≤ x ↔ 1 x ≤ 1 n
21 20 3ad2ant2 ⊢ φ ∧ n ∈ ℝ + ∧ x ∈ ℝ + ∧ 1 ≤ n ∧ n ≤ x → n ≤ x ↔ 1 x ≤ 1 n
22 16 21 mpbid ⊢ φ ∧ n ∈ ℝ + ∧ x ∈ ℝ + ∧ 1 ≤ n ∧ n ≤ x → 1 x ≤ 1 n
23 ax-1cn ⊢ 1 ∈ ℂ
24 divrcnv ⊢ 1 ∈ ℂ → n ∈ ℝ + ⟼ 1 n ⇝ℝ 0
25 23 24 mp1i ⊢ φ → n ∈ ℝ + ⟼ 1 n ⇝ℝ 0
26 2fveq3 ⊢ a = n → X ⁡ L ⁡ a = X ⁡ L ⁡ n
27 oveq2 ⊢ a = n → 1 a = 1 n
28 26 27 oveq12d ⊢ a = n → X ⁡ L ⁡ a ⁢ 1 a = X ⁡ L ⁡ n ⁢ 1 n
29 28 cbvmptv ⊢ a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ 1 a = n ∈ ℕ ⟼ X ⁡ L ⁡ n ⁢ 1 n
30 1 2 3 4 5 6 7 8 10 12 15 22 25 29 dchrisum ⊢ φ → ∃ t ∃ c ∈ 0 +∞ seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ 1 a ⇝ t ∧ ∀ x ∈ 1 +∞ seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ 1 a ⁡ x − t ≤ c ⁢ 1 x
31 7 adantr ⊢ φ ∧ n ∈ ℕ → X ∈ D
32 nnz ⊢ n ∈ ℕ → n ∈ ℤ
33 32 adantl ⊢ φ ∧ n ∈ ℕ → n ∈ ℤ
34 4 1 5 2 31 33 dchrzrhcl ⊢ φ ∧ n ∈ ℕ → X ⁡ L ⁡ n ∈ ℂ
35 nncn ⊢ n ∈ ℕ → n ∈ ℂ
36 35 adantl ⊢ φ ∧ n ∈ ℕ → n ∈ ℂ
37 nnne0 ⊢ n ∈ ℕ → n ≠ 0
38 37 adantl ⊢ φ ∧ n ∈ ℕ → n ≠ 0
39 34 36 38 divrecd ⊢ φ ∧ n ∈ ℕ → X ⁡ L ⁡ n n = X ⁡ L ⁡ n ⁢ 1 n
40 39 mpteq2dva ⊢ φ → n ∈ ℕ ⟼ X ⁡ L ⁡ n n = n ∈ ℕ ⟼ X ⁡ L ⁡ n ⁢ 1 n
41 id ⊢ a = n → a = n
42 26 41 oveq12d ⊢ a = n → X ⁡ L ⁡ a a = X ⁡ L ⁡ n n
43 42 cbvmptv ⊢ a ∈ ℕ ⟼ X ⁡ L ⁡ a a = n ∈ ℕ ⟼ X ⁡ L ⁡ n n
44 9 43 eqtri ⊢ F = n ∈ ℕ ⟼ X ⁡ L ⁡ n n
45 40 44 29 3eqtr4g ⊢ φ → F = a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ 1 a
46 45 adantr ⊢ φ ∧ c ∈ 0 +∞ → F = a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ 1 a
47 46 seqeq3d ⊢ φ ∧ c ∈ 0 +∞ → seq 1 + F = seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ 1 a
48 47 breq1d ⊢ φ ∧ c ∈ 0 +∞ → seq 1 + F ⇝ t ↔ seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ 1 a ⇝ t
49 2fveq3 ⊢ y = x → seq 1 + F ⁡ y = seq 1 + F ⁡ x
50 49 fvoveq1d ⊢ y = x → seq 1 + F ⁡ y − t = seq 1 + F ⁡ x − t
51 oveq2 ⊢ y = x → c y = c x
52 50 51 breq12d ⊢ y = x → seq 1 + F ⁡ y − t ≤ c y ↔ seq 1 + F ⁡ x − t ≤ c x
53 52 cbvralvw ⊢ ∀ y ∈ 1 +∞ seq 1 + F ⁡ y − t ≤ c y ↔ ∀ x ∈ 1 +∞ seq 1 + F ⁡ x − t ≤ c x
54 45 seqeq3d ⊢ φ → seq 1 + F = seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ 1 a
55 54 fveq1d ⊢ φ → seq 1 + F ⁡ x = seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ 1 a ⁡ x
56 55 fvoveq1d ⊢ φ → seq 1 + F ⁡ x − t = seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ 1 a ⁡ x − t
57 56 ad2antrr ⊢ φ ∧ c ∈ 0 +∞ ∧ x ∈ 1 +∞ → seq 1 + F ⁡ x − t = seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ 1 a ⁡ x − t
58 elrege0 ⊢ c ∈ 0 +∞ ↔ c ∈ ℝ ∧ 0 ≤ c
59 58 simplbi ⊢ c ∈ 0 +∞ → c ∈ ℝ
60 59 recnd ⊢ c ∈ 0 +∞ → c ∈ ℂ
61 60 ad2antlr ⊢ φ ∧ c ∈ 0 +∞ ∧ x ∈ 1 +∞ → c ∈ ℂ
62 1re ⊢ 1 ∈ ℝ
63 elicopnf ⊢ 1 ∈ ℝ → x ∈ 1 +∞ ↔ x ∈ ℝ ∧ 1 ≤ x
64 62 63 ax-mp ⊢ x ∈ 1 +∞ ↔ x ∈ ℝ ∧ 1 ≤ x
65 64 simplbi ⊢ x ∈ 1 +∞ → x ∈ ℝ
66 65 adantl ⊢ φ ∧ c ∈ 0 +∞ ∧ x ∈ 1 +∞ → x ∈ ℝ
67 66 recnd ⊢ φ ∧ c ∈ 0 +∞ ∧ x ∈ 1 +∞ → x ∈ ℂ
68 0red ⊢ φ ∧ c ∈ 0 +∞ ∧ x ∈ 1 +∞ → 0 ∈ ℝ
69 1red ⊢ φ ∧ c ∈ 0 +∞ ∧ x ∈ 1 +∞ → 1 ∈ ℝ
70 0lt1 ⊢ 0 < 1
71 70 a1i ⊢ φ ∧ c ∈ 0 +∞ ∧ x ∈ 1 +∞ → 0 < 1
72 64 simprbi ⊢ x ∈ 1 +∞ → 1 ≤ x
73 72 adantl ⊢ φ ∧ c ∈ 0 +∞ ∧ x ∈ 1 +∞ → 1 ≤ x
74 68 69 66 71 73 ltletrd ⊢ φ ∧ c ∈ 0 +∞ ∧ x ∈ 1 +∞ → 0 < x
75 74 gt0ne0d ⊢ φ ∧ c ∈ 0 +∞ ∧ x ∈ 1 +∞ → x ≠ 0
76 61 67 75 divrecd ⊢ φ ∧ c ∈ 0 +∞ ∧ x ∈ 1 +∞ → c x = c ⁢ 1 x
77 57 76 breq12d ⊢ φ ∧ c ∈ 0 +∞ ∧ x ∈ 1 +∞ → seq 1 + F ⁡ x − t ≤ c x ↔ seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ 1 a ⁡ x − t ≤ c ⁢ 1 x
78 77 ralbidva ⊢ φ ∧ c ∈ 0 +∞ → ∀ x ∈ 1 +∞ seq 1 + F ⁡ x − t ≤ c x ↔ ∀ x ∈ 1 +∞ seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ 1 a ⁡ x − t ≤ c ⁢ 1 x
79 53 78 syl5bb ⊢ φ ∧ c ∈ 0 +∞ → ∀ y ∈ 1 +∞ seq 1 + F ⁡ y − t ≤ c y ↔ ∀ x ∈ 1 +∞ seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ 1 a ⁡ x − t ≤ c ⁢ 1 x
80 48 79 anbi12d ⊢ φ ∧ c ∈ 0 +∞ → seq 1 + F ⇝ t ∧ ∀ y ∈ 1 +∞ seq 1 + F ⁡ y − t ≤ c y ↔ seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ 1 a ⇝ t ∧ ∀ x ∈ 1 +∞ seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ 1 a ⁡ x − t ≤ c ⁢ 1 x
81 80 rexbidva ⊢ φ → ∃ c ∈ 0 +∞ seq 1 + F ⇝ t ∧ ∀ y ∈ 1 +∞ seq 1 + F ⁡ y − t ≤ c y ↔ ∃ c ∈ 0 +∞ seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ 1 a ⇝ t ∧ ∀ x ∈ 1 +∞ seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ 1 a ⁡ x − t ≤ c ⁢ 1 x
82 81 exbidv ⊢ φ → ∃ t ∃ c ∈ 0 +∞ seq 1 + F ⇝ t ∧ ∀ y ∈ 1 +∞ seq 1 + F ⁡ y − t ≤ c y ↔ ∃ t ∃ c ∈ 0 +∞ seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ 1 a ⇝ t ∧ ∀ x ∈ 1 +∞ seq 1 + a ∈ ℕ ⟼ X ⁡ L ⁡ a ⁢ 1 a ⁡ x − t ≤ c ⁢ 1 x
83 30 82 mpbird ⊢ φ → ∃ t ∃ c ∈ 0 +∞ seq 1 + F ⇝ t ∧ ∀ y ∈ 1 +∞ seq 1 + F ⁡ y − t ≤ c y