Metamath Proof Explorer

Theorem nn0constr

Description: Nonnegative integers are constructible. (Contributed by Thierry Arnoux, 2-Nov-2025)

Ref Expression
Hypothesis nn0constr.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion nn0constr ( 𝜑 → 𝑁 ∈ Constr )

Proof

Step Hyp Ref Expression
1 nn0constr.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
2 eleq1 ⊢ ( 𝑚 = 0 → ( 𝑚 ∈ Constr ↔ 0 ∈ Constr ) )
3 eleq1 ⊢ ( 𝑚 = 𝑛 → ( 𝑚 ∈ Constr ↔ 𝑛 ∈ Constr ) )
4 eleq1 ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( 𝑚 ∈ Constr ↔ ( 𝑛 + 1 ) ∈ Constr ) )
5 eleq1 ⊢ ( 𝑚 = 𝑁 → ( 𝑚 ∈ Constr ↔ 𝑁 ∈ Constr ) )
6 peano1 ⊢ ∅ ∈ ω
7 6 a1i ⊢ ( 𝜑 → ∅ ∈ ω )
8 fveq2 ⊢ ( 𝑢 = ∅ → ( rec ( ( 𝑧 ∈ V ↦ { 𝑦 ∈ ℂ ∣ ( ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ∃ 𝑝 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ 𝑦 = ( 𝑘 + ( 𝑝 · ( 𝑙 − 𝑘 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑗 − 𝑖 ) ) · ( 𝑙 − 𝑘 ) ) ) ≠ 0 ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ ( abs ‘ ( 𝑦 − 𝑘 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ( 𝑖 ≠ 𝑙 ∧ ( abs ‘ ( 𝑦 − 𝑖 ) ) = ( abs ‘ ( 𝑗 − 𝑘 ) ) ∧ ( abs ‘ ( 𝑦 − 𝑙 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ) } ) , { 0 , 1 } ) ‘ 𝑢 ) = ( rec ( ( 𝑧 ∈ V ↦ { 𝑦 ∈ ℂ ∣ ( ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ∃ 𝑝 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ 𝑦 = ( 𝑘 + ( 𝑝 · ( 𝑙 − 𝑘 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑗 − 𝑖 ) ) · ( 𝑙 − 𝑘 ) ) ) ≠ 0 ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ ( abs ‘ ( 𝑦 − 𝑘 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ( 𝑖 ≠ 𝑙 ∧ ( abs ‘ ( 𝑦 − 𝑖 ) ) = ( abs ‘ ( 𝑗 − 𝑘 ) ) ∧ ( abs ‘ ( 𝑦 − 𝑙 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ) } ) , { 0 , 1 } ) ‘ ∅ ) )
9 8 eleq2d ⊢ ( 𝑢 = ∅ → ( 0 ∈ ( rec ( ( 𝑧 ∈ V ↦ { 𝑦 ∈ ℂ ∣ ( ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ∃ 𝑝 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ 𝑦 = ( 𝑘 + ( 𝑝 · ( 𝑙 − 𝑘 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑗 − 𝑖 ) ) · ( 𝑙 − 𝑘 ) ) ) ≠ 0 ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ ( abs ‘ ( 𝑦 − 𝑘 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ( 𝑖 ≠ 𝑙 ∧ ( abs ‘ ( 𝑦 − 𝑖 ) ) = ( abs ‘ ( 𝑗 − 𝑘 ) ) ∧ ( abs ‘ ( 𝑦 − 𝑙 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ) } ) , { 0 , 1 } ) ‘ 𝑢 ) ↔ 0 ∈ ( rec ( ( 𝑧 ∈ V ↦ { 𝑦 ∈ ℂ ∣ ( ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ∃ 𝑝 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ 𝑦 = ( 𝑘 + ( 𝑝 · ( 𝑙 − 𝑘 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑗 − 𝑖 ) ) · ( 𝑙 − 𝑘 ) ) ) ≠ 0 ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ ( abs ‘ ( 𝑦 − 𝑘 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ( 𝑖 ≠ 𝑙 ∧ ( abs ‘ ( 𝑦 − 𝑖 ) ) = ( abs ‘ ( 𝑗 − 𝑘 ) ) ∧ ( abs ‘ ( 𝑦 − 𝑙 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ) } ) , { 0 , 1 } ) ‘ ∅ ) ) )
10 9 adantl ⊢ ( ( 𝜑 ∧ 𝑢 = ∅ ) → ( 0 ∈ ( rec ( ( 𝑧 ∈ V ↦ { 𝑦 ∈ ℂ ∣ ( ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ∃ 𝑝 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ 𝑦 = ( 𝑘 + ( 𝑝 · ( 𝑙 − 𝑘 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑗 − 𝑖 ) ) · ( 𝑙 − 𝑘 ) ) ) ≠ 0 ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ ( abs ‘ ( 𝑦 − 𝑘 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ( 𝑖 ≠ 𝑙 ∧ ( abs ‘ ( 𝑦 − 𝑖 ) ) = ( abs ‘ ( 𝑗 − 𝑘 ) ) ∧ ( abs ‘ ( 𝑦 − 𝑙 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ) } ) , { 0 , 1 } ) ‘ 𝑢 ) ↔ 0 ∈ ( rec ( ( 𝑧 ∈ V ↦ { 𝑦 ∈ ℂ ∣ ( ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ∃ 𝑝 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ 𝑦 = ( 𝑘 + ( 𝑝 · ( 𝑙 − 𝑘 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑗 − 𝑖 ) ) · ( 𝑙 − 𝑘 ) ) ) ≠ 0 ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ ( abs ‘ ( 𝑦 − 𝑘 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ( 𝑖 ≠ 𝑙 ∧ ( abs ‘ ( 𝑦 − 𝑖 ) ) = ( abs ‘ ( 𝑗 − 𝑘 ) ) ∧ ( abs ‘ ( 𝑦 − 𝑙 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ) } ) , { 0 , 1 } ) ‘ ∅ ) ) )
11 c0ex ⊢ 0 ∈ V
12 11 prid1 ⊢ 0 ∈ { 0 , 1 }
13 12 a1i ⊢ ( 𝜑 → 0 ∈ { 0 , 1 } )
14 constrcbvlem ⊢ rec ( ( 𝑧 ∈ V ↦ { 𝑦 ∈ ℂ ∣ ( ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ∃ 𝑝 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ 𝑦 = ( 𝑘 + ( 𝑝 · ( 𝑙 − 𝑘 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑗 − 𝑖 ) ) · ( 𝑙 − 𝑘 ) ) ) ≠ 0 ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ ( abs ‘ ( 𝑦 − 𝑘 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ( 𝑖 ≠ 𝑙 ∧ ( abs ‘ ( 𝑦 − 𝑖 ) ) = ( abs ‘ ( 𝑗 − 𝑘 ) ) ∧ ( abs ‘ ( 𝑦 − 𝑙 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ) } ) , { 0 , 1 } ) = rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑑 ∈ 𝑠 ∃ 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑 − 𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏 − 𝑎 ) ) · ( 𝑑 − 𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑒 ∈ 𝑠 ∃ 𝑓 ∈ 𝑠 ∃ 𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏 − 𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥 − 𝑐 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ∨ ∃ 𝑎 ∈ 𝑠 ∃ 𝑏 ∈ 𝑠 ∃ 𝑐 ∈ 𝑠 ∃ 𝑑 ∈ 𝑠 ∃ 𝑒 ∈ 𝑠 ∃ 𝑓 ∈ 𝑠 ( 𝑎 ≠ 𝑑 ∧ ( abs ‘ ( 𝑥 − 𝑎 ) ) = ( abs ‘ ( 𝑏 − 𝑐 ) ) ∧ ( abs ‘ ( 𝑥 − 𝑑 ) ) = ( abs ‘ ( 𝑒 − 𝑓 ) ) ) ) } ) , { 0 , 1 } )
15 14 constr0 ⊢ ( rec ( ( 𝑧 ∈ V ↦ { 𝑦 ∈ ℂ ∣ ( ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ∃ 𝑝 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ 𝑦 = ( 𝑘 + ( 𝑝 · ( 𝑙 − 𝑘 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑗 − 𝑖 ) ) · ( 𝑙 − 𝑘 ) ) ) ≠ 0 ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ ( abs ‘ ( 𝑦 − 𝑘 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ( 𝑖 ≠ 𝑙 ∧ ( abs ‘ ( 𝑦 − 𝑖 ) ) = ( abs ‘ ( 𝑗 − 𝑘 ) ) ∧ ( abs ‘ ( 𝑦 − 𝑙 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ) } ) , { 0 , 1 } ) ‘ ∅ ) = { 0 , 1 }
16 13 15 eleqtrrdi ⊢ ( 𝜑 → 0 ∈ ( rec ( ( 𝑧 ∈ V ↦ { 𝑦 ∈ ℂ ∣ ( ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ∃ 𝑝 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ 𝑦 = ( 𝑘 + ( 𝑝 · ( 𝑙 − 𝑘 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑗 − 𝑖 ) ) · ( 𝑙 − 𝑘 ) ) ) ≠ 0 ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ ( abs ‘ ( 𝑦 − 𝑘 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ( 𝑖 ≠ 𝑙 ∧ ( abs ‘ ( 𝑦 − 𝑖 ) ) = ( abs ‘ ( 𝑗 − 𝑘 ) ) ∧ ( abs ‘ ( 𝑦 − 𝑙 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ) } ) , { 0 , 1 } ) ‘ ∅ ) )
17 7 10 16 rspcedvd ⊢ ( 𝜑 → ∃ 𝑢 ∈ ω 0 ∈ ( rec ( ( 𝑧 ∈ V ↦ { 𝑦 ∈ ℂ ∣ ( ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ∃ 𝑝 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ 𝑦 = ( 𝑘 + ( 𝑝 · ( 𝑙 − 𝑘 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑗 − 𝑖 ) ) · ( 𝑙 − 𝑘 ) ) ) ≠ 0 ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ ( abs ‘ ( 𝑦 − 𝑘 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ( 𝑖 ≠ 𝑙 ∧ ( abs ‘ ( 𝑦 − 𝑖 ) ) = ( abs ‘ ( 𝑗 − 𝑘 ) ) ∧ ( abs ‘ ( 𝑦 − 𝑙 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ) } ) , { 0 , 1 } ) ‘ 𝑢 ) )
18 14 isconstr ⊢ ( 0 ∈ Constr ↔ ∃ 𝑢 ∈ ω 0 ∈ ( rec ( ( 𝑧 ∈ V ↦ { 𝑦 ∈ ℂ ∣ ( ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ∃ 𝑝 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ 𝑦 = ( 𝑘 + ( 𝑝 · ( 𝑙 − 𝑘 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑗 − 𝑖 ) ) · ( 𝑙 − 𝑘 ) ) ) ≠ 0 ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ ( abs ‘ ( 𝑦 − 𝑘 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ( 𝑖 ≠ 𝑙 ∧ ( abs ‘ ( 𝑦 − 𝑖 ) ) = ( abs ‘ ( 𝑗 − 𝑘 ) ) ∧ ( abs ‘ ( 𝑦 − 𝑙 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ) } ) , { 0 , 1 } ) ‘ 𝑢 ) )
19 17 18 sylibr ⊢ ( 𝜑 → 0 ∈ Constr )
20 19 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 ∈ Constr ) → 0 ∈ Constr )
21 8 eleq2d ⊢ ( 𝑢 = ∅ → ( 1 ∈ ( rec ( ( 𝑧 ∈ V ↦ { 𝑦 ∈ ℂ ∣ ( ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ∃ 𝑝 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ 𝑦 = ( 𝑘 + ( 𝑝 · ( 𝑙 − 𝑘 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑗 − 𝑖 ) ) · ( 𝑙 − 𝑘 ) ) ) ≠ 0 ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ ( abs ‘ ( 𝑦 − 𝑘 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ( 𝑖 ≠ 𝑙 ∧ ( abs ‘ ( 𝑦 − 𝑖 ) ) = ( abs ‘ ( 𝑗 − 𝑘 ) ) ∧ ( abs ‘ ( 𝑦 − 𝑙 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ) } ) , { 0 , 1 } ) ‘ 𝑢 ) ↔ 1 ∈ ( rec ( ( 𝑧 ∈ V ↦ { 𝑦 ∈ ℂ ∣ ( ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ∃ 𝑝 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ 𝑦 = ( 𝑘 + ( 𝑝 · ( 𝑙 − 𝑘 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑗 − 𝑖 ) ) · ( 𝑙 − 𝑘 ) ) ) ≠ 0 ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ ( abs ‘ ( 𝑦 − 𝑘 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ( 𝑖 ≠ 𝑙 ∧ ( abs ‘ ( 𝑦 − 𝑖 ) ) = ( abs ‘ ( 𝑗 − 𝑘 ) ) ∧ ( abs ‘ ( 𝑦 − 𝑙 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ) } ) , { 0 , 1 } ) ‘ ∅ ) ) )
22 21 adantl ⊢ ( ( 𝜑 ∧ 𝑢 = ∅ ) → ( 1 ∈ ( rec ( ( 𝑧 ∈ V ↦ { 𝑦 ∈ ℂ ∣ ( ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ∃ 𝑝 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ 𝑦 = ( 𝑘 + ( 𝑝 · ( 𝑙 − 𝑘 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑗 − 𝑖 ) ) · ( 𝑙 − 𝑘 ) ) ) ≠ 0 ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ ( abs ‘ ( 𝑦 − 𝑘 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ( 𝑖 ≠ 𝑙 ∧ ( abs ‘ ( 𝑦 − 𝑖 ) ) = ( abs ‘ ( 𝑗 − 𝑘 ) ) ∧ ( abs ‘ ( 𝑦 − 𝑙 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ) } ) , { 0 , 1 } ) ‘ 𝑢 ) ↔ 1 ∈ ( rec ( ( 𝑧 ∈ V ↦ { 𝑦 ∈ ℂ ∣ ( ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ∃ 𝑝 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ 𝑦 = ( 𝑘 + ( 𝑝 · ( 𝑙 − 𝑘 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑗 − 𝑖 ) ) · ( 𝑙 − 𝑘 ) ) ) ≠ 0 ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ ( abs ‘ ( 𝑦 − 𝑘 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ( 𝑖 ≠ 𝑙 ∧ ( abs ‘ ( 𝑦 − 𝑖 ) ) = ( abs ‘ ( 𝑗 − 𝑘 ) ) ∧ ( abs ‘ ( 𝑦 − 𝑙 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ) } ) , { 0 , 1 } ) ‘ ∅ ) ) )
23 1ex ⊢ 1 ∈ V
24 23 prid2 ⊢ 1 ∈ { 0 , 1 }
25 24 a1i ⊢ ( 𝜑 → 1 ∈ { 0 , 1 } )
26 25 15 eleqtrrdi ⊢ ( 𝜑 → 1 ∈ ( rec ( ( 𝑧 ∈ V ↦ { 𝑦 ∈ ℂ ∣ ( ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ∃ 𝑝 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ 𝑦 = ( 𝑘 + ( 𝑝 · ( 𝑙 − 𝑘 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑗 − 𝑖 ) ) · ( 𝑙 − 𝑘 ) ) ) ≠ 0 ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ ( abs ‘ ( 𝑦 − 𝑘 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ( 𝑖 ≠ 𝑙 ∧ ( abs ‘ ( 𝑦 − 𝑖 ) ) = ( abs ‘ ( 𝑗 − 𝑘 ) ) ∧ ( abs ‘ ( 𝑦 − 𝑙 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ) } ) , { 0 , 1 } ) ‘ ∅ ) )
27 7 22 26 rspcedvd ⊢ ( 𝜑 → ∃ 𝑢 ∈ ω 1 ∈ ( rec ( ( 𝑧 ∈ V ↦ { 𝑦 ∈ ℂ ∣ ( ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ∃ 𝑝 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ 𝑦 = ( 𝑘 + ( 𝑝 · ( 𝑙 − 𝑘 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑗 − 𝑖 ) ) · ( 𝑙 − 𝑘 ) ) ) ≠ 0 ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ ( abs ‘ ( 𝑦 − 𝑘 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ( 𝑖 ≠ 𝑙 ∧ ( abs ‘ ( 𝑦 − 𝑖 ) ) = ( abs ‘ ( 𝑗 − 𝑘 ) ) ∧ ( abs ‘ ( 𝑦 − 𝑙 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ) } ) , { 0 , 1 } ) ‘ 𝑢 ) )
28 14 isconstr ⊢ ( 1 ∈ Constr ↔ ∃ 𝑢 ∈ ω 1 ∈ ( rec ( ( 𝑧 ∈ V ↦ { 𝑦 ∈ ℂ ∣ ( ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ∃ 𝑝 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ 𝑦 = ( 𝑘 + ( 𝑝 · ( 𝑙 − 𝑘 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑗 − 𝑖 ) ) · ( 𝑙 − 𝑘 ) ) ) ≠ 0 ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ∃ 𝑜 ∈ ℝ ( 𝑦 = ( 𝑖 + ( 𝑜 · ( 𝑗 − 𝑖 ) ) ) ∧ ( abs ‘ ( 𝑦 − 𝑘 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ∨ ∃ 𝑖 ∈ 𝑧 ∃ 𝑗 ∈ 𝑧 ∃ 𝑘 ∈ 𝑧 ∃ 𝑙 ∈ 𝑧 ∃ 𝑚 ∈ 𝑧 ∃ 𝑞 ∈ 𝑧 ( 𝑖 ≠ 𝑙 ∧ ( abs ‘ ( 𝑦 − 𝑖 ) ) = ( abs ‘ ( 𝑗 − 𝑘 ) ) ∧ ( abs ‘ ( 𝑦 − 𝑙 ) ) = ( abs ‘ ( 𝑚 − 𝑞 ) ) ) ) } ) , { 0 , 1 } ) ‘ 𝑢 ) )
29 27 28 sylibr ⊢ ( 𝜑 → 1 ∈ Constr )
30 29 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 ∈ Constr ) → 1 ∈ Constr )
31 simpr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 ∈ Constr ) → 𝑛 ∈ Constr )
32 peano2nn0 ⊢ ( 𝑛 ∈ ℕ0 → ( 𝑛 + 1 ) ∈ ℕ0 )
33 32 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 ∈ Constr ) → ( 𝑛 + 1 ) ∈ ℕ0 )
34 33 nn0red ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 ∈ Constr ) → ( 𝑛 + 1 ) ∈ ℝ )
35 34 recnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 ∈ Constr ) → ( 𝑛 + 1 ) ∈ ℂ )
36 nn0cn ⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℂ )
37 1cnd ⊢ ( 𝑛 ∈ ℕ0 → 1 ∈ ℂ )
38 36 37 addcld ⊢ ( 𝑛 ∈ ℕ0 → ( 𝑛 + 1 ) ∈ ℂ )
39 37 subid1d ⊢ ( 𝑛 ∈ ℕ0 → ( 1 − 0 ) = 1 )
40 39 37 eqeltrd ⊢ ( 𝑛 ∈ ℕ0 → ( 1 − 0 ) ∈ ℂ )
41 38 40 mulcld ⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝑛 + 1 ) · ( 1 − 0 ) ) ∈ ℂ )
42 41 addlidd ⊢ ( 𝑛 ∈ ℕ0 → ( 0 + ( ( 𝑛 + 1 ) · ( 1 − 0 ) ) ) = ( ( 𝑛 + 1 ) · ( 1 − 0 ) ) )
43 39 oveq2d ⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝑛 + 1 ) · ( 1 − 0 ) ) = ( ( 𝑛 + 1 ) · 1 ) )
44 38 mulridd ⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝑛 + 1 ) · 1 ) = ( 𝑛 + 1 ) )
45 42 43 44 3eqtrrd ⊢ ( 𝑛 ∈ ℕ0 → ( 𝑛 + 1 ) = ( 0 + ( ( 𝑛 + 1 ) · ( 1 − 0 ) ) ) )
46 45 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 ∈ Constr ) → ( 𝑛 + 1 ) = ( 0 + ( ( 𝑛 + 1 ) · ( 1 − 0 ) ) ) )
47 36 37 pncan2d ⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝑛 + 1 ) − 𝑛 ) = 1 )
48 47 39 eqtr4d ⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝑛 + 1 ) − 𝑛 ) = ( 1 − 0 ) )
49 48 fveq2d ⊢ ( 𝑛 ∈ ℕ0 → ( abs ‘ ( ( 𝑛 + 1 ) − 𝑛 ) ) = ( abs ‘ ( 1 − 0 ) ) )
50 49 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 ∈ Constr ) → ( abs ‘ ( ( 𝑛 + 1 ) − 𝑛 ) ) = ( abs ‘ ( 1 − 0 ) ) )
51 20 30 31 30 20 34 35 46 50 constrlccl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 ∈ Constr ) → ( 𝑛 + 1 ) ∈ Constr )
52 2 3 4 5 19 51 nn0indd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ Constr )
53 1 52 mpdan ⊢ ( 𝜑 → 𝑁 ∈ Constr )