Theorem prarloclemup 7327

Description: Contracting the upper side of an interval which straddles a Dedekind cut. Lemma for prarloc 7335. (Contributed by Jim Kingdon, 10-Nov-2019.)

Assertion

Ref	Expression
prarloclemup	⊢ (((𝑋 ∈ ω ∧ (⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → ((𝐴 +Q ([⟨((𝑦 +o 2o) +o 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈 → (((𝐴 +Q0 ([⟨𝑦, 1o⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨((𝑦 +o 2o) +o suc 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈) → ∃𝑦 ∈ ω ((𝐴 +Q0 ([⟨𝑦, 1o⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨((𝑦 +o 2o) +o 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈))))

Proof of Theorem prarloclemup

Step	Hyp	Ref	Expression
1		simpllr 524	. . 3 ⊢ (((((𝑋 ∈ ω ∧ (⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) ∧ (𝐴 +Q ([⟨((𝑦 +o 2o) +o 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈) ∧ ((𝐴 +Q0 ([⟨𝑦, 1o⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨((𝑦 +o 2o) +o suc 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈)) → 𝑦 ∈ ω)
2		simprl 521	. . 3 ⊢ (((((𝑋 ∈ ω ∧ (⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) ∧ (𝐴 +Q ([⟨((𝑦 +o 2o) +o 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈) ∧ ((𝐴 +Q0 ([⟨𝑦, 1o⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨((𝑦 +o 2o) +o suc 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈)) → (𝐴 +Q0 ([⟨𝑦, 1o⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿)
3		simplr 520	. . 3 ⊢ (((((𝑋 ∈ ω ∧ (⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) ∧ (𝐴 +Q ([⟨((𝑦 +o 2o) +o 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈) ∧ ((𝐴 +Q0 ([⟨𝑦, 1o⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨((𝑦 +o 2o) +o suc 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈)) → (𝐴 +Q ([⟨((𝑦 +o 2o) +o 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈)
4		rspe 2484	. . 3 ⊢ ((𝑦 ∈ ω ∧ ((𝐴 +Q0 ([⟨𝑦, 1o⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨((𝑦 +o 2o) +o 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈)) → ∃𝑦 ∈ ω ((𝐴 +Q0 ([⟨𝑦, 1o⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨((𝑦 +o 2o) +o 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈))
5	1, 2, 3, 4	syl12anc 1215	. 2 ⊢ (((((𝑋 ∈ ω ∧ (⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) ∧ (𝐴 +Q ([⟨((𝑦 +o 2o) +o 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈) ∧ ((𝐴 +Q0 ([⟨𝑦, 1o⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨((𝑦 +o 2o) +o suc 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈)) → ∃𝑦 ∈ ω ((𝐴 +Q0 ([⟨𝑦, 1o⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨((𝑦 +o 2o) +o 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈))
6	5	exp31 362	1 ⊢ (((𝑋 ∈ ω ∧ (⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → ((𝐴 +Q ([⟨((𝑦 +o 2o) +o 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈 → (((𝐴 +Q0 ([⟨𝑦, 1o⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨((𝑦 +o 2o) +o suc 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈) → ∃𝑦 ∈ ω ((𝐴 +Q0 ([⟨𝑦, 1o⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨((𝑦 +o 2o) +o 𝑋), 1o⟩] ~Q ·Q 𝑃)) ∈ 𝑈))))

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 963   ∈ wcel 1481  ∃wrex 2418  ⟨cop 3535  suc csuc 4295  ωcom 4512  (class class class)co 5782  1_oc1o 6314  2_oc2o 6315   +_o coa 6318  [cec 6435   ~_Q ceq 7111  Qcnq 7112   +_Q cplq 7114   ·_Q cmq 7115   ~_Q0 ceq0 7118   +_Q0 cplq0 7121   ·_Q0 cmq0 7122  Pcnp 7123

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-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488

This theorem depends on definitions:  df-bi 116  df-rex 2423

This theorem is referenced by:  prarloclem3step  7328