Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  areacirclem5 Structured version   Visualization version   GIF version

Theorem areacirclem5 34867
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.)
Hypothesis
Ref Expression
areacirc.1 𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))}
Assertion
Ref Expression
areacirclem5 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑆 “ {𝑡}) = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))
Distinct variable groups:   𝑥,𝑦,𝑡,𝑅   𝑡,𝑆
Allowed substitution hints:   𝑆(𝑥,𝑦)

Proof of Theorem areacirclem5
Dummy variable 𝑢 is distinct from all other variables.
StepHypRef Expression
1 areacirc.1 . . . 4 𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))}
21imaeq1i 5919 . . 3 (𝑆 “ {𝑡}) = ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))} “ {𝑡})
3 vex 3495 . . . 4 𝑡 ∈ V
4 imasng 5944 . . . 4 (𝑡 ∈ V → ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))} “ {𝑡}) = {𝑢𝑡{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))}𝑢})
53, 4ax-mp 5 . . 3 ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))} “ {𝑡}) = {𝑢𝑡{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))}𝑢}
6 df-br 5058 . . . . 5 (𝑡{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))}𝑢 ↔ ⟨𝑡, 𝑢⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))})
7 vex 3495 . . . . . 6 𝑢 ∈ V
8 eleq1w 2892 . . . . . . . 8 (𝑥 = 𝑡 → (𝑥 ∈ ℝ ↔ 𝑡 ∈ ℝ))
98anbi1d 629 . . . . . . 7 (𝑥 = 𝑡 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ↔ (𝑡 ∈ ℝ ∧ 𝑦 ∈ ℝ)))
10 oveq1 7152 . . . . . . . . 9 (𝑥 = 𝑡 → (𝑥↑2) = (𝑡↑2))
1110oveq1d 7160 . . . . . . . 8 (𝑥 = 𝑡 → ((𝑥↑2) + (𝑦↑2)) = ((𝑡↑2) + (𝑦↑2)))
1211breq1d 5067 . . . . . . 7 (𝑥 = 𝑡 → (((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2) ↔ ((𝑡↑2) + (𝑦↑2)) ≤ (𝑅↑2)))
139, 12anbi12d 630 . . . . . 6 (𝑥 = 𝑡 → (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2)) ↔ ((𝑡 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑡↑2) + (𝑦↑2)) ≤ (𝑅↑2))))
14 eleq1w 2892 . . . . . . . 8 (𝑦 = 𝑢 → (𝑦 ∈ ℝ ↔ 𝑢 ∈ ℝ))
1514anbi2d 628 . . . . . . 7 (𝑦 = 𝑢 → ((𝑡 ∈ ℝ ∧ 𝑦 ∈ ℝ) ↔ (𝑡 ∈ ℝ ∧ 𝑢 ∈ ℝ)))
16 oveq1 7152 . . . . . . . . 9 (𝑦 = 𝑢 → (𝑦↑2) = (𝑢↑2))
1716oveq2d 7161 . . . . . . . 8 (𝑦 = 𝑢 → ((𝑡↑2) + (𝑦↑2)) = ((𝑡↑2) + (𝑢↑2)))
1817breq1d 5067 . . . . . . 7 (𝑦 = 𝑢 → (((𝑡↑2) + (𝑦↑2)) ≤ (𝑅↑2) ↔ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)))
1915, 18anbi12d 630 . . . . . 6 (𝑦 = 𝑢 → (((𝑡 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑡↑2) + (𝑦↑2)) ≤ (𝑅↑2)) ↔ ((𝑡 ∈ ℝ ∧ 𝑢 ∈ ℝ) ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))))
203, 7, 13, 19opelopab 5420 . . . . 5 (⟨𝑡, 𝑢⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))} ↔ ((𝑡 ∈ ℝ ∧ 𝑢 ∈ ℝ) ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)))
21 anass 469 . . . . 5 (((𝑡 ∈ ℝ ∧ 𝑢 ∈ ℝ) ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)) ↔ (𝑡 ∈ ℝ ∧ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))))
226, 20, 213bitri 298 . . . 4 (𝑡{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))}𝑢 ↔ (𝑡 ∈ ℝ ∧ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))))
2322abbii 2883 . . 3 {𝑢𝑡{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))}𝑢} = {𝑢 ∣ (𝑡 ∈ ℝ ∧ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)))}
242, 5, 233eqtri 2845 . 2 (𝑆 “ {𝑡}) = {𝑢 ∣ (𝑡 ∈ ℝ ∧ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)))}
25 simp3 1130 . . . . 5 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → 𝑡 ∈ ℝ)
2625biantrurd 533 . . . 4 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)) ↔ (𝑡 ∈ ℝ ∧ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)))))
2726abbidv 2882 . . 3 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → {𝑢 ∣ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))} = {𝑢 ∣ (𝑡 ∈ ℝ ∧ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)))})
28 resqcl 13478 . . . . . . . . . . . 12 (𝑅 ∈ ℝ → (𝑅↑2) ∈ ℝ)
29283ad2ant1 1125 . . . . . . . . . . 11 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℝ)
30 resqcl 13478 . . . . . . . . . . . 12 (𝑡 ∈ ℝ → (𝑡↑2) ∈ ℝ)
31303ad2ant3 1127 . . . . . . . . . . 11 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑡↑2) ∈ ℝ)
3229, 31resubcld 11056 . . . . . . . . . 10 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((𝑅↑2) − (𝑡↑2)) ∈ ℝ)
3332adantr 481 . . . . . . . . 9 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → ((𝑅↑2) − (𝑡↑2)) ∈ ℝ)
34 absresq 14650 . . . . . . . . . . . . 13 (𝑡 ∈ ℝ → ((abs‘𝑡)↑2) = (𝑡↑2))
35343ad2ant3 1127 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((abs‘𝑡)↑2) = (𝑡↑2))
3635breq1d 5067 . . . . . . . . . . 11 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (((abs‘𝑡)↑2) ≤ (𝑅↑2) ↔ (𝑡↑2) ≤ (𝑅↑2)))
37 recn 10615 . . . . . . . . . . . . . 14 (𝑡 ∈ ℝ → 𝑡 ∈ ℂ)
3837abscld 14784 . . . . . . . . . . . . 13 (𝑡 ∈ ℝ → (abs‘𝑡) ∈ ℝ)
39383ad2ant3 1127 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (abs‘𝑡) ∈ ℝ)
40 simp1 1128 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → 𝑅 ∈ ℝ)
4137absge0d 14792 . . . . . . . . . . . . 13 (𝑡 ∈ ℝ → 0 ≤ (abs‘𝑡))
42413ad2ant3 1127 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → 0 ≤ (abs‘𝑡))
43 simp2 1129 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → 0 ≤ 𝑅)
4439, 40, 42, 43le2sqd 13608 . . . . . . . . . . 11 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ ((abs‘𝑡)↑2) ≤ (𝑅↑2)))
4529, 31subge0d 11218 . . . . . . . . . . 11 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (0 ≤ ((𝑅↑2) − (𝑡↑2)) ↔ (𝑡↑2) ≤ (𝑅↑2)))
4636, 44, 453bitr4d 312 . . . . . . . . . 10 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ 0 ≤ ((𝑅↑2) − (𝑡↑2))))
4746biimpa 477 . . . . . . . . 9 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → 0 ≤ ((𝑅↑2) − (𝑡↑2)))
4833, 47resqrtcld 14765 . . . . . . . 8 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
4948renegcld 11055 . . . . . . 7 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → -(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
5049rexrd 10679 . . . . . 6 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → -(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ*)
5148rexrd 10679 . . . . . 6 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ*)
52 iccval 12765 . . . . . 6 ((-(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ* ∧ (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ*) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) = {𝑢 ∈ ℝ* ∣ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2))))})
5350, 51, 52syl2anc 584 . . . . 5 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) = {𝑢 ∈ ℝ* ∣ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2))))})
54 iftrue 4469 . . . . . 6 ((abs‘𝑡) ≤ 𝑅 → if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅) = (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))))
5554adantl 482 . . . . 5 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅) = (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))))
56 absresq 14650 . . . . . . . . . . . 12 (𝑢 ∈ ℝ → ((abs‘𝑢)↑2) = (𝑢↑2))
5732recnd 10657 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((𝑅↑2) − (𝑡↑2)) ∈ ℂ)
5857adantr 481 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → ((𝑅↑2) − (𝑡↑2)) ∈ ℂ)
5958sqsqrtd 14787 . . . . . . . . . . . 12 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → ((√‘((𝑅↑2) − (𝑡↑2)))↑2) = ((𝑅↑2) − (𝑡↑2)))
6056, 59breqan12rd 5074 . . . . . . . . . . 11 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ 𝑢 ∈ ℝ) → (((abs‘𝑢)↑2) ≤ ((√‘((𝑅↑2) − (𝑡↑2)))↑2) ↔ (𝑢↑2) ≤ ((𝑅↑2) − (𝑡↑2))))
61 recn 10615 . . . . . . . . . . . . . 14 (𝑢 ∈ ℝ → 𝑢 ∈ ℂ)
6261abscld 14784 . . . . . . . . . . . . 13 (𝑢 ∈ ℝ → (abs‘𝑢) ∈ ℝ)
6362adantl 482 . . . . . . . . . . . 12 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ 𝑢 ∈ ℝ) → (abs‘𝑢) ∈ ℝ)
6448adantr 481 . . . . . . . . . . . 12 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ 𝑢 ∈ ℝ) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
6561absge0d 14792 . . . . . . . . . . . . 13 (𝑢 ∈ ℝ → 0 ≤ (abs‘𝑢))
6665adantl 482 . . . . . . . . . . . 12 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ 𝑢 ∈ ℝ) → 0 ≤ (abs‘𝑢))
6733, 47sqrtge0d 14768 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → 0 ≤ (√‘((𝑅↑2) − (𝑡↑2))))
6867adantr 481 . . . . . . . . . . . 12 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ 𝑢 ∈ ℝ) → 0 ≤ (√‘((𝑅↑2) − (𝑡↑2))))
6963, 64, 66, 68le2sqd 13608 . . . . . . . . . . 11 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ 𝑢 ∈ ℝ) → ((abs‘𝑢) ≤ (√‘((𝑅↑2) − (𝑡↑2))) ↔ ((abs‘𝑢)↑2) ≤ ((√‘((𝑅↑2) − (𝑡↑2)))↑2)))
7031adantr 481 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑢 ∈ ℝ) → (𝑡↑2) ∈ ℝ)
71 resqcl 13478 . . . . . . . . . . . . . 14 (𝑢 ∈ ℝ → (𝑢↑2) ∈ ℝ)
7271adantl 482 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑢 ∈ ℝ) → (𝑢↑2) ∈ ℝ)
7329adantr 481 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑢 ∈ ℝ) → (𝑅↑2) ∈ ℝ)
7470, 72, 73leaddsub2d 11230 . . . . . . . . . . . 12 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑢 ∈ ℝ) → (((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2) ↔ (𝑢↑2) ≤ ((𝑅↑2) − (𝑡↑2))))
7574adantlr 711 . . . . . . . . . . 11 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ 𝑢 ∈ ℝ) → (((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2) ↔ (𝑢↑2) ≤ ((𝑅↑2) − (𝑡↑2))))
7660, 69, 753bitr4rd 313 . . . . . . . . . 10 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ 𝑢 ∈ ℝ) → (((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2) ↔ (abs‘𝑢) ≤ (√‘((𝑅↑2) − (𝑡↑2)))))
77 simpr 485 . . . . . . . . . . 11 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ 𝑢 ∈ ℝ) → 𝑢 ∈ ℝ)
7877, 64absled 14778 . . . . . . . . . 10 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ 𝑢 ∈ ℝ) → ((abs‘𝑢) ≤ (√‘((𝑅↑2) − (𝑡↑2))) ↔ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2))))))
79 rexr 10675 . . . . . . . . . . . 12 (𝑢 ∈ ℝ → 𝑢 ∈ ℝ*)
8079adantl 482 . . . . . . . . . . 11 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ 𝑢 ∈ ℝ) → 𝑢 ∈ ℝ*)
8180biantrurd 533 . . . . . . . . . 10 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ 𝑢 ∈ ℝ) → ((-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))) ↔ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))))
8276, 78, 813bitrd 306 . . . . . . . . 9 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ 𝑢 ∈ ℝ) → (((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2) ↔ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))))
8382pm5.32da 579 . . . . . . . 8 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → ((𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)) ↔ (𝑢 ∈ ℝ ∧ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2))))))))
84 simprl 767 . . . . . . . . . . 11 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))) → 𝑢 ∈ ℝ*)
8548adantr 481 . . . . . . . . . . 11 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
86 mnfxr 10686 . . . . . . . . . . . . 13 -∞ ∈ ℝ*
8786a1i 11 . . . . . . . . . . . 12 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))) → -∞ ∈ ℝ*)
8849adantr 481 . . . . . . . . . . . . 13 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))) → -(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
8988rexrd 10679 . . . . . . . . . . . 12 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))) → -(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ*)
9049mnfltd 12507 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → -∞ < -(√‘((𝑅↑2) − (𝑡↑2))))
9190adantr 481 . . . . . . . . . . . 12 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))) → -∞ < -(√‘((𝑅↑2) − (𝑡↑2))))
92 simprrl 777 . . . . . . . . . . . 12 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))) → -(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢)
9387, 89, 84, 91, 92xrltletrd 12542 . . . . . . . . . . 11 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))) → -∞ < 𝑢)
94 simprrr 778 . . . . . . . . . . 11 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))) → 𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2))))
95 xrre 12550 . . . . . . . . . . 11 (((𝑢 ∈ ℝ* ∧ (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ) ∧ (-∞ < 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2))))) → 𝑢 ∈ ℝ)
9684, 85, 93, 94, 95syl22anc 834 . . . . . . . . . 10 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))) → 𝑢 ∈ ℝ)
9796ex 413 . . . . . . . . 9 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → ((𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2))))) → 𝑢 ∈ ℝ))
9897pm4.71rd 563 . . . . . . . 8 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → ((𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2))))) ↔ (𝑢 ∈ ℝ ∧ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2))))))))
9983, 98bitr4d 283 . . . . . . 7 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → ((𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)) ↔ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))))
10099abbidv 2882 . . . . . 6 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → {𝑢 ∣ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))} = {𝑢 ∣ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))})
101 df-rab 3144 . . . . . 6 {𝑢 ∈ ℝ* ∣ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2))))} = {𝑢 ∣ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))}
102100, 101syl6eqr 2871 . . . . 5 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → {𝑢 ∣ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))} = {𝑢 ∈ ℝ* ∣ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2))))})
10353, 55, 1023eqtr4rd 2864 . . . 4 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → {𝑢 ∣ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))} = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))
10440, 39ltnled 10775 . . . . . . . 8 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑅 < (abs‘𝑡) ↔ ¬ (abs‘𝑡) ≤ 𝑅))
105104biimprd 249 . . . . . . 7 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (¬ (abs‘𝑡) ≤ 𝑅𝑅 < (abs‘𝑡)))
106105imdistani 569 . . . . . 6 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ ¬ (abs‘𝑡) ≤ 𝑅) → ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡)))
107 df-rab 3144 . . . . . . 7 {𝑢 ∈ ℝ ∣ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)} = {𝑢 ∣ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))}
108293ad2ant1 1125 . . . . . . . . . . . 12 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡) ∧ 𝑢 ∈ ℝ) → (𝑅↑2) ∈ ℝ)
109313ad2ant1 1125 . . . . . . . . . . . 12 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡) ∧ 𝑢 ∈ ℝ) → (𝑡↑2) ∈ ℝ)
110713ad2ant3 1127 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡) ∧ 𝑢 ∈ ℝ) → (𝑢↑2) ∈ ℝ)
111109, 110readdcld 10658 . . . . . . . . . . . 12 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡) ∧ 𝑢 ∈ ℝ) → ((𝑡↑2) + (𝑢↑2)) ∈ ℝ)
11240, 39, 43, 42lt2sqd 13607 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑅 < (abs‘𝑡) ↔ (𝑅↑2) < ((abs‘𝑡)↑2)))
11335breq2d 5069 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((𝑅↑2) < ((abs‘𝑡)↑2) ↔ (𝑅↑2) < (𝑡↑2)))
114112, 113bitrd 280 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑅 < (abs‘𝑡) ↔ (𝑅↑2) < (𝑡↑2)))
115114biimpa 477 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡)) → (𝑅↑2) < (𝑡↑2))
1161153adant3 1124 . . . . . . . . . . . 12 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡) ∧ 𝑢 ∈ ℝ) → (𝑅↑2) < (𝑡↑2))
117 sqge0 13489 . . . . . . . . . . . . . 14 (𝑢 ∈ ℝ → 0 ≤ (𝑢↑2))
1181173ad2ant3 1127 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡) ∧ 𝑢 ∈ ℝ) → 0 ≤ (𝑢↑2))
119109, 110addge01d 11216 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡) ∧ 𝑢 ∈ ℝ) → (0 ≤ (𝑢↑2) ↔ (𝑡↑2) ≤ ((𝑡↑2) + (𝑢↑2))))
120118, 119mpbid 233 . . . . . . . . . . . 12 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡) ∧ 𝑢 ∈ ℝ) → (𝑡↑2) ≤ ((𝑡↑2) + (𝑢↑2)))
121108, 109, 111, 116, 120ltletrd 10788 . . . . . . . . . . 11 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡) ∧ 𝑢 ∈ ℝ) → (𝑅↑2) < ((𝑡↑2) + (𝑢↑2)))
122108, 111ltnled 10775 . . . . . . . . . . 11 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡) ∧ 𝑢 ∈ ℝ) → ((𝑅↑2) < ((𝑡↑2) + (𝑢↑2)) ↔ ¬ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)))
123121, 122mpbid 233 . . . . . . . . . 10 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡) ∧ 𝑢 ∈ ℝ) → ¬ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))
1241233expa 1110 . . . . . . . . 9 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡)) ∧ 𝑢 ∈ ℝ) → ¬ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))
125124ralrimiva 3179 . . . . . . . 8 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡)) → ∀𝑢 ∈ ℝ ¬ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))
126 rabeq0 4335 . . . . . . . 8 ({𝑢 ∈ ℝ ∣ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)} = ∅ ↔ ∀𝑢 ∈ ℝ ¬ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))
127125, 126sylibr 235 . . . . . . 7 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡)) → {𝑢 ∈ ℝ ∣ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)} = ∅)
128107, 127syl5eqr 2867 . . . . . 6 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡)) → {𝑢 ∣ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))} = ∅)
129106, 128syl 17 . . . . 5 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ ¬ (abs‘𝑡) ≤ 𝑅) → {𝑢 ∣ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))} = ∅)
130 iffalse 4472 . . . . . 6 (¬ (abs‘𝑡) ≤ 𝑅 → if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅) = ∅)
131130adantl 482 . . . . 5 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ ¬ (abs‘𝑡) ≤ 𝑅) → if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅) = ∅)
132129, 131eqtr4d 2856 . . . 4 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ ¬ (abs‘𝑡) ≤ 𝑅) → {𝑢 ∣ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))} = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))
133103, 132pm2.61dan 809 . . 3 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → {𝑢 ∣ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))} = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))
13427, 133eqtr3d 2855 . 2 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → {𝑢 ∣ (𝑡 ∈ ℝ ∧ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)))} = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))
13524, 134syl5eq 2865 1 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑆 “ {𝑡}) = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  w3a 1079   = wceq 1528  wcel 2105  {cab 2796  wral 3135  {crab 3139  Vcvv 3492  c0 4288  ifcif 4463  {csn 4557  cop 4563   class class class wbr 5057  {copab 5119  cima 5551  cfv 6348  (class class class)co 7145  cc 10523  cr 10524  0cc0 10525   + caddc 10528  -∞cmnf 10661  *cxr 10662   < clt 10663  cle 10664  cmin 10858  -cneg 10859  2c2 11680  [,]cicc 12729  cexp 13417  csqrt 14580  abscabs 14581
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-cnex 10581  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601  ax-pre-mulgt0 10602  ax-pre-sup 10603
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7570  df-2nd 7679  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-er 8278  df-en 8498  df-dom 8499  df-sdom 8500  df-sup 8894  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-sub 10860  df-neg 10861  df-div 11286  df-nn 11627  df-2 11688  df-3 11689  df-n0 11886  df-z 11970  df-uz 12232  df-rp 12378  df-icc 12733  df-seq 13358  df-exp 13418  df-cj 14446  df-re 14447  df-im 14448  df-sqrt 14582  df-abs 14583
This theorem is referenced by:  areacirc  34868
  Copyright terms: Public domain W3C validator