Theorem precsexlem11 28603

Description: Lemma for surreal reciprocal. Show that the cut of the left and right sets is a multiplicative inverse for 𝐴. (Contributed by Scott Fenton, 15-Mar-2025.)

Hypotheses

Ref	Expression
precsexlem.1	⊢ 𝐹 = rec((𝑝 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd ‘𝑝) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))⟩), ⟨{ 0s }, ∅⟩)
precsexlem.2	⊢ 𝐿 = (1st ∘ 𝐹)
precsexlem.3	⊢ 𝑅 = (2nd ∘ 𝐹)
precsexlem.4	⊢ (𝜑 → 𝐴 ∈ No)
precsexlem.5	⊢ (𝜑 → 0s <s 𝐴)
precsexlem.6	⊢ (𝜑 → ∀𝑥𝑂 ∈ ((L‘𝐴) ∪ (R‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ))
precsexlem.7	⊢ 𝑌 = (∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))

Assertion

Ref	Expression
precsexlem11	⊢ (𝜑 → (𝐴 ·s 𝑌) = 1s )

Distinct variable groups:   𝐴,𝑎,𝑙,𝑝,𝑟,𝑥,𝑥_𝑂,𝑥_𝐿,𝑥_𝑅,𝑦,𝑦_𝐿,𝑦_𝑅   𝐹,𝑙,𝑝   𝐿,𝑎,𝑙,𝑥_𝐿,𝑥_𝑅,𝑦_𝐿,𝑦_𝑅   𝑅,𝑎,𝑙,𝑟,𝑥_𝐿,𝑥_𝑅,𝑦_𝐿,𝑦_𝑅   𝜑,𝑎,𝑥_𝐿,𝑥_𝑅,𝑦_𝐿,𝑦_𝑅   𝐿,𝑟   𝜑,𝑟

Allowed substitution hints:   𝜑(𝑥, 𝑦, 𝑝, 𝑙, 𝑥_𝑂)   𝑅(𝑥, 𝑦, 𝑝, 𝑥_𝑂)   𝐹(𝑥, 𝑦, 𝑟, 𝑎, 𝑥_𝑂, 𝑥_𝐿, 𝑥_𝑅, 𝑦_𝐿, 𝑦_𝑅)   𝐿(𝑥, 𝑦, 𝑝, 𝑥_𝑂)   𝑌(𝑥, 𝑦, 𝑟, 𝑝, 𝑎, 𝑙, 𝑥_𝑂, 𝑥_𝐿, 𝑥_𝑅, 𝑦_𝐿, 𝑦_𝑅)

Proof of Theorem precsexlem11

Dummy variables 𝑖 𝑗 𝑏 𝑐 𝑑 𝑒 𝑓 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		lltr 28248	. . . 4 ⊢ (L‘𝐴) <<s (R‘𝐴)
2		precsexlem.4	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ No)
3		precsexlem.5	. . . . . . 7 ⊢ (𝜑 → 0s <s 𝐴)
4	2, 3	0elleft 28297	. . . . . 6 ⊢ (𝜑 → 0s ∈ (L‘𝐴))
5	4	snssd 4746	. . . . 5 ⊢ (𝜑 → { 0s } ⊆ (L‘𝐴))
6		ssrab2 4005	. . . . . 6 ⊢ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ⊆ (L‘𝐴)
7	6	a1i 11	. . . . 5 ⊢ (𝜑 → {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ⊆ (L‘𝐴))
8	5, 7	unssd 4190	. . . 4 ⊢ (𝜑 → ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ⊆ (L‘𝐴))
9		ssslts1 28159	. . . 4 ⊢ (((L‘𝐴) <<s (R‘𝐴) ∧ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ⊆ (L‘𝐴)) → ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) <<s (R‘𝐴))
10	1, 8, 9	sylancr 599	. . 3 ⊢ (𝜑 → ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) <<s (R‘𝐴))
11		precsexlem.1	. . . 4 ⊢ 𝐹 = 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 }, ∅⟩)
12		precsexlem.2	. . . 4 ⊢ 𝐿 = (1st ∘ 𝐹)
13		precsexlem.3	. . . 4 ⊢ 𝑅 = (2nd ∘ 𝐹)
14		precsexlem.6	. . . 4 ⊢ (𝜑 → ∀𝑥𝑂 ∈ ((L‘𝐴) ∪ (R‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ))
15	11, 12, 13, 2, 3, 14	precsexlem10 28602	. . 3 ⊢ (𝜑 → ∪ (𝐿 “ ω) <<s ∪ (𝑅 “ ω))
16	2, 3	cutpos 28319	. . 3 ⊢ (𝜑 → 𝐴 = (({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) |s (R‘𝐴)))
17		precsexlem.7	. . . 4 ⊢ 𝑌 = (∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))
18	17	a1i 11	. . 3 ⊢ (𝜑 → 𝑌 = (∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω)))
19	10, 15, 16, 18	mulsunif 28536	. 2 ⊢ (𝜑 → (𝐴 ·s 𝑌) = (({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))}) |s ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))})))
20		0no 28195	. . . . . . . . 9 ⊢ 0s ∈ No
21	20	elexi 3472	. . . . . . . 8 ⊢ 0s ∈ V
22	21	snid 4622	. . . . . . 7 ⊢ 0s ∈ { 0s }
23		elun1 4180	. . . . . . 7 ⊢ ( 0s ∈ { 0s } → 0s ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}))
24	22, 23	ax-mp 5	. . . . . 6 ⊢ 0s ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})
25		peano1 7900	. . . . . . . . 9 ⊢ ∅ ∈ ω
26	11, 12, 13	precsexlem1 28593	. . . . . . . . . 10 ⊢ (𝐿‘∅) = { 0s }
27	22, 26	eleqtrri 2859	. . . . . . . . 9 ⊢ 0s ∈ (𝐿‘∅)
28		fveq2 6885	. . . . . . . . . . 11 ⊢ (𝑏 = ∅ → (𝐿‘𝑏) = (𝐿‘∅))
29	28	eleq2d 2846	. . . . . . . . . 10 ⊢ (𝑏 = ∅ → ( 0s ∈ (𝐿‘𝑏) ↔ 0s ∈ (𝐿‘∅)))
30	29	rspcev 3576	. . . . . . . . 9 ⊢ ((∅ ∈ ω ∧ 0s ∈ (𝐿‘∅)) → ∃𝑏 ∈ ω 0s ∈ (𝐿‘𝑏))
31	25, 27, 30	mp2an 705	. . . . . . . 8 ⊢ ∃𝑏 ∈ ω 0s ∈ (𝐿‘𝑏)
32		eliun 4954	. . . . . . . 8 ⊢ ( 0s ∈ ∪ 𝑏 ∈ ω (𝐿‘𝑏) ↔ ∃𝑏 ∈ ω 0s ∈ (𝐿‘𝑏))
33	31, 32	mpbir 234	. . . . . . 7 ⊢ 0s ∈ ∪ 𝑏 ∈ ω (𝐿‘𝑏)
34		fo1st 8021	. . . . . . . . . . 11 ⊢ 1st :V–onto→V
35		fofun 6797	. . . . . . . . . . 11 ⊢ (1st :V–onto→V → Fun 1st )
36	34, 35	ax-mp 5	. . . . . . . . . 10 ⊢ Fun 1st
37		rdgfun 8424	. . . . . . . . . . 11 ⊢ Fun 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 }, ∅⟩)
38	11	funeqi 6560	. . . . . . . . . . 11 ⊢ (Fun 𝐹 ↔ Fun rec((𝑝 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd ‘𝑝) / 𝑟⦌⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))⟩), ⟨{ 0s }, ∅⟩))
39	37, 38	mpbir 234	. . . . . . . . . 10 ⊢ Fun 𝐹
40		funco 6580	. . . . . . . . . 10 ⊢ ((Fun 1st ∧ Fun 𝐹) → Fun (1st ∘ 𝐹))
41	36, 39, 40	mp2an 705	. . . . . . . . 9 ⊢ Fun (1st ∘ 𝐹)
42	12	funeqi 6560	. . . . . . . . 9 ⊢ (Fun 𝐿 ↔ Fun (1st ∘ 𝐹))
43	41, 42	mpbir 234	. . . . . . . 8 ⊢ Fun 𝐿
44		funiunfv 7252	. . . . . . . 8 ⊢ (Fun 𝐿 → ∪ 𝑏 ∈ ω (𝐿‘𝑏) = ∪ (𝐿 “ ω))
45	43, 44	ax-mp 5	. . . . . . 7 ⊢ ∪ 𝑏 ∈ ω (𝐿‘𝑏) = ∪ (𝐿 “ ω)
46	33, 45	eleqtri 2858	. . . . . 6 ⊢ 0s ∈ ∪ (𝐿 “ ω)
47		addsrid 28350	. . . . . . . . . 10 ⊢ ( 0s ∈ No → ( 0s +s 0s ) = 0s )
48	20, 47	ax-mp 5	. . . . . . . . 9 ⊢ ( 0s +s 0s ) = 0s
49		muls01 28498	. . . . . . . . . 10 ⊢ ( 0s ∈ No → ( 0s ·s 0s ) = 0s )
50	20, 49	ax-mp 5	. . . . . . . . 9 ⊢ ( 0s ·s 0s ) = 0s
51	48, 50	oveq12i 7432	. . . . . . . 8 ⊢ (( 0s +s 0s ) −s ( 0s ·s 0s )) = ( 0s −s 0s )
52		subsid 28455	. . . . . . . . 9 ⊢ ( 0s ∈ No → ( 0s −s 0s ) = 0s )
53	20, 52	ax-mp 5	. . . . . . . 8 ⊢ ( 0s −s 0s ) = 0s
54	51, 53	eqtr2i 2784	. . . . . . 7 ⊢ 0s = (( 0s +s 0s ) −s ( 0s ·s 0s ))
55	15	cutscld 28169	. . . . . . . . . . 11 ⊢ (𝜑 → (∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω)) ∈ No)
56	17, 55	eqeltrid 2864	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 ∈ No)
57		muls02 28527	. . . . . . . . . 10 ⊢ (𝑌 ∈ No → ( 0s ·s 𝑌) = 0s )
58	56, 57	syl 18	. . . . . . . . 9 ⊢ (𝜑 → ( 0s ·s 𝑌) = 0s )
59		muls01 28498	. . . . . . . . . 10 ⊢ (𝐴 ∈ No → (𝐴 ·s 0s ) = 0s )
60	2, 59	syl 18	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 ·s 0s ) = 0s )
61	58, 60	oveq12d 7438	. . . . . . . 8 ⊢ (𝜑 → (( 0s ·s 𝑌) +s (𝐴 ·s 0s )) = ( 0s +s 0s ))
62	61	oveq1d 7435	. . . . . . 7 ⊢ (𝜑 → ((( 0s ·s 𝑌) +s (𝐴 ·s 0s )) −s ( 0s ·s 0s )) = (( 0s +s 0s ) −s ( 0s ·s 0s )))
63	54, 62	eqtr4id 2814	. . . . . 6 ⊢ (𝜑 → 0s = ((( 0s ·s 𝑌) +s (𝐴 ·s 0s )) −s ( 0s ·s 0s )))
64		oveq1 7427	. . . . . . . . . 10 ⊢ (𝑐 = 0s → (𝑐 ·s 𝑌) = ( 0s ·s 𝑌))
65	64	oveq1d 7435	. . . . . . . . 9 ⊢ (𝑐 = 0s → ((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) = (( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)))
66		oveq1 7427	. . . . . . . . 9 ⊢ (𝑐 = 0s → (𝑐 ·s 𝑑) = ( 0s ·s 𝑑))
67	65, 66	oveq12d 7438	. . . . . . . 8 ⊢ (𝑐 = 0s → (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) = ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) −s ( 0s ·s 𝑑)))
68	67	eqeq2d 2771	. . . . . . 7 ⊢ (𝑐 = 0s → ( 0s = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) ↔ 0s = ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) −s ( 0s ·s 𝑑))))
69		oveq2 7428	. . . . . . . . . 10 ⊢ (𝑑 = 0s → (𝐴 ·s 𝑑) = (𝐴 ·s 0s ))
70	69	oveq2d 7436	. . . . . . . . 9 ⊢ (𝑑 = 0s → (( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) = (( 0s ·s 𝑌) +s (𝐴 ·s 0s )))
71		oveq2 7428	. . . . . . . . 9 ⊢ (𝑑 = 0s → ( 0s ·s 𝑑) = ( 0s ·s 0s ))
72	70, 71	oveq12d 7438	. . . . . . . 8 ⊢ (𝑑 = 0s → ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) −s ( 0s ·s 𝑑)) = ((( 0s ·s 𝑌) +s (𝐴 ·s 0s )) −s ( 0s ·s 0s )))
73	72	eqeq2d 2771	. . . . . . 7 ⊢ (𝑑 = 0s → ( 0s = ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) −s ( 0s ·s 𝑑)) ↔ 0s = ((( 0s ·s 𝑌) +s (𝐴 ·s 0s )) −s ( 0s ·s 0s ))))
74	68, 73	rspc2ev 3588	. . . . . 6 ⊢ (( 0s ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∧ 0s ∈ ∪ (𝐿 “ ω) ∧ 0s = ((( 0s ·s 𝑌) +s (𝐴 ·s 0s )) −s ( 0s ·s 0s ))) → ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω) 0s = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)))
75	24, 46, 63, 74	mp3an12i 1494	. . . . 5 ⊢ (𝜑 → ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω) 0s = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)))
76		eqeq1 2764	. . . . . . 7 ⊢ (𝑏 = 0s → (𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) ↔ 0s = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))))
77	76	2rexbidv 3227	. . . . . 6 ⊢ (𝑏 = 0s → (∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) ↔ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω) 0s = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))))
78	21, 77	elab 3632	. . . . 5 ⊢ ( 0s ∈ {𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ↔ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω) 0s = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)))
79	75, 78	sylibr 237	. . . 4 ⊢ (𝜑 → 0s ∈ {𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))})
80		elun1 4180	. . . 4 ⊢ ( 0s ∈ {𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} → 0s ∈ ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))}))
81	79, 80	syl 18	. . 3 ⊢ (𝜑 → 0s ∈ ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))}))
82		eqid 2760	. . . . . . 7 ⊢ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))) = (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)))
83	82	rnmpo 7553	. . . . . 6 ⊢ ran (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))) = {𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))}
84		sltsex1 28149	. . . . . . . . 9 ⊢ (({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) <<s (R‘𝐴) → ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∈ V)
85	10, 84	syl 18	. . . . . . . 8 ⊢ (𝜑 → ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∈ V)
86		sltsex1 28149	. . . . . . . . 9 ⊢ (∪ (𝐿 “ ω) <<s ∪ (𝑅 “ ω) → ∪ (𝐿 “ ω) ∈ V)
87	15, 86	syl 18	. . . . . . . 8 ⊢ (𝜑 → ∪ (𝐿 “ ω) ∈ V)
88		mpoexga 8090	. . . . . . . 8 ⊢ ((({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∈ V ∧ ∪ (𝐿 “ ω) ∈ V) → (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))) ∈ V)
89	85, 87, 88	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))) ∈ V)
90		rnexg 7914	. . . . . . 7 ⊢ ((𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))) ∈ V → ran (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))) ∈ V)
91	89, 90	syl 18	. . . . . 6 ⊢ (𝜑 → ran (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))) ∈ V)
92	83, 91	eqeltrrid 2865	. . . . 5 ⊢ (𝜑 → {𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ∈ V)
93		eqid 2760	. . . . . . 7 ⊢ (𝑐 ∈ (R‘𝐴), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))) = (𝑐 ∈ (R‘𝐴), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)))
94	93	rnmpo 7553	. . . . . 6 ⊢ ran (𝑐 ∈ (R‘𝐴), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))) = {𝑏 ∣ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))}
95		fvex 6898	. . . . . . . 8 ⊢ (R‘𝐴) ∈ V
96		sltsex2 28150	. . . . . . . . 9 ⊢ (∪ (𝐿 “ ω) <<s ∪ (𝑅 “ ω) → ∪ (𝑅 “ ω) ∈ V)
97	15, 96	syl 18	. . . . . . . 8 ⊢ (𝜑 → ∪ (𝑅 “ ω) ∈ V)
98		mpoexga 8090	. . . . . . . 8 ⊢ (((R‘𝐴) ∈ V ∧ ∪ (𝑅 “ ω) ∈ V) → (𝑐 ∈ (R‘𝐴), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))) ∈ V)
99	95, 97, 98	sylancr 599	. . . . . . 7 ⊢ (𝜑 → (𝑐 ∈ (R‘𝐴), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))) ∈ V)
100		rnexg 7914	. . . . . . 7 ⊢ ((𝑐 ∈ (R‘𝐴), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))) ∈ V → ran (𝑐 ∈ (R‘𝐴), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))) ∈ V)
101	99, 100	syl 18	. . . . . 6 ⊢ (𝜑 → ran (𝑐 ∈ (R‘𝐴), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))) ∈ V)
102	94, 101	eqeltrrid 2865	. . . . 5 ⊢ (𝜑 → {𝑏 ∣ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ∈ V)
103	92, 102	unexd 7768	. . . 4 ⊢ (𝜑 → ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))}) ∈ V)
104		snex 5396	. . . . 5 ⊢ { 1s } ∈ V
105	104	a1i 11	. . . 4 ⊢ (𝜑 → { 1s } ∈ V)
106		sltsss1 28151	. . . . . . . . . . . . . 14 ⊢ (({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) <<s (R‘𝐴) → ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ⊆ No)
107	10, 106	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ⊆ No)
108	107	sselda 3908	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})) → 𝑐 ∈ No)
109	108	adantrr 730	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 𝑐 ∈ No)
110	56	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 𝑌 ∈ No)
111	109, 110	mulscld 28521	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝑐 ·s 𝑌) ∈ No)
112	2	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 𝐴 ∈ No)
113		sltsss1 28151	. . . . . . . . . . . . . 14 ⊢ (∪ (𝐿 “ ω) <<s ∪ (𝑅 “ ω) → ∪ (𝐿 “ ω) ⊆ No)
114	15, 113	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∪ (𝐿 “ ω) ⊆ No)
115	114	sselda 3908	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝐿 “ ω)) → 𝑑 ∈ No)
116	115	adantrl 729	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 𝑑 ∈ No)
117	112, 116	mulscld 28521	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝐴 ·s 𝑑) ∈ No)
118	111, 117	addscld 28366	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) ∈ No)
119	109, 116	mulscld 28521	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝑐 ·s 𝑑) ∈ No)
120	118, 119	subscld 28449	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) ∈ No)
121		eleq1 2848	. . . . . . . 8 ⊢ (𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) → (𝑏 ∈ No ↔ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) ∈ No))
122	120, 121	syl5ibrcom 250	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) → 𝑏 ∈ No))
123	122	rexlimdvva 3219	. . . . . 6 ⊢ (𝜑 → (∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) → 𝑏 ∈ No))
124	123	abssdv 3992	. . . . 5 ⊢ (𝜑 → {𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ⊆ No)
125		rightssno 28260	. . . . . . . . . . . . . 14 ⊢ (R‘𝐴) ⊆ No
126	125	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → (R‘𝐴) ⊆ No)
127	126	sselda 3908	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ (R‘𝐴)) → 𝑐 ∈ No)
128	127	adantrr 730	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝑐 ∈ No)
129	56	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝑌 ∈ No)
130	128, 129	mulscld 28521	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝑐 ·s 𝑌) ∈ No)
131	2	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝐴 ∈ No)
132		sltsss2 28152	. . . . . . . . . . . . . 14 ⊢ (∪ (𝐿 “ ω) <<s ∪ (𝑅 “ ω) → ∪ (𝑅 “ ω) ⊆ No)
133	15, 132	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∪ (𝑅 “ ω) ⊆ No)
134	133	sselda 3908	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝑅 “ ω)) → 𝑑 ∈ No)
135	134	adantrl 729	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝑑 ∈ No)
136	131, 135	mulscld 28521	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝐴 ·s 𝑑) ∈ No)
137	130, 136	addscld 28366	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) ∈ No)
138	128, 135	mulscld 28521	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝑐 ·s 𝑑) ∈ No)
139	137, 138	subscld 28449	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) ∈ No)
140	139, 121	syl5ibrcom 250	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) → 𝑏 ∈ No))
141	140	rexlimdvva 3219	. . . . . 6 ⊢ (𝜑 → (∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) → 𝑏 ∈ No))
142	141	abssdv 3992	. . . . 5 ⊢ (𝜑 → {𝑏 ∣ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ⊆ No)
143	124, 142	unssd 4190	. . . 4 ⊢ (𝜑 → ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))}) ⊆ No)
144		1no 28196	. . . . 5 ⊢ 1s ∈ No
145		snssi 4745	. . . . 5 ⊢ ( 1s ∈ No → { 1s } ⊆ No)
146	144, 145	mp1i 14	. . . 4 ⊢ (𝜑 → { 1s } ⊆ No)
147		elun 4152	. . . . . . . . 9 ⊢ (𝑒 ∈ ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))}) ↔ (𝑒 ∈ {𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ∨ 𝑒 ∈ {𝑏 ∣ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))}))
148		vex 3454	. . . . . . . . . . 11 ⊢ 𝑒 ∈ V
149		eqeq1 2764	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑒 → (𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) ↔ 𝑒 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))))
150	149	2rexbidv 3227	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑒 → (∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) ↔ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑒 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))))
151	148, 150	elab 3632	. . . . . . . . . 10 ⊢ (𝑒 ∈ {𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ↔ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑒 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)))
152	149	2rexbidv 3227	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑒 → (∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) ↔ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑒 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))))
153	148, 152	elab 3632	. . . . . . . . . 10 ⊢ (𝑒 ∈ {𝑏 ∣ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ↔ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑒 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)))
154	151, 153	orbi12i 928	. . . . . . . . 9 ⊢ ((𝑒 ∈ {𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ∨ 𝑒 ∈ {𝑏 ∣ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))}) ↔ (∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑒 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) ∨ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑒 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))))
155	147, 154	bitri 278	. . . . . . . 8 ⊢ (𝑒 ∈ ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))}) ↔ (∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑒 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) ∨ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑒 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))))
156		elun 4152	. . . . . . . . . . . . . 14 ⊢ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ↔ (𝑐 ∈ { 0s } ∨ 𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}))
157		velsn 4599	. . . . . . . . . . . . . . 15 ⊢ (𝑐 ∈ { 0s } ↔ 𝑐 = 0s )
158	157	orbi1i 927	. . . . . . . . . . . . . 14 ⊢ ((𝑐 ∈ { 0s } ∨ 𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ↔ (𝑐 = 0s ∨ 𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}))
159	156, 158	bitri 278	. . . . . . . . . . . . 13 ⊢ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ↔ (𝑐 = 0s ∨ 𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}))
160	58	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝐿 “ ω)) → ( 0s ·s 𝑌) = 0s )
161	160	oveq1d 7435	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝐿 “ ω)) → (( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) = ( 0s +s (𝐴 ·s 𝑑)))
162		muls02 28527	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 ∈ No → ( 0s ·s 𝑑) = 0s )
163	115, 162	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝐿 “ ω)) → ( 0s ·s 𝑑) = 0s )
164	161, 163	oveq12d 7438	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝐿 “ ω)) → ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) −s ( 0s ·s 𝑑)) = (( 0s +s (𝐴 ·s 𝑑)) −s 0s ))
165	2	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝐿 “ ω)) → 𝐴 ∈ No)
166	165, 115	mulscld 28521	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝐿 “ ω)) → (𝐴 ·s 𝑑) ∈ No)
167		addslid 28354	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ·s 𝑑) ∈ No → ( 0s +s (𝐴 ·s 𝑑)) = (𝐴 ·s 𝑑))
168	166, 167	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝐿 “ ω)) → ( 0s +s (𝐴 ·s 𝑑)) = (𝐴 ·s 𝑑))
169	168	oveq1d 7435	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝐿 “ ω)) → (( 0s +s (𝐴 ·s 𝑑)) −s 0s ) = ((𝐴 ·s 𝑑) −s 0s ))
170		subsid1 28454	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ·s 𝑑) ∈ No → ((𝐴 ·s 𝑑) −s 0s ) = (𝐴 ·s 𝑑))
171	166, 170	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝐿 “ ω)) → ((𝐴 ·s 𝑑) −s 0s ) = (𝐴 ·s 𝑑))
172	164, 169, 171	3eqtrd 2799	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝐿 “ ω)) → ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) −s ( 0s ·s 𝑑)) = (𝐴 ·s 𝑑))
173		eliun 4954	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 ∈ ∪ 𝑖 ∈ ω (𝐿‘𝑖) ↔ ∃𝑖 ∈ ω 𝑑 ∈ (𝐿‘𝑖))
174		funiunfv 7252	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Fun 𝐿 → ∪ 𝑖 ∈ ω (𝐿‘𝑖) = ∪ (𝐿 “ ω))
175	43, 174	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∪ 𝑖 ∈ ω (𝐿‘𝑖) = ∪ (𝐿 “ ω)
176	175	eleq2i 2852	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 ∈ ∪ 𝑖 ∈ ω (𝐿‘𝑖) ↔ 𝑑 ∈ ∪ (𝐿 “ ω))
177	173, 176	bitr3i 280	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑖 ∈ ω 𝑑 ∈ (𝐿‘𝑖) ↔ 𝑑 ∈ ∪ (𝐿 “ ω))
178	11, 12, 13, 2, 3, 14	precsexlem9 28601	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑖 ∈ ω) → (∀𝑑 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑑) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝑖) 1s <s (𝐴 ·s 𝑐)))
179	178	simpld 500	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ ω) → ∀𝑑 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑑) <s 1s )
180		rsp 3250	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑑 ∈ (𝐿‘𝑖)(𝐴 ·s 𝑑) <s 1s → (𝑑 ∈ (𝐿‘𝑖) → (𝐴 ·s 𝑑) <s 1s ))
181	179, 180	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ ω) → (𝑑 ∈ (𝐿‘𝑖) → (𝐴 ·s 𝑑) <s 1s ))
182	181	rexlimdva 3163	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (∃𝑖 ∈ ω 𝑑 ∈ (𝐿‘𝑖) → (𝐴 ·s 𝑑) <s 1s ))
183	177, 182	biimtrrid 246	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑑 ∈ ∪ (𝐿 “ ω) → (𝐴 ·s 𝑑) <s 1s ))
184	183	imp 412	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝐿 “ ω)) → (𝐴 ·s 𝑑) <s 1s )
185	172, 184	eqbrtrd 5126	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝐿 “ ω)) → ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) −s ( 0s ·s 𝑑)) <s 1s )
186	185	ex 418	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑑 ∈ ∪ (𝐿 “ ω) → ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) −s ( 0s ·s 𝑑)) <s 1s ))
187	67	breq1d 5112	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = 0s → ((((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) <s 1s ↔ ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) −s ( 0s ·s 𝑑)) <s 1s ))
188	187	imbi2d 343	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 0s → ((𝑑 ∈ ∪ (𝐿 “ ω) → (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) <s 1s ) ↔ (𝑑 ∈ ∪ (𝐿 “ ω) → ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) −s ( 0s ·s 𝑑)) <s 1s )))
189	186, 188	syl5ibrcom 250	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑐 = 0s → (𝑑 ∈ ∪ (𝐿 “ ω) → (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) <s 1s )))
190		cutcuts 28167	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∪ (𝐿 “ ω) <<s ∪ (𝑅 “ ω) → ((∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω)) ∈ No ∧ ∪ (𝐿 “ ω) <<s {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))} ∧ {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))} <<s ∪ (𝑅 “ ω)))
191	15, 190	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω)) ∈ No ∧ ∪ (𝐿 “ ω) <<s {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))} ∧ {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))} <<s ∪ (𝑅 “ ω)))
192	191	simp3d 1162	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))} <<s ∪ (𝑅 “ ω))
193	192	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))} <<s ∪ (𝑅 “ ω))
194		ovex 7453	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω)) ∈ V
195	194	snid 4622	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω)) ∈ {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))}
196	17, 195	eqeltri 2856	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑌 ∈ {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))}
197	196	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 𝑌 ∈ {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))})
198		peano2 7901	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑖 ∈ ω → suc 𝑖 ∈ ω)
199	198	ad2antrl 741	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝐿‘𝑖))) → suc 𝑖 ∈ ω)
200		eqid 2760	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐)
201		oveq1 7427	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑥𝐿 = 𝑐 → (𝑥𝐿 −s 𝐴) = (𝑐 −s 𝐴))
202	201	oveq1d 7435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑥𝐿 = 𝑐 → ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿) = ((𝑐 −s 𝐴) ·s 𝑦𝐿))
203	202	oveq2d 7436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥𝐿 = 𝑐 → ( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) = ( 1s +s ((𝑐 −s 𝐴) ·s 𝑦𝐿)))
204		id 23	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥𝐿 = 𝑐 → 𝑥𝐿 = 𝑐)
205	203, 204	oveq12d 7438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑥𝐿 = 𝑐 → (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) = (( 1s +s ((𝑐 −s 𝐴) ·s 𝑦𝐿)) /su 𝑐))
206	205	eqeq2d 2771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥𝐿 = 𝑐 → ((( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) ↔ (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑐 −s 𝐴) ·s 𝑦𝐿)) /su 𝑐)))
207		oveq2 7428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑦𝐿 = 𝑑 → ((𝑐 −s 𝐴) ·s 𝑦𝐿) = ((𝑐 −s 𝐴) ·s 𝑑))
208	207	oveq2d 7436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑦𝐿 = 𝑑 → ( 1s +s ((𝑐 −s 𝐴) ·s 𝑦𝐿)) = ( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)))
209	208	oveq1d 7435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑦𝐿 = 𝑑 → (( 1s +s ((𝑐 −s 𝐴) ·s 𝑦𝐿)) /su 𝑐) = (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐))
210	209	eqeq2d 2771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑦𝐿 = 𝑑 → ((( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑐 −s 𝐴) ·s 𝑦𝐿)) /su 𝑐) ↔ (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐)))
211	206, 210	rspc2ev 3588	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ (𝐿‘𝑖) ∧ (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐)) → ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑖)(( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿))
212	200, 211	mp3an3 1479	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ (𝐿‘𝑖)) → ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑖)(( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿))
213	212	ad2ant2l 759	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝐿‘𝑖))) → ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑖)(( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿))
214		ovex 7453	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ V
215		eqeq1 2764	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑎 = (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) → (𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) ↔ (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)))
216	215	2rexbidv 3227	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) → (∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) ↔ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑖)(( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)))
217	214, 216	elab 3632	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ↔ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑖)(( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿))
218	213, 217	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝐿‘𝑖))) → (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)})
219		elun1 4180	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} → (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))
220		elun2 4181	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}) → (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ((𝑅‘𝑖) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)})))
221	218, 219, 220	3syl 19	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝐿‘𝑖))) → (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ((𝑅‘𝑖) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)})))
222	11, 12, 13	precsexlem5 28597	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 ∈ ω → (𝑅‘suc 𝑖) = ((𝑅‘𝑖) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)})))
223	222	ad2antrl 741	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝐿‘𝑖))) → (𝑅‘suc 𝑖) = ((𝑅‘𝑖) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)})))
224	221, 223	eleqtrrd 2863	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝐿‘𝑖))) → (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝑅‘suc 𝑖))
225		fveq2 6885	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗 = suc 𝑖 → (𝑅‘𝑗) = (𝑅‘suc 𝑖))
226	225	eleq2d 2846	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 = suc 𝑖 → ((( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝑅‘𝑗) ↔ (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝑅‘suc 𝑖)))
227	226	rspcev 3576	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((suc 𝑖 ∈ ω ∧ (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝑅‘suc 𝑖)) → ∃𝑗 ∈ ω (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝑅‘𝑗))
228	199, 224, 227	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝐿‘𝑖))) → ∃𝑗 ∈ ω (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝑅‘𝑗))
229	228	rexlimdvaa 3164	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) → (∃𝑖 ∈ ω 𝑑 ∈ (𝐿‘𝑖) → ∃𝑗 ∈ ω (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝑅‘𝑗)))
230		eliun 4954	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ∪ 𝑗 ∈ ω (𝑅‘𝑗) ↔ ∃𝑗 ∈ ω (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝑅‘𝑗))
231		fo2nd 8022	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 2nd :V–onto→V
232		fofun 6797	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (2nd :V–onto→V → Fun 2nd )
233	231, 232	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Fun 2nd
234		funco 6580	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((Fun 2nd ∧ Fun 𝐹) → Fun (2nd ∘ 𝐹))
235	233, 39, 234	mp2an 705	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Fun (2nd ∘ 𝐹)
236	13	funeqi 6560	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Fun 𝑅 ↔ Fun (2nd ∘ 𝐹))
237	235, 236	mpbir 234	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Fun 𝑅
238		funiunfv 7252	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (Fun 𝑅 → ∪ 𝑗 ∈ ω (𝑅‘𝑗) = ∪ (𝑅 “ ω))
239	237, 238	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ∪ 𝑗 ∈ ω (𝑅‘𝑗) = ∪ (𝑅 “ ω)
240	239	eleq2i 2852	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ∪ 𝑗 ∈ ω (𝑅‘𝑗) ↔ (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ∪ (𝑅 “ ω))
241	230, 240	bitr3i 280	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑗 ∈ ω (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝑅‘𝑗) ↔ (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ∪ (𝑅 “ ω))
242	229, 177, 241	3imtr3g 298	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) → (𝑑 ∈ ∪ (𝐿 “ ω) → (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ∪ (𝑅 “ ω)))
243	242	impr 460	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ∪ (𝑅 “ ω))
244	193, 197, 243	sltssepcd 28158	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 𝑌 <s (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐))
245	56	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 𝑌 ∈ No)
246	144	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 1s ∈ No)
247		leftssno 28259	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (L‘𝐴) ⊆ No
248	6, 247	sstri 3917	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ⊆ No
249	248	sseli 3904	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} → 𝑐 ∈ No)
250	249	adantl 487	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) → 𝑐 ∈ No)
251	2	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) → 𝐴 ∈ No)
252	250, 251	subscld 28449	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) → (𝑐 −s 𝐴) ∈ No)
253	252	adantrr 730	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝑐 −s 𝐴) ∈ No)
254	115	adantrl 729	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 𝑑 ∈ No)
255	253, 254	mulscld 28521	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ((𝑐 −s 𝐴) ·s 𝑑) ∈ No)
256	246, 255	addscld 28366	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) ∈ No)
257	249	ad2antrl 741	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 𝑐 ∈ No)
258		breq2 5106	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑐 → ( 0s <s 𝑥 ↔ 0s <s 𝑐))
259	258	elrab 3644	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ↔ (𝑐 ∈ (L‘𝐴) ∧ 0s <s 𝑐))
260	259	simprbi 503	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} → 0s <s 𝑐)
261	260	ad2antrl 741	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 0s <s 𝑐)
262	260	adantl 487	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) → 0s <s 𝑐)
263		breq2 5106	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥𝑂 = 𝑐 → ( 0s <s 𝑥𝑂 ↔ 0s <s 𝑐))
264		oveq1 7427	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥𝑂 = 𝑐 → (𝑥𝑂 ·s 𝑦) = (𝑐 ·s 𝑦))
265	264	eqeq1d 2762	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥𝑂 = 𝑐 → ((𝑥𝑂 ·s 𝑦) = 1s ↔ (𝑐 ·s 𝑦) = 1s ))
266	265	rexbidv 3186	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥𝑂 = 𝑐 → (∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ↔ ∃𝑦 ∈ No (𝑐 ·s 𝑦) = 1s ))
267	263, 266	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥𝑂 = 𝑐 → (( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ) ↔ ( 0s <s 𝑐 → ∃𝑦 ∈ No (𝑐 ·s 𝑦) = 1s )))
268	14	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) → ∀𝑥𝑂 ∈ ((L‘𝐴) ∪ (R‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ))
269		ssun1 4176	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (L‘𝐴) ⊆ ((L‘𝐴) ∪ (R‘𝐴))
270	6, 269	sstri 3917	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ⊆ ((L‘𝐴) ∪ (R‘𝐴))
271	270	sseli 3904	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} → 𝑐 ∈ ((L‘𝐴) ∪ (R‘𝐴)))
272	271	adantl 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) → 𝑐 ∈ ((L‘𝐴) ∪ (R‘𝐴)))
273	267, 268, 272	rspcdva 3577	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) → ( 0s <s 𝑐 → ∃𝑦 ∈ No (𝑐 ·s 𝑦) = 1s ))
274	262, 273	mpd 16	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) → ∃𝑦 ∈ No (𝑐 ·s 𝑦) = 1s )
275	274	adantrr 730	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ∃𝑦 ∈ No (𝑐 ·s 𝑦) = 1s )
276	245, 256, 257, 261, 275	ltmuldivs2wd 28588	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ((𝑐 ·s 𝑌) <s ( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) ↔ 𝑌 <s (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐)))
277	244, 276	mpbird 260	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝑐 ·s 𝑌) <s ( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)))
278	257, 254	mulscld 28521	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝑐 ·s 𝑑) ∈ No)
279	166	adantrl 729	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝐴 ·s 𝑑) ∈ No)
280	246, 278, 279	addsubsassd 28467	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (( 1s +s (𝑐 ·s 𝑑)) −s (𝐴 ·s 𝑑)) = ( 1s +s ((𝑐 ·s 𝑑) −s (𝐴 ·s 𝑑))))
281	2	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 𝐴 ∈ No)
282	257, 281, 254	subsdird 28545	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ((𝑐 −s 𝐴) ·s 𝑑) = ((𝑐 ·s 𝑑) −s (𝐴 ·s 𝑑)))
283	282	oveq2d 7436	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) = ( 1s +s ((𝑐 ·s 𝑑) −s (𝐴 ·s 𝑑))))
284	280, 283	eqtr4d 2798	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (( 1s +s (𝑐 ·s 𝑑)) −s (𝐴 ·s 𝑑)) = ( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)))
285	277, 284	breqtrrd 5132	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝑐 ·s 𝑌) <s (( 1s +s (𝑐 ·s 𝑑)) −s (𝐴 ·s 𝑑)))
286	56	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) → 𝑌 ∈ No)
287	250, 286	mulscld 28521	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) → (𝑐 ·s 𝑌) ∈ No)
288	287	adantrr 730	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝑐 ·s 𝑌) ∈ No)
289	288, 279	addscld 28366	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) ∈ No)
290	289, 278, 246	ltsubaddsd 28475	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ((((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) <s 1s ↔ ((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) <s ( 1s +s (𝑐 ·s 𝑑))))
291	246, 278	addscld 28366	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ( 1s +s (𝑐 ·s 𝑑)) ∈ No)
292	288, 279, 291	ltaddsubsd 28477	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) <s ( 1s +s (𝑐 ·s 𝑑)) ↔ (𝑐 ·s 𝑌) <s (( 1s +s (𝑐 ·s 𝑑)) −s (𝐴 ·s 𝑑))))
293	290, 292	bitrd 282	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ((((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) <s 1s ↔ (𝑐 ·s 𝑌) <s (( 1s +s (𝑐 ·s 𝑑)) −s (𝐴 ·s 𝑑))))
294	285, 293	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) <s 1s )
295	294	exp32 426	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} → (𝑑 ∈ ∪ (𝐿 “ ω) → (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) <s 1s )))
296	189, 295	jaod 873	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑐 = 0s ∨ 𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) → (𝑑 ∈ ∪ (𝐿 “ ω) → (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) <s 1s )))
297	159, 296	biimtrid 245	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) → (𝑑 ∈ ∪ (𝐿 “ ω) → (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) <s 1s )))
298	297	imp32 424	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) <s 1s )
299		breq1 5105	. . . . . . . . . . 11 ⊢ (𝑒 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) → (𝑒 <s 1s ↔ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) <s 1s ))
300	298, 299	syl5ibrcom 250	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝑒 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) → 𝑒 <s 1s ))
301	300	rexlimdvva 3219	. . . . . . . . 9 ⊢ (𝜑 → (∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑒 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) → 𝑒 <s 1s ))
302	192	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))} <<s ∪ (𝑅 “ ω))
303	196	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝑌 ∈ {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))})
304	198	ad2antrl 741	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ (R‘𝐴)) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝑅‘𝑖))) → suc 𝑖 ∈ ω)
305		oveq1 7427	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥𝑅 = 𝑐 → (𝑥𝑅 −s 𝐴) = (𝑐 −s 𝐴))
306	305	oveq1d 7435	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥𝑅 = 𝑐 → ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅) = ((𝑐 −s 𝐴) ·s 𝑦𝑅))
307	306	oveq2d 7436	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥𝑅 = 𝑐 → ( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) = ( 1s +s ((𝑐 −s 𝐴) ·s 𝑦𝑅)))
308		id 23	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥𝑅 = 𝑐 → 𝑥𝑅 = 𝑐)
309	307, 308	oveq12d 7438	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥𝑅 = 𝑐 → (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) = (( 1s +s ((𝑐 −s 𝐴) ·s 𝑦𝑅)) /su 𝑐))
310	309	eqeq2d 2771	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥𝑅 = 𝑐 → ((( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) ↔ (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑐 −s 𝐴) ·s 𝑦𝑅)) /su 𝑐)))
311		oveq2 7428	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦𝑅 = 𝑑 → ((𝑐 −s 𝐴) ·s 𝑦𝑅) = ((𝑐 −s 𝐴) ·s 𝑑))
312	311	oveq2d 7436	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦𝑅 = 𝑑 → ( 1s +s ((𝑐 −s 𝐴) ·s 𝑦𝑅)) = ( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)))
313	312	oveq1d 7435	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦𝑅 = 𝑑 → (( 1s +s ((𝑐 −s 𝐴) ·s 𝑦𝑅)) /su 𝑐) = (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐))
314	313	eqeq2d 2771	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦𝑅 = 𝑑 → ((( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑐 −s 𝐴) ·s 𝑦𝑅)) /su 𝑐) ↔ (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐)))
315	310, 314	rspc2ev 3588	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ (𝑅‘𝑖) ∧ (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐)) → ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑖)(( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅))
316	200, 315	mp3an3 1479	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ (𝑅‘𝑖)) → ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑖)(( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅))
317	316	ad2ant2l 759	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑐 ∈ (R‘𝐴)) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝑅‘𝑖))) → ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑖)(( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅))
318		eqeq1 2764	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) → (𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) ↔ (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)))
319	318	2rexbidv 3227	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) → (∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) ↔ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑖)(( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)))
320	214, 319	elab 3632	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)} ↔ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑖)(( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅))
321	317, 320	sylibr 237	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑐 ∈ (R‘𝐴)) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝑅‘𝑖))) → (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)})
322		elun2 4181	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)} → (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))
323	321, 322, 220	3syl 19	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑐 ∈ (R‘𝐴)) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝑅‘𝑖))) → (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ((𝑅‘𝑖) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)})))
324	222	ad2antrl 741	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑐 ∈ (R‘𝐴)) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝑅‘𝑖))) → (𝑅‘suc 𝑖) = ((𝑅‘𝑖) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)})))
325	323, 324	eleqtrrd 2863	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ (R‘𝐴)) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝑅‘𝑖))) → (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝑅‘suc 𝑖))
326	304, 325, 227	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ (R‘𝐴)) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝑅‘𝑖))) → ∃𝑗 ∈ ω (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝑅‘𝑗))
327	326	rexlimdvaa 3164	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ (R‘𝐴)) → (∃𝑖 ∈ ω 𝑑 ∈ (𝑅‘𝑖) → ∃𝑗 ∈ ω (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝑅‘𝑗)))
328		eliun 4954	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 ∈ ∪ 𝑖 ∈ ω (𝑅‘𝑖) ↔ ∃𝑖 ∈ ω 𝑑 ∈ (𝑅‘𝑖))
329		funiunfv 7252	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Fun 𝑅 → ∪ 𝑖 ∈ ω (𝑅‘𝑖) = ∪ (𝑅 “ ω))
330	237, 329	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ 𝑖 ∈ ω (𝑅‘𝑖) = ∪ (𝑅 “ ω)
331	330	eleq2i 2852	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 ∈ ∪ 𝑖 ∈ ω (𝑅‘𝑖) ↔ 𝑑 ∈ ∪ (𝑅 “ ω))
332	328, 331	bitr3i 280	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑖 ∈ ω 𝑑 ∈ (𝑅‘𝑖) ↔ 𝑑 ∈ ∪ (𝑅 “ ω))
333	327, 332, 241	3imtr3g 298	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ (R‘𝐴)) → (𝑑 ∈ ∪ (𝑅 “ ω) → (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ∪ (𝑅 “ ω)))
334	333	impr 460	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ∪ (𝑅 “ ω))
335	302, 303, 334	sltssepcd 28158	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝑌 <s (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐))
336	144	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 1s ∈ No)
337	2	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ (R‘𝐴)) → 𝐴 ∈ No)
338	127, 337	subscld 28449	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ (R‘𝐴)) → (𝑐 −s 𝐴) ∈ No)
339	338	adantrr 730	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝑐 −s 𝐴) ∈ No)
340	339, 135	mulscld 28521	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ((𝑐 −s 𝐴) ·s 𝑑) ∈ No)
341	336, 340	addscld 28366	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) ∈ No)
342	20	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ (R‘𝐴)) → 0s ∈ No)
343	3	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ (R‘𝐴)) → 0s <s 𝐴)
344		rightgt 28240	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ (R‘𝐴) → 𝐴 <s 𝑐)
345	344	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ (R‘𝐴)) → 𝐴 <s 𝑐)
346	342, 337, 127, 343, 345	ltstrd 28120	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ (R‘𝐴)) → 0s <s 𝑐)
347	346	adantrr 730	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 0s <s 𝑐)
348	14	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ (R‘𝐴)) → ∀𝑥𝑂 ∈ ((L‘𝐴) ∪ (R‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s ))
349		elun2 4181	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 ∈ (R‘𝐴) → 𝑐 ∈ ((L‘𝐴) ∪ (R‘𝐴)))
350	349	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ (R‘𝐴)) → 𝑐 ∈ ((L‘𝐴) ∪ (R‘𝐴)))
351	267, 348, 350	rspcdva 3577	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ (R‘𝐴)) → ( 0s <s 𝑐 → ∃𝑦 ∈ No (𝑐 ·s 𝑦) = 1s ))
352	346, 351	mpd 16	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ (R‘𝐴)) → ∃𝑦 ∈ No (𝑐 ·s 𝑦) = 1s )
353	352	adantrr 730	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ∃𝑦 ∈ No (𝑐 ·s 𝑦) = 1s )
354	129, 341, 128, 347, 353	ltmuldivs2wd 28588	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ((𝑐 ·s 𝑌) <s ( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) ↔ 𝑌 <s (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐)))
355	335, 354	mpbird 260	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝑐 ·s 𝑌) <s ( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)))
356	336, 138, 136	addsubsassd 28467	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (( 1s +s (𝑐 ·s 𝑑)) −s (𝐴 ·s 𝑑)) = ( 1s +s ((𝑐 ·s 𝑑) −s (𝐴 ·s 𝑑))))
357	128, 131, 135	subsdird 28545	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ((𝑐 −s 𝐴) ·s 𝑑) = ((𝑐 ·s 𝑑) −s (𝐴 ·s 𝑑)))
358	357	oveq2d 7436	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) = ( 1s +s ((𝑐 ·s 𝑑) −s (𝐴 ·s 𝑑))))
359	356, 358	eqtr4d 2798	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (( 1s +s (𝑐 ·s 𝑑)) −s (𝐴 ·s 𝑑)) = ( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)))
360	355, 359	breqtrrd 5132	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝑐 ·s 𝑌) <s (( 1s +s (𝑐 ·s 𝑑)) −s (𝐴 ·s 𝑑)))
361	137, 138, 336	ltsubaddsd 28475	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ((((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) <s 1s ↔ ((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) <s ( 1s +s (𝑐 ·s 𝑑))))
362	336, 138	addscld 28366	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ( 1s +s (𝑐 ·s 𝑑)) ∈ No)
363	130, 136, 362	ltaddsubsd 28477	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) <s ( 1s +s (𝑐 ·s 𝑑)) ↔ (𝑐 ·s 𝑌) <s (( 1s +s (𝑐 ·s 𝑑)) −s (𝐴 ·s 𝑑))))
364	361, 363	bitrd 282	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ((((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) <s 1s ↔ (𝑐 ·s 𝑌) <s (( 1s +s (𝑐 ·s 𝑑)) −s (𝐴 ·s 𝑑))))
365	360, 364	mpbird 260	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) <s 1s )
366	365, 299	syl5ibrcom 250	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝑒 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) → 𝑒 <s 1s ))
367	366	rexlimdvva 3219	. . . . . . . . 9 ⊢ (𝜑 → (∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑒 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) → 𝑒 <s 1s ))
368	301, 367	jaod 873	. . . . . . . 8 ⊢ (𝜑 → ((∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑒 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) ∨ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑒 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))) → 𝑒 <s 1s ))
369	155, 368	biimtrid 245	. . . . . . 7 ⊢ (𝜑 → (𝑒 ∈ ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))}) → 𝑒 <s 1s ))
370	369	imp 412	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))})) → 𝑒 <s 1s )
371		velsn 4599	. . . . . . 7 ⊢ (𝑓 ∈ { 1s } ↔ 𝑓 = 1s )
372		breq2 5106	. . . . . . 7 ⊢ (𝑓 = 1s → (𝑒 <s 𝑓 ↔ 𝑒 <s 1s ))
373	371, 372	sylbi 220	. . . . . 6 ⊢ (𝑓 ∈ { 1s } → (𝑒 <s 𝑓 ↔ 𝑒 <s 1s ))
374	370, 373	syl5ibrcom 250	. . . . 5 ⊢ ((𝜑 ∧ 𝑒 ∈ ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))})) → (𝑓 ∈ { 1s } → 𝑒 <s 𝑓))
375	374	3impia 1135	. . . 4 ⊢ ((𝜑 ∧ 𝑒 ∈ ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))}) ∧ 𝑓 ∈ { 1s }) → 𝑒 <s 𝑓)
376	103, 105, 143, 146, 375	sltsd 28154	. . 3 ⊢ (𝜑 → ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))}) <<s { 1s })
377		eqid 2760	. . . . . . 7 ⊢ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))) = (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)))
378	377	rnmpo 7553	. . . . . 6 ⊢ ran (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))) = {𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))}
379		mpoexga 8090	. . . . . . . 8 ⊢ ((({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∈ V ∧ ∪ (𝑅 “ ω) ∈ V) → (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))) ∈ V)
380	85, 97, 379	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))) ∈ V)
381		rnexg 7914	. . . . . . 7 ⊢ ((𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))) ∈ V → ran (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))) ∈ V)
382	380, 381	syl 18	. . . . . 6 ⊢ (𝜑 → ran (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}), 𝑑 ∈ ∪ (𝑅 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))) ∈ V)
383	378, 382	eqeltrrid 2865	. . . . 5 ⊢ (𝜑 → {𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ∈ V)
384		eqid 2760	. . . . . . 7 ⊢ (𝑐 ∈ (R‘𝐴), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))) = (𝑐 ∈ (R‘𝐴), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)))
385	384	rnmpo 7553	. . . . . 6 ⊢ ran (𝑐 ∈ (R‘𝐴), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))) = {𝑏 ∣ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))}
386		mpoexga 8090	. . . . . . . 8 ⊢ (((R‘𝐴) ∈ V ∧ ∪ (𝐿 “ ω) ∈ V) → (𝑐 ∈ (R‘𝐴), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))) ∈ V)
387	95, 87, 386	sylancr 599	. . . . . . 7 ⊢ (𝜑 → (𝑐 ∈ (R‘𝐴), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))) ∈ V)
388		rnexg 7914	. . . . . . 7 ⊢ ((𝑐 ∈ (R‘𝐴), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))) ∈ V → ran (𝑐 ∈ (R‘𝐴), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))) ∈ V)
389	387, 388	syl 18	. . . . . 6 ⊢ (𝜑 → ran (𝑐 ∈ (R‘𝐴), 𝑑 ∈ ∪ (𝐿 “ ω) ↦ (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))) ∈ V)
390	385, 389	eqeltrrid 2865	. . . . 5 ⊢ (𝜑 → {𝑏 ∣ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ∈ V)
391	383, 390	unexd 7768	. . . 4 ⊢ (𝜑 → ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))}) ∈ V)
392	108	adantrr 730	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝑐 ∈ No)
393	56	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝑌 ∈ No)
394	392, 393	mulscld 28521	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝑐 ·s 𝑌) ∈ No)
395	2	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝐴 ∈ No)
396	134	adantrl 729	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝑑 ∈ No)
397	395, 396	mulscld 28521	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝐴 ·s 𝑑) ∈ No)
398	394, 397	addscld 28366	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) ∈ No)
399	392, 396	mulscld 28521	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝑐 ·s 𝑑) ∈ No)
400	398, 399	subscld 28449	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) ∈ No)
401	400, 121	syl5ibrcom 250	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) → 𝑏 ∈ No))
402	401	rexlimdvva 3219	. . . . . 6 ⊢ (𝜑 → (∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) → 𝑏 ∈ No))
403	402	abssdv 3992	. . . . 5 ⊢ (𝜑 → {𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ⊆ No)
404	127	adantrr 730	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 𝑐 ∈ No)
405	56	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 𝑌 ∈ No)
406	404, 405	mulscld 28521	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝑐 ·s 𝑌) ∈ No)
407	2	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 𝐴 ∈ No)
408	115	adantrl 729	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 𝑑 ∈ No)
409	407, 408	mulscld 28521	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝐴 ·s 𝑑) ∈ No)
410	406, 409	addscld 28366	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) ∈ No)
411	404, 408	mulscld 28521	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝑐 ·s 𝑑) ∈ No)
412	410, 411	subscld 28449	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) ∈ No)
413	412, 121	syl5ibrcom 250	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) → 𝑏 ∈ No))
414	413	rexlimdvva 3219	. . . . . 6 ⊢ (𝜑 → (∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) → 𝑏 ∈ No))
415	414	abssdv 3992	. . . . 5 ⊢ (𝜑 → {𝑏 ∣ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ⊆ No)
416	403, 415	unssd 4190	. . . 4 ⊢ (𝜑 → ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))}) ⊆ No)
417		elun 4152	. . . . . . . 8 ⊢ (𝑓 ∈ ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))}) ↔ (𝑓 ∈ {𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ∨ 𝑓 ∈ {𝑏 ∣ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))}))
418		vex 3454	. . . . . . . . . 10 ⊢ 𝑓 ∈ V
419		eqeq1 2764	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑓 → (𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) ↔ 𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))))
420	419	2rexbidv 3227	. . . . . . . . . 10 ⊢ (𝑏 = 𝑓 → (∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) ↔ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))))
421	418, 420	elab 3632	. . . . . . . . 9 ⊢ (𝑓 ∈ {𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ↔ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)))
422	419	2rexbidv 3227	. . . . . . . . . 10 ⊢ (𝑏 = 𝑓 → (∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) ↔ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))))
423	418, 422	elab 3632	. . . . . . . . 9 ⊢ (𝑓 ∈ {𝑏 ∣ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ↔ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)))
424	421, 423	orbi12i 928	. . . . . . . 8 ⊢ ((𝑓 ∈ {𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ∨ 𝑓 ∈ {𝑏 ∣ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))}) ↔ (∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) ∨ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))))
425	417, 424	bitri 278	. . . . . . 7 ⊢ (𝑓 ∈ ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))}) ↔ (∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) ∨ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))))
426		eliun 4954	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 ∈ ∪ 𝑗 ∈ ω (𝑅‘𝑗) ↔ ∃𝑗 ∈ ω 𝑑 ∈ (𝑅‘𝑗))
427	239	eleq2i 2852	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 ∈ ∪ 𝑗 ∈ ω (𝑅‘𝑗) ↔ 𝑑 ∈ ∪ (𝑅 “ ω))
428	426, 427	bitr3i 280	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑗 ∈ ω 𝑑 ∈ (𝑅‘𝑗) ↔ 𝑑 ∈ ∪ (𝑅 “ ω))
429	11, 12, 13, 2, 3, 14	precsexlem9 28601	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ω) → (∀𝑐 ∈ (𝐿‘𝑗)(𝐴 ·s 𝑐) <s 1s ∧ ∀𝑑 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑑)))
430		rsp 3250	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑑 ∈ (𝑅‘𝑗) 1s <s (𝐴 ·s 𝑑) → (𝑑 ∈ (𝑅‘𝑗) → 1s <s (𝐴 ·s 𝑑)))
431	429, 430	simpl2im 513	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ω) → (𝑑 ∈ (𝑅‘𝑗) → 1s <s (𝐴 ·s 𝑑)))
432	431	rexlimdva 3163	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (∃𝑗 ∈ ω 𝑑 ∈ (𝑅‘𝑗) → 1s <s (𝐴 ·s 𝑑)))
433	428, 432	biimtrrid 246	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑑 ∈ ∪ (𝑅 “ ω) → 1s <s (𝐴 ·s 𝑑)))
434	433	imp 412	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝑅 “ ω)) → 1s <s (𝐴 ·s 𝑑))
435	56	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝑅 “ ω)) → 𝑌 ∈ No)
436	57	oveq1d 7435	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑌 ∈ No → (( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) = ( 0s +s (𝐴 ·s 𝑑)))
437	435, 436	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝑅 “ ω)) → (( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) = ( 0s +s (𝐴 ·s 𝑑)))
438	2	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝑅 “ ω)) → 𝐴 ∈ No)
439	438, 134	mulscld 28521	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝑅 “ ω)) → (𝐴 ·s 𝑑) ∈ No)
440	439, 167	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝑅 “ ω)) → ( 0s +s (𝐴 ·s 𝑑)) = (𝐴 ·s 𝑑))
441	437, 440	eqtrd 2795	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝑅 “ ω)) → (( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) = (𝐴 ·s 𝑑))
442	134, 162	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝑅 “ ω)) → ( 0s ·s 𝑑) = 0s )
443	441, 442	oveq12d 7438	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝑅 “ ω)) → ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) −s ( 0s ·s 𝑑)) = ((𝐴 ·s 𝑑) −s 0s ))
444	439, 170	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝑅 “ ω)) → ((𝐴 ·s 𝑑) −s 0s ) = (𝐴 ·s 𝑑))
445	443, 444	eqtrd 2795	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝑅 “ ω)) → ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) −s ( 0s ·s 𝑑)) = (𝐴 ·s 𝑑))
446	434, 445	breqtrrd 5132	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑑 ∈ ∪ (𝑅 “ ω)) → 1s <s ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) −s ( 0s ·s 𝑑)))
447	446	ex 418	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑑 ∈ ∪ (𝑅 “ ω) → 1s <s ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) −s ( 0s ·s 𝑑))))
448	67	breq2d 5114	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 0s → ( 1s <s (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) ↔ 1s <s ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) −s ( 0s ·s 𝑑))))
449	448	imbi2d 343	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 0s → ((𝑑 ∈ ∪ (𝑅 “ ω) → 1s <s (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))) ↔ (𝑑 ∈ ∪ (𝑅 “ ω) → 1s <s ((( 0s ·s 𝑌) +s (𝐴 ·s 𝑑)) −s ( 0s ·s 𝑑)))))
450	447, 449	syl5ibrcom 250	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑐 = 0s → (𝑑 ∈ ∪ (𝑅 “ ω) → 1s <s (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)))))
451	144	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 1s ∈ No)
452	249	ad2antrl 741	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝑐 ∈ No)
453	134	adantrl 729	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝑑 ∈ No)
454	452, 453	mulscld 28521	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝑐 ·s 𝑑) ∈ No)
455	439	adantrl 729	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝐴 ·s 𝑑) ∈ No)
456	451, 454, 455	addsubsassd 28467	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (( 1s +s (𝑐 ·s 𝑑)) −s (𝐴 ·s 𝑑)) = ( 1s +s ((𝑐 ·s 𝑑) −s (𝐴 ·s 𝑑))))
457	2	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝐴 ∈ No)
458	452, 457, 453	subsdird 28545	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ((𝑐 −s 𝐴) ·s 𝑑) = ((𝑐 ·s 𝑑) −s (𝐴 ·s 𝑑)))
459	458	oveq2d 7436	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) = ( 1s +s ((𝑐 ·s 𝑑) −s (𝐴 ·s 𝑑))))
460	456, 459	eqtr4d 2798	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (( 1s +s (𝑐 ·s 𝑑)) −s (𝐴 ·s 𝑑)) = ( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)))
461	191	simp2d 1161	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∪ (𝐿 “ ω) <<s {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))})
462	461	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ∪ (𝐿 “ ω) <<s {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))})
463	198	ad2antrl 741	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝑅‘𝑖))) → suc 𝑖 ∈ ω)
464	201	oveq1d 7435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥𝐿 = 𝑐 → ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅) = ((𝑐 −s 𝐴) ·s 𝑦𝑅))
465	464	oveq2d 7436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑥𝐿 = 𝑐 → ( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) = ( 1s +s ((𝑐 −s 𝐴) ·s 𝑦𝑅)))
466	465, 204	oveq12d 7438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥𝐿 = 𝑐 → (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) = (( 1s +s ((𝑐 −s 𝐴) ·s 𝑦𝑅)) /su 𝑐))
467	466	eqeq2d 2771	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥𝐿 = 𝑐 → ((( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) ↔ (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑐 −s 𝐴) ·s 𝑦𝑅)) /su 𝑐)))
468	467, 314	rspc2ev 3588	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ (𝑅‘𝑖) ∧ (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐)) → ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)(( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿))
469	200, 468	mp3an3 1479	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ (𝑅‘𝑖)) → ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)(( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿))
470	469	ad2ant2l 759	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝑅‘𝑖))) → ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)(( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿))
471		eqeq1 2764	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) → (𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) ↔ (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)))
472	471	2rexbidv 3227	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) → (∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) ↔ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)(( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)))
473	214, 472	elab 3632	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)} ↔ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)(( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿))
474	470, 473	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝑅‘𝑖))) → (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})
475		elun2 4181	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)} → (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ({𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)}))
476		elun2 4181	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ({𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)}) → (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ((𝐿‘𝑖) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})))
477	474, 475, 476	3syl 19	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝑅‘𝑖))) → (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ((𝐿‘𝑖) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})))
478	11, 12, 13	precsexlem4 28596	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑖 ∈ ω → (𝐿‘suc 𝑖) = ((𝐿‘𝑖) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})))
479	478	ad2antrl 741	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝑅‘𝑖))) → (𝐿‘suc 𝑖) = ((𝐿‘𝑖) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})))
480	477, 479	eleqtrrd 2863	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝑅‘𝑖))) → (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝐿‘suc 𝑖))
481		fveq2 6885	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 = suc 𝑖 → (𝐿‘𝑗) = (𝐿‘suc 𝑖))
482	481	eleq2d 2846	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 = suc 𝑖 → ((( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝐿‘𝑗) ↔ (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝐿‘suc 𝑖)))
483	482	rspcev 3576	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((suc 𝑖 ∈ ω ∧ (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝐿‘suc 𝑖)) → ∃𝑗 ∈ ω (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝐿‘𝑗))
484	463, 480, 483	syl2anc 596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝑅‘𝑖))) → ∃𝑗 ∈ ω (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝐿‘𝑗))
485	484	rexlimdvaa 3164	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) → (∃𝑖 ∈ ω 𝑑 ∈ (𝑅‘𝑖) → ∃𝑗 ∈ ω (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝐿‘𝑗)))
486		eliun 4954	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ∪ 𝑗 ∈ ω (𝐿‘𝑗) ↔ ∃𝑗 ∈ ω (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝐿‘𝑗))
487		funiunfv 7252	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (Fun 𝐿 → ∪ 𝑗 ∈ ω (𝐿‘𝑗) = ∪ (𝐿 “ ω))
488	43, 487	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ∪ 𝑗 ∈ ω (𝐿‘𝑗) = ∪ (𝐿 “ ω)
489	488	eleq2i 2852	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ∪ 𝑗 ∈ ω (𝐿‘𝑗) ↔ (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ∪ (𝐿 “ ω))
490	486, 489	bitr3i 280	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑗 ∈ ω (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝐿‘𝑗) ↔ (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ∪ (𝐿 “ ω))
491	485, 332, 490	3imtr3g 298	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) → (𝑑 ∈ ∪ (𝑅 “ ω) → (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ∪ (𝐿 “ ω)))
492	491	impr 460	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ∪ (𝐿 “ ω))
493	196	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝑌 ∈ {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))})
494	462, 492, 493	sltssepcd 28158	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) <s 𝑌)
495	252	adantrr 730	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝑐 −s 𝐴) ∈ No)
496	495, 453	mulscld 28521	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ((𝑐 −s 𝐴) ·s 𝑑) ∈ No)
497	451, 496	addscld 28366	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) ∈ No)
498	56	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 𝑌 ∈ No)
499	260	ad2antrl 741	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 0s <s 𝑐)
500	274	adantrr 730	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ∃𝑦 ∈ No (𝑐 ·s 𝑦) = 1s )
501	497, 498, 452, 499, 500	ltdivmulswd 28585	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ((( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) <s 𝑌 ↔ ( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) <s (𝑐 ·s 𝑌)))
502	494, 501	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) <s (𝑐 ·s 𝑌))
503	460, 502	eqbrtrd 5126	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (( 1s +s (𝑐 ·s 𝑑)) −s (𝐴 ·s 𝑑)) <s (𝑐 ·s 𝑌))
504	451, 454	addscld 28366	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ( 1s +s (𝑐 ·s 𝑑)) ∈ No)
505	287	adantrr 730	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝑐 ·s 𝑌) ∈ No)
506	504, 455, 505	ltsubaddsd 28475	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ((( 1s +s (𝑐 ·s 𝑑)) −s (𝐴 ·s 𝑑)) <s (𝑐 ·s 𝑌) ↔ ( 1s +s (𝑐 ·s 𝑑)) <s ((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑))))
507	505, 455	addscld 28366	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) ∈ No)
508	451, 454, 507	ltaddsubsd 28477	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (( 1s +s (𝑐 ·s 𝑑)) <s ((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) ↔ 1s <s (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))))
509	506, 508	bitrd 282	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → ((( 1s +s (𝑐 ·s 𝑑)) −s (𝐴 ·s 𝑑)) <s (𝑐 ·s 𝑌) ↔ 1s <s (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))))
510	503, 509	mpbid 235	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 1s <s (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)))
511	510	exp32 426	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥} → (𝑑 ∈ ∪ (𝑅 “ ω) → 1s <s (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)))))
512	450, 511	jaod 873	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑐 = 0s ∨ 𝑐 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) → (𝑑 ∈ ∪ (𝑅 “ ω) → 1s <s (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)))))
513	159, 512	biimtrid 245	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) → (𝑑 ∈ ∪ (𝑅 “ ω) → 1s <s (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)))))
514	513	imp32 424	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → 1s <s (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)))
515		breq2 5106	. . . . . . . . . 10 ⊢ (𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) → ( 1s <s 𝑓 ↔ 1s <s (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))))
516	514, 515	syl5ibrcom 250	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}) ∧ 𝑑 ∈ ∪ (𝑅 “ ω))) → (𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) → 1s <s 𝑓))
517	516	rexlimdvva 3219	. . . . . . . 8 ⊢ (𝜑 → (∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) → 1s <s 𝑓))
518	144	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 1s ∈ No)
519	518, 411, 409	addsubsassd 28467	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (( 1s +s (𝑐 ·s 𝑑)) −s (𝐴 ·s 𝑑)) = ( 1s +s ((𝑐 ·s 𝑑) −s (𝐴 ·s 𝑑))))
520	404, 407, 408	subsdird 28545	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ((𝑐 −s 𝐴) ·s 𝑑) = ((𝑐 ·s 𝑑) −s (𝐴 ·s 𝑑)))
521	520	oveq2d 7436	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) = ( 1s +s ((𝑐 ·s 𝑑) −s (𝐴 ·s 𝑑))))
522	519, 521	eqtr4d 2798	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (( 1s +s (𝑐 ·s 𝑑)) −s (𝐴 ·s 𝑑)) = ( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)))
523	461	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ∪ (𝐿 “ ω) <<s {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))})
524	198	ad2antrl 741	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ (R‘𝐴)) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝐿‘𝑖))) → suc 𝑖 ∈ ω)
525	305	oveq1d 7435	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥𝑅 = 𝑐 → ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿) = ((𝑐 −s 𝐴) ·s 𝑦𝐿))
526	525	oveq2d 7436	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥𝑅 = 𝑐 → ( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) = ( 1s +s ((𝑐 −s 𝐴) ·s 𝑦𝐿)))
527	526, 308	oveq12d 7438	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥𝑅 = 𝑐 → (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) = (( 1s +s ((𝑐 −s 𝐴) ·s 𝑦𝐿)) /su 𝑐))
528	527	eqeq2d 2771	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥𝑅 = 𝑐 → ((( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) ↔ (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑐 −s 𝐴) ·s 𝑦𝐿)) /su 𝑐)))
529	528, 210	rspc2ev 3588	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ (𝐿‘𝑖) ∧ (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐)) → ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)(( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅))
530	200, 529	mp3an3 1479	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ (𝐿‘𝑖)) → ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)(( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅))
531	530	ad2ant2l 759	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑐 ∈ (R‘𝐴)) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝐿‘𝑖))) → ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)(( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅))
532		eqeq1 2764	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) → (𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) ↔ (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)))
533	532	2rexbidv 3227	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) → (∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) ↔ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)(( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)))
534	214, 533	elab 3632	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ↔ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)(( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅))
535	531, 534	sylibr 237	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑐 ∈ (R‘𝐴)) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝐿‘𝑖))) → (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)})
536		elun1 4180	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} → (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ({𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)}))
537	535, 536, 476	3syl 19	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ (R‘𝐴)) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝐿‘𝑖))) → (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ((𝐿‘𝑖) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})))
538	478	ad2antrl 741	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ (R‘𝐴)) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝐿‘𝑖))) → (𝐿‘suc 𝑖) = ((𝐿‘𝑖) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝑖)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝑖)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})))
539	537, 538	eleqtrrd 2863	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ (R‘𝐴)) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝐿‘𝑖))) → (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝐿‘suc 𝑖))
540	524, 539, 483	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ (R‘𝐴)) ∧ (𝑖 ∈ ω ∧ 𝑑 ∈ (𝐿‘𝑖))) → ∃𝑗 ∈ ω (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝐿‘𝑗))
541	540	rexlimdvaa 3164	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ (R‘𝐴)) → (∃𝑖 ∈ ω 𝑑 ∈ (𝐿‘𝑖) → ∃𝑗 ∈ ω (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ (𝐿‘𝑗)))
542	541, 177, 490	3imtr3g 298	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ (R‘𝐴)) → (𝑑 ∈ ∪ (𝐿 “ ω) → (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ∪ (𝐿 “ ω)))
543	542	impr 460	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) ∈ ∪ (𝐿 “ ω))
544	196	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 𝑌 ∈ {(∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω))})
545	523, 543, 544	sltssepcd 28158	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) <s 𝑌)
546	338	adantrr 730	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝑐 −s 𝐴) ∈ No)
547	546, 408	mulscld 28521	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ((𝑐 −s 𝐴) ·s 𝑑) ∈ No)
548	518, 547	addscld 28366	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) ∈ No)
549	346	adantrr 730	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 0s <s 𝑐)
550	352	adantrr 730	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ∃𝑦 ∈ No (𝑐 ·s 𝑦) = 1s )
551	548, 405, 404, 549, 550	ltdivmulswd 28585	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ((( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) /su 𝑐) <s 𝑌 ↔ ( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) <s (𝑐 ·s 𝑌)))
552	545, 551	mpbid 235	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ( 1s +s ((𝑐 −s 𝐴) ·s 𝑑)) <s (𝑐 ·s 𝑌))
553	522, 552	eqbrtrd 5126	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (( 1s +s (𝑐 ·s 𝑑)) −s (𝐴 ·s 𝑑)) <s (𝑐 ·s 𝑌))
554	518, 411	addscld 28366	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ( 1s +s (𝑐 ·s 𝑑)) ∈ No)
555	554, 409, 406	ltsubaddsd 28475	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ((( 1s +s (𝑐 ·s 𝑑)) −s (𝐴 ·s 𝑑)) <s (𝑐 ·s 𝑌) ↔ ( 1s +s (𝑐 ·s 𝑑)) <s ((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑))))
556	518, 411, 410	ltaddsubsd 28477	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (( 1s +s (𝑐 ·s 𝑑)) <s ((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) ↔ 1s <s (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))))
557	555, 556	bitrd 282	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → ((( 1s +s (𝑐 ·s 𝑑)) −s (𝐴 ·s 𝑑)) <s (𝑐 ·s 𝑌) ↔ 1s <s (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))))
558	553, 557	mpbid 235	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → 1s <s (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)))
559	558, 515	syl5ibrcom 250	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑐 ∈ (R‘𝐴) ∧ 𝑑 ∈ ∪ (𝐿 “ ω))) → (𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) → 1s <s 𝑓))
560	559	rexlimdvva 3219	. . . . . . . 8 ⊢ (𝜑 → (∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) → 1s <s 𝑓))
561	517, 560	jaod 873	. . . . . . 7 ⊢ (𝜑 → ((∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑)) ∨ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑓 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))) → 1s <s 𝑓))
562	425, 561	biimtrid 245	. . . . . 6 ⊢ (𝜑 → (𝑓 ∈ ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))}) → 1s <s 𝑓))
563		velsn 4599	. . . . . . 7 ⊢ (𝑒 ∈ { 1s } ↔ 𝑒 = 1s )
564		breq1 5105	. . . . . . . 8 ⊢ (𝑒 = 1s → (𝑒 <s 𝑓 ↔ 1s <s 𝑓))
565	564	imbi2d 343	. . . . . . 7 ⊢ (𝑒 = 1s → ((𝑓 ∈ ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))}) → 𝑒 <s 𝑓) ↔ (𝑓 ∈ ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))}) → 1s <s 𝑓)))
566	563, 565	sylbi 220	. . . . . 6 ⊢ (𝑒 ∈ { 1s } → ((𝑓 ∈ ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))}) → 𝑒 <s 𝑓) ↔ (𝑓 ∈ ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))}) → 1s <s 𝑓)))
567	562, 566	syl5ibrcom 250	. . . . 5 ⊢ (𝜑 → (𝑒 ∈ { 1s } → (𝑓 ∈ ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))}) → 𝑒 <s 𝑓)))
568	567	3imp 1128	. . . 4 ⊢ ((𝜑 ∧ 𝑒 ∈ { 1s } ∧ 𝑓 ∈ ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))})) → 𝑒 <s 𝑓)
569	105, 391, 146, 416, 568	sltsd 28154	. . 3 ⊢ (𝜑 → { 1s } <<s ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))}))
570	81, 376, 569	cuteq1 28203	. 2 ⊢ (𝜑 → (({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))}) |s ({𝑏 ∣ ∃𝑐 ∈ ({ 0s } ∪ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥})∃𝑑 ∈ ∪ (𝑅 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))} ∪ {𝑏 ∣ ∃𝑐 ∈ (R‘𝐴)∃𝑑 ∈ ∪ (𝐿 “ ω)𝑏 = (((𝑐 ·s 𝑌) +s (𝐴 ·s 𝑑)) −s (𝑐 ·s 𝑑))})) = 1s )
571	19, 570	eqtrd 2795	1 ⊢ (𝜑 → (𝐴 ·s 𝑌) = 1s )

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1569   ∈ wcel 2144  {cab 2738  ∀wral 3076  ∃wrex 3086  {crab 3412  Vcvv 3450  ⦋csb 3846   ⊆ wss 3895   ∪ cun 4149  ∅c0 4278  {csn 4583  ⟨cop 4589  ∪ cuni 4866  ∪ ciun 4950   class class class wbr 5102   ↦ cmpt 5185  ran crn 5651   “ cima 5653   ∘ ccom 5654  suc csuc 6364  Fun wfun 6532  –onto→wfo 6536  ‘cfv 6538  (class class class)co 7420   ∈ cmpo 7422  ωcom 7877  1^st c1st 7999  2^nd c2nd 8000  reccrdg 8417  Nocsur 27997   <s clts 27998   <<s cslts 28143   |s ccuts 28145   0_s c0s 28191   1_s c1s 28192  Lcleft 28211  Rcright 28212   +_s cadds 28345   −_s csubs 28406   ·_s cmuls 28492   /_su cdivs 28573

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-dc 10524

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-tp 4588  df-op 4590  df-ot 4592  df-uni 4867  df-int 4907  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-se 5604  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7878  df-1st 8001  df-2nd 8002  df-frecs 8299  df-wrecs 8330  df-recs 8379  df-rdg 8418  df-1o 8476  df-2o 8477  df-oadd 8480  df-nadd 8675  df-no 28000  df-lts 28001  df-bday 28002  df-les 28102  df-slts 28144  df-cuts 28146  df-0s 28193  df-1s 28194  df-made 28213  df-old 28214  df-left 28216  df-right 28217  df-norec 28324  df-norec2 28335  df-adds 28346  df-negs 28407  df-subs 28408  df-muls 28493  df-divs 28574

This theorem is used by:  precsex  28604