precsexlem8 - Metamath Proof Explorer

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

Theorem precsexlem8 28418

Description: Lemma for surreal reciprocal. Show that the left and right functions give sets of surreals. (Contributed by Scott Fenton, 13-Mar-2025.)

**Hypotheses**
Ref	Expression
precsexlem.1	⊢ 𝐹 = rec((𝑝 ∈ V ↦ ⦋(1^st ‘𝑝) / 𝑙⦌⦋(2^nd ‘𝑝) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥_𝑅 ∈ ( R ‘𝐴)∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝑅 -_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅)} ∪ {𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝐿 -_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝐿 -_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿)} ∪ {𝑎 ∣ ∃𝑥_𝑅 ∈ ( R ‘𝐴)∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝑅 -_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅)}))⟩), ⟨{ 0_s }, ∅⟩)
precsexlem.2	⊢ 𝐿 = (1^st ∘ 𝐹)
precsexlem.3	⊢ 𝑅 = (2^nd ∘ 𝐹)
precsexlem.4	⊢ (𝜑 → 𝐴 ∈ No )
precsexlem.5	⊢ (𝜑 → 0_s <s 𝐴)
precsexlem.6	⊢ (𝜑 → ∀𝑥_𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0_s <s 𝑥_𝑂 → ∃𝑦 ∈ No (𝑥_𝑂 ·_s 𝑦) = 1_s ))

**Assertion**
Ref	Expression
precsexlem8	⊢ ((𝜑 ∧ 𝐼 ∈ ω) → ((𝐿‘𝐼) ⊆ No ∧ (𝑅‘𝐼) ⊆ No ))

Distinct variable groups: 𝐴,𝑎,𝑙,𝑝,𝑟,𝑥,𝑥_𝑂,𝑥_𝐿,𝑥_𝑅,𝑦,𝑦_𝐿,𝑦_𝑅 𝐹,𝑙,𝑝 𝐿,𝑎,𝑙,𝑥_𝐿,𝑥_𝑅,𝑦_𝐿,𝑦_𝑅 𝑅,𝑎,𝑙,𝑟,𝑥_𝐿,𝑥_𝑅,𝑦_𝐿,𝑦_𝑅 𝜑,𝑎,𝑥_𝐿,𝑥_𝑅,𝑦_𝐿,𝑦_𝑅 Allowed substitution hints: 𝜑(𝑥, 𝑦, 𝑟, 𝑝, 𝑙, 𝑥_𝑂) 𝑅(𝑥, 𝑦, 𝑝, 𝑥_𝑂) 𝐹(𝑥, 𝑦, 𝑟, 𝑎, 𝑥_𝑂, 𝑥_𝐿, 𝑥_𝑅, 𝑦_𝐿, 𝑦_𝑅) 𝐼(𝑥, 𝑦, 𝑟, 𝑝, 𝑎, 𝑙, 𝑥_𝑂, 𝑥_𝐿, 𝑥_𝑅, 𝑦_𝐿, 𝑦_𝑅) 𝐿(𝑥, 𝑦, 𝑟, 𝑝, 𝑥_𝑂)

Proof of Theorem precsexlem8 Dummy variables 𝑖 𝑗 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6881	. . . . . 6 ⊢ (𝑖 = ∅ → (𝐿‘𝑖) = (𝐿‘∅))
2	1	sseq1d 3967	. . . . 5 ⊢ (𝑖 = ∅ → ((𝐿‘𝑖) ⊆ No ↔ (𝐿‘∅) ⊆ No ))
3		fveq2 6881	. . . . . 6 ⊢ (𝑖 = ∅ → (𝑅‘𝑖) = (𝑅‘∅))
4	3	sseq1d 3967	. . . . 5 ⊢ (𝑖 = ∅ → ((𝑅‘𝑖) ⊆ No ↔ (𝑅‘∅) ⊆ No ))
5	2, 4	anbi12d 643	. . . 4 ⊢ (𝑖 = ∅ → (((𝐿‘𝑖) ⊆ No ∧ (𝑅‘𝑖) ⊆ No ) ↔ ((𝐿‘∅) ⊆ No ∧ (𝑅‘∅) ⊆ No )))
6	5	imbi2d 343	. . 3 ⊢ (𝑖 = ∅ → ((𝜑 → ((𝐿‘𝑖) ⊆ No ∧ (𝑅‘𝑖) ⊆ No )) ↔ (𝜑 → ((𝐿‘∅) ⊆ No ∧ (𝑅‘∅) ⊆ No ))))
7		fveq2 6881	. . . . . 6 ⊢ (𝑖 = 𝑗 → (𝐿‘𝑖) = (𝐿‘𝑗))
8	7	sseq1d 3967	. . . . 5 ⊢ (𝑖 = 𝑗 → ((𝐿‘𝑖) ⊆ No ↔ (𝐿‘𝑗) ⊆ No ))
9		fveq2 6881	. . . . . 6 ⊢ (𝑖 = 𝑗 → (𝑅‘𝑖) = (𝑅‘𝑗))
10	9	sseq1d 3967	. . . . 5 ⊢ (𝑖 = 𝑗 → ((𝑅‘𝑖) ⊆ No ↔ (𝑅‘𝑗) ⊆ No ))
11	8, 10	anbi12d 643	. . . 4 ⊢ (𝑖 = 𝑗 → (((𝐿‘𝑖) ⊆ No ∧ (𝑅‘𝑖) ⊆ No ) ↔ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )))
12	11	imbi2d 343	. . 3 ⊢ (𝑖 = 𝑗 → ((𝜑 → ((𝐿‘𝑖) ⊆ No ∧ (𝑅‘𝑖) ⊆ No )) ↔ (𝜑 → ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No ))))
13		fveq2 6881	. . . . . 6 ⊢ (𝑖 = suc 𝑗 → (𝐿‘𝑖) = (𝐿‘suc 𝑗))
14	13	sseq1d 3967	. . . . 5 ⊢ (𝑖 = suc 𝑗 → ((𝐿‘𝑖) ⊆ No ↔ (𝐿‘suc 𝑗) ⊆ No ))
15		fveq2 6881	. . . . . 6 ⊢ (𝑖 = suc 𝑗 → (𝑅‘𝑖) = (𝑅‘suc 𝑗))
16	15	sseq1d 3967	. . . . 5 ⊢ (𝑖 = suc 𝑗 → ((𝑅‘𝑖) ⊆ No ↔ (𝑅‘suc 𝑗) ⊆ No ))
17	14, 16	anbi12d 643	. . . 4 ⊢ (𝑖 = suc 𝑗 → (((𝐿‘𝑖) ⊆ No ∧ (𝑅‘𝑖) ⊆ No ) ↔ ((𝐿‘suc 𝑗) ⊆ No ∧ (𝑅‘suc 𝑗) ⊆ No )))
18	17	imbi2d 343	. . 3 ⊢ (𝑖 = suc 𝑗 → ((𝜑 → ((𝐿‘𝑖) ⊆ No ∧ (𝑅‘𝑖) ⊆ No )) ↔ (𝜑 → ((𝐿‘suc 𝑗) ⊆ No ∧ (𝑅‘suc 𝑗) ⊆ No ))))
19		fveq2 6881	. . . . . 6 ⊢ (𝑖 = 𝐼 → (𝐿‘𝑖) = (𝐿‘𝐼))
20	19	sseq1d 3967	. . . . 5 ⊢ (𝑖 = 𝐼 → ((𝐿‘𝑖) ⊆ No ↔ (𝐿‘𝐼) ⊆ No ))
21		fveq2 6881	. . . . . 6 ⊢ (𝑖 = 𝐼 → (𝑅‘𝑖) = (𝑅‘𝐼))
22	21	sseq1d 3967	. . . . 5 ⊢ (𝑖 = 𝐼 → ((𝑅‘𝑖) ⊆ No ↔ (𝑅‘𝐼) ⊆ No ))
23	20, 22	anbi12d 643	. . . 4 ⊢ (𝑖 = 𝐼 → (((𝐿‘𝑖) ⊆ No ∧ (𝑅‘𝑖) ⊆ No ) ↔ ((𝐿‘𝐼) ⊆ No ∧ (𝑅‘𝐼) ⊆ No )))
24	23	imbi2d 343	. . 3 ⊢ (𝑖 = 𝐼 → ((𝜑 → ((𝐿‘𝑖) ⊆ No ∧ (𝑅‘𝑖) ⊆ No )) ↔ (𝜑 → ((𝐿‘𝐼) ⊆ No ∧ (𝑅‘𝐼) ⊆ No ))))
25		precsexlem.1	. . . . . . 7 ⊢ 𝐹 = rec((𝑝 ∈ V ↦ ⦋(1^st ‘𝑝) / 𝑙⦌⦋(2^nd ‘𝑝) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥_𝑅 ∈ ( R ‘𝐴)∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝑅 -_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅)} ∪ {𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝐿 -_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝐿 ∈ 𝑙 𝑎 = (( 1_s +_s ((𝑥_𝐿 -_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿)} ∪ {𝑎 ∣ ∃𝑥_𝑅 ∈ ( R ‘𝐴)∃𝑦_𝑅 ∈ 𝑟 𝑎 = (( 1_s +_s ((𝑥_𝑅 -_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅)}))⟩), ⟨{ 0_s }, ∅⟩)
26		precsexlem.2	. . . . . . 7 ⊢ 𝐿 = (1^st ∘ 𝐹)
27		precsexlem.3	. . . . . . 7 ⊢ 𝑅 = (2^nd ∘ 𝐹)
28	25, 26, 27	precsexlem1 28411	. . . . . 6 ⊢ (𝐿‘∅) = { 0_s }
29		0no 28013	. . . . . . 7 ⊢ 0_s ∈ No
30		snssi 4750	. . . . . . 7 ⊢ ( 0_s ∈ No → { 0_s } ⊆ No )
31	29, 30	ax-mp 5	. . . . . 6 ⊢ { 0_s } ⊆ No
32	28, 31	eqsstri 3982	. . . . 5 ⊢ (𝐿‘∅) ⊆ No
33	25, 26, 27	precsexlem2 28412	. . . . . 6 ⊢ (𝑅‘∅) = ∅
34		0ss 4356	. . . . . 6 ⊢ ∅ ⊆ No
35	33, 34	eqsstri 3982	. . . . 5 ⊢ (𝑅‘∅) ⊆ No
36	32, 35	pm3.2i 475	. . . 4 ⊢ ((𝐿‘∅) ⊆ No ∧ (𝑅‘∅) ⊆ No )
37	36	a1i 11	. . 3 ⊢ (𝜑 → ((𝐿‘∅) ⊆ No ∧ (𝑅‘∅) ⊆ No ))
38	25, 26, 27	precsexlem4 28414	. . . . . . . . 9 ⊢ (𝑗 ∈ ω → (𝐿‘suc 𝑗) = ((𝐿‘𝑗) ∪ ({𝑎 ∣ ∃𝑥_𝑅 ∈ ( R ‘𝐴)∃𝑦_𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1_s +_s ((𝑥_𝑅 -_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅)} ∪ {𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1_s +_s ((𝑥_𝐿 -_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿)})))
39	38	3ad2ant2 1151	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → (𝐿‘suc 𝑗) = ((𝐿‘𝑗) ∪ ({𝑎 ∣ ∃𝑥_𝑅 ∈ ( R ‘𝐴)∃𝑦_𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1_s +_s ((𝑥_𝑅 -_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅)} ∪ {𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1_s +_s ((𝑥_𝐿 -_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿)})))
40		simp3l 1219	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → (𝐿‘𝑗) ⊆ No )
41		1no 28014	. . . . . . . . . . . . . . . 16 ⊢ 1_s ∈ No
42	41	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝑅 ∈ ( R ‘𝐴) ∧ 𝑦_𝐿 ∈ (𝐿‘𝑗))) → 1_s ∈ No )
43		simprl 782	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝑅 ∈ ( R ‘𝐴) ∧ 𝑦_𝐿 ∈ (𝐿‘𝑗))) → 𝑥_𝑅 ∈ ( R ‘𝐴))
44	43	rightnod 28086	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝑅 ∈ ( R ‘𝐴) ∧ 𝑦_𝐿 ∈ (𝐿‘𝑗))) → 𝑥_𝑅 ∈ No )
45		precsexlem.4	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 ∈ No )
46	45	3ad2ant1 1150	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → 𝐴 ∈ No )
47	46	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝑅 ∈ ( R ‘𝐴) ∧ 𝑦_𝐿 ∈ (𝐿‘𝑗))) → 𝐴 ∈ No )
48	44, 47	subscld 28267	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝑅 ∈ ( R ‘𝐴) ∧ 𝑦_𝐿 ∈ (𝐿‘𝑗))) → (𝑥_𝑅 -_s 𝐴) ∈ No )
49		simpl3l 1246	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝑅 ∈ ( R ‘𝐴) ∧ 𝑦_𝐿 ∈ (𝐿‘𝑗))) → (𝐿‘𝑗) ⊆ No )
50		simprr 784	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝑅 ∈ ( R ‘𝐴) ∧ 𝑦_𝐿 ∈ (𝐿‘𝑗))) → 𝑦_𝐿 ∈ (𝐿‘𝑗))
51	49, 50	sseldd 3937	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝑅 ∈ ( R ‘𝐴) ∧ 𝑦_𝐿 ∈ (𝐿‘𝑗))) → 𝑦_𝐿 ∈ No )
52	48, 51	mulscld 28339	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝑅 ∈ ( R ‘𝐴) ∧ 𝑦_𝐿 ∈ (𝐿‘𝑗))) → ((𝑥_𝑅 -_s 𝐴) ·_s 𝑦_𝐿) ∈ No )
53	42, 52	addscld 28184	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝑅 ∈ ( R ‘𝐴) ∧ 𝑦_𝐿 ∈ (𝐿‘𝑗))) → ( 1_s +_s ((𝑥_𝑅 -_s 𝐴) ·_s 𝑦_𝐿)) ∈ No )
54	29	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝑅 ∈ ( R ‘𝐴) ∧ 𝑦_𝐿 ∈ (𝐿‘𝑗))) → 0_s ∈ No )
55		precsexlem.5	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 0_s <s 𝐴)
56	55	3ad2ant1 1150	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → 0_s <s 𝐴)
57	56	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝑅 ∈ ( R ‘𝐴) ∧ 𝑦_𝐿 ∈ (𝐿‘𝑗))) → 0_s <s 𝐴)
58		rightgt 28058	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥_𝑅 ∈ ( R ‘𝐴) → 𝐴 <s 𝑥_𝑅)
59	43, 58	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝑅 ∈ ( R ‘𝐴) ∧ 𝑦_𝐿 ∈ (𝐿‘𝑗))) → 𝐴 <s 𝑥_𝑅)
60	54, 47, 44, 57, 59	ltstrd 27938	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝑅 ∈ ( R ‘𝐴) ∧ 𝑦_𝐿 ∈ (𝐿‘𝑗))) → 0_s <s 𝑥_𝑅)
61	60	gt0ne0sd 28023	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝑅 ∈ ( R ‘𝐴) ∧ 𝑦_𝐿 ∈ (𝐿‘𝑗))) → 𝑥_𝑅 ≠ 0_s )
62		breq2 5112	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥_𝑂 = 𝑥_𝑅 → ( 0_s <s 𝑥_𝑂 ↔ 0_s <s 𝑥_𝑅))
63		oveq1 7419	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥_𝑂 = 𝑥_𝑅 → (𝑥_𝑂 ·_s 𝑦) = (𝑥_𝑅 ·_s 𝑦))
64	63	eqeq1d 2764	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥_𝑂 = 𝑥_𝑅 → ((𝑥_𝑂 ·_s 𝑦) = 1_s ↔ (𝑥_𝑅 ·_s 𝑦) = 1_s ))
65	64	rexbidv 3188	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥_𝑂 = 𝑥_𝑅 → (∃𝑦 ∈ No (𝑥_𝑂 ·_s 𝑦) = 1_s ↔ ∃𝑦 ∈ No (𝑥_𝑅 ·_s 𝑦) = 1_s ))
66	62, 65	imbi12d 347	. . . . . . . . . . . . . . . 16 ⊢ (𝑥_𝑂 = 𝑥_𝑅 → (( 0_s <s 𝑥_𝑂 → ∃𝑦 ∈ No (𝑥_𝑂 ·_s 𝑦) = 1_s ) ↔ ( 0_s <s 𝑥_𝑅 → ∃𝑦 ∈ No (𝑥_𝑅 ·_s 𝑦) = 1_s )))
67		precsexlem.6	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∀𝑥_𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0_s <s 𝑥_𝑂 → ∃𝑦 ∈ No (𝑥_𝑂 ·_s 𝑦) = 1_s ))
68	67	3ad2ant1 1150	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → ∀𝑥_𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0_s <s 𝑥_𝑂 → ∃𝑦 ∈ No (𝑥_𝑂 ·_s 𝑦) = 1_s ))
69	68	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝑅 ∈ ( R ‘𝐴) ∧ 𝑦_𝐿 ∈ (𝐿‘𝑗))) → ∀𝑥_𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0_s <s 𝑥_𝑂 → ∃𝑦 ∈ No (𝑥_𝑂 ·_s 𝑦) = 1_s ))
70		elun2 4135	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥_𝑅 ∈ ( R ‘𝐴) → 𝑥_𝑅 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))
71	43, 70	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝑅 ∈ ( R ‘𝐴) ∧ 𝑦_𝐿 ∈ (𝐿‘𝑗))) → 𝑥_𝑅 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))
72	66, 69, 71	rspcdva 3581	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝑅 ∈ ( R ‘𝐴) ∧ 𝑦_𝐿 ∈ (𝐿‘𝑗))) → ( 0_s <s 𝑥_𝑅 → ∃𝑦 ∈ No (𝑥_𝑅 ·_s 𝑦) = 1_s ))
73	60, 72	mpd 16	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝑅 ∈ ( R ‘𝐴) ∧ 𝑦_𝐿 ∈ (𝐿‘𝑗))) → ∃𝑦 ∈ No (𝑥_𝑅 ·_s 𝑦) = 1_s )
74	53, 44, 61, 73	divsclwd 28400	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝑅 ∈ ( R ‘𝐴) ∧ 𝑦_𝐿 ∈ (𝐿‘𝑗))) → (( 1_s +_s ((𝑥_𝑅 -_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅) ∈ No )
75		eleq1 2850	. . . . . . . . . . . . 13 ⊢ (𝑎 = (( 1_s +_s ((𝑥_𝑅 -_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅) → (𝑎 ∈ No ↔ (( 1_s +_s ((𝑥_𝑅 -_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅) ∈ No ))
76	74, 75	syl5ibrcom 250	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝑅 ∈ ( R ‘𝐴) ∧ 𝑦_𝐿 ∈ (𝐿‘𝑗))) → (𝑎 = (( 1_s +_s ((𝑥_𝑅 -_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅) → 𝑎 ∈ No ))
77	76	rexlimdvva 3221	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → (∃𝑥_𝑅 ∈ ( R ‘𝐴)∃𝑦_𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1_s +_s ((𝑥_𝑅 -_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅) → 𝑎 ∈ No ))
78	77	abssdv 4020	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → {𝑎 ∣ ∃𝑥_𝑅 ∈ ( R ‘𝐴)∃𝑦_𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1_s +_s ((𝑥_𝑅 -_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅)} ⊆ No )
79	41	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥} ∧ 𝑦_𝑅 ∈ (𝑅‘𝑗))) → 1_s ∈ No )
80		ssrab2 4033	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥} ⊆ ( L ‘𝐴)
81		simprl 782	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥} ∧ 𝑦_𝑅 ∈ (𝑅‘𝑗))) → 𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥})
82	80, 81	sselid 3934	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥} ∧ 𝑦_𝑅 ∈ (𝑅‘𝑗))) → 𝑥_𝐿 ∈ ( L ‘𝐴))
83	82	leftnod 28084	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥} ∧ 𝑦_𝑅 ∈ (𝑅‘𝑗))) → 𝑥_𝐿 ∈ No )
84	46	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥} ∧ 𝑦_𝑅 ∈ (𝑅‘𝑗))) → 𝐴 ∈ No )
85	83, 84	subscld 28267	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥} ∧ 𝑦_𝑅 ∈ (𝑅‘𝑗))) → (𝑥_𝐿 -_s 𝐴) ∈ No )
86		simpl3r 1247	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥} ∧ 𝑦_𝑅 ∈ (𝑅‘𝑗))) → (𝑅‘𝑗) ⊆ No )
87		simprr 784	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥} ∧ 𝑦_𝑅 ∈ (𝑅‘𝑗))) → 𝑦_𝑅 ∈ (𝑅‘𝑗))
88	86, 87	sseldd 3937	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥} ∧ 𝑦_𝑅 ∈ (𝑅‘𝑗))) → 𝑦_𝑅 ∈ No )
89	85, 88	mulscld 28339	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥} ∧ 𝑦_𝑅 ∈ (𝑅‘𝑗))) → ((𝑥_𝐿 -_s 𝐴) ·_s 𝑦_𝑅) ∈ No )
90	79, 89	addscld 28184	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥} ∧ 𝑦_𝑅 ∈ (𝑅‘𝑗))) → ( 1_s +_s ((𝑥_𝐿 -_s 𝐴) ·_s 𝑦_𝑅)) ∈ No )
91		breq2 5112	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑥_𝐿 → ( 0_s <s 𝑥 ↔ 0_s <s 𝑥_𝐿))
92	91	elrab 3649	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥} ↔ (𝑥_𝐿 ∈ ( L ‘𝐴) ∧ 0_s <s 𝑥_𝐿))
93	92	simprbi 502	. . . . . . . . . . . . . . . 16 ⊢ (𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥} → 0_s <s 𝑥_𝐿)
94	81, 93	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥} ∧ 𝑦_𝑅 ∈ (𝑅‘𝑗))) → 0_s <s 𝑥_𝐿)
95	94	gt0ne0sd 28023	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥} ∧ 𝑦_𝑅 ∈ (𝑅‘𝑗))) → 𝑥_𝐿 ≠ 0_s )
96		breq2 5112	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥_𝑂 = 𝑥_𝐿 → ( 0_s <s 𝑥_𝑂 ↔ 0_s <s 𝑥_𝐿))
97		oveq1 7419	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥_𝑂 = 𝑥_𝐿 → (𝑥_𝑂 ·_s 𝑦) = (𝑥_𝐿 ·_s 𝑦))
98	97	eqeq1d 2764	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥_𝑂 = 𝑥_𝐿 → ((𝑥_𝑂 ·_s 𝑦) = 1_s ↔ (𝑥_𝐿 ·_s 𝑦) = 1_s ))
99	98	rexbidv 3188	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥_𝑂 = 𝑥_𝐿 → (∃𝑦 ∈ No (𝑥_𝑂 ·_s 𝑦) = 1_s ↔ ∃𝑦 ∈ No (𝑥_𝐿 ·_s 𝑦) = 1_s ))
100	96, 99	imbi12d 347	. . . . . . . . . . . . . . . 16 ⊢ (𝑥_𝑂 = 𝑥_𝐿 → (( 0_s <s 𝑥_𝑂 → ∃𝑦 ∈ No (𝑥_𝑂 ·_s 𝑦) = 1_s ) ↔ ( 0_s <s 𝑥_𝐿 → ∃𝑦 ∈ No (𝑥_𝐿 ·_s 𝑦) = 1_s )))
101	68	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥} ∧ 𝑦_𝑅 ∈ (𝑅‘𝑗))) → ∀𝑥_𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0_s <s 𝑥_𝑂 → ∃𝑦 ∈ No (𝑥_𝑂 ·_s 𝑦) = 1_s ))
102		elun1 4134	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥_𝐿 ∈ ( L ‘𝐴) → 𝑥_𝐿 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))
103	82, 102	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥} ∧ 𝑦_𝑅 ∈ (𝑅‘𝑗))) → 𝑥_𝐿 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))
104	100, 101, 103	rspcdva 3581	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥} ∧ 𝑦_𝑅 ∈ (𝑅‘𝑗))) → ( 0_s <s 𝑥_𝐿 → ∃𝑦 ∈ No (𝑥_𝐿 ·_s 𝑦) = 1_s ))
105	94, 104	mpd 16	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥} ∧ 𝑦_𝑅 ∈ (𝑅‘𝑗))) → ∃𝑦 ∈ No (𝑥_𝐿 ·_s 𝑦) = 1_s )
106	90, 83, 95, 105	divsclwd 28400	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥} ∧ 𝑦_𝑅 ∈ (𝑅‘𝑗))) → (( 1_s +_s ((𝑥_𝐿 -_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿) ∈ No )
107		eleq1 2850	. . . . . . . . . . . . 13 ⊢ (𝑎 = (( 1_s +_s ((𝑥_𝐿 -_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿) → (𝑎 ∈ No ↔ (( 1_s +_s ((𝑥_𝐿 -_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿) ∈ No ))
108	106, 107	syl5ibrcom 250	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥} ∧ 𝑦_𝑅 ∈ (𝑅‘𝑗))) → (𝑎 = (( 1_s +_s ((𝑥_𝐿 -_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿) → 𝑎 ∈ No ))
109	108	rexlimdvva 3221	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → (∃𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1_s +_s ((𝑥_𝐿 -_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿) → 𝑎 ∈ No ))
110	109	abssdv 4020	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → {𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1_s +_s ((𝑥_𝐿 -_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿)} ⊆ No )
111	78, 110	unssd 4144	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → ({𝑎 ∣ ∃𝑥_𝑅 ∈ ( R ‘𝐴)∃𝑦_𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1_s +_s ((𝑥_𝑅 -_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅)} ∪ {𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1_s +_s ((𝑥_𝐿 -_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿)}) ⊆ No )
112	40, 111	unssd 4144	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → ((𝐿‘𝑗) ∪ ({𝑎 ∣ ∃𝑥_𝑅 ∈ ( R ‘𝐴)∃𝑦_𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1_s +_s ((𝑥_𝑅 -_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝑅)} ∪ {𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1_s +_s ((𝑥_𝐿 -_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝐿)})) ⊆ No )
113	39, 112	eqsstrd 3970	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → (𝐿‘suc 𝑗) ⊆ No )
114	25, 26, 27	precsexlem5 28415	. . . . . . . . 9 ⊢ (𝑗 ∈ ω → (𝑅‘suc 𝑗) = ((𝑅‘𝑗) ∪ ({𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1_s +_s ((𝑥_𝐿 -_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿)} ∪ {𝑎 ∣ ∃𝑥_𝑅 ∈ ( R ‘𝐴)∃𝑦_𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1_s +_s ((𝑥_𝑅 -_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅)})))
115	114	3ad2ant2 1151	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → (𝑅‘suc 𝑗) = ((𝑅‘𝑗) ∪ ({𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1_s +_s ((𝑥_𝐿 -_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿)} ∪ {𝑎 ∣ ∃𝑥_𝑅 ∈ ( R ‘𝐴)∃𝑦_𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1_s +_s ((𝑥_𝑅 -_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅)})))
116		simp3r 1220	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → (𝑅‘𝑗) ⊆ No )
117	41	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥} ∧ 𝑦_𝐿 ∈ (𝐿‘𝑗))) → 1_s ∈ No )
118		simprl 782	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥} ∧ 𝑦_𝐿 ∈ (𝐿‘𝑗))) → 𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥})
119	80, 118	sselid 3934	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥} ∧ 𝑦_𝐿 ∈ (𝐿‘𝑗))) → 𝑥_𝐿 ∈ ( L ‘𝐴))
120	119	leftnod 28084	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥} ∧ 𝑦_𝐿 ∈ (𝐿‘𝑗))) → 𝑥_𝐿 ∈ No )
121	46	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥} ∧ 𝑦_𝐿 ∈ (𝐿‘𝑗))) → 𝐴 ∈ No )
122	120, 121	subscld 28267	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥} ∧ 𝑦_𝐿 ∈ (𝐿‘𝑗))) → (𝑥_𝐿 -_s 𝐴) ∈ No )
123		simpl3l 1246	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥} ∧ 𝑦_𝐿 ∈ (𝐿‘𝑗))) → (𝐿‘𝑗) ⊆ No )
124		simprr 784	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥} ∧ 𝑦_𝐿 ∈ (𝐿‘𝑗))) → 𝑦_𝐿 ∈ (𝐿‘𝑗))
125	123, 124	sseldd 3937	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥} ∧ 𝑦_𝐿 ∈ (𝐿‘𝑗))) → 𝑦_𝐿 ∈ No )
126	122, 125	mulscld 28339	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥} ∧ 𝑦_𝐿 ∈ (𝐿‘𝑗))) → ((𝑥_𝐿 -_s 𝐴) ·_s 𝑦_𝐿) ∈ No )
127	117, 126	addscld 28184	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥} ∧ 𝑦_𝐿 ∈ (𝐿‘𝑗))) → ( 1_s +_s ((𝑥_𝐿 -_s 𝐴) ·_s 𝑦_𝐿)) ∈ No )
128	118, 93	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥} ∧ 𝑦_𝐿 ∈ (𝐿‘𝑗))) → 0_s <s 𝑥_𝐿)
129	128	gt0ne0sd 28023	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥} ∧ 𝑦_𝐿 ∈ (𝐿‘𝑗))) → 𝑥_𝐿 ≠ 0_s )
130	68	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥} ∧ 𝑦_𝐿 ∈ (𝐿‘𝑗))) → ∀𝑥_𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0_s <s 𝑥_𝑂 → ∃𝑦 ∈ No (𝑥_𝑂 ·_s 𝑦) = 1_s ))
131	119, 102	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥} ∧ 𝑦_𝐿 ∈ (𝐿‘𝑗))) → 𝑥_𝐿 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))
132	100, 130, 131	rspcdva 3581	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥} ∧ 𝑦_𝐿 ∈ (𝐿‘𝑗))) → ( 0_s <s 𝑥_𝐿 → ∃𝑦 ∈ No (𝑥_𝐿 ·_s 𝑦) = 1_s ))
133	128, 132	mpd 16	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥} ∧ 𝑦_𝐿 ∈ (𝐿‘𝑗))) → ∃𝑦 ∈ No (𝑥_𝐿 ·_s 𝑦) = 1_s )
134	127, 120, 129, 133	divsclwd 28400	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥} ∧ 𝑦_𝐿 ∈ (𝐿‘𝑗))) → (( 1_s +_s ((𝑥_𝐿 -_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿) ∈ No )
135		eleq1 2850	. . . . . . . . . . . . 13 ⊢ (𝑎 = (( 1_s +_s ((𝑥_𝐿 -_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿) → (𝑎 ∈ No ↔ (( 1_s +_s ((𝑥_𝐿 -_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿) ∈ No ))
136	134, 135	syl5ibrcom 250	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥} ∧ 𝑦_𝐿 ∈ (𝐿‘𝑗))) → (𝑎 = (( 1_s +_s ((𝑥_𝐿 -_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿) → 𝑎 ∈ No ))
137	136	rexlimdvva 3221	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → (∃𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1_s +_s ((𝑥_𝐿 -_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿) → 𝑎 ∈ No ))
138	137	abssdv 4020	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → {𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1_s +_s ((𝑥_𝐿 -_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿)} ⊆ No )
139	41	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝑅 ∈ ( R ‘𝐴) ∧ 𝑦_𝑅 ∈ (𝑅‘𝑗))) → 1_s ∈ No )
140		simprl 782	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝑅 ∈ ( R ‘𝐴) ∧ 𝑦_𝑅 ∈ (𝑅‘𝑗))) → 𝑥_𝑅 ∈ ( R ‘𝐴))
141	140	rightnod 28086	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝑅 ∈ ( R ‘𝐴) ∧ 𝑦_𝑅 ∈ (𝑅‘𝑗))) → 𝑥_𝑅 ∈ No )
142	46	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝑅 ∈ ( R ‘𝐴) ∧ 𝑦_𝑅 ∈ (𝑅‘𝑗))) → 𝐴 ∈ No )
143	141, 142	subscld 28267	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝑅 ∈ ( R ‘𝐴) ∧ 𝑦_𝑅 ∈ (𝑅‘𝑗))) → (𝑥_𝑅 -_s 𝐴) ∈ No )
144		simpl3r 1247	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝑅 ∈ ( R ‘𝐴) ∧ 𝑦_𝑅 ∈ (𝑅‘𝑗))) → (𝑅‘𝑗) ⊆ No )
145		simprr 784	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝑅 ∈ ( R ‘𝐴) ∧ 𝑦_𝑅 ∈ (𝑅‘𝑗))) → 𝑦_𝑅 ∈ (𝑅‘𝑗))
146	144, 145	sseldd 3937	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝑅 ∈ ( R ‘𝐴) ∧ 𝑦_𝑅 ∈ (𝑅‘𝑗))) → 𝑦_𝑅 ∈ No )
147	143, 146	mulscld 28339	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝑅 ∈ ( R ‘𝐴) ∧ 𝑦_𝑅 ∈ (𝑅‘𝑗))) → ((𝑥_𝑅 -_s 𝐴) ·_s 𝑦_𝑅) ∈ No )
148	139, 147	addscld 28184	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝑅 ∈ ( R ‘𝐴) ∧ 𝑦_𝑅 ∈ (𝑅‘𝑗))) → ( 1_s +_s ((𝑥_𝑅 -_s 𝐴) ·_s 𝑦_𝑅)) ∈ No )
149	29	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝑅 ∈ ( R ‘𝐴) ∧ 𝑦_𝑅 ∈ (𝑅‘𝑗))) → 0_s ∈ No )
150	56	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝑅 ∈ ( R ‘𝐴) ∧ 𝑦_𝑅 ∈ (𝑅‘𝑗))) → 0_s <s 𝐴)
151	140, 58	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝑅 ∈ ( R ‘𝐴) ∧ 𝑦_𝑅 ∈ (𝑅‘𝑗))) → 𝐴 <s 𝑥_𝑅)
152	149, 142, 141, 150, 151	ltstrd 27938	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝑅 ∈ ( R ‘𝐴) ∧ 𝑦_𝑅 ∈ (𝑅‘𝑗))) → 0_s <s 𝑥_𝑅)
153	152	gt0ne0sd 28023	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝑅 ∈ ( R ‘𝐴) ∧ 𝑦_𝑅 ∈ (𝑅‘𝑗))) → 𝑥_𝑅 ≠ 0_s )
154	68	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝑅 ∈ ( R ‘𝐴) ∧ 𝑦_𝑅 ∈ (𝑅‘𝑗))) → ∀𝑥_𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0_s <s 𝑥_𝑂 → ∃𝑦 ∈ No (𝑥_𝑂 ·_s 𝑦) = 1_s ))
155	140, 70	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝑅 ∈ ( R ‘𝐴) ∧ 𝑦_𝑅 ∈ (𝑅‘𝑗))) → 𝑥_𝑅 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))
156	66, 154, 155	rspcdva 3581	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝑅 ∈ ( R ‘𝐴) ∧ 𝑦_𝑅 ∈ (𝑅‘𝑗))) → ( 0_s <s 𝑥_𝑅 → ∃𝑦 ∈ No (𝑥_𝑅 ·_s 𝑦) = 1_s ))
157	152, 156	mpd 16	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝑅 ∈ ( R ‘𝐴) ∧ 𝑦_𝑅 ∈ (𝑅‘𝑗))) → ∃𝑦 ∈ No (𝑥_𝑅 ·_s 𝑦) = 1_s )
158	148, 141, 153, 157	divsclwd 28400	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝑅 ∈ ( R ‘𝐴) ∧ 𝑦_𝑅 ∈ (𝑅‘𝑗))) → (( 1_s +_s ((𝑥_𝑅 -_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅) ∈ No )
159		eleq1 2850	. . . . . . . . . . . . 13 ⊢ (𝑎 = (( 1_s +_s ((𝑥_𝑅 -_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅) → (𝑎 ∈ No ↔ (( 1_s +_s ((𝑥_𝑅 -_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅) ∈ No ))
160	158, 159	syl5ibrcom 250	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) ∧ (𝑥_𝑅 ∈ ( R ‘𝐴) ∧ 𝑦_𝑅 ∈ (𝑅‘𝑗))) → (𝑎 = (( 1_s +_s ((𝑥_𝑅 -_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅) → 𝑎 ∈ No ))
161	160	rexlimdvva 3221	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → (∃𝑥_𝑅 ∈ ( R ‘𝐴)∃𝑦_𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1_s +_s ((𝑥_𝑅 -_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅) → 𝑎 ∈ No ))
162	161	abssdv 4020	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → {𝑎 ∣ ∃𝑥_𝑅 ∈ ( R ‘𝐴)∃𝑦_𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1_s +_s ((𝑥_𝑅 -_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅)} ⊆ No )
163	138, 162	unssd 4144	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → ({𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1_s +_s ((𝑥_𝐿 -_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿)} ∪ {𝑎 ∣ ∃𝑥_𝑅 ∈ ( R ‘𝐴)∃𝑦_𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1_s +_s ((𝑥_𝑅 -_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅)}) ⊆ No )
164	116, 163	unssd 4144	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → ((𝑅‘𝑗) ∪ ({𝑎 ∣ ∃𝑥_𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0_s <s 𝑥}∃𝑦_𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1_s +_s ((𝑥_𝐿 -_s 𝐴) ·_s 𝑦_𝐿)) /_su 𝑥_𝐿)} ∪ {𝑎 ∣ ∃𝑥_𝑅 ∈ ( R ‘𝐴)∃𝑦_𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1_s +_s ((𝑥_𝑅 -_s 𝐴) ·_s 𝑦_𝑅)) /_su 𝑥_𝑅)})) ⊆ No )
165	115, 164	eqsstrd 3970	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → (𝑅‘suc 𝑗) ⊆ No )
166	113, 165	jca 520	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → ((𝐿‘suc 𝑗) ⊆ No ∧ (𝑅‘suc 𝑗) ⊆ No ))
167	166	3exp 1136	. . . . 5 ⊢ (𝜑 → (𝑗 ∈ ω → (((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No ) → ((𝐿‘suc 𝑗) ⊆ No ∧ (𝑅‘suc 𝑗) ⊆ No ))))
168	167	com12 33	. . . 4 ⊢ (𝑗 ∈ ω → (𝜑 → (((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No ) → ((𝐿‘suc 𝑗) ⊆ No ∧ (𝑅‘suc 𝑗) ⊆ No ))))
169	168	a2d 30	. . 3 ⊢ (𝑗 ∈ ω → ((𝜑 → ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No )) → (𝜑 → ((𝐿‘suc 𝑗) ⊆ No ∧ (𝑅‘suc 𝑗) ⊆ No ))))
170	6, 12, 18, 24, 37, 169	finds 7891	. 2 ⊢ (𝐼 ∈ ω → (𝜑 → ((𝐿‘𝐼) ⊆ No ∧ (𝑅‘𝐼) ⊆ No )))
171	170	impcom 412	1 ⊢ ((𝜑 ∧ 𝐼 ∈ ω) → ((𝐿‘𝐼) ⊆ No ∧ (𝑅‘𝐼) ⊆ No ))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 400 ∧ w3a 1102 = wceq 1569 ∈ wcel 2142 {cab 2740 ∀wral 3078 ∃wrex 3088 {crab 3415 Vcvv 3454 ⦋csb 3852 ∪ cun 3902 ⊆ wss 3904 ∅c0 4285 {csn 4588 ⟨cop 4594 class class class wbr 5108 ↦ cmpt 5191 ∘ ccom 5664 suc csuc 6362 ‘cfv 6536 (class class class)co 7412 ωcom 7860 1^st c1st 7982 2^nd c2nd 7983 reccrdg 8394 No csur 27815 <s clts 27816 0_s c0s 28009 1_s c1s 28010 L cleft 28029 R cright 28030 +_s cadds 28163 -_s csubs 28224 ·_s cmuls 28310 /_su cdivs 28391

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1824 ax-4 1838 ax-5 1939 ax-6 1996 ax-7 2037 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-rep 5237 ax-sep 5256 ax-nul 5268 ax-pow 5335 ax-pr 5403 ax-un 7734

This proof depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1103 df-3an 1104 df-tru 1572 df-fal 1582 df-ex 1809 df-nf 1813 df-sb 2096 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-ral 3079 df-rex 3089 df-rmo 3368 df-reu 3369 df-rab 3416 df-v 3456 df-sbc 3744 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4487 df-pw 4563 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4595 df-ot 4597 df-uni 4872 df-int 4912 df-iun 4957 df-br 5109 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5555 df-eprel 5560 df-po 5568 df-so 5569 df-fr 5613 df-se 5614 df-we 5615 df-xp 5666 df-rel 5667 df-cnv 5668 df-co 5669 df-dm 5670 df-rn 5671 df-res 5672 df-ima 5673 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7861 df-1st 7984 df-2nd 7985 df-frecs 8276 df-wrecs 8307 df-recs 8356 df-rdg 8395 df-1o 8451 df-2o 8452 df-nadd 8650 df-no 27818 df-lts 27819 df-bday 27820 df-les 27920 df-slts 27962 df-cuts 27964 df-0s 28011 df-1s 28012 df-made 28031 df-old 28032 df-left 28034 df-right 28035 df-norec 28142 df-norec2 28153 df-adds 28164 df-negs 28225 df-subs 28226 df-muls 28311 df-divs 28392

This theorem is used by: precsexlem9 28419 precsexlem10 28420

W3C validator