ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eirraplem Unicode version

Theorem eirraplem 11797
Description: Lemma for eirrap 11798. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Jim Kingdon, 5-Jan-2022.)
Hypotheses
Ref Expression
eirr.1  |-  F  =  ( n  e.  NN0  |->  ( 1  /  ( ! `  n )
) )
eirr.2  |-  ( ph  ->  P  e.  ZZ )
eirr.3  |-  ( ph  ->  Q  e.  NN )
Assertion
Ref Expression
eirraplem  |-  ( ph  ->  _e #  ( P  /  Q ) )
Distinct variable group:    Q, n
Allowed substitution hints:    ph( n)    P( n)    F( n)

Proof of Theorem eirraplem
Dummy variable  k is distinct from all other variables.
StepHypRef Expression
1 esum 11683 . . . . . . . . . . 11  |-  _e  =  sum_ k  e.  NN0  (
1  /  ( ! `
 k ) )
2 faccl 10728 . . . . . . . . . . . . . 14  |-  ( k  e.  NN0  ->  ( ! `
 k )  e.  NN )
32nnrecred 8979 . . . . . . . . . . . . 13  |-  ( k  e.  NN0  ->  ( 1  /  ( ! `  k ) )  e.  RR )
4 fveq2 5527 . . . . . . . . . . . . . . 15  |-  ( n  =  k  ->  ( ! `  n )  =  ( ! `  k ) )
54oveq2d 5904 . . . . . . . . . . . . . 14  |-  ( n  =  k  ->  (
1  /  ( ! `
 n ) )  =  ( 1  / 
( ! `  k
) ) )
6 eirr.1 . . . . . . . . . . . . . 14  |-  F  =  ( n  e.  NN0  |->  ( 1  /  ( ! `  n )
) )
75, 6fvmptg 5605 . . . . . . . . . . . . 13  |-  ( ( k  e.  NN0  /\  ( 1  /  ( ! `  k )
)  e.  RR )  ->  ( F `  k )  =  ( 1  /  ( ! `
 k ) ) )
83, 7mpdan 421 . . . . . . . . . . . 12  |-  ( k  e.  NN0  ->  ( F `
 k )  =  ( 1  /  ( ! `  k )
) )
98sumeq2i 11385 . . . . . . . . . . 11  |-  sum_ k  e.  NN0  ( F `  k )  =  sum_ k  e.  NN0  ( 1  /  ( ! `  k ) )
101, 9eqtr4i 2211 . . . . . . . . . 10  |-  _e  =  sum_ k  e.  NN0  ( F `  k )
11 nn0uz 9575 . . . . . . . . . . 11  |-  NN0  =  ( ZZ>= `  0 )
12 eqid 2187 . . . . . . . . . . 11  |-  ( ZZ>= `  ( Q  +  1
) )  =  (
ZZ>= `  ( Q  + 
1 ) )
13 eirr.3 . . . . . . . . . . . . 13  |-  ( ph  ->  Q  e.  NN )
1413peano2nnd 8947 . . . . . . . . . . . 12  |-  ( ph  ->  ( Q  +  1 )  e.  NN )
1514nnnn0d 9242 . . . . . . . . . . 11  |-  ( ph  ->  ( Q  +  1 )  e.  NN0 )
16 eqidd 2188 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( F `  k )  =  ( F `  k ) )
17 ax-1cn 7917 . . . . . . . . . . . . . 14  |-  1  e.  CC
18 nn0z 9286 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  NN0  ->  n  e.  ZZ )
19 1exp 10562 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  ZZ  ->  (
1 ^ n )  =  1 )
2018, 19syl 14 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  NN0  ->  ( 1 ^ n )  =  1 )
2120oveq1d 5903 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  NN0  ->  ( ( 1 ^ n )  /  ( ! `  n ) )  =  ( 1  /  ( ! `  n )
) )
2221mpteq2ia 4101 . . . . . . . . . . . . . . . 16  |-  ( n  e.  NN0  |->  ( ( 1 ^ n )  /  ( ! `  n ) ) )  =  ( n  e. 
NN0  |->  ( 1  / 
( ! `  n
) ) )
236, 22eqtr4i 2211 . . . . . . . . . . . . . . 15  |-  F  =  ( n  e.  NN0  |->  ( ( 1 ^ n )  /  ( ! `  n )
) )
2423eftvalcn 11678 . . . . . . . . . . . . . 14  |-  ( ( 1  e.  CC  /\  k  e.  NN0 )  -> 
( F `  k
)  =  ( ( 1 ^ k )  /  ( ! `  k ) ) )
2517, 24mpan 424 . . . . . . . . . . . . 13  |-  ( k  e.  NN0  ->  ( F `
 k )  =  ( ( 1 ^ k )  /  ( ! `  k )
) )
2625adantl 277 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( F `  k )  =  ( ( 1 ^ k
)  /  ( ! `
 k ) ) )
2717a1i 9 . . . . . . . . . . . . 13  |-  ( ph  ->  1  e.  CC )
28 eftcl 11675 . . . . . . . . . . . . 13  |-  ( ( 1  e.  CC  /\  k  e.  NN0 )  -> 
( ( 1 ^ k )  /  ( ! `  k )
)  e.  CC )
2927, 28sylan 283 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( (
1 ^ k )  /  ( ! `  k ) )  e.  CC )
3026, 29eqeltrd 2264 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( F `  k )  e.  CC )
3123efcllem 11680 . . . . . . . . . . . 12  |-  ( 1  e.  CC  ->  seq 0 (  +  ,  F )  e.  dom  ~~>  )
3227, 31syl 14 . . . . . . . . . . 11  |-  ( ph  ->  seq 0 (  +  ,  F )  e. 
dom 
~~>  )
3311, 12, 15, 16, 30, 32isumsplit 11512 . . . . . . . . . 10  |-  ( ph  -> 
sum_ k  e.  NN0  ( F `  k )  =  ( sum_ k  e.  ( 0 ... (
( Q  +  1 )  -  1 ) ) ( F `  k )  +  sum_ k  e.  ( ZZ>= `  ( Q  +  1
) ) ( F `
 k ) ) )
3410, 33eqtrid 2232 . . . . . . . . 9  |-  ( ph  ->  _e  =  ( sum_ k  e.  ( 0 ... ( ( Q  +  1 )  - 
1 ) ) ( F `  k )  +  sum_ k  e.  (
ZZ>= `  ( Q  + 
1 ) ) ( F `  k ) ) )
3513nncnd 8946 . . . . . . . . . . . . 13  |-  ( ph  ->  Q  e.  CC )
36 pncan 8176 . . . . . . . . . . . . 13  |-  ( ( Q  e.  CC  /\  1  e.  CC )  ->  ( ( Q  + 
1 )  -  1 )  =  Q )
3735, 17, 36sylancl 413 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( Q  + 
1 )  -  1 )  =  Q )
3837oveq2d 5904 . . . . . . . . . . 11  |-  ( ph  ->  ( 0 ... (
( Q  +  1 )  -  1 ) )  =  ( 0 ... Q ) )
3938sumeq1d 11387 . . . . . . . . . 10  |-  ( ph  -> 
sum_ k  e.  ( 0 ... ( ( Q  +  1 )  -  1 ) ) ( F `  k
)  =  sum_ k  e.  ( 0 ... Q
) ( F `  k ) )
4039oveq1d 5903 . . . . . . . . 9  |-  ( ph  ->  ( sum_ k  e.  ( 0 ... ( ( Q  +  1 )  -  1 ) ) ( F `  k
)  +  sum_ k  e.  ( ZZ>= `  ( Q  +  1 ) ) ( F `  k
) )  =  (
sum_ k  e.  ( 0 ... Q ) ( F `  k
)  +  sum_ k  e.  ( ZZ>= `  ( Q  +  1 ) ) ( F `  k
) ) )
4134, 40eqtrd 2220 . . . . . . . 8  |-  ( ph  ->  _e  =  ( sum_ k  e.  ( 0 ... Q ) ( F `  k )  +  sum_ k  e.  (
ZZ>= `  ( Q  + 
1 ) ) ( F `  k ) ) )
4241oveq1d 5903 . . . . . . 7  |-  ( ph  ->  ( _e  -  sum_ k  e.  ( 0 ... Q ) ( F `  k ) )  =  ( (
sum_ k  e.  ( 0 ... Q ) ( F `  k
)  +  sum_ k  e.  ( ZZ>= `  ( Q  +  1 ) ) ( F `  k
) )  -  sum_ k  e.  ( 0 ... Q ) ( F `  k ) ) )
43 0zd 9278 . . . . . . . . . 10  |-  ( ph  ->  0  e.  ZZ )
4413nnzd 9387 . . . . . . . . . 10  |-  ( ph  ->  Q  e.  ZZ )
4543, 44fzfigd 10444 . . . . . . . . 9  |-  ( ph  ->  ( 0 ... Q
)  e.  Fin )
46 elfznn0 10127 . . . . . . . . . 10  |-  ( k  e.  ( 0 ... Q )  ->  k  e.  NN0 )
4746, 30sylan2 286 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 0 ... Q
) )  ->  ( F `  k )  e.  CC )
4845, 47fsumcl 11421 . . . . . . . 8  |-  ( ph  -> 
sum_ k  e.  ( 0 ... Q ) ( F `  k
)  e.  CC )
498adantl 277 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( F `  k )  =  ( 1  /  ( ! `
 k ) ) )
502adantl 277 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( ! `  k )  e.  NN )
5150nnrpd 9707 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( ! `  k )  e.  RR+ )
5251rpreccld 9720 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( 1  /  ( ! `  k ) )  e.  RR+ )
5349, 52eqeltrd 2264 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( F `  k )  e.  RR+ )
5411, 12, 15, 16, 53, 32isumrpcl 11515 . . . . . . . . . 10  |-  ( ph  -> 
sum_ k  e.  (
ZZ>= `  ( Q  + 
1 ) ) ( F `  k )  e.  RR+ )
5554rpred 9709 . . . . . . . . 9  |-  ( ph  -> 
sum_ k  e.  (
ZZ>= `  ( Q  + 
1 ) ) ( F `  k )  e.  RR )
5655recnd 7999 . . . . . . . 8  |-  ( ph  -> 
sum_ k  e.  (
ZZ>= `  ( Q  + 
1 ) ) ( F `  k )  e.  CC )
5748, 56pncan2d 8283 . . . . . . 7  |-  ( ph  ->  ( ( sum_ k  e.  ( 0 ... Q
) ( F `  k )  +  sum_ k  e.  ( ZZ>= `  ( Q  +  1
) ) ( F `
 k ) )  -  sum_ k  e.  ( 0 ... Q ) ( F `  k
) )  =  sum_ k  e.  ( ZZ>= `  ( Q  +  1
) ) ( F `
 k ) )
5842, 57eqtrd 2220 . . . . . 6  |-  ( ph  ->  ( _e  -  sum_ k  e.  ( 0 ... Q ) ( F `  k ) )  =  sum_ k  e.  ( ZZ>= `  ( Q  +  1 ) ) ( F `  k
) )
5958oveq2d 5904 . . . . 5  |-  ( ph  ->  ( ( ! `  Q )  x.  (
_e  -  sum_ k  e.  ( 0 ... Q
) ( F `  k ) ) )  =  ( ( ! `
 Q )  x. 
sum_ k  e.  (
ZZ>= `  ( Q  + 
1 ) ) ( F `  k ) ) )
6013nnnn0d 9242 . . . . . . . 8  |-  ( ph  ->  Q  e.  NN0 )
6160faccld 10729 . . . . . . 7  |-  ( ph  ->  ( ! `  Q
)  e.  NN )
6261nncnd 8946 . . . . . 6  |-  ( ph  ->  ( ! `  Q
)  e.  CC )
63 ere 11691 . . . . . . . 8  |-  _e  e.  RR
6463recni 7982 . . . . . . 7  |-  _e  e.  CC
6564a1i 9 . . . . . 6  |-  ( ph  ->  _e  e.  CC )
6662, 65, 48subdid 8384 . . . . 5  |-  ( ph  ->  ( ( ! `  Q )  x.  (
_e  -  sum_ k  e.  ( 0 ... Q
) ( F `  k ) ) )  =  ( ( ( ! `  Q )  x.  _e )  -  ( ( ! `  Q )  x.  sum_ k  e.  ( 0 ... Q ) ( F `  k ) ) ) )
6759, 66eqtr3d 2222 . . . 4  |-  ( ph  ->  ( ( ! `  Q )  x.  sum_ k  e.  ( ZZ>= `  ( Q  +  1
) ) ( F `
 k ) )  =  ( ( ( ! `  Q )  x.  _e )  -  ( ( ! `  Q )  x.  sum_ k  e.  ( 0 ... Q ) ( F `  k ) ) ) )
6861nnrpd 9707 . . . . . . 7  |-  ( ph  ->  ( ! `  Q
)  e.  RR+ )
6968, 54rpmulcld 9726 . . . . . 6  |-  ( ph  ->  ( ( ! `  Q )  x.  sum_ k  e.  ( ZZ>= `  ( Q  +  1
) ) ( F `
 k ) )  e.  RR+ )
7069rpred 9709 . . . . 5  |-  ( ph  ->  ( ( ! `  Q )  x.  sum_ k  e.  ( ZZ>= `  ( Q  +  1
) ) ( F `
 k ) )  e.  RR )
71 eirr.2 . . . . . . . . 9  |-  ( ph  ->  P  e.  ZZ )
7271zcnd 9389 . . . . . . . 8  |-  ( ph  ->  P  e.  CC )
7313nnap0d 8978 . . . . . . . 8  |-  ( ph  ->  Q #  0 )
7462, 72, 35, 73div12apd 8797 . . . . . . 7  |-  ( ph  ->  ( ( ! `  Q )  x.  ( P  /  Q ) )  =  ( P  x.  ( ( ! `  Q )  /  Q
) ) )
7513nnred 8945 . . . . . . . . . . 11  |-  ( ph  ->  Q  e.  RR )
7675leidd 8484 . . . . . . . . . 10  |-  ( ph  ->  Q  <_  Q )
77 facdiv 10731 . . . . . . . . . 10  |-  ( ( Q  e.  NN0  /\  Q  e.  NN  /\  Q  <_  Q )  ->  (
( ! `  Q
)  /  Q )  e.  NN )
7860, 13, 76, 77syl3anc 1248 . . . . . . . . 9  |-  ( ph  ->  ( ( ! `  Q )  /  Q
)  e.  NN )
7978nnzd 9387 . . . . . . . 8  |-  ( ph  ->  ( ( ! `  Q )  /  Q
)  e.  ZZ )
8071, 79zmulcld 9394 . . . . . . 7  |-  ( ph  ->  ( P  x.  (
( ! `  Q
)  /  Q ) )  e.  ZZ )
8174, 80eqeltrd 2264 . . . . . 6  |-  ( ph  ->  ( ( ! `  Q )  x.  ( P  /  Q ) )  e.  ZZ )
8245, 62, 47fsummulc2 11469 . . . . . . 7  |-  ( ph  ->  ( ( ! `  Q )  x.  sum_ k  e.  ( 0 ... Q ) ( F `  k ) )  =  sum_ k  e.  ( 0 ... Q
) ( ( ! `
 Q )  x.  ( F `  k
) ) )
8346adantl 277 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  ( 0 ... Q
) )  ->  k  e.  NN0 )
8483, 8syl 14 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( 0 ... Q
) )  ->  ( F `  k )  =  ( 1  / 
( ! `  k
) ) )
8584oveq2d 5904 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( 0 ... Q
) )  ->  (
( ! `  Q
)  x.  ( F `
 k ) )  =  ( ( ! `
 Q )  x.  ( 1  /  ( ! `  k )
) ) )
8662adantr 276 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( 0 ... Q
) )  ->  ( ! `  Q )  e.  CC )
8746, 50sylan2 286 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  ( 0 ... Q
) )  ->  ( ! `  k )  e.  NN )
8887nncnd 8946 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( 0 ... Q
) )  ->  ( ! `  k )  e.  CC )
8987nnap0d 8978 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( 0 ... Q
) )  ->  ( ! `  k ) #  0 )
9086, 88, 89divrecapd 8763 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( 0 ... Q
) )  ->  (
( ! `  Q
)  /  ( ! `
 k ) )  =  ( ( ! `
 Q )  x.  ( 1  /  ( ! `  k )
) ) )
9185, 90eqtr4d 2223 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( 0 ... Q
) )  ->  (
( ! `  Q
)  x.  ( F `
 k ) )  =  ( ( ! `
 Q )  / 
( ! `  k
) ) )
92 permnn 10764 . . . . . . . . . . 11  |-  ( k  e.  ( 0 ... Q )  ->  (
( ! `  Q
)  /  ( ! `
 k ) )  e.  NN )
9392adantl 277 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( 0 ... Q
) )  ->  (
( ! `  Q
)  /  ( ! `
 k ) )  e.  NN )
9491, 93eqeltrd 2264 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 0 ... Q
) )  ->  (
( ! `  Q
)  x.  ( F `
 k ) )  e.  NN )
9594nnzd 9387 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( 0 ... Q
) )  ->  (
( ! `  Q
)  x.  ( F `
 k ) )  e.  ZZ )
9645, 95fsumzcl 11423 . . . . . . 7  |-  ( ph  -> 
sum_ k  e.  ( 0 ... Q ) ( ( ! `  Q )  x.  ( F `  k )
)  e.  ZZ )
9782, 96eqeltrd 2264 . . . . . 6  |-  ( ph  ->  ( ( ! `  Q )  x.  sum_ k  e.  ( 0 ... Q ) ( F `  k ) )  e.  ZZ )
9881, 97zsubcld 9393 . . . . 5  |-  ( ph  ->  ( ( ( ! `
 Q )  x.  ( P  /  Q
) )  -  (
( ! `  Q
)  x.  sum_ k  e.  ( 0 ... Q
) ( F `  k ) ) )  e.  ZZ )
9969rpgt0d 9712 . . . . 5  |-  ( ph  ->  0  <  ( ( ! `  Q )  x.  sum_ k  e.  (
ZZ>= `  ( Q  + 
1 ) ) ( F `  k ) ) )
10014peano2nnd 8947 . . . . . . . . . 10  |-  ( ph  ->  ( ( Q  + 
1 )  +  1 )  e.  NN )
101100nnred 8945 . . . . . . . . 9  |-  ( ph  ->  ( ( Q  + 
1 )  +  1 )  e.  RR )
10215faccld 10729 . . . . . . . . . 10  |-  ( ph  ->  ( ! `  ( Q  +  1 ) )  e.  NN )
103102, 14nnmulcld 8981 . . . . . . . . 9  |-  ( ph  ->  ( ( ! `  ( Q  +  1
) )  x.  ( Q  +  1 ) )  e.  NN )
104101, 103nndivred 8982 . . . . . . . 8  |-  ( ph  ->  ( ( ( Q  +  1 )  +  1 )  /  (
( ! `  ( Q  +  1 ) )  x.  ( Q  +  1 ) ) )  e.  RR )
10561nnrecred 8979 . . . . . . . 8  |-  ( ph  ->  ( 1  /  ( ! `  Q )
)  e.  RR )
106 abs1 11094 . . . . . . . . . . . . . 14  |-  ( abs `  1 )  =  1
107106oveq1i 5898 . . . . . . . . . . . . 13  |-  ( ( abs `  1 ) ^ n )  =  ( 1 ^ n
)
108107oveq1i 5898 . . . . . . . . . . . 12  |-  ( ( ( abs `  1
) ^ n )  /  ( ! `  n ) )  =  ( ( 1 ^ n )  /  ( ! `  n )
)
109108mpteq2i 4102 . . . . . . . . . . 11  |-  ( n  e.  NN0  |->  ( ( ( abs `  1
) ^ n )  /  ( ! `  n ) ) )  =  ( n  e. 
NN0  |->  ( ( 1 ^ n )  / 
( ! `  n
) ) )
11023, 109eqtr4i 2211 . . . . . . . . . 10  |-  F  =  ( n  e.  NN0  |->  ( ( ( abs `  1 ) ^
n )  /  ( ! `  n )
) )
111 eqid 2187 . . . . . . . . . 10  |-  ( n  e.  NN0  |->  ( ( ( ( abs `  1
) ^ ( Q  +  1 ) )  /  ( ! `  ( Q  +  1
) ) )  x.  ( ( 1  / 
( ( Q  + 
1 )  +  1 ) ) ^ n
) ) )  =  ( n  e.  NN0  |->  ( ( ( ( abs `  1 ) ^ ( Q  + 
1 ) )  / 
( ! `  ( Q  +  1 ) ) )  x.  (
( 1  /  (
( Q  +  1 )  +  1 ) ) ^ n ) ) )
112 1le1 8542 . . . . . . . . . . . 12  |-  1  <_  1
113106, 112eqbrtri 4036 . . . . . . . . . . 11  |-  ( abs `  1 )  <_ 
1
114113a1i 9 . . . . . . . . . 10  |-  ( ph  ->  ( abs `  1
)  <_  1 )
11523, 110, 111, 14, 27, 114eftlub 11711 . . . . . . . . 9  |-  ( ph  ->  ( abs `  sum_ k  e.  ( ZZ>= `  ( Q  +  1
) ) ( F `
 k ) )  <_  ( ( ( abs `  1 ) ^ ( Q  + 
1 ) )  x.  ( ( ( Q  +  1 )  +  1 )  /  (
( ! `  ( Q  +  1 ) )  x.  ( Q  +  1 ) ) ) ) )
11654rprege0d 9717 . . . . . . . . . 10  |-  ( ph  ->  ( sum_ k  e.  (
ZZ>= `  ( Q  + 
1 ) ) ( F `  k )  e.  RR  /\  0  <_ 
sum_ k  e.  (
ZZ>= `  ( Q  + 
1 ) ) ( F `  k ) ) )
117 absid 11093 . . . . . . . . . 10  |-  ( (
sum_ k  e.  (
ZZ>= `  ( Q  + 
1 ) ) ( F `  k )  e.  RR  /\  0  <_ 
sum_ k  e.  (
ZZ>= `  ( Q  + 
1 ) ) ( F `  k ) )  ->  ( abs ` 
sum_ k  e.  (
ZZ>= `  ( Q  + 
1 ) ) ( F `  k ) )  =  sum_ k  e.  ( ZZ>= `  ( Q  +  1 ) ) ( F `  k
) )
118116, 117syl 14 . . . . . . . . 9  |-  ( ph  ->  ( abs `  sum_ k  e.  ( ZZ>= `  ( Q  +  1
) ) ( F `
 k ) )  =  sum_ k  e.  (
ZZ>= `  ( Q  + 
1 ) ) ( F `  k ) )
119106oveq1i 5898 . . . . . . . . . . . 12  |-  ( ( abs `  1 ) ^ ( Q  + 
1 ) )  =  ( 1 ^ ( Q  +  1 ) )
12014nnzd 9387 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Q  +  1 )  e.  ZZ )
121 1exp 10562 . . . . . . . . . . . . 13  |-  ( ( Q  +  1 )  e.  ZZ  ->  (
1 ^ ( Q  +  1 ) )  =  1 )
122120, 121syl 14 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1 ^ ( Q  +  1 ) )  =  1 )
123119, 122eqtrid 2232 . . . . . . . . . . 11  |-  ( ph  ->  ( ( abs `  1
) ^ ( Q  +  1 ) )  =  1 )
124123oveq1d 5903 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( abs `  1 ) ^
( Q  +  1 ) )  x.  (
( ( Q  + 
1 )  +  1 )  /  ( ( ! `  ( Q  +  1 ) )  x.  ( Q  + 
1 ) ) ) )  =  ( 1  x.  ( ( ( Q  +  1 )  +  1 )  / 
( ( ! `  ( Q  +  1
) )  x.  ( Q  +  1 ) ) ) ) )
125104recnd 7999 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( Q  +  1 )  +  1 )  /  (
( ! `  ( Q  +  1 ) )  x.  ( Q  +  1 ) ) )  e.  CC )
126125mulid2d 7989 . . . . . . . . . 10  |-  ( ph  ->  ( 1  x.  (
( ( Q  + 
1 )  +  1 )  /  ( ( ! `  ( Q  +  1 ) )  x.  ( Q  + 
1 ) ) ) )  =  ( ( ( Q  +  1 )  +  1 )  /  ( ( ! `
 ( Q  + 
1 ) )  x.  ( Q  +  1 ) ) ) )
127124, 126eqtrd 2220 . . . . . . . . 9  |-  ( ph  ->  ( ( ( abs `  1 ) ^
( Q  +  1 ) )  x.  (
( ( Q  + 
1 )  +  1 )  /  ( ( ! `  ( Q  +  1 ) )  x.  ( Q  + 
1 ) ) ) )  =  ( ( ( Q  +  1 )  +  1 )  /  ( ( ! `
 ( Q  + 
1 ) )  x.  ( Q  +  1 ) ) ) )
128115, 118, 1273brtr3d 4046 . . . . . . . 8  |-  ( ph  -> 
sum_ k  e.  (
ZZ>= `  ( Q  + 
1 ) ) ( F `  k )  <_  ( ( ( Q  +  1 )  +  1 )  / 
( ( ! `  ( Q  +  1
) )  x.  ( Q  +  1 ) ) ) )
12914nnred 8945 . . . . . . . . . . . 12  |-  ( ph  ->  ( Q  +  1 )  e.  RR )
130129, 129readdcld 8000 . . . . . . . . . . 11  |-  ( ph  ->  ( ( Q  + 
1 )  +  ( Q  +  1 ) )  e.  RR )
131129, 129remulcld 8001 . . . . . . . . . . 11  |-  ( ph  ->  ( ( Q  + 
1 )  x.  ( Q  +  1 ) )  e.  RR )
132 1red 7985 . . . . . . . . . . . 12  |-  ( ph  ->  1  e.  RR )
13313nnge1d 8975 . . . . . . . . . . . . 13  |-  ( ph  ->  1  <_  Q )
134 1nn 8943 . . . . . . . . . . . . . 14  |-  1  e.  NN
135 nnleltp1 9325 . . . . . . . . . . . . . 14  |-  ( ( 1  e.  NN  /\  Q  e.  NN )  ->  ( 1  <_  Q  <->  1  <  ( Q  + 
1 ) ) )
136134, 13, 135sylancr 414 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1  <_  Q  <->  1  <  ( Q  + 
1 ) ) )
137133, 136mpbid 147 . . . . . . . . . . . 12  |-  ( ph  ->  1  <  ( Q  +  1 ) )
138132, 129, 129, 137ltadd2dd 8392 . . . . . . . . . . 11  |-  ( ph  ->  ( ( Q  + 
1 )  +  1 )  <  ( ( Q  +  1 )  +  ( Q  + 
1 ) ) )
13914nncnd 8946 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Q  +  1 )  e.  CC )
1401392timesd 9174 . . . . . . . . . . . 12  |-  ( ph  ->  ( 2  x.  ( Q  +  1 ) )  =  ( ( Q  +  1 )  +  ( Q  + 
1 ) ) )
141 df-2 8991 . . . . . . . . . . . . . 14  |-  2  =  ( 1  +  1 )
142132, 75, 132, 133leadd1dd 8529 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1  +  1 )  <_  ( Q  +  1 ) )
143141, 142eqbrtrid 4050 . . . . . . . . . . . . 13  |-  ( ph  ->  2  <_  ( Q  +  1 ) )
144 2re 9002 . . . . . . . . . . . . . . 15  |-  2  e.  RR
145144a1i 9 . . . . . . . . . . . . . 14  |-  ( ph  ->  2  e.  RR )
14614nngt0d 8976 . . . . . . . . . . . . . 14  |-  ( ph  ->  0  <  ( Q  +  1 ) )
147 lemul1 8563 . . . . . . . . . . . . . 14  |-  ( ( 2  e.  RR  /\  ( Q  +  1
)  e.  RR  /\  ( ( Q  + 
1 )  e.  RR  /\  0  <  ( Q  +  1 ) ) )  ->  ( 2  <_  ( Q  + 
1 )  <->  ( 2  x.  ( Q  + 
1 ) )  <_ 
( ( Q  + 
1 )  x.  ( Q  +  1 ) ) ) )
148145, 129, 129, 146, 147syl112anc 1252 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 2  <_  ( Q  +  1 )  <-> 
( 2  x.  ( Q  +  1 ) )  <_  ( ( Q  +  1 )  x.  ( Q  + 
1 ) ) ) )
149143, 148mpbid 147 . . . . . . . . . . . 12  |-  ( ph  ->  ( 2  x.  ( Q  +  1 ) )  <_  ( ( Q  +  1 )  x.  ( Q  + 
1 ) ) )
150140, 149eqbrtrrd 4039 . . . . . . . . . . 11  |-  ( ph  ->  ( ( Q  + 
1 )  +  ( Q  +  1 ) )  <_  ( ( Q  +  1 )  x.  ( Q  + 
1 ) ) )
151101, 130, 131, 138, 150ltletrd 8393 . . . . . . . . . 10  |-  ( ph  ->  ( ( Q  + 
1 )  +  1 )  <  ( ( Q  +  1 )  x.  ( Q  + 
1 ) ) )
152 facp1 10723 . . . . . . . . . . . . . . 15  |-  ( Q  e.  NN0  ->  ( ! `
 ( Q  + 
1 ) )  =  ( ( ! `  Q )  x.  ( Q  +  1 ) ) )
15360, 152syl 14 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ! `  ( Q  +  1 ) )  =  ( ( ! `  Q )  x.  ( Q  + 
1 ) ) )
154153oveq1d 5903 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ! `  ( Q  +  1
) )  /  ( ! `  Q )
)  =  ( ( ( ! `  Q
)  x.  ( Q  +  1 ) )  /  ( ! `  Q ) ) )
155102nncnd 8946 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ! `  ( Q  +  1 ) )  e.  CC )
15661nnap0d 8978 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ! `  Q
) #  0 )
157155, 62, 156divrecapd 8763 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ! `  ( Q  +  1
) )  /  ( ! `  Q )
)  =  ( ( ! `  ( Q  +  1 ) )  x.  ( 1  / 
( ! `  Q
) ) ) )
158139, 62, 156divcanap3d 8765 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( ! `
 Q )  x.  ( Q  +  1 ) )  /  ( ! `  Q )
)  =  ( Q  +  1 ) )
159154, 157, 1583eqtr3rd 2229 . . . . . . . . . . . 12  |-  ( ph  ->  ( Q  +  1 )  =  ( ( ! `  ( Q  +  1 ) )  x.  ( 1  / 
( ! `  Q
) ) ) )
160159oveq1d 5903 . . . . . . . . . . 11  |-  ( ph  ->  ( ( Q  + 
1 )  x.  ( Q  +  1 ) )  =  ( ( ( ! `  ( Q  +  1 ) )  x.  ( 1  /  ( ! `  Q ) ) )  x.  ( Q  + 
1 ) ) )
161105recnd 7999 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1  /  ( ! `  Q )
)  e.  CC )
162155, 161, 139mul32d 8123 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ! `
 ( Q  + 
1 ) )  x.  ( 1  /  ( ! `  Q )
) )  x.  ( Q  +  1 ) )  =  ( ( ( ! `  ( Q  +  1 ) )  x.  ( Q  +  1 ) )  x.  ( 1  / 
( ! `  Q
) ) ) )
163160, 162eqtrd 2220 . . . . . . . . . 10  |-  ( ph  ->  ( ( Q  + 
1 )  x.  ( Q  +  1 ) )  =  ( ( ( ! `  ( Q  +  1 ) )  x.  ( Q  +  1 ) )  x.  ( 1  / 
( ! `  Q
) ) ) )
164151, 163breqtrd 4041 . . . . . . . . 9  |-  ( ph  ->  ( ( Q  + 
1 )  +  1 )  <  ( ( ( ! `  ( Q  +  1 ) )  x.  ( Q  +  1 ) )  x.  ( 1  / 
( ! `  Q
) ) ) )
165103nnred 8945 . . . . . . . . . 10  |-  ( ph  ->  ( ( ! `  ( Q  +  1
) )  x.  ( Q  +  1 ) )  e.  RR )
166103nngt0d 8976 . . . . . . . . . 10  |-  ( ph  ->  0  <  ( ( ! `  ( Q  +  1 ) )  x.  ( Q  + 
1 ) ) )
167 ltdivmul 8846 . . . . . . . . . 10  |-  ( ( ( ( Q  + 
1 )  +  1 )  e.  RR  /\  ( 1  /  ( ! `  Q )
)  e.  RR  /\  ( ( ( ! `
 ( Q  + 
1 ) )  x.  ( Q  +  1 ) )  e.  RR  /\  0  <  ( ( ! `  ( Q  +  1 ) )  x.  ( Q  + 
1 ) ) ) )  ->  ( (
( ( Q  + 
1 )  +  1 )  /  ( ( ! `  ( Q  +  1 ) )  x.  ( Q  + 
1 ) ) )  <  ( 1  / 
( ! `  Q
) )  <->  ( ( Q  +  1 )  +  1 )  < 
( ( ( ! `
 ( Q  + 
1 ) )  x.  ( Q  +  1 ) )  x.  (
1  /  ( ! `
 Q ) ) ) ) )
168101, 105, 165, 166, 167syl112anc 1252 . . . . . . . . 9  |-  ( ph  ->  ( ( ( ( Q  +  1 )  +  1 )  / 
( ( ! `  ( Q  +  1
) )  x.  ( Q  +  1 ) ) )  <  (
1  /  ( ! `
 Q ) )  <-> 
( ( Q  + 
1 )  +  1 )  <  ( ( ( ! `  ( Q  +  1 ) )  x.  ( Q  +  1 ) )  x.  ( 1  / 
( ! `  Q
) ) ) ) )
169164, 168mpbird 167 . . . . . . . 8  |-  ( ph  ->  ( ( ( Q  +  1 )  +  1 )  /  (
( ! `  ( Q  +  1 ) )  x.  ( Q  +  1 ) ) )  <  ( 1  /  ( ! `  Q ) ) )
17055, 104, 105, 128, 169lelttrd 8095 . . . . . . 7  |-  ( ph  -> 
sum_ k  e.  (
ZZ>= `  ( Q  + 
1 ) ) ( F `  k )  <  ( 1  / 
( ! `  Q
) ) )
17155, 132, 68ltmuldiv2d 9758 . . . . . . 7  |-  ( ph  ->  ( ( ( ! `
 Q )  x. 
sum_ k  e.  (
ZZ>= `  ( Q  + 
1 ) ) ( F `  k ) )  <  1  <->  sum_ k  e.  ( ZZ>= `  ( Q  +  1
) ) ( F `
 k )  < 
( 1  /  ( ! `  Q )
) ) )
172170, 171mpbird 167 . . . . . 6  |-  ( ph  ->  ( ( ! `  Q )  x.  sum_ k  e.  ( ZZ>= `  ( Q  +  1
) ) ( F `
 k ) )  <  1 )
173 0p1e1 9046 . . . . . 6  |-  ( 0  +  1 )  =  1
174172, 173breqtrrdi 4057 . . . . 5  |-  ( ph  ->  ( ( ! `  Q )  x.  sum_ k  e.  ( ZZ>= `  ( Q  +  1
) ) ( F `
 k ) )  <  ( 0  +  1 ) )
17543, 70, 98, 99, 174btwnapz 9396 . . . 4  |-  ( ph  ->  ( ( ! `  Q )  x.  sum_ k  e.  ( ZZ>= `  ( Q  +  1
) ) ( F `
 k ) ) #  ( ( ( ! `
 Q )  x.  ( P  /  Q
) )  -  (
( ! `  Q
)  x.  sum_ k  e.  ( 0 ... Q
) ( F `  k ) ) ) )
17667, 175eqbrtrrd 4039 . . 3  |-  ( ph  ->  ( ( ( ! `
 Q )  x.  _e )  -  (
( ! `  Q
)  x.  sum_ k  e.  ( 0 ... Q
) ( F `  k ) ) ) #  ( ( ( ! `
 Q )  x.  ( P  /  Q
) )  -  (
( ! `  Q
)  x.  sum_ k  e.  ( 0 ... Q
) ( F `  k ) ) ) )
17762, 65mulcld 7991 . . . 4  |-  ( ph  ->  ( ( ! `  Q )  x.  _e )  e.  CC )
17881zcnd 9389 . . . 4  |-  ( ph  ->  ( ( ! `  Q )  x.  ( P  /  Q ) )  e.  CC )
17962, 48mulcld 7991 . . . 4  |-  ( ph  ->  ( ( ! `  Q )  x.  sum_ k  e.  ( 0 ... Q ) ( F `  k ) )  e.  CC )
180 apsub1 8612 . . . 4  |-  ( ( ( ( ! `  Q )  x.  _e )  e.  CC  /\  (
( ! `  Q
)  x.  ( P  /  Q ) )  e.  CC  /\  (
( ! `  Q
)  x.  sum_ k  e.  ( 0 ... Q
) ( F `  k ) )  e.  CC )  ->  (
( ( ! `  Q )  x.  _e ) #  ( ( ! `  Q )  x.  ( P  /  Q ) )  <-> 
( ( ( ! `
 Q )  x.  _e )  -  (
( ! `  Q
)  x.  sum_ k  e.  ( 0 ... Q
) ( F `  k ) ) ) #  ( ( ( ! `
 Q )  x.  ( P  /  Q
) )  -  (
( ! `  Q
)  x.  sum_ k  e.  ( 0 ... Q
) ( F `  k ) ) ) ) )
181177, 178, 179, 180syl3anc 1248 . . 3  |-  ( ph  ->  ( ( ( ! `
 Q )  x.  _e ) #  ( ( ! `  Q )  x.  ( P  /  Q ) )  <->  ( (
( ! `  Q
)  x.  _e )  -  ( ( ! `
 Q )  x. 
sum_ k  e.  ( 0 ... Q ) ( F `  k
) ) ) #  ( ( ( ! `  Q )  x.  ( P  /  Q ) )  -  ( ( ! `
 Q )  x. 
sum_ k  e.  ( 0 ... Q ) ( F `  k
) ) ) ) )
182176, 181mpbird 167 . 2  |-  ( ph  ->  ( ( ! `  Q )  x.  _e ) #  ( ( ! `  Q )  x.  ( P  /  Q ) ) )
183 znq 9637 . . . . 5  |-  ( ( P  e.  ZZ  /\  Q  e.  NN )  ->  ( P  /  Q
)  e.  QQ )
18471, 13, 183syl2anc 411 . . . 4  |-  ( ph  ->  ( P  /  Q
)  e.  QQ )
185 qcn 9647 . . . 4  |-  ( ( P  /  Q )  e.  QQ  ->  ( P  /  Q )  e.  CC )
186184, 185syl 14 . . 3  |-  ( ph  ->  ( P  /  Q
)  e.  CC )
187 apmul2 8759 . . 3  |-  ( ( _e  e.  CC  /\  ( P  /  Q
)  e.  CC  /\  ( ( ! `  Q )  e.  CC  /\  ( ! `  Q
) #  0 ) )  ->  ( _e #  ( P  /  Q )  <->  ( ( ! `  Q )  x.  _e ) #  ( ( ! `  Q )  x.  ( P  /  Q ) ) ) )
18865, 186, 62, 156, 187syl112anc 1252 . 2  |-  ( ph  ->  ( _e #  ( P  /  Q )  <->  ( ( ! `  Q )  x.  _e ) #  ( ( ! `  Q )  x.  ( P  /  Q ) ) ) )
189182, 188mpbird 167 1  |-  ( ph  ->  _e #  ( P  /  Q ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    <-> wb 105    = wceq 1363    e. wcel 2158   class class class wbr 4015    |-> cmpt 4076   dom cdm 4638   ` cfv 5228  (class class class)co 5888   CCcc 7822   RRcr 7823   0cc0 7824   1c1 7825    + caddc 7827    x. cmul 7829    < clt 8005    <_ cle 8006    - cmin 8141   # cap 8551    / cdiv 8642   NNcn 8932   2c2 8983   NN0cn0 9189   ZZcz 9266   ZZ>=cuz 9541   QQcq 9632   RR+crp 9666   ...cfz 10021    seqcseq 10458   ^cexp 10532   !cfa 10718   abscabs 11019    ~~> cli 11299   sum_csu 11374   _eceu 11664
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-13 2160  ax-14 2161  ax-ext 2169  ax-coll 4130  ax-sep 4133  ax-nul 4141  ax-pow 4186  ax-pr 4221  ax-un 4445  ax-setind 4548  ax-iinf 4599  ax-cnex 7915  ax-resscn 7916  ax-1cn 7917  ax-1re 7918  ax-icn 7919  ax-addcl 7920  ax-addrcl 7921  ax-mulcl 7922  ax-mulrcl 7923  ax-addcom 7924  ax-mulcom 7925  ax-addass 7926  ax-mulass 7927  ax-distr 7928  ax-i2m1 7929  ax-0lt1 7930  ax-1rid 7931  ax-0id 7932  ax-rnegex 7933  ax-precex 7934  ax-cnre 7935  ax-pre-ltirr 7936  ax-pre-ltwlin 7937  ax-pre-lttrn 7938  ax-pre-apti 7939  ax-pre-ltadd 7940  ax-pre-mulgt0 7941  ax-pre-mulext 7942  ax-arch 7943  ax-caucvg 7944
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 980  df-3an 981  df-tru 1366  df-fal 1369  df-nf 1471  df-sb 1773  df-eu 2039  df-mo 2040  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ne 2358  df-nel 2453  df-ral 2470  df-rex 2471  df-reu 2472  df-rmo 2473  df-rab 2474  df-v 2751  df-sbc 2975  df-csb 3070  df-dif 3143  df-un 3145  df-in 3147  df-ss 3154  df-nul 3435  df-if 3547  df-pw 3589  df-sn 3610  df-pr 3611  df-op 3613  df-uni 3822  df-int 3857  df-iun 3900  df-br 4016  df-opab 4077  df-mpt 4078  df-tr 4114  df-id 4305  df-po 4308  df-iso 4309  df-iord 4378  df-on 4380  df-ilim 4381  df-suc 4383  df-iom 4602  df-xp 4644  df-rel 4645  df-cnv 4646  df-co 4647  df-dm 4648  df-rn 4649  df-res 4650  df-ima 4651  df-iota 5190  df-fun 5230  df-fn 5231  df-f 5232  df-f1 5233  df-fo 5234  df-f1o 5235  df-fv 5236  df-isom 5237  df-riota 5844  df-ov 5891  df-oprab 5892  df-mpo 5893  df-1st 6154  df-2nd 6155  df-recs 6319  df-irdg 6384  df-frec 6405  df-1o 6430  df-oadd 6434  df-er 6548  df-en 6754  df-dom 6755  df-fin 6756  df-pnf 8007  df-mnf 8008  df-xr 8009  df-ltxr 8010  df-le 8011  df-sub 8143  df-neg 8144  df-reap 8545  df-ap 8552  df-div 8643  df-inn 8933  df-2 8991  df-3 8992  df-4 8993  df-n0 9190  df-z 9267  df-uz 9542  df-q 9633  df-rp 9667  df-ico 9907  df-fz 10022  df-fzo 10156  df-seqfrec 10459  df-exp 10533  df-fac 10719  df-bc 10741  df-ihash 10769  df-shft 10837  df-cj 10864  df-re 10865  df-im 10866  df-rsqrt 11020  df-abs 11021  df-clim 11300  df-sumdc 11375  df-ef 11669  df-e 11670
This theorem is referenced by:  eirrap  11798
  Copyright terms: Public domain W3C validator