Theorem 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	⊢ ( 𝐵 ∈ Q → ( 𝐴 <Q 𝐵 ↔ ∃ 𝑥 ( 𝐴 +Q 𝑥 ) = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ltrelnq	⊢ <Q ⊆ ( Q × Q )
2	1	brel	⊢ ( 𝐴 <Q 𝐵 → ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) )
3		ordpinq	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → ( 𝐴 <Q 𝐵 ↔ ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) <N ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) ) )
4		elpqn	⊢ ( 𝐴 ∈ Q → 𝐴 ∈ ( N × N ) )
5	4	adantr	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → 𝐴 ∈ ( N × N ) )
6		xp1st	⊢ ( 𝐴 ∈ ( N × N ) → ( 1st ‘ 𝐴 ) ∈ N )
7	5 6	syl	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → ( 1st ‘ 𝐴 ) ∈ N )
8		elpqn	⊢ ( 𝐵 ∈ Q → 𝐵 ∈ ( N × N ) )
9	8	adantl	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → 𝐵 ∈ ( N × N ) )
10		xp2nd	⊢ ( 𝐵 ∈ ( N × N ) → ( 2nd ‘ 𝐵 ) ∈ N )
11	9 10	syl	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → ( 2nd ‘ 𝐵 ) ∈ N )
12		mulclpi	⊢ ( ( ( 1st ‘ 𝐴 ) ∈ N ∧ ( 2nd ‘ 𝐵 ) ∈ N ) → ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ∈ N )
13	7 11 12	syl2anc	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ∈ N )
14		xp1st	⊢ ( 𝐵 ∈ ( N × N ) → ( 1st ‘ 𝐵 ) ∈ N )
15	9 14	syl	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → ( 1st ‘ 𝐵 ) ∈ N )
16		xp2nd	⊢ ( 𝐴 ∈ ( N × N ) → ( 2nd ‘ 𝐴 ) ∈ N )
17	5 16	syl	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → ( 2nd ‘ 𝐴 ) ∈ N )
18		mulclpi	⊢ ( ( ( 1st ‘ 𝐵 ) ∈ N ∧ ( 2nd ‘ 𝐴 ) ∈ N ) → ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) ∈ N )
19	15 17 18	syl2anc	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) ∈ N )
20		ltexpi	⊢ ( ( ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ∈ N ∧ ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) ∈ N ) → ( ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) <N ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) ↔ ∃ 𝑦 ∈ N ( ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) +N 𝑦 ) = ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) ) )
21	13 19 20	syl2anc	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → ( ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) <N ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) ↔ ∃ 𝑦 ∈ N ( ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) +N 𝑦 ) = ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) ) )
22		relxp	⊢ Rel ( N × N )
23	4	ad2antrr	⊢ ( ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) ∧ 𝑦 ∈ N ) → 𝐴 ∈ ( N × N ) )
24		1st2nd	⊢ ( ( Rel ( N × N ) ∧ 𝐴 ∈ ( N × N ) ) → 𝐴 = ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ )
25	22 23 24	sylancr	⊢ ( ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) ∧ 𝑦 ∈ N ) → 𝐴 = ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ )
26	25	oveq1d	⊢ ( ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) ∧ 𝑦 ∈ N ) → ( 𝐴 +pQ ⟨ 𝑦 , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ ) = ( ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ +pQ ⟨ 𝑦 , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ ) )
27	7	adantr	⊢ ( ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) ∧ 𝑦 ∈ N ) → ( 1st ‘ 𝐴 ) ∈ N )
28	17	adantr	⊢ ( ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) ∧ 𝑦 ∈ N ) → ( 2nd ‘ 𝐴 ) ∈ N )
29		simpr	⊢ ( ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) ∧ 𝑦 ∈ N ) → 𝑦 ∈ N )
30		mulclpi	⊢ ( ( ( 2nd ‘ 𝐴 ) ∈ N ∧ ( 2nd ‘ 𝐵 ) ∈ N ) → ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ∈ N )
31	17 11 30	syl2anc	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ∈ N )
32	31	adantr	⊢ ( ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) ∧ 𝑦 ∈ N ) → ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ∈ N )
33		addpipq	⊢ ( ( ( ( 1st ‘ 𝐴 ) ∈ N ∧ ( 2nd ‘ 𝐴 ) ∈ N ) ∧ ( 𝑦 ∈ N ∧ ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ∈ N ) ) → ( ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ +pQ ⟨ 𝑦 , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ ) = ⟨ ( ( ( 1st ‘ 𝐴 ) ·N ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ) +N ( 𝑦 ·N ( 2nd ‘ 𝐴 ) ) ) , ( ( 2nd ‘ 𝐴 ) ·N ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ) ⟩ )
34	27 28 29 32 33	syl22anc	⊢ ( ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) ∧ 𝑦 ∈ N ) → ( ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ +pQ ⟨ 𝑦 , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ ) = ⟨ ( ( ( 1st ‘ 𝐴 ) ·N ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ) +N ( 𝑦 ·N ( 2nd ‘ 𝐴 ) ) ) , ( ( 2nd ‘ 𝐴 ) ·N ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ) ⟩ )
35	26 34	eqtrd	⊢ ( ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) ∧ 𝑦 ∈ N ) → ( 𝐴 +pQ ⟨ 𝑦 , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ ) = ⟨ ( ( ( 1st ‘ 𝐴 ) ·N ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ) +N ( 𝑦 ·N ( 2nd ‘ 𝐴 ) ) ) , ( ( 2nd ‘ 𝐴 ) ·N ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ) ⟩ )
36		oveq2	⊢ ( ( ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) +N 𝑦 ) = ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) → ( ( 2nd ‘ 𝐴 ) ·N ( ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) +N 𝑦 ) ) = ( ( 2nd ‘ 𝐴 ) ·N ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) ) )
37		distrpi	⊢ ( ( 2nd ‘ 𝐴 ) ·N ( ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) +N 𝑦 ) ) = ( ( ( 2nd ‘ 𝐴 ) ·N ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ) +N ( ( 2nd ‘ 𝐴 ) ·N 𝑦 ) )
38		fvex	⊢ ( 2nd ‘ 𝐴 ) ∈ V
39		fvex	⊢ ( 1st ‘ 𝐴 ) ∈ V
40		fvex	⊢ ( 2nd ‘ 𝐵 ) ∈ V
41		mulcompi	⊢ ( 𝑥 ·N 𝑦 ) = ( 𝑦 ·N 𝑥 )
42		mulasspi	⊢ ( ( 𝑥 ·N 𝑦 ) ·N 𝑧 ) = ( 𝑥 ·N ( 𝑦 ·N 𝑧 ) )
43	38 39 40 41 42	caov12	⊢ ( ( 2nd ‘ 𝐴 ) ·N ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ) = ( ( 1st ‘ 𝐴 ) ·N ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) )
44		mulcompi	⊢ ( ( 2nd ‘ 𝐴 ) ·N 𝑦 ) = ( 𝑦 ·N ( 2nd ‘ 𝐴 ) )
45	43 44	oveq12i	⊢ ( ( ( 2nd ‘ 𝐴 ) ·N ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ) +N ( ( 2nd ‘ 𝐴 ) ·N 𝑦 ) ) = ( ( ( 1st ‘ 𝐴 ) ·N ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ) +N ( 𝑦 ·N ( 2nd ‘ 𝐴 ) ) )
46	37 45	eqtr2i	⊢ ( ( ( 1st ‘ 𝐴 ) ·N ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ) +N ( 𝑦 ·N ( 2nd ‘ 𝐴 ) ) ) = ( ( 2nd ‘ 𝐴 ) ·N ( ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) +N 𝑦 ) )
47		mulasspi	⊢ ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 1st ‘ 𝐵 ) ) = ( ( 2nd ‘ 𝐴 ) ·N ( ( 2nd ‘ 𝐴 ) ·N ( 1st ‘ 𝐵 ) ) )
48		mulcompi	⊢ ( ( 2nd ‘ 𝐴 ) ·N ( 1st ‘ 𝐵 ) ) = ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) )
49	48	oveq2i	⊢ ( ( 2nd ‘ 𝐴 ) ·N ( ( 2nd ‘ 𝐴 ) ·N ( 1st ‘ 𝐵 ) ) ) = ( ( 2nd ‘ 𝐴 ) ·N ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) )
50	47 49	eqtri	⊢ ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 1st ‘ 𝐵 ) ) = ( ( 2nd ‘ 𝐴 ) ·N ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) )
51	36 46 50	3eqtr4g	⊢ ( ( ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) +N 𝑦 ) = ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) → ( ( ( 1st ‘ 𝐴 ) ·N ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ) +N ( 𝑦 ·N ( 2nd ‘ 𝐴 ) ) ) = ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 1st ‘ 𝐵 ) ) )
52		mulasspi	⊢ ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 2nd ‘ 𝐵 ) ) = ( ( 2nd ‘ 𝐴 ) ·N ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) )
53	52	eqcomi	⊢ ( ( 2nd ‘ 𝐴 ) ·N ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ) = ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 2nd ‘ 𝐵 ) )
54	53	a1i	⊢ ( ( ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) +N 𝑦 ) = ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) → ( ( 2nd ‘ 𝐴 ) ·N ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ) = ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 2nd ‘ 𝐵 ) ) )
55	51 54	opeq12d	⊢ ( ( ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) +N 𝑦 ) = ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) → ⟨ ( ( ( 1st ‘ 𝐴 ) ·N ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ) +N ( 𝑦 ·N ( 2nd ‘ 𝐴 ) ) ) , ( ( 2nd ‘ 𝐴 ) ·N ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ) ⟩ = ⟨ ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 1st ‘ 𝐵 ) ) , ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ )
56	55	eqeq2d	⊢ ( ( ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) +N 𝑦 ) = ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) → ( ( 𝐴 +pQ ⟨ 𝑦 , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ ) = ⟨ ( ( ( 1st ‘ 𝐴 ) ·N ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ) +N ( 𝑦 ·N ( 2nd ‘ 𝐴 ) ) ) , ( ( 2nd ‘ 𝐴 ) ·N ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ) ⟩ ↔ ( 𝐴 +pQ ⟨ 𝑦 , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ ) = ⟨ ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 1st ‘ 𝐵 ) ) , ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ ) )
57	35 56	syl5ibcom	⊢ ( ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) ∧ 𝑦 ∈ N ) → ( ( ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) +N 𝑦 ) = ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) → ( 𝐴 +pQ ⟨ 𝑦 , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ ) = ⟨ ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 1st ‘ 𝐵 ) ) , ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ ) )
58		fveq2	⊢ ( ( 𝐴 +pQ ⟨ 𝑦 , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ ) = ⟨ ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 1st ‘ 𝐵 ) ) , ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ → ( [Q] ‘ ( 𝐴 +pQ ⟨ 𝑦 , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ ) ) = ( [Q] ‘ ⟨ ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 1st ‘ 𝐵 ) ) , ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ ) )
59		adderpq	⊢ ( ( [Q] ‘ 𝐴 ) +Q ( [Q] ‘ ⟨ 𝑦 , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ ) ) = ( [Q] ‘ ( 𝐴 +pQ ⟨ 𝑦 , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ ) )
60		nqerid	⊢ ( 𝐴 ∈ Q → ( [Q] ‘ 𝐴 ) = 𝐴 )
61	60	ad2antrr	⊢ ( ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) ∧ 𝑦 ∈ N ) → ( [Q] ‘ 𝐴 ) = 𝐴 )
62	61	oveq1d	⊢ ( ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) ∧ 𝑦 ∈ N ) → ( ( [Q] ‘ 𝐴 ) +Q ( [Q] ‘ ⟨ 𝑦 , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ ) ) = ( 𝐴 +Q ( [Q] ‘ ⟨ 𝑦 , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ ) ) )
63	59 62	eqtr3id	⊢ ( ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) ∧ 𝑦 ∈ N ) → ( [Q] ‘ ( 𝐴 +pQ ⟨ 𝑦 , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ ) ) = ( 𝐴 +Q ( [Q] ‘ ⟨ 𝑦 , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ ) ) )
64		mulclpi	⊢ ( ( ( 2nd ‘ 𝐴 ) ∈ N ∧ ( 2nd ‘ 𝐴 ) ∈ N ) → ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ∈ N )
65	17 17 64	syl2anc	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ∈ N )
66	65	adantr	⊢ ( ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) ∧ 𝑦 ∈ N ) → ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ∈ N )
67	15	adantr	⊢ ( ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) ∧ 𝑦 ∈ N ) → ( 1st ‘ 𝐵 ) ∈ N )
68	11	adantr	⊢ ( ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) ∧ 𝑦 ∈ N ) → ( 2nd ‘ 𝐵 ) ∈ N )
69		mulcanenq	⊢ ( ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ∈ N ∧ ( 1st ‘ 𝐵 ) ∈ N ∧ ( 2nd ‘ 𝐵 ) ∈ N ) → ⟨ ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 1st ‘ 𝐵 ) ) , ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ ~Q ⟨ ( 1st ‘ 𝐵 ) , ( 2nd ‘ 𝐵 ) ⟩ )
70	66 67 68 69	syl3anc	⊢ ( ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) ∧ 𝑦 ∈ N ) → ⟨ ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 1st ‘ 𝐵 ) ) , ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ ~Q ⟨ ( 1st ‘ 𝐵 ) , ( 2nd ‘ 𝐵 ) ⟩ )
71	8	ad2antlr	⊢ ( ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) ∧ 𝑦 ∈ N ) → 𝐵 ∈ ( N × N ) )
72		1st2nd	⊢ ( ( Rel ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → 𝐵 = ⟨ ( 1st ‘ 𝐵 ) , ( 2nd ‘ 𝐵 ) ⟩ )
73	22 71 72	sylancr	⊢ ( ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) ∧ 𝑦 ∈ N ) → 𝐵 = ⟨ ( 1st ‘ 𝐵 ) , ( 2nd ‘ 𝐵 ) ⟩ )
74	70 73	breqtrrd	⊢ ( ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) ∧ 𝑦 ∈ N ) → ⟨ ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 1st ‘ 𝐵 ) ) , ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ ~Q 𝐵 )
75		mulclpi	⊢ ( ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ∈ N ∧ ( 1st ‘ 𝐵 ) ∈ N ) → ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 1st ‘ 𝐵 ) ) ∈ N )
76	66 67 75	syl2anc	⊢ ( ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) ∧ 𝑦 ∈ N ) → ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 1st ‘ 𝐵 ) ) ∈ N )
77		mulclpi	⊢ ( ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ∈ N ∧ ( 2nd ‘ 𝐵 ) ∈ N ) → ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 2nd ‘ 𝐵 ) ) ∈ N )
78	66 68 77	syl2anc	⊢ ( ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) ∧ 𝑦 ∈ N ) → ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 2nd ‘ 𝐵 ) ) ∈ N )
79	76 78	opelxpd	⊢ ( ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) ∧ 𝑦 ∈ N ) → ⟨ ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 1st ‘ 𝐵 ) ) , ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ ∈ ( N × N ) )
80		nqereq	⊢ ( ( ⟨ ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 1st ‘ 𝐵 ) ) , ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( ⟨ ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 1st ‘ 𝐵 ) ) , ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ ~Q 𝐵 ↔ ( [Q] ‘ ⟨ ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 1st ‘ 𝐵 ) ) , ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ ) = ( [Q] ‘ 𝐵 ) ) )
81	79 71 80	syl2anc	⊢ ( ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) ∧ 𝑦 ∈ N ) → ( ⟨ ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 1st ‘ 𝐵 ) ) , ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ ~Q 𝐵 ↔ ( [Q] ‘ ⟨ ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 1st ‘ 𝐵 ) ) , ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ ) = ( [Q] ‘ 𝐵 ) ) )
82	74 81	mpbid	⊢ ( ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) ∧ 𝑦 ∈ N ) → ( [Q] ‘ ⟨ ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 1st ‘ 𝐵 ) ) , ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ ) = ( [Q] ‘ 𝐵 ) )
83		nqerid	⊢ ( 𝐵 ∈ Q → ( [Q] ‘ 𝐵 ) = 𝐵 )
84	83	ad2antlr	⊢ ( ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) ∧ 𝑦 ∈ N ) → ( [Q] ‘ 𝐵 ) = 𝐵 )
85	82 84	eqtrd	⊢ ( ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) ∧ 𝑦 ∈ N ) → ( [Q] ‘ ⟨ ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 1st ‘ 𝐵 ) ) , ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ ) = 𝐵 )
86	63 85	eqeq12d	⊢ ( ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) ∧ 𝑦 ∈ N ) → ( ( [Q] ‘ ( 𝐴 +pQ ⟨ 𝑦 , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ ) ) = ( [Q] ‘ ⟨ ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 1st ‘ 𝐵 ) ) , ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ ) ↔ ( 𝐴 +Q ( [Q] ‘ ⟨ 𝑦 , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ ) ) = 𝐵 ) )
87	58 86	imbitrid	⊢ ( ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) ∧ 𝑦 ∈ N ) → ( ( 𝐴 +pQ ⟨ 𝑦 , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ ) = ⟨ ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 1st ‘ 𝐵 ) ) , ( ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐴 ) ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ → ( 𝐴 +Q ( [Q] ‘ ⟨ 𝑦 , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ ) ) = 𝐵 ) )
88	57 87	syld	⊢ ( ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) ∧ 𝑦 ∈ N ) → ( ( ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) +N 𝑦 ) = ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) → ( 𝐴 +Q ( [Q] ‘ ⟨ 𝑦 , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ ) ) = 𝐵 ) )
89		fvex	⊢ ( [Q] ‘ ⟨ 𝑦 , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ ) ∈ V
90		oveq2	⊢ ( 𝑥 = ( [Q] ‘ ⟨ 𝑦 , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ ) → ( 𝐴 +Q 𝑥 ) = ( 𝐴 +Q ( [Q] ‘ ⟨ 𝑦 , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ ) ) )
91	90	eqeq1d	⊢ ( 𝑥 = ( [Q] ‘ ⟨ 𝑦 , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ ) → ( ( 𝐴 +Q 𝑥 ) = 𝐵 ↔ ( 𝐴 +Q ( [Q] ‘ ⟨ 𝑦 , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ ) ) = 𝐵 ) )
92	89 91	spcev	⊢ ( ( 𝐴 +Q ( [Q] ‘ ⟨ 𝑦 , ( ( 2nd ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) ⟩ ) ) = 𝐵 → ∃ 𝑥 ( 𝐴 +Q 𝑥 ) = 𝐵 )
93	88 92	syl6	⊢ ( ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) ∧ 𝑦 ∈ N ) → ( ( ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) +N 𝑦 ) = ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) → ∃ 𝑥 ( 𝐴 +Q 𝑥 ) = 𝐵 ) )
94	93	rexlimdva	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → ( ∃ 𝑦 ∈ N ( ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) +N 𝑦 ) = ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) → ∃ 𝑥 ( 𝐴 +Q 𝑥 ) = 𝐵 ) )
95	21 94	sylbid	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → ( ( ( 1st ‘ 𝐴 ) ·N ( 2nd ‘ 𝐵 ) ) <N ( ( 1st ‘ 𝐵 ) ·N ( 2nd ‘ 𝐴 ) ) → ∃ 𝑥 ( 𝐴 +Q 𝑥 ) = 𝐵 ) )
96	3 95	sylbid	⊢ ( ( 𝐴 ∈ Q ∧ 𝐵 ∈ Q ) → ( 𝐴 <Q 𝐵 → ∃ 𝑥 ( 𝐴 +Q 𝑥 ) = 𝐵 ) )
97	2 96	mpcom	⊢ ( 𝐴 <Q 𝐵 → ∃ 𝑥 ( 𝐴 +Q 𝑥 ) = 𝐵 )
98		eleq1	⊢ ( ( 𝐴 +Q 𝑥 ) = 𝐵 → ( ( 𝐴 +Q 𝑥 ) ∈ Q ↔ 𝐵 ∈ Q ) )
99	98	biimparc	⊢ ( ( 𝐵 ∈ Q ∧ ( 𝐴 +Q 𝑥 ) = 𝐵 ) → ( 𝐴 +Q 𝑥 ) ∈ Q )
100		addnqf	⊢ +Q : ( Q × Q ) ⟶ Q
101	100	fdmi	⊢ dom +Q = ( Q × Q )
102		0nnq	⊢ ¬ ∅ ∈ Q
103	101 102	ndmovrcl	⊢ ( ( 𝐴 +Q 𝑥 ) ∈ Q → ( 𝐴 ∈ Q ∧ 𝑥 ∈ Q ) )
104		ltaddnq	⊢ ( ( 𝐴 ∈ Q ∧ 𝑥 ∈ Q ) → 𝐴 <Q ( 𝐴 +Q 𝑥 ) )
105	99 103 104	3syl	⊢ ( ( 𝐵 ∈ Q ∧ ( 𝐴 +Q 𝑥 ) = 𝐵 ) → 𝐴 <Q ( 𝐴 +Q 𝑥 ) )
106		simpr	⊢ ( ( 𝐵 ∈ Q ∧ ( 𝐴 +Q 𝑥 ) = 𝐵 ) → ( 𝐴 +Q 𝑥 ) = 𝐵 )
107	105 106	breqtrd	⊢ ( ( 𝐵 ∈ Q ∧ ( 𝐴 +Q 𝑥 ) = 𝐵 ) → 𝐴 <Q 𝐵 )
108	107	ex	⊢ ( 𝐵 ∈ Q → ( ( 𝐴 +Q 𝑥 ) = 𝐵 → 𝐴 <Q 𝐵 ) )
109	108	exlimdv	⊢ ( 𝐵 ∈ Q → ( ∃ 𝑥 ( 𝐴 +Q 𝑥 ) = 𝐵 → 𝐴 <Q 𝐵 ) )
110	97 109	impbid2	⊢ ( 𝐵 ∈ Q → ( 𝐴 <Q 𝐵 ↔ ∃ 𝑥 ( 𝐴 +Q 𝑥 ) = 𝐵 ) )