Metamath Proof Explorer

Theorem wallispilem3

Description: I maps to real values. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypothesis wallispilem3.1 ⊢ 𝐼 = ( 𝑛 ∈ ℕ0 ↦ ∫ ( 0 (,) π ) ( ( sin ‘ 𝑥 ) ↑ 𝑛 ) d 𝑥 )
Assertion wallispilem3 ( 𝑁 ∈ ℕ0 → ( 𝐼 ‘ 𝑁 ) ∈ ℝ+ )

Proof

Step Hyp Ref Expression
1 wallispilem3.1 ⊢ 𝐼 = ( 𝑛 ∈ ℕ0 ↦ ∫ ( 0 (,) π ) ( ( sin ‘ 𝑥 ) ↑ 𝑛 ) d 𝑥 )
2 breq2 ⊢ ( 𝑤 = 0 → ( 𝑚 ≤ 𝑤 ↔ 𝑚 ≤ 0 ) )
3 2 imbi1d ⊢ ( 𝑤 = 0 → ( ( 𝑚 ≤ 𝑤 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ↔ ( 𝑚 ≤ 0 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ) )
4 3 ralbidv ⊢ ( 𝑤 = 0 → ( ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑤 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ↔ ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 0 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ) )
5 breq2 ⊢ ( 𝑤 = 𝑦 → ( 𝑚 ≤ 𝑤 ↔ 𝑚 ≤ 𝑦 ) )
6 5 imbi1d ⊢ ( 𝑤 = 𝑦 → ( ( 𝑚 ≤ 𝑤 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ↔ ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ) )
7 6 ralbidv ⊢ ( 𝑤 = 𝑦 → ( ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑤 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ↔ ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ) )
8 breq2 ⊢ ( 𝑤 = ( 𝑦 + 1 ) → ( 𝑚 ≤ 𝑤 ↔ 𝑚 ≤ ( 𝑦 + 1 ) ) )
9 8 imbi1d ⊢ ( 𝑤 = ( 𝑦 + 1 ) → ( ( 𝑚 ≤ 𝑤 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ↔ ( 𝑚 ≤ ( 𝑦 + 1 ) → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ) )
10 9 ralbidv ⊢ ( 𝑤 = ( 𝑦 + 1 ) → ( ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑤 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ↔ ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ ( 𝑦 + 1 ) → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ) )
11 breq2 ⊢ ( 𝑤 = 𝑁 → ( 𝑚 ≤ 𝑤 ↔ 𝑚 ≤ 𝑁 ) )
12 11 imbi1d ⊢ ( 𝑤 = 𝑁 → ( ( 𝑚 ≤ 𝑤 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ↔ ( 𝑚 ≤ 𝑁 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ) )
13 12 ralbidv ⊢ ( 𝑤 = 𝑁 → ( ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑤 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ↔ ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑁 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ) )
14 simpr ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑚 ≤ 0 ) → 𝑚 ≤ 0 )
15 nn0ge0 ⊢ ( 𝑚 ∈ ℕ0 → 0 ≤ 𝑚 )
16 15 adantr ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑚 ≤ 0 ) → 0 ≤ 𝑚 )
17 nn0re ⊢ ( 𝑚 ∈ ℕ0 → 𝑚 ∈ ℝ )
18 17 adantr ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑚 ≤ 0 ) → 𝑚 ∈ ℝ )
19 0red ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑚 ≤ 0 ) → 0 ∈ ℝ )
20 18 19 letri3d ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑚 ≤ 0 ) → ( 𝑚 = 0 ↔ ( 𝑚 ≤ 0 ∧ 0 ≤ 𝑚 ) ) )
21 14 16 20 mpbir2and ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑚 ≤ 0 ) → 𝑚 = 0 )
22 21 fveq2d ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑚 ≤ 0 ) → ( 𝐼 ‘ 𝑚 ) = ( 𝐼 ‘ 0 ) )
23 1 wallispilem2 ⊢ ( ( 𝐼 ‘ 0 ) = π ∧ ( 𝐼 ‘ 1 ) = 2 ∧ ( 𝑚 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐼 ‘ 𝑚 ) = ( ( ( 𝑚 − 1 ) / 𝑚 ) · ( 𝐼 ‘ ( 𝑚 − 2 ) ) ) ) )
24 23 simp1i ⊢ ( 𝐼 ‘ 0 ) = π
25 pirp ⊢ π ∈ ℝ+
26 24 25 eqeltri ⊢ ( 𝐼 ‘ 0 ) ∈ ℝ+
27 22 26 eqeltrdi ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑚 ≤ 0 ) → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ )
28 27 ex ⊢ ( 𝑚 ∈ ℕ0 → ( 𝑚 ≤ 0 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) )
29 28 rgen ⊢ ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 0 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ )
30 nfv ⊢ Ⅎ 𝑚 𝑦 ∈ ℕ0
31 nfra1 ⊢ Ⅎ 𝑚 ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ )
32 30 31 nfan ⊢ Ⅎ 𝑚 ( 𝑦 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) )
33 simpllr ⊢ ( ( ( ( 𝑦 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 ≤ ( 𝑦 + 1 ) ) → ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) )
34 simplr ⊢ ( ( ( ( 𝑦 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 ≤ ( 𝑦 + 1 ) ) → 𝑚 ∈ ℕ0 )
35 rsp ⊢ ( ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) → ( 𝑚 ∈ ℕ0 → ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ) )
36 33 34 35 sylc ⊢ ( ( ( ( 𝑦 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 ≤ ( 𝑦 + 1 ) ) → ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) )
37 fveq2 ⊢ ( 𝑚 = 1 → ( 𝐼 ‘ 𝑚 ) = ( 𝐼 ‘ 1 ) )
38 23 simp2i ⊢ ( 𝐼 ‘ 1 ) = 2
39 2rp ⊢ 2 ∈ ℝ+
40 38 39 eqeltri ⊢ ( 𝐼 ‘ 1 ) ∈ ℝ+
41 37 40 eqeltrdi ⊢ ( 𝑚 = 1 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ )
42 41 a1i ⊢ ( ( ( ( 𝑦 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 = ( 𝑦 + 1 ) ) → ( 𝑚 = 1 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) )
43 23 simp3i ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐼 ‘ 𝑚 ) = ( ( ( 𝑚 − 1 ) / 𝑚 ) · ( 𝐼 ‘ ( 𝑚 − 2 ) ) ) )
44 43 adantl ⊢ ( ( ( ( 𝑦 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ) ∧ 𝑚 = ( 𝑦 + 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐼 ‘ 𝑚 ) = ( ( ( 𝑚 − 1 ) / 𝑚 ) · ( 𝐼 ‘ ( 𝑚 − 2 ) ) ) )
45 eluz2nn ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 2 ) → 𝑚 ∈ ℕ )
46 nnre ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℝ )
47 1red ⊢ ( 𝑚 ∈ ℕ → 1 ∈ ℝ )
48 46 47 resubcld ⊢ ( 𝑚 ∈ ℕ → ( 𝑚 − 1 ) ∈ ℝ )
49 45 48 syl ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑚 − 1 ) ∈ ℝ )
50 1m1e0 ⊢ ( 1 − 1 ) = 0
51 1red ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 2 ) → 1 ∈ ℝ )
52 eluzelre ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 2 ) → 𝑚 ∈ ℝ )
53 eluz2b2 ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑚 ∈ ℕ ∧ 1 < 𝑚 ) )
54 53 simprbi ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 2 ) → 1 < 𝑚 )
55 51 52 51 54 ltsub1dd ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 2 ) → ( 1 − 1 ) < ( 𝑚 − 1 ) )
56 50 55 eqbrtrrid ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 2 ) → 0 < ( 𝑚 − 1 ) )
57 49 56 elrpd ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑚 − 1 ) ∈ ℝ+ )
58 45 nnrpd ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 2 ) → 𝑚 ∈ ℝ+ )
59 57 58 rpdivcld ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝑚 − 1 ) / 𝑚 ) ∈ ℝ+ )
60 59 adantl ⊢ ( ( ( ( 𝑦 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ) ∧ 𝑚 = ( 𝑦 + 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝑚 − 1 ) / 𝑚 ) ∈ ℝ+ )
61 breq1 ⊢ ( 𝑚 = 𝑘 → ( 𝑚 ≤ 𝑦 ↔ 𝑘 ≤ 𝑦 ) )
62 fveq2 ⊢ ( 𝑚 = 𝑘 → ( 𝐼 ‘ 𝑚 ) = ( 𝐼 ‘ 𝑘 ) )
63 62 eleq1d ⊢ ( 𝑚 = 𝑘 → ( ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ↔ ( 𝐼 ‘ 𝑘 ) ∈ ℝ+ ) )
64 61 63 imbi12d ⊢ ( 𝑚 = 𝑘 → ( ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ↔ ( 𝑘 ≤ 𝑦 → ( 𝐼 ‘ 𝑘 ) ∈ ℝ+ ) ) )
65 64 cbvralvw ⊢ ( ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ↔ ∀ 𝑘 ∈ ℕ0 ( 𝑘 ≤ 𝑦 → ( 𝐼 ‘ 𝑘 ) ∈ ℝ+ ) )
66 65 biimpi ⊢ ( ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) → ∀ 𝑘 ∈ ℕ0 ( 𝑘 ≤ 𝑦 → ( 𝐼 ‘ 𝑘 ) ∈ ℝ+ ) )
67 66 ad3antlr ⊢ ( ( ( ( 𝑦 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ) ∧ 𝑚 = ( 𝑦 + 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 2 ) ) → ∀ 𝑘 ∈ ℕ0 ( 𝑘 ≤ 𝑦 → ( 𝐼 ‘ 𝑘 ) ∈ ℝ+ ) )
68 uznn0sub ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑚 − 2 ) ∈ ℕ0 )
69 68 adantl ⊢ ( ( ( ( 𝑦 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ) ∧ 𝑚 = ( 𝑦 + 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑚 − 2 ) ∈ ℕ0 )
70 67 69 jca ⊢ ( ( ( ( 𝑦 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ) ∧ 𝑚 = ( 𝑦 + 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 2 ) ) → ( ∀ 𝑘 ∈ ℕ0 ( 𝑘 ≤ 𝑦 → ( 𝐼 ‘ 𝑘 ) ∈ ℝ+ ) ∧ ( 𝑚 − 2 ) ∈ ℕ0 ) )
71 simplll ⊢ ( ( ( ( 𝑦 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ) ∧ 𝑚 = ( 𝑦 + 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑦 ∈ ℕ0 )
72 simplr ⊢ ( ( ( ( 𝑦 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ) ∧ 𝑚 = ( 𝑦 + 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑚 = ( 𝑦 + 1 ) )
73 simpr ⊢ ( ( ( ( 𝑦 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ) ∧ 𝑚 = ( 𝑦 + 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑚 ∈ ( ℤ≥ ‘ 2 ) )
74 simp2 ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 = ( 𝑦 + 1 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑚 = ( 𝑦 + 1 ) )
75 74 oveq1d ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 = ( 𝑦 + 1 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑚 − 2 ) = ( ( 𝑦 + 1 ) − 2 ) )
76 nn0re ⊢ ( 𝑦 ∈ ℕ0 → 𝑦 ∈ ℝ )
77 76 3ad2ant1 ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 = ( 𝑦 + 1 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑦 ∈ ℝ )
78 77 recnd ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 = ( 𝑦 + 1 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑦 ∈ ℂ )
79 df-2 ⊢ 2 = ( 1 + 1 )
80 79 a1i ⊢ ( 𝑦 ∈ ℂ → 2 = ( 1 + 1 ) )
81 80 oveq2d ⊢ ( 𝑦 ∈ ℂ → ( ( 𝑦 + 1 ) − 2 ) = ( ( 𝑦 + 1 ) − ( 1 + 1 ) ) )
82 id ⊢ ( 𝑦 ∈ ℂ → 𝑦 ∈ ℂ )
83 1cnd ⊢ ( 𝑦 ∈ ℂ → 1 ∈ ℂ )
84 82 83 83 pnpcan2d ⊢ ( 𝑦 ∈ ℂ → ( ( 𝑦 + 1 ) − ( 1 + 1 ) ) = ( 𝑦 − 1 ) )
85 81 84 eqtrd ⊢ ( 𝑦 ∈ ℂ → ( ( 𝑦 + 1 ) − 2 ) = ( 𝑦 − 1 ) )
86 78 85 syl ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 = ( 𝑦 + 1 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝑦 + 1 ) − 2 ) = ( 𝑦 − 1 ) )
87 75 86 eqtrd ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 = ( 𝑦 + 1 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑚 − 2 ) = ( 𝑦 − 1 ) )
88 77 lem1d ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 = ( 𝑦 + 1 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑦 − 1 ) ≤ 𝑦 )
89 87 88 eqbrtrd ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 = ( 𝑦 + 1 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑚 − 2 ) ≤ 𝑦 )
90 71 72 73 89 syl3anc ⊢ ( ( ( ( 𝑦 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ) ∧ 𝑚 = ( 𝑦 + 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑚 − 2 ) ≤ 𝑦 )
91 breq1 ⊢ ( 𝑘 = ( 𝑚 − 2 ) → ( 𝑘 ≤ 𝑦 ↔ ( 𝑚 − 2 ) ≤ 𝑦 ) )
92 fveq2 ⊢ ( 𝑘 = ( 𝑚 − 2 ) → ( 𝐼 ‘ 𝑘 ) = ( 𝐼 ‘ ( 𝑚 − 2 ) ) )
93 92 eleq1d ⊢ ( 𝑘 = ( 𝑚 − 2 ) → ( ( 𝐼 ‘ 𝑘 ) ∈ ℝ+ ↔ ( 𝐼 ‘ ( 𝑚 − 2 ) ) ∈ ℝ+ ) )
94 91 93 imbi12d ⊢ ( 𝑘 = ( 𝑚 − 2 ) → ( ( 𝑘 ≤ 𝑦 → ( 𝐼 ‘ 𝑘 ) ∈ ℝ+ ) ↔ ( ( 𝑚 − 2 ) ≤ 𝑦 → ( 𝐼 ‘ ( 𝑚 − 2 ) ) ∈ ℝ+ ) ) )
95 94 rspccva ⊢ ( ( ∀ 𝑘 ∈ ℕ0 ( 𝑘 ≤ 𝑦 → ( 𝐼 ‘ 𝑘 ) ∈ ℝ+ ) ∧ ( 𝑚 − 2 ) ∈ ℕ0 ) → ( ( 𝑚 − 2 ) ≤ 𝑦 → ( 𝐼 ‘ ( 𝑚 − 2 ) ) ∈ ℝ+ ) )
96 70 90 95 sylc ⊢ ( ( ( ( 𝑦 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ) ∧ 𝑚 = ( 𝑦 + 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐼 ‘ ( 𝑚 − 2 ) ) ∈ ℝ+ )
97 60 96 rpmulcld ⊢ ( ( ( ( 𝑦 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ) ∧ 𝑚 = ( 𝑦 + 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ( 𝑚 − 1 ) / 𝑚 ) · ( 𝐼 ‘ ( 𝑚 − 2 ) ) ) ∈ ℝ+ )
98 44 97 eqeltrd ⊢ ( ( ( ( 𝑦 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ) ∧ 𝑚 = ( 𝑦 + 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ )
99 98 adantllr ⊢ ( ( ( ( ( 𝑦 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 = ( 𝑦 + 1 ) ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ )
100 99 ex ⊢ ( ( ( ( 𝑦 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 = ( 𝑦 + 1 ) ) → ( 𝑚 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) )
101 simplll ⊢ ( ( ( ( 𝑦 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 = ( 𝑦 + 1 ) ) → 𝑦 ∈ ℕ0 )
102 simplr ⊢ ( ( ( ( 𝑦 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 = ( 𝑦 + 1 ) ) → 𝑚 ∈ ℕ0 )
103 simpr ⊢ ( ( ( ( 𝑦 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 = ( 𝑦 + 1 ) ) → 𝑚 = ( 𝑦 + 1 ) )
104 simp3 ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ∧ 𝑚 = ( 𝑦 + 1 ) ) → 𝑚 = ( 𝑦 + 1 ) )
105 nn0p1nn ⊢ ( 𝑦 ∈ ℕ0 → ( 𝑦 + 1 ) ∈ ℕ )
106 105 3ad2ant1 ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ∧ 𝑚 = ( 𝑦 + 1 ) ) → ( 𝑦 + 1 ) ∈ ℕ )
107 104 106 eqeltrd ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ∧ 𝑚 = ( 𝑦 + 1 ) ) → 𝑚 ∈ ℕ )
108 elnnuz ⊢ ( 𝑚 ∈ ℕ ↔ 𝑚 ∈ ( ℤ≥ ‘ 1 ) )
109 107 108 sylib ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ∧ 𝑚 = ( 𝑦 + 1 ) ) → 𝑚 ∈ ( ℤ≥ ‘ 1 ) )
110 uzp1 ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 1 ) → ( 𝑚 = 1 ∨ 𝑚 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) )
111 1p1e2 ⊢ ( 1 + 1 ) = 2
112 111 fveq2i ⊢ ( ℤ≥ ‘ ( 1 + 1 ) ) = ( ℤ≥ ‘ 2 )
113 112 eleq2i ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ↔ 𝑚 ∈ ( ℤ≥ ‘ 2 ) )
114 113 orbi2i ⊢ ( ( 𝑚 = 1 ∨ 𝑚 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) ↔ ( 𝑚 = 1 ∨ 𝑚 ∈ ( ℤ≥ ‘ 2 ) ) )
115 110 114 sylib ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 1 ) → ( 𝑚 = 1 ∨ 𝑚 ∈ ( ℤ≥ ‘ 2 ) ) )
116 109 115 syl ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ∧ 𝑚 = ( 𝑦 + 1 ) ) → ( 𝑚 = 1 ∨ 𝑚 ∈ ( ℤ≥ ‘ 2 ) ) )
117 101 102 103 116 syl3anc ⊢ ( ( ( ( 𝑦 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 = ( 𝑦 + 1 ) ) → ( 𝑚 = 1 ∨ 𝑚 ∈ ( ℤ≥ ‘ 2 ) ) )
118 42 100 117 mpjaod ⊢ ( ( ( ( 𝑦 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 = ( 𝑦 + 1 ) ) → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ )
119 118 adantlr ⊢ ( ( ( ( ( 𝑦 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 ≤ ( 𝑦 + 1 ) ) ∧ 𝑚 = ( 𝑦 + 1 ) ) → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ )
120 119 ex ⊢ ( ( ( ( 𝑦 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 ≤ ( 𝑦 + 1 ) ) → ( 𝑚 = ( 𝑦 + 1 ) → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) )
121 simplll ⊢ ( ( ( ( 𝑦 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 ≤ ( 𝑦 + 1 ) ) → 𝑦 ∈ ℕ0 )
122 simpr ⊢ ( ( ( ( 𝑦 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 ≤ ( 𝑦 + 1 ) ) → 𝑚 ≤ ( 𝑦 + 1 ) )
123 simpl1 ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ∧ 𝑚 ≤ ( 𝑦 + 1 ) ) ∧ 𝑚 < ( 𝑦 + 1 ) ) → 𝑦 ∈ ℕ0 )
124 simpl2 ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ∧ 𝑚 ≤ ( 𝑦 + 1 ) ) ∧ 𝑚 < ( 𝑦 + 1 ) ) → 𝑚 ∈ ℕ0 )
125 simpr ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ∧ 𝑚 ≤ ( 𝑦 + 1 ) ) ∧ 𝑚 < ( 𝑦 + 1 ) ) → 𝑚 < ( 𝑦 + 1 ) )
126 simpr ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 = 0 ) → 𝑚 = 0 )
127 nn0ge0 ⊢ ( 𝑦 ∈ ℕ0 → 0 ≤ 𝑦 )
128 127 adantr ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 = 0 ) → 0 ≤ 𝑦 )
129 126 128 eqbrtrd ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 = 0 ) → 𝑚 ≤ 𝑦 )
130 129 3ad2antl1 ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ∧ 𝑚 < ( 𝑦 + 1 ) ) ∧ 𝑚 = 0 ) → 𝑚 ≤ 𝑦 )
131 simpl1 ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ∧ 𝑚 < ( 𝑦 + 1 ) ) ∧ 𝑚 ∈ ℕ ) → 𝑦 ∈ ℕ0 )
132 simpr ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ∧ 𝑚 < ( 𝑦 + 1 ) ) ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℕ )
133 simpl3 ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ∧ 𝑚 < ( 𝑦 + 1 ) ) ∧ 𝑚 ∈ ℕ ) → 𝑚 < ( 𝑦 + 1 ) )
134 simp3 ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ ∧ 𝑚 < ( 𝑦 + 1 ) ) → 𝑚 < ( 𝑦 + 1 ) )
135 simp2 ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ ∧ 𝑚 < ( 𝑦 + 1 ) ) → 𝑚 ∈ ℕ )
136 simp1 ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ ∧ 𝑚 < ( 𝑦 + 1 ) ) → 𝑦 ∈ ℕ0 )
137 0red ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ ∧ 𝑚 < ( 𝑦 + 1 ) ) → 0 ∈ ℝ )
138 48 3ad2ant2 ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ ∧ 𝑚 < ( 𝑦 + 1 ) ) → ( 𝑚 − 1 ) ∈ ℝ )
139 76 3ad2ant1 ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ ∧ 𝑚 < ( 𝑦 + 1 ) ) → 𝑦 ∈ ℝ )
140 nnm1ge0 ⊢ ( 𝑚 ∈ ℕ → 0 ≤ ( 𝑚 − 1 ) )
141 140 3ad2ant2 ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ ∧ 𝑚 < ( 𝑦 + 1 ) ) → 0 ≤ ( 𝑚 − 1 ) )
142 46 3ad2ant2 ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ ∧ 𝑚 < ( 𝑦 + 1 ) ) → 𝑚 ∈ ℝ )
143 1red ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ ∧ 𝑚 < ( 𝑦 + 1 ) ) → 1 ∈ ℝ )
144 142 143 139 ltsubaddd ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ ∧ 𝑚 < ( 𝑦 + 1 ) ) → ( ( 𝑚 − 1 ) < 𝑦 ↔ 𝑚 < ( 𝑦 + 1 ) ) )
145 134 144 mpbird ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ ∧ 𝑚 < ( 𝑦 + 1 ) ) → ( 𝑚 − 1 ) < 𝑦 )
146 137 138 139 141 145 lelttrd ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ ∧ 𝑚 < ( 𝑦 + 1 ) ) → 0 < 𝑦 )
147 146 gt0ne0d ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ ∧ 𝑚 < ( 𝑦 + 1 ) ) → 𝑦 ≠ 0 )
148 elnnne0 ⊢ ( 𝑦 ∈ ℕ ↔ ( 𝑦 ∈ ℕ0 ∧ 𝑦 ≠ 0 ) )
149 136 147 148 sylanbrc ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ ∧ 𝑚 < ( 𝑦 + 1 ) ) → 𝑦 ∈ ℕ )
150 nnleltp1 ⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℕ ) → ( 𝑚 ≤ 𝑦 ↔ 𝑚 < ( 𝑦 + 1 ) ) )
151 135 149 150 syl2anc ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ ∧ 𝑚 < ( 𝑦 + 1 ) ) → ( 𝑚 ≤ 𝑦 ↔ 𝑚 < ( 𝑦 + 1 ) ) )
152 134 151 mpbird ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ ∧ 𝑚 < ( 𝑦 + 1 ) ) → 𝑚 ≤ 𝑦 )
153 131 132 133 152 syl3anc ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ∧ 𝑚 < ( 𝑦 + 1 ) ) ∧ 𝑚 ∈ ℕ ) → 𝑚 ≤ 𝑦 )
154 elnn0 ⊢ ( 𝑚 ∈ ℕ0 ↔ ( 𝑚 ∈ ℕ ∨ 𝑚 = 0 ) )
155 154 biimpi ⊢ ( 𝑚 ∈ ℕ0 → ( 𝑚 ∈ ℕ ∨ 𝑚 = 0 ) )
156 155 orcomd ⊢ ( 𝑚 ∈ ℕ0 → ( 𝑚 = 0 ∨ 𝑚 ∈ ℕ ) )
157 156 3ad2ant2 ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ∧ 𝑚 < ( 𝑦 + 1 ) ) → ( 𝑚 = 0 ∨ 𝑚 ∈ ℕ ) )
158 130 153 157 mpjaodan ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ∧ 𝑚 < ( 𝑦 + 1 ) ) → 𝑚 ≤ 𝑦 )
159 158 orcd ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ∧ 𝑚 < ( 𝑦 + 1 ) ) → ( 𝑚 ≤ 𝑦 ∨ 𝑚 = ( 𝑦 + 1 ) ) )
160 123 124 125 159 syl3anc ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ∧ 𝑚 ≤ ( 𝑦 + 1 ) ) ∧ 𝑚 < ( 𝑦 + 1 ) ) → ( 𝑚 ≤ 𝑦 ∨ 𝑚 = ( 𝑦 + 1 ) ) )
161 simpr ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ∧ 𝑚 ≤ ( 𝑦 + 1 ) ) ∧ 𝑚 = ( 𝑦 + 1 ) ) → 𝑚 = ( 𝑦 + 1 ) )
162 161 olcd ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ∧ 𝑚 ≤ ( 𝑦 + 1 ) ) ∧ 𝑚 = ( 𝑦 + 1 ) ) → ( 𝑚 ≤ 𝑦 ∨ 𝑚 = ( 𝑦 + 1 ) ) )
163 simp3 ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ∧ 𝑚 ≤ ( 𝑦 + 1 ) ) → 𝑚 ≤ ( 𝑦 + 1 ) )
164 17 3ad2ant2 ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ∧ 𝑚 ≤ ( 𝑦 + 1 ) ) → 𝑚 ∈ ℝ )
165 76 3ad2ant1 ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ∧ 𝑚 ≤ ( 𝑦 + 1 ) ) → 𝑦 ∈ ℝ )
166 1red ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ∧ 𝑚 ≤ ( 𝑦 + 1 ) ) → 1 ∈ ℝ )
167 165 166 readdcld ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ∧ 𝑚 ≤ ( 𝑦 + 1 ) ) → ( 𝑦 + 1 ) ∈ ℝ )
168 164 167 leloed ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ∧ 𝑚 ≤ ( 𝑦 + 1 ) ) → ( 𝑚 ≤ ( 𝑦 + 1 ) ↔ ( 𝑚 < ( 𝑦 + 1 ) ∨ 𝑚 = ( 𝑦 + 1 ) ) ) )
169 163 168 mpbid ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ∧ 𝑚 ≤ ( 𝑦 + 1 ) ) → ( 𝑚 < ( 𝑦 + 1 ) ∨ 𝑚 = ( 𝑦 + 1 ) ) )
170 160 162 169 mpjaodan ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ∧ 𝑚 ≤ ( 𝑦 + 1 ) ) → ( 𝑚 ≤ 𝑦 ∨ 𝑚 = ( 𝑦 + 1 ) ) )
171 121 34 122 170 syl3anc ⊢ ( ( ( ( 𝑦 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 ≤ ( 𝑦 + 1 ) ) → ( 𝑚 ≤ 𝑦 ∨ 𝑚 = ( 𝑦 + 1 ) ) )
172 36 120 171 mpjaod ⊢ ( ( ( ( 𝑦 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 ≤ ( 𝑦 + 1 ) ) → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ )
173 172 exp31 ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ) → ( 𝑚 ∈ ℕ0 → ( 𝑚 ≤ ( 𝑦 + 1 ) → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ) )
174 32 173 ralrimi ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ) → ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ ( 𝑦 + 1 ) → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) )
175 174 ex ⊢ ( 𝑦 ∈ ℕ0 → ( ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑦 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) → ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ ( 𝑦 + 1 ) → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ) )
176 4 7 10 13 29 175 nn0ind ⊢ ( 𝑁 ∈ ℕ0 → ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑁 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) )
177 176 ancri ⊢ ( 𝑁 ∈ ℕ0 → ( ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑁 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ∧ 𝑁 ∈ ℕ0 ) )
178 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
179 178 leidd ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ≤ 𝑁 )
180 breq1 ⊢ ( 𝑚 = 𝑁 → ( 𝑚 ≤ 𝑁 ↔ 𝑁 ≤ 𝑁 ) )
181 fveq2 ⊢ ( 𝑚 = 𝑁 → ( 𝐼 ‘ 𝑚 ) = ( 𝐼 ‘ 𝑁 ) )
182 181 eleq1d ⊢ ( 𝑚 = 𝑁 → ( ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ↔ ( 𝐼 ‘ 𝑁 ) ∈ ℝ+ ) )
183 180 182 imbi12d ⊢ ( 𝑚 = 𝑁 → ( ( 𝑚 ≤ 𝑁 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ↔ ( 𝑁 ≤ 𝑁 → ( 𝐼 ‘ 𝑁 ) ∈ ℝ+ ) ) )
184 183 rspccva ⊢ ( ( ∀ 𝑚 ∈ ℕ0 ( 𝑚 ≤ 𝑁 → ( 𝐼 ‘ 𝑚 ) ∈ ℝ+ ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 ≤ 𝑁 → ( 𝐼 ‘ 𝑁 ) ∈ ℝ+ ) )
185 177 179 184 sylc ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐼 ‘ 𝑁 ) ∈ ℝ+ )