| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fveq2 6906 | . . . . . 6
⊢ (𝑖 = ∅ → (𝐿‘𝑖) = (𝐿‘∅)) | 
| 2 | 1 | raleqdv 3326 | . . . . 5
⊢ (𝑖 = ∅ → (∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ↔ ∀𝑏 ∈ (𝐿‘∅)(𝐴 ·s 𝑏) <s 1s )) | 
| 3 |  | fveq2 6906 | . . . . . 6
⊢ (𝑖 = ∅ → (𝑅‘𝑖) = (𝑅‘∅)) | 
| 4 | 3 | raleqdv 3326 | . . . . 5
⊢ (𝑖 = ∅ → (∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐) ↔ ∀𝑐 ∈ (𝑅‘∅) 1s <s (𝐴 ·s 𝑐))) | 
| 5 | 2, 4 | anbi12d 632 | . . . 4
⊢ (𝑖 = ∅ →
((∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐)) ↔ (∀𝑏 ∈ (𝐿‘∅)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘∅) 1s <s (𝐴 ·s 𝑐)))) | 
| 6 | 5 | imbi2d 340 | . . 3
⊢ (𝑖 = ∅ → ((𝜑 → (∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐))) ↔ (𝜑 → (∀𝑏 ∈ (𝐿‘∅)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘∅) 1s <s (𝐴 ·s 𝑐))))) | 
| 7 |  | fveq2 6906 | . . . . . 6
⊢ (𝑖 = 𝑗 → (𝐿‘𝑖) = (𝐿‘𝑗)) | 
| 8 | 7 | raleqdv 3326 | . . . . 5
⊢ (𝑖 = 𝑗 → (∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ↔ ∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s )) | 
| 9 |  | fveq2 6906 | . . . . . 6
⊢ (𝑖 = 𝑗 → (𝑅‘𝑖) = (𝑅‘𝑗)) | 
| 10 | 9 | raleqdv 3326 | . . . . 5
⊢ (𝑖 = 𝑗 → (∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐) ↔ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) | 
| 11 | 8, 10 | anbi12d 632 | . . . 4
⊢ (𝑖 = 𝑗 → ((∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐)) ↔ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐)))) | 
| 12 | 11 | imbi2d 340 | . . 3
⊢ (𝑖 = 𝑗 → ((𝜑 → (∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐))) ↔ (𝜑 → (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))))) | 
| 13 |  | fveq2 6906 | . . . . . . 7
⊢ (𝑖 = suc 𝑗 → (𝐿‘𝑖) = (𝐿‘suc 𝑗)) | 
| 14 | 13 | raleqdv 3326 | . . . . . 6
⊢ (𝑖 = suc 𝑗 → (∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ↔ ∀𝑏 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑏) <s 1s )) | 
| 15 |  | fveq2 6906 | . . . . . . 7
⊢ (𝑖 = suc 𝑗 → (𝑅‘𝑖) = (𝑅‘suc 𝑗)) | 
| 16 | 15 | raleqdv 3326 | . . . . . 6
⊢ (𝑖 = suc 𝑗 → (∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐) ↔ ∀𝑐 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑐))) | 
| 17 | 14, 16 | anbi12d 632 | . . . . 5
⊢ (𝑖 = suc 𝑗 → ((∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐)) ↔ (∀𝑏 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑐)))) | 
| 18 |  | oveq2 7439 | . . . . . . . 8
⊢ (𝑏 = 𝑟 → (𝐴 ·s 𝑏) = (𝐴 ·s 𝑟)) | 
| 19 | 18 | breq1d 5153 | . . . . . . 7
⊢ (𝑏 = 𝑟 → ((𝐴 ·s 𝑏) <s 1s ↔ (𝐴 ·s 𝑟) <s 1s
)) | 
| 20 | 19 | cbvralvw 3237 | . . . . . 6
⊢
(∀𝑏 ∈
(𝐿‘suc 𝑗)(𝐴 ·s 𝑏) <s 1s ↔ ∀𝑟 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑟) <s 1s ) | 
| 21 |  | oveq2 7439 | . . . . . . . 8
⊢ (𝑐 = 𝑠 → (𝐴 ·s 𝑐) = (𝐴 ·s 𝑠)) | 
| 22 | 21 | breq2d 5155 | . . . . . . 7
⊢ (𝑐 = 𝑠 → ( 1s <s (𝐴 ·s 𝑐) ↔ 1s <s
(𝐴 ·s
𝑠))) | 
| 23 | 22 | cbvralvw 3237 | . . . . . 6
⊢
(∀𝑐 ∈
(𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑐) ↔ ∀𝑠 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑠)) | 
| 24 | 20, 23 | anbi12i 628 | . . . . 5
⊢
((∀𝑏 ∈
(𝐿‘suc 𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑐)) ↔ (∀𝑟 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑟) <s 1s ∧ ∀𝑠 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑠))) | 
| 25 | 17, 24 | bitrdi 287 | . . . 4
⊢ (𝑖 = suc 𝑗 → ((∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐)) ↔ (∀𝑟 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑟) <s 1s ∧ ∀𝑠 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑠)))) | 
| 26 | 25 | imbi2d 340 | . . 3
⊢ (𝑖 = suc 𝑗 → ((𝜑 → (∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐))) ↔ (𝜑 → (∀𝑟 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑟) <s 1s ∧ ∀𝑠 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑠))))) | 
| 27 |  | fveq2 6906 | . . . . . 6
⊢ (𝑖 = 𝐼 → (𝐿‘𝑖) = (𝐿‘𝐼)) | 
| 28 | 27 | raleqdv 3326 | . . . . 5
⊢ (𝑖 = 𝐼 → (∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ↔ ∀𝑏 ∈ (𝐿‘𝐼)(𝐴 ·s 𝑏) <s 1s )) | 
| 29 |  | fveq2 6906 | . . . . . 6
⊢ (𝑖 = 𝐼 → (𝑅‘𝑖) = (𝑅‘𝐼)) | 
| 30 | 29 | raleqdv 3326 | . . . . 5
⊢ (𝑖 = 𝐼 → (∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐) ↔ ∀𝑐 ∈ (𝑅‘𝐼) 1s <s (𝐴 ·s 𝑐))) | 
| 31 | 28, 30 | anbi12d 632 | . . . 4
⊢ (𝑖 = 𝐼 → ((∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐)) ↔ (∀𝑏 ∈ (𝐿‘𝐼)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝐼) 1s <s (𝐴 ·s 𝑐)))) | 
| 32 | 31 | imbi2d 340 | . . 3
⊢ (𝑖 = 𝐼 → ((𝜑 → (∀𝑏 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐))) ↔ (𝜑 → (∀𝑏 ∈ (𝐿‘𝐼)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝐼) 1s <s (𝐴 ·s 𝑐))))) | 
| 33 |  | precsexlem.4 | . . . . . . 7
⊢ (𝜑 → 𝐴 ∈  No
) | 
| 34 |  | muls01 28138 | . . . . . . 7
⊢ (𝐴 ∈ 
No  → (𝐴
·s 0s ) = 0s ) | 
| 35 | 33, 34 | syl 17 | . . . . . 6
⊢ (𝜑 → (𝐴 ·s 0s ) =
0s ) | 
| 36 |  | 0slt1s 27874 | . . . . . 6
⊢ 
0s <s 1s | 
| 37 | 35, 36 | eqbrtrdi 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 ∘ 𝐹) | 
| 41 | 38, 39, 40 | precsexlem1 28231 | . . . . . . 7
⊢ (𝐿‘∅) = {
0s } | 
| 42 | 41 | raleqi 3324 | . . . . . 6
⊢
(∀𝑏 ∈
(𝐿‘∅)(𝐴 ·s 𝑏) <s 1s ↔
∀𝑏 ∈ {
0s } (𝐴
·s 𝑏)
<s 1s ) | 
| 43 |  | 0sno 27871 | . . . . . . . 8
⊢ 
0s ∈  No | 
| 44 | 43 | elexi 3503 | . . . . . . 7
⊢ 
0s ∈ V | 
| 45 |  | oveq2 7439 | . . . . . . . 8
⊢ (𝑏 = 0s → (𝐴 ·s 𝑏) = (𝐴 ·s 0s
)) | 
| 46 | 45 | breq1d 5153 | . . . . . . 7
⊢ (𝑏 = 0s → ((𝐴 ·s 𝑏) <s 1s ↔
(𝐴 ·s
0s ) <s 1s )) | 
| 47 | 44, 46 | ralsn 4681 | . . . . . 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 4513 | . . . . 5
⊢
∀𝑐 ∈
∅ 1s <s (𝐴 ·s 𝑐) | 
| 51 | 38, 39, 40 | precsexlem2 28232 | . . . . . 6
⊢ (𝑅‘∅) =
∅ | 
| 52 | 51 | raleqi 3324 | . . . . 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 28234 | . . . . . . . . . . . 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 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 𝑥𝑅))) | 
| 62 | 61 | 2rexbidv 3222 | . . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑟 → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)
↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑟 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅))) | 
| 63 | 60, 62 | elab 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 𝑥𝐿))) | 
| 65 | 64 | 2rexbidv 3222 | . . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑟 → (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)
↔ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑟 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿))) | 
| 66 | 60, 65 | elab 3679 | . . . . . . . . . . . . . 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 1202 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → ∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ) | 
| 73 | 19 | rspccv 3619 | . . . . . . . . . . 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 |  | 1sno 27872 | . . . . . . . . . . . . . . . . 17
⊢ 
1s ∈  No | 
| 78 | 77 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 1s ∈  No ) | 
| 79 |  | rightssno 27920 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ( R
‘𝐴) ⊆  No | 
| 80 | 79 | sseli 3979 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥𝑅 ∈ ( R
‘𝐴) → 𝑥𝑅 ∈
 No ) | 
| 81 | 80 | adantl 481 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 𝑥𝑅 ∈  No ) | 
| 82 | 75 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 𝐴 ∈  No
) | 
| 83 | 81, 82 | subscld 28093 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → (𝑥𝑅 -s 𝐴) ∈ 
No ) | 
| 84 | 83 | adantrr 717 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝑥𝑅 -s 𝐴) ∈ 
No ) | 
| 85 |  | precsexlem.5 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 0s <s 𝐴) | 
| 86 |  | precsexlem.6 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0s <s 𝑥𝑂 →
∃𝑦 ∈  No  (𝑥𝑂 ·s
𝑦) = 1s
)) | 
| 87 | 38, 39, 40, 33, 85, 86 | precsexlem8 28238 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ ω) → ((𝐿‘𝑗) ⊆  No 
∧ (𝑅‘𝑗) ⊆ 
No )) | 
| 88 | 87 | simpld 494 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ ω) → (𝐿‘𝑗) ⊆  No
) | 
| 89 | 88 | 3adant3 1133 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝐿‘𝑗) ⊆  No
) | 
| 90 | 89 | sselda 3983 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗)) → 𝑦𝐿 ∈  No ) | 
| 91 | 90 | adantrl 716 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑦𝐿 ∈  No ) | 
| 92 | 84, 91 | mulscld 28161 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿) ∈
 No ) | 
| 93 | 78, 92 | addscld 28013 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( 1s +s
((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) ∈  No ) | 
| 94 | 81 | adantrr 717 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑥𝑅 ∈  No ) | 
| 95 | 43 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 0s ∈
 No ) | 
| 96 | 85 | 3ad2ant1 1134 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → 0s <s 𝐴) | 
| 97 | 96 | adantr 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 𝑥𝑂} | 
| 100 | 98, 99 | elrab2 3695 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥𝑅 ∈ ( R
‘𝐴) ↔ (𝑥𝑅 ∈ ( O
‘( bday ‘𝐴)) ∧ 𝐴 <s 𝑥𝑅)) | 
| 101 | 100 | simprbi 496 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥𝑅 ∈ ( R
‘𝐴) → 𝐴 <s 𝑥𝑅) | 
| 102 | 101 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 𝐴 <s 𝑥𝑅) | 
| 103 | 95, 82, 81, 97, 102 | slttrd 27804 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 0s <s
𝑥𝑅) | 
| 104 | 103 | sgt0ne0d 27880 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 𝑥𝑅 ≠ 0s
) | 
| 105 | 104 | adantrr 717 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑥𝑅 ≠ 0s
) | 
| 106 |  | breq2 5147 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥𝑂 = 𝑥𝑅 → (
0s <s 𝑥𝑂 ↔ 0s
<s 𝑥𝑅)) | 
| 107 |  | oveq1 7438 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥𝑂 = 𝑥𝑅 →
(𝑥𝑂
·s 𝑦) =
(𝑥𝑅
·s 𝑦)) | 
| 108 | 107 | eqeq1d 2739 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥𝑂 = 𝑥𝑅 →
((𝑥𝑂
·s 𝑦) =
1s ↔ (𝑥𝑅 ·s
𝑦) = 1s
)) | 
| 109 | 108 | rexbidv 3179 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥𝑂 = 𝑥𝑅 →
(∃𝑦 ∈  No  (𝑥𝑂 ·s
𝑦) = 1s ↔
∃𝑦 ∈  No  (𝑥𝑅 ·s
𝑦) = 1s
)) | 
| 110 | 106, 109 | imbi12d 344 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥𝑂 = 𝑥𝑅 → ((
0s <s 𝑥𝑂 → ∃𝑦 ∈ 
No  (𝑥𝑂 ·s
𝑦) = 1s ) ↔
( 0s <s 𝑥𝑅 → ∃𝑦 ∈ 
No  (𝑥𝑅 ·s
𝑦) = 1s
))) | 
| 111 | 86 | 3ad2ant1 1134 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0s <s 𝑥𝑂 →
∃𝑦 ∈  No  (𝑥𝑂 ·s
𝑦) = 1s
)) | 
| 112 | 111 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → ∀𝑥𝑂 ∈ (( L
‘𝐴) ∪ ( R
‘𝐴))( 0s
<s 𝑥𝑂
→ ∃𝑦 ∈
 No  (𝑥𝑂 ·s
𝑦) = 1s
)) | 
| 113 |  | elun2 4183 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥𝑅 ∈ ( R
‘𝐴) → 𝑥𝑅 ∈ (( L
‘𝐴) ∪ ( R
‘𝐴))) | 
| 114 | 113 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 𝑥𝑅 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))) | 
| 115 | 110, 112,
114 | rspcdva 3623 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → ( 0s <s
𝑥𝑅
→ ∃𝑦 ∈
 No  (𝑥𝑅 ·s
𝑦) = 1s
)) | 
| 116 | 103, 115 | mpd 15 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → ∃𝑦 ∈ 
No  (𝑥𝑅 ·s
𝑦) = 1s
) | 
| 117 | 116 | adantrr 717 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ∃𝑦 ∈  No 
(𝑥𝑅
·s 𝑦) =
1s ) | 
| 118 | 76, 93, 94, 105, 117 | divsasswd 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 𝑦𝐿)) | 
| 120 | 119 | breq1d 5153 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑏 = 𝑦𝐿 → ((𝐴 ·s 𝑏) <s 1s ↔
(𝐴 ·s
𝑦𝐿) <s
1s )) | 
| 121 | 120 | rspccva 3621 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((∀𝑏 ∈
(𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ 𝑦𝐿 ∈
(𝐿‘𝑗)) → (𝐴 ·s 𝑦𝐿) <s 1s
) | 
| 122 | 72, 121 | sylan 580 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗)) → (𝐴 ·s 𝑦𝐿) <s 1s
) | 
| 123 | 122 | adantrl 716 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s 𝑦𝐿) <s 1s
) | 
| 124 | 76, 91 | mulscld 28161 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s 𝑦𝐿) ∈  No ) | 
| 125 | 82, 81 | posdifsd 28127 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → (𝐴 <s 𝑥𝑅 ↔ 0s
<s (𝑥𝑅 -s 𝐴))) | 
| 126 | 102, 125 | mpbid 232 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 0s <s
(𝑥𝑅
-s 𝐴)) | 
| 127 | 126 | adantrr 717 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 0s <s (𝑥𝑅
-s 𝐴)) | 
| 128 | 124, 78, 84, 127 | sltmul2d 28198 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 ·s 𝑦𝐿) <s 1s
↔ ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)) <s
((𝑥𝑅
-s 𝐴)
·s 1s ))) | 
| 129 | 123, 128 | mpbid 232 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)) <s
((𝑥𝑅
-s 𝐴)
·s 1s )) | 
| 130 | 84 | mulsridd 28140 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s
1s ) = (𝑥𝑅 -s 𝐴)) | 
| 131 | 129, 130 | breqtrd 5169 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)) <s
(𝑥𝑅
-s 𝐴)) | 
| 132 | 84, 124 | mulscld 28161 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)) ∈
 No ) | 
| 133 | 76, 132, 94 | sltaddsub2d 28122 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 +s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))) <s
𝑥𝑅
↔ ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)) <s
(𝑥𝑅
-s 𝐴))) | 
| 134 | 131, 133 | mpbird 257 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 +s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))) <s
𝑥𝑅) | 
| 135 | 76, 78, 92 | addsdid 28182 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ( 1s
+s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) = ((𝐴 ·s
1s ) +s (𝐴 ·s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)))) | 
| 136 | 76 | mulsridd 28140 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s 1s ) =
𝐴) | 
| 137 | 76, 84, 91 | muls12d 28207 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) = ((𝑥𝑅
-s 𝐴)
·s (𝐴
·s 𝑦𝐿))) | 
| 138 | 136, 137 | oveq12d 7449 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 ·s 1s )
+s (𝐴
·s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) = (𝐴 +s ((𝑥𝑅
-s 𝐴)
·s (𝐴
·s 𝑦𝐿)))) | 
| 139 | 135, 138 | eqtrd 2777 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ( 1s
+s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) = (𝐴 +s ((𝑥𝑅
-s 𝐴)
·s (𝐴
·s 𝑦𝐿)))) | 
| 140 | 94 | mulslidd 28169 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( 1s
·s 𝑥𝑅) = 𝑥𝑅) | 
| 141 | 134, 139,
140 | 3brtr4d 5175 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ( 1s
+s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) <s (
1s ·s 𝑥𝑅)) | 
| 142 | 76, 93 | mulscld 28161 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ( 1s
+s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))) ∈
 No ) | 
| 143 | 103 | adantrr 717 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 0s <s 𝑥𝑅) | 
| 144 | 142, 78, 94, 143, 117 | sltdivmul2wd 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 𝑥𝑅))) | 
| 145 | 141, 144 | mpbird 257 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 ·s ( 1s
+s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)))
/su 𝑥𝑅) <s 1s
) | 
| 146 | 118, 145 | eqbrtrrd 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 𝑥𝑅))) | 
| 148 | 147 | breq1d 5153 | . . . . . . . . . . . . 13
⊢ (𝑟 = (( 1s
+s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))
/su 𝑥𝑅) → ((𝐴 ·s 𝑟) <s 1s ↔
(𝐴 ·s ((
1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿))
/su 𝑥𝑅)) <s 1s
)) | 
| 149 | 146, 148 | syl5ibrcom 247 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝑟 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)
→ (𝐴
·s 𝑟)
<s 1s )) | 
| 150 | 149 | rexlimdvva 3213 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑟 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)
→ (𝐴
·s 𝑟)
<s 1s )) | 
| 151 | 75 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝐴 ∈  No
) | 
| 152 | 77 | a1i 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
‘𝐴)) | 
| 155 | 154 | adantl 481 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}) → 𝑥𝐿 ∈ ( L
‘𝐴)) | 
| 156 | 153, 155 | sselid 3981 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}) → 𝑥𝐿 ∈
 No ) | 
| 157 | 75 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}) → 𝐴 ∈ 
No ) | 
| 158 | 156, 157 | subscld 28093 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}) → (𝑥𝐿
-s 𝐴) ∈
 No ) | 
| 159 | 158 | adantrr 717 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝑥𝐿 -s 𝐴) ∈ 
No ) | 
| 160 | 87 | simprd 495 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ ω) → (𝑅‘𝑗) ⊆  No
) | 
| 161 | 160 | 3adant3 1133 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝑅‘𝑗) ⊆  No
) | 
| 162 | 161 | sselda 3983 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗)) → 𝑦𝑅 ∈  No ) | 
| 163 | 162 | adantrl 716 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑦𝑅 ∈  No ) | 
| 164 | 159, 163 | mulscld 28161 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅) ∈
 No ) | 
| 165 | 152, 164 | addscld 28013 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( 1s +s
((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) ∈  No ) | 
| 166 | 156 | adantrr 717 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑥𝐿 ∈  No ) | 
| 167 |  | breq2 5147 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑥𝐿 → ( 0s
<s 𝑥 ↔
0s <s 𝑥𝐿)) | 
| 168 | 167 | elrab 3692 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥𝐿 ∈
{𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ↔ (𝑥𝐿 ∈ ( L
‘𝐴) ∧
0s <s 𝑥𝐿)) | 
| 169 | 168 | simprbi 496 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥𝐿 ∈
{𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} → 0s
<s 𝑥𝐿) | 
| 170 | 169 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}) → 0s
<s 𝑥𝐿) | 
| 171 | 170 | sgt0ne0d 27880 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}) → 𝑥𝐿 ≠
0s ) | 
| 172 | 171 | adantrr 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 𝑦)) | 
| 175 | 174 | eqeq1d 2739 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥𝑂 = 𝑥𝐿 →
((𝑥𝑂
·s 𝑦) =
1s ↔ (𝑥𝐿 ·s
𝑦) = 1s
)) | 
| 176 | 175 | rexbidv 3179 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥𝑂 = 𝑥𝐿 →
(∃𝑦 ∈  No  (𝑥𝑂 ·s
𝑦) = 1s ↔
∃𝑦 ∈  No  (𝑥𝐿 ·s
𝑦) = 1s
)) | 
| 177 | 173, 176 | imbi12d 344 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥𝑂 = 𝑥𝐿 → ((
0s <s 𝑥𝑂 → ∃𝑦 ∈ 
No  (𝑥𝑂 ·s
𝑦) = 1s ) ↔
( 0s <s 𝑥𝐿 → ∃𝑦 ∈ 
No  (𝑥𝐿 ·s
𝑦) = 1s
))) | 
| 178 | 111 | adantr 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
‘𝐴))) | 
| 180 | 155, 179 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}) → 𝑥𝐿 ∈ (( L
‘𝐴) ∪ ( R
‘𝐴))) | 
| 181 | 177, 178,
180 | rspcdva 3623 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}) → ( 0s
<s 𝑥𝐿
→ ∃𝑦 ∈
 No  (𝑥𝐿 ·s
𝑦) = 1s
)) | 
| 182 | 170, 181 | mpd 15 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}) → ∃𝑦 ∈ 
No  (𝑥𝐿 ·s
𝑦) = 1s
) | 
| 183 | 182 | adantrr 717 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ∃𝑦 ∈  No 
(𝑥𝐿
·s 𝑦) =
1s ) | 
| 184 | 151, 165,
166, 172, 183 | divsasswd 28228 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝐴 ·s ( 1s
+s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)))
/su 𝑥𝐿) = (𝐴 ·s (( 1s
+s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))
/su 𝑥𝐿))) | 
| 185 | 157, 156 | subscld 28093 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}) → (𝐴 -s 𝑥𝐿) ∈
 No ) | 
| 186 | 185 | adantrr 717 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 -s 𝑥𝐿) ∈  No ) | 
| 187 | 186 | mulsridd 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 𝑦𝑅)) | 
| 190 | 189 | breq2d 5155 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑐 = 𝑦𝑅 → ( 1s
<s (𝐴
·s 𝑐)
↔ 1s <s (𝐴 ·s 𝑦𝑅))) | 
| 191 | 190 | rspccva 3621 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
((∀𝑐 ∈
(𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗)) → 1s <s (𝐴 ·s 𝑦𝑅)) | 
| 192 | 188, 191 | sylan 580 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗)) → 1s <s (𝐴 ·s 𝑦𝑅)) | 
| 193 | 192 | adantrl 716 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 1s <s (𝐴 ·s 𝑦𝑅)) | 
| 194 | 151, 163 | mulscld 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 𝐴} | 
| 197 | 195, 196 | elrab2 3695 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥𝐿 ∈ ( L
‘𝐴) ↔ (𝑥𝐿 ∈ ( O
‘( bday ‘𝐴)) ∧ 𝑥𝐿 <s 𝐴)) | 
| 198 | 197 | simprbi 496 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥𝐿 ∈ ( L
‘𝐴) → 𝑥𝐿 <s 𝐴) | 
| 199 | 155, 198 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}) → 𝑥𝐿 <s 𝐴) | 
| 200 | 156, 157 | posdifsd 28127 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}) → (𝑥𝐿 <s 𝐴 ↔ 0s <s
(𝐴 -s 𝑥𝐿))) | 
| 201 | 199, 200 | mpbid 232 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}) → 0s
<s (𝐴 -s
𝑥𝐿)) | 
| 202 | 201 | adantrr 717 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 0s <s (𝐴 -s 𝑥𝐿)) | 
| 203 | 152, 194,
186, 202 | sltmul2d 28198 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( 1s <s (𝐴 ·s 𝑦𝑅) ↔
((𝐴 -s 𝑥𝐿)
·s 1s ) <s ((𝐴 -s 𝑥𝐿) ·s
(𝐴 ·s
𝑦𝑅)))) | 
| 204 | 193, 203 | mpbid 232 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝐴 -s 𝑥𝐿) ·s
1s ) <s ((𝐴
-s 𝑥𝐿) ·s
(𝐴 ·s
𝑦𝑅))) | 
| 205 | 187, 204 | eqbrtrrd 5167 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 -s 𝑥𝐿) <s ((𝐴 -s 𝑥𝐿)
·s (𝐴
·s 𝑦𝑅))) | 
| 206 | 156, 157 | negsubsdi2d 28110 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}) → ( -us
‘(𝑥𝐿 -s 𝐴)) = (𝐴 -s 𝑥𝐿)) | 
| 207 | 206 | adantrr 717 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( -us ‘(𝑥𝐿
-s 𝐴)) = (𝐴 -s 𝑥𝐿)) | 
| 208 | 159, 194 | mulnegs1d 28186 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (( -us ‘(𝑥𝐿
-s 𝐴))
·s (𝐴
·s 𝑦𝑅)) = ( -us
‘((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)))) | 
| 209 | 206 | oveq1d 7446 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}) → ((
-us ‘(𝑥𝐿 -s 𝐴)) ·s (𝐴 ·s 𝑦𝑅)) = ((𝐴 -s 𝑥𝐿)
·s (𝐴
·s 𝑦𝑅))) | 
| 210 | 209 | adantrr 717 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (( -us ‘(𝑥𝐿
-s 𝐴))
·s (𝐴
·s 𝑦𝑅)) = ((𝐴 -s 𝑥𝐿) ·s
(𝐴 ·s
𝑦𝑅))) | 
| 211 | 208, 210 | eqtr3d 2779 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( -us ‘((𝑥𝐿
-s 𝐴)
·s (𝐴
·s 𝑦𝑅))) = ((𝐴 -s 𝑥𝐿) ·s
(𝐴 ·s
𝑦𝑅))) | 
| 212 | 205, 207,
211 | 3brtr4d 5175 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( -us ‘(𝑥𝐿
-s 𝐴)) <s (
-us ‘((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)))) | 
| 213 | 159, 194 | mulscld 28161 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)) ∈
 No ) | 
| 214 | 213, 159 | sltnegd 28079 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)) <s
(𝑥𝐿
-s 𝐴) ↔ (
-us ‘(𝑥𝐿 -s 𝐴)) <s ( -us
‘((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))))) | 
| 215 | 212, 214 | mpbird 257 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)) <s
(𝑥𝐿
-s 𝐴)) | 
| 216 | 151, 213,
166 | sltaddsub2d 28122 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝐴 +s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))) <s
𝑥𝐿
↔ ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)) <s
(𝑥𝐿
-s 𝐴))) | 
| 217 | 215, 216 | mpbird 257 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 +s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))) <s
𝑥𝐿) | 
| 218 | 151, 152,
164 | addsdid 28182 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ( 1s
+s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))) =
((𝐴 ·s
1s ) +s (𝐴 ·s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)))) | 
| 219 | 151 | mulsridd 28140 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s 1s ) =
𝐴) | 
| 220 | 151, 159,
163 | muls12d 28207 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) = ((𝑥𝐿
-s 𝐴)
·s (𝐴
·s 𝑦𝑅))) | 
| 221 | 219, 220 | oveq12d 7449 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝐴 ·s 1s )
+s (𝐴
·s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))) = (𝐴 +s ((𝑥𝐿
-s 𝐴)
·s (𝐴
·s 𝑦𝑅)))) | 
| 222 | 218, 221 | eqtrd 2777 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ( 1s
+s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))) = (𝐴 +s ((𝑥𝐿
-s 𝐴)
·s (𝐴
·s 𝑦𝑅)))) | 
| 223 | 166 | mulsridd 28140 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝑥𝐿 ·s
1s ) = 𝑥𝐿) | 
| 224 | 217, 222,
223 | 3brtr4d 5175 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ( 1s
+s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))) <s
(𝑥𝐿
·s 1s )) | 
| 225 | 151, 165 | mulscld 28161 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ( 1s
+s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))) ∈
 No ) | 
| 226 | 170 | adantrr 717 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 0s <s 𝑥𝐿) | 
| 227 | 225, 152,
166, 226, 183 | sltdivmulwd 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 ))) | 
| 228 | 224, 227 | mpbird 257 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝐴 ·s ( 1s
+s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)))
/su 𝑥𝐿) <s 1s
) | 
| 229 | 184, 228 | eqbrtrrd 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 𝑥𝐿))) | 
| 231 | 230 | breq1d 5153 | . . . . . . . . . . . . 13
⊢ (𝑟 = (( 1s
+s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))
/su 𝑥𝐿) → ((𝐴 ·s 𝑟) <s 1s ↔
(𝐴 ·s ((
1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅))
/su 𝑥𝐿)) <s 1s
)) | 
| 232 | 229, 231 | syl5ibrcom 247 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝑟 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)
→ (𝐴
·s 𝑟)
<s 1s )) | 
| 233 | 232 | rexlimdvva 3213 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑟 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)
→ (𝐴
·s 𝑟)
<s 1s )) | 
| 234 | 150, 233 | 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 )) | 
| 235 | 74, 234 | 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 )) | 
| 236 | 71, 235 | sylbid 240 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝑟 ∈ (𝐿‘suc 𝑗) → (𝐴 ·s 𝑟) <s 1s )) | 
| 237 | 236 | ralrimiv 3145 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → ∀𝑟 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑟) <s 1s ) | 
| 238 | 38, 39, 40 | precsexlem5 28235 | . . . . . . . . . . . 12
⊢ (𝑗 ∈ ω → (𝑅‘suc 𝑗) = ((𝑅‘𝑗) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)}))) | 
| 239 | 238 | 3ad2ant2 1135 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝑅‘suc 𝑗) = ((𝑅‘𝑗) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)}))) | 
| 240 | 239 | eleq2d 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 𝑥𝐿))) | 
| 245 | 244 | 2rexbidv 3222 | . . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑠 → (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)
↔ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑠 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿))) | 
| 246 | 243, 245 | elab 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 𝑥𝑅))) | 
| 248 | 247 | 2rexbidv 3222 | . . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑠 → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)
↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑠 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅))) | 
| 249 | 243, 248 | elab 3679 | . . . . . . . . . . . . . 14
⊢ (𝑠 ∈ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)}
↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑠 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)) | 
| 250 | 246, 249 | 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
𝑥𝑅))) | 
| 251 | 242, 250 | 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
𝑥𝑅))) | 
| 252 | 251 | 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
𝑥𝑅)))) | 
| 253 | 241, 252 | 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
𝑥𝑅)))) | 
| 254 | 240, 253 | bitrdi 287 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝑠 ∈ (𝑅‘suc 𝑗) ↔ (𝑠 ∈ (𝑅‘𝑗) ∨ (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑠 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿) ∨
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑠 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅))))) | 
| 255 | 22 | rspccv 3619 | . . . . . . . . . . 11
⊢
(∀𝑐 ∈
(𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐) → (𝑠 ∈ (𝑅‘𝑗) → 1s <s (𝐴 ·s 𝑠))) | 
| 256 | 188, 255 | syl 17 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝑠 ∈ (𝑅‘𝑗) → 1s <s (𝐴 ·s 𝑠))) | 
| 257 | 122 | adantrl 716 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s 𝑦𝐿) <s 1s
) | 
| 258 | 75 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝐴 ∈  No
) | 
| 259 | 90 | adantrl 716 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑦𝐿 ∈  No ) | 
| 260 | 258, 259 | mulscld 28161 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s 𝑦𝐿) ∈  No ) | 
| 261 | 77 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 1s ∈  No ) | 
| 262 | 185 | adantrr 717 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 -s 𝑥𝐿) ∈  No ) | 
| 263 | 201 | adantrr 717 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 0s <s (𝐴 -s 𝑥𝐿)) | 
| 264 | 260, 261,
262, 263 | sltmul2d 28198 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 ·s 𝑦𝐿) <s 1s
↔ ((𝐴 -s
𝑥𝐿)
·s (𝐴
·s 𝑦𝐿)) <s ((𝐴 -s 𝑥𝐿)
·s 1s ))) | 
| 265 | 257, 264 | mpbid 232 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 -s 𝑥𝐿) ·s
(𝐴 ·s
𝑦𝐿))
<s ((𝐴 -s
𝑥𝐿)
·s 1s )) | 
| 266 | 262 | mulsridd 28140 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 -s 𝑥𝐿) ·s
1s ) = (𝐴
-s 𝑥𝐿)) | 
| 267 | 265, 266 | breqtrd 5169 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 -s 𝑥𝐿) ·s
(𝐴 ·s
𝑦𝐿))
<s (𝐴 -s
𝑥𝐿)) | 
| 268 | 158 | adantrr 717 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝑥𝐿 -s 𝐴) ∈ 
No ) | 
| 269 | 268, 260 | mulnegs1d 28186 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (( -us ‘(𝑥𝐿
-s 𝐴))
·s (𝐴
·s 𝑦𝐿)) = ( -us
‘((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)))) | 
| 270 | 206 | oveq1d 7446 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ 𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}) → ((
-us ‘(𝑥𝐿 -s 𝐴)) ·s (𝐴 ·s 𝑦𝐿)) = ((𝐴 -s 𝑥𝐿)
·s (𝐴
·s 𝑦𝐿))) | 
| 271 | 270 | adantrr 717 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (( -us ‘(𝑥𝐿
-s 𝐴))
·s (𝐴
·s 𝑦𝐿)) = ((𝐴 -s 𝑥𝐿) ·s
(𝐴 ·s
𝑦𝐿))) | 
| 272 | 269, 271 | eqtr3d 2779 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( -us ‘((𝑥𝐿
-s 𝐴)
·s (𝐴
·s 𝑦𝐿))) = ((𝐴 -s 𝑥𝐿) ·s
(𝐴 ·s
𝑦𝐿))) | 
| 273 | 206 | adantrr 717 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( -us ‘(𝑥𝐿
-s 𝐴)) = (𝐴 -s 𝑥𝐿)) | 
| 274 | 267, 272,
273 | 3brtr4d 5175 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( -us ‘((𝑥𝐿
-s 𝐴)
·s (𝐴
·s 𝑦𝐿))) <s ( -us
‘(𝑥𝐿 -s 𝐴))) | 
| 275 | 268, 260 | mulscld 28161 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)) ∈
 No ) | 
| 276 | 268, 275 | sltnegd 28079 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝐿 -s 𝐴) <s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)) ↔ (
-us ‘((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))) <s (
-us ‘(𝑥𝐿 -s 𝐴)))) | 
| 277 | 274, 276 | mpbird 257 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝑥𝐿 -s 𝐴) <s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿))) | 
| 278 | 156 | adantrr 717 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑥𝐿 ∈  No ) | 
| 279 | 278, 258,
275 | sltsubadd2d 28120 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝐿 -s 𝐴) <s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)) ↔
𝑥𝐿 <s
(𝐴 +s ((𝑥𝐿
-s 𝐴)
·s (𝐴
·s 𝑦𝐿))))) | 
| 280 | 277, 279 | mpbid 232 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑥𝐿 <s (𝐴 +s ((𝑥𝐿 -s 𝐴) ·s (𝐴 ·s 𝑦𝐿)))) | 
| 281 | 278 | mulslidd 28169 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( 1s
·s 𝑥𝐿) = 𝑥𝐿) | 
| 282 | 268, 259 | mulscld 28161 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿) ∈
 No ) | 
| 283 | 258, 261,
282 | addsdid 28182 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ( 1s
+s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))) = ((𝐴 ·s
1s ) +s (𝐴 ·s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)))) | 
| 284 | 258 | mulsridd 28140 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s 1s ) =
𝐴) | 
| 285 | 258, 268,
259 | muls12d 28207 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) = ((𝑥𝐿
-s 𝐴)
·s (𝐴
·s 𝑦𝐿))) | 
| 286 | 284, 285 | oveq12d 7449 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 ·s 1s )
+s (𝐴
·s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))) = (𝐴 +s ((𝑥𝐿
-s 𝐴)
·s (𝐴
·s 𝑦𝐿)))) | 
| 287 | 283, 286 | eqtrd 2777 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ( 1s
+s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))) = (𝐴 +s ((𝑥𝐿
-s 𝐴)
·s (𝐴
·s 𝑦𝐿)))) | 
| 288 | 280, 281,
287 | 3brtr4d 5175 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( 1s
·s 𝑥𝐿) <s (𝐴 ·s (
1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)))) | 
| 289 | 261, 282 | addscld 28013 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ( 1s +s
((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) ∈  No ) | 
| 290 | 258, 289 | mulscld 28161 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝐴 ·s ( 1s
+s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))) ∈
 No ) | 
| 291 | 170 | adantrr 717 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 0s <s 𝑥𝐿) | 
| 292 | 182 | adantrr 717 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ∃𝑦 ∈  No 
(𝑥𝐿
·s 𝑦) =
1s ) | 
| 293 | 261, 290,
278, 291, 292 | sltmuldivwd 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 𝑥𝐿))) | 
| 294 | 288, 293 | mpbid 232 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 1s <s ((𝐴 ·s (
1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)))
/su 𝑥𝐿)) | 
| 295 | 171 | adantrr 717 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → 𝑥𝐿 ≠ 0s
) | 
| 296 | 258, 289,
278, 295, 292 | divsasswd 28228 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → ((𝐴 ·s ( 1s
+s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)))
/su 𝑥𝐿) = (𝐴 ·s (( 1s
+s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))
/su 𝑥𝐿))) | 
| 297 | 294, 296 | breqtrd 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 𝑥𝐿))) | 
| 299 | 298 | breq2d 5155 | . . . . . . . . . . . . 13
⊢ (𝑠 = (( 1s
+s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))
/su 𝑥𝐿) → ( 1s
<s (𝐴
·s 𝑠)
↔ 1s <s (𝐴 ·s (( 1s
+s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿))
/su 𝑥𝐿)))) | 
| 300 | 297, 299 | syl5ibrcom 247 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥} ∧ 𝑦𝐿 ∈ (𝐿‘𝑗))) → (𝑠 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)
→ 1s <s (𝐴 ·s 𝑠))) | 
| 301 | 300 | rexlimdvva 3213 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑗)𝑠 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)
→ 1s <s (𝐴 ·s 𝑠))) | 
| 302 | 83 | adantrr 717 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝑥𝑅 -s 𝐴) ∈ 
No ) | 
| 303 | 302 | mulsridd 28140 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s
1s ) = (𝑥𝑅 -s 𝐴)) | 
| 304 | 192 | adantrl 716 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 1s <s (𝐴 ·s 𝑦𝑅)) | 
| 305 | 77 | a1i 11 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 1s ∈  No ) | 
| 306 | 75 | adantr 480 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝐴 ∈  No
) | 
| 307 | 162 | adantrl 716 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑦𝑅 ∈  No ) | 
| 308 | 306, 307 | mulscld 28161 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s 𝑦𝑅) ∈  No ) | 
| 309 | 126 | adantrr 717 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 0s <s (𝑥𝑅
-s 𝐴)) | 
| 310 | 305, 308,
302, 309 | sltmul2d 28198 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( 1s <s (𝐴 ·s 𝑦𝑅) ↔
((𝑥𝑅
-s 𝐴)
·s 1s ) <s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)))) | 
| 311 | 304, 310 | mpbid 232 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s
1s ) <s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))) | 
| 312 | 303, 311 | eqbrtrrd 5167 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝑥𝑅 -s 𝐴) <s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅))) | 
| 313 | 81 | adantrr 717 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑥𝑅 ∈  No ) | 
| 314 | 302, 308 | mulscld 28161 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)) ∈
 No ) | 
| 315 | 313, 306,
314 | sltsubadd2d 28120 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝑥𝑅 -s 𝐴) <s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)) ↔
𝑥𝑅 <s
(𝐴 +s ((𝑥𝑅
-s 𝐴)
·s (𝐴
·s 𝑦𝑅))))) | 
| 316 | 312, 315 | mpbid 232 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑥𝑅 <s (𝐴 +s ((𝑥𝑅 -s 𝐴) ·s (𝐴 ·s 𝑦𝑅)))) | 
| 317 | 313 | mulslidd 28169 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( 1s
·s 𝑥𝑅) = 𝑥𝑅) | 
| 318 | 302, 307 | mulscld 28161 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅) ∈
 No ) | 
| 319 | 306, 305,
318 | addsdid 28182 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ( 1s
+s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))) =
((𝐴 ·s
1s ) +s (𝐴 ·s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)))) | 
| 320 | 306 | mulsridd 28140 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s 1s ) =
𝐴) | 
| 321 | 306, 302,
307 | muls12d 28207 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) = ((𝑥𝑅
-s 𝐴)
·s (𝐴
·s 𝑦𝑅))) | 
| 322 | 320, 321 | oveq12d 7449 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝐴 ·s 1s )
+s (𝐴
·s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))) = (𝐴 +s ((𝑥𝑅
-s 𝐴)
·s (𝐴
·s 𝑦𝑅)))) | 
| 323 | 319, 322 | eqtrd 2777 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ( 1s
+s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))) = (𝐴 +s ((𝑥𝑅
-s 𝐴)
·s (𝐴
·s 𝑦𝑅)))) | 
| 324 | 316, 317,
323 | 3brtr4d 5175 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( 1s
·s 𝑥𝑅) <s (𝐴 ·s (
1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)))) | 
| 325 | 305, 318 | addscld 28013 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ( 1s +s
((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) ∈  No ) | 
| 326 | 306, 325 | mulscld 28161 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝐴 ·s ( 1s
+s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))) ∈
 No ) | 
| 327 | 103 | adantrr 717 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 0s <s 𝑥𝑅) | 
| 328 | 116 | adantrr 717 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ∃𝑦 ∈  No 
(𝑥𝑅
·s 𝑦) =
1s ) | 
| 329 | 305, 326,
313, 327, 328 | sltmuldivwd 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 𝑥𝑅))) | 
| 330 | 324, 329 | mpbid 232 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 1s <s ((𝐴 ·s (
1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)))
/su 𝑥𝑅)) | 
| 331 | 104 | adantrr 717 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → 𝑥𝑅 ≠ 0s
) | 
| 332 | 306, 325,
313, 331, 328 | divsasswd 28228 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → ((𝐴 ·s ( 1s
+s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)))
/su 𝑥𝑅) = (𝐴 ·s (( 1s
+s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))
/su 𝑥𝑅))) | 
| 333 | 330, 332 | breqtrd 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 𝑥𝑅))) | 
| 335 | 334 | breq2d 5155 | . . . . . . . . . . . . 13
⊢ (𝑠 = (( 1s
+s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))
/su 𝑥𝑅) → ( 1s
<s (𝐴
·s 𝑠)
↔ 1s <s (𝐴 ·s (( 1s
+s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅))
/su 𝑥𝑅)))) | 
| 336 | 333, 335 | syl5ibrcom 247 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑦𝑅 ∈ (𝑅‘𝑗))) → (𝑠 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)
→ 1s <s (𝐴 ·s 𝑠))) | 
| 337 | 336 | rexlimdvva 3213 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑗)𝑠 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)
→ 1s <s (𝐴 ·s 𝑠))) | 
| 338 | 301, 337 | 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 𝑠))) | 
| 339 | 256, 338 | 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 𝑠))) | 
| 340 | 254, 339 | sylbid 240 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝑠 ∈ (𝑅‘suc 𝑗) → 1s <s (𝐴 ·s 𝑠))) | 
| 341 | 340 | ralrimiv 3145 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → ∀𝑠 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑠)) | 
| 342 | 237, 341 | jca 511 | . . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ω ∧ (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (∀𝑟 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑟) <s 1s ∧ ∀𝑠 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑠))) | 
| 343 | 342 | 3exp 1120 | . . . . 5
⊢ (𝜑 → (𝑗 ∈ ω → ((∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐)) → (∀𝑟 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑟) <s 1s ∧ ∀𝑠 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑠))))) | 
| 344 | 343 | com12 32 | . . . 4
⊢ (𝑗 ∈ ω → (𝜑 → ((∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐)) → (∀𝑟 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑟) <s 1s ∧ ∀𝑠 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑠))))) | 
| 345 | 344 | a2d 29 | . . 3
⊢ (𝑗 ∈ ω → ((𝜑 → (∀𝑏 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑐))) → (𝜑 → (∀𝑟 ∈ (𝐿‘suc 𝑗)(𝐴 ·s 𝑟) <s 1s ∧ ∀𝑠 ∈ (𝑅‘suc 𝑗) 1s <s (𝐴 ·s 𝑠))))) | 
| 346 | 6, 12, 26, 32, 54, 345 | finds 7918 | . 2
⊢ (𝐼 ∈ ω → (𝜑 → (∀𝑏 ∈ (𝐿‘𝐼)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝐼) 1s <s (𝐴 ·s 𝑐)))) | 
| 347 | 346 | impcom 407 | 1
⊢ ((𝜑 ∧ 𝐼 ∈ ω) → (∀𝑏 ∈ (𝐿‘𝐼)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝐼) 1s <s (𝐴 ·s 𝑐))) |