Metamath Proof Explorer

Theorem prlem936

Description: Lemma 9-3.6 of Gleason p. 124. (Contributed by NM, 26-Apr-1996) (Revised by Mario Carneiro, 12-Jun-2013) (New usage is discouraged.)

Ref Expression
Assertion prlem936 ( ( 𝐴 ∈ P ∧ 1Q <Q 𝐵 ) → ∃ 𝑥 ∈ 𝐴 ¬ ( 𝑥 ·Q 𝐵 ) ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 ltrelnq ⊢ <Q ⊆ ( Q × Q )
2 1 brel ⊢ ( 1Q <Q 𝐵 → ( 1Q ∈ Q ∧ 𝐵 ∈ Q ) )
3 2 simprd ⊢ ( 1Q <Q 𝐵 → 𝐵 ∈ Q )
4 3 adantl ⊢ ( ( 𝐴 ∈ P ∧ 1Q <Q 𝐵 ) → 𝐵 ∈ Q )
5 breq2 ⊢ ( 𝑏 = 𝐵 → ( 1Q <Q 𝑏 ↔ 1Q <Q 𝐵 ) )
6 5 anbi2d ⊢ ( 𝑏 = 𝐵 → ( ( 𝐴 ∈ P ∧ 1Q <Q 𝑏 ) ↔ ( 𝐴 ∈ P ∧ 1Q <Q 𝐵 ) ) )
7 oveq2 ⊢ ( 𝑏 = 𝐵 → ( 𝑥 ·Q 𝑏 ) = ( 𝑥 ·Q 𝐵 ) )
8 7 eleq1d ⊢ ( 𝑏 = 𝐵 → ( ( 𝑥 ·Q 𝑏 ) ∈ 𝐴 ↔ ( 𝑥 ·Q 𝐵 ) ∈ 𝐴 ) )
9 8 notbid ⊢ ( 𝑏 = 𝐵 → ( ¬ ( 𝑥 ·Q 𝑏 ) ∈ 𝐴 ↔ ¬ ( 𝑥 ·Q 𝐵 ) ∈ 𝐴 ) )
10 9 rexbidv ⊢ ( 𝑏 = 𝐵 → ( ∃ 𝑥 ∈ 𝐴 ¬ ( 𝑥 ·Q 𝑏 ) ∈ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 ¬ ( 𝑥 ·Q 𝐵 ) ∈ 𝐴 ) )
11 6 10 imbi12d ⊢ ( 𝑏 = 𝐵 → ( ( ( 𝐴 ∈ P ∧ 1Q <Q 𝑏 ) → ∃ 𝑥 ∈ 𝐴 ¬ ( 𝑥 ·Q 𝑏 ) ∈ 𝐴 ) ↔ ( ( 𝐴 ∈ P ∧ 1Q <Q 𝐵 ) → ∃ 𝑥 ∈ 𝐴 ¬ ( 𝑥 ·Q 𝐵 ) ∈ 𝐴 ) ) )
12 prn0 ⊢ ( 𝐴 ∈ P → 𝐴 ≠ ∅ )
13 n0 ⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ 𝐴 )
14 12 13 sylib ⊢ ( 𝐴 ∈ P → ∃ 𝑦 𝑦 ∈ 𝐴 )
15 14 adantr ⊢ ( ( 𝐴 ∈ P ∧ 1Q <Q 𝑏 ) → ∃ 𝑦 𝑦 ∈ 𝐴 )
16 elprnq ⊢ ( ( 𝐴 ∈ P ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ Q )
17 16 ad2ant2r ⊢ ( ( ( 𝐴 ∈ P ∧ 1Q <Q 𝑏 ) ∧ ( 𝑦 ∈ 𝐴 ∧ ( 𝑦 ·Q 𝑏 ) ∈ 𝐴 ) ) → 𝑦 ∈ Q )
18 mulidnq ⊢ ( 𝑦 ∈ Q → ( 𝑦 ·Q 1Q ) = 𝑦 )
19 17 18 syl ⊢ ( ( ( 𝐴 ∈ P ∧ 1Q <Q 𝑏 ) ∧ ( 𝑦 ∈ 𝐴 ∧ ( 𝑦 ·Q 𝑏 ) ∈ 𝐴 ) ) → ( 𝑦 ·Q 1Q ) = 𝑦 )
20 simplr ⊢ ( ( ( 𝐴 ∈ P ∧ 1Q <Q 𝑏 ) ∧ ( 𝑦 ∈ 𝐴 ∧ ( 𝑦 ·Q 𝑏 ) ∈ 𝐴 ) ) → 1Q <Q 𝑏 )
21 ltmnq ⊢ ( 𝑦 ∈ Q → ( 1Q <Q 𝑏 ↔ ( 𝑦 ·Q 1Q ) <Q ( 𝑦 ·Q 𝑏 ) ) )
22 21 biimpa ⊢ ( ( 𝑦 ∈ Q ∧ 1Q <Q 𝑏 ) → ( 𝑦 ·Q 1Q ) <Q ( 𝑦 ·Q 𝑏 ) )
23 17 20 22 syl2anc ⊢ ( ( ( 𝐴 ∈ P ∧ 1Q <Q 𝑏 ) ∧ ( 𝑦 ∈ 𝐴 ∧ ( 𝑦 ·Q 𝑏 ) ∈ 𝐴 ) ) → ( 𝑦 ·Q 1Q ) <Q ( 𝑦 ·Q 𝑏 ) )
24 19 23 eqbrtrrd ⊢ ( ( ( 𝐴 ∈ P ∧ 1Q <Q 𝑏 ) ∧ ( 𝑦 ∈ 𝐴 ∧ ( 𝑦 ·Q 𝑏 ) ∈ 𝐴 ) ) → 𝑦 <Q ( 𝑦 ·Q 𝑏 ) )
25 1 brel ⊢ ( 1Q <Q 𝑏 → ( 1Q ∈ Q ∧ 𝑏 ∈ Q ) )
26 25 simprd ⊢ ( 1Q <Q 𝑏 → 𝑏 ∈ Q )
27 26 ad2antlr ⊢ ( ( ( 𝐴 ∈ P ∧ 1Q <Q 𝑏 ) ∧ ( 𝑦 ∈ 𝐴 ∧ ( 𝑦 ·Q 𝑏 ) ∈ 𝐴 ) ) → 𝑏 ∈ Q )
28 mulclnq ⊢ ( ( 𝑦 ∈ Q ∧ 𝑏 ∈ Q ) → ( 𝑦 ·Q 𝑏 ) ∈ Q )
29 17 27 28 syl2anc ⊢ ( ( ( 𝐴 ∈ P ∧ 1Q <Q 𝑏 ) ∧ ( 𝑦 ∈ 𝐴 ∧ ( 𝑦 ·Q 𝑏 ) ∈ 𝐴 ) ) → ( 𝑦 ·Q 𝑏 ) ∈ Q )
30 ltexnq ⊢ ( ( 𝑦 ·Q 𝑏 ) ∈ Q → ( 𝑦 <Q ( 𝑦 ·Q 𝑏 ) ↔ ∃ 𝑧 ( 𝑦 +Q 𝑧 ) = ( 𝑦 ·Q 𝑏 ) ) )
31 29 30 syl ⊢ ( ( ( 𝐴 ∈ P ∧ 1Q <Q 𝑏 ) ∧ ( 𝑦 ∈ 𝐴 ∧ ( 𝑦 ·Q 𝑏 ) ∈ 𝐴 ) ) → ( 𝑦 <Q ( 𝑦 ·Q 𝑏 ) ↔ ∃ 𝑧 ( 𝑦 +Q 𝑧 ) = ( 𝑦 ·Q 𝑏 ) ) )
32 24 31 mpbid ⊢ ( ( ( 𝐴 ∈ P ∧ 1Q <Q 𝑏 ) ∧ ( 𝑦 ∈ 𝐴 ∧ ( 𝑦 ·Q 𝑏 ) ∈ 𝐴 ) ) → ∃ 𝑧 ( 𝑦 +Q 𝑧 ) = ( 𝑦 ·Q 𝑏 ) )
33 simplll ⊢ ( ( ( ( 𝐴 ∈ P ∧ 1Q <Q 𝑏 ) ∧ ( 𝑦 ∈ 𝐴 ∧ ( 𝑦 ·Q 𝑏 ) ∈ 𝐴 ) ) ∧ ( 𝑦 +Q 𝑧 ) = ( 𝑦 ·Q 𝑏 ) ) → 𝐴 ∈ P )
34 vex ⊢ 𝑧 ∈ V
35 34 prlem934 ⊢ ( 𝐴 ∈ P → ∃ 𝑥 ∈ 𝐴 ¬ ( 𝑥 +Q 𝑧 ) ∈ 𝐴 )
36 33 35 syl ⊢ ( ( ( ( 𝐴 ∈ P ∧ 1Q <Q 𝑏 ) ∧ ( 𝑦 ∈ 𝐴 ∧ ( 𝑦 ·Q 𝑏 ) ∈ 𝐴 ) ) ∧ ( 𝑦 +Q 𝑧 ) = ( 𝑦 ·Q 𝑏 ) ) → ∃ 𝑥 ∈ 𝐴 ¬ ( 𝑥 +Q 𝑧 ) ∈ 𝐴 )
37 33 adantr ⊢ ( ( ( ( ( 𝐴 ∈ P ∧ 1Q <Q 𝑏 ) ∧ ( 𝑦 ∈ 𝐴 ∧ ( 𝑦 ·Q 𝑏 ) ∈ 𝐴 ) ) ∧ ( 𝑦 +Q 𝑧 ) = ( 𝑦 ·Q 𝑏 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝐴 ∈ P )
38 simprr ⊢ ( ( ( 𝐴 ∈ P ∧ 1Q <Q 𝑏 ) ∧ ( 𝑦 ∈ 𝐴 ∧ ( 𝑦 ·Q 𝑏 ) ∈ 𝐴 ) ) → ( 𝑦 ·Q 𝑏 ) ∈ 𝐴 )
39 eleq1 ⊢ ( ( 𝑦 +Q 𝑧 ) = ( 𝑦 ·Q 𝑏 ) → ( ( 𝑦 +Q 𝑧 ) ∈ 𝐴 ↔ ( 𝑦 ·Q 𝑏 ) ∈ 𝐴 ) )
40 39 biimparc ⊢ ( ( ( 𝑦 ·Q 𝑏 ) ∈ 𝐴 ∧ ( 𝑦 +Q 𝑧 ) = ( 𝑦 ·Q 𝑏 ) ) → ( 𝑦 +Q 𝑧 ) ∈ 𝐴 )
41 38 40 sylan ⊢ ( ( ( ( 𝐴 ∈ P ∧ 1Q <Q 𝑏 ) ∧ ( 𝑦 ∈ 𝐴 ∧ ( 𝑦 ·Q 𝑏 ) ∈ 𝐴 ) ) ∧ ( 𝑦 +Q 𝑧 ) = ( 𝑦 ·Q 𝑏 ) ) → ( 𝑦 +Q 𝑧 ) ∈ 𝐴 )
42 41 adantr ⊢ ( ( ( ( ( 𝐴 ∈ P ∧ 1Q <Q 𝑏 ) ∧ ( 𝑦 ∈ 𝐴 ∧ ( 𝑦 ·Q 𝑏 ) ∈ 𝐴 ) ) ∧ ( 𝑦 +Q 𝑧 ) = ( 𝑦 ·Q 𝑏 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 +Q 𝑧 ) ∈ 𝐴 )
43 elprnq ⊢ ( ( 𝐴 ∈ P ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ Q )
44 33 43 sylan ⊢ ( ( ( ( ( 𝐴 ∈ P ∧ 1Q <Q 𝑏 ) ∧ ( 𝑦 ∈ 𝐴 ∧ ( 𝑦 ·Q 𝑏 ) ∈ 𝐴 ) ) ∧ ( 𝑦 +Q 𝑧 ) = ( 𝑦 ·Q 𝑏 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ Q )
45 elprnq ⊢ ( ( 𝐴 ∈ P ∧ ( 𝑦 +Q 𝑧 ) ∈ 𝐴 ) → ( 𝑦 +Q 𝑧 ) ∈ Q )
46 addnqf ⊢ +Q : ( Q × Q ) ⟶ Q
47 46 fdmi ⊢ dom +Q = ( Q × Q )
48 0nnq ⊢ ¬ ∅ ∈ Q
49 47 48 ndmovrcl ⊢ ( ( 𝑦 +Q 𝑧 ) ∈ Q → ( 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) )
50 49 simprd ⊢ ( ( 𝑦 +Q 𝑧 ) ∈ Q → 𝑧 ∈ Q )
51 45 50 syl ⊢ ( ( 𝐴 ∈ P ∧ ( 𝑦 +Q 𝑧 ) ∈ 𝐴 ) → 𝑧 ∈ Q )
52 33 41 51 syl2anc ⊢ ( ( ( ( 𝐴 ∈ P ∧ 1Q <Q 𝑏 ) ∧ ( 𝑦 ∈ 𝐴 ∧ ( 𝑦 ·Q 𝑏 ) ∈ 𝐴 ) ) ∧ ( 𝑦 +Q 𝑧 ) = ( 𝑦 ·Q 𝑏 ) ) → 𝑧 ∈ Q )
53 52 adantr ⊢ ( ( ( ( ( 𝐴 ∈ P ∧ 1Q <Q 𝑏 ) ∧ ( 𝑦 ∈ 𝐴 ∧ ( 𝑦 ·Q 𝑏 ) ∈ 𝐴 ) ) ∧ ( 𝑦 +Q 𝑧 ) = ( 𝑦 ·Q 𝑏 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑧 ∈ Q )
54 addclnq ⊢ ( ( 𝑥 ∈ Q ∧ 𝑧 ∈ Q ) → ( 𝑥 +Q 𝑧 ) ∈ Q )
55 44 53 54 syl2anc ⊢ ( ( ( ( ( 𝐴 ∈ P ∧ 1Q <Q 𝑏 ) ∧ ( 𝑦 ∈ 𝐴 ∧ ( 𝑦 ·Q 𝑏 ) ∈ 𝐴 ) ) ∧ ( 𝑦 +Q 𝑧 ) = ( 𝑦 ·Q 𝑏 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 +Q 𝑧 ) ∈ Q )
56 prub ⊢ ( ( ( 𝐴 ∈ P ∧ ( 𝑦 +Q 𝑧 ) ∈ 𝐴 ) ∧ ( 𝑥 +Q 𝑧 ) ∈ Q ) → ( ¬ ( 𝑥 +Q 𝑧 ) ∈ 𝐴 → ( 𝑦 +Q 𝑧 ) <Q ( 𝑥 +Q 𝑧 ) ) )
57 37 42 55 56 syl21anc ⊢ ( ( ( ( ( 𝐴 ∈ P ∧ 1Q <Q 𝑏 ) ∧ ( 𝑦 ∈ 𝐴 ∧ ( 𝑦 ·Q 𝑏 ) ∈ 𝐴 ) ) ∧ ( 𝑦 +Q 𝑧 ) = ( 𝑦 ·Q 𝑏 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ¬ ( 𝑥 +Q 𝑧 ) ∈ 𝐴 → ( 𝑦 +Q 𝑧 ) <Q ( 𝑥 +Q 𝑧 ) ) )
58 27 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ P ∧ 1Q <Q 𝑏 ) ∧ ( 𝑦 ∈ 𝐴 ∧ ( 𝑦 ·Q 𝑏 ) ∈ 𝐴 ) ) ∧ ( 𝑦 +Q 𝑧 ) = ( 𝑦 ·Q 𝑏 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑏 ∈ Q )
59 mulclnq ⊢ ( ( 𝑥 ∈ Q ∧ 𝑏 ∈ Q ) → ( 𝑥 ·Q 𝑏 ) ∈ Q )
60 44 58 59 syl2anc ⊢ ( ( ( ( ( 𝐴 ∈ P ∧ 1Q <Q 𝑏 ) ∧ ( 𝑦 ∈ 𝐴 ∧ ( 𝑦 ·Q 𝑏 ) ∈ 𝐴 ) ) ∧ ( 𝑦 +Q 𝑧 ) = ( 𝑦 ·Q 𝑏 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ·Q 𝑏 ) ∈ Q )
61 17 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ P ∧ 1Q <Q 𝑏 ) ∧ ( 𝑦 ∈ 𝐴 ∧ ( 𝑦 ·Q 𝑏 ) ∈ 𝐴 ) ) ∧ ( 𝑦 +Q 𝑧 ) = ( 𝑦 ·Q 𝑏 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ Q )
62 simplr ⊢ ( ( ( ( ( 𝐴 ∈ P ∧ 1Q <Q 𝑏 ) ∧ ( 𝑦 ∈ 𝐴 ∧ ( 𝑦 ·Q 𝑏 ) ∈ 𝐴 ) ) ∧ ( 𝑦 +Q 𝑧 ) = ( 𝑦 ·Q 𝑏 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 +Q 𝑧 ) = ( 𝑦 ·Q 𝑏 ) )
63 recclnq ⊢ ( 𝑦 ∈ Q → ( *Q ‘ 𝑦 ) ∈ Q )
64 mulclnq ⊢ ( ( 𝑧 ∈ Q ∧ ( *Q ‘ 𝑦 ) ∈ Q ) → ( 𝑧 ·Q ( *Q ‘ 𝑦 ) ) ∈ Q )
65 63 64 sylan2 ⊢ ( ( 𝑧 ∈ Q ∧ 𝑦 ∈ Q ) → ( 𝑧 ·Q ( *Q ‘ 𝑦 ) ) ∈ Q )
66 65 ancoms ⊢ ( ( 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( 𝑧 ·Q ( *Q ‘ 𝑦 ) ) ∈ Q )
67 ltmnq ⊢ ( ( 𝑧 ·Q ( *Q ‘ 𝑦 ) ) ∈ Q → ( 𝑦 <Q 𝑥 ↔ ( ( 𝑧 ·Q ( *Q ‘ 𝑦 ) ) ·Q 𝑦 ) <Q ( ( 𝑧 ·Q ( *Q ‘ 𝑦 ) ) ·Q 𝑥 ) ) )
68 66 67 syl ⊢ ( ( 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( 𝑦 <Q 𝑥 ↔ ( ( 𝑧 ·Q ( *Q ‘ 𝑦 ) ) ·Q 𝑦 ) <Q ( ( 𝑧 ·Q ( *Q ‘ 𝑦 ) ) ·Q 𝑥 ) ) )
69 mulassnq ⊢ ( ( 𝑧 ·Q ( *Q ‘ 𝑦 ) ) ·Q 𝑦 ) = ( 𝑧 ·Q ( ( *Q ‘ 𝑦 ) ·Q 𝑦 ) )
70 mulcomnq ⊢ ( ( *Q ‘ 𝑦 ) ·Q 𝑦 ) = ( 𝑦 ·Q ( *Q ‘ 𝑦 ) )
71 70 oveq2i ⊢ ( 𝑧 ·Q ( ( *Q ‘ 𝑦 ) ·Q 𝑦 ) ) = ( 𝑧 ·Q ( 𝑦 ·Q ( *Q ‘ 𝑦 ) ) )
72 69 71 eqtri ⊢ ( ( 𝑧 ·Q ( *Q ‘ 𝑦 ) ) ·Q 𝑦 ) = ( 𝑧 ·Q ( 𝑦 ·Q ( *Q ‘ 𝑦 ) ) )
73 recidnq ⊢ ( 𝑦 ∈ Q → ( 𝑦 ·Q ( *Q ‘ 𝑦 ) ) = 1Q )
74 73 oveq2d ⊢ ( 𝑦 ∈ Q → ( 𝑧 ·Q ( 𝑦 ·Q ( *Q ‘ 𝑦 ) ) ) = ( 𝑧 ·Q 1Q ) )
75 mulidnq ⊢ ( 𝑧 ∈ Q → ( 𝑧 ·Q 1Q ) = 𝑧 )
76 74 75 sylan9eq ⊢ ( ( 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( 𝑧 ·Q ( 𝑦 ·Q ( *Q ‘ 𝑦 ) ) ) = 𝑧 )
77 72 76 syl5eq ⊢ ( ( 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( ( 𝑧 ·Q ( *Q ‘ 𝑦 ) ) ·Q 𝑦 ) = 𝑧 )
78 77 breq1d ⊢ ( ( 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( ( ( 𝑧 ·Q ( *Q ‘ 𝑦 ) ) ·Q 𝑦 ) <Q ( ( 𝑧 ·Q ( *Q ‘ 𝑦 ) ) ·Q 𝑥 ) ↔ 𝑧 <Q ( ( 𝑧 ·Q ( *Q ‘ 𝑦 ) ) ·Q 𝑥 ) ) )
79 68 78 bitrd ⊢ ( ( 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( 𝑦 <Q 𝑥 ↔ 𝑧 <Q ( ( 𝑧 ·Q ( *Q ‘ 𝑦 ) ) ·Q 𝑥 ) ) )
80 79 adantll ⊢ ( ( ( ( 𝑥 ·Q 𝑏 ) ∈ Q ∧ 𝑦 ∈ Q ) ∧ 𝑧 ∈ Q ) → ( 𝑦 <Q 𝑥 ↔ 𝑧 <Q ( ( 𝑧 ·Q ( *Q ‘ 𝑦 ) ) ·Q 𝑥 ) ) )
81 mulnqf ⊢ ·Q : ( Q × Q ) ⟶ Q
82 81 fdmi ⊢ dom ·Q = ( Q × Q )
83 82 48 ndmovrcl ⊢ ( ( 𝑥 ·Q 𝑏 ) ∈ Q → ( 𝑥 ∈ Q ∧ 𝑏 ∈ Q ) )
84 83 simpld ⊢ ( ( 𝑥 ·Q 𝑏 ) ∈ Q → 𝑥 ∈ Q )
85 ltanq ⊢ ( 𝑥 ∈ Q → ( 𝑧 <Q ( ( 𝑧 ·Q ( *Q ‘ 𝑦 ) ) ·Q 𝑥 ) ↔ ( 𝑥 +Q 𝑧 ) <Q ( 𝑥 +Q ( ( 𝑧 ·Q ( *Q ‘ 𝑦 ) ) ·Q 𝑥 ) ) ) )
86 84 85 syl ⊢ ( ( 𝑥 ·Q 𝑏 ) ∈ Q → ( 𝑧 <Q ( ( 𝑧 ·Q ( *Q ‘ 𝑦 ) ) ·Q 𝑥 ) ↔ ( 𝑥 +Q 𝑧 ) <Q ( 𝑥 +Q ( ( 𝑧 ·Q ( *Q ‘ 𝑦 ) ) ·Q 𝑥 ) ) ) )
87 86 adantr ⊢ ( ( ( 𝑥 ·Q 𝑏 ) ∈ Q ∧ 𝑦 ∈ Q ) → ( 𝑧 <Q ( ( 𝑧 ·Q ( *Q ‘ 𝑦 ) ) ·Q 𝑥 ) ↔ ( 𝑥 +Q 𝑧 ) <Q ( 𝑥 +Q ( ( 𝑧 ·Q ( *Q ‘ 𝑦 ) ) ·Q 𝑥 ) ) ) )
88 vex ⊢ 𝑦 ∈ V
89 ovex ⊢ ( 𝑥 ·Q ( *Q ‘ 𝑦 ) ) ∈ V
90 mulcomnq ⊢ ( 𝑢 ·Q 𝑤 ) = ( 𝑤 ·Q 𝑢 )
91 distrnq ⊢ ( 𝑢 ·Q ( 𝑤 +Q 𝑣 ) ) = ( ( 𝑢 ·Q 𝑤 ) +Q ( 𝑢 ·Q 𝑣 ) )
92 88 34 89 90 91 caovdir ⊢ ( ( 𝑦 +Q 𝑧 ) ·Q ( 𝑥 ·Q ( *Q ‘ 𝑦 ) ) ) = ( ( 𝑦 ·Q ( 𝑥 ·Q ( *Q ‘ 𝑦 ) ) ) +Q ( 𝑧 ·Q ( 𝑥 ·Q ( *Q ‘ 𝑦 ) ) ) )
93 vex ⊢ 𝑥 ∈ V
94 fvex ⊢ ( *Q ‘ 𝑦 ) ∈ V
95 mulassnq ⊢ ( ( 𝑢 ·Q 𝑤 ) ·Q 𝑣 ) = ( 𝑢 ·Q ( 𝑤 ·Q 𝑣 ) )
96 88 93 94 90 95 caov12 ⊢ ( 𝑦 ·Q ( 𝑥 ·Q ( *Q ‘ 𝑦 ) ) ) = ( 𝑥 ·Q ( 𝑦 ·Q ( *Q ‘ 𝑦 ) ) )
97 73 oveq2d ⊢ ( 𝑦 ∈ Q → ( 𝑥 ·Q ( 𝑦 ·Q ( *Q ‘ 𝑦 ) ) ) = ( 𝑥 ·Q 1Q ) )
98 mulidnq ⊢ ( 𝑥 ∈ Q → ( 𝑥 ·Q 1Q ) = 𝑥 )
99 84 98 syl ⊢ ( ( 𝑥 ·Q 𝑏 ) ∈ Q → ( 𝑥 ·Q 1Q ) = 𝑥 )
100 97 99 sylan9eqr ⊢ ( ( ( 𝑥 ·Q 𝑏 ) ∈ Q ∧ 𝑦 ∈ Q ) → ( 𝑥 ·Q ( 𝑦 ·Q ( *Q ‘ 𝑦 ) ) ) = 𝑥 )
101 96 100 syl5eq ⊢ ( ( ( 𝑥 ·Q 𝑏 ) ∈ Q ∧ 𝑦 ∈ Q ) → ( 𝑦 ·Q ( 𝑥 ·Q ( *Q ‘ 𝑦 ) ) ) = 𝑥 )
102 mulcomnq ⊢ ( 𝑥 ·Q ( *Q ‘ 𝑦 ) ) = ( ( *Q ‘ 𝑦 ) ·Q 𝑥 )
103 102 oveq2i ⊢ ( 𝑧 ·Q ( 𝑥 ·Q ( *Q ‘ 𝑦 ) ) ) = ( 𝑧 ·Q ( ( *Q ‘ 𝑦 ) ·Q 𝑥 ) )
104 mulassnq ⊢ ( ( 𝑧 ·Q ( *Q ‘ 𝑦 ) ) ·Q 𝑥 ) = ( 𝑧 ·Q ( ( *Q ‘ 𝑦 ) ·Q 𝑥 ) )
105 103 104 eqtr4i ⊢ ( 𝑧 ·Q ( 𝑥 ·Q ( *Q ‘ 𝑦 ) ) ) = ( ( 𝑧 ·Q ( *Q ‘ 𝑦 ) ) ·Q 𝑥 )
106 105 a1i ⊢ ( ( ( 𝑥 ·Q 𝑏 ) ∈ Q ∧ 𝑦 ∈ Q ) → ( 𝑧 ·Q ( 𝑥 ·Q ( *Q ‘ 𝑦 ) ) ) = ( ( 𝑧 ·Q ( *Q ‘ 𝑦 ) ) ·Q 𝑥 ) )
107 101 106 oveq12d ⊢ ( ( ( 𝑥 ·Q 𝑏 ) ∈ Q ∧ 𝑦 ∈ Q ) → ( ( 𝑦 ·Q ( 𝑥 ·Q ( *Q ‘ 𝑦 ) ) ) +Q ( 𝑧 ·Q ( 𝑥 ·Q ( *Q ‘ 𝑦 ) ) ) ) = ( 𝑥 +Q ( ( 𝑧 ·Q ( *Q ‘ 𝑦 ) ) ·Q 𝑥 ) ) )
108 92 107 syl5eq ⊢ ( ( ( 𝑥 ·Q 𝑏 ) ∈ Q ∧ 𝑦 ∈ Q ) → ( ( 𝑦 +Q 𝑧 ) ·Q ( 𝑥 ·Q ( *Q ‘ 𝑦 ) ) ) = ( 𝑥 +Q ( ( 𝑧 ·Q ( *Q ‘ 𝑦 ) ) ·Q 𝑥 ) ) )
109 108 breq2d ⊢ ( ( ( 𝑥 ·Q 𝑏 ) ∈ Q ∧ 𝑦 ∈ Q ) → ( ( 𝑥 +Q 𝑧 ) <Q ( ( 𝑦 +Q 𝑧 ) ·Q ( 𝑥 ·Q ( *Q ‘ 𝑦 ) ) ) ↔ ( 𝑥 +Q 𝑧 ) <Q ( 𝑥 +Q ( ( 𝑧 ·Q ( *Q ‘ 𝑦 ) ) ·Q 𝑥 ) ) ) )
110 87 109 bitr4d ⊢ ( ( ( 𝑥 ·Q 𝑏 ) ∈ Q ∧ 𝑦 ∈ Q ) → ( 𝑧 <Q ( ( 𝑧 ·Q ( *Q ‘ 𝑦 ) ) ·Q 𝑥 ) ↔ ( 𝑥 +Q 𝑧 ) <Q ( ( 𝑦 +Q 𝑧 ) ·Q ( 𝑥 ·Q ( *Q ‘ 𝑦 ) ) ) ) )
111 110 adantr ⊢ ( ( ( ( 𝑥 ·Q 𝑏 ) ∈ Q ∧ 𝑦 ∈ Q ) ∧ 𝑧 ∈ Q ) → ( 𝑧 <Q ( ( 𝑧 ·Q ( *Q ‘ 𝑦 ) ) ·Q 𝑥 ) ↔ ( 𝑥 +Q 𝑧 ) <Q ( ( 𝑦 +Q 𝑧 ) ·Q ( 𝑥 ·Q ( *Q ‘ 𝑦 ) ) ) ) )
112 80 111 bitrd ⊢ ( ( ( ( 𝑥 ·Q 𝑏 ) ∈ Q ∧ 𝑦 ∈ Q ) ∧ 𝑧 ∈ Q ) → ( 𝑦 <Q 𝑥 ↔ ( 𝑥 +Q 𝑧 ) <Q ( ( 𝑦 +Q 𝑧 ) ·Q ( 𝑥 ·Q ( *Q ‘ 𝑦 ) ) ) ) )
113 112 adantrr ⊢ ( ( ( ( 𝑥 ·Q 𝑏 ) ∈ Q ∧ 𝑦 ∈ Q ) ∧ ( 𝑧 ∈ Q ∧ ( 𝑦 +Q 𝑧 ) = ( 𝑦 ·Q 𝑏 ) ) ) → ( 𝑦 <Q 𝑥 ↔ ( 𝑥 +Q 𝑧 ) <Q ( ( 𝑦 +Q 𝑧 ) ·Q ( 𝑥 ·Q ( *Q ‘ 𝑦 ) ) ) ) )
114 ltanq ⊢ ( 𝑧 ∈ Q → ( 𝑦 <Q 𝑥 ↔ ( 𝑧 +Q 𝑦 ) <Q ( 𝑧 +Q 𝑥 ) ) )
115 addcomnq ⊢ ( 𝑧 +Q 𝑦 ) = ( 𝑦 +Q 𝑧 )
116 addcomnq ⊢ ( 𝑧 +Q 𝑥 ) = ( 𝑥 +Q 𝑧 )
117 115 116 breq12i ⊢ ( ( 𝑧 +Q 𝑦 ) <Q ( 𝑧 +Q 𝑥 ) ↔ ( 𝑦 +Q 𝑧 ) <Q ( 𝑥 +Q 𝑧 ) )
118 114 117 bitrdi ⊢ ( 𝑧 ∈ Q → ( 𝑦 <Q 𝑥 ↔ ( 𝑦 +Q 𝑧 ) <Q ( 𝑥 +Q 𝑧 ) ) )
119 118 ad2antrl ⊢ ( ( ( ( 𝑥 ·Q 𝑏 ) ∈ Q ∧ 𝑦 ∈ Q ) ∧ ( 𝑧 ∈ Q ∧ ( 𝑦 +Q 𝑧 ) = ( 𝑦 ·Q 𝑏 ) ) ) → ( 𝑦 <Q 𝑥 ↔ ( 𝑦 +Q 𝑧 ) <Q ( 𝑥 +Q 𝑧 ) ) )
120 oveq1 ⊢ ( ( 𝑦 +Q 𝑧 ) = ( 𝑦 ·Q 𝑏 ) → ( ( 𝑦 +Q 𝑧 ) ·Q ( 𝑥 ·Q ( *Q ‘ 𝑦 ) ) ) = ( ( 𝑦 ·Q 𝑏 ) ·Q ( 𝑥 ·Q ( *Q ‘ 𝑦 ) ) ) )
121 vex ⊢ 𝑏 ∈ V
122 88 121 93 90 95 94 caov411 ⊢ ( ( 𝑦 ·Q 𝑏 ) ·Q ( 𝑥 ·Q ( *Q ‘ 𝑦 ) ) ) = ( ( 𝑥 ·Q 𝑏 ) ·Q ( 𝑦 ·Q ( *Q ‘ 𝑦 ) ) )
123 73 oveq2d ⊢ ( 𝑦 ∈ Q → ( ( 𝑥 ·Q 𝑏 ) ·Q ( 𝑦 ·Q ( *Q ‘ 𝑦 ) ) ) = ( ( 𝑥 ·Q 𝑏 ) ·Q 1Q ) )
124 mulidnq ⊢ ( ( 𝑥 ·Q 𝑏 ) ∈ Q → ( ( 𝑥 ·Q 𝑏 ) ·Q 1Q ) = ( 𝑥 ·Q 𝑏 ) )
125 123 124 sylan9eqr ⊢ ( ( ( 𝑥 ·Q 𝑏 ) ∈ Q ∧ 𝑦 ∈ Q ) → ( ( 𝑥 ·Q 𝑏 ) ·Q ( 𝑦 ·Q ( *Q ‘ 𝑦 ) ) ) = ( 𝑥 ·Q 𝑏 ) )
126 122 125 syl5eq ⊢ ( ( ( 𝑥 ·Q 𝑏 ) ∈ Q ∧ 𝑦 ∈ Q ) → ( ( 𝑦 ·Q 𝑏 ) ·Q ( 𝑥 ·Q ( *Q ‘ 𝑦 ) ) ) = ( 𝑥 ·Q 𝑏 ) )
127 120 126 sylan9eqr ⊢ ( ( ( ( 𝑥 ·Q 𝑏 ) ∈ Q ∧ 𝑦 ∈ Q ) ∧ ( 𝑦 +Q 𝑧 ) = ( 𝑦 ·Q 𝑏 ) ) → ( ( 𝑦 +Q 𝑧 ) ·Q ( 𝑥 ·Q ( *Q ‘ 𝑦 ) ) ) = ( 𝑥 ·Q 𝑏 ) )
128 127 breq2d ⊢ ( ( ( ( 𝑥 ·Q 𝑏 ) ∈ Q ∧ 𝑦 ∈ Q ) ∧ ( 𝑦 +Q 𝑧 ) = ( 𝑦 ·Q 𝑏 ) ) → ( ( 𝑥 +Q 𝑧 ) <Q ( ( 𝑦 +Q 𝑧 ) ·Q ( 𝑥 ·Q ( *Q ‘ 𝑦 ) ) ) ↔ ( 𝑥 +Q 𝑧 ) <Q ( 𝑥 ·Q 𝑏 ) ) )
129 128 adantrl ⊢ ( ( ( ( 𝑥 ·Q 𝑏 ) ∈ Q ∧ 𝑦 ∈ Q ) ∧ ( 𝑧 ∈ Q ∧ ( 𝑦 +Q 𝑧 ) = ( 𝑦 ·Q 𝑏 ) ) ) → ( ( 𝑥 +Q 𝑧 ) <Q ( ( 𝑦 +Q 𝑧 ) ·Q ( 𝑥 ·Q ( *Q ‘ 𝑦 ) ) ) ↔ ( 𝑥 +Q 𝑧 ) <Q ( 𝑥 ·Q 𝑏 ) ) )
130 113 119 129 3bitr3d ⊢ ( ( ( ( 𝑥 ·Q 𝑏 ) ∈ Q ∧ 𝑦 ∈ Q ) ∧ ( 𝑧 ∈ Q ∧ ( 𝑦 +Q 𝑧 ) = ( 𝑦 ·Q 𝑏 ) ) ) → ( ( 𝑦 +Q 𝑧 ) <Q ( 𝑥 +Q 𝑧 ) ↔ ( 𝑥 +Q 𝑧 ) <Q ( 𝑥 ·Q 𝑏 ) ) )
131 60 61 53 62 130 syl22anc ⊢ ( ( ( ( ( 𝐴 ∈ P ∧ 1Q <Q 𝑏 ) ∧ ( 𝑦 ∈ 𝐴 ∧ ( 𝑦 ·Q 𝑏 ) ∈ 𝐴 ) ) ∧ ( 𝑦 +Q 𝑧 ) = ( 𝑦 ·Q 𝑏 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑦 +Q 𝑧 ) <Q ( 𝑥 +Q 𝑧 ) ↔ ( 𝑥 +Q 𝑧 ) <Q ( 𝑥 ·Q 𝑏 ) ) )
132 57 131 sylibd ⊢ ( ( ( ( ( 𝐴 ∈ P ∧ 1Q <Q 𝑏 ) ∧ ( 𝑦 ∈ 𝐴 ∧ ( 𝑦 ·Q 𝑏 ) ∈ 𝐴 ) ) ∧ ( 𝑦 +Q 𝑧 ) = ( 𝑦 ·Q 𝑏 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ¬ ( 𝑥 +Q 𝑧 ) ∈ 𝐴 → ( 𝑥 +Q 𝑧 ) <Q ( 𝑥 ·Q 𝑏 ) ) )
133 prcdnq ⊢ ( ( 𝐴 ∈ P ∧ ( 𝑥 ·Q 𝑏 ) ∈ 𝐴 ) → ( ( 𝑥 +Q 𝑧 ) <Q ( 𝑥 ·Q 𝑏 ) → ( 𝑥 +Q 𝑧 ) ∈ 𝐴 ) )
134 133 impancom ⊢ ( ( 𝐴 ∈ P ∧ ( 𝑥 +Q 𝑧 ) <Q ( 𝑥 ·Q 𝑏 ) ) → ( ( 𝑥 ·Q 𝑏 ) ∈ 𝐴 → ( 𝑥 +Q 𝑧 ) ∈ 𝐴 ) )
135 134 con3d ⊢ ( ( 𝐴 ∈ P ∧ ( 𝑥 +Q 𝑧 ) <Q ( 𝑥 ·Q 𝑏 ) ) → ( ¬ ( 𝑥 +Q 𝑧 ) ∈ 𝐴 → ¬ ( 𝑥 ·Q 𝑏 ) ∈ 𝐴 ) )
136 135 ex ⊢ ( 𝐴 ∈ P → ( ( 𝑥 +Q 𝑧 ) <Q ( 𝑥 ·Q 𝑏 ) → ( ¬ ( 𝑥 +Q 𝑧 ) ∈ 𝐴 → ¬ ( 𝑥 ·Q 𝑏 ) ∈ 𝐴 ) ) )
137 136 com23 ⊢ ( 𝐴 ∈ P → ( ¬ ( 𝑥 +Q 𝑧 ) ∈ 𝐴 → ( ( 𝑥 +Q 𝑧 ) <Q ( 𝑥 ·Q 𝑏 ) → ¬ ( 𝑥 ·Q 𝑏 ) ∈ 𝐴 ) ) )
138 37 137 syl ⊢ ( ( ( ( ( 𝐴 ∈ P ∧ 1Q <Q 𝑏 ) ∧ ( 𝑦 ∈ 𝐴 ∧ ( 𝑦 ·Q 𝑏 ) ∈ 𝐴 ) ) ∧ ( 𝑦 +Q 𝑧 ) = ( 𝑦 ·Q 𝑏 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ¬ ( 𝑥 +Q 𝑧 ) ∈ 𝐴 → ( ( 𝑥 +Q 𝑧 ) <Q ( 𝑥 ·Q 𝑏 ) → ¬ ( 𝑥 ·Q 𝑏 ) ∈ 𝐴 ) ) )
139 132 138 mpdd ⊢ ( ( ( ( ( 𝐴 ∈ P ∧ 1Q <Q 𝑏 ) ∧ ( 𝑦 ∈ 𝐴 ∧ ( 𝑦 ·Q 𝑏 ) ∈ 𝐴 ) ) ∧ ( 𝑦 +Q 𝑧 ) = ( 𝑦 ·Q 𝑏 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ¬ ( 𝑥 +Q 𝑧 ) ∈ 𝐴 → ¬ ( 𝑥 ·Q 𝑏 ) ∈ 𝐴 ) )
140 139 reximdva ⊢ ( ( ( ( 𝐴 ∈ P ∧ 1Q <Q 𝑏 ) ∧ ( 𝑦 ∈ 𝐴 ∧ ( 𝑦 ·Q 𝑏 ) ∈ 𝐴 ) ) ∧ ( 𝑦 +Q 𝑧 ) = ( 𝑦 ·Q 𝑏 ) ) → ( ∃ 𝑥 ∈ 𝐴 ¬ ( 𝑥 +Q 𝑧 ) ∈ 𝐴 → ∃ 𝑥 ∈ 𝐴 ¬ ( 𝑥 ·Q 𝑏 ) ∈ 𝐴 ) )
141 36 140 mpd ⊢ ( ( ( ( 𝐴 ∈ P ∧ 1Q <Q 𝑏 ) ∧ ( 𝑦 ∈ 𝐴 ∧ ( 𝑦 ·Q 𝑏 ) ∈ 𝐴 ) ) ∧ ( 𝑦 +Q 𝑧 ) = ( 𝑦 ·Q 𝑏 ) ) → ∃ 𝑥 ∈ 𝐴 ¬ ( 𝑥 ·Q 𝑏 ) ∈ 𝐴 )
142 32 141 exlimddv ⊢ ( ( ( 𝐴 ∈ P ∧ 1Q <Q 𝑏 ) ∧ ( 𝑦 ∈ 𝐴 ∧ ( 𝑦 ·Q 𝑏 ) ∈ 𝐴 ) ) → ∃ 𝑥 ∈ 𝐴 ¬ ( 𝑥 ·Q 𝑏 ) ∈ 𝐴 )
143 142 expr ⊢ ( ( ( 𝐴 ∈ P ∧ 1Q <Q 𝑏 ) ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑦 ·Q 𝑏 ) ∈ 𝐴 → ∃ 𝑥 ∈ 𝐴 ¬ ( 𝑥 ·Q 𝑏 ) ∈ 𝐴 ) )
144 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ·Q 𝑏 ) = ( 𝑦 ·Q 𝑏 ) )
145 144 eleq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ·Q 𝑏 ) ∈ 𝐴 ↔ ( 𝑦 ·Q 𝑏 ) ∈ 𝐴 ) )
146 145 notbid ⊢ ( 𝑥 = 𝑦 → ( ¬ ( 𝑥 ·Q 𝑏 ) ∈ 𝐴 ↔ ¬ ( 𝑦 ·Q 𝑏 ) ∈ 𝐴 ) )
147 146 rspcev ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ¬ ( 𝑦 ·Q 𝑏 ) ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝐴 ¬ ( 𝑥 ·Q 𝑏 ) ∈ 𝐴 )
148 147 ex ⊢ ( 𝑦 ∈ 𝐴 → ( ¬ ( 𝑦 ·Q 𝑏 ) ∈ 𝐴 → ∃ 𝑥 ∈ 𝐴 ¬ ( 𝑥 ·Q 𝑏 ) ∈ 𝐴 ) )
149 148 adantl ⊢ ( ( ( 𝐴 ∈ P ∧ 1Q <Q 𝑏 ) ∧ 𝑦 ∈ 𝐴 ) → ( ¬ ( 𝑦 ·Q 𝑏 ) ∈ 𝐴 → ∃ 𝑥 ∈ 𝐴 ¬ ( 𝑥 ·Q 𝑏 ) ∈ 𝐴 ) )
150 143 149 pm2.61d ⊢ ( ( ( 𝐴 ∈ P ∧ 1Q <Q 𝑏 ) ∧ 𝑦 ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝐴 ¬ ( 𝑥 ·Q 𝑏 ) ∈ 𝐴 )
151 15 150 exlimddv ⊢ ( ( 𝐴 ∈ P ∧ 1Q <Q 𝑏 ) → ∃ 𝑥 ∈ 𝐴 ¬ ( 𝑥 ·Q 𝑏 ) ∈ 𝐴 )
152 11 151 vtoclg ⊢ ( 𝐵 ∈ Q → ( ( 𝐴 ∈ P ∧ 1Q <Q 𝐵 ) → ∃ 𝑥 ∈ 𝐴 ¬ ( 𝑥 ·Q 𝐵 ) ∈ 𝐴 ) )
153 4 152 mpcom ⊢ ( ( 𝐴 ∈ P ∧ 1Q <Q 𝐵 ) → ∃ 𝑥 ∈ 𝐴 ¬ ( 𝑥 ·Q 𝐵 ) ∈ 𝐴 )