Theorem precsexlem9 28174

Description: Lemma for surreal reciprocal. Show that the product of 𝐴 and a left element is less than one and the product of 𝐴 and a right element is greater than one. (Contributed by Scott Fenton, 14-Mar-2025.)

Hypotheses

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

Assertion

Ref	Expression
precsexlem9	⊢ ((𝜑 ∧ 𝐼 ∈ ω) → (∀𝑏 ∈ (𝐿‘𝐼)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝐼) 1s <s (𝐴 ·s 𝑐)))

Distinct variable groups:   𝐴,𝑎,𝑙,𝑝,𝑟,𝑥,𝑥_𝑂,𝑥_𝐿,𝑥_𝑅,𝑦,𝑦_𝐿,𝑦_𝑅   𝐹,𝑙,𝑝   𝐿,𝑎,𝑙,𝑥_𝐿,𝑥_𝑅,𝑦_𝐿,𝑦_𝑅   𝑅,𝑎,𝑙,𝑟,𝑥_𝐿,𝑥_𝑅,𝑦_𝐿,𝑦_𝑅   𝜑,𝑎,𝑥_𝐿,𝑥_𝑅,𝑦_𝐿,𝑦_𝑅   𝐴,𝑏,𝑐,𝑎,𝑙,𝑝,𝑟,𝑥,𝑥_𝑂,𝑥_𝐿,𝑥_𝑅,𝑦_𝐿,𝑦_𝑅   𝜑,𝑟   𝐼,𝑏,𝑐   𝐿,𝑏,𝑟   𝑅,𝑐

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑝,𝑏,𝑐,𝑙,𝑥_𝑂)   𝑅(𝑥,𝑦,𝑝,𝑏,𝑥_𝑂)   𝐹(𝑥,𝑦,𝑟,𝑎,𝑏,𝑐,𝑥_𝑂,𝑥_𝐿,𝑥_𝑅,𝑦_𝐿,𝑦_𝑅)   𝐼(𝑥,𝑦,𝑟,𝑝,𝑎,𝑙,𝑥_𝑂,𝑥_𝐿,𝑥_𝑅,𝑦_𝐿,𝑦_𝑅)   𝐿(𝑥,𝑦,𝑝,𝑐,𝑥_𝑂)

Proof of Theorem precsexlem9

Dummy variables 𝑖 𝑗 𝑠 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6881	. . . . . 6 ⊢ (𝑖 = ∅ → (𝐿‘𝑖) = (𝐿‘∅))
2	1	raleqdv 3309	. . . . 5 ⊢ (𝑖 = ∅ → (∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ↔ ∀𝑏 ∈ (𝐿‘∅)(𝐴 ·s 𝑏) <s 1s ))
3		fveq2 6881	. . . . . 6 ⊢ (𝑖 = ∅ → (𝑅‘𝑖) = (𝑅‘∅))
4	3	raleqdv 3309	. . . . 5 ⊢ (𝑖 = ∅ → (∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐) ↔ ∀𝑐 ∈ (𝑅‘∅) 1s <s (𝐴 ·s 𝑐)))
5	2, 4	anbi12d 632	. . . 4 ⊢ (𝑖 = ∅ → ((∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐)) ↔ (∀𝑏 ∈ (𝐿‘∅)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘∅) 1s <s (𝐴 ·s 𝑐))))
6	5	imbi2d 340	. . 3 ⊢ (𝑖 = ∅ → ((𝜑 → (∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐))) ↔ (𝜑 → (∀𝑏 ∈ (𝐿‘∅)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘∅) 1s <s (𝐴 ·s 𝑐)))))
7		fveq2 6881	. . . . . 6 ⊢ (𝑖 = 𝑗 → (𝐿‘𝑖) = (𝐿‘𝑗))
8	7	raleqdv 3309	. . . . 5 ⊢ (𝑖 = 𝑗 → (∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ↔ ∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ))
9		fveq2 6881	. . . . . 6 ⊢ (𝑖 = 𝑗 → (𝑅‘𝑖) = (𝑅‘𝑗))
10	9	raleqdv 3309	. . . . 5 ⊢ (𝑖 = 𝑗 → (∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐) ↔ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐)))
11	8, 10	anbi12d 632	. . . 4 ⊢ (𝑖 = 𝑗 → ((∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐)) ↔ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))))
12	11	imbi2d 340	. . 3 ⊢ (𝑖 = 𝑗 → ((𝜑 → (∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐))) ↔ (𝜑 → (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐)))))
13		fveq2 6881	. . . . . . 7 ⊢ (𝑖 = suc 𝑗 → (𝐿‘𝑖) = (𝐿‘suc 𝑗))
14	13	raleqdv 3309	. . . . . 6 ⊢ (𝑖 = suc 𝑗 → (∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ↔ ∀𝑏 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑏) <s 1s ))
15		fveq2 6881	. . . . . . 7 ⊢ (𝑖 = suc 𝑗 → (𝑅‘𝑖) = (𝑅‘suc 𝑗))
16	15	raleqdv 3309	. . . . . 6 ⊢ (𝑖 = suc 𝑗 → (∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐) ↔ ∀𝑐 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑐)))
17	14, 16	anbi12d 632	. . . . 5 ⊢ (𝑖 = suc 𝑗 → ((∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐)) ↔ (∀𝑏 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑐))))
18		oveq2 7418	. . . . . . . 8 ⊢ (𝑏 = 𝑟 → (𝐴 ·s 𝑏) = (𝐴 ·s 𝑟))
19	18	breq1d 5134	. . . . . . 7 ⊢ (𝑏 = 𝑟 → ((𝐴 ·s 𝑏) <s 1s ↔ (𝐴 ·s 𝑟) <s 1s ))
20	19	cbvralvw 3224	. . . . . 6 ⊢ (∀𝑏 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑏) <s 1s ↔ ∀𝑟 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑟) <s 1s )
21		oveq2 7418	. . . . . . . 8 ⊢ (𝑐 = 𝑠 → (𝐴 ·s 𝑐) = (𝐴 ·s 𝑠))
22	21	breq2d 5136	. . . . . . 7 ⊢ (𝑐 = 𝑠 → ( 1s <s (𝐴 ·s 𝑐) ↔ 1s <s (𝐴 ·s 𝑠)))
23	22	cbvralvw 3224	. . . . . 6 ⊢ (∀𝑐 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑐) ↔ ∀𝑠 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑠))
24	20, 23	anbi12i 628	. . . . 5 ⊢ ((∀𝑏 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑐)) ↔ (∀𝑟 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑟) <s 1s ∧ ∀𝑠 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑠)))
25	17, 24	bitrdi 287	. . . 4 ⊢ (𝑖 = suc 𝑗 → ((∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐)) ↔ (∀𝑟 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑟) <s 1s ∧ ∀𝑠 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑠))))
26	25	imbi2d 340	. . 3 ⊢ (𝑖 = suc 𝑗 → ((𝜑 → (∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐))) ↔ (𝜑 → (∀𝑟 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑟) <s 1s ∧ ∀𝑠 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑠)))))
27		fveq2 6881	. . . . . 6 ⊢ (𝑖 = 𝐼 → (𝐿‘𝑖) = (𝐿‘𝐼))
28	27	raleqdv 3309	. . . . 5 ⊢ (𝑖 = 𝐼 → (∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ↔ ∀𝑏 ∈ (𝐿‘𝐼)(𝐴 ·s 𝑏) <s 1s ))
29		fveq2 6881	. . . . . 6 ⊢ (𝑖 = 𝐼 → (𝑅‘𝑖) = (𝑅‘𝐼))
30	29	raleqdv 3309	. . . . 5 ⊢ (𝑖 = 𝐼 → (∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐) ↔ ∀𝑐 ∈ (𝑅‘𝐼) 1s <s (𝐴 ·s 𝑐)))
31	28, 30	anbi12d 632	. . . 4 ⊢ (𝑖 = 𝐼 → ((∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐)) ↔ (∀𝑏 ∈ (𝐿‘𝐼)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝐼) 1s <s (𝐴 ·s 𝑐))))
32	31	imbi2d 340	. . 3 ⊢ (𝑖 = 𝐼 → ((𝜑 → (∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐))) ↔ (𝜑 → (∀𝑏 ∈ (𝐿‘𝐼)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝐼) 1s <s (𝐴 ·s 𝑐)))))
33		precsexlem.4	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ No )
34		muls01 28072	. . . . . . 7 ⊢ (𝐴 ∈ No → (𝐴 ·s 0s ) = 0s )
35	33, 34	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐴 ·s 0s ) = 0s )
36		0slt1s 27798	. . . . . 6 ⊢ 0s <s 1s
37	35, 36	eqbrtrdi 5163	. . . . 5 ⊢ (𝜑 → (𝐴 ·s 0s ) <s 1s )
38		precsexlem.1	. . . . . . . 8 ⊢ 𝐹 = rec((𝑝 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd ‘𝑝) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))⟩), ⟨{ 0s }, ∅⟩)
39		precsexlem.2	. . . . . . . 8 ⊢ 𝐿 = (1st ∘ 𝐹)
40		precsexlem.3	. . . . . . . 8 ⊢ 𝑅 = (2nd ∘ 𝐹)
41	38, 39, 40	precsexlem1 28166	. . . . . . 7 ⊢ (𝐿‘∅) = { 0s }
42	41	raleqi 3307	. . . . . 6 ⊢ (∀𝑏 ∈ (𝐿‘∅)(𝐴 ·s 𝑏) <s 1s ↔ ∀𝑏 ∈ { 0s } (𝐴 ·s 𝑏) <s 1s )
43		0sno 27795	. . . . . . . 8 ⊢ 0s ∈ No
44	43	elexi 3487	. . . . . . 7 ⊢ 0s ∈ V
45		oveq2 7418	. . . . . . . 8 ⊢ (𝑏 = 0s → (𝐴 ·s 𝑏) = (𝐴 ·s 0s ))
46	45	breq1d 5134	. . . . . . 7 ⊢ (𝑏 = 0s → ((𝐴 ·s 𝑏) <s 1s ↔ (𝐴 ·s 0s ) <s 1s ))
47	44, 46	ralsn 4662	. . . . . 6 ⊢ (∀𝑏 ∈ { 0s } (𝐴 ·s 𝑏) <s 1s ↔ (𝐴 ·s 0s ) <s 1s )
48	42, 47	bitri 275	. . . . 5 ⊢ (∀𝑏 ∈ (𝐿‘∅)(𝐴 ·s 𝑏) <s 1s ↔ (𝐴 ·s 0s ) <s 1s )
49	37, 48	sylibr 234	. . . 4 ⊢ (𝜑 → ∀𝑏 ∈ (𝐿‘∅)(𝐴 ·s 𝑏) <s 1s )
50		ral0 4493	. . . . 5 ⊢ ∀𝑐 ∈ ∅ 1s <s (𝐴 ·s 𝑐)
51	38, 39, 40	precsexlem2 28167	. . . . . 6 ⊢ (𝑅‘∅) = ∅
52	51	raleqi 3307	. . . . 5 ⊢ (∀𝑐 ∈ (𝑅‘∅) 1s <s (𝐴 ·s 𝑐) ↔ ∀𝑐 ∈ ∅ 1s <s (𝐴 ·s 𝑐))
53	50, 52	mpbir 231	. . . 4 ⊢ ∀𝑐 ∈ (𝑅‘∅) 1s <s (𝐴 ·s 𝑐)
54	49, 53	jctir 520	. . 3 ⊢ (𝜑 → (∀𝑏 ∈ (𝐿‘∅)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘∅) 1s <s (𝐴 ·s 𝑐)))
55	38, 39, 40	precsexlem4 28169	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ω → (𝐿‘suc 𝑗) = ((𝐿‘𝑗) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})))
56	55	3ad2ant2 1134	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝐿‘suc 𝑗) = ((𝐿‘𝑗) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})))
57	56	eleq2d 2821	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝑟 ∈ (𝐿‘suc 𝑗) ↔ 𝑟 ∈ ((𝐿‘𝑗) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)}))))
58		elun 4133	. . . . . . . . . . 11 ⊢ (𝑟 ∈ ((𝐿‘𝑗) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})) ↔ (𝑟 ∈ (𝐿‘𝑗) ∨ 𝑟 ∈ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})))
59		elun 4133	. . . . . . . . . . . . 13 ⊢ (𝑟 ∈ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)}) ↔ (𝑟 ∈ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∨ 𝑟 ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)}))
60		vex 3468	. . . . . . . . . . . . . . 15 ⊢ 𝑟 ∈ V
61		eqeq1 2740	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑟 → (𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) ↔ 𝑟 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)))
62	61	2rexbidv 3210	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑟 → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) ↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑟 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)))
63	60, 62	elab 3663	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑟 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅))
64		eqeq1 2740	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑟 → (𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) ↔ 𝑟 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)))
65	64	2rexbidv 3210	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑟 → (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) ↔ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑟 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)))
66	60, 65	elab 3663	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)} ↔ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑟 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿))
67	63, 66	orbi12i 914	. . . . . . . . . . . . 13 ⊢ ((𝑟 ∈ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∨ 𝑟 ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)}) ↔ (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑟 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) ∨ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑟 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)))
68	59, 67	bitri 275	. . . . . . . . . . . 12 ⊢ (𝑟 ∈ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)}) ↔ (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑟 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) ∨ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑟 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)))
69	68	orbi2i 912	. . . . . . . . . . 11 ⊢ ((𝑟 ∈ (𝐿‘𝑗) ∨ 𝑟 ∈ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})) ↔ (𝑟 ∈ (𝐿‘𝑗) ∨ (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑟 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) ∨ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑟 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿))))
70	58, 69	bitri 275	. . . . . . . . . 10 ⊢ (𝑟 ∈ ((𝐿‘𝑗) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})) ↔ (𝑟 ∈ (𝐿‘𝑗) ∨ (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑟 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) ∨ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑟 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿))))
71	57, 70	bitrdi 287	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝑟 ∈ (𝐿‘suc 𝑗) ↔ (𝑟 ∈ (𝐿‘𝑗) ∨ (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑟 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) ∨ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑟 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)))))
72		simp3l 1202	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → ∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s )
73	19	rspccv 3603	. . . . . . . . . . 11 ⊢ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s → (𝑟 ∈ (𝐿‘𝑗) → (𝐴 ·s 𝑟) <s 1s ))
74	72, 73	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝑟 ∈ (𝐿‘𝑗) → (𝐴 ·s 𝑟) <s 1s ))
75	33	3ad2ant1 1133	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → 𝐴 ∈ No )
76	75	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝐴 ∈ No )
77		1sno 27796	. . . . . . . . . . . . . . . . 17 ⊢ 1s ∈ No
78	77	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 1s ∈ No )
79		rightssno 27850	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ( R ‘𝐴) ⊆ No
80	79	sseli 3959	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥𝑅 ∈ ( R ‘𝐴) → 𝑥𝑅 ∈ No )
81	80	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 𝑥𝑅 ∈ No )
82	75	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 𝐴 ∈ No )
83	81, 82	subscld 28024	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → (𝑥𝑅 -s 𝐴) ∈ No )
84	83	adantrr 717	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝑥𝑅 -s 𝐴) ∈ No )
85		precsexlem.5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 0s <s 𝐴)
86		precsexlem.6	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ))
87	38, 39, 40, 33, 85, 86	precsexlem8 28173	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ ω) → ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No ))
88	87	simpld 494	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ω) → (𝐿‘𝑗) ⊆ No )
89	88	3adant3 1132	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝐿‘𝑗) ⊆ No )
90	89	sselda 3963	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗)) → 𝑦𝐿 ∈ No )
91	90	adantrl 716	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑦𝐿 ∈ No )
92	84, 91	mulscld 28095	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿) ∈ No )
93	78, 92	addscld 27944	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) ∈ No )
94	81	adantrr 717	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑥𝑅 ∈ No )
95	43	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 0s ∈ No )
96	85	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → 0s <s 𝐴)
97	96	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 0s <s 𝐴)
98		rightgt 27833	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝑅 ∈ ( R ‘𝐴) → 𝐴 <s 𝑥𝑅)
99	98	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 𝐴 <s 𝑥𝑅)
100	95, 82, 81, 97, 99	slttrd 27728	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 0s <s 𝑥𝑅)
101	100	sgt0ne0d 27805	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 𝑥𝑅 ≠ 0s )
102	101	adantrr 717	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑥𝑅 ≠ 0s )
103		breq2 5128	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝑂 = 𝑥𝑅 → ( 0s <s 𝑥𝑂 ↔ 0s <s 𝑥𝑅))
104		oveq1 7417	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥𝑂 = 𝑥𝑅 → (𝑥𝑂 ·s 𝑦) = (𝑥𝑅 ·s 𝑦))
105	104	eqeq1d 2738	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥𝑂 = 𝑥𝑅 → ((𝑥𝑂 ·s 𝑦) = 1s ↔ (𝑥𝑅 ·s 𝑦) = 1s ))
106	105	rexbidv 3165	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝑂 = 𝑥𝑅 → (∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ↔ ∃𝑦 ∈ No (𝑥𝑅 ·s 𝑦) = 1s ))
107	103, 106	imbi12d 344	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥𝑂 = 𝑥𝑅 → (( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ) ↔ ( 0s <s 𝑥𝑅 → ∃𝑦 ∈ No (𝑥𝑅 ·s 𝑦) = 1s )))
108	86	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ))
109	108	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ))
110		elun2 4163	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝑅 ∈ ( R ‘𝐴) → 𝑥𝑅 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))
111	110	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 𝑥𝑅 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))
112	107, 109, 111	rspcdva 3607	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → ( 0s <s 𝑥𝑅 → ∃𝑦 ∈ No (𝑥𝑅 ·s 𝑦) = 1s ))
113	100, 112	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → ∃𝑦 ∈ No (𝑥𝑅 ·s 𝑦) = 1s )
114	113	adantrr 717	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ∃𝑦 ∈ No (𝑥𝑅 ·s 𝑦) = 1s )
115	76, 93, 94, 102, 114	divsasswd 28163	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) /su 𝑥𝑅) = (𝐴 ·s (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)))
116		oveq2 7418	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = 𝑦𝐿 → (𝐴 ·s 𝑏) = (𝐴 ·s 𝑦𝐿))
117	116	breq1d 5134	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = 𝑦𝐿 → ((𝐴 ·s 𝑏) <s 1s ↔ (𝐴 ·s 𝑦𝐿) <s 1s ))
118	117	rspccva 3605	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ 𝑦𝐿 ∈ (𝐿‘𝑗)) → (𝐴 ·s 𝑦𝐿) <s 1s )
119	72, 118	sylan 580	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗)) → (𝐴 ·s 𝑦𝐿) <s 1s )
120	119	adantrl 716	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s 𝑦𝐿) <s 1s )
121	76, 91	mulscld 28095	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s 𝑦𝐿) ∈ No )
122	82, 81	posdifsd 28058	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → (𝐴 <s 𝑥𝑅 ↔ 0s <s (𝑥𝑅 -s 𝐴)))
123	99, 122	mpbid 232	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 0s <s (𝑥𝑅 -s 𝐴))
124	123	adantrr 717	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 0s <s (𝑥𝑅 -s 𝐴))
125	121, 78, 84, 124	sltmul2d 28132	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 ·s 𝑦𝐿) <s 1s ↔ ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)) <s ((𝑥𝑅 -s 𝐴) ·s 1s )))
126	120, 125	mpbid 232	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)) <s ((𝑥𝑅 -s 𝐴) ·s 1s ))
127	84	mulsridd 28074	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s 1s ) = (𝑥𝑅 -s 𝐴))
128	126, 127	breqtrd 5150	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)) <s (𝑥𝑅 -s 𝐴))
129	84, 121	mulscld 28095	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)) ∈ No )
130	76, 129, 94	sltaddsub2d 28053	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 +s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))) <s 𝑥𝑅 ↔ ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)) <s (𝑥𝑅 -s 𝐴)))
131	128, 130	mpbird 257	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 +s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))) <s 𝑥𝑅)
132	76, 78, 92	addsdid 28116	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) = ((𝐴 ·s 1s ) +s (𝐴 ·s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))))
133	76	mulsridd 28074	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s 1s ) = 𝐴)
134	76, 84, 91	muls12d 28141	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) = ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)))
135	133, 134	oveq12d 7428	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 ·s 1s ) +s (𝐴 ·s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) = (𝐴 +s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))))
136	132, 135	eqtrd 2771	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) = (𝐴 +s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))))
137	94	mulslidd 28103	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( 1s ·s 𝑥𝑅) = 𝑥𝑅)
138	131, 136, 137	3brtr4d 5156	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) <s ( 1s ·s 𝑥𝑅))
139	76, 93	mulscld 28095	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) ∈ No )
140	100	adantrr 717	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 0s <s 𝑥𝑅)
141	139, 78, 94, 140, 114	sltdivmul2wd 28160	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (((𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) /su 𝑥𝑅) <s 1s ↔ (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) <s ( 1s ·s 𝑥𝑅)))
142	138, 141	mpbird 257	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) /su 𝑥𝑅) <s 1s )
143	115, 142	eqbrtrrd 5148	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)) <s 1s )
144		oveq2 7418	. . . . . . . . . . . . . 14 ⊢ (𝑟 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) → (𝐴 ·s 𝑟) = (𝐴 ·s (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)))
145	144	breq1d 5134	. . . . . . . . . . . . 13 ⊢ (𝑟 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) → ((𝐴 ·s 𝑟) <s 1s ↔ (𝐴 ·s (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)) <s 1s ))
146	143, 145	syl5ibrcom 247	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝑟 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) → (𝐴 ·s 𝑟) <s 1s ))
147	146	rexlimdvva 3202	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑟 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) → (𝐴 ·s 𝑟) <s 1s ))
148	75	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝐴 ∈ No )
149	77	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 1s ∈ No )
150		leftssno 27849	. . . . . . . . . . . . . . . . . . . 20 ⊢ ( L ‘𝐴) ⊆ No
151		elrabi 3671	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} → 𝑥𝐿 ∈ ( L ‘𝐴))
152	151	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → 𝑥𝐿 ∈ ( L ‘𝐴))
153	150, 152	sselid 3961	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → 𝑥𝐿 ∈ No )
154	75	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → 𝐴 ∈ No )
155	153, 154	subscld 28024	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → (𝑥𝐿 -s 𝐴) ∈ No )
156	155	adantrr 717	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝑥𝐿 -s 𝐴) ∈ No )
157	87	simprd 495	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ω) → (𝑅‘𝑗) ⊆ No )
158	157	3adant3 1132	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝑅‘𝑗) ⊆ No )
159	158	sselda 3963	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗)) → 𝑦𝑅 ∈ No )
160	159	adantrl 716	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑦𝑅 ∈ No )
161	156, 160	mulscld 28095	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅) ∈ No )
162	149, 161	addscld 27944	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) ∈ No )
163	153	adantrr 717	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑥𝐿 ∈ No )
164		breq2 5128	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑥𝐿 → ( 0s <s 𝑥 ↔ 0s <s 𝑥𝐿))
165	164	elrab 3676	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ↔ (𝑥𝐿 ∈ ( L ‘𝐴) ∧ 0s <s 𝑥𝐿))
166	165	simprbi 496	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} → 0s <s 𝑥𝐿)
167	166	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → 0s <s 𝑥𝐿)
168	167	sgt0ne0d 27805	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → 𝑥𝐿 ≠ 0s )
169	168	adantrr 717	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑥𝐿 ≠ 0s )
170		breq2 5128	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝑂 = 𝑥𝐿 → ( 0s <s 𝑥𝑂 ↔ 0s <s 𝑥𝐿))
171		oveq1 7417	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥𝑂 = 𝑥𝐿 → (𝑥𝑂 ·s 𝑦) = (𝑥𝐿 ·s 𝑦))
172	171	eqeq1d 2738	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥𝑂 = 𝑥𝐿 → ((𝑥𝑂 ·s 𝑦) = 1s ↔ (𝑥𝐿 ·s 𝑦) = 1s ))
173	172	rexbidv 3165	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝑂 = 𝑥𝐿 → (∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ↔ ∃𝑦 ∈ No (𝑥𝐿 ·s 𝑦) = 1s ))
174	170, 173	imbi12d 344	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥𝑂 = 𝑥𝐿 → (( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ) ↔ ( 0s <s 𝑥𝐿 → ∃𝑦 ∈ No (𝑥𝐿 ·s 𝑦) = 1s )))
175	108	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ))
176		elun1 4162	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝐿 ∈ ( L ‘𝐴) → 𝑥𝐿 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))
177	152, 176	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → 𝑥𝐿 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))
178	174, 175, 177	rspcdva 3607	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → ( 0s <s 𝑥𝐿 → ∃𝑦 ∈ No (𝑥𝐿 ·s 𝑦) = 1s ))
179	167, 178	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → ∃𝑦 ∈ No (𝑥𝐿 ·s 𝑦) = 1s )
180	179	adantrr 717	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ∃𝑦 ∈ No (𝑥𝐿 ·s 𝑦) = 1s )
181	148, 162, 163, 169, 180	divsasswd 28163	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))) /su 𝑥𝐿) = (𝐴 ·s (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)))
182	154, 153	subscld 28024	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → (𝐴 -s 𝑥𝐿) ∈ No )
183	182	adantrr 717	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 -s 𝑥𝐿) ∈ No )
184	183	mulsridd 28074	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝐴 -s 𝑥𝐿) ·s 1s ) = (𝐴 -s 𝑥𝐿))
185		simp3r 1203	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))
186		oveq2 7418	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = 𝑦𝑅 → (𝐴 ·s 𝑐) = (𝐴 ·s 𝑦𝑅))
187	186	breq2d 5136	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = 𝑦𝑅 → ( 1s <s (𝐴 ·s 𝑐) ↔ 1s <s (𝐴 ·s 𝑦𝑅)))
188	187	rspccva 3605	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗)) → 1s <s (𝐴 ·s 𝑦𝑅))
189	185, 188	sylan 580	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗)) → 1s <s (𝐴 ·s 𝑦𝑅))
190	189	adantrl 716	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 1s <s (𝐴 ·s 𝑦𝑅))
191	148, 160	mulscld 28095	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s 𝑦𝑅) ∈ No )
192		leftlt 27832	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥𝐿 ∈ ( L ‘𝐴) → 𝑥𝐿 <s 𝐴)
193	152, 192	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → 𝑥𝐿 <s 𝐴)
194	153, 154	posdifsd 28058	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → (𝑥𝐿 <s 𝐴 ↔ 0s <s (𝐴 -s 𝑥𝐿)))
195	193, 194	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → 0s <s (𝐴 -s 𝑥𝐿))
196	195	adantrr 717	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 0s <s (𝐴 -s 𝑥𝐿))
197	149, 191, 183, 196	sltmul2d 28132	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( 1s <s (𝐴 ·s 𝑦𝑅) ↔ ((𝐴 -s 𝑥𝐿) ·s 1s ) <s ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝑅))))
198	190, 197	mpbid 232	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝐴 -s 𝑥𝐿) ·s 1s ) <s ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝑅)))
199	184, 198	eqbrtrrd 5148	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 -s 𝑥𝐿) <s ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝑅)))
200	153, 154	negsubsdi2d 28041	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → ( -us ‘(𝑥𝐿 -s 𝐴)) = (𝐴 -s 𝑥𝐿))
201	200	adantrr 717	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( -us ‘(𝑥𝐿 -s 𝐴)) = (𝐴 -s 𝑥𝐿))
202	156, 191	mulnegs1d 28120	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (( -us ‘(𝑥𝐿 -s 𝐴)) ·s (𝐴 ·s 𝑦𝑅)) = ( -us ‘((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))))
203	200	oveq1d 7425	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → (( -us ‘(𝑥𝐿 -s 𝐴)) ·s (𝐴 ·s 𝑦𝑅)) = ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝑅)))
204	203	adantrr 717	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (( -us ‘(𝑥𝐿 -s 𝐴)) ·s (𝐴 ·s 𝑦𝑅)) = ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝑅)))
205	202, 204	eqtr3d 2773	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( -us ‘((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))) = ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝑅)))
206	199, 201, 205	3brtr4d 5156	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( -us ‘(𝑥𝐿 -s 𝐴)) <s ( -us ‘((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))))
207	156, 191	mulscld 28095	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)) ∈ No )
208	207, 156	sltnegd 28010	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)) <s (𝑥𝐿 -s 𝐴) ↔ ( -us ‘(𝑥𝐿 -s 𝐴)) <s ( -us ‘((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)))))
209	206, 208	mpbird 257	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)) <s (𝑥𝐿 -s 𝐴))
210	148, 207, 163	sltaddsub2d 28053	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝐴 +s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))) <s 𝑥𝐿 ↔ ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)) <s (𝑥𝐿 -s 𝐴)))
211	209, 210	mpbird 257	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 +s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))) <s 𝑥𝐿)
212	148, 149, 161	addsdid 28116	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))) = ((𝐴 ·s 1s ) +s (𝐴 ·s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))))
213	148	mulsridd 28074	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s 1s ) = 𝐴)
214	148, 156, 160	muls12d 28141	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) = ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)))
215	213, 214	oveq12d 7428	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝐴 ·s 1s ) +s (𝐴 ·s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))) = (𝐴 +s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))))
216	212, 215	eqtrd 2771	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))) = (𝐴 +s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))))
217	163	mulsridd 28074	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝑥𝐿 ·s 1s ) = 𝑥𝐿)
218	211, 216, 217	3brtr4d 5156	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))) <s (𝑥𝐿 ·s 1s ))
219	148, 162	mulscld 28095	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))) ∈ No )
220	167	adantrr 717	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 0s <s 𝑥𝐿)
221	219, 149, 163, 220, 180	sltdivmulwd 28159	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (((𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))) /su 𝑥𝐿) <s 1s ↔ (𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))) <s (𝑥𝐿 ·s 1s )))
222	218, 221	mpbird 257	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))) /su 𝑥𝐿) <s 1s )
223	181, 222	eqbrtrrd 5148	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)) <s 1s )
224		oveq2 7418	. . . . . . . . . . . . . 14 ⊢ (𝑟 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) → (𝐴 ·s 𝑟) = (𝐴 ·s (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)))
225	224	breq1d 5134	. . . . . . . . . . . . 13 ⊢ (𝑟 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) → ((𝐴 ·s 𝑟) <s 1s ↔ (𝐴 ·s (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)) <s 1s ))
226	223, 225	syl5ibrcom 247	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝑟 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) → (𝐴 ·s 𝑟) <s 1s ))
227	226	rexlimdvva 3202	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑟 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) → (𝐴 ·s 𝑟) <s 1s ))
228	147, 227	jaod 859	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → ((∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑟 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) ∨ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑟 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)) → (𝐴 ·s 𝑟) <s 1s ))
229	74, 228	jaod 859	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → ((𝑟 ∈ (𝐿‘𝑗) ∨ (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑟 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) ∨ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑟 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿))) → (𝐴 ·s 𝑟) <s 1s ))
230	71, 229	sylbid 240	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝑟 ∈ (𝐿‘suc 𝑗) → (𝐴 ·s 𝑟) <s 1s ))
231	230	ralrimiv 3132	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → ∀𝑟 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑟) <s 1s )
232	38, 39, 40	precsexlem5 28170	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ω → (𝑅‘suc 𝑗) = ((𝑅‘𝑗) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)})))
233	232	3ad2ant2 1134	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝑅‘suc 𝑗) = ((𝑅‘𝑗) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)})))
234	233	eleq2d 2821	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝑠 ∈ (𝑅‘suc 𝑗) ↔ 𝑠 ∈ ((𝑅‘𝑗) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))))
235		elun 4133	. . . . . . . . . . 11 ⊢ (𝑠 ∈ ((𝑅‘𝑗) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)})) ↔ (𝑠 ∈ (𝑅‘𝑗) ∨ 𝑠 ∈ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)})))
236		elun 4133	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}) ↔ (𝑠 ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∨ 𝑠 ∈ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))
237		vex 3468	. . . . . . . . . . . . . . 15 ⊢ 𝑠 ∈ V
238		eqeq1 2740	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑠 → (𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) ↔ 𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)))
239	238	2rexbidv 3210	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑠 → (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) ↔ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)))
240	237, 239	elab 3663	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ↔ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿))
241		eqeq1 2740	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑠 → (𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) ↔ 𝑠 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)))
242	241	2rexbidv 3210	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑠 → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) ↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑠 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)))
243	237, 242	elab 3663	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)} ↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑠 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅))
244	240, 243	orbi12i 914	. . . . . . . . . . . . 13 ⊢ ((𝑠 ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∨ 𝑠 ∈ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}) ↔ (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) ∨ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑠 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)))
245	236, 244	bitri 275	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}) ↔ (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) ∨ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑠 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)))
246	245	orbi2i 912	. . . . . . . . . . 11 ⊢ ((𝑠 ∈ (𝑅‘𝑗) ∨ 𝑠 ∈ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)})) ↔ (𝑠 ∈ (𝑅‘𝑗) ∨ (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) ∨ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑠 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅))))
247	235, 246	bitri 275	. . . . . . . . . 10 ⊢ (𝑠 ∈ ((𝑅‘𝑗) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)})) ↔ (𝑠 ∈ (𝑅‘𝑗) ∨ (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) ∨ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑠 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅))))
248	234, 247	bitrdi 287	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝑠 ∈ (𝑅‘suc 𝑗) ↔ (𝑠 ∈ (𝑅‘𝑗) ∨ (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) ∨ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑠 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)))))
249	22	rspccv 3603	. . . . . . . . . . 11 ⊢ (∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐) → (𝑠 ∈ (𝑅‘𝑗) → 1s <s (𝐴 ·s 𝑠)))
250	185, 249	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝑠 ∈ (𝑅‘𝑗) → 1s <s (𝐴 ·s 𝑠)))
251	119	adantrl 716	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s 𝑦𝐿) <s 1s )
252	75	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝐴 ∈ No )
253	90	adantrl 716	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑦𝐿 ∈ No )
254	252, 253	mulscld 28095	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s 𝑦𝐿) ∈ No )
255	77	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 1s ∈ No )
256	182	adantrr 717	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 -s 𝑥𝐿) ∈ No )
257	195	adantrr 717	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 0s <s (𝐴 -s 𝑥𝐿))
258	254, 255, 256, 257	sltmul2d 28132	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 ·s 𝑦𝐿) <s 1s ↔ ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝐿)) <s ((𝐴 -s 𝑥𝐿) ·s 1s )))
259	251, 258	mpbid 232	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝐿)) <s ((𝐴 -s 𝑥𝐿) ·s 1s ))
260	256	mulsridd 28074	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 -s 𝑥𝐿) ·s 1s ) = (𝐴 -s 𝑥𝐿))
261	259, 260	breqtrd 5150	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝐿)) <s (𝐴 -s 𝑥𝐿))
262	155	adantrr 717	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝑥𝐿 -s 𝐴) ∈ No )
263	262, 254	mulnegs1d 28120	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (( -us ‘(𝑥𝐿 -s 𝐴)) ·s (𝐴 ·s 𝑦𝐿)) = ( -us ‘((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))))
264	200	oveq1d 7425	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → (( -us ‘(𝑥𝐿 -s 𝐴)) ·s (𝐴 ·s 𝑦𝐿)) = ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝐿)))
265	264	adantrr 717	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (( -us ‘(𝑥𝐿 -s 𝐴)) ·s (𝐴 ·s 𝑦𝐿)) = ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝐿)))
266	263, 265	eqtr3d 2773	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( -us ‘((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))) = ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝐿)))
267	200	adantrr 717	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( -us ‘(𝑥𝐿 -s 𝐴)) = (𝐴 -s 𝑥𝐿))
268	261, 266, 267	3brtr4d 5156	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( -us ‘((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))) <s ( -us ‘(𝑥𝐿 -s 𝐴)))
269	262, 254	mulscld 28095	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)) ∈ No )
270	262, 269	sltnegd 28010	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝐿 -s 𝐴) <s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)) ↔ ( -us ‘((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))) <s ( -us ‘(𝑥𝐿 -s 𝐴))))
271	268, 270	mpbird 257	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝑥𝐿 -s 𝐴) <s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)))
272	153	adantrr 717	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑥𝐿 ∈ No )
273	272, 252, 269	sltsubadd2d 28051	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝐿 -s 𝐴) <s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)) ↔ 𝑥𝐿 <s (𝐴 +s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)))))
274	271, 273	mpbid 232	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑥𝐿 <s (𝐴 +s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))))
275	272	mulslidd 28103	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( 1s ·s 𝑥𝐿) = 𝑥𝐿)
276	262, 253	mulscld 28095	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿) ∈ No )
277	252, 255, 276	addsdid 28116	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))) = ((𝐴 ·s 1s ) +s (𝐴 ·s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))))
278	252	mulsridd 28074	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s 1s ) = 𝐴)
279	252, 262, 253	muls12d 28141	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) = ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)))
280	278, 279	oveq12d 7428	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 ·s 1s ) +s (𝐴 ·s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))) = (𝐴 +s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))))
281	277, 280	eqtrd 2771	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))) = (𝐴 +s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))))
282	274, 275, 281	3brtr4d 5156	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( 1s ·s 𝑥𝐿) <s (𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))))
283	255, 276	addscld 27944	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) ∈ No )
284	252, 283	mulscld 28095	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))) ∈ No )
285	167	adantrr 717	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 0s <s 𝑥𝐿)
286	179	adantrr 717	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ∃𝑦 ∈ No (𝑥𝐿 ·s 𝑦) = 1s )
287	255, 284, 272, 285, 286	sltmuldivwd 28161	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (( 1s ·s 𝑥𝐿) <s (𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))) ↔ 1s <s ((𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))) /su 𝑥𝐿)))
288	282, 287	mpbid 232	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 1s <s ((𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))) /su 𝑥𝐿))
289	168	adantrr 717	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑥𝐿 ≠ 0s )
290	252, 283, 272, 289, 286	divsasswd 28163	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))) /su 𝑥𝐿) = (𝐴 ·s (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)))
291	288, 290	breqtrd 5150	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 1s <s (𝐴 ·s (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)))
292		oveq2 7418	. . . . . . . . . . . . . 14 ⊢ (𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) → (𝐴 ·s 𝑠) = (𝐴 ·s (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)))
293	292	breq2d 5136	. . . . . . . . . . . . 13 ⊢ (𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) → ( 1s <s (𝐴 ·s 𝑠) ↔ 1s <s (𝐴 ·s (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿))))
294	291, 293	syl5ibrcom 247	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) → 1s <s (𝐴 ·s 𝑠)))
295	294	rexlimdvva 3202	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) → 1s <s (𝐴 ·s 𝑠)))
296	83	adantrr 717	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝑥𝑅 -s 𝐴) ∈ No )
297	296	mulsridd 28074	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s 1s ) = (𝑥𝑅 -s 𝐴))
298	189	adantrl 716	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 1s <s (𝐴 ·s 𝑦𝑅))
299	77	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 1s ∈ No )
300	75	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝐴 ∈ No )
301	159	adantrl 716	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑦𝑅 ∈ No )
302	300, 301	mulscld 28095	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s 𝑦𝑅) ∈ No )
303	123	adantrr 717	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 0s <s (𝑥𝑅 -s 𝐴))
304	299, 302, 296, 303	sltmul2d 28132	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( 1s <s (𝐴 ·s 𝑦𝑅) ↔ ((𝑥𝑅 -s 𝐴) ·s 1s ) <s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))))
305	298, 304	mpbid 232	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s 1s ) <s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)))
306	297, 305	eqbrtrrd 5148	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝑥𝑅 -s 𝐴) <s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)))
307	81	adantrr 717	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑥𝑅 ∈ No )
308	296, 302	mulscld 28095	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)) ∈ No )
309	307, 300, 308	sltsubadd2d 28051	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝑥𝑅 -s 𝐴) <s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)) ↔ 𝑥𝑅 <s (𝐴 +s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)))))
310	306, 309	mpbid 232	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑥𝑅 <s (𝐴 +s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))))
311	307	mulslidd 28103	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( 1s ·s 𝑥𝑅) = 𝑥𝑅)
312	296, 301	mulscld 28095	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅) ∈ No )
313	300, 299, 312	addsdid 28116	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))) = ((𝐴 ·s 1s ) +s (𝐴 ·s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))))
314	300	mulsridd 28074	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s 1s ) = 𝐴)
315	300, 296, 301	muls12d 28141	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) = ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)))
316	314, 315	oveq12d 7428	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝐴 ·s 1s ) +s (𝐴 ·s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))) = (𝐴 +s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))))
317	313, 316	eqtrd 2771	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))) = (𝐴 +s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))))
318	310, 311, 317	3brtr4d 5156	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( 1s ·s 𝑥𝑅) <s (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))))
319	299, 312	addscld 27944	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) ∈ No )
320	300, 319	mulscld 28095	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))) ∈ No )
321	100	adantrr 717	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 0s <s 𝑥𝑅)
322	113	adantrr 717	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ∃𝑦 ∈ No (𝑥𝑅 ·s 𝑦) = 1s )
323	299, 320, 307, 321, 322	sltmuldivwd 28161	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (( 1s ·s 𝑥𝑅) <s (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))) ↔ 1s <s ((𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))) /su 𝑥𝑅)))
324	318, 323	mpbid 232	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 1s <s ((𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))) /su 𝑥𝑅))
325	101	adantrr 717	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑥𝑅 ≠ 0s )
326	300, 319, 307, 325, 322	divsasswd 28163	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))) /su 𝑥𝑅) = (𝐴 ·s (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)))
327	324, 326	breqtrd 5150	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 1s <s (𝐴 ·s (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)))
328		oveq2 7418	. . . . . . . . . . . . . 14 ⊢ (𝑠 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) → (𝐴 ·s 𝑠) = (𝐴 ·s (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)))
329	328	breq2d 5136	. . . . . . . . . . . . 13 ⊢ (𝑠 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) → ( 1s <s (𝐴 ·s 𝑠) ↔ 1s <s (𝐴 ·s (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅))))
330	327, 329	syl5ibrcom 247	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝑠 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) → 1s <s (𝐴 ·s 𝑠)))
331	330	rexlimdvva 3202	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑠 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) → 1s <s (𝐴 ·s 𝑠)))
332	295, 331	jaod 859	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → ((∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) ∨ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑠 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)) → 1s <s (𝐴 ·s 𝑠)))
333	250, 332	jaod 859	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → ((𝑠 ∈ (𝑅‘𝑗) ∨ (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) ∨ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑠 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅))) → 1s <s (𝐴 ·s 𝑠)))
334	248, 333	sylbid 240	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝑠 ∈ (𝑅‘suc 𝑗) → 1s <s (𝐴 ·s 𝑠)))
335	334	ralrimiv 3132	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → ∀𝑠 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑠))
336	231, 335	jca 511	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (∀𝑟 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑟) <s 1s ∧ ∀𝑠 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑠)))
337	336	3exp 1119	. . . . 5 ⊢ (𝜑 → (𝑗 ∈ ω → ((∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐)) → (∀𝑟 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑟) <s 1s ∧ ∀𝑠 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑠)))))
338	337	com12 32	. . . 4 ⊢ (𝑗 ∈ ω → (𝜑 → ((∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐)) → (∀𝑟 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑟) <s 1s ∧ ∀𝑠 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑠)))))
339	338	a2d 29	. . 3 ⊢ (𝑗 ∈ ω → ((𝜑 → (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝜑 → (∀𝑟 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑟) <s 1s ∧ ∀𝑠 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑠)))))
340	6, 12, 26, 32, 54, 339	finds 7897	. 2 ⊢ (𝐼 ∈ ω → (𝜑 → (∀𝑏 ∈ (𝐿‘𝐼)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝐼) 1s <s (𝐴 ·s 𝑐))))
341	340	impcom 407	1 ⊢ ((𝜑 ∧ 𝐼 ∈ ω) → (∀𝑏 ∈ (𝐿‘𝐼)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝐼) 1s <s (𝐴 ·s 𝑐)))

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  {cab 2714   ≠ wne 2933  ∀wral 3052  ∃wrex 3061  {crab 3420  Vcvv 3464  ⦋csb 3879   ∪ cun 3929   ⊆ wss 3931  ∅c0 4313  {csn 4606  ⟨cop 4612   class class class wbr 5124   ↦ cmpt 5206   ∘ ccom 5663  suc csuc 6359  ‘cfv 6536  (class class class)co 7410  ωcom 7866  1^st c1st 7991  2^nd c2nd 7992  reccrdg 8428   No csur 27608   <s cslt 27609   0_s c0s 27791   1_s c1s 27792   L cleft 27810   R cright 27811   +_s cadds 27923   -u_s cnegs 27982   -_s csubs 27983   ·_s cmuls 28066   /_su cdivs 28147

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-rep 5254  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rmo 3364  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-tp 4611  df-op 4613  df-ot 4615  df-uni 4889  df-int 4928  df-iun 4974  df-br 5125  df-opab 5187  df-mpt 5207  df-tr 5235  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-se 5612  df-we 5613  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6295  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7867  df-1st 7993  df-2nd 7994  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-1o 8485  df-2o 8486  df-nadd 8683  df-no 27611  df-slt 27612  df-bday 27613  df-sle 27714  df-sslt 27750  df-scut 27752  df-0s 27793  df-1s 27794  df-made 27812  df-old 27813  df-left 27815  df-right 27816  df-norec 27902  df-norec2 27913  df-adds 27924  df-negs 27984  df-subs 27985  df-muls 28067  df-divs 28148

This theorem is referenced by:  precsexlem10  28175  precsexlem11  28176