wallispilem3

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

		Ref	Expression
	Hypothesis	wallispilem3.1	$⊢ I = (n \in ℕ_{0} ⟼ \int_{(0, π)} {\sin x}^{n} d x)$
	Assertion	wallispilem3	$⊢ N \in ℕ_{0} \to I (N) \in ℝ^{+}$

Proof

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

Metamath Proof Explorer

Theorem wallispilem3

Proof