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