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+ )