Metamath Proof Explorer

Theorem precsexlem9

Description: Lemma for surreal reciprocal. Show that the product of A and a left element is less than one and the product of A and a right element is greater than one. (Contributed by Scott Fenton, 14-Mar-2025)

Ref Expression
Hypotheses 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 precsexlem9 ( ( 𝜑 ∧ 𝐼 ∈ ω ) → ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝐼 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝐼 ) 1s <s ( 𝐴 ·s 𝑐 ) ) )

Proof

Step Hyp Ref Expression
1 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 } , ∅ ⟩ )
2 precsexlem.2 ⊢ 𝐿 = ( 1st ∘ 𝐹 )
3 precsexlem.3 ⊢ 𝑅 = ( 2nd ∘ 𝐹 )
4 precsexlem.4 ⊢ ( 𝜑 → 𝐴 ∈ No )
5 precsexlem.5 ⊢ ( 𝜑 → 0s <s 𝐴 )
6 precsexlem.6 ⊢ ( 𝜑 → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ( 0s <s 𝑥𝑂 → ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) )
7 fveq2 ⊢ ( 𝑖 = ∅ → ( 𝐿 ‘ 𝑖 ) = ( 𝐿 ‘ ∅ ) )
8 7 raleqdv ⊢ ( 𝑖 = ∅ → ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑖 ) ( 𝐴 ·s 𝑏 ) <s 1s ↔ ∀ 𝑏 ∈ ( 𝐿 ‘ ∅ ) ( 𝐴 ·s 𝑏 ) <s 1s ) )
9 fveq2 ⊢ ( 𝑖 = ∅ → ( 𝑅 ‘ 𝑖 ) = ( 𝑅 ‘ ∅ ) )
10 9 raleqdv ⊢ ( 𝑖 = ∅ → ( ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑖 ) 1s <s ( 𝐴 ·s 𝑐 ) ↔ ∀ 𝑐 ∈ ( 𝑅 ‘ ∅ ) 1s <s ( 𝐴 ·s 𝑐 ) ) )
11 8 10 anbi12d ⊢ ( 𝑖 = ∅ → ( ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑖 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑖 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ↔ ( ∀ 𝑏 ∈ ( 𝐿 ‘ ∅ ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ ∅ ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) )
12 11 imbi2d ⊢ ( 𝑖 = ∅ → ( ( 𝜑 → ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑖 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑖 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ↔ ( 𝜑 → ( ∀ 𝑏 ∈ ( 𝐿 ‘ ∅ ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ ∅ ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ) )
13 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝐿 ‘ 𝑖 ) = ( 𝐿 ‘ 𝑗 ) )
14 13 raleqdv ⊢ ( 𝑖 = 𝑗 → ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑖 ) ( 𝐴 ·s 𝑏 ) <s 1s ↔ ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ) )
15 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝑅 ‘ 𝑖 ) = ( 𝑅 ‘ 𝑗 ) )
16 15 raleqdv ⊢ ( 𝑖 = 𝑗 → ( ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑖 ) 1s <s ( 𝐴 ·s 𝑐 ) ↔ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) )
17 14 16 anbi12d ⊢ ( 𝑖 = 𝑗 → ( ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑖 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑖 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ↔ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) )
18 17 imbi2d ⊢ ( 𝑖 = 𝑗 → ( ( 𝜑 → ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑖 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑖 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ↔ ( 𝜑 → ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ) )
19 fveq2 ⊢ ( 𝑖 = suc 𝑗 → ( 𝐿 ‘ 𝑖 ) = ( 𝐿 ‘ suc 𝑗 ) )
20 19 raleqdv ⊢ ( 𝑖 = suc 𝑗 → ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑖 ) ( 𝐴 ·s 𝑏 ) <s 1s ↔ ∀ 𝑏 ∈ ( 𝐿 ‘ suc 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ) )
21 fveq2 ⊢ ( 𝑖 = suc 𝑗 → ( 𝑅 ‘ 𝑖 ) = ( 𝑅 ‘ suc 𝑗 ) )
22 21 raleqdv ⊢ ( 𝑖 = suc 𝑗 → ( ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑖 ) 1s <s ( 𝐴 ·s 𝑐 ) ↔ ∀ 𝑐 ∈ ( 𝑅 ‘ suc 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) )
23 20 22 anbi12d ⊢ ( 𝑖 = suc 𝑗 → ( ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑖 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑖 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ↔ ( ∀ 𝑏 ∈ ( 𝐿 ‘ suc 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ suc 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) )
24 oveq2 ⊢ ( 𝑏 = 𝑟 → ( 𝐴 ·s 𝑏 ) = ( 𝐴 ·s 𝑟 ) )
25 24 breq1d ⊢ ( 𝑏 = 𝑟 → ( ( 𝐴 ·s 𝑏 ) <s 1s ↔ ( 𝐴 ·s 𝑟 ) <s 1s ) )
26 25 cbvralvw ⊢ ( ∀ 𝑏 ∈ ( 𝐿 ‘ suc 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ↔ ∀ 𝑟 ∈ ( 𝐿 ‘ suc 𝑗 ) ( 𝐴 ·s 𝑟 ) <s 1s )
27 oveq2 ⊢ ( 𝑐 = 𝑠 → ( 𝐴 ·s 𝑐 ) = ( 𝐴 ·s 𝑠 ) )
28 27 breq2d ⊢ ( 𝑐 = 𝑠 → ( 1s <s ( 𝐴 ·s 𝑐 ) ↔ 1s <s ( 𝐴 ·s 𝑠 ) ) )
29 28 cbvralvw ⊢ ( ∀ 𝑐 ∈ ( 𝑅 ‘ suc 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ↔ ∀ 𝑠 ∈ ( 𝑅 ‘ suc 𝑗 ) 1s <s ( 𝐴 ·s 𝑠 ) )
30 26 29 anbi12i ⊢ ( ( ∀ 𝑏 ∈ ( 𝐿 ‘ suc 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ suc 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ↔ ( ∀ 𝑟 ∈ ( 𝐿 ‘ suc 𝑗 ) ( 𝐴 ·s 𝑟 ) <s 1s ∧ ∀ 𝑠 ∈ ( 𝑅 ‘ suc 𝑗 ) 1s <s ( 𝐴 ·s 𝑠 ) ) )
31 23 30 bitrdi ⊢ ( 𝑖 = suc 𝑗 → ( ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑖 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑖 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ↔ ( ∀ 𝑟 ∈ ( 𝐿 ‘ suc 𝑗 ) ( 𝐴 ·s 𝑟 ) <s 1s ∧ ∀ 𝑠 ∈ ( 𝑅 ‘ suc 𝑗 ) 1s <s ( 𝐴 ·s 𝑠 ) ) ) )
32 31 imbi2d ⊢ ( 𝑖 = suc 𝑗 → ( ( 𝜑 → ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑖 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑖 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ↔ ( 𝜑 → ( ∀ 𝑟 ∈ ( 𝐿 ‘ suc 𝑗 ) ( 𝐴 ·s 𝑟 ) <s 1s ∧ ∀ 𝑠 ∈ ( 𝑅 ‘ suc 𝑗 ) 1s <s ( 𝐴 ·s 𝑠 ) ) ) ) )
33 fveq2 ⊢ ( 𝑖 = 𝐼 → ( 𝐿 ‘ 𝑖 ) = ( 𝐿 ‘ 𝐼 ) )
34 33 raleqdv ⊢ ( 𝑖 = 𝐼 → ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑖 ) ( 𝐴 ·s 𝑏 ) <s 1s ↔ ∀ 𝑏 ∈ ( 𝐿 ‘ 𝐼 ) ( 𝐴 ·s 𝑏 ) <s 1s ) )
35 fveq2 ⊢ ( 𝑖 = 𝐼 → ( 𝑅 ‘ 𝑖 ) = ( 𝑅 ‘ 𝐼 ) )
36 35 raleqdv ⊢ ( 𝑖 = 𝐼 → ( ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑖 ) 1s <s ( 𝐴 ·s 𝑐 ) ↔ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝐼 ) 1s <s ( 𝐴 ·s 𝑐 ) ) )
37 34 36 anbi12d ⊢ ( 𝑖 = 𝐼 → ( ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑖 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑖 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ↔ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝐼 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝐼 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) )
38 37 imbi2d ⊢ ( 𝑖 = 𝐼 → ( ( 𝜑 → ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑖 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑖 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ↔ ( 𝜑 → ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝐼 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝐼 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ) )
39 muls01 ⊢ ( 𝐴 ∈ No → ( 𝐴 ·s 0s ) = 0s )
40 4 39 syl ⊢ ( 𝜑 → ( 𝐴 ·s 0s ) = 0s )
41 0slt1s ⊢ 0s <s 1s
42 40 41 eqbrtrdi ⊢ ( 𝜑 → ( 𝐴 ·s 0s ) <s 1s )
43 1 2 3 precsexlem1 ⊢ ( 𝐿 ‘ ∅ ) = { 0s }
44 43 raleqi ⊢ ( ∀ 𝑏 ∈ ( 𝐿 ‘ ∅ ) ( 𝐴 ·s 𝑏 ) <s 1s ↔ ∀ 𝑏 ∈ { 0s } ( 𝐴 ·s 𝑏 ) <s 1s )
45 0sno ⊢ 0s ∈ No
46 45 elexi ⊢ 0s ∈ V
47 oveq2 ⊢ ( 𝑏 = 0s → ( 𝐴 ·s 𝑏 ) = ( 𝐴 ·s 0s ) )
48 47 breq1d ⊢ ( 𝑏 = 0s → ( ( 𝐴 ·s 𝑏 ) <s 1s ↔ ( 𝐴 ·s 0s ) <s 1s ) )
49 46 48 ralsn ⊢ ( ∀ 𝑏 ∈ { 0s } ( 𝐴 ·s 𝑏 ) <s 1s ↔ ( 𝐴 ·s 0s ) <s 1s )
50 44 49 bitri ⊢ ( ∀ 𝑏 ∈ ( 𝐿 ‘ ∅ ) ( 𝐴 ·s 𝑏 ) <s 1s ↔ ( 𝐴 ·s 0s ) <s 1s )
51 42 50 sylibr ⊢ ( 𝜑 → ∀ 𝑏 ∈ ( 𝐿 ‘ ∅ ) ( 𝐴 ·s 𝑏 ) <s 1s )
52 ral0 ⊢ ∀ 𝑐 ∈ ∅ 1s <s ( 𝐴 ·s 𝑐 )
53 1 2 3 precsexlem2 ⊢ ( 𝑅 ‘ ∅ ) = ∅
54 53 raleqi ⊢ ( ∀ 𝑐 ∈ ( 𝑅 ‘ ∅ ) 1s <s ( 𝐴 ·s 𝑐 ) ↔ ∀ 𝑐 ∈ ∅ 1s <s ( 𝐴 ·s 𝑐 ) )
55 52 54 mpbir ⊢ ∀ 𝑐 ∈ ( 𝑅 ‘ ∅ ) 1s <s ( 𝐴 ·s 𝑐 )
56 51 55 jctir ⊢ ( 𝜑 → ( ∀ 𝑏 ∈ ( 𝐿 ‘ ∅ ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ ∅ ) 1s <s ( 𝐴 ·s 𝑐 ) ) )
57 1 2 3 precsexlem4 ⊢ ( 𝑗 ∈ ω → ( 𝐿 ‘ suc 𝑗 ) = ( ( 𝐿 ‘ 𝑗 ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) } ) ) )
58 57 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ( 𝐿 ‘ suc 𝑗 ) = ( ( 𝐿 ‘ 𝑗 ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) } ) ) )
59 58 eleq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ( 𝑟 ∈ ( 𝐿 ‘ suc 𝑗 ) ↔ 𝑟 ∈ ( ( 𝐿 ‘ 𝑗 ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) } ) ) ) )
60 elun ⊢ ( 𝑟 ∈ ( ( 𝐿 ‘ 𝑗 ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( 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 𝑥𝐿 ) } ) ) )
61 elun ⊢ ( 𝑟 ∈ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( 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 𝑥𝐿 ) } ) )
62 vex ⊢ 𝑟 ∈ V
63 eqeq1 ⊢ ( 𝑎 = 𝑟 → ( 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) ↔ 𝑟 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) ) )
64 63 2rexbidv ⊢ ( 𝑎 = 𝑟 → ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) ↔ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑟 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) ) )
65 62 64 elab ⊢ ( 𝑟 ∈ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) } ↔ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑟 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) )
66 eqeq1 ⊢ ( 𝑎 = 𝑟 → ( 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) ↔ 𝑟 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) ) )
67 66 2rexbidv ⊢ ( 𝑎 = 𝑟 → ( ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) ↔ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑟 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) ) )
68 62 67 elab ⊢ ( 𝑟 ∈ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) } ↔ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑟 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) )
69 65 68 orbi12i ⊢ ( ( 𝑟 ∈ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( 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 61 69 bitri ⊢ ( 𝑟 ∈ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( 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 70 orbi2i ⊢ ( ( 𝑟 ∈ ( 𝐿 ‘ 𝑗 ) ∨ 𝑟 ∈ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( 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 𝑥𝐿 ) ) ) )
72 60 71 bitri ⊢ ( 𝑟 ∈ ( ( 𝐿 ‘ 𝑗 ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( 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 𝑥𝐿 ) ) ) )
73 59 72 bitrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ( 𝑟 ∈ ( 𝐿 ‘ suc 𝑗 ) ↔ ( 𝑟 ∈ ( 𝐿 ‘ 𝑗 ) ∨ ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑟 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) ∨ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑟 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) ) ) ) )
74 simp3l ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s )
75 25 rspccv ⊢ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s → ( 𝑟 ∈ ( 𝐿 ‘ 𝑗 ) → ( 𝐴 ·s 𝑟 ) <s 1s ) )
76 74 75 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ( 𝑟 ∈ ( 𝐿 ‘ 𝑗 ) → ( 𝐴 ·s 𝑟 ) <s 1s ) )
77 4 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → 𝐴 ∈ No )
78 77 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 𝐴 ∈ No )
79 1sno ⊢ 1s ∈ No
80 79 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 1s ∈ No )
81 rightssno ⊢ ( R ‘ 𝐴 ) ⊆ No
82 81 sseli ⊢ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) → 𝑥𝑅 ∈ No )
83 82 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ) → 𝑥𝑅 ∈ No )
84 77 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ) → 𝐴 ∈ No )
85 83 84 subscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ) → ( 𝑥𝑅 -s 𝐴 ) ∈ No )
86 85 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝑥𝑅 -s 𝐴 ) ∈ No )
87 1 2 3 4 5 6 precsexlem8 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ) → ( ( 𝐿 ‘ 𝑗 ) ⊆ No ∧ ( 𝑅 ‘ 𝑗 ) ⊆ No ) )
88 87 simpld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ) → ( 𝐿 ‘ 𝑗 ) ⊆ No )
89 88 3adant3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ( 𝐿 ‘ 𝑗 ) ⊆ No )
90 89 sselda ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) → 𝑦𝐿 ∈ No )
91 90 adantrl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 𝑦𝐿 ∈ No )
92 86 91 mulscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ∈ No )
93 80 92 addscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) ∈ No )
94 83 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 𝑥𝑅 ∈ No )
95 45 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ) → 0s ∈ No )
96 5 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → 0s <s 𝐴 )
97 96 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ) → 0s <s 𝐴 )
98 rightgt ⊢ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) → 𝐴 <s 𝑥𝑅 )
99 98 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ) → 𝐴 <s 𝑥𝑅 )
100 95 84 83 97 99 slttrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ) → 0s <s 𝑥𝑅 )
101 100 sgt0ne0d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ) → 𝑥𝑅 ≠ 0s )
102 101 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 𝑥𝑅 ≠ 0s )
103 breq2 ⊢ ( 𝑥𝑂 = 𝑥𝑅 → ( 0s <s 𝑥𝑂 ↔ 0s <s 𝑥𝑅 ) )
104 oveq1 ⊢ ( 𝑥𝑂 = 𝑥𝑅 → ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑥𝑅 ·s 𝑦 ) )
105 104 eqeq1d ⊢ ( 𝑥𝑂 = 𝑥𝑅 → ( ( 𝑥𝑂 ·s 𝑦 ) = 1s ↔ ( 𝑥𝑅 ·s 𝑦 ) = 1s ) )
106 105 rexbidv ⊢ ( 𝑥𝑂 = 𝑥𝑅 → ( ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ↔ ∃ 𝑦 ∈ No ( 𝑥𝑅 ·s 𝑦 ) = 1s ) )
107 103 106 imbi12d ⊢ ( 𝑥𝑂 = 𝑥𝑅 → ( ( 0s <s 𝑥𝑂 → ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) ↔ ( 0s <s 𝑥𝑅 → ∃ 𝑦 ∈ No ( 𝑥𝑅 ·s 𝑦 ) = 1s ) ) )
108 6 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ( 0s <s 𝑥𝑂 → ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) )
109 108 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ( 0s <s 𝑥𝑂 → ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) )
110 elun2 ⊢ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) → 𝑥𝑅 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
111 110 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ) → 𝑥𝑅 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
112 107 109 111 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ) → ( 0s <s 𝑥𝑅 → ∃ 𝑦 ∈ No ( 𝑥𝑅 ·s 𝑦 ) = 1s ) )
113 100 112 mpd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ) → ∃ 𝑦 ∈ No ( 𝑥𝑅 ·s 𝑦 ) = 1s )
114 113 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ∃ 𝑦 ∈ No ( 𝑥𝑅 ·s 𝑦 ) = 1s )
115 78 93 94 102 114 divsasswd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 𝐴 ·s ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) ) /su 𝑥𝑅 ) = ( 𝐴 ·s ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) ) )
116 oveq2 ⊢ ( 𝑏 = 𝑦𝐿 → ( 𝐴 ·s 𝑏 ) = ( 𝐴 ·s 𝑦𝐿 ) )
117 116 breq1d ⊢ ( 𝑏 = 𝑦𝐿 → ( ( 𝐴 ·s 𝑏 ) <s 1s ↔ ( 𝐴 ·s 𝑦𝐿 ) <s 1s ) )
118 117 rspccva ⊢ ( ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) → ( 𝐴 ·s 𝑦𝐿 ) <s 1s )
119 74 118 sylan ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) → ( 𝐴 ·s 𝑦𝐿 ) <s 1s )
120 119 adantrl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝐴 ·s 𝑦𝐿 ) <s 1s )
121 78 91 mulscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝐴 ·s 𝑦𝐿 ) ∈ No )
122 84 83 posdifsd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ) → ( 𝐴 <s 𝑥𝑅 ↔ 0s <s ( 𝑥𝑅 -s 𝐴 ) ) )
123 99 122 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ) → 0s <s ( 𝑥𝑅 -s 𝐴 ) )
124 123 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 0s <s ( 𝑥𝑅 -s 𝐴 ) )
125 121 80 86 124 sltmul2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 𝐴 ·s 𝑦𝐿 ) <s 1s ↔ ( ( 𝑥𝑅 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) <s ( ( 𝑥𝑅 -s 𝐴 ) ·s 1s ) ) )
126 120 125 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 𝑥𝑅 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) <s ( ( 𝑥𝑅 -s 𝐴 ) ·s 1s ) )
127 86 mulsridd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 𝑥𝑅 -s 𝐴 ) ·s 1s ) = ( 𝑥𝑅 -s 𝐴 ) )
128 126 127 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 𝑥𝑅 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) <s ( 𝑥𝑅 -s 𝐴 ) )
129 86 121 mulscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 𝑥𝑅 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) ∈ No )
130 78 129 94 sltaddsub2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 𝐴 +s ( ( 𝑥𝑅 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) ) <s 𝑥𝑅 ↔ ( ( 𝑥𝑅 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) <s ( 𝑥𝑅 -s 𝐴 ) ) )
131 128 130 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝐴 +s ( ( 𝑥𝑅 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) ) <s 𝑥𝑅 )
132 78 80 92 addsdid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝐴 ·s ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) ) = ( ( 𝐴 ·s 1s ) +s ( 𝐴 ·s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) ) )
133 78 mulsridd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝐴 ·s 1s ) = 𝐴 )
134 78 86 91 muls12d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝐴 ·s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) = ( ( 𝑥𝑅 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) )
135 133 134 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 𝐴 ·s 1s ) +s ( 𝐴 ·s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) ) = ( 𝐴 +s ( ( 𝑥𝑅 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) ) )
136 132 135 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝐴 ·s ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) ) = ( 𝐴 +s ( ( 𝑥𝑅 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) ) )
137 94 mulslidd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 1s ·s 𝑥𝑅 ) = 𝑥𝑅 )
138 131 136 137 3brtr4d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝐴 ·s ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) ) <s ( 1s ·s 𝑥𝑅 ) )
139 78 93 mulscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝐴 ·s ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) ) ∈ No )
140 100 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 0s <s 𝑥𝑅 )
141 139 80 94 140 114 sltdivmul2wd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( ( 𝐴 ·s ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) ) /su 𝑥𝑅 ) <s 1s ↔ ( 𝐴 ·s ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) ) <s ( 1s ·s 𝑥𝑅 ) ) )
142 138 141 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 𝐴 ·s ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) ) /su 𝑥𝑅 ) <s 1s )
143 115 142 eqbrtrrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝐴 ·s ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) ) <s 1s )
144 oveq2 ⊢ ( 𝑟 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) → ( 𝐴 ·s 𝑟 ) = ( 𝐴 ·s ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) ) )
145 144 breq1d ⊢ ( 𝑟 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) → ( ( 𝐴 ·s 𝑟 ) <s 1s ↔ ( 𝐴 ·s ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) ) <s 1s ) )
146 143 145 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝑟 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) → ( 𝐴 ·s 𝑟 ) <s 1s ) )
147 146 rexlimdvva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑟 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) → ( 𝐴 ·s 𝑟 ) <s 1s ) )
148 77 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝐴 ∈ No )
149 79 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 1s ∈ No )
150 leftssno ⊢ ( L ‘ 𝐴 ) ⊆ No
151 elrabi ⊢ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } → 𝑥𝐿 ∈ ( L ‘ 𝐴 ) )
152 151 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → 𝑥𝐿 ∈ ( L ‘ 𝐴 ) )
153 150 152 sselid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → 𝑥𝐿 ∈ No )
154 77 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → 𝐴 ∈ No )
155 153 154 subscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → ( 𝑥𝐿 -s 𝐴 ) ∈ No )
156 155 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝑥𝐿 -s 𝐴 ) ∈ No )
157 87 simprd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ) → ( 𝑅 ‘ 𝑗 ) ⊆ No )
158 157 3adant3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ( 𝑅 ‘ 𝑗 ) ⊆ No )
159 158 sselda ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) → 𝑦𝑅 ∈ No )
160 159 adantrl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝑦𝑅 ∈ No )
161 156 160 mulscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ∈ No )
162 149 161 addscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) ∈ No )
163 153 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝑥𝐿 ∈ No )
164 breq2 ⊢ ( 𝑥 = 𝑥𝐿 → ( 0s <s 𝑥 ↔ 0s <s 𝑥𝐿 ) )
165 164 elrab ⊢ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ↔ ( 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ∧ 0s <s 𝑥𝐿 ) )
166 165 simprbi ⊢ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } → 0s <s 𝑥𝐿 )
167 166 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → 0s <s 𝑥𝐿 )
168 167 sgt0ne0d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → 𝑥𝐿 ≠ 0s )
169 168 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝑥𝐿 ≠ 0s )
170 breq2 ⊢ ( 𝑥𝑂 = 𝑥𝐿 → ( 0s <s 𝑥𝑂 ↔ 0s <s 𝑥𝐿 ) )
171 oveq1 ⊢ ( 𝑥𝑂 = 𝑥𝐿 → ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑥𝐿 ·s 𝑦 ) )
172 171 eqeq1d ⊢ ( 𝑥𝑂 = 𝑥𝐿 → ( ( 𝑥𝑂 ·s 𝑦 ) = 1s ↔ ( 𝑥𝐿 ·s 𝑦 ) = 1s ) )
173 172 rexbidv ⊢ ( 𝑥𝑂 = 𝑥𝐿 → ( ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ↔ ∃ 𝑦 ∈ No ( 𝑥𝐿 ·s 𝑦 ) = 1s ) )
174 170 173 imbi12d ⊢ ( 𝑥𝑂 = 𝑥𝐿 → ( ( 0s <s 𝑥𝑂 → ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) ↔ ( 0s <s 𝑥𝐿 → ∃ 𝑦 ∈ No ( 𝑥𝐿 ·s 𝑦 ) = 1s ) ) )
175 108 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ( 0s <s 𝑥𝑂 → ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) )
176 elun1 ⊢ ( 𝑥𝐿 ∈ ( L ‘ 𝐴 ) → 𝑥𝐿 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
177 152 176 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → 𝑥𝐿 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
178 174 175 177 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → ( 0s <s 𝑥𝐿 → ∃ 𝑦 ∈ No ( 𝑥𝐿 ·s 𝑦 ) = 1s ) )
179 167 178 mpd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → ∃ 𝑦 ∈ No ( 𝑥𝐿 ·s 𝑦 ) = 1s )
180 179 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ∃ 𝑦 ∈ No ( 𝑥𝐿 ·s 𝑦 ) = 1s )
181 148 162 163 169 180 divsasswd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( 𝐴 ·s ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) ) /su 𝑥𝐿 ) = ( 𝐴 ·s ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) ) )
182 154 153 subscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → ( 𝐴 -s 𝑥𝐿 ) ∈ No )
183 182 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝐴 -s 𝑥𝐿 ) ∈ No )
184 183 mulsridd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( 𝐴 -s 𝑥𝐿 ) ·s 1s ) = ( 𝐴 -s 𝑥𝐿 ) )
185 simp3r ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) )
186 oveq2 ⊢ ( 𝑐 = 𝑦𝑅 → ( 𝐴 ·s 𝑐 ) = ( 𝐴 ·s 𝑦𝑅 ) )
187 186 breq2d ⊢ ( 𝑐 = 𝑦𝑅 → ( 1s <s ( 𝐴 ·s 𝑐 ) ↔ 1s <s ( 𝐴 ·s 𝑦𝑅 ) ) )
188 187 rspccva ⊢ ( ( ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) → 1s <s ( 𝐴 ·s 𝑦𝑅 ) )
189 185 188 sylan ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) → 1s <s ( 𝐴 ·s 𝑦𝑅 ) )
190 189 adantrl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 1s <s ( 𝐴 ·s 𝑦𝑅 ) )
191 148 160 mulscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝐴 ·s 𝑦𝑅 ) ∈ No )
192 leftlt ⊢ ( 𝑥𝐿 ∈ ( L ‘ 𝐴 ) → 𝑥𝐿 <s 𝐴 )
193 152 192 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → 𝑥𝐿 <s 𝐴 )
194 153 154 posdifsd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → ( 𝑥𝐿 <s 𝐴 ↔ 0s <s ( 𝐴 -s 𝑥𝐿 ) ) )
195 193 194 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → 0s <s ( 𝐴 -s 𝑥𝐿 ) )
196 195 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 0s <s ( 𝐴 -s 𝑥𝐿 ) )
197 149 191 183 196 sltmul2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 1s <s ( 𝐴 ·s 𝑦𝑅 ) ↔ ( ( 𝐴 -s 𝑥𝐿 ) ·s 1s ) <s ( ( 𝐴 -s 𝑥𝐿 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) ) )
198 190 197 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( 𝐴 -s 𝑥𝐿 ) ·s 1s ) <s ( ( 𝐴 -s 𝑥𝐿 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) )
199 184 198 eqbrtrrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝐴 -s 𝑥𝐿 ) <s ( ( 𝐴 -s 𝑥𝐿 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) )
200 153 154 negsubsdi2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → ( -us ‘ ( 𝑥𝐿 -s 𝐴 ) ) = ( 𝐴 -s 𝑥𝐿 ) )
201 200 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( -us ‘ ( 𝑥𝐿 -s 𝐴 ) ) = ( 𝐴 -s 𝑥𝐿 ) )
202 156 191 mulnegs1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( -us ‘ ( 𝑥𝐿 -s 𝐴 ) ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) = ( -us ‘ ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) ) )
203 200 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → ( ( -us ‘ ( 𝑥𝐿 -s 𝐴 ) ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) = ( ( 𝐴 -s 𝑥𝐿 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) )
204 203 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( -us ‘ ( 𝑥𝐿 -s 𝐴 ) ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) = ( ( 𝐴 -s 𝑥𝐿 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) )
205 202 204 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( -us ‘ ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) ) = ( ( 𝐴 -s 𝑥𝐿 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) )
206 199 201 205 3brtr4d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( -us ‘ ( 𝑥𝐿 -s 𝐴 ) ) <s ( -us ‘ ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) ) )
207 156 191 mulscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) ∈ No )
208 207 156 sltnegd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) <s ( 𝑥𝐿 -s 𝐴 ) ↔ ( -us ‘ ( 𝑥𝐿 -s 𝐴 ) ) <s ( -us ‘ ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) ) ) )
209 206 208 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) <s ( 𝑥𝐿 -s 𝐴 ) )
210 148 207 163 sltaddsub2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( 𝐴 +s ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) ) <s 𝑥𝐿 ↔ ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) <s ( 𝑥𝐿 -s 𝐴 ) ) )
211 209 210 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝐴 +s ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) ) <s 𝑥𝐿 )
212 148 149 161 addsdid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝐴 ·s ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) ) = ( ( 𝐴 ·s 1s ) +s ( 𝐴 ·s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) ) )
213 148 mulsridd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝐴 ·s 1s ) = 𝐴 )
214 148 156 160 muls12d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝐴 ·s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) = ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) )
215 213 214 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( 𝐴 ·s 1s ) +s ( 𝐴 ·s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) ) = ( 𝐴 +s ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) ) )
216 212 215 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝐴 ·s ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) ) = ( 𝐴 +s ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) ) )
217 163 mulsridd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝑥𝐿 ·s 1s ) = 𝑥𝐿 )
218 211 216 217 3brtr4d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝐴 ·s ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) ) <s ( 𝑥𝐿 ·s 1s ) )
219 148 162 mulscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝐴 ·s ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) ) ∈ No )
220 167 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 0s <s 𝑥𝐿 )
221 219 149 163 220 180 sltdivmulwd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( ( 𝐴 ·s ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) ) /su 𝑥𝐿 ) <s 1s ↔ ( 𝐴 ·s ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) ) <s ( 𝑥𝐿 ·s 1s ) ) )
222 218 221 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( 𝐴 ·s ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) ) /su 𝑥𝐿 ) <s 1s )
223 181 222 eqbrtrrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝐴 ·s ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) ) <s 1s )
224 oveq2 ⊢ ( 𝑟 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) → ( 𝐴 ·s 𝑟 ) = ( 𝐴 ·s ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) ) )
225 224 breq1d ⊢ ( 𝑟 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) → ( ( 𝐴 ·s 𝑟 ) <s 1s ↔ ( 𝐴 ·s ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) ) <s 1s ) )
226 223 225 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝑟 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) → ( 𝐴 ·s 𝑟 ) <s 1s ) )
227 226 rexlimdvva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ( ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑟 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) → ( 𝐴 ·s 𝑟 ) <s 1s ) )
228 147 227 jaod ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ( ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑟 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) ∨ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑟 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) ) → ( 𝐴 ·s 𝑟 ) <s 1s ) )
229 76 228 jaod ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ( ( 𝑟 ∈ ( 𝐿 ‘ 𝑗 ) ∨ ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑟 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) ∨ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑟 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) ) ) → ( 𝐴 ·s 𝑟 ) <s 1s ) )
230 73 229 sylbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ( 𝑟 ∈ ( 𝐿 ‘ suc 𝑗 ) → ( 𝐴 ·s 𝑟 ) <s 1s ) )
231 230 ralrimiv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ∀ 𝑟 ∈ ( 𝐿 ‘ suc 𝑗 ) ( 𝐴 ·s 𝑟 ) <s 1s )
232 1 2 3 precsexlem5 ⊢ ( 𝑗 ∈ ω → ( 𝑅 ‘ suc 𝑗 ) = ( ( 𝑅 ‘ 𝑗 ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ) ) )
233 232 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ( 𝑅 ‘ suc 𝑗 ) = ( ( 𝑅 ‘ 𝑗 ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ) ) )
234 233 eleq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ( 𝑠 ∈ ( 𝑅 ‘ suc 𝑗 ) ↔ 𝑠 ∈ ( ( 𝑅 ‘ 𝑗 ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ) ) ) )
235 elun ⊢ ( 𝑠 ∈ ( ( 𝑅 ‘ 𝑗 ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ) ) ↔ ( 𝑠 ∈ ( 𝑅 ‘ 𝑗 ) ∨ 𝑠 ∈ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ) ) )
236 elun ⊢ ( 𝑠 ∈ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ) ↔ ( 𝑠 ∈ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ∨ 𝑠 ∈ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ) )
237 vex ⊢ 𝑠 ∈ V
238 eqeq1 ⊢ ( 𝑎 = 𝑠 → ( 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) ↔ 𝑠 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) ) )
239 238 2rexbidv ⊢ ( 𝑎 = 𝑠 → ( ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) ↔ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑠 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) ) )
240 237 239 elab ⊢ ( 𝑠 ∈ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ↔ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑠 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) )
241 eqeq1 ⊢ ( 𝑎 = 𝑠 → ( 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ↔ 𝑠 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ) )
242 241 2rexbidv ⊢ ( 𝑎 = 𝑠 → ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ↔ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑠 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ) )
243 237 242 elab ⊢ ( 𝑠 ∈ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ↔ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑠 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) )
244 240 243 orbi12i ⊢ ( ( 𝑠 ∈ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ∨ 𝑠 ∈ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ) ↔ ( ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑠 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) ∨ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑠 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ) )
245 236 244 bitri ⊢ ( 𝑠 ∈ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ) ↔ ( ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑠 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) ∨ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑠 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ) )
246 245 orbi2i ⊢ ( ( 𝑠 ∈ ( 𝑅 ‘ 𝑗 ) ∨ 𝑠 ∈ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ) ) ↔ ( 𝑠 ∈ ( 𝑅 ‘ 𝑗 ) ∨ ( ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑠 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) ∨ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑠 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ) ) )
247 235 246 bitri ⊢ ( 𝑠 ∈ ( ( 𝑅 ‘ 𝑗 ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ) ) ↔ ( 𝑠 ∈ ( 𝑅 ‘ 𝑗 ) ∨ ( ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑠 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) ∨ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑠 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ) ) )
248 234 247 bitrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ( 𝑠 ∈ ( 𝑅 ‘ suc 𝑗 ) ↔ ( 𝑠 ∈ ( 𝑅 ‘ 𝑗 ) ∨ ( ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑠 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) ∨ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑠 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ) ) ) )
249 28 rspccv ⊢ ( ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) → ( 𝑠 ∈ ( 𝑅 ‘ 𝑗 ) → 1s <s ( 𝐴 ·s 𝑠 ) ) )
250 185 249 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ( 𝑠 ∈ ( 𝑅 ‘ 𝑗 ) → 1s <s ( 𝐴 ·s 𝑠 ) ) )
251 119 adantrl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝐴 ·s 𝑦𝐿 ) <s 1s )
252 77 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 𝐴 ∈ No )
253 90 adantrl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 𝑦𝐿 ∈ No )
254 252 253 mulscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝐴 ·s 𝑦𝐿 ) ∈ No )
255 79 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 1s ∈ No )
256 182 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝐴 -s 𝑥𝐿 ) ∈ No )
257 195 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 0s <s ( 𝐴 -s 𝑥𝐿 ) )
258 254 255 256 257 sltmul2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 𝐴 ·s 𝑦𝐿 ) <s 1s ↔ ( ( 𝐴 -s 𝑥𝐿 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) <s ( ( 𝐴 -s 𝑥𝐿 ) ·s 1s ) ) )
259 251 258 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 𝐴 -s 𝑥𝐿 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) <s ( ( 𝐴 -s 𝑥𝐿 ) ·s 1s ) )
260 256 mulsridd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 𝐴 -s 𝑥𝐿 ) ·s 1s ) = ( 𝐴 -s 𝑥𝐿 ) )
261 259 260 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 𝐴 -s 𝑥𝐿 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) <s ( 𝐴 -s 𝑥𝐿 ) )
262 155 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝑥𝐿 -s 𝐴 ) ∈ No )
263 262 254 mulnegs1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( -us ‘ ( 𝑥𝐿 -s 𝐴 ) ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) = ( -us ‘ ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) ) )
264 200 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → ( ( -us ‘ ( 𝑥𝐿 -s 𝐴 ) ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) = ( ( 𝐴 -s 𝑥𝐿 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) )
265 264 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( -us ‘ ( 𝑥𝐿 -s 𝐴 ) ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) = ( ( 𝐴 -s 𝑥𝐿 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) )
266 263 265 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( -us ‘ ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) ) = ( ( 𝐴 -s 𝑥𝐿 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) )
267 200 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( -us ‘ ( 𝑥𝐿 -s 𝐴 ) ) = ( 𝐴 -s 𝑥𝐿 ) )
268 261 266 267 3brtr4d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( -us ‘ ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) ) <s ( -us ‘ ( 𝑥𝐿 -s 𝐴 ) ) )
269 262 254 mulscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) ∈ No )
270 262 269 sltnegd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 𝑥𝐿 -s 𝐴 ) <s ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) ↔ ( -us ‘ ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) ) <s ( -us ‘ ( 𝑥𝐿 -s 𝐴 ) ) ) )
271 268 270 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝑥𝐿 -s 𝐴 ) <s ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) )
272 153 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 𝑥𝐿 ∈ No )
273 272 252 269 sltsubadd2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 𝑥𝐿 -s 𝐴 ) <s ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) ↔ 𝑥𝐿 <s ( 𝐴 +s ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) ) ) )
274 271 273 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 𝑥𝐿 <s ( 𝐴 +s ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) ) )
275 272 mulslidd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 1s ·s 𝑥𝐿 ) = 𝑥𝐿 )
276 262 253 mulscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ∈ No )
277 252 255 276 addsdid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝐴 ·s ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) ) = ( ( 𝐴 ·s 1s ) +s ( 𝐴 ·s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) ) )
278 252 mulsridd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝐴 ·s 1s ) = 𝐴 )
279 252 262 253 muls12d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝐴 ·s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) = ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) )
280 278 279 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 𝐴 ·s 1s ) +s ( 𝐴 ·s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) ) = ( 𝐴 +s ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) ) )
281 277 280 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝐴 ·s ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) ) = ( 𝐴 +s ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) ) )
282 274 275 281 3brtr4d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 1s ·s 𝑥𝐿 ) <s ( 𝐴 ·s ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) ) )
283 255 276 addscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) ∈ No )
284 252 283 mulscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝐴 ·s ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) ) ∈ No )
285 167 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 0s <s 𝑥𝐿 )
286 179 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ∃ 𝑦 ∈ No ( 𝑥𝐿 ·s 𝑦 ) = 1s )
287 255 284 272 285 286 sltmuldivwd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 1s ·s 𝑥𝐿 ) <s ( 𝐴 ·s ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) ) ↔ 1s <s ( ( 𝐴 ·s ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) ) /su 𝑥𝐿 ) ) )
288 282 287 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 1s <s ( ( 𝐴 ·s ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) ) /su 𝑥𝐿 ) )
289 168 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 𝑥𝐿 ≠ 0s )
290 252 283 272 289 286 divsasswd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 𝐴 ·s ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) ) /su 𝑥𝐿 ) = ( 𝐴 ·s ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) ) )
291 288 290 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 1s <s ( 𝐴 ·s ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) ) )
292 oveq2 ⊢ ( 𝑠 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) → ( 𝐴 ·s 𝑠 ) = ( 𝐴 ·s ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) ) )
293 292 breq2d ⊢ ( 𝑠 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) → ( 1s <s ( 𝐴 ·s 𝑠 ) ↔ 1s <s ( 𝐴 ·s ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) ) ) )
294 291 293 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝑠 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) → 1s <s ( 𝐴 ·s 𝑠 ) ) )
295 294 rexlimdvva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ( ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑠 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) → 1s <s ( 𝐴 ·s 𝑠 ) ) )
296 85 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝑥𝑅 -s 𝐴 ) ∈ No )
297 296 mulsridd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( 𝑥𝑅 -s 𝐴 ) ·s 1s ) = ( 𝑥𝑅 -s 𝐴 ) )
298 189 adantrl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 1s <s ( 𝐴 ·s 𝑦𝑅 ) )
299 79 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 1s ∈ No )
300 77 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝐴 ∈ No )
301 159 adantrl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝑦𝑅 ∈ No )
302 300 301 mulscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝐴 ·s 𝑦𝑅 ) ∈ No )
303 123 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 0s <s ( 𝑥𝑅 -s 𝐴 ) )
304 299 302 296 303 sltmul2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 1s <s ( 𝐴 ·s 𝑦𝑅 ) ↔ ( ( 𝑥𝑅 -s 𝐴 ) ·s 1s ) <s ( ( 𝑥𝑅 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) ) )
305 298 304 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( 𝑥𝑅 -s 𝐴 ) ·s 1s ) <s ( ( 𝑥𝑅 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) )
306 297 305 eqbrtrrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝑥𝑅 -s 𝐴 ) <s ( ( 𝑥𝑅 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) )
307 83 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝑥𝑅 ∈ No )
308 296 302 mulscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( 𝑥𝑅 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) ∈ No )
309 307 300 308 sltsubadd2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( 𝑥𝑅 -s 𝐴 ) <s ( ( 𝑥𝑅 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) ↔ 𝑥𝑅 <s ( 𝐴 +s ( ( 𝑥𝑅 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) ) ) )
310 306 309 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝑥𝑅 <s ( 𝐴 +s ( ( 𝑥𝑅 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) ) )
311 307 mulslidd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 1s ·s 𝑥𝑅 ) = 𝑥𝑅 )
312 296 301 mulscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ∈ No )
313 300 299 312 addsdid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝐴 ·s ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) ) = ( ( 𝐴 ·s 1s ) +s ( 𝐴 ·s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) ) )
314 300 mulsridd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝐴 ·s 1s ) = 𝐴 )
315 300 296 301 muls12d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝐴 ·s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) = ( ( 𝑥𝑅 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) )
316 314 315 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( 𝐴 ·s 1s ) +s ( 𝐴 ·s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) ) = ( 𝐴 +s ( ( 𝑥𝑅 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) ) )
317 313 316 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝐴 ·s ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) ) = ( 𝐴 +s ( ( 𝑥𝑅 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) ) )
318 310 311 317 3brtr4d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 1s ·s 𝑥𝑅 ) <s ( 𝐴 ·s ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) ) )
319 299 312 addscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) ∈ No )
320 300 319 mulscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝐴 ·s ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) ) ∈ No )
321 100 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 0s <s 𝑥𝑅 )
322 113 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ∃ 𝑦 ∈ No ( 𝑥𝑅 ·s 𝑦 ) = 1s )
323 299 320 307 321 322 sltmuldivwd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( 1s ·s 𝑥𝑅 ) <s ( 𝐴 ·s ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) ) ↔ 1s <s ( ( 𝐴 ·s ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) ) /su 𝑥𝑅 ) ) )
324 318 323 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 1s <s ( ( 𝐴 ·s ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) ) /su 𝑥𝑅 ) )
325 101 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝑥𝑅 ≠ 0s )
326 300 319 307 325 322 divsasswd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( 𝐴 ·s ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) ) /su 𝑥𝑅 ) = ( 𝐴 ·s ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ) )
327 324 326 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 1s <s ( 𝐴 ·s ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ) )
328 oveq2 ⊢ ( 𝑠 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) → ( 𝐴 ·s 𝑠 ) = ( 𝐴 ·s ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ) )
329 328 breq2d ⊢ ( 𝑠 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) → ( 1s <s ( 𝐴 ·s 𝑠 ) ↔ 1s <s ( 𝐴 ·s ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ) ) )
330 327 329 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝑠 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) → 1s <s ( 𝐴 ·s 𝑠 ) ) )
331 330 rexlimdvva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑠 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) → 1s <s ( 𝐴 ·s 𝑠 ) ) )
332 295 331 jaod ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ( ( ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑠 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) ∨ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑠 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ) → 1s <s ( 𝐴 ·s 𝑠 ) ) )
333 250 332 jaod ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ( ( 𝑠 ∈ ( 𝑅 ‘ 𝑗 ) ∨ ( ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑠 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) ∨ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑠 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ) ) → 1s <s ( 𝐴 ·s 𝑠 ) ) )
334 248 333 sylbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ( 𝑠 ∈ ( 𝑅 ‘ suc 𝑗 ) → 1s <s ( 𝐴 ·s 𝑠 ) ) )
335 334 ralrimiv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ∀ 𝑠 ∈ ( 𝑅 ‘ suc 𝑗 ) 1s <s ( 𝐴 ·s 𝑠 ) )
336 231 335 jca ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ( ∀ 𝑟 ∈ ( 𝐿 ‘ suc 𝑗 ) ( 𝐴 ·s 𝑟 ) <s 1s ∧ ∀ 𝑠 ∈ ( 𝑅 ‘ suc 𝑗 ) 1s <s ( 𝐴 ·s 𝑠 ) ) )
337 336 3exp ⊢ ( 𝜑 → ( 𝑗 ∈ ω → ( ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) → ( ∀ 𝑟 ∈ ( 𝐿 ‘ suc 𝑗 ) ( 𝐴 ·s 𝑟 ) <s 1s ∧ ∀ 𝑠 ∈ ( 𝑅 ‘ suc 𝑗 ) 1s <s ( 𝐴 ·s 𝑠 ) ) ) ) )
338 337 com12 ⊢ ( 𝑗 ∈ ω → ( 𝜑 → ( ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) → ( ∀ 𝑟 ∈ ( 𝐿 ‘ suc 𝑗 ) ( 𝐴 ·s 𝑟 ) <s 1s ∧ ∀ 𝑠 ∈ ( 𝑅 ‘ suc 𝑗 ) 1s <s ( 𝐴 ·s 𝑠 ) ) ) ) )
339 338 a2d ⊢ ( 𝑗 ∈ ω → ( ( 𝜑 → ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ( 𝜑 → ( ∀ 𝑟 ∈ ( 𝐿 ‘ suc 𝑗 ) ( 𝐴 ·s 𝑟 ) <s 1s ∧ ∀ 𝑠 ∈ ( 𝑅 ‘ suc 𝑗 ) 1s <s ( 𝐴 ·s 𝑠 ) ) ) ) )
340 12 18 32 38 56 339 finds ⊢ ( 𝐼 ∈ ω → ( 𝜑 → ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝐼 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝐼 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) )
341 340 impcom ⊢ ( ( 𝜑 ∧ 𝐼 ∈ ω ) → ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝐼 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝐼 ) 1s <s ( 𝐴 ·s 𝑐 ) ) )