Theorem recexsrlem

Description: The reciprocal of a positive signed real exists. Part of Proposition 9-4.3 of Gleason p. 126. (Contributed by NM, 15-May-1996) (New usage is discouraged.)

	Ref	Expression
Assertion	recexsrlem	⊢ ( 0R <R 𝐴 → ∃ 𝑥 ∈ R ( 𝐴 ·R 𝑥 ) = 1R )

Proof

Step	Hyp	Ref	Expression
1		ltrelsr	⊢ <R ⊆ ( R × R )
2	1	brel	⊢ ( 0R <R 𝐴 → ( 0R ∈ R ∧ 𝐴 ∈ R ) )
3	2	simprd	⊢ ( 0R <R 𝐴 → 𝐴 ∈ R )
4		df-nr	⊢ R = ( ( P × P ) / ~R )
5		breq2	⊢ ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R = 𝐴 → ( 0R <R [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ↔ 0R <R 𝐴 ) )
6		oveq1	⊢ ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R = 𝐴 → ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ·R 𝑥 ) = ( 𝐴 ·R 𝑥 ) )
7	6	eqeq1d	⊢ ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R = 𝐴 → ( ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ·R 𝑥 ) = 1R ↔ ( 𝐴 ·R 𝑥 ) = 1R ) )
8	7	rexbidv	⊢ ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R = 𝐴 → ( ∃ 𝑥 ∈ R ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ·R 𝑥 ) = 1R ↔ ∃ 𝑥 ∈ R ( 𝐴 ·R 𝑥 ) = 1R ) )
9	5 8	imbi12d	⊢ ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R = 𝐴 → ( ( 0R <R [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R → ∃ 𝑥 ∈ R ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ·R 𝑥 ) = 1R ) ↔ ( 0R <R 𝐴 → ∃ 𝑥 ∈ R ( 𝐴 ·R 𝑥 ) = 1R ) ) )
10		gt0srpr	⊢ ( 0R <R [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ↔ 𝑧 <P 𝑦 )
11		ltexpri	⊢ ( 𝑧 <P 𝑦 → ∃ 𝑤 ∈ P ( 𝑧 +P 𝑤 ) = 𝑦 )
12	10 11	sylbi	⊢ ( 0R <R [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R → ∃ 𝑤 ∈ P ( 𝑧 +P 𝑤 ) = 𝑦 )
13		recexpr	⊢ ( 𝑤 ∈ P → ∃ 𝑣 ∈ P ( 𝑤 ·P 𝑣 ) = 1P )
14		1pr	⊢ 1P ∈ P
15		addclpr	⊢ ( ( 𝑣 ∈ P ∧ 1P ∈ P ) → ( 𝑣 +P 1P ) ∈ P )
16	14 15	mpan2	⊢ ( 𝑣 ∈ P → ( 𝑣 +P 1P ) ∈ P )
17		enrex	⊢ ~R ∈ V
18	17 4	ecopqsi	⊢ ( ( ( 𝑣 +P 1P ) ∈ P ∧ 1P ∈ P ) → [ ⟨ ( 𝑣 +P 1P ) , 1P ⟩ ] ~R ∈ R )
19	16 14 18	sylancl	⊢ ( 𝑣 ∈ P → [ ⟨ ( 𝑣 +P 1P ) , 1P ⟩ ] ~R ∈ R )
20	19	ad2antlr	⊢ ( ( ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ∧ 𝑣 ∈ P ) ∧ ( ( 𝑤 ·P 𝑣 ) = 1P ∧ ( 𝑧 +P 𝑤 ) = 𝑦 ) ) → [ ⟨ ( 𝑣 +P 1P ) , 1P ⟩ ] ~R ∈ R )
21	16 14	jctir	⊢ ( 𝑣 ∈ P → ( ( 𝑣 +P 1P ) ∈ P ∧ 1P ∈ P ) )
22	21	anim2i	⊢ ( ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ∧ 𝑣 ∈ P ) → ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ∧ ( ( 𝑣 +P 1P ) ∈ P ∧ 1P ∈ P ) ) )
23	22	adantr	⊢ ( ( ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ∧ 𝑣 ∈ P ) ∧ ( ( 𝑤 ·P 𝑣 ) = 1P ∧ ( 𝑧 +P 𝑤 ) = 𝑦 ) ) → ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ∧ ( ( 𝑣 +P 1P ) ∈ P ∧ 1P ∈ P ) ) )
24		mulsrpr	⊢ ( ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ∧ ( ( 𝑣 +P 1P ) ∈ P ∧ 1P ∈ P ) ) → ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ·R [ ⟨ ( 𝑣 +P 1P ) , 1P ⟩ ] ~R ) = [ ⟨ ( ( 𝑦 ·P ( 𝑣 +P 1P ) ) +P ( 𝑧 ·P 1P ) ) , ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P ( 𝑣 +P 1P ) ) ) ⟩ ] ~R )
25	23 24	syl	⊢ ( ( ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ∧ 𝑣 ∈ P ) ∧ ( ( 𝑤 ·P 𝑣 ) = 1P ∧ ( 𝑧 +P 𝑤 ) = 𝑦 ) ) → ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ·R [ ⟨ ( 𝑣 +P 1P ) , 1P ⟩ ] ~R ) = [ ⟨ ( ( 𝑦 ·P ( 𝑣 +P 1P ) ) +P ( 𝑧 ·P 1P ) ) , ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P ( 𝑣 +P 1P ) ) ) ⟩ ] ~R )
26		oveq1	⊢ ( ( 𝑧 +P 𝑤 ) = 𝑦 → ( ( 𝑧 +P 𝑤 ) ·P 𝑣 ) = ( 𝑦 ·P 𝑣 ) )
27	26	eqcomd	⊢ ( ( 𝑧 +P 𝑤 ) = 𝑦 → ( 𝑦 ·P 𝑣 ) = ( ( 𝑧 +P 𝑤 ) ·P 𝑣 ) )
28		vex	⊢ 𝑧 ∈ V
29		vex	⊢ 𝑤 ∈ V
30		vex	⊢ 𝑣 ∈ V
31		mulcompr	⊢ ( 𝑢 ·P 𝑓 ) = ( 𝑓 ·P 𝑢 )
32		distrpr	⊢ ( 𝑢 ·P ( 𝑓 +P 𝑥 ) ) = ( ( 𝑢 ·P 𝑓 ) +P ( 𝑢 ·P 𝑥 ) )
33	28 29 30 31 32	caovdir	⊢ ( ( 𝑧 +P 𝑤 ) ·P 𝑣 ) = ( ( 𝑧 ·P 𝑣 ) +P ( 𝑤 ·P 𝑣 ) )
34		oveq2	⊢ ( ( 𝑤 ·P 𝑣 ) = 1P → ( ( 𝑧 ·P 𝑣 ) +P ( 𝑤 ·P 𝑣 ) ) = ( ( 𝑧 ·P 𝑣 ) +P 1P ) )
35	33 34	syl5eq	⊢ ( ( 𝑤 ·P 𝑣 ) = 1P → ( ( 𝑧 +P 𝑤 ) ·P 𝑣 ) = ( ( 𝑧 ·P 𝑣 ) +P 1P ) )
36	27 35	sylan9eqr	⊢ ( ( ( 𝑤 ·P 𝑣 ) = 1P ∧ ( 𝑧 +P 𝑤 ) = 𝑦 ) → ( 𝑦 ·P 𝑣 ) = ( ( 𝑧 ·P 𝑣 ) +P 1P ) )
37	36	oveq1d	⊢ ( ( ( 𝑤 ·P 𝑣 ) = 1P ∧ ( 𝑧 +P 𝑤 ) = 𝑦 ) → ( ( 𝑦 ·P 𝑣 ) +P ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P 1P ) ) ) = ( ( ( 𝑧 ·P 𝑣 ) +P 1P ) +P ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P 1P ) ) ) )
38		ovex	⊢ ( 𝑧 ·P 𝑣 ) ∈ V
39	14	elexi	⊢ 1P ∈ V
40		ovex	⊢ ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P 1P ) ) ∈ V
41		addcompr	⊢ ( 𝑢 +P 𝑓 ) = ( 𝑓 +P 𝑢 )
42		addasspr	⊢ ( ( 𝑢 +P 𝑓 ) +P 𝑥 ) = ( 𝑢 +P ( 𝑓 +P 𝑥 ) )
43	38 39 40 41 42	caov32	⊢ ( ( ( 𝑧 ·P 𝑣 ) +P 1P ) +P ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P 1P ) ) ) = ( ( ( 𝑧 ·P 𝑣 ) +P ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P 1P ) ) ) +P 1P )
44	37 43	syl6eq	⊢ ( ( ( 𝑤 ·P 𝑣 ) = 1P ∧ ( 𝑧 +P 𝑤 ) = 𝑦 ) → ( ( 𝑦 ·P 𝑣 ) +P ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P 1P ) ) ) = ( ( ( 𝑧 ·P 𝑣 ) +P ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P 1P ) ) ) +P 1P ) )
45	44	oveq1d	⊢ ( ( ( 𝑤 ·P 𝑣 ) = 1P ∧ ( 𝑧 +P 𝑤 ) = 𝑦 ) → ( ( ( 𝑦 ·P 𝑣 ) +P ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P 1P ) ) ) +P 1P ) = ( ( ( ( 𝑧 ·P 𝑣 ) +P ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P 1P ) ) ) +P 1P ) +P 1P ) )
46		addasspr	⊢ ( ( ( ( 𝑧 ·P 𝑣 ) +P ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P 1P ) ) ) +P 1P ) +P 1P ) = ( ( ( 𝑧 ·P 𝑣 ) +P ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P 1P ) ) ) +P ( 1P +P 1P ) )
47	45 46	syl6eq	⊢ ( ( ( 𝑤 ·P 𝑣 ) = 1P ∧ ( 𝑧 +P 𝑤 ) = 𝑦 ) → ( ( ( 𝑦 ·P 𝑣 ) +P ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P 1P ) ) ) +P 1P ) = ( ( ( 𝑧 ·P 𝑣 ) +P ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P 1P ) ) ) +P ( 1P +P 1P ) ) )
48		distrpr	⊢ ( 𝑦 ·P ( 𝑣 +P 1P ) ) = ( ( 𝑦 ·P 𝑣 ) +P ( 𝑦 ·P 1P ) )
49	48	oveq1i	⊢ ( ( 𝑦 ·P ( 𝑣 +P 1P ) ) +P ( 𝑧 ·P 1P ) ) = ( ( ( 𝑦 ·P 𝑣 ) +P ( 𝑦 ·P 1P ) ) +P ( 𝑧 ·P 1P ) )
50		addasspr	⊢ ( ( ( 𝑦 ·P 𝑣 ) +P ( 𝑦 ·P 1P ) ) +P ( 𝑧 ·P 1P ) ) = ( ( 𝑦 ·P 𝑣 ) +P ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P 1P ) ) )
51	49 50	eqtri	⊢ ( ( 𝑦 ·P ( 𝑣 +P 1P ) ) +P ( 𝑧 ·P 1P ) ) = ( ( 𝑦 ·P 𝑣 ) +P ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P 1P ) ) )
52	51	oveq1i	⊢ ( ( ( 𝑦 ·P ( 𝑣 +P 1P ) ) +P ( 𝑧 ·P 1P ) ) +P 1P ) = ( ( ( 𝑦 ·P 𝑣 ) +P ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P 1P ) ) ) +P 1P )
53		distrpr	⊢ ( 𝑧 ·P ( 𝑣 +P 1P ) ) = ( ( 𝑧 ·P 𝑣 ) +P ( 𝑧 ·P 1P ) )
54	53	oveq2i	⊢ ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P ( 𝑣 +P 1P ) ) ) = ( ( 𝑦 ·P 1P ) +P ( ( 𝑧 ·P 𝑣 ) +P ( 𝑧 ·P 1P ) ) )
55		ovex	⊢ ( 𝑦 ·P 1P ) ∈ V
56		ovex	⊢ ( 𝑧 ·P 1P ) ∈ V
57	55 38 56 41 42	caov12	⊢ ( ( 𝑦 ·P 1P ) +P ( ( 𝑧 ·P 𝑣 ) +P ( 𝑧 ·P 1P ) ) ) = ( ( 𝑧 ·P 𝑣 ) +P ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P 1P ) ) )
58	54 57	eqtri	⊢ ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P ( 𝑣 +P 1P ) ) ) = ( ( 𝑧 ·P 𝑣 ) +P ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P 1P ) ) )
59	58	oveq1i	⊢ ( ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P ( 𝑣 +P 1P ) ) ) +P ( 1P +P 1P ) ) = ( ( ( 𝑧 ·P 𝑣 ) +P ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P 1P ) ) ) +P ( 1P +P 1P ) )
60	47 52 59	3eqtr4g	⊢ ( ( ( 𝑤 ·P 𝑣 ) = 1P ∧ ( 𝑧 +P 𝑤 ) = 𝑦 ) → ( ( ( 𝑦 ·P ( 𝑣 +P 1P ) ) +P ( 𝑧 ·P 1P ) ) +P 1P ) = ( ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P ( 𝑣 +P 1P ) ) ) +P ( 1P +P 1P ) ) )
61		mulclpr	⊢ ( ( 𝑦 ∈ P ∧ ( 𝑣 +P 1P ) ∈ P ) → ( 𝑦 ·P ( 𝑣 +P 1P ) ) ∈ P )
62	16 61	sylan2	⊢ ( ( 𝑦 ∈ P ∧ 𝑣 ∈ P ) → ( 𝑦 ·P ( 𝑣 +P 1P ) ) ∈ P )
63		mulclpr	⊢ ( ( 𝑧 ∈ P ∧ 1P ∈ P ) → ( 𝑧 ·P 1P ) ∈ P )
64	14 63	mpan2	⊢ ( 𝑧 ∈ P → ( 𝑧 ·P 1P ) ∈ P )
65		addclpr	⊢ ( ( ( 𝑦 ·P ( 𝑣 +P 1P ) ) ∈ P ∧ ( 𝑧 ·P 1P ) ∈ P ) → ( ( 𝑦 ·P ( 𝑣 +P 1P ) ) +P ( 𝑧 ·P 1P ) ) ∈ P )
66	62 64 65	syl2an	⊢ ( ( ( 𝑦 ∈ P ∧ 𝑣 ∈ P ) ∧ 𝑧 ∈ P ) → ( ( 𝑦 ·P ( 𝑣 +P 1P ) ) +P ( 𝑧 ·P 1P ) ) ∈ P )
67	66	an32s	⊢ ( ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ∧ 𝑣 ∈ P ) → ( ( 𝑦 ·P ( 𝑣 +P 1P ) ) +P ( 𝑧 ·P 1P ) ) ∈ P )
68		mulclpr	⊢ ( ( 𝑦 ∈ P ∧ 1P ∈ P ) → ( 𝑦 ·P 1P ) ∈ P )
69	14 68	mpan2	⊢ ( 𝑦 ∈ P → ( 𝑦 ·P 1P ) ∈ P )
70		mulclpr	⊢ ( ( 𝑧 ∈ P ∧ ( 𝑣 +P 1P ) ∈ P ) → ( 𝑧 ·P ( 𝑣 +P 1P ) ) ∈ P )
71	16 70	sylan2	⊢ ( ( 𝑧 ∈ P ∧ 𝑣 ∈ P ) → ( 𝑧 ·P ( 𝑣 +P 1P ) ) ∈ P )
72		addclpr	⊢ ( ( ( 𝑦 ·P 1P ) ∈ P ∧ ( 𝑧 ·P ( 𝑣 +P 1P ) ) ∈ P ) → ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P ( 𝑣 +P 1P ) ) ) ∈ P )
73	69 71 72	syl2an	⊢ ( ( 𝑦 ∈ P ∧ ( 𝑧 ∈ P ∧ 𝑣 ∈ P ) ) → ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P ( 𝑣 +P 1P ) ) ) ∈ P )
74	73	anassrs	⊢ ( ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ∧ 𝑣 ∈ P ) → ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P ( 𝑣 +P 1P ) ) ) ∈ P )
75	67 74	jca	⊢ ( ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ∧ 𝑣 ∈ P ) → ( ( ( 𝑦 ·P ( 𝑣 +P 1P ) ) +P ( 𝑧 ·P 1P ) ) ∈ P ∧ ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P ( 𝑣 +P 1P ) ) ) ∈ P ) )
76		addclpr	⊢ ( ( 1P ∈ P ∧ 1P ∈ P ) → ( 1P +P 1P ) ∈ P )
77	14 14 76	mp2an	⊢ ( 1P +P 1P ) ∈ P
78	77 14	pm3.2i	⊢ ( ( 1P +P 1P ) ∈ P ∧ 1P ∈ P )
79		enreceq	⊢ ( ( ( ( ( 𝑦 ·P ( 𝑣 +P 1P ) ) +P ( 𝑧 ·P 1P ) ) ∈ P ∧ ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P ( 𝑣 +P 1P ) ) ) ∈ P ) ∧ ( ( 1P +P 1P ) ∈ P ∧ 1P ∈ P ) ) → ( [ ⟨ ( ( 𝑦 ·P ( 𝑣 +P 1P ) ) +P ( 𝑧 ·P 1P ) ) , ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P ( 𝑣 +P 1P ) ) ) ⟩ ] ~R = [ ⟨ ( 1P +P 1P ) , 1P ⟩ ] ~R ↔ ( ( ( 𝑦 ·P ( 𝑣 +P 1P ) ) +P ( 𝑧 ·P 1P ) ) +P 1P ) = ( ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P ( 𝑣 +P 1P ) ) ) +P ( 1P +P 1P ) ) ) )
80	75 78 79	sylancl	⊢ ( ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ∧ 𝑣 ∈ P ) → ( [ ⟨ ( ( 𝑦 ·P ( 𝑣 +P 1P ) ) +P ( 𝑧 ·P 1P ) ) , ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P ( 𝑣 +P 1P ) ) ) ⟩ ] ~R = [ ⟨ ( 1P +P 1P ) , 1P ⟩ ] ~R ↔ ( ( ( 𝑦 ·P ( 𝑣 +P 1P ) ) +P ( 𝑧 ·P 1P ) ) +P 1P ) = ( ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P ( 𝑣 +P 1P ) ) ) +P ( 1P +P 1P ) ) ) )
81	60 80	syl5ibr	⊢ ( ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ∧ 𝑣 ∈ P ) → ( ( ( 𝑤 ·P 𝑣 ) = 1P ∧ ( 𝑧 +P 𝑤 ) = 𝑦 ) → [ ⟨ ( ( 𝑦 ·P ( 𝑣 +P 1P ) ) +P ( 𝑧 ·P 1P ) ) , ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P ( 𝑣 +P 1P ) ) ) ⟩ ] ~R = [ ⟨ ( 1P +P 1P ) , 1P ⟩ ] ~R ) )
82	81	imp	⊢ ( ( ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ∧ 𝑣 ∈ P ) ∧ ( ( 𝑤 ·P 𝑣 ) = 1P ∧ ( 𝑧 +P 𝑤 ) = 𝑦 ) ) → [ ⟨ ( ( 𝑦 ·P ( 𝑣 +P 1P ) ) +P ( 𝑧 ·P 1P ) ) , ( ( 𝑦 ·P 1P ) +P ( 𝑧 ·P ( 𝑣 +P 1P ) ) ) ⟩ ] ~R = [ ⟨ ( 1P +P 1P ) , 1P ⟩ ] ~R )
83	25 82	eqtrd	⊢ ( ( ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ∧ 𝑣 ∈ P ) ∧ ( ( 𝑤 ·P 𝑣 ) = 1P ∧ ( 𝑧 +P 𝑤 ) = 𝑦 ) ) → ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ·R [ ⟨ ( 𝑣 +P 1P ) , 1P ⟩ ] ~R ) = [ ⟨ ( 1P +P 1P ) , 1P ⟩ ] ~R )
84		df-1r	⊢ 1R = [ ⟨ ( 1P +P 1P ) , 1P ⟩ ] ~R
85	83 84	syl6eqr	⊢ ( ( ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ∧ 𝑣 ∈ P ) ∧ ( ( 𝑤 ·P 𝑣 ) = 1P ∧ ( 𝑧 +P 𝑤 ) = 𝑦 ) ) → ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ·R [ ⟨ ( 𝑣 +P 1P ) , 1P ⟩ ] ~R ) = 1R )
86		oveq2	⊢ ( 𝑥 = [ ⟨ ( 𝑣 +P 1P ) , 1P ⟩ ] ~R → ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ·R 𝑥 ) = ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ·R [ ⟨ ( 𝑣 +P 1P ) , 1P ⟩ ] ~R ) )
87	86	eqeq1d	⊢ ( 𝑥 = [ ⟨ ( 𝑣 +P 1P ) , 1P ⟩ ] ~R → ( ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ·R 𝑥 ) = 1R ↔ ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ·R [ ⟨ ( 𝑣 +P 1P ) , 1P ⟩ ] ~R ) = 1R ) )
88	87	rspcev	⊢ ( ( [ ⟨ ( 𝑣 +P 1P ) , 1P ⟩ ] ~R ∈ R ∧ ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ·R [ ⟨ ( 𝑣 +P 1P ) , 1P ⟩ ] ~R ) = 1R ) → ∃ 𝑥 ∈ R ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ·R 𝑥 ) = 1R )
89	20 85 88	syl2anc	⊢ ( ( ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ∧ 𝑣 ∈ P ) ∧ ( ( 𝑤 ·P 𝑣 ) = 1P ∧ ( 𝑧 +P 𝑤 ) = 𝑦 ) ) → ∃ 𝑥 ∈ R ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ·R 𝑥 ) = 1R )
90	89	exp43	⊢ ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) → ( 𝑣 ∈ P → ( ( 𝑤 ·P 𝑣 ) = 1P → ( ( 𝑧 +P 𝑤 ) = 𝑦 → ∃ 𝑥 ∈ R ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ·R 𝑥 ) = 1R ) ) ) )
91	90	rexlimdv	⊢ ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) → ( ∃ 𝑣 ∈ P ( 𝑤 ·P 𝑣 ) = 1P → ( ( 𝑧 +P 𝑤 ) = 𝑦 → ∃ 𝑥 ∈ R ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ·R 𝑥 ) = 1R ) ) )
92	13 91	syl5	⊢ ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) → ( 𝑤 ∈ P → ( ( 𝑧 +P 𝑤 ) = 𝑦 → ∃ 𝑥 ∈ R ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ·R 𝑥 ) = 1R ) ) )
93	92	rexlimdv	⊢ ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) → ( ∃ 𝑤 ∈ P ( 𝑧 +P 𝑤 ) = 𝑦 → ∃ 𝑥 ∈ R ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ·R 𝑥 ) = 1R ) )
94	12 93	syl5	⊢ ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) → ( 0R <R [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R → ∃ 𝑥 ∈ R ( [ ⟨ 𝑦 , 𝑧 ⟩ ] ~R ·R 𝑥 ) = 1R ) )
95	4 9 94	ecoptocl	⊢ ( 𝐴 ∈ R → ( 0R <R 𝐴 → ∃ 𝑥 ∈ R ( 𝐴 ·R 𝑥 ) = 1R ) )
96	3 95	mpcom	⊢ ( 0R <R 𝐴 → ∃ 𝑥 ∈ R ( 𝐴 ·R 𝑥 ) = 1R )