Metamath Proof Explorer


Theorem constrlim

Description: Limit step of the construction of constructible numbers. (Contributed by Thierry Arnoux, 25-Jun-2025)

Ref Expression
Hypotheses constr0.1 𝐶 = rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ) , { 0 , 1 } )
constrlim.1 ( 𝜑𝑁𝑉 )
constrlim.2 ( 𝜑 → Lim 𝑁 )
Assertion constrlim ( 𝜑 → ( 𝐶𝑁 ) = 𝑛𝑁 ( 𝐶𝑛 ) )

Proof

Step Hyp Ref Expression
1 constr0.1 𝐶 = rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ) , { 0 , 1 } )
2 constrlim.1 ( 𝜑𝑁𝑉 )
3 constrlim.2 ( 𝜑 → Lim 𝑁 )
4 rdglim2a ( ( 𝑁𝑉 ∧ Lim 𝑁 ) → ( rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ) , { 0 , 1 } ) ‘ 𝑁 ) = 𝑛𝑁 ( rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ) , { 0 , 1 } ) ‘ 𝑛 ) )
5 2 3 4 syl2anc ( 𝜑 → ( rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ) , { 0 , 1 } ) ‘ 𝑁 ) = 𝑛𝑁 ( rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ) , { 0 , 1 } ) ‘ 𝑛 ) )
6 1 fveq1i ( 𝐶𝑁 ) = ( rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ) , { 0 , 1 } ) ‘ 𝑁 )
7 6 a1i ( 𝜑 → ( 𝐶𝑁 ) = ( rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ) , { 0 , 1 } ) ‘ 𝑁 ) )
8 1 fveq1i ( 𝐶𝑛 ) = ( rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ) , { 0 , 1 } ) ‘ 𝑛 )
9 8 a1i ( 𝜑 → ( 𝐶𝑛 ) = ( rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ) , { 0 , 1 } ) ‘ 𝑛 ) )
10 9 iuneq2d ( 𝜑 𝑛𝑁 ( 𝐶𝑛 ) = 𝑛𝑁 ( rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ) , { 0 , 1 } ) ‘ 𝑛 ) )
11 5 7 10 3eqtr4d ( 𝜑 → ( 𝐶𝑁 ) = 𝑛𝑁 ( 𝐶𝑛 ) )