This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cndrngOLD

Description: Obsolete version of cndrng as of 30-Apr-2025. (Contributed by Stefan O'Rear, 27-Nov-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion cndrngOLD ℂfld ∈ DivRing

Proof

Step Hyp Ref Expression
1 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
2 1 a1i ⊢ ( ⊤ → ℂ = ( Base ‘ ℂfld ) )
3 cnfldmul ⊢ · = ( .r ‘ ℂfld )
4 3 a1i ⊢ ( ⊤ → · = ( .r ‘ ℂfld ) )
5 cnfld0 ⊢ 0 = ( 0g ‘ ℂfld )
6 5 a1i ⊢ ( ⊤ → 0 = ( 0g ‘ ℂfld ) )
7 cnfld1 ⊢ 1 = ( 1r ‘ ℂfld )
8 7 a1i ⊢ ( ⊤ → 1 = ( 1r ‘ ℂfld ) )
9 cnring ⊢ ℂfld ∈ Ring
10 9 a1i ⊢ ( ⊤ → ℂfld ∈ Ring )
11 mulne0 ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) ) → ( 𝑥 · 𝑦 ) ≠ 0 )
12 11 3adant1 ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) ) → ( 𝑥 · 𝑦 ) ≠ 0 )
13 ax-1ne0 ⊢ 1 ≠ 0
14 13 a1i ⊢ ( ⊤ → 1 ≠ 0 )
15 reccl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) → ( 1 / 𝑥 ) ∈ ℂ )
16 15 adantl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ) → ( 1 / 𝑥 ) ∈ ℂ )
17 recid2 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) → ( ( 1 / 𝑥 ) · 𝑥 ) = 1 )
18 17 adantl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ) → ( ( 1 / 𝑥 ) · 𝑥 ) = 1 )
19 2 4 6 8 10 12 14 16 18 isdrngd ⊢ ( ⊤ → ℂfld ∈ DivRing )
20 19 mptru ⊢ ℂfld ∈ DivRing