ltaddpr

Description: The sum of two positive reals is greater than one of them. Proposition 9-3.5(iii) of Gleason p. 123. (Contributed by NM, 26-Mar-1996) (Revised by Mario Carneiro, 12-Jun-2013) (New usage is discouraged.)

		Ref	Expression
	Assertion	ltaddpr	$⊢ (A \in 𝑷 \land B \in 𝑷) \to A <_{𝑷} (A +_{𝑷} B)$

Proof

Step	Hyp	Ref	Expression
1		prn0	$⊢ B \in 𝑷 \to B \neq \emptyset$
2		n0	$⊢ B \neq \emptyset \leftrightarrow \exists y y \in B$
3	1 2	sylib	$⊢ B \in 𝑷 \to \exists y y \in B$
4	3	adantl	$⊢ (A \in 𝑷 \land B \in 𝑷) \to \exists y y \in B$
5		addclpr	$⊢ (A \in 𝑷 \land B \in 𝑷) \to A +_{𝑷} B \in 𝑷$
6		df-plp	$⊢ +_{𝑷} = (w \in 𝑷, v \in 𝑷 ⟼ \{x \| \exists y \in w \exists z \in v x = y +_{𝑸} z\})$
7		addclnq	$⊢ (y \in 𝑸 \land z \in 𝑸) \to y +_{𝑸} z \in 𝑸$
8	6 7	genpprecl	$⊢ (A \in 𝑷 \land B \in 𝑷) \to ((x \in A \land y \in B) \to x +_{𝑸} y \in (A +_{𝑷} B))$
9	8	imp	$⊢ ((A \in 𝑷 \land B \in 𝑷) \land (x \in A \land y \in B)) \to x +_{𝑸} y \in (A +_{𝑷} B)$
10		elprnq	$⊢ (A +_{𝑷} B \in 𝑷 \land x +_{𝑸} y \in (A +_{𝑷} B)) \to x +_{𝑸} y \in 𝑸$
11		addnqf	$⊢ +_{𝑸} : 𝑸 \times 𝑸 ⟶ 𝑸$
12	11	fdmi	$⊢ dom +_{𝑸} = 𝑸 \times 𝑸$
13		0nnq	$⊢ \neg \emptyset \in 𝑸$
14	12 13	ndmovrcl	$⊢ x +_{𝑸} y \in 𝑸 \to (x \in 𝑸 \land y \in 𝑸)$
15		ltaddnq	$⊢ (x \in 𝑸 \land y \in 𝑸) \to x <_{𝑸} (x +_{𝑸} y)$
16	10 14 15	3syl	$⊢ (A +_{𝑷} B \in 𝑷 \land x +_{𝑸} y \in (A +_{𝑷} B)) \to x <_{𝑸} (x +_{𝑸} y)$
17		prcdnq	$⊢ (A +_{𝑷} B \in 𝑷 \land x +_{𝑸} y \in (A +_{𝑷} B)) \to (x <_{𝑸} (x +_{𝑸} y) \to x \in (A +_{𝑷} B))$
18	16 17	mpd	$⊢ (A +_{𝑷} B \in 𝑷 \land x +_{𝑸} y \in (A +_{𝑷} B)) \to x \in (A +_{𝑷} B)$
19	5 9 18	syl2an2r	$⊢ ((A \in 𝑷 \land B \in 𝑷) \land (x \in A \land y \in B)) \to x \in (A +_{𝑷} B)$
20	19	exp32	$⊢ (A \in 𝑷 \land B \in 𝑷) \to (x \in A \to (y \in B \to x \in (A +_{𝑷} B)))$
21	20	com23	$⊢ (A \in 𝑷 \land B \in 𝑷) \to (y \in B \to (x \in A \to x \in (A +_{𝑷} B)))$
22	21	alrimdv	$⊢ (A \in 𝑷 \land B \in 𝑷) \to (y \in B \to \forall x (x \in A \to x \in (A +_{𝑷} B)))$
23		df-ss	$⊢ A \subseteq A +_{𝑷} B \leftrightarrow \forall x (x \in A \to x \in (A +_{𝑷} B))$
24	22 23	imbitrrdi	$⊢ (A \in 𝑷 \land B \in 𝑷) \to (y \in B \to A \subseteq A +_{𝑷} B)$
25		vex	$⊢ y \in V$
26	25	prlem934	$⊢ A \in 𝑷 \to \exists x \in A \neg x +_{𝑸} y \in A$
27	26	adantr	$⊢ (A \in 𝑷 \land B \in 𝑷) \to \exists x \in A \neg x +_{𝑸} y \in A$
28		eleq2	$⊢ A = A +_{𝑷} B \to (x +_{𝑸} y \in A \leftrightarrow x +_{𝑸} y \in (A +_{𝑷} B))$
29	28	biimprcd	$⊢ x +_{𝑸} y \in (A +_{𝑷} B) \to (A = A +_{𝑷} B \to x +_{𝑸} y \in A)$
30	29	con3d	$⊢ x +_{𝑸} y \in (A +_{𝑷} B) \to (\neg x +_{𝑸} y \in A \to \neg A = A +_{𝑷} B)$
31	8 30	syl6	$⊢ (A \in 𝑷 \land B \in 𝑷) \to ((x \in A \land y \in B) \to (\neg x +_{𝑸} y \in A \to \neg A = A +_{𝑷} B))$
32	31	expd	$⊢ (A \in 𝑷 \land B \in 𝑷) \to (x \in A \to (y \in B \to (\neg x +_{𝑸} y \in A \to \neg A = A +_{𝑷} B)))$
33	32	com34	$⊢ (A \in 𝑷 \land B \in 𝑷) \to (x \in A \to (\neg x +_{𝑸} y \in A \to (y \in B \to \neg A = A +_{𝑷} B)))$
34	33	rexlimdv	$⊢ (A \in 𝑷 \land B \in 𝑷) \to (\exists x \in A \neg x +_{𝑸} y \in A \to (y \in B \to \neg A = A +_{𝑷} B))$
35	27 34	mpd	$⊢ (A \in 𝑷 \land B \in 𝑷) \to (y \in B \to \neg A = A +_{𝑷} B)$
36	24 35	jcad	$⊢ (A \in 𝑷 \land B \in 𝑷) \to (y \in B \to (A \subseteq A +_{𝑷} B \land \neg A = A +_{𝑷} B))$
37		dfpss2	$⊢ A \subset A +_{𝑷} B \leftrightarrow (A \subseteq A +_{𝑷} B \land \neg A = A +_{𝑷} B)$
38	36 37	imbitrrdi	$⊢ (A \in 𝑷 \land B \in 𝑷) \to (y \in B \to A \subset A +_{𝑷} B)$
39	38	exlimdv	$⊢ (A \in 𝑷 \land B \in 𝑷) \to (\exists y y \in B \to A \subset A +_{𝑷} B)$
40	4 39	mpd	$⊢ (A \in 𝑷 \land B \in 𝑷) \to A \subset A +_{𝑷} B$
41		ltprord	$⊢ (A \in 𝑷 \land A +_{𝑷} B \in 𝑷) \to (A <_{𝑷} (A +_{𝑷} B) \leftrightarrow A \subset A +_{𝑷} B)$
42	5 41	syldan	$⊢ (A \in 𝑷 \land B \in 𝑷) \to (A <_{𝑷} (A +_{𝑷} B) \leftrightarrow A \subset A +_{𝑷} B)$
43	40 42	mpbird	$⊢ (A \in 𝑷 \land B \in 𝑷) \to A <_{𝑷} (A +_{𝑷} B)$

Metamath Proof Explorer

Theorem ltaddpr

Proof