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	$⊢ 0_{𝑹} <_{𝑹} A \to \exists x \in 𝑹 A \cdot_{𝑹} x = 1_{𝑹}$

Proof

Step	Hyp	Ref	Expression
1		ltrelsr	$⊢ <_{𝑹} \subseteq 𝑹 \times 𝑹$
2	1	brel	$⊢ 0_{𝑹} <_{𝑹} A \to (0_{𝑹} \in 𝑹 \land A \in 𝑹)$
3	2	simprd	$⊢ 0_{𝑹} <_{𝑹} A \to A \in 𝑹$
4		df-nr	$⊢ 𝑹 = (𝑷 \times 𝑷) / ~_{𝑹}$
5		breq2	$⊢ [⟨y, z⟩] ~_{𝑹} = A \to (0_{𝑹} <_{𝑹} [⟨y, z⟩] ~_{𝑹} \leftrightarrow 0_{𝑹} <_{𝑹} A)$
6		oveq1	$⊢ [⟨y, z⟩] ~_{𝑹} = A \to [⟨y, z⟩] ~_{𝑹} \cdot_{𝑹} x = A \cdot_{𝑹} x$
7	6	eqeq1d	$⊢ [⟨y, z⟩] ~_{𝑹} = A \to ([⟨y, z⟩] ~_{𝑹} \cdot_{𝑹} x = 1_{𝑹} \leftrightarrow A \cdot_{𝑹} x = 1_{𝑹})$
8	7	rexbidv	$⊢ [⟨y, z⟩] ~_{𝑹} = A \to (\exists x \in 𝑹 [⟨y, z⟩] ~_{𝑹} \cdot_{𝑹} x = 1_{𝑹} \leftrightarrow \exists x \in 𝑹 A \cdot_{𝑹} x = 1_{𝑹})$
9	5 8	imbi12d	$⊢ [⟨y, z⟩] ~_{𝑹} = A \to ((0_{𝑹} <_{𝑹} [⟨y, z⟩] ~_{𝑹} \to \exists x \in 𝑹 [⟨y, z⟩] ~_{𝑹} \cdot_{𝑹} x = 1_{𝑹}) \leftrightarrow (0_{𝑹} <_{𝑹} A \to \exists x \in 𝑹 A \cdot_{𝑹} x = 1_{𝑹}))$
10		gt0srpr	$⊢ 0_{𝑹} <_{𝑹} [⟨y, z⟩] ~_{𝑹} \leftrightarrow z <_{𝑷} y$
11		ltexpri	$⊢ z <_{𝑷} y \to \exists w \in 𝑷 z +_{𝑷} w = y$
12	10 11	sylbi	$⊢ 0_{𝑹} <_{𝑹} [⟨y, z⟩] ~_{𝑹} \to \exists w \in 𝑷 z +_{𝑷} w = y$
13		recexpr	$⊢ w \in 𝑷 \to \exists v \in 𝑷 w \cdot_{𝑷} v = 1_{𝑷}$
14		1pr	$⊢ 1_{𝑷} \in 𝑷$
15		addclpr	$⊢ (v \in 𝑷 \land 1_{𝑷} \in 𝑷) \to v +_{𝑷} 1_{𝑷} \in 𝑷$
16	14 15	mpan2	$⊢ v \in 𝑷 \to v +_{𝑷} 1_{𝑷} \in 𝑷$
17		enrex	$⊢ ~_{𝑹} \in V$
18	17 4	ecopqsi	$⊢ (v +_{𝑷} 1_{𝑷} \in 𝑷 \land 1_{𝑷} \in 𝑷) \to [⟨v +_{𝑷} 1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹} \in 𝑹$
19	16 14 18	sylancl	$⊢ v \in 𝑷 \to [⟨v +_{𝑷} 1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹} \in 𝑹$
20	19	ad2antlr	$⊢ (((y \in 𝑷 \land z \in 𝑷) \land v \in 𝑷) \land (w \cdot_{𝑷} v = 1_{𝑷} \land z +_{𝑷} w = y)) \to [⟨v +_{𝑷} 1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹} \in 𝑹$
21	16 14	jctir	$⊢ v \in 𝑷 \to (v +_{𝑷} 1_{𝑷} \in 𝑷 \land 1_{𝑷} \in 𝑷)$
22	21	anim2i	$⊢ ((y \in 𝑷 \land z \in 𝑷) \land v \in 𝑷) \to ((y \in 𝑷 \land z \in 𝑷) \land (v +_{𝑷} 1_{𝑷} \in 𝑷 \land 1_{𝑷} \in 𝑷))$
23	22	adantr	$⊢ (((y \in 𝑷 \land z \in 𝑷) \land v \in 𝑷) \land (w \cdot_{𝑷} v = 1_{𝑷} \land z +_{𝑷} w = y)) \to ((y \in 𝑷 \land z \in 𝑷) \land (v +_{𝑷} 1_{𝑷} \in 𝑷 \land 1_{𝑷} \in 𝑷))$
24		mulsrpr	$⊢ ((y \in 𝑷 \land z \in 𝑷) \land (v +_{𝑷} 1_{𝑷} \in 𝑷 \land 1_{𝑷} \in 𝑷)) \to [⟨y, z⟩] ~_{𝑹} \cdot_{𝑹} [⟨v +_{𝑷} 1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹} = [⟨(y \cdot_{𝑷} (v +_{𝑷} 1_{𝑷})) +_{𝑷} (z \cdot_{𝑷} 1_{𝑷}), (y \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (z \cdot_{𝑷} (v +_{𝑷} 1_{𝑷}))⟩] ~_{𝑹}$
25	23 24	syl	$⊢ (((y \in 𝑷 \land z \in 𝑷) \land v \in 𝑷) \land (w \cdot_{𝑷} v = 1_{𝑷} \land z +_{𝑷} w = y)) \to [⟨y, z⟩] ~_{𝑹} \cdot_{𝑹} [⟨v +_{𝑷} 1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹} = [⟨(y \cdot_{𝑷} (v +_{𝑷} 1_{𝑷})) +_{𝑷} (z \cdot_{𝑷} 1_{𝑷}), (y \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (z \cdot_{𝑷} (v +_{𝑷} 1_{𝑷}))⟩] ~_{𝑹}$
26		oveq1	$⊢ z +_{𝑷} w = y \to (z +_{𝑷} w) \cdot_{𝑷} v = y \cdot_{𝑷} v$
27	26	eqcomd	$⊢ z +_{𝑷} w = y \to y \cdot_{𝑷} v = (z +_{𝑷} w) \cdot_{𝑷} v$
28		vex	$⊢ z \in V$
29		vex	$⊢ w \in V$
30		vex	$⊢ v \in V$
31		mulcompr	$⊢ u \cdot_{𝑷} f = f \cdot_{𝑷} u$
32		distrpr	$⊢ u \cdot_{𝑷} (f +_{𝑷} x) = (u \cdot_{𝑷} f) +_{𝑷} (u \cdot_{𝑷} x)$
33	28 29 30 31 32	caovdir	$⊢ (z +_{𝑷} w) \cdot_{𝑷} v = (z \cdot_{𝑷} v) +_{𝑷} (w \cdot_{𝑷} v)$
34		oveq2	$⊢ w \cdot_{𝑷} v = 1_{𝑷} \to (z \cdot_{𝑷} v) +_{𝑷} (w \cdot_{𝑷} v) = (z \cdot_{𝑷} v) +_{𝑷} 1_{𝑷}$
35	33 34	eqtrid	$⊢ w \cdot_{𝑷} v = 1_{𝑷} \to (z +_{𝑷} w) \cdot_{𝑷} v = (z \cdot_{𝑷} v) +_{𝑷} 1_{𝑷}$
36	27 35	sylan9eqr	$⊢ (w \cdot_{𝑷} v = 1_{𝑷} \land z +_{𝑷} w = y) \to y \cdot_{𝑷} v = (z \cdot_{𝑷} v) +_{𝑷} 1_{𝑷}$
37	36	oveq1d	$⊢ (w \cdot_{𝑷} v = 1_{𝑷} \land z +_{𝑷} w = y) \to (y \cdot_{𝑷} v) +_{𝑷} ((y \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (z \cdot_{𝑷} 1_{𝑷})) = ((z \cdot_{𝑷} v) +_{𝑷} 1_{𝑷}) +_{𝑷} ((y \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (z \cdot_{𝑷} 1_{𝑷}))$
38		ovex	$⊢ z \cdot_{𝑷} v \in V$
39	14	elexi	$⊢ 1_{𝑷} \in V$
40		ovex	$⊢ (y \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (z \cdot_{𝑷} 1_{𝑷}) \in V$
41		addcompr	$⊢ u +_{𝑷} f = f +_{𝑷} u$
42		addasspr	$⊢ (u +_{𝑷} f) +_{𝑷} x = u +_{𝑷} (f +_{𝑷} x)$
43	38 39 40 41 42	caov32	$⊢ ((z \cdot_{𝑷} v) +_{𝑷} 1_{𝑷}) +_{𝑷} ((y \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (z \cdot_{𝑷} 1_{𝑷})) = ((z \cdot_{𝑷} v) +_{𝑷} ((y \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (z \cdot_{𝑷} 1_{𝑷}))) +_{𝑷} 1_{𝑷}$
44	37 43	eqtrdi	$⊢ (w \cdot_{𝑷} v = 1_{𝑷} \land z +_{𝑷} w = y) \to (y \cdot_{𝑷} v) +_{𝑷} ((y \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (z \cdot_{𝑷} 1_{𝑷})) = ((z \cdot_{𝑷} v) +_{𝑷} ((y \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (z \cdot_{𝑷} 1_{𝑷}))) +_{𝑷} 1_{𝑷}$
45	44	oveq1d	$⊢ (w \cdot_{𝑷} v = 1_{𝑷} \land z +_{𝑷} w = y) \to ((y \cdot_{𝑷} v) +_{𝑷} ((y \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (z \cdot_{𝑷} 1_{𝑷}))) +_{𝑷} 1_{𝑷} = (((z \cdot_{𝑷} v) +_{𝑷} ((y \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (z \cdot_{𝑷} 1_{𝑷}))) +_{𝑷} 1_{𝑷}) +_{𝑷} 1_{𝑷}$
46		addasspr	$⊢ (((z \cdot_{𝑷} v) +_{𝑷} ((y \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (z \cdot_{𝑷} 1_{𝑷}))) +_{𝑷} 1_{𝑷}) +_{𝑷} 1_{𝑷} = ((z \cdot_{𝑷} v) +_{𝑷} ((y \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (z \cdot_{𝑷} 1_{𝑷}))) +_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})$
47	45 46	eqtrdi	$⊢ (w \cdot_{𝑷} v = 1_{𝑷} \land z +_{𝑷} w = y) \to ((y \cdot_{𝑷} v) +_{𝑷} ((y \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (z \cdot_{𝑷} 1_{𝑷}))) +_{𝑷} 1_{𝑷} = ((z \cdot_{𝑷} v) +_{𝑷} ((y \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (z \cdot_{𝑷} 1_{𝑷}))) +_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})$
48		distrpr	$⊢ y \cdot_{𝑷} (v +_{𝑷} 1_{𝑷}) = (y \cdot_{𝑷} v) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷})$
49	48	oveq1i	$⊢ (y \cdot_{𝑷} (v +_{𝑷} 1_{𝑷})) +_{𝑷} (z \cdot_{𝑷} 1_{𝑷}) = ((y \cdot_{𝑷} v) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷})) +_{𝑷} (z \cdot_{𝑷} 1_{𝑷})$
50		addasspr	$⊢ ((y \cdot_{𝑷} v) +_{𝑷} (y \cdot_{𝑷} 1_{𝑷})) +_{𝑷} (z \cdot_{𝑷} 1_{𝑷}) = (y \cdot_{𝑷} v) +_{𝑷} ((y \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (z \cdot_{𝑷} 1_{𝑷}))$
51	49 50	eqtri	$⊢ (y \cdot_{𝑷} (v +_{𝑷} 1_{𝑷})) +_{𝑷} (z \cdot_{𝑷} 1_{𝑷}) = (y \cdot_{𝑷} v) +_{𝑷} ((y \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (z \cdot_{𝑷} 1_{𝑷}))$
52	51	oveq1i	$⊢ ((y \cdot_{𝑷} (v +_{𝑷} 1_{𝑷})) +_{𝑷} (z \cdot_{𝑷} 1_{𝑷})) +_{𝑷} 1_{𝑷} = ((y \cdot_{𝑷} v) +_{𝑷} ((y \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (z \cdot_{𝑷} 1_{𝑷}))) +_{𝑷} 1_{𝑷}$
53		distrpr	$⊢ z \cdot_{𝑷} (v +_{𝑷} 1_{𝑷}) = (z \cdot_{𝑷} v) +_{𝑷} (z \cdot_{𝑷} 1_{𝑷})$
54	53	oveq2i	$⊢ (y \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (z \cdot_{𝑷} (v +_{𝑷} 1_{𝑷})) = (y \cdot_{𝑷} 1_{𝑷}) +_{𝑷} ((z \cdot_{𝑷} v) +_{𝑷} (z \cdot_{𝑷} 1_{𝑷}))$
55		ovex	$⊢ y \cdot_{𝑷} 1_{𝑷} \in V$
56		ovex	$⊢ z \cdot_{𝑷} 1_{𝑷} \in V$
57	55 38 56 41 42	caov12	$⊢ (y \cdot_{𝑷} 1_{𝑷}) +_{𝑷} ((z \cdot_{𝑷} v) +_{𝑷} (z \cdot_{𝑷} 1_{𝑷})) = (z \cdot_{𝑷} v) +_{𝑷} ((y \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (z \cdot_{𝑷} 1_{𝑷}))$
58	54 57	eqtri	$⊢ (y \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (z \cdot_{𝑷} (v +_{𝑷} 1_{𝑷})) = (z \cdot_{𝑷} v) +_{𝑷} ((y \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (z \cdot_{𝑷} 1_{𝑷}))$
59	58	oveq1i	$⊢ ((y \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (z \cdot_{𝑷} (v +_{𝑷} 1_{𝑷}))) +_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}) = ((z \cdot_{𝑷} v) +_{𝑷} ((y \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (z \cdot_{𝑷} 1_{𝑷}))) +_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})$
60	47 52 59	3eqtr4g	$⊢ (w \cdot_{𝑷} v = 1_{𝑷} \land z +_{𝑷} w = y) \to ((y \cdot_{𝑷} (v +_{𝑷} 1_{𝑷})) +_{𝑷} (z \cdot_{𝑷} 1_{𝑷})) +_{𝑷} 1_{𝑷} = ((y \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (z \cdot_{𝑷} (v +_{𝑷} 1_{𝑷}))) +_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷})$
61		mulclpr	$⊢ (y \in 𝑷 \land v +_{𝑷} 1_{𝑷} \in 𝑷) \to y \cdot_{𝑷} (v +_{𝑷} 1_{𝑷}) \in 𝑷$
62	16 61	sylan2	$⊢ (y \in 𝑷 \land v \in 𝑷) \to y \cdot_{𝑷} (v +_{𝑷} 1_{𝑷}) \in 𝑷$
63		mulclpr	$⊢ (z \in 𝑷 \land 1_{𝑷} \in 𝑷) \to z \cdot_{𝑷} 1_{𝑷} \in 𝑷$
64	14 63	mpan2	$⊢ z \in 𝑷 \to z \cdot_{𝑷} 1_{𝑷} \in 𝑷$
65		addclpr	$⊢ (y \cdot_{𝑷} (v +_{𝑷} 1_{𝑷}) \in 𝑷 \land z \cdot_{𝑷} 1_{𝑷} \in 𝑷) \to (y \cdot_{𝑷} (v +_{𝑷} 1_{𝑷})) +_{𝑷} (z \cdot_{𝑷} 1_{𝑷}) \in 𝑷$
66	62 64 65	syl2an	$⊢ ((y \in 𝑷 \land v \in 𝑷) \land z \in 𝑷) \to (y \cdot_{𝑷} (v +_{𝑷} 1_{𝑷})) +_{𝑷} (z \cdot_{𝑷} 1_{𝑷}) \in 𝑷$
67	66	an32s	$⊢ ((y \in 𝑷 \land z \in 𝑷) \land v \in 𝑷) \to (y \cdot_{𝑷} (v +_{𝑷} 1_{𝑷})) +_{𝑷} (z \cdot_{𝑷} 1_{𝑷}) \in 𝑷$
68		mulclpr	$⊢ (y \in 𝑷 \land 1_{𝑷} \in 𝑷) \to y \cdot_{𝑷} 1_{𝑷} \in 𝑷$
69	14 68	mpan2	$⊢ y \in 𝑷 \to y \cdot_{𝑷} 1_{𝑷} \in 𝑷$
70		mulclpr	$⊢ (z \in 𝑷 \land v +_{𝑷} 1_{𝑷} \in 𝑷) \to z \cdot_{𝑷} (v +_{𝑷} 1_{𝑷}) \in 𝑷$
71	16 70	sylan2	$⊢ (z \in 𝑷 \land v \in 𝑷) \to z \cdot_{𝑷} (v +_{𝑷} 1_{𝑷}) \in 𝑷$
72		addclpr	$⊢ (y \cdot_{𝑷} 1_{𝑷} \in 𝑷 \land z \cdot_{𝑷} (v +_{𝑷} 1_{𝑷}) \in 𝑷) \to (y \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (z \cdot_{𝑷} (v +_{𝑷} 1_{𝑷})) \in 𝑷$
73	69 71 72	syl2an	$⊢ (y \in 𝑷 \land (z \in 𝑷 \land v \in 𝑷)) \to (y \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (z \cdot_{𝑷} (v +_{𝑷} 1_{𝑷})) \in 𝑷$
74	73	anassrs	$⊢ ((y \in 𝑷 \land z \in 𝑷) \land v \in 𝑷) \to (y \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (z \cdot_{𝑷} (v +_{𝑷} 1_{𝑷})) \in 𝑷$
75	67 74	jca	$⊢ ((y \in 𝑷 \land z \in 𝑷) \land v \in 𝑷) \to ((y \cdot_{𝑷} (v +_{𝑷} 1_{𝑷})) +_{𝑷} (z \cdot_{𝑷} 1_{𝑷}) \in 𝑷 \land (y \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (z \cdot_{𝑷} (v +_{𝑷} 1_{𝑷})) \in 𝑷)$
76		addclpr	$⊢ (1_{𝑷} \in 𝑷 \land 1_{𝑷} \in 𝑷) \to 1_{𝑷} +_{𝑷} 1_{𝑷} \in 𝑷$
77	14 14 76	mp2an	$⊢ 1_{𝑷} +_{𝑷} 1_{𝑷} \in 𝑷$
78	77 14	pm3.2i	$⊢ (1_{𝑷} +_{𝑷} 1_{𝑷} \in 𝑷 \land 1_{𝑷} \in 𝑷)$
79		enreceq	$⊢ (((y \cdot_{𝑷} (v +_{𝑷} 1_{𝑷})) +_{𝑷} (z \cdot_{𝑷} 1_{𝑷}) \in 𝑷 \land (y \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (z \cdot_{𝑷} (v +_{𝑷} 1_{𝑷})) \in 𝑷) \land (1_{𝑷} +_{𝑷} 1_{𝑷} \in 𝑷 \land 1_{𝑷} \in 𝑷)) \to ([⟨(y \cdot_{𝑷} (v +_{𝑷} 1_{𝑷})) +_{𝑷} (z \cdot_{𝑷} 1_{𝑷}), (y \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (z \cdot_{𝑷} (v +_{𝑷} 1_{𝑷}))⟩] ~_{𝑹} = [⟨1_{𝑷} +_{𝑷} 1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹} \leftrightarrow ((y \cdot_{𝑷} (v +_{𝑷} 1_{𝑷})) +_{𝑷} (z \cdot_{𝑷} 1_{𝑷})) +_{𝑷} 1_{𝑷} = ((y \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (z \cdot_{𝑷} (v +_{𝑷} 1_{𝑷}))) +_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}))$
80	75 78 79	sylancl	$⊢ ((y \in 𝑷 \land z \in 𝑷) \land v \in 𝑷) \to ([⟨(y \cdot_{𝑷} (v +_{𝑷} 1_{𝑷})) +_{𝑷} (z \cdot_{𝑷} 1_{𝑷}), (y \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (z \cdot_{𝑷} (v +_{𝑷} 1_{𝑷}))⟩] ~_{𝑹} = [⟨1_{𝑷} +_{𝑷} 1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹} \leftrightarrow ((y \cdot_{𝑷} (v +_{𝑷} 1_{𝑷})) +_{𝑷} (z \cdot_{𝑷} 1_{𝑷})) +_{𝑷} 1_{𝑷} = ((y \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (z \cdot_{𝑷} (v +_{𝑷} 1_{𝑷}))) +_{𝑷} (1_{𝑷} +_{𝑷} 1_{𝑷}))$
81	60 80	imbitrrid	$⊢ ((y \in 𝑷 \land z \in 𝑷) \land v \in 𝑷) \to ((w \cdot_{𝑷} v = 1_{𝑷} \land z +_{𝑷} w = y) \to [⟨(y \cdot_{𝑷} (v +_{𝑷} 1_{𝑷})) +_{𝑷} (z \cdot_{𝑷} 1_{𝑷}), (y \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (z \cdot_{𝑷} (v +_{𝑷} 1_{𝑷}))⟩] ~_{𝑹} = [⟨1_{𝑷} +_{𝑷} 1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹})$
82	81	imp	$⊢ (((y \in 𝑷 \land z \in 𝑷) \land v \in 𝑷) \land (w \cdot_{𝑷} v = 1_{𝑷} \land z +_{𝑷} w = y)) \to [⟨(y \cdot_{𝑷} (v +_{𝑷} 1_{𝑷})) +_{𝑷} (z \cdot_{𝑷} 1_{𝑷}), (y \cdot_{𝑷} 1_{𝑷}) +_{𝑷} (z \cdot_{𝑷} (v +_{𝑷} 1_{𝑷}))⟩] ~_{𝑹} = [⟨1_{𝑷} +_{𝑷} 1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹}$
83	25 82	eqtrd	$⊢ (((y \in 𝑷 \land z \in 𝑷) \land v \in 𝑷) \land (w \cdot_{𝑷} v = 1_{𝑷} \land z +_{𝑷} w = y)) \to [⟨y, z⟩] ~_{𝑹} \cdot_{𝑹} [⟨v +_{𝑷} 1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹} = [⟨1_{𝑷} +_{𝑷} 1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹}$
84		df-1r	$⊢ 1_{𝑹} = [⟨1_{𝑷} +_{𝑷} 1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹}$
85	83 84	eqtr4di	$⊢ (((y \in 𝑷 \land z \in 𝑷) \land v \in 𝑷) \land (w \cdot_{𝑷} v = 1_{𝑷} \land z +_{𝑷} w = y)) \to [⟨y, z⟩] ~_{𝑹} \cdot_{𝑹} [⟨v +_{𝑷} 1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹} = 1_{𝑹}$
86		oveq2	$⊢ x = [⟨v +_{𝑷} 1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹} \to [⟨y, z⟩] ~_{𝑹} \cdot_{𝑹} x = [⟨y, z⟩] ~_{𝑹} \cdot_{𝑹} [⟨v +_{𝑷} 1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹}$
87	86	eqeq1d	$⊢ x = [⟨v +_{𝑷} 1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹} \to ([⟨y, z⟩] ~_{𝑹} \cdot_{𝑹} x = 1_{𝑹} \leftrightarrow [⟨y, z⟩] ~_{𝑹} \cdot_{𝑹} [⟨v +_{𝑷} 1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹} = 1_{𝑹})$
88	87	rspcev	$⊢ ([⟨v +_{𝑷} 1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹} \in 𝑹 \land [⟨y, z⟩] ~_{𝑹} \cdot_{𝑹} [⟨v +_{𝑷} 1_{𝑷}, 1_{𝑷}⟩] ~_{𝑹} = 1_{𝑹}) \to \exists x \in 𝑹 [⟨y, z⟩] ~_{𝑹} \cdot_{𝑹} x = 1_{𝑹}$
89	20 85 88	syl2anc	$⊢ (((y \in 𝑷 \land z \in 𝑷) \land v \in 𝑷) \land (w \cdot_{𝑷} v = 1_{𝑷} \land z +_{𝑷} w = y)) \to \exists x \in 𝑹 [⟨y, z⟩] ~_{𝑹} \cdot_{𝑹} x = 1_{𝑹}$
90	89	exp43	$⊢ (y \in 𝑷 \land z \in 𝑷) \to (v \in 𝑷 \to (w \cdot_{𝑷} v = 1_{𝑷} \to (z +_{𝑷} w = y \to \exists x \in 𝑹 [⟨y, z⟩] ~_{𝑹} \cdot_{𝑹} x = 1_{𝑹})))$
91	90	rexlimdv	$⊢ (y \in 𝑷 \land z \in 𝑷) \to (\exists v \in 𝑷 w \cdot_{𝑷} v = 1_{𝑷} \to (z +_{𝑷} w = y \to \exists x \in 𝑹 [⟨y, z⟩] ~_{𝑹} \cdot_{𝑹} x = 1_{𝑹}))$
92	13 91	syl5	$⊢ (y \in 𝑷 \land z \in 𝑷) \to (w \in 𝑷 \to (z +_{𝑷} w = y \to \exists x \in 𝑹 [⟨y, z⟩] ~_{𝑹} \cdot_{𝑹} x = 1_{𝑹}))$
93	92	rexlimdv	$⊢ (y \in 𝑷 \land z \in 𝑷) \to (\exists w \in 𝑷 z +_{𝑷} w = y \to \exists x \in 𝑹 [⟨y, z⟩] ~_{𝑹} \cdot_{𝑹} x = 1_{𝑹})$
94	12 93	syl5	$⊢ (y \in 𝑷 \land z \in 𝑷) \to (0_{𝑹} <_{𝑹} [⟨y, z⟩] ~_{𝑹} \to \exists x \in 𝑹 [⟨y, z⟩] ~_{𝑹} \cdot_{𝑹} x = 1_{𝑹})$
95	4 9 94	ecoptocl	$⊢ A \in 𝑹 \to (0_{𝑹} <_{𝑹} A \to \exists x \in 𝑹 A \cdot_{𝑹} x = 1_{𝑹})$
96	3 95	mpcom	$⊢ 0_{𝑹} <_{𝑹} A \to \exists x \in 𝑹 A \cdot_{𝑹} x = 1_{𝑹}$

Metamath Proof Explorer

Theorem recexsrlem

Proof