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

Theorem precsexlem9 28239
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.
StepHypRef Expression
1 fveq2 6906 . . . . . 6 (𝑖 = ∅ → (𝐿𝑖) = (𝐿‘∅))
21raleqdv 3326 . . . . 5 (𝑖 = ∅ → (∀𝑏 ∈ (𝐿𝑖)(𝐴 ·s 𝑏) <s 1s ↔ ∀𝑏 ∈ (𝐿‘∅)(𝐴 ·s 𝑏) <s 1s ))
3 fveq2 6906 . . . . . 6 (𝑖 = ∅ → (𝑅𝑖) = (𝑅‘∅))
43raleqdv 3326 . . . . 5 (𝑖 = ∅ → (∀𝑐 ∈ (𝑅𝑖) 1s <s (𝐴 ·s 𝑐) ↔ ∀𝑐 ∈ (𝑅‘∅) 1s <s (𝐴 ·s 𝑐)))
52, 4anbi12d 632 . . . 4 (𝑖 = ∅ → ((∀𝑏 ∈ (𝐿𝑖)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑖) 1s <s (𝐴 ·s 𝑐)) ↔ (∀𝑏 ∈ (𝐿‘∅)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘∅) 1s <s (𝐴 ·s 𝑐))))
65imbi2d 340 . . 3 (𝑖 = ∅ → ((𝜑 → (∀𝑏 ∈ (𝐿𝑖)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑖) 1s <s (𝐴 ·s 𝑐))) ↔ (𝜑 → (∀𝑏 ∈ (𝐿‘∅)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘∅) 1s <s (𝐴 ·s 𝑐)))))
7 fveq2 6906 . . . . . 6 (𝑖 = 𝑗 → (𝐿𝑖) = (𝐿𝑗))
87raleqdv 3326 . . . . 5 (𝑖 = 𝑗 → (∀𝑏 ∈ (𝐿𝑖)(𝐴 ·s 𝑏) <s 1s ↔ ∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ))
9 fveq2 6906 . . . . . 6 (𝑖 = 𝑗 → (𝑅𝑖) = (𝑅𝑗))
109raleqdv 3326 . . . . 5 (𝑖 = 𝑗 → (∀𝑐 ∈ (𝑅𝑖) 1s <s (𝐴 ·s 𝑐) ↔ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐)))
118, 10anbi12d 632 . . . 4 (𝑖 = 𝑗 → ((∀𝑏 ∈ (𝐿𝑖)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑖) 1s <s (𝐴 ·s 𝑐)) ↔ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))))
1211imbi2d 340 . . 3 (𝑖 = 𝑗 → ((𝜑 → (∀𝑏 ∈ (𝐿𝑖)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑖) 1s <s (𝐴 ·s 𝑐))) ↔ (𝜑 → (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐)))))
13 fveq2 6906 . . . . . . 7 (𝑖 = suc 𝑗 → (𝐿𝑖) = (𝐿‘suc 𝑗))
1413raleqdv 3326 . . . . . 6 (𝑖 = suc 𝑗 → (∀𝑏 ∈ (𝐿𝑖)(𝐴 ·s 𝑏) <s 1s ↔ ∀𝑏 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑏) <s 1s ))
15 fveq2 6906 . . . . . . 7 (𝑖 = suc 𝑗 → (𝑅𝑖) = (𝑅‘suc 𝑗))
1615raleqdv 3326 . . . . . 6 (𝑖 = suc 𝑗 → (∀𝑐 ∈ (𝑅𝑖) 1s <s (𝐴 ·s 𝑐) ↔ ∀𝑐 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑐)))
1714, 16anbi12d 632 . . . . 5 (𝑖 = suc 𝑗 → ((∀𝑏 ∈ (𝐿𝑖)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑖) 1s <s (𝐴 ·s 𝑐)) ↔ (∀𝑏 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑐))))
18 oveq2 7439 . . . . . . . 8 (𝑏 = 𝑟 → (𝐴 ·s 𝑏) = (𝐴 ·s 𝑟))
1918breq1d 5153 . . . . . . 7 (𝑏 = 𝑟 → ((𝐴 ·s 𝑏) <s 1s ↔ (𝐴 ·s 𝑟) <s 1s ))
2019cbvralvw 3237 . . . . . 6 (∀𝑏 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑏) <s 1s ↔ ∀𝑟 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑟) <s 1s )
21 oveq2 7439 . . . . . . . 8 (𝑐 = 𝑠 → (𝐴 ·s 𝑐) = (𝐴 ·s 𝑠))
2221breq2d 5155 . . . . . . 7 (𝑐 = 𝑠 → ( 1s <s (𝐴 ·s 𝑐) ↔ 1s <s (𝐴 ·s 𝑠)))
2322cbvralvw 3237 . . . . . 6 (∀𝑐 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑐) ↔ ∀𝑠 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑠))
2420, 23anbi12i 628 . . . . 5 ((∀𝑏 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑐)) ↔ (∀𝑟 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑟) <s 1s ∧ ∀𝑠 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑠)))
2517, 24bitrdi 287 . . . 4 (𝑖 = suc 𝑗 → ((∀𝑏 ∈ (𝐿𝑖)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑖) 1s <s (𝐴 ·s 𝑐)) ↔ (∀𝑟 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑟) <s 1s ∧ ∀𝑠 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑠))))
2625imbi2d 340 . . 3 (𝑖 = suc 𝑗 → ((𝜑 → (∀𝑏 ∈ (𝐿𝑖)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑖) 1s <s (𝐴 ·s 𝑐))) ↔ (𝜑 → (∀𝑟 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑟) <s 1s ∧ ∀𝑠 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑠)))))
27 fveq2 6906 . . . . . 6 (𝑖 = 𝐼 → (𝐿𝑖) = (𝐿𝐼))
2827raleqdv 3326 . . . . 5 (𝑖 = 𝐼 → (∀𝑏 ∈ (𝐿𝑖)(𝐴 ·s 𝑏) <s 1s ↔ ∀𝑏 ∈ (𝐿𝐼)(𝐴 ·s 𝑏) <s 1s ))
29 fveq2 6906 . . . . . 6 (𝑖 = 𝐼 → (𝑅𝑖) = (𝑅𝐼))
3029raleqdv 3326 . . . . 5 (𝑖 = 𝐼 → (∀𝑐 ∈ (𝑅𝑖) 1s <s (𝐴 ·s 𝑐) ↔ ∀𝑐 ∈ (𝑅𝐼) 1s <s (𝐴 ·s 𝑐)))
3128, 30anbi12d 632 . . . 4 (𝑖 = 𝐼 → ((∀𝑏 ∈ (𝐿𝑖)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑖) 1s <s (𝐴 ·s 𝑐)) ↔ (∀𝑏 ∈ (𝐿𝐼)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝐼) 1s <s (𝐴 ·s 𝑐))))
3231imbi2d 340 . . 3 (𝑖 = 𝐼 → ((𝜑 → (∀𝑏 ∈ (𝐿𝑖)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑖) 1s <s (𝐴 ·s 𝑐))) ↔ (𝜑 → (∀𝑏 ∈ (𝐿𝐼)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝐼) 1s <s (𝐴 ·s 𝑐)))))
33 precsexlem.4 . . . . . . 7 (𝜑𝐴 No )
34 muls01 28138 . . . . . . 7 (𝐴 No → (𝐴 ·s 0s ) = 0s )
3533, 34syl 17 . . . . . 6 (𝜑 → (𝐴 ·s 0s ) = 0s )
36 0slt1s 27874 . . . . . 6 0s <s 1s
3735, 36eqbrtrdi 5182 . . . . 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𝐹)
4138, 39, 40precsexlem1 28231 . . . . . . 7 (𝐿‘∅) = { 0s }
4241raleqi 3324 . . . . . 6 (∀𝑏 ∈ (𝐿‘∅)(𝐴 ·s 𝑏) <s 1s ↔ ∀𝑏 ∈ { 0s } (𝐴 ·s 𝑏) <s 1s )
43 0sno 27871 . . . . . . . 8 0s No
4443elexi 3503 . . . . . . 7 0s ∈ V
45 oveq2 7439 . . . . . . . 8 (𝑏 = 0s → (𝐴 ·s 𝑏) = (𝐴 ·s 0s ))
4645breq1d 5153 . . . . . . 7 (𝑏 = 0s → ((𝐴 ·s 𝑏) <s 1s ↔ (𝐴 ·s 0s ) <s 1s ))
4744, 46ralsn 4681 . . . . . 6 (∀𝑏 ∈ { 0s } (𝐴 ·s 𝑏) <s 1s ↔ (𝐴 ·s 0s ) <s 1s )
4842, 47bitri 275 . . . . 5 (∀𝑏 ∈ (𝐿‘∅)(𝐴 ·s 𝑏) <s 1s ↔ (𝐴 ·s 0s ) <s 1s )
4937, 48sylibr 234 . . . 4 (𝜑 → ∀𝑏 ∈ (𝐿‘∅)(𝐴 ·s 𝑏) <s 1s )
50 ral0 4513 . . . . 5 𝑐 ∈ ∅ 1s <s (𝐴 ·s 𝑐)
5138, 39, 40precsexlem2 28232 . . . . . 6 (𝑅‘∅) = ∅
5251raleqi 3324 . . . . 5 (∀𝑐 ∈ (𝑅‘∅) 1s <s (𝐴 ·s 𝑐) ↔ ∀𝑐 ∈ ∅ 1s <s (𝐴 ·s 𝑐))
5350, 52mpbir 231 . . . 4 𝑐 ∈ (𝑅‘∅) 1s <s (𝐴 ·s 𝑐)
5449, 53jctir 520 . . 3 (𝜑 → (∀𝑏 ∈ (𝐿‘∅)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘∅) 1s <s (𝐴 ·s 𝑐)))
5538, 39, 40precsexlem4 28234 . . . . . . . . . . . 12 (𝑗 ∈ ω → (𝐿‘suc 𝑗) = ((𝐿𝑗) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})))
56553ad2ant2 1135 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝐿‘suc 𝑗) = ((𝐿𝑗) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})))
5756eleq2d 2827 . . . . . . . . . 10 ((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝑟 ∈ (𝐿‘suc 𝑗) ↔ 𝑟 ∈ ((𝐿𝑗) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)}))))
58 elun 4153 . . . . . . . . . . 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 4153 . . . . . . . . . . . . 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 3484 . . . . . . . . . . . . . . 15 𝑟 ∈ V
61 eqeq1 2741 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑟 → (𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) ↔ 𝑟 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)))
62612rexbidv 3222 . . . . . . . . . . . . . . 15 (𝑎 = 𝑟 → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) ↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿𝑗)𝑟 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)))
6360, 62elab 3679 . . . . . . . . . . . . . 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 𝑥𝐿)))
65642rexbidv 3222 . . . . . . . . . . . . . . 15 (𝑎 = 𝑟 → (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) ↔ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅𝑗)𝑟 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)))
6660, 65elab 3679 . . . . . . . . . . . . . 14 (𝑟 ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)} ↔ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅𝑗)𝑟 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿))
6763, 66orbi12i 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 𝑥𝐿)))
6859, 67bitri 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 𝑥𝐿)))
6968orbi2i 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 𝑥𝐿))))
7058, 69bitri 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 𝑥𝐿))))
7157, 70bitrdi 287 . . . . . . . . 9 ((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝑟 ∈ (𝐿‘suc 𝑗) ↔ (𝑟 ∈ (𝐿𝑗) ∨ (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿𝑗)𝑟 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) ∨ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅𝑗)𝑟 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)))))
72 simp3l 1202 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) → ∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s )
7319rspccv 3619 . . . . . . . . . . 11 (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s → (𝑟 ∈ (𝐿𝑗) → (𝐴 ·s 𝑟) <s 1s ))
7472, 73syl 17 . . . . . . . . . 10 ((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝑟 ∈ (𝐿𝑗) → (𝐴 ·s 𝑟) <s 1s ))
75333ad2ant1 1134 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) → 𝐴 No )
7675adantr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → 𝐴 No )
77 1sno 27872 . . . . . . . . . . . . . . . . 17 1s No
7877a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → 1s No )
79 rightssno 27920 . . . . . . . . . . . . . . . . . . . . 21 ( R ‘𝐴) ⊆ No
8079sseli 3979 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝑅 ∈ ( R ‘𝐴) → 𝑥𝑅 No )
8180adantl 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 𝑥𝑅 No )
8275adantr 480 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 𝐴 No )
8381, 82subscld 28093 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → (𝑥𝑅 -s 𝐴) ∈ No )
8483adantrr 717 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → (𝑥𝑅 -s 𝐴) ∈ No )
85 precsexlem.5 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → 0s <s 𝐴)
86 precsexlem.6 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 No (𝑥𝑂 ·s 𝑦) = 1s ))
8738, 39, 40, 33, 85, 86precsexlem8 28238 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ ω) → ((𝐿𝑗) ⊆ No ∧ (𝑅𝑗) ⊆ No ))
8887simpld 494 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ω) → (𝐿𝑗) ⊆ No )
89883adant3 1133 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝐿𝑗) ⊆ No )
9089sselda 3983 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑦𝐿 ∈ (𝐿𝑗)) → 𝑦𝐿 No )
9190adantrl 716 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → 𝑦𝐿 No )
9284, 91mulscld 28161 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿) ∈ No )
9378, 92addscld 28013 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) ∈ No )
9481adantrr 717 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → 𝑥𝑅 No )
9543a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 0s No )
96853ad2ant1 1134 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) → 0s <s 𝐴)
9796adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 0s <s 𝐴)
98 breq2 5147 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝑂 = 𝑥𝑅 → (𝐴 <s 𝑥𝑂𝐴 <s 𝑥𝑅))
99 rightval 27903 . . . . . . . . . . . . . . . . . . . . 21 ( R ‘𝐴) = {𝑥𝑂 ∈ ( O ‘( bday 𝐴)) ∣ 𝐴 <s 𝑥𝑂}
10098, 99elrab2 3695 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝑅 ∈ ( R ‘𝐴) ↔ (𝑥𝑅 ∈ ( O ‘( bday 𝐴)) ∧ 𝐴 <s 𝑥𝑅))
101100simprbi 496 . . . . . . . . . . . . . . . . . . 19 (𝑥𝑅 ∈ ( R ‘𝐴) → 𝐴 <s 𝑥𝑅)
102101adantl 481 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 𝐴 <s 𝑥𝑅)
10395, 82, 81, 97, 102slttrd 27804 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 0s <s 𝑥𝑅)
104103sgt0ne0d 27880 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 𝑥𝑅 ≠ 0s )
105104adantrr 717 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → 𝑥𝑅 ≠ 0s )
106 breq2 5147 . . . . . . . . . . . . . . . . . . 19 (𝑥𝑂 = 𝑥𝑅 → ( 0s <s 𝑥𝑂 ↔ 0s <s 𝑥𝑅))
107 oveq1 7438 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝑂 = 𝑥𝑅 → (𝑥𝑂 ·s 𝑦) = (𝑥𝑅 ·s 𝑦))
108107eqeq1d 2739 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝑂 = 𝑥𝑅 → ((𝑥𝑂 ·s 𝑦) = 1s ↔ (𝑥𝑅 ·s 𝑦) = 1s ))
109108rexbidv 3179 . . . . . . . . . . . . . . . . . . 19 (𝑥𝑂 = 𝑥𝑅 → (∃𝑦 No (𝑥𝑂 ·s 𝑦) = 1s ↔ ∃𝑦 No (𝑥𝑅 ·s 𝑦) = 1s ))
110106, 109imbi12d 344 . . . . . . . . . . . . . . . . . 18 (𝑥𝑂 = 𝑥𝑅 → (( 0s <s 𝑥𝑂 → ∃𝑦 No (𝑥𝑂 ·s 𝑦) = 1s ) ↔ ( 0s <s 𝑥𝑅 → ∃𝑦 No (𝑥𝑅 ·s 𝑦) = 1s )))
111863ad2ant1 1134 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 No (𝑥𝑂 ·s 𝑦) = 1s ))
112111adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 No (𝑥𝑂 ·s 𝑦) = 1s ))
113 elun2 4183 . . . . . . . . . . . . . . . . . . 19 (𝑥𝑅 ∈ ( R ‘𝐴) → 𝑥𝑅 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))
114113adantl 481 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 𝑥𝑅 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))
115110, 112, 114rspcdva 3623 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → ( 0s <s 𝑥𝑅 → ∃𝑦 No (𝑥𝑅 ·s 𝑦) = 1s ))
116103, 115mpd 15 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → ∃𝑦 No (𝑥𝑅 ·s 𝑦) = 1s )
117116adantrr 717 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → ∃𝑦 No (𝑥𝑅 ·s 𝑦) = 1s )
11876, 93, 94, 105, 117divsasswd 28228 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → ((𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) /su 𝑥𝑅) = (𝐴 ·s (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)))
119 oveq2 7439 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑏 = 𝑦𝐿 → (𝐴 ·s 𝑏) = (𝐴 ·s 𝑦𝐿))
120119breq1d 5153 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = 𝑦𝐿 → ((𝐴 ·s 𝑏) <s 1s ↔ (𝐴 ·s 𝑦𝐿) <s 1s ))
121120rspccva 3621 . . . . . . . . . . . . . . . . . . . . 21 ((∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s𝑦𝐿 ∈ (𝐿𝑗)) → (𝐴 ·s 𝑦𝐿) <s 1s )
12272, 121sylan 580 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑦𝐿 ∈ (𝐿𝑗)) → (𝐴 ·s 𝑦𝐿) <s 1s )
123122adantrl 716 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → (𝐴 ·s 𝑦𝐿) <s 1s )
12476, 91mulscld 28161 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → (𝐴 ·s 𝑦𝐿) ∈ No )
12582, 81posdifsd 28127 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → (𝐴 <s 𝑥𝑅 ↔ 0s <s (𝑥𝑅 -s 𝐴)))
126102, 125mpbid 232 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 0s <s (𝑥𝑅 -s 𝐴))
127126adantrr 717 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → 0s <s (𝑥𝑅 -s 𝐴))
128124, 78, 84, 127sltmul2d 28198 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → ((𝐴 ·s 𝑦𝐿) <s 1s ↔ ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)) <s ((𝑥𝑅 -s 𝐴) ·s 1s )))
129123, 128mpbid 232 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)) <s ((𝑥𝑅 -s 𝐴) ·s 1s ))
13084mulsridd 28140 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → ((𝑥𝑅 -s 𝐴) ·s 1s ) = (𝑥𝑅 -s 𝐴))
131129, 130breqtrd 5169 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)) <s (𝑥𝑅 -s 𝐴))
13284, 124mulscld 28161 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)) ∈ No )
13376, 132, 94sltaddsub2d 28122 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → ((𝐴 +s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))) <s 𝑥𝑅 ↔ ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)) <s (𝑥𝑅 -s 𝐴)))
134131, 133mpbird 257 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → (𝐴 +s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))) <s 𝑥𝑅)
13576, 78, 92addsdid 28182 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) = ((𝐴 ·s 1s ) +s (𝐴 ·s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))))
13676mulsridd 28140 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → (𝐴 ·s 1s ) = 𝐴)
13776, 84, 91muls12d 28207 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → (𝐴 ·s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) = ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)))
138136, 137oveq12d 7449 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → ((𝐴 ·s 1s ) +s (𝐴 ·s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) = (𝐴 +s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))))
139135, 138eqtrd 2777 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) = (𝐴 +s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))))
14094mulslidd 28169 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → ( 1s ·s 𝑥𝑅) = 𝑥𝑅)
141134, 139, 1403brtr4d 5175 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) <s ( 1s ·s 𝑥𝑅))
14276, 93mulscld 28161 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) ∈ No )
143103adantrr 717 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → 0s <s 𝑥𝑅)
144142, 78, 94, 143, 117sltdivmul2wd 28225 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → (((𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) /su 𝑥𝑅) <s 1s ↔ (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) <s ( 1s ·s 𝑥𝑅)))
145141, 144mpbird 257 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → ((𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) /su 𝑥𝑅) <s 1s )
146118, 145eqbrtrrd 5167 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → (𝐴 ·s (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)) <s 1s )
147 oveq2 7439 . . . . . . . . . . . . . 14 (𝑟 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) → (𝐴 ·s 𝑟) = (𝐴 ·s (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)))
148147breq1d 5153 . . . . . . . . . . . . 13 (𝑟 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) → ((𝐴 ·s 𝑟) <s 1s ↔ (𝐴 ·s (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)) <s 1s ))
149146, 148syl5ibrcom 247 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → (𝑟 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) → (𝐴 ·s 𝑟) <s 1s ))
150149rexlimdvva 3213 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿𝑗)𝑟 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) → (𝐴 ·s 𝑟) <s 1s ))
15175adantr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → 𝐴 No )
15277a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → 1s No )
153 leftssno 27919 . . . . . . . . . . . . . . . . . . . 20 ( L ‘𝐴) ⊆ No
154 elrabi 3687 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} → 𝑥𝐿 ∈ ( L ‘𝐴))
155154adantl 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → 𝑥𝐿 ∈ ( L ‘𝐴))
156153, 155sselid 3981 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → 𝑥𝐿 No )
15775adantr 480 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → 𝐴 No )
158156, 157subscld 28093 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → (𝑥𝐿 -s 𝐴) ∈ No )
159158adantrr 717 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → (𝑥𝐿 -s 𝐴) ∈ No )
16087simprd 495 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ ω) → (𝑅𝑗) ⊆ No )
1611603adant3 1133 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝑅𝑗) ⊆ No )
162161sselda 3983 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑦𝑅 ∈ (𝑅𝑗)) → 𝑦𝑅 No )
163162adantrl 716 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → 𝑦𝑅 No )
164159, 163mulscld 28161 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅) ∈ No )
165152, 164addscld 28013 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) ∈ No )
166156adantrr 717 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → 𝑥𝐿 No )
167 breq2 5147 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑥𝐿 → ( 0s <s 𝑥 ↔ 0s <s 𝑥𝐿))
168167elrab 3692 . . . . . . . . . . . . . . . . . . 19 (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ↔ (𝑥𝐿 ∈ ( L ‘𝐴) ∧ 0s <s 𝑥𝐿))
169168simprbi 496 . . . . . . . . . . . . . . . . . 18 (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} → 0s <s 𝑥𝐿)
170169adantl 481 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → 0s <s 𝑥𝐿)
171170sgt0ne0d 27880 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → 𝑥𝐿 ≠ 0s )
172171adantrr 717 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → 𝑥𝐿 ≠ 0s )
173 breq2 5147 . . . . . . . . . . . . . . . . . . 19 (𝑥𝑂 = 𝑥𝐿 → ( 0s <s 𝑥𝑂 ↔ 0s <s 𝑥𝐿))
174 oveq1 7438 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝑂 = 𝑥𝐿 → (𝑥𝑂 ·s 𝑦) = (𝑥𝐿 ·s 𝑦))
175174eqeq1d 2739 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝑂 = 𝑥𝐿 → ((𝑥𝑂 ·s 𝑦) = 1s ↔ (𝑥𝐿 ·s 𝑦) = 1s ))
176175rexbidv 3179 . . . . . . . . . . . . . . . . . . 19 (𝑥𝑂 = 𝑥𝐿 → (∃𝑦 No (𝑥𝑂 ·s 𝑦) = 1s ↔ ∃𝑦 No (𝑥𝐿 ·s 𝑦) = 1s ))
177173, 176imbi12d 344 . . . . . . . . . . . . . . . . . 18 (𝑥𝑂 = 𝑥𝐿 → (( 0s <s 𝑥𝑂 → ∃𝑦 No (𝑥𝑂 ·s 𝑦) = 1s ) ↔ ( 0s <s 𝑥𝐿 → ∃𝑦 No (𝑥𝐿 ·s 𝑦) = 1s )))
178111adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 No (𝑥𝑂 ·s 𝑦) = 1s ))
179 elun1 4182 . . . . . . . . . . . . . . . . . . 19 (𝑥𝐿 ∈ ( L ‘𝐴) → 𝑥𝐿 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))
180155, 179syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → 𝑥𝐿 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)))
181177, 178, 180rspcdva 3623 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → ( 0s <s 𝑥𝐿 → ∃𝑦 No (𝑥𝐿 ·s 𝑦) = 1s ))
182170, 181mpd 15 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → ∃𝑦 No (𝑥𝐿 ·s 𝑦) = 1s )
183182adantrr 717 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → ∃𝑦 No (𝑥𝐿 ·s 𝑦) = 1s )
184151, 165, 166, 172, 183divsasswd 28228 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → ((𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))) /su 𝑥𝐿) = (𝐴 ·s (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)))
185157, 156subscld 28093 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → (𝐴 -s 𝑥𝐿) ∈ No )
186185adantrr 717 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → (𝐴 -s 𝑥𝐿) ∈ No )
187186mulsridd 28140 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → ((𝐴 -s 𝑥𝐿) ·s 1s ) = (𝐴 -s 𝑥𝐿))
188 simp3r 1203 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) → ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))
189 oveq2 7439 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = 𝑦𝑅 → (𝐴 ·s 𝑐) = (𝐴 ·s 𝑦𝑅))
190189breq2d 5155 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = 𝑦𝑅 → ( 1s <s (𝐴 ·s 𝑐) ↔ 1s <s (𝐴 ·s 𝑦𝑅)))
191190rspccva 3621 . . . . . . . . . . . . . . . . . . . . . . 23 ((∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐) ∧ 𝑦𝑅 ∈ (𝑅𝑗)) → 1s <s (𝐴 ·s 𝑦𝑅))
192188, 191sylan 580 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑦𝑅 ∈ (𝑅𝑗)) → 1s <s (𝐴 ·s 𝑦𝑅))
193192adantrl 716 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → 1s <s (𝐴 ·s 𝑦𝑅))
194151, 163mulscld 28161 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → (𝐴 ·s 𝑦𝑅) ∈ No )
195 breq1 5146 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥𝑂 = 𝑥𝐿 → (𝑥𝑂 <s 𝐴𝑥𝐿 <s 𝐴))
196 leftval 27902 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ( L ‘𝐴) = {𝑥𝑂 ∈ ( O ‘( bday 𝐴)) ∣ 𝑥𝑂 <s 𝐴}
197195, 196elrab2 3695 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥𝐿 ∈ ( L ‘𝐴) ↔ (𝑥𝐿 ∈ ( O ‘( bday 𝐴)) ∧ 𝑥𝐿 <s 𝐴))
198197simprbi 496 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥𝐿 ∈ ( L ‘𝐴) → 𝑥𝐿 <s 𝐴)
199155, 198syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → 𝑥𝐿 <s 𝐴)
200156, 157posdifsd 28127 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → (𝑥𝐿 <s 𝐴 ↔ 0s <s (𝐴 -s 𝑥𝐿)))
201199, 200mpbid 232 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → 0s <s (𝐴 -s 𝑥𝐿))
202201adantrr 717 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → 0s <s (𝐴 -s 𝑥𝐿))
203152, 194, 186, 202sltmul2d 28198 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → ( 1s <s (𝐴 ·s 𝑦𝑅) ↔ ((𝐴 -s 𝑥𝐿) ·s 1s ) <s ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝑅))))
204193, 203mpbid 232 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → ((𝐴 -s 𝑥𝐿) ·s 1s ) <s ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝑅)))
205187, 204eqbrtrrd 5167 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → (𝐴 -s 𝑥𝐿) <s ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝑅)))
206156, 157negsubsdi2d 28110 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → ( -us ‘(𝑥𝐿 -s 𝐴)) = (𝐴 -s 𝑥𝐿))
207206adantrr 717 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → ( -us ‘(𝑥𝐿 -s 𝐴)) = (𝐴 -s 𝑥𝐿))
208159, 194mulnegs1d 28186 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → (( -us ‘(𝑥𝐿 -s 𝐴)) ·s (𝐴 ·s 𝑦𝑅)) = ( -us ‘((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))))
209206oveq1d 7446 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → (( -us ‘(𝑥𝐿 -s 𝐴)) ·s (𝐴 ·s 𝑦𝑅)) = ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝑅)))
210209adantrr 717 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → (( -us ‘(𝑥𝐿 -s 𝐴)) ·s (𝐴 ·s 𝑦𝑅)) = ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝑅)))
211208, 210eqtr3d 2779 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → ( -us ‘((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))) = ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝑅)))
212205, 207, 2113brtr4d 5175 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → ( -us ‘(𝑥𝐿 -s 𝐴)) <s ( -us ‘((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))))
213159, 194mulscld 28161 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)) ∈ No )
214213, 159sltnegd 28079 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → (((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)) <s (𝑥𝐿 -s 𝐴) ↔ ( -us ‘(𝑥𝐿 -s 𝐴)) <s ( -us ‘((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)))))
215212, 214mpbird 257 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)) <s (𝑥𝐿 -s 𝐴))
216151, 213, 166sltaddsub2d 28122 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → ((𝐴 +s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))) <s 𝑥𝐿 ↔ ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)) <s (𝑥𝐿 -s 𝐴)))
217215, 216mpbird 257 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → (𝐴 +s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))) <s 𝑥𝐿)
218151, 152, 164addsdid 28182 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))) = ((𝐴 ·s 1s ) +s (𝐴 ·s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))))
219151mulsridd 28140 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → (𝐴 ·s 1s ) = 𝐴)
220151, 159, 163muls12d 28207 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → (𝐴 ·s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) = ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)))
221219, 220oveq12d 7449 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → ((𝐴 ·s 1s ) +s (𝐴 ·s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))) = (𝐴 +s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))))
222218, 221eqtrd 2777 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))) = (𝐴 +s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))))
223166mulsridd 28140 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → (𝑥𝐿 ·s 1s ) = 𝑥𝐿)
224217, 222, 2233brtr4d 5175 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))) <s (𝑥𝐿 ·s 1s ))
225151, 165mulscld 28161 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))) ∈ No )
226170adantrr 717 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → 0s <s 𝑥𝐿)
227225, 152, 166, 226, 183sltdivmulwd 28224 . . . . . . . . . . . . . . 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 )))
228224, 227mpbird 257 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → ((𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))) /su 𝑥𝐿) <s 1s )
229184, 228eqbrtrrd 5167 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → (𝐴 ·s (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)) <s 1s )
230 oveq2 7439 . . . . . . . . . . . . . 14 (𝑟 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) → (𝐴 ·s 𝑟) = (𝐴 ·s (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)))
231230breq1d 5153 . . . . . . . . . . . . 13 (𝑟 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) → ((𝐴 ·s 𝑟) <s 1s ↔ (𝐴 ·s (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)) <s 1s ))
232229, 231syl5ibrcom 247 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → (𝑟 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) → (𝐴 ·s 𝑟) <s 1s ))
233232rexlimdvva 3213 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) → (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅𝑗)𝑟 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) → (𝐴 ·s 𝑟) <s 1s ))
234150, 233jaod 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 ))
23574, 234jaod 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 ))
23671, 235sylbid 240 . . . . . . . 8 ((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝑟 ∈ (𝐿‘suc 𝑗) → (𝐴 ·s 𝑟) <s 1s ))
237236ralrimiv 3145 . . . . . . 7 ((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) → ∀𝑟 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑟) <s 1s )
23838, 39, 40precsexlem5 28235 . . . . . . . . . . . 12 (𝑗 ∈ ω → (𝑅‘suc 𝑗) = ((𝑅𝑗) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)})))
2392383ad2ant2 1135 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝑅‘suc 𝑗) = ((𝑅𝑗) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)})))
240239eleq2d 2827 . . . . . . . . . 10 ((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝑠 ∈ (𝑅‘suc 𝑗) ↔ 𝑠 ∈ ((𝑅𝑗) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))))
241 elun 4153 . . . . . . . . . . 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 𝑥𝑅)})))
242 elun 4153 . . . . . . . . . . . . 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 vex 3484 . . . . . . . . . . . . . . 15 𝑠 ∈ V
244 eqeq1 2741 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑠 → (𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) ↔ 𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)))
2452442rexbidv 3222 . . . . . . . . . . . . . . 15 (𝑎 = 𝑠 → (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) ↔ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿𝑗)𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)))
246243, 245elab 3679 . . . . . . . . . . . . . 14 (𝑠 ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿𝑗)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ↔ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿𝑗)𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿))
247 eqeq1 2741 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑠 → (𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) ↔ 𝑠 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)))
2482472rexbidv 3222 . . . . . . . . . . . . . . 15 (𝑎 = 𝑠 → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) ↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅𝑗)𝑠 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)))
249243, 248elab 3679 . . . . . . . . . . . . . 14 (𝑠 ∈ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅𝑗)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)} ↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅𝑗)𝑠 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅))
250246, 249orbi12i 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 𝑥𝑅)))
251242, 250bitri 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 𝑥𝑅)))
252251orbi2i 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 𝑥𝑅))))
253241, 252bitri 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 𝑥𝑅))))
254240, 253bitrdi 287 . . . . . . . . 9 ((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝑠 ∈ (𝑅‘suc 𝑗) ↔ (𝑠 ∈ (𝑅𝑗) ∨ (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿𝑗)𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) ∨ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅𝑗)𝑠 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)))))
25522rspccv 3619 . . . . . . . . . . 11 (∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐) → (𝑠 ∈ (𝑅𝑗) → 1s <s (𝐴 ·s 𝑠)))
256188, 255syl 17 . . . . . . . . . 10 ((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝑠 ∈ (𝑅𝑗) → 1s <s (𝐴 ·s 𝑠)))
257122adantrl 716 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → (𝐴 ·s 𝑦𝐿) <s 1s )
25875adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → 𝐴 No )
25990adantrl 716 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → 𝑦𝐿 No )
260258, 259mulscld 28161 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → (𝐴 ·s 𝑦𝐿) ∈ No )
26177a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → 1s No )
262185adantrr 717 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → (𝐴 -s 𝑥𝐿) ∈ No )
263201adantrr 717 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → 0s <s (𝐴 -s 𝑥𝐿))
264260, 261, 262, 263sltmul2d 28198 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → ((𝐴 ·s 𝑦𝐿) <s 1s ↔ ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝐿)) <s ((𝐴 -s 𝑥𝐿) ·s 1s )))
265257, 264mpbid 232 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝐿)) <s ((𝐴 -s 𝑥𝐿) ·s 1s ))
266262mulsridd 28140 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → ((𝐴 -s 𝑥𝐿) ·s 1s ) = (𝐴 -s 𝑥𝐿))
267265, 266breqtrd 5169 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝐿)) <s (𝐴 -s 𝑥𝐿))
268158adantrr 717 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → (𝑥𝐿 -s 𝐴) ∈ No )
269268, 260mulnegs1d 28186 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → (( -us ‘(𝑥𝐿 -s 𝐴)) ·s (𝐴 ·s 𝑦𝐿)) = ( -us ‘((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))))
270206oveq1d 7446 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) → (( -us ‘(𝑥𝐿 -s 𝐴)) ·s (𝐴 ·s 𝑦𝐿)) = ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝐿)))
271270adantrr 717 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → (( -us ‘(𝑥𝐿 -s 𝐴)) ·s (𝐴 ·s 𝑦𝐿)) = ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝐿)))
272269, 271eqtr3d 2779 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → ( -us ‘((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))) = ((𝐴 -s 𝑥𝐿) ·s (𝐴 ·s 𝑦𝐿)))
273206adantrr 717 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → ( -us ‘(𝑥𝐿 -s 𝐴)) = (𝐴 -s 𝑥𝐿))
274267, 272, 2733brtr4d 5175 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → ( -us ‘((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))) <s ( -us ‘(𝑥𝐿 -s 𝐴)))
275268, 260mulscld 28161 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)) ∈ No )
276268, 275sltnegd 28079 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → ((𝑥𝐿 -s 𝐴) <s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)) ↔ ( -us ‘((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))) <s ( -us ‘(𝑥𝐿 -s 𝐴))))
277274, 276mpbird 257 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → (𝑥𝐿 -s 𝐴) <s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)))
278156adantrr 717 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → 𝑥𝐿 No )
279278, 258, 275sltsubadd2d 28120 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → ((𝑥𝐿 -s 𝐴) <s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)) ↔ 𝑥𝐿 <s (𝐴 +s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)))))
280277, 279mpbid 232 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → 𝑥𝐿 <s (𝐴 +s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))))
281278mulslidd 28169 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → ( 1s ·s 𝑥𝐿) = 𝑥𝐿)
282268, 259mulscld 28161 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿) ∈ No )
283258, 261, 282addsdid 28182 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))) = ((𝐴 ·s 1s ) +s (𝐴 ·s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))))
284258mulsridd 28140 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → (𝐴 ·s 1s ) = 𝐴)
285258, 268, 259muls12d 28207 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → (𝐴 ·s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) = ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)))
286284, 285oveq12d 7449 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → ((𝐴 ·s 1s ) +s (𝐴 ·s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))) = (𝐴 +s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))))
287283, 286eqtrd 2777 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))) = (𝐴 +s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))))
288280, 281, 2873brtr4d 5175 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → ( 1s ·s 𝑥𝐿) <s (𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))))
289261, 282addscld 28013 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) ∈ No )
290258, 289mulscld 28161 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))) ∈ No )
291170adantrr 717 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → 0s <s 𝑥𝐿)
292182adantrr 717 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → ∃𝑦 No (𝑥𝐿 ·s 𝑦) = 1s )
293261, 290, 278, 291, 292sltmuldivwd 28226 . . . . . . . . . . . . . . 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 𝑥𝐿)))
294288, 293mpbid 232 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → 1s <s ((𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))) /su 𝑥𝐿))
295171adantrr 717 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → 𝑥𝐿 ≠ 0s )
296258, 289, 278, 295, 292divsasswd 28228 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → ((𝐴 ·s ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))) /su 𝑥𝐿) = (𝐴 ·s (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)))
297294, 296breqtrd 5169 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → 1s <s (𝐴 ·s (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)))
298 oveq2 7439 . . . . . . . . . . . . . 14 (𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) → (𝐴 ·s 𝑠) = (𝐴 ·s (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)))
299298breq2d 5155 . . . . . . . . . . . . 13 (𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) → ( 1s <s (𝐴 ·s 𝑠) ↔ 1s <s (𝐴 ·s (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿))))
300297, 299syl5ibrcom 247 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑦𝐿 ∈ (𝐿𝑗))) → (𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) → 1s <s (𝐴 ·s 𝑠)))
301300rexlimdvva 3213 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) → (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿𝑗)𝑠 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) → 1s <s (𝐴 ·s 𝑠)))
30283adantrr 717 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → (𝑥𝑅 -s 𝐴) ∈ No )
303302mulsridd 28140 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → ((𝑥𝑅 -s 𝐴) ·s 1s ) = (𝑥𝑅 -s 𝐴))
304192adantrl 716 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → 1s <s (𝐴 ·s 𝑦𝑅))
30577a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → 1s No )
30675adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → 𝐴 No )
307162adantrl 716 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → 𝑦𝑅 No )
308306, 307mulscld 28161 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → (𝐴 ·s 𝑦𝑅) ∈ No )
309126adantrr 717 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → 0s <s (𝑥𝑅 -s 𝐴))
310305, 308, 302, 309sltmul2d 28198 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → ( 1s <s (𝐴 ·s 𝑦𝑅) ↔ ((𝑥𝑅 -s 𝐴) ·s 1s ) <s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))))
311304, 310mpbid 232 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → ((𝑥𝑅 -s 𝐴) ·s 1s ) <s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)))
312303, 311eqbrtrrd 5167 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → (𝑥𝑅 -s 𝐴) <s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)))
31381adantrr 717 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → 𝑥𝑅 No )
314302, 308mulscld 28161 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)) ∈ No )
315313, 306, 314sltsubadd2d 28120 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → ((𝑥𝑅 -s 𝐴) <s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)) ↔ 𝑥𝑅 <s (𝐴 +s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)))))
316312, 315mpbid 232 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → 𝑥𝑅 <s (𝐴 +s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))))
317313mulslidd 28169 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → ( 1s ·s 𝑥𝑅) = 𝑥𝑅)
318302, 307mulscld 28161 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅) ∈ No )
319306, 305, 318addsdid 28182 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))) = ((𝐴 ·s 1s ) +s (𝐴 ·s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))))
320306mulsridd 28140 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → (𝐴 ·s 1s ) = 𝐴)
321306, 302, 307muls12d 28207 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → (𝐴 ·s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) = ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)))
322320, 321oveq12d 7449 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → ((𝐴 ·s 1s ) +s (𝐴 ·s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))) = (𝐴 +s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))))
323319, 322eqtrd 2777 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))) = (𝐴 +s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))))
324316, 317, 3233brtr4d 5175 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → ( 1s ·s 𝑥𝑅) <s (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))))
325305, 318addscld 28013 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) ∈ No )
326306, 325mulscld 28161 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))) ∈ No )
327103adantrr 717 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → 0s <s 𝑥𝑅)
328116adantrr 717 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → ∃𝑦 No (𝑥𝑅 ·s 𝑦) = 1s )
329305, 326, 313, 327, 328sltmuldivwd 28226 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → (( 1s ·s 𝑥𝑅) <s (𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))) ↔ 1s <s ((𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))) /su 𝑥𝑅)))
330324, 329mpbid 232 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → 1s <s ((𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))) /su 𝑥𝑅))
331104adantrr 717 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → 𝑥𝑅 ≠ 0s )
332306, 325, 313, 331, 328divsasswd 28228 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → ((𝐴 ·s ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))) /su 𝑥𝑅) = (𝐴 ·s (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)))
333330, 332breqtrd 5169 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → 1s <s (𝐴 ·s (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)))
334 oveq2 7439 . . . . . . . . . . . . . 14 (𝑠 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) → (𝐴 ·s 𝑠) = (𝐴 ·s (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)))
335334breq2d 5155 . . . . . . . . . . . . 13 (𝑠 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) → ( 1s <s (𝐴 ·s 𝑠) ↔ 1s <s (𝐴 ·s (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅))))
336333, 335syl5ibrcom 247 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅𝑗))) → (𝑠 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) → 1s <s (𝐴 ·s 𝑠)))
337336rexlimdvva 3213 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅𝑗)𝑠 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) → 1s <s (𝐴 ·s 𝑠)))
338301, 337jaod 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 𝑠)))
339256, 338jaod 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 𝑠)))
340254, 339sylbid 240 . . . . . . . 8 ((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝑠 ∈ (𝑅‘suc 𝑗) → 1s <s (𝐴 ·s 𝑠)))
341340ralrimiv 3145 . . . . . . 7 ((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) → ∀𝑠 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑠))
342237, 341jca 511 . . . . . 6 ((𝜑𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) → (∀𝑟 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑟) <s 1s ∧ ∀𝑠 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑠)))
3433423exp 1120 . . . . 5 (𝜑 → (𝑗 ∈ ω → ((∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐)) → (∀𝑟 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑟) <s 1s ∧ ∀𝑠 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑠)))))
344343com12 32 . . . 4 (𝑗 ∈ ω → (𝜑 → ((∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐)) → (∀𝑟 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑟) <s 1s ∧ ∀𝑠 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑠)))))
345344a2d 29 . . 3 (𝑗 ∈ ω → ((𝜑 → (∀𝑏 ∈ (𝐿𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝜑 → (∀𝑟 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑟) <s 1s ∧ ∀𝑠 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑠)))))
3466, 12, 26, 32, 54, 345finds 7918 . 2 (𝐼 ∈ ω → (𝜑 → (∀𝑏 ∈ (𝐿𝐼)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝐼) 1s <s (𝐴 ·s 𝑐))))
347346impcom 407 1 ((𝜑𝐼 ∈ ω) → (∀𝑏 ∈ (𝐿𝐼)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅𝐼) 1s <s (𝐴 ·s 𝑐)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wo 848  w3a 1087   = wceq 1540  wcel 2108  {cab 2714  wne 2940  wral 3061  wrex 3070  {crab 3436  Vcvv 3480  csb 3899  cun 3949  wss 3951  c0 4333  {csn 4626  cop 4632   class class class wbr 5143  cmpt 5225  ccom 5689  suc csuc 6386  cfv 6561  (class class class)co 7431  ωcom 7887  1st c1st 8012  2nd c2nd 8013  reccrdg 8449   No csur 27684   <s cslt 27685   bday cbday 27686   0s c0s 27867   1s c1s 27868   O cold 27882   L cleft 27884   R cright 27885   +s cadds 27992   -us cnegs 28051   -s csubs 28052   ·s cmuls 28132   /su cdivs 28213
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-ot 4635  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-nadd 8704  df-no 27687  df-slt 27688  df-bday 27689  df-sle 27790  df-sslt 27826  df-scut 27828  df-0s 27869  df-1s 27870  df-made 27886  df-old 27887  df-left 27889  df-right 27890  df-norec 27971  df-norec2 27982  df-adds 27993  df-negs 28053  df-subs 28054  df-muls 28133  df-divs 28214
This theorem is referenced by:  precsexlem10  28240  precsexlem11  28241
  Copyright terms: Public domain W3C validator