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 → ( 𝐼𝑁 ) ∈ ℝ+ )