Metamath Proof Explorer

Theorem tgextale

Description: The non-strict exterior-angle bound, a checkpoint only. tgmircgra gives the reflected copy of the interior angle, tgextalem1inag puts that copy inside the exterior angle; inaglea turns "inside" into leA and leacgra1 transports the bound along the congruence (flipped with cgracom ). No new geometry. This bound is deliberately too weak for tgaas , whose contradiction branch already holds an angle congruence and so satisfies leA for free -- strictness comes later, and only tgexta is the exterior-angle theorem. (Contributed by JAG, 12-Aug-2026)

Ref Expression
Hypotheses tgextalem1inag.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
tgextalem1inag.m ⊢ − = ( dist ‘ 𝐺 )
tgextalem1inag.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
tgextalem1inag.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
tgextalem1inag.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
tgextalem1inag.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
tgextalem1inag.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
tgextalem1inag.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
tgextalem1inag.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
tgextalem1inag.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
tgextalem1inag.ext ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) )
tgextalem1inag.ncol ⊢ ( 𝜑 → ¬ ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
tgextalem1inag.ne ⊢ ( 𝜑 → 𝐶 ≠ 𝐷 )
Assertion tgextale ( 𝜑 → ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( ≤∠ ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ )

Proof

Step Hyp Ref Expression
1 tgextalem1inag.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 tgextalem1inag.m ⊢ − = ( dist ‘ 𝐺 )
3 tgextalem1inag.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 tgextalem1inag.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
5 tgextalem1inag.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
6 tgextalem1inag.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
7 tgextalem1inag.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
8 tgextalem1inag.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
9 tgextalem1inag.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
10 tgextalem1inag.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
11 tgextalem1inag.ext ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) )
12 tgextalem1inag.ncol ⊢ ( 𝜑 → ¬ ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
13 tgextalem1inag.ne ⊢ ( 𝜑 → 𝐶 ≠ 𝐷 )
14 eqid ⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
15 1 4 3 6 8 9 7 12 ncoltgdim2 ⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )
16 1 2 3 6 15 7 9 midcl ⊢ ( 𝜑 → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ∈ 𝑃 )
17 eqid ⊢ ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) = ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) )
18 1 2 3 4 14 6 16 17 8 mircl ⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ∈ 𝑃 )
19 1 2 3 4 5 6 7 8 9 10 11 12 13 tgextalem1inag ⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ( inA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ )
20 1 3 5 6 7 9 18 10 19 inaglea ⊢ ( 𝜑 → ⟨“ 𝐴 𝐶 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ”⟩ ( ≤∠ ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ )
21 1 2 3 4 6 7 8 9 12 tgmircgra ⊢ ( 𝜑 → ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ”⟩ )
22 1 3 6 5 9 7 8 7 9 18 21 cgracom ⊢ ( 𝜑 → ⟨“ 𝐴 𝐶 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐶 𝐴 𝐵 ”⟩ )
23 1 3 5 6 7 9 18 7 9 10 9 7 8 20 22 leacgra1 ⊢ ( 𝜑 → ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( ≤∠ ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ )