ltexnq

Description: Ordering on positive fractions in terms of existence of sum. Definition in Proposition 9-2.6 of Gleason p. 119. (Contributed by NM, 24-Apr-1996) (Revised by Mario Carneiro, 10-May-2013) (New usage is discouraged.)

		Ref	Expression
	Assertion	ltexnq	$⊢ B \in 𝑸 \to (A <_{𝑸} B \leftrightarrow \exists x A +_{𝑸} x = B)$

Proof

Step	Hyp	Ref	Expression
1		ltrelnq	$⊢ <_{𝑸} \subseteq 𝑸 \times 𝑸$
2	1	brel	$⊢ A <_{𝑸} B \to (A \in 𝑸 \land B \in 𝑸)$
3		ordpinq	$⊢ (A \in 𝑸 \land B \in 𝑸) \to (A <_{𝑸} B \leftrightarrow (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) <_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)))$
4		elpqn	$⊢ A \in 𝑸 \to A \in (𝑵 \times 𝑵)$
5	4	adantr	$⊢ (A \in 𝑸 \land B \in 𝑸) \to A \in (𝑵 \times 𝑵)$
6		xp1st	$⊢ A \in (𝑵 \times 𝑵) \to 1^{st} (A) \in 𝑵$
7	5 6	syl	$⊢ (A \in 𝑸 \land B \in 𝑸) \to 1^{st} (A) \in 𝑵$
8		elpqn	$⊢ B \in 𝑸 \to B \in (𝑵 \times 𝑵)$
9	8	adantl	$⊢ (A \in 𝑸 \land B \in 𝑸) \to B \in (𝑵 \times 𝑵)$
10		xp2nd	$⊢ B \in (𝑵 \times 𝑵) \to 2^{nd} (B) \in 𝑵$
11	9 10	syl	$⊢ (A \in 𝑸 \land B \in 𝑸) \to 2^{nd} (B) \in 𝑵$
12		mulclpi	$⊢ (1^{st} (A) \in 𝑵 \land 2^{nd} (B) \in 𝑵) \to 1^{st} (A) \cdot_{𝑵} 2^{nd} (B) \in 𝑵$
13	7 11 12	syl2anc	$⊢ (A \in 𝑸 \land B \in 𝑸) \to 1^{st} (A) \cdot_{𝑵} 2^{nd} (B) \in 𝑵$
14		xp1st	$⊢ B \in (𝑵 \times 𝑵) \to 1^{st} (B) \in 𝑵$
15	9 14	syl	$⊢ (A \in 𝑸 \land B \in 𝑸) \to 1^{st} (B) \in 𝑵$
16		xp2nd	$⊢ A \in (𝑵 \times 𝑵) \to 2^{nd} (A) \in 𝑵$
17	5 16	syl	$⊢ (A \in 𝑸 \land B \in 𝑸) \to 2^{nd} (A) \in 𝑵$
18		mulclpi	$⊢ (1^{st} (B) \in 𝑵 \land 2^{nd} (A) \in 𝑵) \to 1^{st} (B) \cdot_{𝑵} 2^{nd} (A) \in 𝑵$
19	15 17 18	syl2anc	$⊢ (A \in 𝑸 \land B \in 𝑸) \to 1^{st} (B) \cdot_{𝑵} 2^{nd} (A) \in 𝑵$
20		ltexpi	$⊢ (1^{st} (A) \cdot_{𝑵} 2^{nd} (B) \in 𝑵 \land 1^{st} (B) \cdot_{𝑵} 2^{nd} (A) \in 𝑵) \to ((1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) <_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) \leftrightarrow \exists y \in 𝑵 (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} y = 1^{st} (B) \cdot_{𝑵} 2^{nd} (A))$
21	13 19 20	syl2anc	$⊢ (A \in 𝑸 \land B \in 𝑸) \to ((1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) <_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) \leftrightarrow \exists y \in 𝑵 (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} y = 1^{st} (B) \cdot_{𝑵} 2^{nd} (A))$
22		relxp	$⊢ Rel (𝑵 \times 𝑵)$
23	4	ad2antrr	$⊢ ((A \in 𝑸 \land B \in 𝑸) \land y \in 𝑵) \to A \in (𝑵 \times 𝑵)$
24		1st2nd	$⊢ (Rel (𝑵 \times 𝑵) \land A \in (𝑵 \times 𝑵)) \to A = ⟨1^{st} (A), 2^{nd} (A)⟩$
25	22 23 24	sylancr	$⊢ ((A \in 𝑸 \land B \in 𝑸) \land y \in 𝑵) \to A = ⟨1^{st} (A), 2^{nd} (A)⟩$
26	25	oveq1d	$⊢ ((A \in 𝑸 \land B \in 𝑸) \land y \in 𝑵) \to A +_{𝑝𝑸} ⟨y, 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)⟩ = ⟨1^{st} (A), 2^{nd} (A)⟩ +_{𝑝𝑸} ⟨y, 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)⟩$
27	7	adantr	$⊢ ((A \in 𝑸 \land B \in 𝑸) \land y \in 𝑵) \to 1^{st} (A) \in 𝑵$
28	17	adantr	$⊢ ((A \in 𝑸 \land B \in 𝑸) \land y \in 𝑵) \to 2^{nd} (A) \in 𝑵$
29		simpr	$⊢ ((A \in 𝑸 \land B \in 𝑸) \land y \in 𝑵) \to y \in 𝑵$
30		mulclpi	$⊢ (2^{nd} (A) \in 𝑵 \land 2^{nd} (B) \in 𝑵) \to 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B) \in 𝑵$
31	17 11 30	syl2anc	$⊢ (A \in 𝑸 \land B \in 𝑸) \to 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B) \in 𝑵$
32	31	adantr	$⊢ ((A \in 𝑸 \land B \in 𝑸) \land y \in 𝑵) \to 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B) \in 𝑵$
33		addpipq	$⊢ ((1^{st} (A) \in 𝑵 \land 2^{nd} (A) \in 𝑵) \land (y \in 𝑵 \land 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B) \in 𝑵)) \to ⟨1^{st} (A), 2^{nd} (A)⟩ +_{𝑝𝑸} ⟨y, 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)⟩ = ⟨(1^{st} (A) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B))) +_{𝑵} (y \cdot_{𝑵} 2^{nd} (A)), 2^{nd} (A) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B))⟩$
34	27 28 29 32 33	syl22anc	$⊢ ((A \in 𝑸 \land B \in 𝑸) \land y \in 𝑵) \to ⟨1^{st} (A), 2^{nd} (A)⟩ +_{𝑝𝑸} ⟨y, 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)⟩ = ⟨(1^{st} (A) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B))) +_{𝑵} (y \cdot_{𝑵} 2^{nd} (A)), 2^{nd} (A) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B))⟩$
35	26 34	eqtrd	$⊢ ((A \in 𝑸 \land B \in 𝑸) \land y \in 𝑵) \to A +_{𝑝𝑸} ⟨y, 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)⟩ = ⟨(1^{st} (A) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B))) +_{𝑵} (y \cdot_{𝑵} 2^{nd} (A)), 2^{nd} (A) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B))⟩$
36		oveq2	$⊢ (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} y = 1^{st} (B) \cdot_{𝑵} 2^{nd} (A) \to 2^{nd} (A) \cdot_{𝑵} ((1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} y) = 2^{nd} (A) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A))$
37		distrpi	$⊢ 2^{nd} (A) \cdot_{𝑵} ((1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} y) = (2^{nd} (A) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (B))) +_{𝑵} (2^{nd} (A) \cdot_{𝑵} y)$
38		fvex	$⊢ 2^{nd} (A) \in V$
39		fvex	$⊢ 1^{st} (A) \in V$
40		fvex	$⊢ 2^{nd} (B) \in V$
41		mulcompi	$⊢ x \cdot_{𝑵} y = y \cdot_{𝑵} x$
42		mulasspi	$⊢ (x \cdot_{𝑵} y) \cdot_{𝑵} z = x \cdot_{𝑵} (y \cdot_{𝑵} z)$
43	38 39 40 41 42	caov12	$⊢ 2^{nd} (A) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) = 1^{st} (A) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B))$
44		mulcompi	$⊢ 2^{nd} (A) \cdot_{𝑵} y = y \cdot_{𝑵} 2^{nd} (A)$
45	43 44	oveq12i	$⊢ (2^{nd} (A) \cdot_{𝑵} (1^{st} (A) \cdot_{𝑵} 2^{nd} (B))) +_{𝑵} (2^{nd} (A) \cdot_{𝑵} y) = (1^{st} (A) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B))) +_{𝑵} (y \cdot_{𝑵} 2^{nd} (A))$
46	37 45	eqtr2i	$⊢ (1^{st} (A) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B))) +_{𝑵} (y \cdot_{𝑵} 2^{nd} (A)) = 2^{nd} (A) \cdot_{𝑵} ((1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} y)$
47		mulasspi	$⊢ (2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 1^{st} (B) = 2^{nd} (A) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 1^{st} (B))$
48		mulcompi	$⊢ 2^{nd} (A) \cdot_{𝑵} 1^{st} (B) = 1^{st} (B) \cdot_{𝑵} 2^{nd} (A)$
49	48	oveq2i	$⊢ 2^{nd} (A) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 1^{st} (B)) = 2^{nd} (A) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A))$
50	47 49	eqtri	$⊢ (2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 1^{st} (B) = 2^{nd} (A) \cdot_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A))$
51	36 46 50	3eqtr4g	$⊢ (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} y = 1^{st} (B) \cdot_{𝑵} 2^{nd} (A) \to (1^{st} (A) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B))) +_{𝑵} (y \cdot_{𝑵} 2^{nd} (A)) = (2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 1^{st} (B)$
52		mulasspi	$⊢ (2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 2^{nd} (B) = 2^{nd} (A) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B))$
53	52	eqcomi	$⊢ 2^{nd} (A) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)) = (2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 2^{nd} (B)$
54	53	a1i	$⊢ (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} y = 1^{st} (B) \cdot_{𝑵} 2^{nd} (A) \to 2^{nd} (A) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)) = (2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 2^{nd} (B)$
55	51 54	opeq12d	$⊢ (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} y = 1^{st} (B) \cdot_{𝑵} 2^{nd} (A) \to ⟨(1^{st} (A) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B))) +_{𝑵} (y \cdot_{𝑵} 2^{nd} (A)), 2^{nd} (A) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B))⟩ = ⟨(2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 1^{st} (B), (2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 2^{nd} (B)⟩$
56	55	eqeq2d	$⊢ (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} y = 1^{st} (B) \cdot_{𝑵} 2^{nd} (A) \to (A +_{𝑝𝑸} ⟨y, 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)⟩ = ⟨(1^{st} (A) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B))) +_{𝑵} (y \cdot_{𝑵} 2^{nd} (A)), 2^{nd} (A) \cdot_{𝑵} (2^{nd} (A) \cdot_{𝑵} 2^{nd} (B))⟩ \leftrightarrow A +_{𝑝𝑸} ⟨y, 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)⟩ = ⟨(2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 1^{st} (B), (2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 2^{nd} (B)⟩)$
57	35 56	syl5ibcom	$⊢ ((A \in 𝑸 \land B \in 𝑸) \land y \in 𝑵) \to ((1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} y = 1^{st} (B) \cdot_{𝑵} 2^{nd} (A) \to A +_{𝑝𝑸} ⟨y, 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)⟩ = ⟨(2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 1^{st} (B), (2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 2^{nd} (B)⟩)$
58		fveq2	$⊢ A +_{𝑝𝑸} ⟨y, 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)⟩ = ⟨(2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 1^{st} (B), (2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 2^{nd} (B)⟩ \to /_{𝑸} (A +_{𝑝𝑸} ⟨y, 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)⟩) = /_{𝑸} (⟨(2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 1^{st} (B), (2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 2^{nd} (B)⟩)$
59		adderpq	$⊢ /_{𝑸} (A) +_{𝑸} /_{𝑸} (⟨y, 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)⟩) = /_{𝑸} (A +_{𝑝𝑸} ⟨y, 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)⟩)$
60		nqerid	$⊢ A \in 𝑸 \to /_{𝑸} (A) = A$
61	60	ad2antrr	$⊢ ((A \in 𝑸 \land B \in 𝑸) \land y \in 𝑵) \to /_{𝑸} (A) = A$
62	61	oveq1d	$⊢ ((A \in 𝑸 \land B \in 𝑸) \land y \in 𝑵) \to /_{𝑸} (A) +_{𝑸} /_{𝑸} (⟨y, 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)⟩) = A +_{𝑸} /_{𝑸} (⟨y, 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)⟩)$
63	59 62	syl5eqr	$⊢ ((A \in 𝑸 \land B \in 𝑸) \land y \in 𝑵) \to /_{𝑸} (A +_{𝑝𝑸} ⟨y, 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)⟩) = A +_{𝑸} /_{𝑸} (⟨y, 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)⟩)$
64		mulclpi	$⊢ (2^{nd} (A) \in 𝑵 \land 2^{nd} (A) \in 𝑵) \to 2^{nd} (A) \cdot_{𝑵} 2^{nd} (A) \in 𝑵$
65	17 17 64	syl2anc	$⊢ (A \in 𝑸 \land B \in 𝑸) \to 2^{nd} (A) \cdot_{𝑵} 2^{nd} (A) \in 𝑵$
66	65	adantr	$⊢ ((A \in 𝑸 \land B \in 𝑸) \land y \in 𝑵) \to 2^{nd} (A) \cdot_{𝑵} 2^{nd} (A) \in 𝑵$
67	15	adantr	$⊢ ((A \in 𝑸 \land B \in 𝑸) \land y \in 𝑵) \to 1^{st} (B) \in 𝑵$
68	11	adantr	$⊢ ((A \in 𝑸 \land B \in 𝑸) \land y \in 𝑵) \to 2^{nd} (B) \in 𝑵$
69		mulcanenq	$⊢ (2^{nd} (A) \cdot_{𝑵} 2^{nd} (A) \in 𝑵 \land 1^{st} (B) \in 𝑵 \land 2^{nd} (B) \in 𝑵) \to ⟨(2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 1^{st} (B), (2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 2^{nd} (B)⟩ ~_{𝑸} ⟨1^{st} (B), 2^{nd} (B)⟩$
70	66 67 68 69	syl3anc	$⊢ ((A \in 𝑸 \land B \in 𝑸) \land y \in 𝑵) \to ⟨(2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 1^{st} (B), (2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 2^{nd} (B)⟩ ~_{𝑸} ⟨1^{st} (B), 2^{nd} (B)⟩$
71	8	ad2antlr	$⊢ ((A \in 𝑸 \land B \in 𝑸) \land y \in 𝑵) \to B \in (𝑵 \times 𝑵)$
72		1st2nd	$⊢ (Rel (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵)) \to B = ⟨1^{st} (B), 2^{nd} (B)⟩$
73	22 71 72	sylancr	$⊢ ((A \in 𝑸 \land B \in 𝑸) \land y \in 𝑵) \to B = ⟨1^{st} (B), 2^{nd} (B)⟩$
74	70 73	breqtrrd	$⊢ ((A \in 𝑸 \land B \in 𝑸) \land y \in 𝑵) \to ⟨(2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 1^{st} (B), (2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 2^{nd} (B)⟩ ~_{𝑸} B$
75		mulclpi	$⊢ (2^{nd} (A) \cdot_{𝑵} 2^{nd} (A) \in 𝑵 \land 1^{st} (B) \in 𝑵) \to (2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 1^{st} (B) \in 𝑵$
76	66 67 75	syl2anc	$⊢ ((A \in 𝑸 \land B \in 𝑸) \land y \in 𝑵) \to (2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 1^{st} (B) \in 𝑵$
77		mulclpi	$⊢ (2^{nd} (A) \cdot_{𝑵} 2^{nd} (A) \in 𝑵 \land 2^{nd} (B) \in 𝑵) \to (2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 2^{nd} (B) \in 𝑵$
78	66 68 77	syl2anc	$⊢ ((A \in 𝑸 \land B \in 𝑸) \land y \in 𝑵) \to (2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 2^{nd} (B) \in 𝑵$
79	76 78	opelxpd	$⊢ ((A \in 𝑸 \land B \in 𝑸) \land y \in 𝑵) \to ⟨(2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 1^{st} (B), (2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 2^{nd} (B)⟩ \in (𝑵 \times 𝑵)$
80		nqereq	$⊢ (⟨(2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 1^{st} (B), (2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 2^{nd} (B)⟩ \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵)) \to (⟨(2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 1^{st} (B), (2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 2^{nd} (B)⟩ ~_{𝑸} B \leftrightarrow /_{𝑸} (⟨(2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 1^{st} (B), (2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 2^{nd} (B)⟩) = /_{𝑸} (B))$
81	79 71 80	syl2anc	$⊢ ((A \in 𝑸 \land B \in 𝑸) \land y \in 𝑵) \to (⟨(2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 1^{st} (B), (2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 2^{nd} (B)⟩ ~_{𝑸} B \leftrightarrow /_{𝑸} (⟨(2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 1^{st} (B), (2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 2^{nd} (B)⟩) = /_{𝑸} (B))$
82	74 81	mpbid	$⊢ ((A \in 𝑸 \land B \in 𝑸) \land y \in 𝑵) \to /_{𝑸} (⟨(2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 1^{st} (B), (2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 2^{nd} (B)⟩) = /_{𝑸} (B)$
83		nqerid	$⊢ B \in 𝑸 \to /_{𝑸} (B) = B$
84	83	ad2antlr	$⊢ ((A \in 𝑸 \land B \in 𝑸) \land y \in 𝑵) \to /_{𝑸} (B) = B$
85	82 84	eqtrd	$⊢ ((A \in 𝑸 \land B \in 𝑸) \land y \in 𝑵) \to /_{𝑸} (⟨(2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 1^{st} (B), (2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 2^{nd} (B)⟩) = B$
86	63 85	eqeq12d	$⊢ ((A \in 𝑸 \land B \in 𝑸) \land y \in 𝑵) \to (/_{𝑸} (A +_{𝑝𝑸} ⟨y, 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)⟩) = /_{𝑸} (⟨(2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 1^{st} (B), (2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 2^{nd} (B)⟩) \leftrightarrow A +_{𝑸} /_{𝑸} (⟨y, 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)⟩) = B)$
87	58 86	syl5ib	$⊢ ((A \in 𝑸 \land B \in 𝑸) \land y \in 𝑵) \to (A +_{𝑝𝑸} ⟨y, 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)⟩ = ⟨(2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 1^{st} (B), (2^{nd} (A) \cdot_{𝑵} 2^{nd} (A)) \cdot_{𝑵} 2^{nd} (B)⟩ \to A +_{𝑸} /_{𝑸} (⟨y, 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)⟩) = B)$
88	57 87	syld	$⊢ ((A \in 𝑸 \land B \in 𝑸) \land y \in 𝑵) \to ((1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} y = 1^{st} (B) \cdot_{𝑵} 2^{nd} (A) \to A +_{𝑸} /_{𝑸} (⟨y, 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)⟩) = B)$
89		fvex	$⊢ /_{𝑸} (⟨y, 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)⟩) \in V$
90		oveq2	$⊢ x = /_{𝑸} (⟨y, 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)⟩) \to A +_{𝑸} x = A +_{𝑸} /_{𝑸} (⟨y, 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)⟩)$
91	90	eqeq1d	$⊢ x = /_{𝑸} (⟨y, 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)⟩) \to (A +_{𝑸} x = B \leftrightarrow A +_{𝑸} /_{𝑸} (⟨y, 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)⟩) = B)$
92	89 91	spcev	$⊢ A +_{𝑸} /_{𝑸} (⟨y, 2^{nd} (A) \cdot_{𝑵} 2^{nd} (B)⟩) = B \to \exists x A +_{𝑸} x = B$
93	88 92	syl6	$⊢ ((A \in 𝑸 \land B \in 𝑸) \land y \in 𝑵) \to ((1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} y = 1^{st} (B) \cdot_{𝑵} 2^{nd} (A) \to \exists x A +_{𝑸} x = B)$
94	93	rexlimdva	$⊢ (A \in 𝑸 \land B \in 𝑸) \to (\exists y \in 𝑵 (1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) +_{𝑵} y = 1^{st} (B) \cdot_{𝑵} 2^{nd} (A) \to \exists x A +_{𝑸} x = B)$
95	21 94	sylbid	$⊢ (A \in 𝑸 \land B \in 𝑸) \to ((1^{st} (A) \cdot_{𝑵} 2^{nd} (B)) <_{𝑵} (1^{st} (B) \cdot_{𝑵} 2^{nd} (A)) \to \exists x A +_{𝑸} x = B)$
96	3 95	sylbid	$⊢ (A \in 𝑸 \land B \in 𝑸) \to (A <_{𝑸} B \to \exists x A +_{𝑸} x = B)$
97	2 96	mpcom	$⊢ A <_{𝑸} B \to \exists x A +_{𝑸} x = B$
98		eleq1	$⊢ A +_{𝑸} x = B \to (A +_{𝑸} x \in 𝑸 \leftrightarrow B \in 𝑸)$
99	98	biimparc	$⊢ (B \in 𝑸 \land A +_{𝑸} x = B) \to A +_{𝑸} x \in 𝑸$
100		addnqf	$⊢ +_{𝑸} : 𝑸 \times 𝑸 ⟶ 𝑸$
101	100	fdmi	$⊢ dom +_{𝑸} = 𝑸 \times 𝑸$
102		0nnq	$⊢ \neg \emptyset \in 𝑸$
103	101 102	ndmovrcl	$⊢ A +_{𝑸} x \in 𝑸 \to (A \in 𝑸 \land x \in 𝑸)$
104		ltaddnq	$⊢ (A \in 𝑸 \land x \in 𝑸) \to A <_{𝑸} (A +_{𝑸} x)$
105	99 103 104	3syl	$⊢ (B \in 𝑸 \land A +_{𝑸} x = B) \to A <_{𝑸} (A +_{𝑸} x)$
106		simpr	$⊢ (B \in 𝑸 \land A +_{𝑸} x = B) \to A +_{𝑸} x = B$
107	105 106	breqtrd	$⊢ (B \in 𝑸 \land A +_{𝑸} x = B) \to A <_{𝑸} B$
108	107	ex	$⊢ B \in 𝑸 \to (A +_{𝑸} x = B \to A <_{𝑸} B)$
109	108	exlimdv	$⊢ B \in 𝑸 \to (\exists x A +_{𝑸} x = B \to A <_{𝑸} B)$
110	97 109	impbid2	$⊢ B \in 𝑸 \to (A <_{𝑸} B \leftrightarrow \exists x A +_{𝑸} x = B)$

Metamath Proof Explorer

Theorem ltexnq

Proof