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

 Description: Lemma for addlocpr 6634. The 𝑄
Hypotheses
Ref Expression
addlocprlem.qppr (𝜑 → (𝑄 +Q (𝑃 +Q 𝑃)) = 𝑅)
addlocprlem.du (𝜑𝑈 <Q (𝐷 +Q 𝑃))
addlocprlem.et (𝜑𝑇 <Q (𝐸 +Q 𝑃))
Assertion
Ref Expression
addlocprlemlt (𝜑 → (𝑄 <Q (𝐷 +Q 𝐸) → 𝑄 ∈ (1st ‘(𝐴 +P 𝐵))))

StepHypRef Expression
1 addlocprlem.a . . 3 (𝜑𝐴P)
2 addlocprlem.dlo . . 3 (𝜑𝐷 ∈ (1st𝐴))
31, 2jca 290 . 2 (𝜑 → (𝐴P𝐷 ∈ (1st𝐴)))
4 addlocprlem.b . . 3 (𝜑𝐵P)
5 addlocprlem.elo . . 3 (𝜑𝐸 ∈ (1st𝐵))
64, 5jca 290 . 2 (𝜑 → (𝐵P𝐸 ∈ (1st𝐵)))
7 addlocprlem.qr . . 3 (𝜑𝑄 <Q 𝑅)
8 ltrelnq 6463 . . . . 5 <Q ⊆ (Q × Q)
98brel 4392 . . . 4 (𝑄 <Q 𝑅 → (𝑄Q𝑅Q))
109simpld 105 . . 3 (𝑄 <Q 𝑅𝑄Q)
117, 10syl 14 . 2 (𝜑𝑄Q)
12 addnqprl 6627 . 2 ((((𝐴P𝐷 ∈ (1st𝐴)) ∧ (𝐵P𝐸 ∈ (1st𝐵))) ∧ 𝑄Q) → (𝑄 <Q (𝐷 +Q 𝐸) → 𝑄 ∈ (1st ‘(𝐴 +P 𝐵))))
133, 6, 11, 12syl21anc 1134 1 (𝜑 → (𝑄 <Q (𝐷 +Q 𝐸) → 𝑄 ∈ (1st ‘(𝐴 +P 𝐵))))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   = wceq 1243   ∈ wcel 1393   class class class wbr 3764  ‘cfv 4902  (class class class)co 5512  1st c1st 5765  2nd c2nd 5766  Qcnq 6378   +Q cplq 6380
 Copyright terms: Public domain W3C validator