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 35982
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 5996 . . 3 (𝑆 “ {𝑡}) = ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))} “ {𝑡})
3 vex 3445 . . . 4 𝑡 ∈ V
4 imasng 6021 . . . 4 (𝑡 ∈ V → ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))} “ {𝑡}) = {𝑢𝑡{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))}𝑢})
53, 4ax-mp 5 . . 3 ({⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))} “ {𝑡}) = {𝑢𝑡{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))}𝑢}
6 df-br 5093 . . . . 5 (𝑡{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))}𝑢 ↔ ⟨𝑡, 𝑢⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))})
7 vex 3445 . . . . . 6 𝑢 ∈ V
8 eleq1w 2819 . . . . . . . 8 (𝑥 = 𝑡 → (𝑥 ∈ ℝ ↔ 𝑡 ∈ ℝ))
98anbi1d 630 . . . . . . 7 (𝑥 = 𝑡 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ↔ (𝑡 ∈ ℝ ∧ 𝑦 ∈ ℝ)))
10 oveq1 7344 . . . . . . . . 9 (𝑥 = 𝑡 → (𝑥↑2) = (𝑡↑2))
1110oveq1d 7352 . . . . . . . 8 (𝑥 = 𝑡 → ((𝑥↑2) + (𝑦↑2)) = ((𝑡↑2) + (𝑦↑2)))
1211breq1d 5102 . . . . . . 7 (𝑥 = 𝑡 → (((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2) ↔ ((𝑡↑2) + (𝑦↑2)) ≤ (𝑅↑2)))
139, 12anbi12d 631 . . . . . 6 (𝑥 = 𝑡 → (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2)) ↔ ((𝑡 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑡↑2) + (𝑦↑2)) ≤ (𝑅↑2))))
14 eleq1w 2819 . . . . . . . 8 (𝑦 = 𝑢 → (𝑦 ∈ ℝ ↔ 𝑢 ∈ ℝ))
1514anbi2d 629 . . . . . . 7 (𝑦 = 𝑢 → ((𝑡 ∈ ℝ ∧ 𝑦 ∈ ℝ) ↔ (𝑡 ∈ ℝ ∧ 𝑢 ∈ ℝ)))
16 oveq1 7344 . . . . . . . . 9 (𝑦 = 𝑢 → (𝑦↑2) = (𝑢↑2))
1716oveq2d 7353 . . . . . . . 8 (𝑦 = 𝑢 → ((𝑡↑2) + (𝑦↑2)) = ((𝑡↑2) + (𝑢↑2)))
1817breq1d 5102 . . . . . . 7 (𝑦 = 𝑢 → (((𝑡↑2) + (𝑦↑2)) ≤ (𝑅↑2) ↔ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)))
1915, 18anbi12d 631 . . . . . 6 (𝑦 = 𝑢 → (((𝑡 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑡↑2) + (𝑦↑2)) ≤ (𝑅↑2)) ↔ ((𝑡 ∈ ℝ ∧ 𝑢 ∈ ℝ) ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))))
203, 7, 13, 19opelopab 5486 . . . . 5 (⟨𝑡, 𝑢⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))} ↔ ((𝑡 ∈ ℝ ∧ 𝑢 ∈ ℝ) ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)))
21 anass 469 . . . . 5 (((𝑡 ∈ ℝ ∧ 𝑢 ∈ ℝ) ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)) ↔ (𝑡 ∈ ℝ ∧ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))))
226, 20, 213bitri 296 . . . 4 (𝑡{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))}𝑢 ↔ (𝑡 ∈ ℝ ∧ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))))
2322abbii 2806 . . 3 {𝑢𝑡{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ((𝑥↑2) + (𝑦↑2)) ≤ (𝑅↑2))}𝑢} = {𝑢 ∣ (𝑡 ∈ ℝ ∧ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)))}
242, 5, 233eqtri 2768 . 2 (𝑆 “ {𝑡}) = {𝑢 ∣ (𝑡 ∈ ℝ ∧ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)))}
25 simp3 1137 . . . . 5 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → 𝑡 ∈ ℝ)
2625biantrurd 533 . . . 4 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)) ↔ (𝑡 ∈ ℝ ∧ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)))))
2726abbidv 2805 . . 3 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → {𝑢 ∣ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))} = {𝑢 ∣ (𝑡 ∈ ℝ ∧ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)))})
28 resqcl 13945 . . . . . . . . . . . 12 (𝑅 ∈ ℝ → (𝑅↑2) ∈ ℝ)
29283ad2ant1 1132 . . . . . . . . . . 11 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑅↑2) ∈ ℝ)
30 resqcl 13945 . . . . . . . . . . . 12 (𝑡 ∈ ℝ → (𝑡↑2) ∈ ℝ)
31303ad2ant3 1134 . . . . . . . . . . 11 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑡↑2) ∈ ℝ)
3229, 31resubcld 11504 . . . . . . . . . 10 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((𝑅↑2) − (𝑡↑2)) ∈ ℝ)
3332adantr 481 . . . . . . . . 9 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → ((𝑅↑2) − (𝑡↑2)) ∈ ℝ)
34 absresq 15113 . . . . . . . . . . . . 13 (𝑡 ∈ ℝ → ((abs‘𝑡)↑2) = (𝑡↑2))
35343ad2ant3 1134 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((abs‘𝑡)↑2) = (𝑡↑2))
3635breq1d 5102 . . . . . . . . . . 11 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (((abs‘𝑡)↑2) ≤ (𝑅↑2) ↔ (𝑡↑2) ≤ (𝑅↑2)))
37 recn 11062 . . . . . . . . . . . . . 14 (𝑡 ∈ ℝ → 𝑡 ∈ ℂ)
3837abscld 15247 . . . . . . . . . . . . 13 (𝑡 ∈ ℝ → (abs‘𝑡) ∈ ℝ)
39383ad2ant3 1134 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (abs‘𝑡) ∈ ℝ)
40 simp1 1135 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → 𝑅 ∈ ℝ)
4137absge0d 15255 . . . . . . . . . . . . 13 (𝑡 ∈ ℝ → 0 ≤ (abs‘𝑡))
42413ad2ant3 1134 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → 0 ≤ (abs‘𝑡))
43 simp2 1136 . . . . . . . . . . . 12 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → 0 ≤ 𝑅)
4439, 40, 42, 43le2sqd 14075 . . . . . . . . . . 11 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ ((abs‘𝑡)↑2) ≤ (𝑅↑2)))
4529, 31subge0d 11666 . . . . . . . . . . 11 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (0 ≤ ((𝑅↑2) − (𝑡↑2)) ↔ (𝑡↑2) ≤ (𝑅↑2)))
4636, 44, 453bitr4d 310 . . . . . . . . . 10 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((abs‘𝑡) ≤ 𝑅 ↔ 0 ≤ ((𝑅↑2) − (𝑡↑2))))
4746biimpa 477 . . . . . . . . 9 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → 0 ≤ ((𝑅↑2) − (𝑡↑2)))
4833, 47resqrtcld 15228 . . . . . . . 8 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
4948renegcld 11503 . . . . . . 7 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → -(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
5049rexrd 11126 . . . . . 6 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → -(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ*)
5148rexrd 11126 . . . . . 6 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ*)
52 iccval 13219 . . . . . 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 4479 . . . . . 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 15113 . . . . . . . . . . . 12 (𝑢 ∈ ℝ → ((abs‘𝑢)↑2) = (𝑢↑2))
5732recnd 11104 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((𝑅↑2) − (𝑡↑2)) ∈ ℂ)
5857adantr 481 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → ((𝑅↑2) − (𝑡↑2)) ∈ ℂ)
5958sqsqrtd 15250 . . . . . . . . . . . 12 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → ((√‘((𝑅↑2) − (𝑡↑2)))↑2) = ((𝑅↑2) − (𝑡↑2)))
6056, 59breqan12rd 5109 . . . . . . . . . . 11 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ 𝑢 ∈ ℝ) → (((abs‘𝑢)↑2) ≤ ((√‘((𝑅↑2) − (𝑡↑2)))↑2) ↔ (𝑢↑2) ≤ ((𝑅↑2) − (𝑡↑2))))
61 recn 11062 . . . . . . . . . . . . . 14 (𝑢 ∈ ℝ → 𝑢 ∈ ℂ)
6261abscld 15247 . . . . . . . . . . . . 13 (𝑢 ∈ ℝ → (abs‘𝑢) ∈ ℝ)
6362adantl 482 . . . . . . . . . . . 12 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ 𝑢 ∈ ℝ) → (abs‘𝑢) ∈ ℝ)
6448adantr 481 . . . . . . . . . . . 12 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ 𝑢 ∈ ℝ) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
6561absge0d 15255 . . . . . . . . . . . . 13 (𝑢 ∈ ℝ → 0 ≤ (abs‘𝑢))
6665adantl 482 . . . . . . . . . . . 12 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ 𝑢 ∈ ℝ) → 0 ≤ (abs‘𝑢))
6733, 47sqrtge0d 15231 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → 0 ≤ (√‘((𝑅↑2) − (𝑡↑2))))
6867adantr 481 . . . . . . . . . . . 12 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ 𝑢 ∈ ℝ) → 0 ≤ (√‘((𝑅↑2) − (𝑡↑2))))
6963, 64, 66, 68le2sqd 14075 . . . . . . . . . . 11 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ 𝑢 ∈ ℝ) → ((abs‘𝑢) ≤ (√‘((𝑅↑2) − (𝑡↑2))) ↔ ((abs‘𝑢)↑2) ≤ ((√‘((𝑅↑2) − (𝑡↑2)))↑2)))
7031adantr 481 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑢 ∈ ℝ) → (𝑡↑2) ∈ ℝ)
71 resqcl 13945 . . . . . . . . . . . . . 14 (𝑢 ∈ ℝ → (𝑢↑2) ∈ ℝ)
7271adantl 482 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑢 ∈ ℝ) → (𝑢↑2) ∈ ℝ)
7329adantr 481 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑢 ∈ ℝ) → (𝑅↑2) ∈ ℝ)
7470, 72, 73leaddsub2d 11678 . . . . . . . . . . . 12 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑢 ∈ ℝ) → (((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2) ↔ (𝑢↑2) ≤ ((𝑅↑2) − (𝑡↑2))))
7574adantlr 712 . . . . . . . . . . 11 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ 𝑢 ∈ ℝ) → (((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2) ↔ (𝑢↑2) ≤ ((𝑅↑2) − (𝑡↑2))))
7660, 69, 753bitr4rd 311 . . . . . . . . . 10 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ 𝑢 ∈ ℝ) → (((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2) ↔ (abs‘𝑢) ≤ (√‘((𝑅↑2) − (𝑡↑2)))))
77 simpr 485 . . . . . . . . . . 11 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ 𝑢 ∈ ℝ) → 𝑢 ∈ ℝ)
7877, 64absled 15241 . . . . . . . . . 10 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ 𝑢 ∈ ℝ) → ((abs‘𝑢) ≤ (√‘((𝑅↑2) − (𝑡↑2))) ↔ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2))))))
79 rexr 11122 . . . . . . . . . . . 12 (𝑢 ∈ ℝ → 𝑢 ∈ ℝ*)
8079adantl 482 . . . . . . . . . . 11 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ 𝑢 ∈ ℝ) → 𝑢 ∈ ℝ*)
8180biantrurd 533 . . . . . . . . . 10 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ 𝑢 ∈ ℝ) → ((-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))) ↔ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))))
8276, 78, 813bitrd 304 . . . . . . . . 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 768 . . . . . . . . . . 11 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))) → 𝑢 ∈ ℝ*)
8548adantr 481 . . . . . . . . . . 11 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))) → (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
86 mnfxr 11133 . . . . . . . . . . . . 13 -∞ ∈ ℝ*
8786a1i 11 . . . . . . . . . . . 12 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))) → -∞ ∈ ℝ*)
8849adantr 481 . . . . . . . . . . . . 13 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))) → -(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ)
8988rexrd 11126 . . . . . . . . . . . 12 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))) → -(√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ*)
9049mnfltd 12961 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → -∞ < -(√‘((𝑅↑2) − (𝑡↑2))))
9190adantr 481 . . . . . . . . . . . 12 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))) → -∞ < -(√‘((𝑅↑2) − (𝑡↑2))))
92 simprrl 778 . . . . . . . . . . . 12 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))) → -(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢)
9387, 89, 84, 91, 92xrltletrd 12996 . . . . . . . . . . 11 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))) → -∞ < 𝑢)
94 simprrr 779 . . . . . . . . . . 11 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) ∧ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))) → 𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2))))
95 xrre 13004 . . . . . . . . . . 11 (((𝑢 ∈ ℝ* ∧ (√‘((𝑅↑2) − (𝑡↑2))) ∈ ℝ) ∧ (-∞ < 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2))))) → 𝑢 ∈ ℝ)
9684, 85, 93, 94, 95syl22anc 836 . . . . . . . . . 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 281 . . . . . . 7 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → ((𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)) ↔ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))))
10099abbidv 2805 . . . . . 6 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → {𝑢 ∣ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))} = {𝑢 ∣ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))})
101 df-rab 3404 . . . . . 6 {𝑢 ∈ ℝ* ∣ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2))))} = {𝑢 ∣ (𝑢 ∈ ℝ* ∧ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2)))))}
102100, 101eqtr4di 2794 . . . . 5 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → {𝑢 ∣ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))} = {𝑢 ∈ ℝ* ∣ (-(√‘((𝑅↑2) − (𝑡↑2))) ≤ 𝑢𝑢 ≤ (√‘((𝑅↑2) − (𝑡↑2))))})
10353, 55, 1023eqtr4rd 2787 . . . 4 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ (abs‘𝑡) ≤ 𝑅) → {𝑢 ∣ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))} = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))
10440, 39ltnled 11223 . . . . . . . 8 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑅 < (abs‘𝑡) ↔ ¬ (abs‘𝑡) ≤ 𝑅))
105104biimprd 247 . . . . . . 7 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (¬ (abs‘𝑡) ≤ 𝑅𝑅 < (abs‘𝑡)))
106105imdistani 569 . . . . . 6 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ ¬ (abs‘𝑡) ≤ 𝑅) → ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡)))
107 df-rab 3404 . . . . . . 7 {𝑢 ∈ ℝ ∣ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)} = {𝑢 ∣ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))}
108293ad2ant1 1132 . . . . . . . . . . . 12 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡) ∧ 𝑢 ∈ ℝ) → (𝑅↑2) ∈ ℝ)
109313ad2ant1 1132 . . . . . . . . . . . 12 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡) ∧ 𝑢 ∈ ℝ) → (𝑡↑2) ∈ ℝ)
110713ad2ant3 1134 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡) ∧ 𝑢 ∈ ℝ) → (𝑢↑2) ∈ ℝ)
111109, 110readdcld 11105 . . . . . . . . . . . 12 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡) ∧ 𝑢 ∈ ℝ) → ((𝑡↑2) + (𝑢↑2)) ∈ ℝ)
11240, 39, 43, 42lt2sqd 14074 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑅 < (abs‘𝑡) ↔ (𝑅↑2) < ((abs‘𝑡)↑2)))
11335breq2d 5104 . . . . . . . . . . . . . . 15 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → ((𝑅↑2) < ((abs‘𝑡)↑2) ↔ (𝑅↑2) < (𝑡↑2)))
114112, 113bitrd 278 . . . . . . . . . . . . . 14 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑅 < (abs‘𝑡) ↔ (𝑅↑2) < (𝑡↑2)))
115114biimpa 477 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡)) → (𝑅↑2) < (𝑡↑2))
1161153adant3 1131 . . . . . . . . . . . 12 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡) ∧ 𝑢 ∈ ℝ) → (𝑅↑2) < (𝑡↑2))
117 sqge0 13956 . . . . . . . . . . . . . 14 (𝑢 ∈ ℝ → 0 ≤ (𝑢↑2))
1181173ad2ant3 1134 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡) ∧ 𝑢 ∈ ℝ) → 0 ≤ (𝑢↑2))
119109, 110addge01d 11664 . . . . . . . . . . . . 13 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡) ∧ 𝑢 ∈ ℝ) → (0 ≤ (𝑢↑2) ↔ (𝑡↑2) ≤ ((𝑡↑2) + (𝑢↑2))))
120118, 119mpbid 231 . . . . . . . . . . . 12 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡) ∧ 𝑢 ∈ ℝ) → (𝑡↑2) ≤ ((𝑡↑2) + (𝑢↑2)))
121108, 109, 111, 116, 120ltletrd 11236 . . . . . . . . . . 11 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡) ∧ 𝑢 ∈ ℝ) → (𝑅↑2) < ((𝑡↑2) + (𝑢↑2)))
122108, 111ltnled 11223 . . . . . . . . . . 11 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡) ∧ 𝑢 ∈ ℝ) → ((𝑅↑2) < ((𝑡↑2) + (𝑢↑2)) ↔ ¬ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)))
123121, 122mpbid 231 . . . . . . . . . 10 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡) ∧ 𝑢 ∈ ℝ) → ¬ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))
1241233expa 1117 . . . . . . . . 9 ((((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡)) ∧ 𝑢 ∈ ℝ) → ¬ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))
125124ralrimiva 3139 . . . . . . . 8 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡)) → ∀𝑢 ∈ ℝ ¬ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))
126 rabeq0 4331 . . . . . . . 8 ({𝑢 ∈ ℝ ∣ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)} = ∅ ↔ ∀𝑢 ∈ ℝ ¬ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))
127125, 126sylibr 233 . . . . . . 7 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡)) → {𝑢 ∈ ℝ ∣ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)} = ∅)
128107, 127eqtr3id 2790 . . . . . 6 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ 𝑅 < (abs‘𝑡)) → {𝑢 ∣ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))} = ∅)
129106, 128syl 17 . . . . 5 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ ¬ (abs‘𝑡) ≤ 𝑅) → {𝑢 ∣ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))} = ∅)
130 iffalse 4482 . . . . . 6 (¬ (abs‘𝑡) ≤ 𝑅 → if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅) = ∅)
131130adantl 482 . . . . 5 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ ¬ (abs‘𝑡) ≤ 𝑅) → if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅) = ∅)
132129, 131eqtr4d 2779 . . . 4 (((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) ∧ ¬ (abs‘𝑡) ≤ 𝑅) → {𝑢 ∣ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))} = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))
133103, 132pm2.61dan 810 . . 3 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → {𝑢 ∣ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2))} = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))
13427, 133eqtr3d 2778 . 2 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → {𝑢 ∣ (𝑡 ∈ ℝ ∧ (𝑢 ∈ ℝ ∧ ((𝑡↑2) + (𝑢↑2)) ≤ (𝑅↑2)))} = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))
13524, 134eqtrid 2788 1 ((𝑅 ∈ ℝ ∧ 0 ≤ 𝑅𝑡 ∈ ℝ) → (𝑆 “ {𝑡}) = if((abs‘𝑡) ≤ 𝑅, (-(√‘((𝑅↑2) − (𝑡↑2)))[,](√‘((𝑅↑2) − (𝑡↑2)))), ∅))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1086   = wceq 1540  wcel 2105  {cab 2713  wral 3061  {crab 3403  Vcvv 3441  c0 4269  ifcif 4473  {csn 4573  cop 4579   class class class wbr 5092  {copab 5154  cima 5623  cfv 6479  (class class class)co 7337  cc 10970  cr 10971  0cc0 10972   + caddc 10975  -∞cmnf 11108  *cxr 11109   < clt 11110  cle 11111  cmin 11306  -cneg 11307  2c2 12129  [,]cicc 13183  cexp 13883  csqrt 15043  abscabs 15044
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5243  ax-nul 5250  ax-pow 5308  ax-pr 5372  ax-un 7650  ax-cnex 11028  ax-resscn 11029  ax-1cn 11030  ax-icn 11031  ax-addcl 11032  ax-addrcl 11033  ax-mulcl 11034  ax-mulrcl 11035  ax-mulcom 11036  ax-addass 11037  ax-mulass 11038  ax-distr 11039  ax-i2m1 11040  ax-1ne0 11041  ax-1rid 11042  ax-rnegex 11043  ax-rrecex 11044  ax-cnre 11045  ax-pre-lttri 11046  ax-pre-lttrn 11047  ax-pre-ltadd 11048  ax-pre-mulgt0 11049  ax-pre-sup 11050
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3917  df-nul 4270  df-if 4474  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4853  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5176  df-tr 5210  df-id 5518  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5575  df-we 5577  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-pred 6238  df-ord 6305  df-on 6306  df-lim 6307  df-suc 6308  df-iota 6431  df-fun 6481  df-fn 6482  df-f 6483  df-f1 6484  df-fo 6485  df-f1o 6486  df-fv 6487  df-riota 7293  df-ov 7340  df-oprab 7341  df-mpo 7342  df-om 7781  df-2nd 7900  df-frecs 8167  df-wrecs 8198  df-recs 8272  df-rdg 8311  df-er 8569  df-en 8805  df-dom 8806  df-sdom 8807  df-sup 9299  df-pnf 11112  df-mnf 11113  df-xr 11114  df-ltxr 11115  df-le 11116  df-sub 11308  df-neg 11309  df-div 11734  df-nn 12075  df-2 12137  df-3 12138  df-n0 12335  df-z 12421  df-uz 12684  df-rp 12832  df-icc 13187  df-seq 13823  df-exp 13884  df-cj 14909  df-re 14910  df-im 14911  df-sqrt 15045  df-abs 15046
This theorem is referenced by:  areacirc  35983
  Copyright terms: Public domain W3C validator