Theorem wallispilem3 31367

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

Hypothesis

Ref	Expression
wallispilem3.1	|- I = ( n e. NN0 |-> S. ( 0 (,) pi ) ( ( sin ` x ) ^ n ) _d x )

Assertion

Ref	Expression
wallispilem3	|- ( N e. NN0 -> ( I ` N ) e. RR+ )

Distinct variable group:   x, n

Allowed substitution hints:   I( x, n)   N( x, n)

Proof of Theorem wallispilem3

Dummy variables k m y w are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq2 4451	. . . . . 6 |- ( w = 0 -> ( m <_ w <-> m <_ 0 ) )
2	1	imbi1d 317	. . . . 5 |- ( w = 0 -> ( ( m <_ w -> ( I ` m ) e. RR+ ) <-> ( m <_ 0 -> ( I ` m ) e. RR+ ) ) )
3	2	ralbidv 2903	. . . 4 |- ( w = 0 -> ( A. m e. NN0 ( m <_ w -> ( I ` m ) e. RR+ ) <-> A. m e. NN0 ( m <_ 0 -> ( I ` m ) e. RR+ ) ) )
4		breq2 4451	. . . . . 6 |- ( w = y -> ( m <_ w <-> m <_ y ) )
5	4	imbi1d 317	. . . . 5 |- ( w = y -> ( ( m <_ w -> ( I ` m ) e. RR+ ) <-> ( m <_ y -> ( I ` m ) e. RR+ ) ) )
6	5	ralbidv 2903	. . . 4 |- ( w = y -> ( A. m e. NN0 ( m <_ w -> ( I ` m ) e. RR+ ) <-> A. m e. NN0 ( m <_ y -> ( I ` m ) e. RR+ ) ) )
7		breq2 4451	. . . . . 6 |- ( w = ( y + 1 ) -> ( m <_ w <-> m <_ ( y + 1 ) ) )
8	7	imbi1d 317	. . . . 5 |- ( w = ( y + 1 ) -> ( ( m <_ w -> ( I ` m ) e. RR+ ) <-> ( m <_ ( y + 1 ) -> ( I ` m ) e. RR+ ) ) )
9	8	ralbidv 2903	. . . 4 |- ( w = ( y + 1 ) -> ( A. m e. NN0 ( m <_ w -> ( I ` m ) e. RR+ ) <-> A. m e. NN0 ( m <_ ( y + 1 ) -> ( I ` m ) e. RR+ ) ) )
10		breq2 4451	. . . . . 6 |- ( w = N -> ( m <_ w <-> m <_ N ) )
11	10	imbi1d 317	. . . . 5 |- ( w = N -> ( ( m <_ w -> ( I ` m ) e. RR+ ) <-> ( m <_ N -> ( I ` m ) e. RR+ ) ) )
12	11	ralbidv 2903	. . . 4 |- ( w = N -> ( A. m e. NN0 ( m <_ w -> ( I ` m ) e. RR+ ) <-> A. m e. NN0 ( m <_ N -> ( I ` m ) e. RR+ ) ) )
13		simpr 461	. . . . . . . . 9 |- ( ( m e. NN0 /\ m <_ 0 ) -> m <_ 0 )
14		nn0ge0 10817	. . . . . . . . . 10 |- ( m e. NN0 -> 0 <_ m )
15	14	adantr 465	. . . . . . . . 9 |- ( ( m e. NN0 /\ m <_ 0 ) -> 0 <_ m )
16		nn0re 10800	. . . . . . . . . . 11 |- ( m e. NN0 -> m e. RR )
17	16	adantr 465	. . . . . . . . . 10 |- ( ( m e. NN0 /\ m <_ 0 ) -> m e. RR )
18		0re 9592	. . . . . . . . . . 11 |- 0 e. RR
19	18	a1i 11	. . . . . . . . . 10 |- ( ( m e. NN0 /\ m <_ 0 ) -> 0 e. RR )
20	17, 19	letri3d 9722	. . . . . . . . 9 |- ( ( m e. NN0 /\ m <_ 0 ) -> ( m = 0 <-> ( m <_ 0 /\ 0 <_ m ) ) )
21	13, 15, 20	mpbir2and 920	. . . . . . . 8 |- ( ( m e. NN0 /\ m <_ 0 ) -> m = 0 )
22	21	fveq2d 5868	. . . . . . 7 |- ( ( m e. NN0 /\ m <_ 0 ) -> ( I ` m ) = ( I ` 0 ) )
23		wallispilem3.1	. . . . . . . . . 10 |- I = ( n e. NN0 |-> S. ( 0 (,) pi ) ( ( sin ` x ) ^ n ) _d x )
24	23	wallispilem2 31366	. . . . . . . . 9 |- ( ( I ` 0 ) = pi /\ ( I ` 1 ) = 2 /\ ( m e. ( ZZ>= ` 2 ) -> ( I ` m ) = ( ( ( m - 1 ) / m ) x. ( I ` ( m - 2 ) ) ) ) )
25	24	simp1i 1005	. . . . . . . 8 |- ( I ` 0 ) = pi
26		pire 22585	. . . . . . . . 9 |- pi e. RR
27		pipos 22587	. . . . . . . . 9 |- 0 < pi
28	26, 27	elrpii 11219	. . . . . . . 8 |- pi e. RR+
29	25, 28	eqeltri 2551	. . . . . . 7 |- ( I ` 0 ) e. RR+
30	22, 29	syl6eqel 2563	. . . . . 6 |- ( ( m e. NN0 /\ m <_ 0 ) -> ( I ` m ) e. RR+ )
31	30	ex 434	. . . . 5 |- ( m e. NN0 -> ( m <_ 0 -> ( I ` m ) e. RR+ ) )
32	31	rgen 2824	. . . 4 |- A. m e. NN0 ( m <_ 0 -> ( I ` m ) e. RR+ )
33		nfv 1683	. . . . . . 7 |- F/ m y e. NN0
34		nfra1 2845	. . . . . . 7 |- F/ m A. m e. NN0 ( m <_ y -> ( I ` m ) e. RR+ )
35	33, 34	nfan 1875	. . . . . 6 |- F/ m ( y e. NN0 /\ A. m e. NN0 ( m <_ y -> ( I ` m ) e. RR+ ) )
36		simpllr 758	. . . . . . . . 9 |- ( ( ( ( y e. NN0 /\ A. m e. NN0 ( m <_ y -> ( I ` m ) e. RR+ ) ) /\ m e. NN0 ) /\ m <_ ( y + 1 ) ) -> A. m e. NN0 ( m <_ y -> ( I ` m ) e. RR+ ) )
37		simplr 754	. . . . . . . . 9 |- ( ( ( ( y e. NN0 /\ A. m e. NN0 ( m <_ y -> ( I ` m ) e. RR+ ) ) /\ m e. NN0 ) /\ m <_ ( y + 1 ) ) -> m e. NN0 )
38		rsp 2830	. . . . . . . . 9 |- ( A. m e. NN0 ( m <_ y -> ( I ` m ) e. RR+ ) -> ( m e. NN0 -> ( m <_ y -> ( I ` m ) e. RR+ ) ) )
39	36, 37, 38	sylc 60	. . . . . . . 8 |- ( ( ( ( y e. NN0 /\ A. m e. NN0 ( m <_ y -> ( I ` m ) e. RR+ ) ) /\ m e. NN0 ) /\ m <_ ( y + 1 ) ) -> ( m <_ y -> ( I ` m ) e. RR+ ) )
40		fveq2 5864	. . . . . . . . . . . . 13 |- ( m = 1 -> ( I ` m ) = ( I ` 1 ) )
41	24	simp2i 1006	. . . . . . . . . . . . . 14 |- ( I ` 1 ) = 2
42		2rp 11221	. . . . . . . . . . . . . 14 |- 2 e. RR+
43	41, 42	eqeltri 2551	. . . . . . . . . . . . 13 |- ( I ` 1 ) e. RR+
44	40, 43	syl6eqel 2563	. . . . . . . . . . . 12 |- ( m = 1 -> ( I ` m ) e. RR+ )
45	44	a1i 11	. . . . . . . . . . 11 |- ( ( ( ( y e. NN0 /\ A. m e. NN0 ( m <_ y -> ( I ` m ) e. RR+ ) ) /\ m e. NN0 ) /\ m = ( y + 1 ) ) -> ( m = 1 -> ( I ` m ) e. RR+ ) )
46	24	simp3i 1007	. . . . . . . . . . . . . . 15 |- ( m e. ( ZZ>= ` 2 ) -> ( I ` m ) = ( ( ( m - 1 ) / m ) x. ( I ` ( m - 2 ) ) ) )
47	46	adantl 466	. . . . . . . . . . . . . 14 |- ( ( ( ( y e. NN0 /\ A. m e. NN0 ( m <_ y -> ( I ` m ) e. RR+ ) ) /\ m = ( y + 1 ) ) /\ m e. ( ZZ>= ` 2 ) ) -> ( I ` m ) = ( ( ( m - 1 ) / m ) x. ( I ` ( m - 2 ) ) ) )
48		eluz2b2 11150	. . . . . . . . . . . . . . . . . . . 20 |- ( m e. ( ZZ>= ` 2 ) <-> ( m e. NN /\ 1 < m ) )
49	48	simplbi 460	. . . . . . . . . . . . . . . . . . 19 |- ( m e. ( ZZ>= ` 2 ) -> m e. NN )
50		nnre 10539	. . . . . . . . . . . . . . . . . . . 20 |- ( m e. NN -> m e. RR )
51		1re 9591	. . . . . . . . . . . . . . . . . . . . 21 |- 1 e. RR
52	51	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( m e. NN -> 1 e. RR )
53	50, 52	resubcld 9983	. . . . . . . . . . . . . . . . . . 19 |- ( m e. NN -> ( m - 1 ) e. RR )
54	49, 53	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( m e. ( ZZ>= ` 2 ) -> ( m - 1 ) e. RR )
55		1m1e0 10600	. . . . . . . . . . . . . . . . . . 19 |- ( 1 - 1 ) = 0
56	51	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( m e. ( ZZ>= ` 2 ) -> 1 e. RR )
57		eluzelre 11088	. . . . . . . . . . . . . . . . . . . 20 |- ( m e. ( ZZ>= ` 2 ) -> m e. RR )
58	48	simprbi 464	. . . . . . . . . . . . . . . . . . . 20 |- ( m e. ( ZZ>= ` 2 ) -> 1 < m )
59	56, 57, 56, 58	ltsub1dd 10160	. . . . . . . . . . . . . . . . . . 19 |- ( m e. ( ZZ>= ` 2 ) -> ( 1 - 1 ) < ( m - 1 ) )
60	55, 59	syl5eqbrr 4481	. . . . . . . . . . . . . . . . . 18 |- ( m e. ( ZZ>= ` 2 ) -> 0 < ( m - 1 ) )
61	54, 60	elrpd 11250	. . . . . . . . . . . . . . . . 17 |- ( m e. ( ZZ>= ` 2 ) -> ( m - 1 ) e. RR+ )
62	49	nnrpd 11251	. . . . . . . . . . . . . . . . 17 |- ( m e. ( ZZ>= ` 2 ) -> m e. RR+ )
63	61, 62	rpdivcld 11269	. . . . . . . . . . . . . . . 16 |- ( m e. ( ZZ>= ` 2 ) -> ( ( m - 1 ) / m ) e. RR+ )
64	63	adantl 466	. . . . . . . . . . . . . . 15 |- ( ( ( ( y e. NN0 /\ A. m e. NN0 ( m <_ y -> ( I ` m ) e. RR+ ) ) /\ m = ( y + 1 ) ) /\ m e. ( ZZ>= ` 2 ) ) -> ( ( m - 1 ) / m ) e. RR+ )
65		breq1 4450	. . . . . . . . . . . . . . . . . . . . 21 |- ( m = k -> ( m <_ y <-> k <_ y ) )
66		fveq2 5864	. . . . . . . . . . . . . . . . . . . . . 22 |- ( m = k -> ( I ` m ) = ( I ` k ) )
67	66	eleq1d 2536	. . . . . . . . . . . . . . . . . . . . 21 |- ( m = k -> ( ( I ` m ) e. RR+ <-> ( I ` k ) e. RR+ ) )
68	65, 67	imbi12d 320	. . . . . . . . . . . . . . . . . . . 20 |- ( m = k -> ( ( m <_ y -> ( I ` m ) e. RR+ ) <-> ( k <_ y -> ( I ` k ) e. RR+ ) ) )
69	68	cbvralv 3088	. . . . . . . . . . . . . . . . . . 19 |- ( A. m e. NN0 ( m <_ y -> ( I ` m ) e. RR+ ) <-> A. k e. NN0 ( k <_ y -> ( I ` k ) e. RR+ ) )
70	69	biimpi 194	. . . . . . . . . . . . . . . . . 18 |- ( A. m e. NN0 ( m <_ y -> ( I ` m ) e. RR+ ) -> A. k e. NN0 ( k <_ y -> ( I ` k ) e. RR+ ) )
71	70	ad3antlr 730	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( y e. NN0 /\ A. m e. NN0 ( m <_ y -> ( I ` m ) e. RR+ ) ) /\ m = ( y + 1 ) ) /\ m e. ( ZZ>= ` 2 ) ) -> A. k e. NN0 ( k <_ y -> ( I ` k ) e. RR+ ) )
72		uznn0sub 11109	. . . . . . . . . . . . . . . . . 18 |- ( m e. ( ZZ>= ` 2 ) -> ( m - 2 ) e. NN0 )
73	72	adantl 466	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( y e. NN0 /\ A. m e. NN0 ( m <_ y -> ( I ` m ) e. RR+ ) ) /\ m = ( y + 1 ) ) /\ m e. ( ZZ>= ` 2 ) ) -> ( m - 2 ) e. NN0 )
74	71, 73	jca 532	. . . . . . . . . . . . . . . 16 |- ( ( ( ( y e. NN0 /\ A. m e. NN0 ( m <_ y -> ( I ` m ) e. RR+ ) ) /\ m = ( y + 1 ) ) /\ m e. ( ZZ>= ` 2 ) ) -> ( A. k e. NN0 ( k <_ y -> ( I ` k ) e. RR+ ) /\ ( m - 2 ) e. NN0 ) )
75		simplll 757	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( y e. NN0 /\ A. m e. NN0 ( m <_ y -> ( I ` m ) e. RR+ ) ) /\ m = ( y + 1 ) ) /\ m e. ( ZZ>= ` 2 ) ) -> y e. NN0 )
76		simplr 754	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( y e. NN0 /\ A. m e. NN0 ( m <_ y -> ( I ` m ) e. RR+ ) ) /\ m = ( y + 1 ) ) /\ m e. ( ZZ>= ` 2 ) ) -> m = ( y + 1 ) )
77		simpr 461	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( y e. NN0 /\ A. m e. NN0 ( m <_ y -> ( I ` m ) e. RR+ ) ) /\ m = ( y + 1 ) ) /\ m e. ( ZZ>= ` 2 ) ) -> m e. ( ZZ>= ` 2 ) )
78		simp2 997	. . . . . . . . . . . . . . . . . . . 20 |- ( ( y e. NN0 /\ m = ( y + 1 ) /\ m e. ( ZZ>= ` 2 ) ) -> m = ( y + 1 ) )
79	78	oveq1d 6297	. . . . . . . . . . . . . . . . . . 19 |- ( ( y e. NN0 /\ m = ( y + 1 ) /\ m e. ( ZZ>= ` 2 ) ) -> ( m - 2 ) = ( ( y + 1 ) - 2 ) )
80		nn0re 10800	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y e. NN0 -> y e. RR )
81	80	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( y e. NN0 /\ m = ( y + 1 ) /\ m e. ( ZZ>= ` 2 ) ) -> y e. RR )
82	81	recnd 9618	. . . . . . . . . . . . . . . . . . . 20 |- ( ( y e. NN0 /\ m = ( y + 1 ) /\ m e. ( ZZ>= ` 2 ) ) -> y e. CC )
83		df-2 10590	. . . . . . . . . . . . . . . . . . . . . . 23 |- 2 = ( 1 + 1 )
84	83	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y e. CC -> 2 = ( 1 + 1 ) )
85	84	oveq2d 6298	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. CC -> ( ( y + 1 ) - 2 ) = ( ( y + 1 ) - ( 1 + 1 ) ) )
86		id 22	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y e. CC -> y e. CC )
87		ax-1cn 9546	. . . . . . . . . . . . . . . . . . . . . . 23 |- 1 e. CC
88	87	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y e. CC -> 1 e. CC )
89	86, 88, 88	pnpcan2d 9964	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. CC -> ( ( y + 1 ) - ( 1 + 1 ) ) = ( y - 1 ) )
90	85, 89	eqtrd 2508	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. CC -> ( ( y + 1 ) - 2 ) = ( y - 1 ) )
91	82, 90	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ( y e. NN0 /\ m = ( y + 1 ) /\ m e. ( ZZ>= ` 2 ) ) -> ( ( y + 1 ) - 2 ) = ( y - 1 ) )
92	79, 91	eqtrd 2508	. . . . . . . . . . . . . . . . . 18 |- ( ( y e. NN0 /\ m = ( y + 1 ) /\ m e. ( ZZ>= ` 2 ) ) -> ( m - 2 ) = ( y - 1 ) )
93	81	lem1d 10475	. . . . . . . . . . . . . . . . . 18 |- ( ( y e. NN0 /\ m = ( y + 1 ) /\ m e. ( ZZ>= ` 2 ) ) -> ( y - 1 ) <_ y )
94	92, 93	eqbrtrd 4467	. . . . . . . . . . . . . . . . 17 |- ( ( y e. NN0 /\ m = ( y + 1 ) /\ m e. ( ZZ>= ` 2 ) ) -> ( m - 2 ) <_ y )
95	75, 76, 77, 94	syl3anc 1228	. . . . . . . . . . . . . . . 16 |- ( ( ( ( y e. NN0 /\ A. m e. NN0 ( m <_ y -> ( I ` m ) e. RR+ ) ) /\ m = ( y + 1 ) ) /\ m e. ( ZZ>= ` 2 ) ) -> ( m - 2 ) <_ y )
96		breq1 4450	. . . . . . . . . . . . . . . . . 18 |- ( k = ( m - 2 ) -> ( k <_ y <-> ( m - 2 ) <_ y ) )
97		fveq2 5864	. . . . . . . . . . . . . . . . . . 19 |- ( k = ( m - 2 ) -> ( I ` k ) = ( I ` ( m - 2 ) ) )
98	97	eleq1d 2536	. . . . . . . . . . . . . . . . . 18 |- ( k = ( m - 2 ) -> ( ( I ` k ) e. RR+ <-> ( I ` ( m - 2 ) ) e. RR+ ) )
99	96, 98	imbi12d 320	. . . . . . . . . . . . . . . . 17 |- ( k = ( m - 2 ) -> ( ( k <_ y -> ( I ` k ) e. RR+ ) <-> ( ( m - 2 ) <_ y -> ( I ` ( m - 2 ) ) e. RR+ ) ) )
100	99	rspccva 3213	. . . . . . . . . . . . . . . 16 |- ( ( A. k e. NN0 ( k <_ y -> ( I ` k ) e. RR+ ) /\ ( m - 2 ) e. NN0 ) -> ( ( m - 2 ) <_ y -> ( I ` ( m - 2 ) ) e. RR+ ) )
101	74, 95, 100	sylc 60	. . . . . . . . . . . . . . 15 |- ( ( ( ( y e. NN0 /\ A. m e. NN0 ( m <_ y -> ( I ` m ) e. RR+ ) ) /\ m = ( y + 1 ) ) /\ m e. ( ZZ>= ` 2 ) ) -> ( I ` ( m - 2 ) ) e. RR+ )
102	64, 101	rpmulcld 11268	. . . . . . . . . . . . . 14 |- ( ( ( ( y e. NN0 /\ A. m e. NN0 ( m <_ y -> ( I ` m ) e. RR+ ) ) /\ m = ( y + 1 ) ) /\ m e. ( ZZ>= ` 2 ) ) -> ( ( ( m - 1 ) / m ) x. ( I ` ( m - 2 ) ) ) e. RR+ )
103	47, 102	eqeltrd 2555	. . . . . . . . . . . . 13 |- ( ( ( ( y e. NN0 /\ A. m e. NN0 ( m <_ y -> ( I ` m ) e. RR+ ) ) /\ m = ( y + 1 ) ) /\ m e. ( ZZ>= ` 2 ) ) -> ( I ` m ) e. RR+ )
104	103	adantllr 718	. . . . . . . . . . . 12 |- ( ( ( ( ( y e. NN0 /\ A. m e. NN0 ( m <_ y -> ( I ` m ) e. RR+ ) ) /\ m e. NN0 ) /\ m = ( y + 1 ) ) /\ m e. ( ZZ>= ` 2 ) ) -> ( I ` m ) e. RR+ )
105	104	ex 434	. . . . . . . . . . 11 |- ( ( ( ( y e. NN0 /\ A. m e. NN0 ( m <_ y -> ( I ` m ) e. RR+ ) ) /\ m e. NN0 ) /\ m = ( y + 1 ) ) -> ( m e. ( ZZ>= ` 2 ) -> ( I ` m ) e. RR+ ) )
106		simplll 757	. . . . . . . . . . . 12 |- ( ( ( ( y e. NN0 /\ A. m e. NN0 ( m <_ y -> ( I ` m ) e. RR+ ) ) /\ m e. NN0 ) /\ m = ( y + 1 ) ) -> y e. NN0 )
107		simplr 754	. . . . . . . . . . . 12 |- ( ( ( ( y e. NN0 /\ A. m e. NN0 ( m <_ y -> ( I ` m ) e. RR+ ) ) /\ m e. NN0 ) /\ m = ( y + 1 ) ) -> m e. NN0 )
108		simpr 461	. . . . . . . . . . . 12 |- ( ( ( ( y e. NN0 /\ A. m e. NN0 ( m <_ y -> ( I ` m ) e. RR+ ) ) /\ m e. NN0 ) /\ m = ( y + 1 ) ) -> m = ( y + 1 ) )
109		simp3 998	. . . . . . . . . . . . . . 15 |- ( ( y e. NN0 /\ m e. NN0 /\ m = ( y + 1 ) ) -> m = ( y + 1 ) )
110		nn0p1nn 10831	. . . . . . . . . . . . . . . 16 |- ( y e. NN0 -> ( y + 1 ) e. NN )
111	110	3ad2ant1 1017	. . . . . . . . . . . . . . 15 |- ( ( y e. NN0 /\ m e. NN0 /\ m = ( y + 1 ) ) -> ( y + 1 ) e. NN )
112	109, 111	eqeltrd 2555	. . . . . . . . . . . . . 14 |- ( ( y e. NN0 /\ m e. NN0 /\ m = ( y + 1 ) ) -> m e. NN )
113		elnnuz 11114	. . . . . . . . . . . . . 14 |- ( m e. NN <-> m e. ( ZZ>= ` 1 ) )
114	112, 113	sylib 196	. . . . . . . . . . . . 13 |- ( ( y e. NN0 /\ m e. NN0 /\ m = ( y + 1 ) ) -> m e. ( ZZ>= ` 1 ) )
115		uzp1 11111	. . . . . . . . . . . . . 14 |- ( m e. ( ZZ>= ` 1 ) -> ( m = 1 \/ m e. ( ZZ>= ` ( 1 + 1 ) ) ) )
116		1p1e2 10645	. . . . . . . . . . . . . . . . 17 |- ( 1 + 1 ) = 2
117	116	fveq2i 5867	. . . . . . . . . . . . . . . 16 |- ( ZZ>= ` ( 1 + 1 ) ) = ( ZZ>= ` 2 )
118	117	eleq2i 2545	. . . . . . . . . . . . . . 15 |- ( m e. ( ZZ>= ` ( 1 + 1 ) ) <-> m e. ( ZZ>= ` 2 ) )
119	118	orbi2i 519	. . . . . . . . . . . . . 14 |- ( ( m = 1 \/ m e. ( ZZ>= ` ( 1 + 1 ) ) ) <-> ( m = 1 \/ m e. ( ZZ>= ` 2 ) ) )
120	115, 119	sylib 196	. . . . . . . . . . . . 13 |- ( m e. ( ZZ>= ` 1 ) -> ( m = 1 \/ m e. ( ZZ>= ` 2 ) ) )
121	114, 120	syl 16	. . . . . . . . . . . 12 |- ( ( y e. NN0 /\ m e. NN0 /\ m = ( y + 1 ) ) -> ( m = 1 \/ m e. ( ZZ>= ` 2 ) ) )
122	106, 107, 108, 121	syl3anc 1228	. . . . . . . . . . 11 |- ( ( ( ( y e. NN0 /\ A. m e. NN0 ( m <_ y -> ( I ` m ) e. RR+ ) ) /\ m e. NN0 ) /\ m = ( y + 1 ) ) -> ( m = 1 \/ m e. ( ZZ>= ` 2 ) ) )
123	45, 105, 122	mpjaod 381	. . . . . . . . . 10 |- ( ( ( ( y e. NN0 /\ A. m e. NN0 ( m <_ y -> ( I ` m ) e. RR+ ) ) /\ m e. NN0 ) /\ m = ( y + 1 ) ) -> ( I ` m ) e. RR+ )
124	123	adantlr 714	. . . . . . . . 9 |- ( ( ( ( ( y e. NN0 /\ A. m e. NN0 ( m <_ y -> ( I ` m ) e. RR+ ) ) /\ m e. NN0 ) /\ m <_ ( y + 1 ) ) /\ m = ( y + 1 ) ) -> ( I ` m ) e. RR+ )
125	124	ex 434	. . . . . . . 8 |- ( ( ( ( y e. NN0 /\ A. m e. NN0 ( m <_ y -> ( I ` m ) e. RR+ ) ) /\ m e. NN0 ) /\ m <_ ( y + 1 ) ) -> ( m = ( y + 1 ) -> ( I ` m ) e. RR+ ) )
126		simplll 757	. . . . . . . . 9 |- ( ( ( ( y e. NN0 /\ A. m e. NN0 ( m <_ y -> ( I ` m ) e. RR+ ) ) /\ m e. NN0 ) /\ m <_ ( y + 1 ) ) -> y e. NN0 )
127		simpr 461	. . . . . . . . 9 |- ( ( ( ( y e. NN0 /\ A. m e. NN0 ( m <_ y -> ( I ` m ) e. RR+ ) ) /\ m e. NN0 ) /\ m <_ ( y + 1 ) ) -> m <_ ( y + 1 ) )
128		simpl1 999	. . . . . . . . . . 11 |- ( ( ( y e. NN0 /\ m e. NN0 /\ m <_ ( y + 1 ) ) /\ m < ( y + 1 ) ) -> y e. NN0 )
129		simpl2 1000	. . . . . . . . . . 11 |- ( ( ( y e. NN0 /\ m e. NN0 /\ m <_ ( y + 1 ) ) /\ m < ( y + 1 ) ) -> m e. NN0 )
130		simpr 461	. . . . . . . . . . 11 |- ( ( ( y e. NN0 /\ m e. NN0 /\ m <_ ( y + 1 ) ) /\ m < ( y + 1 ) ) -> m < ( y + 1 ) )
131		simpr 461	. . . . . . . . . . . . . . 15 |- ( ( y e. NN0 /\ m = 0 ) -> m = 0 )
132		nn0ge0 10817	. . . . . . . . . . . . . . . 16 |- ( y e. NN0 -> 0 <_ y )
133	132	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( y e. NN0 /\ m = 0 ) -> 0 <_ y )
134	131, 133	eqbrtrd 4467	. . . . . . . . . . . . . 14 |- ( ( y e. NN0 /\ m = 0 ) -> m <_ y )
135	134	3ad2antl1 1158	. . . . . . . . . . . . 13 |- ( ( ( y e. NN0 /\ m e. NN0 /\ m < ( y + 1 ) ) /\ m = 0 ) -> m <_ y )
136		simpl1 999	. . . . . . . . . . . . . 14 |- ( ( ( y e. NN0 /\ m e. NN0 /\ m < ( y + 1 ) ) /\ m e. NN ) -> y e. NN0 )
137		simpr 461	. . . . . . . . . . . . . 14 |- ( ( ( y e. NN0 /\ m e. NN0 /\ m < ( y + 1 ) ) /\ m e. NN ) -> m e. NN )
138		simpl3 1001	. . . . . . . . . . . . . 14 |- ( ( ( y e. NN0 /\ m e. NN0 /\ m < ( y + 1 ) ) /\ m e. NN ) -> m < ( y + 1 ) )
139		simp3 998	. . . . . . . . . . . . . . 15 |- ( ( y e. NN0 /\ m e. NN /\ m < ( y + 1 ) ) -> m < ( y + 1 ) )
140		simp2 997	. . . . . . . . . . . . . . . 16 |- ( ( y e. NN0 /\ m e. NN /\ m < ( y + 1 ) ) -> m e. NN )
141		simp1 996	. . . . . . . . . . . . . . . . 17 |- ( ( y e. NN0 /\ m e. NN /\ m < ( y + 1 ) ) -> y e. NN0 )
142	18	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( y e. NN0 /\ m e. NN /\ m < ( y + 1 ) ) -> 0 e. RR )
143	53	3ad2ant2 1018	. . . . . . . . . . . . . . . . . . 19 |- ( ( y e. NN0 /\ m e. NN /\ m < ( y + 1 ) ) -> ( m - 1 ) e. RR )
144	80	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . 19 |- ( ( y e. NN0 /\ m e. NN /\ m < ( y + 1 ) ) -> y e. RR )
145		nnm1nn0 10833	. . . . . . . . . . . . . . . . . . . . 21 |- ( m e. NN -> ( m - 1 ) e. NN0 )
146	145	nn0ge0d 10851	. . . . . . . . . . . . . . . . . . . 20 |- ( m e. NN -> 0 <_ ( m - 1 ) )
147	146	3ad2ant2 1018	. . . . . . . . . . . . . . . . . . 19 |- ( ( y e. NN0 /\ m e. NN /\ m < ( y + 1 ) ) -> 0 <_ ( m - 1 ) )
148	50	3ad2ant2 1018	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( y e. NN0 /\ m e. NN /\ m < ( y + 1 ) ) -> m e. RR )
149	51	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( y e. NN0 /\ m e. NN /\ m < ( y + 1 ) ) -> 1 e. RR )
150	148, 149, 144	ltsubaddd 10144	. . . . . . . . . . . . . . . . . . . 20 |- ( ( y e. NN0 /\ m e. NN /\ m < ( y + 1 ) ) -> ( ( m - 1 ) < y <-> m < ( y + 1 ) ) )
151	139, 150	mpbird 232	. . . . . . . . . . . . . . . . . . 19 |- ( ( y e. NN0 /\ m e. NN /\ m < ( y + 1 ) ) -> ( m - 1 ) < y )
152	142, 143, 144, 147, 151	lelttrd 9735	. . . . . . . . . . . . . . . . . 18 |- ( ( y e. NN0 /\ m e. NN /\ m < ( y + 1 ) ) -> 0 < y )
153	152	gt0ne0d 10113	. . . . . . . . . . . . . . . . 17 |- ( ( y e. NN0 /\ m e. NN /\ m < ( y + 1 ) ) -> y =/= 0 )
154		elnnne0 10805	. . . . . . . . . . . . . . . . 17 |- ( y e. NN <-> ( y e. NN0 /\ y =/= 0 ) )
155	141, 153, 154	sylanbrc 664	. . . . . . . . . . . . . . . 16 |- ( ( y e. NN0 /\ m e. NN /\ m < ( y + 1 ) ) -> y e. NN )
156		nnleltp1 10913	. . . . . . . . . . . . . . . 16 |- ( ( m e. NN /\ y e. NN ) -> ( m <_ y <-> m < ( y + 1 ) ) )
157	140, 155, 156	syl2anc 661	. . . . . . . . . . . . . . 15 |- ( ( y e. NN0 /\ m e. NN /\ m < ( y + 1 ) ) -> ( m <_ y <-> m < ( y + 1 ) ) )
158	139, 157	mpbird 232	. . . . . . . . . . . . . 14 |- ( ( y e. NN0 /\ m e. NN /\ m < ( y + 1 ) ) -> m <_ y )
159	136, 137, 138, 158	syl3anc 1228	. . . . . . . . . . . . 13 |- ( ( ( y e. NN0 /\ m e. NN0 /\ m < ( y + 1 ) ) /\ m e. NN ) -> m <_ y )
160		elnn0 10793	. . . . . . . . . . . . . . . 16 |- ( m e. NN0 <-> ( m e. NN \/ m = 0 ) )
161	160	biimpi 194	. . . . . . . . . . . . . . 15 |- ( m e. NN0 -> ( m e. NN \/ m = 0 ) )
162	161	orcomd 388	. . . . . . . . . . . . . 14 |- ( m e. NN0 -> ( m = 0 \/ m e. NN ) )
163	162	3ad2ant2 1018	. . . . . . . . . . . . 13 |- ( ( y e. NN0 /\ m e. NN0 /\ m < ( y + 1 ) ) -> ( m = 0 \/ m e. NN ) )
164	135, 159, 163	mpjaodan 784	. . . . . . . . . . . 12 |- ( ( y e. NN0 /\ m e. NN0 /\ m < ( y + 1 ) ) -> m <_ y )
165	164	orcd 392	. . . . . . . . . . 11 |- ( ( y e. NN0 /\ m e. NN0 /\ m < ( y + 1 ) ) -> ( m <_ y \/ m = ( y + 1 ) ) )
166	128, 129, 130, 165	syl3anc 1228	. . . . . . . . . 10 |- ( ( ( y e. NN0 /\ m e. NN0 /\ m <_ ( y + 1 ) ) /\ m < ( y + 1 ) ) -> ( m <_ y \/ m = ( y + 1 ) ) )
167		simpr 461	. . . . . . . . . . 11 |- ( ( ( y e. NN0 /\ m e. NN0 /\ m <_ ( y + 1 ) ) /\ m = ( y + 1 ) ) -> m = ( y + 1 ) )
168	167	olcd 393	. . . . . . . . . 10 |- ( ( ( y e. NN0 /\ m e. NN0 /\ m <_ ( y + 1 ) ) /\ m = ( y + 1 ) ) -> ( m <_ y \/ m = ( y + 1 ) ) )
169		simp3 998	. . . . . . . . . . 11 |- ( ( y e. NN0 /\ m e. NN0 /\ m <_ ( y + 1 ) ) -> m <_ ( y + 1 ) )
170	16	3ad2ant2 1018	. . . . . . . . . . . 12 |- ( ( y e. NN0 /\ m e. NN0 /\ m <_ ( y + 1 ) ) -> m e. RR )
171	80	3ad2ant1 1017	. . . . . . . . . . . . 13 |- ( ( y e. NN0 /\ m e. NN0 /\ m <_ ( y + 1 ) ) -> y e. RR )
172	51	a1i 11	. . . . . . . . . . . . 13 |- ( ( y e. NN0 /\ m e. NN0 /\ m <_ ( y + 1 ) ) -> 1 e. RR )
173	171, 172	readdcld 9619	. . . . . . . . . . . 12 |- ( ( y e. NN0 /\ m e. NN0 /\ m <_ ( y + 1 ) ) -> ( y + 1 ) e. RR )
174	170, 173	leloed 9723	. . . . . . . . . . 11 |- ( ( y e. NN0 /\ m e. NN0 /\ m <_ ( y + 1 ) ) -> ( m <_ ( y + 1 ) <-> ( m < ( y + 1 ) \/ m = ( y + 1 ) ) ) )
175	169, 174	mpbid 210	. . . . . . . . . 10 |- ( ( y e. NN0 /\ m e. NN0 /\ m <_ ( y + 1 ) ) -> ( m < ( y + 1 ) \/ m = ( y + 1 ) ) )
176	166, 168, 175	mpjaodan 784	. . . . . . . . 9 |- ( ( y e. NN0 /\ m e. NN0 /\ m <_ ( y + 1 ) ) -> ( m <_ y \/ m = ( y + 1 ) ) )
177	126, 37, 127, 176	syl3anc 1228	. . . . . . . 8 |- ( ( ( ( y e. NN0 /\ A. m e. NN0 ( m <_ y -> ( I ` m ) e. RR+ ) ) /\ m e. NN0 ) /\ m <_ ( y + 1 ) ) -> ( m <_ y \/ m = ( y + 1 ) ) )
178	39, 125, 177	mpjaod 381	. . . . . . 7 |- ( ( ( ( y e. NN0 /\ A. m e. NN0 ( m <_ y -> ( I ` m ) e. RR+ ) ) /\ m e. NN0 ) /\ m <_ ( y + 1 ) ) -> ( I ` m ) e. RR+ )
179	178	exp31 604	. . . . . 6 |- ( ( y e. NN0 /\ A. m e. NN0 ( m <_ y -> ( I ` m ) e. RR+ ) ) -> ( m e. NN0 -> ( m <_ ( y + 1 ) -> ( I ` m ) e. RR+ ) ) )
180	35, 179	ralrimi 2864	. . . . 5 |- ( ( y e. NN0 /\ A. m e. NN0 ( m <_ y -> ( I ` m ) e. RR+ ) ) -> A. m e. NN0 ( m <_ ( y + 1 ) -> ( I ` m ) e. RR+ ) )
181	180	ex 434	. . . 4 |- ( y e. NN0 -> ( A. m e. NN0 ( m <_ y -> ( I ` m ) e. RR+ ) -> A. m e. NN0 ( m <_ ( y + 1 ) -> ( I ` m ) e. RR+ ) ) )
182	3, 6, 9, 12, 32, 181	nn0ind 10953	. . 3 |- ( N e. NN0 -> A. m e. NN0 ( m <_ N -> ( I ` m ) e. RR+ ) )
183	182	ancri 552	. 2 |- ( N e. NN0 -> ( A. m e. NN0 ( m <_ N -> ( I ` m ) e. RR+ ) /\ N e. NN0 ) )
184		nn0re 10800	. . 3 |- ( N e. NN0 -> N e. RR )
185	184	leidd 10115	. 2 |- ( N e. NN0 -> N <_ N )
186		breq1 4450	. . . 4 |- ( m = N -> ( m <_ N <-> N <_ N ) )
187		fveq2 5864	. . . . 5 |- ( m = N -> ( I ` m ) = ( I ` N ) )
188	187	eleq1d 2536	. . . 4 |- ( m = N -> ( ( I ` m ) e. RR+ <-> ( I ` N ) e. RR+ ) )
189	186, 188	imbi12d 320	. . 3 |- ( m = N -> ( ( m <_ N -> ( I ` m ) e. RR+ ) <-> ( N <_ N -> ( I ` N ) e. RR+ ) ) )
190	189	rspccva 3213	. 2 |- ( ( A. m e. NN0 ( m <_ N -> ( I ` m ) e. RR+ ) /\ N e. NN0 ) -> ( N <_ N -> ( I ` N ) e. RR+ ) )
191	183, 185, 190	sylc 60	1 |- ( N e. NN0 -> ( I ` N ) e. RR+ )

Syntax hints:   -> wi 4   <-> wb 184   \/ wo 368   /\ wa 369   /\ w3a 973   = wceq 1379   e. wcel 1767   =/= wne 2662   A.wral 2814   class class class wbr 4447   |-> cmpt 4505   ` cfv 5586  (class class class)co 6282   CCcc 9486   RRcr 9487   0cc0 9488   1c1 9489   + caddc 9491   x. cmul 9493   < clt 9624   <_ cle 9625   - cmin 9801   / cdiv 10202   NNcn 10532   2c2 10581   NN0cn0 10791   ZZ>=cuz 11078   RR+crp 11216   (,)cioo 11525   ^cexp 12130   sincsin 13657   picpi 13660   S.citg 21762

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6574  ax-inf2 8054  ax-cc 8811  ax-cnex 9544  ax-resscn 9545  ax-1cn 9546  ax-icn 9547  ax-addcl 9548  ax-addrcl 9549  ax-mulcl 9550  ax-mulrcl 9551  ax-mulcom 9552  ax-addass 9553  ax-mulass 9554  ax-distr 9555  ax-i2m1 9556  ax-1ne0 9557  ax-1rid 9558  ax-rnegex 9559  ax-rrecex 9560  ax-cnre 9561  ax-pre-lttri 9562  ax-pre-lttrn 9563  ax-pre-ltadd 9564  ax-pre-mulgt0 9565  ax-pre-sup 9566  ax-addf 9567  ax-mulf 9568

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-fal 1385  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rmo 2822  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-iin 4328  df-disj 4418  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-se 4839  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5549  df-fun 5588  df-fn 5589  df-f 5590  df-f1 5591  df-fo 5592  df-f1o 5593  df-fv 5594  df-isom 5595  df-riota 6243  df-ov 6285  df-oprab 6286  df-mpt2 6287  df-of 6522  df-ofr 6523  df-om 6679  df-1st 6781  df-2nd 6782  df-supp 6899  df-recs 7039  df-rdg 7073  df-1o 7127  df-2o 7128  df-oadd 7131  df-omul 7132  df-er 7308  df-map 7419  df-pm 7420  df-ixp 7467  df-en 7514  df-dom 7515  df-sdom 7516  df-fin 7517  df-fsupp 7826  df-fi 7867  df-sup 7897  df-oi 7931  df-card 8316  df-acn 8319  df-cda 8544  df-pnf 9626  df-mnf 9627  df-xr 9628  df-ltxr 9629  df-le 9630  df-sub 9803  df-neg 9804  df-div 10203  df-nn 10533  df-2 10590  df-3 10591  df-4 10592  df-5 10593  df-6 10594  df-7 10595  df-8 10596  df-9 10597  df-10 10598  df-n0 10792  df-z 10861  df-dec 10973  df-uz 11079  df-q 11179  df-rp 11217  df-xneg 11314  df-xadd 11315  df-xmul 11316  df-ioo 11529  df-ioc 11530  df-ico 11531  df-icc 11532  df-fz 11669  df-fzo 11789  df-fl 11893  df-mod 11961  df-seq 12072  df-exp 12131  df-fac 12318  df-bc 12345  df-hash 12370  df-shft 12859  df-cj 12891  df-re 12892  df-im 12893  df-sqrt 13027  df-abs 13028  df-limsup 13253  df-clim 13270  df-rlim 13271  df-sum 13468  df-ef 13661  df-sin 13663  df-cos 13664  df-pi 13666  df-struct 14488  df-ndx 14489  df-slot 14490  df-base 14491  df-sets 14492  df-ress 14493  df-plusg 14564  df-mulr 14565  df-starv 14566  df-sca 14567  df-vsca 14568  df-ip 14569  df-tset 14570  df-ple 14571  df-ds 14573  df-unif 14574  df-hom 14575  df-cco 14576  df-rest 14674  df-topn 14675  df-0g 14693  df-gsum 14694  df-topgen 14695  df-pt 14696  df-prds 14699  df-xrs 14753  df-qtop 14758  df-imas 14759  df-xps 14761  df-mre 14837  df-mrc 14838  df-acs 14840  df-mnd 15728  df-submnd 15778  df-mulg 15861  df-cntz 16150  df-cmn 16596  df-psmet 18182  df-xmet 18183  df-met 18184  df-bl 18185  df-mopn 18186  df-fbas 18187  df-fg 18188  df-cnfld 18192  df-top 19166  df-bases 19168  df-topon 19169  df-topsp 19170  df-cld 19286  df-ntr 19287  df-cls 19288  df-nei 19365  df-lp 19403  df-perf 19404  df-cn 19494  df-cnp 19495  df-haus 19582  df-cmp 19653  df-tx 19798  df-hmeo 19991  df-fil 20082  df-fm 20174  df-flim 20175  df-flf 20176  df-xms 20558  df-ms 20559  df-tms 20560  df-cncf 21117  df-ovol 21611  df-vol 21612  df-mbf 21763  df-itg1 21764  df-itg2 21765  df-ibl 21766  df-itg 21767  df-0p 21812  df-limc 22005  df-dv 22006

This theorem is referenced by:  wallispilem4  31368  wallispilem5  31369