Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  smprngopr Structured version   Visualization version   GIF version

Theorem smprngopr 35213
Description: A simple ring (one whose only ideals are 0 and 𝑅) is a prime ring. (Contributed by Jeff Madsen, 6-Jan-2011.)
Hypotheses
Ref Expression
smprngpr.1 𝐺 = (1st𝑅)
smprngpr.2 𝐻 = (2nd𝑅)
smprngpr.3 𝑋 = ran 𝐺
smprngpr.4 𝑍 = (GId‘𝐺)
smprngpr.5 𝑈 = (GId‘𝐻)
Assertion
Ref Expression
smprngopr ((𝑅 ∈ RingOps ∧ 𝑈𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → 𝑅 ∈ PrRing)

Proof of Theorem smprngopr
Dummy variables 𝑖 𝑗 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp1 1128 . 2 ((𝑅 ∈ RingOps ∧ 𝑈𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → 𝑅 ∈ RingOps)
2 smprngpr.1 . . . . 5 𝐺 = (1st𝑅)
3 smprngpr.4 . . . . 5 𝑍 = (GId‘𝐺)
42, 30idl 35186 . . . 4 (𝑅 ∈ RingOps → {𝑍} ∈ (Idl‘𝑅))
543ad2ant1 1125 . . 3 ((𝑅 ∈ RingOps ∧ 𝑈𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → {𝑍} ∈ (Idl‘𝑅))
6 smprngpr.2 . . . . . . . 8 𝐻 = (2nd𝑅)
7 smprngpr.3 . . . . . . . 8 𝑋 = ran 𝐺
8 smprngpr.5 . . . . . . . 8 𝑈 = (GId‘𝐻)
92, 6, 7, 3, 80rngo 35188 . . . . . . 7 (𝑅 ∈ RingOps → (𝑍 = 𝑈𝑋 = {𝑍}))
10 eqcom 2828 . . . . . . 7 (𝑈 = 𝑍𝑍 = 𝑈)
11 eqcom 2828 . . . . . . 7 ({𝑍} = 𝑋𝑋 = {𝑍})
129, 10, 113bitr4g 315 . . . . . 6 (𝑅 ∈ RingOps → (𝑈 = 𝑍 ↔ {𝑍} = 𝑋))
1312necon3bid 3060 . . . . 5 (𝑅 ∈ RingOps → (𝑈𝑍 ↔ {𝑍} ≠ 𝑋))
1413biimpa 477 . . . 4 ((𝑅 ∈ RingOps ∧ 𝑈𝑍) → {𝑍} ≠ 𝑋)
15143adant3 1124 . . 3 ((𝑅 ∈ RingOps ∧ 𝑈𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → {𝑍} ≠ 𝑋)
16 df-pr 4562 . . . . . . . 8 {{𝑍}, 𝑋} = ({{𝑍}} ∪ {𝑋})
1716eqeq2i 2834 . . . . . . 7 ((Idl‘𝑅) = {{𝑍}, 𝑋} ↔ (Idl‘𝑅) = ({{𝑍}} ∪ {𝑋}))
18 eleq2 2901 . . . . . . . . 9 ((Idl‘𝑅) = ({{𝑍}} ∪ {𝑋}) → (𝑖 ∈ (Idl‘𝑅) ↔ 𝑖 ∈ ({{𝑍}} ∪ {𝑋})))
19 eleq2 2901 . . . . . . . . 9 ((Idl‘𝑅) = ({{𝑍}} ∪ {𝑋}) → (𝑗 ∈ (Idl‘𝑅) ↔ 𝑗 ∈ ({{𝑍}} ∪ {𝑋})))
2018, 19anbi12d 630 . . . . . . . 8 ((Idl‘𝑅) = ({{𝑍}} ∪ {𝑋}) → ((𝑖 ∈ (Idl‘𝑅) ∧ 𝑗 ∈ (Idl‘𝑅)) ↔ (𝑖 ∈ ({{𝑍}} ∪ {𝑋}) ∧ 𝑗 ∈ ({{𝑍}} ∪ {𝑋}))))
21 elun 4124 . . . . . . . . . 10 (𝑖 ∈ ({{𝑍}} ∪ {𝑋}) ↔ (𝑖 ∈ {{𝑍}} ∨ 𝑖 ∈ {𝑋}))
22 velsn 4575 . . . . . . . . . . 11 (𝑖 ∈ {{𝑍}} ↔ 𝑖 = {𝑍})
23 velsn 4575 . . . . . . . . . . 11 (𝑖 ∈ {𝑋} ↔ 𝑖 = 𝑋)
2422, 23orbi12i 908 . . . . . . . . . 10 ((𝑖 ∈ {{𝑍}} ∨ 𝑖 ∈ {𝑋}) ↔ (𝑖 = {𝑍} ∨ 𝑖 = 𝑋))
2521, 24bitri 276 . . . . . . . . 9 (𝑖 ∈ ({{𝑍}} ∪ {𝑋}) ↔ (𝑖 = {𝑍} ∨ 𝑖 = 𝑋))
26 elun 4124 . . . . . . . . . 10 (𝑗 ∈ ({{𝑍}} ∪ {𝑋}) ↔ (𝑗 ∈ {{𝑍}} ∨ 𝑗 ∈ {𝑋}))
27 velsn 4575 . . . . . . . . . . 11 (𝑗 ∈ {{𝑍}} ↔ 𝑗 = {𝑍})
28 velsn 4575 . . . . . . . . . . 11 (𝑗 ∈ {𝑋} ↔ 𝑗 = 𝑋)
2927, 28orbi12i 908 . . . . . . . . . 10 ((𝑗 ∈ {{𝑍}} ∨ 𝑗 ∈ {𝑋}) ↔ (𝑗 = {𝑍} ∨ 𝑗 = 𝑋))
3026, 29bitri 276 . . . . . . . . 9 (𝑗 ∈ ({{𝑍}} ∪ {𝑋}) ↔ (𝑗 = {𝑍} ∨ 𝑗 = 𝑋))
3125, 30anbi12i 626 . . . . . . . 8 ((𝑖 ∈ ({{𝑍}} ∪ {𝑋}) ∧ 𝑗 ∈ ({{𝑍}} ∪ {𝑋})) ↔ ((𝑖 = {𝑍} ∨ 𝑖 = 𝑋) ∧ (𝑗 = {𝑍} ∨ 𝑗 = 𝑋)))
3220, 31syl6bb 288 . . . . . . 7 ((Idl‘𝑅) = ({{𝑍}} ∪ {𝑋}) → ((𝑖 ∈ (Idl‘𝑅) ∧ 𝑗 ∈ (Idl‘𝑅)) ↔ ((𝑖 = {𝑍} ∨ 𝑖 = 𝑋) ∧ (𝑗 = {𝑍} ∨ 𝑗 = 𝑋))))
3317, 32sylbi 218 . . . . . 6 ((Idl‘𝑅) = {{𝑍}, 𝑋} → ((𝑖 ∈ (Idl‘𝑅) ∧ 𝑗 ∈ (Idl‘𝑅)) ↔ ((𝑖 = {𝑍} ∨ 𝑖 = 𝑋) ∧ (𝑗 = {𝑍} ∨ 𝑗 = 𝑋))))
34333ad2ant3 1127 . . . . 5 ((𝑅 ∈ RingOps ∧ 𝑈𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → ((𝑖 ∈ (Idl‘𝑅) ∧ 𝑗 ∈ (Idl‘𝑅)) ↔ ((𝑖 = {𝑍} ∨ 𝑖 = 𝑋) ∧ (𝑗 = {𝑍} ∨ 𝑗 = 𝑋))))
35 eqimss 4022 . . . . . . . . . . 11 (𝑖 = {𝑍} → 𝑖 ⊆ {𝑍})
3635orcd 869 . . . . . . . . . 10 (𝑖 = {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))
3736adantr 481 . . . . . . . . 9 ((𝑖 = {𝑍} ∧ 𝑗 = {𝑍}) → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))
3837a1d 25 . . . . . . . 8 ((𝑖 = {𝑍} ∧ 𝑗 = {𝑍}) → (∀𝑥𝑖𝑦𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})))
3938a1i 11 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝑈𝑍) → ((𝑖 = {𝑍} ∧ 𝑗 = {𝑍}) → (∀𝑥𝑖𝑦𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))))
40 eqimss 4022 . . . . . . . . . . 11 (𝑗 = {𝑍} → 𝑗 ⊆ {𝑍})
4140olcd 870 . . . . . . . . . 10 (𝑗 = {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))
4241adantl 482 . . . . . . . . 9 ((𝑖 = 𝑋𝑗 = {𝑍}) → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))
4342a1d 25 . . . . . . . 8 ((𝑖 = 𝑋𝑗 = {𝑍}) → (∀𝑥𝑖𝑦𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})))
4443a1i 11 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝑈𝑍) → ((𝑖 = 𝑋𝑗 = {𝑍}) → (∀𝑥𝑖𝑦𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))))
4536adantr 481 . . . . . . . . 9 ((𝑖 = {𝑍} ∧ 𝑗 = 𝑋) → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))
4645a1d 25 . . . . . . . 8 ((𝑖 = {𝑍} ∧ 𝑗 = 𝑋) → (∀𝑥𝑖𝑦𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})))
4746a1i 11 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝑈𝑍) → ((𝑖 = {𝑍} ∧ 𝑗 = 𝑋) → (∀𝑥𝑖𝑦𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))))
482rneqi 5801 . . . . . . . . . . . . . 14 ran 𝐺 = ran (1st𝑅)
497, 48eqtri 2844 . . . . . . . . . . . . 13 𝑋 = ran (1st𝑅)
5049, 6, 8rngo1cl 35100 . . . . . . . . . . . 12 (𝑅 ∈ RingOps → 𝑈𝑋)
5150adantr 481 . . . . . . . . . . 11 ((𝑅 ∈ RingOps ∧ 𝑈𝑍) → 𝑈𝑋)
526, 49, 8rngolidm 35098 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ RingOps ∧ 𝑈𝑋) → (𝑈𝐻𝑈) = 𝑈)
5350, 52mpdan 683 . . . . . . . . . . . . . . 15 (𝑅 ∈ RingOps → (𝑈𝐻𝑈) = 𝑈)
5453eleq1d 2897 . . . . . . . . . . . . . 14 (𝑅 ∈ RingOps → ((𝑈𝐻𝑈) ∈ {𝑍} ↔ 𝑈 ∈ {𝑍}))
558fvexi 6678 . . . . . . . . . . . . . . 15 𝑈 ∈ V
5655elsn 4574 . . . . . . . . . . . . . 14 (𝑈 ∈ {𝑍} ↔ 𝑈 = 𝑍)
5754, 56syl6bb 288 . . . . . . . . . . . . 13 (𝑅 ∈ RingOps → ((𝑈𝐻𝑈) ∈ {𝑍} ↔ 𝑈 = 𝑍))
5857necon3bbid 3053 . . . . . . . . . . . 12 (𝑅 ∈ RingOps → (¬ (𝑈𝐻𝑈) ∈ {𝑍} ↔ 𝑈𝑍))
5958biimpar 478 . . . . . . . . . . 11 ((𝑅 ∈ RingOps ∧ 𝑈𝑍) → ¬ (𝑈𝐻𝑈) ∈ {𝑍})
60 oveq1 7152 . . . . . . . . . . . . . 14 (𝑥 = 𝑈 → (𝑥𝐻𝑦) = (𝑈𝐻𝑦))
6160eleq1d 2897 . . . . . . . . . . . . 13 (𝑥 = 𝑈 → ((𝑥𝐻𝑦) ∈ {𝑍} ↔ (𝑈𝐻𝑦) ∈ {𝑍}))
6261notbid 319 . . . . . . . . . . . 12 (𝑥 = 𝑈 → (¬ (𝑥𝐻𝑦) ∈ {𝑍} ↔ ¬ (𝑈𝐻𝑦) ∈ {𝑍}))
63 oveq2 7153 . . . . . . . . . . . . . 14 (𝑦 = 𝑈 → (𝑈𝐻𝑦) = (𝑈𝐻𝑈))
6463eleq1d 2897 . . . . . . . . . . . . 13 (𝑦 = 𝑈 → ((𝑈𝐻𝑦) ∈ {𝑍} ↔ (𝑈𝐻𝑈) ∈ {𝑍}))
6564notbid 319 . . . . . . . . . . . 12 (𝑦 = 𝑈 → (¬ (𝑈𝐻𝑦) ∈ {𝑍} ↔ ¬ (𝑈𝐻𝑈) ∈ {𝑍}))
6662, 65rspc2ev 3634 . . . . . . . . . . 11 ((𝑈𝑋𝑈𝑋 ∧ ¬ (𝑈𝐻𝑈) ∈ {𝑍}) → ∃𝑥𝑋𝑦𝑋 ¬ (𝑥𝐻𝑦) ∈ {𝑍})
6751, 51, 59, 66syl3anc 1363 . . . . . . . . . 10 ((𝑅 ∈ RingOps ∧ 𝑈𝑍) → ∃𝑥𝑋𝑦𝑋 ¬ (𝑥𝐻𝑦) ∈ {𝑍})
68 rexnal2 3258 . . . . . . . . . 10 (∃𝑥𝑋𝑦𝑋 ¬ (𝑥𝐻𝑦) ∈ {𝑍} ↔ ¬ ∀𝑥𝑋𝑦𝑋 (𝑥𝐻𝑦) ∈ {𝑍})
6967, 68sylib 219 . . . . . . . . 9 ((𝑅 ∈ RingOps ∧ 𝑈𝑍) → ¬ ∀𝑥𝑋𝑦𝑋 (𝑥𝐻𝑦) ∈ {𝑍})
7069pm2.21d 121 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ 𝑈𝑍) → (∀𝑥𝑋𝑦𝑋 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})))
71 raleq 3406 . . . . . . . . . 10 (𝑖 = 𝑋 → (∀𝑥𝑖𝑦𝑗 (𝑥𝐻𝑦) ∈ {𝑍} ↔ ∀𝑥𝑋𝑦𝑗 (𝑥𝐻𝑦) ∈ {𝑍}))
72 raleq 3406 . . . . . . . . . . 11 (𝑗 = 𝑋 → (∀𝑦𝑗 (𝑥𝐻𝑦) ∈ {𝑍} ↔ ∀𝑦𝑋 (𝑥𝐻𝑦) ∈ {𝑍}))
7372ralbidv 3197 . . . . . . . . . 10 (𝑗 = 𝑋 → (∀𝑥𝑋𝑦𝑗 (𝑥𝐻𝑦) ∈ {𝑍} ↔ ∀𝑥𝑋𝑦𝑋 (𝑥𝐻𝑦) ∈ {𝑍}))
7471, 73sylan9bb 510 . . . . . . . . 9 ((𝑖 = 𝑋𝑗 = 𝑋) → (∀𝑥𝑖𝑦𝑗 (𝑥𝐻𝑦) ∈ {𝑍} ↔ ∀𝑥𝑋𝑦𝑋 (𝑥𝐻𝑦) ∈ {𝑍}))
7574imbi1d 343 . . . . . . . 8 ((𝑖 = 𝑋𝑗 = 𝑋) → ((∀𝑥𝑖𝑦𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})) ↔ (∀𝑥𝑋𝑦𝑋 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))))
7670, 75syl5ibrcom 248 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝑈𝑍) → ((𝑖 = 𝑋𝑗 = 𝑋) → (∀𝑥𝑖𝑦𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))))
7739, 44, 47, 76ccased 1030 . . . . . 6 ((𝑅 ∈ RingOps ∧ 𝑈𝑍) → (((𝑖 = {𝑍} ∨ 𝑖 = 𝑋) ∧ (𝑗 = {𝑍} ∨ 𝑗 = 𝑋)) → (∀𝑥𝑖𝑦𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))))
78773adant3 1124 . . . . 5 ((𝑅 ∈ RingOps ∧ 𝑈𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → (((𝑖 = {𝑍} ∨ 𝑖 = 𝑋) ∧ (𝑗 = {𝑍} ∨ 𝑗 = 𝑋)) → (∀𝑥𝑖𝑦𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))))
7934, 78sylbid 241 . . . 4 ((𝑅 ∈ RingOps ∧ 𝑈𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → ((𝑖 ∈ (Idl‘𝑅) ∧ 𝑗 ∈ (Idl‘𝑅)) → (∀𝑥𝑖𝑦𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍}))))
8079ralrimivv 3190 . . 3 ((𝑅 ∈ RingOps ∧ 𝑈𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → ∀𝑖 ∈ (Idl‘𝑅)∀𝑗 ∈ (Idl‘𝑅)(∀𝑥𝑖𝑦𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})))
812, 6, 7ispridl 35195 . . . 4 (𝑅 ∈ RingOps → ({𝑍} ∈ (PrIdl‘𝑅) ↔ ({𝑍} ∈ (Idl‘𝑅) ∧ {𝑍} ≠ 𝑋 ∧ ∀𝑖 ∈ (Idl‘𝑅)∀𝑗 ∈ (Idl‘𝑅)(∀𝑥𝑖𝑦𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})))))
82813ad2ant1 1125 . . 3 ((𝑅 ∈ RingOps ∧ 𝑈𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → ({𝑍} ∈ (PrIdl‘𝑅) ↔ ({𝑍} ∈ (Idl‘𝑅) ∧ {𝑍} ≠ 𝑋 ∧ ∀𝑖 ∈ (Idl‘𝑅)∀𝑗 ∈ (Idl‘𝑅)(∀𝑥𝑖𝑦𝑗 (𝑥𝐻𝑦) ∈ {𝑍} → (𝑖 ⊆ {𝑍} ∨ 𝑗 ⊆ {𝑍})))))
835, 15, 80, 82mpbir3and 1334 . 2 ((𝑅 ∈ RingOps ∧ 𝑈𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → {𝑍} ∈ (PrIdl‘𝑅))
842, 3isprrngo 35211 . 2 (𝑅 ∈ PrRing ↔ (𝑅 ∈ RingOps ∧ {𝑍} ∈ (PrIdl‘𝑅)))
851, 83, 84sylanbrc 583 1 ((𝑅 ∈ RingOps ∧ 𝑈𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → 𝑅 ∈ PrRing)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 841  w3a 1079   = wceq 1528  wcel 2105  wne 3016  wral 3138  wrex 3139  cun 3933  wss 3935  {csn 4559  {cpr 4561  ran crn 5550  cfv 6349  (class class class)co 7145  1st c1st 7678  2nd c2nd 7679  GIdcgi 28195  RingOpscrngo 35055  Idlcidl 35168  PrIdlcpridl 35169  PrRingcprrng 35207
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-rep 5182  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-iun 4914  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-riota 7103  df-ov 7148  df-1st 7680  df-2nd 7681  df-grpo 28198  df-gid 28199  df-ginv 28200  df-ablo 28250  df-ass 35004  df-exid 35006  df-mgmOLD 35010  df-sgrOLD 35022  df-mndo 35028  df-rngo 35056  df-idl 35171  df-pridl 35172  df-prrngo 35209
This theorem is referenced by:  divrngpr  35214
  Copyright terms: Public domain W3C validator