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 breq2 ⊢ ( 𝑥𝑂 = 𝑥𝑅 → ( 𝐴 <s 𝑥𝑂 ↔ 𝐴 <s 𝑥𝑅 ) )
99 rightval ⊢ ( R ‘ 𝐴 ) = { 𝑥𝑂 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝐴 <s 𝑥𝑂 }
100 98 99 elrab2 ⊢ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ↔ ( 𝑥𝑅 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∧ 𝐴 <s 𝑥𝑅 ) )
101 100 simprbi ⊢ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) → 𝐴 <s 𝑥𝑅 )
102 101 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ) → 𝐴 <s 𝑥𝑅 )
103 95 84 83 97 102 slttrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ) → 0s <s 𝑥𝑅 )
104 103 sgt0ne0d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ) → 𝑥𝑅 ≠ 0s )
105 104 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 𝑥𝑅 ≠ 0s )
106 breq2 ⊢ ( 𝑥𝑂 = 𝑥𝑅 → ( 0s <s 𝑥𝑂 ↔ 0s <s 𝑥𝑅 ) )
107 oveq1 ⊢ ( 𝑥𝑂 = 𝑥𝑅 → ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑥𝑅 ·s 𝑦 ) )
108 107 eqeq1d ⊢ ( 𝑥𝑂 = 𝑥𝑅 → ( ( 𝑥𝑂 ·s 𝑦 ) = 1s ↔ ( 𝑥𝑅 ·s 𝑦 ) = 1s ) )
109 108 rexbidv ⊢ ( 𝑥𝑂 = 𝑥𝑅 → ( ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ↔ ∃ 𝑦 ∈ No ( 𝑥𝑅 ·s 𝑦 ) = 1s ) )
110 106 109 imbi12d ⊢ ( 𝑥𝑂 = 𝑥𝑅 → ( ( 0s <s 𝑥𝑂 → ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) ↔ ( 0s <s 𝑥𝑅 → ∃ 𝑦 ∈ No ( 𝑥𝑅 ·s 𝑦 ) = 1s ) ) )
111 6 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ( 0s <s 𝑥𝑂 → ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) )
112 111 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ( 0s <s 𝑥𝑂 → ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) )
113 elun2 ⊢ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) → 𝑥𝑅 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
114 113 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ) → 𝑥𝑅 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
115 110 112 114 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ) → ( 0s <s 𝑥𝑅 → ∃ 𝑦 ∈ No ( 𝑥𝑅 ·s 𝑦 ) = 1s ) )
116 103 115 mpd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ) → ∃ 𝑦 ∈ No ( 𝑥𝑅 ·s 𝑦 ) = 1s )
117 116 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ∃ 𝑦 ∈ No ( 𝑥𝑅 ·s 𝑦 ) = 1s )
118 78 93 94 105 117 divsasswd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 𝐴 ·s ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) ) /su 𝑥𝑅 ) = ( 𝐴 ·s ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) ) )
119 oveq2 ⊢ ( 𝑏 = 𝑦𝐿 → ( 𝐴 ·s 𝑏 ) = ( 𝐴 ·s 𝑦𝐿 ) )
120 119 breq1d ⊢ ( 𝑏 = 𝑦𝐿 → ( ( 𝐴 ·s 𝑏 ) <s 1s ↔ ( 𝐴 ·s 𝑦𝐿 ) <s 1s ) )
121 120 rspccva ⊢ ( ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) → ( 𝐴 ·s 𝑦𝐿 ) <s 1s )
122 74 121 sylan ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) → ( 𝐴 ·s 𝑦𝐿 ) <s 1s )
123 122 adantrl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝐴 ·s 𝑦𝐿 ) <s 1s )
124 78 91 mulscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝐴 ·s 𝑦𝐿 ) ∈ No )
125 84 83 posdifsd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ) → ( 𝐴 <s 𝑥𝑅 ↔ 0s <s ( 𝑥𝑅 -s 𝐴 ) ) )
126 102 125 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ) → 0s <s ( 𝑥𝑅 -s 𝐴 ) )
127 126 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 0s <s ( 𝑥𝑅 -s 𝐴 ) )
128 124 80 86 127 sltmul2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 𝐴 ·s 𝑦𝐿 ) <s 1s ↔ ( ( 𝑥𝑅 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) <s ( ( 𝑥𝑅 -s 𝐴 ) ·s 1s ) ) )
129 123 128 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 𝑥𝑅 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) <s ( ( 𝑥𝑅 -s 𝐴 ) ·s 1s ) )
130 86 mulsridd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 𝑥𝑅 -s 𝐴 ) ·s 1s ) = ( 𝑥𝑅 -s 𝐴 ) )
131 129 130 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 𝑥𝑅 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) <s ( 𝑥𝑅 -s 𝐴 ) )
132 86 124 mulscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 𝑥𝑅 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) ∈ No )
133 78 132 94 sltaddsub2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 𝐴 +s ( ( 𝑥𝑅 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) ) <s 𝑥𝑅 ↔ ( ( 𝑥𝑅 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) <s ( 𝑥𝑅 -s 𝐴 ) ) )
134 131 133 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝐴 +s ( ( 𝑥𝑅 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) ) <s 𝑥𝑅 )
135 78 80 92 addsdid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝐴 ·s ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) ) = ( ( 𝐴 ·s 1s ) +s ( 𝐴 ·s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) ) )
136 78 mulsridd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝐴 ·s 1s ) = 𝐴 )
137 78 86 91 muls12d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝐴 ·s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) = ( ( 𝑥𝑅 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) )
138 136 137 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 𝐴 ·s 1s ) +s ( 𝐴 ·s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) ) = ( 𝐴 +s ( ( 𝑥𝑅 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) ) )
139 135 138 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝐴 ·s ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) ) = ( 𝐴 +s ( ( 𝑥𝑅 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) ) )
140 94 mulslidd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 1s ·s 𝑥𝑅 ) = 𝑥𝑅 )
141 134 139 140 3brtr4d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝐴 ·s ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) ) <s ( 1s ·s 𝑥𝑅 ) )
142 78 93 mulscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝐴 ·s ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) ) ∈ No )
143 103 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 0s <s 𝑥𝑅 )
144 142 80 94 143 117 sltdivmul2wd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·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 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 𝐴 ·s ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) ) /su 𝑥𝑅 ) <s 1s )
146 118 145 eqbrtrrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝐴 ·s ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) ) <s 1s )
147 oveq2 ⊢ ( 𝑟 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) → ( 𝐴 ·s 𝑟 ) = ( 𝐴 ·s ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) ) )
148 147 breq1d ⊢ ( 𝑟 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) → ( ( 𝐴 ·s 𝑟 ) <s 1s ↔ ( 𝐴 ·s ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) ) <s 1s ) )
149 146 148 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝑟 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) → ( 𝐴 ·s 𝑟 ) <s 1s ) )
150 149 rexlimdvva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑟 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) → ( 𝐴 ·s 𝑟 ) <s 1s ) )
151 77 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝐴 ∈ No )
152 79 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 1s ∈ No )
153 leftssno ⊢ ( L ‘ 𝐴 ) ⊆ No
154 elrabi ⊢ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } → 𝑥𝐿 ∈ ( L ‘ 𝐴 ) )
155 154 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → 𝑥𝐿 ∈ ( L ‘ 𝐴 ) )
156 153 155 sselid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → 𝑥𝐿 ∈ No )
157 77 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → 𝐴 ∈ No )
158 156 157 subscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → ( 𝑥𝐿 -s 𝐴 ) ∈ No )
159 158 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝑥𝐿 -s 𝐴 ) ∈ No )
160 87 simprd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ) → ( 𝑅 ‘ 𝑗 ) ⊆ No )
161 160 3adant3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ( 𝑅 ‘ 𝑗 ) ⊆ No )
162 161 sselda ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) → 𝑦𝑅 ∈ No )
163 162 adantrl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝑦𝑅 ∈ No )
164 159 163 mulscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ∈ No )
165 152 164 addscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) ∈ No )
166 156 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝑥𝐿 ∈ No )
167 breq2 ⊢ ( 𝑥 = 𝑥𝐿 → ( 0s <s 𝑥 ↔ 0s <s 𝑥𝐿 ) )
168 167 elrab ⊢ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ↔ ( 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ∧ 0s <s 𝑥𝐿 ) )
169 168 simprbi ⊢ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } → 0s <s 𝑥𝐿 )
170 169 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → 0s <s 𝑥𝐿 )
171 170 sgt0ne0d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → 𝑥𝐿 ≠ 0s )
172 171 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝑥𝐿 ≠ 0s )
173 breq2 ⊢ ( 𝑥𝑂 = 𝑥𝐿 → ( 0s <s 𝑥𝑂 ↔ 0s <s 𝑥𝐿 ) )
174 oveq1 ⊢ ( 𝑥𝑂 = 𝑥𝐿 → ( 𝑥𝑂 ·s 𝑦 ) = ( 𝑥𝐿 ·s 𝑦 ) )
175 174 eqeq1d ⊢ ( 𝑥𝑂 = 𝑥𝐿 → ( ( 𝑥𝑂 ·s 𝑦 ) = 1s ↔ ( 𝑥𝐿 ·s 𝑦 ) = 1s ) )
176 175 rexbidv ⊢ ( 𝑥𝑂 = 𝑥𝐿 → ( ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ↔ ∃ 𝑦 ∈ No ( 𝑥𝐿 ·s 𝑦 ) = 1s ) )
177 173 176 imbi12d ⊢ ( 𝑥𝑂 = 𝑥𝐿 → ( ( 0s <s 𝑥𝑂 → ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) ↔ ( 0s <s 𝑥𝐿 → ∃ 𝑦 ∈ No ( 𝑥𝐿 ·s 𝑦 ) = 1s ) ) )
178 111 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ( 0s <s 𝑥𝑂 → ∃ 𝑦 ∈ No ( 𝑥𝑂 ·s 𝑦 ) = 1s ) )
179 elun1 ⊢ ( 𝑥𝐿 ∈ ( L ‘ 𝐴 ) → 𝑥𝐿 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
180 155 179 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → 𝑥𝐿 ∈ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) )
181 177 178 180 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → ( 0s <s 𝑥𝐿 → ∃ 𝑦 ∈ No ( 𝑥𝐿 ·s 𝑦 ) = 1s ) )
182 170 181 mpd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → ∃ 𝑦 ∈ No ( 𝑥𝐿 ·s 𝑦 ) = 1s )
183 182 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ∃ 𝑦 ∈ No ( 𝑥𝐿 ·s 𝑦 ) = 1s )
184 151 165 166 172 183 divsasswd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·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 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → ( 𝐴 -s 𝑥𝐿 ) ∈ No )
186 185 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝐴 -s 𝑥𝐿 ) ∈ No )
187 186 mulsridd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( 𝐴 -s 𝑥𝐿 ) ·s 1s ) = ( 𝐴 -s 𝑥𝐿 ) )
188 simp3r ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) )
189 oveq2 ⊢ ( 𝑐 = 𝑦𝑅 → ( 𝐴 ·s 𝑐 ) = ( 𝐴 ·s 𝑦𝑅 ) )
190 189 breq2d ⊢ ( 𝑐 = 𝑦𝑅 → ( 1s <s ( 𝐴 ·s 𝑐 ) ↔ 1s <s ( 𝐴 ·s 𝑦𝑅 ) ) )
191 190 rspccva ⊢ ( ( ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) → 1s <s ( 𝐴 ·s 𝑦𝑅 ) )
192 188 191 sylan ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) → 1s <s ( 𝐴 ·s 𝑦𝑅 ) )
193 192 adantrl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 1s <s ( 𝐴 ·s 𝑦𝑅 ) )
194 151 163 mulscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝐴 ·s 𝑦𝑅 ) ∈ No )
195 breq1 ⊢ ( 𝑥𝑂 = 𝑥𝐿 → ( 𝑥𝑂 <s 𝐴 ↔ 𝑥𝐿 <s 𝐴 ) )
196 leftval ⊢ ( L ‘ 𝐴 ) = { 𝑥𝑂 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝑥𝑂 <s 𝐴 }
197 195 196 elrab2 ⊢ ( 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ↔ ( 𝑥𝐿 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∧ 𝑥𝐿 <s 𝐴 ) )
198 197 simprbi ⊢ ( 𝑥𝐿 ∈ ( L ‘ 𝐴 ) → 𝑥𝐿 <s 𝐴 )
199 155 198 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → 𝑥𝐿 <s 𝐴 )
200 156 157 posdifsd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → ( 𝑥𝐿 <s 𝐴 ↔ 0s <s ( 𝐴 -s 𝑥𝐿 ) ) )
201 199 200 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → 0s <s ( 𝐴 -s 𝑥𝐿 ) )
202 201 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 0s <s ( 𝐴 -s 𝑥𝐿 ) )
203 152 194 186 202 sltmul2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 1s <s ( 𝐴 ·s 𝑦𝑅 ) ↔ ( ( 𝐴 -s 𝑥𝐿 ) ·s 1s ) <s ( ( 𝐴 -s 𝑥𝐿 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) ) )
204 193 203 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( 𝐴 -s 𝑥𝐿 ) ·s 1s ) <s ( ( 𝐴 -s 𝑥𝐿 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) )
205 187 204 eqbrtrrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝐴 -s 𝑥𝐿 ) <s ( ( 𝐴 -s 𝑥𝐿 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) )
206 156 157 negsubsdi2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → ( -us ‘ ( 𝑥𝐿 -s 𝐴 ) ) = ( 𝐴 -s 𝑥𝐿 ) )
207 206 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( -us ‘ ( 𝑥𝐿 -s 𝐴 ) ) = ( 𝐴 -s 𝑥𝐿 ) )
208 159 194 mulnegs1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( -us ‘ ( 𝑥𝐿 -s 𝐴 ) ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) = ( -us ‘ ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) ) )
209 206 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → ( ( -us ‘ ( 𝑥𝐿 -s 𝐴 ) ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) = ( ( 𝐴 -s 𝑥𝐿 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) )
210 209 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( -us ‘ ( 𝑥𝐿 -s 𝐴 ) ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) = ( ( 𝐴 -s 𝑥𝐿 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) )
211 208 210 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( -us ‘ ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) ) = ( ( 𝐴 -s 𝑥𝐿 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) )
212 205 207 211 3brtr4d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( -us ‘ ( 𝑥𝐿 -s 𝐴 ) ) <s ( -us ‘ ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) ) )
213 159 194 mulscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) ∈ No )
214 213 159 sltnegd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·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 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) <s ( 𝑥𝐿 -s 𝐴 ) )
216 151 213 166 sltaddsub2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( 𝐴 +s ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) ) <s 𝑥𝐿 ↔ ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) <s ( 𝑥𝐿 -s 𝐴 ) ) )
217 215 216 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝐴 +s ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) ) <s 𝑥𝐿 )
218 151 152 164 addsdid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝐴 ·s ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) ) = ( ( 𝐴 ·s 1s ) +s ( 𝐴 ·s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) ) )
219 151 mulsridd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝐴 ·s 1s ) = 𝐴 )
220 151 159 163 muls12d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝐴 ·s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) = ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) )
221 219 220 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( 𝐴 ·s 1s ) +s ( 𝐴 ·s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) ) = ( 𝐴 +s ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) ) )
222 218 221 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝐴 ·s ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) ) = ( 𝐴 +s ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) ) )
223 166 mulsridd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝑥𝐿 ·s 1s ) = 𝑥𝐿 )
224 217 222 223 3brtr4d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝐴 ·s ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) ) <s ( 𝑥𝐿 ·s 1s ) )
225 151 165 mulscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝐴 ·s ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) ) ∈ No )
226 170 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 0s <s 𝑥𝐿 )
227 225 152 166 226 183 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 ) ) )
228 224 227 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( 𝐴 ·s ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) ) /su 𝑥𝐿 ) <s 1s )
229 184 228 eqbrtrrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝐴 ·s ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) ) <s 1s )
230 oveq2 ⊢ ( 𝑟 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) → ( 𝐴 ·s 𝑟 ) = ( 𝐴 ·s ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) ) )
231 230 breq1d ⊢ ( 𝑟 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) → ( ( 𝐴 ·s 𝑟 ) <s 1s ↔ ( 𝐴 ·s ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) ) <s 1s ) )
232 229 231 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝑟 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) → ( 𝐴 ·s 𝑟 ) <s 1s ) )
233 232 rexlimdvva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ( ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑟 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) → ( 𝐴 ·s 𝑟 ) <s 1s ) )
234 150 233 jaod ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ( ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑟 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) ∨ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑟 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) ) → ( 𝐴 ·s 𝑟 ) <s 1s ) )
235 76 234 jaod ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ( ( 𝑟 ∈ ( 𝐿 ‘ 𝑗 ) ∨ ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑟 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) ∨ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑟 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) ) ) → ( 𝐴 ·s 𝑟 ) <s 1s ) )
236 73 235 sylbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ( 𝑟 ∈ ( 𝐿 ‘ suc 𝑗 ) → ( 𝐴 ·s 𝑟 ) <s 1s ) )
237 236 ralrimiv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ∀ 𝑟 ∈ ( 𝐿 ‘ suc 𝑗 ) ( 𝐴 ·s 𝑟 ) <s 1s )
238 1 2 3 precsexlem5 ⊢ ( 𝑗 ∈ ω → ( 𝑅 ‘ suc 𝑗 ) = ( ( 𝑅 ‘ 𝑗 ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ) ) )
239 238 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ( 𝑅 ‘ suc 𝑗 ) = ( ( 𝑅 ‘ 𝑗 ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ) ) )
240 239 eleq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ( 𝑠 ∈ ( 𝑅 ‘ suc 𝑗 ) ↔ 𝑠 ∈ ( ( 𝑅 ‘ 𝑗 ) ∪ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ∪ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ) ) ) )
241 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 𝑥𝑅 ) } ) ) )
242 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 𝑥𝑅 ) } ) )
243 vex ⊢ 𝑠 ∈ V
244 eqeq1 ⊢ ( 𝑎 = 𝑠 → ( 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) ↔ 𝑠 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) ) )
245 244 2rexbidv ⊢ ( 𝑎 = 𝑠 → ( ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) ↔ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑠 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) ) )
246 243 245 elab ⊢ ( 𝑠 ∈ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } ↔ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑠 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) )
247 eqeq1 ⊢ ( 𝑎 = 𝑠 → ( 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ↔ 𝑠 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ) )
248 247 2rexbidv ⊢ ( 𝑎 = 𝑠 → ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ↔ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑠 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ) )
249 243 248 elab ⊢ ( 𝑠 ∈ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } ↔ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑠 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) )
250 246 249 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 𝑥𝑅 ) ) )
251 242 250 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 𝑥𝑅 ) ) )
252 251 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 𝑥𝑅 ) ) ) )
253 241 252 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 𝑥𝑅 ) ) ) )
254 240 253 bitrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ( 𝑠 ∈ ( 𝑅 ‘ suc 𝑗 ) ↔ ( 𝑠 ∈ ( 𝑅 ‘ 𝑗 ) ∨ ( ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑠 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) ∨ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑠 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ) ) ) )
255 28 rspccv ⊢ ( ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) → ( 𝑠 ∈ ( 𝑅 ‘ 𝑗 ) → 1s <s ( 𝐴 ·s 𝑠 ) ) )
256 188 255 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ( 𝑠 ∈ ( 𝑅 ‘ 𝑗 ) → 1s <s ( 𝐴 ·s 𝑠 ) ) )
257 122 adantrl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝐴 ·s 𝑦𝐿 ) <s 1s )
258 77 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 𝐴 ∈ No )
259 90 adantrl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 𝑦𝐿 ∈ No )
260 258 259 mulscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝐴 ·s 𝑦𝐿 ) ∈ No )
261 79 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 1s ∈ No )
262 185 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝐴 -s 𝑥𝐿 ) ∈ No )
263 201 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 0s <s ( 𝐴 -s 𝑥𝐿 ) )
264 260 261 262 263 sltmul2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 𝐴 ·s 𝑦𝐿 ) <s 1s ↔ ( ( 𝐴 -s 𝑥𝐿 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) <s ( ( 𝐴 -s 𝑥𝐿 ) ·s 1s ) ) )
265 257 264 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 𝐴 -s 𝑥𝐿 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) <s ( ( 𝐴 -s 𝑥𝐿 ) ·s 1s ) )
266 262 mulsridd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 𝐴 -s 𝑥𝐿 ) ·s 1s ) = ( 𝐴 -s 𝑥𝐿 ) )
267 265 266 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 𝐴 -s 𝑥𝐿 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) <s ( 𝐴 -s 𝑥𝐿 ) )
268 158 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝑥𝐿 -s 𝐴 ) ∈ No )
269 268 260 mulnegs1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( -us ‘ ( 𝑥𝐿 -s 𝐴 ) ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) = ( -us ‘ ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) ) )
270 206 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ) → ( ( -us ‘ ( 𝑥𝐿 -s 𝐴 ) ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) = ( ( 𝐴 -s 𝑥𝐿 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) )
271 270 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( -us ‘ ( 𝑥𝐿 -s 𝐴 ) ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) = ( ( 𝐴 -s 𝑥𝐿 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) )
272 269 271 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( -us ‘ ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) ) = ( ( 𝐴 -s 𝑥𝐿 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) )
273 206 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( -us ‘ ( 𝑥𝐿 -s 𝐴 ) ) = ( 𝐴 -s 𝑥𝐿 ) )
274 267 272 273 3brtr4d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( -us ‘ ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) ) <s ( -us ‘ ( 𝑥𝐿 -s 𝐴 ) ) )
275 268 260 mulscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) ∈ No )
276 268 275 sltnegd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·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 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝑥𝐿 -s 𝐴 ) <s ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) )
278 156 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 𝑥𝐿 ∈ No )
279 278 258 275 sltsubadd2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 𝑥𝐿 -s 𝐴 ) <s ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) ↔ 𝑥𝐿 <s ( 𝐴 +s ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) ) ) )
280 277 279 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 𝑥𝐿 <s ( 𝐴 +s ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) ) )
281 278 mulslidd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 1s ·s 𝑥𝐿 ) = 𝑥𝐿 )
282 268 259 mulscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ∈ No )
283 258 261 282 addsdid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝐴 ·s ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) ) = ( ( 𝐴 ·s 1s ) +s ( 𝐴 ·s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) ) )
284 258 mulsridd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝐴 ·s 1s ) = 𝐴 )
285 258 268 259 muls12d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝐴 ·s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) = ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) )
286 284 285 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( ( 𝐴 ·s 1s ) +s ( 𝐴 ·s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) ) = ( 𝐴 +s ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) ) )
287 283 286 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝐴 ·s ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) ) = ( 𝐴 +s ( ( 𝑥𝐿 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝐿 ) ) ) )
288 280 281 287 3brtr4d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 1s ·s 𝑥𝐿 ) <s ( 𝐴 ·s ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) ) )
289 261 282 addscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) ∈ No )
290 258 289 mulscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝐴 ·s ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) ) ∈ No )
291 170 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 0s <s 𝑥𝐿 )
292 182 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ∃ 𝑦 ∈ No ( 𝑥𝐿 ·s 𝑦 ) = 1s )
293 261 290 278 291 292 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 𝑥𝐿 ) ) )
294 288 293 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 1s <s ( ( 𝐴 ·s ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) ) /su 𝑥𝐿 ) )
295 171 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 𝑥𝐿 ≠ 0s )
296 258 289 278 295 292 divsasswd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·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 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → 1s <s ( 𝐴 ·s ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) ) )
298 oveq2 ⊢ ( 𝑠 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) → ( 𝐴 ·s 𝑠 ) = ( 𝐴 ·s ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) ) )
299 298 breq2d ⊢ ( 𝑠 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) → ( 1s <s ( 𝐴 ·s 𝑠 ) ↔ 1s <s ( 𝐴 ·s ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) ) ) )
300 297 299 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∧ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) ) ) → ( 𝑠 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) → 1s <s ( 𝐴 ·s 𝑠 ) ) )
301 300 rexlimdvva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ( ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ ( 𝐿 ‘ 𝑗 ) 𝑠 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) → 1s <s ( 𝐴 ·s 𝑠 ) ) )
302 85 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝑥𝑅 -s 𝐴 ) ∈ No )
303 302 mulsridd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( 𝑥𝑅 -s 𝐴 ) ·s 1s ) = ( 𝑥𝑅 -s 𝐴 ) )
304 192 adantrl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 1s <s ( 𝐴 ·s 𝑦𝑅 ) )
305 79 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 1s ∈ No )
306 77 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝐴 ∈ No )
307 162 adantrl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝑦𝑅 ∈ No )
308 306 307 mulscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝐴 ·s 𝑦𝑅 ) ∈ No )
309 126 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 0s <s ( 𝑥𝑅 -s 𝐴 ) )
310 305 308 302 309 sltmul2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 1s <s ( 𝐴 ·s 𝑦𝑅 ) ↔ ( ( 𝑥𝑅 -s 𝐴 ) ·s 1s ) <s ( ( 𝑥𝑅 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) ) )
311 304 310 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( 𝑥𝑅 -s 𝐴 ) ·s 1s ) <s ( ( 𝑥𝑅 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) )
312 303 311 eqbrtrrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝑥𝑅 -s 𝐴 ) <s ( ( 𝑥𝑅 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) )
313 83 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝑥𝑅 ∈ No )
314 302 308 mulscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( 𝑥𝑅 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) ∈ No )
315 313 306 314 sltsubadd2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( 𝑥𝑅 -s 𝐴 ) <s ( ( 𝑥𝑅 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) ↔ 𝑥𝑅 <s ( 𝐴 +s ( ( 𝑥𝑅 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) ) ) )
316 312 315 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝑥𝑅 <s ( 𝐴 +s ( ( 𝑥𝑅 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) ) )
317 313 mulslidd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 1s ·s 𝑥𝑅 ) = 𝑥𝑅 )
318 302 307 mulscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ∈ No )
319 306 305 318 addsdid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝐴 ·s ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) ) = ( ( 𝐴 ·s 1s ) +s ( 𝐴 ·s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) ) )
320 306 mulsridd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝐴 ·s 1s ) = 𝐴 )
321 306 302 307 muls12d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝐴 ·s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) = ( ( 𝑥𝑅 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) )
322 320 321 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( 𝐴 ·s 1s ) +s ( 𝐴 ·s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) ) = ( 𝐴 +s ( ( 𝑥𝑅 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) ) )
323 319 322 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝐴 ·s ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) ) = ( 𝐴 +s ( ( 𝑥𝑅 -s 𝐴 ) ·s ( 𝐴 ·s 𝑦𝑅 ) ) ) )
324 316 317 323 3brtr4d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 1s ·s 𝑥𝑅 ) <s ( 𝐴 ·s ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) ) )
325 305 318 addscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) ∈ No )
326 306 325 mulscld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝐴 ·s ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) ) ∈ No )
327 103 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 0s <s 𝑥𝑅 )
328 116 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ∃ 𝑦 ∈ No ( 𝑥𝑅 ·s 𝑦 ) = 1s )
329 305 326 313 327 328 sltmuldivwd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·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 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 1s <s ( ( 𝐴 ·s ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) ) /su 𝑥𝑅 ) )
331 104 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 𝑥𝑅 ≠ 0s )
332 306 325 313 331 328 divsasswd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( ( 𝐴 ·s ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) ) /su 𝑥𝑅 ) = ( 𝐴 ·s ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ) )
333 330 332 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → 1s <s ( 𝐴 ·s ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ) )
334 oveq2 ⊢ ( 𝑠 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) → ( 𝐴 ·s 𝑠 ) = ( 𝐴 ·s ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ) )
335 334 breq2d ⊢ ( 𝑠 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) → ( 1s <s ( 𝐴 ·s 𝑠 ) ↔ 1s <s ( 𝐴 ·s ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ) ) )
336 333 335 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) ) ) → ( 𝑠 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) → 1s <s ( 𝐴 ·s 𝑠 ) ) )
337 336 rexlimdvva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ ( 𝑅 ‘ 𝑗 ) 𝑠 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) → 1s <s ( 𝐴 ·s 𝑠 ) ) )
338 301 337 jaod ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·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 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·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 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ( 𝑠 ∈ ( 𝑅 ‘ suc 𝑗 ) → 1s <s ( 𝐴 ·s 𝑠 ) ) )
341 340 ralrimiv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ∀ 𝑠 ∈ ( 𝑅 ‘ suc 𝑗 ) 1s <s ( 𝐴 ·s 𝑠 ) )
342 237 341 jca ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ω ∧ ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ( ∀ 𝑟 ∈ ( 𝐿 ‘ suc 𝑗 ) ( 𝐴 ·s 𝑟 ) <s 1s ∧ ∀ 𝑠 ∈ ( 𝑅 ‘ suc 𝑗 ) 1s <s ( 𝐴 ·s 𝑠 ) ) )
343 342 3exp ⊢ ( 𝜑 → ( 𝑗 ∈ ω → ( ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) → ( ∀ 𝑟 ∈ ( 𝐿 ‘ suc 𝑗 ) ( 𝐴 ·s 𝑟 ) <s 1s ∧ ∀ 𝑠 ∈ ( 𝑅 ‘ suc 𝑗 ) 1s <s ( 𝐴 ·s 𝑠 ) ) ) ) )
344 343 com12 ⊢ ( 𝑗 ∈ ω → ( 𝜑 → ( ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) → ( ∀ 𝑟 ∈ ( 𝐿 ‘ suc 𝑗 ) ( 𝐴 ·s 𝑟 ) <s 1s ∧ ∀ 𝑠 ∈ ( 𝑅 ‘ suc 𝑗 ) 1s <s ( 𝐴 ·s 𝑠 ) ) ) ) )
345 344 a2d ⊢ ( 𝑗 ∈ ω → ( ( 𝜑 → ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝑗 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝑗 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) → ( 𝜑 → ( ∀ 𝑟 ∈ ( 𝐿 ‘ suc 𝑗 ) ( 𝐴 ·s 𝑟 ) <s 1s ∧ ∀ 𝑠 ∈ ( 𝑅 ‘ suc 𝑗 ) 1s <s ( 𝐴 ·s 𝑠 ) ) ) ) )
346 12 18 32 38 56 345 finds ⊢ ( 𝐼 ∈ ω → ( 𝜑 → ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝐼 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝐼 ) 1s <s ( 𝐴 ·s 𝑐 ) ) ) )
347 346 impcom ⊢ ( ( 𝜑 ∧ 𝐼 ∈ ω ) → ( ∀ 𝑏 ∈ ( 𝐿 ‘ 𝐼 ) ( 𝐴 ·s 𝑏 ) <s 1s ∧ ∀ 𝑐 ∈ ( 𝑅 ‘ 𝐼 ) 1s <s ( 𝐴 ·s 𝑐 ) ) )