sqsscirc1 - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > sqsscirc1		Structured version Visualization version GIF version

Theorem sqsscirc1 33418

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

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

**Proof of Theorem sqsscirc1**
Step	Hyp	Ref	Expression
1		simp-4l 780	. . . . . 6 ⊢ (((((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ ℝ ∧ 0 ≤ 𝑌)) ∧ 𝐷 ∈ ℝ⁺) ∧ (𝑋 < (𝐷 / 2) ∧ 𝑌 < (𝐷 / 2))) → 𝑋 ∈ ℝ)
2	1	resqcld 14095	. . . . 5 ⊢ (((((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ ℝ ∧ 0 ≤ 𝑌)) ∧ 𝐷 ∈ ℝ⁺) ∧ (𝑋 < (𝐷 / 2) ∧ 𝑌 < (𝐷 / 2))) → (𝑋↑2) ∈ ℝ)
3		simpllr 773	. . . . . . 7 ⊢ (((((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ ℝ ∧ 0 ≤ 𝑌)) ∧ 𝐷 ∈ ℝ⁺) ∧ (𝑋 < (𝐷 / 2) ∧ 𝑌 < (𝐷 / 2))) → (𝑌 ∈ ℝ ∧ 0 ≤ 𝑌))
4	3	simpld 494	. . . . . 6 ⊢ (((((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ ℝ ∧ 0 ≤ 𝑌)) ∧ 𝐷 ∈ ℝ⁺) ∧ (𝑋 < (𝐷 / 2) ∧ 𝑌 < (𝐷 / 2))) → 𝑌 ∈ ℝ)
5	4	resqcld 14095	. . . . 5 ⊢ (((((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ ℝ ∧ 0 ≤ 𝑌)) ∧ 𝐷 ∈ ℝ⁺) ∧ (𝑋 < (𝐷 / 2) ∧ 𝑌 < (𝐷 / 2))) → (𝑌↑2) ∈ ℝ)
6	2, 5	readdcld 11247	. . . 4 ⊢ (((((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ ℝ ∧ 0 ≤ 𝑌)) ∧ 𝐷 ∈ ℝ⁺) ∧ (𝑋 < (𝐷 / 2) ∧ 𝑌 < (𝐷 / 2))) → ((𝑋↑2) + (𝑌↑2)) ∈ ℝ)
7	1	sqge0d 14107	. . . . 5 ⊢ (((((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ ℝ ∧ 0 ≤ 𝑌)) ∧ 𝐷 ∈ ℝ⁺) ∧ (𝑋 < (𝐷 / 2) ∧ 𝑌 < (𝐷 / 2))) → 0 ≤ (𝑋↑2))
8	4	sqge0d 14107	. . . . 5 ⊢ (((((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ ℝ ∧ 0 ≤ 𝑌)) ∧ 𝐷 ∈ ℝ⁺) ∧ (𝑋 < (𝐷 / 2) ∧ 𝑌 < (𝐷 / 2))) → 0 ≤ (𝑌↑2))
9	2, 5, 7, 8	addge0d 11794	. . . 4 ⊢ (((((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ ℝ ∧ 0 ≤ 𝑌)) ∧ 𝐷 ∈ ℝ⁺) ∧ (𝑋 < (𝐷 / 2) ∧ 𝑌 < (𝐷 / 2))) → 0 ≤ ((𝑋↑2) + (𝑌↑2)))
10	6, 9	resqrtcld 15370	. . 3 ⊢ (((((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ ℝ ∧ 0 ≤ 𝑌)) ∧ 𝐷 ∈ ℝ⁺) ∧ (𝑋 < (𝐷 / 2) ∧ 𝑌 < (𝐷 / 2))) → (√‘((𝑋↑2) + (𝑌↑2))) ∈ ℝ)
11		simplr 766	. . . . . . . 8 ⊢ (((((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ ℝ ∧ 0 ≤ 𝑌)) ∧ 𝐷 ∈ ℝ⁺) ∧ (𝑋 < (𝐷 / 2) ∧ 𝑌 < (𝐷 / 2))) → 𝐷 ∈ ℝ⁺)
12	11	rpred 13022	. . . . . . 7 ⊢ (((((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ ℝ ∧ 0 ≤ 𝑌)) ∧ 𝐷 ∈ ℝ⁺) ∧ (𝑋 < (𝐷 / 2) ∧ 𝑌 < (𝐷 / 2))) → 𝐷 ∈ ℝ)
13	12	rehalfcld 12463	. . . . . 6 ⊢ (((((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ ℝ ∧ 0 ≤ 𝑌)) ∧ 𝐷 ∈ ℝ⁺) ∧ (𝑋 < (𝐷 / 2) ∧ 𝑌 < (𝐷 / 2))) → (𝐷 / 2) ∈ ℝ)
14	13	resqcld 14095	. . . . 5 ⊢ (((((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ ℝ ∧ 0 ≤ 𝑌)) ∧ 𝐷 ∈ ℝ⁺) ∧ (𝑋 < (𝐷 / 2) ∧ 𝑌 < (𝐷 / 2))) → ((𝐷 / 2)↑2) ∈ ℝ)
15	14, 14	readdcld 11247	. . . 4 ⊢ (((((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ ℝ ∧ 0 ≤ 𝑌)) ∧ 𝐷 ∈ ℝ⁺) ∧ (𝑋 < (𝐷 / 2) ∧ 𝑌 < (𝐷 / 2))) → (((𝐷 / 2)↑2) + ((𝐷 / 2)↑2)) ∈ ℝ)
16	13	sqge0d 14107	. . . . 5 ⊢ (((((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ ℝ ∧ 0 ≤ 𝑌)) ∧ 𝐷 ∈ ℝ⁺) ∧ (𝑋 < (𝐷 / 2) ∧ 𝑌 < (𝐷 / 2))) → 0 ≤ ((𝐷 / 2)↑2))
17	14, 14, 16, 16	addge0d 11794	. . . 4 ⊢ (((((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ ℝ ∧ 0 ≤ 𝑌)) ∧ 𝐷 ∈ ℝ⁺) ∧ (𝑋 < (𝐷 / 2) ∧ 𝑌 < (𝐷 / 2))) → 0 ≤ (((𝐷 / 2)↑2) + ((𝐷 / 2)↑2)))
18	15, 17	resqrtcld 15370	. . 3 ⊢ (((((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ ℝ ∧ 0 ≤ 𝑌)) ∧ 𝐷 ∈ ℝ⁺) ∧ (𝑋 < (𝐷 / 2) ∧ 𝑌 < (𝐷 / 2))) → (√‘(((𝐷 / 2)↑2) + ((𝐷 / 2)↑2))) ∈ ℝ)
19		simprl 768	. . . . . 6 ⊢ (((((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ ℝ ∧ 0 ≤ 𝑌)) ∧ 𝐷 ∈ ℝ⁺) ∧ (𝑋 < (𝐷 / 2) ∧ 𝑌 < (𝐷 / 2))) → 𝑋 < (𝐷 / 2))
20		simp-4r 781	. . . . . . 7 ⊢ (((((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ ℝ ∧ 0 ≤ 𝑌)) ∧ 𝐷 ∈ ℝ⁺) ∧ (𝑋 < (𝐷 / 2) ∧ 𝑌 < (𝐷 / 2))) → 0 ≤ 𝑋)
21		2rp 12985	. . . . . . . . 9 ⊢ 2 ∈ ℝ⁺
22	21	a1i 11	. . . . . . . 8 ⊢ (((((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ ℝ ∧ 0 ≤ 𝑌)) ∧ 𝐷 ∈ ℝ⁺) ∧ (𝑋 < (𝐷 / 2) ∧ 𝑌 < (𝐷 / 2))) → 2 ∈ ℝ⁺)
23	11	rpge0d 13026	. . . . . . . 8 ⊢ (((((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ ℝ ∧ 0 ≤ 𝑌)) ∧ 𝐷 ∈ ℝ⁺) ∧ (𝑋 < (𝐷 / 2) ∧ 𝑌 < (𝐷 / 2))) → 0 ≤ 𝐷)
24	12, 22, 23	divge0d 13062	. . . . . . 7 ⊢ (((((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ ℝ ∧ 0 ≤ 𝑌)) ∧ 𝐷 ∈ ℝ⁺) ∧ (𝑋 < (𝐷 / 2) ∧ 𝑌 < (𝐷 / 2))) → 0 ≤ (𝐷 / 2))
25	1, 13, 20, 24	lt2sqd 14224	. . . . . 6 ⊢ (((((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ ℝ ∧ 0 ≤ 𝑌)) ∧ 𝐷 ∈ ℝ⁺) ∧ (𝑋 < (𝐷 / 2) ∧ 𝑌 < (𝐷 / 2))) → (𝑋 < (𝐷 / 2) ↔ (𝑋↑2) < ((𝐷 / 2)↑2)))
26	19, 25	mpbid 231	. . . . 5 ⊢ (((((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ ℝ ∧ 0 ≤ 𝑌)) ∧ 𝐷 ∈ ℝ⁺) ∧ (𝑋 < (𝐷 / 2) ∧ 𝑌 < (𝐷 / 2))) → (𝑋↑2) < ((𝐷 / 2)↑2))
27		simprr 770	. . . . . 6 ⊢ (((((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ ℝ ∧ 0 ≤ 𝑌)) ∧ 𝐷 ∈ ℝ⁺) ∧ (𝑋 < (𝐷 / 2) ∧ 𝑌 < (𝐷 / 2))) → 𝑌 < (𝐷 / 2))
28	3	simprd 495	. . . . . . 7 ⊢ (((((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ ℝ ∧ 0 ≤ 𝑌)) ∧ 𝐷 ∈ ℝ⁺) ∧ (𝑋 < (𝐷 / 2) ∧ 𝑌 < (𝐷 / 2))) → 0 ≤ 𝑌)
29	4, 13, 28, 24	lt2sqd 14224	. . . . . 6 ⊢ (((((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ ℝ ∧ 0 ≤ 𝑌)) ∧ 𝐷 ∈ ℝ⁺) ∧ (𝑋 < (𝐷 / 2) ∧ 𝑌 < (𝐷 / 2))) → (𝑌 < (𝐷 / 2) ↔ (𝑌↑2) < ((𝐷 / 2)↑2)))
30	27, 29	mpbid 231	. . . . 5 ⊢ (((((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ ℝ ∧ 0 ≤ 𝑌)) ∧ 𝐷 ∈ ℝ⁺) ∧ (𝑋 < (𝐷 / 2) ∧ 𝑌 < (𝐷 / 2))) → (𝑌↑2) < ((𝐷 / 2)↑2))
31	2, 5, 14, 14, 26, 30	lt2addd 11841	. . . 4 ⊢ (((((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ ℝ ∧ 0 ≤ 𝑌)) ∧ 𝐷 ∈ ℝ⁺) ∧ (𝑋 < (𝐷 / 2) ∧ 𝑌 < (𝐷 / 2))) → ((𝑋↑2) + (𝑌↑2)) < (((𝐷 / 2)↑2) + ((𝐷 / 2)↑2)))
32	6, 9, 15, 17	sqrtltd 15380	. . . 4 ⊢ (((((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ ℝ ∧ 0 ≤ 𝑌)) ∧ 𝐷 ∈ ℝ⁺) ∧ (𝑋 < (𝐷 / 2) ∧ 𝑌 < (𝐷 / 2))) → (((𝑋↑2) + (𝑌↑2)) < (((𝐷 / 2)↑2) + ((𝐷 / 2)↑2)) ↔ (√‘((𝑋↑2) + (𝑌↑2))) < (√‘(((𝐷 / 2)↑2) + ((𝐷 / 2)↑2)))))
33	31, 32	mpbid 231	. . 3 ⊢ (((((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ ℝ ∧ 0 ≤ 𝑌)) ∧ 𝐷 ∈ ℝ⁺) ∧ (𝑋 < (𝐷 / 2) ∧ 𝑌 < (𝐷 / 2))) → (√‘((𝑋↑2) + (𝑌↑2))) < (√‘(((𝐷 / 2)↑2) + ((𝐷 / 2)↑2))))
34		rpre 12988	. . . . . . . . . . 11 ⊢ (𝐷 ∈ ℝ⁺ → 𝐷 ∈ ℝ)
35	34	rehalfcld 12463	. . . . . . . . . 10 ⊢ (𝐷 ∈ ℝ⁺ → (𝐷 / 2) ∈ ℝ)
36	35	resqcld 14095	. . . . . . . . 9 ⊢ (𝐷 ∈ ℝ⁺ → ((𝐷 / 2)↑2) ∈ ℝ)
37	36	recnd 11246	. . . . . . . 8 ⊢ (𝐷 ∈ ℝ⁺ → ((𝐷 / 2)↑2) ∈ ℂ)
38	37	2timesd 12459	. . . . . . 7 ⊢ (𝐷 ∈ ℝ⁺ → (2 · ((𝐷 / 2)↑2)) = (((𝐷 / 2)↑2) + ((𝐷 / 2)↑2)))
39	38	fveq2d 6889	. . . . . 6 ⊢ (𝐷 ∈ ℝ⁺ → (√‘(2 · ((𝐷 / 2)↑2))) = (√‘(((𝐷 / 2)↑2) + ((𝐷 / 2)↑2))))
40	21	a1i 11	. . . . . . . . . 10 ⊢ (𝐷 ∈ ℝ⁺ → 2 ∈ ℝ⁺)
41		rpge0 12993	. . . . . . . . . 10 ⊢ (𝐷 ∈ ℝ⁺ → 0 ≤ 𝐷)
42	34, 40, 41	divge0d 13062	. . . . . . . . 9 ⊢ (𝐷 ∈ ℝ⁺ → 0 ≤ (𝐷 / 2))
43	35, 42	sqrtsqd 15372	. . . . . . . 8 ⊢ (𝐷 ∈ ℝ⁺ → (√‘((𝐷 / 2)↑2)) = (𝐷 / 2))
44	43	oveq2d 7421	. . . . . . 7 ⊢ (𝐷 ∈ ℝ⁺ → ((√‘2) · (√‘((𝐷 / 2)↑2))) = ((√‘2) · (𝐷 / 2)))
45		2re 12290	. . . . . . . . 9 ⊢ 2 ∈ ℝ
46	45	a1i 11	. . . . . . . 8 ⊢ (𝐷 ∈ ℝ⁺ → 2 ∈ ℝ)
47		0le2 12318	. . . . . . . . 9 ⊢ 0 ≤ 2
48	47	a1i 11	. . . . . . . 8 ⊢ (𝐷 ∈ ℝ⁺ → 0 ≤ 2)
49	35	sqge0d 14107	. . . . . . . 8 ⊢ (𝐷 ∈ ℝ⁺ → 0 ≤ ((𝐷 / 2)↑2))
50	46, 48, 36, 49	sqrtmuld 15377	. . . . . . 7 ⊢ (𝐷 ∈ ℝ⁺ → (√‘(2 · ((𝐷 / 2)↑2))) = ((√‘2) · (√‘((𝐷 / 2)↑2))))
51		2cnd 12294	. . . . . . . . 9 ⊢ (𝐷 ∈ ℝ⁺ → 2 ∈ ℂ)
52	51	sqrtcld 15390	. . . . . . . 8 ⊢ (𝐷 ∈ ℝ⁺ → (√‘2) ∈ ℂ)
53		rpcn 12990	. . . . . . . 8 ⊢ (𝐷 ∈ ℝ⁺ → 𝐷 ∈ ℂ)
54		2ne0 12320	. . . . . . . . 9 ⊢ 2 ≠ 0
55	54	a1i 11	. . . . . . . 8 ⊢ (𝐷 ∈ ℝ⁺ → 2 ≠ 0)
56	52, 51, 53, 55	div32d 12017	. . . . . . 7 ⊢ (𝐷 ∈ ℝ⁺ → (((√‘2) / 2) · 𝐷) = ((√‘2) · (𝐷 / 2)))
57	44, 50, 56	3eqtr4d 2776	. . . . . 6 ⊢ (𝐷 ∈ ℝ⁺ → (√‘(2 · ((𝐷 / 2)↑2))) = (((√‘2) / 2) · 𝐷))
58	39, 57	eqtr3d 2768	. . . . 5 ⊢ (𝐷 ∈ ℝ⁺ → (√‘(((𝐷 / 2)↑2) + ((𝐷 / 2)↑2))) = (((√‘2) / 2) · 𝐷))
59		2lt4 12391	. . . . . . . . . 10 ⊢ 2 < 4
60		4re 12300	. . . . . . . . . . 11 ⊢ 4 ∈ ℝ
61		0re 11220	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ
62		4pos 12323	. . . . . . . . . . . 12 ⊢ 0 < 4
63	61, 60, 62	ltleii 11341	. . . . . . . . . . 11 ⊢ 0 ≤ 4
64		sqrtlt 15214	. . . . . . . . . . 11 ⊢ (((2 ∈ ℝ ∧ 0 ≤ 2) ∧ (4 ∈ ℝ ∧ 0 ≤ 4)) → (2 < 4 ↔ (√‘2) < (√‘4)))
65	45, 47, 60, 63, 64	mp4an 690	. . . . . . . . . 10 ⊢ (2 < 4 ↔ (√‘2) < (√‘4))
66	59, 65	mpbi 229	. . . . . . . . 9 ⊢ (√‘2) < (√‘4)
67		2pos 12319	. . . . . . . . . . 11 ⊢ 0 < 2
68	45, 67	sqrtpclii 15335	. . . . . . . . . 10 ⊢ (√‘2) ∈ ℝ
69	60, 62	sqrtpclii 15335	. . . . . . . . . 10 ⊢ (√‘4) ∈ ℝ
70	68, 69, 45, 67	ltdiv1ii 12147	. . . . . . . . 9 ⊢ ((√‘2) < (√‘4) ↔ ((√‘2) / 2) < ((√‘4) / 2))
71	66, 70	mpbi 229	. . . . . . . 8 ⊢ ((√‘2) / 2) < ((√‘4) / 2)
72		sqrtsq 15222	. . . . . . . . . . 11 ⊢ ((2 ∈ ℝ ∧ 0 ≤ 2) → (√‘(2↑2)) = 2)
73	45, 47, 72	mp2an 689	. . . . . . . . . 10 ⊢ (√‘(2↑2)) = 2
74	73	oveq1i 7415	. . . . . . . . 9 ⊢ ((√‘(2↑2)) / 2) = (2 / 2)
75		sq2 14166	. . . . . . . . . . 11 ⊢ (2↑2) = 4
76	75	fveq2i 6888	. . . . . . . . . 10 ⊢ (√‘(2↑2)) = (√‘4)
77	76	oveq1i 7415	. . . . . . . . 9 ⊢ ((√‘(2↑2)) / 2) = ((√‘4) / 2)
78		2div2e1 12357	. . . . . . . . 9 ⊢ (2 / 2) = 1
79	74, 77, 78	3eqtr3i 2762	. . . . . . . 8 ⊢ ((√‘4) / 2) = 1
80	71, 79	breqtri 5166	. . . . . . 7 ⊢ ((√‘2) / 2) < 1
81	46, 48	resqrtcld 15370	. . . . . . . . 9 ⊢ (𝐷 ∈ ℝ⁺ → (√‘2) ∈ ℝ)
82	81	rehalfcld 12463	. . . . . . . 8 ⊢ (𝐷 ∈ ℝ⁺ → ((√‘2) / 2) ∈ ℝ)
83		1red 11219	. . . . . . . 8 ⊢ (𝐷 ∈ ℝ⁺ → 1 ∈ ℝ)
84		id 22	. . . . . . . 8 ⊢ (𝐷 ∈ ℝ⁺ → 𝐷 ∈ ℝ⁺)
85	82, 83, 84	ltmul1d 13063	. . . . . . 7 ⊢ (𝐷 ∈ ℝ⁺ → (((√‘2) / 2) < 1 ↔ (((√‘2) / 2) · 𝐷) < (1 · 𝐷)))
86	80, 85	mpbii 232	. . . . . 6 ⊢ (𝐷 ∈ ℝ⁺ → (((√‘2) / 2) · 𝐷) < (1 · 𝐷))
87	53	mullidd 11236	. . . . . 6 ⊢ (𝐷 ∈ ℝ⁺ → (1 · 𝐷) = 𝐷)
88	86, 87	breqtrd 5167	. . . . 5 ⊢ (𝐷 ∈ ℝ⁺ → (((√‘2) / 2) · 𝐷) < 𝐷)
89	58, 88	eqbrtrd 5163	. . . 4 ⊢ (𝐷 ∈ ℝ⁺ → (√‘(((𝐷 / 2)↑2) + ((𝐷 / 2)↑2))) < 𝐷)
90	11, 89	syl 17	. . 3 ⊢ (((((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ ℝ ∧ 0 ≤ 𝑌)) ∧ 𝐷 ∈ ℝ⁺) ∧ (𝑋 < (𝐷 / 2) ∧ 𝑌 < (𝐷 / 2))) → (√‘(((𝐷 / 2)↑2) + ((𝐷 / 2)↑2))) < 𝐷)
91	10, 18, 12, 33, 90	lttrd 11379	. 2 ⊢ (((((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ ℝ ∧ 0 ≤ 𝑌)) ∧ 𝐷 ∈ ℝ⁺) ∧ (𝑋 < (𝐷 / 2) ∧ 𝑌 < (𝐷 / 2))) → (√‘((𝑋↑2) + (𝑌↑2))) < 𝐷)
92	91	ex 412	1 ⊢ ((((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ ℝ ∧ 0 ≤ 𝑌)) ∧ 𝐷 ∈ ℝ⁺) → ((𝑋 < (𝐷 / 2) ∧ 𝑌 < (𝐷 / 2)) → (√‘((𝑋↑2) + (𝑌↑2))) < 𝐷))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1533 ∈ wcel 2098 ≠ wne 2934 class class class wbr 5141 ‘cfv 6537 (class class class)co 7405 ℝcr 11111 0cc0 11112 1c1 11113 + caddc 11115 · cmul 11117 < clt 11252 ≤ cle 11253 / cdiv 11875 2c2 12271 4c4 12273 ℝ⁺crp 12980 ↑cexp 14032 √csqrt 15186

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2697 ax-sep 5292 ax-nul 5299 ax-pow 5356 ax-pr 5420 ax-un 7722 ax-cnex 11168 ax-resscn 11169 ax-1cn 11170 ax-icn 11171 ax-addcl 11172 ax-addrcl 11173 ax-mulcl 11174 ax-mulrcl 11175 ax-mulcom 11176 ax-addass 11177 ax-mulass 11178 ax-distr 11179 ax-i2m1 11180 ax-1ne0 11181 ax-1rid 11182 ax-rnegex 11183 ax-rrecex 11184 ax-cnre 11185 ax-pre-lttri 11186 ax-pre-lttrn 11187 ax-pre-ltadd 11188 ax-pre-mulgt0 11189 ax-pre-sup 11190

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2704 df-cleq 2718 df-clel 2804 df-nfc 2879 df-ne 2935 df-nel 3041 df-ral 3056 df-rex 3065 df-rmo 3370 df-reu 3371 df-rab 3427 df-v 3470 df-sbc 3773 df-csb 3889 df-dif 3946 df-un 3948 df-in 3950 df-ss 3960 df-pss 3962 df-nul 4318 df-if 4524 df-pw 4599 df-sn 4624 df-pr 4626 df-op 4630 df-uni 4903 df-iun 4992 df-br 5142 df-opab 5204 df-mpt 5225 df-tr 5259 df-id 5567 df-eprel 5573 df-po 5581 df-so 5582 df-fr 5624 df-we 5626 df-xp 5675 df-rel 5676 df-cnv 5677 df-co 5678 df-dm 5679 df-rn 5680 df-res 5681 df-ima 5682 df-pred 6294 df-ord 6361 df-on 6362 df-lim 6363 df-suc 6364 df-iota 6489 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7361 df-ov 7408 df-oprab 7409 df-mpo 7410 df-om 7853 df-2nd 7975 df-frecs 8267 df-wrecs 8298 df-recs 8372 df-rdg 8411 df-er 8705 df-en 8942 df-dom 8943 df-sdom 8944 df-sup 9439 df-pnf 11254 df-mnf 11255 df-xr 11256 df-ltxr 11257 df-le 11258 df-sub 11450 df-neg 11451 df-div 11876 df-nn 12217 df-2 12279 df-3 12280 df-4 12281 df-n0 12477 df-z 12563 df-uz 12827 df-rp 12981 df-seq 13973 df-exp 14033 df-cj 15052 df-re 15053 df-im 15054 df-sqrt 15188 df-abs 15189

This theorem is referenced by: sqsscirc2 33419

W3C validator