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

Theorem poimirlem23 35026
 Description: Lemma for poimir 35036, 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 7183 . . . . . 6 (𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
21csbex 5202 . . . . 5 if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
32rgenw 3145 . . . 4 𝑦 ∈ (0...(𝑁 − 1))if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
4 eqid 2824 . . . . 5 (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
5 fveq1 6661 . . . . . . 7 (𝑝 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) → (𝑝𝑁) = (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁))
65neeq1d 3073 . . . . . 6 (𝑝 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) → ((𝑝𝑁) ≠ 0 ↔ (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0))
7 df-ne 3015 . . . . . 6 ((if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0 ↔ ¬ (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
86, 7syl6bb 290 . . . . 5 (𝑝 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) → ((𝑝𝑁) ≠ 0 ↔ ¬ (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
94, 8rexrnmptw 6853 . . . 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 3233 . . 3 (∃𝑦 ∈ (0...(𝑁 − 1)) ¬ (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ¬ ∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
1210, 11bitri 278 . 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 12086 . . . . . . . . . 10 (𝜑𝑁 ∈ ℤ)
15 poimirlem23.3 . . . . . . . . . . 11 (𝜑𝑉 ∈ (0...𝑁))
16 elfzelz 12914 . . . . . . . . . . 11 (𝑉 ∈ (0...𝑁) → 𝑉 ∈ ℤ)
1715, 16syl 17 . . . . . . . . . 10 (𝜑𝑉 ∈ ℤ)
18 zlem1lt 12034 . . . . . . . . . 10 ((𝑁 ∈ ℤ ∧ 𝑉 ∈ ℤ) → (𝑁𝑉 ↔ (𝑁 − 1) < 𝑉))
1914, 17, 18syl2anc 587 . . . . . . . . 9 (𝜑 → (𝑁𝑉 ↔ (𝑁 − 1) < 𝑉))
20 elfzle2 12918 . . . . . . . . . . 11 (𝑉 ∈ (0...𝑁) → 𝑉𝑁)
2115, 20syl 17 . . . . . . . . . 10 (𝜑𝑉𝑁)
2217zred 12087 . . . . . . . . . . . 12 (𝜑𝑉 ∈ ℝ)
2313nnred 11652 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℝ)
2422, 23letri3d 10781 . . . . . . . . . . 11 (𝜑 → (𝑉 = 𝑁 ↔ (𝑉𝑁𝑁𝑉)))
2524biimprd 251 . . . . . . . . . 10 (𝜑 → ((𝑉𝑁𝑁𝑉) → 𝑉 = 𝑁))
2621, 25mpand 694 . . . . . . . . 9 (𝜑 → (𝑁𝑉𝑉 = 𝑁))
2719, 26sylbird 263 . . . . . . . 8 (𝜑 → ((𝑁 − 1) < 𝑉𝑉 = 𝑁))
2827necon3ad 3027 . . . . . . 7 (𝜑 → (𝑉𝑁 → ¬ (𝑁 − 1) < 𝑉))
29 nnm1nn0 11938 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
3013, 29syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑁 − 1) ∈ ℕ0)
31 nn0fz0 13012 . . . . . . . . . . . 12 ((𝑁 − 1) ∈ ℕ0 ↔ (𝑁 − 1) ∈ (0...(𝑁 − 1)))
3230, 31sylib 221 . . . . . . . . . . 11 (𝜑 → (𝑁 − 1) ∈ (0...(𝑁 − 1)))
3332adantr 484 . . . . . . . . . 10 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → (𝑁 − 1) ∈ (0...(𝑁 − 1)))
34 iffalse 4460 . . . . . . . . . . . . . . . 16 (¬ (𝑁 − 1) < 𝑉 → if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) = ((𝑁 − 1) + 1))
3513nncnd 11653 . . . . . . . . . . . . . . . . 17 (𝜑𝑁 ∈ ℂ)
36 npcan1 11064 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
3735, 36syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
3834, 37sylan9eqr 2881 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) = 𝑁)
3938csbeq1d 3871 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = 𝑁 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
40 oveq2 7158 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑁 → (1...𝑗) = (1...𝑁))
4140imaeq2d 5917 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑁 → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...𝑁)))
4241xpeq1d 5572 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑁 → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...𝑁)) × {1}))
43 oveq1 7157 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑁 → (𝑗 + 1) = (𝑁 + 1))
4443oveq1d 7165 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑁 → ((𝑗 + 1)...𝑁) = ((𝑁 + 1)...𝑁))
4544imaeq2d 5917 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑁 → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ ((𝑁 + 1)...𝑁)))
4645xpeq1d 5572 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑁 → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0}))
4742, 46uneq12d 4127 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑁 → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...𝑁)) × {1}) ∪ ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0})))
48 poimirlem23.2 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑈:(1...𝑁)–1-1-onto→(1...𝑁))
49 f1ofo 6614 . . . . . . . . . . . . . . . . . . . . . 22 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)–onto→(1...𝑁))
50 foima 6587 . . . . . . . . . . . . . . . . . . . . . 22 (𝑈:(1...𝑁)–onto→(1...𝑁) → (𝑈 “ (1...𝑁)) = (1...𝑁))
5148, 49, 503syl 18 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑈 “ (1...𝑁)) = (1...𝑁))
5251xpeq1d 5572 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑈 “ (1...𝑁)) × {1}) = ((1...𝑁) × {1}))
5323ltp1d 11569 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑁 < (𝑁 + 1))
5414peano2zd 12090 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝑁 + 1) ∈ ℤ)
55 fzn 12930 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑁 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 < (𝑁 + 1) ↔ ((𝑁 + 1)...𝑁) = ∅))
5654, 14, 55syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑁 < (𝑁 + 1) ↔ ((𝑁 + 1)...𝑁) = ∅))
5753, 56mpbid 235 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑁 + 1)...𝑁) = ∅)
5857imaeq2d 5917 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑈 “ ((𝑁 + 1)...𝑁)) = (𝑈 “ ∅))
5958xpeq1d 5572 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0}) = ((𝑈 “ ∅) × {0}))
60 ima0 5933 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑈 “ ∅) = ∅
6160xpeq1i 5569 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑈 “ ∅) × {0}) = (∅ × {0})
62 0xp 5637 . . . . . . . . . . . . . . . . . . . . . 22 (∅ × {0}) = ∅
6361, 62eqtri 2847 . . . . . . . . . . . . . . . . . . . . 21 ((𝑈 “ ∅) × {0}) = ∅
6459, 63syl6eq 2875 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0}) = ∅)
6552, 64uneq12d 4127 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((𝑈 “ (1...𝑁)) × {1}) ∪ ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0})) = (((1...𝑁) × {1}) ∪ ∅))
66 un0 4328 . . . . . . . . . . . . . . . . . . 19 (((1...𝑁) × {1}) ∪ ∅) = ((1...𝑁) × {1})
6765, 66syl6eq 2875 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((𝑈 “ (1...𝑁)) × {1}) ∪ ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0})) = ((1...𝑁) × {1}))
6847, 67sylan9eqr 2881 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 = 𝑁) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = ((1...𝑁) × {1}))
6968oveq2d 7166 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 = 𝑁) → (𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇f + ((1...𝑁) × {1})))
7013, 69csbied 3903 . . . . . . . . . . . . . . 15 (𝜑𝑁 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇f + ((1...𝑁) × {1})))
7170adantr 484 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → 𝑁 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇f + ((1...𝑁) × {1})))
7239, 71eqtrd 2859 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇f + ((1...𝑁) × {1})))
7372fveq1d 6664 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → (if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = ((𝑇f + ((1...𝑁) × {1}))‘𝑁))
74 elfzonn0 13089 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0..^𝐾) → 𝑗 ∈ ℕ0)
75 nn0p1nn 11936 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ0 → (𝑗 + 1) ∈ ℕ)
7674, 75syl 17 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0..^𝐾) → (𝑗 + 1) ∈ ℕ)
77 elsni 4568 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ {1} → 𝑦 = 1)
7877oveq2d 7166 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ {1} → (𝑗 + 𝑦) = (𝑗 + 1))
7978eleq1d 2900 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ {1} → ((𝑗 + 𝑦) ∈ ℕ ↔ (𝑗 + 1) ∈ ℕ))
8076, 79syl5ibrcom 250 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0..^𝐾) → (𝑦 ∈ {1} → (𝑗 + 𝑦) ∈ ℕ))
8180imp 410 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (0..^𝐾) ∧ 𝑦 ∈ {1}) → (𝑗 + 𝑦) ∈ ℕ)
8281adantl 485 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗 ∈ (0..^𝐾) ∧ 𝑦 ∈ {1})) → (𝑗 + 𝑦) ∈ ℕ)
83 poimirlem23.1 . . . . . . . . . . . . . . 15 (𝜑𝑇:(1...𝑁)⟶(0..^𝐾))
84 1ex 10636 . . . . . . . . . . . . . . . . 17 1 ∈ V
8584fconst 6556 . . . . . . . . . . . . . . . 16 ((1...𝑁) × {1}):(1...𝑁)⟶{1}
8685a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → ((1...𝑁) × {1}):(1...𝑁)⟶{1})
87 ovexd 7185 . . . . . . . . . . . . . . 15 (𝜑 → (1...𝑁) ∈ V)
88 inidm 4181 . . . . . . . . . . . . . . 15 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
8982, 83, 86, 87, 87, 88off 7419 . . . . . . . . . . . . . 14 (𝜑 → (𝑇f + ((1...𝑁) × {1})):(1...𝑁)⟶ℕ)
90 elfz1end 12944 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℕ ↔ 𝑁 ∈ (1...𝑁))
9113, 90sylib 221 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ (1...𝑁))
9289, 91ffvelrnd 6844 . . . . . . . . . . . . 13 (𝜑 → ((𝑇f + ((1...𝑁) × {1}))‘𝑁) ∈ ℕ)
9392adantr 484 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → ((𝑇f + ((1...𝑁) × {1}))‘𝑁) ∈ ℕ)
9473, 93eqeltrd 2916 . . . . . . . . . . 11 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → (if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ∈ ℕ)
9594nnne0d 11687 . . . . . . . . . 10 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → (if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0)
96 breq1 5056 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑁 − 1) → (𝑦 < 𝑉 ↔ (𝑁 − 1) < 𝑉))
97 id 22 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑁 − 1) → 𝑦 = (𝑁 − 1))
98 oveq1 7157 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑁 − 1) → (𝑦 + 1) = ((𝑁 − 1) + 1))
9996, 97, 98ifbieq12d 4478 . . . . . . . . . . . . . . 15 (𝑦 = (𝑁 − 1) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) = if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)))
10099csbeq1d 3871 . . . . . . . . . . . . . 14 (𝑦 = (𝑁 − 1) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
101100fveq1d 6664 . . . . . . . . . . . . 13 (𝑦 = (𝑁 − 1) → (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = (if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁))
102101neeq1d 3073 . . . . . . . . . . . 12 (𝑦 = (𝑁 − 1) → ((if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0 ↔ (if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0))
1037, 102bitr3id 288 . . . . . . . . . . 11 (𝑦 = (𝑁 − 1) → (¬ (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ (if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0))
104103rspcev 3610 . . . . . . . . . 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 587 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → ∃𝑦 ∈ (0...(𝑁 − 1)) ¬ (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
106105, 11sylib 221 . . . . . . . 8 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → ¬ ∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
107106ex 416 . . . . . . 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 3033 . . . . 5 (𝜑 → (∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 → 𝑉 = 𝑁))
110109pm4.71rd 566 . . . 4 (𝜑 → (∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ (𝑉 = 𝑁 ∧ ∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)))
11130nn0zd 12085 . . . . . . . . . . . . 13 (𝜑 → (𝑁 − 1) ∈ ℤ)
112 uzid 12258 . . . . . . . . . . . . 13 ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)))
113 peano2uz 12301 . . . . . . . . . . . . 13 ((𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
114111, 112, 1133syl 18 . . . . . . . . . . . 12 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
11537, 114eqeltrrd 2917 . . . . . . . . . . 11 (𝜑𝑁 ∈ (ℤ‘(𝑁 − 1)))
116 fzss2 12954 . . . . . . . . . . 11 (𝑁 ∈ (ℤ‘(𝑁 − 1)) → (0...(𝑁 − 1)) ⊆ (0...𝑁))
117115, 116syl 17 . . . . . . . . . 10 (𝜑 → (0...(𝑁 − 1)) ⊆ (0...𝑁))
118117sselda 3954 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → 𝑗 ∈ (0...𝑁))
11991adantr 484 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑁 ∈ (1...𝑁))
12083ffnd 6505 . . . . . . . . . . . . . 14 (𝜑𝑇 Fn (1...𝑁))
121120adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑇 Fn (1...𝑁))
12284fconst 6556 . . . . . . . . . . . . . . . . 17 ((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1}
123 c0ex 10634 . . . . . . . . . . . . . . . . . 18 0 ∈ V
124123fconst 6556 . . . . . . . . . . . . . . . . 17 ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0}
125122, 124pm3.2i 474 . . . . . . . . . . . . . . . 16 (((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1} ∧ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0})
126 dff1o3 6613 . . . . . . . . . . . . . . . . . . 19 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (𝑈:(1...𝑁)–onto→(1...𝑁) ∧ Fun 𝑈))
127126simprbi 500 . . . . . . . . . . . . . . . . . 18 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → Fun 𝑈)
128 imain 6428 . . . . . . . . . . . . . . . . . 18 (Fun 𝑈 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))))
12948, 127, 1283syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))))
130 elfzelz 12914 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℤ)
131130zred 12087 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℝ)
132131ltp1d 11569 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...𝑁) → 𝑗 < (𝑗 + 1))
133 fzdisj 12941 . . . . . . . . . . . . . . . . . . . 20 (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
134132, 133syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑁) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
135134imaeq2d 5917 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑁) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (𝑈 “ ∅))
136135, 60syl6eq 2875 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑁) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ∅)
137129, 136sylan9req 2880 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅)
138 fun 6531 . . . . . . . . . . . . . . . 16 (((((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1} ∧ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0}) ∧ ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}))
139125, 137, 138sylancr 590 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...𝑁)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}))
140 elfznn0 13007 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℕ0)
141140, 75syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ ℕ)
142 nnuz 12281 . . . . . . . . . . . . . . . . . . . . 21 ℕ = (ℤ‘1)
143141, 142eleqtrdi 2926 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ (ℤ‘1))
144 elfzuz3 12911 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...𝑁) → 𝑁 ∈ (ℤ𝑗))
145 fzsplit2 12939 . . . . . . . . . . . . . . . . . . . 20 (((𝑗 + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ𝑗)) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
146143, 144, 145syl2anc 587 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑁) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
147146imaeq2d 5917 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑁) → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))))
148 imaundi 5996 . . . . . . . . . . . . . . . . . 18 (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))
149147, 148syl6req 2876 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑁) → ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁))) = (𝑈 “ (1...𝑁)))
150149, 51sylan9eqr 2881 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁))) = (1...𝑁))
151150feq2d 6490 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...𝑁)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}) ↔ (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0})))
152139, 151mpbid 235 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑁)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0}))
153152ffnd 6505 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑁)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) Fn (1...𝑁))
154 ovexd 7185 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑁)) → (1...𝑁) ∈ V)
155 eqidd 2825 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑁 ∈ (1...𝑁)) → (𝑇𝑁) = (𝑇𝑁))
156 eqidd 2825 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑁 ∈ (1...𝑁)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))
157121, 153, 154, 154, 88, 155, 156ofval 7413 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑁 ∈ (1...𝑁)) → ((𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = ((𝑇𝑁) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)))
158119, 157mpdan 686 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = ((𝑇𝑁) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)))
159158eqeq1d 2826 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑁)) → (((𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ((𝑇𝑁) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)) = 0))
16083, 91ffvelrnd 6844 . . . . . . . . . . . . . 14 (𝜑 → (𝑇𝑁) ∈ (0..^𝐾))
161 elfzonn0 13089 . . . . . . . . . . . . . 14 ((𝑇𝑁) ∈ (0..^𝐾) → (𝑇𝑁) ∈ ℕ0)
162160, 161syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑇𝑁) ∈ ℕ0)
163162nn0red 11956 . . . . . . . . . . . 12 (𝜑 → (𝑇𝑁) ∈ ℝ)
164163adantr 484 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑇𝑁) ∈ ℝ)
165162nn0ge0d 11958 . . . . . . . . . . . 12 (𝜑 → 0 ≤ (𝑇𝑁))
166165adantr 484 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑁)) → 0 ≤ (𝑇𝑁))
167 1re 10640 . . . . . . . . . . . . . 14 1 ∈ ℝ
168 snssi 4726 . . . . . . . . . . . . . 14 (1 ∈ ℝ → {1} ⊆ ℝ)
169167, 168ax-mp 5 . . . . . . . . . . . . 13 {1} ⊆ ℝ
170 0re 10642 . . . . . . . . . . . . . 14 0 ∈ ℝ
171 snssi 4726 . . . . . . . . . . . . . 14 (0 ∈ ℝ → {0} ⊆ ℝ)
172170, 171ax-mp 5 . . . . . . . . . . . . 13 {0} ⊆ ℝ
173169, 172unssi 4148 . . . . . . . . . . . 12 ({1} ∪ {0}) ⊆ ℝ
174152, 119ffvelrnd 6844 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑁)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ ({1} ∪ {0}))
175173, 174sseldi 3952 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑁)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ ℝ)
176 elun 4112 . . . . . . . . . . . . 13 (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ ({1} ∪ {0}) ↔ (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {1} ∨ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {0}))
177 0le1 11162 . . . . . . . . . . . . . . 15 0 ≤ 1
178 elsni 4568 . . . . . . . . . . . . . . 15 (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {1} → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 1)
179177, 178breqtrrid 5091 . . . . . . . . . . . . . 14 (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {1} → 0 ≤ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))
180 0le0 11738 . . . . . . . . . . . . . . 15 0 ≤ 0
181 elsni 4568 . . . . . . . . . . . . . . 15 (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {0} → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
182180, 181breqtrrid 5091 . . . . . . . . . . . . . 14 (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {0} → 0 ≤ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))
183179, 182jaoi 854 . . . . . . . . . . . . 13 ((((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {1} ∨ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {0}) → 0 ≤ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))
184176, 183sylbi 220 . . . . . . . . . . . 12 (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ ({1} ∪ {0}) → 0 ≤ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))
185174, 184syl 17 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑁)) → 0 ≤ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))
186 add20 11151 . . . . . . . . . . 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 282 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑁)) → (((𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ((𝑇𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
189118, 188syldan 594 . . . . . . . 8 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → (((𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ((𝑇𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
190189ralbidva 3191 . . . . . . 7 (𝜑 → (∀𝑗 ∈ (0...(𝑁 − 1))((𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((𝑇𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
191190adantr 484 . . . . . 6 ((𝜑𝑉 = 𝑁) → (∀𝑗 ∈ (0...(𝑁 − 1))((𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((𝑇𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
192 breq2 5057 . . . . . . . . . . . . . 14 (𝑉 = 𝑁 → (𝑦 < 𝑉𝑦 < 𝑁))
193192ifbid 4473 . . . . . . . . . . . . 13 (𝑉 = 𝑁 → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) = if(𝑦 < 𝑁, 𝑦, (𝑦 + 1)))
194 elfzelz 12914 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℤ)
195194zred 12087 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℝ)
196195adantl 485 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ∈ ℝ)
19730nn0red 11956 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑁 − 1) ∈ ℝ)
198197adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ)
19923adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℝ)
200 elfzle2 12918 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ≤ (𝑁 − 1))
201200adantl 485 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ≤ (𝑁 − 1))
20223ltm1d 11571 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑁 − 1) < 𝑁)
203202adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑁 − 1) < 𝑁)
204196, 198, 199, 201, 203lelttrd 10797 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 < 𝑁)
205204iftrued 4459 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < 𝑁, 𝑦, (𝑦 + 1)) = 𝑦)
206193, 205sylan9eqr 2881 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑉 = 𝑁) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) = 𝑦)
207206an32s 651 . . . . . . . . . . 11 (((𝜑𝑉 = 𝑁) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) = 𝑦)
208207csbeq1d 3871 . . . . . . . . . 10 (((𝜑𝑉 = 𝑁) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = 𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
209208fveq1d 6664 . . . . . . . . 9 (((𝜑𝑉 = 𝑁) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = (𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁))
210209eqeq1d 2826 . . . . . . . 8 (((𝜑𝑉 = 𝑁) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ (𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
211210ralbidva 3191 . . . . . . 7 ((𝜑𝑉 = 𝑁) → (∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ∀𝑦 ∈ (0...(𝑁 − 1))(𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
212 nfv 1916 . . . . . . . 8 𝑦((𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0
213 nfcsb1v 3891 . . . . . . . . . 10 𝑗𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))
214 nfcv 2982 . . . . . . . . . 10 𝑗𝑁
215213, 214nffv 6672 . . . . . . . . 9 𝑗(𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁)
216215nfeq1 2997 . . . . . . . 8 𝑗(𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0
217 csbeq1a 3881 . . . . . . . . . 10 (𝑗 = 𝑦 → (𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = 𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
218217fveq1d 6664 . . . . . . . . 9 (𝑗 = 𝑦 → ((𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = (𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁))
219218eqeq1d 2826 . . . . . . . 8 (𝑗 = 𝑦 → (((𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ (𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
220212, 216, 219cbvralw 3426 . . . . . . 7 (∀𝑗 ∈ (0...(𝑁 − 1))((𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ∀𝑦 ∈ (0...(𝑁 − 1))(𝑦 / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
221211, 220syl6bbr 292 . . . . . 6 ((𝜑𝑉 = 𝑁) → (∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
222 ne0i 4284 . . . . . . . . . 10 ((𝑁 − 1) ∈ (0...(𝑁 − 1)) → (0...(𝑁 − 1)) ≠ ∅)
223 r19.3rzv 4428 . . . . . . . . . 10 ((0...(𝑁 − 1)) ≠ ∅ → ((𝑇𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))(𝑇𝑁) = 0))
22432, 222, 2233syl 18 . . . . . . . . 9 (𝜑 → ((𝑇𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))(𝑇𝑁) = 0))
225 elfzelz 12914 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 ∈ ℤ)
226225zred 12087 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 ∈ ℝ)
227226ltp1d 11569 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 < (𝑗 + 1))
228227, 133syl 17 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...(𝑁 − 1)) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
229228imaeq2d 5917 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...(𝑁 − 1)) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (𝑈 “ ∅))
230229, 60syl6eq 2875 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...(𝑁 − 1)) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ∅)
231129, 230sylan9req 2880 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅)
232231adantlr 714 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑈𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅)
233 simplr 768 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑈𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑈𝑁) = 𝑁)
234 f1ofn 6608 . . . . . . . . . . . . . . . . . . 19 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈 Fn (1...𝑁))
23548, 234syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝑈 Fn (1...𝑁))
236235adantr 484 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → 𝑈 Fn (1...𝑁))
237 elfznn0 13007 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 ∈ ℕ0)
238237, 75syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...(𝑁 − 1)) → (𝑗 + 1) ∈ ℕ)
239238, 142eleqtrdi 2926 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...(𝑁 − 1)) → (𝑗 + 1) ∈ (ℤ‘1))
240 fzss1 12953 . . . . . . . . . . . . . . . . . . 19 ((𝑗 + 1) ∈ (ℤ‘1) → ((𝑗 + 1)...𝑁) ⊆ (1...𝑁))
241239, 240syl 17 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...(𝑁 − 1)) → ((𝑗 + 1)...𝑁) ⊆ (1...𝑁))
242241adantl 485 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → ((𝑗 + 1)...𝑁) ⊆ (1...𝑁))
24337adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) = 𝑁)
244 elfzuz3 12911 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (0...(𝑁 − 1)) → (𝑁 − 1) ∈ (ℤ𝑗))
245 eluzp1p1 12270 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 − 1) ∈ (ℤ𝑗) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑗 + 1)))
246244, 245syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑗 + 1)))
247246adantl 485 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑗 + 1)))
248243, 247eqeltrrd 2917 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ‘(𝑗 + 1)))
249 eluzfz2 12922 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ (ℤ‘(𝑗 + 1)) → 𝑁 ∈ ((𝑗 + 1)...𝑁))
250248, 249syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ((𝑗 + 1)...𝑁))
251 fnfvima 6988 . . . . . . . . . . . . . . . . 17 ((𝑈 Fn (1...𝑁) ∧ ((𝑗 + 1)...𝑁) ⊆ (1...𝑁) ∧ 𝑁 ∈ ((𝑗 + 1)...𝑁)) → (𝑈𝑁) ∈ (𝑈 “ ((𝑗 + 1)...𝑁)))
252236, 242, 250, 251syl3anc 1368 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → (𝑈𝑁) ∈ (𝑈 “ ((𝑗 + 1)...𝑁)))
253252adantlr 714 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑈𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑈𝑁) ∈ (𝑈 “ ((𝑗 + 1)...𝑁)))
254233, 253eqeltrrd 2917 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑈𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (𝑈 “ ((𝑗 + 1)...𝑁)))
255 fnconstg 6558 . . . . . . . . . . . . . . . 16 (1 ∈ V → ((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗)))
25684, 255ax-mp 5 . . . . . . . . . . . . . . 15 ((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗))
257 fnconstg 6558 . . . . . . . . . . . . . . . 16 (0 ∈ V → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑁)))
258123, 257ax-mp 5 . . . . . . . . . . . . . . 15 ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑁))
259 fvun2 6747 . . . . . . . . . . . . . . 15 ((((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗)) ∧ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑁)) ∧ (((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅ ∧ 𝑁 ∈ (𝑈 “ ((𝑗 + 1)...𝑁)))) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁))
260256, 258, 259mp3an12 1448 . . . . . . . . . . . . . 14 ((((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅ ∧ 𝑁 ∈ (𝑈 “ ((𝑗 + 1)...𝑁))) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁))
261232, 254, 260syl2anc 587 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑈𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁))
262123fvconst2 6958 . . . . . . . . . . . . . 14 (𝑁 ∈ (𝑈 “ ((𝑗 + 1)...𝑁)) → (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁) = 0)
263254, 262syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑈𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁) = 0)
264261, 263eqtrd 2859 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑈𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
265264ralrimiva 3177 . . . . . . . . . . 11 ((𝜑 ∧ (𝑈𝑁) = 𝑁) → ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
266265ex 416 . . . . . . . . . 10 (𝜑 → ((𝑈𝑁) = 𝑁 → ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))
26732adantr 484 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → (𝑁 − 1) ∈ (0...(𝑁 − 1)))
268 ax-1ne0 10605 . . . . . . . . . . . . . . 15 1 ≠ 0
269 imain 6428 . . . . . . . . . . . . . . . . . . . . 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 5081 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑁 − 1) < ((𝑁 − 1) + 1))
272 fzdisj 12941 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 − 1) < ((𝑁 − 1) + 1) → ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁)) = ∅)
273271, 272syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁)) = ∅)
274273imaeq2d 5917 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑈 “ ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁))) = (𝑈 “ ∅))
275274, 60syl6eq 2875 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑈 “ ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁))) = ∅)
276270, 275eqtr3d 2861 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑈 “ (1...(𝑁 − 1))) ∩ (𝑈 “ (((𝑁 − 1) + 1)...𝑁))) = ∅)
277276adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → ((𝑈 “ (1...(𝑁 − 1))) ∩ (𝑈 “ (((𝑁 − 1) + 1)...𝑁))) = ∅)
27891adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → 𝑁 ∈ (1...𝑁))
279 elimasni 5944 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ (𝑈 “ {𝑁}) → 𝑁𝑈𝑁)
280 fnbrfvb 6710 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑈 Fn (1...𝑁) ∧ 𝑁 ∈ (1...𝑁)) → ((𝑈𝑁) = 𝑁𝑁𝑈𝑁))
281235, 91, 280syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑈𝑁) = 𝑁𝑁𝑈𝑁))
282279, 281syl5ibr 249 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑁 ∈ (𝑈 “ {𝑁}) → (𝑈𝑁) = 𝑁))
283282necon3ad 3027 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑈𝑁) ≠ 𝑁 → ¬ 𝑁 ∈ (𝑈 “ {𝑁})))
284283imp 410 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → ¬ 𝑁 ∈ (𝑈 “ {𝑁}))
285278, 284eldifd 3931 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → 𝑁 ∈ ((1...𝑁) ∖ (𝑈 “ {𝑁})))
286 imadif 6427 . . . . . . . . . . . . . . . . . . . . . 22 (Fun 𝑈 → (𝑈 “ ((1...𝑁) ∖ {𝑁})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑁})))
28748, 127, 2863syl 18 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑈 “ ((1...𝑁) ∖ {𝑁})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑁})))
288 difun2 4413 . . . . . . . . . . . . . . . . . . . . . . 23 (((1...(𝑁 − 1)) ∪ {𝑁}) ∖ {𝑁}) = ((1...(𝑁 − 1)) ∖ {𝑁})
28913, 142eleqtrdi 2926 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑁 ∈ (ℤ‘1))
290 fzm1 12994 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ (ℤ‘1) → (𝑗 ∈ (1...𝑁) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 = 𝑁)))
291289, 290syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝑗 ∈ (1...𝑁) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 = 𝑁)))
292 elun 4112 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ ((1...(𝑁 − 1)) ∪ {𝑁}) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 ∈ {𝑁}))
293 velsn 4567 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ {𝑁} ↔ 𝑗 = 𝑁)
294293orbi2i 910 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 ∈ {𝑁}) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 = 𝑁))
295292, 294bitri 278 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 ∈ ((1...(𝑁 − 1)) ∪ {𝑁}) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 = 𝑁))
296291, 295syl6rbbr 293 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝑗 ∈ ((1...(𝑁 − 1)) ∪ {𝑁}) ↔ 𝑗 ∈ (1...𝑁)))
297296eqrdv 2822 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((1...(𝑁 − 1)) ∪ {𝑁}) = (1...𝑁))
298297difeq1d 4085 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((1...(𝑁 − 1)) ∪ {𝑁}) ∖ {𝑁}) = ((1...𝑁) ∖ {𝑁}))
299197, 23ltnled 10786 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((𝑁 − 1) < 𝑁 ↔ ¬ 𝑁 ≤ (𝑁 − 1)))
300202, 299mpbid 235 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ¬ 𝑁 ≤ (𝑁 − 1))
301 elfzle2 12918 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ (1...(𝑁 − 1)) → 𝑁 ≤ (𝑁 − 1))
302300, 301nsyl 142 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ¬ 𝑁 ∈ (1...(𝑁 − 1)))
303 difsn 4716 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑁 ∈ (1...(𝑁 − 1)) → ((1...(𝑁 − 1)) ∖ {𝑁}) = (1...(𝑁 − 1)))
304302, 303syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((1...(𝑁 − 1)) ∖ {𝑁}) = (1...(𝑁 − 1)))
305288, 298, 3043eqtr3a 2883 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1)))
306305imaeq2d 5917 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑈 “ ((1...𝑁) ∖ {𝑁})) = (𝑈 “ (1...(𝑁 − 1))))
30751difeq1d 4085 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑁})) = ((1...𝑁) ∖ (𝑈 “ {𝑁})))
308287, 306, 3073eqtr3rd 2868 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((1...𝑁) ∖ (𝑈 “ {𝑁})) = (𝑈 “ (1...(𝑁 − 1))))
309308adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → ((1...𝑁) ∖ (𝑈 “ {𝑁})) = (𝑈 “ (1...(𝑁 − 1))))
310285, 309eleqtrd 2918 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → 𝑁 ∈ (𝑈 “ (1...(𝑁 − 1))))
311 fnconstg 6558 . . . . . . . . . . . . . . . . . . . 20 (1 ∈ V → ((𝑈 “ (1...(𝑁 − 1))) × {1}) Fn (𝑈 “ (1...(𝑁 − 1))))
31284, 311ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((𝑈 “ (1...(𝑁 − 1))) × {1}) Fn (𝑈 “ (1...(𝑁 − 1)))
313 fnconstg 6558 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ V → ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑁 − 1) + 1)...𝑁)))
314123, 313ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑁 − 1) + 1)...𝑁))
315 fvun1 6746 . . . . . . . . . . . . . . . . . . 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 1448 . . . . . . . . . . . . . . . . . 18 ((((𝑈 “ (1...(𝑁 − 1))) ∩ (𝑈 “ (((𝑁 − 1) + 1)...𝑁))) = ∅ ∧ 𝑁 ∈ (𝑈 “ (1...(𝑁 − 1)))) → ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ (1...(𝑁 − 1))) × {1})‘𝑁))
317277, 310, 316syl2anc 587 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ (1...(𝑁 − 1))) × {1})‘𝑁))
31884fvconst2 6958 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ (𝑈 “ (1...(𝑁 − 1))) → (((𝑈 “ (1...(𝑁 − 1))) × {1})‘𝑁) = 1)
319310, 318syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → (((𝑈 “ (1...(𝑁 − 1))) × {1})‘𝑁) = 1)
320317, 319eqtrd 2859 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) = 1)
321320neeq1d 3073 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → (((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) ≠ 0 ↔ 1 ≠ 0))
322268, 321mpbiri 261 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) ≠ 0)
323 df-ne 3015 . . . . . . . . . . . . . . . 16 (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ≠ 0 ↔ ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
324 oveq2 7158 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = (𝑁 − 1) → (1...𝑗) = (1...(𝑁 − 1)))
325324imaeq2d 5917 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = (𝑁 − 1) → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...(𝑁 − 1))))
326325xpeq1d 5572 . . . . . . . . . . . . . . . . . . 19 (𝑗 = (𝑁 − 1) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑁 − 1))) × {1}))
327 oveq1 7157 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = (𝑁 − 1) → (𝑗 + 1) = ((𝑁 − 1) + 1))
328327oveq1d 7165 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = (𝑁 − 1) → ((𝑗 + 1)...𝑁) = (((𝑁 − 1) + 1)...𝑁))
329328imaeq2d 5917 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = (𝑁 − 1) → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ (((𝑁 − 1) + 1)...𝑁)))
330329xpeq1d 5572 . . . . . . . . . . . . . . . . . . 19 (𝑗 = (𝑁 − 1) → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))
331326, 330uneq12d 4127 . . . . . . . . . . . . . . . . . 18 (𝑗 = (𝑁 − 1) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0})))
332331fveq1d 6664 . . . . . . . . . . . . . . . . 17 (𝑗 = (𝑁 − 1) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁))
333332neeq1d 3073 . . . . . . . . . . . . . . . 16 (𝑗 = (𝑁 − 1) → (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ≠ 0 ↔ ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) ≠ 0))
334323, 333bitr3id 288 . . . . . . . . . . . . . . 15 (𝑗 = (𝑁 − 1) → (¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0 ↔ ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) ≠ 0))
335334rspcev 3610 . . . . . . . . . . . . . 14 (((𝑁 − 1) ∈ (0...(𝑁 − 1)) ∧ ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) ≠ 0) → ∃𝑗 ∈ (0...(𝑁 − 1)) ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
336267, 322, 335syl2anc 587 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → ∃𝑗 ∈ (0...(𝑁 − 1)) ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
337336ex 416 . . . . . . . . . . . 12 (𝜑 → ((𝑈𝑁) ≠ 𝑁 → ∃𝑗 ∈ (0...(𝑁 − 1)) ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))
338 rexnal 3233 . . . . . . . . . . . 12 (∃𝑗 ∈ (0...(𝑁 − 1)) ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0 ↔ ¬ ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
339337, 338syl6ib 254 . . . . . . . . . . 11 (𝜑 → ((𝑈𝑁) ≠ 𝑁 → ¬ ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))
340339necon4ad 3033 . . . . . . . . . 10 (𝜑 → (∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0 → (𝑈𝑁) = 𝑁))
341266, 340impbid 215 . . . . . . . . 9 (𝜑 → ((𝑈𝑁) = 𝑁 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))
342224, 341anbi12d 633 . . . . . . . 8 (𝜑 → (((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁) ↔ (∀𝑗 ∈ (0...(𝑁 − 1))(𝑇𝑁) = 0 ∧ ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
343 r19.26 3165 . . . . . . . 8 (∀𝑗 ∈ (0...(𝑁 − 1))((𝑇𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0) ↔ (∀𝑗 ∈ (0...(𝑁 − 1))(𝑇𝑁) = 0 ∧ ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))
344342, 343syl6bbr 292 . . . . . . 7 (𝜑 → (((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁) ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((𝑇𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
345344adantr 484 . . . . . 6 ((𝜑𝑉 = 𝑁) → (((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁) ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((𝑇𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
346191, 221, 3453bitr4d 314 . . . . 5 ((𝜑𝑉 = 𝑁) → (∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁)))
347346pm5.32da 582 . . . 4 (𝜑 → ((𝑉 = 𝑁 ∧ ∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0) ↔ (𝑉 = 𝑁 ∧ ((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁))))
348110, 347bitrd 282 . . 3 (𝜑 → (∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ (𝑉 = 𝑁 ∧ ((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁))))
349348notbid 321 . 2 (𝜑 → (¬ ∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ¬ (𝑉 = 𝑁 ∧ ((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁))))
35012, 349syl5bb 286 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 209   ∧ wa 399   ∨ wo 844   = wceq 1538   ∈ wcel 2115   ≠ wne 3014  ∀wral 3133  ∃wrex 3134  Vcvv 3481  ⦋csb 3867   ∖ cdif 3917   ∪ cun 3918   ∩ cin 3919   ⊆ wss 3920  ∅c0 4277  ifcif 4451  {csn 4551   class class class wbr 5053   ↦ cmpt 5133   × cxp 5541  ◡ccnv 5542  ran crn 5544   “ cima 5546  Fun wfun 6338   Fn wfn 6339  ⟶wf 6340  –onto→wfo 6342  –1-1-onto→wf1o 6343  ‘cfv 6344  (class class class)co 7150   ∘f cof 7402  ℂcc 10534  ℝcr 10535  0cc0 10536  1c1 10537   + caddc 10539   < clt 10674   ≤ cle 10675   − cmin 10869  ℕcn 11637  ℕ0cn0 11897  ℤcz 11981  ℤ≥cuz 12243  ...cfz 12897  ..^cfzo 13040 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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5177  ax-sep 5190  ax-nul 5197  ax-pow 5254  ax-pr 5318  ax-un 7456  ax-cnex 10592  ax-resscn 10593  ax-1cn 10594  ax-icn 10595  ax-addcl 10596  ax-addrcl 10597  ax-mulcl 10598  ax-mulrcl 10599  ax-mulcom 10600  ax-addass 10601  ax-mulass 10602  ax-distr 10603  ax-i2m1 10604  ax-1ne0 10605  ax-1rid 10606  ax-rnegex 10607  ax-rrecex 10608  ax-cnre 10609  ax-pre-lttri 10610  ax-pre-lttrn 10611  ax-pre-ltadd 10612  ax-pre-mulgt0 10613 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rab 3142  df-v 3483  df-sbc 3760  df-csb 3868  df-dif 3923  df-un 3925  df-in 3927  df-ss 3937  df-pss 3939  df-nul 4278  df-if 4452  df-pw 4525  df-sn 4552  df-pr 4554  df-tp 4556  df-op 4558  df-uni 4826  df-iun 4908  df-br 5054  df-opab 5116  df-mpt 5134  df-tr 5160  df-id 5448  df-eprel 5453  df-po 5462  df-so 5463  df-fr 5502  df-we 5504  df-xp 5549  df-rel 5550  df-cnv 5551  df-co 5552  df-dm 5553  df-rn 5554  df-res 5555  df-ima 5556  df-pred 6136  df-ord 6182  df-on 6183  df-lim 6184  df-suc 6185  df-iota 6303  df-fun 6346  df-fn 6347  df-f 6348  df-f1 6349  df-fo 6350  df-f1o 6351  df-fv 6352  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-of 7404  df-om 7576  df-1st 7685  df-2nd 7686  df-wrecs 7944  df-recs 8005  df-rdg 8043  df-er 8286  df-en 8507  df-dom 8508  df-sdom 8509  df-pnf 10676  df-mnf 10677  df-xr 10678  df-ltxr 10679  df-le 10680  df-sub 10871  df-neg 10872  df-nn 11638  df-n0 11898  df-z 11982  df-uz 12244  df-fz 12898  df-fzo 13041 This theorem is referenced by:  poimirlem24  35027
 Copyright terms: Public domain W3C validator