Theorem recexgt0sr 7888

Description: The reciprocal of a positive signed real exists and is positive. (Contributed by Jim Kingdon, 6-Feb-2020.)

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem recexgt0sr

Dummy variables 𝑦 𝑧 𝑤 𝑣 𝑓 𝑔 ℎ are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ltrelsr 7853	. . . 4 ⊢ <R ⊆ (R × R)
2	1	brel 4728	. . 3 ⊢ (0R <R 𝐴 → (0R ∈ R ∧ 𝐴 ∈ R))
3	2	simprd 114	. 2 ⊢ (0R <R 𝐴 → 𝐴 ∈ R)
4		df-nr 7842	. . 3 ⊢ R = ((P × P) / ~R )
5		breq2 4049	. . . 4 ⊢ ([⟨𝑦, 𝑧⟩] ~R = 𝐴 → (0R <R [⟨𝑦, 𝑧⟩] ~R ↔ 0R <R 𝐴))
6		oveq1 5953	. . . . . . 7 ⊢ ([⟨𝑦, 𝑧⟩] ~R = 𝐴 → ([⟨𝑦, 𝑧⟩] ~R ·R 𝑥) = (𝐴 ·R 𝑥))
7	6	eqeq1d 2214	. . . . . 6 ⊢ ([⟨𝑦, 𝑧⟩] ~R = 𝐴 → (([⟨𝑦, 𝑧⟩] ~R ·R 𝑥) = 1R ↔ (𝐴 ·R 𝑥) = 1R))
8	7	anbi2d 464	. . . . 5 ⊢ ([⟨𝑦, 𝑧⟩] ~R = 𝐴 → ((0R <R 𝑥 ∧ ([⟨𝑦, 𝑧⟩] ~R ·R 𝑥) = 1R) ↔ (0R <R 𝑥 ∧ (𝐴 ·R 𝑥) = 1R)))
9	8	rexbidv 2507	. . . 4 ⊢ ([⟨𝑦, 𝑧⟩] ~R = 𝐴 → (∃𝑥 ∈ R (0R <R 𝑥 ∧ ([⟨𝑦, 𝑧⟩] ~R ·R 𝑥) = 1R) ↔ ∃𝑥 ∈ R (0R <R 𝑥 ∧ (𝐴 ·R 𝑥) = 1R)))
10	5, 9	imbi12d 234	. . 3 ⊢ ([⟨𝑦, 𝑧⟩] ~R = 𝐴 → ((0R <R [⟨𝑦, 𝑧⟩] ~R → ∃𝑥 ∈ R (0R <R 𝑥 ∧ ([⟨𝑦, 𝑧⟩] ~R ·R 𝑥) = 1R)) ↔ (0R <R 𝐴 → ∃𝑥 ∈ R (0R <R 𝑥 ∧ (𝐴 ·R 𝑥) = 1R))))
11		gt0srpr 7863	. . . . 5 ⊢ (0R <R [⟨𝑦, 𝑧⟩] ~R ↔ 𝑧<P 𝑦)
12		ltexpri 7728	. . . . 5 ⊢ (𝑧<P 𝑦 → ∃𝑤 ∈ P (𝑧 +P 𝑤) = 𝑦)
13	11, 12	sylbi 121	. . . 4 ⊢ (0R <R [⟨𝑦, 𝑧⟩] ~R → ∃𝑤 ∈ P (𝑧 +P 𝑤) = 𝑦)
14		recexpr 7753	. . . . . . 7 ⊢ (𝑤 ∈ P → ∃𝑣 ∈ P (𝑤 ·P 𝑣) = 1P)
15	14	adantl 277	. . . . . 6 ⊢ (((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ 𝑤 ∈ P) → ∃𝑣 ∈ P (𝑤 ·P 𝑣) = 1P)
16		1pr 7669	. . . . . . . . . . . . . 14 ⊢ 1P ∈ P
17		addclpr 7652	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ∈ P ∧ 1P ∈ P) → (𝑣 +P 1P) ∈ P)
18	16, 17	mpan2 425	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ P → (𝑣 +P 1P) ∈ P)
19		enrex 7852	. . . . . . . . . . . . . 14 ⊢ ~R ∈ V
20	19, 4	ecopqsi 6679	. . . . . . . . . . . . 13 ⊢ (((𝑣 +P 1P) ∈ P ∧ 1P ∈ P) → [⟨(𝑣 +P 1P), 1P⟩] ~R ∈ R)
21	18, 16, 20	sylancl 413	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ P → [⟨(𝑣 +P 1P), 1P⟩] ~R ∈ R)
22	21	adantl 277	. . . . . . . . . . 11 ⊢ ((𝑤 ∈ P ∧ 𝑣 ∈ P) → [⟨(𝑣 +P 1P), 1P⟩] ~R ∈ R)
23	22	ad2antlr 489	. . . . . . . . . 10 ⊢ ((((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) ∧ ((𝑤 ·P 𝑣) = 1P ∧ (𝑧 +P 𝑤) = 𝑦)) → [⟨(𝑣 +P 1P), 1P⟩] ~R ∈ R)
24		simprr 531	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) → 𝑣 ∈ P)
25	24	adantr 276	. . . . . . . . . . 11 ⊢ ((((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) ∧ ((𝑤 ·P 𝑣) = 1P ∧ (𝑧 +P 𝑤) = 𝑦)) → 𝑣 ∈ P)
26		ltaddpr 7712	. . . . . . . . . . . . . 14 ⊢ ((1P ∈ P ∧ 𝑣 ∈ P) → 1P<P (1P +P 𝑣))
27	16, 26	mpan 424	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ P → 1P<P (1P +P 𝑣))
28		addcomprg 7693	. . . . . . . . . . . . . 14 ⊢ ((1P ∈ P ∧ 𝑣 ∈ P) → (1P +P 𝑣) = (𝑣 +P 1P))
29	16, 28	mpan 424	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ P → (1P +P 𝑣) = (𝑣 +P 1P))
30	27, 29	breqtrd 4071	. . . . . . . . . . . 12 ⊢ (𝑣 ∈ P → 1P<P (𝑣 +P 1P))
31		gt0srpr 7863	. . . . . . . . . . . 12 ⊢ (0R <R [⟨(𝑣 +P 1P), 1P⟩] ~R ↔ 1P<P (𝑣 +P 1P))
32	30, 31	sylibr 134	. . . . . . . . . . 11 ⊢ (𝑣 ∈ P → 0R <R [⟨(𝑣 +P 1P), 1P⟩] ~R )
33	25, 32	syl 14	. . . . . . . . . 10 ⊢ ((((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) ∧ ((𝑤 ·P 𝑣) = 1P ∧ (𝑧 +P 𝑤) = 𝑦)) → 0R <R [⟨(𝑣 +P 1P), 1P⟩] ~R )
34	18, 16	jctir 313	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ P → ((𝑣 +P 1P) ∈ P ∧ 1P ∈ P))
35	34	anim2i 342	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ 𝑣 ∈ P) → ((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ ((𝑣 +P 1P) ∈ P ∧ 1P ∈ P)))
36	35	adantr 276	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ 𝑣 ∈ P) ∧ ((𝑤 ·P 𝑣) = 1P ∧ (𝑧 +P 𝑤) = 𝑦)) → ((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ ((𝑣 +P 1P) ∈ P ∧ 1P ∈ P)))
37		mulsrpr 7861	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ 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 )
38	36, 37	syl 14	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ 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 )
39	38	adantlrl 482	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ P ∧ 𝑧 ∈ 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 )
40		oveq1 5953	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑧 +P 𝑤) = 𝑦 → ((𝑧 +P 𝑤) ·P 𝑣) = (𝑦 ·P 𝑣))
41	40	eqcomd 2211	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 +P 𝑤) = 𝑦 → (𝑦 ·P 𝑣) = ((𝑧 +P 𝑤) ·P 𝑣))
42	41	ad2antll 491	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) ∧ ((𝑤 ·P 𝑣) = 1P ∧ (𝑧 +P 𝑤) = 𝑦)) → (𝑦 ·P 𝑣) = ((𝑧 +P 𝑤) ·P 𝑣))
43		mulcomprg 7695	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑓 ∈ P ∧ ℎ ∈ P) → (𝑓 ·P ℎ) = (ℎ ·P 𝑓))
44	43	3adant2 1019	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑓 ∈ P ∧ 𝑔 ∈ P ∧ ℎ ∈ P) → (𝑓 ·P ℎ) = (ℎ ·P 𝑓))
45		mulcomprg 7695	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑔 ∈ P ∧ ℎ ∈ P) → (𝑔 ·P ℎ) = (ℎ ·P 𝑔))
46	45	3adant1 1018	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑓 ∈ P ∧ 𝑔 ∈ P ∧ ℎ ∈ P) → (𝑔 ·P ℎ) = (ℎ ·P 𝑔))
47	44, 46	oveq12d 5964	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑓 ∈ P ∧ 𝑔 ∈ P ∧ ℎ ∈ P) → ((𝑓 ·P ℎ) +P (𝑔 ·P ℎ)) = ((ℎ ·P 𝑓) +P (ℎ ·P 𝑔)))
48		distrprg 7703	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((ℎ ∈ P ∧ 𝑓 ∈ P ∧ 𝑔 ∈ P) → (ℎ ·P (𝑓 +P 𝑔)) = ((ℎ ·P 𝑓) +P (ℎ ·P 𝑔)))
49	48	3coml 1213	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑓 ∈ P ∧ 𝑔 ∈ P ∧ ℎ ∈ P) → (ℎ ·P (𝑓 +P 𝑔)) = ((ℎ ·P 𝑓) +P (ℎ ·P 𝑔)))
50		simp3 1002	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑓 ∈ P ∧ 𝑔 ∈ P ∧ ℎ ∈ P) → ℎ ∈ P)
51		addclpr 7652	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑓 ∈ P ∧ 𝑔 ∈ P) → (𝑓 +P 𝑔) ∈ P)
52	51	3adant3 1020	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑓 ∈ P ∧ 𝑔 ∈ P ∧ ℎ ∈ P) → (𝑓 +P 𝑔) ∈ P)
53		mulcomprg 7695	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((ℎ ∈ P ∧ (𝑓 +P 𝑔) ∈ P) → (ℎ ·P (𝑓 +P 𝑔)) = ((𝑓 +P 𝑔) ·P ℎ))
54	50, 52, 53	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑓 ∈ P ∧ 𝑔 ∈ P ∧ ℎ ∈ P) → (ℎ ·P (𝑓 +P 𝑔)) = ((𝑓 +P 𝑔) ·P ℎ))
55	47, 49, 54	3eqtr2rd 2245	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑓 ∈ P ∧ 𝑔 ∈ P ∧ ℎ ∈ P) → ((𝑓 +P 𝑔) ·P ℎ) = ((𝑓 ·P ℎ) +P (𝑔 ·P ℎ)))
56	55	adantl 277	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) ∧ (𝑓 ∈ P ∧ 𝑔 ∈ P ∧ ℎ ∈ P)) → ((𝑓 +P 𝑔) ·P ℎ) = ((𝑓 ·P ℎ) +P (𝑔 ·P ℎ)))
57		simplr 528	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) → 𝑧 ∈ P)
58		simprl 529	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) → 𝑤 ∈ P)
59	56, 57, 58, 24	caovdird 6127	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) → ((𝑧 +P 𝑤) ·P 𝑣) = ((𝑧 ·P 𝑣) +P (𝑤 ·P 𝑣)))
60		oveq2 5954	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑤 ·P 𝑣) = 1P → ((𝑧 ·P 𝑣) +P (𝑤 ·P 𝑣)) = ((𝑧 ·P 𝑣) +P 1P))
61	59, 60	sylan9eq 2258	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) ∧ (𝑤 ·P 𝑣) = 1P) → ((𝑧 +P 𝑤) ·P 𝑣) = ((𝑧 ·P 𝑣) +P 1P))
62	61	adantrr 479	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) ∧ ((𝑤 ·P 𝑣) = 1P ∧ (𝑧 +P 𝑤) = 𝑦)) → ((𝑧 +P 𝑤) ·P 𝑣) = ((𝑧 ·P 𝑣) +P 1P))
63	42, 62	eqtrd 2238	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) ∧ ((𝑤 ·P 𝑣) = 1P ∧ (𝑧 +P 𝑤) = 𝑦)) → (𝑦 ·P 𝑣) = ((𝑧 ·P 𝑣) +P 1P))
64	63	oveq1d 5961	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) ∧ ((𝑤 ·P 𝑣) = 1P ∧ (𝑧 +P 𝑤) = 𝑦)) → ((𝑦 ·P 𝑣) +P ((𝑦 ·P 1P) +P (𝑧 ·P 1P))) = (((𝑧 ·P 𝑣) +P 1P) +P ((𝑦 ·P 1P) +P (𝑧 ·P 1P))))
65		mulclpr 7687	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ P ∧ 𝑣 ∈ P) → (𝑧 ·P 𝑣) ∈ P)
66	57, 24, 65	syl2anc 411	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) → (𝑧 ·P 𝑣) ∈ P)
67	16	a1i 9	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) → 1P ∈ P)
68		simpll 527	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) → 𝑦 ∈ P)
69		mulclpr 7687	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ∈ P ∧ 1P ∈ P) → (𝑦 ·P 1P) ∈ P)
70	68, 16, 69	sylancl 413	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) → (𝑦 ·P 1P) ∈ P)
71		mulclpr 7687	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑧 ∈ P ∧ 1P ∈ P) → (𝑧 ·P 1P) ∈ P)
72	57, 16, 71	sylancl 413	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) → (𝑧 ·P 1P) ∈ P)
73		addclpr 7652	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑦 ·P 1P) ∈ P ∧ (𝑧 ·P 1P) ∈ P) → ((𝑦 ·P 1P) +P (𝑧 ·P 1P)) ∈ P)
74	70, 72, 73	syl2anc 411	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) → ((𝑦 ·P 1P) +P (𝑧 ·P 1P)) ∈ P)
75		addcomprg 7693	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓 ∈ P ∧ 𝑔 ∈ P) → (𝑓 +P 𝑔) = (𝑔 +P 𝑓))
76	75	adantl 277	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) ∧ (𝑓 ∈ P ∧ 𝑔 ∈ P)) → (𝑓 +P 𝑔) = (𝑔 +P 𝑓))
77		addassprg 7694	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓 ∈ P ∧ 𝑔 ∈ P ∧ ℎ ∈ P) → ((𝑓 +P 𝑔) +P ℎ) = (𝑓 +P (𝑔 +P ℎ)))
78	77	adantl 277	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) ∧ (𝑓 ∈ P ∧ 𝑔 ∈ P ∧ ℎ ∈ P)) → ((𝑓 +P 𝑔) +P ℎ) = (𝑓 +P (𝑔 +P ℎ)))
79	66, 67, 74, 76, 78	caov32d 6129	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) → (((𝑧 ·P 𝑣) +P 1P) +P ((𝑦 ·P 1P) +P (𝑧 ·P 1P))) = (((𝑧 ·P 𝑣) +P ((𝑦 ·P 1P) +P (𝑧 ·P 1P))) +P 1P))
80	79	adantr 276	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) ∧ ((𝑤 ·P 𝑣) = 1P ∧ (𝑧 +P 𝑤) = 𝑦)) → (((𝑧 ·P 𝑣) +P 1P) +P ((𝑦 ·P 1P) +P (𝑧 ·P 1P))) = (((𝑧 ·P 𝑣) +P ((𝑦 ·P 1P) +P (𝑧 ·P 1P))) +P 1P))
81	64, 80	eqtrd 2238	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) ∧ ((𝑤 ·P 𝑣) = 1P ∧ (𝑧 +P 𝑤) = 𝑦)) → ((𝑦 ·P 𝑣) +P ((𝑦 ·P 1P) +P (𝑧 ·P 1P))) = (((𝑧 ·P 𝑣) +P ((𝑦 ·P 1P) +P (𝑧 ·P 1P))) +P 1P))
82	81	oveq1d 5961	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) ∧ ((𝑤 ·P 𝑣) = 1P ∧ (𝑧 +P 𝑤) = 𝑦)) → (((𝑦 ·P 𝑣) +P ((𝑦 ·P 1P) +P (𝑧 ·P 1P))) +P 1P) = ((((𝑧 ·P 𝑣) +P ((𝑦 ·P 1P) +P (𝑧 ·P 1P))) +P 1P) +P 1P))
83		addclpr 7652	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑧 ·P 𝑣) ∈ P ∧ ((𝑦 ·P 1P) +P (𝑧 ·P 1P)) ∈ P) → ((𝑧 ·P 𝑣) +P ((𝑦 ·P 1P) +P (𝑧 ·P 1P))) ∈ P)
84	66, 74, 83	syl2anc 411	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) → ((𝑧 ·P 𝑣) +P ((𝑦 ·P 1P) +P (𝑧 ·P 1P))) ∈ P)
85	84	adantr 276	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) ∧ ((𝑤 ·P 𝑣) = 1P ∧ (𝑧 +P 𝑤) = 𝑦)) → ((𝑧 ·P 𝑣) +P ((𝑦 ·P 1P) +P (𝑧 ·P 1P))) ∈ P)
86	16	a1i 9	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) ∧ ((𝑤 ·P 𝑣) = 1P ∧ (𝑧 +P 𝑤) = 𝑦)) → 1P ∈ P)
87		addassprg 7694	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑧 ·P 𝑣) +P ((𝑦 ·P 1P) +P (𝑧 ·P 1P))) ∈ P ∧ 1P ∈ P ∧ 1P ∈ P) → ((((𝑧 ·P 𝑣) +P ((𝑦 ·P 1P) +P (𝑧 ·P 1P))) +P 1P) +P 1P) = (((𝑧 ·P 𝑣) +P ((𝑦 ·P 1P) +P (𝑧 ·P 1P))) +P (1P +P 1P)))
88	85, 86, 86, 87	syl3anc 1250	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) ∧ ((𝑤 ·P 𝑣) = 1P ∧ (𝑧 +P 𝑤) = 𝑦)) → ((((𝑧 ·P 𝑣) +P ((𝑦 ·P 1P) +P (𝑧 ·P 1P))) +P 1P) +P 1P) = (((𝑧 ·P 𝑣) +P ((𝑦 ·P 1P) +P (𝑧 ·P 1P))) +P (1P +P 1P)))
89	82, 88	eqtrd 2238	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) ∧ ((𝑤 ·P 𝑣) = 1P ∧ (𝑧 +P 𝑤) = 𝑦)) → (((𝑦 ·P 𝑣) +P ((𝑦 ·P 1P) +P (𝑧 ·P 1P))) +P 1P) = (((𝑧 ·P 𝑣) +P ((𝑦 ·P 1P) +P (𝑧 ·P 1P))) +P (1P +P 1P)))
90		distrprg 7703	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ P ∧ 𝑣 ∈ P ∧ 1P ∈ P) → (𝑦 ·P (𝑣 +P 1P)) = ((𝑦 ·P 𝑣) +P (𝑦 ·P 1P)))
91	68, 24, 67, 90	syl3anc 1250	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) → (𝑦 ·P (𝑣 +P 1P)) = ((𝑦 ·P 𝑣) +P (𝑦 ·P 1P)))
92	91	oveq1d 5961	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) → ((𝑦 ·P (𝑣 +P 1P)) +P (𝑧 ·P 1P)) = (((𝑦 ·P 𝑣) +P (𝑦 ·P 1P)) +P (𝑧 ·P 1P)))
93		mulclpr 7687	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ P ∧ 𝑣 ∈ P) → (𝑦 ·P 𝑣) ∈ P)
94	68, 24, 93	syl2anc 411	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) → (𝑦 ·P 𝑣) ∈ P)
95		addassprg 7694	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 ·P 𝑣) ∈ P ∧ (𝑦 ·P 1P) ∈ P ∧ (𝑧 ·P 1P) ∈ P) → (((𝑦 ·P 𝑣) +P (𝑦 ·P 1P)) +P (𝑧 ·P 1P)) = ((𝑦 ·P 𝑣) +P ((𝑦 ·P 1P) +P (𝑧 ·P 1P))))
96	94, 70, 72, 95	syl3anc 1250	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) → (((𝑦 ·P 𝑣) +P (𝑦 ·P 1P)) +P (𝑧 ·P 1P)) = ((𝑦 ·P 𝑣) +P ((𝑦 ·P 1P) +P (𝑧 ·P 1P))))
97	92, 96	eqtrd 2238	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) → ((𝑦 ·P (𝑣 +P 1P)) +P (𝑧 ·P 1P)) = ((𝑦 ·P 𝑣) +P ((𝑦 ·P 1P) +P (𝑧 ·P 1P))))
98	97	oveq1d 5961	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) → (((𝑦 ·P (𝑣 +P 1P)) +P (𝑧 ·P 1P)) +P 1P) = (((𝑦 ·P 𝑣) +P ((𝑦 ·P 1P) +P (𝑧 ·P 1P))) +P 1P))
99	98	adantr 276	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) ∧ ((𝑤 ·P 𝑣) = 1P ∧ (𝑧 +P 𝑤) = 𝑦)) → (((𝑦 ·P (𝑣 +P 1P)) +P (𝑧 ·P 1P)) +P 1P) = (((𝑦 ·P 𝑣) +P ((𝑦 ·P 1P) +P (𝑧 ·P 1P))) +P 1P))
100		distrprg 7703	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 ∈ P ∧ 𝑣 ∈ P ∧ 1P ∈ P) → (𝑧 ·P (𝑣 +P 1P)) = ((𝑧 ·P 𝑣) +P (𝑧 ·P 1P)))
101	57, 24, 67, 100	syl3anc 1250	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) → (𝑧 ·P (𝑣 +P 1P)) = ((𝑧 ·P 𝑣) +P (𝑧 ·P 1P)))
102	101	oveq2d 5962	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) → ((𝑦 ·P 1P) +P (𝑧 ·P (𝑣 +P 1P))) = ((𝑦 ·P 1P) +P ((𝑧 ·P 𝑣) +P (𝑧 ·P 1P))))
103	70, 66, 72, 76, 78	caov12d 6130	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) → ((𝑦 ·P 1P) +P ((𝑧 ·P 𝑣) +P (𝑧 ·P 1P))) = ((𝑧 ·P 𝑣) +P ((𝑦 ·P 1P) +P (𝑧 ·P 1P))))
104	102, 103	eqtrd 2238	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) → ((𝑦 ·P 1P) +P (𝑧 ·P (𝑣 +P 1P))) = ((𝑧 ·P 𝑣) +P ((𝑦 ·P 1P) +P (𝑧 ·P 1P))))
105	104	oveq1d 5961	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) → (((𝑦 ·P 1P) +P (𝑧 ·P (𝑣 +P 1P))) +P (1P +P 1P)) = (((𝑧 ·P 𝑣) +P ((𝑦 ·P 1P) +P (𝑧 ·P 1P))) +P (1P +P 1P)))
106	105	adantr 276	. . . . . . . . . . . . . 14 ⊢ ((((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) ∧ ((𝑤 ·P 𝑣) = 1P ∧ (𝑧 +P 𝑤) = 𝑦)) → (((𝑦 ·P 1P) +P (𝑧 ·P (𝑣 +P 1P))) +P (1P +P 1P)) = (((𝑧 ·P 𝑣) +P ((𝑦 ·P 1P) +P (𝑧 ·P 1P))) +P (1P +P 1P)))
107	89, 99, 106	3eqtr4d 2248	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) ∧ ((𝑤 ·P 𝑣) = 1P ∧ (𝑧 +P 𝑤) = 𝑦)) → (((𝑦 ·P (𝑣 +P 1P)) +P (𝑧 ·P 1P)) +P 1P) = (((𝑦 ·P 1P) +P (𝑧 ·P (𝑣 +P 1P))) +P (1P +P 1P)))
108	24, 16, 17	sylancl 413	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) → (𝑣 +P 1P) ∈ P)
109		mulclpr 7687	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ P ∧ (𝑣 +P 1P) ∈ P) → (𝑦 ·P (𝑣 +P 1P)) ∈ P)
110	68, 108, 109	syl2anc 411	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) → (𝑦 ·P (𝑣 +P 1P)) ∈ P)
111		addclpr 7652	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 ·P (𝑣 +P 1P)) ∈ P ∧ (𝑧 ·P 1P) ∈ P) → ((𝑦 ·P (𝑣 +P 1P)) +P (𝑧 ·P 1P)) ∈ P)
112	110, 72, 111	syl2anc 411	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) → ((𝑦 ·P (𝑣 +P 1P)) +P (𝑧 ·P 1P)) ∈ P)
113	104, 84	eqeltrd 2282	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) → ((𝑦 ·P 1P) +P (𝑧 ·P (𝑣 +P 1P))) ∈ P)
114		addclpr 7652	. . . . . . . . . . . . . . . . 17 ⊢ ((1P ∈ P ∧ 1P ∈ P) → (1P +P 1P) ∈ P)
115	16, 16, 114	mp2an 426	. . . . . . . . . . . . . . . 16 ⊢ (1P +P 1P) ∈ P
116	115	a1i 9	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) → (1P +P 1P) ∈ P)
117		enreceq 7851	. . . . . . . . . . . . . . 15 ⊢ (((((𝑦 ·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))))
118	112, 113, 116, 67, 117	syl22anc 1251	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ P ∧ 𝑧 ∈ 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))))
119	118	adantr 276	. . . . . . . . . . . . 13 ⊢ ((((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) ∧ ((𝑤 ·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))))
120	107, 119	mpbird 167	. . . . . . . . . . . 12 ⊢ ((((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) ∧ ((𝑤 ·P 𝑣) = 1P ∧ (𝑧 +P 𝑤) = 𝑦)) → [⟨((𝑦 ·P (𝑣 +P 1P)) +P (𝑧 ·P 1P)), ((𝑦 ·P 1P) +P (𝑧 ·P (𝑣 +P 1P)))⟩] ~R = [⟨(1P +P 1P), 1P⟩] ~R )
121	39, 120	eqtrd 2238	. . . . . . . . . . 11 ⊢ ((((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) ∧ ((𝑤 ·P 𝑣) = 1P ∧ (𝑧 +P 𝑤) = 𝑦)) → ([⟨𝑦, 𝑧⟩] ~R ·R [⟨(𝑣 +P 1P), 1P⟩] ~R ) = [⟨(1P +P 1P), 1P⟩] ~R )
122		df-1r 7847	. . . . . . . . . . 11 ⊢ 1R = [⟨(1P +P 1P), 1P⟩] ~R
123	121, 122	eqtr4di 2256	. . . . . . . . . 10 ⊢ ((((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) ∧ ((𝑤 ·P 𝑣) = 1P ∧ (𝑧 +P 𝑤) = 𝑦)) → ([⟨𝑦, 𝑧⟩] ~R ·R [⟨(𝑣 +P 1P), 1P⟩] ~R ) = 1R)
124		breq2 4049	. . . . . . . . . . . 12 ⊢ (𝑥 = [⟨(𝑣 +P 1P), 1P⟩] ~R → (0R <R 𝑥 ↔ 0R <R [⟨(𝑣 +P 1P), 1P⟩] ~R ))
125		oveq2 5954	. . . . . . . . . . . . 13 ⊢ (𝑥 = [⟨(𝑣 +P 1P), 1P⟩] ~R → ([⟨𝑦, 𝑧⟩] ~R ·R 𝑥) = ([⟨𝑦, 𝑧⟩] ~R ·R [⟨(𝑣 +P 1P), 1P⟩] ~R ))
126	125	eqeq1d 2214	. . . . . . . . . . . 12 ⊢ (𝑥 = [⟨(𝑣 +P 1P), 1P⟩] ~R → (([⟨𝑦, 𝑧⟩] ~R ·R 𝑥) = 1R ↔ ([⟨𝑦, 𝑧⟩] ~R ·R [⟨(𝑣 +P 1P), 1P⟩] ~R ) = 1R))
127	124, 126	anbi12d 473	. . . . . . . . . . 11 ⊢ (𝑥 = [⟨(𝑣 +P 1P), 1P⟩] ~R → ((0R <R 𝑥 ∧ ([⟨𝑦, 𝑧⟩] ~R ·R 𝑥) = 1R) ↔ (0R <R [⟨(𝑣 +P 1P), 1P⟩] ~R ∧ ([⟨𝑦, 𝑧⟩] ~R ·R [⟨(𝑣 +P 1P), 1P⟩] ~R ) = 1R)))
128	127	rspcev 2877	. . . . . . . . . 10 ⊢ (([⟨(𝑣 +P 1P), 1P⟩] ~R ∈ R ∧ (0R <R [⟨(𝑣 +P 1P), 1P⟩] ~R ∧ ([⟨𝑦, 𝑧⟩] ~R ·R [⟨(𝑣 +P 1P), 1P⟩] ~R ) = 1R)) → ∃𝑥 ∈ R (0R <R 𝑥 ∧ ([⟨𝑦, 𝑧⟩] ~R ·R 𝑥) = 1R))
129	23, 33, 123, 128	syl12anc 1248	. . . . . . . . 9 ⊢ ((((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) ∧ ((𝑤 ·P 𝑣) = 1P ∧ (𝑧 +P 𝑤) = 𝑦)) → ∃𝑥 ∈ R (0R <R 𝑥 ∧ ([⟨𝑦, 𝑧⟩] ~R ·R 𝑥) = 1R))
130	129	exp32 365	. . . . . . . 8 ⊢ (((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑤 ∈ P ∧ 𝑣 ∈ P)) → ((𝑤 ·P 𝑣) = 1P → ((𝑧 +P 𝑤) = 𝑦 → ∃𝑥 ∈ R (0R <R 𝑥 ∧ ([⟨𝑦, 𝑧⟩] ~R ·R 𝑥) = 1R))))
131	130	anassrs 400	. . . . . . 7 ⊢ ((((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ 𝑤 ∈ P) ∧ 𝑣 ∈ P) → ((𝑤 ·P 𝑣) = 1P → ((𝑧 +P 𝑤) = 𝑦 → ∃𝑥 ∈ R (0R <R 𝑥 ∧ ([⟨𝑦, 𝑧⟩] ~R ·R 𝑥) = 1R))))
132	131	rexlimdva 2623	. . . . . 6 ⊢ (((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ 𝑤 ∈ P) → (∃𝑣 ∈ P (𝑤 ·P 𝑣) = 1P → ((𝑧 +P 𝑤) = 𝑦 → ∃𝑥 ∈ R (0R <R 𝑥 ∧ ([⟨𝑦, 𝑧⟩] ~R ·R 𝑥) = 1R))))
133	15, 132	mpd 13	. . . . 5 ⊢ (((𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ 𝑤 ∈ P) → ((𝑧 +P 𝑤) = 𝑦 → ∃𝑥 ∈ R (0R <R 𝑥 ∧ ([⟨𝑦, 𝑧⟩] ~R ·R 𝑥) = 1R)))
134	133	rexlimdva 2623	. . . 4 ⊢ ((𝑦 ∈ P ∧ 𝑧 ∈ P) → (∃𝑤 ∈ P (𝑧 +P 𝑤) = 𝑦 → ∃𝑥 ∈ R (0R <R 𝑥 ∧ ([⟨𝑦, 𝑧⟩] ~R ·R 𝑥) = 1R)))
135	13, 134	syl5 32	. . 3 ⊢ ((𝑦 ∈ P ∧ 𝑧 ∈ P) → (0R <R [⟨𝑦, 𝑧⟩] ~R → ∃𝑥 ∈ R (0R <R 𝑥 ∧ ([⟨𝑦, 𝑧⟩] ~R ·R 𝑥) = 1R)))
136	4, 10, 135	ecoptocl 6711	. 2 ⊢ (𝐴 ∈ R → (0R <R 𝐴 → ∃𝑥 ∈ R (0R <R 𝑥 ∧ (𝐴 ·R 𝑥) = 1R)))
137	3, 136	mpcom 36	1 ⊢ (0R <R 𝐴 → ∃𝑥 ∈ R (0R <R 𝑥 ∧ (𝐴 ·R 𝑥) = 1R))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∧ w3a 981   = wceq 1373   ∈ wcel 2176  ∃wrex 2485  ⟨cop 3636   class class class wbr 4045  (class class class)co 5946  [cec 6620  Pcnp 7406  1_Pc1p 7407   +_P cpp 7408   ·_P cmp 7409  <_P cltp 7410   ~_R cer 7411  Rcnr 7412  0_Rc0r 7413  1_Rc1r 7414   ·_R cmr 7417   <_R cltr 7418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-13 2178  ax-14 2179  ax-ext 2187  ax-coll 4160  ax-sep 4163  ax-nul 4171  ax-pow 4219  ax-pr 4254  ax-un 4481  ax-setind 4586  ax-iinf 4637

This theorem depends on definitions:  df-bi 117  df-dc 837  df-3or 982  df-3an 983  df-tru 1376  df-fal 1379  df-nf 1484  df-sb 1786  df-eu 2057  df-mo 2058  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ne 2377  df-ral 2489  df-rex 2490  df-reu 2491  df-rab 2493  df-v 2774  df-sbc 2999  df-csb 3094  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3461  df-pw 3618  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-int 3886  df-iun 3929  df-br 4046  df-opab 4107  df-mpt 4108  df-tr 4144  df-eprel 4337  df-id 4341  df-po 4344  df-iso 4345  df-iord 4414  df-on 4416  df-suc 4419  df-iom 4640  df-xp 4682  df-rel 4683  df-cnv 4684  df-co 4685  df-dm 4686  df-rn 4687  df-res 4688  df-ima 4689  df-iota 5233  df-fun 5274  df-fn 5275  df-f 5276  df-f1 5277  df-fo 5278  df-f1o 5279  df-fv 5280  df-ov 5949  df-oprab 5950  df-mpo 5951  df-1st 6228  df-2nd 6229  df-recs 6393  df-irdg 6458  df-1o 6504  df-2o 6505  df-oadd 6508  df-omul 6509  df-er 6622  df-ec 6624  df-qs 6628  df-ni 7419  df-pli 7420  df-mi 7421  df-lti 7422  df-plpq 7459  df-mpq 7460  df-enq 7462  df-nqqs 7463  df-plqqs 7464  df-mqqs 7465  df-1nqqs 7466  df-rq 7467  df-ltnqqs 7468  df-enq0 7539  df-nq0 7540  df-0nq0 7541  df-plq0 7542  df-mq0 7543  df-inp 7581  df-i1p 7582  df-iplp 7583  df-imp 7584  df-iltp 7585  df-enr 7841  df-nr 7842  df-mr 7844  df-ltr 7845  df-0r 7846  df-1r 7847

This theorem is referenced by:  recexsrlem  7889  axprecex  7995