Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  poimirlem23 Structured version   Visualization version   GIF version

Theorem poimirlem23 36603
Description: Lemma for poimir 36613, two ways of expressing the property that a face is not on the back face of the cube. (Contributed by Brendan Leahy, 21-Aug-2020.)
Hypotheses
Ref Expression
poimir.0 (𝜑𝑁 ∈ ℕ)
poimirlem23.1 (𝜑𝑇:(1...𝑁)⟶(0..^𝐾))
poimirlem23.2 (𝜑𝑈:(1...𝑁)–1-1-onto→(1...𝑁))
poimirlem23.3 (𝜑𝑉 ∈ (0...𝑁))
Assertion
Ref Expression
poimirlem23 (𝜑 → (∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝𝑁) ≠ 0 ↔ ¬ (𝑉 = 𝑁 ∧ ((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁))))
Distinct variable groups:   𝑗,𝑝,𝑦,𝜑   𝑗,𝑁,𝑦   𝑇,𝑗,𝑦   𝑈,𝑗,𝑦   𝑗,𝑉,𝑦   𝜑,𝑝   𝑗,𝐾,𝑝   𝑁,𝑝   𝑇,𝑝   𝑈,𝑝   𝑦,𝐾   𝑉,𝑝

Proof of Theorem poimirlem23
StepHypRef Expression
1 ovex 7444 . . . . . 6 (𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
21csbex 5311 . . . . 5 if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
32rgenw 3065 . . . 4 𝑦 ∈ (0...(𝑁 − 1))if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
4 eqid 2732 . . . . 5 (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
5 fveq1 6890 . . . . . . 7 (𝑝 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) → (𝑝𝑁) = (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁))
65neeq1d 3000 . . . . . 6 (𝑝 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) → ((𝑝𝑁) ≠ 0 ↔ (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0))
7 df-ne 2941 . . . . . 6 ((if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0 ↔ ¬ (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
86, 7bitrdi 286 . . . . 5 (𝑝 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) → ((𝑝𝑁) ≠ 0 ↔ ¬ (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
94, 8rexrnmptw 7096 . . . 4 (∀𝑦 ∈ (0...(𝑁 − 1))if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V → (∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝𝑁) ≠ 0 ↔ ∃𝑦 ∈ (0...(𝑁 − 1)) ¬ (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
103, 9ax-mp 5 . . 3 (∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝𝑁) ≠ 0 ↔ ∃𝑦 ∈ (0...(𝑁 − 1)) ¬ (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
11 rexnal 3100 . . 3 (∃𝑦 ∈ (0...(𝑁 − 1)) ¬ (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ¬ ∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
1210, 11bitri 274 . 2 (∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝𝑁) ≠ 0 ↔ ¬ ∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
13 poimir.0 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℕ)
1413nnzd 12587 . . . . . . . . . 10 (𝜑𝑁 ∈ ℤ)
15 poimirlem23.3 . . . . . . . . . . 11 (𝜑𝑉 ∈ (0...𝑁))
16 elfzelz 13503 . . . . . . . . . . 11 (𝑉 ∈ (0...𝑁) → 𝑉 ∈ ℤ)
1715, 16syl 17 . . . . . . . . . 10 (𝜑𝑉 ∈ ℤ)
18 zlem1lt 12616 . . . . . . . . . 10 ((𝑁 ∈ ℤ ∧ 𝑉 ∈ ℤ) → (𝑁𝑉 ↔ (𝑁 − 1) < 𝑉))
1914, 17, 18syl2anc 584 . . . . . . . . 9 (𝜑 → (𝑁𝑉 ↔ (𝑁 − 1) < 𝑉))
20 elfzle2 13507 . . . . . . . . . . 11 (𝑉 ∈ (0...𝑁) → 𝑉𝑁)
2115, 20syl 17 . . . . . . . . . 10 (𝜑𝑉𝑁)
2217zred 12668 . . . . . . . . . . . 12 (𝜑𝑉 ∈ ℝ)
2313nnred 12229 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℝ)
2422, 23letri3d 11358 . . . . . . . . . . 11 (𝜑 → (𝑉 = 𝑁 ↔ (𝑉𝑁𝑁𝑉)))
2524biimprd 247 . . . . . . . . . 10 (𝜑 → ((𝑉𝑁𝑁𝑉) → 𝑉 = 𝑁))
2621, 25mpand 693 . . . . . . . . 9 (𝜑 → (𝑁𝑉𝑉 = 𝑁))
2719, 26sylbird 259 . . . . . . . 8 (𝜑 → ((𝑁 − 1) < 𝑉𝑉 = 𝑁))
2827necon3ad 2953 . . . . . . 7 (𝜑 → (𝑉𝑁 → ¬ (𝑁 − 1) < 𝑉))
29 nnm1nn0 12515 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
3013, 29syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑁 − 1) ∈ ℕ0)
31 nn0fz0 13601 . . . . . . . . . . . 12 ((𝑁 − 1) ∈ ℕ0 ↔ (𝑁 − 1) ∈ (0...(𝑁 − 1)))
3230, 31sylib 217 . . . . . . . . . . 11 (𝜑 → (𝑁 − 1) ∈ (0...(𝑁 − 1)))
3332adantr 481 . . . . . . . . . 10 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → (𝑁 − 1) ∈ (0...(𝑁 − 1)))
34 iffalse 4537 . . . . . . . . . . . . . . . 16 (¬ (𝑁 − 1) < 𝑉 → if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) = ((𝑁 − 1) + 1))
3513nncnd 12230 . . . . . . . . . . . . . . . . 17 (𝜑𝑁 ∈ ℂ)
36 npcan1 11641 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
3735, 36syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
3834, 37sylan9eqr 2794 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) = 𝑁)
3938csbeq1d 3897 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = 𝑁 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
40 oveq2 7419 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑁 → (1...𝑗) = (1...𝑁))
4140imaeq2d 6059 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑁 → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...𝑁)))
4241xpeq1d 5705 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑁 → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...𝑁)) × {1}))
43 oveq1 7418 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑁 → (𝑗 + 1) = (𝑁 + 1))
4443oveq1d 7426 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑁 → ((𝑗 + 1)...𝑁) = ((𝑁 + 1)...𝑁))
4544imaeq2d 6059 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑁 → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ ((𝑁 + 1)...𝑁)))
4645xpeq1d 5705 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑁 → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0}))
4742, 46uneq12d 4164 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑁 → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...𝑁)) × {1}) ∪ ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0})))
48 poimirlem23.2 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑈:(1...𝑁)–1-1-onto→(1...𝑁))
49 f1ofo 6840 . . . . . . . . . . . . . . . . . . . . . 22 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)–onto→(1...𝑁))
50 foima 6810 . . . . . . . . . . . . . . . . . . . . . 22 (𝑈:(1...𝑁)–onto→(1...𝑁) → (𝑈 “ (1...𝑁)) = (1...𝑁))
5148, 49, 503syl 18 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑈 “ (1...𝑁)) = (1...𝑁))
5251xpeq1d 5705 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑈 “ (1...𝑁)) × {1}) = ((1...𝑁) × {1}))
5323ltp1d 12146 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑁 < (𝑁 + 1))
5414peano2zd 12671 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝑁 + 1) ∈ ℤ)
55 fzn 13519 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑁 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 < (𝑁 + 1) ↔ ((𝑁 + 1)...𝑁) = ∅))
5654, 14, 55syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑁 < (𝑁 + 1) ↔ ((𝑁 + 1)...𝑁) = ∅))
5753, 56mpbid 231 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑁 + 1)...𝑁) = ∅)
5857imaeq2d 6059 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑈 “ ((𝑁 + 1)...𝑁)) = (𝑈 “ ∅))
5958xpeq1d 5705 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0}) = ((𝑈 “ ∅) × {0}))
60 ima0 6076 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑈 “ ∅) = ∅
6160xpeq1i 5702 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑈 “ ∅) × {0}) = (∅ × {0})
62 0xp 5774 . . . . . . . . . . . . . . . . . . . . . 22 (∅ × {0}) = ∅
6361, 62eqtri 2760 . . . . . . . . . . . . . . . . . . . . 21 ((𝑈 “ ∅) × {0}) = ∅
6459, 63eqtrdi 2788 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0}) = ∅)
6552, 64uneq12d 4164 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((𝑈 “ (1...𝑁)) × {1}) ∪ ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0})) = (((1...𝑁) × {1}) ∪ ∅))
66 un0 4390 . . . . . . . . . . . . . . . . . . 19 (((1...𝑁) × {1}) ∪ ∅) = ((1...𝑁) × {1})
6765, 66eqtrdi 2788 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((𝑈 “ (1...𝑁)) × {1}) ∪ ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0})) = ((1...𝑁) × {1}))
6847, 67sylan9eqr 2794 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 = 𝑁) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = ((1...𝑁) × {1}))
6968oveq2d 7427 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 = 𝑁) → (𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇f + ((1...𝑁) × {1})))
7013, 69csbied 3931 . . . . . . . . . . . . . . 15 (𝜑𝑁 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇f + ((1...𝑁) × {1})))
7170adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → 𝑁 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇f + ((1...𝑁) × {1})))
7239, 71eqtrd 2772 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇f + ((1...𝑁) × {1})))
7372fveq1d 6893 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → (if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = ((𝑇f + ((1...𝑁) × {1}))‘𝑁))
74 elfzonn0 13679 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0..^𝐾) → 𝑗 ∈ ℕ0)
75 nn0p1nn 12513 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ0 → (𝑗 + 1) ∈ ℕ)
7674, 75syl 17 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0..^𝐾) → (𝑗 + 1) ∈ ℕ)
77 elsni 4645 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ {1} → 𝑦 = 1)
7877oveq2d 7427 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ {1} → (𝑗 + 𝑦) = (𝑗 + 1))
7978eleq1d 2818 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ {1} → ((𝑗 + 𝑦) ∈ ℕ ↔ (𝑗 + 1) ∈ ℕ))
8076, 79syl5ibrcom 246 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0..^𝐾) → (𝑦 ∈ {1} → (𝑗 + 𝑦) ∈ ℕ))
8180imp 407 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (0..^𝐾) ∧ 𝑦 ∈ {1}) → (𝑗 + 𝑦) ∈ ℕ)
8281adantl 482 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗 ∈ (0..^𝐾) ∧ 𝑦 ∈ {1})) → (𝑗 + 𝑦) ∈ ℕ)
83 poimirlem23.1 . . . . . . . . . . . . . . 15 (𝜑𝑇:(1...𝑁)⟶(0..^𝐾))
84 1ex 11212 . . . . . . . . . . . . . . . . 17 1 ∈ V
8584fconst 6777 . . . . . . . . . . . . . . . 16 ((1...𝑁) × {1}):(1...𝑁)⟶{1}
8685a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → ((1...𝑁) × {1}):(1...𝑁)⟶{1})
87 ovexd 7446 . . . . . . . . . . . . . . 15 (𝜑 → (1...𝑁) ∈ V)
88 inidm 4218 . . . . . . . . . . . . . . 15 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
8982, 83, 86, 87, 87, 88off 7690 . . . . . . . . . . . . . 14 (𝜑 → (𝑇f + ((1...𝑁) × {1})):(1...𝑁)⟶ℕ)
90 elfz1end 13533 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℕ ↔ 𝑁 ∈ (1...𝑁))
9113, 90sylib 217 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ (1...𝑁))
9289, 91ffvelcdmd 7087 . . . . . . . . . . . . 13 (𝜑 → ((𝑇f + ((1...𝑁) × {1}))‘𝑁) ∈ ℕ)
9392adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → ((𝑇f + ((1...𝑁) × {1}))‘𝑁) ∈ ℕ)
9473, 93eqeltrd 2833 . . . . . . . . . . 11 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → (if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ∈ ℕ)
9594nnne0d 12264 . . . . . . . . . 10 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → (if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0)
96 breq1 5151 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑁 − 1) → (𝑦 < 𝑉 ↔ (𝑁 − 1) < 𝑉))
97 id 22 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑁 − 1) → 𝑦 = (𝑁 − 1))
98 oveq1 7418 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑁 − 1) → (𝑦 + 1) = ((𝑁 − 1) + 1))
9996, 97, 98ifbieq12d 4556 . . . . . . . . . . . . . . 15 (𝑦 = (𝑁 − 1) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) = if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)))
10099csbeq1d 3897 . . . . . . . . . . . . . 14 (𝑦 = (𝑁 − 1) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
101100fveq1d 6893 . . . . . . . . . . . . 13 (𝑦 = (𝑁 − 1) → (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = (if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁))
102101neeq1d 3000 . . . . . . . . . . . 12 (𝑦 = (𝑁 − 1) → ((if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0 ↔ (if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0))
1037, 102bitr3id 284 . . . . . . . . . . 11 (𝑦 = (𝑁 − 1) → (¬ (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ (if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0))
104103rspcev 3612 . . . . . . . . . 10 (((𝑁 − 1) ∈ (0...(𝑁 − 1)) ∧ (if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0) → ∃𝑦 ∈ (0...(𝑁 − 1)) ¬ (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
10533, 95, 104syl2anc 584 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → ∃𝑦 ∈ (0...(𝑁 − 1)) ¬ (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
106105, 11sylib 217 . . . . . . . 8 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → ¬ ∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
107106ex 413 . . . . . . 7 (𝜑 → (¬ (𝑁 − 1) < 𝑉 → ¬ ∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
10828, 107syld 47 . . . . . 6 (𝜑 → (𝑉𝑁 → ¬ ∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
109108necon4ad 2959 . . . . 5 (𝜑 → (∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 → 𝑉 = 𝑁))
110109pm4.71rd 563 . . . 4 (𝜑 → (∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ (𝑉 = 𝑁 ∧ ∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)))
11130nn0zd 12586 . . . . . . . . . . . . 13 (𝜑 → (𝑁 − 1) ∈ ℤ)
112 uzid 12839 . . . . . . . . . . . . 13 ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)))
113 peano2uz 12887 . . . . . . . . . . . . 13 ((𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
114111, 112, 1133syl 18 . . . . . . . . . . . 12 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
11537, 114eqeltrrd 2834 . . . . . . . . . . 11 (𝜑𝑁 ∈ (ℤ‘(𝑁 − 1)))
116 fzss2 13543 . . . . . . . . . . 11 (𝑁 ∈ (ℤ‘(𝑁 − 1)) → (0...(𝑁 − 1)) ⊆ (0...𝑁))
117115, 116syl 17 . . . . . . . . . 10 (𝜑 → (0...(𝑁 − 1)) ⊆ (0...𝑁))
118117sselda 3982 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → 𝑗 ∈ (0...𝑁))
11991adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑁 ∈ (1...𝑁))
12083ffnd 6718 . . . . . . . . . . . . . 14 (𝜑𝑇 Fn (1...𝑁))
121120adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑇 Fn (1...𝑁))
12284fconst 6777 . . . . . . . . . . . . . . . . 17 ((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1}
123 c0ex 11210 . . . . . . . . . . . . . . . . . 18 0 ∈ V
124123fconst 6777 . . . . . . . . . . . . . . . . 17 ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0}
125122, 124pm3.2i 471 . . . . . . . . . . . . . . . 16 (((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1} ∧ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0})
126 dff1o3 6839 . . . . . . . . . . . . . . . . . . 19 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (𝑈:(1...𝑁)–onto→(1...𝑁) ∧ Fun 𝑈))
127126simprbi 497 . . . . . . . . . . . . . . . . . 18 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → Fun 𝑈)
128 imain 6633 . . . . . . . . . . . . . . . . . 18 (Fun 𝑈 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))))
12948, 127, 1283syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))))
130 elfzelz 13503 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℤ)
131130zred 12668 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℝ)
132131ltp1d 12146 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...𝑁) → 𝑗 < (𝑗 + 1))
133 fzdisj 13530 . . . . . . . . . . . . . . . . . . . 20 (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
134132, 133syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑁) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
135134imaeq2d 6059 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑁) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (𝑈 “ ∅))
136135, 60eqtrdi 2788 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑁) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ∅)
137129, 136sylan9req 2793 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅)
138 fun 6753 . . . . . . . . . . . . . . . 16 (((((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1} ∧ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0}) ∧ ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}))
139125, 137, 138sylancr 587 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...𝑁)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}))
140 elfznn0 13596 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℕ0)
141140, 75syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ ℕ)
142 nnuz 12867 . . . . . . . . . . . . . . . . . . . . 21 ℕ = (ℤ‘1)
143141, 142eleqtrdi 2843 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ (ℤ‘1))
144 elfzuz3 13500 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...𝑁) → 𝑁 ∈ (ℤ𝑗))
145 fzsplit2 13528 . . . . . . . . . . . . . . . . . . . 20 (((𝑗 + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ𝑗)) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
146143, 144, 145syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑁) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
147146imaeq2d 6059 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑁) → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))))
148 imaundi 6149 . . . . . . . . . . . . . . . . . 18 (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))
149147, 148eqtr2di 2789 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑁) → ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁))) = (𝑈 “ (1...𝑁)))
150149, 51sylan9eqr 2794 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁))) = (1...𝑁))
151150feq2d 6703 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...𝑁)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}) ↔ (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0})))
152139, 151mpbid 231 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑁)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0}))
153152ffnd 6718 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑁)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) Fn (1...𝑁))
154 ovexd 7446 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑁)) → (1...𝑁) ∈ V)
155 eqidd 2733 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑁 ∈ (1...𝑁)) → (𝑇𝑁) = (𝑇𝑁))
156 eqidd 2733 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑁 ∈ (1...𝑁)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))
157121, 153, 154, 154, 88, 155, 156ofval 7683 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑁 ∈ (1...𝑁)) → ((𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = ((𝑇𝑁) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)))
158119, 157mpdan 685 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = ((𝑇𝑁) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)))
159158eqeq1d 2734 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑁)) → (((𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ((𝑇𝑁) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)) = 0))
16083, 91ffvelcdmd 7087 . . . . . . . . . . . . . 14 (𝜑 → (𝑇𝑁) ∈ (0..^𝐾))
161 elfzonn0 13679 . . . . . . . . . . . . . 14 ((𝑇𝑁) ∈ (0..^𝐾) → (𝑇𝑁) ∈ ℕ0)
162160, 161syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑇𝑁) ∈ ℕ0)
163162nn0red 12535 . . . . . . . . . . . 12 (𝜑 → (𝑇𝑁) ∈ ℝ)
164163adantr 481 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑇𝑁) ∈ ℝ)
165162nn0ge0d 12537 . . . . . . . . . . . 12 (𝜑 → 0 ≤ (𝑇𝑁))
166165adantr 481 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑁)) → 0 ≤ (𝑇𝑁))
167 1re 11216 . . . . . . . . . . . . . 14 1 ∈ ℝ
168 snssi 4811 . . . . . . . . . . . . . 14 (1 ∈ ℝ → {1} ⊆ ℝ)
169167, 168ax-mp 5 . . . . . . . . . . . . 13 {1} ⊆ ℝ
170 0re 11218 . . . . . . . . . . . . . 14 0 ∈ ℝ
171 snssi 4811 . . . . . . . . . . . . . 14 (0 ∈ ℝ → {0} ⊆ ℝ)
172170, 171ax-mp 5 . . . . . . . . . . . . 13 {0} ⊆ ℝ
173169, 172unssi 4185 . . . . . . . . . . . 12 ({1} ∪ {0}) ⊆ ℝ
174152, 119ffvelcdmd 7087 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑁)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ ({1} ∪ {0}))
175173, 174sselid 3980 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑁)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ ℝ)
176 elun 4148 . . . . . . . . . . . . 13 (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ ({1} ∪ {0}) ↔ (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {1} ∨ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {0}))
177 0le1 11739 . . . . . . . . . . . . . . 15 0 ≤ 1
178 elsni 4645 . . . . . . . . . . . . . . 15 (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {1} → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 1)
179177, 178breqtrrid 5186 . . . . . . . . . . . . . 14 (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {1} → 0 ≤ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))
180 0le0 12315 . . . . . . . . . . . . . . 15 0 ≤ 0
181 elsni 4645 . . . . . . . . . . . . . . 15 (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {0} → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
182180, 181breqtrrid 5186 . . . . . . . . . . . . . 14 (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {0} → 0 ≤ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))
183179, 182jaoi 855 . . . . . . . . . . . . 13 ((((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {1} ∨ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {0}) → 0 ≤ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))
184176, 183sylbi 216 . . . . . . . . . . . 12 (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ ({1} ∪ {0}) → 0 ≤ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))
185174, 184syl 17 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑁)) → 0 ≤ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))
186 add20 11728 . . . . . . . . . . 11 ((((𝑇𝑁) ∈ ℝ ∧ 0 ≤ (𝑇𝑁)) ∧ (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ ℝ ∧ 0 ≤ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))) → (((𝑇𝑁) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)) = 0 ↔ ((𝑇𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
187164, 166, 175, 185, 186syl22anc 837 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑁)) → (((𝑇𝑁) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)) = 0 ↔ ((𝑇𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
188159, 187bitrd 278 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑁)) → (((𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ((𝑇𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
189118, 188syldan 591 . . . . . . . 8 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → (((𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ((𝑇𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
190189ralbidva 3175 . . . . . . 7 (𝜑 → (∀𝑗 ∈ (0...(𝑁 − 1))((𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((𝑇𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
191190adantr 481 . . . . . 6 ((𝜑𝑉 = 𝑁) → (∀𝑗 ∈ (0...(𝑁 − 1))((𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((𝑇𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
192 breq2 5152 . . . . . . . . . . . . . 14 (𝑉 = 𝑁 → (𝑦 < 𝑉𝑦 < 𝑁))
193192ifbid 4551 . . . . . . . . . . . . 13 (𝑉 = 𝑁 → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) = if(𝑦 < 𝑁, 𝑦, (𝑦 + 1)))
194 elfzelz 13503 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℤ)
195194zred 12668 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℝ)
196195adantl 482 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ∈ ℝ)
19730nn0red 12535 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑁 − 1) ∈ ℝ)
198197adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ)
19923adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℝ)
200 elfzle2 13507 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ≤ (𝑁 − 1))
201200adantl 482 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ≤ (𝑁 − 1))
20223ltm1d 12148 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑁 − 1) < 𝑁)
203202adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑁 − 1) < 𝑁)
204196, 198, 199, 201, 203lelttrd 11374 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 < 𝑁)
205204iftrued 4536 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < 𝑁, 𝑦, (𝑦 + 1)) = 𝑦)
206193, 205sylan9eqr 2794 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑉 = 𝑁) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) = 𝑦)
207206an32s 650 . . . . . . . . . . 11 (((𝜑𝑉 = 𝑁) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) = 𝑦)
208207csbeq1d 3897 . . . . . . . . . 10 (((𝜑𝑉 = 𝑁) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = 𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
209208fveq1d 6893 . . . . . . . . 9 (((𝜑𝑉 = 𝑁) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = (𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁))
210209eqeq1d 2734 . . . . . . . 8 (((𝜑𝑉 = 𝑁) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ (𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
211210ralbidva 3175 . . . . . . 7 ((𝜑𝑉 = 𝑁) → (∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ∀𝑦 ∈ (0...(𝑁 − 1))(𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
212 nfv 1917 . . . . . . . 8 𝑦((𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0
213 nfcsb1v 3918 . . . . . . . . . 10 𝑗𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))
214 nfcv 2903 . . . . . . . . . 10 𝑗𝑁
215213, 214nffv 6901 . . . . . . . . 9 𝑗(𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁)
216215nfeq1 2918 . . . . . . . 8 𝑗(𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0
217 csbeq1a 3907 . . . . . . . . . 10 (𝑗 = 𝑦 → (𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = 𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
218217fveq1d 6893 . . . . . . . . 9 (𝑗 = 𝑦 → ((𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = (𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁))
219218eqeq1d 2734 . . . . . . . 8 (𝑗 = 𝑦 → (((𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ (𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
220212, 216, 219cbvralw 3303 . . . . . . 7 (∀𝑗 ∈ (0...(𝑁 − 1))((𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ∀𝑦 ∈ (0...(𝑁 − 1))(𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
221211, 220bitr4di 288 . . . . . 6 ((𝜑𝑉 = 𝑁) → (∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
222 ne0i 4334 . . . . . . . . . 10 ((𝑁 − 1) ∈ (0...(𝑁 − 1)) → (0...(𝑁 − 1)) ≠ ∅)
223 r19.3rzv 4498 . . . . . . . . . 10 ((0...(𝑁 − 1)) ≠ ∅ → ((𝑇𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))(𝑇𝑁) = 0))
22432, 222, 2233syl 18 . . . . . . . . 9 (𝜑 → ((𝑇𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))(𝑇𝑁) = 0))
225 elfzelz 13503 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 ∈ ℤ)
226225zred 12668 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 ∈ ℝ)
227226ltp1d 12146 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 < (𝑗 + 1))
228227, 133syl 17 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...(𝑁 − 1)) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
229228imaeq2d 6059 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...(𝑁 − 1)) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (𝑈 “ ∅))
230229, 60eqtrdi 2788 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...(𝑁 − 1)) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ∅)
231129, 230sylan9req 2793 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅)
232231adantlr 713 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑈𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅)
233 simplr 767 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑈𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑈𝑁) = 𝑁)
234 f1ofn 6834 . . . . . . . . . . . . . . . . . . 19 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈 Fn (1...𝑁))
23548, 234syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝑈 Fn (1...𝑁))
236235adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → 𝑈 Fn (1...𝑁))
237 elfznn0 13596 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 ∈ ℕ0)
238237, 75syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...(𝑁 − 1)) → (𝑗 + 1) ∈ ℕ)
239238, 142eleqtrdi 2843 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...(𝑁 − 1)) → (𝑗 + 1) ∈ (ℤ‘1))
240 fzss1 13542 . . . . . . . . . . . . . . . . . . 19 ((𝑗 + 1) ∈ (ℤ‘1) → ((𝑗 + 1)...𝑁) ⊆ (1...𝑁))
241239, 240syl 17 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...(𝑁 − 1)) → ((𝑗 + 1)...𝑁) ⊆ (1...𝑁))
242241adantl 482 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → ((𝑗 + 1)...𝑁) ⊆ (1...𝑁))
24337adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) = 𝑁)
244 elfzuz3 13500 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (0...(𝑁 − 1)) → (𝑁 − 1) ∈ (ℤ𝑗))
245 eluzp1p1 12852 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 − 1) ∈ (ℤ𝑗) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑗 + 1)))
246244, 245syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑗 + 1)))
247246adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑗 + 1)))
248243, 247eqeltrrd 2834 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ‘(𝑗 + 1)))
249 eluzfz2 13511 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ (ℤ‘(𝑗 + 1)) → 𝑁 ∈ ((𝑗 + 1)...𝑁))
250248, 249syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ((𝑗 + 1)...𝑁))
251 fnfvima 7237 . . . . . . . . . . . . . . . . 17 ((𝑈 Fn (1...𝑁) ∧ ((𝑗 + 1)...𝑁) ⊆ (1...𝑁) ∧ 𝑁 ∈ ((𝑗 + 1)...𝑁)) → (𝑈𝑁) ∈ (𝑈 “ ((𝑗 + 1)...𝑁)))
252236, 242, 250, 251syl3anc 1371 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → (𝑈𝑁) ∈ (𝑈 “ ((𝑗 + 1)...𝑁)))
253252adantlr 713 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑈𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑈𝑁) ∈ (𝑈 “ ((𝑗 + 1)...𝑁)))
254233, 253eqeltrrd 2834 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑈𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (𝑈 “ ((𝑗 + 1)...𝑁)))
255 fnconstg 6779 . . . . . . . . . . . . . . . 16 (1 ∈ V → ((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗)))
25684, 255ax-mp 5 . . . . . . . . . . . . . . 15 ((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗))
257 fnconstg 6779 . . . . . . . . . . . . . . . 16 (0 ∈ V → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑁)))
258123, 257ax-mp 5 . . . . . . . . . . . . . . 15 ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑁))
259 fvun2 6983 . . . . . . . . . . . . . . 15 ((((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗)) ∧ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑁)) ∧ (((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅ ∧ 𝑁 ∈ (𝑈 “ ((𝑗 + 1)...𝑁)))) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁))
260256, 258, 259mp3an12 1451 . . . . . . . . . . . . . 14 ((((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅ ∧ 𝑁 ∈ (𝑈 “ ((𝑗 + 1)...𝑁))) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁))
261232, 254, 260syl2anc 584 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑈𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁))
262123fvconst2 7207 . . . . . . . . . . . . . 14 (𝑁 ∈ (𝑈 “ ((𝑗 + 1)...𝑁)) → (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁) = 0)
263254, 262syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑈𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁) = 0)
264261, 263eqtrd 2772 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑈𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
265264ralrimiva 3146 . . . . . . . . . . 11 ((𝜑 ∧ (𝑈𝑁) = 𝑁) → ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
266265ex 413 . . . . . . . . . 10 (𝜑 → ((𝑈𝑁) = 𝑁 → ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))
26732adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → (𝑁 − 1) ∈ (0...(𝑁 − 1)))
268 ax-1ne0 11181 . . . . . . . . . . . . . . 15 1 ≠ 0
269 imain 6633 . . . . . . . . . . . . . . . . . . . . 21 (Fun 𝑈 → (𝑈 “ ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑁 − 1))) ∩ (𝑈 “ (((𝑁 − 1) + 1)...𝑁))))
27048, 127, 2693syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑈 “ ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑁 − 1))) ∩ (𝑈 “ (((𝑁 − 1) + 1)...𝑁))))
271202, 37breqtrrd 5176 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑁 − 1) < ((𝑁 − 1) + 1))
272 fzdisj 13530 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 − 1) < ((𝑁 − 1) + 1) → ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁)) = ∅)
273271, 272syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁)) = ∅)
274273imaeq2d 6059 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑈 “ ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁))) = (𝑈 “ ∅))
275274, 60eqtrdi 2788 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑈 “ ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁))) = ∅)
276270, 275eqtr3d 2774 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑈 “ (1...(𝑁 − 1))) ∩ (𝑈 “ (((𝑁 − 1) + 1)...𝑁))) = ∅)
277276adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → ((𝑈 “ (1...(𝑁 − 1))) ∩ (𝑈 “ (((𝑁 − 1) + 1)...𝑁))) = ∅)
27891adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → 𝑁 ∈ (1...𝑁))
279 elimasni 6090 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ (𝑈 “ {𝑁}) → 𝑁𝑈𝑁)
280 fnbrfvb 6944 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑈 Fn (1...𝑁) ∧ 𝑁 ∈ (1...𝑁)) → ((𝑈𝑁) = 𝑁𝑁𝑈𝑁))
281235, 91, 280syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑈𝑁) = 𝑁𝑁𝑈𝑁))
282279, 281imbitrrid 245 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑁 ∈ (𝑈 “ {𝑁}) → (𝑈𝑁) = 𝑁))
283282necon3ad 2953 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑈𝑁) ≠ 𝑁 → ¬ 𝑁 ∈ (𝑈 “ {𝑁})))
284283imp 407 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → ¬ 𝑁 ∈ (𝑈 “ {𝑁}))
285278, 284eldifd 3959 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → 𝑁 ∈ ((1...𝑁) ∖ (𝑈 “ {𝑁})))
286 imadif 6632 . . . . . . . . . . . . . . . . . . . . . 22 (Fun 𝑈 → (𝑈 “ ((1...𝑁) ∖ {𝑁})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑁})))
28748, 127, 2863syl 18 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑈 “ ((1...𝑁) ∖ {𝑁})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑁})))
288 difun2 4480 . . . . . . . . . . . . . . . . . . . . . . 23 (((1...(𝑁 − 1)) ∪ {𝑁}) ∖ {𝑁}) = ((1...(𝑁 − 1)) ∖ {𝑁})
289 elun 4148 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ ((1...(𝑁 − 1)) ∪ {𝑁}) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 ∈ {𝑁}))
290 velsn 4644 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ {𝑁} ↔ 𝑗 = 𝑁)
291290orbi2i 911 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 ∈ {𝑁}) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 = 𝑁))
292289, 291bitri 274 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 ∈ ((1...(𝑁 − 1)) ∪ {𝑁}) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 = 𝑁))
29313, 142eleqtrdi 2843 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑁 ∈ (ℤ‘1))
294 fzm1 13583 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ (ℤ‘1) → (𝑗 ∈ (1...𝑁) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 = 𝑁)))
295293, 294syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝑗 ∈ (1...𝑁) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 = 𝑁)))
296292, 295bitr4id 289 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝑗 ∈ ((1...(𝑁 − 1)) ∪ {𝑁}) ↔ 𝑗 ∈ (1...𝑁)))
297296eqrdv 2730 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((1...(𝑁 − 1)) ∪ {𝑁}) = (1...𝑁))
298297difeq1d 4121 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((1...(𝑁 − 1)) ∪ {𝑁}) ∖ {𝑁}) = ((1...𝑁) ∖ {𝑁}))
299197, 23ltnled 11363 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((𝑁 − 1) < 𝑁 ↔ ¬ 𝑁 ≤ (𝑁 − 1)))
300202, 299mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ¬ 𝑁 ≤ (𝑁 − 1))
301 elfzle2 13507 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ (1...(𝑁 − 1)) → 𝑁 ≤ (𝑁 − 1))
302300, 301nsyl 140 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ¬ 𝑁 ∈ (1...(𝑁 − 1)))
303 difsn 4801 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑁 ∈ (1...(𝑁 − 1)) → ((1...(𝑁 − 1)) ∖ {𝑁}) = (1...(𝑁 − 1)))
304302, 303syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((1...(𝑁 − 1)) ∖ {𝑁}) = (1...(𝑁 − 1)))
305288, 298, 3043eqtr3a 2796 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1)))
306305imaeq2d 6059 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑈 “ ((1...𝑁) ∖ {𝑁})) = (𝑈 “ (1...(𝑁 − 1))))
30751difeq1d 4121 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑁})) = ((1...𝑁) ∖ (𝑈 “ {𝑁})))
308287, 306, 3073eqtr3rd 2781 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((1...𝑁) ∖ (𝑈 “ {𝑁})) = (𝑈 “ (1...(𝑁 − 1))))
309308adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → ((1...𝑁) ∖ (𝑈 “ {𝑁})) = (𝑈 “ (1...(𝑁 − 1))))
310285, 309eleqtrd 2835 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → 𝑁 ∈ (𝑈 “ (1...(𝑁 − 1))))
311 fnconstg 6779 . . . . . . . . . . . . . . . . . . . 20 (1 ∈ V → ((𝑈 “ (1...(𝑁 − 1))) × {1}) Fn (𝑈 “ (1...(𝑁 − 1))))
31284, 311ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((𝑈 “ (1...(𝑁 − 1))) × {1}) Fn (𝑈 “ (1...(𝑁 − 1)))
313 fnconstg 6779 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ V → ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑁 − 1) + 1)...𝑁)))
314123, 313ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑁 − 1) + 1)...𝑁))
315 fvun1 6982 . . . . . . . . . . . . . . . . . . 19 ((((𝑈 “ (1...(𝑁 − 1))) × {1}) Fn (𝑈 “ (1...(𝑁 − 1))) ∧ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑁 − 1) + 1)...𝑁)) ∧ (((𝑈 “ (1...(𝑁 − 1))) ∩ (𝑈 “ (((𝑁 − 1) + 1)...𝑁))) = ∅ ∧ 𝑁 ∈ (𝑈 “ (1...(𝑁 − 1))))) → ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ (1...(𝑁 − 1))) × {1})‘𝑁))
316312, 314, 315mp3an12 1451 . . . . . . . . . . . . . . . . . 18 ((((𝑈 “ (1...(𝑁 − 1))) ∩ (𝑈 “ (((𝑁 − 1) + 1)...𝑁))) = ∅ ∧ 𝑁 ∈ (𝑈 “ (1...(𝑁 − 1)))) → ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ (1...(𝑁 − 1))) × {1})‘𝑁))
317277, 310, 316syl2anc 584 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ (1...(𝑁 − 1))) × {1})‘𝑁))
31884fvconst2 7207 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ (𝑈 “ (1...(𝑁 − 1))) → (((𝑈 “ (1...(𝑁 − 1))) × {1})‘𝑁) = 1)
319310, 318syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → (((𝑈 “ (1...(𝑁 − 1))) × {1})‘𝑁) = 1)
320317, 319eqtrd 2772 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) = 1)
321320neeq1d 3000 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → (((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) ≠ 0 ↔ 1 ≠ 0))
322268, 321mpbiri 257 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) ≠ 0)
323 df-ne 2941 . . . . . . . . . . . . . . . 16 (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ≠ 0 ↔ ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
324 oveq2 7419 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = (𝑁 − 1) → (1...𝑗) = (1...(𝑁 − 1)))
325324imaeq2d 6059 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = (𝑁 − 1) → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...(𝑁 − 1))))
326325xpeq1d 5705 . . . . . . . . . . . . . . . . . . 19 (𝑗 = (𝑁 − 1) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑁 − 1))) × {1}))
327 oveq1 7418 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = (𝑁 − 1) → (𝑗 + 1) = ((𝑁 − 1) + 1))
328327oveq1d 7426 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = (𝑁 − 1) → ((𝑗 + 1)...𝑁) = (((𝑁 − 1) + 1)...𝑁))
329328imaeq2d 6059 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = (𝑁 − 1) → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ (((𝑁 − 1) + 1)...𝑁)))
330329xpeq1d 5705 . . . . . . . . . . . . . . . . . . 19 (𝑗 = (𝑁 − 1) → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))
331326, 330uneq12d 4164 . . . . . . . . . . . . . . . . . 18 (𝑗 = (𝑁 − 1) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0})))
332331fveq1d 6893 . . . . . . . . . . . . . . . . 17 (𝑗 = (𝑁 − 1) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁))
333332neeq1d 3000 . . . . . . . . . . . . . . . 16 (𝑗 = (𝑁 − 1) → (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ≠ 0 ↔ ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) ≠ 0))
334323, 333bitr3id 284 . . . . . . . . . . . . . . 15 (𝑗 = (𝑁 − 1) → (¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0 ↔ ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) ≠ 0))
335334rspcev 3612 . . . . . . . . . . . . . 14 (((𝑁 − 1) ∈ (0...(𝑁 − 1)) ∧ ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) ≠ 0) → ∃𝑗 ∈ (0...(𝑁 − 1)) ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
336267, 322, 335syl2anc 584 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → ∃𝑗 ∈ (0...(𝑁 − 1)) ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
337336ex 413 . . . . . . . . . . . 12 (𝜑 → ((𝑈𝑁) ≠ 𝑁 → ∃𝑗 ∈ (0...(𝑁 − 1)) ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))
338 rexnal 3100 . . . . . . . . . . . 12 (∃𝑗 ∈ (0...(𝑁 − 1)) ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0 ↔ ¬ ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
339337, 338imbitrdi 250 . . . . . . . . . . 11 (𝜑 → ((𝑈𝑁) ≠ 𝑁 → ¬ ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))
340339necon4ad 2959 . . . . . . . . . 10 (𝜑 → (∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0 → (𝑈𝑁) = 𝑁))
341266, 340impbid 211 . . . . . . . . 9 (𝜑 → ((𝑈𝑁) = 𝑁 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))
342224, 341anbi12d 631 . . . . . . . 8 (𝜑 → (((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁) ↔ (∀𝑗 ∈ (0...(𝑁 − 1))(𝑇𝑁) = 0 ∧ ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
343 r19.26 3111 . . . . . . . 8 (∀𝑗 ∈ (0...(𝑁 − 1))((𝑇𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0) ↔ (∀𝑗 ∈ (0...(𝑁 − 1))(𝑇𝑁) = 0 ∧ ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))
344342, 343bitr4di 288 . . . . . . 7 (𝜑 → (((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁) ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((𝑇𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
345344adantr 481 . . . . . 6 ((𝜑𝑉 = 𝑁) → (((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁) ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((𝑇𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
346191, 221, 3453bitr4d 310 . . . . 5 ((𝜑𝑉 = 𝑁) → (∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁)))
347346pm5.32da 579 . . . 4 (𝜑 → ((𝑉 = 𝑁 ∧ ∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0) ↔ (𝑉 = 𝑁 ∧ ((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁))))
348110, 347bitrd 278 . . 3 (𝜑 → (∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ (𝑉 = 𝑁 ∧ ((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁))))
349348notbid 317 . 2 (𝜑 → (¬ ∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ¬ (𝑉 = 𝑁 ∧ ((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁))))
35012, 349bitrid 282 1 (𝜑 → (∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝𝑁) ≠ 0 ↔ ¬ (𝑉 = 𝑁 ∧ ((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845   = wceq 1541  wcel 2106  wne 2940  wral 3061  wrex 3070  Vcvv 3474  csb 3893  cdif 3945  cun 3946  cin 3947  wss 3948  c0 4322  ifcif 4528  {csn 4628   class class class wbr 5148  cmpt 5231   × cxp 5674  ccnv 5675  ran crn 5677  cima 5679  Fun wfun 6537   Fn wfn 6538  wf 6539  ontowfo 6541  1-1-ontowf1o 6542  cfv 6543  (class class class)co 7411  f cof 7670  cc 11110  cr 11111  0cc0 11112  1c1 11113   + caddc 11115   < clt 11250  cle 11251  cmin 11446  cn 12214  0cn0 12474  cz 12560  cuz 12824  ...cfz 13486  ..^cfzo 13629
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-of 7672  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11252  df-mnf 11253  df-xr 11254  df-ltxr 11255  df-le 11256  df-sub 11448  df-neg 11449  df-nn 12215  df-n0 12475  df-z 12561  df-uz 12825  df-fz 13487  df-fzo 13630
This theorem is referenced by:  poimirlem24  36604
  Copyright terms: Public domain W3C validator