Metamath Proof Explorer

Theorem rpnnen2lem7

Description: Lemma for rpnnen2 . (Contributed by Mario Carneiro, 13-May-2013) (Revised by Mario Carneiro, 30-Apr-2014)

Ref Expression
Hypothesis rpnnen2.1 ⊢ F = x ∈ 𝒫 ℕ ⟼ n ∈ ℕ ⟼ if n ∈ x 1 3 n 0
Assertion rpnnen2lem7 ⊢ A ⊆ B ∧ B ⊆ ℕ ∧ M ∈ ℕ → ∑ k ∈ ℤ ≥ M F ⁡ A ⁡ k ≤ ∑ k ∈ ℤ ≥ M F ⁡ B ⁡ k

Proof

Step Hyp Ref Expression
1 rpnnen2.1 ⊢ F = x ∈ 𝒫 ℕ ⟼ n ∈ ℕ ⟼ if n ∈ x 1 3 n 0
2 eqid ⊢ ℤ ≥ M = ℤ ≥ M
3 simp3 ⊢ A ⊆ B ∧ B ⊆ ℕ ∧ M ∈ ℕ → M ∈ ℕ
4 3 nnzd ⊢ A ⊆ B ∧ B ⊆ ℕ ∧ M ∈ ℕ → M ∈ ℤ
5 eqidd ⊢ A ⊆ B ∧ B ⊆ ℕ ∧ M ∈ ℕ ∧ k ∈ ℤ ≥ M → F ⁡ A ⁡ k = F ⁡ A ⁡ k
6 eluznn ⊢ M ∈ ℕ ∧ k ∈ ℤ ≥ M → k ∈ ℕ
7 3 6 sylan ⊢ A ⊆ B ∧ B ⊆ ℕ ∧ M ∈ ℕ ∧ k ∈ ℤ ≥ M → k ∈ ℕ
8 sstr ⊢ A ⊆ B ∧ B ⊆ ℕ → A ⊆ ℕ
9 8 3adant3 ⊢ A ⊆ B ∧ B ⊆ ℕ ∧ M ∈ ℕ → A ⊆ ℕ
10 1 rpnnen2lem2 ⊢ A ⊆ ℕ → F ⁡ A : ℕ ⟶ ℝ
11 9 10 syl ⊢ A ⊆ B ∧ B ⊆ ℕ ∧ M ∈ ℕ → F ⁡ A : ℕ ⟶ ℝ
12 11 ffvelrnda ⊢ A ⊆ B ∧ B ⊆ ℕ ∧ M ∈ ℕ ∧ k ∈ ℕ → F ⁡ A ⁡ k ∈ ℝ
13 7 12 syldan ⊢ A ⊆ B ∧ B ⊆ ℕ ∧ M ∈ ℕ ∧ k ∈ ℤ ≥ M → F ⁡ A ⁡ k ∈ ℝ
14 eqidd ⊢ A ⊆ B ∧ B ⊆ ℕ ∧ M ∈ ℕ ∧ k ∈ ℤ ≥ M → F ⁡ B ⁡ k = F ⁡ B ⁡ k
15 1 rpnnen2lem2 ⊢ B ⊆ ℕ → F ⁡ B : ℕ ⟶ ℝ
16 15 3ad2ant2 ⊢ A ⊆ B ∧ B ⊆ ℕ ∧ M ∈ ℕ → F ⁡ B : ℕ ⟶ ℝ
17 16 ffvelrnda ⊢ A ⊆ B ∧ B ⊆ ℕ ∧ M ∈ ℕ ∧ k ∈ ℕ → F ⁡ B ⁡ k ∈ ℝ
18 7 17 syldan ⊢ A ⊆ B ∧ B ⊆ ℕ ∧ M ∈ ℕ ∧ k ∈ ℤ ≥ M → F ⁡ B ⁡ k ∈ ℝ
19 1 rpnnen2lem4 ⊢ A ⊆ B ∧ B ⊆ ℕ ∧ k ∈ ℕ → 0 ≤ F ⁡ A ⁡ k ∧ F ⁡ A ⁡ k ≤ F ⁡ B ⁡ k
20 19 simprd ⊢ A ⊆ B ∧ B ⊆ ℕ ∧ k ∈ ℕ → F ⁡ A ⁡ k ≤ F ⁡ B ⁡ k
21 20 3expa ⊢ A ⊆ B ∧ B ⊆ ℕ ∧ k ∈ ℕ → F ⁡ A ⁡ k ≤ F ⁡ B ⁡ k
22 21 3adantl3 ⊢ A ⊆ B ∧ B ⊆ ℕ ∧ M ∈ ℕ ∧ k ∈ ℕ → F ⁡ A ⁡ k ≤ F ⁡ B ⁡ k
23 7 22 syldan ⊢ A ⊆ B ∧ B ⊆ ℕ ∧ M ∈ ℕ ∧ k ∈ ℤ ≥ M → F ⁡ A ⁡ k ≤ F ⁡ B ⁡ k
24 1 rpnnen2lem5 ⊢ A ⊆ ℕ ∧ M ∈ ℕ → seq M + F ⁡ A ∈ dom ⁡ ⇝
25 8 24 stoic3 ⊢ A ⊆ B ∧ B ⊆ ℕ ∧ M ∈ ℕ → seq M + F ⁡ A ∈ dom ⁡ ⇝
26 1 rpnnen2lem5 ⊢ B ⊆ ℕ ∧ M ∈ ℕ → seq M + F ⁡ B ∈ dom ⁡ ⇝
27 26 3adant1 ⊢ A ⊆ B ∧ B ⊆ ℕ ∧ M ∈ ℕ → seq M + F ⁡ B ∈ dom ⁡ ⇝
28 2 4 5 13 14 18 23 25 27 isumle ⊢ A ⊆ B ∧ B ⊆ ℕ ∧ M ∈ ℕ → ∑ k ∈ ℤ ≥ M F ⁡ A ⁡ k ≤ ∑ k ∈ ℤ ≥ M F ⁡ B ⁡ k