Metamath Proof Explorer

Theorem aalioulem2

Description: Lemma for aaliou . (Contributed by Stefan O'Rear, 15-Nov-2014) (Proof shortened by AV, 28-Sep-2020)

Ref Expression
Hypotheses aalioulem2.a ⊢N=deg⁡F
aalioulem2.b ⊢φ→F∈Poly⁡ℤ
aalioulem2.c ⊢φ→N∈ℕ
aalioulem2.d ⊢φ→A∈ℝ
Assertion aalioulem2 ⊢φ→∃x∈ℝ+∀p∈ℤ∀q∈ℕF⁡pq=0→A=pq∨xqN≤A−pq

Proof

Step Hyp Ref Expression
1 aalioulem2.a ⊢N=deg⁡F
2 aalioulem2.b ⊢φ→F∈Poly⁡ℤ
3 aalioulem2.c ⊢φ→N∈ℕ
4 aalioulem2.d ⊢φ→A∈ℝ
5 1rp ⊢1∈ℝ+
6 snssi ⊢1∈ℝ+→1⊆ℝ+
7 5 6 ax-mp ⊢1⊆ℝ+
8 ssrab2 ⊢a∈ℝ+|∃b∈F-10a=A−b⊆ℝ+
9 7 8 unssi ⊢1∪a∈ℝ+|∃b∈F-10a=A−b⊆ℝ+
10 ltso ⊢<Orℝ
11 10 a1i ⊢φ→<Orℝ
12 snfi ⊢1∈Fin
13 3 nnne0d ⊢φ→N≠0
14 1 eqcomi ⊢deg⁡F=N
15 dgr0 ⊢deg⁡0𝑝=0
16 13 14 15 3netr4g ⊢φ→deg⁡F≠deg⁡0𝑝
17 fveq2 ⊢F=0𝑝→deg⁡F=deg⁡0𝑝
18 17 necon3i ⊢deg⁡F≠deg⁡0𝑝→F≠0𝑝
19 16 18 syl ⊢φ→F≠0𝑝
20 eqid ⊢F-10=F-10
21 20 fta1 ⊢F∈Poly⁡ℤ∧F≠0𝑝→F-10∈Fin∧F-10≤deg⁡F
22 2 19 21 syl2anc ⊢φ→F-10∈Fin∧F-10≤deg⁡F
23 22 simpld ⊢φ→F-10∈Fin
24 abrexfi ⊢F-10∈Fin→a|∃b∈F-10a=A−b∈Fin
25 23 24 syl ⊢φ→a|∃b∈F-10a=A−b∈Fin
26 rabssab ⊢a∈ℝ+|∃b∈F-10a=A−b⊆a|∃b∈F-10a=A−b
27 ssfi ⊢a|∃b∈F-10a=A−b∈Fin∧a∈ℝ+|∃b∈F-10a=A−b⊆a|∃b∈F-10a=A−b→a∈ℝ+|∃b∈F-10a=A−b∈Fin
28 25 26 27 sylancl ⊢φ→a∈ℝ+|∃b∈F-10a=A−b∈Fin
29 unfi ⊢1∈Fin∧a∈ℝ+|∃b∈F-10a=A−b∈Fin→1∪a∈ℝ+|∃b∈F-10a=A−b∈Fin
30 12 28 29 sylancr ⊢φ→1∪a∈ℝ+|∃b∈F-10a=A−b∈Fin
31 1ex ⊢1∈V
32 31 snid ⊢1∈1
33 elun1 ⊢1∈1→1∈1∪a∈ℝ+|∃b∈F-10a=A−b
34 ne0i ⊢1∈1∪a∈ℝ+|∃b∈F-10a=A−b→1∪a∈ℝ+|∃b∈F-10a=A−b≠∅
35 32 33 34 mp2b ⊢1∪a∈ℝ+|∃b∈F-10a=A−b≠∅
36 35 a1i ⊢φ→1∪a∈ℝ+|∃b∈F-10a=A−b≠∅
37 rpssre ⊢ℝ+⊆ℝ
38 9 37 sstri ⊢1∪a∈ℝ+|∃b∈F-10a=A−b⊆ℝ
39 38 a1i ⊢φ→1∪a∈ℝ+|∃b∈F-10a=A−b⊆ℝ
40 fiinfcl ⊢<Orℝ∧1∪a∈ℝ+|∃b∈F-10a=A−b∈Fin∧1∪a∈ℝ+|∃b∈F-10a=A−b≠∅∧1∪a∈ℝ+|∃b∈F-10a=A−b⊆ℝ→sup1∪a∈ℝ+|∃b∈F-10a=A−bℝ<∈1∪a∈ℝ+|∃b∈F-10a=A−b
41 11 30 36 39 40 syl13anc ⊢φ→sup1∪a∈ℝ+|∃b∈F-10a=A−bℝ<∈1∪a∈ℝ+|∃b∈F-10a=A−b
42 9 41 sselid ⊢φ→sup1∪a∈ℝ+|∃b∈F-10a=A−bℝ<∈ℝ+
43 0re ⊢0∈ℝ
44 rpge0 ⊢d∈ℝ+→0≤d
45 44 rgen ⊢∀d∈ℝ+0≤d
46 breq1 ⊢c=0→c≤d↔0≤d
47 46 ralbidv ⊢c=0→∀d∈ℝ+c≤d↔∀d∈ℝ+0≤d
48 47 rspcev ⊢0∈ℝ∧∀d∈ℝ+0≤d→∃c∈ℝ∀d∈ℝ+c≤d
49 43 45 48 mp2an ⊢∃c∈ℝ∀d∈ℝ+c≤d
50 ssralv ⊢1∪a∈ℝ+|∃b∈F-10a=A−b⊆ℝ+→∀d∈ℝ+c≤d→∀d∈1∪a∈ℝ+|∃b∈F-10a=A−bc≤d
51 9 50 ax-mp ⊢∀d∈ℝ+c≤d→∀d∈1∪a∈ℝ+|∃b∈F-10a=A−bc≤d
52 51 reximi ⊢∃c∈ℝ∀d∈ℝ+c≤d→∃c∈ℝ∀d∈1∪a∈ℝ+|∃b∈F-10a=A−bc≤d
53 49 52 ax-mp ⊢∃c∈ℝ∀d∈1∪a∈ℝ+|∃b∈F-10a=A−bc≤d
54 eqeq1 ⊢a=A−r→a=A−b↔A−r=A−b
55 54 rexbidv ⊢a=A−r→∃b∈F-10a=A−b↔∃b∈F-10A−r=A−b
56 4 ad2antrr ⊢φ∧r∈ℝ∧F⁡r=0∧¬A=r→A∈ℝ
57 simplr ⊢φ∧r∈ℝ∧F⁡r=0∧¬A=r→r∈ℝ
58 56 57 resubcld ⊢φ∧r∈ℝ∧F⁡r=0∧¬A=r→A−r∈ℝ
59 58 recnd ⊢φ∧r∈ℝ∧F⁡r=0∧¬A=r→A−r∈ℂ
60 4 ad2antrr ⊢φ∧r∈ℝ∧F⁡r=0→A∈ℝ
61 60 recnd ⊢φ∧r∈ℝ∧F⁡r=0→A∈ℂ
62 simplr ⊢φ∧r∈ℝ∧F⁡r=0→r∈ℝ
63 62 recnd ⊢φ∧r∈ℝ∧F⁡r=0→r∈ℂ
64 61 63 subeq0ad ⊢φ∧r∈ℝ∧F⁡r=0→A−r=0↔A=r
65 64 necon3abid ⊢φ∧r∈ℝ∧F⁡r=0→A−r≠0↔¬A=r
66 65 biimprd ⊢φ∧r∈ℝ∧F⁡r=0→¬A=r→A−r≠0
67 66 impr ⊢φ∧r∈ℝ∧F⁡r=0∧¬A=r→A−r≠0
68 59 67 absrpcld ⊢φ∧r∈ℝ∧F⁡r=0∧¬A=r→A−r∈ℝ+
69 57 recnd ⊢φ∧r∈ℝ∧F⁡r=0∧¬A=r→r∈ℂ
70 simprl ⊢φ∧r∈ℝ∧F⁡r=0∧¬A=r→F⁡r=0
71 plyf ⊢F∈Poly⁡ℤ→F:ℂ⟶ℂ
72 2 71 syl ⊢φ→F:ℂ⟶ℂ
73 72 ffnd ⊢φ→FFnℂ
74 73 ad2antrr ⊢φ∧r∈ℝ∧F⁡r=0∧¬A=r→FFnℂ
75 fniniseg ⊢FFnℂ→r∈F-10↔r∈ℂ∧F⁡r=0
76 74 75 syl ⊢φ∧r∈ℝ∧F⁡r=0∧¬A=r→r∈F-10↔r∈ℂ∧F⁡r=0
77 69 70 76 mpbir2and ⊢φ∧r∈ℝ∧F⁡r=0∧¬A=r→r∈F-10
78 eqid ⊢A−r=A−r
79 oveq2 ⊢b=r→A−b=A−r
80 79 fveq2d ⊢b=r→A−b=A−r
81 80 rspceeqv ⊢r∈F-10∧A−r=A−r→∃b∈F-10A−r=A−b
82 77 78 81 sylancl ⊢φ∧r∈ℝ∧F⁡r=0∧¬A=r→∃b∈F-10A−r=A−b
83 55 68 82 elrabd ⊢φ∧r∈ℝ∧F⁡r=0∧¬A=r→A−r∈a∈ℝ+|∃b∈F-10a=A−b
84 elun2 ⊢A−r∈a∈ℝ+|∃b∈F-10a=A−b→A−r∈1∪a∈ℝ+|∃b∈F-10a=A−b
85 83 84 syl ⊢φ∧r∈ℝ∧F⁡r=0∧¬A=r→A−r∈1∪a∈ℝ+|∃b∈F-10a=A−b
86 infrelb ⊢1∪a∈ℝ+|∃b∈F-10a=A−b⊆ℝ∧∃c∈ℝ∀d∈1∪a∈ℝ+|∃b∈F-10a=A−bc≤d∧A−r∈1∪a∈ℝ+|∃b∈F-10a=A−b→sup1∪a∈ℝ+|∃b∈F-10a=A−bℝ<≤A−r
87 38 53 85 86 mp3an12i ⊢φ∧r∈ℝ∧F⁡r=0∧¬A=r→sup1∪a∈ℝ+|∃b∈F-10a=A−bℝ<≤A−r
88 87 expr ⊢φ∧r∈ℝ∧F⁡r=0→¬A=r→sup1∪a∈ℝ+|∃b∈F-10a=A−bℝ<≤A−r
89 88 orrd ⊢φ∧r∈ℝ∧F⁡r=0→A=r∨sup1∪a∈ℝ+|∃b∈F-10a=A−bℝ<≤A−r
90 89 ex ⊢φ∧r∈ℝ→F⁡r=0→A=r∨sup1∪a∈ℝ+|∃b∈F-10a=A−bℝ<≤A−r
91 90 ralrimiva ⊢φ→∀r∈ℝF⁡r=0→A=r∨sup1∪a∈ℝ+|∃b∈F-10a=A−bℝ<≤A−r
92 breq1 ⊢x=sup1∪a∈ℝ+|∃b∈F-10a=A−bℝ<→x≤A−r↔sup1∪a∈ℝ+|∃b∈F-10a=A−bℝ<≤A−r
93 92 orbi2d ⊢x=sup1∪a∈ℝ+|∃b∈F-10a=A−bℝ<→A=r∨x≤A−r↔A=r∨sup1∪a∈ℝ+|∃b∈F-10a=A−bℝ<≤A−r
94 93 imbi2d ⊢x=sup1∪a∈ℝ+|∃b∈F-10a=A−bℝ<→F⁡r=0→A=r∨x≤A−r↔F⁡r=0→A=r∨sup1∪a∈ℝ+|∃b∈F-10a=A−bℝ<≤A−r
95 94 ralbidv ⊢x=sup1∪a∈ℝ+|∃b∈F-10a=A−bℝ<→∀r∈ℝF⁡r=0→A=r∨x≤A−r↔∀r∈ℝF⁡r=0→A=r∨sup1∪a∈ℝ+|∃b∈F-10a=A−bℝ<≤A−r
96 95 rspcev ⊢sup1∪a∈ℝ+|∃b∈F-10a=A−bℝ<∈ℝ+∧∀r∈ℝF⁡r=0→A=r∨sup1∪a∈ℝ+|∃b∈F-10a=A−bℝ<≤A−r→∃x∈ℝ+∀r∈ℝF⁡r=0→A=r∨x≤A−r
97 42 91 96 syl2anc ⊢φ→∃x∈ℝ+∀r∈ℝF⁡r=0→A=r∨x≤A−r
98 fveqeq2 ⊢r=pq→F⁡r=0↔F⁡pq=0
99 eqeq2 ⊢r=pq→A=r↔A=pq
100 oveq2 ⊢r=pq→A−r=A−pq
101 100 fveq2d ⊢r=pq→A−r=A−pq
102 101 breq2d ⊢r=pq→x≤A−r↔x≤A−pq
103 99 102 orbi12d ⊢r=pq→A=r∨x≤A−r↔A=pq∨x≤A−pq
104 98 103 imbi12d ⊢r=pq→F⁡r=0→A=r∨x≤A−r↔F⁡pq=0→A=pq∨x≤A−pq
105 104 rspcv ⊢pq∈ℝ→∀r∈ℝF⁡r=0→A=r∨x≤A−r→F⁡pq=0→A=pq∨x≤A−pq
106 znq ⊢p∈ℤ∧q∈ℕ→pq∈ℚ
107 qre ⊢pq∈ℚ→pq∈ℝ
108 106 107 syl ⊢p∈ℤ∧q∈ℕ→pq∈ℝ
109 105 108 syl11 ⊢∀r∈ℝF⁡r=0→A=r∨x≤A−r→p∈ℤ∧q∈ℕ→F⁡pq=0→A=pq∨x≤A−pq
110 109 ralrimivv ⊢∀r∈ℝF⁡r=0→A=r∨x≤A−r→∀p∈ℤ∀q∈ℕF⁡pq=0→A=pq∨x≤A−pq
111 110 reximi ⊢∃x∈ℝ+∀r∈ℝF⁡r=0→A=r∨x≤A−r→∃x∈ℝ+∀p∈ℤ∀q∈ℕF⁡pq=0→A=pq∨x≤A−pq
112 97 111 syl ⊢φ→∃x∈ℝ+∀p∈ℤ∀q∈ℕF⁡pq=0→A=pq∨x≤A−pq
113 simplr ⊢φ∧x∈ℝ+∧p∈ℤ∧q∈ℕ→x∈ℝ+
114 simprr ⊢φ∧x∈ℝ+∧p∈ℤ∧q∈ℕ→q∈ℕ
115 3 nnnn0d ⊢φ→N∈ℕ0
116 115 ad2antrr ⊢φ∧x∈ℝ+∧p∈ℤ∧q∈ℕ→N∈ℕ0
117 114 116 nnexpcld ⊢φ∧x∈ℝ+∧p∈ℤ∧q∈ℕ→qN∈ℕ
118 117 nnrpd ⊢φ∧x∈ℝ+∧p∈ℤ∧q∈ℕ→qN∈ℝ+
119 113 118 rpdivcld ⊢φ∧x∈ℝ+∧p∈ℤ∧q∈ℕ→xqN∈ℝ+
120 119 rpred ⊢φ∧x∈ℝ+∧p∈ℤ∧q∈ℕ→xqN∈ℝ
121 120 adantr ⊢φ∧x∈ℝ+∧p∈ℤ∧q∈ℕ∧x≤A−pq→xqN∈ℝ
122 simpllr ⊢φ∧x∈ℝ+∧p∈ℤ∧q∈ℕ∧x≤A−pq→x∈ℝ+
123 122 rpred ⊢φ∧x∈ℝ+∧p∈ℤ∧q∈ℕ∧x≤A−pq→x∈ℝ
124 4 ad2antrr ⊢φ∧x∈ℝ+∧p∈ℤ∧q∈ℕ→A∈ℝ
125 108 adantl ⊢φ∧x∈ℝ+∧p∈ℤ∧q∈ℕ→pq∈ℝ
126 124 125 resubcld ⊢φ∧x∈ℝ+∧p∈ℤ∧q∈ℕ→A−pq∈ℝ
127 126 recnd ⊢φ∧x∈ℝ+∧p∈ℤ∧q∈ℕ→A−pq∈ℂ
128 127 abscld ⊢φ∧x∈ℝ+∧p∈ℤ∧q∈ℕ→A−pq∈ℝ
129 128 adantr ⊢φ∧x∈ℝ+∧p∈ℤ∧q∈ℕ∧x≤A−pq→A−pq∈ℝ
130 rpre ⊢x∈ℝ+→x∈ℝ
131 130 ad2antlr ⊢φ∧x∈ℝ+∧p∈ℤ∧q∈ℕ→x∈ℝ
132 113 rpcnne0d ⊢φ∧x∈ℝ+∧p∈ℤ∧q∈ℕ→x∈ℂ∧x≠0
133 divid ⊢x∈ℂ∧x≠0→xx=1
134 132 133 syl ⊢φ∧x∈ℝ+∧p∈ℤ∧q∈ℕ→xx=1
135 117 nnge1d ⊢φ∧x∈ℝ+∧p∈ℤ∧q∈ℕ→1≤qN
136 134 135 eqbrtrd ⊢φ∧x∈ℝ+∧p∈ℤ∧q∈ℕ→xx≤qN
137 131 113 118 136 lediv23d ⊢φ∧x∈ℝ+∧p∈ℤ∧q∈ℕ→xqN≤x
138 137 adantr ⊢φ∧x∈ℝ+∧p∈ℤ∧q∈ℕ∧x≤A−pq→xqN≤x
139 simpr ⊢φ∧x∈ℝ+∧p∈ℤ∧q∈ℕ∧x≤A−pq→x≤A−pq
140 121 123 129 138 139 letrd ⊢φ∧x∈ℝ+∧p∈ℤ∧q∈ℕ∧x≤A−pq→xqN≤A−pq
141 140 ex ⊢φ∧x∈ℝ+∧p∈ℤ∧q∈ℕ→x≤A−pq→xqN≤A−pq
142 141 orim2d ⊢φ∧x∈ℝ+∧p∈ℤ∧q∈ℕ→A=pq∨x≤A−pq→A=pq∨xqN≤A−pq
143 142 imim2d ⊢φ∧x∈ℝ+∧p∈ℤ∧q∈ℕ→F⁡pq=0→A=pq∨x≤A−pq→F⁡pq=0→A=pq∨xqN≤A−pq
144 143 ralimdvva ⊢φ∧x∈ℝ+→∀p∈ℤ∀q∈ℕF⁡pq=0→A=pq∨x≤A−pq→∀p∈ℤ∀q∈ℕF⁡pq=0→A=pq∨xqN≤A−pq
145 144 reximdva ⊢φ→∃x∈ℝ+∀p∈ℤ∀q∈ℕF⁡pq=0→A=pq∨x≤A−pq→∃x∈ℝ+∀p∈ℤ∀q∈ℕF⁡pq=0→A=pq∨xqN≤A−pq
146 112 145 mpd ⊢φ→∃x∈ℝ+∀p∈ℤ∀q∈ℕF⁡pq=0→A=pq∨xqN≤A−pq