Metamath Proof Explorer


Theorem wallispilem3

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

Ref Expression
Hypothesis wallispilem3.1
|- I = ( n e. NN0 |-> S. ( 0 (,) _pi ) ( ( sin ` x ) ^ n ) _d x )
Assertion wallispilem3
|- ( N e. NN0 -> ( I ` N ) e. RR+ )

Proof

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