Metamath Proof Explorer

Theorem fta1lem

Description: Lemma for fta1 . (Contributed by Mario Carneiro, 26-Jul-2014)

Ref Expression
Hypotheses fta1.1 ⊢ 𝑅 = ( ◡ 𝐹 “ { 0 } )
fta1.2 ⊢ ( 𝜑 → 𝐷 ∈ ℕ0 )
fta1.3 ⊢ ( 𝜑 → 𝐹 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) )
fta1.4 ⊢ ( 𝜑 → ( deg ‘ 𝐹 ) = ( 𝐷 + 1 ) )
fta1.5 ⊢ ( 𝜑 → 𝐴 ∈ ( ◡ 𝐹 “ { 0 } ) )
fta1.6 ⊢ ( 𝜑 → ∀ 𝑔 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑔 ) = 𝐷 → ( ( ◡ 𝑔 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( ◡ 𝑔 “ { 0 } ) ) ≤ ( deg ‘ 𝑔 ) ) ) )
Assertion fta1lem ( 𝜑 → ( 𝑅 ∈ Fin ∧ ( ♯ ‘ 𝑅 ) ≤ ( deg ‘ 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 fta1.1 ⊢ 𝑅 = ( ◡ 𝐹 “ { 0 } )
2 fta1.2 ⊢ ( 𝜑 → 𝐷 ∈ ℕ0 )
3 fta1.3 ⊢ ( 𝜑 → 𝐹 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) )
4 fta1.4 ⊢ ( 𝜑 → ( deg ‘ 𝐹 ) = ( 𝐷 + 1 ) )
5 fta1.5 ⊢ ( 𝜑 → 𝐴 ∈ ( ◡ 𝐹 “ { 0 } ) )
6 fta1.6 ⊢ ( 𝜑 → ∀ 𝑔 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑔 ) = 𝐷 → ( ( ◡ 𝑔 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( ◡ 𝑔 “ { 0 } ) ) ≤ ( deg ‘ 𝑔 ) ) ) )
7 eldifsn ⊢ ( 𝐹 ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ↔ ( 𝐹 ∈ ( Poly ‘ ℂ ) ∧ 𝐹 ≠ 0𝑝 ) )
8 3 7 sylib ⊢ ( 𝜑 → ( 𝐹 ∈ ( Poly ‘ ℂ ) ∧ 𝐹 ≠ 0𝑝 ) )
9 8 simpld ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ ℂ ) )
10 plyf ⊢ ( 𝐹 ∈ ( Poly ‘ ℂ ) → 𝐹 : ℂ ⟶ ℂ )
11 ffn ⊢ ( 𝐹 : ℂ ⟶ ℂ → 𝐹 Fn ℂ )
12 fniniseg ⊢ ( 𝐹 Fn ℂ → ( 𝐴 ∈ ( ◡ 𝐹 “ { 0 } ) ↔ ( 𝐴 ∈ ℂ ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) ) )
13 9 10 11 12 4syl ⊢ ( 𝜑 → ( 𝐴 ∈ ( ◡ 𝐹 “ { 0 } ) ↔ ( 𝐴 ∈ ℂ ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) ) )
14 5 13 mpbid ⊢ ( 𝜑 → ( 𝐴 ∈ ℂ ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) )
15 14 simpld ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
16 14 simprd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = 0 )
17 eqid ⊢ ( Xp ∘f − ( ℂ × { 𝐴 } ) ) = ( Xp ∘f − ( ℂ × { 𝐴 } ) )
18 17 facth ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℂ ) ∧ 𝐴 ∈ ℂ ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) → 𝐹 = ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ∘f · ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ) )
19 9 15 16 18 syl3anc ⊢ ( 𝜑 → 𝐹 = ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ∘f · ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ) )
20 19 cnveqd ⊢ ( 𝜑 → ◡ 𝐹 = ◡ ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ∘f · ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ) )
21 20 imaeq1d ⊢ ( 𝜑 → ( ◡ 𝐹 “ { 0 } ) = ( ◡ ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ∘f · ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ) “ { 0 } ) )
22 cnex ⊢ ℂ ∈ V
23 22 a1i ⊢ ( 𝜑 → ℂ ∈ V )
24 ssid ⊢ ℂ ⊆ ℂ
25 ax-1cn ⊢ 1 ∈ ℂ
26 plyid ⊢ ( ( ℂ ⊆ ℂ ∧ 1 ∈ ℂ ) → Xp ∈ ( Poly ‘ ℂ ) )
27 24 25 26 mp2an ⊢ Xp ∈ ( Poly ‘ ℂ )
28 plyconst ⊢ ( ( ℂ ⊆ ℂ ∧ 𝐴 ∈ ℂ ) → ( ℂ × { 𝐴 } ) ∈ ( Poly ‘ ℂ ) )
29 24 15 28 sylancr ⊢ ( 𝜑 → ( ℂ × { 𝐴 } ) ∈ ( Poly ‘ ℂ ) )
30 plysubcl ⊢ ( ( Xp ∈ ( Poly ‘ ℂ ) ∧ ( ℂ × { 𝐴 } ) ∈ ( Poly ‘ ℂ ) ) → ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ∈ ( Poly ‘ ℂ ) )
31 27 29 30 sylancr ⊢ ( 𝜑 → ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ∈ ( Poly ‘ ℂ ) )
32 plyf ⊢ ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ∈ ( Poly ‘ ℂ ) → ( Xp ∘f − ( ℂ × { 𝐴 } ) ) : ℂ ⟶ ℂ )
33 31 32 syl ⊢ ( 𝜑 → ( Xp ∘f − ( ℂ × { 𝐴 } ) ) : ℂ ⟶ ℂ )
34 17 plyremlem ⊢ ( 𝐴 ∈ ℂ → ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) = 1 ∧ ( ◡ ( Xp ∘f − ( ℂ × { 𝐴 } ) ) “ { 0 } ) = { 𝐴 } ) )
35 15 34 syl ⊢ ( 𝜑 → ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) = 1 ∧ ( ◡ ( Xp ∘f − ( ℂ × { 𝐴 } ) ) “ { 0 } ) = { 𝐴 } ) )
36 35 simp2d ⊢ ( 𝜑 → ( deg ‘ ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) = 1 )
37 ax-1ne0 ⊢ 1 ≠ 0
38 37 a1i ⊢ ( 𝜑 → 1 ≠ 0 )
39 36 38 eqnetrd ⊢ ( 𝜑 → ( deg ‘ ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ≠ 0 )
40 fveq2 ⊢ ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) = 0𝑝 → ( deg ‘ ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) = ( deg ‘ 0𝑝 ) )
41 dgr0 ⊢ ( deg ‘ 0𝑝 ) = 0
42 40 41 eqtrdi ⊢ ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) = 0𝑝 → ( deg ‘ ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) = 0 )
43 42 necon3i ⊢ ( ( deg ‘ ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ≠ 0 → ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ≠ 0𝑝 )
44 39 43 syl ⊢ ( 𝜑 → ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ≠ 0𝑝 )
45 quotcl2 ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℂ ) ∧ ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ∈ ( Poly ‘ ℂ ) ∧ ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ≠ 0𝑝 ) → ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ∈ ( Poly ‘ ℂ ) )
46 9 31 44 45 syl3anc ⊢ ( 𝜑 → ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ∈ ( Poly ‘ ℂ ) )
47 plyf ⊢ ( ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ∈ ( Poly ‘ ℂ ) → ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) : ℂ ⟶ ℂ )
48 46 47 syl ⊢ ( 𝜑 → ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) : ℂ ⟶ ℂ )
49 ofmulrt ⊢ ( ( ℂ ∈ V ∧ ( Xp ∘f − ( ℂ × { 𝐴 } ) ) : ℂ ⟶ ℂ ∧ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) : ℂ ⟶ ℂ ) → ( ◡ ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ∘f · ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ) “ { 0 } ) = ( ( ◡ ( Xp ∘f − ( ℂ × { 𝐴 } ) ) “ { 0 } ) ∪ ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) )
50 23 33 48 49 syl3anc ⊢ ( 𝜑 → ( ◡ ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ∘f · ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ) “ { 0 } ) = ( ( ◡ ( Xp ∘f − ( ℂ × { 𝐴 } ) ) “ { 0 } ) ∪ ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) )
51 35 simp3d ⊢ ( 𝜑 → ( ◡ ( Xp ∘f − ( ℂ × { 𝐴 } ) ) “ { 0 } ) = { 𝐴 } )
52 51 uneq1d ⊢ ( 𝜑 → ( ( ◡ ( Xp ∘f − ( ℂ × { 𝐴 } ) ) “ { 0 } ) ∪ ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) = ( { 𝐴 } ∪ ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) )
53 21 50 52 3eqtrd ⊢ ( 𝜑 → ( ◡ 𝐹 “ { 0 } ) = ( { 𝐴 } ∪ ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) )
54 uncom ⊢ ( ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∪ { 𝐴 } ) = ( { 𝐴 } ∪ ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) )
55 53 1 54 3eqtr4g ⊢ ( 𝜑 → 𝑅 = ( ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∪ { 𝐴 } ) )
56 25 a1i ⊢ ( 𝜑 → 1 ∈ ℂ )
57 dgrcl ⊢ ( ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ∈ ( Poly ‘ ℂ ) → ( deg ‘ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ) ∈ ℕ0 )
58 46 57 syl ⊢ ( 𝜑 → ( deg ‘ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ) ∈ ℕ0 )
59 58 nn0cnd ⊢ ( 𝜑 → ( deg ‘ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ) ∈ ℂ )
60 2 nn0cnd ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
61 addcom ⊢ ( ( 1 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( 1 + 𝐷 ) = ( 𝐷 + 1 ) )
62 25 60 61 sylancr ⊢ ( 𝜑 → ( 1 + 𝐷 ) = ( 𝐷 + 1 ) )
63 19 fveq2d ⊢ ( 𝜑 → ( deg ‘ 𝐹 ) = ( deg ‘ ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ∘f · ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ) ) )
64 8 simprd ⊢ ( 𝜑 → 𝐹 ≠ 0𝑝 )
65 19 eqcomd ⊢ ( 𝜑 → ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ∘f · ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ) = 𝐹 )
66 0cnd ⊢ ( 𝜑 → 0 ∈ ℂ )
67 mul01 ⊢ ( 𝑥 ∈ ℂ → ( 𝑥 · 0 ) = 0 )
68 67 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝑥 · 0 ) = 0 )
69 23 33 66 66 68 caofid1 ⊢ ( 𝜑 → ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ∘f · ( ℂ × { 0 } ) ) = ( ℂ × { 0 } ) )
70 df-0p ⊢ 0𝑝 = ( ℂ × { 0 } )
71 70 oveq2i ⊢ ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ∘f · 0𝑝 ) = ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ∘f · ( ℂ × { 0 } ) )
72 69 71 70 3eqtr4g ⊢ ( 𝜑 → ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ∘f · 0𝑝 ) = 0𝑝 )
73 64 65 72 3netr4d ⊢ ( 𝜑 → ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ∘f · ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ) ≠ ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ∘f · 0𝑝 ) )
74 oveq2 ⊢ ( ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) = 0𝑝 → ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ∘f · ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ) = ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ∘f · 0𝑝 ) )
75 74 necon3i ⊢ ( ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ∘f · ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ) ≠ ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ∘f · 0𝑝 ) → ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ≠ 0𝑝 )
76 73 75 syl ⊢ ( 𝜑 → ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ≠ 0𝑝 )
77 eqid ⊢ ( deg ‘ ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) = ( deg ‘ ( Xp ∘f − ( ℂ × { 𝐴 } ) ) )
78 eqid ⊢ ( deg ‘ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ) = ( deg ‘ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) )
79 77 78 dgrmul ⊢ ( ( ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ∈ ( Poly ‘ ℂ ) ∧ ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ≠ 0𝑝 ) ∧ ( ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ∈ ( Poly ‘ ℂ ) ∧ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ≠ 0𝑝 ) ) → ( deg ‘ ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ∘f · ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ) ) = ( ( deg ‘ ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) + ( deg ‘ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ) ) )
80 31 44 46 76 79 syl22anc ⊢ ( 𝜑 → ( deg ‘ ( ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ∘f · ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ) ) = ( ( deg ‘ ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) + ( deg ‘ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ) ) )
81 63 4 80 3eqtr3d ⊢ ( 𝜑 → ( 𝐷 + 1 ) = ( ( deg ‘ ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) + ( deg ‘ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ) ) )
82 36 oveq1d ⊢ ( 𝜑 → ( ( deg ‘ ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) + ( deg ‘ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ) ) = ( 1 + ( deg ‘ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ) ) )
83 62 81 82 3eqtrrd ⊢ ( 𝜑 → ( 1 + ( deg ‘ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ) ) = ( 1 + 𝐷 ) )
84 56 59 60 83 addcanad ⊢ ( 𝜑 → ( deg ‘ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ) = 𝐷 )
85 fveqeq2 ⊢ ( 𝑔 = ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) → ( ( deg ‘ 𝑔 ) = 𝐷 ↔ ( deg ‘ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ) = 𝐷 ) )
86 cnveq ⊢ ( 𝑔 = ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) → ◡ 𝑔 = ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) )
87 86 imaeq1d ⊢ ( 𝑔 = ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) → ( ◡ 𝑔 “ { 0 } ) = ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) )
88 87 eleq1d ⊢ ( 𝑔 = ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) → ( ( ◡ 𝑔 “ { 0 } ) ∈ Fin ↔ ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∈ Fin ) )
89 87 fveq2d ⊢ ( 𝑔 = ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) → ( ♯ ‘ ( ◡ 𝑔 “ { 0 } ) ) = ( ♯ ‘ ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) )
90 fveq2 ⊢ ( 𝑔 = ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) → ( deg ‘ 𝑔 ) = ( deg ‘ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ) )
91 89 90 breq12d ⊢ ( 𝑔 = ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) → ( ( ♯ ‘ ( ◡ 𝑔 “ { 0 } ) ) ≤ ( deg ‘ 𝑔 ) ↔ ( ♯ ‘ ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) ≤ ( deg ‘ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ) ) )
92 88 91 anbi12d ⊢ ( 𝑔 = ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) → ( ( ( ◡ 𝑔 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( ◡ 𝑔 “ { 0 } ) ) ≤ ( deg ‘ 𝑔 ) ) ↔ ( ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) ≤ ( deg ‘ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ) ) ) )
93 85 92 imbi12d ⊢ ( 𝑔 = ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) → ( ( ( deg ‘ 𝑔 ) = 𝐷 → ( ( ◡ 𝑔 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( ◡ 𝑔 “ { 0 } ) ) ≤ ( deg ‘ 𝑔 ) ) ) ↔ ( ( deg ‘ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ) = 𝐷 → ( ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) ≤ ( deg ‘ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ) ) ) ) )
94 eldifsn ⊢ ( ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) ↔ ( ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ∈ ( Poly ‘ ℂ ) ∧ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ≠ 0𝑝 ) )
95 46 76 94 sylanbrc ⊢ ( 𝜑 → ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ∈ ( ( Poly ‘ ℂ ) ∖ { 0𝑝 } ) )
96 93 6 95 rspcdva ⊢ ( 𝜑 → ( ( deg ‘ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ) = 𝐷 → ( ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) ≤ ( deg ‘ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ) ) ) )
97 84 96 mpd ⊢ ( 𝜑 → ( ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) ≤ ( deg ‘ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ) ) )
98 97 simpld ⊢ ( 𝜑 → ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∈ Fin )
99 snfi ⊢ { 𝐴 } ∈ Fin
100 unfi ⊢ ( ( ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∈ Fin ∧ { 𝐴 } ∈ Fin ) → ( ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∪ { 𝐴 } ) ∈ Fin )
101 98 99 100 sylancl ⊢ ( 𝜑 → ( ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∪ { 𝐴 } ) ∈ Fin )
102 55 101 eqeltrd ⊢ ( 𝜑 → 𝑅 ∈ Fin )
103 55 fveq2d ⊢ ( 𝜑 → ( ♯ ‘ 𝑅 ) = ( ♯ ‘ ( ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∪ { 𝐴 } ) ) )
104 hashcl ⊢ ( ( ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∪ { 𝐴 } ) ∈ Fin → ( ♯ ‘ ( ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∪ { 𝐴 } ) ) ∈ ℕ0 )
105 101 104 syl ⊢ ( 𝜑 → ( ♯ ‘ ( ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∪ { 𝐴 } ) ) ∈ ℕ0 )
106 105 nn0red ⊢ ( 𝜑 → ( ♯ ‘ ( ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∪ { 𝐴 } ) ) ∈ ℝ )
107 hashcl ⊢ ( ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∈ Fin → ( ♯ ‘ ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) ∈ ℕ0 )
108 98 107 syl ⊢ ( 𝜑 → ( ♯ ‘ ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) ∈ ℕ0 )
109 108 nn0red ⊢ ( 𝜑 → ( ♯ ‘ ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) ∈ ℝ )
110 peano2re ⊢ ( ( ♯ ‘ ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) ∈ ℝ → ( ( ♯ ‘ ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) + 1 ) ∈ ℝ )
111 109 110 syl ⊢ ( 𝜑 → ( ( ♯ ‘ ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) + 1 ) ∈ ℝ )
112 dgrcl ⊢ ( 𝐹 ∈ ( Poly ‘ ℂ ) → ( deg ‘ 𝐹 ) ∈ ℕ0 )
113 9 112 syl ⊢ ( 𝜑 → ( deg ‘ 𝐹 ) ∈ ℕ0 )
114 113 nn0red ⊢ ( 𝜑 → ( deg ‘ 𝐹 ) ∈ ℝ )
115 hashun2 ⊢ ( ( ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∈ Fin ∧ { 𝐴 } ∈ Fin ) → ( ♯ ‘ ( ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∪ { 𝐴 } ) ) ≤ ( ( ♯ ‘ ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) + ( ♯ ‘ { 𝐴 } ) ) )
116 98 99 115 sylancl ⊢ ( 𝜑 → ( ♯ ‘ ( ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∪ { 𝐴 } ) ) ≤ ( ( ♯ ‘ ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) + ( ♯ ‘ { 𝐴 } ) ) )
117 hashsng ⊢ ( 𝐴 ∈ ℂ → ( ♯ ‘ { 𝐴 } ) = 1 )
118 15 117 syl ⊢ ( 𝜑 → ( ♯ ‘ { 𝐴 } ) = 1 )
119 118 oveq2d ⊢ ( 𝜑 → ( ( ♯ ‘ ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) + ( ♯ ‘ { 𝐴 } ) ) = ( ( ♯ ‘ ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) + 1 ) )
120 116 119 breqtrd ⊢ ( 𝜑 → ( ♯ ‘ ( ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∪ { 𝐴 } ) ) ≤ ( ( ♯ ‘ ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) + 1 ) )
121 2 nn0red ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
122 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
123 97 simprd ⊢ ( 𝜑 → ( ♯ ‘ ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) ≤ ( deg ‘ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) ) )
124 123 84 breqtrd ⊢ ( 𝜑 → ( ♯ ‘ ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) ≤ 𝐷 )
125 109 121 122 124 leadd1dd ⊢ ( 𝜑 → ( ( ♯ ‘ ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) + 1 ) ≤ ( 𝐷 + 1 ) )
126 125 4 breqtrrd ⊢ ( 𝜑 → ( ( ♯ ‘ ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ) + 1 ) ≤ ( deg ‘ 𝐹 ) )
127 106 111 114 120 126 letrd ⊢ ( 𝜑 → ( ♯ ‘ ( ( ◡ ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ) “ { 0 } ) ∪ { 𝐴 } ) ) ≤ ( deg ‘ 𝐹 ) )
128 103 127 eqbrtrd ⊢ ( 𝜑 → ( ♯ ‘ 𝑅 ) ≤ ( deg ‘ 𝐹 ) )
129 102 128 jca ⊢ ( 𝜑 → ( 𝑅 ∈ Fin ∧ ( ♯ ‘ 𝑅 ) ≤ ( deg ‘ 𝐹 ) ) )