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

Theorem div4p1lem1div2 8177
 Description: An integer greater than 5, divided by 4 and increased by 1, is less than or equal to the half of the integer minus 1. (Contributed by AV, 8-Jul-2021.)
Assertion
Ref Expression
div4p1lem1div2

Proof of Theorem div4p1lem1div2
StepHypRef Expression
1 6re 7996 . . . . . . 7
21a1i 9 . . . . . 6
3 id 19 . . . . . 6
42, 3, 3leadd2d 7531 . . . . 5
54biimpa 280 . . . 4
6 recn 7014 . . . . . 6
76times2d 8168 . . . . 5
87adantr 261 . . . 4
95, 8breqtrrd 3790 . . 3
10 4cn 7993 . . . . . . . 8
1110a1i 9 . . . . . . 7
12 2cn 7986 . . . . . . . 8
1312a1i 9 . . . . . . 7
146, 11, 13addassd 7049 . . . . . 6
15 4p2e6 8054 . . . . . . 7
1615oveq2i 5523 . . . . . 6
1714, 16syl6eq 2088 . . . . 5
1817breq1d 3774 . . . 4
209, 19mpbird 156 . 2
21 4re 7992 . . . . . . . 8
2221a1i 9 . . . . . . 7
23 4ap0 8015 . . . . . . . 8 #
2423a1i 9 . . . . . . 7 #
253, 22, 24redivclapd 7808 . . . . . 6
26 peano2re 7149 . . . . . 6
2725, 26syl 14 . . . . 5
28 peano2rem 7278 . . . . . 6
2928rehalfcld 8171 . . . . 5
30 4pos 8013 . . . . . . 7
3121, 30pm3.2i 257 . . . . . 6
3231a1i 9 . . . . 5
33 lemul1 7584 . . . . 5
3427, 29, 32, 33syl3anc 1135 . . . 4
3525recnd 7054 . . . . . 6
36 1cnd 7043 . . . . . 6
376, 11, 24divcanap1d 7766 . . . . . . 7
3810mulid2i 7030 . . . . . . . 8
3938a1i 9 . . . . . . 7
4037, 39oveq12d 5530 . . . . . 6
4135, 11, 36, 40joinlmuladdmuld 7053 . . . . 5
42 2t2e4 8069 . . . . . . . . 9
4342eqcomi 2044 . . . . . . . 8
4443a1i 9 . . . . . . 7
4544oveq2d 5528 . . . . . 6
4629recnd 7054 . . . . . . 7
47 mulass 7012 . . . . . . . 8
4847eqcomd 2045 . . . . . . 7
4946, 13, 13, 48syl3anc 1135 . . . . . 6
5028recnd 7054 . . . . . . . . 9
51 2ap0 8009 . . . . . . . . . 10 #
5251a1i 9 . . . . . . . . 9 #
5350, 13, 52divcanap1d 7766 . . . . . . . 8
5453oveq1d 5527 . . . . . . 7
556, 36, 13subdird 7412 . . . . . . 7
5612mulid2i 7030 . . . . . . . . 9
5756a1i 9 . . . . . . . 8
5857oveq2d 5528 . . . . . . 7
5954, 55, 583eqtrd 2076 . . . . . 6
6045, 49, 593eqtrd 2076 . . . . 5
6141, 60breq12d 3777 . . . 4
623, 22readdcld 7055 . . . . 5
63 2re 7985 . . . . . 6
6463a1i 9 . . . . 5
653, 64remulcld 7056 . . . . 5
66 leaddsub 7433 . . . . . 6
6766bicomd 129 . . . . 5
6862, 64, 65, 67syl3anc 1135 . . . 4
6934, 61, 683bitrd 203 . . 3