Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  wallispilem3 Structured version   Visualization version   Unicode version

Theorem wallispilem3 37939
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.
StepHypRef Expression
1 breq2 4409 . . . . . 6  |-  ( w  =  0  ->  (
m  <_  w  <->  m  <_  0 ) )
21imbi1d 319 . . . . 5  |-  ( w  =  0  ->  (
( m  <_  w  ->  ( I `  m
)  e.  RR+ )  <->  ( m  <_  0  ->  ( I `  m )  e.  RR+ ) ) )
32ralbidv 2829 . . . 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 4409 . . . . . 6  |-  ( w  =  y  ->  (
m  <_  w  <->  m  <_  y ) )
54imbi1d 319 . . . . 5  |-  ( w  =  y  ->  (
( m  <_  w  ->  ( I `  m
)  e.  RR+ )  <->  ( m  <_  y  ->  ( I `  m )  e.  RR+ ) ) )
65ralbidv 2829 . . . 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 4409 . . . . . 6  |-  ( w  =  ( y  +  1 )  ->  (
m  <_  w  <->  m  <_  ( y  +  1 ) ) )
87imbi1d 319 . . . . 5  |-  ( w  =  ( y  +  1 )  ->  (
( m  <_  w  ->  ( I `  m
)  e.  RR+ )  <->  ( m  <_  ( y  +  1 )  -> 
( I `  m
)  e.  RR+ )
) )
98ralbidv 2829 . . . 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 4409 . . . . . 6  |-  ( w  =  N  ->  (
m  <_  w  <->  m  <_  N ) )
1110imbi1d 319 . . . . 5  |-  ( w  =  N  ->  (
( m  <_  w  ->  ( I `  m
)  e.  RR+ )  <->  ( m  <_  N  ->  ( I `  m )  e.  RR+ ) ) )
1211ralbidv 2829 . . . 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 463 . . . . . . . . 9  |-  ( ( m  e.  NN0  /\  m  <_  0 )  ->  m  <_  0 )
14 nn0ge0 10902 . . . . . . . . . 10  |-  ( m  e.  NN0  ->  0  <_  m )
1514adantr 467 . . . . . . . . 9  |-  ( ( m  e.  NN0  /\  m  <_  0 )  -> 
0  <_  m )
16 nn0re 10885 . . . . . . . . . . 11  |-  ( m  e.  NN0  ->  m  e.  RR )
1716adantr 467 . . . . . . . . . 10  |-  ( ( m  e.  NN0  /\  m  <_  0 )  ->  m  e.  RR )
18 0red 9649 . . . . . . . . . 10  |-  ( ( m  e.  NN0  /\  m  <_  0 )  -> 
0  e.  RR )
1917, 18letri3d 9782 . . . . . . . . 9  |-  ( ( m  e.  NN0  /\  m  <_  0 )  -> 
( m  =  0  <-> 
( m  <_  0  /\  0  <_  m ) ) )
2013, 15, 19mpbir2and 934 . . . . . . . 8  |-  ( ( m  e.  NN0  /\  m  <_  0 )  ->  m  =  0 )
2120fveq2d 5874 . . . . . . 7  |-  ( ( m  e.  NN0  /\  m  <_  0 )  -> 
( I `  m
)  =  ( I `
 0 ) )
22 wallispilem3.1 . . . . . . . . . 10  |-  I  =  ( n  e.  NN0  |->  S. ( 0 (,) pi ) ( ( sin `  x ) ^ n
)  _d x )
2322wallispilem2 37938 . . . . . . . . 9  |-  ( ( I `  0 )  =  pi  /\  (
I `  1 )  =  2  /\  (
m  e.  ( ZZ>= ` 
2 )  ->  (
I `  m )  =  ( ( ( m  -  1 )  /  m )  x.  ( I `  (
m  -  2 ) ) ) ) )
2423simp1i 1018 . . . . . . . 8  |-  ( I `
 0 )  =  pi
25 pirp 23428 . . . . . . . 8  |-  pi  e.  RR+
2624, 25eqeltri 2527 . . . . . . 7  |-  ( I `
 0 )  e.  RR+
2721, 26syl6eqel 2539 . . . . . 6  |-  ( ( m  e.  NN0  /\  m  <_  0 )  -> 
( I `  m
)  e.  RR+ )
2827ex 436 . . . . 5  |-  ( m  e.  NN0  ->  ( m  <_  0  ->  (
I `  m )  e.  RR+ ) )
2928rgen 2749 . . . 4  |-  A. m  e.  NN0  ( m  <_ 
0  ->  ( I `  m )  e.  RR+ )
30 nfv 1763 . . . . . . 7  |-  F/ m  y  e.  NN0
31 nfra1 2771 . . . . . . 7  |-  F/ m A. m  e.  NN0  ( m  <_  y  -> 
( I `  m
)  e.  RR+ )
3230, 31nfan 2013 . . . . . 6  |-  F/ m
( y  e.  NN0  /\ 
A. m  e.  NN0  ( m  <_  y  -> 
( I `  m
)  e.  RR+ )
)
33 simpllr 770 . . . . . . . . 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+ ) )
34 simplr 763 . . . . . . . . 9  |-  ( ( ( ( y  e. 
NN0  /\  A. m  e.  NN0  ( m  <_ 
y  ->  ( I `  m )  e.  RR+ ) )  /\  m  e.  NN0 )  /\  m  <_  ( y  +  1 ) )  ->  m  e.  NN0 )
35 rsp 2756 . . . . . . . . 9  |-  ( A. m  e.  NN0  ( m  <_  y  ->  (
I `  m )  e.  RR+ )  ->  (
m  e.  NN0  ->  ( m  <_  y  ->  ( I `  m )  e.  RR+ ) ) )
3633, 34, 35sylc 62 . . . . . . . 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+ ) )
37 fveq2 5870 . . . . . . . . . . . . 13  |-  ( m  =  1  ->  (
I `  m )  =  ( I ` 
1 ) )
3823simp2i 1019 . . . . . . . . . . . . . 14  |-  ( I `
 1 )  =  2
39 2rp 11314 . . . . . . . . . . . . . 14  |-  2  e.  RR+
4038, 39eqeltri 2527 . . . . . . . . . . . . 13  |-  ( I `
 1 )  e.  RR+
4137, 40syl6eqel 2539 . . . . . . . . . . . 12  |-  ( m  =  1  ->  (
I `  m )  e.  RR+ )
4241a1i 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+ ) )
4323simp3i 1020 . . . . . . . . . . . . . . 15  |-  ( m  e.  ( ZZ>= `  2
)  ->  ( I `  m )  =  ( ( ( m  - 
1 )  /  m
)  x.  ( I `
 ( m  - 
2 ) ) ) )
4443adantl 468 . . . . . . . . . . . . . 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
) ) ) )
45 eluz2nn 11204 . . . . . . . . . . . . . . . . . . 19  |-  ( m  e.  ( ZZ>= `  2
)  ->  m  e.  NN )
46 nnre 10623 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  e.  NN  ->  m  e.  RR )
47 1red 9663 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  e.  NN  ->  1  e.  RR )
4846, 47resubcld 10054 . . . . . . . . . . . . . . . . . . 19  |-  ( m  e.  NN  ->  (
m  -  1 )  e.  RR )
4945, 48syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( m  e.  ( ZZ>= `  2
)  ->  ( m  -  1 )  e.  RR )
50 1m1e0 10685 . . . . . . . . . . . . . . . . . . 19  |-  ( 1  -  1 )  =  0
51 1red 9663 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  e.  ( ZZ>= `  2
)  ->  1  e.  RR )
52 eluzelre 11176 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  e.  ( ZZ>= `  2
)  ->  m  e.  RR )
53 eluz2b2 11238 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  e.  ( ZZ>= `  2
)  <->  ( m  e.  NN  /\  1  < 
m ) )
5453simprbi 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  e.  ( ZZ>= `  2
)  ->  1  <  m )
5551, 52, 51, 54ltsub1dd 10232 . . . . . . . . . . . . . . . . . . 19  |-  ( m  e.  ( ZZ>= `  2
)  ->  ( 1  -  1 )  < 
( m  -  1 ) )
5650, 55syl5eqbrr 4440 . . . . . . . . . . . . . . . . . 18  |-  ( m  e.  ( ZZ>= `  2
)  ->  0  <  ( m  -  1 ) )
5749, 56elrpd 11345 . . . . . . . . . . . . . . . . 17  |-  ( m  e.  ( ZZ>= `  2
)  ->  ( m  -  1 )  e.  RR+ )
5845nnrpd 11346 . . . . . . . . . . . . . . . . 17  |-  ( m  e.  ( ZZ>= `  2
)  ->  m  e.  RR+ )
5957, 58rpdivcld 11365 . . . . . . . . . . . . . . . 16  |-  ( m  e.  ( ZZ>= `  2
)  ->  ( (
m  -  1 )  /  m )  e.  RR+ )
6059adantl 468 . . . . . . . . . . . . . . 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+ )
61 breq1 4408 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  =  k  ->  (
m  <_  y  <->  k  <_  y ) )
62 fveq2 5870 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( m  =  k  ->  (
I `  m )  =  ( I `  k ) )
6362eleq1d 2515 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  =  k  ->  (
( I `  m
)  e.  RR+  <->  ( I `  k )  e.  RR+ ) )
6461, 63imbi12d 322 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  k  ->  (
( m  <_  y  ->  ( I `  m
)  e.  RR+ )  <->  ( k  <_  y  ->  ( I `  k )  e.  RR+ ) ) )
6564cbvralv 3021 . . . . . . . . . . . . . . . . . . 19  |-  ( A. m  e.  NN0  ( m  <_  y  ->  (
I `  m )  e.  RR+ )  <->  A. k  e.  NN0  ( k  <_ 
y  ->  ( I `  k )  e.  RR+ ) )
6665biimpi 198 . . . . . . . . . . . . . . . . . 18  |-  ( A. m  e.  NN0  ( m  <_  y  ->  (
I `  m )  e.  RR+ )  ->  A. k  e.  NN0  ( k  <_ 
y  ->  ( I `  k )  e.  RR+ ) )
6766ad3antlr 738 . . . . . . . . . . . . . . . . 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+ )
)
68 uznn0sub 11197 . . . . . . . . . . . . . . . . . 18  |-  ( m  e.  ( ZZ>= `  2
)  ->  ( m  -  2 )  e. 
NN0 )
6968adantl 468 . . . . . . . . . . . . . . . . 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 )
7067, 69jca 535 . . . . . . . . . . . . . . . 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 ) )
71 simplll 769 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 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 763 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 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 463 . . . . . . . . . . . . . . . . 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 ) )
74 simp2 1010 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( y  e.  NN0  /\  m  =  ( y  +  1 )  /\  m  e.  ( ZZ>= ` 
2 ) )  ->  m  =  ( y  +  1 ) )
7574oveq1d 6310 . . . . . . . . . . . . . . . . . . 19  |-  ( ( y  e.  NN0  /\  m  =  ( y  +  1 )  /\  m  e.  ( ZZ>= ` 
2 ) )  -> 
( m  -  2 )  =  ( ( y  +  1 )  -  2 ) )
76 nn0re 10885 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  NN0  ->  y  e.  RR )
77763ad2ant1 1030 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( y  e.  NN0  /\  m  =  ( y  +  1 )  /\  m  e.  ( ZZ>= ` 
2 ) )  -> 
y  e.  RR )
7877recnd 9674 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( y  e.  NN0  /\  m  =  ( y  +  1 )  /\  m  e.  ( ZZ>= ` 
2 ) )  -> 
y  e.  CC )
79 df-2 10675 . . . . . . . . . . . . . . . . . . . . . . 23  |-  2  =  ( 1  +  1 )
8079a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  CC  ->  2  =  ( 1  +  1 ) )
8180oveq2d 6311 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  CC  ->  (
( y  +  1 )  -  2 )  =  ( ( y  +  1 )  -  ( 1  +  1 ) ) )
82 id 22 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  CC  ->  y  e.  CC )
83 1cnd 9664 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  CC  ->  1  e.  CC )
8482, 83, 83pnpcan2d 10029 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  CC  ->  (
( y  +  1 )  -  ( 1  +  1 ) )  =  ( y  - 
1 ) )
8581, 84eqtrd 2487 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  CC  ->  (
( y  +  1 )  -  2 )  =  ( y  - 
1 ) )
8678, 85syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ( y  e.  NN0  /\  m  =  ( y  +  1 )  /\  m  e.  ( ZZ>= ` 
2 ) )  -> 
( ( y  +  1 )  -  2 )  =  ( y  -  1 ) )
8775, 86eqtrd 2487 . . . . . . . . . . . . . . . . . 18  |-  ( ( y  e.  NN0  /\  m  =  ( y  +  1 )  /\  m  e.  ( ZZ>= ` 
2 ) )  -> 
( m  -  2 )  =  ( y  -  1 ) )
8877lem1d 10547 . . . . . . . . . . . . . . . . . 18  |-  ( ( y  e.  NN0  /\  m  =  ( y  +  1 )  /\  m  e.  ( ZZ>= ` 
2 ) )  -> 
( y  -  1 )  <_  y )
8987, 88eqbrtrd 4426 . . . . . . . . . . . . . . . . 17  |-  ( ( y  e.  NN0  /\  m  =  ( y  +  1 )  /\  m  e.  ( ZZ>= ` 
2 ) )  -> 
( m  -  2 )  <_  y )
9071, 72, 73, 89syl3anc 1269 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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 4408 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  ( m  - 
2 )  ->  (
k  <_  y  <->  ( m  -  2 )  <_ 
y ) )
92 fveq2 5870 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  ( m  - 
2 )  ->  (
I `  k )  =  ( I `  ( m  -  2
) ) )
9392eleq1d 2515 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  ( m  - 
2 )  ->  (
( I `  k
)  e.  RR+  <->  ( I `  ( m  -  2 ) )  e.  RR+ ) )
9491, 93imbi12d 322 . . . . . . . . . . . . . . . . 17  |-  ( k  =  ( m  - 
2 )  ->  (
( k  <_  y  ->  ( I `  k
)  e.  RR+ )  <->  ( ( m  -  2 )  <_  y  ->  ( I `  ( m  -  2 ) )  e.  RR+ ) ) )
9594rspccva 3151 . . . . . . . . . . . . . . . 16  |-  ( ( A. k  e.  NN0  ( k  <_  y  ->  ( I `  k
)  e.  RR+ )  /\  ( m  -  2 )  e.  NN0 )  ->  ( ( m  - 
2 )  <_  y  ->  ( I `  (
m  -  2 ) )  e.  RR+ )
)
9670, 90, 95sylc 62 . . . . . . . . . . . . . . 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+ )
9760, 96rpmulcld 11364 . . . . . . . . . . . . . 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+ )
9844, 97eqeltrd 2531 . . . . . . . . . . . . 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+ )
9998adantllr 726 . . . . . . . . . . . 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+ )
10099ex 436 . . . . . . . . . . 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+ )
)
101 simplll 769 . . . . . . . . . . . 12  |-  ( ( ( ( y  e. 
NN0  /\  A. m  e.  NN0  ( m  <_ 
y  ->  ( I `  m )  e.  RR+ ) )  /\  m  e.  NN0 )  /\  m  =  ( y  +  1 ) )  -> 
y  e.  NN0 )
102 simplr 763 . . . . . . . . . . . 12  |-  ( ( ( ( y  e. 
NN0  /\  A. m  e.  NN0  ( m  <_ 
y  ->  ( I `  m )  e.  RR+ ) )  /\  m  e.  NN0 )  /\  m  =  ( y  +  1 ) )  ->  m  e.  NN0 )
103 simpr 463 . . . . . . . . . . . 12  |-  ( ( ( ( y  e. 
NN0  /\  A. m  e.  NN0  ( m  <_ 
y  ->  ( I `  m )  e.  RR+ ) )  /\  m  e.  NN0 )  /\  m  =  ( y  +  1 ) )  ->  m  =  ( y  +  1 ) )
104 simp3 1011 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  NN0  /\  m  e.  NN0  /\  m  =  ( y  +  1 ) )  ->  m  =  ( y  +  1 ) )
105 nn0p1nn 10916 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN0  ->  ( y  +  1 )  e.  NN )
1061053ad2ant1 1030 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  NN0  /\  m  e.  NN0  /\  m  =  ( y  +  1 ) )  -> 
( y  +  1 )  e.  NN )
107104, 106eqeltrd 2531 . . . . . . . . . . . . . 14  |-  ( ( y  e.  NN0  /\  m  e.  NN0  /\  m  =  ( y  +  1 ) )  ->  m  e.  NN )
108 elnnuz 11202 . . . . . . . . . . . . . 14  |-  ( m  e.  NN  <->  m  e.  ( ZZ>= `  1 )
)
109107, 108sylib 200 . . . . . . . . . . . . 13  |-  ( ( y  e.  NN0  /\  m  e.  NN0  /\  m  =  ( y  +  1 ) )  ->  m  e.  ( ZZ>= ` 
1 ) )
110 uzp1 11199 . . . . . . . . . . . . . 14  |-  ( m  e.  ( ZZ>= `  1
)  ->  ( m  =  1  \/  m  e.  ( ZZ>= `  ( 1  +  1 ) ) ) )
111 1p1e2 10730 . . . . . . . . . . . . . . . . 17  |-  ( 1  +  1 )  =  2
112111fveq2i 5873 . . . . . . . . . . . . . . . 16  |-  ( ZZ>= `  ( 1  +  1 ) )  =  (
ZZ>= `  2 )
113112eleq2i 2523 . . . . . . . . . . . . . . 15  |-  ( m  e.  ( ZZ>= `  (
1  +  1 ) )  <->  m  e.  ( ZZ>=
`  2 ) )
114113orbi2i 522 . . . . . . . . . . . . . 14  |-  ( ( m  =  1  \/  m  e.  ( ZZ>= `  ( 1  +  1 ) ) )  <->  ( m  =  1  \/  m  e.  ( ZZ>= `  2 )
) )
115110, 114sylib 200 . . . . . . . . . . . . 13  |-  ( m  e.  ( ZZ>= `  1
)  ->  ( m  =  1  \/  m  e.  ( ZZ>= `  2 )
) )
116109, 115syl 17 . . . . . . . . . . . 12  |-  ( ( y  e.  NN0  /\  m  e.  NN0  /\  m  =  ( y  +  1 ) )  -> 
( m  =  1  \/  m  e.  (
ZZ>= `  2 ) ) )
117101, 102, 103, 116syl3anc 1269 . . . . . . . . . . 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 ) ) )
11842, 100, 117mpjaod 383 . . . . . . . . . 10  |-  ( ( ( ( y  e. 
NN0  /\  A. m  e.  NN0  ( m  <_ 
y  ->  ( I `  m )  e.  RR+ ) )  /\  m  e.  NN0 )  /\  m  =  ( y  +  1 ) )  -> 
( I `  m
)  e.  RR+ )
119118adantlr 722 . . . . . . . . 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+ )
120119ex 436 . . . . . . . 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+ )
)
121 simplll 769 . . . . . . . . 9  |-  ( ( ( ( y  e. 
NN0  /\  A. m  e.  NN0  ( m  <_ 
y  ->  ( I `  m )  e.  RR+ ) )  /\  m  e.  NN0 )  /\  m  <_  ( y  +  1 ) )  ->  y  e.  NN0 )
122 simpr 463 . . . . . . . . 9  |-  ( ( ( ( y  e. 
NN0  /\  A. m  e.  NN0  ( m  <_ 
y  ->  ( I `  m )  e.  RR+ ) )  /\  m  e.  NN0 )  /\  m  <_  ( y  +  1 ) )  ->  m  <_  ( y  +  1 ) )
123 simpl1 1012 . . . . . . . . . . 11  |-  ( ( ( y  e.  NN0  /\  m  e.  NN0  /\  m  <_  ( y  +  1 ) )  /\  m  <  ( y  +  1 ) )  -> 
y  e.  NN0 )
124 simpl2 1013 . . . . . . . . . . 11  |-  ( ( ( y  e.  NN0  /\  m  e.  NN0  /\  m  <_  ( y  +  1 ) )  /\  m  <  ( y  +  1 ) )  ->  m  e.  NN0 )
125 simpr 463 . . . . . . . . . . 11  |-  ( ( ( y  e.  NN0  /\  m  e.  NN0  /\  m  <_  ( y  +  1 ) )  /\  m  <  ( y  +  1 ) )  ->  m  <  ( y  +  1 ) )
126 simpr 463 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  NN0  /\  m  =  0 )  ->  m  =  0 )
127 nn0ge0 10902 . . . . . . . . . . . . . . . 16  |-  ( y  e.  NN0  ->  0  <_ 
y )
128127adantr 467 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  NN0  /\  m  =  0 )  ->  0  <_  y
)
129126, 128eqbrtrd 4426 . . . . . . . . . . . . . 14  |-  ( ( y  e.  NN0  /\  m  =  0 )  ->  m  <_  y
)
1301293ad2antl1 1171 . . . . . . . . . . . . 13  |-  ( ( ( y  e.  NN0  /\  m  e.  NN0  /\  m  <  ( y  +  1 ) )  /\  m  =  0 )  ->  m  <_  y
)
131 simpl1 1012 . . . . . . . . . . . . . 14  |-  ( ( ( y  e.  NN0  /\  m  e.  NN0  /\  m  <  ( y  +  1 ) )  /\  m  e.  NN )  ->  y  e.  NN0 )
132 simpr 463 . . . . . . . . . . . . . 14  |-  ( ( ( y  e.  NN0  /\  m  e.  NN0  /\  m  <  ( y  +  1 ) )  /\  m  e.  NN )  ->  m  e.  NN )
133 simpl3 1014 . . . . . . . . . . . . . 14  |-  ( ( ( y  e.  NN0  /\  m  e.  NN0  /\  m  <  ( y  +  1 ) )  /\  m  e.  NN )  ->  m  <  ( y  +  1 ) )
134 simp3 1011 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  NN0  /\  m  e.  NN  /\  m  <  ( y  +  1 ) )  ->  m  <  ( y  +  1 ) )
135 simp2 1010 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  NN0  /\  m  e.  NN  /\  m  <  ( y  +  1 ) )  ->  m  e.  NN )
136 simp1 1009 . . . . . . . . . . . . . . . . 17  |-  ( ( y  e.  NN0  /\  m  e.  NN  /\  m  <  ( y  +  1 ) )  ->  y  e.  NN0 )
137 0red 9649 . . . . . . . . . . . . . . . . . . 19  |-  ( ( y  e.  NN0  /\  m  e.  NN  /\  m  <  ( y  +  1 ) )  ->  0  e.  RR )
138483ad2ant2 1031 . . . . . . . . . . . . . . . . . . 19  |-  ( ( y  e.  NN0  /\  m  e.  NN  /\  m  <  ( y  +  1 ) )  ->  (
m  -  1 )  e.  RR )
139763ad2ant1 1030 . . . . . . . . . . . . . . . . . . 19  |-  ( ( y  e.  NN0  /\  m  e.  NN  /\  m  <  ( y  +  1 ) )  ->  y  e.  RR )
140 nnm1ge0 11011 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  e.  NN  ->  0  <_  ( m  -  1 ) )
1411403ad2ant2 1031 . . . . . . . . . . . . . . . . . . 19  |-  ( ( y  e.  NN0  /\  m  e.  NN  /\  m  <  ( y  +  1 ) )  ->  0  <_  ( m  -  1 ) )
142463ad2ant2 1031 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( y  e.  NN0  /\  m  e.  NN  /\  m  <  ( y  +  1 ) )  ->  m  e.  RR )
143 1red 9663 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( y  e.  NN0  /\  m  e.  NN  /\  m  <  ( y  +  1 ) )  ->  1  e.  RR )
144142, 143, 139ltsubaddd 10216 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( y  e.  NN0  /\  m  e.  NN  /\  m  <  ( y  +  1 ) )  ->  (
( m  -  1 )  <  y  <->  m  <  ( y  +  1 ) ) )
145134, 144mpbird 236 . . . . . . . . . . . . . . . . . . 19  |-  ( ( y  e.  NN0  /\  m  e.  NN  /\  m  <  ( y  +  1 ) )  ->  (
m  -  1 )  <  y )
146137, 138, 139, 141, 145lelttrd 9798 . . . . . . . . . . . . . . . . . 18  |-  ( ( y  e.  NN0  /\  m  e.  NN  /\  m  <  ( y  +  1 ) )  ->  0  <  y )
147146gt0ne0d 10185 . . . . . . . . . . . . . . . . 17  |-  ( ( y  e.  NN0  /\  m  e.  NN  /\  m  <  ( y  +  1 ) )  ->  y  =/=  0 )
148 elnnne0 10890 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  NN  <->  ( y  e.  NN0  /\  y  =/=  0 ) )
149136, 147, 148sylanbrc 671 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  NN0  /\  m  e.  NN  /\  m  <  ( y  +  1 ) )  ->  y  e.  NN )
150 nnleltp1 10998 . . . . . . . . . . . . . . . 16  |-  ( ( m  e.  NN  /\  y  e.  NN )  ->  ( m  <_  y  <->  m  <  ( y  +  1 ) ) )
151135, 149, 150syl2anc 667 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  NN0  /\  m  e.  NN  /\  m  <  ( y  +  1 ) )  ->  (
m  <_  y  <->  m  <  ( y  +  1 ) ) )
152134, 151mpbird 236 . . . . . . . . . . . . . 14  |-  ( ( y  e.  NN0  /\  m  e.  NN  /\  m  <  ( y  +  1 ) )  ->  m  <_  y )
153131, 132, 133, 152syl3anc 1269 . . . . . . . . . . . . 13  |-  ( ( ( y  e.  NN0  /\  m  e.  NN0  /\  m  <  ( y  +  1 ) )  /\  m  e.  NN )  ->  m  <_  y )
154 elnn0 10878 . . . . . . . . . . . . . . . 16  |-  ( m  e.  NN0  <->  ( m  e.  NN  \/  m  =  0 ) )
155154biimpi 198 . . . . . . . . . . . . . . 15  |-  ( m  e.  NN0  ->  ( m  e.  NN  \/  m  =  0 ) )
156155orcomd 390 . . . . . . . . . . . . . 14  |-  ( m  e.  NN0  ->  ( m  =  0  \/  m  e.  NN ) )
1571563ad2ant2 1031 . . . . . . . . . . . . 13  |-  ( ( y  e.  NN0  /\  m  e.  NN0  /\  m  <  ( y  +  1 ) )  ->  (
m  =  0  \/  m  e.  NN ) )
158130, 153, 157mpjaodan 796 . . . . . . . . . . . 12  |-  ( ( y  e.  NN0  /\  m  e.  NN0  /\  m  <  ( y  +  1 ) )  ->  m  <_  y )
159158orcd 394 . . . . . . . . . . 11  |-  ( ( y  e.  NN0  /\  m  e.  NN0  /\  m  <  ( y  +  1 ) )  ->  (
m  <_  y  \/  m  =  ( y  +  1 ) ) )
160123, 124, 125, 159syl3anc 1269 . . . . . . . . . 10  |-  ( ( ( y  e.  NN0  /\  m  e.  NN0  /\  m  <_  ( y  +  1 ) )  /\  m  <  ( y  +  1 ) )  -> 
( m  <_  y  \/  m  =  (
y  +  1 ) ) )
161 simpr 463 . . . . . . . . . . 11  |-  ( ( ( y  e.  NN0  /\  m  e.  NN0  /\  m  <_  ( y  +  1 ) )  /\  m  =  ( y  +  1 ) )  ->  m  =  ( y  +  1 ) )
162161olcd 395 . . . . . . . . . 10  |-  ( ( ( y  e.  NN0  /\  m  e.  NN0  /\  m  <_  ( y  +  1 ) )  /\  m  =  ( y  +  1 ) )  ->  ( m  <_ 
y  \/  m  =  ( y  +  1 ) ) )
163 simp3 1011 . . . . . . . . . . 11  |-  ( ( y  e.  NN0  /\  m  e.  NN0  /\  m  <_  ( y  +  1 ) )  ->  m  <_  ( y  +  1 ) )
164163ad2ant2 1031 . . . . . . . . . . . 12  |-  ( ( y  e.  NN0  /\  m  e.  NN0  /\  m  <_  ( y  +  1 ) )  ->  m  e.  RR )
165763ad2ant1 1030 . . . . . . . . . . . . 13  |-  ( ( y  e.  NN0  /\  m  e.  NN0  /\  m  <_  ( y  +  1 ) )  ->  y  e.  RR )
166 1red 9663 . . . . . . . . . . . . 13  |-  ( ( y  e.  NN0  /\  m  e.  NN0  /\  m  <_  ( y  +  1 ) )  ->  1  e.  RR )
167165, 166readdcld 9675 . . . . . . . . . . . 12  |-  ( ( y  e.  NN0  /\  m  e.  NN0  /\  m  <_  ( y  +  1 ) )  ->  (
y  +  1 )  e.  RR )
168164, 167leloed 9783 . . . . . . . . . . 11  |-  ( ( y  e.  NN0  /\  m  e.  NN0  /\  m  <_  ( y  +  1 ) )  ->  (
m  <_  ( y  +  1 )  <->  ( m  <  ( y  +  1 )  \/  m  =  ( y  +  1 ) ) ) )
169163, 168mpbid 214 . . . . . . . . . 10  |-  ( ( y  e.  NN0  /\  m  e.  NN0  /\  m  <_  ( y  +  1 ) )  ->  (
m  <  ( y  +  1 )  \/  m  =  ( y  +  1 ) ) )
170160, 162, 169mpjaodan 796 . . . . . . . . 9  |-  ( ( y  e.  NN0  /\  m  e.  NN0  /\  m  <_  ( y  +  1 ) )  ->  (
m  <_  y  \/  m  =  ( y  +  1 ) ) )
171121, 34, 122, 170syl3anc 1269 . . . . . . . 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 ) ) )
17236, 120, 171mpjaod 383 . . . . . . 7  |-  ( ( ( ( y  e. 
NN0  /\  A. m  e.  NN0  ( m  <_ 
y  ->  ( I `  m )  e.  RR+ ) )  /\  m  e.  NN0 )  /\  m  <_  ( y  +  1 ) )  ->  (
I `  m )  e.  RR+ )
173172exp31 609 . . . . . 6  |-  ( ( y  e.  NN0  /\  A. m  e.  NN0  (
m  <_  y  ->  ( I `  m )  e.  RR+ ) )  -> 
( m  e.  NN0  ->  ( m  <_  (
y  +  1 )  ->  ( I `  m )  e.  RR+ ) ) )
17432, 173ralrimi 2790 . . . . 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+ )
)
175174ex 436 . . . 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+ ) ) )
1763, 6, 9, 12, 29, 175nn0ind 11037 . . 3  |-  ( N  e.  NN0  ->  A. m  e.  NN0  ( m  <_  N  ->  ( I `  m )  e.  RR+ ) )
177176ancri 555 . 2  |-  ( N  e.  NN0  ->  ( A. m  e.  NN0  ( m  <_  N  ->  (
I `  m )  e.  RR+ )  /\  N  e.  NN0 ) )
178 nn0re 10885 . . 3  |-  ( N  e.  NN0  ->  N  e.  RR )
179178leidd 10187 . 2  |-  ( N  e.  NN0  ->  N  <_  N )
180 breq1 4408 . . . 4  |-  ( m  =  N  ->  (
m  <_  N  <->  N  <_  N ) )
181 fveq2 5870 . . . . 5  |-  ( m  =  N  ->  (
I `  m )  =  ( I `  N ) )
182181eleq1d 2515 . . . 4  |-  ( m  =  N  ->  (
( I `  m
)  e.  RR+  <->  ( I `  N )  e.  RR+ ) )
183180, 182imbi12d 322 . . 3  |-  ( m  =  N  ->  (
( m  <_  N  ->  ( I `  m
)  e.  RR+ )  <->  ( N  <_  N  ->  ( I `  N )  e.  RR+ ) ) )
184183rspccva 3151 . 2  |-  ( ( A. m  e.  NN0  ( m  <_  N  -> 
( I `  m
)  e.  RR+ )  /\  N  e.  NN0 )  ->  ( N  <_  N  ->  ( I `  N )  e.  RR+ ) )
185177, 179, 184sylc 62 1  |-  ( N  e.  NN0  ->  ( I `
 N )  e.  RR+ )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    \/ wo 370    /\ wa 371    /\ w3a 986    = wceq 1446    e. wcel 1889    =/= wne 2624   A.wral 2739   class class class wbr 4405    |-> cmpt 4464   ` cfv 5585  (class class class)co 6295   CCcc 9542   RRcr 9543   0cc0 9544   1c1 9545    + caddc 9547    x. cmul 9549    < clt 9680    <_ cle 9681    - cmin 9865    / cdiv 10276   NNcn 10616   2c2 10666   NN0cn0 10876   ZZ>=cuz 11166   RR+crp 11309   (,)cioo 11642   ^cexp 12279   sincsin 14128   picpi 14131   S.citg 22588
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-8 1891  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-rep 4518  ax-sep 4528  ax-nul 4537  ax-pow 4584  ax-pr 4642  ax-un 6588  ax-inf2 8151  ax-cc 8870  ax-cnex 9600  ax-resscn 9601  ax-1cn 9602  ax-icn 9603  ax-addcl 9604  ax-addrcl 9605  ax-mulcl 9606  ax-mulrcl 9607  ax-mulcom 9608  ax-addass 9609  ax-mulass 9610  ax-distr 9611  ax-i2m1 9612  ax-1ne0 9613  ax-1rid 9614  ax-rnegex 9615  ax-rrecex 9616  ax-cnre 9617  ax-pre-lttri 9618  ax-pre-lttrn 9619  ax-pre-ltadd 9620  ax-pre-mulgt0 9621  ax-pre-sup 9622  ax-addf 9623  ax-mulf 9624
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 987  df-3an 988  df-tru 1449  df-fal 1452  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-nel 2627  df-ral 2744  df-rex 2745  df-reu 2746  df-rmo 2747  df-rab 2748  df-v 3049  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-pss 3422  df-nul 3734  df-if 3884  df-pw 3955  df-sn 3971  df-pr 3973  df-tp 3975  df-op 3977  df-uni 4202  df-int 4238  df-iun 4283  df-iin 4284  df-disj 4377  df-br 4406  df-opab 4465  df-mpt 4466  df-tr 4501  df-eprel 4748  df-id 4752  df-po 4758  df-so 4759  df-fr 4796  df-se 4797  df-we 4798  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-pred 5383  df-ord 5429  df-on 5430  df-lim 5431  df-suc 5432  df-iota 5549  df-fun 5587  df-fn 5588  df-f 5589  df-f1 5590  df-fo 5591  df-f1o 5592  df-fv 5593  df-isom 5594  df-riota 6257  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-of 6536  df-ofr 6537  df-om 6698  df-1st 6798  df-2nd 6799  df-supp 6920  df-wrecs 7033  df-recs 7095  df-rdg 7133  df-1o 7187  df-2o 7188  df-oadd 7191  df-omul 7192  df-er 7368  df-map 7479  df-pm 7480  df-ixp 7528  df-en 7575  df-dom 7576  df-sdom 7577  df-fin 7578  df-fsupp 7889  df-fi 7930  df-sup 7961  df-inf 7962  df-oi 8030  df-card 8378  df-acn 8381  df-cda 8603  df-pnf 9682  df-mnf 9683  df-xr 9684  df-ltxr 9685  df-le 9686  df-sub 9867  df-neg 9868  df-div 10277  df-nn 10617  df-2 10675  df-3 10676  df-4 10677  df-5 10678  df-6 10679  df-7 10680  df-8 10681  df-9 10682  df-10 10683  df-n0 10877  df-z 10945  df-dec 11059  df-uz 11167  df-q 11272  df-rp 11310  df-xneg 11416  df-xadd 11417  df-xmul 11418  df-ioo 11646  df-ioc 11647  df-ico 11648  df-icc 11649  df-fz 11792  df-fzo 11923  df-fl 12035  df-mod 12104  df-seq 12221  df-exp 12280  df-fac 12467  df-bc 12495  df-hash 12523  df-shft 13142  df-cj 13174  df-re 13175  df-im 13176  df-sqrt 13310  df-abs 13311  df-limsup 13538  df-clim 13564  df-rlim 13565  df-sum 13765  df-ef 14133  df-sin 14135  df-cos 14136  df-pi 14138  df-struct 15135  df-ndx 15136  df-slot 15137  df-base 15138  df-sets 15139  df-ress 15140  df-plusg 15215  df-mulr 15216  df-starv 15217  df-sca 15218  df-vsca 15219  df-ip 15220  df-tset 15221  df-ple 15222  df-ds 15224  df-unif 15225  df-hom 15226  df-cco 15227  df-rest 15333  df-topn 15334  df-0g 15352  df-gsum 15353  df-topgen 15354  df-pt 15355  df-prds 15358  df-xrs 15412  df-qtop 15418  df-imas 15419  df-xps 15422  df-mre 15504  df-mrc 15505  df-acs 15507  df-mgm 16500  df-sgrp 16539  df-mnd 16549  df-submnd 16595  df-mulg 16688  df-cntz 16983  df-cmn 17444  df-psmet 18974  df-xmet 18975  df-met 18976  df-bl 18977  df-mopn 18978  df-fbas 18979  df-fg 18980  df-cnfld 18983  df-top 19933  df-bases 19934  df-topon 19935  df-topsp 19936  df-cld 20046  df-ntr 20047  df-cls 20048  df-nei 20126  df-lp 20164  df-perf 20165  df-cn 20255  df-cnp 20256  df-haus 20343  df-cmp 20414  df-tx 20589  df-hmeo 20782  df-fil 20873  df-fm 20965  df-flim 20966  df-flf 20967  df-xms 21347  df-ms 21348  df-tms 21349  df-cncf 21922  df-ovol 22428  df-vol 22430  df-mbf 22589  df-itg1 22590  df-itg2 22591  df-ibl 22592  df-itg 22593  df-0p 22640  df-limc 22833  df-dv 22834
This theorem is referenced by:  wallispilem4  37940  wallispilem5  37941
  Copyright terms: Public domain W3C validator