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 33835
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 5603 . . 3 (𝑆 “ {𝑡}) = ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))} “ {𝑡})
3 vex 3354 . . . 4 𝑡 ∈ V
4 imasng 5627 . . . 4 (𝑡 ∈ V → ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))} “ {𝑡}) = {𝑢𝑡{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))}𝑢})
53, 4ax-mp 5 . . 3 ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))} “ {𝑡}) = {𝑢𝑡{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))}𝑢}
6 df-br 4788 . . . . 5 (𝑡{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))}𝑢 ↔ ⟨𝑡, 𝑢⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))})
7 vex 3354 . . . . . 6 𝑢 ∈ V
8 eleq1w 2833 . . . . . . . 8 (𝑥 = 𝑡 → (𝑥 ∈ ℝ ↔ 𝑡 ∈ ℝ))
98anbi1d 615 . . . . . . 7 (𝑥 = 𝑡 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ↔ (𝑡 ∈ ℝ ∧ 𝑦 ∈ ℝ)))
10 oveq1 6802 . . . . . . . . 9 (𝑥 = 𝑡 → (𝑥↑2) = (𝑡↑2))
1110oveq1d 6810 . . . . . . . 8 (𝑥 = 𝑡 → ((𝑥↑2) + (𝑦↑2)) = ((𝑡↑2) + (𝑦↑2)))
1211breq1d 4797 . . . . . . 7 (𝑥 = 𝑡 → (((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2) ↔ ((𝑡↑2) + (𝑦↑2)) ≤ (𝑅↑2)))
139, 12anbi12d 616 . . . . . 6 (𝑥 = 𝑡 → (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2)) ↔ ((𝑡 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑡↑2) + (𝑦↑2)) ≤ (𝑅↑2))))
14 eleq1w 2833 . . . . . . . 8 (𝑦 = 𝑢 → (𝑦 ∈ ℝ ↔ 𝑢 ∈ ℝ))
1514anbi2d 614 . . . . . . 7 (𝑦 = 𝑢 → ((𝑡 ∈ ℝ ∧ 𝑦 ∈ ℝ) ↔ (𝑡 ∈ ℝ ∧ 𝑢 ∈ ℝ)))
16 oveq1 6802 . . . . . . . . 9 (𝑦 = 𝑢 → (𝑦↑2) = (𝑢↑2))
1716oveq2d 6811 . . . . . . . 8 (𝑦 = 𝑢 → ((𝑡↑2) + (𝑦↑2)) = ((𝑡↑2) + (𝑢↑2)))
1817breq1d 4797 . . . . . . 7 (𝑦 = 𝑢 → (((𝑡↑2) + (𝑦↑2)) ≤ (𝑅↑2) ↔ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)))
1915, 18anbi12d 616 . . . . . 6 (𝑦 = 𝑢 → (((𝑡 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑡↑2) + (𝑦↑2)) ≤ (𝑅↑2)) ↔ ((𝑡 ∈ ℝ ∧ 𝑢 ∈ ℝ) ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))))
203, 7, 13, 19opelopab 5131 . . . . 5 (⟨𝑡, 𝑢⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))} ↔ ((𝑡 ∈ ℝ ∧ 𝑢 ∈ ℝ) ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)))
21 anass 454 . . . . 5 (((𝑡 ∈ ℝ ∧ 𝑢 ∈ ℝ) ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)) ↔ (𝑡 ∈ ℝ ∧ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))))
226, 20, 213bitri 286 . . . 4 (𝑡{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))}𝑢 ↔ (𝑡 ∈ ℝ ∧ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))))
2322abbii 2888 . . 3 {𝑢𝑡{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))}𝑢} = {𝑢 ∣ (𝑡 ∈ ℝ ∧ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)))}
242, 5, 233eqtri 2797 . 2 (𝑆 “ {𝑡}) = {𝑢 ∣ (𝑡 ∈ ℝ ∧ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)))}
25 simp3 1132 . . . . 5 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → 𝑡 ∈ ℝ)
2625biantrurd 522 . . . 4 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)) ↔ (𝑡 ∈ ℝ ∧ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)))))
2726abbidv 2890 . . 3 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → {𝑢 ∣ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))} = {𝑢 ∣ (𝑡 ∈ ℝ ∧ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)))})
28 resqcl 13137 . . . . . . . . . . . 12 (𝑅 ∈ ℝ → (𝑅↑2) ∈ ℝ)
29283ad2ant1 1127 . . . . . . . . . . 11 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℝ)
30 resqcl 13137 . . . . . . . . . . . 12 (𝑡 ∈ ℝ → (𝑡↑2) ∈ ℝ)
31303ad2ant3 1129 . . . . . . . . . . 11 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑡↑2) ∈ ℝ)
3229, 31resubcld 10663 . . . . . . . . . 10 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((𝑅↑2) − (𝑡↑2)) ∈ ℝ)
3332adantr 466 . . . . . . . . 9 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → ((𝑅↑2) − (𝑡↑2)) ∈ ℝ)
34 absresq 14249 . . . . . . . . . . . . 13 (𝑡 ∈ ℝ → ((abs‘𝑡)↑2) = (𝑡↑2))
35343ad2ant3 1129 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((abs‘𝑡)↑2) = (𝑡↑2))
3635breq1d 4797 . . . . . . . . . . 11 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (((abs‘𝑡)↑2) ≤ (𝑅↑2) ↔ (𝑡↑2) ≤ (𝑅↑2)))
37 recn 10231 . . . . . . . . . . . . . 14 (𝑡 ∈ ℝ → 𝑡 ∈ ℂ)
3837abscld 14382 . . . . . . . . . . . . 13 (𝑡 ∈ ℝ → (abs‘𝑡) ∈ ℝ)
39383ad2ant3 1129 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (abs‘𝑡) ∈ ℝ)
40 simp1 1130 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → 𝑅 ∈ ℝ)
4137absge0d 14390 . . . . . . . . . . . . 13 (𝑡 ∈ ℝ → 0 ≤ (abs‘𝑡))
42413ad2ant3 1129 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → 0 ≤ (abs‘𝑡))
43 simp2 1131 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → 0 ≤ 𝑅)
4439, 40, 42, 43le2sqd 13250 . . . . . . . . . . 11 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ ((abs‘𝑡)↑2) ≤ (𝑅↑2)))
4529, 31subge0d 10822 . . . . . . . . . . 11 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (0 ≤ ((𝑅↑2) − (𝑡↑2)) ↔ (𝑡↑2) ≤ (𝑅↑2)))
4636, 44, 453bitr4d 300 . . . . . . . . . 10 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ 0 ≤ ((𝑅↑2) − (𝑡↑2))))
4746biimpa 462 . . . . . . . . 9 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → 0 ≤ ((𝑅↑2) − (𝑡↑2)))
4833, 47resqrtcld 14363 . . . . . . . 8 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
4948renegcld 10662 . . . . . . 7 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → -(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
5049rexrd 10294 . . . . . 6 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → -(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ*)
5148rexrd 10294 . . . . . 6 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ*)
52 iccval 12418 . . . . . 6 ((-(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ* ∧ (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ*) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) = {𝑢 ∈ ℝ* ∣ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2))))})
5350, 51, 52syl2anc 573 . . . . 5 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))) = {𝑢 ∈ ℝ* ∣ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2))))})
54 iftrue 4232 . . . . . 6 ((abs‘𝑡) ≤ 𝑅 → if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅) = (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))))
5554adantl 467 . . . . 5 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅) = (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))))
56 absresq 14249 . . . . . . . . . . . 12 (𝑢 ∈ ℝ → ((abs‘𝑢)↑2) = (𝑢↑2))
5732recnd 10273 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((𝑅↑2) − (𝑡↑2)) ∈ ℂ)
5857adantr 466 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → ((𝑅↑2) − (𝑡↑2)) ∈ ℂ)
5958sqsqrtd 14385 . . . . . . . . . . . 12 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → ((√‘((𝑅↑2) − (𝑡↑2)))↑2) = ((𝑅↑2) − (𝑡↑2)))
6056, 59breqan12rd 4804 . . . . . . . . . . 11 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ 𝑢 ∈ ℝ) → (((abs‘𝑢)↑2) ≤ ((√‘((𝑅↑2) − (𝑡↑2)))↑2) ↔ (𝑢↑2) ≤ ((𝑅↑2) − (𝑡↑2))))
61 recn 10231 . . . . . . . . . . . . . 14 (𝑢 ∈ ℝ → 𝑢 ∈ ℂ)
6261abscld 14382 . . . . . . . . . . . . 13 (𝑢 ∈ ℝ → (abs‘𝑢) ∈ ℝ)
6362adantl 467 . . . . . . . . . . . 12 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ 𝑢 ∈ ℝ) → (abs‘𝑢) ∈ ℝ)
6448adantr 466 . . . . . . . . . . . 12 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ 𝑢 ∈ ℝ) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
6561absge0d 14390 . . . . . . . . . . . . 13 (𝑢 ∈ ℝ → 0 ≤ (abs‘𝑢))
6665adantl 467 . . . . . . . . . . . 12 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ 𝑢 ∈ ℝ) → 0 ≤ (abs‘𝑢))
6733, 47sqrtge0d 14366 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → 0 ≤ (√‘((𝑅↑2) − (𝑡↑2))))
6867adantr 466 . . . . . . . . . . . 12 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ 𝑢 ∈ ℝ) → 0 ≤ (√‘((𝑅↑2) − (𝑡↑2))))
6963, 64, 66, 68le2sqd 13250 . . . . . . . . . . 11 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ 𝑢 ∈ ℝ) → ((abs‘𝑢) ≤ (√‘((𝑅↑2) − (𝑡↑2))) ↔ ((abs‘𝑢)↑2) ≤ ((√‘((𝑅↑2) − (𝑡↑2)))↑2)))
7031adantr 466 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑢 ∈ ℝ) → (𝑡↑2) ∈ ℝ)
71 resqcl 13137 . . . . . . . . . . . . . 14 (𝑢 ∈ ℝ → (𝑢↑2) ∈ ℝ)
7271adantl 467 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑢 ∈ ℝ) → (𝑢↑2) ∈ ℝ)
7329adantr 466 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑢 ∈ ℝ) → (𝑅↑2) ∈ ℝ)
7470, 72, 73leaddsub2d 10834 . . . . . . . . . . . 12 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑢 ∈ ℝ) → (((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2) ↔ (𝑢↑2) ≤ ((𝑅↑2) − (𝑡↑2))))
7574adantlr 694 . . . . . . . . . . 11 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ 𝑢 ∈ ℝ) → (((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2) ↔ (𝑢↑2) ≤ ((𝑅↑2) − (𝑡↑2))))
7660, 69, 753bitr4rd 301 . . . . . . . . . 10 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ 𝑢 ∈ ℝ) → (((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2) ↔ (abs‘𝑢) ≤ (√‘((𝑅↑2) − (𝑡↑2)))))
77 simpr 471 . . . . . . . . . . 11 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ 𝑢 ∈ ℝ) → 𝑢 ∈ ℝ)
7877, 64absled 14376 . . . . . . . . . 10 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ 𝑢 ∈ ℝ) → ((abs‘𝑢) ≤ (√‘((𝑅↑2) − (𝑡↑2))) ↔ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2))))))
79 rexr 10290 . . . . . . . . . . . 12 (𝑢 ∈ ℝ → 𝑢 ∈ ℝ*)
8079adantl 467 . . . . . . . . . . 11 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ 𝑢 ∈ ℝ) → 𝑢 ∈ ℝ*)
8180biantrurd 522 . . . . . . . . . 10 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ 𝑢 ∈ ℝ) → ((-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))) ↔ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))))
8276, 78, 813bitrd 294 . . . . . . . . 9 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ 𝑢 ∈ ℝ) → (((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2) ↔ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))))
8382pm5.32da 568 . . . . . . . 8 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → ((𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)) ↔ (𝑢 ∈ ℝ ∧ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2))))))))
84 simprl 754 . . . . . . . . . . 11 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))) → 𝑢 ∈ ℝ*)
8548adantr 466 . . . . . . . . . . 11 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
86 mnfxr 10301 . . . . . . . . . . . . 13 -∞ ∈ ℝ*
8786a1i 11 . . . . . . . . . . . 12 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))) → -∞ ∈ ℝ*)
8849adantr 466 . . . . . . . . . . . . 13 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))) → -(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
8988rexrd 10294 . . . . . . . . . . . 12 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))) → -(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ*)
9049mnfltd 12162 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → -∞ < -(√‘((𝑅↑2) − (𝑡↑2))))
9190adantr 466 . . . . . . . . . . . 12 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))) → -∞ < -(√‘((𝑅↑2) − (𝑡↑2))))
92 simprrl 766 . . . . . . . . . . . 12 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))) → -(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢)
9387, 89, 84, 91, 92xrltletrd 12196 . . . . . . . . . . 11 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))) → -∞ < 𝑢)
94 simprrr 767 . . . . . . . . . . 11 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))) → 𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2))))
95 xrre 12204 . . . . . . . . . . 11 (((𝑢 ∈ ℝ* ∧ (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ) ∧ (-∞ < 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2))))) → 𝑢 ∈ ℝ)
9684, 85, 93, 94, 95syl22anc 1477 . . . . . . . . . 10 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))) → 𝑢 ∈ ℝ)
9796ex 397 . . . . . . . . 9 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → ((𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2))))) → 𝑢 ∈ ℝ))
9897pm4.71rd 552 . . . . . . . 8 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → ((𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2))))) ↔ (𝑢 ∈ ℝ ∧ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2))))))))
9983, 98bitr4d 271 . . . . . . 7 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → ((𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)) ↔ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))))
10099abbidv 2890 . . . . . 6 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → {𝑢 ∣ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))} = {𝑢 ∣ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))})
101 df-rab 3070 . . . . . 6 {𝑢 ∈ ℝ* ∣ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2))))} = {𝑢 ∣ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))}
102100, 101syl6eqr 2823 . . . . 5 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → {𝑢 ∣ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))} = {𝑢 ∈ ℝ* ∣ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2))))})
10353, 55, 1023eqtr4rd 2816 . . . 4 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → {𝑢 ∣ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))} = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))
10440, 39ltnled 10389 . . . . . . . 8 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑅 < (abs‘𝑡) ↔ ¬ (abs‘𝑡) ≤ 𝑅))
105104biimprd 238 . . . . . . 7 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (¬ (abs‘𝑡) ≤ 𝑅𝑅 < (abs‘𝑡)))
106105imdistani 558 . . . . . 6 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ ¬ (abs‘𝑡) ≤ 𝑅) → ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡)))
107 df-rab 3070 . . . . . . 7 {𝑢 ∈ ℝ ∣ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)} = {𝑢 ∣ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))}
108293ad2ant1 1127 . . . . . . . . . . . 12 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡) ∧ 𝑢 ∈ ℝ) → (𝑅↑2) ∈ ℝ)
109313ad2ant1 1127 . . . . . . . . . . . 12 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡) ∧ 𝑢 ∈ ℝ) → (𝑡↑2) ∈ ℝ)
110713ad2ant3 1129 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡) ∧ 𝑢 ∈ ℝ) → (𝑢↑2) ∈ ℝ)
111109, 110readdcld 10274 . . . . . . . . . . . 12 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡) ∧ 𝑢 ∈ ℝ) → ((𝑡↑2) + (𝑢↑2)) ∈ ℝ)
11240, 39, 43, 42lt2sqd 13249 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑅 < (abs‘𝑡) ↔ (𝑅↑2) < ((abs‘𝑡)↑2)))
11335breq2d 4799 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((𝑅↑2) < ((abs‘𝑡)↑2) ↔ (𝑅↑2) < (𝑡↑2)))
114112, 113bitrd 268 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑅 < (abs‘𝑡) ↔ (𝑅↑2) < (𝑡↑2)))
115114biimpa 462 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡)) → (𝑅↑2) < (𝑡↑2))
1161153adant3 1126 . . . . . . . . . . . 12 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡) ∧ 𝑢 ∈ ℝ) → (𝑅↑2) < (𝑡↑2))
117 sqge0 13146 . . . . . . . . . . . . . 14 (𝑢 ∈ ℝ → 0 ≤ (𝑢↑2))
1181173ad2ant3 1129 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡) ∧ 𝑢 ∈ ℝ) → 0 ≤ (𝑢↑2))
119109, 110addge01d 10820 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡) ∧ 𝑢 ∈ ℝ) → (0 ≤ (𝑢↑2) ↔ (𝑡↑2) ≤ ((𝑡↑2) + (𝑢↑2))))
120118, 119mpbid 222 . . . . . . . . . . . 12 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡) ∧ 𝑢 ∈ ℝ) → (𝑡↑2) ≤ ((𝑡↑2) + (𝑢↑2)))
121108, 109, 111, 116, 120ltletrd 10402 . . . . . . . . . . 11 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡) ∧ 𝑢 ∈ ℝ) → (𝑅↑2) < ((𝑡↑2) + (𝑢↑2)))
122108, 111ltnled 10389 . . . . . . . . . . 11 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡) ∧ 𝑢 ∈ ℝ) → ((𝑅↑2) < ((𝑡↑2) + (𝑢↑2)) ↔ ¬ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)))
123121, 122mpbid 222 . . . . . . . . . 10 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡) ∧ 𝑢 ∈ ℝ) → ¬ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))
1241233expa 1111 . . . . . . . . 9 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡)) ∧ 𝑢 ∈ ℝ) → ¬ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))
125124ralrimiva 3115 . . . . . . . 8 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡)) → ∀𝑢 ∈ ℝ ¬ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))
126 rabeq0 4104 . . . . . . . 8 ({𝑢 ∈ ℝ ∣ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)} = ∅ ↔ ∀𝑢 ∈ ℝ ¬ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))
127125, 126sylibr 224 . . . . . . 7 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡)) → {𝑢 ∈ ℝ ∣ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)} = ∅)
128107, 127syl5eqr 2819 . . . . . 6 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡)) → {𝑢 ∣ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))} = ∅)
129106, 128syl 17 . . . . 5 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ ¬ (abs‘𝑡) ≤ 𝑅) → {𝑢 ∣ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))} = ∅)
130 iffalse 4235 . . . . . 6 (¬ (abs‘𝑡) ≤ 𝑅 → if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅) = ∅)
131130adantl 467 . . . . 5 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ ¬ (abs‘𝑡) ≤ 𝑅) → if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅) = ∅)
132129, 131eqtr4d 2808 . . . 4 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ ¬ (abs‘𝑡) ≤ 𝑅) → {𝑢 ∣ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))} = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))
133103, 132pm2.61dan 814 . . 3 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → {𝑢 ∣ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))} = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))
13427, 133eqtr3d 2807 . 2 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → {𝑢 ∣ (𝑡 ∈ ℝ ∧ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)))} = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))
13524, 134syl5eq 2817 1 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑆 “ {𝑡}) = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  w3a 1071   = wceq 1631  wcel 2145  {cab 2757  wral 3061  {crab 3065  Vcvv 3351  c0 4063  ifcif 4226  {csn 4317  cop 4323   class class class wbr 4787  {copab 4847  cima 5253  cfv 6030  (class class class)co 6795  cc 10139  cr 10140  0cc0 10141   + caddc 10144  -∞cmnf 10277  *cxr 10278   < clt 10279  cle 10280  cmin 10471  -cneg 10472  2c2 11275  [,]cicc 12382  cexp 13066  csqrt 14180  abscabs 14181
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7099  ax-cnex 10197  ax-resscn 10198  ax-1cn 10199  ax-icn 10200  ax-addcl 10201  ax-addrcl 10202  ax-mulcl 10203  ax-mulrcl 10204  ax-mulcom 10205  ax-addass 10206  ax-mulass 10207  ax-distr 10208  ax-i2m1 10209  ax-1ne0 10210  ax-1rid 10211  ax-rnegex 10212  ax-rrecex 10213  ax-cnre 10214  ax-pre-lttri 10215  ax-pre-lttrn 10216  ax-pre-ltadd 10217  ax-pre-mulgt0 10218  ax-pre-sup 10219
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4576  df-iun 4657  df-br 4788  df-opab 4848  df-mpt 4865  df-tr 4888  df-id 5158  df-eprel 5163  df-po 5171  df-so 5172  df-fr 5209  df-we 5211  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-pred 5822  df-ord 5868  df-on 5869  df-lim 5870  df-suc 5871  df-iota 5993  df-fun 6032  df-fn 6033  df-f 6034  df-f1 6035  df-fo 6036  df-f1o 6037  df-fv 6038  df-riota 6756  df-ov 6798  df-oprab 6799  df-mpt2 6800  df-om 7216  df-2nd 7319  df-wrecs 7562  df-recs 7624  df-rdg 7662  df-er 7899  df-en 8113  df-dom 8114  df-sdom 8115  df-sup 8507  df-pnf 10281  df-mnf 10282  df-xr 10283  df-ltxr 10284  df-le 10285  df-sub 10473  df-neg 10474  df-div 10890  df-nn 11226  df-2 11284  df-3 11285  df-n0 11499  df-z 11584  df-uz 11893  df-rp 12035  df-icc 12386  df-seq 13008  df-exp 13067  df-cj 14046  df-re 14047  df-im 14048  df-sqrt 14182  df-abs 14183
This theorem is referenced by:  areacirc  33836
  Copyright terms: Public domain W3C validator