Metamath Proof Explorer

Theorem rpnnen2lem4

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

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

Proof

Step Hyp Ref Expression
1 rpnnen2.1 ⊢ F = x ∈ 𝒫 ℕ ⟼ n ∈ ℕ ⟼ if n ∈ x 1 3 n 0
2 nnnn0 ⊢ k ∈ ℕ → k ∈ ℕ 0
3 0re ⊢ 0 ∈ ℝ
4 1re ⊢ 1 ∈ ℝ
5 3nn ⊢ 3 ∈ ℕ
6 nndivre ⊢ 1 ∈ ℝ ∧ 3 ∈ ℕ → 1 3 ∈ ℝ
7 4 5 6 mp2an ⊢ 1 3 ∈ ℝ
8 3re ⊢ 3 ∈ ℝ
9 3pos ⊢ 0 < 3
10 8 9 recgt0ii ⊢ 0 < 1 3
11 3 7 10 ltleii ⊢ 0 ≤ 1 3
12 expge0 ⊢ 1 3 ∈ ℝ ∧ k ∈ ℕ 0 ∧ 0 ≤ 1 3 → 0 ≤ 1 3 k
13 7 12 mp3an1 ⊢ k ∈ ℕ 0 ∧ 0 ≤ 1 3 → 0 ≤ 1 3 k
14 2 11 13 sylancl ⊢ k ∈ ℕ → 0 ≤ 1 3 k
15 14 3ad2ant3 ⊢ A ⊆ B ∧ B ⊆ ℕ ∧ k ∈ ℕ → 0 ≤ 1 3 k
16 0le0 ⊢ 0 ≤ 0
17 breq2 ⊢ 1 3 k = if k ∈ A 1 3 k 0 → 0 ≤ 1 3 k ↔ 0 ≤ if k ∈ A 1 3 k 0
18 breq2 ⊢ 0 = if k ∈ A 1 3 k 0 → 0 ≤ 0 ↔ 0 ≤ if k ∈ A 1 3 k 0
19 17 18 ifboth ⊢ 0 ≤ 1 3 k ∧ 0 ≤ 0 → 0 ≤ if k ∈ A 1 3 k 0
20 15 16 19 sylancl ⊢ A ⊆ B ∧ B ⊆ ℕ ∧ k ∈ ℕ → 0 ≤ if k ∈ A 1 3 k 0
21 sstr ⊢ A ⊆ B ∧ B ⊆ ℕ → A ⊆ ℕ
22 1 rpnnen2lem1 ⊢ A ⊆ ℕ ∧ k ∈ ℕ → F ⁡ A ⁡ k = if k ∈ A 1 3 k 0
23 21 22 stoic3 ⊢ A ⊆ B ∧ B ⊆ ℕ ∧ k ∈ ℕ → F ⁡ A ⁡ k = if k ∈ A 1 3 k 0
24 20 23 breqtrrd ⊢ A ⊆ B ∧ B ⊆ ℕ ∧ k ∈ ℕ → 0 ≤ F ⁡ A ⁡ k
25 reexpcl ⊢ 1 3 ∈ ℝ ∧ k ∈ ℕ 0 → 1 3 k ∈ ℝ
26 7 2 25 sylancr ⊢ k ∈ ℕ → 1 3 k ∈ ℝ
27 26 3ad2ant3 ⊢ A ⊆ B ∧ B ⊆ ℕ ∧ k ∈ ℕ → 1 3 k ∈ ℝ
28 0red ⊢ A ⊆ B ∧ B ⊆ ℕ ∧ k ∈ ℕ → 0 ∈ ℝ
29 simp1 ⊢ A ⊆ B ∧ B ⊆ ℕ ∧ k ∈ ℕ → A ⊆ B
30 29 sseld ⊢ A ⊆ B ∧ B ⊆ ℕ ∧ k ∈ ℕ → k ∈ A → k ∈ B
31 ifle ⊢ 1 3 k ∈ ℝ ∧ 0 ∈ ℝ ∧ 0 ≤ 1 3 k ∧ k ∈ A → k ∈ B → if k ∈ A 1 3 k 0 ≤ if k ∈ B 1 3 k 0
32 27 28 15 30 31 syl31anc ⊢ A ⊆ B ∧ B ⊆ ℕ ∧ k ∈ ℕ → if k ∈ A 1 3 k 0 ≤ if k ∈ B 1 3 k 0
33 1 rpnnen2lem1 ⊢ B ⊆ ℕ ∧ k ∈ ℕ → F ⁡ B ⁡ k = if k ∈ B 1 3 k 0
34 33 3adant1 ⊢ A ⊆ B ∧ B ⊆ ℕ ∧ k ∈ ℕ → F ⁡ B ⁡ k = if k ∈ B 1 3 k 0
35 32 23 34 3brtr4d ⊢ A ⊆ B ∧ B ⊆ ℕ ∧ k ∈ ℕ → F ⁡ A ⁡ k ≤ F ⁡ B ⁡ k
36 24 35 jca ⊢ A ⊆ B ∧ B ⊆ ℕ ∧ k ∈ ℕ → 0 ≤ F ⁡ A ⁡ k ∧ F ⁡ A ⁡ k ≤ F ⁡ B ⁡ k