Step |
Hyp |
Ref |
Expression |
1 |
|
qrng.q |
|- Q = ( CCfld |`s QQ ) |
2 |
|
qabsabv.a |
|- A = ( AbsVal ` Q ) |
3 |
|
padic.j |
|- J = ( q e. Prime |-> ( x e. QQ |-> if ( x = 0 , 0 , ( q ^ -u ( q pCnt x ) ) ) ) ) |
4 |
|
ostth.k |
|- K = ( x e. QQ |-> if ( x = 0 , 0 , 1 ) ) |
5 |
|
ostth.1 |
|- ( ph -> F e. A ) |
6 |
|
ostth2.2 |
|- ( ph -> N e. ( ZZ>= ` 2 ) ) |
7 |
|
ostth2.3 |
|- ( ph -> 1 < ( F ` N ) ) |
8 |
|
ostth2.4 |
|- R = ( ( log ` ( F ` N ) ) / ( log ` N ) ) |
9 |
|
ostth2.5 |
|- ( ph -> M e. ( ZZ>= ` 2 ) ) |
10 |
|
ostth2.6 |
|- S = ( ( log ` ( F ` M ) ) / ( log ` M ) ) |
11 |
|
ostth2.7 |
|- T = if ( ( F ` M ) <_ 1 , 1 , ( F ` M ) ) |
12 |
|
oveq2 |
|- ( x = 0 -> ( M ^ x ) = ( M ^ 0 ) ) |
13 |
12
|
oveq1d |
|- ( x = 0 -> ( ( M ^ x ) - 1 ) = ( ( M ^ 0 ) - 1 ) ) |
14 |
13
|
oveq2d |
|- ( x = 0 -> ( 0 ... ( ( M ^ x ) - 1 ) ) = ( 0 ... ( ( M ^ 0 ) - 1 ) ) ) |
15 |
|
oveq2 |
|- ( x = 0 -> ( M x. x ) = ( M x. 0 ) ) |
16 |
|
oveq2 |
|- ( x = 0 -> ( T ^ x ) = ( T ^ 0 ) ) |
17 |
15 16
|
oveq12d |
|- ( x = 0 -> ( ( M x. x ) x. ( T ^ x ) ) = ( ( M x. 0 ) x. ( T ^ 0 ) ) ) |
18 |
17
|
breq2d |
|- ( x = 0 -> ( ( F ` k ) <_ ( ( M x. x ) x. ( T ^ x ) ) <-> ( F ` k ) <_ ( ( M x. 0 ) x. ( T ^ 0 ) ) ) ) |
19 |
14 18
|
raleqbidv |
|- ( x = 0 -> ( A. k e. ( 0 ... ( ( M ^ x ) - 1 ) ) ( F ` k ) <_ ( ( M x. x ) x. ( T ^ x ) ) <-> A. k e. ( 0 ... ( ( M ^ 0 ) - 1 ) ) ( F ` k ) <_ ( ( M x. 0 ) x. ( T ^ 0 ) ) ) ) |
20 |
19
|
imbi2d |
|- ( x = 0 -> ( ( ph -> A. k e. ( 0 ... ( ( M ^ x ) - 1 ) ) ( F ` k ) <_ ( ( M x. x ) x. ( T ^ x ) ) ) <-> ( ph -> A. k e. ( 0 ... ( ( M ^ 0 ) - 1 ) ) ( F ` k ) <_ ( ( M x. 0 ) x. ( T ^ 0 ) ) ) ) ) |
21 |
|
oveq2 |
|- ( x = n -> ( M ^ x ) = ( M ^ n ) ) |
22 |
21
|
oveq1d |
|- ( x = n -> ( ( M ^ x ) - 1 ) = ( ( M ^ n ) - 1 ) ) |
23 |
22
|
oveq2d |
|- ( x = n -> ( 0 ... ( ( M ^ x ) - 1 ) ) = ( 0 ... ( ( M ^ n ) - 1 ) ) ) |
24 |
|
oveq2 |
|- ( x = n -> ( M x. x ) = ( M x. n ) ) |
25 |
|
oveq2 |
|- ( x = n -> ( T ^ x ) = ( T ^ n ) ) |
26 |
24 25
|
oveq12d |
|- ( x = n -> ( ( M x. x ) x. ( T ^ x ) ) = ( ( M x. n ) x. ( T ^ n ) ) ) |
27 |
26
|
breq2d |
|- ( x = n -> ( ( F ` k ) <_ ( ( M x. x ) x. ( T ^ x ) ) <-> ( F ` k ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) |
28 |
23 27
|
raleqbidv |
|- ( x = n -> ( A. k e. ( 0 ... ( ( M ^ x ) - 1 ) ) ( F ` k ) <_ ( ( M x. x ) x. ( T ^ x ) ) <-> A. k e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` k ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) |
29 |
28
|
imbi2d |
|- ( x = n -> ( ( ph -> A. k e. ( 0 ... ( ( M ^ x ) - 1 ) ) ( F ` k ) <_ ( ( M x. x ) x. ( T ^ x ) ) ) <-> ( ph -> A. k e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` k ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) ) |
30 |
|
oveq2 |
|- ( x = ( n + 1 ) -> ( M ^ x ) = ( M ^ ( n + 1 ) ) ) |
31 |
30
|
oveq1d |
|- ( x = ( n + 1 ) -> ( ( M ^ x ) - 1 ) = ( ( M ^ ( n + 1 ) ) - 1 ) ) |
32 |
31
|
oveq2d |
|- ( x = ( n + 1 ) -> ( 0 ... ( ( M ^ x ) - 1 ) ) = ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) ) |
33 |
|
oveq2 |
|- ( x = ( n + 1 ) -> ( M x. x ) = ( M x. ( n + 1 ) ) ) |
34 |
|
oveq2 |
|- ( x = ( n + 1 ) -> ( T ^ x ) = ( T ^ ( n + 1 ) ) ) |
35 |
33 34
|
oveq12d |
|- ( x = ( n + 1 ) -> ( ( M x. x ) x. ( T ^ x ) ) = ( ( M x. ( n + 1 ) ) x. ( T ^ ( n + 1 ) ) ) ) |
36 |
35
|
breq2d |
|- ( x = ( n + 1 ) -> ( ( F ` k ) <_ ( ( M x. x ) x. ( T ^ x ) ) <-> ( F ` k ) <_ ( ( M x. ( n + 1 ) ) x. ( T ^ ( n + 1 ) ) ) ) ) |
37 |
32 36
|
raleqbidv |
|- ( x = ( n + 1 ) -> ( A. k e. ( 0 ... ( ( M ^ x ) - 1 ) ) ( F ` k ) <_ ( ( M x. x ) x. ( T ^ x ) ) <-> A. k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) ( F ` k ) <_ ( ( M x. ( n + 1 ) ) x. ( T ^ ( n + 1 ) ) ) ) ) |
38 |
37
|
imbi2d |
|- ( x = ( n + 1 ) -> ( ( ph -> A. k e. ( 0 ... ( ( M ^ x ) - 1 ) ) ( F ` k ) <_ ( ( M x. x ) x. ( T ^ x ) ) ) <-> ( ph -> A. k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) ( F ` k ) <_ ( ( M x. ( n + 1 ) ) x. ( T ^ ( n + 1 ) ) ) ) ) ) |
39 |
|
oveq2 |
|- ( x = X -> ( M ^ x ) = ( M ^ X ) ) |
40 |
39
|
oveq1d |
|- ( x = X -> ( ( M ^ x ) - 1 ) = ( ( M ^ X ) - 1 ) ) |
41 |
40
|
oveq2d |
|- ( x = X -> ( 0 ... ( ( M ^ x ) - 1 ) ) = ( 0 ... ( ( M ^ X ) - 1 ) ) ) |
42 |
|
oveq2 |
|- ( x = X -> ( M x. x ) = ( M x. X ) ) |
43 |
|
oveq2 |
|- ( x = X -> ( T ^ x ) = ( T ^ X ) ) |
44 |
42 43
|
oveq12d |
|- ( x = X -> ( ( M x. x ) x. ( T ^ x ) ) = ( ( M x. X ) x. ( T ^ X ) ) ) |
45 |
44
|
breq2d |
|- ( x = X -> ( ( F ` k ) <_ ( ( M x. x ) x. ( T ^ x ) ) <-> ( F ` k ) <_ ( ( M x. X ) x. ( T ^ X ) ) ) ) |
46 |
41 45
|
raleqbidv |
|- ( x = X -> ( A. k e. ( 0 ... ( ( M ^ x ) - 1 ) ) ( F ` k ) <_ ( ( M x. x ) x. ( T ^ x ) ) <-> A. k e. ( 0 ... ( ( M ^ X ) - 1 ) ) ( F ` k ) <_ ( ( M x. X ) x. ( T ^ X ) ) ) ) |
47 |
46
|
imbi2d |
|- ( x = X -> ( ( ph -> A. k e. ( 0 ... ( ( M ^ x ) - 1 ) ) ( F ` k ) <_ ( ( M x. x ) x. ( T ^ x ) ) ) <-> ( ph -> A. k e. ( 0 ... ( ( M ^ X ) - 1 ) ) ( F ` k ) <_ ( ( M x. X ) x. ( T ^ X ) ) ) ) ) |
48 |
|
eluz2nn |
|- ( M e. ( ZZ>= ` 2 ) -> M e. NN ) |
49 |
9 48
|
syl |
|- ( ph -> M e. NN ) |
50 |
49
|
nncnd |
|- ( ph -> M e. CC ) |
51 |
50
|
exp0d |
|- ( ph -> ( M ^ 0 ) = 1 ) |
52 |
51
|
oveq1d |
|- ( ph -> ( ( M ^ 0 ) - 1 ) = ( 1 - 1 ) ) |
53 |
|
1m1e0 |
|- ( 1 - 1 ) = 0 |
54 |
52 53
|
eqtrdi |
|- ( ph -> ( ( M ^ 0 ) - 1 ) = 0 ) |
55 |
54
|
oveq2d |
|- ( ph -> ( 0 ... ( ( M ^ 0 ) - 1 ) ) = ( 0 ... 0 ) ) |
56 |
55
|
eleq2d |
|- ( ph -> ( k e. ( 0 ... ( ( M ^ 0 ) - 1 ) ) <-> k e. ( 0 ... 0 ) ) ) |
57 |
|
0le0 |
|- 0 <_ 0 |
58 |
57
|
a1i |
|- ( ph -> 0 <_ 0 ) |
59 |
1
|
qrng0 |
|- 0 = ( 0g ` Q ) |
60 |
2 59
|
abv0 |
|- ( F e. A -> ( F ` 0 ) = 0 ) |
61 |
5 60
|
syl |
|- ( ph -> ( F ` 0 ) = 0 ) |
62 |
50
|
mul01d |
|- ( ph -> ( M x. 0 ) = 0 ) |
63 |
62
|
oveq1d |
|- ( ph -> ( ( M x. 0 ) x. ( T ^ 0 ) ) = ( 0 x. ( T ^ 0 ) ) ) |
64 |
|
1re |
|- 1 e. RR |
65 |
|
nnq |
|- ( M e. NN -> M e. QQ ) |
66 |
49 65
|
syl |
|- ( ph -> M e. QQ ) |
67 |
1
|
qrngbas |
|- QQ = ( Base ` Q ) |
68 |
2 67
|
abvcl |
|- ( ( F e. A /\ M e. QQ ) -> ( F ` M ) e. RR ) |
69 |
5 66 68
|
syl2anc |
|- ( ph -> ( F ` M ) e. RR ) |
70 |
|
ifcl |
|- ( ( 1 e. RR /\ ( F ` M ) e. RR ) -> if ( ( F ` M ) <_ 1 , 1 , ( F ` M ) ) e. RR ) |
71 |
64 69 70
|
sylancr |
|- ( ph -> if ( ( F ` M ) <_ 1 , 1 , ( F ` M ) ) e. RR ) |
72 |
11 71
|
eqeltrid |
|- ( ph -> T e. RR ) |
73 |
72
|
recnd |
|- ( ph -> T e. CC ) |
74 |
|
0nn0 |
|- 0 e. NN0 |
75 |
|
expcl |
|- ( ( T e. CC /\ 0 e. NN0 ) -> ( T ^ 0 ) e. CC ) |
76 |
73 74 75
|
sylancl |
|- ( ph -> ( T ^ 0 ) e. CC ) |
77 |
76
|
mul02d |
|- ( ph -> ( 0 x. ( T ^ 0 ) ) = 0 ) |
78 |
63 77
|
eqtrd |
|- ( ph -> ( ( M x. 0 ) x. ( T ^ 0 ) ) = 0 ) |
79 |
58 61 78
|
3brtr4d |
|- ( ph -> ( F ` 0 ) <_ ( ( M x. 0 ) x. ( T ^ 0 ) ) ) |
80 |
|
elfz1eq |
|- ( k e. ( 0 ... 0 ) -> k = 0 ) |
81 |
80
|
fveq2d |
|- ( k e. ( 0 ... 0 ) -> ( F ` k ) = ( F ` 0 ) ) |
82 |
81
|
breq1d |
|- ( k e. ( 0 ... 0 ) -> ( ( F ` k ) <_ ( ( M x. 0 ) x. ( T ^ 0 ) ) <-> ( F ` 0 ) <_ ( ( M x. 0 ) x. ( T ^ 0 ) ) ) ) |
83 |
79 82
|
syl5ibrcom |
|- ( ph -> ( k e. ( 0 ... 0 ) -> ( F ` k ) <_ ( ( M x. 0 ) x. ( T ^ 0 ) ) ) ) |
84 |
56 83
|
sylbid |
|- ( ph -> ( k e. ( 0 ... ( ( M ^ 0 ) - 1 ) ) -> ( F ` k ) <_ ( ( M x. 0 ) x. ( T ^ 0 ) ) ) ) |
85 |
84
|
ralrimiv |
|- ( ph -> A. k e. ( 0 ... ( ( M ^ 0 ) - 1 ) ) ( F ` k ) <_ ( ( M x. 0 ) x. ( T ^ 0 ) ) ) |
86 |
|
fveq2 |
|- ( k = j -> ( F ` k ) = ( F ` j ) ) |
87 |
86
|
breq1d |
|- ( k = j -> ( ( F ` k ) <_ ( ( M x. n ) x. ( T ^ n ) ) <-> ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) |
88 |
87
|
cbvralvw |
|- ( A. k e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` k ) <_ ( ( M x. n ) x. ( T ^ n ) ) <-> A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) |
89 |
5
|
ad2antrr |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> F e. A ) |
90 |
|
elfzelz |
|- ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) -> k e. ZZ ) |
91 |
90
|
ad2antrl |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> k e. ZZ ) |
92 |
|
zq |
|- ( k e. ZZ -> k e. QQ ) |
93 |
91 92
|
syl |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> k e. QQ ) |
94 |
2 67
|
abvcl |
|- ( ( F e. A /\ k e. QQ ) -> ( F ` k ) e. RR ) |
95 |
89 93 94
|
syl2anc |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( F ` k ) e. RR ) |
96 |
49
|
ad2antrr |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> M e. NN ) |
97 |
|
simplr |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> n e. NN0 ) |
98 |
96 97
|
nnexpcld |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( M ^ n ) e. NN ) |
99 |
91 98
|
zmodcld |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( k mod ( M ^ n ) ) e. NN0 ) |
100 |
99
|
nn0zd |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( k mod ( M ^ n ) ) e. ZZ ) |
101 |
|
zq |
|- ( ( k mod ( M ^ n ) ) e. ZZ -> ( k mod ( M ^ n ) ) e. QQ ) |
102 |
100 101
|
syl |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( k mod ( M ^ n ) ) e. QQ ) |
103 |
2 67
|
abvcl |
|- ( ( F e. A /\ ( k mod ( M ^ n ) ) e. QQ ) -> ( F ` ( k mod ( M ^ n ) ) ) e. RR ) |
104 |
89 102 103
|
syl2anc |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( F ` ( k mod ( M ^ n ) ) ) e. RR ) |
105 |
96 65
|
syl |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> M e. QQ ) |
106 |
89 105 68
|
syl2anc |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( F ` M ) e. RR ) |
107 |
106 97
|
reexpcld |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( F ` M ) ^ n ) e. RR ) |
108 |
91
|
zred |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> k e. RR ) |
109 |
108 98
|
nndivred |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( k / ( M ^ n ) ) e. RR ) |
110 |
109
|
flcld |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( |_ ` ( k / ( M ^ n ) ) ) e. ZZ ) |
111 |
|
zq |
|- ( ( |_ ` ( k / ( M ^ n ) ) ) e. ZZ -> ( |_ ` ( k / ( M ^ n ) ) ) e. QQ ) |
112 |
110 111
|
syl |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( |_ ` ( k / ( M ^ n ) ) ) e. QQ ) |
113 |
2 67
|
abvcl |
|- ( ( F e. A /\ ( |_ ` ( k / ( M ^ n ) ) ) e. QQ ) -> ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) e. RR ) |
114 |
89 112 113
|
syl2anc |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) e. RR ) |
115 |
107 114
|
remulcld |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( ( F ` M ) ^ n ) x. ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) ) e. RR ) |
116 |
104 115
|
readdcld |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( F ` ( k mod ( M ^ n ) ) ) + ( ( ( F ` M ) ^ n ) x. ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) ) ) e. RR ) |
117 |
96
|
nnred |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> M e. RR ) |
118 |
|
nn0p1nn |
|- ( n e. NN0 -> ( n + 1 ) e. NN ) |
119 |
118
|
ad2antlr |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( n + 1 ) e. NN ) |
120 |
119
|
nnred |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( n + 1 ) e. RR ) |
121 |
117 120
|
remulcld |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( M x. ( n + 1 ) ) e. RR ) |
122 |
72
|
ad2antrr |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> T e. RR ) |
123 |
|
peano2nn0 |
|- ( n e. NN0 -> ( n + 1 ) e. NN0 ) |
124 |
123
|
ad2antlr |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( n + 1 ) e. NN0 ) |
125 |
122 124
|
reexpcld |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( T ^ ( n + 1 ) ) e. RR ) |
126 |
121 125
|
remulcld |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( M x. ( n + 1 ) ) x. ( T ^ ( n + 1 ) ) ) e. RR ) |
127 |
|
nnq |
|- ( ( M ^ n ) e. NN -> ( M ^ n ) e. QQ ) |
128 |
98 127
|
syl |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( M ^ n ) e. QQ ) |
129 |
|
qmulcl |
|- ( ( ( M ^ n ) e. QQ /\ ( |_ ` ( k / ( M ^ n ) ) ) e. QQ ) -> ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) e. QQ ) |
130 |
128 112 129
|
syl2anc |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) e. QQ ) |
131 |
|
qex |
|- QQ e. _V |
132 |
|
cnfldadd |
|- + = ( +g ` CCfld ) |
133 |
1 132
|
ressplusg |
|- ( QQ e. _V -> + = ( +g ` Q ) ) |
134 |
131 133
|
ax-mp |
|- + = ( +g ` Q ) |
135 |
2 67 134
|
abvtri |
|- ( ( F e. A /\ ( k mod ( M ^ n ) ) e. QQ /\ ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) e. QQ ) -> ( F ` ( ( k mod ( M ^ n ) ) + ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) ) ) <_ ( ( F ` ( k mod ( M ^ n ) ) ) + ( F ` ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) ) ) ) |
136 |
89 102 130 135
|
syl3anc |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( F ` ( ( k mod ( M ^ n ) ) + ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) ) ) <_ ( ( F ` ( k mod ( M ^ n ) ) ) + ( F ` ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) ) ) ) |
137 |
98
|
nnrpd |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( M ^ n ) e. RR+ ) |
138 |
|
modval |
|- ( ( k e. RR /\ ( M ^ n ) e. RR+ ) -> ( k mod ( M ^ n ) ) = ( k - ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) ) ) |
139 |
108 137 138
|
syl2anc |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( k mod ( M ^ n ) ) = ( k - ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) ) ) |
140 |
139
|
oveq1d |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( k mod ( M ^ n ) ) + ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) ) = ( ( k - ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) ) + ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) ) ) |
141 |
108
|
recnd |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> k e. CC ) |
142 |
|
qcn |
|- ( ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) e. QQ -> ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) e. CC ) |
143 |
130 142
|
syl |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) e. CC ) |
144 |
141 143
|
npcand |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( k - ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) ) + ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) ) = k ) |
145 |
140 144
|
eqtrd |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( k mod ( M ^ n ) ) + ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) ) = k ) |
146 |
145
|
fveq2d |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( F ` ( ( k mod ( M ^ n ) ) + ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) ) ) = ( F ` k ) ) |
147 |
|
cnfldmul |
|- x. = ( .r ` CCfld ) |
148 |
1 147
|
ressmulr |
|- ( QQ e. _V -> x. = ( .r ` Q ) ) |
149 |
131 148
|
ax-mp |
|- x. = ( .r ` Q ) |
150 |
2 67 149
|
abvmul |
|- ( ( F e. A /\ ( M ^ n ) e. QQ /\ ( |_ ` ( k / ( M ^ n ) ) ) e. QQ ) -> ( F ` ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) ) = ( ( F ` ( M ^ n ) ) x. ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) ) ) |
151 |
89 128 112 150
|
syl3anc |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( F ` ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) ) = ( ( F ` ( M ^ n ) ) x. ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) ) ) |
152 |
1 2
|
qabvexp |
|- ( ( F e. A /\ M e. QQ /\ n e. NN0 ) -> ( F ` ( M ^ n ) ) = ( ( F ` M ) ^ n ) ) |
153 |
89 105 97 152
|
syl3anc |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( F ` ( M ^ n ) ) = ( ( F ` M ) ^ n ) ) |
154 |
153
|
oveq1d |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( F ` ( M ^ n ) ) x. ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) ) = ( ( ( F ` M ) ^ n ) x. ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) ) ) |
155 |
151 154
|
eqtrd |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( F ` ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) ) = ( ( ( F ` M ) ^ n ) x. ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) ) ) |
156 |
155
|
oveq2d |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( F ` ( k mod ( M ^ n ) ) ) + ( F ` ( ( M ^ n ) x. ( |_ ` ( k / ( M ^ n ) ) ) ) ) ) = ( ( F ` ( k mod ( M ^ n ) ) ) + ( ( ( F ` M ) ^ n ) x. ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) ) ) ) |
157 |
136 146 156
|
3brtr3d |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( F ` k ) <_ ( ( F ` ( k mod ( M ^ n ) ) ) + ( ( ( F ` M ) ^ n ) x. ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) ) ) ) |
158 |
122 97
|
reexpcld |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( T ^ n ) e. RR ) |
159 |
121 158
|
remulcld |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( M x. ( n + 1 ) ) x. ( T ^ n ) ) e. RR ) |
160 |
|
nn0re |
|- ( n e. NN0 -> n e. RR ) |
161 |
160
|
ad2antlr |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> n e. RR ) |
162 |
117 161
|
remulcld |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( M x. n ) e. RR ) |
163 |
162 158
|
remulcld |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( M x. n ) x. ( T ^ n ) ) e. RR ) |
164 |
117 158
|
remulcld |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( M x. ( T ^ n ) ) e. RR ) |
165 |
|
fveq2 |
|- ( j = ( k mod ( M ^ n ) ) -> ( F ` j ) = ( F ` ( k mod ( M ^ n ) ) ) ) |
166 |
165
|
breq1d |
|- ( j = ( k mod ( M ^ n ) ) -> ( ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) <-> ( F ` ( k mod ( M ^ n ) ) ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) |
167 |
|
simprr |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) |
168 |
|
zmodfz |
|- ( ( k e. ZZ /\ ( M ^ n ) e. NN ) -> ( k mod ( M ^ n ) ) e. ( 0 ... ( ( M ^ n ) - 1 ) ) ) |
169 |
91 98 168
|
syl2anc |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( k mod ( M ^ n ) ) e. ( 0 ... ( ( M ^ n ) - 1 ) ) ) |
170 |
166 167 169
|
rspcdva |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( F ` ( k mod ( M ^ n ) ) ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) |
171 |
117 107
|
remulcld |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( M x. ( ( F ` M ) ^ n ) ) e. RR ) |
172 |
107
|
recnd |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( F ` M ) ^ n ) e. CC ) |
173 |
114
|
recnd |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) e. CC ) |
174 |
172 173
|
mulcomd |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( ( F ` M ) ^ n ) x. ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) ) = ( ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) x. ( ( F ` M ) ^ n ) ) ) |
175 |
2 67
|
abvge0 |
|- ( ( F e. A /\ M e. QQ ) -> 0 <_ ( F ` M ) ) |
176 |
89 105 175
|
syl2anc |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> 0 <_ ( F ` M ) ) |
177 |
106 97 176
|
expge0d |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> 0 <_ ( ( F ` M ) ^ n ) ) |
178 |
110
|
zred |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( |_ ` ( k / ( M ^ n ) ) ) e. RR ) |
179 |
|
elfzle1 |
|- ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) -> 0 <_ k ) |
180 |
179
|
ad2antrl |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> 0 <_ k ) |
181 |
98
|
nnred |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( M ^ n ) e. RR ) |
182 |
98
|
nngt0d |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> 0 < ( M ^ n ) ) |
183 |
|
divge0 |
|- ( ( ( k e. RR /\ 0 <_ k ) /\ ( ( M ^ n ) e. RR /\ 0 < ( M ^ n ) ) ) -> 0 <_ ( k / ( M ^ n ) ) ) |
184 |
108 180 181 182 183
|
syl22anc |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> 0 <_ ( k / ( M ^ n ) ) ) |
185 |
|
flge0nn0 |
|- ( ( ( k / ( M ^ n ) ) e. RR /\ 0 <_ ( k / ( M ^ n ) ) ) -> ( |_ ` ( k / ( M ^ n ) ) ) e. NN0 ) |
186 |
109 184 185
|
syl2anc |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( |_ ` ( k / ( M ^ n ) ) ) e. NN0 ) |
187 |
1 2
|
qabvle |
|- ( ( F e. A /\ ( |_ ` ( k / ( M ^ n ) ) ) e. NN0 ) -> ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) <_ ( |_ ` ( k / ( M ^ n ) ) ) ) |
188 |
89 186 187
|
syl2anc |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) <_ ( |_ ` ( k / ( M ^ n ) ) ) ) |
189 |
|
simprl |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) ) |
190 |
|
0z |
|- 0 e. ZZ |
191 |
96 124
|
nnexpcld |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( M ^ ( n + 1 ) ) e. NN ) |
192 |
191
|
nnzd |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( M ^ ( n + 1 ) ) e. ZZ ) |
193 |
|
elfzm11 |
|- ( ( 0 e. ZZ /\ ( M ^ ( n + 1 ) ) e. ZZ ) -> ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) <-> ( k e. ZZ /\ 0 <_ k /\ k < ( M ^ ( n + 1 ) ) ) ) ) |
194 |
190 192 193
|
sylancr |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) <-> ( k e. ZZ /\ 0 <_ k /\ k < ( M ^ ( n + 1 ) ) ) ) ) |
195 |
189 194
|
mpbid |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( k e. ZZ /\ 0 <_ k /\ k < ( M ^ ( n + 1 ) ) ) ) |
196 |
195
|
simp3d |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> k < ( M ^ ( n + 1 ) ) ) |
197 |
96
|
nncnd |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> M e. CC ) |
198 |
197 97
|
expp1d |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( M ^ ( n + 1 ) ) = ( ( M ^ n ) x. M ) ) |
199 |
196 198
|
breqtrd |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> k < ( ( M ^ n ) x. M ) ) |
200 |
|
ltdivmul |
|- ( ( k e. RR /\ M e. RR /\ ( ( M ^ n ) e. RR /\ 0 < ( M ^ n ) ) ) -> ( ( k / ( M ^ n ) ) < M <-> k < ( ( M ^ n ) x. M ) ) ) |
201 |
108 117 181 182 200
|
syl112anc |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( k / ( M ^ n ) ) < M <-> k < ( ( M ^ n ) x. M ) ) ) |
202 |
199 201
|
mpbird |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( k / ( M ^ n ) ) < M ) |
203 |
96
|
nnzd |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> M e. ZZ ) |
204 |
|
fllt |
|- ( ( ( k / ( M ^ n ) ) e. RR /\ M e. ZZ ) -> ( ( k / ( M ^ n ) ) < M <-> ( |_ ` ( k / ( M ^ n ) ) ) < M ) ) |
205 |
109 203 204
|
syl2anc |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( k / ( M ^ n ) ) < M <-> ( |_ ` ( k / ( M ^ n ) ) ) < M ) ) |
206 |
202 205
|
mpbid |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( |_ ` ( k / ( M ^ n ) ) ) < M ) |
207 |
178 117 206
|
ltled |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( |_ ` ( k / ( M ^ n ) ) ) <_ M ) |
208 |
114 178 117 188 207
|
letrd |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) <_ M ) |
209 |
114 117 107 177 208
|
lemul1ad |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) x. ( ( F ` M ) ^ n ) ) <_ ( M x. ( ( F ` M ) ^ n ) ) ) |
210 |
174 209
|
eqbrtrd |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( ( F ` M ) ^ n ) x. ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) ) <_ ( M x. ( ( F ` M ) ^ n ) ) ) |
211 |
96
|
nnnn0d |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> M e. NN0 ) |
212 |
211
|
nn0ge0d |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> 0 <_ M ) |
213 |
|
max1 |
|- ( ( ( F ` M ) e. RR /\ 1 e. RR ) -> ( F ` M ) <_ if ( ( F ` M ) <_ 1 , 1 , ( F ` M ) ) ) |
214 |
106 64 213
|
sylancl |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( F ` M ) <_ if ( ( F ` M ) <_ 1 , 1 , ( F ` M ) ) ) |
215 |
214 11
|
breqtrrdi |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( F ` M ) <_ T ) |
216 |
|
leexp1a |
|- ( ( ( ( F ` M ) e. RR /\ T e. RR /\ n e. NN0 ) /\ ( 0 <_ ( F ` M ) /\ ( F ` M ) <_ T ) ) -> ( ( F ` M ) ^ n ) <_ ( T ^ n ) ) |
217 |
106 122 97 176 215 216
|
syl32anc |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( F ` M ) ^ n ) <_ ( T ^ n ) ) |
218 |
107 158 117 212 217
|
lemul2ad |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( M x. ( ( F ` M ) ^ n ) ) <_ ( M x. ( T ^ n ) ) ) |
219 |
115 171 164 210 218
|
letrd |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( ( F ` M ) ^ n ) x. ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) ) <_ ( M x. ( T ^ n ) ) ) |
220 |
104 115 163 164 170 219
|
le2addd |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( F ` ( k mod ( M ^ n ) ) ) + ( ( ( F ` M ) ^ n ) x. ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) ) ) <_ ( ( ( M x. n ) x. ( T ^ n ) ) + ( M x. ( T ^ n ) ) ) ) |
221 |
|
nn0cn |
|- ( n e. NN0 -> n e. CC ) |
222 |
221
|
ad2antlr |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> n e. CC ) |
223 |
|
1cnd |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> 1 e. CC ) |
224 |
197 222 223
|
adddid |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( M x. ( n + 1 ) ) = ( ( M x. n ) + ( M x. 1 ) ) ) |
225 |
197
|
mulid1d |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( M x. 1 ) = M ) |
226 |
225
|
oveq2d |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( M x. n ) + ( M x. 1 ) ) = ( ( M x. n ) + M ) ) |
227 |
224 226
|
eqtrd |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( M x. ( n + 1 ) ) = ( ( M x. n ) + M ) ) |
228 |
227
|
oveq1d |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( M x. ( n + 1 ) ) x. ( T ^ n ) ) = ( ( ( M x. n ) + M ) x. ( T ^ n ) ) ) |
229 |
197 222
|
mulcld |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( M x. n ) e. CC ) |
230 |
158
|
recnd |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( T ^ n ) e. CC ) |
231 |
229 197 230
|
adddird |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( ( M x. n ) + M ) x. ( T ^ n ) ) = ( ( ( M x. n ) x. ( T ^ n ) ) + ( M x. ( T ^ n ) ) ) ) |
232 |
228 231
|
eqtrd |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( M x. ( n + 1 ) ) x. ( T ^ n ) ) = ( ( ( M x. n ) x. ( T ^ n ) ) + ( M x. ( T ^ n ) ) ) ) |
233 |
220 232
|
breqtrrd |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( F ` ( k mod ( M ^ n ) ) ) + ( ( ( F ` M ) ^ n ) x. ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) ) ) <_ ( ( M x. ( n + 1 ) ) x. ( T ^ n ) ) ) |
234 |
|
max2 |
|- ( ( ( F ` M ) e. RR /\ 1 e. RR ) -> 1 <_ if ( ( F ` M ) <_ 1 , 1 , ( F ` M ) ) ) |
235 |
106 64 234
|
sylancl |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> 1 <_ if ( ( F ` M ) <_ 1 , 1 , ( F ` M ) ) ) |
236 |
235 11
|
breqtrrdi |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> 1 <_ T ) |
237 |
|
nn0z |
|- ( n e. NN0 -> n e. ZZ ) |
238 |
237
|
ad2antlr |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> n e. ZZ ) |
239 |
|
uzid |
|- ( n e. ZZ -> n e. ( ZZ>= ` n ) ) |
240 |
238 239
|
syl |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> n e. ( ZZ>= ` n ) ) |
241 |
|
peano2uz |
|- ( n e. ( ZZ>= ` n ) -> ( n + 1 ) e. ( ZZ>= ` n ) ) |
242 |
240 241
|
syl |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( n + 1 ) e. ( ZZ>= ` n ) ) |
243 |
122 236 242
|
leexp2ad |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( T ^ n ) <_ ( T ^ ( n + 1 ) ) ) |
244 |
96 119
|
nnmulcld |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( M x. ( n + 1 ) ) e. NN ) |
245 |
244
|
nngt0d |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> 0 < ( M x. ( n + 1 ) ) ) |
246 |
|
lemul2 |
|- ( ( ( T ^ n ) e. RR /\ ( T ^ ( n + 1 ) ) e. RR /\ ( ( M x. ( n + 1 ) ) e. RR /\ 0 < ( M x. ( n + 1 ) ) ) ) -> ( ( T ^ n ) <_ ( T ^ ( n + 1 ) ) <-> ( ( M x. ( n + 1 ) ) x. ( T ^ n ) ) <_ ( ( M x. ( n + 1 ) ) x. ( T ^ ( n + 1 ) ) ) ) ) |
247 |
158 125 121 245 246
|
syl112anc |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( T ^ n ) <_ ( T ^ ( n + 1 ) ) <-> ( ( M x. ( n + 1 ) ) x. ( T ^ n ) ) <_ ( ( M x. ( n + 1 ) ) x. ( T ^ ( n + 1 ) ) ) ) ) |
248 |
243 247
|
mpbid |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( M x. ( n + 1 ) ) x. ( T ^ n ) ) <_ ( ( M x. ( n + 1 ) ) x. ( T ^ ( n + 1 ) ) ) ) |
249 |
116 159 126 233 248
|
letrd |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( ( F ` ( k mod ( M ^ n ) ) ) + ( ( ( F ` M ) ^ n ) x. ( F ` ( |_ ` ( k / ( M ^ n ) ) ) ) ) ) <_ ( ( M x. ( n + 1 ) ) x. ( T ^ ( n + 1 ) ) ) ) |
250 |
95 116 126 157 249
|
letrd |
|- ( ( ( ph /\ n e. NN0 ) /\ ( k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) /\ A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) ) -> ( F ` k ) <_ ( ( M x. ( n + 1 ) ) x. ( T ^ ( n + 1 ) ) ) ) |
251 |
250
|
expr |
|- ( ( ( ph /\ n e. NN0 ) /\ k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) ) -> ( A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) -> ( F ` k ) <_ ( ( M x. ( n + 1 ) ) x. ( T ^ ( n + 1 ) ) ) ) ) |
252 |
251
|
ralrimdva |
|- ( ( ph /\ n e. NN0 ) -> ( A. j e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` j ) <_ ( ( M x. n ) x. ( T ^ n ) ) -> A. k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) ( F ` k ) <_ ( ( M x. ( n + 1 ) ) x. ( T ^ ( n + 1 ) ) ) ) ) |
253 |
88 252
|
syl5bi |
|- ( ( ph /\ n e. NN0 ) -> ( A. k e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` k ) <_ ( ( M x. n ) x. ( T ^ n ) ) -> A. k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) ( F ` k ) <_ ( ( M x. ( n + 1 ) ) x. ( T ^ ( n + 1 ) ) ) ) ) |
254 |
253
|
expcom |
|- ( n e. NN0 -> ( ph -> ( A. k e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` k ) <_ ( ( M x. n ) x. ( T ^ n ) ) -> A. k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) ( F ` k ) <_ ( ( M x. ( n + 1 ) ) x. ( T ^ ( n + 1 ) ) ) ) ) ) |
255 |
254
|
a2d |
|- ( n e. NN0 -> ( ( ph -> A. k e. ( 0 ... ( ( M ^ n ) - 1 ) ) ( F ` k ) <_ ( ( M x. n ) x. ( T ^ n ) ) ) -> ( ph -> A. k e. ( 0 ... ( ( M ^ ( n + 1 ) ) - 1 ) ) ( F ` k ) <_ ( ( M x. ( n + 1 ) ) x. ( T ^ ( n + 1 ) ) ) ) ) ) |
256 |
20 29 38 47 85 255
|
nn0ind |
|- ( X e. NN0 -> ( ph -> A. k e. ( 0 ... ( ( M ^ X ) - 1 ) ) ( F ` k ) <_ ( ( M x. X ) x. ( T ^ X ) ) ) ) |
257 |
256
|
impcom |
|- ( ( ph /\ X e. NN0 ) -> A. k e. ( 0 ... ( ( M ^ X ) - 1 ) ) ( F ` k ) <_ ( ( M x. X ) x. ( T ^ X ) ) ) |
258 |
|
fveq2 |
|- ( k = Y -> ( F ` k ) = ( F ` Y ) ) |
259 |
258
|
breq1d |
|- ( k = Y -> ( ( F ` k ) <_ ( ( M x. X ) x. ( T ^ X ) ) <-> ( F ` Y ) <_ ( ( M x. X ) x. ( T ^ X ) ) ) ) |
260 |
259
|
rspccv |
|- ( A. k e. ( 0 ... ( ( M ^ X ) - 1 ) ) ( F ` k ) <_ ( ( M x. X ) x. ( T ^ X ) ) -> ( Y e. ( 0 ... ( ( M ^ X ) - 1 ) ) -> ( F ` Y ) <_ ( ( M x. X ) x. ( T ^ X ) ) ) ) |
261 |
257 260
|
syl |
|- ( ( ph /\ X e. NN0 ) -> ( Y e. ( 0 ... ( ( M ^ X ) - 1 ) ) -> ( F ` Y ) <_ ( ( M x. X ) x. ( T ^ X ) ) ) ) |
262 |
261
|
3impia |
|- ( ( ph /\ X e. NN0 /\ Y e. ( 0 ... ( ( M ^ X ) - 1 ) ) ) -> ( F ` Y ) <_ ( ( M x. X ) x. ( T ^ X ) ) ) |