Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  sadc0 Structured version   Visualization version   GIF version

 Description: The initial element of the carry sequence is ⊥. (Contributed by Mario Carneiro, 5-Sep-2016.)
Hypotheses
Ref Expression
sadval.c 𝐶 = seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))
Assertion
Ref Expression
sadc0 (𝜑 → ¬ ∅ ∈ (𝐶‘0))
Distinct variable groups:   𝑚,𝑐,𝑛   𝐴,𝑐,𝑚   𝐵,𝑐,𝑚
Allowed substitution hints:   𝜑(𝑚,𝑛,𝑐)   𝐴(𝑛)   𝐵(𝑛)   𝐶(𝑚,𝑛,𝑐)

StepHypRef Expression
1 noel 4146 . . 3 ¬ ∅ ∈ ∅
2 sadval.c . . . . . 6 𝐶 = seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))
32fveq1i 6449 . . . . 5 (𝐶‘0) = (seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘0)
4 0z 11744 . . . . . 6 0 ∈ ℤ
5 seq1 13137 . . . . . 6 (0 ∈ ℤ → (seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘0) = ((𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))‘0))
64, 5ax-mp 5 . . . . 5 (seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘0) = ((𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))‘0)
7 0nn0 11664 . . . . . 6 0 ∈ ℕ0
8 iftrue 4313 . . . . . . 7 (𝑛 = 0 → if(𝑛 = 0, ∅, (𝑛 − 1)) = ∅)
9 eqid 2778 . . . . . . 7 (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))) = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))
10 0ex 5028 . . . . . . 7 ∅ ∈ V
118, 9, 10fvmpt 6544 . . . . . 6 (0 ∈ ℕ0 → ((𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))‘0) = ∅)
127, 11ax-mp 5 . . . . 5 ((𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))‘0) = ∅
133, 6, 123eqtri 2806 . . . 4 (𝐶‘0) = ∅
1413eleq2i 2851 . . 3 (∅ ∈ (𝐶‘0) ↔ ∅ ∈ ∅)
151, 14mtbir 315 . 2 ¬ ∅ ∈ (𝐶‘0)
1615a1i 11 1 (𝜑 → ¬ ∅ ∈ (𝐶‘0))