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

Theorem pw2dvdslemn 11899
 Description: Lemma for pw2dvds 11900. If a natural number has some power of two which does not divide it, there is a highest power of two which does divide it. (Contributed by Jim Kingdon, 14-Nov-2021.)
Assertion
Ref Expression
pw2dvdslemn
Distinct variable group:   ,
Allowed substitution hint:   ()

Proof of Theorem pw2dvdslemn
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 3simpb 980 . 2
2 oveq2 5791 . . . . . . . 8
32breq1d 3948 . . . . . . 7
43notbid 657 . . . . . 6
54anbi2d 460 . . . . 5
65imbi1d 230 . . . 4
7 oveq2 5791 . . . . . . . 8
87breq1d 3948 . . . . . . 7
98notbid 657 . . . . . 6
109anbi2d 460 . . . . 5
1110imbi1d 230 . . . 4
12 oveq2 5791 . . . . . . . 8
1312breq1d 3948 . . . . . . 7
1413notbid 657 . . . . . 6
1514anbi2d 460 . . . . 5
1615imbi1d 230 . . . 4
17 oveq2 5791 . . . . . . . 8
1817breq1d 3948 . . . . . . 7
1918notbid 657 . . . . . 6
2019anbi2d 460 . . . . 5
2120imbi1d 230 . . . 4
22 0nn0 9036 . . . . . 6
2322a1i 9 . . . . 5
24 oveq2 5791 . . . . . . . 8
2524breq1d 3948 . . . . . . 7
26 oveq1 5790 . . . . . . . . . 10
2726oveq2d 5799 . . . . . . . . 9
2827breq1d 3948 . . . . . . . 8
2928notbid 657 . . . . . . 7
3025, 29anbi12d 465 . . . . . 6
3130adantl 275 . . . . 5
32 2cnd 8837 . . . . . . . 8
3332exp0d 10469 . . . . . . 7
34 simpl 108 . . . . . . . . 9
3534nnzd 9216 . . . . . . . 8
36 1dvds 11563 . . . . . . . 8
3735, 36syl 14 . . . . . . 7
3833, 37eqbrtrd 3959 . . . . . 6
39 simpr 109 . . . . . . 7
40 0p1e1 8878 . . . . . . . . 9
4140oveq2i 5794 . . . . . . . 8
4241breq1i 3945 . . . . . . 7
4339, 42sylnibr 667 . . . . . 6
4438, 43jca 304 . . . . 5
4523, 31, 44rspcedvd 2800 . . . 4
46 simpll 519 . . . . . . . . 9
4746nnnn0d 9074 . . . . . . . 8
48 oveq2 5791 . . . . . . . . . . 11
4948breq1d 3948 . . . . . . . . . 10
50 oveq1 5790 . . . . . . . . . . . . 13
5150oveq2d 5799 . . . . . . . . . . . 12
5251breq1d 3948 . . . . . . . . . . 11
5352notbid 657 . . . . . . . . . 10
5449, 53anbi12d 465 . . . . . . . . 9
5554adantl 275 . . . . . . . 8
56 simpr 109 . . . . . . . . 9
57 simplrr 526 . . . . . . . . 9
5856, 57jca 304 . . . . . . . 8
5947, 55, 58rspcedvd 2800 . . . . . . 7
6059adantllr 473 . . . . . 6
61 simprl 521 . . . . . . . 8
6261anim1i 338 . . . . . . 7
63 simpllr 524 . . . . . . 7
6462, 63mpd 13 . . . . . 6
65 2nn 8925 . . . . . . . . 9
66 simpll 519 . . . . . . . . . 10
6766nnnn0d 9074 . . . . . . . . 9
68 nnexpcl 10357 . . . . . . . . 9
6965, 67, 68sylancr 411 . . . . . . . 8
7061nnzd 9216 . . . . . . . 8
71 dvdsdc 11557 . . . . . . . 8 DECID
7269, 70, 71syl2anc 409 . . . . . . 7 DECID
73 exmiddc 822 . . . . . . 7 DECID
7472, 73syl 14 . . . . . 6
7560, 64, 74mpjaodan 788 . . . . 5
7675exp31 362 . . . 4
776, 11, 16, 21, 45, 76nnind 8780 . . 3