Theorem precsexlem9 28315

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 6867	. . . . . 6 ⊢ (𝑖 = ∅ → (𝐿‘𝑖) = (𝐿‘∅))
2	1	raleqdv 3321	. . . . 5 ⊢ (𝑖 = ∅ → (∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ↔ ∀𝑏 ∈ (𝐿‘∅)(𝐴 ·s 𝑏) <s 1s ))
3		fveq2 6867	. . . . . 6 ⊢ (𝑖 = ∅ → (𝑅‘𝑖) = (𝑅‘∅))
4	3	raleqdv 3321	. . . . 5 ⊢ (𝑖 = ∅ → (∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐) ↔ ∀𝑐 ∈ (𝑅‘∅) 1s <s (𝐴 ·s 𝑐)))
5	2, 4	anbi12d 641	. . . 4 ⊢ (𝑖 = ∅ → ((∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐)) ↔ (∀𝑏 ∈ (𝐿‘∅)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘∅) 1s <s (𝐴 ·s 𝑐))))
6	5	imbi2d 342	. . 3 ⊢ (𝑖 = ∅ → ((𝜑 → (∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐))) ↔ (𝜑 → (∀𝑏 ∈ (𝐿‘∅)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘∅) 1s <s (𝐴 ·s 𝑐)))))
7		fveq2 6867	. . . . . 6 ⊢ (𝑖 = 𝑗 → (𝐿‘𝑖) = (𝐿‘𝑗))
8	7	raleqdv 3321	. . . . 5 ⊢ (𝑖 = 𝑗 → (∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ↔ ∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ))
9		fveq2 6867	. . . . . 6 ⊢ (𝑖 = 𝑗 → (𝑅‘𝑖) = (𝑅‘𝑗))
10	9	raleqdv 3321	. . . . 5 ⊢ (𝑖 = 𝑗 → (∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐) ↔ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐)))
11	8, 10	anbi12d 641	. . . 4 ⊢ (𝑖 = 𝑗 → ((∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐)) ↔ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))))
12	11	imbi2d 342	. . 3 ⊢ (𝑖 = 𝑗 → ((𝜑 → (∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐))) ↔ (𝜑 → (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐)))))
13		fveq2 6867	. . . . . . 7 ⊢ (𝑖 = suc 𝑗 → (𝐿‘𝑖) = (𝐿‘suc 𝑗))
14	13	raleqdv 3321	. . . . . 6 ⊢ (𝑖 = suc 𝑗 → (∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ↔ ∀𝑏 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑏) <s 1s ))
15		fveq2 6867	. . . . . . 7 ⊢ (𝑖 = suc 𝑗 → (𝑅‘𝑖) = (𝑅‘suc 𝑗))
16	15	raleqdv 3321	. . . . . 6 ⊢ (𝑖 = suc 𝑗 → (∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐) ↔ ∀𝑐 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑐)))
17	14, 16	anbi12d 641	. . . . 5 ⊢ (𝑖 = suc 𝑗 → ((∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐)) ↔ (∀𝑏 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑐))))
18		oveq2 7404	. . . . . . . 8 ⊢ (𝑏 = 𝑟 → (𝐴 ·s 𝑏) = (𝐴 ·s 𝑟))
19	18	breq1d 5111	. . . . . . 7 ⊢ (𝑏 = 𝑟 → ((𝐴 ·s 𝑏) <s 1s ↔ (𝐴 ·s 𝑟) <s 1s ))
20	19	cbvralvw 3241	. . . . . 6 ⊢ (∀𝑏 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑏) <s 1s ↔ ∀𝑟 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑟) <s 1s )
21		oveq2 7404	. . . . . . . 8 ⊢ (𝑐 = 𝑠 → (𝐴 ·s 𝑐) = (𝐴 ·s 𝑠))
22	21	breq2d 5113	. . . . . . 7 ⊢ (𝑐 = 𝑠 → ( 1s <s (𝐴 ·s 𝑐) ↔ 1s <s (𝐴 ·s 𝑠)))
23	22	cbvralvw 3241	. . . . . 6 ⊢ (∀𝑐 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑐) ↔ ∀𝑠 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑠))
24	20, 23	anbi12i 637	. . . . 5 ⊢ ((∀𝑏 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑐)) ↔ (∀𝑟 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑟) <s 1s ∧ ∀𝑠 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑠)))
25	17, 24	bitrdi 289	. . . 4 ⊢ (𝑖 = suc 𝑗 → ((∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐)) ↔ (∀𝑟 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑟) <s 1s ∧ ∀𝑠 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑠))))
26	25	imbi2d 342	. . 3 ⊢ (𝑖 = suc 𝑗 → ((𝜑 → (∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐))) ↔ (𝜑 → (∀𝑟 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑟) <s 1s ∧ ∀𝑠 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑠)))))
27		fveq2 6867	. . . . . 6 ⊢ (𝑖 = 𝐼 → (𝐿‘𝑖) = (𝐿‘𝐼))
28	27	raleqdv 3321	. . . . 5 ⊢ (𝑖 = 𝐼 → (∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ↔ ∀𝑏 ∈ (𝐿‘𝐼)(𝐴 ·s 𝑏) <s 1s ))
29		fveq2 6867	. . . . . 6 ⊢ (𝑖 = 𝐼 → (𝑅‘𝑖) = (𝑅‘𝐼))
30	29	raleqdv 3321	. . . . 5 ⊢ (𝑖 = 𝐼 → (∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐) ↔ ∀𝑐 ∈ (𝑅‘𝐼) 1s <s (𝐴 ·s 𝑐)))
31	28, 30	anbi12d 641	. . . 4 ⊢ (𝑖 = 𝐼 → ((∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐)) ↔ (∀𝑏 ∈ (𝐿‘𝐼)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝐼) 1s <s (𝐴 ·s 𝑐))))
32	31	imbi2d 342	. . 3 ⊢ (𝑖 = 𝐼 → ((𝜑 → (∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐))) ↔ (𝜑 → (∀𝑏 ∈ (𝐿‘𝐼)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝐼) 1s <s (𝐴 ·s 𝑐)))))
33		precsexlem.4	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ No )
34		muls01 28212	. . . . . . 7 ⊢ (𝐴 ∈ No → (𝐴 ·s 0s ) = 0s )
35	33, 34	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐴 ·s 0s ) = 0s )
36		0lt1s 27912	. . . . . 6 ⊢ 0s <s 1s
37	35, 36	eqbrtrdi 5140	. . . . 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 28307	. . . . . . 7 ⊢ (𝐿‘∅) = { 0s }
42	41	raleqi 3319	. . . . . 6 ⊢ (∀𝑏 ∈ (𝐿‘∅)(𝐴 ·s 𝑏) <s 1s ↔ ∀𝑏 ∈ { 0s } (𝐴 ·s 𝑏) <s 1s )
43		0no 27909	. . . . . . . 8 ⊢ 0s ∈ No
44	43	elexi 3477	. . . . . . 7 ⊢ 0s ∈ V
45		oveq2 7404	. . . . . . . 8 ⊢ (𝑏 = 0s → (𝐴 ·s 𝑏) = (𝐴 ·s 0s ))
46	45	breq1d 5111	. . . . . . 7 ⊢ (𝑏 = 0s → ((𝐴 ·s 𝑏) <s 1s ↔ (𝐴 ·s 0s ) <s 1s ))
47	44, 46	ralsn 4641	. . . . . 6 ⊢ (∀𝑏 ∈ { 0s } (𝐴 ·s 𝑏) <s 1s ↔ (𝐴 ·s 0s ) <s 1s )
48	42, 47	bitri 277	. . . . 5 ⊢ (∀𝑏 ∈ (𝐿‘∅)(𝐴 ·s 𝑏) <s 1s ↔ (𝐴 ·s 0s ) <s 1s )
49	37, 48	sylibr 236	. . . 4 ⊢ (𝜑 → ∀𝑏 ∈ (𝐿‘∅)(𝐴 ·s 𝑏) <s 1s )
50		ral0 4453	. . . . 5 ⊢ ∀𝑐 ∈ ∅ 1s <s (𝐴 ·s 𝑐)
51	38, 39, 40	precsexlem2 28308	. . . . . 6 ⊢ (𝑅‘∅) = ∅
52	51	raleqi 3319	. . . . 5 ⊢ (∀𝑐 ∈ (𝑅‘∅) 1s <s (𝐴 ·s 𝑐) ↔ ∀𝑐 ∈ ∅ 1s <s (𝐴 ·s 𝑐))
53	50, 52	mpbir 233	. . . 4 ⊢ ∀𝑐 ∈ (𝑅‘∅) 1s <s (𝐴 ·s 𝑐)
54	49, 53	jctir 528	. . 3 ⊢ (𝜑 → (∀𝑏 ∈ (𝐿‘∅)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘∅) 1s <s (𝐴 ·s 𝑐)))
55	38, 39, 40	precsexlem4 28310	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ω → (𝐿‘suc 𝑗) = ((𝐿‘𝑗) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})))
56	55	3ad2ant2 1148	. . . . . . . . . . 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 2849	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝑟 ∈ (𝐿‘suc 𝑗) ↔ 𝑟 ∈ ((𝐿‘𝑗) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)}))))
58		elun 4107	. . . . . . . . . . 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 4107	. . . . . . . . . . . . 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 3459	. . . . . . . . . . . . . . 15 ⊢ 𝑟 ∈ V
61		eqeq1 2767	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑟 → (𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) ↔ 𝑟 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)))
62	61	2rexbidv 3228	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑟 → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) ↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑟 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)))
63	60, 62	elab 3639	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑟 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅))
64		eqeq1 2767	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑟 → (𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) ↔ 𝑟 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)))
65	64	2rexbidv 3228	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑟 → (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) ↔ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑟 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)))
66	60, 65	elab 3639	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)} ↔ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑟 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿))
67	63, 66	orbi12i 925	. . . . . . . . . . . . 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 277	. . . . . . . . . . . 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 923	. . . . . . . . . . 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 277	. . . . . . . . . 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 289	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝑟 ∈ (𝐿‘suc 𝑗) ↔ (𝑟 ∈ (𝐿‘𝑗) ∨ (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑟 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) ∨ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑟 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)))))
72		simp3l 1216	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → ∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s )
73	19	rspccv 3579	. . . . . . . . . . 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 1147	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → 𝐴 ∈ No )
76	75	adantr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝐴 ∈ No )
77		1no 27910	. . . . . . . . . . . . . . . . 17 ⊢ 1s ∈ No
78	77	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 1s ∈ No )
79		rightno 27978	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥𝑅 ∈ ( R ‘𝐴) → 𝑥𝑅 ∈ No )
80	79	adantl 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 𝑥𝑅 ∈ No )
81	75	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 𝐴 ∈ No )
82	80, 81	subscld 28163	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → (𝑥𝑅 -s 𝐴) ∈ No )
83	82	adantrr 727	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝑥𝑅 -s 𝐴) ∈ No )
84		precsexlem.5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 0s <s 𝐴)
85		precsexlem.6	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ))
86	38, 39, 40, 33, 84, 85	precsexlem8 28314	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ ω) → ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No ))
87	86	simpld 498	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ω) → (𝐿‘𝑗) ⊆ No )
88	87	3adant3 1146	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝐿‘𝑗) ⊆ No )
89	88	sselda 3937	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗)) → 𝑦𝐿 ∈ No )
90	89	adantrl 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑦𝐿 ∈ No )
91	83, 90	mulscld 28235	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿) ∈ No )
92	78, 91	addscld 28080	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) ∈ No )
93	80	adantrr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑥𝑅 ∈ No )
94	43	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 0s ∈ No )
95	84	3ad2ant1 1147	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → 0s <s 𝐴)
96	95	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 0s <s 𝐴)
97		rightgt 27954	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝑅 ∈ ( R ‘𝐴) → 𝐴 <s 𝑥𝑅)
98	97	adantl 485	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 𝐴 <s 𝑥𝑅)
99	94, 81, 80, 96, 98	ltstrd 27834	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 0s <s 𝑥𝑅)
100	99	gt0ne0sd 27919	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 𝑥𝑅 ≠ 0s )
101	100	adantrr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑥𝑅 ≠ 0s )
102		breq2 5105	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝑂 = 𝑥𝑅 → ( 0s <s 𝑥𝑂 ↔ 0s <s 𝑥𝑅))
103		oveq1 7403	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥𝑂 = 𝑥𝑅 → (𝑥𝑂 ·s 𝑦) = (𝑥𝑅 ·s 𝑦))
104	103	eqeq1d 2765	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥𝑂 = 𝑥𝑅 → ((𝑥𝑂 ·s 𝑦) = 1s ↔ (𝑥𝑅 ·s 𝑦) = 1s ))
105	104	rexbidv 3187	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝑂 = 𝑥𝑅 → (∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ↔ ∃𝑦 ∈ No (𝑥𝑅 ·s 𝑦) = 1s ))
106	102, 105	imbi12d 346	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥𝑂 = 𝑥𝑅 → (( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ) ↔ ( 0s <s 𝑥𝑅 → ∃𝑦 ∈ No (𝑥𝑅 ·s 𝑦) = 1s )))
107	85	3ad2ant1 1147	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ))
108	107	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ))
109		elun2 4136	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝑅 ∈ ( R ‘𝐴) → 𝑥𝑅 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))
110	109	adantl 485	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 𝑥𝑅 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))
111	106, 108, 110	rspcdva 3583	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → ( 0s <s 𝑥𝑅 → ∃𝑦 ∈ No (𝑥𝑅 ·s 𝑦) = 1s ))
112	99, 111	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → ∃𝑦 ∈ No (𝑥𝑅 ·s 𝑦) = 1s )
113	112	adantrr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ∃𝑦 ∈ No (𝑥𝑅 ·s 𝑦) = 1s )
114	76, 92, 93, 101, 113	divsasswd 28303	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) /su 𝑥𝑅) = (𝐴 ·s (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)))
115		oveq2 7404	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = 𝑦𝐿 → (𝐴 ·s 𝑏) = (𝐴 ·s 𝑦𝐿))
116	115	breq1d 5111	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = 𝑦𝐿 → ((𝐴 ·s 𝑏) <s 1s ↔ (𝐴 ·s 𝑦𝐿) <s 1s ))
117	116	rspccva 3581	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ 𝑦𝐿 ∈ (𝐿‘𝑗)) → (𝐴 ·s 𝑦𝐿) <s 1s )
118	72, 117	sylan 589	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗)) → (𝐴 ·s 𝑦𝐿) <s 1s )
119	118	adantrl 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s 𝑦𝐿) <s 1s )
120	76, 90	mulscld 28235	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s 𝑦𝐿) ∈ No )
121	81, 80	posdifsd 28198	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → (𝐴 <s 𝑥𝑅 ↔ 0s <s (𝑥𝑅 -s 𝐴)))
122	98, 121	mpbid 234	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 0s <s (𝑥𝑅 -s 𝐴))
123	122	adantrr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 0s <s (𝑥𝑅 -s 𝐴))
124	120, 78, 83, 123	ltmuls2d 28272	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 ·s 𝑦𝐿) <s 1s ↔ ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)) <s ((𝑥𝑅 -s 𝐴) ·s 1s )))
125	119, 124	mpbid 234	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)) <s ((𝑥𝑅 -s 𝐴) ·s 1s ))
126	83	mulsridd 28214	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s 1s ) = (𝑥𝑅 -s 𝐴))
127	125, 126	breqtrd 5127	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)) <s (𝑥𝑅 -s 𝐴))
128	83, 120	mulscld 28235	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)) ∈ No )
129	76, 128, 93	ltaddsubs2d 28192	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 +s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))) <s 𝑥𝑅 ↔ ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)) <s (𝑥𝑅 -s 𝐴)))
130	127, 129	mpbird 259	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 +s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))) <s 𝑥𝑅)
131	76, 78, 91	addsdid 28256	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) = ((𝐴 ·s 1s ) +s (𝐴 ·s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))))
132	76	mulsridd 28214	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s 1s ) = 𝐴)
133	76, 83, 90	muls12d 28281	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) = ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)))
134	132, 133	oveq12d 7414	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 ·s 1s ) +s (𝐴 ·s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) = (𝐴 +s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))))
135	131, 134	eqtrd 2798	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) = (𝐴 +s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))))
136	93	mulslidd 28243	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( 1s ·s 𝑥𝑅) = 𝑥𝑅)
137	130, 135, 136	3brtr4d 5133	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) <s ( 1s ·s 𝑥𝑅))
138	76, 92	mulscld 28235	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) ∈ No )
139	99	adantrr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 0s <s 𝑥𝑅)
140	138, 78, 93, 139, 113	ltdivmuls2wd 28300	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (((𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) /su 𝑥𝑅) <s 1s ↔ (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) <s ( 1s ·s 𝑥𝑅)))
141	137, 140	mpbird 259	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) /su 𝑥𝑅) <s 1s )
142	114, 141	eqbrtrrd 5125	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)) <s 1s )
143		oveq2 7404	. . . . . . . . . . . . . 14 ⊢ (𝑟 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) → (𝐴 ·s 𝑟) = (𝐴 ·s (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)))
144	143	breq1d 5111	. . . . . . . . . . . . 13 ⊢ (𝑟 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) → ((𝐴 ·s 𝑟) <s 1s ↔ (𝐴 ·s (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)) <s 1s ))
145	142, 144	syl5ibrcom 249	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝑟 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) → (𝐴 ·s 𝑟) <s 1s ))
146	145	rexlimdvva 3220	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑟 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) → (𝐴 ·s 𝑟) <s 1s ))
147	75	adantr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝐴 ∈ No )
148	77	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 1s ∈ No )
149		elrabi 3647	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} → 𝑥𝐿 ∈ ( L ‘𝐴))
150	149	adantl 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → 𝑥𝐿 ∈ ( L ‘𝐴))
151	150	leftnod 27980	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → 𝑥𝐿 ∈ No )
152	75	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → 𝐴 ∈ No )
153	151, 152	subscld 28163	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → (𝑥𝐿 -s 𝐴) ∈ No )
154	153	adantrr 727	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝑥𝐿 -s 𝐴) ∈ No )
155	86	simprd 499	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ω) → (𝑅‘𝑗) ⊆ No )
156	155	3adant3 1146	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝑅‘𝑗) ⊆ No )
157	156	sselda 3937	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗)) → 𝑦𝑅 ∈ No )
158	157	adantrl 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑦𝑅 ∈ No )
159	154, 158	mulscld 28235	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅) ∈ No )
160	148, 159	addscld 28080	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) ∈ No )
161	151	adantrr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑥𝐿 ∈ No )
162		breq2 5105	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑥𝐿 → ( 0s <s 𝑥 ↔ 0s <s 𝑥𝐿))
163	162	elrab 3651	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ↔ (𝑥𝐿 ∈ ( L ‘𝐴) ∧ 0s <s 𝑥𝐿))
164	163	simprbi 501	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} → 0s <s 𝑥𝐿)
165	164	adantl 485	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → 0s <s 𝑥𝐿)
166	165	gt0ne0sd 27919	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → 𝑥𝐿 ≠ 0s )
167	166	adantrr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑥𝐿 ≠ 0s )
168		breq2 5105	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝑂 = 𝑥𝐿 → ( 0s <s 𝑥𝑂 ↔ 0s <s 𝑥𝐿))
169		oveq1 7403	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥𝑂 = 𝑥𝐿 → (𝑥𝑂 ·s 𝑦) = (𝑥𝐿 ·s 𝑦))
170	169	eqeq1d 2765	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥𝑂 = 𝑥𝐿 → ((𝑥𝑂 ·s 𝑦) = 1s ↔ (𝑥𝐿 ·s 𝑦) = 1s ))
171	170	rexbidv 3187	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝑂 = 𝑥𝐿 → (∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ↔ ∃𝑦 ∈ No (𝑥𝐿 ·s 𝑦) = 1s ))
172	168, 171	imbi12d 346	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥𝑂 = 𝑥𝐿 → (( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ) ↔ ( 0s <s 𝑥𝐿 → ∃𝑦 ∈ No (𝑥𝐿 ·s 𝑦) = 1s )))
173	107	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ))
174		elun1 4135	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝐿 ∈ ( L ‘𝐴) → 𝑥𝐿 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))
175	150, 174	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → 𝑥𝐿 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))
176	172, 173, 175	rspcdva 3583	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → ( 0s <s 𝑥𝐿 → ∃𝑦 ∈ No (𝑥𝐿 ·s 𝑦) = 1s ))
177	165, 176	mpd 15	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → ∃𝑦 ∈ No (𝑥𝐿 ·s 𝑦) = 1s )
178	177	adantrr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ∃𝑦 ∈ No (𝑥𝐿 ·s 𝑦) = 1s )
179	147, 160, 161, 167, 178	divsasswd 28303	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))) /su 𝑥𝐿) = (𝐴 ·s (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)))
180	152, 151	subscld 28163	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → (𝐴 -s 𝑥𝐿) ∈ No )
181	180	adantrr 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 -s 𝑥𝐿) ∈ No )
182	181	mulsridd 28214	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝐴 -s 𝑥𝐿) ·s 1s ) = (𝐴 -s 𝑥𝐿))
183		simp3r 1217	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))
184		oveq2 7404	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = 𝑦𝑅 → (𝐴 ·s 𝑐) = (𝐴 ·s 𝑦𝑅))
185	184	breq2d 5113	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = 𝑦𝑅 → ( 1s <s (𝐴 ·s 𝑐) ↔ 1s <s (𝐴 ·s 𝑦𝑅)))
186	185	rspccva 3581	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗)) → 1s <s (𝐴 ·s 𝑦𝑅))
187	183, 186	sylan 589	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗)) → 1s <s (𝐴 ·s 𝑦𝑅))
188	187	adantrl 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 1s <s (𝐴 ·s 𝑦𝑅))
189	147, 158	mulscld 28235	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s 𝑦𝑅) ∈ No )
190		leftlt 27953	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥𝐿 ∈ ( L ‘𝐴) → 𝑥𝐿 <s 𝐴)
191	150, 190	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → 𝑥𝐿 <s 𝐴)
192	151, 152	posdifsd 28198	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → (𝑥𝐿 <s 𝐴 ↔ 0s <s (𝐴 -s 𝑥𝐿)))
193	191, 192	mpbid 234	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → 0s <s (𝐴 -s 𝑥𝐿))
194	193	adantrr 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 0s <s (𝐴 -s 𝑥𝐿))
195	148, 189, 181, 194	ltmuls2d 28272	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( 1s <s (𝐴 ·s 𝑦𝑅) ↔ ((𝐴 -s 𝑥𝐿) ·s 1s ) <s ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝑅))))
196	188, 195	mpbid 234	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝐴 -s 𝑥𝐿) ·s 1s ) <s ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝑅)))
197	182, 196	eqbrtrrd 5125	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 -s 𝑥𝐿) <s ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝑅)))
198	151, 152	negsubsdi2d 28180	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → ( -us ‘(𝑥𝐿 -s 𝐴)) = (𝐴 -s 𝑥𝐿))
199	198	adantrr 727	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( -us ‘(𝑥𝐿 -s 𝐴)) = (𝐴 -s 𝑥𝐿))
200	154, 189	mulnegs1d 28260	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (( -us ‘(𝑥𝐿 -s 𝐴)) ·s (𝐴 ·s 𝑦𝑅)) = ( -us ‘((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))))
201	198	oveq1d 7411	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → (( -us ‘(𝑥𝐿 -s 𝐴)) ·s (𝐴 ·s 𝑦𝑅)) = ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝑅)))
202	201	adantrr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (( -us ‘(𝑥𝐿 -s 𝐴)) ·s (𝐴 ·s 𝑦𝑅)) = ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝑅)))
203	200, 202	eqtr3d 2800	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( -us ‘((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))) = ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝑅)))
204	197, 199, 203	3brtr4d 5133	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( -us ‘(𝑥𝐿 -s 𝐴)) <s ( -us ‘((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))))
205	154, 189	mulscld 28235	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)) ∈ No )
206	205, 154	ltnegsd 28147	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)) <s (𝑥𝐿 -s 𝐴) ↔ ( -us ‘(𝑥𝐿 -s 𝐴)) <s ( -us ‘((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)))))
207	204, 206	mpbird 259	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)) <s (𝑥𝐿 -s 𝐴))
208	147, 205, 161	ltaddsubs2d 28192	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝐴 +s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))) <s 𝑥𝐿 ↔ ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)) <s (𝑥𝐿 -s 𝐴)))
209	207, 208	mpbird 259	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 +s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))) <s 𝑥𝐿)
210	147, 148, 159	addsdid 28256	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))) = ((𝐴 ·s 1s ) +s (𝐴 ·s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))))
211	147	mulsridd 28214	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s 1s ) = 𝐴)
212	147, 154, 158	muls12d 28281	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) = ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)))
213	211, 212	oveq12d 7414	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝐴 ·s 1s ) +s (𝐴 ·s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))) = (𝐴 +s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))))
214	210, 213	eqtrd 2798	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))) = (𝐴 +s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))))
215	161	mulsridd 28214	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝑥𝐿 ·s 1s ) = 𝑥𝐿)
216	209, 214, 215	3brtr4d 5133	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))) <s (𝑥𝐿 ·s 1s ))
217	147, 160	mulscld 28235	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))) ∈ No )
218	165	adantrr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 0s <s 𝑥𝐿)
219	217, 148, 161, 218, 178	ltdivmulswd 28299	. . . . . . . . . . . . . . 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 )))
220	216, 219	mpbird 259	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))) /su 𝑥𝐿) <s 1s )
221	179, 220	eqbrtrrd 5125	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)) <s 1s )
222		oveq2 7404	. . . . . . . . . . . . . 14 ⊢ (𝑟 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) → (𝐴 ·s 𝑟) = (𝐴 ·s (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)))
223	222	breq1d 5111	. . . . . . . . . . . . 13 ⊢ (𝑟 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) → ((𝐴 ·s 𝑟) <s 1s ↔ (𝐴 ·s (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)) <s 1s ))
224	221, 223	syl5ibrcom 249	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝑟 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) → (𝐴 ·s 𝑟) <s 1s ))
225	224	rexlimdvva 3220	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑟 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) → (𝐴 ·s 𝑟) <s 1s ))
226	146, 225	jaod 870	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → ((∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑟 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) ∨ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑟 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)) → (𝐴 ·s 𝑟) <s 1s ))
227	74, 226	jaod 870	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → ((𝑟 ∈ (𝐿‘𝑗) ∨ (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑟 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) ∨ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑟 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿))) → (𝐴 ·s 𝑟) <s 1s ))
228	71, 227	sylbid 242	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝑟 ∈ (𝐿‘suc 𝑗) → (𝐴 ·s 𝑟) <s 1s ))
229	228	ralrimiv 3154	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → ∀𝑟 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑟) <s 1s )
230	38, 39, 40	precsexlem5 28311	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ω → (𝑅‘suc 𝑗) = ((𝑅‘𝑗) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)})))
231	230	3ad2ant2 1148	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝑅‘suc 𝑗) = ((𝑅‘𝑗) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)})))
232	231	eleq2d 2849	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝑠 ∈ (𝑅‘suc 𝑗) ↔ 𝑠 ∈ ((𝑅‘𝑗) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))))
233		elun 4107	. . . . . . . . . . 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 𝑥𝑅)})))
234		elun 4107	. . . . . . . . . . . . 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 𝑥𝑅)}))
235		vex 3459	. . . . . . . . . . . . . . 15 ⊢ 𝑠 ∈ V
236		eqeq1 2767	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑠 → (𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) ↔ 𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)))
237	236	2rexbidv 3228	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑠 → (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) ↔ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)))
238	235, 237	elab 3639	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ↔ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿))
239		eqeq1 2767	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑠 → (𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) ↔ 𝑠 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)))
240	239	2rexbidv 3228	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑠 → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) ↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑠 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)))
241	235, 240	elab 3639	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)} ↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑠 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅))
242	238, 241	orbi12i 925	. . . . . . . . . . . . 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 𝑥𝑅)))
243	234, 242	bitri 277	. . . . . . . . . . . 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 𝑥𝑅)))
244	243	orbi2i 923	. . . . . . . . . . 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 𝑥𝑅))))
245	233, 244	bitri 277	. . . . . . . . . 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 𝑥𝑅))))
246	232, 245	bitrdi 289	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝑠 ∈ (𝑅‘suc 𝑗) ↔ (𝑠 ∈ (𝑅‘𝑗) ∨ (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) ∨ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑠 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)))))
247	22	rspccv 3579	. . . . . . . . . . 11 ⊢ (∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐) → (𝑠 ∈ (𝑅‘𝑗) → 1s <s (𝐴 ·s 𝑠)))
248	183, 247	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝑠 ∈ (𝑅‘𝑗) → 1s <s (𝐴 ·s 𝑠)))
249	118	adantrl 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s 𝑦𝐿) <s 1s )
250	75	adantr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝐴 ∈ No )
251	89	adantrl 726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑦𝐿 ∈ No )
252	250, 251	mulscld 28235	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s 𝑦𝐿) ∈ No )
253	77	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 1s ∈ No )
254	180	adantrr 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 -s 𝑥𝐿) ∈ No )
255	193	adantrr 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 0s <s (𝐴 -s 𝑥𝐿))
256	252, 253, 254, 255	ltmuls2d 28272	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 ·s 𝑦𝐿) <s 1s ↔ ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝐿)) <s ((𝐴 -s 𝑥𝐿) ·s 1s )))
257	249, 256	mpbid 234	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝐿)) <s ((𝐴 -s 𝑥𝐿) ·s 1s ))
258	254	mulsridd 28214	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 -s 𝑥𝐿) ·s 1s ) = (𝐴 -s 𝑥𝐿))
259	257, 258	breqtrd 5127	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝐿)) <s (𝐴 -s 𝑥𝐿))
260	153	adantrr 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝑥𝐿 -s 𝐴) ∈ No )
261	260, 252	mulnegs1d 28260	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (( -us ‘(𝑥𝐿 -s 𝐴)) ·s (𝐴 ·s 𝑦𝐿)) = ( -us ‘((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))))
262	198	oveq1d 7411	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → (( -us ‘(𝑥𝐿 -s 𝐴)) ·s (𝐴 ·s 𝑦𝐿)) = ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝐿)))
263	262	adantrr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (( -us ‘(𝑥𝐿 -s 𝐴)) ·s (𝐴 ·s 𝑦𝐿)) = ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝐿)))
264	261, 263	eqtr3d 2800	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( -us ‘((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))) = ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝐿)))
265	198	adantrr 727	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( -us ‘(𝑥𝐿 -s 𝐴)) = (𝐴 -s 𝑥𝐿))
266	259, 264, 265	3brtr4d 5133	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( -us ‘((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))) <s ( -us ‘(𝑥𝐿 -s 𝐴)))
267	260, 252	mulscld 28235	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)) ∈ No )
268	260, 267	ltnegsd 28147	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝐿 -s 𝐴) <s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)) ↔ ( -us ‘((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))) <s ( -us ‘(𝑥𝐿 -s 𝐴))))
269	266, 268	mpbird 259	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝑥𝐿 -s 𝐴) <s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)))
270	151	adantrr 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑥𝐿 ∈ No )
271	270, 250, 267	ltsubadds2d 28190	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝐿 -s 𝐴) <s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)) ↔ 𝑥𝐿 <s (𝐴 +s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)))))
272	269, 271	mpbid 234	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑥𝐿 <s (𝐴 +s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))))
273	270	mulslidd 28243	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( 1s ·s 𝑥𝐿) = 𝑥𝐿)
274	260, 251	mulscld 28235	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿) ∈ No )
275	250, 253, 274	addsdid 28256	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))) = ((𝐴 ·s 1s ) +s (𝐴 ·s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))))
276	250	mulsridd 28214	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s 1s ) = 𝐴)
277	250, 260, 251	muls12d 28281	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) = ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)))
278	276, 277	oveq12d 7414	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 ·s 1s ) +s (𝐴 ·s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))) = (𝐴 +s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))))
279	275, 278	eqtrd 2798	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))) = (𝐴 +s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))))
280	272, 273, 279	3brtr4d 5133	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( 1s ·s 𝑥𝐿) <s (𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))))
281	253, 274	addscld 28080	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) ∈ No )
282	250, 281	mulscld 28235	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))) ∈ No )
283	165	adantrr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 0s <s 𝑥𝐿)
284	177	adantrr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ∃𝑦 ∈ No (𝑥𝐿 ·s 𝑦) = 1s )
285	253, 282, 270, 283, 284	ltmuldivswd 28301	. . . . . . . . . . . . . . 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 𝑥𝐿)))
286	280, 285	mpbid 234	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 1s <s ((𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))) /su 𝑥𝐿))
287	166	adantrr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑥𝐿 ≠ 0s )
288	250, 281, 270, 287, 284	divsasswd 28303	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))) /su 𝑥𝐿) = (𝐴 ·s (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)))
289	286, 288	breqtrd 5127	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 1s <s (𝐴 ·s (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)))
290		oveq2 7404	. . . . . . . . . . . . . 14 ⊢ (𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) → (𝐴 ·s 𝑠) = (𝐴 ·s (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)))
291	290	breq2d 5113	. . . . . . . . . . . . 13 ⊢ (𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) → ( 1s <s (𝐴 ·s 𝑠) ↔ 1s <s (𝐴 ·s (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿))))
292	289, 291	syl5ibrcom 249	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) → 1s <s (𝐴 ·s 𝑠)))
293	292	rexlimdvva 3220	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) → 1s <s (𝐴 ·s 𝑠)))
294	82	adantrr 727	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝑥𝑅 -s 𝐴) ∈ No )
295	294	mulsridd 28214	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s 1s ) = (𝑥𝑅 -s 𝐴))
296	187	adantrl 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 1s <s (𝐴 ·s 𝑦𝑅))
297	77	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 1s ∈ No )
298	75	adantr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝐴 ∈ No )
299	157	adantrl 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑦𝑅 ∈ No )
300	298, 299	mulscld 28235	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s 𝑦𝑅) ∈ No )
301	122	adantrr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 0s <s (𝑥𝑅 -s 𝐴))
302	297, 300, 294, 301	ltmuls2d 28272	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( 1s <s (𝐴 ·s 𝑦𝑅) ↔ ((𝑥𝑅 -s 𝐴) ·s 1s ) <s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))))
303	296, 302	mpbid 234	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s 1s ) <s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)))
304	295, 303	eqbrtrrd 5125	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝑥𝑅 -s 𝐴) <s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)))
305	80	adantrr 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑥𝑅 ∈ No )
306	294, 300	mulscld 28235	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)) ∈ No )
307	305, 298, 306	ltsubadds2d 28190	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝑥𝑅 -s 𝐴) <s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)) ↔ 𝑥𝑅 <s (𝐴 +s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)))))
308	304, 307	mpbid 234	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑥𝑅 <s (𝐴 +s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))))
309	305	mulslidd 28243	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( 1s ·s 𝑥𝑅) = 𝑥𝑅)
310	294, 299	mulscld 28235	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅) ∈ No )
311	298, 297, 310	addsdid 28256	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))) = ((𝐴 ·s 1s ) +s (𝐴 ·s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))))
312	298	mulsridd 28214	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s 1s ) = 𝐴)
313	298, 294, 299	muls12d 28281	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) = ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)))
314	312, 313	oveq12d 7414	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝐴 ·s 1s ) +s (𝐴 ·s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))) = (𝐴 +s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))))
315	311, 314	eqtrd 2798	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))) = (𝐴 +s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))))
316	308, 309, 315	3brtr4d 5133	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( 1s ·s 𝑥𝑅) <s (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))))
317	297, 310	addscld 28080	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) ∈ No )
318	298, 317	mulscld 28235	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))) ∈ No )
319	99	adantrr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 0s <s 𝑥𝑅)
320	112	adantrr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ∃𝑦 ∈ No (𝑥𝑅 ·s 𝑦) = 1s )
321	297, 318, 305, 319, 320	ltmuldivswd 28301	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (( 1s ·s 𝑥𝑅) <s (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))) ↔ 1s <s ((𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))) /su 𝑥𝑅)))
322	316, 321	mpbid 234	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 1s <s ((𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))) /su 𝑥𝑅))
323	100	adantrr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑥𝑅 ≠ 0s )
324	298, 317, 305, 323, 320	divsasswd 28303	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))) /su 𝑥𝑅) = (𝐴 ·s (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)))
325	322, 324	breqtrd 5127	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 1s <s (𝐴 ·s (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)))
326		oveq2 7404	. . . . . . . . . . . . . 14 ⊢ (𝑠 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) → (𝐴 ·s 𝑠) = (𝐴 ·s (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)))
327	326	breq2d 5113	. . . . . . . . . . . . 13 ⊢ (𝑠 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) → ( 1s <s (𝐴 ·s 𝑠) ↔ 1s <s (𝐴 ·s (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅))))
328	325, 327	syl5ibrcom 249	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝑠 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) → 1s <s (𝐴 ·s 𝑠)))
329	328	rexlimdvva 3220	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑠 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) → 1s <s (𝐴 ·s 𝑠)))
330	293, 329	jaod 870	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → ((∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) ∨ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑠 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)) → 1s <s (𝐴 ·s 𝑠)))
331	248, 330	jaod 870	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → ((𝑠 ∈ (𝑅‘𝑗) ∨ (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) ∨ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑠 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅))) → 1s <s (𝐴 ·s 𝑠)))
332	246, 331	sylbid 242	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝑠 ∈ (𝑅‘suc 𝑗) → 1s <s (𝐴 ·s 𝑠)))
333	332	ralrimiv 3154	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → ∀𝑠 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑠))
334	229, 333	jca 519	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (∀𝑟 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑟) <s 1s ∧ ∀𝑠 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑠)))
335	334	3exp 1133	. . . . 5 ⊢ (𝜑 → (𝑗 ∈ ω → ((∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐)) → (∀𝑟 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑟) <s 1s ∧ ∀𝑠 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑠)))))
336	335	com12 32	. . . 4 ⊢ (𝑗 ∈ ω → (𝜑 → ((∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐)) → (∀𝑟 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑟) <s 1s ∧ ∀𝑠 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑠)))))
337	336	a2d 29	. . 3 ⊢ (𝑗 ∈ ω → ((𝜑 → (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝜑 → (∀𝑟 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑟) <s 1s ∧ ∀𝑠 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑠)))))
338	6, 12, 26, 32, 54, 337	finds 7877	. 2 ⊢ (𝐼 ∈ ω → (𝜑 → (∀𝑏 ∈ (𝐿‘𝐼)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝐼) 1s <s (𝐴 ·s 𝑐))))
339	338	impcom 411	1 ⊢ ((𝜑 ∧ 𝐼 ∈ ω) → (∀𝑏 ∈ (𝐿‘𝐼)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝐼) 1s <s (𝐴 ·s 𝑐)))

Syntax hints:   → wi 4   ∧ wa 399   ∨ wo 858   ∧ w3a 1099   = wceq 1561   ∈ wcel 2143  {cab 2741   ≠ wne 2958  ∀wral 3077  ∃wrex 3087  {crab 3415  Vcvv 3455  ⦋csb 3853   ∪ cun 3903   ⊆ wss 3905  ∅c0 4286  {csn 4583  ⟨cop 4589   class class class wbr 5101   ↦ cmpt 5182   ∘ ccom 5652  suc csuc 6348  ‘cfv 6521  (class class class)co 7396  ωcom 7846  1^st c1st 7968  2^nd c2nd 7969  reccrdg 8380   No csur 27711   <s clts 27712   0_s c0s 27905   1_s c1s 27906   L cleft 27925   R cright 27926   +_s cadds 28059   -u_s cnegs 28119   -_s csubs 28120   ·_s cmuls 28206   /_su cdivs 28287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5228  ax-sep 5247  ax-nul 5257  ax-pow 5323  ax-pr 5391  ax-un 7718

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-nf 1805  df-sb 2092  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3078  df-rex 3088  df-rmo 3368  df-reu 3369  df-rab 3416  df-v 3457  df-sbc 3746  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-tp 4588  df-op 4590  df-ot 4592  df-uni 4867  df-int 4907  df-iun 4952  df-br 5102  df-opab 5164  df-mpt 5183  df-tr 5209  df-id 5543  df-eprel 5548  df-po 5556  df-so 5557  df-fr 5601  df-se 5602  df-we 5603  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-pred 6288  df-ord 6349  df-on 6350  df-lim 6351  df-suc 6352  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-riota 7353  df-ov 7399  df-oprab 7400  df-mpo 7401  df-om 7847  df-1st 7970  df-2nd 7971  df-frecs 8262  df-wrecs 8293  df-recs 8342  df-rdg 8381  df-1o 8437  df-2o 8438  df-nadd 8636  df-no 27714  df-lts 27715  df-bday 27716  df-les 27816  df-slts 27858  df-cuts 27860  df-0s 27907  df-1s 27908  df-made 27927  df-old 27928  df-left 27930  df-right 27931  df-norec 28038  df-norec2 28049  df-adds 28060  df-negs 28121  df-subs 28122  df-muls 28207  df-divs 28288

This theorem is referenced by:  precsexlem10  28316  precsexlem11  28317