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	eqtrid	⊢ ( ( 𝑦 ∈ 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	eqtrid	⊢ ( ( ( 𝑥 ·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	eqtrid	⊢ ( ( ( 𝑥 ·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	eqtrid	⊢ ( ( ( 𝑥 ·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 𝐵 ) ∈ 𝐴 )