Metamath Proof Explorer

Theorem sqsscirc2

Description: The complex square of side D is a subset of the complex disc of radius D . (Contributed by Thierry Arnoux, 25-Sep-2017)

Ref Expression
Assertion sqsscirc2 ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐷 ∈ ℝ+ ) → ( ( ( abs ‘ ( ℜ ‘ ( 𝐵 − 𝐴 ) ) ) < ( 𝐷 / 2 ) ∧ ( abs ‘ ( ℑ ‘ ( 𝐵 − 𝐴 ) ) ) < ( 𝐷 / 2 ) ) → ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝐷 ) )

Proof

Step Hyp Ref Expression
1 simplr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐷 ∈ ℝ+ ) → 𝐵 ∈ ℂ )
2 simpll ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐷 ∈ ℝ+ ) → 𝐴 ∈ ℂ )
3 1 2 subcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐷 ∈ ℝ+ ) → ( 𝐵 − 𝐴 ) ∈ ℂ )
4 3 recld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐷 ∈ ℝ+ ) → ( ℜ ‘ ( 𝐵 − 𝐴 ) ) ∈ ℝ )
5 4 recnd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐷 ∈ ℝ+ ) → ( ℜ ‘ ( 𝐵 − 𝐴 ) ) ∈ ℂ )
6 5 abscld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐷 ∈ ℝ+ ) → ( abs ‘ ( ℜ ‘ ( 𝐵 − 𝐴 ) ) ) ∈ ℝ )
7 5 absge0d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐷 ∈ ℝ+ ) → 0 ≤ ( abs ‘ ( ℜ ‘ ( 𝐵 − 𝐴 ) ) ) )
8 6 7 jca ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐷 ∈ ℝ+ ) → ( ( abs ‘ ( ℜ ‘ ( 𝐵 − 𝐴 ) ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( ℜ ‘ ( 𝐵 − 𝐴 ) ) ) ) )
9 3 imcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐷 ∈ ℝ+ ) → ( ℑ ‘ ( 𝐵 − 𝐴 ) ) ∈ ℝ )
10 9 recnd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐷 ∈ ℝ+ ) → ( ℑ ‘ ( 𝐵 − 𝐴 ) ) ∈ ℂ )
11 10 abscld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐷 ∈ ℝ+ ) → ( abs ‘ ( ℑ ‘ ( 𝐵 − 𝐴 ) ) ) ∈ ℝ )
12 10 absge0d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐷 ∈ ℝ+ ) → 0 ≤ ( abs ‘ ( ℑ ‘ ( 𝐵 − 𝐴 ) ) ) )
13 11 12 jca ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐷 ∈ ℝ+ ) → ( ( abs ‘ ( ℑ ‘ ( 𝐵 − 𝐴 ) ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( ℑ ‘ ( 𝐵 − 𝐴 ) ) ) ) )
14 simpr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐷 ∈ ℝ+ ) → 𝐷 ∈ ℝ+ )
15 sqsscirc1 ⊢ ( ( ( ( ( abs ‘ ( ℜ ‘ ( 𝐵 − 𝐴 ) ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( ℜ ‘ ( 𝐵 − 𝐴 ) ) ) ) ∧ ( ( abs ‘ ( ℑ ‘ ( 𝐵 − 𝐴 ) ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( ℑ ‘ ( 𝐵 − 𝐴 ) ) ) ) ) ∧ 𝐷 ∈ ℝ+ ) → ( ( ( abs ‘ ( ℜ ‘ ( 𝐵 − 𝐴 ) ) ) < ( 𝐷 / 2 ) ∧ ( abs ‘ ( ℑ ‘ ( 𝐵 − 𝐴 ) ) ) < ( 𝐷 / 2 ) ) → ( √ ‘ ( ( ( abs ‘ ( ℜ ‘ ( 𝐵 − 𝐴 ) ) ) ↑ 2 ) + ( ( abs ‘ ( ℑ ‘ ( 𝐵 − 𝐴 ) ) ) ↑ 2 ) ) ) < 𝐷 ) )
16 8 13 14 15 syl21anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐷 ∈ ℝ+ ) → ( ( ( abs ‘ ( ℜ ‘ ( 𝐵 − 𝐴 ) ) ) < ( 𝐷 / 2 ) ∧ ( abs ‘ ( ℑ ‘ ( 𝐵 − 𝐴 ) ) ) < ( 𝐷 / 2 ) ) → ( √ ‘ ( ( ( abs ‘ ( ℜ ‘ ( 𝐵 − 𝐴 ) ) ) ↑ 2 ) + ( ( abs ‘ ( ℑ ‘ ( 𝐵 − 𝐴 ) ) ) ↑ 2 ) ) ) < 𝐷 ) )
17 3 absval2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐷 ∈ ℝ+ ) → ( abs ‘ ( 𝐵 − 𝐴 ) ) = ( √ ‘ ( ( ( ℜ ‘ ( 𝐵 − 𝐴 ) ) ↑ 2 ) + ( ( ℑ ‘ ( 𝐵 − 𝐴 ) ) ↑ 2 ) ) ) )
18 17 breq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐷 ∈ ℝ+ ) → ( ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝐷 ↔ ( √ ‘ ( ( ( ℜ ‘ ( 𝐵 − 𝐴 ) ) ↑ 2 ) + ( ( ℑ ‘ ( 𝐵 − 𝐴 ) ) ↑ 2 ) ) ) < 𝐷 ) )
19 absresq ⊢ ( ( ℜ ‘ ( 𝐵 − 𝐴 ) ) ∈ ℝ → ( ( abs ‘ ( ℜ ‘ ( 𝐵 − 𝐴 ) ) ) ↑ 2 ) = ( ( ℜ ‘ ( 𝐵 − 𝐴 ) ) ↑ 2 ) )
20 4 19 syl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐷 ∈ ℝ+ ) → ( ( abs ‘ ( ℜ ‘ ( 𝐵 − 𝐴 ) ) ) ↑ 2 ) = ( ( ℜ ‘ ( 𝐵 − 𝐴 ) ) ↑ 2 ) )
21 absresq ⊢ ( ( ℑ ‘ ( 𝐵 − 𝐴 ) ) ∈ ℝ → ( ( abs ‘ ( ℑ ‘ ( 𝐵 − 𝐴 ) ) ) ↑ 2 ) = ( ( ℑ ‘ ( 𝐵 − 𝐴 ) ) ↑ 2 ) )
22 9 21 syl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐷 ∈ ℝ+ ) → ( ( abs ‘ ( ℑ ‘ ( 𝐵 − 𝐴 ) ) ) ↑ 2 ) = ( ( ℑ ‘ ( 𝐵 − 𝐴 ) ) ↑ 2 ) )
23 20 22 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐷 ∈ ℝ+ ) → ( ( ( abs ‘ ( ℜ ‘ ( 𝐵 − 𝐴 ) ) ) ↑ 2 ) + ( ( abs ‘ ( ℑ ‘ ( 𝐵 − 𝐴 ) ) ) ↑ 2 ) ) = ( ( ( ℜ ‘ ( 𝐵 − 𝐴 ) ) ↑ 2 ) + ( ( ℑ ‘ ( 𝐵 − 𝐴 ) ) ↑ 2 ) ) )
24 23 fveq2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐷 ∈ ℝ+ ) → ( √ ‘ ( ( ( abs ‘ ( ℜ ‘ ( 𝐵 − 𝐴 ) ) ) ↑ 2 ) + ( ( abs ‘ ( ℑ ‘ ( 𝐵 − 𝐴 ) ) ) ↑ 2 ) ) ) = ( √ ‘ ( ( ( ℜ ‘ ( 𝐵 − 𝐴 ) ) ↑ 2 ) + ( ( ℑ ‘ ( 𝐵 − 𝐴 ) ) ↑ 2 ) ) ) )
25 24 breq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐷 ∈ ℝ+ ) → ( ( √ ‘ ( ( ( abs ‘ ( ℜ ‘ ( 𝐵 − 𝐴 ) ) ) ↑ 2 ) + ( ( abs ‘ ( ℑ ‘ ( 𝐵 − 𝐴 ) ) ) ↑ 2 ) ) ) < 𝐷 ↔ ( √ ‘ ( ( ( ℜ ‘ ( 𝐵 − 𝐴 ) ) ↑ 2 ) + ( ( ℑ ‘ ( 𝐵 − 𝐴 ) ) ↑ 2 ) ) ) < 𝐷 ) )
26 18 25 bitr4d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐷 ∈ ℝ+ ) → ( ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝐷 ↔ ( √ ‘ ( ( ( abs ‘ ( ℜ ‘ ( 𝐵 − 𝐴 ) ) ) ↑ 2 ) + ( ( abs ‘ ( ℑ ‘ ( 𝐵 − 𝐴 ) ) ) ↑ 2 ) ) ) < 𝐷 ) )
27 16 26 sylibrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐷 ∈ ℝ+ ) → ( ( ( abs ‘ ( ℜ ‘ ( 𝐵 − 𝐴 ) ) ) < ( 𝐷 / 2 ) ∧ ( abs ‘ ( ℑ ‘ ( 𝐵 − 𝐴 ) ) ) < ( 𝐷 / 2 ) ) → ( abs ‘ ( 𝐵 − 𝐴 ) ) < 𝐷 ) )