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

Theorem prarloclem 6349
 Description: A special case of Lemma 6.16 from [BauerTaylor], p. 32. Given evenly spaced rational numbers from A to A +Q (𝑁 ·Q 𝑃) (which are in the lower and upper cuts, respectively, of a real number), there are a pair of numbers, two positions apart in the even spacing, which straddle the cut. (Contributed by Jim Kingdon, 22-Oct-2019.)
Assertion
Ref Expression
prarloclem (((⟨𝐿, 𝑈 P A 𝐿) (𝑁 N 𝑃 Q 1𝑜 <N 𝑁) (A +Q ([⟨𝑁, 1𝑜⟩] ~Q ·Q 𝑃)) 𝑈) → 𝑗 𝜔 ((A +Q0 ([⟨𝑗, 1𝑜⟩] ~Q0 ·Q0 𝑃)) 𝐿 (A +Q ([⟨(𝑗 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑃)) 𝑈))
Distinct variable groups:   A,𝑗   𝑗,𝐿   𝑗,𝑁   𝑃,𝑗   𝑈,𝑗

Proof of Theorem prarloclem
Dummy variables x y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 prarloclem5 6348 . 2 (((⟨𝐿, 𝑈 P A 𝐿) (𝑁 N 𝑃 Q 1𝑜 <N 𝑁) (A +Q ([⟨𝑁, 1𝑜⟩] ~Q ·Q 𝑃)) 𝑈) → x 𝜔 y 𝜔 ((A +Q0 ([⟨y, 1𝑜⟩] ~Q0 ·Q0 𝑃)) 𝐿 (A +Q ([⟨((y +𝑜 2𝑜) +𝑜 x), 1𝑜⟩] ~Q ·Q 𝑃)) 𝑈))
2 prarloclem4 6346 . . . 4 (((⟨𝐿, 𝑈 P A 𝐿) 𝑃 Q) → (x 𝜔 y 𝜔 ((A +Q0 ([⟨y, 1𝑜⟩] ~Q0 ·Q0 𝑃)) 𝐿 (A +Q ([⟨((y +𝑜 2𝑜) +𝑜 x), 1𝑜⟩] ~Q ·Q 𝑃)) 𝑈) → 𝑗 𝜔 ((A +Q0 ([⟨𝑗, 1𝑜⟩] ~Q0 ·Q0 𝑃)) 𝐿 (A +Q ([⟨(𝑗 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑃)) 𝑈)))
323ad2antr2 1056 . . 3 (((⟨𝐿, 𝑈 P A 𝐿) (𝑁 N 𝑃 Q 1𝑜 <N 𝑁)) → (x 𝜔 y 𝜔 ((A +Q0 ([⟨y, 1𝑜⟩] ~Q0 ·Q0 𝑃)) 𝐿 (A +Q ([⟨((y +𝑜 2𝑜) +𝑜 x), 1𝑜⟩] ~Q ·Q 𝑃)) 𝑈) → 𝑗 𝜔 ((A +Q0 ([⟨𝑗, 1𝑜⟩] ~Q0 ·Q0 𝑃)) 𝐿 (A +Q ([⟨(𝑗 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑃)) 𝑈)))
433adant3 910 . 2 (((⟨𝐿, 𝑈 P A 𝐿) (𝑁 N 𝑃 Q 1𝑜 <N 𝑁) (A +Q ([⟨𝑁, 1𝑜⟩] ~Q ·Q 𝑃)) 𝑈) → (x 𝜔 y 𝜔 ((A +Q0 ([⟨y, 1𝑜⟩] ~Q0 ·Q0 𝑃)) 𝐿 (A +Q ([⟨((y +𝑜 2𝑜) +𝑜 x), 1𝑜⟩] ~Q ·Q 𝑃)) 𝑈) → 𝑗 𝜔 ((A +Q0 ([⟨𝑗, 1𝑜⟩] ~Q0 ·Q0 𝑃)) 𝐿 (A +Q ([⟨(𝑗 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑃)) 𝑈)))
51, 4mpd 13 1 (((⟨𝐿, 𝑈 P A 𝐿) (𝑁 N 𝑃 Q 1𝑜 <N 𝑁) (A +Q ([⟨𝑁, 1𝑜⟩] ~Q ·Q 𝑃)) 𝑈) → 𝑗 𝜔 ((A +Q0 ([⟨𝑗, 1𝑜⟩] ~Q0 ·Q0 𝑃)) 𝐿 (A +Q ([⟨(𝑗 +𝑜 2𝑜), 1𝑜⟩] ~Q ·Q 𝑃)) 𝑈))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ∧ w3a 871   ∈ wcel 1370  ∃wrex 2281  ⟨cop 3349   class class class wbr 3734  𝜔com 4236  (class class class)co 5432  1𝑜c1o 5905  2𝑜c2o 5906   +𝑜 coa 5909  [cec 6011  Ncnpi 6126
 Copyright terms: Public domain W3C validator