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

Theorem oddpwdc 12028
 Description: The function that decomposes a number into its "odd" and "even" parts, which is to say the largest power of two and largest odd divisor of a number, is a bijection from pairs of a nonnegative integer and an odd number to positive integers. (Contributed by Thierry Arnoux, 15-Aug-2017.)
Hypotheses
Ref Expression
oddpwdc.j
oddpwdc.f
Assertion
Ref Expression
oddpwdc
Distinct variable groups:   ,,   ,,
Allowed substitution hints:   (,,)   ()

Proof of Theorem oddpwdc
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 oddpwdc.f . . 3
2 2cnd 8889 . . . . . 6
3 simpr 109 . . . . . 6
42, 3expcld 10533 . . . . 5
5 breq2 3969 . . . . . . . . . 10
65notbid 657 . . . . . . . . 9
7 oddpwdc.j . . . . . . . . 9
86, 7elrab2 2871 . . . . . . . 8
98simplbi 272 . . . . . . 7
109adantr 274 . . . . . 6
1110nncnd 8830 . . . . 5
124, 11mulcld 7881 . . . 4
14 nnnn0 9080 . . . . . 6
15 2nn 8977 . . . . . . 7
16 pw2dvdseu 12022 . . . . . . . 8
17 riotacl 5788 . . . . . . . 8
1816, 17syl 14 . . . . . . 7
19 nnexpcl 10414 . . . . . . 7
2015, 18, 19sylancr 411 . . . . . 6
21 nn0nndivcl 9135 . . . . . 6
2214, 20, 21syl2anc 409 . . . . 5
2322, 18jca 304 . . . 4