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	|- ( ( N e. RR /\ 6 <_ N ) -> ( ( N / 4 ) + 1 ) <_ ( ( N - 1 ) / 2 ) )

Proof of Theorem div4p1lem1div2

Step	Hyp	Ref	Expression
1		6re 7996	. . . . . . 7 |- 6 e. RR
2	1	a1i 9	. . . . . 6 |- ( N e. RR -> 6 e. RR )
3		id 19	. . . . . 6 |- ( N e. RR -> N e. RR )
4	2, 3, 3	leadd2d 7531	. . . . 5 |- ( N e. RR -> ( 6 <_ N <-> ( N + 6 ) <_ ( N + N ) ) )
5	4	biimpa 280	. . . 4 |- ( ( N e. RR /\ 6 <_ N ) -> ( N + 6 ) <_ ( N + N ) )
6		recn 7014	. . . . . 6 |- ( N e. RR -> N e. CC )
7	6	times2d 8168	. . . . 5 |- ( N e. RR -> ( N x. 2 ) = ( N + N ) )
8	7	adantr 261	. . . 4 |- ( ( N e. RR /\ 6 <_ N ) -> ( N x. 2 ) = ( N + N ) )
9	5, 8	breqtrrd 3790	. . 3 |- ( ( N e. RR /\ 6 <_ N ) -> ( N + 6 ) <_ ( N x. 2 ) )
10		4cn 7993	. . . . . . . 8 |- 4 e. CC
11	10	a1i 9	. . . . . . 7 |- ( N e. RR -> 4 e. CC )
12		2cn 7986	. . . . . . . 8 |- 2 e. CC
13	12	a1i 9	. . . . . . 7 |- ( N e. RR -> 2 e. CC )
14	6, 11, 13	addassd 7049	. . . . . 6 |- ( N e. RR -> ( ( N + 4 ) + 2 ) = ( N + ( 4 + 2 ) ) )
15		4p2e6 8054	. . . . . . 7 |- ( 4 + 2 ) = 6
16	15	oveq2i 5523	. . . . . 6 |- ( N + ( 4 + 2 ) ) = ( N + 6 )
17	14, 16	syl6eq 2088	. . . . 5 |- ( N e. RR -> ( ( N + 4 ) + 2 ) = ( N + 6 ) )
18	17	breq1d 3774	. . . 4 |- ( N e. RR -> ( ( ( N + 4 ) + 2 ) <_ ( N x. 2 ) <-> ( N + 6 ) <_ ( N x. 2 ) ) )
19	18	adantr 261	. . 3 |- ( ( N e. RR /\ 6 <_ N ) -> ( ( ( N + 4 ) + 2 ) <_ ( N x. 2 ) <-> ( N + 6 ) <_ ( N x. 2 ) ) )
20	9, 19	mpbird 156	. 2 |- ( ( N e. RR /\ 6 <_ N ) -> ( ( N + 4 ) + 2 ) <_ ( N x. 2 ) )
21		4re 7992	. . . . . . . 8 |- 4 e. RR
22	21	a1i 9	. . . . . . 7 |- ( N e. RR -> 4 e. RR )
23		4ap0 8015	. . . . . . . 8 |- 4 # 0
24	23	a1i 9	. . . . . . 7 |- ( N e. RR -> 4 # 0 )
25	3, 22, 24	redivclapd 7808	. . . . . 6 |- ( N e. RR -> ( N / 4 ) e. RR )
26		peano2re 7149	. . . . . 6 |- ( ( N / 4 ) e. RR -> ( ( N / 4 ) + 1 ) e. RR )
27	25, 26	syl 14	. . . . 5 |- ( N e. RR -> ( ( N / 4 ) + 1 ) e. RR )
28		peano2rem 7278	. . . . . 6 |- ( N e. RR -> ( N - 1 ) e. RR )
29	28	rehalfcld 8171	. . . . 5 |- ( N e. RR -> ( ( N - 1 ) / 2 ) e. RR )
30		4pos 8013	. . . . . . 7 |- 0 < 4
31	21, 30	pm3.2i 257	. . . . . 6 |- ( 4 e. RR /\ 0 < 4 )
32	31	a1i 9	. . . . 5 |- ( N e. RR -> ( 4 e. RR /\ 0 < 4 ) )
33		lemul1 7584	. . . . 5 |- ( ( ( ( N / 4 ) + 1 ) e. RR /\ ( ( N - 1 ) / 2 ) e. RR /\ ( 4 e. RR /\ 0 < 4 ) ) -> ( ( ( N / 4 ) + 1 ) <_ ( ( N - 1 ) / 2 ) <-> ( ( ( N / 4 ) + 1 ) x. 4 ) <_ ( ( ( N - 1 ) / 2 ) x. 4 ) ) )
34	27, 29, 32, 33	syl3anc 1135	. . . 4 |- ( N e. RR -> ( ( ( N / 4 ) + 1 ) <_ ( ( N - 1 ) / 2 ) <-> ( ( ( N / 4 ) + 1 ) x. 4 ) <_ ( ( ( N - 1 ) / 2 ) x. 4 ) ) )
35	25	recnd 7054	. . . . . 6 |- ( N e. RR -> ( N / 4 ) e. CC )
36		1cnd 7043	. . . . . 6 |- ( N e. RR -> 1 e. CC )
37	6, 11, 24	divcanap1d 7766	. . . . . . 7 |- ( N e. RR -> ( ( N / 4 ) x. 4 ) = N )
38	10	mulid2i 7030	. . . . . . . 8 |- ( 1 x. 4 ) = 4
39	38	a1i 9	. . . . . . 7 |- ( N e. RR -> ( 1 x. 4 ) = 4 )
40	37, 39	oveq12d 5530	. . . . . 6 |- ( N e. RR -> ( ( ( N / 4 ) x. 4 ) + ( 1 x. 4 ) ) = ( N + 4 ) )
41	35, 11, 36, 40	joinlmuladdmuld 7053	. . . . 5 |- ( N e. RR -> ( ( ( N / 4 ) + 1 ) x. 4 ) = ( N + 4 ) )
42		2t2e4 8069	. . . . . . . . 9 |- ( 2 x. 2 ) = 4
43	42	eqcomi 2044	. . . . . . . 8 |- 4 = ( 2 x. 2 )
44	43	a1i 9	. . . . . . 7 |- ( N e. RR -> 4 = ( 2 x. 2 ) )
45	44	oveq2d 5528	. . . . . 6 |- ( N e. RR -> ( ( ( N - 1 ) / 2 ) x. 4 ) = ( ( ( N - 1 ) / 2 ) x. ( 2 x. 2 ) ) )
46	29	recnd 7054	. . . . . . 7 |- ( N e. RR -> ( ( N - 1 ) / 2 ) e. CC )
47		mulass 7012	. . . . . . . 8 |- ( ( ( ( N - 1 ) / 2 ) e. CC /\ 2 e. CC /\ 2 e. CC ) -> ( ( ( ( N - 1 ) / 2 ) x. 2 ) x. 2 ) = ( ( ( N - 1 ) / 2 ) x. ( 2 x. 2 ) ) )
48	47	eqcomd 2045	. . . . . . 7 |- ( ( ( ( N - 1 ) / 2 ) e. CC /\ 2 e. CC /\ 2 e. CC ) -> ( ( ( N - 1 ) / 2 ) x. ( 2 x. 2 ) ) = ( ( ( ( N - 1 ) / 2 ) x. 2 ) x. 2 ) )
49	46, 13, 13, 48	syl3anc 1135	. . . . . 6 |- ( N e. RR -> ( ( ( N - 1 ) / 2 ) x. ( 2 x. 2 ) ) = ( ( ( ( N - 1 ) / 2 ) x. 2 ) x. 2 ) )
50	28	recnd 7054	. . . . . . . . 9 |- ( N e. RR -> ( N - 1 ) e. CC )
51		2ap0 8009	. . . . . . . . . 10 |- 2 # 0
52	51	a1i 9	. . . . . . . . 9 |- ( N e. RR -> 2 # 0 )
53	50, 13, 52	divcanap1d 7766	. . . . . . . 8 |- ( N e. RR -> ( ( ( N - 1 ) / 2 ) x. 2 ) = ( N - 1 ) )
54	53	oveq1d 5527	. . . . . . 7 |- ( N e. RR -> ( ( ( ( N - 1 ) / 2 ) x. 2 ) x. 2 ) = ( ( N - 1 ) x. 2 ) )
55	6, 36, 13	subdird 7412	. . . . . . 7 |- ( N e. RR -> ( ( N - 1 ) x. 2 ) = ( ( N x. 2 ) - ( 1 x. 2 ) ) )
56	12	mulid2i 7030	. . . . . . . . 9 |- ( 1 x. 2 ) = 2
57	56	a1i 9	. . . . . . . 8 |- ( N e. RR -> ( 1 x. 2 ) = 2 )
58	57	oveq2d 5528	. . . . . . 7 |- ( N e. RR -> ( ( N x. 2 ) - ( 1 x. 2 ) ) = ( ( N x. 2 ) - 2 ) )
59	54, 55, 58	3eqtrd 2076	. . . . . 6 |- ( N e. RR -> ( ( ( ( N - 1 ) / 2 ) x. 2 ) x. 2 ) = ( ( N x. 2 ) - 2 ) )
60	45, 49, 59	3eqtrd 2076	. . . . 5 |- ( N e. RR -> ( ( ( N - 1 ) / 2 ) x. 4 ) = ( ( N x. 2 ) - 2 ) )
61	41, 60	breq12d 3777	. . . 4 |- ( N e. RR -> ( ( ( ( N / 4 ) + 1 ) x. 4 ) <_ ( ( ( N - 1 ) / 2 ) x. 4 ) <-> ( N + 4 ) <_ ( ( N x. 2 ) - 2 ) ) )
62	3, 22	readdcld 7055	. . . . 5 |- ( N e. RR -> ( N + 4 ) e. RR )
63		2re 7985	. . . . . 6 |- 2 e. RR
64	63	a1i 9	. . . . 5 |- ( N e. RR -> 2 e. RR )
65	3, 64	remulcld 7056	. . . . 5 |- ( N e. RR -> ( N x. 2 ) e. RR )
66		leaddsub 7433	. . . . . 6 |- ( ( ( N + 4 ) e. RR /\ 2 e. RR /\ ( N x. 2 ) e. RR ) -> ( ( ( N + 4 ) + 2 ) <_ ( N x. 2 ) <-> ( N + 4 ) <_ ( ( N x. 2 ) - 2 ) ) )
67	66	bicomd 129	. . . . 5 |- ( ( ( N + 4 ) e. RR /\ 2 e. RR /\ ( N x. 2 ) e. RR ) -> ( ( N + 4 ) <_ ( ( N x. 2 ) - 2 ) <-> ( ( N + 4 ) + 2 ) <_ ( N x. 2 ) ) )
68	62, 64, 65, 67	syl3anc 1135	. . . 4 |- ( N e. RR -> ( ( N + 4 ) <_ ( ( N x. 2 ) - 2 ) <-> ( ( N + 4 ) + 2 ) <_ ( N x. 2 ) ) )
69	34, 61, 68	3bitrd 203	. . 3 |- ( N e. RR -> ( ( ( N / 4 ) + 1 ) <_ ( ( N - 1 ) / 2 ) <-> ( ( N + 4 ) + 2 ) <_ ( N x. 2 ) ) )
70	69	adantr 261	. 2 |- ( ( N e. RR /\ 6 <_ N ) -> ( ( ( N / 4 ) + 1 ) <_ ( ( N - 1 ) / 2 ) <-> ( ( N + 4 ) + 2 ) <_ ( N x. 2 ) ) )
71	20, 70	mpbird 156	1 |- ( ( N e. RR /\ 6 <_ N ) -> ( ( N / 4 ) + 1 ) <_ ( ( N - 1 ) / 2 ) )

Syntax hints:   -> wi 4   /\ wa 97   <-> wb 98   /\ w3a 885   = wceq 1243   e. wcel 1393   class class class wbr 3764  (class class class)co 5512   CCcc 6887   RRcr 6888   0cc0 6889   1c1 6890   + caddc 6892   x. cmul 6894   < clt 7060   <_ cle 7061   - cmin 7182   # cap 7572   / cdiv 7651   2c2 7964   4c4 7966   6c6 7968

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-13 1404  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-coll 3872  ax-sep 3875  ax-nul 3883  ax-pow 3927  ax-pr 3944  ax-un 4170  ax-setind 4262  ax-iinf 4311  ax-cnex 6975  ax-resscn 6976  ax-1cn 6977  ax-1re 6978  ax-icn 6979  ax-addcl 6980  ax-addrcl 6981  ax-mulcl 6982  ax-mulrcl 6983  ax-addcom 6984  ax-mulcom 6985  ax-addass 6986  ax-mulass 6987  ax-distr 6988  ax-i2m1 6989  ax-1rid 6991  ax-0id 6992  ax-rnegex 6993  ax-precex 6994  ax-cnre 6995  ax-pre-ltirr 6996  ax-pre-ltwlin 6997  ax-pre-lttrn 6998  ax-pre-apti 6999  ax-pre-ltadd 7000  ax-pre-mulgt0 7001  ax-pre-mulext 7002

This theorem depends on definitions:  df-bi 110  df-dc 743  df-3or 886  df-3an 887  df-tru 1246  df-fal 1249  df-nf 1350  df-sb 1646  df-eu 1903  df-mo 1904  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ne 2206  df-nel 2207  df-ral 2311  df-rex 2312  df-reu 2313  df-rmo 2314  df-rab 2315  df-v 2559  df-sbc 2765  df-csb 2853  df-dif 2920  df-un 2922  df-in 2924  df-ss 2931  df-nul 3225  df-pw 3361  df-sn 3381  df-pr 3382  df-op 3384  df-uni 3581  df-int 3616  df-iun 3659  df-br 3765  df-opab 3819  df-mpt 3820  df-tr 3855  df-eprel 4026  df-id 4030  df-po 4033  df-iso 4034  df-iord 4103  df-on 4105  df-suc 4108  df-iom 4314  df-xp 4351  df-rel 4352  df-cnv 4353  df-co 4354  df-dm 4355  df-rn 4356  df-res 4357  df-ima 4358  df-iota 4867  df-fun 4904  df-fn 4905  df-f 4906  df-f1 4907  df-fo 4908  df-f1o 4909  df-fv 4910  df-riota 5468  df-ov 5515  df-oprab 5516  df-mpt2 5517  df-1st 5767  df-2nd 5768  df-recs 5920  df-irdg 5957  df-1o 6001  df-2o 6002  df-oadd 6005  df-omul 6006  df-er 6106  df-ec 6108  df-qs 6112  df-ni 6402  df-pli 6403  df-mi 6404  df-lti 6405  df-plpq 6442  df-mpq 6443  df-enq 6445  df-nqqs 6446  df-plqqs 6447  df-mqqs 6448  df-1nqqs 6449  df-rq 6450  df-ltnqqs 6451  df-enq0 6522  df-nq0 6523  df-0nq0 6524  df-plq0 6525  df-mq0 6526  df-inp 6564  df-i1p 6565  df-iplp 6566  df-iltp 6568  df-enr 6811  df-nr 6812  df-ltr 6815  df-0r 6816  df-1r 6817  df-0 6896  df-1 6897  df-r 6899  df-lt 6902  df-pnf 7062  df-mnf 7063  df-xr 7064  df-ltxr 7065  df-le 7066  df-sub 7184  df-neg 7185  df-reap 7566  df-ap 7573  df-div 7652  df-2 7973  df-3 7974  df-4 7975  df-5 7976  df-6 7977

This theorem is referenced by:  fldiv4p1lem1div2  9147