Theorem precsexlem9 28207

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 6841	. . . . . 6 ⊢ (𝑖 = ∅ → (𝐿‘𝑖) = (𝐿‘∅))
2	1	raleqdv 3296	. . . . 5 ⊢ (𝑖 = ∅ → (∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ↔ ∀𝑏 ∈ (𝐿‘∅)(𝐴 ·s 𝑏) <s 1s ))
3		fveq2 6841	. . . . . 6 ⊢ (𝑖 = ∅ → (𝑅‘𝑖) = (𝑅‘∅))
4	3	raleqdv 3296	. . . . 5 ⊢ (𝑖 = ∅ → (∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐) ↔ ∀𝑐 ∈ (𝑅‘∅) 1s <s (𝐴 ·s 𝑐)))
5	2, 4	anbi12d 633	. . . 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 6841	. . . . . 6 ⊢ (𝑖 = 𝑗 → (𝐿‘𝑖) = (𝐿‘𝑗))
8	7	raleqdv 3296	. . . . 5 ⊢ (𝑖 = 𝑗 → (∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ↔ ∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ))
9		fveq2 6841	. . . . . 6 ⊢ (𝑖 = 𝑗 → (𝑅‘𝑖) = (𝑅‘𝑗))
10	9	raleqdv 3296	. . . . 5 ⊢ (𝑖 = 𝑗 → (∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐) ↔ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐)))
11	8, 10	anbi12d 633	. . . 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 6841	. . . . . . 7 ⊢ (𝑖 = suc 𝑗 → (𝐿‘𝑖) = (𝐿‘suc 𝑗))
14	13	raleqdv 3296	. . . . . 6 ⊢ (𝑖 = suc 𝑗 → (∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ↔ ∀𝑏 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑏) <s 1s ))
15		fveq2 6841	. . . . . . 7 ⊢ (𝑖 = suc 𝑗 → (𝑅‘𝑖) = (𝑅‘suc 𝑗))
16	15	raleqdv 3296	. . . . . 6 ⊢ (𝑖 = suc 𝑗 → (∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐) ↔ ∀𝑐 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑐)))
17	14, 16	anbi12d 633	. . . . 5 ⊢ (𝑖 = suc 𝑗 → ((∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐)) ↔ (∀𝑏 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑐))))
18		oveq2 7375	. . . . . . . 8 ⊢ (𝑏 = 𝑟 → (𝐴 ·s 𝑏) = (𝐴 ·s 𝑟))
19	18	breq1d 5096	. . . . . . 7 ⊢ (𝑏 = 𝑟 → ((𝐴 ·s 𝑏) <s 1s ↔ (𝐴 ·s 𝑟) <s 1s ))
20	19	cbvralvw 3216	. . . . . 6 ⊢ (∀𝑏 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑏) <s 1s ↔ ∀𝑟 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑟) <s 1s )
21		oveq2 7375	. . . . . . . 8 ⊢ (𝑐 = 𝑠 → (𝐴 ·s 𝑐) = (𝐴 ·s 𝑠))
22	21	breq2d 5098	. . . . . . 7 ⊢ (𝑐 = 𝑠 → ( 1s <s (𝐴 ·s 𝑐) ↔ 1s <s (𝐴 ·s 𝑠)))
23	22	cbvralvw 3216	. . . . . 6 ⊢ (∀𝑐 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑐) ↔ ∀𝑠 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑠))
24	20, 23	anbi12i 629	. . . . 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 6841	. . . . . 6 ⊢ (𝑖 = 𝐼 → (𝐿‘𝑖) = (𝐿‘𝐼))
28	27	raleqdv 3296	. . . . 5 ⊢ (𝑖 = 𝐼 → (∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ↔ ∀𝑏 ∈ (𝐿‘𝐼)(𝐴 ·s 𝑏) <s 1s ))
29		fveq2 6841	. . . . . 6 ⊢ (𝑖 = 𝐼 → (𝑅‘𝑖) = (𝑅‘𝐼))
30	29	raleqdv 3296	. . . . 5 ⊢ (𝑖 = 𝐼 → (∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐) ↔ ∀𝑐 ∈ (𝑅‘𝐼) 1s <s (𝐴 ·s 𝑐)))
31	28, 30	anbi12d 633	. . . 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 28104	. . . . . . 7 ⊢ (𝐴 ∈ No → (𝐴 ·s 0s ) = 0s )
35	33, 34	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐴 ·s 0s ) = 0s )
36		0lt1s 27804	. . . . . 6 ⊢ 0s <s 1s
37	35, 36	eqbrtrdi 5125	. . . . 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 28199	. . . . . . 7 ⊢ (𝐿‘∅) = { 0s }
42	41	raleqi 3294	. . . . . 6 ⊢ (∀𝑏 ∈ (𝐿‘∅)(𝐴 ·s 𝑏) <s 1s ↔ ∀𝑏 ∈ { 0s } (𝐴 ·s 𝑏) <s 1s )
43		0no 27801	. . . . . . . 8 ⊢ 0s ∈ No
44	43	elexi 3453	. . . . . . 7 ⊢ 0s ∈ V
45		oveq2 7375	. . . . . . . 8 ⊢ (𝑏 = 0s → (𝐴 ·s 𝑏) = (𝐴 ·s 0s ))
46	45	breq1d 5096	. . . . . . 7 ⊢ (𝑏 = 0s → ((𝐴 ·s 𝑏) <s 1s ↔ (𝐴 ·s 0s ) <s 1s ))
47	44, 46	ralsn 4626	. . . . . 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 4439	. . . . 5 ⊢ ∀𝑐 ∈ ∅ 1s <s (𝐴 ·s 𝑐)
51	38, 39, 40	precsexlem2 28200	. . . . . 6 ⊢ (𝑅‘∅) = ∅
52	51	raleqi 3294	. . . . 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 28202	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ω → (𝐿‘suc 𝑗) = ((𝐿‘𝑗) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})))
56	55	3ad2ant2 1135	. . . . . . . . . . 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 2823	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝑟 ∈ (𝐿‘suc 𝑗) ↔ 𝑟 ∈ ((𝐿‘𝑗) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)}))))
58		elun 4094	. . . . . . . . . . 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 4094	. . . . . . . . . . . . 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 3434	. . . . . . . . . . . . . . 15 ⊢ 𝑟 ∈ V
61		eqeq1 2741	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑟 → (𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) ↔ 𝑟 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)))
62	61	2rexbidv 3203	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑟 → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) ↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑟 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)))
63	60, 62	elab 3623	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑟 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅))
64		eqeq1 2741	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑟 → (𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) ↔ 𝑟 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)))
65	64	2rexbidv 3203	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑟 → (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) ↔ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑟 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)))
66	60, 65	elab 3623	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)} ↔ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑟 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿))
67	63, 66	orbi12i 915	. . . . . . . . . . . . 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 913	. . . . . . . . . . 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 1203	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → ∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s )
73	19	rspccv 3562	. . . . . . . . . . 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 1134	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → 𝐴 ∈ No )
76	75	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝐴 ∈ No )
77		1no 27802	. . . . . . . . . . . . . . . . 17 ⊢ 1s ∈ No
78	77	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 1s ∈ No )
79		rightno 27870	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥𝑅 ∈ ( R ‘𝐴) → 𝑥𝑅 ∈ No )
80	79	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 𝑥𝑅 ∈ No )
81	75	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 𝐴 ∈ No )
82	80, 81	subscld 28055	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → (𝑥𝑅 -s 𝐴) ∈ No )
83	82	adantrr 718	. . . . . . . . . . . . . . . . 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 28206	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ ω) → ((𝐿‘𝑗) ⊆ No ∧ (𝑅‘𝑗) ⊆ No ))
87	86	simpld 494	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ω) → (𝐿‘𝑗) ⊆ No )
88	87	3adant3 1133	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝐿‘𝑗) ⊆ No )
89	88	sselda 3922	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗)) → 𝑦𝐿 ∈ No )
90	89	adantrl 717	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑦𝐿 ∈ No )
91	83, 90	mulscld 28127	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿) ∈ No )
92	78, 91	addscld 27972	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) ∈ No )
93	80	adantrr 718	. . . . . . . . . . . . . . 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 1134	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → 0s <s 𝐴)
96	95	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 0s <s 𝐴)
97		rightgt 27846	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝑅 ∈ ( R ‘𝐴) → 𝐴 <s 𝑥𝑅)
98	97	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 𝐴 <s 𝑥𝑅)
99	94, 81, 80, 96, 98	ltstrd 27727	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 0s <s 𝑥𝑅)
100	99	gt0ne0sd 27811	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 𝑥𝑅 ≠ 0s )
101	100	adantrr 718	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑥𝑅 ≠ 0s )
102		breq2 5090	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝑂 = 𝑥𝑅 → ( 0s <s 𝑥𝑂 ↔ 0s <s 𝑥𝑅))
103		oveq1 7374	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥𝑂 = 𝑥𝑅 → (𝑥𝑂 ·s 𝑦) = (𝑥𝑅 ·s 𝑦))
104	103	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥𝑂 = 𝑥𝑅 → ((𝑥𝑂 ·s 𝑦) = 1s ↔ (𝑥𝑅 ·s 𝑦) = 1s ))
105	104	rexbidv 3162	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝑂 = 𝑥𝑅 → (∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ↔ ∃𝑦 ∈ No (𝑥𝑅 ·s 𝑦) = 1s ))
106	102, 105	imbi12d 344	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥𝑂 = 𝑥𝑅 → (( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ) ↔ ( 0s <s 𝑥𝑅 → ∃𝑦 ∈ No (𝑥𝑅 ·s 𝑦) = 1s )))
107	85	3ad2ant1 1134	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ))
108	107	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ))
109		elun2 4124	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝑅 ∈ ( R ‘𝐴) → 𝑥𝑅 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))
110	109	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 𝑥𝑅 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))
111	106, 108, 110	rspcdva 3566	. . . . . . . . . . . . . . . . 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 718	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ∃𝑦 ∈ No (𝑥𝑅 ·s 𝑦) = 1s )
114	76, 92, 93, 101, 113	divsasswd 28195	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) /su 𝑥𝑅) = (𝐴 ·s (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)))
115		oveq2 7375	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = 𝑦𝐿 → (𝐴 ·s 𝑏) = (𝐴 ·s 𝑦𝐿))
116	115	breq1d 5096	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = 𝑦𝐿 → ((𝐴 ·s 𝑏) <s 1s ↔ (𝐴 ·s 𝑦𝐿) <s 1s ))
117	116	rspccva 3564	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ 𝑦𝐿 ∈ (𝐿‘𝑗)) → (𝐴 ·s 𝑦𝐿) <s 1s )
118	72, 117	sylan 581	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗)) → (𝐴 ·s 𝑦𝐿) <s 1s )
119	118	adantrl 717	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s 𝑦𝐿) <s 1s )
120	76, 90	mulscld 28127	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s 𝑦𝐿) ∈ No )
121	81, 80	posdifsd 28090	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → (𝐴 <s 𝑥𝑅 ↔ 0s <s (𝑥𝑅 -s 𝐴)))
122	98, 121	mpbid 232	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 0s <s (𝑥𝑅 -s 𝐴))
123	122	adantrr 718	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 0s <s (𝑥𝑅 -s 𝐴))
124	120, 78, 83, 123	ltmuls2d 28164	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 ·s 𝑦𝐿) <s 1s ↔ ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)) <s ((𝑥𝑅 -s 𝐴) ·s 1s )))
125	119, 124	mpbid 232	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)) <s ((𝑥𝑅 -s 𝐴) ·s 1s ))
126	83	mulsridd 28106	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s 1s ) = (𝑥𝑅 -s 𝐴))
127	125, 126	breqtrd 5112	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)) <s (𝑥𝑅 -s 𝐴))
128	83, 120	mulscld 28127	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)) ∈ No )
129	76, 128, 93	ltaddsubs2d 28084	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 +s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))) <s 𝑥𝑅 ↔ ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)) <s (𝑥𝑅 -s 𝐴)))
130	127, 129	mpbird 257	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 +s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))) <s 𝑥𝑅)
131	76, 78, 91	addsdid 28148	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) = ((𝐴 ·s 1s ) +s (𝐴 ·s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))))
132	76	mulsridd 28106	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s 1s ) = 𝐴)
133	76, 83, 90	muls12d 28173	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) = ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)))
134	132, 133	oveq12d 7385	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 ·s 1s ) +s (𝐴 ·s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) = (𝐴 +s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))))
135	131, 134	eqtrd 2772	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) = (𝐴 +s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))))
136	93	mulslidd 28135	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( 1s ·s 𝑥𝑅) = 𝑥𝑅)
137	130, 135, 136	3brtr4d 5118	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) <s ( 1s ·s 𝑥𝑅))
138	76, 92	mulscld 28127	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) ∈ No )
139	99	adantrr 718	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 0s <s 𝑥𝑅)
140	138, 78, 93, 139, 113	ltdivmuls2wd 28192	. . . . . . . . . . . . . . 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 257	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) /su 𝑥𝑅) <s 1s )
142	114, 141	eqbrtrrd 5110	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)) <s 1s )
143		oveq2 7375	. . . . . . . . . . . . . 14 ⊢ (𝑟 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) → (𝐴 ·s 𝑟) = (𝐴 ·s (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)))
144	143	breq1d 5096	. . . . . . . . . . . . 13 ⊢ (𝑟 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) → ((𝐴 ·s 𝑟) <s 1s ↔ (𝐴 ·s (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)) <s 1s ))
145	142, 144	syl5ibrcom 247	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝑟 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) → (𝐴 ·s 𝑟) <s 1s ))
146	145	rexlimdvva 3195	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑟 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) → (𝐴 ·s 𝑟) <s 1s ))
147	75	adantr 480	. . . . . . . . . . . . . . 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 3631	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} → 𝑥𝐿 ∈ ( L ‘𝐴))
150	149	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → 𝑥𝐿 ∈ ( L ‘𝐴))
151	150	leftnod 27872	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → 𝑥𝐿 ∈ No )
152	75	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → 𝐴 ∈ No )
153	151, 152	subscld 28055	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → (𝑥𝐿 -s 𝐴) ∈ No )
154	153	adantrr 718	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝑥𝐿 -s 𝐴) ∈ No )
155	86	simprd 495	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ω) → (𝑅‘𝑗) ⊆ No )
156	155	3adant3 1133	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝑅‘𝑗) ⊆ No )
157	156	sselda 3922	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗)) → 𝑦𝑅 ∈ No )
158	157	adantrl 717	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑦𝑅 ∈ No )
159	154, 158	mulscld 28127	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅) ∈ No )
160	148, 159	addscld 27972	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) ∈ No )
161	151	adantrr 718	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑥𝐿 ∈ No )
162		breq2 5090	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑥𝐿 → ( 0s <s 𝑥 ↔ 0s <s 𝑥𝐿))
163	162	elrab 3635	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ↔ (𝑥𝐿 ∈ ( L ‘𝐴) ∧ 0s <s 𝑥𝐿))
164	163	simprbi 497	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} → 0s <s 𝑥𝐿)
165	164	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → 0s <s 𝑥𝐿)
166	165	gt0ne0sd 27811	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → 𝑥𝐿 ≠ 0s )
167	166	adantrr 718	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑥𝐿 ≠ 0s )
168		breq2 5090	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝑂 = 𝑥𝐿 → ( 0s <s 𝑥𝑂 ↔ 0s <s 𝑥𝐿))
169		oveq1 7374	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥𝑂 = 𝑥𝐿 → (𝑥𝑂 ·s 𝑦) = (𝑥𝐿 ·s 𝑦))
170	169	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥𝑂 = 𝑥𝐿 → ((𝑥𝑂 ·s 𝑦) = 1s ↔ (𝑥𝐿 ·s 𝑦) = 1s ))
171	170	rexbidv 3162	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝑂 = 𝑥𝐿 → (∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ↔ ∃𝑦 ∈ No (𝑥𝐿 ·s 𝑦) = 1s ))
172	168, 171	imbi12d 344	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥𝑂 = 𝑥𝐿 → (( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ) ↔ ( 0s <s 𝑥𝐿 → ∃𝑦 ∈ No (𝑥𝐿 ·s 𝑦) = 1s )))
173	107	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ))
174		elun1 4123	. . . . . . . . . . . . . . . . . . 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 3566	. . . . . . . . . . . . . . . . 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 718	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ∃𝑦 ∈ No (𝑥𝐿 ·s 𝑦) = 1s )
179	147, 160, 161, 167, 178	divsasswd 28195	. . . . . . . . . . . . . 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 28055	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → (𝐴 -s 𝑥𝐿) ∈ No )
181	180	adantrr 718	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 -s 𝑥𝐿) ∈ No )
182	181	mulsridd 28106	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝐴 -s 𝑥𝐿) ·s 1s ) = (𝐴 -s 𝑥𝐿))
183		simp3r 1204	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))
184		oveq2 7375	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = 𝑦𝑅 → (𝐴 ·s 𝑐) = (𝐴 ·s 𝑦𝑅))
185	184	breq2d 5098	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = 𝑦𝑅 → ( 1s <s (𝐴 ·s 𝑐) ↔ 1s <s (𝐴 ·s 𝑦𝑅)))
186	185	rspccva 3564	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗)) → 1s <s (𝐴 ·s 𝑦𝑅))
187	183, 186	sylan 581	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗)) → 1s <s (𝐴 ·s 𝑦𝑅))
188	187	adantrl 717	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 1s <s (𝐴 ·s 𝑦𝑅))
189	147, 158	mulscld 28127	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s 𝑦𝑅) ∈ No )
190		leftlt 27845	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥𝐿 ∈ ( L ‘𝐴) → 𝑥𝐿 <s 𝐴)
191	150, 190	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → 𝑥𝐿 <s 𝐴)
192	151, 152	posdifsd 28090	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → (𝑥𝐿 <s 𝐴 ↔ 0s <s (𝐴 -s 𝑥𝐿)))
193	191, 192	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → 0s <s (𝐴 -s 𝑥𝐿))
194	193	adantrr 718	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 0s <s (𝐴 -s 𝑥𝐿))
195	148, 189, 181, 194	ltmuls2d 28164	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( 1s <s (𝐴 ·s 𝑦𝑅) ↔ ((𝐴 -s 𝑥𝐿) ·s 1s ) <s ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝑅))))
196	188, 195	mpbid 232	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝐴 -s 𝑥𝐿) ·s 1s ) <s ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝑅)))
197	182, 196	eqbrtrrd 5110	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 -s 𝑥𝐿) <s ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝑅)))
198	151, 152	negsubsdi2d 28072	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → ( -us ‘(𝑥𝐿 -s 𝐴)) = (𝐴 -s 𝑥𝐿))
199	198	adantrr 718	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( -us ‘(𝑥𝐿 -s 𝐴)) = (𝐴 -s 𝑥𝐿))
200	154, 189	mulnegs1d 28152	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (( -us ‘(𝑥𝐿 -s 𝐴)) ·s (𝐴 ·s 𝑦𝑅)) = ( -us ‘((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))))
201	198	oveq1d 7382	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → (( -us ‘(𝑥𝐿 -s 𝐴)) ·s (𝐴 ·s 𝑦𝑅)) = ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝑅)))
202	201	adantrr 718	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (( -us ‘(𝑥𝐿 -s 𝐴)) ·s (𝐴 ·s 𝑦𝑅)) = ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝑅)))
203	200, 202	eqtr3d 2774	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( -us ‘((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))) = ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝑅)))
204	197, 199, 203	3brtr4d 5118	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( -us ‘(𝑥𝐿 -s 𝐴)) <s ( -us ‘((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))))
205	154, 189	mulscld 28127	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)) ∈ No )
206	205, 154	ltnegsd 28039	. . . . . . . . . . . . . . . . . 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 257	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)) <s (𝑥𝐿 -s 𝐴))
208	147, 205, 161	ltaddsubs2d 28084	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝐴 +s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))) <s 𝑥𝐿 ↔ ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)) <s (𝑥𝐿 -s 𝐴)))
209	207, 208	mpbird 257	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 +s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))) <s 𝑥𝐿)
210	147, 148, 159	addsdid 28148	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))) = ((𝐴 ·s 1s ) +s (𝐴 ·s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))))
211	147	mulsridd 28106	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s 1s ) = 𝐴)
212	147, 154, 158	muls12d 28173	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) = ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)))
213	211, 212	oveq12d 7385	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝐴 ·s 1s ) +s (𝐴 ·s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))) = (𝐴 +s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))))
214	210, 213	eqtrd 2772	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))) = (𝐴 +s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))))
215	161	mulsridd 28106	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝑥𝐿 ·s 1s ) = 𝑥𝐿)
216	209, 214, 215	3brtr4d 5118	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))) <s (𝑥𝐿 ·s 1s ))
217	147, 160	mulscld 28127	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))) ∈ No )
218	165	adantrr 718	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 0s <s 𝑥𝐿)
219	217, 148, 161, 218, 178	ltdivmulswd 28191	. . . . . . . . . . . . . . 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 257	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))) /su 𝑥𝐿) <s 1s )
221	179, 220	eqbrtrrd 5110	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)) <s 1s )
222		oveq2 7375	. . . . . . . . . . . . . 14 ⊢ (𝑟 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) → (𝐴 ·s 𝑟) = (𝐴 ·s (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)))
223	222	breq1d 5096	. . . . . . . . . . . . 13 ⊢ (𝑟 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) → ((𝐴 ·s 𝑟) <s 1s ↔ (𝐴 ·s (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)) <s 1s ))
224	221, 223	syl5ibrcom 247	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝑟 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) → (𝐴 ·s 𝑟) <s 1s ))
225	224	rexlimdvva 3195	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑟 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) → (𝐴 ·s 𝑟) <s 1s ))
226	146, 225	jaod 860	. . . . . . . . . 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 860	. . . . . . . . 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 240	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝑟 ∈ (𝐿‘suc 𝑗) → (𝐴 ·s 𝑟) <s 1s ))
229	228	ralrimiv 3129	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → ∀𝑟 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑟) <s 1s )
230	38, 39, 40	precsexlem5 28203	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ω → (𝑅‘suc 𝑗) = ((𝑅‘𝑗) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)})))
231	230	3ad2ant2 1135	. . . . . . . . . . 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 2823	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝑠 ∈ (𝑅‘suc 𝑗) ↔ 𝑠 ∈ ((𝑅‘𝑗) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))))
233		elun 4094	. . . . . . . . . . 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 4094	. . . . . . . . . . . . 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 3434	. . . . . . . . . . . . . . 15 ⊢ 𝑠 ∈ V
236		eqeq1 2741	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑠 → (𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) ↔ 𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)))
237	236	2rexbidv 3203	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑠 → (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) ↔ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)))
238	235, 237	elab 3623	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ↔ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿))
239		eqeq1 2741	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑠 → (𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) ↔ 𝑠 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)))
240	239	2rexbidv 3203	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑠 → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) ↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑠 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)))
241	235, 240	elab 3623	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)} ↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑠 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅))
242	238, 241	orbi12i 915	. . . . . . . . . . . . 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 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 𝑥𝑅)))
244	243	orbi2i 913	. . . . . . . . . . 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 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 𝑥𝑅))))
246	232, 245	bitrdi 287	. . . . . . . . 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 3562	. . . . . . . . . . 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 717	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s 𝑦𝐿) <s 1s )
250	75	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝐴 ∈ No )
251	89	adantrl 717	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑦𝐿 ∈ No )
252	250, 251	mulscld 28127	. . . . . . . . . . . . . . . . . . . . . 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 718	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 -s 𝑥𝐿) ∈ No )
255	193	adantrr 718	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 0s <s (𝐴 -s 𝑥𝐿))
256	252, 253, 254, 255	ltmuls2d 28164	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 ·s 𝑦𝐿) <s 1s ↔ ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝐿)) <s ((𝐴 -s 𝑥𝐿) ·s 1s )))
257	249, 256	mpbid 232	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝐿)) <s ((𝐴 -s 𝑥𝐿) ·s 1s ))
258	254	mulsridd 28106	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 -s 𝑥𝐿) ·s 1s ) = (𝐴 -s 𝑥𝐿))
259	257, 258	breqtrd 5112	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝐿)) <s (𝐴 -s 𝑥𝐿))
260	153	adantrr 718	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝑥𝐿 -s 𝐴) ∈ No )
261	260, 252	mulnegs1d 28152	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (( -us ‘(𝑥𝐿 -s 𝐴)) ·s (𝐴 ·s 𝑦𝐿)) = ( -us ‘((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))))
262	198	oveq1d 7382	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → (( -us ‘(𝑥𝐿 -s 𝐴)) ·s (𝐴 ·s 𝑦𝐿)) = ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝐿)))
263	262	adantrr 718	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (( -us ‘(𝑥𝐿 -s 𝐴)) ·s (𝐴 ·s 𝑦𝐿)) = ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝐿)))
264	261, 263	eqtr3d 2774	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( -us ‘((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))) = ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝐿)))
265	198	adantrr 718	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( -us ‘(𝑥𝐿 -s 𝐴)) = (𝐴 -s 𝑥𝐿))
266	259, 264, 265	3brtr4d 5118	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( -us ‘((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))) <s ( -us ‘(𝑥𝐿 -s 𝐴)))
267	260, 252	mulscld 28127	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)) ∈ No )
268	260, 267	ltnegsd 28039	. . . . . . . . . . . . . . . . . 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 257	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝑥𝐿 -s 𝐴) <s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)))
270	151	adantrr 718	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑥𝐿 ∈ No )
271	270, 250, 267	ltsubadds2d 28082	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝐿 -s 𝐴) <s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)) ↔ 𝑥𝐿 <s (𝐴 +s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)))))
272	269, 271	mpbid 232	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑥𝐿 <s (𝐴 +s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))))
273	270	mulslidd 28135	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( 1s ·s 𝑥𝐿) = 𝑥𝐿)
274	260, 251	mulscld 28127	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿) ∈ No )
275	250, 253, 274	addsdid 28148	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))) = ((𝐴 ·s 1s ) +s (𝐴 ·s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))))
276	250	mulsridd 28106	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s 1s ) = 𝐴)
277	250, 260, 251	muls12d 28173	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) = ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)))
278	276, 277	oveq12d 7385	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 ·s 1s ) +s (𝐴 ·s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))) = (𝐴 +s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))))
279	275, 278	eqtrd 2772	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))) = (𝐴 +s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))))
280	272, 273, 279	3brtr4d 5118	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( 1s ·s 𝑥𝐿) <s (𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))))
281	253, 274	addscld 27972	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) ∈ No )
282	250, 281	mulscld 28127	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))) ∈ No )
283	165	adantrr 718	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 0s <s 𝑥𝐿)
284	177	adantrr 718	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ∃𝑦 ∈ No (𝑥𝐿 ·s 𝑦) = 1s )
285	253, 282, 270, 283, 284	ltmuldivswd 28193	. . . . . . . . . . . . . . 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 232	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 1s <s ((𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))) /su 𝑥𝐿))
287	166	adantrr 718	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑥𝐿 ≠ 0s )
288	250, 281, 270, 287, 284	divsasswd 28195	. . . . . . . . . . . . . 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 5112	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 1s <s (𝐴 ·s (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)))
290		oveq2 7375	. . . . . . . . . . . . . 14 ⊢ (𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) → (𝐴 ·s 𝑠) = (𝐴 ·s (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)))
291	290	breq2d 5098	. . . . . . . . . . . . 13 ⊢ (𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) → ( 1s <s (𝐴 ·s 𝑠) ↔ 1s <s (𝐴 ·s (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿))))
292	289, 291	syl5ibrcom 247	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) → 1s <s (𝐴 ·s 𝑠)))
293	292	rexlimdvva 3195	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) → 1s <s (𝐴 ·s 𝑠)))
294	82	adantrr 718	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝑥𝑅 -s 𝐴) ∈ No )
295	294	mulsridd 28106	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s 1s ) = (𝑥𝑅 -s 𝐴))
296	187	adantrl 717	. . . . . . . . . . . . . . . . . . 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 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝐴 ∈ No )
299	157	adantrl 717	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑦𝑅 ∈ No )
300	298, 299	mulscld 28127	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s 𝑦𝑅) ∈ No )
301	122	adantrr 718	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 0s <s (𝑥𝑅 -s 𝐴))
302	297, 300, 294, 301	ltmuls2d 28164	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( 1s <s (𝐴 ·s 𝑦𝑅) ↔ ((𝑥𝑅 -s 𝐴) ·s 1s ) <s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))))
303	296, 302	mpbid 232	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s 1s ) <s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)))
304	295, 303	eqbrtrrd 5110	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝑥𝑅 -s 𝐴) <s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)))
305	80	adantrr 718	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑥𝑅 ∈ No )
306	294, 300	mulscld 28127	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)) ∈ No )
307	305, 298, 306	ltsubadds2d 28082	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝑥𝑅 -s 𝐴) <s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)) ↔ 𝑥𝑅 <s (𝐴 +s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)))))
308	304, 307	mpbid 232	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑥𝑅 <s (𝐴 +s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))))
309	305	mulslidd 28135	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( 1s ·s 𝑥𝑅) = 𝑥𝑅)
310	294, 299	mulscld 28127	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅) ∈ No )
311	298, 297, 310	addsdid 28148	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))) = ((𝐴 ·s 1s ) +s (𝐴 ·s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))))
312	298	mulsridd 28106	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s 1s ) = 𝐴)
313	298, 294, 299	muls12d 28173	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) = ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)))
314	312, 313	oveq12d 7385	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝐴 ·s 1s ) +s (𝐴 ·s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))) = (𝐴 +s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))))
315	311, 314	eqtrd 2772	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))) = (𝐴 +s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))))
316	308, 309, 315	3brtr4d 5118	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( 1s ·s 𝑥𝑅) <s (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))))
317	297, 310	addscld 27972	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) ∈ No )
318	298, 317	mulscld 28127	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))) ∈ No )
319	99	adantrr 718	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 0s <s 𝑥𝑅)
320	112	adantrr 718	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ∃𝑦 ∈ No (𝑥𝑅 ·s 𝑦) = 1s )
321	297, 318, 305, 319, 320	ltmuldivswd 28193	. . . . . . . . . . . . . . 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 232	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 1s <s ((𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))) /su 𝑥𝑅))
323	100	adantrr 718	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑥𝑅 ≠ 0s )
324	298, 317, 305, 323, 320	divsasswd 28195	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))) /su 𝑥𝑅) = (𝐴 ·s (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)))
325	322, 324	breqtrd 5112	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 1s <s (𝐴 ·s (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)))
326		oveq2 7375	. . . . . . . . . . . . . 14 ⊢ (𝑠 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) → (𝐴 ·s 𝑠) = (𝐴 ·s (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)))
327	326	breq2d 5098	. . . . . . . . . . . . 13 ⊢ (𝑠 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) → ( 1s <s (𝐴 ·s 𝑠) ↔ 1s <s (𝐴 ·s (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅))))
328	325, 327	syl5ibrcom 247	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝑠 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) → 1s <s (𝐴 ·s 𝑠)))
329	328	rexlimdvva 3195	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑠 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) → 1s <s (𝐴 ·s 𝑠)))
330	293, 329	jaod 860	. . . . . . . . . 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 860	. . . . . . . . 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 240	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝑠 ∈ (𝑅‘suc 𝑗) → 1s <s (𝐴 ·s 𝑠)))
333	332	ralrimiv 3129	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → ∀𝑠 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑠))
334	229, 333	jca 511	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (∀𝑟 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑟) <s 1s ∧ ∀𝑠 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑠)))
335	334	3exp 1120	. . . . 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 7847	. 2 ⊢ (𝐼 ∈ ω → (𝜑 → (∀𝑏 ∈ (𝐿‘𝐼)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝐼) 1s <s (𝐴 ·s 𝑐))))
339	338	impcom 407	1 ⊢ ((𝜑 ∧ 𝐼 ∈ ω) → (∀𝑏 ∈ (𝐿‘𝐼)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝐼) 1s <s (𝐴 ·s 𝑐)))

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 848   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  {cab 2715   ≠ wne 2933  ∀wral 3052  ∃wrex 3062  {crab 3390  Vcvv 3430  ⦋csb 3838   ∪ cun 3888   ⊆ wss 3890  ∅c0 4274  {csn 4568  ⟨cop 4574   class class class wbr 5086   ↦ cmpt 5167   ∘ ccom 5635  suc csuc 6326  ‘cfv 6499  (class class class)co 7367  ωcom 7817  1^st c1st 7940  2^nd c2nd 7941  reccrdg 8348   No csur 27603   <s clts 27604   0_s c0s 27797   1_s c1s 27798   L cleft 27817   R cright 27818   +_s cadds 27951   -u_s cnegs 28011   -_s csubs 28012   ·_s cmuls 28098   /_su cdivs 28179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5213  ax-sep 5232  ax-nul 5242  ax-pow 5308  ax-pr 5376  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-tp 4573  df-op 4575  df-ot 4577  df-uni 4852  df-int 4891  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-se 5585  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6266  df-ord 6327  df-on 6328  df-lim 6329  df-suc 6330  df-iota 6455  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-om 7818  df-1st 7942  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-1o 8405  df-2o 8406  df-nadd 8602  df-no 27606  df-lts 27607  df-bday 27608  df-les 27709  df-slts 27750  df-cuts 27752  df-0s 27799  df-1s 27800  df-made 27819  df-old 27820  df-left 27822  df-right 27823  df-norec 27930  df-norec2 27941  df-adds 27952  df-negs 28013  df-subs 28014  df-muls 28099  df-divs 28180

This theorem is referenced by:  precsexlem10  28208  precsexlem11  28209