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

Theorem poimirlem23 33103
 Description: Lemma for poimir 33113, 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)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝𝑁) ≠ 0 ↔ ¬ (𝑉 = 𝑁 ∧ ((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁))))
Distinct variable groups:   𝑗,𝑝,𝑦,𝜑   𝑗,𝑁,𝑦   𝑇,𝑗,𝑦   𝑈,𝑗,𝑦   𝑗,𝑉,𝑦   𝜑,𝑝   𝑗,𝐾,𝑝   𝑁,𝑝   𝑇,𝑝   𝑈,𝑝   𝑦,𝐾   𝑉,𝑝

Proof of Theorem poimirlem23
StepHypRef Expression
1 ovex 6643 . . . . . 6 (𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
21csbex 4763 . . . . 5 if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
32rgenw 2920 . . . 4 𝑦 ∈ (0...(𝑁 − 1))if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
4 eqid 2621 . . . . 5 (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
5 fveq1 6157 . . . . . . 7 (𝑝 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) → (𝑝𝑁) = (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁))
65neeq1d 2849 . . . . . 6 (𝑝 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) → ((𝑝𝑁) ≠ 0 ↔ (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0))
7 df-ne 2791 . . . . . 6 ((if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0 ↔ ¬ (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
86, 7syl6bb 276 . . . . 5 (𝑝 = if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) → ((𝑝𝑁) ≠ 0 ↔ ¬ (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
94, 8rexrnmpt 6335 . . . 4 (∀𝑦 ∈ (0...(𝑁 − 1))if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V → (∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝𝑁) ≠ 0 ↔ ∃𝑦 ∈ (0...(𝑁 − 1)) ¬ (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
103, 9ax-mp 5 . . 3 (∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝𝑁) ≠ 0 ↔ ∃𝑦 ∈ (0...(𝑁 − 1)) ¬ (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
11 rexnal 2991 . . 3 (∃𝑦 ∈ (0...(𝑁 − 1)) ¬ (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ¬ ∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
1210, 11bitri 264 . 2 (∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝𝑁) ≠ 0 ↔ ¬ ∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
13 poimir.0 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℕ)
1413nnzd 11441 . . . . . . . . . 10 (𝜑𝑁 ∈ ℤ)
15 poimirlem23.3 . . . . . . . . . . 11 (𝜑𝑉 ∈ (0...𝑁))
16 elfzelz 12300 . . . . . . . . . . 11 (𝑉 ∈ (0...𝑁) → 𝑉 ∈ ℤ)
1715, 16syl 17 . . . . . . . . . 10 (𝜑𝑉 ∈ ℤ)
18 zlem1lt 11389 . . . . . . . . . 10 ((𝑁 ∈ ℤ ∧ 𝑉 ∈ ℤ) → (𝑁𝑉 ↔ (𝑁 − 1) < 𝑉))
1914, 17, 18syl2anc 692 . . . . . . . . 9 (𝜑 → (𝑁𝑉 ↔ (𝑁 − 1) < 𝑉))
20 elfzle2 12303 . . . . . . . . . . 11 (𝑉 ∈ (0...𝑁) → 𝑉𝑁)
2115, 20syl 17 . . . . . . . . . 10 (𝜑𝑉𝑁)
2217zred 11442 . . . . . . . . . . . 12 (𝜑𝑉 ∈ ℝ)
2313nnred 10995 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℝ)
2422, 23letri3d 10139 . . . . . . . . . . 11 (𝜑 → (𝑉 = 𝑁 ↔ (𝑉𝑁𝑁𝑉)))
2524biimprd 238 . . . . . . . . . 10 (𝜑 → ((𝑉𝑁𝑁𝑉) → 𝑉 = 𝑁))
2621, 25mpand 710 . . . . . . . . 9 (𝜑 → (𝑁𝑉𝑉 = 𝑁))
2719, 26sylbird 250 . . . . . . . 8 (𝜑 → ((𝑁 − 1) < 𝑉𝑉 = 𝑁))
2827necon3ad 2803 . . . . . . 7 (𝜑 → (𝑉𝑁 → ¬ (𝑁 − 1) < 𝑉))
29 nnm1nn0 11294 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
3013, 29syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑁 − 1) ∈ ℕ0)
31 nn0fz0 12394 . . . . . . . . . . . 12 ((𝑁 − 1) ∈ ℕ0 ↔ (𝑁 − 1) ∈ (0...(𝑁 − 1)))
3230, 31sylib 208 . . . . . . . . . . 11 (𝜑 → (𝑁 − 1) ∈ (0...(𝑁 − 1)))
3332adantr 481 . . . . . . . . . 10 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → (𝑁 − 1) ∈ (0...(𝑁 − 1)))
34 iffalse 4073 . . . . . . . . . . . . . . . 16 (¬ (𝑁 − 1) < 𝑉 → if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) = ((𝑁 − 1) + 1))
3513nncnd 10996 . . . . . . . . . . . . . . . . 17 (𝜑𝑁 ∈ ℂ)
36 npcan1 10415 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
3735, 36syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
3834, 37sylan9eqr 2677 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) = 𝑁)
3938csbeq1d 3526 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = 𝑁 / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
40 oveq2 6623 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑁 → (1...𝑗) = (1...𝑁))
4140imaeq2d 5435 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑁 → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...𝑁)))
4241xpeq1d 5108 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑁 → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...𝑁)) × {1}))
43 oveq1 6622 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑁 → (𝑗 + 1) = (𝑁 + 1))
4443oveq1d 6630 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑁 → ((𝑗 + 1)...𝑁) = ((𝑁 + 1)...𝑁))
4544imaeq2d 5435 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑁 → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ ((𝑁 + 1)...𝑁)))
4645xpeq1d 5108 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑁 → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0}))
4742, 46uneq12d 3752 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑁 → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...𝑁)) × {1}) ∪ ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0})))
48 poimirlem23.2 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑈:(1...𝑁)–1-1-onto→(1...𝑁))
49 f1ofo 6111 . . . . . . . . . . . . . . . . . . . . . 22 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)–onto→(1...𝑁))
50 foima 6087 . . . . . . . . . . . . . . . . . . . . . 22 (𝑈:(1...𝑁)–onto→(1...𝑁) → (𝑈 “ (1...𝑁)) = (1...𝑁))
5148, 49, 503syl 18 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑈 “ (1...𝑁)) = (1...𝑁))
5251xpeq1d 5108 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑈 “ (1...𝑁)) × {1}) = ((1...𝑁) × {1}))
5323ltp1d 10914 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑁 < (𝑁 + 1))
5414peano2zd 11445 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝑁 + 1) ∈ ℤ)
55 fzn 12315 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑁 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 < (𝑁 + 1) ↔ ((𝑁 + 1)...𝑁) = ∅))
5654, 14, 55syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑁 < (𝑁 + 1) ↔ ((𝑁 + 1)...𝑁) = ∅))
5753, 56mpbid 222 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑁 + 1)...𝑁) = ∅)
5857imaeq2d 5435 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑈 “ ((𝑁 + 1)...𝑁)) = (𝑈 “ ∅))
5958xpeq1d 5108 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0}) = ((𝑈 “ ∅) × {0}))
60 ima0 5450 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑈 “ ∅) = ∅
6160xpeq1i 5105 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑈 “ ∅) × {0}) = (∅ × {0})
62 0xp 5170 . . . . . . . . . . . . . . . . . . . . . 22 (∅ × {0}) = ∅
6361, 62eqtri 2643 . . . . . . . . . . . . . . . . . . . . 21 ((𝑈 “ ∅) × {0}) = ∅
6459, 63syl6eq 2671 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0}) = ∅)
6552, 64uneq12d 3752 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((𝑈 “ (1...𝑁)) × {1}) ∪ ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0})) = (((1...𝑁) × {1}) ∪ ∅))
66 un0 3945 . . . . . . . . . . . . . . . . . . 19 (((1...𝑁) × {1}) ∪ ∅) = ((1...𝑁) × {1})
6765, 66syl6eq 2671 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((𝑈 “ (1...𝑁)) × {1}) ∪ ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0})) = ((1...𝑁) × {1}))
6847, 67sylan9eqr 2677 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 = 𝑁) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = ((1...𝑁) × {1}))
6968oveq2d 6631 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 = 𝑁) → (𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇𝑓 + ((1...𝑁) × {1})))
7013, 69csbied 3546 . . . . . . . . . . . . . . 15 (𝜑𝑁 / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇𝑓 + ((1...𝑁) × {1})))
7170adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → 𝑁 / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇𝑓 + ((1...𝑁) × {1})))
7239, 71eqtrd 2655 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇𝑓 + ((1...𝑁) × {1})))
7372fveq1d 6160 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → (if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = ((𝑇𝑓 + ((1...𝑁) × {1}))‘𝑁))
74 elfzonn0 12469 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0..^𝐾) → 𝑗 ∈ ℕ0)
75 nn0p1nn 11292 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℕ0 → (𝑗 + 1) ∈ ℕ)
7674, 75syl 17 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0..^𝐾) → (𝑗 + 1) ∈ ℕ)
77 elsni 4172 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ {1} → 𝑦 = 1)
7877oveq2d 6631 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ {1} → (𝑗 + 𝑦) = (𝑗 + 1))
7978eleq1d 2683 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ {1} → ((𝑗 + 𝑦) ∈ ℕ ↔ (𝑗 + 1) ∈ ℕ))
8076, 79syl5ibrcom 237 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0..^𝐾) → (𝑦 ∈ {1} → (𝑗 + 𝑦) ∈ ℕ))
8180imp 445 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (0..^𝐾) ∧ 𝑦 ∈ {1}) → (𝑗 + 𝑦) ∈ ℕ)
8281adantl 482 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗 ∈ (0..^𝐾) ∧ 𝑦 ∈ {1})) → (𝑗 + 𝑦) ∈ ℕ)
83 poimirlem23.1 . . . . . . . . . . . . . . 15 (𝜑𝑇:(1...𝑁)⟶(0..^𝐾))
84 1ex 9995 . . . . . . . . . . . . . . . . 17 1 ∈ V
8584fconst 6058 . . . . . . . . . . . . . . . 16 ((1...𝑁) × {1}):(1...𝑁)⟶{1}
8685a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → ((1...𝑁) × {1}):(1...𝑁)⟶{1})
87 ovexd 6645 . . . . . . . . . . . . . . 15 (𝜑 → (1...𝑁) ∈ V)
88 inidm 3806 . . . . . . . . . . . . . . 15 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
8982, 83, 86, 87, 87, 88off 6877 . . . . . . . . . . . . . 14 (𝜑 → (𝑇𝑓 + ((1...𝑁) × {1})):(1...𝑁)⟶ℕ)
90 elfz1end 12329 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℕ ↔ 𝑁 ∈ (1...𝑁))
9113, 90sylib 208 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ (1...𝑁))
9289, 91ffvelrnd 6326 . . . . . . . . . . . . 13 (𝜑 → ((𝑇𝑓 + ((1...𝑁) × {1}))‘𝑁) ∈ ℕ)
9392adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → ((𝑇𝑓 + ((1...𝑁) × {1}))‘𝑁) ∈ ℕ)
9473, 93eqeltrd 2698 . . . . . . . . . . 11 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → (if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ∈ ℕ)
9594nnne0d 11025 . . . . . . . . . 10 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → (if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0)
96 breq1 4626 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑁 − 1) → (𝑦 < 𝑉 ↔ (𝑁 − 1) < 𝑉))
97 id 22 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑁 − 1) → 𝑦 = (𝑁 − 1))
98 oveq1 6622 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑁 − 1) → (𝑦 + 1) = ((𝑁 − 1) + 1))
9996, 97, 98ifbieq12d 4091 . . . . . . . . . . . . . . 15 (𝑦 = (𝑁 − 1) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) = if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)))
10099csbeq1d 3526 . . . . . . . . . . . . . 14 (𝑦 = (𝑁 − 1) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
101100fveq1d 6160 . . . . . . . . . . . . 13 (𝑦 = (𝑁 − 1) → (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = (if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁))
102101neeq1d 2849 . . . . . . . . . . . 12 (𝑦 = (𝑁 − 1) → ((if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0 ↔ (if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0))
1037, 102syl5bbr 274 . . . . . . . . . . 11 (𝑦 = (𝑁 − 1) → (¬ (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ (if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0))
104103rspcev 3299 . . . . . . . . . 10 (((𝑁 − 1) ∈ (0...(𝑁 − 1)) ∧ (if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0) → ∃𝑦 ∈ (0...(𝑁 − 1)) ¬ (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
10533, 95, 104syl2anc 692 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → ∃𝑦 ∈ (0...(𝑁 − 1)) ¬ (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
106105, 11sylib 208 . . . . . . . 8 ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → ¬ ∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
107106ex 450 . . . . . . 7 (𝜑 → (¬ (𝑁 − 1) < 𝑉 → ¬ ∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
10828, 107syld 47 . . . . . 6 (𝜑 → (𝑉𝑁 → ¬ ∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
109108necon4ad 2809 . . . . 5 (𝜑 → (∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 → 𝑉 = 𝑁))
110109pm4.71rd 666 . . . 4 (𝜑 → (∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ (𝑉 = 𝑁 ∧ ∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)))
11130nn0zd 11440 . . . . . . . . . . . . 13 (𝜑 → (𝑁 − 1) ∈ ℤ)
112 uzid 11662 . . . . . . . . . . . . 13 ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)))
113 peano2uz 11701 . . . . . . . . . . . . 13 ((𝑁 − 1) ∈ (ℤ‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
114111, 112, 1133syl 18 . . . . . . . . . . . 12 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑁 − 1)))
11537, 114eqeltrrd 2699 . . . . . . . . . . 11 (𝜑𝑁 ∈ (ℤ‘(𝑁 − 1)))
116 fzss2 12339 . . . . . . . . . . 11 (𝑁 ∈ (ℤ‘(𝑁 − 1)) → (0...(𝑁 − 1)) ⊆ (0...𝑁))
117115, 116syl 17 . . . . . . . . . 10 (𝜑 → (0...(𝑁 − 1)) ⊆ (0...𝑁))
118117sselda 3588 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → 𝑗 ∈ (0...𝑁))
11991adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑁 ∈ (1...𝑁))
120 ffn 6012 . . . . . . . . . . . . . . 15 (𝑇:(1...𝑁)⟶(0..^𝐾) → 𝑇 Fn (1...𝑁))
12183, 120syl 17 . . . . . . . . . . . . . 14 (𝜑𝑇 Fn (1...𝑁))
122121adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑇 Fn (1...𝑁))
12384fconst 6058 . . . . . . . . . . . . . . . . 17 ((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1}
124 c0ex 9994 . . . . . . . . . . . . . . . . . 18 0 ∈ V
125124fconst 6058 . . . . . . . . . . . . . . . . 17 ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0}
126123, 125pm3.2i 471 . . . . . . . . . . . . . . . 16 (((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1} ∧ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0})
127 dff1o3 6110 . . . . . . . . . . . . . . . . . . 19 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (𝑈:(1...𝑁)–onto→(1...𝑁) ∧ Fun 𝑈))
128127simprbi 480 . . . . . . . . . . . . . . . . . 18 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → Fun 𝑈)
129 imain 5942 . . . . . . . . . . . . . . . . . 18 (Fun 𝑈 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))))
13048, 128, 1293syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))))
131 elfzelz 12300 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℤ)
132131zred 11442 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℝ)
133132ltp1d 10914 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...𝑁) → 𝑗 < (𝑗 + 1))
134 fzdisj 12326 . . . . . . . . . . . . . . . . . . . 20 (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
135133, 134syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑁) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
136135imaeq2d 5435 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑁) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (𝑈 “ ∅))
137136, 60syl6eq 2671 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑁) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ∅)
138130, 137sylan9req 2676 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅)
139 fun 6033 . . . . . . . . . . . . . . . 16 (((((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1} ∧ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0}) ∧ ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}))
140126, 138, 139sylancr 694 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...𝑁)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}))
141 elfznn0 12390 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℕ0)
142141, 75syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ ℕ)
143 nnuz 11683 . . . . . . . . . . . . . . . . . . . . 21 ℕ = (ℤ‘1)
144142, 143syl6eleq 2708 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ (ℤ‘1))
145 elfzuz3 12297 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...𝑁) → 𝑁 ∈ (ℤ𝑗))
146 fzsplit2 12324 . . . . . . . . . . . . . . . . . . . 20 (((𝑗 + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ𝑗)) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
147144, 145, 146syl2anc 692 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑁) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
148147imaeq2d 5435 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑁) → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))))
149 imaundi 5514 . . . . . . . . . . . . . . . . . 18 (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))
150148, 149syl6req 2672 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...𝑁) → ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁))) = (𝑈 “ (1...𝑁)))
151150, 51sylan9eqr 2677 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁))) = (1...𝑁))
152151feq2d 5998 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...𝑁)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}) ↔ (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0})))
153140, 152mpbid 222 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑁)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0}))
154 ffn 6012 . . . . . . . . . . . . . 14 ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0}) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) Fn (1...𝑁))
155153, 154syl 17 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑁)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) Fn (1...𝑁))
156 ovexd 6645 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑁)) → (1...𝑁) ∈ V)
157 eqidd 2622 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑁 ∈ (1...𝑁)) → (𝑇𝑁) = (𝑇𝑁))
158 eqidd 2622 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑁 ∈ (1...𝑁)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))
159122, 155, 156, 156, 88, 157, 158ofval 6871 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑁 ∈ (1...𝑁)) → ((𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = ((𝑇𝑁) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)))
160119, 159mpdan 701 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = ((𝑇𝑁) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)))
161160eqeq1d 2623 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑁)) → (((𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ((𝑇𝑁) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)) = 0))
16283, 91ffvelrnd 6326 . . . . . . . . . . . . . 14 (𝜑 → (𝑇𝑁) ∈ (0..^𝐾))
163 elfzonn0 12469 . . . . . . . . . . . . . 14 ((𝑇𝑁) ∈ (0..^𝐾) → (𝑇𝑁) ∈ ℕ0)
164162, 163syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑇𝑁) ∈ ℕ0)
165164nn0red 11312 . . . . . . . . . . . 12 (𝜑 → (𝑇𝑁) ∈ ℝ)
166165adantr 481 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑇𝑁) ∈ ℝ)
167164nn0ge0d 11314 . . . . . . . . . . . 12 (𝜑 → 0 ≤ (𝑇𝑁))
168167adantr 481 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑁)) → 0 ≤ (𝑇𝑁))
169 1re 9999 . . . . . . . . . . . . . 14 1 ∈ ℝ
170 snssi 4315 . . . . . . . . . . . . . 14 (1 ∈ ℝ → {1} ⊆ ℝ)
171169, 170ax-mp 5 . . . . . . . . . . . . 13 {1} ⊆ ℝ
172 0re 10000 . . . . . . . . . . . . . 14 0 ∈ ℝ
173 snssi 4315 . . . . . . . . . . . . . 14 (0 ∈ ℝ → {0} ⊆ ℝ)
174172, 173ax-mp 5 . . . . . . . . . . . . 13 {0} ⊆ ℝ
175171, 174unssi 3772 . . . . . . . . . . . 12 ({1} ∪ {0}) ⊆ ℝ
176153, 119ffvelrnd 6326 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑁)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ ({1} ∪ {0}))
177175, 176sseldi 3586 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑁)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ ℝ)
178 elun 3737 . . . . . . . . . . . . 13 (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ ({1} ∪ {0}) ↔ (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {1} ∨ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {0}))
179 0le1 10511 . . . . . . . . . . . . . . 15 0 ≤ 1
180 elsni 4172 . . . . . . . . . . . . . . 15 (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {1} → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 1)
181179, 180syl5breqr 4661 . . . . . . . . . . . . . 14 (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {1} → 0 ≤ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))
182 0le0 11070 . . . . . . . . . . . . . . 15 0 ≤ 0
183 elsni 4172 . . . . . . . . . . . . . . 15 (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {0} → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
184182, 183syl5breqr 4661 . . . . . . . . . . . . . 14 (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {0} → 0 ≤ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))
185181, 184jaoi 394 . . . . . . . . . . . . 13 ((((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {1} ∨ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {0}) → 0 ≤ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))
186178, 185sylbi 207 . . . . . . . . . . . 12 (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ ({1} ∪ {0}) → 0 ≤ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))
187176, 186syl 17 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑁)) → 0 ≤ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))
188 add20 10500 . . . . . . . . . . 11 ((((𝑇𝑁) ∈ ℝ ∧ 0 ≤ (𝑇𝑁)) ∧ (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ ℝ ∧ 0 ≤ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))) → (((𝑇𝑁) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)) = 0 ↔ ((𝑇𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
189166, 168, 177, 187, 188syl22anc 1324 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑁)) → (((𝑇𝑁) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)) = 0 ↔ ((𝑇𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
190161, 189bitrd 268 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑁)) → (((𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ((𝑇𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
191118, 190syldan 487 . . . . . . . 8 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → (((𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ((𝑇𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
192191ralbidva 2981 . . . . . . 7 (𝜑 → (∀𝑗 ∈ (0...(𝑁 − 1))((𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((𝑇𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
193192adantr 481 . . . . . 6 ((𝜑𝑉 = 𝑁) → (∀𝑗 ∈ (0...(𝑁 − 1))((𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((𝑇𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
194 breq2 4627 . . . . . . . . . . . . . 14 (𝑉 = 𝑁 → (𝑦 < 𝑉𝑦 < 𝑁))
195194ifbid 4086 . . . . . . . . . . . . 13 (𝑉 = 𝑁 → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) = if(𝑦 < 𝑁, 𝑦, (𝑦 + 1)))
196 elfzelz 12300 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℤ)
197196zred 11442 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℝ)
198197adantl 482 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ∈ ℝ)
19930nn0red 11312 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑁 − 1) ∈ ℝ)
200199adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ)
20123adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℝ)
202 elfzle2 12303 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ≤ (𝑁 − 1))
203202adantl 482 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ≤ (𝑁 − 1))
20423ltm1d 10916 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑁 − 1) < 𝑁)
205204adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → (𝑁 − 1) < 𝑁)
206198, 200, 201, 203, 205lelttrd 10155 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 < 𝑁)
207206iftrued 4072 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < 𝑁, 𝑦, (𝑦 + 1)) = 𝑦)
208195, 207sylan9eqr 2677 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑉 = 𝑁) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) = 𝑦)
209208an32s 845 . . . . . . . . . . 11 (((𝜑𝑉 = 𝑁) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) = 𝑦)
210209csbeq1d 3526 . . . . . . . . . 10 (((𝜑𝑉 = 𝑁) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = 𝑦 / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
211210fveq1d 6160 . . . . . . . . 9 (((𝜑𝑉 = 𝑁) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = (𝑦 / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁))
212211eqeq1d 2623 . . . . . . . 8 (((𝜑𝑉 = 𝑁) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ (𝑦 / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
213212ralbidva 2981 . . . . . . 7 ((𝜑𝑉 = 𝑁) → (∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ∀𝑦 ∈ (0...(𝑁 − 1))(𝑦 / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
214 nfv 1840 . . . . . . . 8 𝑦((𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0
215 nfcsb1v 3535 . . . . . . . . . 10 𝑗𝑦 / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))
216 nfcv 2761 . . . . . . . . . 10 𝑗𝑁
217215, 216nffv 6165 . . . . . . . . 9 𝑗(𝑦 / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁)
218217nfeq1 2774 . . . . . . . 8 𝑗(𝑦 / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0
219 csbeq1a 3528 . . . . . . . . . 10 (𝑗 = 𝑦 → (𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = 𝑦 / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
220219fveq1d 6160 . . . . . . . . 9 (𝑗 = 𝑦 → ((𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = (𝑦 / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁))
221220eqeq1d 2623 . . . . . . . 8 (𝑗 = 𝑦 → (((𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ (𝑦 / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
222214, 218, 221cbvral 3159 . . . . . . 7 (∀𝑗 ∈ (0...(𝑁 − 1))((𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ∀𝑦 ∈ (0...(𝑁 − 1))(𝑦 / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
223213, 222syl6bbr 278 . . . . . 6 ((𝜑𝑉 = 𝑁) → (∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
224 ne0i 3903 . . . . . . . . . 10 ((𝑁 − 1) ∈ (0...(𝑁 − 1)) → (0...(𝑁 − 1)) ≠ ∅)
225 r19.3rzv 4042 . . . . . . . . . 10 ((0...(𝑁 − 1)) ≠ ∅ → ((𝑇𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))(𝑇𝑁) = 0))
22632, 224, 2253syl 18 . . . . . . . . 9 (𝜑 → ((𝑇𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))(𝑇𝑁) = 0))
227 elfzelz 12300 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 ∈ ℤ)
228227zred 11442 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 ∈ ℝ)
229228ltp1d 10914 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 < (𝑗 + 1))
230229, 134syl 17 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...(𝑁 − 1)) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
231230imaeq2d 5435 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (0...(𝑁 − 1)) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (𝑈 “ ∅))
232231, 60syl6eq 2671 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...(𝑁 − 1)) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ∅)
233130, 232sylan9req 2676 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅)
234233adantlr 750 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑈𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅)
235 simplr 791 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑈𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑈𝑁) = 𝑁)
236 f1ofn 6105 . . . . . . . . . . . . . . . . . . 19 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈 Fn (1...𝑁))
23748, 236syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝑈 Fn (1...𝑁))
238237adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → 𝑈 Fn (1...𝑁))
239 elfznn0 12390 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 ∈ ℕ0)
240239, 75syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...(𝑁 − 1)) → (𝑗 + 1) ∈ ℕ)
241240, 143syl6eleq 2708 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...(𝑁 − 1)) → (𝑗 + 1) ∈ (ℤ‘1))
242 fzss1 12338 . . . . . . . . . . . . . . . . . . 19 ((𝑗 + 1) ∈ (ℤ‘1) → ((𝑗 + 1)...𝑁) ⊆ (1...𝑁))
243241, 242syl 17 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...(𝑁 − 1)) → ((𝑗 + 1)...𝑁) ⊆ (1...𝑁))
244243adantl 482 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → ((𝑗 + 1)...𝑁) ⊆ (1...𝑁))
24537adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) = 𝑁)
246 elfzuz3 12297 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (0...(𝑁 − 1)) → (𝑁 − 1) ∈ (ℤ𝑗))
247 eluzp1p1 11673 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 − 1) ∈ (ℤ𝑗) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑗 + 1)))
248246, 247syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑗 + 1)))
249248adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) ∈ (ℤ‘(𝑗 + 1)))
250245, 249eqeltrrd 2699 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ‘(𝑗 + 1)))
251 eluzfz2 12307 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ (ℤ‘(𝑗 + 1)) → 𝑁 ∈ ((𝑗 + 1)...𝑁))
252250, 251syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ((𝑗 + 1)...𝑁))
253 fnfvima 6461 . . . . . . . . . . . . . . . . 17 ((𝑈 Fn (1...𝑁) ∧ ((𝑗 + 1)...𝑁) ⊆ (1...𝑁) ∧ 𝑁 ∈ ((𝑗 + 1)...𝑁)) → (𝑈𝑁) ∈ (𝑈 “ ((𝑗 + 1)...𝑁)))
254238, 244, 252, 253syl3anc 1323 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...(𝑁 − 1))) → (𝑈𝑁) ∈ (𝑈 “ ((𝑗 + 1)...𝑁)))
255254adantlr 750 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑈𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑈𝑁) ∈ (𝑈 “ ((𝑗 + 1)...𝑁)))
256235, 255eqeltrrd 2699 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑈𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (𝑈 “ ((𝑗 + 1)...𝑁)))
257 fnconstg 6060 . . . . . . . . . . . . . . . 16 (1 ∈ V → ((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗)))
25884, 257ax-mp 5 . . . . . . . . . . . . . . 15 ((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗))
259 fnconstg 6060 . . . . . . . . . . . . . . . 16 (0 ∈ V → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑁)))
260124, 259ax-mp 5 . . . . . . . . . . . . . . 15 ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑁))
261 fvun2 6237 . . . . . . . . . . . . . . 15 ((((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗)) ∧ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑁)) ∧ (((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅ ∧ 𝑁 ∈ (𝑈 “ ((𝑗 + 1)...𝑁)))) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁))
262258, 260, 261mp3an12 1411 . . . . . . . . . . . . . 14 ((((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅ ∧ 𝑁 ∈ (𝑈 “ ((𝑗 + 1)...𝑁))) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁))
263234, 256, 262syl2anc 692 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑈𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁))
264124fvconst2 6434 . . . . . . . . . . . . . 14 (𝑁 ∈ (𝑈 “ ((𝑗 + 1)...𝑁)) → (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁) = 0)
265256, 264syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑈𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁) = 0)
266263, 265eqtrd 2655 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑈𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
267266ralrimiva 2962 . . . . . . . . . . 11 ((𝜑 ∧ (𝑈𝑁) = 𝑁) → ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
268267ex 450 . . . . . . . . . 10 (𝜑 → ((𝑈𝑁) = 𝑁 → ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))
26932adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → (𝑁 − 1) ∈ (0...(𝑁 − 1)))
270 ax-1ne0 9965 . . . . . . . . . . . . . . 15 1 ≠ 0
271 imain 5942 . . . . . . . . . . . . . . . . . . . . 21 (Fun 𝑈 → (𝑈 “ ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑁 − 1))) ∩ (𝑈 “ (((𝑁 − 1) + 1)...𝑁))))
27248, 128, 2713syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑈 “ ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑁 − 1))) ∩ (𝑈 “ (((𝑁 − 1) + 1)...𝑁))))
273204, 37breqtrrd 4651 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑁 − 1) < ((𝑁 − 1) + 1))
274 fzdisj 12326 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 − 1) < ((𝑁 − 1) + 1) → ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁)) = ∅)
275273, 274syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁)) = ∅)
276275imaeq2d 5435 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑈 “ ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁))) = (𝑈 “ ∅))
277276, 60syl6eq 2671 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑈 “ ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁))) = ∅)
278272, 277eqtr3d 2657 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑈 “ (1...(𝑁 − 1))) ∩ (𝑈 “ (((𝑁 − 1) + 1)...𝑁))) = ∅)
279278adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → ((𝑈 “ (1...(𝑁 − 1))) ∩ (𝑈 “ (((𝑁 − 1) + 1)...𝑁))) = ∅)
28091adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → 𝑁 ∈ (1...𝑁))
281 elimasni 5461 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ (𝑈 “ {𝑁}) → 𝑁𝑈𝑁)
282 fnbrfvb 6203 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑈 Fn (1...𝑁) ∧ 𝑁 ∈ (1...𝑁)) → ((𝑈𝑁) = 𝑁𝑁𝑈𝑁))
283237, 91, 282syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑈𝑁) = 𝑁𝑁𝑈𝑁))
284281, 283syl5ibr 236 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑁 ∈ (𝑈 “ {𝑁}) → (𝑈𝑁) = 𝑁))
285284necon3ad 2803 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑈𝑁) ≠ 𝑁 → ¬ 𝑁 ∈ (𝑈 “ {𝑁})))
286285imp 445 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → ¬ 𝑁 ∈ (𝑈 “ {𝑁}))
287280, 286eldifd 3571 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → 𝑁 ∈ ((1...𝑁) ∖ (𝑈 “ {𝑁})))
288 imadif 5941 . . . . . . . . . . . . . . . . . . . . . 22 (Fun 𝑈 → (𝑈 “ ((1...𝑁) ∖ {𝑁})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑁})))
28948, 128, 2883syl 18 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑈 “ ((1...𝑁) ∖ {𝑁})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑁})))
290 difun2 4026 . . . . . . . . . . . . . . . . . . . . . . 23 (((1...(𝑁 − 1)) ∪ {𝑁}) ∖ {𝑁}) = ((1...(𝑁 − 1)) ∖ {𝑁})
29113, 143syl6eleq 2708 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑁 ∈ (ℤ‘1))
292 fzm1 12377 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ (ℤ‘1) → (𝑗 ∈ (1...𝑁) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 = 𝑁)))
293291, 292syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝑗 ∈ (1...𝑁) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 = 𝑁)))
294 elun 3737 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ ((1...(𝑁 − 1)) ∪ {𝑁}) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 ∈ {𝑁}))
295 velsn 4171 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ {𝑁} ↔ 𝑗 = 𝑁)
296295orbi2i 541 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 ∈ {𝑁}) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 = 𝑁))
297294, 296bitri 264 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 ∈ ((1...(𝑁 − 1)) ∪ {𝑁}) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 = 𝑁))
298293, 297syl6rbbr 279 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝑗 ∈ ((1...(𝑁 − 1)) ∪ {𝑁}) ↔ 𝑗 ∈ (1...𝑁)))
299298eqrdv 2619 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((1...(𝑁 − 1)) ∪ {𝑁}) = (1...𝑁))
300299difeq1d 3711 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((1...(𝑁 − 1)) ∪ {𝑁}) ∖ {𝑁}) = ((1...𝑁) ∖ {𝑁}))
301199, 23ltnled 10144 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((𝑁 − 1) < 𝑁 ↔ ¬ 𝑁 ≤ (𝑁 − 1)))
302204, 301mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ¬ 𝑁 ≤ (𝑁 − 1))
303 elfzle2 12303 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ (1...(𝑁 − 1)) → 𝑁 ≤ (𝑁 − 1))
304302, 303nsyl 135 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ¬ 𝑁 ∈ (1...(𝑁 − 1)))
305 difsn 4304 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑁 ∈ (1...(𝑁 − 1)) → ((1...(𝑁 − 1)) ∖ {𝑁}) = (1...(𝑁 − 1)))
306304, 305syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((1...(𝑁 − 1)) ∖ {𝑁}) = (1...(𝑁 − 1)))
307290, 300, 3063eqtr3a 2679 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1)))
308307imaeq2d 5435 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑈 “ ((1...𝑁) ∖ {𝑁})) = (𝑈 “ (1...(𝑁 − 1))))
30951difeq1d 3711 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑁})) = ((1...𝑁) ∖ (𝑈 “ {𝑁})))
310289, 308, 3093eqtr3rd 2664 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((1...𝑁) ∖ (𝑈 “ {𝑁})) = (𝑈 “ (1...(𝑁 − 1))))
311310adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → ((1...𝑁) ∖ (𝑈 “ {𝑁})) = (𝑈 “ (1...(𝑁 − 1))))
312287, 311eleqtrd 2700 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → 𝑁 ∈ (𝑈 “ (1...(𝑁 − 1))))
313 fnconstg 6060 . . . . . . . . . . . . . . . . . . . 20 (1 ∈ V → ((𝑈 “ (1...(𝑁 − 1))) × {1}) Fn (𝑈 “ (1...(𝑁 − 1))))
31484, 313ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((𝑈 “ (1...(𝑁 − 1))) × {1}) Fn (𝑈 “ (1...(𝑁 − 1)))
315 fnconstg 6060 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ V → ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑁 − 1) + 1)...𝑁)))
316124, 315ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑁 − 1) + 1)...𝑁))
317 fvun1 6236 . . . . . . . . . . . . . . . . . . 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})‘𝑁))
318314, 316, 317mp3an12 1411 . . . . . . . . . . . . . . . . . 18 ((((𝑈 “ (1...(𝑁 − 1))) ∩ (𝑈 “ (((𝑁 − 1) + 1)...𝑁))) = ∅ ∧ 𝑁 ∈ (𝑈 “ (1...(𝑁 − 1)))) → ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ (1...(𝑁 − 1))) × {1})‘𝑁))
319279, 312, 318syl2anc 692 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ (1...(𝑁 − 1))) × {1})‘𝑁))
32084fvconst2 6434 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ (𝑈 “ (1...(𝑁 − 1))) → (((𝑈 “ (1...(𝑁 − 1))) × {1})‘𝑁) = 1)
321312, 320syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → (((𝑈 “ (1...(𝑁 − 1))) × {1})‘𝑁) = 1)
322319, 321eqtrd 2655 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) = 1)
323322neeq1d 2849 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → (((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) ≠ 0 ↔ 1 ≠ 0))
324270, 323mpbiri 248 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) ≠ 0)
325 df-ne 2791 . . . . . . . . . . . . . . . 16 (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ≠ 0 ↔ ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
326 oveq2 6623 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = (𝑁 − 1) → (1...𝑗) = (1...(𝑁 − 1)))
327326imaeq2d 5435 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = (𝑁 − 1) → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...(𝑁 − 1))))
328327xpeq1d 5108 . . . . . . . . . . . . . . . . . . 19 (𝑗 = (𝑁 − 1) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑁 − 1))) × {1}))
329 oveq1 6622 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = (𝑁 − 1) → (𝑗 + 1) = ((𝑁 − 1) + 1))
330329oveq1d 6630 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = (𝑁 − 1) → ((𝑗 + 1)...𝑁) = (((𝑁 − 1) + 1)...𝑁))
331330imaeq2d 5435 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = (𝑁 − 1) → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ (((𝑁 − 1) + 1)...𝑁)))
332331xpeq1d 5108 . . . . . . . . . . . . . . . . . . 19 (𝑗 = (𝑁 − 1) → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))
333328, 332uneq12d 3752 . . . . . . . . . . . . . . . . . 18 (𝑗 = (𝑁 − 1) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0})))
334333fveq1d 6160 . . . . . . . . . . . . . . . . 17 (𝑗 = (𝑁 − 1) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁))
335334neeq1d 2849 . . . . . . . . . . . . . . . 16 (𝑗 = (𝑁 − 1) → (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ≠ 0 ↔ ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) ≠ 0))
336325, 335syl5bbr 274 . . . . . . . . . . . . . . 15 (𝑗 = (𝑁 − 1) → (¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0 ↔ ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) ≠ 0))
337336rspcev 3299 . . . . . . . . . . . . . 14 (((𝑁 − 1) ∈ (0...(𝑁 − 1)) ∧ ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) ≠ 0) → ∃𝑗 ∈ (0...(𝑁 − 1)) ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
338269, 324, 337syl2anc 692 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑈𝑁) ≠ 𝑁) → ∃𝑗 ∈ (0...(𝑁 − 1)) ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
339338ex 450 . . . . . . . . . . . 12 (𝜑 → ((𝑈𝑁) ≠ 𝑁 → ∃𝑗 ∈ (0...(𝑁 − 1)) ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))
340 rexnal 2991 . . . . . . . . . . . 12 (∃𝑗 ∈ (0...(𝑁 − 1)) ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0 ↔ ¬ ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
341339, 340syl6ib 241 . . . . . . . . . . 11 (𝜑 → ((𝑈𝑁) ≠ 𝑁 → ¬ ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))
342341necon4ad 2809 . . . . . . . . . 10 (𝜑 → (∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0 → (𝑈𝑁) = 𝑁))
343268, 342impbid 202 . . . . . . . . 9 (𝜑 → ((𝑈𝑁) = 𝑁 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))
344226, 343anbi12d 746 . . . . . . . 8 (𝜑 → (((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁) ↔ (∀𝑗 ∈ (0...(𝑁 − 1))(𝑇𝑁) = 0 ∧ ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
345 r19.26 3059 . . . . . . . 8 (∀𝑗 ∈ (0...(𝑁 − 1))((𝑇𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0) ↔ (∀𝑗 ∈ (0...(𝑁 − 1))(𝑇𝑁) = 0 ∧ ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))
346344, 345syl6bbr 278 . . . . . . 7 (𝜑 → (((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁) ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((𝑇𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
347346adantr 481 . . . . . 6 ((𝜑𝑉 = 𝑁) → (((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁) ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((𝑇𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
348193, 223, 3473bitr4d 300 . . . . 5 ((𝜑𝑉 = 𝑁) → (∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁)))
349348pm5.32da 672 . . . 4 (𝜑 → ((𝑉 = 𝑁 ∧ ∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0) ↔ (𝑉 = 𝑁 ∧ ((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁))))
350110, 349bitrd 268 . . 3 (𝜑 → (∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ (𝑉 = 𝑁 ∧ ((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁))))
351350notbid 308 . 2 (𝜑 → (¬ ∀𝑦 ∈ (0...(𝑁 − 1))(if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ¬ (𝑉 = 𝑁 ∧ ((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁))))
35212, 351syl5bb 272 1 (𝜑 → (∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗(𝑇𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝𝑁) ≠ 0 ↔ ¬ (𝑉 = 𝑁 ∧ ((𝑇𝑁) = 0 ∧ (𝑈𝑁) = 𝑁))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 383   ∧ wa 384   = wceq 1480   ∈ wcel 1987   ≠ wne 2790  ∀wral 2908  ∃wrex 2909  Vcvv 3190  ⦋csb 3519   ∖ cdif 3557   ∪ cun 3558   ∩ cin 3559   ⊆ wss 3560  ∅c0 3897  ifcif 4064  {csn 4155   class class class wbr 4623   ↦ cmpt 4683   × cxp 5082  ◡ccnv 5083  ran crn 5085   “ cima 5087  Fun wfun 5851   Fn wfn 5852  ⟶wf 5853  –onto→wfo 5855  –1-1-onto→wf1o 5856  ‘cfv 5857  (class class class)co 6615   ∘𝑓 cof 6860  ℂcc 9894  ℝcr 9895  0cc0 9896  1c1 9897   + caddc 9899   < clt 10034   ≤ cle 10035   − cmin 10226  ℕcn 10980  ℕ0cn0 11252  ℤcz 11337  ℤ≥cuz 11647  ...cfz 12284  ..^cfzo 12422 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4741  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914  ax-cnex 9952  ax-resscn 9953  ax-1cn 9954  ax-icn 9955  ax-addcl 9956  ax-addrcl 9957  ax-mulcl 9958  ax-mulrcl 9959  ax-mulcom 9960  ax-addass 9961  ax-mulass 9962  ax-distr 9963  ax-i2m1 9964  ax-1ne0 9965  ax-1rid 9966  ax-rnegex 9967  ax-rrecex 9968  ax-cnre 9969  ax-pre-lttri 9970  ax-pre-lttrn 9971  ax-pre-ltadd 9972  ax-pre-mulgt0 9973 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2913  df-rex 2914  df-reu 2915  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-uni 4410  df-iun 4494  df-br 4624  df-opab 4684  df-mpt 4685  df-tr 4723  df-eprel 4995  df-id 4999  df-po 5005  df-so 5006  df-fr 5043  df-we 5045  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-pred 5649  df-ord 5695  df-on 5696  df-lim 5697  df-suc 5698  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864  df-fv 5865  df-riota 6576  df-ov 6618  df-oprab 6619  df-mpt2 6620  df-of 6862  df-om 7028  df-1st 7128  df-2nd 7129  df-wrecs 7367  df-recs 7428  df-rdg 7466  df-er 7702  df-en 7916  df-dom 7917  df-sdom 7918  df-pnf 10036  df-mnf 10037  df-xr 10038  df-ltxr 10039  df-le 10040  df-sub 10228  df-neg 10229  df-nn 10981  df-n0 11253  df-z 11338  df-uz 11648  df-fz 12285  df-fzo 12423 This theorem is referenced by:  poimirlem24  33104
 Copyright terms: Public domain W3C validator