Step | Hyp | Ref
| Expression |
1 | | inlinecirc02p.p |
. . . 4
β’ π = (β βm
πΌ) |
2 | 1 | ovexi 7337 |
. . 3
β’ π β V |
3 | 2 | a1i 11 |
. 2
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ (ππ· 0 ) < π
)) β π β V) |
4 | | simpl 484 |
. . 3
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ (ππ· 0 ) < π
)) β (π β π β§ π β π β§ π β π)) |
5 | | simpl 484 |
. . . 4
β’ ((π
β β+
β§ (ππ· 0 ) < π
) β π
β
β+) |
6 | 5 | adantl 483 |
. . 3
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ (ππ· 0 ) < π
)) β π
β
β+) |
7 | | inlinecirc02p.i |
. . . . . . . 8
β’ πΌ = {1, 2} |
8 | 7, 1 | rrx2pxel 46114 |
. . . . . . 7
β’ (π β π β (πβ1) β β) |
9 | 8 | 3ad2ant1 1133 |
. . . . . 6
β’ ((π β π β§ π β π β§ π β π) β (πβ1) β β) |
10 | 9 | adantr 482 |
. . . . 5
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ (ππ· 0 ) < π
)) β (πβ1) β β) |
11 | 7, 1 | rrx2pyel 46115 |
. . . . . . 7
β’ (π β π β (πβ2) β β) |
12 | 11 | 3ad2ant1 1133 |
. . . . . 6
β’ ((π β π β§ π β π β§ π β π) β (πβ2) β β) |
13 | 12 | adantr 482 |
. . . . 5
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ (ππ· 0 ) < π
)) β (πβ2) β β) |
14 | 7, 1 | rrx2pxel 46114 |
. . . . . . 7
β’ (π β π β (πβ1) β β) |
15 | 14 | 3ad2ant2 1134 |
. . . . . 6
β’ ((π β π β§ π β π β§ π β π) β (πβ1) β β) |
16 | 15 | adantr 482 |
. . . . 5
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ (ππ· 0 ) < π
)) β (πβ1) β β) |
17 | 7, 1 | rrx2pyel 46115 |
. . . . . . 7
β’ (π β π β (πβ2) β β) |
18 | 17 | 3ad2ant2 1134 |
. . . . . 6
β’ ((π β π β§ π β π β§ π β π) β (πβ2) β β) |
19 | 18 | adantr 482 |
. . . . 5
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ (ππ· 0 ) < π
)) β (πβ2) β β) |
20 | | eqid 2736 |
. . . . 5
β’ ((πβ1) β (πβ1)) = ((πβ1) β (πβ1)) |
21 | | eqid 2736 |
. . . . 5
β’ ((πβ2) β (πβ2)) = ((πβ2) β (πβ2)) |
22 | | eqid 2736 |
. . . . 5
β’ ((((πβ1) β (πβ1)) Β· (πβ2)) + (((πβ2) β (πβ2)) Β· (πβ1))) = ((((πβ1) β (πβ1)) Β· (πβ2)) + (((πβ2) β (πβ2)) Β· (πβ1))) |
23 | | rpre 12780 |
. . . . . . 7
β’ (π
β β+
β π
β
β) |
24 | 23 | adantr 482 |
. . . . . 6
β’ ((π
β β+
β§ (ππ· 0 ) < π
) β π
β β) |
25 | 24 | adantl 483 |
. . . . 5
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ (ππ· 0 ) < π
)) β π
β β) |
26 | | inlinecirc02p.e |
. . . . . . . . . 10
β’ πΈ = (β^βπΌ) |
27 | | 2nn0 12292 |
. . . . . . . . . . . 12
β’ 2 β
β0 |
28 | | eqid 2736 |
. . . . . . . . . . . . 13
β’
(πΌhilβ2) =
(πΌhilβ2) |
29 | 28 | ehlval 24619 |
. . . . . . . . . . . 12
β’ (2 β
β0 β (πΌhilβ2) =
(β^β(1...2))) |
30 | 27, 29 | ax-mp 5 |
. . . . . . . . . . 11
β’
(πΌhilβ2) =
(β^β(1...2)) |
31 | | fz12pr 13355 |
. . . . . . . . . . . . 13
β’ (1...2) =
{1, 2} |
32 | 31, 7 | eqtr4i 2767 |
. . . . . . . . . . . 12
β’ (1...2) =
πΌ |
33 | 32 | fveq2i 6803 |
. . . . . . . . . . 11
β’
(β^β(1...2)) = (β^βπΌ) |
34 | 30, 33 | eqtri 2764 |
. . . . . . . . . 10
β’
(πΌhilβ2) = (β^βπΌ) |
35 | 26, 34 | eqtr4i 2767 |
. . . . . . . . 9
β’ πΈ =
(πΌhilβ2) |
36 | 7 | oveq2i 7314 |
. . . . . . . . . 10
β’ (β
βm πΌ) =
(β βm {1, 2}) |
37 | 1, 36 | eqtri 2764 |
. . . . . . . . 9
β’ π = (β βm
{1, 2}) |
38 | | inlinecirc02p.d |
. . . . . . . . 9
β’ π· = (distβπΈ) |
39 | | inlinecirc02p.0 |
. . . . . . . . . 10
β’ 0 = (πΌ Γ {0}) |
40 | 7 | xpeq1i 5622 |
. . . . . . . . . 10
β’ (πΌ Γ {0}) = ({1, 2} Γ
{0}) |
41 | 39, 40 | eqtri 2764 |
. . . . . . . . 9
β’ 0 = ({1, 2}
Γ {0}) |
42 | 35, 37, 38, 41 | ehl2eudis0lt 46129 |
. . . . . . . 8
β’ ((π β π β§ π
β β+) β ((ππ· 0 ) < π
β (((πβ1)β2) + ((πβ2)β2)) < (π
β2))) |
43 | 42 | 3ad2antl1 1185 |
. . . . . . 7
β’ (((π β π β§ π β π β§ π β π) β§ π
β β+) β ((ππ· 0 ) < π
β (((πβ1)β2) + ((πβ2)β2)) < (π
β2))) |
44 | 43 | biimpd 228 |
. . . . . 6
β’ (((π β π β§ π β π β§ π β π) β§ π
β β+) β ((ππ· 0 ) < π
β (((πβ1)β2) + ((πβ2)β2)) < (π
β2))) |
45 | 44 | impr 456 |
. . . . 5
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ (ππ· 0 ) < π
)) β (((πβ1)β2) + ((πβ2)β2)) < (π
β2)) |
46 | 7, 1 | rrx2pnecoorneor 46118 |
. . . . . . 7
β’ ((π β π β§ π β π β§ π β π) β ((πβ1) β (πβ1) β¨ (πβ2) β (πβ2))) |
47 | 46 | orcomd 869 |
. . . . . 6
β’ ((π β π β§ π β π β§ π β π) β ((πβ2) β (πβ2) β¨ (πβ1) β (πβ1))) |
48 | 47 | adantr 482 |
. . . . 5
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ (ππ· 0 ) < π
)) β ((πβ2) β (πβ2) β¨ (πβ1) β (πβ1))) |
49 | | eqid 2736 |
. . . . 5
β’ ((((πβ2) β (πβ2))β2) + (((πβ1) β (πβ1))β2)) = ((((πβ2) β (πβ2))β2) + (((πβ1) β (πβ1))β2)) |
50 | | eqid 2736 |
. . . . 5
β’ (((π
β2) Β· ((((πβ2) β (πβ2))β2) + (((πβ1) β (πβ1))β2))) β
(((((πβ1) β
(πβ1)) Β·
(πβ2)) + (((πβ2) β (πβ2)) Β· (πβ1)))β2)) = (((π
β2) Β· ((((πβ2) β (πβ2))β2) + (((πβ1) β (πβ1))β2))) β
(((((πβ1) β
(πβ1)) Β·
(πβ2)) + (((πβ2) β (πβ2)) Β· (πβ1)))β2)) |
51 | 10, 13, 16, 19, 20, 21, 22, 25, 45, 48, 49, 50 | 2itscp 46184 |
. . . 4
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ (ππ· 0 ) < π
)) β 0 < (((π
β2) Β· ((((πβ2) β (πβ2))β2) + (((πβ1) β (πβ1))β2))) β (((((πβ1) β (πβ1)) Β· (πβ2)) + (((πβ2) β (πβ2)) Β· (πβ1)))β2))) |
52 | 14 | recnd 11045 |
. . . . . . . . . . . . 13
β’ (π β π β (πβ1) β β) |
53 | 52 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β π β§ π β π) β (πβ1) β β) |
54 | 8 | recnd 11045 |
. . . . . . . . . . . . 13
β’ (π β π β (πβ1) β β) |
55 | 54 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β π β§ π β π) β (πβ1) β β) |
56 | 11 | recnd 11045 |
. . . . . . . . . . . . 13
β’ (π β π β (πβ2) β β) |
57 | 56 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β π β§ π β π) β (πβ2) β β) |
58 | 53, 55, 57 | subdird 11474 |
. . . . . . . . . . 11
β’ ((π β π β§ π β π) β (((πβ1) β (πβ1)) Β· (πβ2)) = (((πβ1) Β· (πβ2)) β ((πβ1) Β· (πβ2)))) |
59 | 17 | recnd 11045 |
. . . . . . . . . . . . 13
β’ (π β π β (πβ2) β β) |
60 | 59 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β π β§ π β π) β (πβ2) β β) |
61 | 57, 60, 55 | subdird 11474 |
. . . . . . . . . . 11
β’ ((π β π β§ π β π) β (((πβ2) β (πβ2)) Β· (πβ1)) = (((πβ2) Β· (πβ1)) β ((πβ2) Β· (πβ1)))) |
62 | 58, 61 | oveq12d 7321 |
. . . . . . . . . 10
β’ ((π β π β§ π β π) β ((((πβ1) β (πβ1)) Β· (πβ2)) + (((πβ2) β (πβ2)) Β· (πβ1))) = ((((πβ1) Β· (πβ2)) β ((πβ1) Β· (πβ2))) + (((πβ2) Β· (πβ1)) β ((πβ2) Β· (πβ1))))) |
63 | 53, 57 | mulcomd 11038 |
. . . . . . . . . . . 12
β’ ((π β π β§ π β π) β ((πβ1) Β· (πβ2)) = ((πβ2) Β· (πβ1))) |
64 | 63 | oveq1d 7318 |
. . . . . . . . . . 11
β’ ((π β π β§ π β π) β (((πβ1) Β· (πβ2)) β ((πβ1) Β· (πβ2))) = (((πβ2) Β· (πβ1)) β ((πβ1) Β· (πβ2)))) |
65 | 57, 55 | mulcomd 11038 |
. . . . . . . . . . . 12
β’ ((π β π β§ π β π) β ((πβ2) Β· (πβ1)) = ((πβ1) Β· (πβ2))) |
66 | 60, 55 | mulcomd 11038 |
. . . . . . . . . . . 12
β’ ((π β π β§ π β π) β ((πβ2) Β· (πβ1)) = ((πβ1) Β· (πβ2))) |
67 | 65, 66 | oveq12d 7321 |
. . . . . . . . . . 11
β’ ((π β π β§ π β π) β (((πβ2) Β· (πβ1)) β ((πβ2) Β· (πβ1))) = (((πβ1) Β· (πβ2)) β ((πβ1) Β· (πβ2)))) |
68 | 64, 67 | oveq12d 7321 |
. . . . . . . . . 10
β’ ((π β π β§ π β π) β ((((πβ1) Β· (πβ2)) β ((πβ1) Β· (πβ2))) + (((πβ2) Β· (πβ1)) β ((πβ2) Β· (πβ1)))) = ((((πβ2) Β· (πβ1)) β ((πβ1) Β· (πβ2))) + (((πβ1) Β· (πβ2)) β ((πβ1) Β· (πβ2))))) |
69 | 57, 53 | mulcld 11037 |
. . . . . . . . . . 11
β’ ((π β π β§ π β π) β ((πβ2) Β· (πβ1)) β β) |
70 | 55, 57 | mulcld 11037 |
. . . . . . . . . . 11
β’ ((π β π β§ π β π) β ((πβ1) Β· (πβ2)) β β) |
71 | 55, 60 | mulcld 11037 |
. . . . . . . . . . 11
β’ ((π β π β§ π β π) β ((πβ1) Β· (πβ2)) β β) |
72 | 69, 70, 71 | npncand 11398 |
. . . . . . . . . 10
β’ ((π β π β§ π β π) β ((((πβ2) Β· (πβ1)) β ((πβ1) Β· (πβ2))) + (((πβ1) Β· (πβ2)) β ((πβ1) Β· (πβ2)))) = (((πβ2) Β· (πβ1)) β ((πβ1) Β· (πβ2)))) |
73 | 62, 68, 72 | 3eqtrd 2780 |
. . . . . . . . 9
β’ ((π β π β§ π β π) β ((((πβ1) β (πβ1)) Β· (πβ2)) + (((πβ2) β (πβ2)) Β· (πβ1))) = (((πβ2) Β· (πβ1)) β ((πβ1) Β· (πβ2)))) |
74 | 73 | 3adant3 1132 |
. . . . . . . 8
β’ ((π β π β§ π β π β§ π β π) β ((((πβ1) β (πβ1)) Β· (πβ2)) + (((πβ2) β (πβ2)) Β· (πβ1))) = (((πβ2) Β· (πβ1)) β ((πβ1) Β· (πβ2)))) |
75 | 74 | adantr 482 |
. . . . . . 7
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ (ππ· 0 ) < π
)) β ((((πβ1) β (πβ1)) Β· (πβ2)) + (((πβ2) β (πβ2)) Β· (πβ1))) = (((πβ2) Β· (πβ1)) β ((πβ1) Β· (πβ2)))) |
76 | 75 | eqcomd 2742 |
. . . . . 6
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ (ππ· 0 ) < π
)) β (((πβ2) Β· (πβ1)) β ((πβ1) Β· (πβ2))) = ((((πβ1) β (πβ1)) Β· (πβ2)) + (((πβ2) β (πβ2)) Β· (πβ1)))) |
77 | 76 | oveq1d 7318 |
. . . . 5
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ (ππ· 0 ) < π
)) β ((((πβ2) Β· (πβ1)) β ((πβ1) Β· (πβ2)))β2) = (((((πβ1) β (πβ1)) Β· (πβ2)) + (((πβ2) β (πβ2)) Β· (πβ1)))β2)) |
78 | 77 | oveq2d 7319 |
. . . 4
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ (ππ· 0 ) < π
)) β (((π
β2) Β· ((((πβ2) β (πβ2))β2) + (((πβ1) β (πβ1))β2))) β ((((πβ2) Β· (πβ1)) β ((πβ1) Β· (πβ2)))β2)) = (((π
β2) Β· ((((πβ2) β (πβ2))β2) + (((πβ1) β (πβ1))β2))) β
(((((πβ1) β
(πβ1)) Β·
(πβ2)) + (((πβ2) β (πβ2)) Β· (πβ1)))β2))) |
79 | 51, 78 | breqtrrd 5109 |
. . 3
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ (ππ· 0 ) < π
)) β 0 < (((π
β2) Β· ((((πβ2) β (πβ2))β2) + (((πβ1) β (πβ1))β2))) β ((((πβ2) Β· (πβ1)) β ((πβ1) Β· (πβ2)))β2))) |
80 | | inlinecirc02p.s |
. . . 4
β’ π = (SphereβπΈ) |
81 | | inlinecirc02p.l |
. . . 4
β’ πΏ = (LineMβπΈ) |
82 | | eqid 2736 |
. . . 4
β’ (((π
β2) Β· ((((πβ2) β (πβ2))β2) + (((πβ1) β (πβ1))β2))) β
((((πβ2) Β·
(πβ1)) β
((πβ1) Β·
(πβ2)))β2)) =
(((π
β2) Β·
((((πβ2) β
(πβ2))β2) +
(((πβ1) β
(πβ1))β2)))
β ((((πβ2)
Β· (πβ1))
β ((πβ1)
Β· (πβ2)))β2)) |
83 | | eqid 2736 |
. . . 4
β’ (((πβ2) Β· (πβ1)) β ((πβ1) Β· (πβ2))) = (((πβ2) Β· (πβ1)) β ((πβ1) Β· (πβ2))) |
84 | 7, 26, 1, 80, 39, 81, 49, 82, 21, 20, 83 | inlinecirc02plem 46189 |
. . 3
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ 0 <
(((π
β2) Β·
((((πβ2) β
(πβ2))β2) +
(((πβ1) β
(πβ1))β2)))
β ((((πβ2)
Β· (πβ1))
β ((πβ1)
Β· (πβ2)))β2)))) β βπ β π βπ β π ((( 0 ππ
) β© (ππΏπ)) = {π, π} β§ π β π)) |
85 | 4, 6, 79, 84 | syl12anc 835 |
. 2
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ (ππ· 0 ) < π
)) β βπ β π βπ β π ((( 0 ππ
) β© (ππΏπ)) = {π, π} β§ π β π)) |
86 | | prprelprb 45026 |
. 2
β’ ((( 0 ππ
) β© (ππΏπ)) β
(Pairsproperβπ) β (π β V β§ βπ β π βπ β π ((( 0 ππ
) β© (ππΏπ)) = {π, π} β§ π β π))) |
87 | 3, 85, 86 | sylanbrc 584 |
1
β’ (((π β π β§ π β π β§ π β π) β§ (π
β β+ β§ (ππ· 0 ) < π
)) β (( 0 ππ
) β© (ππΏπ)) β
(Pairsproperβπ)) |