Metamath Proof Explorer

Theorem itscnhlinecirc02plem3

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

Ref Expression
Hypotheses itscnhlinecirc02p.i 
|- I = ( 0 ..^ 2 )
itscnhlinecirc02p.e 
|- E = ( RR^ ` I )
itscnhlinecirc02p.p 
|- P = ( RR ^m I )
itscnhlinecirc02p.s 
|- S = ( Sphere ` E )
itscnhlinecirc02p.0 
|- .0. = ( I X. { 0 } )
itscnhlinecirc02p.l 
|- L = ( LineM ` E )
itscnhlinecirc02p.d 
|- D = ( dist ` E )
Assertion itscnhlinecirc02plem3 
|- ( ( ( X e. P /\ Y e. P /\ ( X ` 1 ) =/= ( Y ` 1 ) ) /\ ( R e. RR+ /\ ( X D .0. ) < R ) ) -> 0 < ( ( -u ( 2 x. ( ( ( Y ` 0 ) - ( X ` 0 ) ) x. ( ( ( X ` 1 ) x. ( Y ` 0 ) ) - ( ( X ` 0 ) x. ( Y ` 1 ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( ( X ` 1 ) - ( Y ` 1 ) ) ^ 2 ) + ( ( ( Y ` 0 ) - ( X ` 0 ) ) ^ 2 ) ) x. ( ( ( ( ( X ` 1 ) x. ( Y ` 0 ) ) - ( ( X ` 0 ) x. ( Y ` 1 ) ) ) ^ 2 ) - ( ( ( ( X ` 1 ) - ( Y ` 1 ) ) ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) )

Proof

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