areacirclem5

Description: Finding the cross-section of a circle. (Contributed by Brendan Leahy, 31-Aug-2017) (Revised by Brendan Leahy, 22-Sep-2017) (Revised by Brendan Leahy, 11-Jul-2018)

		Ref	Expression
	Hypothesis	areacirc.1	⊢ 𝑆 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) }
	Assertion	areacirclem5	⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( 𝑆 “ { 𝑡 } ) = if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		areacirc.1	⊢ 𝑆 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) }
2	1	imaeq1i	⊢ ( 𝑆 “ { 𝑡 } ) = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) } “ { 𝑡 } )
3		vex	⊢ 𝑡 ∈ V
4		imasng	⊢ ( 𝑡 ∈ V → ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) } “ { 𝑡 } ) = { 𝑢 ∣ 𝑡 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) } 𝑢 } )
5	3 4	ax-mp	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) } “ { 𝑡 } ) = { 𝑢 ∣ 𝑡 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) } 𝑢 }
6		df-br	⊢ ( 𝑡 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) } 𝑢 ↔ ⟨ 𝑡 , 𝑢 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) } )
7		vex	⊢ 𝑢 ∈ V
8		eleq1w	⊢ ( 𝑥 = 𝑡 → ( 𝑥 ∈ ℝ ↔ 𝑡 ∈ ℝ ) )
9	8	anbi1d	⊢ ( 𝑥 = 𝑡 → ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ↔ ( 𝑡 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) )
10		oveq1	⊢ ( 𝑥 = 𝑡 → ( 𝑥 ↑ 2 ) = ( 𝑡 ↑ 2 ) )
11	10	oveq1d	⊢ ( 𝑥 = 𝑡 → ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( ( 𝑡 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )
12	11	breq1d	⊢ ( 𝑥 = 𝑡 → ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ↔ ( ( 𝑡 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) )
13	9 12	anbi12d	⊢ ( 𝑥 = 𝑡 → ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) ↔ ( ( 𝑡 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( ( 𝑡 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) ) )
14		eleq1w	⊢ ( 𝑦 = 𝑢 → ( 𝑦 ∈ ℝ ↔ 𝑢 ∈ ℝ ) )
15	14	anbi2d	⊢ ( 𝑦 = 𝑢 → ( ( 𝑡 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ↔ ( 𝑡 ∈ ℝ ∧ 𝑢 ∈ ℝ ) ) )
16		oveq1	⊢ ( 𝑦 = 𝑢 → ( 𝑦 ↑ 2 ) = ( 𝑢 ↑ 2 ) )
17	16	oveq2d	⊢ ( 𝑦 = 𝑢 → ( ( 𝑡 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( ( 𝑡 ↑ 2 ) + ( 𝑢 ↑ 2 ) ) )
18	17	breq1d	⊢ ( 𝑦 = 𝑢 → ( ( ( 𝑡 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ↔ ( ( 𝑡 ↑ 2 ) + ( 𝑢 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) )
19	15 18	anbi12d	⊢ ( 𝑦 = 𝑢 → ( ( ( 𝑡 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( ( 𝑡 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) ↔ ( ( 𝑡 ∈ ℝ ∧ 𝑢 ∈ ℝ ) ∧ ( ( 𝑡 ↑ 2 ) + ( 𝑢 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) ) )
20	3 7 13 19	opelopab	⊢ ( ⟨ 𝑡 , 𝑢 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) } ↔ ( ( 𝑡 ∈ ℝ ∧ 𝑢 ∈ ℝ ) ∧ ( ( 𝑡 ↑ 2 ) + ( 𝑢 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) )
21		anass	⊢ ( ( ( 𝑡 ∈ ℝ ∧ 𝑢 ∈ ℝ ) ∧ ( ( 𝑡 ↑ 2 ) + ( 𝑢 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) ↔ ( 𝑡 ∈ ℝ ∧ ( 𝑢 ∈ ℝ ∧ ( ( 𝑡 ↑ 2 ) + ( 𝑢 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) ) )
22	6 20 21	3bitri	⊢ ( 𝑡 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) } 𝑢 ↔ ( 𝑡 ∈ ℝ ∧ ( 𝑢 ∈ ℝ ∧ ( ( 𝑡 ↑ 2 ) + ( 𝑢 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) ) )
23	22	abbii	⊢ { 𝑢 ∣ 𝑡 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) } 𝑢 } = { 𝑢 ∣ ( 𝑡 ∈ ℝ ∧ ( 𝑢 ∈ ℝ ∧ ( ( 𝑡 ↑ 2 ) + ( 𝑢 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) ) }
24	2 5 23	3eqtri	⊢ ( 𝑆 “ { 𝑡 } ) = { 𝑢 ∣ ( 𝑡 ∈ ℝ ∧ ( 𝑢 ∈ ℝ ∧ ( ( 𝑡 ↑ 2 ) + ( 𝑢 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) ) }
25		simp3	⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → 𝑡 ∈ ℝ )
26	25	biantrurd	⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( ( 𝑢 ∈ ℝ ∧ ( ( 𝑡 ↑ 2 ) + ( 𝑢 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) ↔ ( 𝑡 ∈ ℝ ∧ ( 𝑢 ∈ ℝ ∧ ( ( 𝑡 ↑ 2 ) + ( 𝑢 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) ) ) )
27	26	abbidv	⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → { 𝑢 ∣ ( 𝑢 ∈ ℝ ∧ ( ( 𝑡 ↑ 2 ) + ( 𝑢 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) } = { 𝑢 ∣ ( 𝑡 ∈ ℝ ∧ ( 𝑢 ∈ ℝ ∧ ( ( 𝑡 ↑ 2 ) + ( 𝑢 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) ) } )
28		resqcl	⊢ ( 𝑅 ∈ ℝ → ( 𝑅 ↑ 2 ) ∈ ℝ )
29	28	3ad2ant1	⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( 𝑅 ↑ 2 ) ∈ ℝ )
30		resqcl	⊢ ( 𝑡 ∈ ℝ → ( 𝑡 ↑ 2 ) ∈ ℝ )
31	30	3ad2ant3	⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( 𝑡 ↑ 2 ) ∈ ℝ )
32	29 31	resubcld	⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ∈ ℝ )
33	32	adantr	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ∈ ℝ )
34		absresq	⊢ ( 𝑡 ∈ ℝ → ( ( abs ‘ 𝑡 ) ↑ 2 ) = ( 𝑡 ↑ 2 ) )
35	34	3ad2ant3	⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( ( abs ‘ 𝑡 ) ↑ 2 ) = ( 𝑡 ↑ 2 ) )
36	35	breq1d	⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( ( ( abs ‘ 𝑡 ) ↑ 2 ) ≤ ( 𝑅 ↑ 2 ) ↔ ( 𝑡 ↑ 2 ) ≤ ( 𝑅 ↑ 2 ) ) )
37		recn	⊢ ( 𝑡 ∈ ℝ → 𝑡 ∈ ℂ )
38	37	abscld	⊢ ( 𝑡 ∈ ℝ → ( abs ‘ 𝑡 ) ∈ ℝ )
39	38	3ad2ant3	⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( abs ‘ 𝑡 ) ∈ ℝ )
40		simp1	⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → 𝑅 ∈ ℝ )
41	37	absge0d	⊢ ( 𝑡 ∈ ℝ → 0 ≤ ( abs ‘ 𝑡 ) )
42	41	3ad2ant3	⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → 0 ≤ ( abs ‘ 𝑡 ) )
43		simp2	⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → 0 ≤ 𝑅 )
44	39 40 42 43	le2sqd	⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( ( abs ‘ 𝑡 ) ≤ 𝑅 ↔ ( ( abs ‘ 𝑡 ) ↑ 2 ) ≤ ( 𝑅 ↑ 2 ) ) )
45	29 31	subge0d	⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( 0 ≤ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ↔ ( 𝑡 ↑ 2 ) ≤ ( 𝑅 ↑ 2 ) ) )
46	36 44 45	3bitr4d	⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( ( abs ‘ 𝑡 ) ≤ 𝑅 ↔ 0 ≤ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) )
47	46	biimpa	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → 0 ≤ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) )
48	33 47	resqrtcld	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ∈ ℝ )
49	48	renegcld	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ∈ ℝ )
50	49	rexrd	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ∈ ℝ^* )
51	48	rexrd	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ∈ ℝ^* )
52		iccval	⊢ ( ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ∈ ℝ^* ∧ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ∈ ℝ^* ) → ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) = { 𝑢 ∈ ℝ^* ∣ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ≤ 𝑢 ∧ 𝑢 ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) } )
53	50 51 52	syl2anc	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) = { 𝑢 ∈ ℝ^* ∣ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ≤ 𝑢 ∧ 𝑢 ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) } )
54		iftrue	⊢ ( ( abs ‘ 𝑡 ) ≤ 𝑅 → if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) = ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) )
55	54	adantl	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) = ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) )
56		absresq	⊢ ( 𝑢 ∈ ℝ → ( ( abs ‘ 𝑢 ) ↑ 2 ) = ( 𝑢 ↑ 2 ) )
57	32	recnd	⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ∈ ℂ )
58	57	adantr	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ∈ ℂ )
59	58	sqsqrtd	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → ( ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ↑ 2 ) = ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) )
60	56 59	breqan12rd	⊢ ( ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) ∧ 𝑢 ∈ ℝ ) → ( ( ( abs ‘ 𝑢 ) ↑ 2 ) ≤ ( ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ↑ 2 ) ↔ ( 𝑢 ↑ 2 ) ≤ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) )
61		recn	⊢ ( 𝑢 ∈ ℝ → 𝑢 ∈ ℂ )
62	61	abscld	⊢ ( 𝑢 ∈ ℝ → ( abs ‘ 𝑢 ) ∈ ℝ )
63	62	adantl	⊢ ( ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) ∧ 𝑢 ∈ ℝ ) → ( abs ‘ 𝑢 ) ∈ ℝ )
64	48	adantr	⊢ ( ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) ∧ 𝑢 ∈ ℝ ) → ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ∈ ℝ )
65	61	absge0d	⊢ ( 𝑢 ∈ ℝ → 0 ≤ ( abs ‘ 𝑢 ) )
66	65	adantl	⊢ ( ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) ∧ 𝑢 ∈ ℝ ) → 0 ≤ ( abs ‘ 𝑢 ) )
67	33 47	sqrtge0d	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → 0 ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) )
68	67	adantr	⊢ ( ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) ∧ 𝑢 ∈ ℝ ) → 0 ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) )
69	63 64 66 68	le2sqd	⊢ ( ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) ∧ 𝑢 ∈ ℝ ) → ( ( abs ‘ 𝑢 ) ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ↔ ( ( abs ‘ 𝑢 ) ↑ 2 ) ≤ ( ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ↑ 2 ) ) )
70	31	adantr	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ 𝑢 ∈ ℝ ) → ( 𝑡 ↑ 2 ) ∈ ℝ )
71		resqcl	⊢ ( 𝑢 ∈ ℝ → ( 𝑢 ↑ 2 ) ∈ ℝ )
72	71	adantl	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ 𝑢 ∈ ℝ ) → ( 𝑢 ↑ 2 ) ∈ ℝ )
73	29	adantr	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ 𝑢 ∈ ℝ ) → ( 𝑅 ↑ 2 ) ∈ ℝ )
74	70 72 73	leaddsub2d	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ 𝑢 ∈ ℝ ) → ( ( ( 𝑡 ↑ 2 ) + ( 𝑢 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ↔ ( 𝑢 ↑ 2 ) ≤ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) )
75	74	adantlr	⊢ ( ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) ∧ 𝑢 ∈ ℝ ) → ( ( ( 𝑡 ↑ 2 ) + ( 𝑢 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ↔ ( 𝑢 ↑ 2 ) ≤ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) )
76	60 69 75	3bitr4rd	⊢ ( ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) ∧ 𝑢 ∈ ℝ ) → ( ( ( 𝑡 ↑ 2 ) + ( 𝑢 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ↔ ( abs ‘ 𝑢 ) ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) )
77		simpr	⊢ ( ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) ∧ 𝑢 ∈ ℝ ) → 𝑢 ∈ ℝ )
78	77 64	absled	⊢ ( ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) ∧ 𝑢 ∈ ℝ ) → ( ( abs ‘ 𝑢 ) ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ↔ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ≤ 𝑢 ∧ 𝑢 ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) )
79		rexr	⊢ ( 𝑢 ∈ ℝ → 𝑢 ∈ ℝ^* )
80	79	adantl	⊢ ( ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) ∧ 𝑢 ∈ ℝ ) → 𝑢 ∈ ℝ^* )
81	80	biantrurd	⊢ ( ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) ∧ 𝑢 ∈ ℝ ) → ( ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ≤ 𝑢 ∧ 𝑢 ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ↔ ( 𝑢 ∈ ℝ^* ∧ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ≤ 𝑢 ∧ 𝑢 ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) ) )
82	76 78 81	3bitrd	⊢ ( ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) ∧ 𝑢 ∈ ℝ ) → ( ( ( 𝑡 ↑ 2 ) + ( 𝑢 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ↔ ( 𝑢 ∈ ℝ^* ∧ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ≤ 𝑢 ∧ 𝑢 ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) ) )
83	82	pm5.32da	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → ( ( 𝑢 ∈ ℝ ∧ ( ( 𝑡 ↑ 2 ) + ( 𝑢 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) ↔ ( 𝑢 ∈ ℝ ∧ ( 𝑢 ∈ ℝ^* ∧ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ≤ 𝑢 ∧ 𝑢 ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) ) ) )
84		simprl	⊢ ( ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) ∧ ( 𝑢 ∈ ℝ^* ∧ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ≤ 𝑢 ∧ 𝑢 ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) ) → 𝑢 ∈ ℝ^* )
85	48	adantr	⊢ ( ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) ∧ ( 𝑢 ∈ ℝ^* ∧ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ≤ 𝑢 ∧ 𝑢 ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) ) → ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ∈ ℝ )
86		mnfxr	⊢ -∞ ∈ ℝ^*
87	86	a1i	⊢ ( ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) ∧ ( 𝑢 ∈ ℝ^* ∧ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ≤ 𝑢 ∧ 𝑢 ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) ) → -∞ ∈ ℝ^* )
88	49	adantr	⊢ ( ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) ∧ ( 𝑢 ∈ ℝ^* ∧ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ≤ 𝑢 ∧ 𝑢 ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) ) → - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ∈ ℝ )
89	88	rexrd	⊢ ( ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) ∧ ( 𝑢 ∈ ℝ^* ∧ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ≤ 𝑢 ∧ 𝑢 ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) ) → - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ∈ ℝ^* )
90	49	mnfltd	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → -∞ < - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) )
91	90	adantr	⊢ ( ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) ∧ ( 𝑢 ∈ ℝ^* ∧ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ≤ 𝑢 ∧ 𝑢 ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) ) → -∞ < - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) )
92		simprrl	⊢ ( ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) ∧ ( 𝑢 ∈ ℝ^* ∧ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ≤ 𝑢 ∧ 𝑢 ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) ) → - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ≤ 𝑢 )
93	87 89 84 91 92	xrltletrd	⊢ ( ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) ∧ ( 𝑢 ∈ ℝ^* ∧ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ≤ 𝑢 ∧ 𝑢 ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) ) → -∞ < 𝑢 )
94		simprrr	⊢ ( ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) ∧ ( 𝑢 ∈ ℝ^* ∧ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ≤ 𝑢 ∧ 𝑢 ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) ) → 𝑢 ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) )
95		xrre	⊢ ( ( ( 𝑢 ∈ ℝ^* ∧ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ∈ ℝ ) ∧ ( -∞ < 𝑢 ∧ 𝑢 ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) → 𝑢 ∈ ℝ )
96	84 85 93 94 95	syl22anc	⊢ ( ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) ∧ ( 𝑢 ∈ ℝ^* ∧ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ≤ 𝑢 ∧ 𝑢 ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) ) → 𝑢 ∈ ℝ )
97	96	ex	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → ( ( 𝑢 ∈ ℝ^* ∧ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ≤ 𝑢 ∧ 𝑢 ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) → 𝑢 ∈ ℝ ) )
98	97	pm4.71rd	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → ( ( 𝑢 ∈ ℝ^* ∧ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ≤ 𝑢 ∧ 𝑢 ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) ↔ ( 𝑢 ∈ ℝ ∧ ( 𝑢 ∈ ℝ^* ∧ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ≤ 𝑢 ∧ 𝑢 ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) ) ) )
99	83 98	bitr4d	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → ( ( 𝑢 ∈ ℝ ∧ ( ( 𝑡 ↑ 2 ) + ( 𝑢 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) ↔ ( 𝑢 ∈ ℝ^* ∧ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ≤ 𝑢 ∧ 𝑢 ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) ) )
100	99	abbidv	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → { 𝑢 ∣ ( 𝑢 ∈ ℝ ∧ ( ( 𝑡 ↑ 2 ) + ( 𝑢 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) } = { 𝑢 ∣ ( 𝑢 ∈ ℝ^* ∧ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ≤ 𝑢 ∧ 𝑢 ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) } )
101		df-rab	⊢ { 𝑢 ∈ ℝ^* ∣ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ≤ 𝑢 ∧ 𝑢 ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) } = { 𝑢 ∣ ( 𝑢 ∈ ℝ^* ∧ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ≤ 𝑢 ∧ 𝑢 ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) ) }
102	100 101	eqtr4di	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → { 𝑢 ∣ ( 𝑢 ∈ ℝ ∧ ( ( 𝑡 ↑ 2 ) + ( 𝑢 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) } = { 𝑢 ∈ ℝ^* ∣ ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ≤ 𝑢 ∧ 𝑢 ≤ ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) } )
103	53 55 102	3eqtr4rd	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → { 𝑢 ∣ ( 𝑢 ∈ ℝ ∧ ( ( 𝑡 ↑ 2 ) + ( 𝑢 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) } = if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) )
104	40 39	ltnled	⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( 𝑅 < ( abs ‘ 𝑡 ) ↔ ¬ ( abs ‘ 𝑡 ) ≤ 𝑅 ) )
105	104	biimprd	⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( ¬ ( abs ‘ 𝑡 ) ≤ 𝑅 → 𝑅 < ( abs ‘ 𝑡 ) ) )
106	105	imdistani	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ¬ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ 𝑅 < ( abs ‘ 𝑡 ) ) )
107		df-rab	⊢ { 𝑢 ∈ ℝ ∣ ( ( 𝑡 ↑ 2 ) + ( 𝑢 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) } = { 𝑢 ∣ ( 𝑢 ∈ ℝ ∧ ( ( 𝑡 ↑ 2 ) + ( 𝑢 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) }
108	29	3ad2ant1	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ 𝑅 < ( abs ‘ 𝑡 ) ∧ 𝑢 ∈ ℝ ) → ( 𝑅 ↑ 2 ) ∈ ℝ )
109	31	3ad2ant1	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ 𝑅 < ( abs ‘ 𝑡 ) ∧ 𝑢 ∈ ℝ ) → ( 𝑡 ↑ 2 ) ∈ ℝ )
110	71	3ad2ant3	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ 𝑅 < ( abs ‘ 𝑡 ) ∧ 𝑢 ∈ ℝ ) → ( 𝑢 ↑ 2 ) ∈ ℝ )
111	109 110	readdcld	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ 𝑅 < ( abs ‘ 𝑡 ) ∧ 𝑢 ∈ ℝ ) → ( ( 𝑡 ↑ 2 ) + ( 𝑢 ↑ 2 ) ) ∈ ℝ )
112	40 39 43 42	lt2sqd	⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( 𝑅 < ( abs ‘ 𝑡 ) ↔ ( 𝑅 ↑ 2 ) < ( ( abs ‘ 𝑡 ) ↑ 2 ) ) )
113	35	breq2d	⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( ( 𝑅 ↑ 2 ) < ( ( abs ‘ 𝑡 ) ↑ 2 ) ↔ ( 𝑅 ↑ 2 ) < ( 𝑡 ↑ 2 ) ) )
114	112 113	bitrd	⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( 𝑅 < ( abs ‘ 𝑡 ) ↔ ( 𝑅 ↑ 2 ) < ( 𝑡 ↑ 2 ) ) )
115	114	biimpa	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ 𝑅 < ( abs ‘ 𝑡 ) ) → ( 𝑅 ↑ 2 ) < ( 𝑡 ↑ 2 ) )
116	115	3adant3	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ 𝑅 < ( abs ‘ 𝑡 ) ∧ 𝑢 ∈ ℝ ) → ( 𝑅 ↑ 2 ) < ( 𝑡 ↑ 2 ) )
117		sqge0	⊢ ( 𝑢 ∈ ℝ → 0 ≤ ( 𝑢 ↑ 2 ) )
118	117	3ad2ant3	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ 𝑅 < ( abs ‘ 𝑡 ) ∧ 𝑢 ∈ ℝ ) → 0 ≤ ( 𝑢 ↑ 2 ) )
119	109 110	addge01d	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ 𝑅 < ( abs ‘ 𝑡 ) ∧ 𝑢 ∈ ℝ ) → ( 0 ≤ ( 𝑢 ↑ 2 ) ↔ ( 𝑡 ↑ 2 ) ≤ ( ( 𝑡 ↑ 2 ) + ( 𝑢 ↑ 2 ) ) ) )
120	118 119	mpbid	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ 𝑅 < ( abs ‘ 𝑡 ) ∧ 𝑢 ∈ ℝ ) → ( 𝑡 ↑ 2 ) ≤ ( ( 𝑡 ↑ 2 ) + ( 𝑢 ↑ 2 ) ) )
121	108 109 111 116 120	ltletrd	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ 𝑅 < ( abs ‘ 𝑡 ) ∧ 𝑢 ∈ ℝ ) → ( 𝑅 ↑ 2 ) < ( ( 𝑡 ↑ 2 ) + ( 𝑢 ↑ 2 ) ) )
122	108 111	ltnled	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ 𝑅 < ( abs ‘ 𝑡 ) ∧ 𝑢 ∈ ℝ ) → ( ( 𝑅 ↑ 2 ) < ( ( 𝑡 ↑ 2 ) + ( 𝑢 ↑ 2 ) ) ↔ ¬ ( ( 𝑡 ↑ 2 ) + ( 𝑢 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) )
123	121 122	mpbid	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ 𝑅 < ( abs ‘ 𝑡 ) ∧ 𝑢 ∈ ℝ ) → ¬ ( ( 𝑡 ↑ 2 ) + ( 𝑢 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) )
124	123	3expa	⊢ ( ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ 𝑅 < ( abs ‘ 𝑡 ) ) ∧ 𝑢 ∈ ℝ ) → ¬ ( ( 𝑡 ↑ 2 ) + ( 𝑢 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) )
125	124	ralrimiva	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ 𝑅 < ( abs ‘ 𝑡 ) ) → ∀ 𝑢 ∈ ℝ ¬ ( ( 𝑡 ↑ 2 ) + ( 𝑢 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) )
126		rabeq0	⊢ ( { 𝑢 ∈ ℝ ∣ ( ( 𝑡 ↑ 2 ) + ( 𝑢 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) } = ∅ ↔ ∀ 𝑢 ∈ ℝ ¬ ( ( 𝑡 ↑ 2 ) + ( 𝑢 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) )
127	125 126	sylibr	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ 𝑅 < ( abs ‘ 𝑡 ) ) → { 𝑢 ∈ ℝ ∣ ( ( 𝑡 ↑ 2 ) + ( 𝑢 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) } = ∅ )
128	107 127	syl5eqr	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ 𝑅 < ( abs ‘ 𝑡 ) ) → { 𝑢 ∣ ( 𝑢 ∈ ℝ ∧ ( ( 𝑡 ↑ 2 ) + ( 𝑢 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) } = ∅ )
129	106 128	syl	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ¬ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → { 𝑢 ∣ ( 𝑢 ∈ ℝ ∧ ( ( 𝑡 ↑ 2 ) + ( 𝑢 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) } = ∅ )
130		iffalse	⊢ ( ¬ ( abs ‘ 𝑡 ) ≤ 𝑅 → if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) = ∅ )
131	130	adantl	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ¬ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) = ∅ )
132	129 131	eqtr4d	⊢ ( ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) ∧ ¬ ( abs ‘ 𝑡 ) ≤ 𝑅 ) → { 𝑢 ∣ ( 𝑢 ∈ ℝ ∧ ( ( 𝑡 ↑ 2 ) + ( 𝑢 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) } = if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) )
133	103 132	pm2.61dan	⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → { 𝑢 ∣ ( 𝑢 ∈ ℝ ∧ ( ( 𝑡 ↑ 2 ) + ( 𝑢 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) } = if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) )
134	27 133	eqtr3d	⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → { 𝑢 ∣ ( 𝑡 ∈ ℝ ∧ ( 𝑢 ∈ ℝ ∧ ( ( 𝑡 ↑ 2 ) + ( 𝑢 ↑ 2 ) ) ≤ ( 𝑅 ↑ 2 ) ) ) } = if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) )
135	24 134	syl5eq	⊢ ( ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ∧ 𝑡 ∈ ℝ ) → ( 𝑆 “ { 𝑡 } ) = if ( ( abs ‘ 𝑡 ) ≤ 𝑅 , ( - ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) [,] ( √ ‘ ( ( 𝑅 ↑ 2 ) − ( 𝑡 ↑ 2 ) ) ) ) , ∅ ) )

Metamath Proof Explorer

Theorem areacirclem5

Proof