addnqprl - Intuitionistic Logic Explorer

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

Theorem addnqprl 6512

Description: Lemma to prove downward closure in positive real addition. (Contributed by Jim Kingdon, 5-Dec-2019.)

**Assertion**
Ref	Expression
addnqprl	⊢ ((((A ∈ P ∧ 𝐺 ∈ (1^st ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈ (1^st ‘B))) ∧ 𝑋 ∈ Q) → (𝑋 <_Q (𝐺 +_Q 𝐻) → 𝑋 ∈ (1^st ‘(A +_P B))))

Proof of Theorem addnqprl Dummy variables x y 𝑟 𝑞 𝑠 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		prop 6458	. . . . . 6 ⊢ (A ∈ P → ⟨(1^st ‘A), (2^nd ‘A)⟩ ∈ P)
2		addnqprllem 6510	. . . . . 6 ⊢ (((⟨(1^st ‘A), (2^nd ‘A)⟩ ∈ P ∧ 𝐺 ∈ (1^st ‘A)) ∧ 𝑋 ∈ Q) → (𝑋 <_Q (𝐺 +_Q 𝐻) → ((𝑋 ·_Q (*_Q‘(𝐺 +_Q 𝐻))) ·_Q 𝐺) ∈ (1^st ‘A)))
3	1, 2	sylanl1 382	. . . . 5 ⊢ (((A ∈ P ∧ 𝐺 ∈ (1^st ‘A)) ∧ 𝑋 ∈ Q) → (𝑋 <_Q (𝐺 +_Q 𝐻) → ((𝑋 ·_Q (*_Q‘(𝐺 +_Q 𝐻))) ·_Q 𝐺) ∈ (1^st ‘A)))
4	3	adantlr 446	. . . 4 ⊢ ((((A ∈ P ∧ 𝐺 ∈ (1^st ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈ (1^st ‘B))) ∧ 𝑋 ∈ Q) → (𝑋 <_Q (𝐺 +_Q 𝐻) → ((𝑋 ·_Q (*_Q‘(𝐺 +_Q 𝐻))) ·_Q 𝐺) ∈ (1^st ‘A)))
5		prop 6458	. . . . . 6 ⊢ (B ∈ P → ⟨(1^st ‘B), (2^nd ‘B)⟩ ∈ P)
6		addnqprllem 6510	. . . . . 6 ⊢ (((⟨(1^st ‘B), (2^nd ‘B)⟩ ∈ P ∧ 𝐻 ∈ (1^st ‘B)) ∧ 𝑋 ∈ Q) → (𝑋 <_Q (𝐺 +_Q 𝐻) → ((𝑋 ·_Q (*_Q‘(𝐺 +_Q 𝐻))) ·_Q 𝐻) ∈ (1^st ‘B)))
7	5, 6	sylanl1 382	. . . . 5 ⊢ (((B ∈ P ∧ 𝐻 ∈ (1^st ‘B)) ∧ 𝑋 ∈ Q) → (𝑋 <_Q (𝐺 +_Q 𝐻) → ((𝑋 ·_Q (*_Q‘(𝐺 +_Q 𝐻))) ·_Q 𝐻) ∈ (1^st ‘B)))
8	7	adantll 445	. . . 4 ⊢ ((((A ∈ P ∧ 𝐺 ∈ (1^st ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈ (1^st ‘B))) ∧ 𝑋 ∈ Q) → (𝑋 <_Q (𝐺 +_Q 𝐻) → ((𝑋 ·_Q (*_Q‘(𝐺 +_Q 𝐻))) ·_Q 𝐻) ∈ (1^st ‘B)))
9	4, 8	jcad 291	. . 3 ⊢ ((((A ∈ P ∧ 𝐺 ∈ (1^st ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈ (1^st ‘B))) ∧ 𝑋 ∈ Q) → (𝑋 <_Q (𝐺 +_Q 𝐻) → (((𝑋 ·_Q (_Q‘(𝐺 +_Q 𝐻))) ·_Q 𝐺) ∈ (1^st ‘A) ∧ ((𝑋 ·_Q (_Q‘(𝐺 +_Q 𝐻))) ·_Q 𝐻) ∈ (1^st ‘B))))
10		simpl 102	. . . 4 ⊢ ((((A ∈ P ∧ 𝐺 ∈ (1^st ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈ (1^st ‘B))) ∧ 𝑋 ∈ Q) → ((A ∈ P ∧ 𝐺 ∈ (1^st ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈ (1^st ‘B))))
11		simpl 102	. . . . 5 ⊢ ((A ∈ P ∧ 𝐺 ∈ (1^st ‘A)) → A ∈ P)
12		simpl 102	. . . . 5 ⊢ ((B ∈ P ∧ 𝐻 ∈ (1^st ‘B)) → B ∈ P)
13	11, 12	anim12i 321	. . . 4 ⊢ (((A ∈ P ∧ 𝐺 ∈ (1^st ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈ (1^st ‘B))) → (A ∈ P ∧ B ∈ P))
14		df-iplp 6451	. . . . 5 ⊢ +_P = (x ∈ P, y ∈ P ↦ ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1^st ‘x) ∧ 𝑠 ∈ (1^st ‘y) ∧ 𝑞 = (𝑟 +_Q 𝑠))}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2^nd ‘x) ∧ 𝑠 ∈ (2^nd ‘y) ∧ 𝑞 = (𝑟 +_Q 𝑠))}⟩)
15		addclnq 6359	. . . . 5 ⊢ ((𝑟 ∈ Q ∧ 𝑠 ∈ Q) → (𝑟 +_Q 𝑠) ∈ Q)
16	14, 15	genpprecll 6497	. . . 4 ⊢ ((A ∈ P ∧ B ∈ P) → ((((𝑋 ·_Q (_Q‘(𝐺 +_Q 𝐻))) ·_Q 𝐺) ∈ (1^st ‘A) ∧ ((𝑋 ·_Q (_Q‘(𝐺 +_Q 𝐻))) ·_Q 𝐻) ∈ (1^st ‘B)) → (((𝑋 ·_Q (_Q‘(𝐺 +_Q 𝐻))) ·_Q 𝐺) +_Q ((𝑋 ·_Q (_Q‘(𝐺 +_Q 𝐻))) ·_Q 𝐻)) ∈ (1^st ‘(A +_P B))))
17	10, 13, 16	3syl 17	. . 3 ⊢ ((((A ∈ P ∧ 𝐺 ∈ (1^st ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈ (1^st ‘B))) ∧ 𝑋 ∈ Q) → ((((𝑋 ·_Q (_Q‘(𝐺 +_Q 𝐻))) ·_Q 𝐺) ∈ (1^st ‘A) ∧ ((𝑋 ·_Q (_Q‘(𝐺 +_Q 𝐻))) ·_Q 𝐻) ∈ (1^st ‘B)) → (((𝑋 ·_Q (_Q‘(𝐺 +_Q 𝐻))) ·_Q 𝐺) +_Q ((𝑋 ·_Q (_Q‘(𝐺 +_Q 𝐻))) ·_Q 𝐻)) ∈ (1^st ‘(A +_P B))))
18	9, 17	syld 40	. 2 ⊢ ((((A ∈ P ∧ 𝐺 ∈ (1^st ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈ (1^st ‘B))) ∧ 𝑋 ∈ Q) → (𝑋 <_Q (𝐺 +_Q 𝐻) → (((𝑋 ·_Q (_Q‘(𝐺 +_Q 𝐻))) ·_Q 𝐺) +_Q ((𝑋 ·_Q (_Q‘(𝐺 +_Q 𝐻))) ·_Q 𝐻)) ∈ (1^st ‘(A +_P B))))
19		simpr 103	. . . . 5 ⊢ ((((A ∈ P ∧ 𝐺 ∈ (1^st ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈ (1^st ‘B))) ∧ 𝑋 ∈ Q) → 𝑋 ∈ Q)
20		elprnql 6464	. . . . . . . . 9 ⊢ ((⟨(1^st ‘A), (2^nd ‘A)⟩ ∈ P ∧ 𝐺 ∈ (1^st ‘A)) → 𝐺 ∈ Q)
21	1, 20	sylan 267	. . . . . . . 8 ⊢ ((A ∈ P ∧ 𝐺 ∈ (1^st ‘A)) → 𝐺 ∈ Q)
22	21	ad2antrr 457	. . . . . . 7 ⊢ ((((A ∈ P ∧ 𝐺 ∈ (1^st ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈ (1^st ‘B))) ∧ 𝑋 ∈ Q) → 𝐺 ∈ Q)
23		elprnql 6464	. . . . . . . . 9 ⊢ ((⟨(1^st ‘B), (2^nd ‘B)⟩ ∈ P ∧ 𝐻 ∈ (1^st ‘B)) → 𝐻 ∈ Q)
24	5, 23	sylan 267	. . . . . . . 8 ⊢ ((B ∈ P ∧ 𝐻 ∈ (1^st ‘B)) → 𝐻 ∈ Q)
25	24	ad2antlr 458	. . . . . . 7 ⊢ ((((A ∈ P ∧ 𝐺 ∈ (1^st ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈ (1^st ‘B))) ∧ 𝑋 ∈ Q) → 𝐻 ∈ Q)
26		addclnq 6359	. . . . . . 7 ⊢ ((𝐺 ∈ Q ∧ 𝐻 ∈ Q) → (𝐺 +_Q 𝐻) ∈ Q)
27	22, 25, 26	syl2anc 391	. . . . . 6 ⊢ ((((A ∈ P ∧ 𝐺 ∈ (1^st ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈ (1^st ‘B))) ∧ 𝑋 ∈ Q) → (𝐺 +_Q 𝐻) ∈ Q)
28		recclnq 6376	. . . . . 6 ⊢ ((𝐺 +_Q 𝐻) ∈ Q → (*_Q‘(𝐺 +_Q 𝐻)) ∈ Q)
29	27, 28	syl 14	. . . . 5 ⊢ ((((A ∈ P ∧ 𝐺 ∈ (1^st ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈ (1^st ‘B))) ∧ 𝑋 ∈ Q) → (*_Q‘(𝐺 +_Q 𝐻)) ∈ Q)
30		mulassnqg 6368	. . . . 5 ⊢ ((𝑋 ∈ Q ∧ (_Q‘(𝐺 +_Q 𝐻)) ∈ Q ∧ (𝐺 +_Q 𝐻) ∈ Q) → ((𝑋 ·_Q (_Q‘(𝐺 +_Q 𝐻))) ·_Q (𝐺 +_Q 𝐻)) = (𝑋 ·_Q ((*_Q‘(𝐺 +_Q 𝐻)) ·_Q (𝐺 +_Q 𝐻))))
31	19, 29, 27, 30	syl3anc 1134	. . . 4 ⊢ ((((A ∈ P ∧ 𝐺 ∈ (1^st ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈ (1^st ‘B))) ∧ 𝑋 ∈ Q) → ((𝑋 ·_Q (_Q‘(𝐺 +_Q 𝐻))) ·_Q (𝐺 +_Q 𝐻)) = (𝑋 ·_Q ((_Q‘(𝐺 +_Q 𝐻)) ·_Q (𝐺 +_Q 𝐻))))
32		mulclnq 6360	. . . . . 6 ⊢ ((𝑋 ∈ Q ∧ (_Q‘(𝐺 +_Q 𝐻)) ∈ Q) → (𝑋 ·_Q (_Q‘(𝐺 +_Q 𝐻))) ∈ Q)
33	19, 29, 32	syl2anc 391	. . . . 5 ⊢ ((((A ∈ P ∧ 𝐺 ∈ (1^st ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈ (1^st ‘B))) ∧ 𝑋 ∈ 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 𝐻)))
35	33, 22, 25, 34	syl3anc 1134	. . . 4 ⊢ ((((A ∈ P ∧ 𝐺 ∈ (1^st ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈ (1^st ‘B))) ∧ 𝑋 ∈ 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 𝐻))))
37	29, 27, 36	syl2anc 391	. . . . . . 7 ⊢ ((((A ∈ P ∧ 𝐺 ∈ (1^st ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈ (1^st ‘B))) ∧ 𝑋 ∈ Q) → ((_Q‘(𝐺 +_Q 𝐻)) ·_Q (𝐺 +_Q 𝐻)) = ((𝐺 +_Q 𝐻) ·_Q (_Q‘(𝐺 +_Q 𝐻))))
38		recidnq 6377	. . . . . . . 8 ⊢ ((𝐺 +_Q 𝐻) ∈ Q → ((𝐺 +_Q 𝐻) ·_Q (*_Q‘(𝐺 +_Q 𝐻))) = 1_Q)
39	27, 38	syl 14	. . . . . . 7 ⊢ ((((A ∈ P ∧ 𝐺 ∈ (1^st ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈ (1^st ‘B))) ∧ 𝑋 ∈ Q) → ((𝐺 +_Q 𝐻) ·_Q (*_Q‘(𝐺 +_Q 𝐻))) = 1_Q)
40	37, 39	eqtrd 2069	. . . . . 6 ⊢ ((((A ∈ P ∧ 𝐺 ∈ (1^st ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈ (1^st ‘B))) ∧ 𝑋 ∈ Q) → ((*_Q‘(𝐺 +_Q 𝐻)) ·_Q (𝐺 +_Q 𝐻)) = 1_Q)
41	40	oveq2d 5471	. . . . 5 ⊢ ((((A ∈ P ∧ 𝐺 ∈ (1^st ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈ (1^st ‘B))) ∧ 𝑋 ∈ Q) → (𝑋 ·_Q ((*_Q‘(𝐺 +_Q 𝐻)) ·_Q (𝐺 +_Q 𝐻))) = (𝑋 ·_Q 1_Q))
42		mulidnq 6373	. . . . . 6 ⊢ (𝑋 ∈ Q → (𝑋 ·_Q 1_Q) = 𝑋)
43	42	adantl 262	. . . . 5 ⊢ ((((A ∈ P ∧ 𝐺 ∈ (1^st ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈ (1^st ‘B))) ∧ 𝑋 ∈ Q) → (𝑋 ·_Q 1_Q) = 𝑋)
44	41, 43	eqtrd 2069	. . . 4 ⊢ ((((A ∈ P ∧ 𝐺 ∈ (1^st ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈ (1^st ‘B))) ∧ 𝑋 ∈ Q) → (𝑋 ·_Q ((*_Q‘(𝐺 +_Q 𝐻)) ·_Q (𝐺 +_Q 𝐻))) = 𝑋)
45	31, 35, 44	3eqtr3d 2077	. . 3 ⊢ ((((A ∈ P ∧ 𝐺 ∈ (1^st ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈ (1^st ‘B))) ∧ 𝑋 ∈ Q) → (((𝑋 ·_Q (_Q‘(𝐺 +_Q 𝐻))) ·_Q 𝐺) +_Q ((𝑋 ·_Q (_Q‘(𝐺 +_Q 𝐻))) ·_Q 𝐻)) = 𝑋)
46	45	eleq1d 2103	. 2 ⊢ ((((A ∈ P ∧ 𝐺 ∈ (1^st ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈ (1^st ‘B))) ∧ 𝑋 ∈ Q) → ((((𝑋 ·_Q (_Q‘(𝐺 +_Q 𝐻))) ·_Q 𝐺) +_Q ((𝑋 ·_Q (_Q‘(𝐺 +_Q 𝐻))) ·_Q 𝐻)) ∈ (1^st ‘(A +_P B)) ↔ 𝑋 ∈ (1^st ‘(A +_P B))))
47	18, 46	sylibd 138	1 ⊢ ((((A ∈ P ∧ 𝐺 ∈ (1^st ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈ (1^st ‘B))) ∧ 𝑋 ∈ Q) → (𝑋 <_Q (𝐺 +_Q 𝐻) → 𝑋 ∈ (1^st ‘(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 1^st c1st 5707 2^nd c2nd 5708 Qcnq 6264 1_Qc1q 6265 +_Q cplq 6266 ·_Q cmq 6267 *_Qcrq 6268 <_Q cltq 6269 Pcnp 6275 +_P cpp 6277

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-in1 544 ax-in2 545 ax-io 629 ax-5 1333 ax-7 1334 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-8 1392 ax-10 1393 ax-11 1394 ax-i12 1395 ax-bndl 1396 ax-4 1397 ax-13 1401 ax-14 1402 ax-17 1416 ax-i9 1420 ax-ial 1424 ax-i5r 1425 ax-ext 2019 ax-coll 3863 ax-sep 3866 ax-nul 3874 ax-pow 3918 ax-pr 3935 ax-un 4136 ax-setind 4220 ax-iinf 4254

This theorem depends on definitions: df-bi 110 df-dc 742 df-3or 885 df-3an 886 df-tru 1245 df-fal 1248 df-nf 1347 df-sb 1643 df-eu 1900 df-mo 1901 df-clab 2024 df-cleq 2030 df-clel 2033 df-nfc 2164 df-ne 2203 df-ral 2305 df-rex 2306 df-reu 2307 df-rab 2309 df-v 2553 df-sbc 2759 df-csb 2847 df-dif 2914 df-un 2916 df-in 2918 df-ss 2925 df-nul 3219 df-pw 3353 df-sn 3373 df-pr 3374 df-op 3376 df-uni 3572 df-int 3607 df-iun 3650 df-br 3756 df-opab 3810 df-mpt 3811 df-tr 3846 df-eprel 4017 df-id 4021 df-iord 4069 df-on 4071 df-suc 4074 df-iom 4257 df-xp 4294 df-rel 4295 df-cnv 4296 df-co 4297 df-dm 4298 df-rn 4299 df-res 4300 df-ima 4301 df-iota 4810 df-fun 4847 df-fn 4848 df-f 4849 df-f1 4850 df-fo 4851 df-f1o 4852 df-fv 4853 df-ov 5458 df-oprab 5459 df-mpt2 5460 df-1st 5709 df-2nd 5710 df-recs 5861 df-irdg 5897 df-1o 5940 df-oadd 5944 df-omul 5945 df-er 6042 df-ec 6044 df-qs 6048 df-ni 6288 df-pli 6289 df-mi 6290 df-lti 6291 df-plpq 6328 df-mpq 6329 df-enq 6331 df-nqqs 6332 df-plqqs 6333 df-mqqs 6334 df-1nqqs 6335 df-rq 6336 df-ltnqqs 6337 df-inp 6449 df-iplp 6451

This theorem is referenced by: addlocprlemlt 6514 addclpr 6520

W3C validator