Metamath Proof Explorer

Theorem prlem934

Description: Lemma 9-3.4 of Gleason p. 122. (Contributed by NM, 25-Mar-1996) (Revised by Mario Carneiro, 11-May-2013) (New usage is discouraged.)

Ref Expression
Hypothesis prlem934.1 ⊢ 𝐵 ∈ V
Assertion prlem934 ( 𝐴 ∈ P → ∃ 𝑥 ∈ 𝐴 ¬ ( 𝑥 +Q 𝐵 ) ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 prlem934.1 ⊢ 𝐵 ∈ V
2 prn0 ⊢ ( 𝐴 ∈ P → 𝐴 ≠ ∅ )
3 r19.2z ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝐵 ) ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝐵 ) ∈ 𝐴 )
4 3 ex ⊢ ( 𝐴 ≠ ∅ → ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝐵 ) ∈ 𝐴 → ∃ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝐵 ) ∈ 𝐴 ) )
5 2 4 syl ⊢ ( 𝐴 ∈ P → ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝐵 ) ∈ 𝐴 → ∃ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝐵 ) ∈ 𝐴 ) )
6 prpssnq ⊢ ( 𝐴 ∈ P → 𝐴 ⊊ Q )
7 6 pssssd ⊢ ( 𝐴 ∈ P → 𝐴 ⊆ Q )
8 7 sseld ⊢ ( 𝐴 ∈ P → ( ( 𝑥 +Q 𝐵 ) ∈ 𝐴 → ( 𝑥 +Q 𝐵 ) ∈ Q ) )
9 addnqf ⊢ +Q : ( Q × Q ) ⟶ Q
10 9 fdmi ⊢ dom +Q = ( Q × Q )
11 0nnq ⊢ ¬ ∅ ∈ Q
12 10 11 ndmovrcl ⊢ ( ( 𝑥 +Q 𝐵 ) ∈ Q → ( 𝑥 ∈ Q ∧ 𝐵 ∈ Q ) )
13 12 simprd ⊢ ( ( 𝑥 +Q 𝐵 ) ∈ Q → 𝐵 ∈ Q )
14 8 13 syl6com ⊢ ( ( 𝑥 +Q 𝐵 ) ∈ 𝐴 → ( 𝐴 ∈ P → 𝐵 ∈ Q ) )
15 14 rexlimivw ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝐵 ) ∈ 𝐴 → ( 𝐴 ∈ P → 𝐵 ∈ Q ) )
16 15 com12 ⊢ ( 𝐴 ∈ P → ( ∃ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝐵 ) ∈ 𝐴 → 𝐵 ∈ Q ) )
17 oveq2 ⊢ ( 𝑏 = 𝐵 → ( 𝑥 +Q 𝑏 ) = ( 𝑥 +Q 𝐵 ) )
18 17 eleq1d ⊢ ( 𝑏 = 𝐵 → ( ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ↔ ( 𝑥 +Q 𝐵 ) ∈ 𝐴 ) )
19 18 ralbidv ⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝐵 ) ∈ 𝐴 ) )
20 19 notbid ⊢ ( 𝑏 = 𝐵 → ( ¬ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ↔ ¬ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝐵 ) ∈ 𝐴 ) )
21 20 imbi2d ⊢ ( 𝑏 = 𝐵 → ( ( 𝐴 ∈ P → ¬ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ) ↔ ( 𝐴 ∈ P → ¬ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝐵 ) ∈ 𝐴 ) ) )
22 dfpss2 ⊢ ( 𝐴 ⊊ Q ↔ ( 𝐴 ⊆ Q ∧ ¬ 𝐴 = Q ) )
23 6 22 sylib ⊢ ( 𝐴 ∈ P → ( 𝐴 ⊆ Q ∧ ¬ 𝐴 = Q ) )
24 23 simprd ⊢ ( 𝐴 ∈ P → ¬ 𝐴 = Q )
25 24 adantr ⊢ ( ( 𝐴 ∈ P ∧ 𝑏 ∈ Q ) → ¬ 𝐴 = Q )
26 7 3ad2ant1 ⊢ ( ( 𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ) → 𝐴 ⊆ Q )
27 simpl1 ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ) ∧ 𝑤 ∈ Q ) → 𝐴 ∈ P )
28 n0 ⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ 𝐴 )
29 2 28 sylib ⊢ ( 𝐴 ∈ P → ∃ 𝑦 𝑦 ∈ 𝐴 )
30 27 29 syl ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ) ∧ 𝑤 ∈ Q ) → ∃ 𝑦 𝑦 ∈ 𝐴 )
31 simprl ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ) ∧ ( 𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴 ) ) → 𝑤 ∈ Q )
32 simpl2 ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ) ∧ ( 𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴 ) ) → 𝑏 ∈ Q )
33 recclnq ⊢ ( 𝑏 ∈ Q → ( *Q ‘ 𝑏 ) ∈ Q )
34 mulclnq ⊢ ( ( 𝑤 ∈ Q ∧ ( *Q ‘ 𝑏 ) ∈ Q ) → ( 𝑤 ·Q ( *Q ‘ 𝑏 ) ) ∈ Q )
35 archnq ⊢ ( ( 𝑤 ·Q ( *Q ‘ 𝑏 ) ) ∈ Q → ∃ 𝑧 ∈ N ( 𝑤 ·Q ( *Q ‘ 𝑏 ) ) <Q ⟨ 𝑧 , 1o ⟩ )
36 34 35 syl ⊢ ( ( 𝑤 ∈ Q ∧ ( *Q ‘ 𝑏 ) ∈ Q ) → ∃ 𝑧 ∈ N ( 𝑤 ·Q ( *Q ‘ 𝑏 ) ) <Q ⟨ 𝑧 , 1o ⟩ )
37 33 36 sylan2 ⊢ ( ( 𝑤 ∈ Q ∧ 𝑏 ∈ Q ) → ∃ 𝑧 ∈ N ( 𝑤 ·Q ( *Q ‘ 𝑏 ) ) <Q ⟨ 𝑧 , 1o ⟩ )
38 31 32 37 syl2anc ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ) ∧ ( 𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴 ) ) → ∃ 𝑧 ∈ N ( 𝑤 ·Q ( *Q ‘ 𝑏 ) ) <Q ⟨ 𝑧 , 1o ⟩ )
39 simpll2 ⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ) ∧ ( 𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( 𝑧 ∈ N ∧ ( 𝑤 ·Q ( *Q ‘ 𝑏 ) ) <Q ⟨ 𝑧 , 1o ⟩ ) ) → 𝑏 ∈ Q )
40 simplrl ⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ) ∧ ( 𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( 𝑧 ∈ N ∧ ( 𝑤 ·Q ( *Q ‘ 𝑏 ) ) <Q ⟨ 𝑧 , 1o ⟩ ) ) → 𝑤 ∈ Q )
41 simprr ⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ) ∧ ( 𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( 𝑧 ∈ N ∧ ( 𝑤 ·Q ( *Q ‘ 𝑏 ) ) <Q ⟨ 𝑧 , 1o ⟩ ) ) → ( 𝑤 ·Q ( *Q ‘ 𝑏 ) ) <Q ⟨ 𝑧 , 1o ⟩ )
42 ltmnq ⊢ ( 𝑏 ∈ Q → ( ( 𝑤 ·Q ( *Q ‘ 𝑏 ) ) <Q ⟨ 𝑧 , 1o ⟩ ↔ ( 𝑏 ·Q ( 𝑤 ·Q ( *Q ‘ 𝑏 ) ) ) <Q ( 𝑏 ·Q ⟨ 𝑧 , 1o ⟩ ) ) )
43 vex ⊢ 𝑏 ∈ V
44 vex ⊢ 𝑤 ∈ V
45 fvex ⊢ ( *Q ‘ 𝑏 ) ∈ V
46 mulcomnq ⊢ ( 𝑣 ·Q 𝑥 ) = ( 𝑥 ·Q 𝑣 )
47 mulassnq ⊢ ( ( 𝑣 ·Q 𝑥 ) ·Q 𝑦 ) = ( 𝑣 ·Q ( 𝑥 ·Q 𝑦 ) )
48 43 44 45 46 47 caov12 ⊢ ( 𝑏 ·Q ( 𝑤 ·Q ( *Q ‘ 𝑏 ) ) ) = ( 𝑤 ·Q ( 𝑏 ·Q ( *Q ‘ 𝑏 ) ) )
49 mulcomnq ⊢ ( 𝑏 ·Q ⟨ 𝑧 , 1o ⟩ ) = ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 )
50 48 49 breq12i ⊢ ( ( 𝑏 ·Q ( 𝑤 ·Q ( *Q ‘ 𝑏 ) ) ) <Q ( 𝑏 ·Q ⟨ 𝑧 , 1o ⟩ ) ↔ ( 𝑤 ·Q ( 𝑏 ·Q ( *Q ‘ 𝑏 ) ) ) <Q ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) )
51 42 50 syl6bb ⊢ ( 𝑏 ∈ Q → ( ( 𝑤 ·Q ( *Q ‘ 𝑏 ) ) <Q ⟨ 𝑧 , 1o ⟩ ↔ ( 𝑤 ·Q ( 𝑏 ·Q ( *Q ‘ 𝑏 ) ) ) <Q ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) ) )
52 51 adantr ⊢ ( ( 𝑏 ∈ Q ∧ 𝑤 ∈ Q ) → ( ( 𝑤 ·Q ( *Q ‘ 𝑏 ) ) <Q ⟨ 𝑧 , 1o ⟩ ↔ ( 𝑤 ·Q ( 𝑏 ·Q ( *Q ‘ 𝑏 ) ) ) <Q ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) ) )
53 recidnq ⊢ ( 𝑏 ∈ Q → ( 𝑏 ·Q ( *Q ‘ 𝑏 ) ) = 1Q )
54 53 oveq2d ⊢ ( 𝑏 ∈ Q → ( 𝑤 ·Q ( 𝑏 ·Q ( *Q ‘ 𝑏 ) ) ) = ( 𝑤 ·Q 1Q ) )
55 mulidnq ⊢ ( 𝑤 ∈ Q → ( 𝑤 ·Q 1Q ) = 𝑤 )
56 54 55 sylan9eq ⊢ ( ( 𝑏 ∈ Q ∧ 𝑤 ∈ Q ) → ( 𝑤 ·Q ( 𝑏 ·Q ( *Q ‘ 𝑏 ) ) ) = 𝑤 )
57 56 breq1d ⊢ ( ( 𝑏 ∈ Q ∧ 𝑤 ∈ Q ) → ( ( 𝑤 ·Q ( 𝑏 ·Q ( *Q ‘ 𝑏 ) ) ) <Q ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) ↔ 𝑤 <Q ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) ) )
58 52 57 bitrd ⊢ ( ( 𝑏 ∈ Q ∧ 𝑤 ∈ Q ) → ( ( 𝑤 ·Q ( *Q ‘ 𝑏 ) ) <Q ⟨ 𝑧 , 1o ⟩ ↔ 𝑤 <Q ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) ) )
59 58 biimpa ⊢ ( ( ( 𝑏 ∈ Q ∧ 𝑤 ∈ Q ) ∧ ( 𝑤 ·Q ( *Q ‘ 𝑏 ) ) <Q ⟨ 𝑧 , 1o ⟩ ) → 𝑤 <Q ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) )
60 39 40 41 59 syl21anc ⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ) ∧ ( 𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( 𝑧 ∈ N ∧ ( 𝑤 ·Q ( *Q ‘ 𝑏 ) ) <Q ⟨ 𝑧 , 1o ⟩ ) ) → 𝑤 <Q ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) )
61 simprl ⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ) ∧ ( 𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( 𝑧 ∈ N ∧ ( 𝑤 ·Q ( *Q ‘ 𝑏 ) ) <Q ⟨ 𝑧 , 1o ⟩ ) ) → 𝑧 ∈ N )
62 pinq ⊢ ( 𝑧 ∈ N → ⟨ 𝑧 , 1o ⟩ ∈ Q )
63 mulclnq ⊢ ( ( ⟨ 𝑧 , 1o ⟩ ∈ Q ∧ 𝑏 ∈ Q ) → ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) ∈ Q )
64 62 63 sylan ⊢ ( ( 𝑧 ∈ N ∧ 𝑏 ∈ Q ) → ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) ∈ Q )
65 61 39 64 syl2anc ⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ) ∧ ( 𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( 𝑧 ∈ N ∧ ( 𝑤 ·Q ( *Q ‘ 𝑏 ) ) <Q ⟨ 𝑧 , 1o ⟩ ) ) → ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) ∈ Q )
66 simpll1 ⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ) ∧ ( 𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( 𝑧 ∈ N ∧ ( 𝑤 ·Q ( *Q ‘ 𝑏 ) ) <Q ⟨ 𝑧 , 1o ⟩ ) ) → 𝐴 ∈ P )
67 simplrr ⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ) ∧ ( 𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( 𝑧 ∈ N ∧ ( 𝑤 ·Q ( *Q ‘ 𝑏 ) ) <Q ⟨ 𝑧 , 1o ⟩ ) ) → 𝑦 ∈ 𝐴 )
68 elprnq ⊢ ( ( 𝐴 ∈ P ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ Q )
69 66 67 68 syl2anc ⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ) ∧ ( 𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( 𝑧 ∈ N ∧ ( 𝑤 ·Q ( *Q ‘ 𝑏 ) ) <Q ⟨ 𝑧 , 1o ⟩ ) ) → 𝑦 ∈ Q )
70 ltaddnq ⊢ ( ( ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) ∈ Q ∧ 𝑦 ∈ Q ) → ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) <Q ( ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) +Q 𝑦 ) )
71 addcomnq ⊢ ( ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) +Q 𝑦 ) = ( 𝑦 +Q ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) )
72 70 71 breqtrdi ⊢ ( ( ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) ∈ Q ∧ 𝑦 ∈ Q ) → ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) <Q ( 𝑦 +Q ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) ) )
73 65 69 72 syl2anc ⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ) ∧ ( 𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( 𝑧 ∈ N ∧ ( 𝑤 ·Q ( *Q ‘ 𝑏 ) ) <Q ⟨ 𝑧 , 1o ⟩ ) ) → ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) <Q ( 𝑦 +Q ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) ) )
74 ltsonq ⊢ <Q Or Q
75 ltrelnq ⊢ <Q ⊆ ( Q × Q )
76 74 75 sotri ⊢ ( ( 𝑤 <Q ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) ∧ ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) <Q ( 𝑦 +Q ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) ) ) → 𝑤 <Q ( 𝑦 +Q ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) ) )
77 60 73 76 syl2anc ⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ) ∧ ( 𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( 𝑧 ∈ N ∧ ( 𝑤 ·Q ( *Q ‘ 𝑏 ) ) <Q ⟨ 𝑧 , 1o ⟩ ) ) → 𝑤 <Q ( 𝑦 +Q ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) ) )
78 simpll3 ⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ) ∧ ( 𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( 𝑧 ∈ N ∧ ( 𝑤 ·Q ( *Q ‘ 𝑏 ) ) <Q ⟨ 𝑧 , 1o ⟩ ) ) → ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 )
79 opeq1 ⊢ ( 𝑤 = 1o → ⟨ 𝑤 , 1o ⟩ = ⟨ 1o , 1o ⟩ )
80 df-1nq ⊢ 1Q = ⟨ 1o , 1o ⟩
81 79 80 syl6eqr ⊢ ( 𝑤 = 1o → ⟨ 𝑤 , 1o ⟩ = 1Q )
82 81 oveq1d ⊢ ( 𝑤 = 1o → ( ⟨ 𝑤 , 1o ⟩ ·Q 𝑏 ) = ( 1Q ·Q 𝑏 ) )
83 82 oveq2d ⊢ ( 𝑤 = 1o → ( 𝑦 +Q ( ⟨ 𝑤 , 1o ⟩ ·Q 𝑏 ) ) = ( 𝑦 +Q ( 1Q ·Q 𝑏 ) ) )
84 83 eleq1d ⊢ ( 𝑤 = 1o → ( ( 𝑦 +Q ( ⟨ 𝑤 , 1o ⟩ ·Q 𝑏 ) ) ∈ 𝐴 ↔ ( 𝑦 +Q ( 1Q ·Q 𝑏 ) ) ∈ 𝐴 ) )
85 84 imbi2d ⊢ ( 𝑤 = 1o → ( ( ( 𝑏 ∈ Q ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 +Q ( ⟨ 𝑤 , 1o ⟩ ·Q 𝑏 ) ) ∈ 𝐴 ) ↔ ( ( 𝑏 ∈ Q ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 +Q ( 1Q ·Q 𝑏 ) ) ∈ 𝐴 ) ) )
86 opeq1 ⊢ ( 𝑤 = 𝑧 → ⟨ 𝑤 , 1o ⟩ = ⟨ 𝑧 , 1o ⟩ )
87 86 oveq1d ⊢ ( 𝑤 = 𝑧 → ( ⟨ 𝑤 , 1o ⟩ ·Q 𝑏 ) = ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) )
88 87 oveq2d ⊢ ( 𝑤 = 𝑧 → ( 𝑦 +Q ( ⟨ 𝑤 , 1o ⟩ ·Q 𝑏 ) ) = ( 𝑦 +Q ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) ) )
89 88 eleq1d ⊢ ( 𝑤 = 𝑧 → ( ( 𝑦 +Q ( ⟨ 𝑤 , 1o ⟩ ·Q 𝑏 ) ) ∈ 𝐴 ↔ ( 𝑦 +Q ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) ) ∈ 𝐴 ) )
90 89 imbi2d ⊢ ( 𝑤 = 𝑧 → ( ( ( 𝑏 ∈ Q ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 +Q ( ⟨ 𝑤 , 1o ⟩ ·Q 𝑏 ) ) ∈ 𝐴 ) ↔ ( ( 𝑏 ∈ Q ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 +Q ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) ) ∈ 𝐴 ) ) )
91 opeq1 ⊢ ( 𝑤 = ( 𝑧 +N 1o ) → ⟨ 𝑤 , 1o ⟩ = ⟨ ( 𝑧 +N 1o ) , 1o ⟩ )
92 91 oveq1d ⊢ ( 𝑤 = ( 𝑧 +N 1o ) → ( ⟨ 𝑤 , 1o ⟩ ·Q 𝑏 ) = ( ⟨ ( 𝑧 +N 1o ) , 1o ⟩ ·Q 𝑏 ) )
93 92 oveq2d ⊢ ( 𝑤 = ( 𝑧 +N 1o ) → ( 𝑦 +Q ( ⟨ 𝑤 , 1o ⟩ ·Q 𝑏 ) ) = ( 𝑦 +Q ( ⟨ ( 𝑧 +N 1o ) , 1o ⟩ ·Q 𝑏 ) ) )
94 93 eleq1d ⊢ ( 𝑤 = ( 𝑧 +N 1o ) → ( ( 𝑦 +Q ( ⟨ 𝑤 , 1o ⟩ ·Q 𝑏 ) ) ∈ 𝐴 ↔ ( 𝑦 +Q ( ⟨ ( 𝑧 +N 1o ) , 1o ⟩ ·Q 𝑏 ) ) ∈ 𝐴 ) )
95 94 imbi2d ⊢ ( 𝑤 = ( 𝑧 +N 1o ) → ( ( ( 𝑏 ∈ Q ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 +Q ( ⟨ 𝑤 , 1o ⟩ ·Q 𝑏 ) ) ∈ 𝐴 ) ↔ ( ( 𝑏 ∈ Q ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 +Q ( ⟨ ( 𝑧 +N 1o ) , 1o ⟩ ·Q 𝑏 ) ) ∈ 𝐴 ) ) )
96 mulcomnq ⊢ ( 1Q ·Q 𝑏 ) = ( 𝑏 ·Q 1Q )
97 mulidnq ⊢ ( 𝑏 ∈ Q → ( 𝑏 ·Q 1Q ) = 𝑏 )
98 96 97 syl5eq ⊢ ( 𝑏 ∈ Q → ( 1Q ·Q 𝑏 ) = 𝑏 )
99 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 +Q 𝑏 ) = ( 𝑦 +Q 𝑏 ) )
100 99 eleq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ↔ ( 𝑦 +Q 𝑏 ) ∈ 𝐴 ) )
101 100 rspccva ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 +Q 𝑏 ) ∈ 𝐴 )
102 oveq2 ⊢ ( ( 1Q ·Q 𝑏 ) = 𝑏 → ( 𝑦 +Q ( 1Q ·Q 𝑏 ) ) = ( 𝑦 +Q 𝑏 ) )
103 102 eleq1d ⊢ ( ( 1Q ·Q 𝑏 ) = 𝑏 → ( ( 𝑦 +Q ( 1Q ·Q 𝑏 ) ) ∈ 𝐴 ↔ ( 𝑦 +Q 𝑏 ) ∈ 𝐴 ) )
104 103 biimpar ⊢ ( ( ( 1Q ·Q 𝑏 ) = 𝑏 ∧ ( 𝑦 +Q 𝑏 ) ∈ 𝐴 ) → ( 𝑦 +Q ( 1Q ·Q 𝑏 ) ) ∈ 𝐴 )
105 98 101 104 syl2an ⊢ ( ( 𝑏 ∈ Q ∧ ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑦 +Q ( 1Q ·Q 𝑏 ) ) ∈ 𝐴 )
106 105 3impb ⊢ ( ( 𝑏 ∈ Q ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 +Q ( 1Q ·Q 𝑏 ) ) ∈ 𝐴 )
107 3simpa ⊢ ( ( 𝑏 ∈ Q ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑏 ∈ Q ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ) )
108 oveq1 ⊢ ( 𝑥 = ( 𝑦 +Q ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) ) → ( 𝑥 +Q 𝑏 ) = ( ( 𝑦 +Q ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) ) +Q 𝑏 ) )
109 108 eleq1d ⊢ ( 𝑥 = ( 𝑦 +Q ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) ) → ( ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ↔ ( ( 𝑦 +Q ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) ) +Q 𝑏 ) ∈ 𝐴 ) )
110 109 rspccva ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ∧ ( 𝑦 +Q ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) ) ∈ 𝐴 ) → ( ( 𝑦 +Q ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) ) +Q 𝑏 ) ∈ 𝐴 )
111 addassnq ⊢ ( ( 𝑦 +Q ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) ) +Q 𝑏 ) = ( 𝑦 +Q ( ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) +Q 𝑏 ) )
112 opex ⊢ ⟨ 𝑧 , 1o ⟩ ∈ V
113 1nq ⊢ 1Q ∈ Q
114 113 elexi ⊢ 1Q ∈ V
115 distrnq ⊢ ( 𝑣 ·Q ( 𝑥 +Q 𝑦 ) ) = ( ( 𝑣 ·Q 𝑥 ) +Q ( 𝑣 ·Q 𝑦 ) )
116 112 114 43 46 115 caovdir ⊢ ( ( ⟨ 𝑧 , 1o ⟩ +Q 1Q ) ·Q 𝑏 ) = ( ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) +Q ( 1Q ·Q 𝑏 ) )
117 116 a1i ⊢ ( ( 𝑧 ∈ N ∧ 𝑏 ∈ Q ) → ( ( ⟨ 𝑧 , 1o ⟩ +Q 1Q ) ·Q 𝑏 ) = ( ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) +Q ( 1Q ·Q 𝑏 ) ) )
118 addpqnq ⊢ ( ( ⟨ 𝑧 , 1o ⟩ ∈ Q ∧ 1Q ∈ Q ) → ( ⟨ 𝑧 , 1o ⟩ +Q 1Q ) = ( [Q] ‘ ( ⟨ 𝑧 , 1o ⟩ +pQ 1Q ) ) )
119 62 113 118 sylancl ⊢ ( 𝑧 ∈ N → ( ⟨ 𝑧 , 1o ⟩ +Q 1Q ) = ( [Q] ‘ ( ⟨ 𝑧 , 1o ⟩ +pQ 1Q ) ) )
120 80 oveq2i ⊢ ( ⟨ 𝑧 , 1o ⟩ +pQ 1Q ) = ( ⟨ 𝑧 , 1o ⟩ +pQ ⟨ 1o , 1o ⟩ )
121 1pi ⊢ 1o ∈ N
122 addpipq ⊢ ( ( ( 𝑧 ∈ N ∧ 1o ∈ N ) ∧ ( 1o ∈ N ∧ 1o ∈ N ) ) → ( ⟨ 𝑧 , 1o ⟩ +pQ ⟨ 1o , 1o ⟩ ) = ⟨ ( ( 𝑧 ·N 1o ) +N ( 1o ·N 1o ) ) , ( 1o ·N 1o ) ⟩ )
123 121 121 122 mpanr12 ⊢ ( ( 𝑧 ∈ N ∧ 1o ∈ N ) → ( ⟨ 𝑧 , 1o ⟩ +pQ ⟨ 1o , 1o ⟩ ) = ⟨ ( ( 𝑧 ·N 1o ) +N ( 1o ·N 1o ) ) , ( 1o ·N 1o ) ⟩ )
124 121 123 mpan2 ⊢ ( 𝑧 ∈ N → ( ⟨ 𝑧 , 1o ⟩ +pQ ⟨ 1o , 1o ⟩ ) = ⟨ ( ( 𝑧 ·N 1o ) +N ( 1o ·N 1o ) ) , ( 1o ·N 1o ) ⟩ )
125 120 124 syl5eq ⊢ ( 𝑧 ∈ N → ( ⟨ 𝑧 , 1o ⟩ +pQ 1Q ) = ⟨ ( ( 𝑧 ·N 1o ) +N ( 1o ·N 1o ) ) , ( 1o ·N 1o ) ⟩ )
126 mulidpi ⊢ ( 𝑧 ∈ N → ( 𝑧 ·N 1o ) = 𝑧 )
127 mulidpi ⊢ ( 1o ∈ N → ( 1o ·N 1o ) = 1o )
128 121 127 mp1i ⊢ ( 𝑧 ∈ N → ( 1o ·N 1o ) = 1o )
129 126 128 oveq12d ⊢ ( 𝑧 ∈ N → ( ( 𝑧 ·N 1o ) +N ( 1o ·N 1o ) ) = ( 𝑧 +N 1o ) )
130 129 128 opeq12d ⊢ ( 𝑧 ∈ N → ⟨ ( ( 𝑧 ·N 1o ) +N ( 1o ·N 1o ) ) , ( 1o ·N 1o ) ⟩ = ⟨ ( 𝑧 +N 1o ) , 1o ⟩ )
131 125 130 eqtrd ⊢ ( 𝑧 ∈ N → ( ⟨ 𝑧 , 1o ⟩ +pQ 1Q ) = ⟨ ( 𝑧 +N 1o ) , 1o ⟩ )
132 131 fveq2d ⊢ ( 𝑧 ∈ N → ( [Q] ‘ ( ⟨ 𝑧 , 1o ⟩ +pQ 1Q ) ) = ( [Q] ‘ ⟨ ( 𝑧 +N 1o ) , 1o ⟩ ) )
133 addclpi ⊢ ( ( 𝑧 ∈ N ∧ 1o ∈ N ) → ( 𝑧 +N 1o ) ∈ N )
134 121 133 mpan2 ⊢ ( 𝑧 ∈ N → ( 𝑧 +N 1o ) ∈ N )
135 pinq ⊢ ( ( 𝑧 +N 1o ) ∈ N → ⟨ ( 𝑧 +N 1o ) , 1o ⟩ ∈ Q )
136 nqerid ⊢ ( ⟨ ( 𝑧 +N 1o ) , 1o ⟩ ∈ Q → ( [Q] ‘ ⟨ ( 𝑧 +N 1o ) , 1o ⟩ ) = ⟨ ( 𝑧 +N 1o ) , 1o ⟩ )
137 134 135 136 3syl ⊢ ( 𝑧 ∈ N → ( [Q] ‘ ⟨ ( 𝑧 +N 1o ) , 1o ⟩ ) = ⟨ ( 𝑧 +N 1o ) , 1o ⟩ )
138 119 132 137 3eqtrd ⊢ ( 𝑧 ∈ N → ( ⟨ 𝑧 , 1o ⟩ +Q 1Q ) = ⟨ ( 𝑧 +N 1o ) , 1o ⟩ )
139 138 adantr ⊢ ( ( 𝑧 ∈ N ∧ 𝑏 ∈ Q ) → ( ⟨ 𝑧 , 1o ⟩ +Q 1Q ) = ⟨ ( 𝑧 +N 1o ) , 1o ⟩ )
140 139 oveq1d ⊢ ( ( 𝑧 ∈ N ∧ 𝑏 ∈ Q ) → ( ( ⟨ 𝑧 , 1o ⟩ +Q 1Q ) ·Q 𝑏 ) = ( ⟨ ( 𝑧 +N 1o ) , 1o ⟩ ·Q 𝑏 ) )
141 98 adantl ⊢ ( ( 𝑧 ∈ N ∧ 𝑏 ∈ Q ) → ( 1Q ·Q 𝑏 ) = 𝑏 )
142 141 oveq2d ⊢ ( ( 𝑧 ∈ N ∧ 𝑏 ∈ Q ) → ( ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) +Q ( 1Q ·Q 𝑏 ) ) = ( ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) +Q 𝑏 ) )
143 117 140 142 3eqtr3rd ⊢ ( ( 𝑧 ∈ N ∧ 𝑏 ∈ Q ) → ( ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) +Q 𝑏 ) = ( ⟨ ( 𝑧 +N 1o ) , 1o ⟩ ·Q 𝑏 ) )
144 143 oveq2d ⊢ ( ( 𝑧 ∈ N ∧ 𝑏 ∈ Q ) → ( 𝑦 +Q ( ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) +Q 𝑏 ) ) = ( 𝑦 +Q ( ⟨ ( 𝑧 +N 1o ) , 1o ⟩ ·Q 𝑏 ) ) )
145 111 144 syl5eq ⊢ ( ( 𝑧 ∈ N ∧ 𝑏 ∈ Q ) → ( ( 𝑦 +Q ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) ) +Q 𝑏 ) = ( 𝑦 +Q ( ⟨ ( 𝑧 +N 1o ) , 1o ⟩ ·Q 𝑏 ) ) )
146 145 eleq1d ⊢ ( ( 𝑧 ∈ N ∧ 𝑏 ∈ Q ) → ( ( ( 𝑦 +Q ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) ) +Q 𝑏 ) ∈ 𝐴 ↔ ( 𝑦 +Q ( ⟨ ( 𝑧 +N 1o ) , 1o ⟩ ·Q 𝑏 ) ) ∈ 𝐴 ) )
147 110 146 syl5ib ⊢ ( ( 𝑧 ∈ N ∧ 𝑏 ∈ Q ) → ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ∧ ( 𝑦 +Q ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) ) ∈ 𝐴 ) → ( 𝑦 +Q ( ⟨ ( 𝑧 +N 1o ) , 1o ⟩ ·Q 𝑏 ) ) ∈ 𝐴 ) )
148 147 expd ⊢ ( ( 𝑧 ∈ N ∧ 𝑏 ∈ Q ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 → ( ( 𝑦 +Q ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) ) ∈ 𝐴 → ( 𝑦 +Q ( ⟨ ( 𝑧 +N 1o ) , 1o ⟩ ·Q 𝑏 ) ) ∈ 𝐴 ) ) )
149 148 expimpd ⊢ ( 𝑧 ∈ N → ( ( 𝑏 ∈ Q ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ) → ( ( 𝑦 +Q ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) ) ∈ 𝐴 → ( 𝑦 +Q ( ⟨ ( 𝑧 +N 1o ) , 1o ⟩ ·Q 𝑏 ) ) ∈ 𝐴 ) ) )
150 107 149 syl5 ⊢ ( 𝑧 ∈ N → ( ( 𝑏 ∈ Q ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑦 +Q ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) ) ∈ 𝐴 → ( 𝑦 +Q ( ⟨ ( 𝑧 +N 1o ) , 1o ⟩ ·Q 𝑏 ) ) ∈ 𝐴 ) ) )
151 150 a2d ⊢ ( 𝑧 ∈ N → ( ( ( 𝑏 ∈ Q ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 +Q ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) ) ∈ 𝐴 ) → ( ( 𝑏 ∈ Q ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 +Q ( ⟨ ( 𝑧 +N 1o ) , 1o ⟩ ·Q 𝑏 ) ) ∈ 𝐴 ) ) )
152 85 90 95 90 106 151 indpi ⊢ ( 𝑧 ∈ N → ( ( 𝑏 ∈ Q ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 +Q ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) ) ∈ 𝐴 ) )
153 152 imp ⊢ ( ( 𝑧 ∈ N ∧ ( 𝑏 ∈ Q ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑦 +Q ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) ) ∈ 𝐴 )
154 61 39 78 67 153 syl13anc ⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ) ∧ ( 𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( 𝑧 ∈ N ∧ ( 𝑤 ·Q ( *Q ‘ 𝑏 ) ) <Q ⟨ 𝑧 , 1o ⟩ ) ) → ( 𝑦 +Q ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) ) ∈ 𝐴 )
155 prcdnq ⊢ ( ( 𝐴 ∈ P ∧ ( 𝑦 +Q ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) ) ∈ 𝐴 ) → ( 𝑤 <Q ( 𝑦 +Q ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) ) → 𝑤 ∈ 𝐴 ) )
156 66 154 155 syl2anc ⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ) ∧ ( 𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( 𝑧 ∈ N ∧ ( 𝑤 ·Q ( *Q ‘ 𝑏 ) ) <Q ⟨ 𝑧 , 1o ⟩ ) ) → ( 𝑤 <Q ( 𝑦 +Q ( ⟨ 𝑧 , 1o ⟩ ·Q 𝑏 ) ) → 𝑤 ∈ 𝐴 ) )
157 77 156 mpd ⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ) ∧ ( 𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( 𝑧 ∈ N ∧ ( 𝑤 ·Q ( *Q ‘ 𝑏 ) ) <Q ⟨ 𝑧 , 1o ⟩ ) ) → 𝑤 ∈ 𝐴 )
158 38 157 rexlimddv ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ) ∧ ( 𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴 ) ) → 𝑤 ∈ 𝐴 )
159 158 expr ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ) ∧ 𝑤 ∈ Q ) → ( 𝑦 ∈ 𝐴 → 𝑤 ∈ 𝐴 ) )
160 159 exlimdv ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ) ∧ 𝑤 ∈ Q ) → ( ∃ 𝑦 𝑦 ∈ 𝐴 → 𝑤 ∈ 𝐴 ) )
161 30 160 mpd ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ) ∧ 𝑤 ∈ Q ) → 𝑤 ∈ 𝐴 )
162 26 161 eqelssd ⊢ ( ( 𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ) → 𝐴 = Q )
163 162 3expia ⊢ ( ( 𝐴 ∈ P ∧ 𝑏 ∈ Q ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 → 𝐴 = Q ) )
164 25 163 mtod ⊢ ( ( 𝐴 ∈ P ∧ 𝑏 ∈ Q ) → ¬ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 )
165 164 expcom ⊢ ( 𝑏 ∈ Q → ( 𝐴 ∈ P → ¬ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝑏 ) ∈ 𝐴 ) )
166 21 165 vtoclga ⊢ ( 𝐵 ∈ Q → ( 𝐴 ∈ P → ¬ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝐵 ) ∈ 𝐴 ) )
167 166 com12 ⊢ ( 𝐴 ∈ P → ( 𝐵 ∈ Q → ¬ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝐵 ) ∈ 𝐴 ) )
168 5 16 167 3syld ⊢ ( 𝐴 ∈ P → ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝐵 ) ∈ 𝐴 → ¬ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝐵 ) ∈ 𝐴 ) )
169 168 pm2.01d ⊢ ( 𝐴 ∈ P → ¬ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝐵 ) ∈ 𝐴 )
170 rexnal ⊢ ( ∃ 𝑥 ∈ 𝐴 ¬ ( 𝑥 +Q 𝐵 ) ∈ 𝐴 ↔ ¬ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +Q 𝐵 ) ∈ 𝐴 )
171 169 170 sylibr ⊢ ( 𝐴 ∈ P → ∃ 𝑥 ∈ 𝐴 ¬ ( 𝑥 +Q 𝐵 ) ∈ 𝐴 )