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

Theorem div4p1lem1div2 8980
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 ((𝑁 ∈ ℝ ∧ 6 ≤ 𝑁) → ((𝑁 / 4) + 1) ≤ ((𝑁 − 1) / 2))

Proof of Theorem div4p1lem1div2
StepHypRef Expression
1 6re 8808 . . . . . . 7 6 ∈ ℝ
21a1i 9 . . . . . 6 (𝑁 ∈ ℝ → 6 ∈ ℝ)
3 id 19 . . . . . 6 (𝑁 ∈ ℝ → 𝑁 ∈ ℝ)
42, 3, 3leadd2d 8309 . . . . 5 (𝑁 ∈ ℝ → (6 ≤ 𝑁 ↔ (𝑁 + 6) ≤ (𝑁 + 𝑁)))
54biimpa 294 . . . 4 ((𝑁 ∈ ℝ ∧ 6 ≤ 𝑁) → (𝑁 + 6) ≤ (𝑁 + 𝑁))
6 recn 7760 . . . . . 6 (𝑁 ∈ ℝ → 𝑁 ∈ ℂ)
76times2d 8970 . . . . 5 (𝑁 ∈ ℝ → (𝑁 · 2) = (𝑁 + 𝑁))
87adantr 274 . . . 4 ((𝑁 ∈ ℝ ∧ 6 ≤ 𝑁) → (𝑁 · 2) = (𝑁 + 𝑁))
95, 8breqtrrd 3956 . . 3 ((𝑁 ∈ ℝ ∧ 6 ≤ 𝑁) → (𝑁 + 6) ≤ (𝑁 · 2))
10 4cn 8805 . . . . . . . 8 4 ∈ ℂ
1110a1i 9 . . . . . . 7 (𝑁 ∈ ℝ → 4 ∈ ℂ)
12 2cn 8798 . . . . . . . 8 2 ∈ ℂ
1312a1i 9 . . . . . . 7 (𝑁 ∈ ℝ → 2 ∈ ℂ)
146, 11, 13addassd 7795 . . . . . 6 (𝑁 ∈ ℝ → ((𝑁 + 4) + 2) = (𝑁 + (4 + 2)))
15 4p2e6 8870 . . . . . . 7 (4 + 2) = 6
1615oveq2i 5785 . . . . . 6 (𝑁 + (4 + 2)) = (𝑁 + 6)
1714, 16syl6eq 2188 . . . . 5 (𝑁 ∈ ℝ → ((𝑁 + 4) + 2) = (𝑁 + 6))
1817breq1d 3939 . . . 4 (𝑁 ∈ ℝ → (((𝑁 + 4) + 2) ≤ (𝑁 · 2) ↔ (𝑁 + 6) ≤ (𝑁 · 2)))
1918adantr 274 . . 3 ((𝑁 ∈ ℝ ∧ 6 ≤ 𝑁) → (((𝑁 + 4) + 2) ≤ (𝑁 · 2) ↔ (𝑁 + 6) ≤ (𝑁 · 2)))
209, 19mpbird 166 . 2 ((𝑁 ∈ ℝ ∧ 6 ≤ 𝑁) → ((𝑁 + 4) + 2) ≤ (𝑁 · 2))
21 4re 8804 . . . . . . . 8 4 ∈ ℝ
2221a1i 9 . . . . . . 7 (𝑁 ∈ ℝ → 4 ∈ ℝ)
23 4ap0 8826 . . . . . . . 8 4 # 0
2423a1i 9 . . . . . . 7 (𝑁 ∈ ℝ → 4 # 0)
253, 22, 24redivclapd 8601 . . . . . 6 (𝑁 ∈ ℝ → (𝑁 / 4) ∈ ℝ)
26 peano2re 7905 . . . . . 6 ((𝑁 / 4) ∈ ℝ → ((𝑁 / 4) + 1) ∈ ℝ)
2725, 26syl 14 . . . . 5 (𝑁 ∈ ℝ → ((𝑁 / 4) + 1) ∈ ℝ)
28 peano2rem 8036 . . . . . 6 (𝑁 ∈ ℝ → (𝑁 − 1) ∈ ℝ)
2928rehalfcld 8973 . . . . 5 (𝑁 ∈ ℝ → ((𝑁 − 1) / 2) ∈ ℝ)
30 4pos 8824 . . . . . . 7 0 < 4
3121, 30pm3.2i 270 . . . . . 6 (4 ∈ ℝ ∧ 0 < 4)
3231a1i 9 . . . . 5 (𝑁 ∈ ℝ → (4 ∈ ℝ ∧ 0 < 4))
33 lemul1 8362 . . . . 5 ((((𝑁 / 4) + 1) ∈ ℝ ∧ ((𝑁 − 1) / 2) ∈ ℝ ∧ (4 ∈ ℝ ∧ 0 < 4)) → (((𝑁 / 4) + 1) ≤ ((𝑁 − 1) / 2) ↔ (((𝑁 / 4) + 1) · 4) ≤ (((𝑁 − 1) / 2) · 4)))
3427, 29, 32, 33syl3anc 1216 . . . 4 (𝑁 ∈ ℝ → (((𝑁 / 4) + 1) ≤ ((𝑁 − 1) / 2) ↔ (((𝑁 / 4) + 1) · 4) ≤ (((𝑁 − 1) / 2) · 4)))
3525recnd 7801 . . . . . 6 (𝑁 ∈ ℝ → (𝑁 / 4) ∈ ℂ)
36 1cnd 7789 . . . . . 6 (𝑁 ∈ ℝ → 1 ∈ ℂ)
376, 11, 24divcanap1d 8558 . . . . . . 7 (𝑁 ∈ ℝ → ((𝑁 / 4) · 4) = 𝑁)
3810mulid2i 7776 . . . . . . . 8 (1 · 4) = 4
3938a1i 9 . . . . . . 7 (𝑁 ∈ ℝ → (1 · 4) = 4)
4037, 39oveq12d 5792 . . . . . 6 (𝑁 ∈ ℝ → (((𝑁 / 4) · 4) + (1 · 4)) = (𝑁 + 4))
4135, 11, 36, 40joinlmuladdmuld 7800 . . . . 5 (𝑁 ∈ ℝ → (((𝑁 / 4) + 1) · 4) = (𝑁 + 4))
42 2t2e4 8881 . . . . . . . . 9 (2 · 2) = 4
4342eqcomi 2143 . . . . . . . 8 4 = (2 · 2)
4443a1i 9 . . . . . . 7 (𝑁 ∈ ℝ → 4 = (2 · 2))
4544oveq2d 5790 . . . . . 6 (𝑁 ∈ ℝ → (((𝑁 − 1) / 2) · 4) = (((𝑁 − 1) / 2) · (2 · 2)))
4629recnd 7801 . . . . . . 7 (𝑁 ∈ ℝ → ((𝑁 − 1) / 2) ∈ ℂ)
47 mulass 7758 . . . . . . . 8 ((((𝑁 − 1) / 2) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ∈ ℂ) → ((((𝑁 − 1) / 2) · 2) · 2) = (((𝑁 − 1) / 2) · (2 · 2)))
4847eqcomd 2145 . . . . . . 7 ((((𝑁 − 1) / 2) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ∈ ℂ) → (((𝑁 − 1) / 2) · (2 · 2)) = ((((𝑁 − 1) / 2) · 2) · 2))
4946, 13, 13, 48syl3anc 1216 . . . . . 6 (𝑁 ∈ ℝ → (((𝑁 − 1) / 2) · (2 · 2)) = ((((𝑁 − 1) / 2) · 2) · 2))
5028recnd 7801 . . . . . . . . 9 (𝑁 ∈ ℝ → (𝑁 − 1) ∈ ℂ)
51 2ap0 8820 . . . . . . . . . 10 2 # 0
5251a1i 9 . . . . . . . . 9 (𝑁 ∈ ℝ → 2 # 0)
5350, 13, 52divcanap1d 8558 . . . . . . . 8 (𝑁 ∈ ℝ → (((𝑁 − 1) / 2) · 2) = (𝑁 − 1))
5453oveq1d 5789 . . . . . . 7 (𝑁 ∈ ℝ → ((((𝑁 − 1) / 2) · 2) · 2) = ((𝑁 − 1) · 2))
556, 36, 13subdird 8184 . . . . . . 7 (𝑁 ∈ ℝ → ((𝑁 − 1) · 2) = ((𝑁 · 2) − (1 · 2)))
5612mulid2i 7776 . . . . . . . . 9 (1 · 2) = 2
5756a1i 9 . . . . . . . 8 (𝑁 ∈ ℝ → (1 · 2) = 2)
5857oveq2d 5790 . . . . . . 7 (𝑁 ∈ ℝ → ((𝑁 · 2) − (1 · 2)) = ((𝑁 · 2) − 2))
5954, 55, 583eqtrd 2176 . . . . . 6 (𝑁 ∈ ℝ → ((((𝑁 − 1) / 2) · 2) · 2) = ((𝑁 · 2) − 2))
6045, 49, 593eqtrd 2176 . . . . 5 (𝑁 ∈ ℝ → (((𝑁 − 1) / 2) · 4) = ((𝑁 · 2) − 2))
6141, 60breq12d 3942 . . . 4 (𝑁 ∈ ℝ → ((((𝑁 / 4) + 1) · 4) ≤ (((𝑁 − 1) / 2) · 4) ↔ (𝑁 + 4) ≤ ((𝑁 · 2) − 2)))
623, 22readdcld 7802 . . . . 5 (𝑁 ∈ ℝ → (𝑁 + 4) ∈ ℝ)
63 2re 8797 . . . . . 6 2 ∈ ℝ
6463a1i 9 . . . . 5 (𝑁 ∈ ℝ → 2 ∈ ℝ)
653, 64remulcld 7803 . . . . 5 (𝑁 ∈ ℝ → (𝑁 · 2) ∈ ℝ)
66 leaddsub 8207 . . . . . 6 (((𝑁 + 4) ∈ ℝ ∧ 2 ∈ ℝ ∧ (𝑁 · 2) ∈ ℝ) → (((𝑁 + 4) + 2) ≤ (𝑁 · 2) ↔ (𝑁 + 4) ≤ ((𝑁 · 2) − 2)))
6766bicomd 140 . . . . 5 (((𝑁 + 4) ∈ ℝ ∧ 2 ∈ ℝ ∧ (𝑁 · 2) ∈ ℝ) → ((𝑁 + 4) ≤ ((𝑁 · 2) − 2) ↔ ((𝑁 + 4) + 2) ≤ (𝑁 · 2)))
6862, 64, 65, 67syl3anc 1216 . . . 4 (𝑁 ∈ ℝ → ((𝑁 + 4) ≤ ((𝑁 · 2) − 2) ↔ ((𝑁 + 4) + 2) ≤ (𝑁 · 2)))
6934, 61, 683bitrd 213 . . 3 (𝑁 ∈ ℝ → (((𝑁 / 4) + 1) ≤ ((𝑁 − 1) / 2) ↔ ((𝑁 + 4) + 2) ≤ (𝑁 · 2)))
7069adantr 274 . 2 ((𝑁 ∈ ℝ ∧ 6 ≤ 𝑁) → (((𝑁 / 4) + 1) ≤ ((𝑁 − 1) / 2) ↔ ((𝑁 + 4) + 2) ≤ (𝑁 · 2)))
7120, 70mpbird 166 1 ((𝑁 ∈ ℝ ∧ 6 ≤ 𝑁) → ((𝑁 / 4) + 1) ≤ ((𝑁 − 1) / 2))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  w3a 962   = wceq 1331  wcel 1480   class class class wbr 3929  (class class class)co 5774  cc 7625  cr 7626  0cc0 7627  1c1 7628   + caddc 7630   · cmul 7632   < clt 7807  cle 7808  cmin 7940   # cap 8350   / cdiv 8439  2c2 8778  4c4 8780  6c6 8782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-sep 4046  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-setind 4452  ax-cnex 7718  ax-resscn 7719  ax-1cn 7720  ax-1re 7721  ax-icn 7722  ax-addcl 7723  ax-addrcl 7724  ax-mulcl 7725  ax-mulrcl 7726  ax-addcom 7727  ax-mulcom 7728  ax-addass 7729  ax-mulass 7730  ax-distr 7731  ax-i2m1 7732  ax-0lt1 7733  ax-1rid 7734  ax-0id 7735  ax-rnegex 7736  ax-precex 7737  ax-cnre 7738  ax-pre-ltirr 7739  ax-pre-ltwlin 7740  ax-pre-lttrn 7741  ax-pre-apti 7742  ax-pre-ltadd 7743  ax-pre-mulgt0 7744  ax-pre-mulext 7745
This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-nel 2404  df-ral 2421  df-rex 2422  df-reu 2423  df-rmo 2424  df-rab 2425  df-v 2688  df-sbc 2910  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-br 3930  df-opab 3990  df-id 4215  df-po 4218  df-iso 4219  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-iota 5088  df-fun 5125  df-fv 5131  df-riota 5730  df-ov 5777  df-oprab 5778  df-mpo 5779  df-pnf 7809  df-mnf 7810  df-xr 7811  df-ltxr 7812  df-le 7813  df-sub 7942  df-neg 7943  df-reap 8344  df-ap 8351  df-div 8440  df-2 8786  df-3 8787  df-4 8788  df-5 8789  df-6 8790
This theorem is referenced by:  fldiv4p1lem1div2  10085
  Copyright terms: Public domain W3C validator