Metamath Proof Explorer


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 syl5ib ( ( ( 𝐴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 𝑥 ) = 𝐵 ) )