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

Theorem flodddiv4t2lthalf 10544
 Description: The floor of an odd number divided by 4, multiplied by 2 is less than the half of the odd number. (Contributed by AV, 4-Jul-2021.)
Assertion
Ref Expression
flodddiv4t2lthalf

Proof of Theorem flodddiv4t2lthalf
StepHypRef Expression
1 flodddiv4lt 10543 . . 3
2 4nn 8314 . . . . . . . 8
3 znq 8842 . . . . . . . 8
42, 3mpan2 416 . . . . . . 7
54flqcld 9411 . . . . . 6
65zred 8602 . . . . 5
76adantr 270 . . . 4
8 qre 8843 . . . . . 6
94, 8syl 14 . . . . 5
109adantr 270 . . . 4
11 2re 8228 . . . . . 6
12 2pos 8249 . . . . . 6
1311, 12pm3.2i 266 . . . . 5
1413a1i 9 . . . 4
15 ltmul1 7811 . . . 4
167, 10, 14, 15syl3anc 1170 . . 3
171, 16mpbid 145 . 2
18 zcn 8489 . . . . . 6
1918halfcld 8394 . . . . 5
20 2cnd 8231 . . . . 5
21 2ap0 8251 . . . . . 6 #
2221a1i 9 . . . . 5 #
2319, 20, 22divcanap1d 7997 . . . 4
2418, 20, 20, 22, 22divdivap1d 8027 . . . . . 6
25 2t2e4 8305 . . . . . . . 8
2625a1i 9 . . . . . . 7
2726oveq2d 5579 . . . . . 6
2824, 27eqtrd 2115 . . . . 5
2928oveq1d 5578 . . . 4
3023, 29eqtr3d 2117 . . 3