prlem934 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > prlem934		Structured version Visualization version GIF version

Theorem prlem934 9855

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.)

**Hypothesis**
Ref	Expression
prlem934.1	⊢ 𝐵 ∈ V

**Assertion**
Ref	Expression
prlem934	⊢ (𝐴 ∈ P → ∃𝑥 ∈ 𝐴 ¬ (𝑥 +_Q 𝐵) ∈ 𝐴)

Distinct variable groups: 𝑥,𝐴 𝑥,𝐵

Proof of Theorem prlem934 Dummy variables 𝑏 𝑤 𝑦 𝑧 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		prn0 9811	. . . . 5 ⊢ (𝐴 ∈ P → 𝐴 ≠ ∅)
2		r19.2z 4060	. . . . . 6 ⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝐵) ∈ 𝐴) → ∃𝑥 ∈ 𝐴 (𝑥 +_Q 𝐵) ∈ 𝐴)
3	2	ex 450	. . . . 5 ⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝐵) ∈ 𝐴 → ∃𝑥 ∈ 𝐴 (𝑥 +_Q 𝐵) ∈ 𝐴))
4	1, 3	syl 17	. . . 4 ⊢ (𝐴 ∈ P → (∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝐵) ∈ 𝐴 → ∃𝑥 ∈ 𝐴 (𝑥 +_Q 𝐵) ∈ 𝐴))
5		prpssnq 9812	. . . . . . . . 9 ⊢ (𝐴 ∈ P → 𝐴 ⊊ Q)
6	5	pssssd 3704	. . . . . . . 8 ⊢ (𝐴 ∈ P → 𝐴 ⊆ Q)
7	6	sseld 3602	. . . . . . 7 ⊢ (𝐴 ∈ P → ((𝑥 +_Q 𝐵) ∈ 𝐴 → (𝑥 +_Q 𝐵) ∈ Q))
8		addnqf 9770	. . . . . . . . . 10 ⊢ +_Q :(Q × Q)⟶Q
9	8	fdmi 6052	. . . . . . . . 9 ⊢ dom +_Q = (Q × Q)
10		0nnq 9746	. . . . . . . . 9 ⊢ ¬ ∅ ∈ Q
11	9, 10	ndmovrcl 6820	. . . . . . . 8 ⊢ ((𝑥 +_Q 𝐵) ∈ Q → (𝑥 ∈ Q ∧ 𝐵 ∈ Q))
12	11	simprd 479	. . . . . . 7 ⊢ ((𝑥 +_Q 𝐵) ∈ Q → 𝐵 ∈ Q)
13	7, 12	syl6com 37	. . . . . 6 ⊢ ((𝑥 +_Q 𝐵) ∈ 𝐴 → (𝐴 ∈ P → 𝐵 ∈ Q))
14	13	rexlimivw 3029	. . . . 5 ⊢ (∃𝑥 ∈ 𝐴 (𝑥 +_Q 𝐵) ∈ 𝐴 → (𝐴 ∈ P → 𝐵 ∈ Q))
15	14	com12 32	. . . 4 ⊢ (𝐴 ∈ P → (∃𝑥 ∈ 𝐴 (𝑥 +_Q 𝐵) ∈ 𝐴 → 𝐵 ∈ Q))
16		oveq2 6658	. . . . . . . . . 10 ⊢ (𝑏 = 𝐵 → (𝑥 +_Q 𝑏) = (𝑥 +_Q 𝐵))
17	16	eleq1d 2686	. . . . . . . . 9 ⊢ (𝑏 = 𝐵 → ((𝑥 +_Q 𝑏) ∈ 𝐴 ↔ (𝑥 +_Q 𝐵) ∈ 𝐴))
18	17	ralbidv 2986	. . . . . . . 8 ⊢ (𝑏 = 𝐵 → (∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴 ↔ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝐵) ∈ 𝐴))
19	18	notbid 308	. . . . . . 7 ⊢ (𝑏 = 𝐵 → (¬ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴 ↔ ¬ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝐵) ∈ 𝐴))
20	19	imbi2d 330	. . . . . 6 ⊢ (𝑏 = 𝐵 → ((𝐴 ∈ P → ¬ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ↔ (𝐴 ∈ P → ¬ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝐵) ∈ 𝐴)))
21		dfpss2 3692	. . . . . . . . . . 11 ⊢ (𝐴 ⊊ Q ↔ (𝐴 ⊆ Q ∧ ¬ 𝐴 = Q))
22	5, 21	sylib 208	. . . . . . . . . 10 ⊢ (𝐴 ∈ P → (𝐴 ⊆ Q ∧ ¬ 𝐴 = Q))
23	22	simprd 479	. . . . . . . . 9 ⊢ (𝐴 ∈ P → ¬ 𝐴 = Q)
24	23	adantr 481	. . . . . . . 8 ⊢ ((𝐴 ∈ P ∧ 𝑏 ∈ Q) → ¬ 𝐴 = Q)
25	6	3ad2ant1 1082	. . . . . . . . . 10 ⊢ ((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) → 𝐴 ⊆ Q)
26		simpl1 1064	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ 𝑤 ∈ Q) → 𝐴 ∈ P)
27		n0 3931	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ 𝐴)
28	1, 27	sylib 208	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ P → ∃𝑦 𝑦 ∈ 𝐴)
29	26, 28	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ 𝑤 ∈ Q) → ∃𝑦 𝑦 ∈ 𝐴)
30		simprl 794	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) → 𝑤 ∈ Q)
31		simpl2 1065	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) → 𝑏 ∈ Q)
32		recclnq 9788	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ∈ Q → (*_Q‘𝑏) ∈ Q)
33		mulclnq 9769	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑤 ∈ Q ∧ (_Q‘𝑏) ∈ Q) → (𝑤 ·_Q (_Q‘𝑏)) ∈ Q)
34		archnq 9802	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑤 ·_Q (_Q‘𝑏)) ∈ Q → ∃𝑧 ∈ N (𝑤 ·_Q (_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩)
35	33, 34	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑤 ∈ Q ∧ (_Q‘𝑏) ∈ Q) → ∃𝑧 ∈ N (𝑤 ·_Q (_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩)
36	32, 35	sylan2 491	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑤 ∈ Q ∧ 𝑏 ∈ Q) → ∃𝑧 ∈ N (𝑤 ·_Q (*_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩)
37	30, 31, 36	syl2anc 693	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) → ∃𝑧 ∈ N (𝑤 ·_Q (*_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩)
38		simpll2 1101	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·_Q (*_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩)) → 𝑏 ∈ Q)
39		simplrl 800	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·_Q (*_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩)) → 𝑤 ∈ Q)
40		simprr 796	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·_Q (_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩)) → (𝑤 ·_Q (_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩)
41		ltmnq 9794	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 ∈ Q → ((𝑤 ·_Q (_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩ ↔ (𝑏 ·_Q (𝑤 ·_Q (_Q‘𝑏))) <_Q (𝑏 ·_Q ⟨𝑧, 1_𝑜⟩)))
42		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑏 ∈ V
43		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑤 ∈ V
44		fvex 6201	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (*_Q‘𝑏) ∈ V
45		mulcomnq 9775	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑣 ·_Q 𝑥) = (𝑥 ·_Q 𝑣)
46		mulassnq 9781	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑣 ·_Q 𝑥) ·_Q 𝑦) = (𝑣 ·_Q (𝑥 ·_Q 𝑦))
47	42, 43, 44, 45, 46	caov12 6862	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 ·_Q (𝑤 ·_Q (_Q‘𝑏))) = (𝑤 ·_Q (𝑏 ·_Q (_Q‘𝑏)))
48		mulcomnq 9775	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 ·_Q ⟨𝑧, 1_𝑜⟩) = (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)
49	47, 48	breq12i 4662	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑏 ·_Q (𝑤 ·_Q (_Q‘𝑏))) <_Q (𝑏 ·_Q ⟨𝑧, 1_𝑜⟩) ↔ (𝑤 ·_Q (𝑏 ·_Q (_Q‘𝑏))) <_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏))
50	41, 49	syl6bb 276	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 ∈ Q → ((𝑤 ·_Q (_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩ ↔ (𝑤 ·_Q (𝑏 ·_Q (_Q‘𝑏))) <_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)))
51	50	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑏 ∈ Q ∧ 𝑤 ∈ Q) → ((𝑤 ·_Q (_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩ ↔ (𝑤 ·_Q (𝑏 ·_Q (_Q‘𝑏))) <_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)))
52		recidnq 9787	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 ∈ Q → (𝑏 ·_Q (*_Q‘𝑏)) = 1_Q)
53	52	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 ∈ Q → (𝑤 ·_Q (𝑏 ·_Q (*_Q‘𝑏))) = (𝑤 ·_Q 1_Q))
54		mulidnq 9785	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ Q → (𝑤 ·_Q 1_Q) = 𝑤)
55	53, 54	sylan9eq 2676	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑏 ∈ Q ∧ 𝑤 ∈ Q) → (𝑤 ·_Q (𝑏 ·_Q (*_Q‘𝑏))) = 𝑤)
56	55	breq1d 4663	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑏 ∈ Q ∧ 𝑤 ∈ Q) → ((𝑤 ·_Q (𝑏 ·_Q (*_Q‘𝑏))) <_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏) ↔ 𝑤 <_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)))
57	51, 56	bitrd 268	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑏 ∈ Q ∧ 𝑤 ∈ Q) → ((𝑤 ·_Q (*_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩ ↔ 𝑤 <_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)))
58	57	biimpa 501	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑏 ∈ Q ∧ 𝑤 ∈ Q) ∧ (𝑤 ·_Q (*_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩) → 𝑤 <_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏))
59	38, 39, 40, 58	syl21anc 1325	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·_Q (*_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩)) → 𝑤 <_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏))
60		simprl 794	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·_Q (*_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩)) → 𝑧 ∈ N)
61		pinq 9749	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ N → ⟨𝑧, 1_𝑜⟩ ∈ Q)
62		mulclnq 9769	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⟨𝑧, 1_𝑜⟩ ∈ Q ∧ 𝑏 ∈ Q) → (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏) ∈ Q)
63	61, 62	sylan 488	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ N ∧ 𝑏 ∈ Q) → (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏) ∈ Q)
64	60, 38, 63	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·_Q (*_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩)) → (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏) ∈ Q)
65		simpll1 1100	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·_Q (*_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩)) → 𝐴 ∈ P)
66		simplrr 801	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·_Q (*_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩)) → 𝑦 ∈ 𝐴)
67		elprnq 9813	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ P ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ Q)
68	65, 66, 67	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·_Q (*_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩)) → 𝑦 ∈ Q)
69		ltaddnq 9796	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((⟨𝑧, 1_𝑜⟩ ·_Q 𝑏) ∈ Q ∧ 𝑦 ∈ Q) → (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏) <_Q ((⟨𝑧, 1_𝑜⟩ ·_Q 𝑏) +_Q 𝑦))
70		addcomnq 9773	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⟨𝑧, 1_𝑜⟩ ·_Q 𝑏) +_Q 𝑦) = (𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏))
71	69, 70	syl6breq 4694	. . . . . . . . . . . . . . . . . . 19 ⊢ (((⟨𝑧, 1_𝑜⟩ ·_Q 𝑏) ∈ Q ∧ 𝑦 ∈ Q) → (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏) <_Q (𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)))
72	64, 68, 71	syl2anc 693	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·_Q (*_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩)) → (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏) <_Q (𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)))
73		ltsonq 9791	. . . . . . . . . . . . . . . . . . 19 ⊢ <_Q Or Q
74		ltrelnq 9748	. . . . . . . . . . . . . . . . . . 19 ⊢ <_Q ⊆ (Q × Q)
75	73, 74	sotri 5523	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑤 <_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏) ∧ (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏) <_Q (𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏))) → 𝑤 <_Q (𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)))
76	59, 72, 75	syl2anc 693	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·_Q (*_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩)) → 𝑤 <_Q (𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)))
77		simpll3 1102	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·_Q (*_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩)) → ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴)
78		opeq1 4402	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 = 1_𝑜 → ⟨𝑤, 1_𝑜⟩ = ⟨1_𝑜, 1_𝑜⟩)
79		df-1nq 9738	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 1_Q = ⟨1_𝑜, 1_𝑜⟩
80	78, 79	syl6eqr 2674	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = 1_𝑜 → ⟨𝑤, 1_𝑜⟩ = 1_Q)
81	80	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = 1_𝑜 → (⟨𝑤, 1_𝑜⟩ ·_Q 𝑏) = (1_Q ·_Q 𝑏))
82	81	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 1_𝑜 → (𝑦 +_Q (⟨𝑤, 1_𝑜⟩ ·_Q 𝑏)) = (𝑦 +_Q (1_Q ·_Q 𝑏)))
83	82	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 1_𝑜 → ((𝑦 +_Q (⟨𝑤, 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴 ↔ (𝑦 +_Q (1_Q ·_Q 𝑏)) ∈ 𝐴))
84	83	imbi2d 330	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 1_𝑜 → (((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +_Q (⟨𝑤, 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴) ↔ ((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +_Q (1_Q ·_Q 𝑏)) ∈ 𝐴)))
85		opeq1 4402	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = 𝑧 → ⟨𝑤, 1_𝑜⟩ = ⟨𝑧, 1_𝑜⟩)
86	85	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = 𝑧 → (⟨𝑤, 1_𝑜⟩ ·_Q 𝑏) = (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏))
87	86	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑧 → (𝑦 +_Q (⟨𝑤, 1_𝑜⟩ ·_Q 𝑏)) = (𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)))
88	87	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑧 → ((𝑦 +_Q (⟨𝑤, 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴 ↔ (𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴))
89	88	imbi2d 330	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑧 → (((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +_Q (⟨𝑤, 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴) ↔ ((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴)))
90		opeq1 4402	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = (𝑧 +_N 1_𝑜) → ⟨𝑤, 1_𝑜⟩ = ⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩)
91	90	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = (𝑧 +_N 1_𝑜) → (⟨𝑤, 1_𝑜⟩ ·_Q 𝑏) = (⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩ ·_Q 𝑏))
92	91	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = (𝑧 +_N 1_𝑜) → (𝑦 +_Q (⟨𝑤, 1_𝑜⟩ ·_Q 𝑏)) = (𝑦 +_Q (⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩ ·_Q 𝑏)))
93	92	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = (𝑧 +_N 1_𝑜) → ((𝑦 +_Q (⟨𝑤, 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴 ↔ (𝑦 +_Q (⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴))
94	93	imbi2d 330	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = (𝑧 +_N 1_𝑜) → (((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +_Q (⟨𝑤, 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴) ↔ ((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +_Q (⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴)))
95		mulcomnq 9775	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1_Q ·_Q 𝑏) = (𝑏 ·_Q 1_Q)
96		mulidnq 9785	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 ∈ Q → (𝑏 ·_Q 1_Q) = 𝑏)
97	95, 96	syl5eq 2668	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 ∈ Q → (1_Q ·_Q 𝑏) = 𝑏)
98		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑦 → (𝑥 +_Q 𝑏) = (𝑦 +_Q 𝑏))
99	98	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑦 → ((𝑥 +_Q 𝑏) ∈ 𝐴 ↔ (𝑦 +_Q 𝑏) ∈ 𝐴))
100	99	rspccva 3308	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +_Q 𝑏) ∈ 𝐴)
101		oveq2 6658	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((1_Q ·_Q 𝑏) = 𝑏 → (𝑦 +_Q (1_Q ·_Q 𝑏)) = (𝑦 +_Q 𝑏))
102	101	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((1_Q ·_Q 𝑏) = 𝑏 → ((𝑦 +_Q (1_Q ·_Q 𝑏)) ∈ 𝐴 ↔ (𝑦 +_Q 𝑏) ∈ 𝐴))
103	102	biimpar 502	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((1_Q ·_Q 𝑏) = 𝑏 ∧ (𝑦 +_Q 𝑏) ∈ 𝐴) → (𝑦 +_Q (1_Q ·_Q 𝑏)) ∈ 𝐴)
104	97, 100, 103	syl2an 494	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑏 ∈ Q ∧ (∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑦 +_Q (1_Q ·_Q 𝑏)) ∈ 𝐴)
105	104	3impb 1260	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +_Q (1_Q ·_Q 𝑏)) ∈ 𝐴)
106		3simpa 1058	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴))
107		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 = (𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) → (𝑥 +_Q 𝑏) = ((𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) +_Q 𝑏))
108	107	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = (𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) → ((𝑥 +_Q 𝑏) ∈ 𝐴 ↔ ((𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) +_Q 𝑏) ∈ 𝐴))
109	108	rspccva 3308	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴 ∧ (𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴) → ((𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) +_Q 𝑏) ∈ 𝐴)
110		addassnq 9780	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) +_Q 𝑏) = (𝑦 +_Q ((⟨𝑧, 1_𝑜⟩ ·_Q 𝑏) +_Q 𝑏))
111		opex 4932	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ⟨𝑧, 1_𝑜⟩ ∈ V
112		1nq 9750	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 1_Q ∈ Q
113	112	elexi 3213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 1_Q ∈ V
114		distrnq 9783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑣 ·_Q (𝑥 +_Q 𝑦)) = ((𝑣 ·_Q 𝑥) +_Q (𝑣 ·_Q 𝑦))
115	111, 113, 42, 45, 114	caovdir 6868	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((⟨𝑧, 1_𝑜⟩ +_Q 1_Q) ·_Q 𝑏) = ((⟨𝑧, 1_𝑜⟩ ·_Q 𝑏) +_Q (1_Q ·_Q 𝑏))
116	115	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑧 ∈ N ∧ 𝑏 ∈ Q) → ((⟨𝑧, 1_𝑜⟩ +_Q 1_Q) ·_Q 𝑏) = ((⟨𝑧, 1_𝑜⟩ ·_Q 𝑏) +_Q (1_Q ·_Q 𝑏)))
117		addpqnq 9760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((⟨𝑧, 1_𝑜⟩ ∈ Q ∧ 1_Q ∈ Q) → (⟨𝑧, 1_𝑜⟩ +_Q 1_Q) = ([Q]‘(⟨𝑧, 1_𝑜⟩ +_pQ 1_Q)))
118	61, 112, 117	sylancl 694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 ∈ N → (⟨𝑧, 1_𝑜⟩ +_Q 1_Q) = ([Q]‘(⟨𝑧, 1_𝑜⟩ +_pQ 1_Q)))
119	79	oveq2i 6661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (⟨𝑧, 1_𝑜⟩ +_pQ 1_Q) = (⟨𝑧, 1_𝑜⟩ +_pQ ⟨1_𝑜, 1_𝑜⟩)
120		1pi 9705	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ 1_𝑜 ∈ N
121		addpipq 9759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝑧 ∈ N ∧ 1_𝑜 ∈ N) ∧ (1_𝑜 ∈ N ∧ 1_𝑜 ∈ N)) → (⟨𝑧, 1_𝑜⟩ +_pQ ⟨1_𝑜, 1_𝑜⟩) = ⟨((𝑧 ·_N 1_𝑜) +_N (1_𝑜 ·_N 1_𝑜)), (1_𝑜 ·_N 1_𝑜)⟩)
122	120, 120, 121	mpanr12 721	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑧 ∈ N ∧ 1_𝑜 ∈ N) → (⟨𝑧, 1_𝑜⟩ +_pQ ⟨1_𝑜, 1_𝑜⟩) = ⟨((𝑧 ·_N 1_𝑜) +_N (1_𝑜 ·_N 1_𝑜)), (1_𝑜 ·_N 1_𝑜)⟩)
123	120, 122	mpan2 707	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑧 ∈ N → (⟨𝑧, 1_𝑜⟩ +_pQ ⟨1_𝑜, 1_𝑜⟩) = ⟨((𝑧 ·_N 1_𝑜) +_N (1_𝑜 ·_N 1_𝑜)), (1_𝑜 ·_N 1_𝑜)⟩)
124	119, 123	syl5eq 2668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑧 ∈ N → (⟨𝑧, 1_𝑜⟩ +_pQ 1_Q) = ⟨((𝑧 ·_N 1_𝑜) +_N (1_𝑜 ·_N 1_𝑜)), (1_𝑜 ·_N 1_𝑜)⟩)
125		mulidpi 9708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑧 ∈ N → (𝑧 ·_N 1_𝑜) = 𝑧)
126		mulidpi 9708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (1_𝑜 ∈ N → (1_𝑜 ·_N 1_𝑜) = 1_𝑜)
127	120, 126	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑧 ∈ N → (1_𝑜 ·_N 1_𝑜) = 1_𝑜)
128	125, 127	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑧 ∈ N → ((𝑧 ·_N 1_𝑜) +_N (1_𝑜 ·_N 1_𝑜)) = (𝑧 +_N 1_𝑜))
129	128, 127	opeq12d 4410	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑧 ∈ N → ⟨((𝑧 ·_N 1_𝑜) +_N (1_𝑜 ·_N 1_𝑜)), (1_𝑜 ·_N 1_𝑜)⟩ = ⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩)
130	124, 129	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑧 ∈ N → (⟨𝑧, 1_𝑜⟩ +_pQ 1_Q) = ⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩)
131	130	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 ∈ N → ([Q]‘(⟨𝑧, 1_𝑜⟩ +_pQ 1_Q)) = ([Q]‘⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩))
132		addclpi 9714	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑧 ∈ N ∧ 1_𝑜 ∈ N) → (𝑧 +_N 1_𝑜) ∈ N)
133	120, 132	mpan2 707	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑧 ∈ N → (𝑧 +_N 1_𝑜) ∈ N)
134		pinq 9749	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑧 +_N 1_𝑜) ∈ N → ⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩ ∈ Q)
135		nqerid 9755	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩ ∈ Q → ([Q]‘⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩) = ⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩)
136	133, 134, 135	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 ∈ N → ([Q]‘⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩) = ⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩)
137	118, 131, 136	3eqtrd 2660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑧 ∈ N → (⟨𝑧, 1_𝑜⟩ +_Q 1_Q) = ⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩)
138	137	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑧 ∈ N ∧ 𝑏 ∈ Q) → (⟨𝑧, 1_𝑜⟩ +_Q 1_Q) = ⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩)
139	138	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑧 ∈ N ∧ 𝑏 ∈ Q) → ((⟨𝑧, 1_𝑜⟩ +_Q 1_Q) ·_Q 𝑏) = (⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩ ·_Q 𝑏))
140	97	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑧 ∈ N ∧ 𝑏 ∈ Q) → (1_Q ·_Q 𝑏) = 𝑏)
141	140	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑧 ∈ N ∧ 𝑏 ∈ Q) → ((⟨𝑧, 1_𝑜⟩ ·_Q 𝑏) +_Q (1_Q ·_Q 𝑏)) = ((⟨𝑧, 1_𝑜⟩ ·_Q 𝑏) +_Q 𝑏))
142	116, 139, 141	3eqtr3rd 2665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑧 ∈ N ∧ 𝑏 ∈ Q) → ((⟨𝑧, 1_𝑜⟩ ·_Q 𝑏) +_Q 𝑏) = (⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩ ·_Q 𝑏))
143	142	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑧 ∈ N ∧ 𝑏 ∈ Q) → (𝑦 +_Q ((⟨𝑧, 1_𝑜⟩ ·_Q 𝑏) +_Q 𝑏)) = (𝑦 +_Q (⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩ ·_Q 𝑏)))
144	110, 143	syl5eq 2668	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑧 ∈ N ∧ 𝑏 ∈ Q) → ((𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) +_Q 𝑏) = (𝑦 +_Q (⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩ ·_Q 𝑏)))
145	144	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑧 ∈ N ∧ 𝑏 ∈ Q) → (((𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) +_Q 𝑏) ∈ 𝐴 ↔ (𝑦 +_Q (⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴))
146	109, 145	syl5ib 234	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑧 ∈ N ∧ 𝑏 ∈ Q) → ((∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴 ∧ (𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴) → (𝑦 +_Q (⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴))
147	146	expd 452	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑧 ∈ N ∧ 𝑏 ∈ Q) → (∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴 → ((𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴 → (𝑦 +_Q (⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴)))
148	147	expimpd 629	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ N → ((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) → ((𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴 → (𝑦 +_Q (⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴)))
149	106, 148	syl5 34	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ N → ((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴 → (𝑦 +_Q (⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴)))
150	149	a2d 29	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ N → (((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴) → ((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +_Q (⟨(𝑧 +_N 1_𝑜), 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴)))
151	84, 89, 94, 89, 105, 150	indpi 9729	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ N → ((𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴))
152	151	imp 445	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 ∈ N ∧ (𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴)
153	60, 38, 77, 66, 152	syl13anc 1328	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·_Q (*_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩)) → (𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴)
154		prcdnq 9815	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ P ∧ (𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) ∈ 𝐴) → (𝑤 <_Q (𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) → 𝑤 ∈ 𝐴))
155	65, 153, 154	syl2anc 693	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·_Q (*_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩)) → (𝑤 <_Q (𝑦 +_Q (⟨𝑧, 1_𝑜⟩ ·_Q 𝑏)) → 𝑤 ∈ 𝐴))
156	76, 155	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) ∧ (𝑧 ∈ N ∧ (𝑤 ·_Q (*_Q‘𝑏)) <_Q ⟨𝑧, 1_𝑜⟩)) → 𝑤 ∈ 𝐴)
157	37, 156	rexlimddv 3035	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ (𝑤 ∈ Q ∧ 𝑦 ∈ 𝐴)) → 𝑤 ∈ 𝐴)
158	157	expr 643	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ 𝑤 ∈ Q) → (𝑦 ∈ 𝐴 → 𝑤 ∈ 𝐴))
159	158	exlimdv 1861	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ 𝑤 ∈ Q) → (∃𝑦 𝑦 ∈ 𝐴 → 𝑤 ∈ 𝐴))
160	29, 159	mpd 15	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) ∧ 𝑤 ∈ Q) → 𝑤 ∈ 𝐴)
161	160	ex 450	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) → (𝑤 ∈ Q → 𝑤 ∈ 𝐴))
162	161	ssrdv 3609	. . . . . . . . . 10 ⊢ ((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) → Q ⊆ 𝐴)
163	25, 162	eqssd 3620	. . . . . . . . 9 ⊢ ((𝐴 ∈ P ∧ 𝑏 ∈ Q ∧ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴) → 𝐴 = Q)
164	163	3expia 1267	. . . . . . . 8 ⊢ ((𝐴 ∈ P ∧ 𝑏 ∈ Q) → (∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴 → 𝐴 = Q))
165	24, 164	mtod 189	. . . . . . 7 ⊢ ((𝐴 ∈ P ∧ 𝑏 ∈ Q) → ¬ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴)
166	165	expcom 451	. . . . . 6 ⊢ (𝑏 ∈ Q → (𝐴 ∈ P → ¬ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝑏) ∈ 𝐴))
167	20, 166	vtoclga 3272	. . . . 5 ⊢ (𝐵 ∈ Q → (𝐴 ∈ P → ¬ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝐵) ∈ 𝐴))
168	167	com12 32	. . . 4 ⊢ (𝐴 ∈ P → (𝐵 ∈ Q → ¬ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝐵) ∈ 𝐴))
169	4, 15, 168	3syld 60	. . 3 ⊢ (𝐴 ∈ P → (∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝐵) ∈ 𝐴 → ¬ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝐵) ∈ 𝐴))
170	169	pm2.01d 181	. 2 ⊢ (𝐴 ∈ P → ¬ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝐵) ∈ 𝐴)
171		rexnal 2995	. 2 ⊢ (∃𝑥 ∈ 𝐴 ¬ (𝑥 +_Q 𝐵) ∈ 𝐴 ↔ ¬ ∀𝑥 ∈ 𝐴 (𝑥 +_Q 𝐵) ∈ 𝐴)
172	170, 171	sylibr 224	1 ⊢ (𝐴 ∈ P → ∃𝑥 ∈ 𝐴 ¬ (𝑥 +_Q 𝐵) ∈ 𝐴)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∃wex 1704 ∈ wcel 1990 ≠ wne 2794 ∀wral 2912 ∃wrex 2913 Vcvv 3200 ⊆ wss 3574 ⊊ wpss 3575 ∅c0 3915 ⟨cop 4183 class class class wbr 4653 × cxp 5112 ‘cfv 5888 (class class class)co 6650 1_𝑜c1o 7553 Ncnpi 9666 +_N cpli 9667 ·_N cmi 9668 +_pQ cplpq 9670 Qcnq 9674 1_Qc1q 9675 [Q]cerq 9676 +_Q cplq 9677 ·_Q cmq 9678 *_Qcrq 9679 <_Q cltq 9680 Pcnp 9681

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-omul 7565 df-er 7742 df-ni 9694 df-pli 9695 df-mi 9696 df-lti 9697 df-plpq 9730 df-mpq 9731 df-ltpq 9732 df-enq 9733 df-nq 9734 df-erq 9735 df-plq 9736 df-mq 9737 df-1nq 9738 df-rq 9739 df-ltnq 9740 df-np 9803

This theorem is referenced by: ltaddpr 9856 ltexprlem7 9864 prlem936 9869

W3C validator