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 ⊢ 𝐹 = ( 𝑥 ∈ 𝒫 ℕ ↦ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝑥 , ( ( 1 / 3 ) ↑ 𝑛 ) , 0 ) ) )
Assertion rpnnen2lem4 ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℕ ∧ 𝑘 ∈ ℕ ) → ( 0 ≤ ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) ∧ ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) ≤ ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) ) )

Proof

Step Hyp Ref Expression
1 rpnnen2.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝒫 ℕ ↦ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ 𝑥 , ( ( 1 / 3 ) ↑ 𝑛 ) , 0 ) ) )
2 nnnn0 ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ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 ) ∈ ℝ ∧ 𝑘 ∈ ℕ0 ∧ 0 ≤ ( 1 / 3 ) ) → 0 ≤ ( ( 1 / 3 ) ↑ 𝑘 ) )
13 7 12 mp3an1 ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 0 ≤ ( 1 / 3 ) ) → 0 ≤ ( ( 1 / 3 ) ↑ 𝑘 ) )
14 2 11 13 sylancl ⊢ ( 𝑘 ∈ ℕ → 0 ≤ ( ( 1 / 3 ) ↑ 𝑘 ) )
15 14 3ad2ant3 ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℕ ∧ 𝑘 ∈ ℕ ) → 0 ≤ ( ( 1 / 3 ) ↑ 𝑘 ) )
16 0le0 ⊢ 0 ≤ 0
17 breq2 ⊢ ( ( ( 1 / 3 ) ↑ 𝑘 ) = if ( 𝑘 ∈ 𝐴 , ( ( 1 / 3 ) ↑ 𝑘 ) , 0 ) → ( 0 ≤ ( ( 1 / 3 ) ↑ 𝑘 ) ↔ 0 ≤ if ( 𝑘 ∈ 𝐴 , ( ( 1 / 3 ) ↑ 𝑘 ) , 0 ) ) )
18 breq2 ⊢ ( 0 = if ( 𝑘 ∈ 𝐴 , ( ( 1 / 3 ) ↑ 𝑘 ) , 0 ) → ( 0 ≤ 0 ↔ 0 ≤ if ( 𝑘 ∈ 𝐴 , ( ( 1 / 3 ) ↑ 𝑘 ) , 0 ) ) )
19 17 18 ifboth ⊢ ( ( 0 ≤ ( ( 1 / 3 ) ↑ 𝑘 ) ∧ 0 ≤ 0 ) → 0 ≤ if ( 𝑘 ∈ 𝐴 , ( ( 1 / 3 ) ↑ 𝑘 ) , 0 ) )
20 15 16 19 sylancl ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℕ ∧ 𝑘 ∈ ℕ ) → 0 ≤ if ( 𝑘 ∈ 𝐴 , ( ( 1 / 3 ) ↑ 𝑘 ) , 0 ) )
21 sstr ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℕ ) → 𝐴 ⊆ ℕ )
22 1 rpnnen2lem1 ⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐴 , ( ( 1 / 3 ) ↑ 𝑘 ) , 0 ) )
23 21 22 stoic3 ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℕ ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐴 , ( ( 1 / 3 ) ↑ 𝑘 ) , 0 ) )
24 20 23 breqtrrd ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℕ ∧ 𝑘 ∈ ℕ ) → 0 ≤ ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) )
25 reexpcl ⊢ ( ( ( 1 / 3 ) ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( ( 1 / 3 ) ↑ 𝑘 ) ∈ ℝ )
26 7 2 25 sylancr ⊢ ( 𝑘 ∈ ℕ → ( ( 1 / 3 ) ↑ 𝑘 ) ∈ ℝ )
27 26 3ad2ant3 ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℕ ∧ 𝑘 ∈ ℕ ) → ( ( 1 / 3 ) ↑ 𝑘 ) ∈ ℝ )
28 0red ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℕ ∧ 𝑘 ∈ ℕ ) → 0 ∈ ℝ )
29 simp1 ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℕ ∧ 𝑘 ∈ ℕ ) → 𝐴 ⊆ 𝐵 )
30 29 sseld ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℕ ∧ 𝑘 ∈ ℕ ) → ( 𝑘 ∈ 𝐴 → 𝑘 ∈ 𝐵 ) )
31 ifle ⊢ ( ( ( ( ( 1 / 3 ) ↑ 𝑘 ) ∈ ℝ ∧ 0 ∈ ℝ ∧ 0 ≤ ( ( 1 / 3 ) ↑ 𝑘 ) ) ∧ ( 𝑘 ∈ 𝐴 → 𝑘 ∈ 𝐵 ) ) → if ( 𝑘 ∈ 𝐴 , ( ( 1 / 3 ) ↑ 𝑘 ) , 0 ) ≤ if ( 𝑘 ∈ 𝐵 , ( ( 1 / 3 ) ↑ 𝑘 ) , 0 ) )
32 27 28 15 30 31 syl31anc ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℕ ∧ 𝑘 ∈ ℕ ) → if ( 𝑘 ∈ 𝐴 , ( ( 1 / 3 ) ↑ 𝑘 ) , 0 ) ≤ if ( 𝑘 ∈ 𝐵 , ( ( 1 / 3 ) ↑ 𝑘 ) , 0 ) )
33 1 rpnnen2lem1 ⊢ ( ( 𝐵 ⊆ ℕ ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐵 , ( ( 1 / 3 ) ↑ 𝑘 ) , 0 ) )
34 33 3adant1 ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℕ ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐵 , ( ( 1 / 3 ) ↑ 𝑘 ) , 0 ) )
35 32 23 34 3brtr4d ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℕ ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) ≤ ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) )
36 24 35 jca ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℕ ∧ 𝑘 ∈ ℕ ) → ( 0 ≤ ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) ∧ ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑘 ) ≤ ( ( 𝐹 ‘ 𝐵 ) ‘ 𝑘 ) ) )