absabv

Description: The regular absolute value function on the complex numbers is in fact an absolute value under our definition. (Contributed by Mario Carneiro, 4-Dec-2014)

		Ref	Expression
	Assertion	absabv	⊢ abs ∈ ( AbsVal ‘ ℂ_fld )

Proof

Step	Hyp	Ref	Expression
1		eqidd	⊢ ( ⊤ → ( AbsVal ‘ ℂ_fld ) = ( AbsVal ‘ ℂ_fld ) )
2		cnfldbas	⊢ ℂ = ( Base ‘ ℂ_fld )
3	2	a1i	⊢ ( ⊤ → ℂ = ( Base ‘ ℂ_fld ) )
4		cnfldadd	⊢ + = ( +_g ‘ ℂ_fld )
5	4	a1i	⊢ ( ⊤ → + = ( +_g ‘ ℂ_fld ) )
6		cnfldmul	⊢ · = ( ._r ‘ ℂ_fld )
7	6	a1i	⊢ ( ⊤ → · = ( ._r ‘ ℂ_fld ) )
8		cnfld0	⊢ 0 = ( 0_g ‘ ℂ_fld )
9	8	a1i	⊢ ( ⊤ → 0 = ( 0_g ‘ ℂ_fld ) )
10		cnring	⊢ ℂ_fld ∈ Ring
11	10	a1i	⊢ ( ⊤ → ℂ_fld ∈ Ring )
12		absf	⊢ abs : ℂ ⟶ ℝ
13	12	a1i	⊢ ( ⊤ → abs : ℂ ⟶ ℝ )
14		abs0	⊢ ( abs ‘ 0 ) = 0
15	14	a1i	⊢ ( ⊤ → ( abs ‘ 0 ) = 0 )
16		absgt0	⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ≠ 0 ↔ 0 < ( abs ‘ 𝑥 ) ) )
17	16	biimpa	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) → 0 < ( abs ‘ 𝑥 ) )
18	17	3adant1	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) → 0 < ( abs ‘ 𝑥 ) )
19		absmul	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( abs ‘ ( 𝑥 · 𝑦 ) ) = ( ( abs ‘ 𝑥 ) · ( abs ‘ 𝑦 ) ) )
20	19	ad2ant2r	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) ) → ( abs ‘ ( 𝑥 · 𝑦 ) ) = ( ( abs ‘ 𝑥 ) · ( abs ‘ 𝑦 ) ) )
21	20	3adant1	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) ) → ( abs ‘ ( 𝑥 · 𝑦 ) ) = ( ( abs ‘ 𝑥 ) · ( abs ‘ 𝑦 ) ) )
22		abstri	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( abs ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( abs ‘ 𝑥 ) + ( abs ‘ 𝑦 ) ) )
23	22	ad2ant2r	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) ) → ( abs ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( abs ‘ 𝑥 ) + ( abs ‘ 𝑦 ) ) )
24	23	3adant1	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) ) → ( abs ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( abs ‘ 𝑥 ) + ( abs ‘ 𝑦 ) ) )
25	1 3 5 7 9 11 13 15 18 21 24	isabvd	⊢ ( ⊤ → abs ∈ ( AbsVal ‘ ℂ_fld ) )
26	25	mptru	⊢ abs ∈ ( AbsVal ‘ ℂ_fld )

Metamath Proof Explorer

Theorem absabv

Proof