Theorem precsexlem9 28153

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 6822	. . . . . 6 ⊢ (𝑖 = ∅ → (𝐿‘𝑖) = (𝐿‘∅))
2	1	raleqdv 3292	. . . . 5 ⊢ (𝑖 = ∅ → (∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ↔ ∀𝑏 ∈ (𝐿‘∅)(𝐴 ·s 𝑏) <s 1s ))
3		fveq2 6822	. . . . . 6 ⊢ (𝑖 = ∅ → (𝑅‘𝑖) = (𝑅‘∅))
4	3	raleqdv 3292	. . . . 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 6822	. . . . . 6 ⊢ (𝑖 = 𝑗 → (𝐿‘𝑖) = (𝐿‘𝑗))
8	7	raleqdv 3292	. . . . 5 ⊢ (𝑖 = 𝑗 → (∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ↔ ∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ))
9		fveq2 6822	. . . . . 6 ⊢ (𝑖 = 𝑗 → (𝑅‘𝑖) = (𝑅‘𝑗))
10	9	raleqdv 3292	. . . . 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 6822	. . . . . . 7 ⊢ (𝑖 = suc 𝑗 → (𝐿‘𝑖) = (𝐿‘suc 𝑗))
14	13	raleqdv 3292	. . . . . 6 ⊢ (𝑖 = suc 𝑗 → (∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ↔ ∀𝑏 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑏) <s 1s ))
15		fveq2 6822	. . . . . . 7 ⊢ (𝑖 = suc 𝑗 → (𝑅‘𝑖) = (𝑅‘suc 𝑗))
16	15	raleqdv 3292	. . . . . 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 7354	. . . . . . . 8 ⊢ (𝑏 = 𝑟 → (𝐴 ·s 𝑏) = (𝐴 ·s 𝑟))
19	18	breq1d 5099	. . . . . . 7 ⊢ (𝑏 = 𝑟 → ((𝐴 ·s 𝑏) <s 1s ↔ (𝐴 ·s 𝑟) <s 1s ))
20	19	cbvralvw 3210	. . . . . 6 ⊢ (∀𝑏 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑏) <s 1s ↔ ∀𝑟 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑟) <s 1s )
21		oveq2 7354	. . . . . . . 8 ⊢ (𝑐 = 𝑠 → (𝐴 ·s 𝑐) = (𝐴 ·s 𝑠))
22	21	breq2d 5101	. . . . . . 7 ⊢ (𝑐 = 𝑠 → ( 1s <s (𝐴 ·s 𝑐) ↔ 1s <s (𝐴 ·s 𝑠)))
23	22	cbvralvw 3210	. . . . . 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 6822	. . . . . 6 ⊢ (𝑖 = 𝐼 → (𝐿‘𝑖) = (𝐿‘𝐼))
28	27	raleqdv 3292	. . . . 5 ⊢ (𝑖 = 𝐼 → (∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ↔ ∀𝑏 ∈ (𝐿‘𝐼)(𝐴 ·s 𝑏) <s 1s ))
29		fveq2 6822	. . . . . 6 ⊢ (𝑖 = 𝐼 → (𝑅‘𝑖) = (𝑅‘𝐼))
30	29	raleqdv 3292	. . . . 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 28051	. . . . . . 7 ⊢ (𝐴 ∈ No → (𝐴 ·s 0s ) = 0s )
35	33, 34	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐴 ·s 0s ) = 0s )
36		0slt1s 27773	. . . . . 6 ⊢ 0s <s 1s
37	35, 36	eqbrtrdi 5128	. . . . 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 28145	. . . . . . 7 ⊢ (𝐿‘∅) = { 0s }
42	41	raleqi 3290	. . . . . 6 ⊢ (∀𝑏 ∈ (𝐿‘∅)(𝐴 ·s 𝑏) <s 1s ↔ ∀𝑏 ∈ { 0s } (𝐴 ·s 𝑏) <s 1s )
43		0sno 27770	. . . . . . . 8 ⊢ 0s ∈ No
44	43	elexi 3459	. . . . . . 7 ⊢ 0s ∈ V
45		oveq2 7354	. . . . . . . 8 ⊢ (𝑏 = 0s → (𝐴 ·s 𝑏) = (𝐴 ·s 0s ))
46	45	breq1d 5099	. . . . . . 7 ⊢ (𝑏 = 0s → ((𝐴 ·s 𝑏) <s 1s ↔ (𝐴 ·s 0s ) <s 1s ))
47	44, 46	ralsn 4631	. . . . . 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 4460	. . . . 5 ⊢ ∀𝑐 ∈ ∅ 1s <s (𝐴 ·s 𝑐)
51	38, 39, 40	precsexlem2 28146	. . . . . 6 ⊢ (𝑅‘∅) = ∅
52	51	raleqi 3290	. . . . 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 28148	. . . . . . . . . . . 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 2817	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝑟 ∈ (𝐿‘suc 𝑗) ↔ 𝑟 ∈ ((𝐿‘𝑗) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)}))))
58		elun 4100	. . . . . . . . . . 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 4100	. . . . . . . . . . . . 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 3440	. . . . . . . . . . . . . . 15 ⊢ 𝑟 ∈ V
61		eqeq1 2735	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑟 → (𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) ↔ 𝑟 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)))
62	61	2rexbidv 3197	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑟 → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) ↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑟 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)))
63	60, 62	elab 3630	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑟 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅))
64		eqeq1 2735	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑟 → (𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) ↔ 𝑟 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)))
65	64	2rexbidv 3197	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑟 → (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) ↔ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑟 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)))
66	60, 65	elab 3630	. . . . . . . . . . . . . 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 3569	. . . . . . . . . . 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 27771	. . . . . . . . . . . . . . . . 17 ⊢ 1s ∈ No
78	77	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 1s ∈ No )
79		rightssno 27827	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ( R ‘𝐴) ⊆ No
80	79	sseli 3925	. . . . . . . . . . . . . . . . . . . 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 28003	. . . . . . . . . . . . . . . . . 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 28152	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ ω) → ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No ))
88	87	simpld 494	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ω) → (𝐿‘𝑗) ⊆ No )
89	88	3adant3 1132	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝐿‘𝑗) ⊆ No )
90	89	sselda 3929	. . . . . . . . . . . . . . . . . 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 28074	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿) ∈ No )
93	78, 92	addscld 27923	. . . . . . . . . . . . . . 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 27809	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝑅 ∈ ( R ‘𝐴) → 𝐴 <s 𝑥𝑅)
99	98	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 𝐴 <s 𝑥𝑅)
100	95, 82, 81, 97, 99	slttrd 27698	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 0s <s 𝑥𝑅)
101	100	sgt0ne0d 27780	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 𝑥𝑅 ≠ 0s )
102	101	adantrr 717	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑥𝑅 ≠ 0s )
103		breq2 5093	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝑂 = 𝑥𝑅 → ( 0s <s 𝑥𝑂 ↔ 0s <s 𝑥𝑅))
104		oveq1 7353	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥𝑂 = 𝑥𝑅 → (𝑥𝑂 ·s 𝑦) = (𝑥𝑅 ·s 𝑦))
105	104	eqeq1d 2733	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥𝑂 = 𝑥𝑅 → ((𝑥𝑂 ·s 𝑦) = 1s ↔ (𝑥𝑅 ·s 𝑦) = 1s ))
106	105	rexbidv 3156	. . . . . . . . . . . . . . . . . . 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 4130	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝑅 ∈ ( R ‘𝐴) → 𝑥𝑅 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))
111	110	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 𝑥𝑅 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))
112	107, 109, 111	rspcdva 3573	. . . . . . . . . . . . . . . . 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 28142	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) /su 𝑥𝑅) = (𝐴 ·s (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)))
116		oveq2 7354	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = 𝑦𝐿 → (𝐴 ·s 𝑏) = (𝐴 ·s 𝑦𝐿))
117	116	breq1d 5099	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = 𝑦𝐿 → ((𝐴 ·s 𝑏) <s 1s ↔ (𝐴 ·s 𝑦𝐿) <s 1s ))
118	117	rspccva 3571	. . . . . . . . . . . . . . . . . . . . 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 28074	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s 𝑦𝐿) ∈ No )
122	82, 81	posdifsd 28037	. . . . . . . . . . . . . . . . . . . . . 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 28111	. . . . . . . . . . . . . . . . . . 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 28053	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s 1s ) = (𝑥𝑅 -s 𝐴))
128	126, 127	breqtrd 5115	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)) <s (𝑥𝑅 -s 𝐴))
129	84, 121	mulscld 28074	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)) ∈ No )
130	76, 129, 94	sltaddsub2d 28032	. . . . . . . . . . . . . . . . 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 28095	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) = ((𝐴 ·s 1s ) +s (𝐴 ·s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))))
133	76	mulsridd 28053	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s 1s ) = 𝐴)
134	76, 84, 91	muls12d 28120	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) = ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)))
135	133, 134	oveq12d 7364	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 ·s 1s ) +s (𝐴 ·s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) = (𝐴 +s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))))
136	132, 135	eqtrd 2766	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) = (𝐴 +s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))))
137	94	mulslidd 28082	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( 1s ·s 𝑥𝑅) = 𝑥𝑅)
138	131, 136, 137	3brtr4d 5121	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) <s ( 1s ·s 𝑥𝑅))
139	76, 93	mulscld 28074	. . . . . . . . . . . . . . . 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 28139	. . . . . . . . . . . . . . 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 5113	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)) <s 1s )
144		oveq2 7354	. . . . . . . . . . . . . 14 ⊢ (𝑟 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) → (𝐴 ·s 𝑟) = (𝐴 ·s (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)))
145	144	breq1d 5099	. . . . . . . . . . . . 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 3189	. . . . . . . . . . 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 27826	. . . . . . . . . . . . . . . . . . . 20 ⊢ ( L ‘𝐴) ⊆ No
151		elrabi 3638	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} → 𝑥𝐿 ∈ ( L ‘𝐴))
152	151	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → 𝑥𝐿 ∈ ( L ‘𝐴))
153	150, 152	sselid 3927	. . . . . . . . . . . . . . . . . . 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 28003	. . . . . . . . . . . . . . . . . 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 3929	. . . . . . . . . . . . . . . . . 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 28074	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅) ∈ No )
162	149, 161	addscld 27923	. . . . . . . . . . . . . . 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 5093	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑥𝐿 → ( 0s <s 𝑥 ↔ 0s <s 𝑥𝐿))
165	164	elrab 3642	. . . . . . . . . . . . . . . . . . 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 27780	. . . . . . . . . . . . . . . 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 5093	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝑂 = 𝑥𝐿 → ( 0s <s 𝑥𝑂 ↔ 0s <s 𝑥𝐿))
171		oveq1 7353	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥𝑂 = 𝑥𝐿 → (𝑥𝑂 ·s 𝑦) = (𝑥𝐿 ·s 𝑦))
172	171	eqeq1d 2733	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥𝑂 = 𝑥𝐿 → ((𝑥𝑂 ·s 𝑦) = 1s ↔ (𝑥𝐿 ·s 𝑦) = 1s ))
173	172	rexbidv 3156	. . . . . . . . . . . . . . . . . . 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 4129	. . . . . . . . . . . . . . . . . . 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 3573	. . . . . . . . . . . . . . . . 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 28142	. . . . . . . . . . . . . 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 28003	. . . . . . . . . . . . . . . . . . . . . 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 28053	. . . . . . . . . . . . . . . . . . . 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 7354	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = 𝑦𝑅 → (𝐴 ·s 𝑐) = (𝐴 ·s 𝑦𝑅))
187	186	breq2d 5101	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = 𝑦𝑅 → ( 1s <s (𝐴 ·s 𝑐) ↔ 1s <s (𝐴 ·s 𝑦𝑅)))
188	187	rspccva 3571	. . . . . . . . . . . . . . . . . . . . . . 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 28074	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s 𝑦𝑅) ∈ No )
192		leftlt 27808	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥𝐿 ∈ ( L ‘𝐴) → 𝑥𝐿 <s 𝐴)
193	152, 192	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → 𝑥𝐿 <s 𝐴)
194	153, 154	posdifsd 28037	. . . . . . . . . . . . . . . . . . . . . . . 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 28111	. . . . . . . . . . . . . . . . . . . . 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 5113	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 -s 𝑥𝐿) <s ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝑅)))
200	153, 154	negsubsdi2d 28020	. . . . . . . . . . . . . . . . . . . 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 28099	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (( -us ‘(𝑥𝐿 -s 𝐴)) ·s (𝐴 ·s 𝑦𝑅)) = ( -us ‘((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))))
203	200	oveq1d 7361	. . . . . . . . . . . . . . . . . . . . 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 2768	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( -us ‘((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))) = ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝑅)))
206	199, 201, 205	3brtr4d 5121	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( -us ‘(𝑥𝐿 -s 𝐴)) <s ( -us ‘((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))))
207	156, 191	mulscld 28074	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)) ∈ No )
208	207, 156	sltnegd 27989	. . . . . . . . . . . . . . . . . 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 28032	. . . . . . . . . . . . . . . . 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 28095	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))) = ((𝐴 ·s 1s ) +s (𝐴 ·s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))))
213	148	mulsridd 28053	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s 1s ) = 𝐴)
214	148, 156, 160	muls12d 28120	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) = ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)))
215	213, 214	oveq12d 7364	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝐴 ·s 1s ) +s (𝐴 ·s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))) = (𝐴 +s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))))
216	212, 215	eqtrd 2766	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))) = (𝐴 +s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))))
217	163	mulsridd 28053	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝑥𝐿 ·s 1s ) = 𝑥𝐿)
218	211, 216, 217	3brtr4d 5121	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))) <s (𝑥𝐿 ·s 1s ))
219	148, 162	mulscld 28074	. . . . . . . . . . . . . . . 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 28138	. . . . . . . . . . . . . . 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 5113	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)) <s 1s )
224		oveq2 7354	. . . . . . . . . . . . . 14 ⊢ (𝑟 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) → (𝐴 ·s 𝑟) = (𝐴 ·s (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)))
225	224	breq1d 5099	. . . . . . . . . . . . 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 3189	. . . . . . . . . . 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 3123	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → ∀𝑟 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑟) <s 1s )
232	38, 39, 40	precsexlem5 28149	. . . . . . . . . . . 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 2817	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝑠 ∈ (𝑅‘suc 𝑗) ↔ 𝑠 ∈ ((𝑅‘𝑗) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))))
235		elun 4100	. . . . . . . . . . 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 4100	. . . . . . . . . . . . 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 3440	. . . . . . . . . . . . . . 15 ⊢ 𝑠 ∈ V
238		eqeq1 2735	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑠 → (𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) ↔ 𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)))
239	238	2rexbidv 3197	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑠 → (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) ↔ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)))
240	237, 239	elab 3630	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ↔ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿))
241		eqeq1 2735	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑠 → (𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) ↔ 𝑠 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)))
242	241	2rexbidv 3197	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑠 → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) ↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑠 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)))
243	237, 242	elab 3630	. . . . . . . . . . . . . 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 3569	. . . . . . . . . . 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 28074	. . . . . . . . . . . . . . . . . . . . . 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 28111	. . . . . . . . . . . . . . . . . . . . 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 28053	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 -s 𝑥𝐿) ·s 1s ) = (𝐴 -s 𝑥𝐿))
261	259, 260	breqtrd 5115	. . . . . . . . . . . . . . . . . . 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 28099	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (( -us ‘(𝑥𝐿 -s 𝐴)) ·s (𝐴 ·s 𝑦𝐿)) = ( -us ‘((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))))
264	200	oveq1d 7361	. . . . . . . . . . . . . . . . . . . . 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 2768	. . . . . . . . . . . . . . . . . . 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 5121	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( -us ‘((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))) <s ( -us ‘(𝑥𝐿 -s 𝐴)))
269	262, 254	mulscld 28074	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)) ∈ No )
270	262, 269	sltnegd 27989	. . . . . . . . . . . . . . . . . 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 28030	. . . . . . . . . . . . . . . . 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 28082	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( 1s ·s 𝑥𝐿) = 𝑥𝐿)
276	262, 253	mulscld 28074	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿) ∈ No )
277	252, 255, 276	addsdid 28095	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))) = ((𝐴 ·s 1s ) +s (𝐴 ·s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))))
278	252	mulsridd 28053	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s 1s ) = 𝐴)
279	252, 262, 253	muls12d 28120	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) = ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)))
280	278, 279	oveq12d 7364	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 ·s 1s ) +s (𝐴 ·s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))) = (𝐴 +s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))))
281	277, 280	eqtrd 2766	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))) = (𝐴 +s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))))
282	274, 275, 281	3brtr4d 5121	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( 1s ·s 𝑥𝐿) <s (𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))))
283	255, 276	addscld 27923	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) ∈ No )
284	252, 283	mulscld 28074	. . . . . . . . . . . . . . . 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 28140	. . . . . . . . . . . . . . 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 28142	. . . . . . . . . . . . . 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 5115	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 1s <s (𝐴 ·s (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)))
292		oveq2 7354	. . . . . . . . . . . . . 14 ⊢ (𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) → (𝐴 ·s 𝑠) = (𝐴 ·s (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)))
293	292	breq2d 5101	. . . . . . . . . . . . 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 3189	. . . . . . . . . . 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 28053	. . . . . . . . . . . . . . . . . 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 28074	. . . . . . . . . . . . . . . . . . . 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 28111	. . . . . . . . . . . . . . . . . . 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 5113	. . . . . . . . . . . . . . . . 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 28074	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)) ∈ No )
309	307, 300, 308	sltsubadd2d 28030	. . . . . . . . . . . . . . . . 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 28082	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( 1s ·s 𝑥𝑅) = 𝑥𝑅)
312	296, 301	mulscld 28074	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅) ∈ No )
313	300, 299, 312	addsdid 28095	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))) = ((𝐴 ·s 1s ) +s (𝐴 ·s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))))
314	300	mulsridd 28053	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s 1s ) = 𝐴)
315	300, 296, 301	muls12d 28120	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) = ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)))
316	314, 315	oveq12d 7364	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝐴 ·s 1s ) +s (𝐴 ·s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))) = (𝐴 +s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))))
317	313, 316	eqtrd 2766	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))) = (𝐴 +s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))))
318	310, 311, 317	3brtr4d 5121	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( 1s ·s 𝑥𝑅) <s (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))))
319	299, 312	addscld 27923	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) ∈ No )
320	300, 319	mulscld 28074	. . . . . . . . . . . . . . . 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 28140	. . . . . . . . . . . . . . 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 28142	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))) /su 𝑥𝑅) = (𝐴 ·s (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)))
327	324, 326	breqtrd 5115	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 1s <s (𝐴 ·s (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)))
328		oveq2 7354	. . . . . . . . . . . . . 14 ⊢ (𝑠 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) → (𝐴 ·s 𝑠) = (𝐴 ·s (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)))
329	328	breq2d 5101	. . . . . . . . . . . . 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 3189	. . . . . . . . . . 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 3123	. . . . . . 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 7826	. 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 1541   ∈ wcel 2111  {cab 2709   ≠ wne 2928  ∀wral 3047  ∃wrex 3056  {crab 3395  Vcvv 3436  ⦋csb 3845   ∪ cun 3895   ⊆ wss 3897  ∅c0 4280  {csn 4573  ⟨cop 4579   class class class wbr 5089   ↦ cmpt 5170   ∘ ccom 5618  suc csuc 6308  ‘cfv 6481  (class class class)co 7346  ωcom 7796  1^st c1st 7919  2^nd c2nd 7920  reccrdg 8328   No csur 27578   <s cslt 27579   0_s c0s 27766   1_s c1s 27767   L cleft 27786   R cright 27787   +_s cadds 27902   -u_s cnegs 27961   -_s csubs 27962   ·_s cmuls 28045   /_su cdivs 28126

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-rep 5215  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rmo 3346  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-tp 4578  df-op 4580  df-ot 4582  df-uni 4857  df-int 4896  df-iun 4941  df-br 5090  df-opab 5152  df-mpt 5171  df-tr 5197  df-id 5509  df-eprel 5514  df-po 5522  df-so 5523  df-fr 5567  df-se 5568  df-we 5569  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-pred 6248  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-riota 7303  df-ov 7349  df-oprab 7350  df-mpo 7351  df-om 7797  df-1st 7921  df-2nd 7922  df-frecs 8211  df-wrecs 8242  df-recs 8291  df-rdg 8329  df-1o 8385  df-2o 8386  df-nadd 8581  df-no 27581  df-slt 27582  df-bday 27583  df-sle 27684  df-sslt 27721  df-scut 27723  df-0s 27768  df-1s 27769  df-made 27788  df-old 27789  df-left 27791  df-right 27792  df-norec 27881  df-norec2 27892  df-adds 27903  df-negs 27963  df-subs 27964  df-muls 28046  df-divs 28127

This theorem is referenced by:  precsexlem10  28154  precsexlem11  28155