This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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