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

Theorem flodddiv4 11473
Description: The floor of an odd integer divided by 4. (Contributed by AV, 17-Jun-2021.)
Assertion
Ref Expression
flodddiv4  |-  ( ( M  e.  ZZ  /\  N  =  ( (
2  x.  M )  +  1 ) )  ->  ( |_ `  ( N  /  4
) )  =  if ( 2  ||  M ,  ( M  / 
2 ) ,  ( ( M  -  1 )  /  2 ) ) )

Proof of Theorem flodddiv4
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 oveq1 5733 . . . 4  |-  ( N  =  ( ( 2  x.  M )  +  1 )  ->  ( N  /  4 )  =  ( ( ( 2  x.  M )  +  1 )  /  4
) )
2 2cnd 8697 . . . . . . 7  |-  ( M  e.  ZZ  ->  2  e.  CC )
3 zcn 8957 . . . . . . 7  |-  ( M  e.  ZZ  ->  M  e.  CC )
42, 3mulcld 7704 . . . . . 6  |-  ( M  e.  ZZ  ->  (
2  x.  M )  e.  CC )
5 1cnd 7700 . . . . . 6  |-  ( M  e.  ZZ  ->  1  e.  CC )
6 4cn 8702 . . . . . . 7  |-  4  e.  CC
76a1i 9 . . . . . 6  |-  ( M  e.  ZZ  ->  4  e.  CC )
8 4ap0 8723 . . . . . . 7  |-  4 #  0
98a1i 9 . . . . . 6  |-  ( M  e.  ZZ  ->  4 #  0 )
104, 5, 7, 9divdirapd 8496 . . . . 5  |-  ( M  e.  ZZ  ->  (
( ( 2  x.  M )  +  1 )  /  4 )  =  ( ( ( 2  x.  M )  /  4 )  +  ( 1  /  4
) ) )
11 2t2e4 8772 . . . . . . . . . 10  |-  ( 2  x.  2 )  =  4
1211eqcomi 2117 . . . . . . . . 9  |-  4  =  ( 2  x.  2 )
1312a1i 9 . . . . . . . 8  |-  ( M  e.  ZZ  ->  4  =  ( 2  x.  2 ) )
1413oveq2d 5742 . . . . . . 7  |-  ( M  e.  ZZ  ->  (
( 2  x.  M
)  /  4 )  =  ( ( 2  x.  M )  / 
( 2  x.  2 ) ) )
15 2ap0 8717 . . . . . . . . 9  |-  2 #  0
1615a1i 9 . . . . . . . 8  |-  ( M  e.  ZZ  ->  2 #  0 )
173, 2, 2, 16, 16divcanap5d 8484 . . . . . . 7  |-  ( M  e.  ZZ  ->  (
( 2  x.  M
)  /  ( 2  x.  2 ) )  =  ( M  / 
2 ) )
1814, 17eqtrd 2145 . . . . . 6  |-  ( M  e.  ZZ  ->  (
( 2  x.  M
)  /  4 )  =  ( M  / 
2 ) )
1918oveq1d 5741 . . . . 5  |-  ( M  e.  ZZ  ->  (
( ( 2  x.  M )  /  4
)  +  ( 1  /  4 ) )  =  ( ( M  /  2 )  +  ( 1  /  4
) ) )
2010, 19eqtrd 2145 . . . 4  |-  ( M  e.  ZZ  ->  (
( ( 2  x.  M )  +  1 )  /  4 )  =  ( ( M  /  2 )  +  ( 1  /  4
) ) )
211, 20sylan9eqr 2167 . . 3  |-  ( ( M  e.  ZZ  /\  N  =  ( (
2  x.  M )  +  1 ) )  ->  ( N  / 
4 )  =  ( ( M  /  2
)  +  ( 1  /  4 ) ) )
2221fveq2d 5377 . 2  |-  ( ( M  e.  ZZ  /\  N  =  ( (
2  x.  M )  +  1 ) )  ->  ( |_ `  ( N  /  4
) )  =  ( |_ `  ( ( M  /  2 )  +  ( 1  / 
4 ) ) ) )
23 iftrue 3443 . . . . . . . 8  |-  ( 2 
||  M  ->  if ( 2  ||  M ,  ( M  / 
2 ) ,  ( ( M  -  1 )  /  2 ) )  =  ( M  /  2 ) )
2423adantr 272 . . . . . . 7  |-  ( ( 2  ||  M  /\  M  e.  ZZ )  ->  if ( 2  ||  M ,  ( M  /  2 ) ,  ( ( M  - 
1 )  /  2
) )  =  ( M  /  2 ) )
25 1re 7683 . . . . . . . . . 10  |-  1  e.  RR
26 0le1 8156 . . . . . . . . . 10  |-  0  <_  1
27 4re 8701 . . . . . . . . . 10  |-  4  e.  RR
28 4pos 8721 . . . . . . . . . 10  |-  0  <  4
29 divge0 8535 . . . . . . . . . 10  |-  ( ( ( 1  e.  RR  /\  0  <_  1 )  /\  ( 4  e.  RR  /\  0  <  4 ) )  -> 
0  <_  ( 1  /  4 ) )
3025, 26, 27, 28, 29mp4an 421 . . . . . . . . 9  |-  0  <_  ( 1  /  4
)
31 1lt4 8792 . . . . . . . . . 10  |-  1  <  4
32 recgt1 8559 . . . . . . . . . . 11  |-  ( ( 4  e.  RR  /\  0  <  4 )  -> 
( 1  <  4  <->  ( 1  /  4 )  <  1 ) )
3327, 28, 32mp2an 420 . . . . . . . . . 10  |-  ( 1  <  4  <->  ( 1  /  4 )  <  1 )
3431, 33mpbi 144 . . . . . . . . 9  |-  ( 1  /  4 )  <  1
3530, 34pm3.2i 268 . . . . . . . 8  |-  ( 0  <_  ( 1  / 
4 )  /\  (
1  /  4 )  <  1 )
36 evend2 11428 . . . . . . . . . 10  |-  ( M  e.  ZZ  ->  (
2  ||  M  <->  ( M  /  2 )  e.  ZZ ) )
3736biimpac 294 . . . . . . . . 9  |-  ( ( 2  ||  M  /\  M  e.  ZZ )  ->  ( M  /  2
)  e.  ZZ )
38 4nn 8781 . . . . . . . . . 10  |-  4  e.  NN
39 nnrecq 9333 . . . . . . . . . 10  |-  ( 4  e.  NN  ->  (
1  /  4 )  e.  QQ )
4038, 39ax-mp 7 . . . . . . . . 9  |-  ( 1  /  4 )  e.  QQ
41 flqbi2 9951 . . . . . . . . 9  |-  ( ( ( M  /  2
)  e.  ZZ  /\  ( 1  /  4
)  e.  QQ )  ->  ( ( |_
`  ( ( M  /  2 )  +  ( 1  /  4
) ) )  =  ( M  /  2
)  <->  ( 0  <_ 
( 1  /  4
)  /\  ( 1  /  4 )  <  1 ) ) )
4237, 40, 41sylancl 407 . . . . . . . 8  |-  ( ( 2  ||  M  /\  M  e.  ZZ )  ->  ( ( |_ `  ( ( M  / 
2 )  +  ( 1  /  4 ) ) )  =  ( M  /  2 )  <-> 
( 0  <_  (
1  /  4 )  /\  ( 1  / 
4 )  <  1
) ) )
4335, 42mpbiri 167 . . . . . . 7  |-  ( ( 2  ||  M  /\  M  e.  ZZ )  ->  ( |_ `  (
( M  /  2
)  +  ( 1  /  4 ) ) )  =  ( M  /  2 ) )
4424, 43eqtr4d 2148 . . . . . 6  |-  ( ( 2  ||  M  /\  M  e.  ZZ )  ->  if ( 2  ||  M ,  ( M  /  2 ) ,  ( ( M  - 
1 )  /  2
) )  =  ( |_ `  ( ( M  /  2 )  +  ( 1  / 
4 ) ) ) )
4544expcom 115 . . . . 5  |-  ( M  e.  ZZ  ->  (
2  ||  M  ->  if ( 2  ||  M ,  ( M  / 
2 ) ,  ( ( M  -  1 )  /  2 ) )  =  ( |_
`  ( ( M  /  2 )  +  ( 1  /  4
) ) ) ) )
46 iffalse 3446 . . . . . . . 8  |-  ( -.  2  ||  M  ->  if ( 2  ||  M ,  ( M  / 
2 ) ,  ( ( M  -  1 )  /  2 ) )  =  ( ( M  -  1 )  /  2 ) )
4746adantr 272 . . . . . . 7  |-  ( ( -.  2  ||  M  /\  M  e.  ZZ )  ->  if ( 2 
||  M ,  ( M  /  2 ) ,  ( ( M  -  1 )  / 
2 ) )  =  ( ( M  - 
1 )  /  2
) )
48 odd2np1 11412 . . . . . . . . 9  |-  ( M  e.  ZZ  ->  ( -.  2  ||  M  <->  E. x  e.  ZZ  ( ( 2  x.  x )  +  1 )  =  M ) )
49 ax-1cn 7632 . . . . . . . . . . . . . . . . . . . . . 22  |-  1  e.  CC
50 2cn 8695 . . . . . . . . . . . . . . . . . . . . . . 23  |-  2  e.  CC
5150, 15pm3.2i 268 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 2  e.  CC  /\  2 #  0 )
52 divcanap5 8381 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 1  e.  CC  /\  ( 2  e.  CC  /\  2 #  0 )  /\  ( 2  e.  CC  /\  2 #  0 ) )  ->  ( ( 2  x.  1 )  / 
( 2  x.  2 ) )  =  ( 1  /  2 ) )
5349, 51, 51, 52mp3an 1296 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 2  x.  1 )  /  ( 2  x.  2 ) )  =  ( 1  /  2
)
54 2t1e2 8771 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 2  x.  1 )  =  2
5554, 11oveq12i 5738 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 2  x.  1 )  /  ( 2  x.  2 ) )  =  ( 2  /  4
)
5653, 55eqtr3i 2135 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1  /  2 )  =  ( 2  /  4
)
5756oveq1i 5736 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 1  /  2 )  +  ( 1  / 
4 ) )  =  ( ( 2  / 
4 )  +  ( 1  /  4 ) )
5850, 49, 6, 8divdirapi 8436 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 2  +  1 )  /  4 )  =  ( ( 2  / 
4 )  +  ( 1  /  4 ) )
59 2p1e3 8751 . . . . . . . . . . . . . . . . . . . 20  |-  ( 2  +  1 )  =  3
6059oveq1i 5736 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 2  +  1 )  /  4 )  =  ( 3  /  4
)
6157, 58, 603eqtr2i 2139 . . . . . . . . . . . . . . . . . 18  |-  ( ( 1  /  2 )  +  ( 1  / 
4 ) )  =  ( 3  /  4
)
6261a1i 9 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ZZ  ->  (
( 1  /  2
)  +  ( 1  /  4 ) )  =  ( 3  / 
4 ) )
6362oveq2d 5742 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ZZ  ->  (
x  +  ( ( 1  /  2 )  +  ( 1  / 
4 ) ) )  =  ( x  +  ( 3  /  4
) ) )
6463fveq2d 5377 . . . . . . . . . . . . . . 15  |-  ( x  e.  ZZ  ->  ( |_ `  ( x  +  ( ( 1  / 
2 )  +  ( 1  /  4 ) ) ) )  =  ( |_ `  (
x  +  ( 3  /  4 ) ) ) )
65 3re 8698 . . . . . . . . . . . . . . . . . 18  |-  3  e.  RR
66 0re 7684 . . . . . . . . . . . . . . . . . . 19  |-  0  e.  RR
67 3pos 8718 . . . . . . . . . . . . . . . . . . 19  |-  0  <  3
6866, 65, 67ltleii 7783 . . . . . . . . . . . . . . . . . 18  |-  0  <_  3
69 divge0 8535 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 3  e.  RR  /\  0  <_  3 )  /\  ( 4  e.  RR  /\  0  <  4 ) )  -> 
0  <_  ( 3  /  4 ) )
7065, 68, 27, 28, 69mp4an 421 . . . . . . . . . . . . . . . . 17  |-  0  <_  ( 3  /  4
)
71 3lt4 8790 . . . . . . . . . . . . . . . . . 18  |-  3  <  4
72 nnrp 9346 . . . . . . . . . . . . . . . . . . . 20  |-  ( 4  e.  NN  ->  4  e.  RR+ )
7338, 72ax-mp 7 . . . . . . . . . . . . . . . . . . 19  |-  4  e.  RR+
74 divlt1lt 9404 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 3  e.  RR  /\  4  e.  RR+ )  -> 
( ( 3  / 
4 )  <  1  <->  3  <  4 ) )
7565, 73, 74mp2an 420 . . . . . . . . . . . . . . . . . 18  |-  ( ( 3  /  4 )  <  1  <->  3  <  4 )
7671, 75mpbir 145 . . . . . . . . . . . . . . . . 17  |-  ( 3  /  4 )  <  1
7770, 76pm3.2i 268 . . . . . . . . . . . . . . . 16  |-  ( 0  <_  ( 3  / 
4 )  /\  (
3  /  4 )  <  1 )
78 3z 8981 . . . . . . . . . . . . . . . . . 18  |-  3  e.  ZZ
79 znq 9312 . . . . . . . . . . . . . . . . . 18  |-  ( ( 3  e.  ZZ  /\  4  e.  NN )  ->  ( 3  /  4
)  e.  QQ )
8078, 38, 79mp2an 420 . . . . . . . . . . . . . . . . 17  |-  ( 3  /  4 )  e.  QQ
81 flqbi2 9951 . . . . . . . . . . . . . . . . 17  |-  ( ( x  e.  ZZ  /\  ( 3  /  4
)  e.  QQ )  ->  ( ( |_
`  ( x  +  ( 3  /  4
) ) )  =  x  <->  ( 0  <_ 
( 3  /  4
)  /\  ( 3  /  4 )  <  1 ) ) )
8280, 81mpan2 419 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ZZ  ->  (
( |_ `  (
x  +  ( 3  /  4 ) ) )  =  x  <->  ( 0  <_  ( 3  / 
4 )  /\  (
3  /  4 )  <  1 ) ) )
8377, 82mpbiri 167 . . . . . . . . . . . . . . 15  |-  ( x  e.  ZZ  ->  ( |_ `  ( x  +  ( 3  /  4
) ) )  =  x )
8464, 83eqtrd 2145 . . . . . . . . . . . . . 14  |-  ( x  e.  ZZ  ->  ( |_ `  ( x  +  ( ( 1  / 
2 )  +  ( 1  /  4 ) ) ) )  =  x )
8584adantr 272 . . . . . . . . . . . . 13  |-  ( ( x  e.  ZZ  /\  ( ( 2  x.  x )  +  1 )  =  M )  ->  ( |_ `  ( x  +  (
( 1  /  2
)  +  ( 1  /  4 ) ) ) )  =  x )
86 oveq1 5733 . . . . . . . . . . . . . . . . . 18  |-  ( M  =  ( ( 2  x.  x )  +  1 )  ->  ( M  /  2 )  =  ( ( ( 2  x.  x )  +  1 )  /  2
) )
8786eqcoms 2116 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 2  x.  x
)  +  1 )  =  M  ->  ( M  /  2 )  =  ( ( ( 2  x.  x )  +  1 )  /  2
) )
88 2z 8980 . . . . . . . . . . . . . . . . . . . . . 22  |-  2  e.  ZZ
8988a1i 9 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ZZ  ->  2  e.  ZZ )
90 id 19 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ZZ  ->  x  e.  ZZ )
9189, 90zmulcld 9077 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ZZ  ->  (
2  x.  x )  e.  ZZ )
9291zcnd 9072 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ZZ  ->  (
2  x.  x )  e.  CC )
93 1cnd 7700 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ZZ  ->  1  e.  CC )
94 2cnd 8697 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ZZ  ->  2  e.  CC )
9515a1i 9 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ZZ  ->  2 #  0 )
9692, 93, 94, 95divdirapd 8496 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ZZ  ->  (
( ( 2  x.  x )  +  1 )  /  2 )  =  ( ( ( 2  x.  x )  /  2 )  +  ( 1  /  2
) ) )
97 zcn 8957 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ZZ  ->  x  e.  CC )
9897, 94, 95divcanap3d 8462 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ZZ  ->  (
( 2  x.  x
)  /  2 )  =  x )
9998oveq1d 5741 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ZZ  ->  (
( ( 2  x.  x )  /  2
)  +  ( 1  /  2 ) )  =  ( x  +  ( 1  /  2
) ) )
10096, 99eqtrd 2145 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ZZ  ->  (
( ( 2  x.  x )  +  1 )  /  2 )  =  ( x  +  ( 1  /  2
) ) )
10187, 100sylan9eqr 2167 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  ZZ  /\  ( ( 2  x.  x )  +  1 )  =  M )  ->  ( M  / 
2 )  =  ( x  +  ( 1  /  2 ) ) )
102101oveq1d 5741 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  ZZ  /\  ( ( 2  x.  x )  +  1 )  =  M )  ->  ( ( M  /  2 )  +  ( 1  /  4
) )  =  ( ( x  +  ( 1  /  2 ) )  +  ( 1  /  4 ) ) )
103 halfcn 8832 . . . . . . . . . . . . . . . . . 18  |-  ( 1  /  2 )  e.  CC
104103a1i 9 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ZZ  ->  (
1  /  2 )  e.  CC )
1056, 8recclapi 8409 . . . . . . . . . . . . . . . . . 18  |-  ( 1  /  4 )  e.  CC
106105a1i 9 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ZZ  ->  (
1  /  4 )  e.  CC )
10797, 104, 106addassd 7706 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ZZ  ->  (
( x  +  ( 1  /  2 ) )  +  ( 1  /  4 ) )  =  ( x  +  ( ( 1  / 
2 )  +  ( 1  /  4 ) ) ) )
108107adantr 272 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  ZZ  /\  ( ( 2  x.  x )  +  1 )  =  M )  ->  ( ( x  +  ( 1  / 
2 ) )  +  ( 1  /  4
) )  =  ( x  +  ( ( 1  /  2 )  +  ( 1  / 
4 ) ) ) )
109102, 108eqtrd 2145 . . . . . . . . . . . . . 14  |-  ( ( x  e.  ZZ  /\  ( ( 2  x.  x )  +  1 )  =  M )  ->  ( ( M  /  2 )  +  ( 1  /  4
) )  =  ( x  +  ( ( 1  /  2 )  +  ( 1  / 
4 ) ) ) )
110109fveq2d 5377 . . . . . . . . . . . . 13  |-  ( ( x  e.  ZZ  /\  ( ( 2  x.  x )  +  1 )  =  M )  ->  ( |_ `  ( ( M  / 
2 )  +  ( 1  /  4 ) ) )  =  ( |_ `  ( x  +  ( ( 1  /  2 )  +  ( 1  /  4
) ) ) ) )
111 oveq1 5733 . . . . . . . . . . . . . . . . 17  |-  ( M  =  ( ( 2  x.  x )  +  1 )  ->  ( M  -  1 )  =  ( ( ( 2  x.  x )  +  1 )  - 
1 ) )
112111eqcoms 2116 . . . . . . . . . . . . . . . 16  |-  ( ( ( 2  x.  x
)  +  1 )  =  M  ->  ( M  -  1 )  =  ( ( ( 2  x.  x )  +  1 )  - 
1 ) )
113 pncan1 8052 . . . . . . . . . . . . . . . . 17  |-  ( ( 2  x.  x )  e.  CC  ->  (
( ( 2  x.  x )  +  1 )  -  1 )  =  ( 2  x.  x ) )
11492, 113syl 14 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ZZ  ->  (
( ( 2  x.  x )  +  1 )  -  1 )  =  ( 2  x.  x ) )
115112, 114sylan9eqr 2167 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  ZZ  /\  ( ( 2  x.  x )  +  1 )  =  M )  ->  ( M  - 
1 )  =  ( 2  x.  x ) )
116115oveq1d 5741 . . . . . . . . . . . . . 14  |-  ( ( x  e.  ZZ  /\  ( ( 2  x.  x )  +  1 )  =  M )  ->  ( ( M  -  1 )  / 
2 )  =  ( ( 2  x.  x
)  /  2 ) )
11798adantr 272 . . . . . . . . . . . . . 14  |-  ( ( x  e.  ZZ  /\  ( ( 2  x.  x )  +  1 )  =  M )  ->  ( ( 2  x.  x )  / 
2 )  =  x )
118116, 117eqtrd 2145 . . . . . . . . . . . . 13  |-  ( ( x  e.  ZZ  /\  ( ( 2  x.  x )  +  1 )  =  M )  ->  ( ( M  -  1 )  / 
2 )  =  x )
11985, 110, 1183eqtr4rd 2156 . . . . . . . . . . . 12  |-  ( ( x  e.  ZZ  /\  ( ( 2  x.  x )  +  1 )  =  M )  ->  ( ( M  -  1 )  / 
2 )  =  ( |_ `  ( ( M  /  2 )  +  ( 1  / 
4 ) ) ) )
120119ex 114 . . . . . . . . . . 11  |-  ( x  e.  ZZ  ->  (
( ( 2  x.  x )  +  1 )  =  M  -> 
( ( M  - 
1 )  /  2
)  =  ( |_
`  ( ( M  /  2 )  +  ( 1  /  4
) ) ) ) )
121120adantl 273 . . . . . . . . . 10  |-  ( ( M  e.  ZZ  /\  x  e.  ZZ )  ->  ( ( ( 2  x.  x )  +  1 )  =  M  ->  ( ( M  -  1 )  / 
2 )  =  ( |_ `  ( ( M  /  2 )  +  ( 1  / 
4 ) ) ) ) )
122121rexlimdva 2521 . . . . . . . . 9  |-  ( M  e.  ZZ  ->  ( E. x  e.  ZZ  ( ( 2  x.  x )  +  1 )  =  M  -> 
( ( M  - 
1 )  /  2
)  =  ( |_
`  ( ( M  /  2 )  +  ( 1  /  4
) ) ) ) )
12348, 122sylbid 149 . . . . . . . 8  |-  ( M  e.  ZZ  ->  ( -.  2  ||  M  -> 
( ( M  - 
1 )  /  2
)  =  ( |_
`  ( ( M  /  2 )  +  ( 1  /  4
) ) ) ) )
124123impcom 124 . . . . . . 7  |-  ( ( -.  2  ||  M  /\  M  e.  ZZ )  ->  ( ( M  -  1 )  / 
2 )  =  ( |_ `  ( ( M  /  2 )  +  ( 1  / 
4 ) ) ) )
12547, 124eqtrd 2145 . . . . . 6  |-  ( ( -.  2  ||  M  /\  M  e.  ZZ )  ->  if ( 2 
||  M ,  ( M  /  2 ) ,  ( ( M  -  1 )  / 
2 ) )  =  ( |_ `  (
( M  /  2
)  +  ( 1  /  4 ) ) ) )
126125expcom 115 . . . . 5  |-  ( M  e.  ZZ  ->  ( -.  2  ||  M  ->  if ( 2  ||  M ,  ( M  / 
2 ) ,  ( ( M  -  1 )  /  2 ) )  =  ( |_
`  ( ( M  /  2 )  +  ( 1  /  4
) ) ) ) )
127 zeo3 11407 . . . . 5  |-  ( M  e.  ZZ  ->  (
2  ||  M  \/  -.  2  ||  M ) )
12845, 126, 127mpjaod 690 . . . 4  |-  ( M  e.  ZZ  ->  if ( 2  ||  M ,  ( M  / 
2 ) ,  ( ( M  -  1 )  /  2 ) )  =  ( |_
`  ( ( M  /  2 )  +  ( 1  /  4
) ) ) )
129128eqcomd 2118 . . 3  |-  ( M  e.  ZZ  ->  ( |_ `  ( ( M  /  2 )  +  ( 1  /  4
) ) )  =  if ( 2  ||  M ,  ( M  /  2 ) ,  ( ( M  - 
1 )  /  2
) ) )
130129adantr 272 . 2  |-  ( ( M  e.  ZZ  /\  N  =  ( (
2  x.  M )  +  1 ) )  ->  ( |_ `  ( ( M  / 
2 )  +  ( 1  /  4 ) ) )  =  if ( 2  ||  M ,  ( M  / 
2 ) ,  ( ( M  -  1 )  /  2 ) ) )
13122, 130eqtrd 2145 1  |-  ( ( M  e.  ZZ  /\  N  =  ( (
2  x.  M )  +  1 ) )  ->  ( |_ `  ( N  /  4
) )  =  if ( 2  ||  M ,  ( M  / 
2 ) ,  ( ( M  -  1 )  /  2 ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 103    <-> wb 104    = wceq 1312    e. wcel 1461   E.wrex 2389   ifcif 3438   class class class wbr 3893   ` cfv 5079  (class class class)co 5726   CCcc 7539   RRcr 7540   0cc0 7541   1c1 7542    + caddc 7544    x. cmul 7546    < clt 7718    <_ cle 7719    - cmin 7850   # cap 8255    / cdiv 8339   NNcn 8624   2c2 8675   3c3 8676   4c4 8677   ZZcz 8952   QQcq 9307   RR+crp 9337   |_cfl 9928    || cdvds 11335
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-13 1472  ax-14 1473  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-sep 4004  ax-pow 4056  ax-pr 4089  ax-un 4313  ax-setind 4410  ax-cnex 7630  ax-resscn 7631  ax-1cn 7632  ax-1re 7633  ax-icn 7634  ax-addcl 7635  ax-addrcl 7636  ax-mulcl 7637  ax-mulrcl 7638  ax-addcom 7639  ax-mulcom 7640  ax-addass 7641  ax-mulass 7642  ax-distr 7643  ax-i2m1 7644  ax-0lt1 7645  ax-1rid 7646  ax-0id 7647  ax-rnegex 7648  ax-precex 7649  ax-cnre 7650  ax-pre-ltirr 7651  ax-pre-ltwlin 7652  ax-pre-lttrn 7653  ax-pre-apti 7654  ax-pre-ltadd 7655  ax-pre-mulgt0 7656  ax-pre-mulext 7657  ax-arch 7658
This theorem depends on definitions:  df-bi 116  df-3or 944  df-3an 945  df-tru 1315  df-fal 1318  df-xor 1335  df-nf 1418  df-sb 1717  df-eu 1976  df-mo 1977  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-ne 2281  df-nel 2376  df-ral 2393  df-rex 2394  df-reu 2395  df-rmo 2396  df-rab 2397  df-v 2657  df-sbc 2877  df-csb 2970  df-dif 3037  df-un 3039  df-in 3041  df-ss 3048  df-if 3439  df-pw 3476  df-sn 3497  df-pr 3498  df-op 3500  df-uni 3701  df-int 3736  df-iun 3779  df-br 3894  df-opab 3948  df-mpt 3949  df-id 4173  df-po 4176  df-iso 4177  df-xp 4503  df-rel 4504  df-cnv 4505  df-co 4506  df-dm 4507  df-rn 4508  df-res 4509  df-ima 4510  df-iota 5044  df-fun 5081  df-fn 5082  df-f 5083  df-fv 5087  df-riota 5682  df-ov 5729  df-oprab 5730  df-mpo 5731  df-1st 5990  df-2nd 5991  df-pnf 7720  df-mnf 7721  df-xr 7722  df-ltxr 7723  df-le 7724  df-sub 7852  df-neg 7853  df-reap 8249  df-ap 8256  df-div 8340  df-inn 8625  df-2 8683  df-3 8684  df-4 8685  df-n0 8876  df-z 8953  df-q 9308  df-rp 9338  df-fl 9930  df-dvds 11336
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator