Metamath Proof Explorer

Theorem sqsscirc1

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

Ref Expression
Assertion sqsscirc1 ( ( ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ ℝ ∧ 0 ≤ 𝑌 ) ) ∧ 𝐷 ∈ ℝ+ ) → ( ( 𝑋 < ( 𝐷 / 2 ) ∧ 𝑌 < ( 𝐷 / 2 ) ) → ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) ) < 𝐷 ) )

Proof

Step Hyp Ref Expression
1 simp-4l ⊢ ( ( ( ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ ℝ ∧ 0 ≤ 𝑌 ) ) ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝑋 < ( 𝐷 / 2 ) ∧ 𝑌 < ( 𝐷 / 2 ) ) ) → 𝑋 ∈ ℝ )
2 1 resqcld ⊢ ( ( ( ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ ℝ ∧ 0 ≤ 𝑌 ) ) ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝑋 < ( 𝐷 / 2 ) ∧ 𝑌 < ( 𝐷 / 2 ) ) ) → ( 𝑋 ↑ 2 ) ∈ ℝ )
3 simpllr ⊢ ( ( ( ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ ℝ ∧ 0 ≤ 𝑌 ) ) ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝑋 < ( 𝐷 / 2 ) ∧ 𝑌 < ( 𝐷 / 2 ) ) ) → ( 𝑌 ∈ ℝ ∧ 0 ≤ 𝑌 ) )
4 3 simpld ⊢ ( ( ( ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ ℝ ∧ 0 ≤ 𝑌 ) ) ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝑋 < ( 𝐷 / 2 ) ∧ 𝑌 < ( 𝐷 / 2 ) ) ) → 𝑌 ∈ ℝ )
5 4 resqcld ⊢ ( ( ( ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ ℝ ∧ 0 ≤ 𝑌 ) ) ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝑋 < ( 𝐷 / 2 ) ∧ 𝑌 < ( 𝐷 / 2 ) ) ) → ( 𝑌 ↑ 2 ) ∈ ℝ )
6 2 5 readdcld ⊢ ( ( ( ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ ℝ ∧ 0 ≤ 𝑌 ) ) ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝑋 < ( 𝐷 / 2 ) ∧ 𝑌 < ( 𝐷 / 2 ) ) ) → ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) ∈ ℝ )
7 1 sqge0d ⊢ ( ( ( ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ ℝ ∧ 0 ≤ 𝑌 ) ) ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝑋 < ( 𝐷 / 2 ) ∧ 𝑌 < ( 𝐷 / 2 ) ) ) → 0 ≤ ( 𝑋 ↑ 2 ) )
8 4 sqge0d ⊢ ( ( ( ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ ℝ ∧ 0 ≤ 𝑌 ) ) ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝑋 < ( 𝐷 / 2 ) ∧ 𝑌 < ( 𝐷 / 2 ) ) ) → 0 ≤ ( 𝑌 ↑ 2 ) )
9 2 5 7 8 addge0d ⊢ ( ( ( ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ ℝ ∧ 0 ≤ 𝑌 ) ) ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝑋 < ( 𝐷 / 2 ) ∧ 𝑌 < ( 𝐷 / 2 ) ) ) → 0 ≤ ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) )
10 6 9 resqrtcld ⊢ ( ( ( ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ ℝ ∧ 0 ≤ 𝑌 ) ) ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝑋 < ( 𝐷 / 2 ) ∧ 𝑌 < ( 𝐷 / 2 ) ) ) → ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) ) ∈ ℝ )
11 simplr ⊢ ( ( ( ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ ℝ ∧ 0 ≤ 𝑌 ) ) ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝑋 < ( 𝐷 / 2 ) ∧ 𝑌 < ( 𝐷 / 2 ) ) ) → 𝐷 ∈ ℝ+ )
12 11 rpred ⊢ ( ( ( ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ ℝ ∧ 0 ≤ 𝑌 ) ) ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝑋 < ( 𝐷 / 2 ) ∧ 𝑌 < ( 𝐷 / 2 ) ) ) → 𝐷 ∈ ℝ )
13 12 rehalfcld ⊢ ( ( ( ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ ℝ ∧ 0 ≤ 𝑌 ) ) ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝑋 < ( 𝐷 / 2 ) ∧ 𝑌 < ( 𝐷 / 2 ) ) ) → ( 𝐷 / 2 ) ∈ ℝ )
14 13 resqcld ⊢ ( ( ( ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ ℝ ∧ 0 ≤ 𝑌 ) ) ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝑋 < ( 𝐷 / 2 ) ∧ 𝑌 < ( 𝐷 / 2 ) ) ) → ( ( 𝐷 / 2 ) ↑ 2 ) ∈ ℝ )
15 14 14 readdcld ⊢ ( ( ( ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ ℝ ∧ 0 ≤ 𝑌 ) ) ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝑋 < ( 𝐷 / 2 ) ∧ 𝑌 < ( 𝐷 / 2 ) ) ) → ( ( ( 𝐷 / 2 ) ↑ 2 ) + ( ( 𝐷 / 2 ) ↑ 2 ) ) ∈ ℝ )
16 13 sqge0d ⊢ ( ( ( ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ ℝ ∧ 0 ≤ 𝑌 ) ) ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝑋 < ( 𝐷 / 2 ) ∧ 𝑌 < ( 𝐷 / 2 ) ) ) → 0 ≤ ( ( 𝐷 / 2 ) ↑ 2 ) )
17 14 14 16 16 addge0d ⊢ ( ( ( ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ ℝ ∧ 0 ≤ 𝑌 ) ) ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝑋 < ( 𝐷 / 2 ) ∧ 𝑌 < ( 𝐷 / 2 ) ) ) → 0 ≤ ( ( ( 𝐷 / 2 ) ↑ 2 ) + ( ( 𝐷 / 2 ) ↑ 2 ) ) )
18 15 17 resqrtcld ⊢ ( ( ( ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ ℝ ∧ 0 ≤ 𝑌 ) ) ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝑋 < ( 𝐷 / 2 ) ∧ 𝑌 < ( 𝐷 / 2 ) ) ) → ( √ ‘ ( ( ( 𝐷 / 2 ) ↑ 2 ) + ( ( 𝐷 / 2 ) ↑ 2 ) ) ) ∈ ℝ )
19 simprl ⊢ ( ( ( ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ ℝ ∧ 0 ≤ 𝑌 ) ) ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝑋 < ( 𝐷 / 2 ) ∧ 𝑌 < ( 𝐷 / 2 ) ) ) → 𝑋 < ( 𝐷 / 2 ) )
20 simp-4r ⊢ ( ( ( ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ ℝ ∧ 0 ≤ 𝑌 ) ) ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝑋 < ( 𝐷 / 2 ) ∧ 𝑌 < ( 𝐷 / 2 ) ) ) → 0 ≤ 𝑋 )
21 2rp ⊢ 2 ∈ ℝ+
22 21 a1i ⊢ ( ( ( ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ ℝ ∧ 0 ≤ 𝑌 ) ) ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝑋 < ( 𝐷 / 2 ) ∧ 𝑌 < ( 𝐷 / 2 ) ) ) → 2 ∈ ℝ+ )
23 11 rpge0d ⊢ ( ( ( ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ ℝ ∧ 0 ≤ 𝑌 ) ) ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝑋 < ( 𝐷 / 2 ) ∧ 𝑌 < ( 𝐷 / 2 ) ) ) → 0 ≤ 𝐷 )
24 12 22 23 divge0d ⊢ ( ( ( ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ ℝ ∧ 0 ≤ 𝑌 ) ) ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝑋 < ( 𝐷 / 2 ) ∧ 𝑌 < ( 𝐷 / 2 ) ) ) → 0 ≤ ( 𝐷 / 2 ) )
25 1 13 20 24 lt2sqd ⊢ ( ( ( ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ ℝ ∧ 0 ≤ 𝑌 ) ) ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝑋 < ( 𝐷 / 2 ) ∧ 𝑌 < ( 𝐷 / 2 ) ) ) → ( 𝑋 < ( 𝐷 / 2 ) ↔ ( 𝑋 ↑ 2 ) < ( ( 𝐷 / 2 ) ↑ 2 ) ) )
26 19 25 mpbid ⊢ ( ( ( ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ ℝ ∧ 0 ≤ 𝑌 ) ) ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝑋 < ( 𝐷 / 2 ) ∧ 𝑌 < ( 𝐷 / 2 ) ) ) → ( 𝑋 ↑ 2 ) < ( ( 𝐷 / 2 ) ↑ 2 ) )
27 simprr ⊢ ( ( ( ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ ℝ ∧ 0 ≤ 𝑌 ) ) ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝑋 < ( 𝐷 / 2 ) ∧ 𝑌 < ( 𝐷 / 2 ) ) ) → 𝑌 < ( 𝐷 / 2 ) )
28 3 simprd ⊢ ( ( ( ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ ℝ ∧ 0 ≤ 𝑌 ) ) ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝑋 < ( 𝐷 / 2 ) ∧ 𝑌 < ( 𝐷 / 2 ) ) ) → 0 ≤ 𝑌 )
29 4 13 28 24 lt2sqd ⊢ ( ( ( ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ ℝ ∧ 0 ≤ 𝑌 ) ) ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝑋 < ( 𝐷 / 2 ) ∧ 𝑌 < ( 𝐷 / 2 ) ) ) → ( 𝑌 < ( 𝐷 / 2 ) ↔ ( 𝑌 ↑ 2 ) < ( ( 𝐷 / 2 ) ↑ 2 ) ) )
30 27 29 mpbid ⊢ ( ( ( ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ ℝ ∧ 0 ≤ 𝑌 ) ) ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝑋 < ( 𝐷 / 2 ) ∧ 𝑌 < ( 𝐷 / 2 ) ) ) → ( 𝑌 ↑ 2 ) < ( ( 𝐷 / 2 ) ↑ 2 ) )
31 2 5 14 14 26 30 lt2addd ⊢ ( ( ( ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ ℝ ∧ 0 ≤ 𝑌 ) ) ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝑋 < ( 𝐷 / 2 ) ∧ 𝑌 < ( 𝐷 / 2 ) ) ) → ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) < ( ( ( 𝐷 / 2 ) ↑ 2 ) + ( ( 𝐷 / 2 ) ↑ 2 ) ) )
32 6 9 15 17 sqrtltd ⊢ ( ( ( ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ ℝ ∧ 0 ≤ 𝑌 ) ) ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝑋 < ( 𝐷 / 2 ) ∧ 𝑌 < ( 𝐷 / 2 ) ) ) → ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) < ( ( ( 𝐷 / 2 ) ↑ 2 ) + ( ( 𝐷 / 2 ) ↑ 2 ) ) ↔ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) ) < ( √ ‘ ( ( ( 𝐷 / 2 ) ↑ 2 ) + ( ( 𝐷 / 2 ) ↑ 2 ) ) ) ) )
33 31 32 mpbid ⊢ ( ( ( ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ ℝ ∧ 0 ≤ 𝑌 ) ) ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝑋 < ( 𝐷 / 2 ) ∧ 𝑌 < ( 𝐷 / 2 ) ) ) → ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) ) < ( √ ‘ ( ( ( 𝐷 / 2 ) ↑ 2 ) + ( ( 𝐷 / 2 ) ↑ 2 ) ) ) )
34 rpre ⊢ ( 𝐷 ∈ ℝ+ → 𝐷 ∈ ℝ )
35 34 rehalfcld ⊢ ( 𝐷 ∈ ℝ+ → ( 𝐷 / 2 ) ∈ ℝ )
36 35 resqcld ⊢ ( 𝐷 ∈ ℝ+ → ( ( 𝐷 / 2 ) ↑ 2 ) ∈ ℝ )
37 36 recnd ⊢ ( 𝐷 ∈ ℝ+ → ( ( 𝐷 / 2 ) ↑ 2 ) ∈ ℂ )
38 37 2timesd ⊢ ( 𝐷 ∈ ℝ+ → ( 2 · ( ( 𝐷 / 2 ) ↑ 2 ) ) = ( ( ( 𝐷 / 2 ) ↑ 2 ) + ( ( 𝐷 / 2 ) ↑ 2 ) ) )
39 38 fveq2d ⊢ ( 𝐷 ∈ ℝ+ → ( √ ‘ ( 2 · ( ( 𝐷 / 2 ) ↑ 2 ) ) ) = ( √ ‘ ( ( ( 𝐷 / 2 ) ↑ 2 ) + ( ( 𝐷 / 2 ) ↑ 2 ) ) ) )
40 21 a1i ⊢ ( 𝐷 ∈ ℝ+ → 2 ∈ ℝ+ )
41 rpge0 ⊢ ( 𝐷 ∈ ℝ+ → 0 ≤ 𝐷 )
42 34 40 41 divge0d ⊢ ( 𝐷 ∈ ℝ+ → 0 ≤ ( 𝐷 / 2 ) )
43 35 42 sqrtsqd ⊢ ( 𝐷 ∈ ℝ+ → ( √ ‘ ( ( 𝐷 / 2 ) ↑ 2 ) ) = ( 𝐷 / 2 ) )
44 43 oveq2d ⊢ ( 𝐷 ∈ ℝ+ → ( ( √ ‘ 2 ) · ( √ ‘ ( ( 𝐷 / 2 ) ↑ 2 ) ) ) = ( ( √ ‘ 2 ) · ( 𝐷 / 2 ) ) )
45 2re ⊢ 2 ∈ ℝ
46 45 a1i ⊢ ( 𝐷 ∈ ℝ+ → 2 ∈ ℝ )
47 0le2 ⊢ 0 ≤ 2
48 47 a1i ⊢ ( 𝐷 ∈ ℝ+ → 0 ≤ 2 )
49 35 sqge0d ⊢ ( 𝐷 ∈ ℝ+ → 0 ≤ ( ( 𝐷 / 2 ) ↑ 2 ) )
50 46 48 36 49 sqrtmuld ⊢ ( 𝐷 ∈ ℝ+ → ( √ ‘ ( 2 · ( ( 𝐷 / 2 ) ↑ 2 ) ) ) = ( ( √ ‘ 2 ) · ( √ ‘ ( ( 𝐷 / 2 ) ↑ 2 ) ) ) )
51 2cnd ⊢ ( 𝐷 ∈ ℝ+ → 2 ∈ ℂ )
52 51 sqrtcld ⊢ ( 𝐷 ∈ ℝ+ → ( √ ‘ 2 ) ∈ ℂ )
53 rpcn ⊢ ( 𝐷 ∈ ℝ+ → 𝐷 ∈ ℂ )
54 2ne0 ⊢ 2 ≠ 0
55 54 a1i ⊢ ( 𝐷 ∈ ℝ+ → 2 ≠ 0 )
56 52 51 53 55 div32d ⊢ ( 𝐷 ∈ ℝ+ → ( ( ( √ ‘ 2 ) / 2 ) · 𝐷 ) = ( ( √ ‘ 2 ) · ( 𝐷 / 2 ) ) )
57 44 50 56 3eqtr4d ⊢ ( 𝐷 ∈ ℝ+ → ( √ ‘ ( 2 · ( ( 𝐷 / 2 ) ↑ 2 ) ) ) = ( ( ( √ ‘ 2 ) / 2 ) · 𝐷 ) )
58 39 57 eqtr3d ⊢ ( 𝐷 ∈ ℝ+ → ( √ ‘ ( ( ( 𝐷 / 2 ) ↑ 2 ) + ( ( 𝐷 / 2 ) ↑ 2 ) ) ) = ( ( ( √ ‘ 2 ) / 2 ) · 𝐷 ) )
59 2lt4 ⊢ 2 < 4
60 4re ⊢ 4 ∈ ℝ
61 0re ⊢ 0 ∈ ℝ
62 4pos ⊢ 0 < 4
63 61 60 62 ltleii ⊢ 0 ≤ 4
64 sqrtlt ⊢ ( ( ( 2 ∈ ℝ ∧ 0 ≤ 2 ) ∧ ( 4 ∈ ℝ ∧ 0 ≤ 4 ) ) → ( 2 < 4 ↔ ( √ ‘ 2 ) < ( √ ‘ 4 ) ) )
65 45 47 60 63 64 mp4an ⊢ ( 2 < 4 ↔ ( √ ‘ 2 ) < ( √ ‘ 4 ) )
66 59 65 mpbi ⊢ ( √ ‘ 2 ) < ( √ ‘ 4 )
67 2pos ⊢ 0 < 2
68 45 67 sqrtpclii ⊢ ( √ ‘ 2 ) ∈ ℝ
69 60 62 sqrtpclii ⊢ ( √ ‘ 4 ) ∈ ℝ
70 68 69 45 67 ltdiv1ii ⊢ ( ( √ ‘ 2 ) < ( √ ‘ 4 ) ↔ ( ( √ ‘ 2 ) / 2 ) < ( ( √ ‘ 4 ) / 2 ) )
71 66 70 mpbi ⊢ ( ( √ ‘ 2 ) / 2 ) < ( ( √ ‘ 4 ) / 2 )
72 sqrtsq ⊢ ( ( 2 ∈ ℝ ∧ 0 ≤ 2 ) → ( √ ‘ ( 2 ↑ 2 ) ) = 2 )
73 45 47 72 mp2an ⊢ ( √ ‘ ( 2 ↑ 2 ) ) = 2
74 73 oveq1i ⊢ ( ( √ ‘ ( 2 ↑ 2 ) ) / 2 ) = ( 2 / 2 )
75 sq2 ⊢ ( 2 ↑ 2 ) = 4
76 75 fveq2i ⊢ ( √ ‘ ( 2 ↑ 2 ) ) = ( √ ‘ 4 )
77 76 oveq1i ⊢ ( ( √ ‘ ( 2 ↑ 2 ) ) / 2 ) = ( ( √ ‘ 4 ) / 2 )
78 2div2e1 ⊢ ( 2 / 2 ) = 1
79 74 77 78 3eqtr3i ⊢ ( ( √ ‘ 4 ) / 2 ) = 1
80 71 79 breqtri ⊢ ( ( √ ‘ 2 ) / 2 ) < 1
81 46 48 resqrtcld ⊢ ( 𝐷 ∈ ℝ+ → ( √ ‘ 2 ) ∈ ℝ )
82 81 rehalfcld ⊢ ( 𝐷 ∈ ℝ+ → ( ( √ ‘ 2 ) / 2 ) ∈ ℝ )
83 1red ⊢ ( 𝐷 ∈ ℝ+ → 1 ∈ ℝ )
84 id ⊢ ( 𝐷 ∈ ℝ+ → 𝐷 ∈ ℝ+ )
85 82 83 84 ltmul1d ⊢ ( 𝐷 ∈ ℝ+ → ( ( ( √ ‘ 2 ) / 2 ) < 1 ↔ ( ( ( √ ‘ 2 ) / 2 ) · 𝐷 ) < ( 1 · 𝐷 ) ) )
86 80 85 mpbii ⊢ ( 𝐷 ∈ ℝ+ → ( ( ( √ ‘ 2 ) / 2 ) · 𝐷 ) < ( 1 · 𝐷 ) )
87 53 mulid2d ⊢ ( 𝐷 ∈ ℝ+ → ( 1 · 𝐷 ) = 𝐷 )
88 86 87 breqtrd ⊢ ( 𝐷 ∈ ℝ+ → ( ( ( √ ‘ 2 ) / 2 ) · 𝐷 ) < 𝐷 )
89 58 88 eqbrtrd ⊢ ( 𝐷 ∈ ℝ+ → ( √ ‘ ( ( ( 𝐷 / 2 ) ↑ 2 ) + ( ( 𝐷 / 2 ) ↑ 2 ) ) ) < 𝐷 )
90 11 89 syl ⊢ ( ( ( ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ ℝ ∧ 0 ≤ 𝑌 ) ) ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝑋 < ( 𝐷 / 2 ) ∧ 𝑌 < ( 𝐷 / 2 ) ) ) → ( √ ‘ ( ( ( 𝐷 / 2 ) ↑ 2 ) + ( ( 𝐷 / 2 ) ↑ 2 ) ) ) < 𝐷 )
91 10 18 12 33 90 lttrd ⊢ ( ( ( ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ ℝ ∧ 0 ≤ 𝑌 ) ) ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝑋 < ( 𝐷 / 2 ) ∧ 𝑌 < ( 𝐷 / 2 ) ) ) → ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) ) < 𝐷 )
92 91 ex ⊢ ( ( ( ( 𝑋 ∈ ℝ ∧ 0 ≤ 𝑋 ) ∧ ( 𝑌 ∈ ℝ ∧ 0 ≤ 𝑌 ) ) ∧ 𝐷 ∈ ℝ+ ) → ( ( 𝑋 < ( 𝐷 / 2 ) ∧ 𝑌 < ( 𝐷 / 2 ) ) → ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) ) < 𝐷 ) )