Metamath Proof Explorer


Theorem itscnhlinecirc02plem3

Description: Lemma 3 for itscnhlinecirc02p . (Contributed by AV, 10-Mar-2023)

Ref Expression
Hypotheses itscnhlinecirc02p.i I = 1 2
itscnhlinecirc02p.e E = I
itscnhlinecirc02p.p P = I
itscnhlinecirc02p.s S = Sphere E
itscnhlinecirc02p.0 0 ˙ = I × 0
itscnhlinecirc02p.l L = Line M E
itscnhlinecirc02p.d D = dist E
Assertion itscnhlinecirc02plem3 X P Y P X 2 Y 2 R + X D 0 ˙ < R 0 < 2 Y 1 X 1 X 2 Y 1 X 1 Y 2 2 4 X 2 Y 2 2 + Y 1 X 1 2 X 2 Y 1 X 1 Y 2 2 X 2 Y 2 2 R 2

Proof

Step Hyp Ref Expression
1 itscnhlinecirc02p.i I = 1 2
2 itscnhlinecirc02p.e E = I
3 itscnhlinecirc02p.p P = I
4 itscnhlinecirc02p.s S = Sphere E
5 itscnhlinecirc02p.0 0 ˙ = I × 0
6 itscnhlinecirc02p.l L = Line M E
7 itscnhlinecirc02p.d D = dist E
8 1 3 rrx2pxel X P X 1
9 1 3 rrx2pyel X P X 2
10 8 9 jca X P X 1 X 2
11 10 3ad2ant1 X P Y P X 2 Y 2 X 1 X 2
12 11 adantr X P Y P X 2 Y 2 R + X D 0 ˙ < R X 1 X 2
13 1 3 rrx2pxel Y P Y 1
14 1 3 rrx2pyel Y P Y 2
15 13 14 jca Y P Y 1 Y 2
16 15 3ad2ant2 X P Y P X 2 Y 2 Y 1 Y 2
17 16 adantr X P Y P X 2 Y 2 R + X D 0 ˙ < R Y 1 Y 2
18 simpl3 X P Y P X 2 Y 2 R + X D 0 ˙ < R X 2 Y 2
19 rpre R + R
20 19 adantr R + X D 0 ˙ < R R
21 20 adantl X P Y P X 2 Y 2 R + X D 0 ˙ < R R
22 simpl1 X P Y P X 2 Y 2 R + X P
23 2nn0 2 0
24 eqid 𝔼 hil 2 = 𝔼 hil 2
25 24 ehlval 2 0 𝔼 hil 2 = 1 2
26 23 25 ax-mp 𝔼 hil 2 = 1 2
27 fz12pr 1 2 = 1 2
28 27 1 eqtr4i 1 2 = I
29 28 fveq2i 1 2 = I
30 26 29 eqtri 𝔼 hil 2 = I
31 2 30 eqtr4i E = 𝔼 hil 2
32 1 oveq2i I = 1 2
33 3 32 eqtri P = 1 2
34 1 xpeq1i I × 0 = 1 2 × 0
35 5 34 eqtri 0 ˙ = 1 2 × 0
36 31 33 7 35 ehl2eudisval0 X P X D 0 ˙ = X 1 2 + X 2 2
37 22 36 syl X P Y P X 2 Y 2 R + X D 0 ˙ = X 1 2 + X 2 2
38 37 breq1d X P Y P X 2 Y 2 R + X D 0 ˙ < R X 1 2 + X 2 2 < R
39 rpge0 R + 0 R
40 19 39 sqrtsqd R + R 2 = R
41 40 eqcomd R + R = R 2
42 41 adantl X P Y P X 2 Y 2 R + R = R 2
43 42 breq2d X P Y P X 2 Y 2 R + X 1 2 + X 2 2 < R X 1 2 + X 2 2 < R 2
44 43 biimpa X P Y P X 2 Y 2 R + X 1 2 + X 2 2 < R X 1 2 + X 2 2 < R 2
45 22 8 syl X P Y P X 2 Y 2 R + X 1
46 45 adantr X P Y P X 2 Y 2 R + X 1 2 + X 2 2 < R X 1
47 46 resqcld X P Y P X 2 Y 2 R + X 1 2 + X 2 2 < R X 1 2
48 22 9 syl X P Y P X 2 Y 2 R + X 2
49 48 adantr X P Y P X 2 Y 2 R + X 1 2 + X 2 2 < R X 2
50 49 resqcld X P Y P X 2 Y 2 R + X 1 2 + X 2 2 < R X 2 2
51 47 50 readdcld X P Y P X 2 Y 2 R + X 1 2 + X 2 2 < R X 1 2 + X 2 2
52 46 sqge0d X P Y P X 2 Y 2 R + X 1 2 + X 2 2 < R 0 X 1 2
53 49 sqge0d X P Y P X 2 Y 2 R + X 1 2 + X 2 2 < R 0 X 2 2
54 47 50 52 53 addge0d X P Y P X 2 Y 2 R + X 1 2 + X 2 2 < R 0 X 1 2 + X 2 2
55 19 adantl X P Y P X 2 Y 2 R + R
56 55 adantr X P Y P X 2 Y 2 R + X 1 2 + X 2 2 < R R
57 56 resqcld X P Y P X 2 Y 2 R + X 1 2 + X 2 2 < R R 2
58 56 sqge0d X P Y P X 2 Y 2 R + X 1 2 + X 2 2 < R 0 R 2
59 51 54 57 58 sqrtltd X P Y P X 2 Y 2 R + X 1 2 + X 2 2 < R X 1 2 + X 2 2 < R 2 X 1 2 + X 2 2 < R 2
60 44 59 mpbird X P Y P X 2 Y 2 R + X 1 2 + X 2 2 < R X 1 2 + X 2 2 < R 2
61 60 ex X P Y P X 2 Y 2 R + X 1 2 + X 2 2 < R X 1 2 + X 2 2 < R 2
62 38 61 sylbid X P Y P X 2 Y 2 R + X D 0 ˙ < R X 1 2 + X 2 2 < R 2
63 62 impr X P Y P X 2 Y 2 R + X D 0 ˙ < R X 1 2 + X 2 2 < R 2
64 eqid Y 1 X 1 = Y 1 X 1
65 eqid X 2 Y 2 = X 2 Y 2
66 eqid X 2 Y 1 X 1 Y 2 = X 2 Y 1 X 1 Y 2
67 64 65 66 itscnhlinecirc02plem2 X 1 X 2 Y 1 Y 2 X 2 Y 2 R X 1 2 + X 2 2 < R 2 0 < 2 Y 1 X 1 X 2 Y 1 X 1 Y 2 2 4 X 2 Y 2 2 + Y 1 X 1 2 X 2 Y 1 X 1 Y 2 2 X 2 Y 2 2 R 2
68 12 17 18 21 63 67 syl32anc X P Y P X 2 Y 2 R + X D 0 ˙ < R 0 < 2 Y 1 X 1 X 2 Y 1 X 1 Y 2 2 4 X 2 Y 2 2 + Y 1 X 1 2 X 2 Y 1 X 1 Y 2 2 X 2 Y 2 2 R 2