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

 Description: Lemma to prove downward closure in positive real addition. (Contributed by Jim Kingdon, 5-Dec-2019.)
Assertion
Ref Expression
addnqprl ((((A P 𝐺 (1stA)) (B P 𝐻 (1stB))) 𝑋 Q) → (𝑋 <Q (𝐺 +Q 𝐻) → 𝑋 (1st ‘(A +P B))))

Dummy variables x y 𝑟 𝑞 𝑠 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 prop 6458 . . . . . 6 (A P → ⟨(1stA), (2ndA)⟩ P)
2 addnqprllem 6510 . . . . . 6 (((⟨(1stA), (2ndA)⟩ P 𝐺 (1stA)) 𝑋 Q) → (𝑋 <Q (𝐺 +Q 𝐻) → ((𝑋 ·Q (*Q‘(𝐺 +Q 𝐻))) ·Q 𝐺) (1stA)))
31, 2sylanl1 382 . . . . 5 (((A P 𝐺 (1stA)) 𝑋 Q) → (𝑋 <Q (𝐺 +Q 𝐻) → ((𝑋 ·Q (*Q‘(𝐺 +Q 𝐻))) ·Q 𝐺) (1stA)))
43adantlr 446 . . . 4 ((((A P 𝐺 (1stA)) (B P 𝐻 (1stB))) 𝑋 Q) → (𝑋 <Q (𝐺 +Q 𝐻) → ((𝑋 ·Q (*Q‘(𝐺 +Q 𝐻))) ·Q 𝐺) (1stA)))
5 prop 6458 . . . . . 6 (B P → ⟨(1stB), (2ndB)⟩ P)
6 addnqprllem 6510 . . . . . 6 (((⟨(1stB), (2ndB)⟩ P 𝐻 (1stB)) 𝑋 Q) → (𝑋 <Q (𝐺 +Q 𝐻) → ((𝑋 ·Q (*Q‘(𝐺 +Q 𝐻))) ·Q 𝐻) (1stB)))
75, 6sylanl1 382 . . . . 5 (((B P 𝐻 (1stB)) 𝑋 Q) → (𝑋 <Q (𝐺 +Q 𝐻) → ((𝑋 ·Q (*Q‘(𝐺 +Q 𝐻))) ·Q 𝐻) (1stB)))
87adantll 445 . . . 4 ((((A P 𝐺 (1stA)) (B P 𝐻 (1stB))) 𝑋 Q) → (𝑋 <Q (𝐺 +Q 𝐻) → ((𝑋 ·Q (*Q‘(𝐺 +Q 𝐻))) ·Q 𝐻) (1stB)))
94, 8jcad 291 . . 3 ((((A P 𝐺 (1stA)) (B P 𝐻 (1stB))) 𝑋 Q) → (𝑋 <Q (𝐺 +Q 𝐻) → (((𝑋 ·Q (*Q‘(𝐺 +Q 𝐻))) ·Q 𝐺) (1stA) ((𝑋 ·Q (*Q‘(𝐺 +Q 𝐻))) ·Q 𝐻) (1stB))))
10 simpl 102 . . . 4 ((((A P 𝐺 (1stA)) (B P 𝐻 (1stB))) 𝑋 Q) → ((A P 𝐺 (1stA)) (B P 𝐻 (1stB))))
11 simpl 102 . . . . 5 ((A P 𝐺 (1stA)) → A P)
12 simpl 102 . . . . 5 ((B P 𝐻 (1stB)) → B P)
1311, 12anim12i 321 . . . 4 (((A P 𝐺 (1stA)) (B P 𝐻 (1stB))) → (A P B P))
14 df-iplp 6451 . . . . 5 +P = (x P, y P ↦ ⟨{𝑞 Q𝑟 Q 𝑠 Q (𝑟 (1stx) 𝑠 (1sty) 𝑞 = (𝑟 +Q 𝑠))}, {𝑞 Q𝑟 Q 𝑠 Q (𝑟 (2ndx) 𝑠 (2ndy) 𝑞 = (𝑟 +Q 𝑠))}⟩)
15 addclnq 6359 . . . . 5 ((𝑟 Q 𝑠 Q) → (𝑟 +Q 𝑠) Q)
1614, 15genpprecll 6497 . . . 4 ((A P B P) → ((((𝑋 ·Q (*Q‘(𝐺 +Q 𝐻))) ·Q 𝐺) (1stA) ((𝑋 ·Q (*Q‘(𝐺 +Q 𝐻))) ·Q 𝐻) (1stB)) → (((𝑋 ·Q (*Q‘(𝐺 +Q 𝐻))) ·Q 𝐺) +Q ((𝑋 ·Q (*Q‘(𝐺 +Q 𝐻))) ·Q 𝐻)) (1st ‘(A +P B))))
1710, 13, 163syl 17 . . 3 ((((A P 𝐺 (1stA)) (B P 𝐻 (1stB))) 𝑋 Q) → ((((𝑋 ·Q (*Q‘(𝐺 +Q 𝐻))) ·Q 𝐺) (1stA) ((𝑋 ·Q (*Q‘(𝐺 +Q 𝐻))) ·Q 𝐻) (1stB)) → (((𝑋 ·Q (*Q‘(𝐺 +Q 𝐻))) ·Q 𝐺) +Q ((𝑋 ·Q (*Q‘(𝐺 +Q 𝐻))) ·Q 𝐻)) (1st ‘(A +P B))))
189, 17syld 40 . 2 ((((A P 𝐺 (1stA)) (B P 𝐻 (1stB))) 𝑋 Q) → (𝑋 <Q (𝐺 +Q 𝐻) → (((𝑋 ·Q (*Q‘(𝐺 +Q 𝐻))) ·Q 𝐺) +Q ((𝑋 ·Q (*Q‘(𝐺 +Q 𝐻))) ·Q 𝐻)) (1st ‘(A +P B))))
19 simpr 103 . . . . 5 ((((A P 𝐺 (1stA)) (B P 𝐻 (1stB))) 𝑋 Q) → 𝑋 Q)
20 elprnql 6464 . . . . . . . . 9 ((⟨(1stA), (2ndA)⟩ P 𝐺 (1stA)) → 𝐺 Q)
211, 20sylan 267 . . . . . . . 8 ((A P 𝐺 (1stA)) → 𝐺 Q)
2221ad2antrr 457 . . . . . . 7 ((((A P 𝐺 (1stA)) (B P 𝐻 (1stB))) 𝑋 Q) → 𝐺 Q)
23 elprnql 6464 . . . . . . . . 9 ((⟨(1stB), (2ndB)⟩ P 𝐻 (1stB)) → 𝐻 Q)
245, 23sylan 267 . . . . . . . 8 ((B P 𝐻 (1stB)) → 𝐻 Q)
2524ad2antlr 458 . . . . . . 7 ((((A P 𝐺 (1stA)) (B P 𝐻 (1stB))) 𝑋 Q) → 𝐻 Q)
26 addclnq 6359 . . . . . . 7 ((𝐺 Q 𝐻 Q) → (𝐺 +Q 𝐻) Q)
2722, 25, 26syl2anc 391 . . . . . 6 ((((A P 𝐺 (1stA)) (B P 𝐻 (1stB))) 𝑋 Q) → (𝐺 +Q 𝐻) Q)
28 recclnq 6376 . . . . . 6 ((𝐺 +Q 𝐻) Q → (*Q‘(𝐺 +Q 𝐻)) Q)
2927, 28syl 14 . . . . 5 ((((A P 𝐺 (1stA)) (B P 𝐻 (1stB))) 𝑋 Q) → (*Q‘(𝐺 +Q 𝐻)) Q)
30 mulassnqg 6368 . . . . 5 ((𝑋 Q (*Q‘(𝐺 +Q 𝐻)) Q (𝐺 +Q 𝐻) Q) → ((𝑋 ·Q (*Q‘(𝐺 +Q 𝐻))) ·Q (𝐺 +Q 𝐻)) = (𝑋 ·Q ((*Q‘(𝐺 +Q 𝐻)) ·Q (𝐺 +Q 𝐻))))
3119, 29, 27, 30syl3anc 1134 . . . 4 ((((A P 𝐺 (1stA)) (B P 𝐻 (1stB))) 𝑋 Q) → ((𝑋 ·Q (*Q‘(𝐺 +Q 𝐻))) ·Q (𝐺 +Q 𝐻)) = (𝑋 ·Q ((*Q‘(𝐺 +Q 𝐻)) ·Q (𝐺 +Q 𝐻))))
32 mulclnq 6360 . . . . . 6 ((𝑋 Q (*Q‘(𝐺 +Q 𝐻)) Q) → (𝑋 ·Q (*Q‘(𝐺 +Q 𝐻))) Q)
3319, 29, 32syl2anc 391 . . . . 5 ((((A P 𝐺 (1stA)) (B P 𝐻 (1stB))) 𝑋 Q) → (𝑋 ·Q (*Q‘(𝐺 +Q 𝐻))) Q)
34 distrnqg 6371 . . . . 5 (((𝑋 ·Q (*Q‘(𝐺 +Q 𝐻))) Q 𝐺 Q 𝐻 Q) → ((𝑋 ·Q (*Q‘(𝐺 +Q 𝐻))) ·Q (𝐺 +Q 𝐻)) = (((𝑋 ·Q (*Q‘(𝐺 +Q 𝐻))) ·Q 𝐺) +Q ((𝑋 ·Q (*Q‘(𝐺 +Q 𝐻))) ·Q 𝐻)))
3533, 22, 25, 34syl3anc 1134 . . . 4 ((((A P 𝐺 (1stA)) (B P 𝐻 (1stB))) 𝑋 Q) → ((𝑋 ·Q (*Q‘(𝐺 +Q 𝐻))) ·Q (𝐺 +Q 𝐻)) = (((𝑋 ·Q (*Q‘(𝐺 +Q 𝐻))) ·Q 𝐺) +Q ((𝑋 ·Q (*Q‘(𝐺 +Q 𝐻))) ·Q 𝐻)))
36 mulcomnqg 6367 . . . . . . . 8 (((*Q‘(𝐺 +Q 𝐻)) Q (𝐺 +Q 𝐻) Q) → ((*Q‘(𝐺 +Q 𝐻)) ·Q (𝐺 +Q 𝐻)) = ((𝐺 +Q 𝐻) ·Q (*Q‘(𝐺 +Q 𝐻))))
3729, 27, 36syl2anc 391 . . . . . . 7 ((((A P 𝐺 (1stA)) (B P 𝐻 (1stB))) 𝑋 Q) → ((*Q‘(𝐺 +Q 𝐻)) ·Q (𝐺 +Q 𝐻)) = ((𝐺 +Q 𝐻) ·Q (*Q‘(𝐺 +Q 𝐻))))
38 recidnq 6377 . . . . . . . 8 ((𝐺 +Q 𝐻) Q → ((𝐺 +Q 𝐻) ·Q (*Q‘(𝐺 +Q 𝐻))) = 1Q)
3927, 38syl 14 . . . . . . 7 ((((A P 𝐺 (1stA)) (B P 𝐻 (1stB))) 𝑋 Q) → ((𝐺 +Q 𝐻) ·Q (*Q‘(𝐺 +Q 𝐻))) = 1Q)
4037, 39eqtrd 2069 . . . . . 6 ((((A P 𝐺 (1stA)) (B P 𝐻 (1stB))) 𝑋 Q) → ((*Q‘(𝐺 +Q 𝐻)) ·Q (𝐺 +Q 𝐻)) = 1Q)
4140oveq2d 5471 . . . . 5 ((((A P 𝐺 (1stA)) (B P 𝐻 (1stB))) 𝑋 Q) → (𝑋 ·Q ((*Q‘(𝐺 +Q 𝐻)) ·Q (𝐺 +Q 𝐻))) = (𝑋 ·Q 1Q))
42 mulidnq 6373 . . . . . 6 (𝑋 Q → (𝑋 ·Q 1Q) = 𝑋)
4342adantl 262 . . . . 5 ((((A P 𝐺 (1stA)) (B P 𝐻 (1stB))) 𝑋 Q) → (𝑋 ·Q 1Q) = 𝑋)
4441, 43eqtrd 2069 . . . 4 ((((A P 𝐺 (1stA)) (B P 𝐻 (1stB))) 𝑋 Q) → (𝑋 ·Q ((*Q‘(𝐺 +Q 𝐻)) ·Q (𝐺 +Q 𝐻))) = 𝑋)
4531, 35, 443eqtr3d 2077 . . 3 ((((A P 𝐺 (1stA)) (B P 𝐻 (1stB))) 𝑋 Q) → (((𝑋 ·Q (*Q‘(𝐺 +Q 𝐻))) ·Q 𝐺) +Q ((𝑋 ·Q (*Q‘(𝐺 +Q 𝐻))) ·Q 𝐻)) = 𝑋)
4645eleq1d 2103 . 2 ((((A P 𝐺 (1stA)) (B P 𝐻 (1stB))) 𝑋 Q) → ((((𝑋 ·Q (*Q‘(𝐺 +Q 𝐻))) ·Q 𝐺) +Q ((𝑋 ·Q (*Q‘(𝐺 +Q 𝐻))) ·Q 𝐻)) (1st ‘(A +P B)) ↔ 𝑋 (1st ‘(A +P B))))
4718, 46sylibd 138 1 ((((A P 𝐺 (1stA)) (B P 𝐻 (1stB))) 𝑋 Q) → (𝑋 <Q (𝐺 +Q 𝐻) → 𝑋 (1st ‘(A +P B))))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   = wceq 1242   ∈ wcel 1390  ⟨cop 3370   class class class wbr 3755  ‘cfv 4845  (class class class)co 5455  1st c1st 5707  2nd c2nd 5708  Qcnq 6264  1Qc1q 6265   +Q cplq 6266   ·Q cmq 6267  *Qcrq 6268
 Copyright terms: Public domain W3C validator