# Metamath Proof Explorer

## Theorem 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 ${⊢}{S}=\left\{⟨{x},{y}⟩|\left(\left({x}\in ℝ\wedge {y}\in ℝ\right)\wedge {{x}}^{2}+{{y}}^{2}\le {{R}}^{2}\right)\right\}$
Assertion areacirclem5 ${⊢}\left({R}\in ℝ\wedge 0\le {R}\wedge {t}\in ℝ\right)\to {S}\left[\left\{{t}\right\}\right]=if\left(\left|{t}\right|\le {R},\left[-\sqrt{{{R}}^{2}-{{t}}^{2}},\sqrt{{{R}}^{2}-{{t}}^{2}}\right],\varnothing \right)$

### Proof

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