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