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∈ℕ⟼ifn∈x13n0
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∈ℕ⟼ifn∈x13n0
2 nnnn0 ⊢k∈ℕ→k∈ℕ0
3 0re ⊢0∈ℝ
4 1re ⊢1∈ℝ
5 3nn ⊢3∈ℕ
6 nndivre ⊢1∈ℝ∧3∈ℕ→13∈ℝ
7 4 5 6 mp2an ⊢13∈ℝ
8 3re ⊢3∈ℝ
9 3pos ⊢0<3
10 8 9 recgt0ii ⊢0<13
11 3 7 10 ltleii ⊢0≤13
12 expge0 ⊢13∈ℝ∧k∈ℕ0∧0≤13→0≤13k
13 7 12 mp3an1 ⊢k∈ℕ0∧0≤13→0≤13k
14 2 11 13 sylancl ⊢k∈ℕ→0≤13k
15 14 3ad2ant3 ⊢A⊆B∧B⊆ℕ∧k∈ℕ→0≤13k
16 0le0 ⊢0≤0
17 breq2 ⊢13k=ifk∈A13k0→0≤13k↔0≤ifk∈A13k0
18 breq2 ⊢0=ifk∈A13k0→0≤0↔0≤ifk∈A13k0
19 17 18 ifboth ⊢0≤13k∧0≤0→0≤ifk∈A13k0
20 15 16 19 sylancl ⊢A⊆B∧B⊆ℕ∧k∈ℕ→0≤ifk∈A13k0
21 sstr ⊢A⊆B∧B⊆ℕ→A⊆ℕ
22 1 rpnnen2lem1 ⊢A⊆ℕ∧k∈ℕ→F⁡A⁡k=ifk∈A13k0
23 21 22 stoic3 ⊢A⊆B∧B⊆ℕ∧k∈ℕ→F⁡A⁡k=ifk∈A13k0
24 20 23 breqtrrd ⊢A⊆B∧B⊆ℕ∧k∈ℕ→0≤F⁡A⁡k
25 reexpcl ⊢13∈ℝ∧k∈ℕ0→13k∈ℝ
26 7 2 25 sylancr ⊢k∈ℕ→13k∈ℝ
27 26 3ad2ant3 ⊢A⊆B∧B⊆ℕ∧k∈ℕ→13k∈ℝ
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 ⊢13k∈ℝ∧0∈ℝ∧0≤13k∧k∈A→k∈B→ifk∈A13k0≤ifk∈B13k0
32 27 28 15 30 31 syl31anc ⊢A⊆B∧B⊆ℕ∧k∈ℕ→ifk∈A13k0≤ifk∈B13k0
33 1 rpnnen2lem1 ⊢B⊆ℕ∧k∈ℕ→F⁡B⁡k=ifk∈B13k0
34 33 3adant1 ⊢A⊆B∧B⊆ℕ∧k∈ℕ→F⁡B⁡k=ifk∈B13k0
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