Theorem prarloclem5 6690

Description: A substitution of zero for 𝑦 and 𝑁 minus two for 𝑥. Lemma for prarloc 6693. (Contributed by Jim Kingdon, 4-Nov-2019.)

Assertion

Ref	Expression
prarloclem5	⊢ (((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ 𝐿) ∧ (𝑁 ∈ N ∧ 𝑃 ∈ Q ∧ 1𝑜 <N 𝑁) ∧ (𝐴 +Q ([⟨𝑁, 1𝑜⟩] ~Q ·Q 𝑃)) ∈ 𝑈) → ∃𝑥 ∈ ω ∃𝑦 ∈ ω ((𝐴 +Q0 ([⟨𝑦, 1𝑜⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨((𝑦 +𝑜 2𝑜) +𝑜 𝑥), 1𝑜⟩] ~Q ·Q 𝑃)) ∈ 𝑈))

Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐿,𝑦   𝑥,𝑁   𝑥,𝑃,𝑦   𝑥,𝑈,𝑦

Allowed substitution hint:   𝑁(𝑦)

Proof of Theorem prarloclem5

Step	Hyp	Ref	Expression
1		prarloclemn 6689	. . . 4 ⊢ ((𝑁 ∈ N ∧ 1𝑜 <N 𝑁) → ∃𝑥 ∈ ω (2𝑜 +𝑜 𝑥) = 𝑁)
2	1	3adant2 957	. . 3 ⊢ ((𝑁 ∈ N ∧ 𝑃 ∈ Q ∧ 1𝑜 <N 𝑁) → ∃𝑥 ∈ ω (2𝑜 +𝑜 𝑥) = 𝑁)
3	2	3ad2ant2 960	. 2 ⊢ (((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ 𝐿) ∧ (𝑁 ∈ N ∧ 𝑃 ∈ Q ∧ 1𝑜 <N 𝑁) ∧ (𝐴 +Q ([⟨𝑁, 1𝑜⟩] ~Q ·Q 𝑃)) ∈ 𝑈) → ∃𝑥 ∈ ω (2𝑜 +𝑜 𝑥) = 𝑁)
4		elprnql 6671	. . . . . . 7 ⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ 𝐿) → 𝐴 ∈ Q)
5	4	3ad2ant1 959	. . . . . 6 ⊢ (((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ 𝐿) ∧ (𝑁 ∈ N ∧ 𝑃 ∈ Q ∧ 1𝑜 <N 𝑁) ∧ (𝐴 +Q ([⟨𝑁, 1𝑜⟩] ~Q ·Q 𝑃)) ∈ 𝑈) → 𝐴 ∈ Q)
6		simp22 972	. . . . . 6 ⊢ (((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ 𝐿) ∧ (𝑁 ∈ N ∧ 𝑃 ∈ Q ∧ 1𝑜 <N 𝑁) ∧ (𝐴 +Q ([⟨𝑁, 1𝑜⟩] ~Q ·Q 𝑃)) ∈ 𝑈) → 𝑃 ∈ Q)
7		nqnq0 6631	. . . . . . . . 9 ⊢ Q ⊆ Q0
8	7	sseli 2995	. . . . . . . 8 ⊢ (𝐴 ∈ Q → 𝐴 ∈ Q0)
9		nq0a0 6647	. . . . . . . 8 ⊢ (𝐴 ∈ Q0 → (𝐴 +Q0 0Q0) = 𝐴)
10	8, 9	syl 14	. . . . . . 7 ⊢ (𝐴 ∈ Q → (𝐴 +Q0 0Q0) = 𝐴)
11		df-0nq0 6616	. . . . . . . . . 10 ⊢ 0Q0 = [⟨∅, 1𝑜⟩] ~Q0
12	11	oveq1i 5542	. . . . . . . . 9 ⊢ (0Q0 ·Q0 𝑃) = ([⟨∅, 1𝑜⟩] ~Q0 ·Q0 𝑃)
13	7	sseli 2995	. . . . . . . . . 10 ⊢ (𝑃 ∈ Q → 𝑃 ∈ Q0)
14		nq0m0r 6646	. . . . . . . . . 10 ⊢ (𝑃 ∈ Q0 → (0Q0 ·Q0 𝑃) = 0Q0)
15	13, 14	syl 14	. . . . . . . . 9 ⊢ (𝑃 ∈ Q → (0Q0 ·Q0 𝑃) = 0Q0)
16	12, 15	syl5reqr 2128	. . . . . . . 8 ⊢ (𝑃 ∈ Q → 0Q0 = ([⟨∅, 1𝑜⟩] ~Q0 ·Q0 𝑃))
17	16	oveq2d 5548	. . . . . . 7 ⊢ (𝑃 ∈ Q → (𝐴 +Q0 0Q0) = (𝐴 +Q0 ([⟨∅, 1𝑜⟩] ~Q0 ·Q0 𝑃)))
18	10, 17	sylan9req 2134	. . . . . 6 ⊢ ((𝐴 ∈ Q ∧ 𝑃 ∈ Q) → 𝐴 = (𝐴 +Q0 ([⟨∅, 1𝑜⟩] ~Q0 ·Q0 𝑃)))
19	5, 6, 18	syl2anc 403	. . . . 5 ⊢ (((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ 𝐿) ∧ (𝑁 ∈ N ∧ 𝑃 ∈ Q ∧ 1𝑜 <N 𝑁) ∧ (𝐴 +Q ([⟨𝑁, 1𝑜⟩] ~Q ·Q 𝑃)) ∈ 𝑈) → 𝐴 = (𝐴 +Q0 ([⟨∅, 1𝑜⟩] ~Q0 ·Q0 𝑃)))
20		simp1r 963	. . . . 5 ⊢ (((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ 𝐿) ∧ (𝑁 ∈ N ∧ 𝑃 ∈ Q ∧ 1𝑜 <N 𝑁) ∧ (𝐴 +Q ([⟨𝑁, 1𝑜⟩] ~Q ·Q 𝑃)) ∈ 𝑈) → 𝐴 ∈ 𝐿)
21	19, 20	eqeltrrd 2156	. . . 4 ⊢ (((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ 𝐿) ∧ (𝑁 ∈ N ∧ 𝑃 ∈ Q ∧ 1𝑜 <N 𝑁) ∧ (𝐴 +Q ([⟨𝑁, 1𝑜⟩] ~Q ·Q 𝑃)) ∈ 𝑈) → (𝐴 +Q0 ([⟨∅, 1𝑜⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿)
22		2onn 6117	. . . . . . . . . . . . . . 15 ⊢ 2𝑜 ∈ ω
23		nna0r 6080	. . . . . . . . . . . . . . 15 ⊢ (2𝑜 ∈ ω → (∅ +𝑜 2𝑜) = 2𝑜)
24	22, 23	ax-mp 7	. . . . . . . . . . . . . 14 ⊢ (∅ +𝑜 2𝑜) = 2𝑜
25	24	oveq1i 5542	. . . . . . . . . . . . 13 ⊢ ((∅ +𝑜 2𝑜) +𝑜 𝑥) = (2𝑜 +𝑜 𝑥)
26	25	eqeq1i 2088	. . . . . . . . . . . 12 ⊢ (((∅ +𝑜 2𝑜) +𝑜 𝑥) = 𝑁 ↔ (2𝑜 +𝑜 𝑥) = 𝑁)
27	26	biimpri 131	. . . . . . . . . . 11 ⊢ ((2𝑜 +𝑜 𝑥) = 𝑁 → ((∅ +𝑜 2𝑜) +𝑜 𝑥) = 𝑁)
28	27	opeq1d 3576	. . . . . . . . . 10 ⊢ ((2𝑜 +𝑜 𝑥) = 𝑁 → ⟨((∅ +𝑜 2𝑜) +𝑜 𝑥), 1𝑜⟩ = ⟨𝑁, 1𝑜⟩)
29	28	eceq1d 6165	. . . . . . . . 9 ⊢ ((2𝑜 +𝑜 𝑥) = 𝑁 → [⟨((∅ +𝑜 2𝑜) +𝑜 𝑥), 1𝑜⟩] ~Q = [⟨𝑁, 1𝑜⟩] ~Q )
30	29	oveq1d 5547	. . . . . . . 8 ⊢ ((2𝑜 +𝑜 𝑥) = 𝑁 → ([⟨((∅ +𝑜 2𝑜) +𝑜 𝑥), 1𝑜⟩] ~Q ·Q 𝑃) = ([⟨𝑁, 1𝑜⟩] ~Q ·Q 𝑃))
31	30	oveq2d 5548	. . . . . . 7 ⊢ ((2𝑜 +𝑜 𝑥) = 𝑁 → (𝐴 +Q ([⟨((∅ +𝑜 2𝑜) +𝑜 𝑥), 1𝑜⟩] ~Q ·Q 𝑃)) = (𝐴 +Q ([⟨𝑁, 1𝑜⟩] ~Q ·Q 𝑃)))
32	31	eleq1d 2147	. . . . . 6 ⊢ ((2𝑜 +𝑜 𝑥) = 𝑁 → ((𝐴 +Q ([⟨((∅ +𝑜 2𝑜) +𝑜 𝑥), 1𝑜⟩] ~Q ·Q 𝑃)) ∈ 𝑈 ↔ (𝐴 +Q ([⟨𝑁, 1𝑜⟩] ~Q ·Q 𝑃)) ∈ 𝑈))
33	32	biimprcd 158	. . . . 5 ⊢ ((𝐴 +Q ([⟨𝑁, 1𝑜⟩] ~Q ·Q 𝑃)) ∈ 𝑈 → ((2𝑜 +𝑜 𝑥) = 𝑁 → (𝐴 +Q ([⟨((∅ +𝑜 2𝑜) +𝑜 𝑥), 1𝑜⟩] ~Q ·Q 𝑃)) ∈ 𝑈))
34	33	3ad2ant3 961	. . . 4 ⊢ (((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ 𝐿) ∧ (𝑁 ∈ N ∧ 𝑃 ∈ Q ∧ 1𝑜 <N 𝑁) ∧ (𝐴 +Q ([⟨𝑁, 1𝑜⟩] ~Q ·Q 𝑃)) ∈ 𝑈) → ((2𝑜 +𝑜 𝑥) = 𝑁 → (𝐴 +Q ([⟨((∅ +𝑜 2𝑜) +𝑜 𝑥), 1𝑜⟩] ~Q ·Q 𝑃)) ∈ 𝑈))
35		peano1 4335	. . . . 5 ⊢ ∅ ∈ ω
36		opeq1 3570	. . . . . . . . . . 11 ⊢ (𝑦 = ∅ → ⟨𝑦, 1𝑜⟩ = ⟨∅, 1𝑜⟩)
37	36	eceq1d 6165	. . . . . . . . . 10 ⊢ (𝑦 = ∅ → [⟨𝑦, 1𝑜⟩] ~Q0 = [⟨∅, 1𝑜⟩] ~Q0 )
38	37	oveq1d 5547	. . . . . . . . 9 ⊢ (𝑦 = ∅ → ([⟨𝑦, 1𝑜⟩] ~Q0 ·Q0 𝑃) = ([⟨∅, 1𝑜⟩] ~Q0 ·Q0 𝑃))
39	38	oveq2d 5548	. . . . . . . 8 ⊢ (𝑦 = ∅ → (𝐴 +Q0 ([⟨𝑦, 1𝑜⟩] ~Q0 ·Q0 𝑃)) = (𝐴 +Q0 ([⟨∅, 1𝑜⟩] ~Q0 ·Q0 𝑃)))
40	39	eleq1d 2147	. . . . . . 7 ⊢ (𝑦 = ∅ → ((𝐴 +Q0 ([⟨𝑦, 1𝑜⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ↔ (𝐴 +Q0 ([⟨∅, 1𝑜⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿))
41		oveq1 5539	. . . . . . . . . . . . 13 ⊢ (𝑦 = ∅ → (𝑦 +𝑜 2𝑜) = (∅ +𝑜 2𝑜))
42	41	oveq1d 5547	. . . . . . . . . . . 12 ⊢ (𝑦 = ∅ → ((𝑦 +𝑜 2𝑜) +𝑜 𝑥) = ((∅ +𝑜 2𝑜) +𝑜 𝑥))
43	42	opeq1d 3576	. . . . . . . . . . 11 ⊢ (𝑦 = ∅ → ⟨((𝑦 +𝑜 2𝑜) +𝑜 𝑥), 1𝑜⟩ = ⟨((∅ +𝑜 2𝑜) +𝑜 𝑥), 1𝑜⟩)
44	43	eceq1d 6165	. . . . . . . . . 10 ⊢ (𝑦 = ∅ → [⟨((𝑦 +𝑜 2𝑜) +𝑜 𝑥), 1𝑜⟩] ~Q = [⟨((∅ +𝑜 2𝑜) +𝑜 𝑥), 1𝑜⟩] ~Q )
45	44	oveq1d 5547	. . . . . . . . 9 ⊢ (𝑦 = ∅ → ([⟨((𝑦 +𝑜 2𝑜) +𝑜 𝑥), 1𝑜⟩] ~Q ·Q 𝑃) = ([⟨((∅ +𝑜 2𝑜) +𝑜 𝑥), 1𝑜⟩] ~Q ·Q 𝑃))
46	45	oveq2d 5548	. . . . . . . 8 ⊢ (𝑦 = ∅ → (𝐴 +Q ([⟨((𝑦 +𝑜 2𝑜) +𝑜 𝑥), 1𝑜⟩] ~Q ·Q 𝑃)) = (𝐴 +Q ([⟨((∅ +𝑜 2𝑜) +𝑜 𝑥), 1𝑜⟩] ~Q ·Q 𝑃)))
47	46	eleq1d 2147	. . . . . . 7 ⊢ (𝑦 = ∅ → ((𝐴 +Q ([⟨((𝑦 +𝑜 2𝑜) +𝑜 𝑥), 1𝑜⟩] ~Q ·Q 𝑃)) ∈ 𝑈 ↔ (𝐴 +Q ([⟨((∅ +𝑜 2𝑜) +𝑜 𝑥), 1𝑜⟩] ~Q ·Q 𝑃)) ∈ 𝑈))
48	40, 47	anbi12d 456	. . . . . 6 ⊢ (𝑦 = ∅ → (((𝐴 +Q0 ([⟨𝑦, 1𝑜⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨((𝑦 +𝑜 2𝑜) +𝑜 𝑥), 1𝑜⟩] ~Q ·Q 𝑃)) ∈ 𝑈) ↔ ((𝐴 +Q0 ([⟨∅, 1𝑜⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨((∅ +𝑜 2𝑜) +𝑜 𝑥), 1𝑜⟩] ~Q ·Q 𝑃)) ∈ 𝑈)))
49	48	rspcev 2701	. . . . 5 ⊢ ((∅ ∈ ω ∧ ((𝐴 +Q0 ([⟨∅, 1𝑜⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨((∅ +𝑜 2𝑜) +𝑜 𝑥), 1𝑜⟩] ~Q ·Q 𝑃)) ∈ 𝑈)) → ∃𝑦 ∈ ω ((𝐴 +Q0 ([⟨𝑦, 1𝑜⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨((𝑦 +𝑜 2𝑜) +𝑜 𝑥), 1𝑜⟩] ~Q ·Q 𝑃)) ∈ 𝑈))
50	35, 49	mpan 414	. . . 4 ⊢ (((𝐴 +Q0 ([⟨∅, 1𝑜⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨((∅ +𝑜 2𝑜) +𝑜 𝑥), 1𝑜⟩] ~Q ·Q 𝑃)) ∈ 𝑈) → ∃𝑦 ∈ ω ((𝐴 +Q0 ([⟨𝑦, 1𝑜⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨((𝑦 +𝑜 2𝑜) +𝑜 𝑥), 1𝑜⟩] ~Q ·Q 𝑃)) ∈ 𝑈))
51	21, 34, 50	syl6an 1363	. . 3 ⊢ (((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ 𝐿) ∧ (𝑁 ∈ N ∧ 𝑃 ∈ Q ∧ 1𝑜 <N 𝑁) ∧ (𝐴 +Q ([⟨𝑁, 1𝑜⟩] ~Q ·Q 𝑃)) ∈ 𝑈) → ((2𝑜 +𝑜 𝑥) = 𝑁 → ∃𝑦 ∈ ω ((𝐴 +Q0 ([⟨𝑦, 1𝑜⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨((𝑦 +𝑜 2𝑜) +𝑜 𝑥), 1𝑜⟩] ~Q ·Q 𝑃)) ∈ 𝑈)))
52	51	reximdv 2462	. 2 ⊢ (((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ 𝐿) ∧ (𝑁 ∈ N ∧ 𝑃 ∈ Q ∧ 1𝑜 <N 𝑁) ∧ (𝐴 +Q ([⟨𝑁, 1𝑜⟩] ~Q ·Q 𝑃)) ∈ 𝑈) → (∃𝑥 ∈ ω (2𝑜 +𝑜 𝑥) = 𝑁 → ∃𝑥 ∈ ω ∃𝑦 ∈ ω ((𝐴 +Q0 ([⟨𝑦, 1𝑜⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨((𝑦 +𝑜 2𝑜) +𝑜 𝑥), 1𝑜⟩] ~Q ·Q 𝑃)) ∈ 𝑈)))
53	3, 52	mpd 13	1 ⊢ (((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ 𝐿) ∧ (𝑁 ∈ N ∧ 𝑃 ∈ Q ∧ 1𝑜 <N 𝑁) ∧ (𝐴 +Q ([⟨𝑁, 1𝑜⟩] ~Q ·Q 𝑃)) ∈ 𝑈) → ∃𝑥 ∈ ω ∃𝑦 ∈ ω ((𝐴 +Q0 ([⟨𝑦, 1𝑜⟩] ~Q0 ·Q0 𝑃)) ∈ 𝐿 ∧ (𝐴 +Q ([⟨((𝑦 +𝑜 2𝑜) +𝑜 𝑥), 1𝑜⟩] ~Q ·Q 𝑃)) ∈ 𝑈))

Syntax hints:   → wi 4   ∧ wa 102   ∧ w3a 919   = wceq 1284   ∈ wcel 1433  ∃wrex 2349  ∅c0 3251  ⟨cop 3401   class class class wbr 3785  ωcom 4331  (class class class)co 5532  1_𝑜c1o 6017  2_𝑜c2o 6018   +_𝑜 coa 6021  [cec 6127  Ncnpi 6462   <_N clti 6465   ~_Q ceq 6469  Qcnq 6470   +_Q cplq 6472   ·_Q cmq 6473   ~_Q0 ceq0 6476  Q₀cnq0 6477  0_Q0c0q0 6478   +_Q0 cplq0 6479   ·_Q0 cmq0 6480  Pcnp 6481

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 576  ax-in2 577  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-13 1444  ax-14 1445  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063  ax-coll 3893  ax-sep 3896  ax-nul 3904  ax-pow 3948  ax-pr 3964  ax-un 4188  ax-setind 4280  ax-iinf 4329

This theorem depends on definitions:  df-bi 115  df-dc 776  df-3or 920  df-3an 921  df-tru 1287  df-fal 1290  df-nf 1390  df-sb 1686  df-eu 1944  df-mo 1945  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-ne 2246  df-ral 2353  df-rex 2354  df-reu 2355  df-rab 2357  df-v 2603  df-sbc 2816  df-csb 2909  df-dif 2975  df-un 2977  df-in 2979  df-ss 2986  df-nul 3252  df-pw 3384  df-sn 3404  df-pr 3405  df-op 3407  df-uni 3602  df-int 3637  df-iun 3680  df-br 3786  df-opab 3840  df-mpt 3841  df-tr 3876  df-eprel 4044  df-id 4048  df-iord 4121  df-on 4123  df-suc 4126  df-iom 4332  df-xp 4369  df-rel 4370  df-cnv 4371  df-co 4372  df-dm 4373  df-rn 4374  df-res 4375  df-ima 4376  df-iota 4887  df-fun 4924  df-fn 4925  df-f 4926  df-f1 4927  df-fo 4928  df-f1o 4929  df-fv 4930  df-ov 5535  df-oprab 5536  df-mpt2 5537  df-1st 5787  df-2nd 5788  df-recs 5943  df-irdg 5980  df-1o 6024  df-2o 6025  df-oadd 6028  df-omul 6029  df-er 6129  df-ec 6131  df-qs 6135  df-ni 6494  df-mi 6496  df-lti 6497  df-enq 6537  df-nqqs 6538  df-enq0 6614  df-nq0 6615  df-0nq0 6616  df-plq0 6617  df-mq0 6618  df-inp 6656

This theorem is referenced by:  prarloclem  6691